From 6db835db88c4bcf0e00ce1a7a6bc396382b393c3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 11 Nov 2022 21:34:29 +0100
Subject: Reorganize the project to prepare for new backends

---
 compiler/Config.ml           |    5 +-
 compiler/ExtractToBackend.ml | 1639 ++++++++++++++++++++++++++++++++++++++++++
 compiler/ExtractToFStar.ml   | 1639 ------------------------------------------
 compiler/Pure.ml             |    2 +-
 compiler/PureMicroPasses.ml  |    2 +-
 compiler/PureUtils.ml        |    2 +-
 compiler/Translate.ml        |   46 +-
 compiler/dune                |    2 +-
 8 files changed, 1669 insertions(+), 1668 deletions(-)
 create mode 100644 compiler/ExtractToBackend.ml
 delete mode 100644 compiler/ExtractToFStar.ml

(limited to 'compiler')

diff --git a/compiler/Config.ml b/compiler/Config.ml
index 1f91645b..c9723bd4 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -66,11 +66,12 @@ let use_state = ref true (* TODO *)
        (st1, y)  <-- f_fwd x st0;
        ...
        x' <-- f_back x st0 y';
-    }]
+    ]}
 
     The second format is easier to reason about, but the first one is
     necessary to properly handle some Rust functions which use internal
-    mutability such as {{:https://doc.rust-lang.org/std/cell/struct.RefCell.html#method.try_borrow_mut} [RefCell::try_mut_borrow]}:
+    mutability such as
+    {{:https://doc.rust-lang.org/std/cell/struct.RefCell.html#method.try_borrow_mut}[RefCell::try_mut_borrow]}:
     in order to model this behaviour we would need a state, and calling the backward
     function would update the state by reinserting the updated value in it.
  *)
diff --git a/compiler/ExtractToBackend.ml b/compiler/ExtractToBackend.ml
new file mode 100644
index 00000000..fc04ce90
--- /dev/null
+++ b/compiler/ExtractToBackend.ml
@@ -0,0 +1,1639 @@
+(** Extract to F* *)
+
+open Utils
+open Pure
+open PureUtils
+open TranslateCore
+open PureToExtract
+open StringUtils
+module F = Format
+
+(** A qualifier for a type definition.
+
+    Controls whether we should use [type ...] or [and ...] (for mutually
+    recursive datatypes).
+ *)
+type type_decl_qualif =
+  | Type  (** [type t = ...] *)
+  | And  (** [type t0 = ... and t1 = ...] *)
+  | AssumeType  (** [assume type t] *)
+  | TypeVal  (** In an fsti: [val t : Type0] *)
+
+(** A qualifier for function definitions.
+
+    Controls whether we should use [let ...], [let rec ...] or [and ...],
+    or only generate a declaration with [val] or [assume val]
+ *)
+type fun_decl_qualif = Let | LetRec | And | Val | AssumeVal
+
+let fun_decl_qualif_keyword (qualif : fun_decl_qualif) : string =
+  match qualif with
+  | Let -> "let"
+  | LetRec -> "let rec"
+  | And -> "and"
+  | Val -> "val"
+  | AssumeVal -> "assume val"
+
+(** Small helper to compute the name of an int type *)
+let fstar_int_name (int_ty : integer_type) =
+  match int_ty with
+  | Isize -> "isize"
+  | I8 -> "i8"
+  | I16 -> "i16"
+  | I32 -> "i32"
+  | I64 -> "i64"
+  | I128 -> "i128"
+  | Usize -> "usize"
+  | U8 -> "u8"
+  | U16 -> "u16"
+  | U32 -> "u32"
+  | U64 -> "u64"
+  | U128 -> "u128"
+
+(** Small helper to compute the name of a unary operation *)
+let fstar_unop_name (unop : unop) : string =
+  match unop with
+  | Not -> "not"
+  | Neg int_ty -> fstar_int_name int_ty ^ "_neg"
+  | Cast _ -> raise (Failure "Unsupported")
+
+(** Small helper to compute the name of a binary operation (note that many
+    binary operations like "less than" are extracted to primitive operations,
+    like [<].
+ *)
+let fstar_named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
+  let binop =
+    match binop with
+    | Div -> "div"
+    | Rem -> "rem"
+    | Add -> "add"
+    | Sub -> "sub"
+    | Mul -> "mul"
+    | _ -> raise (Failure "Unreachable")
+  in
+  fstar_int_name int_ty ^ "_" ^ binop
+
+(** A list of keywords/identifiers used in F* and with which we want to check
+    collision. *)
+let fstar_keywords =
+  let named_unops =
+    fstar_unop_name Not
+    :: List.map (fun it -> fstar_unop_name (Neg it)) T.all_signed_int_types
+  in
+  let named_binops = [ E.Div; Rem; Add; Sub; Mul ] in
+  let named_binops =
+    List.concat
+      (List.map
+         (fun bn ->
+           List.map (fun it -> fstar_named_binop_name bn it) T.all_int_types)
+         named_binops)
+  in
+  let misc =
+    [
+      "let";
+      "rec";
+      "in";
+      "fn";
+      "val";
+      "int";
+      "nat";
+      "list";
+      "FStar";
+      "FStar.Mul";
+      "type";
+      "match";
+      "with";
+      "assert";
+      "assert_norm";
+      "assume";
+      "Type0";
+      "Type";
+      "unit";
+      "not";
+      "scalar_cast";
+    ]
+  in
+  List.concat [ named_unops; named_binops; misc ]
+
+let fstar_assumed_adts : (assumed_ty * string) list =
+  [ (State, "state"); (Result, "result"); (Option, "option"); (Vec, "vec") ]
+
+let fstar_assumed_structs : (assumed_ty * string) list = []
+
+let fstar_assumed_variants : (assumed_ty * VariantId.id * string) list =
+  [
+    (Result, result_return_id, "Return");
+    (Result, result_fail_id, "Fail");
+    (Option, option_some_id, "Some");
+    (Option, option_none_id, "None");
+  ]
+
+let fstar_assumed_llbc_functions :
+    (A.assumed_fun_id * T.RegionGroupId.id option * string) list =
+  let rg0 = Some T.RegionGroupId.zero in
+  [
+    (Replace, None, "mem_replace_fwd");
+    (Replace, rg0, "mem_replace_back");
+    (VecNew, None, "vec_new");
+    (VecPush, None, "vec_push_fwd") (* Shouldn't be used *);
+    (VecPush, rg0, "vec_push_back");
+    (VecInsert, None, "vec_insert_fwd") (* Shouldn't be used *);
+    (VecInsert, rg0, "vec_insert_back");
+    (VecLen, None, "vec_len");
+    (VecIndex, None, "vec_index_fwd");
+    (VecIndex, rg0, "vec_index_back") (* shouldn't be used *);
+    (VecIndexMut, None, "vec_index_mut_fwd");
+    (VecIndexMut, rg0, "vec_index_mut_back");
+  ]
+
+let fstar_assumed_pure_functions : (pure_assumed_fun_id * string) list =
+  [ (Return, "return"); (Fail, "fail"); (Assert, "massert") ]
+
+let fstar_names_map_init : names_map_init =
+  {
+    keywords = fstar_keywords;
+    assumed_adts = fstar_assumed_adts;
+    assumed_structs = fstar_assumed_structs;
+    assumed_variants = fstar_assumed_variants;
+    assumed_llbc_functions = fstar_assumed_llbc_functions;
+    assumed_pure_functions = fstar_assumed_pure_functions;
+  }
+
+let fstar_extract_unop (extract_expr : bool -> texpression -> unit)
+    (fmt : F.formatter) (inside : bool) (unop : unop) (arg : texpression) : unit
+    =
+  match unop with
+  | Not | Neg _ ->
+      let unop = fstar_unop_name unop in
+      if inside then F.pp_print_string fmt "(";
+      F.pp_print_string fmt unop;
+      F.pp_print_space fmt ();
+      extract_expr true arg;
+      if inside then F.pp_print_string fmt ")"
+  | Cast (src, tgt) ->
+      (* The source type is an implicit parameter *)
+      if inside then F.pp_print_string fmt "(";
+      F.pp_print_string fmt "scalar_cast";
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt
+        (StringUtils.capitalize_first_letter
+           (PrintPure.integer_type_to_string src));
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt
+        (StringUtils.capitalize_first_letter
+           (PrintPure.integer_type_to_string tgt));
+      F.pp_print_space fmt ();
+      extract_expr true arg;
+      if inside then F.pp_print_string fmt ")"
+
+let fstar_extract_binop (extract_expr : bool -> texpression -> unit)
+    (fmt : F.formatter) (inside : bool) (binop : E.binop)
+    (int_ty : integer_type) (arg0 : texpression) (arg1 : texpression) : unit =
+  if inside then F.pp_print_string fmt "(";
+  (* Some binary operations have a special treatment *)
+  (match binop with
+  | Eq | Lt | Le | Ne | Ge | Gt ->
+      let binop =
+        match binop with
+        | Eq -> "="
+        | Lt -> "<"
+        | Le -> "<="
+        | Ne -> "<>"
+        | Ge -> ">="
+        | Gt -> ">"
+        | _ -> raise (Failure "Unreachable")
+      in
+      extract_expr false arg0;
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt binop;
+      F.pp_print_space fmt ();
+      extract_expr false arg1
+  | Div | Rem | Add | Sub | Mul ->
+      let binop = fstar_named_binop_name binop int_ty in
+      F.pp_print_string fmt binop;
+      F.pp_print_space fmt ();
+      extract_expr false arg0;
+      F.pp_print_space fmt ();
+      extract_expr false arg1
+  | BitXor | BitAnd | BitOr | Shl | Shr -> raise Unimplemented);
+  if inside then F.pp_print_string fmt ")"
+
+(**
+   [ctx]: we use the context to lookup type definitions, to retrieve type names.
+   This is used to compute variable names, when they have no basenames: in this
+   case we use the first letter of the type name.
+  
+   [variant_concatenate_type_name]: if true, add the type name as a prefix
+   to the variant names.
+   Ex.:
+   In Rust:
+     {[
+       enum List = {
+         Cons(u32, Box<List>),x
+         Nil,
+       }
+     ]}
+  
+   F*, if option activated:
+     {[
+       type list =
+       | ListCons : u32 -> list -> list
+       | ListNil : list
+     ]}
+  
+   F*, if option not activated:
+     {[
+       type list =
+       | Cons : u32 -> list -> list
+       | Nil : list
+     ]}
+  
+   Rk.: this should be true by default, because in Rust all the variant names
+   are actively uniquely identifier by the type name [List::Cons(...)], while
+   in other languages it is not necessarily the case, and thus clashes can mess
+   up type checking. Note that some languages actually forbids the name clashes
+   (it is the case of F* ).
+ *)
+let mk_formatter (ctx : trans_ctx) (crate_name : string)
+    (variant_concatenate_type_name : bool) : formatter =
+  let int_name = fstar_int_name in
+
+  (* Prepare a name.
+   * The first id elem is always the crate: if it is the local crate,
+   * we remove it.
+   * We also remove all the disambiguators, then convert everything to strings.
+   * **Rmk:** because we remove the disambiguators, there may be name collisions
+   * (which is ok, because we check for name collisions and fail if there is any).
+   *)
+  let get_name (name : name) : string list =
+    (* Rmk.: initially we only filtered the disambiguators equal to 0 *)
+    let name = Names.filter_disambiguators name in
+    match name with
+    | Ident crate :: name ->
+        let name = if crate = crate_name then name else Ident crate :: name in
+        let name =
+          List.map
+            (function
+              | Names.Ident s -> s
+              | Disambiguator d -> Names.Disambiguator.to_string d)
+            name
+        in
+        name
+    | _ ->
+        raise (Failure ("Unexpected name shape: " ^ Print.name_to_string name))
+  in
+  let get_type_name = get_name in
+  let type_name_to_camel_case name =
+    let name = get_type_name name in
+    let name = List.map to_camel_case name in
+    String.concat "" name
+  in
+  let type_name_to_snake_case name =
+    let name = get_type_name name in
+    let name = List.map to_snake_case name in
+    String.concat "_" name
+  in
+  let type_name name = type_name_to_snake_case name ^ "_t" in
+  let field_name (def_name : name) (field_id : FieldId.id)
+      (field_name : string option) : string =
+    let def_name = type_name_to_snake_case def_name ^ "_" in
+    match field_name with
+    | Some field_name -> def_name ^ field_name
+    | None -> def_name ^ FieldId.to_string field_id
+  in
+  let variant_name (def_name : name) (variant : string) : string =
+    let variant = to_camel_case variant in
+    if variant_concatenate_type_name then
+      type_name_to_camel_case def_name ^ variant
+    else variant
+  in
+  let struct_constructor (basename : name) : string =
+    let tname = type_name basename in
+    "Mk" ^ tname
+  in
+  let get_fun_name = get_name in
+  let fun_name_to_snake_case (fname : fun_name) : string =
+    let fname = get_fun_name fname in
+    (* Converting to snake case should be a no-op, but it doesn't cost much *)
+    let fname = List.map to_snake_case fname in
+    (* Concatenate the elements *)
+    String.concat "_" fname
+  in
+  let global_name (name : global_name) : string =
+    (* Converting to snake case also lowercases the letters (in Rust, global
+     * names are written in capital letters). *)
+    let parts = List.map to_snake_case (get_name name) in
+    String.concat "_" parts
+  in
+  let fun_name (fname : fun_name) (num_rgs : int)
+      (rg : region_group_info option) (filter_info : bool * int) : string =
+    let fname = fun_name_to_snake_case fname in
+    (* Compute the suffix *)
+    let suffix = default_fun_suffix num_rgs rg filter_info in
+    (* Concatenate *)
+    fname ^ suffix
+  in
+
+  let decreases_clause_name (_fid : A.FunDeclId.id) (fname : fun_name) : string
+      =
+    let fname = fun_name_to_snake_case fname in
+    (* Compute the suffix *)
+    let suffix = "_decreases" in
+    (* Concatenate *)
+    fname ^ suffix
+  in
+
+  let var_basename (_varset : StringSet.t) (basename : string option) (ty : ty)
+      : string =
+    (* If there is a basename, we use it *)
+    match basename with
+    | Some basename ->
+        (* This should be a no-op *)
+        to_snake_case basename
+    | None -> (
+        (* No basename: we use the first letter of the type *)
+        match ty with
+        | Adt (type_id, tys) -> (
+            match type_id with
+            | Tuple ->
+                (* The "pair" case is frequent enough to have its special treatment *)
+                if List.length tys = 2 then "p" else "t"
+            | Assumed Result -> "r"
+            | Assumed Option -> "opt"
+            | Assumed Vec -> "v"
+            | Assumed State -> "st"
+            | AdtId adt_id ->
+                let def =
+                  TypeDeclId.Map.find adt_id ctx.type_context.type_decls
+                in
+                (* We do the following:
+                 * - compute the type name, and retrieve the last ident
+                 * - convert this to snake case
+                 * - take the first letter of every "letter group"
+                 * Ex.: ["hashmap"; "HashMap"] ~~> "HashMap" -> "hash_map" -> "hm"
+                 *)
+                (* Thename shouldn't be empty, and its last element should
+                 * be an ident *)
+                let cl = List.nth def.name (List.length def.name - 1) in
+                let cl = to_snake_case (Names.as_ident cl) in
+                let cl = String.split_on_char '_' cl in
+                let cl = List.filter (fun s -> String.length s > 0) cl in
+                assert (List.length cl > 0);
+                let cl = List.map (fun s -> s.[0]) cl in
+                StringUtils.string_of_chars cl)
+        | TypeVar _ -> "x" (* lacking imagination here... *)
+        | Bool -> "b"
+        | Char -> "c"
+        | Integer _ -> "i"
+        | Str -> "s"
+        | Arrow _ -> "f"
+        | Array _ | Slice _ -> raise Unimplemented)
+  in
+  let type_var_basename (_varset : StringSet.t) (basename : string) : string =
+    (* This is *not* a no-op: type variables in Rust often start with
+     * a capital letter *)
+    to_snake_case basename
+  in
+  let append_index (basename : string) (i : int) : string =
+    basename ^ string_of_int i
+  in
+
+  let extract_primitive_value (fmt : F.formatter) (_inside : bool)
+      (cv : primitive_value) : unit =
+    match cv with
+    | Scalar sv -> F.pp_print_string fmt (Z.to_string sv.PV.value)
+    | Bool b ->
+        let b = if b then "true" else "false" in
+        F.pp_print_string fmt b
+    | Char c -> F.pp_print_string fmt ("'" ^ String.make 1 c ^ "'")
+    | String s ->
+        (* We need to replace all the line breaks *)
+        let s =
+          StringUtils.map
+            (fun c -> if c = '\n' then "\n" else String.make 1 c)
+            s
+        in
+        F.pp_print_string fmt ("\"" ^ s ^ "\"")
+  in
+  {
+    bool_name = "bool";
+    char_name = "char";
+    int_name;
+    str_name = "string";
+    field_name;
+    variant_name;
+    struct_constructor;
+    type_name;
+    global_name;
+    fun_name;
+    decreases_clause_name;
+    var_basename;
+    type_var_basename;
+    append_index;
+    extract_primitive_value;
+    extract_unop = fstar_extract_unop;
+    extract_binop = fstar_extract_binop;
+  }
+
+(** [inside] constrols whether we should add parentheses or not around type
+    applications (if [true] we add parentheses).
+ *)
+let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
+    (ty : ty) : unit =
+  match ty with
+  | Adt (type_id, tys) -> (
+      match type_id with
+      | Tuple ->
+          (* This is a bit annoying, but in F* [()] is not the unit type:
+           * we have to write [unit]... *)
+          if tys = [] then F.pp_print_string fmt "unit"
+          else (
+            F.pp_print_string fmt "(";
+            Collections.List.iter_link
+              (fun () ->
+                F.pp_print_space fmt ();
+                F.pp_print_string fmt "&";
+                F.pp_print_space fmt ())
+              (extract_ty ctx fmt true) tys;
+            F.pp_print_string fmt ")")
+      | AdtId _ | Assumed _ ->
+          let print_paren = inside && tys <> [] in
+          if print_paren then F.pp_print_string fmt "(";
+          F.pp_print_string fmt (ctx_get_type type_id ctx);
+          if tys <> [] then F.pp_print_space fmt ();
+          Collections.List.iter_link (F.pp_print_space fmt)
+            (extract_ty ctx fmt true) tys;
+          if print_paren then F.pp_print_string fmt ")")
+  | TypeVar vid -> F.pp_print_string fmt (ctx_get_type_var vid ctx)
+  | Bool -> F.pp_print_string fmt ctx.fmt.bool_name
+  | Char -> F.pp_print_string fmt ctx.fmt.char_name
+  | Integer int_ty -> F.pp_print_string fmt (ctx.fmt.int_name int_ty)
+  | Str -> F.pp_print_string fmt ctx.fmt.str_name
+  | Arrow (arg_ty, ret_ty) ->
+      if inside then F.pp_print_string fmt "(";
+      extract_ty ctx fmt false arg_ty;
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt "->";
+      F.pp_print_space fmt ();
+      extract_ty ctx fmt false ret_ty;
+      if inside then F.pp_print_string fmt ")"
+  | Array _ | Slice _ -> raise Unimplemented
+
+(** Compute the names for all the top-level identifiers used in a type
+    definition (type name, variant names, field names, etc. but not type
+    parameters).
+    
+    We need to do this preemptively, beforce extracting any definition,
+    because of recursive definitions.
+ *)
+let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
+    extraction_ctx =
+  (* Compute and register the type def name *)
+  let ctx = ctx_add_type_decl def ctx in
+  (* Compute and register:
+   * - the variant names, if this is an enumeration
+   * - the field names, if this is a structure
+   *)
+  let ctx =
+    match def.kind with
+    | Struct fields ->
+        (* Add the fields *)
+        let ctx =
+          fst
+            (ctx_add_fields def (FieldId.mapi (fun id f -> (id, f)) fields) ctx)
+        in
+        (* Add the constructor name *)
+        fst (ctx_add_struct def ctx)
+    | Enum variants ->
+        fst
+          (ctx_add_variants def
+             (VariantId.mapi (fun id v -> (id, v)) variants)
+             ctx)
+    | Opaque ->
+        (* Nothing to do *)
+        ctx
+  in
+  (* Return *)
+  ctx
+
+let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
+    (def : type_decl) (fields : field list) : unit =
+  (* We want to generate a definition which looks like this:
+     {[
+       type t = { x : int; y : bool; }
+     ]}
+
+     If there isn't enough space on one line:
+     {[
+       type t =
+       {
+         x : int; y : bool;
+       }
+     ]}
+
+     And if there is even less space:
+     {[
+       type t =
+       {
+         x : int;
+         y : bool;
+       }
+     ]}
+
+     Also, in case there are no fields, we need to define the type as [unit]
+     ([type t = {}] doesn't work in F* ).
+  *)
+  (* Note that we already printed: [type t =] *)
+  if fields = [] then (
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt "unit")
+  else (
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt "{";
+    F.pp_print_break fmt 1 ctx.indent_incr;
+    (* The body itself *)
+    F.pp_open_hvbox fmt 0;
+    (* Print the fields *)
+    let print_field (field_id : FieldId.id) (f : field) : unit =
+      let field_name = ctx_get_field (AdtId def.def_id) field_id ctx in
+      F.pp_open_box fmt ctx.indent_incr;
+      F.pp_print_string fmt field_name;
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt ":";
+      F.pp_print_space fmt ();
+      extract_ty ctx fmt false f.field_ty;
+      F.pp_print_string fmt ";";
+      F.pp_close_box fmt ()
+    in
+    let fields = FieldId.mapi (fun fid f -> (fid, f)) fields in
+    Collections.List.iter_link (F.pp_print_space fmt)
+      (fun (fid, f) -> print_field fid f)
+      fields;
+    (* Close *)
+    F.pp_close_box fmt ();
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt "}")
+
+let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
+    (def : type_decl) (def_name : string) (type_params : string list)
+    (variants : variant list) : unit =
+  (* We want to generate a definition which looks like this:
+     {[
+       type list a = | Cons : a -> list a -> list a | Nil : list a
+     ]}
+
+     If there isn't enough space on one line:
+     {[
+       type s =
+       | Cons : a -> list a -> list a
+       | Nil : list a
+     ]}
+
+     And if we need to write the type of a variant on several lines:
+     {[
+       type s =
+       | Cons :
+         a ->
+         list a ->
+         list a
+       | Nil : list a
+     ]}
+
+     Finally, it is possible to give names to the variant fields in Rust.
+     In this situation, we generate a definition like this:
+     {[
+       type s =
+       | Cons : hd:a -> tl:list a -> list a
+       | Nil : list a
+     ]}
+
+     Note that we already printed: [type s =]
+  *)
+  (* Print the variants *)
+  let print_variant (variant_id : VariantId.id) (variant : variant) : unit =
+    let variant_name = ctx_get_variant (AdtId def.def_id) variant_id ctx in
+    F.pp_print_space fmt ();
+    F.pp_open_hvbox fmt ctx.indent_incr;
+    (* variant box *)
+    (* [| Cons :]
+     * Note that we really don't want any break above so we print everything
+     * at once. *)
+    F.pp_print_string fmt ("| " ^ variant_name ^ " :");
+    F.pp_print_space fmt ();
+    let print_field (fid : FieldId.id) (f : field) (ctx : extraction_ctx) :
+        extraction_ctx =
+      (* Open the field box *)
+      F.pp_open_box fmt ctx.indent_incr;
+      (* Print the field names
+       * [  x :]
+       * Note that when printing fields, we register the field names as
+       * *variables*: they don't need to be unique at the top level. *)
+      let ctx =
+        match f.field_name with
+        | None -> ctx
+        | Some field_name ->
+            let var_id = VarId.of_int (FieldId.to_int fid) in
+            let field_name =
+              ctx.fmt.var_basename ctx.names_map.names_set (Some field_name)
+                f.field_ty
+            in
+            let ctx, field_name = ctx_add_var field_name var_id ctx in
+            F.pp_print_string fmt (field_name ^ " :");
+            F.pp_print_space fmt ();
+            ctx
+      in
+      (* Print the field type *)
+      extract_ty ctx fmt false f.field_ty;
+      (* Print the arrow [->]*)
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt "->";
+      (* Close the field box *)
+      F.pp_close_box fmt ();
+      F.pp_print_space fmt ();
+      (* Return *)
+      ctx
+    in
+    (* Print the fields *)
+    let fields = FieldId.mapi (fun fid f -> (fid, f)) variant.fields in
+    let _ =
+      List.fold_left (fun ctx (fid, f) -> print_field fid f ctx) ctx fields
+    in
+    (* Print the final type *)
+    F.pp_open_hovbox fmt 0;
+    F.pp_print_string fmt def_name;
+    List.iter
+      (fun type_param ->
+        F.pp_print_space fmt ();
+        F.pp_print_string fmt type_param)
+      type_params;
+    F.pp_close_box fmt ();
+    (* Close the variant box *)
+    F.pp_close_box fmt ()
+  in
+  (* Print the variants *)
+  let variants = VariantId.mapi (fun vid v -> (vid, v)) variants in
+  List.iter (fun (vid, v) -> print_variant vid v) variants
+
+(** Extract a type declaration.
+
+    Note that all the names used for extraction should already have been
+    registered.
+ *)
+let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
+    (qualif : type_decl_qualif) (def : type_decl) : unit =
+  (* Retrieve the definition name *)
+  let def_name = ctx_get_local_type def.def_id ctx in
+  (* Add the type params - note that we need those bindings only for the
+   * body translation (they are not top-level) *)
+  let ctx_body, type_params = ctx_add_type_params def.type_params ctx in
+  (* Add a break before *)
+  F.pp_print_break fmt 0 0;
+  (* Print a comment to link the extracted type to its original rust definition *)
+  F.pp_print_string fmt ("(** [" ^ Print.name_to_string def.name ^ "] *)");
+  F.pp_print_space fmt ();
+  (* Open a box for the definition, so that whenever possible it gets printed on
+   * one line *)
+  F.pp_open_hvbox fmt 0;
+  (* Open a box for "type TYPE_NAME (TYPE_PARAMS) =" *)
+  F.pp_open_hovbox fmt ctx.indent_incr;
+  (* > "type TYPE_NAME" *)
+  let extract_body, qualif =
+    match qualif with
+    | Type -> (true, "type")
+    | And -> (true, "and")
+    | AssumeType -> (false, "assume type")
+    | TypeVal -> (false, "val")
+  in
+  F.pp_print_string fmt (qualif ^ " " ^ def_name);
+  (* Print the type parameters *)
+  if def.type_params <> [] then (
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt "(";
+    List.iter
+      (fun (p : type_var) ->
+        let pname = ctx_get_type_var p.index ctx_body in
+        F.pp_print_string fmt pname;
+        F.pp_print_space fmt ())
+      def.type_params;
+    F.pp_print_string fmt ":";
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt "Type0)");
+  (* Print the "=" if we extract the body*)
+  if extract_body then (
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt "=")
+  else (
+    (* Otherwise print ": Type0" *)
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt ":";
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt "Type0");
+  (* Close the box for "type TYPE_NAME (TYPE_PARAMS) =" *)
+  F.pp_close_box fmt ();
+  (if extract_body then
+   match def.kind with
+   | Struct fields -> extract_type_decl_struct_body ctx_body fmt def fields
+   | Enum variants ->
+       extract_type_decl_enum_body ctx_body fmt def def_name type_params
+         variants
+   | Opaque -> raise (Failure "Unreachable"));
+  (* Close the box for the definition *)
+  F.pp_close_box fmt ();
+  (* Add breaks to insert new lines between definitions *)
+  F.pp_print_break fmt 0 0
+
+(** Extract the state type declaration. *)
+let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
+    (qualif : type_decl_qualif) : unit =
+  (* Add a break before *)
+  F.pp_print_break fmt 0 0;
+  (* Print a comment  *)
+  F.pp_print_string fmt "(** The state type used in the state-error monad *)";
+  F.pp_print_space fmt ();
+  (* Open a box for the definition, so that whenever possible it gets printed on
+   * one line *)
+  F.pp_open_hvbox fmt 0;
+  (* Retrieve the name *)
+  let state_name = ctx_get_assumed_type State ctx in
+  (* The qualif should be [AssumeType] or [TypeVal] *)
+  (match qualif with
+  | Type | And -> raise (Failure "Unexpected")
+  | AssumeType ->
+      F.pp_print_string fmt "assume";
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt "type";
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt state_name;
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt ":";
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt "Type0"
+  | TypeVal ->
+      F.pp_print_string fmt "val";
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt state_name;
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt ":";
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt "Type0");
+  (* Close the box for the definition *)
+  F.pp_close_box fmt ();
+  (* Add breaks to insert new lines between definitions *)
+  F.pp_print_break fmt 0 0
+
+(** Compute the names for all the pure functions generated from a rust function
+    (forward function and backward functions).
+ *)
+let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool)
+    (has_decreases_clause : bool) (def : pure_fun_translation) : extraction_ctx
+    =
+  let fwd, back_ls = def in
+  (* Register the decrease clause, if necessary *)
+  let ctx =
+    if has_decreases_clause then ctx_add_decrases_clause fwd ctx else ctx
+  in
+  (* Register the forward function name *)
+  let ctx = ctx_add_fun_decl (keep_fwd, def) fwd ctx in
+  (* Register the backward functions' names *)
+  let ctx =
+    List.fold_left
+      (fun ctx back -> ctx_add_fun_decl (keep_fwd, def) back ctx)
+      ctx back_ls
+  in
+  (* Return *)
+  ctx
+
+(** Simply add the global name to the context. *)
+let extract_global_decl_register_names (ctx : extraction_ctx)
+    (def : A.global_decl) : extraction_ctx =
+  ctx_add_global_decl_and_body def ctx
+
+(** The following function factorizes the extraction of ADT values.
+
+    Note that patterns can introduce new variables: we thus return an extraction
+    context updated with new bindings.
+    
+    TODO: we don't need something very generic anymore
+ *)
+let extract_adt_g_value
+    (extract_value : extraction_ctx -> bool -> 'v -> extraction_ctx)
+    (fmt : F.formatter) (ctx : extraction_ctx) (inside : bool)
+    (variant_id : VariantId.id option) (field_values : 'v list) (ty : ty) :
+    extraction_ctx =
+  match ty with
+  | Adt (Tuple, _) ->
+      (* Tuple *)
+      F.pp_print_string fmt "(";
+      let ctx =
+        Collections.List.fold_left_link
+          (fun () ->
+            F.pp_print_string fmt ",";
+            F.pp_print_space fmt ())
+          (fun ctx v -> extract_value ctx false v)
+          ctx field_values
+      in
+      F.pp_print_string fmt ")";
+      ctx
+  | Adt (adt_id, _) ->
+      (* "Regular" ADT *)
+      (* We print something of the form: [Cons field0 ... fieldn].
+       * We could update the code to print something of the form:
+       * [{ field0=...; ...; fieldn=...; }] in case of structures.
+       *)
+      let cons =
+        match variant_id with
+        | Some vid -> ctx_get_variant adt_id vid ctx
+        | None -> ctx_get_struct adt_id ctx
+      in
+      if inside && field_values <> [] then F.pp_print_string fmt "(";
+      F.pp_print_string fmt cons;
+      let ctx =
+        Collections.List.fold_left
+          (fun ctx v ->
+            F.pp_print_space fmt ();
+            extract_value ctx true v)
+          ctx field_values
+      in
+      if inside && field_values <> [] then F.pp_print_string fmt ")";
+      ctx
+  | _ -> raise (Failure "Inconsistent typed value")
+
+(* Extract globals in the same way as variables *)
+let extract_global (ctx : extraction_ctx) (fmt : F.formatter)
+    (id : A.GlobalDeclId.id) : unit =
+  F.pp_print_string fmt (ctx_get_global id ctx)
+
+(** [inside]: see {!extract_ty}.
+
+    As a pattern can introduce new variables, we return an extraction context
+    updated with new bindings.
+ *)
+let rec extract_typed_pattern (ctx : extraction_ctx) (fmt : F.formatter)
+    (inside : bool) (v : typed_pattern) : extraction_ctx =
+  match v.value with
+  | PatConstant cv ->
+      ctx.fmt.extract_primitive_value fmt inside cv;
+      ctx
+  | PatVar (v, _) ->
+      let vname =
+        ctx.fmt.var_basename ctx.names_map.names_set v.basename v.ty
+      in
+      let ctx, vname = ctx_add_var vname v.id ctx in
+      F.pp_print_string fmt vname;
+      ctx
+  | PatDummy ->
+      F.pp_print_string fmt "_";
+      ctx
+  | PatAdt av ->
+      let extract_value ctx inside v = extract_typed_pattern ctx fmt inside v in
+      extract_adt_g_value extract_value fmt ctx inside av.variant_id
+        av.field_values v.ty
+
+(** [inside]: controls the introduction of parentheses. See [extract_ty]
+    
+    TODO: replace the formatting boolean [inside] with something more general?
+    Also, it seems we don't really use it...
+    Cases to consider:
+    - right-expression in a let: [let x = re in _] (never parentheses?)
+    - next expression in a let:  [let x = _ in next_e] (never parentheses?)
+    - application argument: [f (exp)]
+    - match/if scrutinee: [if exp then _ else _]/[match exp | _ -> _]
+ *)
+let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
+    (inside : bool) (e : texpression) : unit =
+  match e.e with
+  | Var var_id ->
+      let var_name = ctx_get_var var_id ctx in
+      F.pp_print_string fmt var_name
+  | Const cv -> ctx.fmt.extract_primitive_value fmt inside cv
+  | App _ ->
+      let app, args = destruct_apps e in
+      extract_App ctx fmt inside app args
+  | Abs _ ->
+      let xl, e = destruct_abs_list e in
+      extract_Abs ctx fmt inside xl e
+  | Qualif _ ->
+      (* We use the app case *)
+      extract_App ctx fmt inside e []
+  | Let (monadic, lv, re, next_e) ->
+      extract_Let ctx fmt inside monadic lv re next_e
+  | Switch (scrut, body) -> extract_Switch ctx fmt inside scrut body
+  | Meta (_, e) -> extract_texpression ctx fmt inside e
+
+(* Extract an application *or* a top-level qualif (function extraction has
+ * to handle top-level qualifiers, so it seemed more natural to merge the
+ * two cases) *)
+and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
+    (app : texpression) (args : texpression list) : unit =
+  (* We don't do the same thing if the app is a top-level identifier (function,
+   * ADT constructor...) or a "regular" expression *)
+  match app.e with
+  | Qualif qualif -> (
+      (* Top-level qualifier *)
+      match qualif.id with
+      | FunOrOp fun_id ->
+          extract_function_call ctx fmt inside fun_id qualif.type_args args
+      | Global global_id -> extract_global ctx fmt global_id
+      | AdtCons adt_cons_id ->
+          extract_adt_cons ctx fmt inside adt_cons_id qualif.type_args args
+      | Proj proj ->
+          extract_field_projector ctx fmt inside app proj qualif.type_args args)
+  | _ ->
+      (* "Regular" expression *)
+      (* Open parentheses *)
+      if inside then F.pp_print_string fmt "(";
+      (* Open a box for the application *)
+      F.pp_open_hovbox fmt ctx.indent_incr;
+      (* Print the app expression *)
+      let app_inside = (inside && args = []) || args <> [] in
+      extract_texpression ctx fmt app_inside app;
+      (* Print the arguments *)
+      List.iter
+        (fun ve ->
+          F.pp_print_space fmt ();
+          extract_texpression ctx fmt true ve)
+        args;
+      (* Close the box for the application *)
+      F.pp_close_box fmt ();
+      (* Close parentheses *)
+      if inside then F.pp_print_string fmt ")"
+
+(** Subcase of the app case: function call *)
+and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
+    (inside : bool) (fid : fun_or_op_id) (type_args : ty list)
+    (args : texpression list) : unit =
+  match (fid, args) with
+  | Unop unop, [ arg ] ->
+      (* A unop can have *at most* one argument (the result can't be a function!).
+       * Note that the way we generate the translation, we shouldn't get the
+       * case where we have no argument (all functions are fully instantiated,
+       * and no AST transformation introduces partial calls). *)
+      ctx.fmt.extract_unop (extract_texpression ctx fmt) fmt inside unop arg
+  | Binop (binop, int_ty), [ arg0; arg1 ] ->
+      (* Number of arguments: similar to unop *)
+      ctx.fmt.extract_binop
+        (extract_texpression ctx fmt)
+        fmt inside binop int_ty arg0 arg1
+  | Fun fun_id, _ ->
+      if inside then F.pp_print_string fmt "(";
+      (* Open a box for the function call *)
+      F.pp_open_hovbox fmt ctx.indent_incr;
+      (* Print the function name *)
+      let fun_name = ctx_get_function fun_id ctx in
+      F.pp_print_string fmt fun_name;
+      (* Print the type parameters *)
+      List.iter
+        (fun ty ->
+          F.pp_print_space fmt ();
+          extract_ty ctx fmt true ty)
+        type_args;
+      (* Print the arguments *)
+      List.iter
+        (fun ve ->
+          F.pp_print_space fmt ();
+          extract_texpression ctx fmt true ve)
+        args;
+      (* Close the box for the function call *)
+      F.pp_close_box fmt ();
+      (* Return *)
+      if inside then F.pp_print_string fmt ")"
+  | (Unop _ | Binop _), _ ->
+      raise
+        (Failure
+           ("Unreachable:\n" ^ "Function: " ^ show_fun_or_op_id fid
+          ^ ",\nNumber of arguments: "
+           ^ string_of_int (List.length args)
+           ^ ",\nArguments: "
+           ^ String.concat " " (List.map show_texpression args)))
+
+(** Subcase of the app case: ADT constructor *)
+and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
+    (adt_cons : adt_cons_id) (type_args : ty list) (args : texpression list) :
+    unit =
+  match adt_cons.adt_id with
+  | Tuple ->
+      (* Tuple *)
+      (* For now, we only support fully applied tuple constructors *)
+      assert (List.length type_args = List.length args);
+      F.pp_print_string fmt "(";
+      Collections.List.iter_link
+        (fun () ->
+          F.pp_print_string fmt ",";
+          F.pp_print_space fmt ())
+        (fun v -> extract_texpression ctx fmt false v)
+        args;
+      F.pp_print_string fmt ")"
+  | _ ->
+      (* "Regular" ADT *)
+      (* We print something of the form: [Cons field0 ... fieldn].
+       * We could update the code to print something of the form:
+       * [{ field0=...; ...; fieldn=...; }] in case of fully
+       * applied structure constructors.
+       *)
+      let cons =
+        match adt_cons.variant_id with
+        | Some vid -> ctx_get_variant adt_cons.adt_id vid ctx
+        | None -> ctx_get_struct adt_cons.adt_id ctx
+      in
+      let use_parentheses = inside && args <> [] in
+      if use_parentheses then F.pp_print_string fmt "(";
+      F.pp_print_string fmt cons;
+      Collections.List.iter
+        (fun v ->
+          F.pp_print_space fmt ();
+          extract_texpression ctx fmt true v)
+        args;
+      if use_parentheses then F.pp_print_string fmt ")"
+
+(** Subcase of the app case: ADT field projector.  *)
+and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter)
+    (inside : bool) (original_app : texpression) (proj : projection)
+    (_proj_type_params : ty list) (args : texpression list) : unit =
+  (* We isolate the first argument (if there is), in order to pretty print the
+   * projection ([x.field] instead of [MkAdt?.field x] *)
+  match args with
+  | [ arg ] ->
+      (* Exactly one argument: pretty-print *)
+      let field_name = ctx_get_field proj.adt_id proj.field_id ctx in
+      (* Open a box *)
+      F.pp_open_hovbox fmt ctx.indent_incr;
+      (* Extract the expression *)
+      extract_texpression ctx fmt true arg;
+      (* We allow to break where the "." appears *)
+      F.pp_print_break fmt 0 0;
+      F.pp_print_string fmt ".";
+      F.pp_print_string fmt field_name;
+      (* Close the box *)
+      F.pp_close_box fmt ()
+  | arg :: args ->
+      (* Call extract_App again, but in such a way that the first argument is
+       * isolated *)
+      extract_App ctx fmt inside (mk_app original_app arg) args
+  | [] ->
+      (* No argument: shouldn't happen *)
+      raise (Failure "Unreachable")
+
+and extract_Abs (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
+    (xl : typed_pattern list) (e : texpression) : unit =
+  (* Open a box for the abs expression *)
+  F.pp_open_hovbox fmt ctx.indent_incr;
+  (* Open parentheses *)
+  if inside then F.pp_print_string fmt "(";
+  (* Print the lambda - note that there should always be at least one variable *)
+  assert (xl <> []);
+  F.pp_print_string fmt "fun";
+  let ctx =
+    List.fold_left
+      (fun ctx x ->
+        F.pp_print_space fmt ();
+        extract_typed_pattern ctx fmt true x)
+      ctx xl
+  in
+  F.pp_print_space fmt ();
+  F.pp_print_string fmt "->";
+  F.pp_print_space fmt ();
+  (* Print the body *)
+  extract_texpression ctx fmt false e;
+  (* Close parentheses *)
+  if inside then F.pp_print_string fmt ")";
+  (* Close the box for the abs expression *)
+  F.pp_close_box fmt ()
+
+and extract_Let (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
+    (monadic : bool) (lv : typed_pattern) (re : texpression)
+    (next_e : texpression) : unit =
+  (* Open a box for the whole expression *)
+  F.pp_open_hvbox fmt 0;
+  (* Open parentheses *)
+  if inside then F.pp_print_string fmt "(";
+  (* Open a box for the let-binding *)
+  F.pp_open_hovbox fmt ctx.indent_incr;
+  let ctx =
+    if monadic then (
+      (* Note that in F*, the left value of a monadic let-binding can only be
+       * a variable *)
+      let ctx = extract_typed_pattern ctx fmt true lv in
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt "<--";
+      F.pp_print_space fmt ();
+      extract_texpression ctx fmt false re;
+      F.pp_print_string fmt ";";
+      ctx)
+    else (
+      F.pp_print_string fmt "let";
+      F.pp_print_space fmt ();
+      let ctx = extract_typed_pattern ctx fmt true lv in
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt "=";
+      F.pp_print_space fmt ();
+      extract_texpression ctx fmt false re;
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt "in";
+      ctx)
+  in
+  (* Close the box for the let-binding *)
+  F.pp_close_box fmt ();
+  (* Print the next expression *)
+  F.pp_print_space fmt ();
+  extract_texpression ctx fmt false next_e;
+  (* Close parentheses *)
+  if inside then F.pp_print_string fmt ")";
+  (* Close the box for the whole expression *)
+  F.pp_close_box fmt ()
+
+and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
+    (scrut : texpression) (body : switch_body) : unit =
+  (* Open a box for the whole expression *)
+  F.pp_open_hvbox fmt 0;
+  (* Open parentheses *)
+  if inside then F.pp_print_string fmt "(";
+  (* Extract the switch *)
+  (match body with
+  | If (e_then, e_else) ->
+      (* Open a box for the [if] *)
+      F.pp_open_hovbox fmt ctx.indent_incr;
+      F.pp_print_string fmt "if";
+      F.pp_print_space fmt ();
+      let scrut_inside = PureUtils.let_group_requires_parentheses scrut in
+      extract_texpression ctx fmt scrut_inside scrut;
+      (* Close the box for the [if] *)
+      F.pp_close_box fmt ();
+      (* Extract the branches *)
+      let extract_branch (is_then : bool) (e_branch : texpression) : unit =
+        F.pp_print_space fmt ();
+        (* Open a box for the then/else+branch *)
+        F.pp_open_hovbox fmt ctx.indent_incr;
+        let then_or_else = if is_then then "then" else "else" in
+        F.pp_print_string fmt then_or_else;
+        F.pp_print_space fmt ();
+        (* Open a box for the branch *)
+        F.pp_open_hovbox fmt ctx.indent_incr;
+        (* Print the [begin] if necessary *)
+        let parenth = PureUtils.let_group_requires_parentheses e_branch in
+        if parenth then (
+          F.pp_print_string fmt "begin";
+          F.pp_print_space fmt ());
+        (* Print the branch expression *)
+        extract_texpression ctx fmt false e_branch;
+        (* Close the [begin ... end ] *)
+        if parenth then (
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "end");
+        (* Close the box for the branch *)
+        F.pp_close_box fmt ();
+        (* Close the box for the then/else+branch *)
+        F.pp_close_box fmt ()
+      in
+
+      extract_branch true e_then;
+      extract_branch false e_else
+  | Match branches ->
+      (* Open a box for the [match ... with] *)
+      F.pp_open_hovbox fmt ctx.indent_incr;
+      (* Print the [match ... with] *)
+      F.pp_print_string fmt "begin match";
+      F.pp_print_space fmt ();
+      let scrut_inside = PureUtils.let_group_requires_parentheses scrut in
+      extract_texpression ctx fmt scrut_inside scrut;
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt "with";
+      (* Close the box for the [match ... with] *)
+      F.pp_close_box fmt ();
+
+      (* Extract the branches *)
+      let extract_branch (br : match_branch) : unit =
+        F.pp_print_space fmt ();
+        (* Open a box for the pattern+branch *)
+        F.pp_open_hovbox fmt ctx.indent_incr;
+        F.pp_print_string fmt "|";
+        (* Print the pattern *)
+        F.pp_print_space fmt ();
+        let ctx = extract_typed_pattern ctx fmt false br.pat in
+        F.pp_print_space fmt ();
+        F.pp_print_string fmt "->";
+        F.pp_print_space fmt ();
+        (* Open a box for the branch *)
+        F.pp_open_hovbox fmt ctx.indent_incr;
+        (* Print the branch itself *)
+        extract_texpression ctx fmt false br.branch;
+        (* Close the box for the branch *)
+        F.pp_close_box fmt ();
+        (* Close the box for the pattern+branch *)
+        F.pp_close_box fmt ()
+      in
+
+      List.iter extract_branch branches;
+
+      (* End the match *)
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt "end");
+  (* Close parentheses *)
+  if inside then F.pp_print_string fmt ")";
+  (* Close the box for the whole expression *)
+  F.pp_close_box fmt ()
+
+(** A small utility to print the parameters of a function signature.
+
+    We return two contexts:
+    - the context augmented with bindings for the type parameters
+    - the previous context augmented with bindings for the input values
+ *)
+let extract_fun_parameters (ctx : extraction_ctx) (fmt : F.formatter)
+    (def : fun_decl) : extraction_ctx * extraction_ctx =
+  (* Add the type parameters - note that we need those bindings only for the
+   * body translation (they are not top-level) *)
+  let ctx, _ = ctx_add_type_params def.signature.type_params ctx in
+  (* Print the parameters - rk.: we should have filtered the functions
+   * with no input parameters *)
+  (* The type parameters *)
+  if def.signature.type_params <> [] then (
+    (* Open a box for the type parameters *)
+    F.pp_open_hovbox fmt 0;
+    F.pp_print_string fmt "(";
+    List.iter
+      (fun (p : type_var) ->
+        let pname = ctx_get_type_var p.index ctx in
+        F.pp_print_string fmt pname;
+        F.pp_print_space fmt ())
+      def.signature.type_params;
+    F.pp_print_string fmt ":";
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt "Type0)";
+    (* Close the box for the type parameters *)
+    F.pp_close_box fmt ();
+    F.pp_print_space fmt ());
+  (* The input parameters - note that doing this adds bindings to the context *)
+  let ctx_body =
+    match def.body with
+    | None -> ctx
+    | Some body ->
+        List.fold_left
+          (fun ctx (lv : typed_pattern) ->
+            (* Open a box for the input parameter *)
+            F.pp_open_hovbox fmt 0;
+            F.pp_print_string fmt "(";
+            let ctx = extract_typed_pattern ctx fmt false lv in
+            F.pp_print_space fmt ();
+            F.pp_print_string fmt ":";
+            F.pp_print_space fmt ();
+            extract_ty ctx fmt false lv.ty;
+            F.pp_print_string fmt ")";
+            (* Close the box for the input parameters *)
+            F.pp_close_box fmt ();
+            F.pp_print_space fmt ();
+            ctx)
+          ctx body.inputs_lvs
+  in
+  (ctx, ctx_body)
+
+(** A small utility to print the types of the input parameters in the form:
+    [u32 -> list u32 -> ...]
+    (we don't print the return type of the function)
+    
+    This is used for opaque function declarations, in particular.
+ *)
+let extract_fun_input_parameters_types (ctx : extraction_ctx)
+    (fmt : F.formatter) (def : fun_decl) : unit =
+  let extract_param (ty : ty) : unit =
+    let inside = false in
+    extract_ty ctx fmt inside ty;
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt "->";
+    F.pp_print_space fmt ()
+  in
+  List.iter extract_param def.signature.inputs
+
+(** Extract a decrease clause function template body.
+
+    In order to help the user, we can generate a template for the functions
+    required by the decreases clauses. We simply generate definitions of
+    the following form in a separate file:
+    {[
+      let f_decrease (t : Type0) (x : t) : nat = admit()
+    ]}
+    
+    Where the translated functions for [f] look like this:
+    {[
+      let f_fwd (t : Type0) (x : t) : Tot ... (decreases (f_decrease t x)) = ...
+    ]}
+ *)
+let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
+    (def : fun_decl) : unit =
+  (* Retrieve the function name *)
+  let def_name = ctx_get_decreases_clause def.def_id ctx in
+  (* Add a break before *)
+  F.pp_print_break fmt 0 0;
+  (* Print a comment to link the extracted type to its original rust definition *)
+  F.pp_print_string fmt
+    ("(** [" ^ Print.fun_name_to_string def.basename ^ "]: decreases clause *)");
+  F.pp_print_space fmt ();
+  (* Open a box for the definition, so that whenever possible it gets printed on
+   * one line *)
+  F.pp_open_hvbox fmt 0;
+  (* Add the [unfold] keyword *)
+  F.pp_print_string fmt "unfold";
+  F.pp_print_space fmt ();
+  (* Open a box for "let FUN_NAME (PARAMS) : EFFECT = admit()" *)
+  F.pp_open_hvbox fmt ctx.indent_incr;
+  (* Open a box for "let FUN_NAME (PARAMS) : EFFECT =" *)
+  F.pp_open_hovbox fmt ctx.indent_incr;
+  (* > "let FUN_NAME" *)
+  F.pp_print_string fmt ("let " ^ def_name);
+  F.pp_print_space fmt ();
+  (* Extract the parameters *)
+  let _, _ = extract_fun_parameters ctx fmt def in
+  F.pp_print_string fmt ":";
+  (* Print the signature *)
+  F.pp_print_space fmt ();
+  F.pp_print_string fmt "nat";
+  (* Print the "=" *)
+  F.pp_print_space fmt ();
+  F.pp_print_string fmt "=";
+  (* Close the box for "let FUN_NAME (PARAMS) : EFFECT =" *)
+  F.pp_close_box fmt ();
+  F.pp_print_space fmt ();
+  (* Print the "admit ()" *)
+  F.pp_print_string fmt "admit ()";
+  (* Close the box for "let FUN_NAME (PARAMS) : EFFECT = admit()" *)
+  F.pp_close_box fmt ();
+  (* Close the box for the whole definition *)
+  F.pp_close_box fmt ();
+  (* Add breaks to insert new lines between definitions *)
+  F.pp_print_break fmt 0 0
+
+(** Extract a function declaration.
+
+    Note that all the names used for extraction should already have been
+    registered.
+    
+    We take the definition of the forward translation as parameter (which is
+    equal to the definition to extract, if we extract a forward function) because
+    it is useful for the decrease clause.
+ *)
+let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
+    (qualif : fun_decl_qualif) (has_decreases_clause : bool) (def : fun_decl) :
+    unit =
+  assert (not def.is_global_decl_body);
+  (* Retrieve the function name *)
+  let def_name = ctx_get_local_function def.def_id def.back_id ctx in
+  (* (* Add the type parameters - note that we need those bindings only for the
+     * body translation (they are not top-level) *)
+      let ctx, _ = ctx_add_type_params def.signature.type_params ctx in *)
+  (* Add a break before *)
+  F.pp_print_break fmt 0 0;
+  (* Print a comment to link the extracted type to its original rust definition *)
+  F.pp_print_string fmt
+    ("(** [" ^ Print.fun_name_to_string def.basename ^ "] *)");
+  F.pp_print_space fmt ();
+  (* Open a box for the definition, so that whenever possible it gets printed on
+   * one line *)
+  F.pp_open_hvbox fmt ctx.indent_incr;
+  (* Open a box for "let FUN_NAME (PARAMS) : EFFECT =" *)
+  F.pp_open_hovbox fmt ctx.indent_incr;
+  (* > "let FUN_NAME" *)
+  let is_opaque = Option.is_none def.body in
+  let qualif = fun_decl_qualif_keyword qualif in
+  F.pp_print_string fmt (qualif ^ " " ^ def_name);
+  F.pp_print_space fmt ();
+  (* Open a box for "(PARAMS) : EFFECT =" *)
+  F.pp_open_hvbox fmt 0;
+  (* Open a box for "(PARAMS)" *)
+  F.pp_open_hovbox fmt 0;
+  let ctx, ctx_body = extract_fun_parameters ctx fmt def in
+  (* Close the box for "(PARAMS)" *)
+  F.pp_close_box fmt ();
+  (* Print the return type - note that we have to be careful when
+   * printing the input values for the decrease clause, because
+   * it introduces bindings in the context... We thus "forget"
+   * the bindings we introduced above.
+   * TODO: figure out a cleaner way *)
+  let _ =
+    F.pp_print_string fmt ":";
+    F.pp_print_space fmt ();
+    (* Open a box for the EFFECT *)
+    F.pp_open_hvbox fmt 0;
+    (* Open a box for the return type *)
+    F.pp_open_hovbox fmt ctx.indent_incr;
+    (* Print the return type *)
+    (* For opaque definitions, as we don't have named parameters under the hand,
+     * we don't print parameters in the form [(x : a) (y : b) ...] above,
+     * but wait until here to print the types: [a -> b -> ...]. *)
+    if is_opaque then extract_fun_input_parameters_types ctx fmt def;
+    (* [Tot] *)
+    if has_decreases_clause then (
+      F.pp_print_string fmt "Tot";
+      F.pp_print_space fmt ());
+    extract_ty ctx fmt has_decreases_clause def.signature.output;
+    (* Close the box for the return type *)
+    F.pp_close_box fmt ();
+    (* Print the decrease clause - rk.: a function with a decreases clause
+     * is necessarily a transparent function *)
+    if has_decreases_clause then (
+      F.pp_print_space fmt ();
+      (* Open a box for the decrease clause *)
+      F.pp_open_hovbox fmt 0;
+      (* *)
+      F.pp_print_string fmt "(decreases";
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt "(";
+      (* The name of the decrease clause *)
+      let decr_name = ctx_get_decreases_clause def.def_id ctx in
+      F.pp_print_string fmt decr_name;
+      (* Print the type parameters *)
+      List.iter
+        (fun (p : type_var) ->
+          let pname = ctx_get_type_var p.index ctx in
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt pname)
+        def.signature.type_params;
+      (* Print the input values: we have to be careful here to print
+       * only the input values which are in common with the *forward*
+       * function (the additional input values "given back" to the
+       * backward functions have no influence on termination: we thus
+       * share the decrease clauses between the forward and the backward
+       * functions - we also ignore the additional state received by the
+       * backward function, if there is one).
+       *)
+      let inputs_lvs =
+        let all_inputs = (Option.get def.body).inputs_lvs in
+        let num_fwd_inputs = def.signature.info.num_fwd_inputs_with_state in
+        Collections.List.prefix num_fwd_inputs all_inputs
+      in
+      let _ =
+        List.fold_left
+          (fun ctx (lv : typed_pattern) ->
+            F.pp_print_space fmt ();
+            let ctx = extract_typed_pattern ctx fmt false lv in
+            ctx)
+          ctx inputs_lvs
+      in
+      F.pp_print_string fmt "))";
+      (* Close the box for the decrease clause *)
+      F.pp_close_box fmt ());
+    (* Close the box for the EFFECT *)
+    F.pp_close_box fmt ()
+  in
+  (* Print the "=" *)
+  if not is_opaque then (
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt "=");
+  (* Close the box for "(PARAMS) : EFFECT =" *)
+  F.pp_close_box fmt ();
+  (* Close the box for "let FUN_NAME (PARAMS) : EFFECT =" *)
+  F.pp_close_box fmt ();
+  if not is_opaque then (
+    F.pp_print_space fmt ();
+    (* Open a box for the body *)
+    F.pp_open_hvbox fmt 0;
+    (* Extract the body *)
+    let _ = extract_texpression ctx_body fmt false (Option.get def.body).body in
+    (* Close the box for the body *)
+    F.pp_close_box fmt ());
+  (* Close the box for the definition *)
+  F.pp_close_box fmt ();
+  (* Add breaks to insert new lines between definitions *)
+  F.pp_print_break fmt 0 0
+
+(** Extract a global declaration body of the shape "QUALIF NAME : TYPE = BODY" with a custom body extractor *)
+let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter)
+    (qualif : fun_decl_qualif) (name : string) (ty : ty)
+    (extract_body : (F.formatter -> unit) Option.t) : unit =
+  let is_opaque = Option.is_none extract_body in
+
+  (* Open the definition box (depth=0) *)
+  F.pp_open_hvbox fmt ctx.indent_incr;
+
+  (* Open "QUALIF NAME : TYPE =" box (depth=1) *)
+  F.pp_open_hovbox fmt ctx.indent_incr;
+  (* Print "QUALIF NAME " *)
+  F.pp_print_string fmt (fun_decl_qualif_keyword qualif ^ " " ^ name);
+  F.pp_print_space fmt ();
+
+  (* Open ": TYPE =" box (depth=2) *)
+  F.pp_open_hvbox fmt 0;
+  (* Print ": " *)
+  F.pp_print_string fmt ":";
+  F.pp_print_space fmt ();
+
+  (* Open "TYPE" box (depth=3) *)
+  F.pp_open_hovbox fmt ctx.indent_incr;
+  (* Print "TYPE" *)
+  extract_ty ctx fmt false ty;
+  (* Close "TYPE" box (depth=3) *)
+  F.pp_close_box fmt ();
+
+  if not is_opaque then (
+    (* Print " =" *)
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt "=");
+  (* Close ": TYPE =" box (depth=2) *)
+  F.pp_close_box fmt ();
+  (* Close "QUALIF NAME : TYPE =" box (depth=1) *)
+  F.pp_close_box fmt ();
+
+  if not is_opaque then (
+    F.pp_print_space fmt ();
+    (* Open "BODY" box (depth=1) *)
+    F.pp_open_hvbox fmt 0;
+    (* Print "BODY" *)
+    (Option.get extract_body) fmt;
+    (* Close "BODY" box (depth=1) *)
+    F.pp_close_box fmt ());
+  (* Close the definition box (depth=0) *)
+  F.pp_close_box fmt ()
+
+(** Extract a global declaration.
+    We generate the body which computes the global value separately from the value declaration itself.
+
+    For example in Rust,
+    [static X: u32 = 3;]
+
+    will be translated to:
+    [let x_body : result u32 = Return 3]
+    [let x_c : u32 = eval_global x_body]
+ *)
+let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
+    (global : A.global_decl) (body : fun_decl) (interface : bool) : unit =
+  assert body.is_global_decl_body;
+  assert (Option.is_none body.back_id);
+  assert (List.length body.signature.inputs = 0);
+  assert (List.length body.signature.doutputs = 1);
+  assert (List.length body.signature.type_params = 0);
+
+  (* Add a break then the name of the corresponding LLBC declaration *)
+  F.pp_print_break fmt 0 0;
+  F.pp_print_string fmt
+    ("(** [" ^ Print.global_name_to_string global.name ^ "] *)");
+  F.pp_print_space fmt ();
+
+  let decl_name = ctx_get_global global.def_id ctx in
+  let body_name =
+    ctx_get_function (FromLlbc (Regular global.body_id, None)) ctx
+  in
+
+  let decl_ty, body_ty =
+    let ty = body.signature.output in
+    if body.signature.info.effect_info.can_fail then (unwrap_result_ty ty, ty)
+    else (ty, mk_result_ty ty)
+  in
+  match body.body with
+  | None ->
+      let qualif = if interface then Val else AssumeVal in
+      extract_global_decl_body ctx fmt qualif decl_name decl_ty None
+  | Some body ->
+      extract_global_decl_body ctx fmt Let body_name body_ty
+        (Some (fun fmt -> extract_texpression ctx fmt false body.body));
+      F.pp_print_break fmt 0 0;
+      extract_global_decl_body ctx fmt Let decl_name decl_ty
+        (Some (fun fmt -> F.pp_print_string fmt ("eval_global " ^ body_name)));
+      F.pp_print_break fmt 0 0
+
+(** Extract a unit test, if the function is a unit function (takes no
+    parameters, returns unit).
+    
+    A unit test simply checks that the function normalizes to [Return ()]:
+    {[
+      let _ = assert_norm (FUNCTION () = Return ())
+    ]}
+ *)
+let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
+    (def : fun_decl) : unit =
+  (* We only insert unit tests for forward functions *)
+  assert (def.back_id = None);
+  (* Check if this is a unit function *)
+  let sg = def.signature in
+  if
+    sg.type_params = []
+    && (sg.inputs = [ mk_unit_ty ] || sg.inputs = [])
+    && sg.output = mk_result_ty mk_unit_ty
+  then (
+    (* Add a break before *)
+    F.pp_print_break fmt 0 0;
+    (* Print a comment *)
+    F.pp_print_string fmt
+      ("(** Unit test for [" ^ Print.fun_name_to_string def.basename ^ "] *)");
+    F.pp_print_space fmt ();
+    (* Open a box for the test *)
+    F.pp_open_hovbox fmt ctx.indent_incr;
+    (* Print the test *)
+    F.pp_print_string fmt "let _ =";
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt "assert_norm";
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt "(";
+    let fun_name = ctx_get_local_function def.def_id def.back_id ctx in
+    F.pp_print_string fmt fun_name;
+    if sg.inputs <> [] then (
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt "()");
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt "=";
+    F.pp_print_space fmt ();
+    let success = ctx_get_variant (Assumed Result) result_return_id ctx in
+    F.pp_print_string fmt (success ^ " ())");
+    (* Close the box for the test *)
+    F.pp_close_box fmt ();
+    (* Add a break after *)
+    F.pp_print_break fmt 0 0)
+  else (* Do nothing *)
+    ()
diff --git a/compiler/ExtractToFStar.ml b/compiler/ExtractToFStar.ml
deleted file mode 100644
index fc04ce90..00000000
--- a/compiler/ExtractToFStar.ml
+++ /dev/null
@@ -1,1639 +0,0 @@
-(** Extract to F* *)
-
-open Utils
-open Pure
-open PureUtils
-open TranslateCore
-open PureToExtract
-open StringUtils
-module F = Format
-
-(** A qualifier for a type definition.
-
-    Controls whether we should use [type ...] or [and ...] (for mutually
-    recursive datatypes).
- *)
-type type_decl_qualif =
-  | Type  (** [type t = ...] *)
-  | And  (** [type t0 = ... and t1 = ...] *)
-  | AssumeType  (** [assume type t] *)
-  | TypeVal  (** In an fsti: [val t : Type0] *)
-
-(** A qualifier for function definitions.
-
-    Controls whether we should use [let ...], [let rec ...] or [and ...],
-    or only generate a declaration with [val] or [assume val]
- *)
-type fun_decl_qualif = Let | LetRec | And | Val | AssumeVal
-
-let fun_decl_qualif_keyword (qualif : fun_decl_qualif) : string =
-  match qualif with
-  | Let -> "let"
-  | LetRec -> "let rec"
-  | And -> "and"
-  | Val -> "val"
-  | AssumeVal -> "assume val"
-
-(** Small helper to compute the name of an int type *)
-let fstar_int_name (int_ty : integer_type) =
-  match int_ty with
-  | Isize -> "isize"
-  | I8 -> "i8"
-  | I16 -> "i16"
-  | I32 -> "i32"
-  | I64 -> "i64"
-  | I128 -> "i128"
-  | Usize -> "usize"
-  | U8 -> "u8"
-  | U16 -> "u16"
-  | U32 -> "u32"
-  | U64 -> "u64"
-  | U128 -> "u128"
-
-(** Small helper to compute the name of a unary operation *)
-let fstar_unop_name (unop : unop) : string =
-  match unop with
-  | Not -> "not"
-  | Neg int_ty -> fstar_int_name int_ty ^ "_neg"
-  | Cast _ -> raise (Failure "Unsupported")
-
-(** Small helper to compute the name of a binary operation (note that many
-    binary operations like "less than" are extracted to primitive operations,
-    like [<].
- *)
-let fstar_named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
-  let binop =
-    match binop with
-    | Div -> "div"
-    | Rem -> "rem"
-    | Add -> "add"
-    | Sub -> "sub"
-    | Mul -> "mul"
-    | _ -> raise (Failure "Unreachable")
-  in
-  fstar_int_name int_ty ^ "_" ^ binop
-
-(** A list of keywords/identifiers used in F* and with which we want to check
-    collision. *)
-let fstar_keywords =
-  let named_unops =
-    fstar_unop_name Not
-    :: List.map (fun it -> fstar_unop_name (Neg it)) T.all_signed_int_types
-  in
-  let named_binops = [ E.Div; Rem; Add; Sub; Mul ] in
-  let named_binops =
-    List.concat
-      (List.map
-         (fun bn ->
-           List.map (fun it -> fstar_named_binop_name bn it) T.all_int_types)
-         named_binops)
-  in
-  let misc =
-    [
-      "let";
-      "rec";
-      "in";
-      "fn";
-      "val";
-      "int";
-      "nat";
-      "list";
-      "FStar";
-      "FStar.Mul";
-      "type";
-      "match";
-      "with";
-      "assert";
-      "assert_norm";
-      "assume";
-      "Type0";
-      "Type";
-      "unit";
-      "not";
-      "scalar_cast";
-    ]
-  in
-  List.concat [ named_unops; named_binops; misc ]
-
-let fstar_assumed_adts : (assumed_ty * string) list =
-  [ (State, "state"); (Result, "result"); (Option, "option"); (Vec, "vec") ]
-
-let fstar_assumed_structs : (assumed_ty * string) list = []
-
-let fstar_assumed_variants : (assumed_ty * VariantId.id * string) list =
-  [
-    (Result, result_return_id, "Return");
-    (Result, result_fail_id, "Fail");
-    (Option, option_some_id, "Some");
-    (Option, option_none_id, "None");
-  ]
-
-let fstar_assumed_llbc_functions :
-    (A.assumed_fun_id * T.RegionGroupId.id option * string) list =
-  let rg0 = Some T.RegionGroupId.zero in
-  [
-    (Replace, None, "mem_replace_fwd");
-    (Replace, rg0, "mem_replace_back");
-    (VecNew, None, "vec_new");
-    (VecPush, None, "vec_push_fwd") (* Shouldn't be used *);
-    (VecPush, rg0, "vec_push_back");
-    (VecInsert, None, "vec_insert_fwd") (* Shouldn't be used *);
-    (VecInsert, rg0, "vec_insert_back");
-    (VecLen, None, "vec_len");
-    (VecIndex, None, "vec_index_fwd");
-    (VecIndex, rg0, "vec_index_back") (* shouldn't be used *);
-    (VecIndexMut, None, "vec_index_mut_fwd");
-    (VecIndexMut, rg0, "vec_index_mut_back");
-  ]
-
-let fstar_assumed_pure_functions : (pure_assumed_fun_id * string) list =
-  [ (Return, "return"); (Fail, "fail"); (Assert, "massert") ]
-
-let fstar_names_map_init : names_map_init =
-  {
-    keywords = fstar_keywords;
-    assumed_adts = fstar_assumed_adts;
-    assumed_structs = fstar_assumed_structs;
-    assumed_variants = fstar_assumed_variants;
-    assumed_llbc_functions = fstar_assumed_llbc_functions;
-    assumed_pure_functions = fstar_assumed_pure_functions;
-  }
-
-let fstar_extract_unop (extract_expr : bool -> texpression -> unit)
-    (fmt : F.formatter) (inside : bool) (unop : unop) (arg : texpression) : unit
-    =
-  match unop with
-  | Not | Neg _ ->
-      let unop = fstar_unop_name unop in
-      if inside then F.pp_print_string fmt "(";
-      F.pp_print_string fmt unop;
-      F.pp_print_space fmt ();
-      extract_expr true arg;
-      if inside then F.pp_print_string fmt ")"
-  | Cast (src, tgt) ->
-      (* The source type is an implicit parameter *)
-      if inside then F.pp_print_string fmt "(";
-      F.pp_print_string fmt "scalar_cast";
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt
-        (StringUtils.capitalize_first_letter
-           (PrintPure.integer_type_to_string src));
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt
-        (StringUtils.capitalize_first_letter
-           (PrintPure.integer_type_to_string tgt));
-      F.pp_print_space fmt ();
-      extract_expr true arg;
-      if inside then F.pp_print_string fmt ")"
-
-let fstar_extract_binop (extract_expr : bool -> texpression -> unit)
-    (fmt : F.formatter) (inside : bool) (binop : E.binop)
-    (int_ty : integer_type) (arg0 : texpression) (arg1 : texpression) : unit =
-  if inside then F.pp_print_string fmt "(";
-  (* Some binary operations have a special treatment *)
-  (match binop with
-  | Eq | Lt | Le | Ne | Ge | Gt ->
-      let binop =
-        match binop with
-        | Eq -> "="
-        | Lt -> "<"
-        | Le -> "<="
-        | Ne -> "<>"
-        | Ge -> ">="
-        | Gt -> ">"
-        | _ -> raise (Failure "Unreachable")
-      in
-      extract_expr false arg0;
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt binop;
-      F.pp_print_space fmt ();
-      extract_expr false arg1
-  | Div | Rem | Add | Sub | Mul ->
-      let binop = fstar_named_binop_name binop int_ty in
-      F.pp_print_string fmt binop;
-      F.pp_print_space fmt ();
-      extract_expr false arg0;
-      F.pp_print_space fmt ();
-      extract_expr false arg1
-  | BitXor | BitAnd | BitOr | Shl | Shr -> raise Unimplemented);
-  if inside then F.pp_print_string fmt ")"
-
-(**
-   [ctx]: we use the context to lookup type definitions, to retrieve type names.
-   This is used to compute variable names, when they have no basenames: in this
-   case we use the first letter of the type name.
-  
-   [variant_concatenate_type_name]: if true, add the type name as a prefix
-   to the variant names.
-   Ex.:
-   In Rust:
-     {[
-       enum List = {
-         Cons(u32, Box<List>),x
-         Nil,
-       }
-     ]}
-  
-   F*, if option activated:
-     {[
-       type list =
-       | ListCons : u32 -> list -> list
-       | ListNil : list
-     ]}
-  
-   F*, if option not activated:
-     {[
-       type list =
-       | Cons : u32 -> list -> list
-       | Nil : list
-     ]}
-  
-   Rk.: this should be true by default, because in Rust all the variant names
-   are actively uniquely identifier by the type name [List::Cons(...)], while
-   in other languages it is not necessarily the case, and thus clashes can mess
-   up type checking. Note that some languages actually forbids the name clashes
-   (it is the case of F* ).
- *)
-let mk_formatter (ctx : trans_ctx) (crate_name : string)
-    (variant_concatenate_type_name : bool) : formatter =
-  let int_name = fstar_int_name in
-
-  (* Prepare a name.
-   * The first id elem is always the crate: if it is the local crate,
-   * we remove it.
-   * We also remove all the disambiguators, then convert everything to strings.
-   * **Rmk:** because we remove the disambiguators, there may be name collisions
-   * (which is ok, because we check for name collisions and fail if there is any).
-   *)
-  let get_name (name : name) : string list =
-    (* Rmk.: initially we only filtered the disambiguators equal to 0 *)
-    let name = Names.filter_disambiguators name in
-    match name with
-    | Ident crate :: name ->
-        let name = if crate = crate_name then name else Ident crate :: name in
-        let name =
-          List.map
-            (function
-              | Names.Ident s -> s
-              | Disambiguator d -> Names.Disambiguator.to_string d)
-            name
-        in
-        name
-    | _ ->
-        raise (Failure ("Unexpected name shape: " ^ Print.name_to_string name))
-  in
-  let get_type_name = get_name in
-  let type_name_to_camel_case name =
-    let name = get_type_name name in
-    let name = List.map to_camel_case name in
-    String.concat "" name
-  in
-  let type_name_to_snake_case name =
-    let name = get_type_name name in
-    let name = List.map to_snake_case name in
-    String.concat "_" name
-  in
-  let type_name name = type_name_to_snake_case name ^ "_t" in
-  let field_name (def_name : name) (field_id : FieldId.id)
-      (field_name : string option) : string =
-    let def_name = type_name_to_snake_case def_name ^ "_" in
-    match field_name with
-    | Some field_name -> def_name ^ field_name
-    | None -> def_name ^ FieldId.to_string field_id
-  in
-  let variant_name (def_name : name) (variant : string) : string =
-    let variant = to_camel_case variant in
-    if variant_concatenate_type_name then
-      type_name_to_camel_case def_name ^ variant
-    else variant
-  in
-  let struct_constructor (basename : name) : string =
-    let tname = type_name basename in
-    "Mk" ^ tname
-  in
-  let get_fun_name = get_name in
-  let fun_name_to_snake_case (fname : fun_name) : string =
-    let fname = get_fun_name fname in
-    (* Converting to snake case should be a no-op, but it doesn't cost much *)
-    let fname = List.map to_snake_case fname in
-    (* Concatenate the elements *)
-    String.concat "_" fname
-  in
-  let global_name (name : global_name) : string =
-    (* Converting to snake case also lowercases the letters (in Rust, global
-     * names are written in capital letters). *)
-    let parts = List.map to_snake_case (get_name name) in
-    String.concat "_" parts
-  in
-  let fun_name (fname : fun_name) (num_rgs : int)
-      (rg : region_group_info option) (filter_info : bool * int) : string =
-    let fname = fun_name_to_snake_case fname in
-    (* Compute the suffix *)
-    let suffix = default_fun_suffix num_rgs rg filter_info in
-    (* Concatenate *)
-    fname ^ suffix
-  in
-
-  let decreases_clause_name (_fid : A.FunDeclId.id) (fname : fun_name) : string
-      =
-    let fname = fun_name_to_snake_case fname in
-    (* Compute the suffix *)
-    let suffix = "_decreases" in
-    (* Concatenate *)
-    fname ^ suffix
-  in
-
-  let var_basename (_varset : StringSet.t) (basename : string option) (ty : ty)
-      : string =
-    (* If there is a basename, we use it *)
-    match basename with
-    | Some basename ->
-        (* This should be a no-op *)
-        to_snake_case basename
-    | None -> (
-        (* No basename: we use the first letter of the type *)
-        match ty with
-        | Adt (type_id, tys) -> (
-            match type_id with
-            | Tuple ->
-                (* The "pair" case is frequent enough to have its special treatment *)
-                if List.length tys = 2 then "p" else "t"
-            | Assumed Result -> "r"
-            | Assumed Option -> "opt"
-            | Assumed Vec -> "v"
-            | Assumed State -> "st"
-            | AdtId adt_id ->
-                let def =
-                  TypeDeclId.Map.find adt_id ctx.type_context.type_decls
-                in
-                (* We do the following:
-                 * - compute the type name, and retrieve the last ident
-                 * - convert this to snake case
-                 * - take the first letter of every "letter group"
-                 * Ex.: ["hashmap"; "HashMap"] ~~> "HashMap" -> "hash_map" -> "hm"
-                 *)
-                (* Thename shouldn't be empty, and its last element should
-                 * be an ident *)
-                let cl = List.nth def.name (List.length def.name - 1) in
-                let cl = to_snake_case (Names.as_ident cl) in
-                let cl = String.split_on_char '_' cl in
-                let cl = List.filter (fun s -> String.length s > 0) cl in
-                assert (List.length cl > 0);
-                let cl = List.map (fun s -> s.[0]) cl in
-                StringUtils.string_of_chars cl)
-        | TypeVar _ -> "x" (* lacking imagination here... *)
-        | Bool -> "b"
-        | Char -> "c"
-        | Integer _ -> "i"
-        | Str -> "s"
-        | Arrow _ -> "f"
-        | Array _ | Slice _ -> raise Unimplemented)
-  in
-  let type_var_basename (_varset : StringSet.t) (basename : string) : string =
-    (* This is *not* a no-op: type variables in Rust often start with
-     * a capital letter *)
-    to_snake_case basename
-  in
-  let append_index (basename : string) (i : int) : string =
-    basename ^ string_of_int i
-  in
-
-  let extract_primitive_value (fmt : F.formatter) (_inside : bool)
-      (cv : primitive_value) : unit =
-    match cv with
-    | Scalar sv -> F.pp_print_string fmt (Z.to_string sv.PV.value)
-    | Bool b ->
-        let b = if b then "true" else "false" in
-        F.pp_print_string fmt b
-    | Char c -> F.pp_print_string fmt ("'" ^ String.make 1 c ^ "'")
-    | String s ->
-        (* We need to replace all the line breaks *)
-        let s =
-          StringUtils.map
-            (fun c -> if c = '\n' then "\n" else String.make 1 c)
-            s
-        in
-        F.pp_print_string fmt ("\"" ^ s ^ "\"")
-  in
-  {
-    bool_name = "bool";
-    char_name = "char";
-    int_name;
-    str_name = "string";
-    field_name;
-    variant_name;
-    struct_constructor;
-    type_name;
-    global_name;
-    fun_name;
-    decreases_clause_name;
-    var_basename;
-    type_var_basename;
-    append_index;
-    extract_primitive_value;
-    extract_unop = fstar_extract_unop;
-    extract_binop = fstar_extract_binop;
-  }
-
-(** [inside] constrols whether we should add parentheses or not around type
-    applications (if [true] we add parentheses).
- *)
-let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
-    (ty : ty) : unit =
-  match ty with
-  | Adt (type_id, tys) -> (
-      match type_id with
-      | Tuple ->
-          (* This is a bit annoying, but in F* [()] is not the unit type:
-           * we have to write [unit]... *)
-          if tys = [] then F.pp_print_string fmt "unit"
-          else (
-            F.pp_print_string fmt "(";
-            Collections.List.iter_link
-              (fun () ->
-                F.pp_print_space fmt ();
-                F.pp_print_string fmt "&";
-                F.pp_print_space fmt ())
-              (extract_ty ctx fmt true) tys;
-            F.pp_print_string fmt ")")
-      | AdtId _ | Assumed _ ->
-          let print_paren = inside && tys <> [] in
-          if print_paren then F.pp_print_string fmt "(";
-          F.pp_print_string fmt (ctx_get_type type_id ctx);
-          if tys <> [] then F.pp_print_space fmt ();
-          Collections.List.iter_link (F.pp_print_space fmt)
-            (extract_ty ctx fmt true) tys;
-          if print_paren then F.pp_print_string fmt ")")
-  | TypeVar vid -> F.pp_print_string fmt (ctx_get_type_var vid ctx)
-  | Bool -> F.pp_print_string fmt ctx.fmt.bool_name
-  | Char -> F.pp_print_string fmt ctx.fmt.char_name
-  | Integer int_ty -> F.pp_print_string fmt (ctx.fmt.int_name int_ty)
-  | Str -> F.pp_print_string fmt ctx.fmt.str_name
-  | Arrow (arg_ty, ret_ty) ->
-      if inside then F.pp_print_string fmt "(";
-      extract_ty ctx fmt false arg_ty;
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt "->";
-      F.pp_print_space fmt ();
-      extract_ty ctx fmt false ret_ty;
-      if inside then F.pp_print_string fmt ")"
-  | Array _ | Slice _ -> raise Unimplemented
-
-(** Compute the names for all the top-level identifiers used in a type
-    definition (type name, variant names, field names, etc. but not type
-    parameters).
-    
-    We need to do this preemptively, beforce extracting any definition,
-    because of recursive definitions.
- *)
-let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
-    extraction_ctx =
-  (* Compute and register the type def name *)
-  let ctx = ctx_add_type_decl def ctx in
-  (* Compute and register:
-   * - the variant names, if this is an enumeration
-   * - the field names, if this is a structure
-   *)
-  let ctx =
-    match def.kind with
-    | Struct fields ->
-        (* Add the fields *)
-        let ctx =
-          fst
-            (ctx_add_fields def (FieldId.mapi (fun id f -> (id, f)) fields) ctx)
-        in
-        (* Add the constructor name *)
-        fst (ctx_add_struct def ctx)
-    | Enum variants ->
-        fst
-          (ctx_add_variants def
-             (VariantId.mapi (fun id v -> (id, v)) variants)
-             ctx)
-    | Opaque ->
-        (* Nothing to do *)
-        ctx
-  in
-  (* Return *)
-  ctx
-
-let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
-    (def : type_decl) (fields : field list) : unit =
-  (* We want to generate a definition which looks like this:
-     {[
-       type t = { x : int; y : bool; }
-     ]}
-
-     If there isn't enough space on one line:
-     {[
-       type t =
-       {
-         x : int; y : bool;
-       }
-     ]}
-
-     And if there is even less space:
-     {[
-       type t =
-       {
-         x : int;
-         y : bool;
-       }
-     ]}
-
-     Also, in case there are no fields, we need to define the type as [unit]
-     ([type t = {}] doesn't work in F* ).
-  *)
-  (* Note that we already printed: [type t =] *)
-  if fields = [] then (
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "unit")
-  else (
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "{";
-    F.pp_print_break fmt 1 ctx.indent_incr;
-    (* The body itself *)
-    F.pp_open_hvbox fmt 0;
-    (* Print the fields *)
-    let print_field (field_id : FieldId.id) (f : field) : unit =
-      let field_name = ctx_get_field (AdtId def.def_id) field_id ctx in
-      F.pp_open_box fmt ctx.indent_incr;
-      F.pp_print_string fmt field_name;
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt ":";
-      F.pp_print_space fmt ();
-      extract_ty ctx fmt false f.field_ty;
-      F.pp_print_string fmt ";";
-      F.pp_close_box fmt ()
-    in
-    let fields = FieldId.mapi (fun fid f -> (fid, f)) fields in
-    Collections.List.iter_link (F.pp_print_space fmt)
-      (fun (fid, f) -> print_field fid f)
-      fields;
-    (* Close *)
-    F.pp_close_box fmt ();
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "}")
-
-let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
-    (def : type_decl) (def_name : string) (type_params : string list)
-    (variants : variant list) : unit =
-  (* We want to generate a definition which looks like this:
-     {[
-       type list a = | Cons : a -> list a -> list a | Nil : list a
-     ]}
-
-     If there isn't enough space on one line:
-     {[
-       type s =
-       | Cons : a -> list a -> list a
-       | Nil : list a
-     ]}
-
-     And if we need to write the type of a variant on several lines:
-     {[
-       type s =
-       | Cons :
-         a ->
-         list a ->
-         list a
-       | Nil : list a
-     ]}
-
-     Finally, it is possible to give names to the variant fields in Rust.
-     In this situation, we generate a definition like this:
-     {[
-       type s =
-       | Cons : hd:a -> tl:list a -> list a
-       | Nil : list a
-     ]}
-
-     Note that we already printed: [type s =]
-  *)
-  (* Print the variants *)
-  let print_variant (variant_id : VariantId.id) (variant : variant) : unit =
-    let variant_name = ctx_get_variant (AdtId def.def_id) variant_id ctx in
-    F.pp_print_space fmt ();
-    F.pp_open_hvbox fmt ctx.indent_incr;
-    (* variant box *)
-    (* [| Cons :]
-     * Note that we really don't want any break above so we print everything
-     * at once. *)
-    F.pp_print_string fmt ("| " ^ variant_name ^ " :");
-    F.pp_print_space fmt ();
-    let print_field (fid : FieldId.id) (f : field) (ctx : extraction_ctx) :
-        extraction_ctx =
-      (* Open the field box *)
-      F.pp_open_box fmt ctx.indent_incr;
-      (* Print the field names
-       * [  x :]
-       * Note that when printing fields, we register the field names as
-       * *variables*: they don't need to be unique at the top level. *)
-      let ctx =
-        match f.field_name with
-        | None -> ctx
-        | Some field_name ->
-            let var_id = VarId.of_int (FieldId.to_int fid) in
-            let field_name =
-              ctx.fmt.var_basename ctx.names_map.names_set (Some field_name)
-                f.field_ty
-            in
-            let ctx, field_name = ctx_add_var field_name var_id ctx in
-            F.pp_print_string fmt (field_name ^ " :");
-            F.pp_print_space fmt ();
-            ctx
-      in
-      (* Print the field type *)
-      extract_ty ctx fmt false f.field_ty;
-      (* Print the arrow [->]*)
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt "->";
-      (* Close the field box *)
-      F.pp_close_box fmt ();
-      F.pp_print_space fmt ();
-      (* Return *)
-      ctx
-    in
-    (* Print the fields *)
-    let fields = FieldId.mapi (fun fid f -> (fid, f)) variant.fields in
-    let _ =
-      List.fold_left (fun ctx (fid, f) -> print_field fid f ctx) ctx fields
-    in
-    (* Print the final type *)
-    F.pp_open_hovbox fmt 0;
-    F.pp_print_string fmt def_name;
-    List.iter
-      (fun type_param ->
-        F.pp_print_space fmt ();
-        F.pp_print_string fmt type_param)
-      type_params;
-    F.pp_close_box fmt ();
-    (* Close the variant box *)
-    F.pp_close_box fmt ()
-  in
-  (* Print the variants *)
-  let variants = VariantId.mapi (fun vid v -> (vid, v)) variants in
-  List.iter (fun (vid, v) -> print_variant vid v) variants
-
-(** Extract a type declaration.
-
-    Note that all the names used for extraction should already have been
-    registered.
- *)
-let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
-    (qualif : type_decl_qualif) (def : type_decl) : unit =
-  (* Retrieve the definition name *)
-  let def_name = ctx_get_local_type def.def_id ctx in
-  (* Add the type params - note that we need those bindings only for the
-   * body translation (they are not top-level) *)
-  let ctx_body, type_params = ctx_add_type_params def.type_params ctx in
-  (* Add a break before *)
-  F.pp_print_break fmt 0 0;
-  (* Print a comment to link the extracted type to its original rust definition *)
-  F.pp_print_string fmt ("(** [" ^ Print.name_to_string def.name ^ "] *)");
-  F.pp_print_space fmt ();
-  (* Open a box for the definition, so that whenever possible it gets printed on
-   * one line *)
-  F.pp_open_hvbox fmt 0;
-  (* Open a box for "type TYPE_NAME (TYPE_PARAMS) =" *)
-  F.pp_open_hovbox fmt ctx.indent_incr;
-  (* > "type TYPE_NAME" *)
-  let extract_body, qualif =
-    match qualif with
-    | Type -> (true, "type")
-    | And -> (true, "and")
-    | AssumeType -> (false, "assume type")
-    | TypeVal -> (false, "val")
-  in
-  F.pp_print_string fmt (qualif ^ " " ^ def_name);
-  (* Print the type parameters *)
-  if def.type_params <> [] then (
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "(";
-    List.iter
-      (fun (p : type_var) ->
-        let pname = ctx_get_type_var p.index ctx_body in
-        F.pp_print_string fmt pname;
-        F.pp_print_space fmt ())
-      def.type_params;
-    F.pp_print_string fmt ":";
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "Type0)");
-  (* Print the "=" if we extract the body*)
-  if extract_body then (
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "=")
-  else (
-    (* Otherwise print ": Type0" *)
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt ":";
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "Type0");
-  (* Close the box for "type TYPE_NAME (TYPE_PARAMS) =" *)
-  F.pp_close_box fmt ();
-  (if extract_body then
-   match def.kind with
-   | Struct fields -> extract_type_decl_struct_body ctx_body fmt def fields
-   | Enum variants ->
-       extract_type_decl_enum_body ctx_body fmt def def_name type_params
-         variants
-   | Opaque -> raise (Failure "Unreachable"));
-  (* Close the box for the definition *)
-  F.pp_close_box fmt ();
-  (* Add breaks to insert new lines between definitions *)
-  F.pp_print_break fmt 0 0
-
-(** Extract the state type declaration. *)
-let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
-    (qualif : type_decl_qualif) : unit =
-  (* Add a break before *)
-  F.pp_print_break fmt 0 0;
-  (* Print a comment  *)
-  F.pp_print_string fmt "(** The state type used in the state-error monad *)";
-  F.pp_print_space fmt ();
-  (* Open a box for the definition, so that whenever possible it gets printed on
-   * one line *)
-  F.pp_open_hvbox fmt 0;
-  (* Retrieve the name *)
-  let state_name = ctx_get_assumed_type State ctx in
-  (* The qualif should be [AssumeType] or [TypeVal] *)
-  (match qualif with
-  | Type | And -> raise (Failure "Unexpected")
-  | AssumeType ->
-      F.pp_print_string fmt "assume";
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt "type";
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt state_name;
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt ":";
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt "Type0"
-  | TypeVal ->
-      F.pp_print_string fmt "val";
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt state_name;
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt ":";
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt "Type0");
-  (* Close the box for the definition *)
-  F.pp_close_box fmt ();
-  (* Add breaks to insert new lines between definitions *)
-  F.pp_print_break fmt 0 0
-
-(** Compute the names for all the pure functions generated from a rust function
-    (forward function and backward functions).
- *)
-let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool)
-    (has_decreases_clause : bool) (def : pure_fun_translation) : extraction_ctx
-    =
-  let fwd, back_ls = def in
-  (* Register the decrease clause, if necessary *)
-  let ctx =
-    if has_decreases_clause then ctx_add_decrases_clause fwd ctx else ctx
-  in
-  (* Register the forward function name *)
-  let ctx = ctx_add_fun_decl (keep_fwd, def) fwd ctx in
-  (* Register the backward functions' names *)
-  let ctx =
-    List.fold_left
-      (fun ctx back -> ctx_add_fun_decl (keep_fwd, def) back ctx)
-      ctx back_ls
-  in
-  (* Return *)
-  ctx
-
-(** Simply add the global name to the context. *)
-let extract_global_decl_register_names (ctx : extraction_ctx)
-    (def : A.global_decl) : extraction_ctx =
-  ctx_add_global_decl_and_body def ctx
-
-(** The following function factorizes the extraction of ADT values.
-
-    Note that patterns can introduce new variables: we thus return an extraction
-    context updated with new bindings.
-    
-    TODO: we don't need something very generic anymore
- *)
-let extract_adt_g_value
-    (extract_value : extraction_ctx -> bool -> 'v -> extraction_ctx)
-    (fmt : F.formatter) (ctx : extraction_ctx) (inside : bool)
-    (variant_id : VariantId.id option) (field_values : 'v list) (ty : ty) :
-    extraction_ctx =
-  match ty with
-  | Adt (Tuple, _) ->
-      (* Tuple *)
-      F.pp_print_string fmt "(";
-      let ctx =
-        Collections.List.fold_left_link
-          (fun () ->
-            F.pp_print_string fmt ",";
-            F.pp_print_space fmt ())
-          (fun ctx v -> extract_value ctx false v)
-          ctx field_values
-      in
-      F.pp_print_string fmt ")";
-      ctx
-  | Adt (adt_id, _) ->
-      (* "Regular" ADT *)
-      (* We print something of the form: [Cons field0 ... fieldn].
-       * We could update the code to print something of the form:
-       * [{ field0=...; ...; fieldn=...; }] in case of structures.
-       *)
-      let cons =
-        match variant_id with
-        | Some vid -> ctx_get_variant adt_id vid ctx
-        | None -> ctx_get_struct adt_id ctx
-      in
-      if inside && field_values <> [] then F.pp_print_string fmt "(";
-      F.pp_print_string fmt cons;
-      let ctx =
-        Collections.List.fold_left
-          (fun ctx v ->
-            F.pp_print_space fmt ();
-            extract_value ctx true v)
-          ctx field_values
-      in
-      if inside && field_values <> [] then F.pp_print_string fmt ")";
-      ctx
-  | _ -> raise (Failure "Inconsistent typed value")
-
-(* Extract globals in the same way as variables *)
-let extract_global (ctx : extraction_ctx) (fmt : F.formatter)
-    (id : A.GlobalDeclId.id) : unit =
-  F.pp_print_string fmt (ctx_get_global id ctx)
-
-(** [inside]: see {!extract_ty}.
-
-    As a pattern can introduce new variables, we return an extraction context
-    updated with new bindings.
- *)
-let rec extract_typed_pattern (ctx : extraction_ctx) (fmt : F.formatter)
-    (inside : bool) (v : typed_pattern) : extraction_ctx =
-  match v.value with
-  | PatConstant cv ->
-      ctx.fmt.extract_primitive_value fmt inside cv;
-      ctx
-  | PatVar (v, _) ->
-      let vname =
-        ctx.fmt.var_basename ctx.names_map.names_set v.basename v.ty
-      in
-      let ctx, vname = ctx_add_var vname v.id ctx in
-      F.pp_print_string fmt vname;
-      ctx
-  | PatDummy ->
-      F.pp_print_string fmt "_";
-      ctx
-  | PatAdt av ->
-      let extract_value ctx inside v = extract_typed_pattern ctx fmt inside v in
-      extract_adt_g_value extract_value fmt ctx inside av.variant_id
-        av.field_values v.ty
-
-(** [inside]: controls the introduction of parentheses. See [extract_ty]
-    
-    TODO: replace the formatting boolean [inside] with something more general?
-    Also, it seems we don't really use it...
-    Cases to consider:
-    - right-expression in a let: [let x = re in _] (never parentheses?)
-    - next expression in a let:  [let x = _ in next_e] (never parentheses?)
-    - application argument: [f (exp)]
-    - match/if scrutinee: [if exp then _ else _]/[match exp | _ -> _]
- *)
-let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
-    (inside : bool) (e : texpression) : unit =
-  match e.e with
-  | Var var_id ->
-      let var_name = ctx_get_var var_id ctx in
-      F.pp_print_string fmt var_name
-  | Const cv -> ctx.fmt.extract_primitive_value fmt inside cv
-  | App _ ->
-      let app, args = destruct_apps e in
-      extract_App ctx fmt inside app args
-  | Abs _ ->
-      let xl, e = destruct_abs_list e in
-      extract_Abs ctx fmt inside xl e
-  | Qualif _ ->
-      (* We use the app case *)
-      extract_App ctx fmt inside e []
-  | Let (monadic, lv, re, next_e) ->
-      extract_Let ctx fmt inside monadic lv re next_e
-  | Switch (scrut, body) -> extract_Switch ctx fmt inside scrut body
-  | Meta (_, e) -> extract_texpression ctx fmt inside e
-
-(* Extract an application *or* a top-level qualif (function extraction has
- * to handle top-level qualifiers, so it seemed more natural to merge the
- * two cases) *)
-and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
-    (app : texpression) (args : texpression list) : unit =
-  (* We don't do the same thing if the app is a top-level identifier (function,
-   * ADT constructor...) or a "regular" expression *)
-  match app.e with
-  | Qualif qualif -> (
-      (* Top-level qualifier *)
-      match qualif.id with
-      | FunOrOp fun_id ->
-          extract_function_call ctx fmt inside fun_id qualif.type_args args
-      | Global global_id -> extract_global ctx fmt global_id
-      | AdtCons adt_cons_id ->
-          extract_adt_cons ctx fmt inside adt_cons_id qualif.type_args args
-      | Proj proj ->
-          extract_field_projector ctx fmt inside app proj qualif.type_args args)
-  | _ ->
-      (* "Regular" expression *)
-      (* Open parentheses *)
-      if inside then F.pp_print_string fmt "(";
-      (* Open a box for the application *)
-      F.pp_open_hovbox fmt ctx.indent_incr;
-      (* Print the app expression *)
-      let app_inside = (inside && args = []) || args <> [] in
-      extract_texpression ctx fmt app_inside app;
-      (* Print the arguments *)
-      List.iter
-        (fun ve ->
-          F.pp_print_space fmt ();
-          extract_texpression ctx fmt true ve)
-        args;
-      (* Close the box for the application *)
-      F.pp_close_box fmt ();
-      (* Close parentheses *)
-      if inside then F.pp_print_string fmt ")"
-
-(** Subcase of the app case: function call *)
-and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
-    (inside : bool) (fid : fun_or_op_id) (type_args : ty list)
-    (args : texpression list) : unit =
-  match (fid, args) with
-  | Unop unop, [ arg ] ->
-      (* A unop can have *at most* one argument (the result can't be a function!).
-       * Note that the way we generate the translation, we shouldn't get the
-       * case where we have no argument (all functions are fully instantiated,
-       * and no AST transformation introduces partial calls). *)
-      ctx.fmt.extract_unop (extract_texpression ctx fmt) fmt inside unop arg
-  | Binop (binop, int_ty), [ arg0; arg1 ] ->
-      (* Number of arguments: similar to unop *)
-      ctx.fmt.extract_binop
-        (extract_texpression ctx fmt)
-        fmt inside binop int_ty arg0 arg1
-  | Fun fun_id, _ ->
-      if inside then F.pp_print_string fmt "(";
-      (* Open a box for the function call *)
-      F.pp_open_hovbox fmt ctx.indent_incr;
-      (* Print the function name *)
-      let fun_name = ctx_get_function fun_id ctx in
-      F.pp_print_string fmt fun_name;
-      (* Print the type parameters *)
-      List.iter
-        (fun ty ->
-          F.pp_print_space fmt ();
-          extract_ty ctx fmt true ty)
-        type_args;
-      (* Print the arguments *)
-      List.iter
-        (fun ve ->
-          F.pp_print_space fmt ();
-          extract_texpression ctx fmt true ve)
-        args;
-      (* Close the box for the function call *)
-      F.pp_close_box fmt ();
-      (* Return *)
-      if inside then F.pp_print_string fmt ")"
-  | (Unop _ | Binop _), _ ->
-      raise
-        (Failure
-           ("Unreachable:\n" ^ "Function: " ^ show_fun_or_op_id fid
-          ^ ",\nNumber of arguments: "
-           ^ string_of_int (List.length args)
-           ^ ",\nArguments: "
-           ^ String.concat " " (List.map show_texpression args)))
-
-(** Subcase of the app case: ADT constructor *)
-and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
-    (adt_cons : adt_cons_id) (type_args : ty list) (args : texpression list) :
-    unit =
-  match adt_cons.adt_id with
-  | Tuple ->
-      (* Tuple *)
-      (* For now, we only support fully applied tuple constructors *)
-      assert (List.length type_args = List.length args);
-      F.pp_print_string fmt "(";
-      Collections.List.iter_link
-        (fun () ->
-          F.pp_print_string fmt ",";
-          F.pp_print_space fmt ())
-        (fun v -> extract_texpression ctx fmt false v)
-        args;
-      F.pp_print_string fmt ")"
-  | _ ->
-      (* "Regular" ADT *)
-      (* We print something of the form: [Cons field0 ... fieldn].
-       * We could update the code to print something of the form:
-       * [{ field0=...; ...; fieldn=...; }] in case of fully
-       * applied structure constructors.
-       *)
-      let cons =
-        match adt_cons.variant_id with
-        | Some vid -> ctx_get_variant adt_cons.adt_id vid ctx
-        | None -> ctx_get_struct adt_cons.adt_id ctx
-      in
-      let use_parentheses = inside && args <> [] in
-      if use_parentheses then F.pp_print_string fmt "(";
-      F.pp_print_string fmt cons;
-      Collections.List.iter
-        (fun v ->
-          F.pp_print_space fmt ();
-          extract_texpression ctx fmt true v)
-        args;
-      if use_parentheses then F.pp_print_string fmt ")"
-
-(** Subcase of the app case: ADT field projector.  *)
-and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter)
-    (inside : bool) (original_app : texpression) (proj : projection)
-    (_proj_type_params : ty list) (args : texpression list) : unit =
-  (* We isolate the first argument (if there is), in order to pretty print the
-   * projection ([x.field] instead of [MkAdt?.field x] *)
-  match args with
-  | [ arg ] ->
-      (* Exactly one argument: pretty-print *)
-      let field_name = ctx_get_field proj.adt_id proj.field_id ctx in
-      (* Open a box *)
-      F.pp_open_hovbox fmt ctx.indent_incr;
-      (* Extract the expression *)
-      extract_texpression ctx fmt true arg;
-      (* We allow to break where the "." appears *)
-      F.pp_print_break fmt 0 0;
-      F.pp_print_string fmt ".";
-      F.pp_print_string fmt field_name;
-      (* Close the box *)
-      F.pp_close_box fmt ()
-  | arg :: args ->
-      (* Call extract_App again, but in such a way that the first argument is
-       * isolated *)
-      extract_App ctx fmt inside (mk_app original_app arg) args
-  | [] ->
-      (* No argument: shouldn't happen *)
-      raise (Failure "Unreachable")
-
-and extract_Abs (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
-    (xl : typed_pattern list) (e : texpression) : unit =
-  (* Open a box for the abs expression *)
-  F.pp_open_hovbox fmt ctx.indent_incr;
-  (* Open parentheses *)
-  if inside then F.pp_print_string fmt "(";
-  (* Print the lambda - note that there should always be at least one variable *)
-  assert (xl <> []);
-  F.pp_print_string fmt "fun";
-  let ctx =
-    List.fold_left
-      (fun ctx x ->
-        F.pp_print_space fmt ();
-        extract_typed_pattern ctx fmt true x)
-      ctx xl
-  in
-  F.pp_print_space fmt ();
-  F.pp_print_string fmt "->";
-  F.pp_print_space fmt ();
-  (* Print the body *)
-  extract_texpression ctx fmt false e;
-  (* Close parentheses *)
-  if inside then F.pp_print_string fmt ")";
-  (* Close the box for the abs expression *)
-  F.pp_close_box fmt ()
-
-and extract_Let (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
-    (monadic : bool) (lv : typed_pattern) (re : texpression)
-    (next_e : texpression) : unit =
-  (* Open a box for the whole expression *)
-  F.pp_open_hvbox fmt 0;
-  (* Open parentheses *)
-  if inside then F.pp_print_string fmt "(";
-  (* Open a box for the let-binding *)
-  F.pp_open_hovbox fmt ctx.indent_incr;
-  let ctx =
-    if monadic then (
-      (* Note that in F*, the left value of a monadic let-binding can only be
-       * a variable *)
-      let ctx = extract_typed_pattern ctx fmt true lv in
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt "<--";
-      F.pp_print_space fmt ();
-      extract_texpression ctx fmt false re;
-      F.pp_print_string fmt ";";
-      ctx)
-    else (
-      F.pp_print_string fmt "let";
-      F.pp_print_space fmt ();
-      let ctx = extract_typed_pattern ctx fmt true lv in
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt "=";
-      F.pp_print_space fmt ();
-      extract_texpression ctx fmt false re;
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt "in";
-      ctx)
-  in
-  (* Close the box for the let-binding *)
-  F.pp_close_box fmt ();
-  (* Print the next expression *)
-  F.pp_print_space fmt ();
-  extract_texpression ctx fmt false next_e;
-  (* Close parentheses *)
-  if inside then F.pp_print_string fmt ")";
-  (* Close the box for the whole expression *)
-  F.pp_close_box fmt ()
-
-and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
-    (scrut : texpression) (body : switch_body) : unit =
-  (* Open a box for the whole expression *)
-  F.pp_open_hvbox fmt 0;
-  (* Open parentheses *)
-  if inside then F.pp_print_string fmt "(";
-  (* Extract the switch *)
-  (match body with
-  | If (e_then, e_else) ->
-      (* Open a box for the [if] *)
-      F.pp_open_hovbox fmt ctx.indent_incr;
-      F.pp_print_string fmt "if";
-      F.pp_print_space fmt ();
-      let scrut_inside = PureUtils.let_group_requires_parentheses scrut in
-      extract_texpression ctx fmt scrut_inside scrut;
-      (* Close the box for the [if] *)
-      F.pp_close_box fmt ();
-      (* Extract the branches *)
-      let extract_branch (is_then : bool) (e_branch : texpression) : unit =
-        F.pp_print_space fmt ();
-        (* Open a box for the then/else+branch *)
-        F.pp_open_hovbox fmt ctx.indent_incr;
-        let then_or_else = if is_then then "then" else "else" in
-        F.pp_print_string fmt then_or_else;
-        F.pp_print_space fmt ();
-        (* Open a box for the branch *)
-        F.pp_open_hovbox fmt ctx.indent_incr;
-        (* Print the [begin] if necessary *)
-        let parenth = PureUtils.let_group_requires_parentheses e_branch in
-        if parenth then (
-          F.pp_print_string fmt "begin";
-          F.pp_print_space fmt ());
-        (* Print the branch expression *)
-        extract_texpression ctx fmt false e_branch;
-        (* Close the [begin ... end ] *)
-        if parenth then (
-          F.pp_print_space fmt ();
-          F.pp_print_string fmt "end");
-        (* Close the box for the branch *)
-        F.pp_close_box fmt ();
-        (* Close the box for the then/else+branch *)
-        F.pp_close_box fmt ()
-      in
-
-      extract_branch true e_then;
-      extract_branch false e_else
-  | Match branches ->
-      (* Open a box for the [match ... with] *)
-      F.pp_open_hovbox fmt ctx.indent_incr;
-      (* Print the [match ... with] *)
-      F.pp_print_string fmt "begin match";
-      F.pp_print_space fmt ();
-      let scrut_inside = PureUtils.let_group_requires_parentheses scrut in
-      extract_texpression ctx fmt scrut_inside scrut;
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt "with";
-      (* Close the box for the [match ... with] *)
-      F.pp_close_box fmt ();
-
-      (* Extract the branches *)
-      let extract_branch (br : match_branch) : unit =
-        F.pp_print_space fmt ();
-        (* Open a box for the pattern+branch *)
-        F.pp_open_hovbox fmt ctx.indent_incr;
-        F.pp_print_string fmt "|";
-        (* Print the pattern *)
-        F.pp_print_space fmt ();
-        let ctx = extract_typed_pattern ctx fmt false br.pat in
-        F.pp_print_space fmt ();
-        F.pp_print_string fmt "->";
-        F.pp_print_space fmt ();
-        (* Open a box for the branch *)
-        F.pp_open_hovbox fmt ctx.indent_incr;
-        (* Print the branch itself *)
-        extract_texpression ctx fmt false br.branch;
-        (* Close the box for the branch *)
-        F.pp_close_box fmt ();
-        (* Close the box for the pattern+branch *)
-        F.pp_close_box fmt ()
-      in
-
-      List.iter extract_branch branches;
-
-      (* End the match *)
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt "end");
-  (* Close parentheses *)
-  if inside then F.pp_print_string fmt ")";
-  (* Close the box for the whole expression *)
-  F.pp_close_box fmt ()
-
-(** A small utility to print the parameters of a function signature.
-
-    We return two contexts:
-    - the context augmented with bindings for the type parameters
-    - the previous context augmented with bindings for the input values
- *)
-let extract_fun_parameters (ctx : extraction_ctx) (fmt : F.formatter)
-    (def : fun_decl) : extraction_ctx * extraction_ctx =
-  (* Add the type parameters - note that we need those bindings only for the
-   * body translation (they are not top-level) *)
-  let ctx, _ = ctx_add_type_params def.signature.type_params ctx in
-  (* Print the parameters - rk.: we should have filtered the functions
-   * with no input parameters *)
-  (* The type parameters *)
-  if def.signature.type_params <> [] then (
-    (* Open a box for the type parameters *)
-    F.pp_open_hovbox fmt 0;
-    F.pp_print_string fmt "(";
-    List.iter
-      (fun (p : type_var) ->
-        let pname = ctx_get_type_var p.index ctx in
-        F.pp_print_string fmt pname;
-        F.pp_print_space fmt ())
-      def.signature.type_params;
-    F.pp_print_string fmt ":";
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "Type0)";
-    (* Close the box for the type parameters *)
-    F.pp_close_box fmt ();
-    F.pp_print_space fmt ());
-  (* The input parameters - note that doing this adds bindings to the context *)
-  let ctx_body =
-    match def.body with
-    | None -> ctx
-    | Some body ->
-        List.fold_left
-          (fun ctx (lv : typed_pattern) ->
-            (* Open a box for the input parameter *)
-            F.pp_open_hovbox fmt 0;
-            F.pp_print_string fmt "(";
-            let ctx = extract_typed_pattern ctx fmt false lv in
-            F.pp_print_space fmt ();
-            F.pp_print_string fmt ":";
-            F.pp_print_space fmt ();
-            extract_ty ctx fmt false lv.ty;
-            F.pp_print_string fmt ")";
-            (* Close the box for the input parameters *)
-            F.pp_close_box fmt ();
-            F.pp_print_space fmt ();
-            ctx)
-          ctx body.inputs_lvs
-  in
-  (ctx, ctx_body)
-
-(** A small utility to print the types of the input parameters in the form:
-    [u32 -> list u32 -> ...]
-    (we don't print the return type of the function)
-    
-    This is used for opaque function declarations, in particular.
- *)
-let extract_fun_input_parameters_types (ctx : extraction_ctx)
-    (fmt : F.formatter) (def : fun_decl) : unit =
-  let extract_param (ty : ty) : unit =
-    let inside = false in
-    extract_ty ctx fmt inside ty;
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "->";
-    F.pp_print_space fmt ()
-  in
-  List.iter extract_param def.signature.inputs
-
-(** Extract a decrease clause function template body.
-
-    In order to help the user, we can generate a template for the functions
-    required by the decreases clauses. We simply generate definitions of
-    the following form in a separate file:
-    {[
-      let f_decrease (t : Type0) (x : t) : nat = admit()
-    ]}
-    
-    Where the translated functions for [f] look like this:
-    {[
-      let f_fwd (t : Type0) (x : t) : Tot ... (decreases (f_decrease t x)) = ...
-    ]}
- *)
-let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
-    (def : fun_decl) : unit =
-  (* Retrieve the function name *)
-  let def_name = ctx_get_decreases_clause def.def_id ctx in
-  (* Add a break before *)
-  F.pp_print_break fmt 0 0;
-  (* Print a comment to link the extracted type to its original rust definition *)
-  F.pp_print_string fmt
-    ("(** [" ^ Print.fun_name_to_string def.basename ^ "]: decreases clause *)");
-  F.pp_print_space fmt ();
-  (* Open a box for the definition, so that whenever possible it gets printed on
-   * one line *)
-  F.pp_open_hvbox fmt 0;
-  (* Add the [unfold] keyword *)
-  F.pp_print_string fmt "unfold";
-  F.pp_print_space fmt ();
-  (* Open a box for "let FUN_NAME (PARAMS) : EFFECT = admit()" *)
-  F.pp_open_hvbox fmt ctx.indent_incr;
-  (* Open a box for "let FUN_NAME (PARAMS) : EFFECT =" *)
-  F.pp_open_hovbox fmt ctx.indent_incr;
-  (* > "let FUN_NAME" *)
-  F.pp_print_string fmt ("let " ^ def_name);
-  F.pp_print_space fmt ();
-  (* Extract the parameters *)
-  let _, _ = extract_fun_parameters ctx fmt def in
-  F.pp_print_string fmt ":";
-  (* Print the signature *)
-  F.pp_print_space fmt ();
-  F.pp_print_string fmt "nat";
-  (* Print the "=" *)
-  F.pp_print_space fmt ();
-  F.pp_print_string fmt "=";
-  (* Close the box for "let FUN_NAME (PARAMS) : EFFECT =" *)
-  F.pp_close_box fmt ();
-  F.pp_print_space fmt ();
-  (* Print the "admit ()" *)
-  F.pp_print_string fmt "admit ()";
-  (* Close the box for "let FUN_NAME (PARAMS) : EFFECT = admit()" *)
-  F.pp_close_box fmt ();
-  (* Close the box for the whole definition *)
-  F.pp_close_box fmt ();
-  (* Add breaks to insert new lines between definitions *)
-  F.pp_print_break fmt 0 0
-
-(** Extract a function declaration.
-
-    Note that all the names used for extraction should already have been
-    registered.
-    
-    We take the definition of the forward translation as parameter (which is
-    equal to the definition to extract, if we extract a forward function) because
-    it is useful for the decrease clause.
- *)
-let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
-    (qualif : fun_decl_qualif) (has_decreases_clause : bool) (def : fun_decl) :
-    unit =
-  assert (not def.is_global_decl_body);
-  (* Retrieve the function name *)
-  let def_name = ctx_get_local_function def.def_id def.back_id ctx in
-  (* (* Add the type parameters - note that we need those bindings only for the
-     * body translation (they are not top-level) *)
-      let ctx, _ = ctx_add_type_params def.signature.type_params ctx in *)
-  (* Add a break before *)
-  F.pp_print_break fmt 0 0;
-  (* Print a comment to link the extracted type to its original rust definition *)
-  F.pp_print_string fmt
-    ("(** [" ^ Print.fun_name_to_string def.basename ^ "] *)");
-  F.pp_print_space fmt ();
-  (* Open a box for the definition, so that whenever possible it gets printed on
-   * one line *)
-  F.pp_open_hvbox fmt ctx.indent_incr;
-  (* Open a box for "let FUN_NAME (PARAMS) : EFFECT =" *)
-  F.pp_open_hovbox fmt ctx.indent_incr;
-  (* > "let FUN_NAME" *)
-  let is_opaque = Option.is_none def.body in
-  let qualif = fun_decl_qualif_keyword qualif in
-  F.pp_print_string fmt (qualif ^ " " ^ def_name);
-  F.pp_print_space fmt ();
-  (* Open a box for "(PARAMS) : EFFECT =" *)
-  F.pp_open_hvbox fmt 0;
-  (* Open a box for "(PARAMS)" *)
-  F.pp_open_hovbox fmt 0;
-  let ctx, ctx_body = extract_fun_parameters ctx fmt def in
-  (* Close the box for "(PARAMS)" *)
-  F.pp_close_box fmt ();
-  (* Print the return type - note that we have to be careful when
-   * printing the input values for the decrease clause, because
-   * it introduces bindings in the context... We thus "forget"
-   * the bindings we introduced above.
-   * TODO: figure out a cleaner way *)
-  let _ =
-    F.pp_print_string fmt ":";
-    F.pp_print_space fmt ();
-    (* Open a box for the EFFECT *)
-    F.pp_open_hvbox fmt 0;
-    (* Open a box for the return type *)
-    F.pp_open_hovbox fmt ctx.indent_incr;
-    (* Print the return type *)
-    (* For opaque definitions, as we don't have named parameters under the hand,
-     * we don't print parameters in the form [(x : a) (y : b) ...] above,
-     * but wait until here to print the types: [a -> b -> ...]. *)
-    if is_opaque then extract_fun_input_parameters_types ctx fmt def;
-    (* [Tot] *)
-    if has_decreases_clause then (
-      F.pp_print_string fmt "Tot";
-      F.pp_print_space fmt ());
-    extract_ty ctx fmt has_decreases_clause def.signature.output;
-    (* Close the box for the return type *)
-    F.pp_close_box fmt ();
-    (* Print the decrease clause - rk.: a function with a decreases clause
-     * is necessarily a transparent function *)
-    if has_decreases_clause then (
-      F.pp_print_space fmt ();
-      (* Open a box for the decrease clause *)
-      F.pp_open_hovbox fmt 0;
-      (* *)
-      F.pp_print_string fmt "(decreases";
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt "(";
-      (* The name of the decrease clause *)
-      let decr_name = ctx_get_decreases_clause def.def_id ctx in
-      F.pp_print_string fmt decr_name;
-      (* Print the type parameters *)
-      List.iter
-        (fun (p : type_var) ->
-          let pname = ctx_get_type_var p.index ctx in
-          F.pp_print_space fmt ();
-          F.pp_print_string fmt pname)
-        def.signature.type_params;
-      (* Print the input values: we have to be careful here to print
-       * only the input values which are in common with the *forward*
-       * function (the additional input values "given back" to the
-       * backward functions have no influence on termination: we thus
-       * share the decrease clauses between the forward and the backward
-       * functions - we also ignore the additional state received by the
-       * backward function, if there is one).
-       *)
-      let inputs_lvs =
-        let all_inputs = (Option.get def.body).inputs_lvs in
-        let num_fwd_inputs = def.signature.info.num_fwd_inputs_with_state in
-        Collections.List.prefix num_fwd_inputs all_inputs
-      in
-      let _ =
-        List.fold_left
-          (fun ctx (lv : typed_pattern) ->
-            F.pp_print_space fmt ();
-            let ctx = extract_typed_pattern ctx fmt false lv in
-            ctx)
-          ctx inputs_lvs
-      in
-      F.pp_print_string fmt "))";
-      (* Close the box for the decrease clause *)
-      F.pp_close_box fmt ());
-    (* Close the box for the EFFECT *)
-    F.pp_close_box fmt ()
-  in
-  (* Print the "=" *)
-  if not is_opaque then (
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "=");
-  (* Close the box for "(PARAMS) : EFFECT =" *)
-  F.pp_close_box fmt ();
-  (* Close the box for "let FUN_NAME (PARAMS) : EFFECT =" *)
-  F.pp_close_box fmt ();
-  if not is_opaque then (
-    F.pp_print_space fmt ();
-    (* Open a box for the body *)
-    F.pp_open_hvbox fmt 0;
-    (* Extract the body *)
-    let _ = extract_texpression ctx_body fmt false (Option.get def.body).body in
-    (* Close the box for the body *)
-    F.pp_close_box fmt ());
-  (* Close the box for the definition *)
-  F.pp_close_box fmt ();
-  (* Add breaks to insert new lines between definitions *)
-  F.pp_print_break fmt 0 0
-
-(** Extract a global declaration body of the shape "QUALIF NAME : TYPE = BODY" with a custom body extractor *)
-let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter)
-    (qualif : fun_decl_qualif) (name : string) (ty : ty)
-    (extract_body : (F.formatter -> unit) Option.t) : unit =
-  let is_opaque = Option.is_none extract_body in
-
-  (* Open the definition box (depth=0) *)
-  F.pp_open_hvbox fmt ctx.indent_incr;
-
-  (* Open "QUALIF NAME : TYPE =" box (depth=1) *)
-  F.pp_open_hovbox fmt ctx.indent_incr;
-  (* Print "QUALIF NAME " *)
-  F.pp_print_string fmt (fun_decl_qualif_keyword qualif ^ " " ^ name);
-  F.pp_print_space fmt ();
-
-  (* Open ": TYPE =" box (depth=2) *)
-  F.pp_open_hvbox fmt 0;
-  (* Print ": " *)
-  F.pp_print_string fmt ":";
-  F.pp_print_space fmt ();
-
-  (* Open "TYPE" box (depth=3) *)
-  F.pp_open_hovbox fmt ctx.indent_incr;
-  (* Print "TYPE" *)
-  extract_ty ctx fmt false ty;
-  (* Close "TYPE" box (depth=3) *)
-  F.pp_close_box fmt ();
-
-  if not is_opaque then (
-    (* Print " =" *)
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "=");
-  (* Close ": TYPE =" box (depth=2) *)
-  F.pp_close_box fmt ();
-  (* Close "QUALIF NAME : TYPE =" box (depth=1) *)
-  F.pp_close_box fmt ();
-
-  if not is_opaque then (
-    F.pp_print_space fmt ();
-    (* Open "BODY" box (depth=1) *)
-    F.pp_open_hvbox fmt 0;
-    (* Print "BODY" *)
-    (Option.get extract_body) fmt;
-    (* Close "BODY" box (depth=1) *)
-    F.pp_close_box fmt ());
-  (* Close the definition box (depth=0) *)
-  F.pp_close_box fmt ()
-
-(** Extract a global declaration.
-    We generate the body which computes the global value separately from the value declaration itself.
-
-    For example in Rust,
-    [static X: u32 = 3;]
-
-    will be translated to:
-    [let x_body : result u32 = Return 3]
-    [let x_c : u32 = eval_global x_body]
- *)
-let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
-    (global : A.global_decl) (body : fun_decl) (interface : bool) : unit =
-  assert body.is_global_decl_body;
-  assert (Option.is_none body.back_id);
-  assert (List.length body.signature.inputs = 0);
-  assert (List.length body.signature.doutputs = 1);
-  assert (List.length body.signature.type_params = 0);
-
-  (* Add a break then the name of the corresponding LLBC declaration *)
-  F.pp_print_break fmt 0 0;
-  F.pp_print_string fmt
-    ("(** [" ^ Print.global_name_to_string global.name ^ "] *)");
-  F.pp_print_space fmt ();
-
-  let decl_name = ctx_get_global global.def_id ctx in
-  let body_name =
-    ctx_get_function (FromLlbc (Regular global.body_id, None)) ctx
-  in
-
-  let decl_ty, body_ty =
-    let ty = body.signature.output in
-    if body.signature.info.effect_info.can_fail then (unwrap_result_ty ty, ty)
-    else (ty, mk_result_ty ty)
-  in
-  match body.body with
-  | None ->
-      let qualif = if interface then Val else AssumeVal in
-      extract_global_decl_body ctx fmt qualif decl_name decl_ty None
-  | Some body ->
-      extract_global_decl_body ctx fmt Let body_name body_ty
-        (Some (fun fmt -> extract_texpression ctx fmt false body.body));
-      F.pp_print_break fmt 0 0;
-      extract_global_decl_body ctx fmt Let decl_name decl_ty
-        (Some (fun fmt -> F.pp_print_string fmt ("eval_global " ^ body_name)));
-      F.pp_print_break fmt 0 0
-
-(** Extract a unit test, if the function is a unit function (takes no
-    parameters, returns unit).
-    
-    A unit test simply checks that the function normalizes to [Return ()]:
-    {[
-      let _ = assert_norm (FUNCTION () = Return ())
-    ]}
- *)
-let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
-    (def : fun_decl) : unit =
-  (* We only insert unit tests for forward functions *)
-  assert (def.back_id = None);
-  (* Check if this is a unit function *)
-  let sg = def.signature in
-  if
-    sg.type_params = []
-    && (sg.inputs = [ mk_unit_ty ] || sg.inputs = [])
-    && sg.output = mk_result_ty mk_unit_ty
-  then (
-    (* Add a break before *)
-    F.pp_print_break fmt 0 0;
-    (* Print a comment *)
-    F.pp_print_string fmt
-      ("(** Unit test for [" ^ Print.fun_name_to_string def.basename ^ "] *)");
-    F.pp_print_space fmt ();
-    (* Open a box for the test *)
-    F.pp_open_hovbox fmt ctx.indent_incr;
-    (* Print the test *)
-    F.pp_print_string fmt "let _ =";
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "assert_norm";
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "(";
-    let fun_name = ctx_get_local_function def.def_id def.back_id ctx in
-    F.pp_print_string fmt fun_name;
-    if sg.inputs <> [] then (
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt "()");
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "=";
-    F.pp_print_space fmt ();
-    let success = ctx_get_variant (Assumed Result) result_return_id ctx in
-    F.pp_print_string fmt (success ^ " ())");
-    (* Close the box for the test *)
-    F.pp_close_box fmt ();
-    (* Add a break after *)
-    F.pp_print_break fmt 0 0)
-  else (* Do nothing *)
-    ()
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index fda2b3a6..b0114baa 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -500,7 +500,7 @@ type fun_effect_info = {
       (** [true] if the function group is stateful. By *function group*, we mean
           the set [{ forward function } U { backward functions }].
 
-          We need this because of the option {!Config.backward_no_state_update}:
+          We need this because of the option {!val:Config.backward_no_state_update}:
           if it is [true], then in case of a backward function {!stateful} is [false],
           but we might need to know whether the corresponding forward function
           is stateful or not.
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 132dc02e..30fc4989 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1083,7 +1083,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
 
 (** Decompose the monadic let-bindings.
 
-    See the explanations in {!Config.decompose_monadic_let_bindings}
+    See the explanations in {!val:Config.decompose_monadic_let_bindings}
  *)
 let decompose_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) :
     fun_decl =
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 0f16b5b4..ff55f322 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -73,7 +73,7 @@ let make_type_subst (vars : type_var list) (tys : ty list) : TypeVarId.id -> ty
   in
   fun id -> TypeVarId.Map.find id mp
 
-(** Retrieve the list of fields for the given variant of a {!type:Pure.type_decl}.
+(** Retrieve the list of fields for the given variant of a {!type:Aeneas.Pure.type_decl}.
 
     Raises [Invalid_argument] if the arguments are incorrect.
  *)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 0171412b..79d1c913 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -343,7 +343,7 @@ let module_has_opaque_decls (ctx : gen_ctx) : bool * bool =
 let extract_definitions (fmt : Format.formatter) (config : gen_config)
     (ctx : gen_ctx) : unit =
   (* Export the definition groups to the file, in the proper order *)
-  let export_type (qualif : ExtractToFStar.type_decl_qualif)
+  let export_type (qualif : ExtractToBackend.type_decl_qualif)
       (id : Pure.TypeDeclId.id) : unit =
     (* Retrive the declaration *)
     let def = Pure.TypeDeclId.Map.find id ctx.trans_types in
@@ -353,8 +353,8 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
       | Enum _ | Struct _ -> (false, qualif)
       | Opaque ->
           let qualif =
-            if config.interface then ExtractToFStar.TypeVal
-            else ExtractToFStar.AssumeType
+            if config.interface then ExtractToBackend.TypeVal
+            else ExtractToBackend.AssumeType
           in
           (true, qualif)
     in
@@ -363,7 +363,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
     if
       (is_opaque && config.extract_opaque)
       || ((not is_opaque) && config.extract_transparent)
-    then ExtractToFStar.extract_type_decl ctx.extract_ctx fmt qualif def
+    then ExtractToBackend.extract_type_decl ctx.extract_ctx fmt qualif def
   in
 
   (* Utility to check a function has a decrease clause *)
@@ -393,7 +393,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
         (fun (_, (fwd, _)) ->
           let has_decr_clause = has_decreases_clause fwd in
           if has_decr_clause then
-            ExtractToFStar.extract_template_decreases_clause ctx.extract_ctx fmt
+            ExtractToBackend.extract_template_decreases_clause ctx.extract_ctx fmt
               fwd)
         pure_ls;
     (* Extract the function definitions *)
@@ -413,12 +413,12 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
          let is_opaque = Option.is_none fwd_def.Pure.body in
          let qualif =
            if is_opaque then
-             if config.interface then ExtractToFStar.Val
-             else ExtractToFStar.AssumeVal
-           else if not is_rec then ExtractToFStar.Let
+             if config.interface then ExtractToBackend.Val
+             else ExtractToBackend.AssumeVal
+           else if not is_rec then ExtractToBackend.Let
            else if is_mut_rec then
-             if i = 0 then ExtractToFStar.LetRec else ExtractToFStar.And
-           else ExtractToFStar.LetRec
+             if i = 0 then ExtractToBackend.LetRec else ExtractToBackend.And
+           else ExtractToBackend.LetRec
          in
          let has_decr_clause =
            has_decreases_clause def && config.extract_decreases_clauses
@@ -428,7 +428,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
            ((not is_opaque) && config.extract_transparent)
            || (is_opaque && config.extract_opaque)
          then
-           ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif
+           ExtractToBackend.extract_fun_decl ctx.extract_ctx fmt qualif
              has_decr_clause def)
        fls);
     (* Insert unit tests if necessary *)
@@ -436,7 +436,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
       List.iter
         (fun (keep_fwd, (fwd, _)) ->
           if keep_fwd then
-            ExtractToFStar.extract_unit_test_if_unit_fun ctx.extract_ctx fmt fwd)
+            ExtractToBackend.extract_unit_test_if_unit_fun ctx.extract_ctx fmt fwd)
         pure_ls
   in
 
@@ -454,29 +454,29 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
       ((not is_opaque) && config.extract_transparent)
       || (is_opaque && config.extract_opaque)
     then
-      ExtractToFStar.extract_global_decl ctx.extract_ctx fmt global body
+      ExtractToBackend.extract_global_decl ctx.extract_ctx fmt global body
         config.interface
   in
 
   let export_state_type () : unit =
     let qualif =
-      if config.interface then ExtractToFStar.TypeVal
-      else ExtractToFStar.AssumeType
+      if config.interface then ExtractToBackend.TypeVal
+      else ExtractToBackend.AssumeType
     in
-    ExtractToFStar.extract_state_type fmt ctx.extract_ctx qualif
+    ExtractToBackend.extract_state_type fmt ctx.extract_ctx qualif
   in
 
   let export_decl (decl : A.declaration_group) : unit =
     match decl with
     | Type (NonRec id) ->
-        if config.extract_types then export_type ExtractToFStar.Type id
+        if config.extract_types then export_type ExtractToBackend.Type id
     | Type (Rec ids) ->
         (* Rk.: we shouldn't have (mutually) recursive opaque types *)
         if config.extract_types then
           List.iteri
             (fun i id ->
               let qualif =
-                if i = 0 then ExtractToFStar.Type else ExtractToFStar.And
+                if i = 0 then ExtractToBackend.Type else ExtractToBackend.And
               in
               export_type qualif id)
             ids
@@ -569,12 +569,12 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
    * language, as well as some primitive names ("u32", etc.) *)
   let variant_concatenate_type_name = true in
   let fstar_fmt =
-    ExtractToFStar.mk_formatter trans_ctx crate.name
+    ExtractToBackend.mk_formatter trans_ctx crate.name
       variant_concatenate_type_name
   in
   let names_map =
     PureToExtract.initialize_names_map fstar_fmt
-      ExtractToFStar.fstar_names_map_init
+      ExtractToBackend.fstar_names_map_init
   in
   let ctx =
     { PureToExtract.trans_ctx; names_map; fmt = fstar_fmt; indent_incr = 2 }
@@ -596,7 +596,7 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
    * sure there are no name clashes. *)
   let ctx =
     List.fold_left
-      (fun ctx def -> ExtractToFStar.extract_type_decl_register_names ctx def)
+      (fun ctx def -> ExtractToBackend.extract_type_decl_register_names ctx def)
       ctx trans_types
   in
 
@@ -612,13 +612,13 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
         let is_global = (fst def).Pure.is_global_decl_body in
         if is_global then ctx
         else
-          ExtractToFStar.extract_fun_decl_register_names ctx keep_fwd
+          ExtractToBackend.extract_fun_decl_register_names ctx keep_fwd
             gen_decr_clause def)
       ctx trans_funs
   in
 
   let ctx =
-    List.fold_left ExtractToFStar.extract_global_decl_register_names ctx
+    List.fold_left ExtractToBackend.extract_global_decl_register_names ctx
       crate.globals
   in
 
diff --git a/compiler/dune b/compiler/dune
index 85f4b75b..10aa9b10 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -20,7 +20,7 @@
   Cps
   Expressions
   ExpressionsUtils
-  ExtractToFStar
+  ExtractToBackend
   FunsAnalysis
   Identifiers
   InterpreterBorrowsCore
-- 
cgit v1.2.3