Make minor fixes, improve formatting for Lean and generate code for all the test suite

3 files changed, 203 insertions, 177 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 24f8d141..1057cc3b 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -17,9 +17,9 @@ let int_name (int_ty : integer_type) =
   let isize, usize, i_format, u_format =
     match !backend with
     | FStar | Coq ->
-        "isize", "usize", format_of_string "i%d", format_of_string "u%d"
+        ("isize", "usize", format_of_string "i%d", format_of_string "u%d")
     | Lean ->
-        "ISize", "USize", format_of_string "Int%d", format_of_string "UInt%d"
+        ("ISize", "USize", format_of_string "Int%d", format_of_string "UInt%d")
   in
   match int_ty with
   | Isize -> isize
@@ -39,11 +39,10 @@ let int_name (int_ty : integer_type) =
 let unop_name (unop : unop) : string =
   match unop with
   | Not -> ( match !backend with FStar | Lean -> "not" | Coq -> "negb")
-  | Neg (int_ty: integer_type) ->
-      begin match !backend with
+  | Neg (int_ty : integer_type) -> (
+      match !backend with
       | Lean -> int_name int_ty ^ ".checked_neg"
-      | _ -> int_name int_ty ^ "_neg"
-      end
+      | _ -> int_name int_ty ^ "_neg")
   | Cast _ -> raise (Failure "Unsupported")
 
 (** Small helper to compute the name of a binary operation (note that many
@@ -74,8 +73,8 @@ let keywords () =
   let named_binops = [ E.Div; Rem; Add; Sub; Mul ] in
   let named_binops =
     List.concat_map
-       (fun bn -> List.map (fun it -> named_binop_name bn it) T.all_int_types)
-       named_binops
+      (fun bn -> List.map (fun it -> named_binop_name bn it) T.all_int_types)
+      named_binops
   in
   let misc =
     match !backend with
@@ -132,8 +131,7 @@ let keywords () =
           "tt";
           "char_of_byte";
         ]
-    | Lean ->
-        [] (* TODO *)
+    | Lean -> [] (* TODO *)
   in
   List.concat [ named_unops; named_binops; misc ]
 
@@ -202,7 +200,7 @@ let assumed_llbc_functions :
     (VecIndexMut, rg0, "vec_index_mut_back");
   ]
 
-let assumed_pure_functions (): (pure_assumed_fun_id * string) list =
+let assumed_pure_functions () : (pure_assumed_fun_id * string) list =
   match !backend with
   | FStar ->
       [
@@ -251,14 +249,12 @@ let extract_unop (extract_expr : bool -> texpression -> unit)
       if inside then F.pp_print_string fmt "(";
       F.pp_print_string fmt "scalar_cast";
       F.pp_print_space fmt ();
-      if !backend <> Lean then begin
+      if !backend <> Lean then (
         F.pp_print_string fmt
           (StringUtils.capitalize_first_letter
              (PrintPure.integer_type_to_string src));
-        F.pp_print_space fmt ()
-      end;
-      if !backend = Lean then
-        F.pp_print_string fmt (int_name tgt)
+        F.pp_print_space fmt ());
+      if !backend = Lean then F.pp_print_string fmt (int_name tgt)
       else
         F.pp_print_string fmt
           (StringUtils.capitalize_first_letter
@@ -284,7 +280,9 @@ let extract_binop (extract_expr : bool -> texpression -> unit)
         | Gt -> ">"
         | _ -> raise (Failure "Unreachable")
       in
-      let binop = match !backend with FStar | Lean -> binop | Coq -> "s" ^ binop in
+      let binop =
+        match !backend with FStar | Lean -> binop | Coq -> "s" ^ binop
+      in
       extract_expr false arg0;
       F.pp_print_space fmt ();
       F.pp_print_string fmt binop;
@@ -301,7 +299,7 @@ let extract_binop (extract_expr : bool -> texpression -> unit)
   if inside then F.pp_print_string fmt ")"
 
 let type_decl_kind_to_qualif (kind : decl_kind)
-    (type_kind : type_decl_kind option): string =
+    (type_kind : type_decl_kind option) : string =
   match !backend with
   | FStar -> (
       match kind with
@@ -326,7 +324,8 @@ let type_decl_kind_to_qualif (kind : decl_kind)
       | _ -> raise (Failure "Unexpected"))
   | Lean -> (
       match kind with
-      | SingleNonRec -> if type_kind = Some Struct then "structure" else "inductive"
+      | SingleNonRec ->
+          if type_kind = Some Struct then "structure" else "inductive"
       | SingleRec -> "inductive"
       | MutRecFirst -> "mutual inductive"
       | MutRecInner -> "inductive"
@@ -364,7 +363,6 @@ let fun_decl_kind_to_qualif (kind : decl_kind) =
       | Assumed -> "axiom"
       | Declared -> "axiom")
 
-
 (**
    [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
@@ -439,7 +437,9 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     let name = get_type_name name in
     let name = List.map to_snake_case name in
     let name = String.concat "_" name in
-    match !backend with FStar | Lean -> name | Coq -> capitalize_first_letter name
+    match !backend with
+    | FStar | Lean -> name
+    | Coq -> capitalize_first_letter name
   in
   let type_name name = type_name_to_snake_case name ^ "_t" in
   let field_name (def_name : name) (field_id : FieldId.id)
@@ -587,7 +587,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
             F.pp_print_string fmt (int_name sv.int_ty);
             F.pp_print_string fmt ".ofNatCore ";
             Z.pp_print fmt sv.value;
-            F.pp_print_string fmt (" (by intlit))"))
+            F.pp_print_string fmt " (by intlit))")
     | Bool b ->
         let b = if b then "true" else "false" in
         F.pp_print_string fmt b
@@ -607,7 +607,6 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
             in
             F.pp_print_string fmt c;
             if inside then F.pp_print_string fmt ")")
-
     | String s ->
         (* We need to replace all the line breaks *)
         let s =
@@ -655,8 +654,7 @@ let print_decl_end_delimiter (fmt : F.formatter) (kind : decl_kind) =
     F.pp_print_cut fmt ();
     F.pp_print_string fmt ".")
 
-let unit_name () =
-  match !backend with | Lean -> "Unit" | Coq | FStar -> "unit"
+let unit_name () = match !backend with Lean -> "Unit" | Coq | FStar -> "unit"
 
 (** [inside] constrols whether we should add parentheses or not around type
     applications (if [true] we add parentheses).
@@ -675,7 +673,9 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
             Collections.List.iter_link
               (fun () ->
                 F.pp_print_space fmt ();
-                let product = match !backend with FStar -> "&" | Coq -> "*" | Lean -> "×" in
+                let product =
+                  match !backend with FStar -> "&" | Coq -> "*" | Lean -> "×"
+                in
                 F.pp_print_string fmt product;
                 F.pp_print_space fmt ())
               (extract_ty ctx fmt true) tys;
@@ -906,8 +906,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
       if !backend = Coq && not is_rec then (
         F.pp_print_string fmt (ctx_get_struct (AdtId def.def_id) ctx);
         F.pp_print_string fmt " ");
-      if !backend <> Lean then
-        F.pp_print_string fmt "{";
+      if !backend <> Lean then F.pp_print_string fmt "{";
       F.pp_print_break fmt 1 ctx.indent_incr;
       (* The body itself *)
       F.pp_open_hvbox fmt 0;
@@ -920,8 +919,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
         F.pp_print_string fmt ":";
         F.pp_print_space fmt ();
         extract_ty ctx fmt false f.field_ty;
-        if !backend <> Lean then
-          F.pp_print_string fmt ";";
+        if !backend <> Lean then F.pp_print_string fmt ";";
         F.pp_close_box fmt ()
       in
       let fields = FieldId.mapi (fun fid f -> (fid, f)) fields in
@@ -931,8 +929,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
       (* Close *)
       F.pp_close_box fmt ();
       F.pp_print_space fmt ();
-      if !backend <> Lean then
-        F.pp_print_string fmt "}")
+      if !backend <> Lean then F.pp_print_string fmt "}")
     else (
       (* We extract for Coq, and we have a recursive record, or a record in
          a group of mutually recursive types: we extract it as an inductive type
@@ -945,12 +942,12 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
   ()
 
 (** Extract a nestable, muti-line comment *)
-let extract_comment (fmt: F.formatter) (s: string): unit =
+let extract_comment (fmt : F.formatter) (s : string) : unit =
   match !backend with
   | Coq | FStar ->
       F.pp_print_string fmt "(** ";
       F.pp_print_string fmt s;
-      F.pp_print_string fmt " *)";
+      F.pp_print_string fmt " *)"
   | Lean ->
       F.pp_print_string fmt "/- ";
       F.pp_print_string fmt s;
@@ -1002,7 +999,9 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
   let qualif = ctx.fmt.type_decl_kind_to_qualif kind type_kind in
   F.pp_print_string fmt (qualif ^ " " ^ def_name);
   (* Print the type parameters *)
-  let type_keyword = match !backend with FStar -> "Type0" | Coq | Lean -> "Type" in
+  let type_keyword =
+    match !backend with FStar -> "Type0" | Coq | Lean -> "Type"
+  in
   if def.type_params <> [] then (
     if use_forall then (
       F.pp_print_space fmt ();
@@ -1023,10 +1022,13 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Print the "=" if we extract the body*)
   if extract_body then (
     F.pp_print_space fmt ();
-    let eq = match !backend with
+    let eq =
+      match !backend with
       | FStar -> "="
       | Coq -> ":="
-      | Lean -> if type_kind = Some Struct && kind = SingleNonRec then "where" else ":="
+      | Lean ->
+          if type_kind = Some Struct && kind = SingleNonRec then "where"
+          else ":="
     in
     F.pp_print_string fmt eq)
   else (
@@ -1307,18 +1309,15 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
   let state_name = ctx_get_assumed_type State ctx in
   (* The syntax for Lean and Coq is almost identical. *)
   let print_axiom () =
-    if !backend = Coq then
-      F.pp_print_string fmt "Axiom"
-    else
-      F.pp_print_string fmt "axiom";
+    if !backend = Coq then F.pp_print_string fmt "Axiom"
+    else F.pp_print_string fmt "axiom";
     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 "Type";
-    if !backend = Coq then
-      F.pp_print_string fmt "."
+    if !backend = Coq then F.pp_print_string fmt "."
   in
   (* The kind should be [Assumed] or [Declared] *)
   (match kind with
@@ -1336,8 +1335,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
           F.pp_print_string fmt ":";
           F.pp_print_space fmt ();
           F.pp_print_string fmt "Type0"
-      | Coq | Lean ->
-          print_axiom ())
+      | Coq | Lean -> print_axiom ())
   | Declared -> (
       match !backend with
       | FStar ->
@@ -1348,8 +1346,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
           F.pp_print_string fmt ":";
           F.pp_print_space fmt ();
           F.pp_print_string fmt "Type0"
-      | Coq | Lean ->
-          print_axiom ()));
+      | Coq | Lean -> print_axiom ()));
   (* Close the box for the definition *)
   F.pp_close_box fmt ();
   (* Add breaks to insert new lines between definitions *)
@@ -1367,8 +1364,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool)
     if has_decreases_clause def then
       let ctx = ctx_add_decreases_clause def ctx in
       ctx_add_terminates_clause def ctx
-    else
-      ctx
+    else ctx
   in
   let ctx = List.fold_left register_decreases ctx (fwd :: loop_fwds) in
   let register_fun ctx f = ctx_add_fun_decl (keep_fwd, def) f ctx in
@@ -1439,8 +1435,7 @@ let extract_adt_g_value
         | Some vid ->
             if !backend = Lean then
               ctx_get_type adt_id ctx ^ "." ^ ctx_get_variant adt_id vid ctx
-            else
-              ctx_get_variant adt_id vid ctx
+            else 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 "(";
@@ -1579,9 +1574,10 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
       (* Open a box for the function call *)
       F.pp_open_hovbox fmt ctx.indent_incr;
       (* Print the function name *)
-      let fun_name = Option.value
-        ~default:(ctx_get_function fun_id ctx)
-        (ctx_maybe_get (DeclaredId fun_id) ctx)
+      let fun_name =
+        Option.value
+          ~default:(ctx_get_function fun_id ctx)
+          (ctx_maybe_get (DeclaredId fun_id) ctx)
       in
       F.pp_print_string fmt fun_name;
       (* Print the type parameters *)
@@ -1641,18 +1637,26 @@ and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
         match adt_cons.variant_id with
         | Some vid ->
             if !backend = Lean then
-              ctx_get_type adt_cons.adt_id ctx ^ "." ^ ctx_get_variant adt_cons.adt_id vid ctx
-            else
-              ctx_get_variant adt_cons.adt_id vid ctx
+              ctx_get_type adt_cons.adt_id ctx
+              ^ "."
+              ^ ctx_get_variant adt_cons.adt_id vid ctx
+            else ctx_get_variant adt_cons.adt_id vid ctx
         | None -> ctx_get_struct adt_cons.adt_id ctx
       in
       let is_lean_struct = !backend = Lean && adt_cons.variant_id = None in
-      if is_lean_struct then
+      if is_lean_struct then (
         (* TODO: when only one or two fields differ, considering using the with
            syntax (peephole optimization) *)
-        let decl_id = match adt_cons.adt_id with | AdtId id -> id | _ -> assert false in
-        let def_kind = (TypeDeclId.Map.find decl_id ctx.trans_ctx.type_context.type_decls).kind in
-        let fields = match def_kind with | T.Struct fields -> fields | _ -> assert false in
+        let decl_id =
+          match adt_cons.adt_id with AdtId id -> id | _ -> assert false
+        in
+        let def_kind =
+          (TypeDeclId.Map.find decl_id ctx.trans_ctx.type_context.type_decls)
+            .kind
+        in
+        let fields =
+          match def_kind with T.Struct fields -> fields | _ -> assert false
+        in
         let fields = FieldId.mapi (fun fid f -> (fid, f)) fields in
         F.pp_open_hvbox fmt 0;
         F.pp_open_hvbox fmt ctx.indent_incr;
@@ -1663,8 +1667,7 @@ and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
         Collections.List.iter_link
           (fun () ->
             F.pp_print_string fmt ",";
-            F.pp_print_space fmt ()
-          )
+            F.pp_print_space fmt ())
           (fun ((fid, _), e) ->
             F.pp_open_hvbox fmt ctx.indent_incr;
             let f = ctx_get_field adt_cons.adt_id fid ctx in
@@ -1673,15 +1676,14 @@ and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
             F.pp_open_hvbox fmt ctx.indent_incr;
             extract_texpression ctx fmt true e;
             F.pp_close_box fmt ();
-            F.pp_close_box fmt ()
-          )
+            F.pp_close_box fmt ())
           (List.combine fields args);
         F.pp_close_box fmt ();
         F.pp_close_box fmt ();
         F.pp_close_box fmt ();
         F.pp_print_space fmt ();
         F.pp_print_string fmt "}";
-        F.pp_close_box fmt ()
+        F.pp_close_box fmt ())
       else
         let use_parentheses = inside && args <> [] in
         if use_parentheses then F.pp_print_string fmt "(";
@@ -1708,15 +1710,13 @@ and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter)
       (* Extract the expression *)
       extract_texpression ctx fmt true arg;
       (* We allow to break where the "." appears (except Lean, it's a syntax error) *)
-      if !backend <> Lean then
-        F.pp_print_break fmt 0 0;
+      if !backend <> Lean then F.pp_print_break fmt 0 0;
       F.pp_print_string fmt ".";
       (* If in Coq, the field projection has to be parenthesized *)
       (match !backend with
       | FStar -> F.pp_print_string fmt field_name
       | Coq -> F.pp_print_string fmt ("(" ^ field_name ^ ")")
-      | Lean -> F.pp_print_string fmt field_name
-      );
+      | Lean -> F.pp_print_string fmt field_name);
       (* Close the box *)
       F.pp_close_box fmt ()
   | arg :: args ->
@@ -1780,7 +1780,11 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
       if monadic && !backend = Coq then (
         let ctx = extract_typed_pattern ctx fmt true lv in
         F.pp_print_space fmt ();
-        let arrow = match !backend with FStar -> "<--" | Coq -> "<-" | Lean -> failwith "impossible" in
+        let arrow =
+          match !backend with
+          | Coq -> "<-"
+          | FStar | Lean -> failwith "impossible"
+        in
         F.pp_print_string fmt arrow;
         F.pp_print_space fmt ();
         extract_texpression ctx fmt false re;
@@ -1791,13 +1795,24 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
         F.pp_print_space fmt ();
         let ctx = extract_typed_pattern ctx fmt true lv in
         F.pp_print_space fmt ();
-        let eq = match !backend with FStar -> "=" | Coq -> ":=" | Lean -> if monadic then "<-" else ":=" in
+        let eq =
+          match !backend with
+          | FStar -> "="
+          | Coq -> ":="
+          | Lean -> if monadic then "<-" else ":="
+        in
         F.pp_print_string fmt eq;
         F.pp_print_space fmt ();
         extract_texpression ctx fmt false re;
-        F.pp_print_space fmt ();
-        if !backend <> Lean then
-          F.pp_print_string fmt "in";
+        (* In Lean, monadic let-bindings don't require to end with "in".
+
+           TODO: does this work because we add a line break? This is very annoying,
+           because we need to enforce there will be a line break. In order to fix
+           this, we should open a vbox instead of an hov_box.
+        *)
+        if !backend <> Lean then (
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "in");
         ctx)
     in
     (* Close the box for the let-binding *)
@@ -1809,11 +1824,10 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
   let exists_monadic = List.exists (fun (m, _, _) -> m) lets in
   (* If Lean, we rely on monadic blocks, so we insert a do and open a new box
      immediately *)
-  if !backend = Lean && exists_monadic then begin
+  if !backend = Lean && exists_monadic then (
     F.pp_open_vbox fmt ctx.indent_incr;
     F.pp_print_string fmt "do";
-    F.pp_print_space fmt ();
-  end;
+    F.pp_print_space fmt ());
   let ctx =
     List.fold_left
       (fun ctx (monadic, lv, re) -> extract_let ctx monadic lv re)
@@ -1826,8 +1840,7 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
   (* Close the box for the next expression *)
   F.pp_close_box fmt ();
   (* do-box (Lean only) *)
-  if !backend = Lean && exists_monadic then
-    F.pp_close_box fmt ();
+  if !backend = Lean && exists_monadic then F.pp_close_box fmt ();
   (* Close parentheses *)
   if inside && !backend <> Lean then F.pp_print_string fmt ")";
   (* Close the box for the whole expression *)
@@ -1874,9 +1887,7 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
          | Coq ->
              F.pp_print_string fmt " (";
              F.pp_print_cut fmt ()
-         | Lean ->
-             F.pp_print_cut fmt ()
-        );
+         | Lean -> F.pp_print_cut fmt ());
         (* Print the branch expression *)
         extract_texpression ctx fmt false e_branch;
         (* Close the parenthesized expression *)
@@ -1886,8 +1897,7 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
              F.pp_print_space fmt ();
              F.pp_print_string fmt "end"
          | Coq -> F.pp_print_string fmt ")"
-         | Lean -> ()
-        );
+         | Lean -> ());
         (* Close the box for the branch *)
         if not parenth then F.pp_close_box fmt ();
         (* Close the box for the then/else+branch *)
@@ -1940,8 +1950,7 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
       (* End the match *)
       F.pp_print_space fmt ();
       (* Relying on indentation in Lean *)
-      if !backend <> Lean then
-        F.pp_print_string fmt "end");
+      if !backend <> Lean then F.pp_print_string fmt "end");
   (* Close parentheses *)
   if inside then F.pp_print_string fmt ")";
   (* Close the box for the whole expression *)
@@ -1978,7 +1987,9 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
       def.signature.type_params;
     F.pp_print_string fmt ":";
     F.pp_print_space fmt ();
-    let type_keyword = match !backend with FStar -> "Type0" | Coq | Lean -> "Type" in
+    let type_keyword =
+      match !backend with FStar -> "Type0" | Coq | Lean -> "Type"
+    in
     F.pp_print_string fmt (type_keyword ^ ")");
     (* Close the box for the type parameters *)
     F.pp_close_box fmt ());
@@ -2053,7 +2064,8 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  extract_comment fmt ("[" ^ Print.fun_name_to_string def.basename ^ "]: decreases clause");
+  extract_comment 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 *)
@@ -2102,7 +2114,8 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
     defines a proof script (allowed to refer to function arguments) that proves
     termination.
 *)
-let extract_termination_and_decreasing (ctx: extraction_ctx) (fmt: F.formatter) (def: fun_decl): unit =
+let extract_termination_and_decreasing (ctx : extraction_ctx)
+    (fmt : F.formatter) (def : fun_decl) : unit =
   assert (!backend = Lean);
 
   (* Retrieve the function name *)
@@ -2111,7 +2124,8 @@ let extract_termination_and_decreasing (ctx: extraction_ctx) (fmt: F.formatter)
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  extract_comment fmt ("[" ^ Print.fun_name_to_string def.basename ^ "]: termination measure");
+  extract_comment fmt
+    ("[" ^ Print.fun_name_to_string def.basename ^ "]: termination measure");
   F.pp_print_space fmt ();
   (* Open a box for the definition, so that whenever possible it gets printed on
    * one line *)
@@ -2136,11 +2150,11 @@ let extract_termination_and_decreasing (ctx: extraction_ctx) (fmt: F.formatter)
   F.pp_close_box fmt ();
   F.pp_print_space fmt ();
   (* Tuple of the arguments *)
-  let vars = List.map (fun (v: var) -> v.id) def_body.inputs in
+  let vars = List.map (fun (v : var) -> v.id) def_body.inputs in
 
   if List.length vars = 1 then
     F.pp_print_string fmt (ctx_get_var (List.hd vars) ctx_body)
-  else begin
+  else (
     F.pp_open_hovbox fmt 0;
     F.pp_print_string fmt "(";
     Collections.List.iter_link
@@ -2150,8 +2164,7 @@ let extract_termination_and_decreasing (ctx: extraction_ctx) (fmt: F.formatter)
       (fun v -> F.pp_print_string fmt (ctx_get_var v ctx_body))
       vars;
     F.pp_print_string fmt ")";
-    F.pp_close_box fmt ();
-  end;
+    F.pp_close_box fmt ());
   (* Close the box for "let FUN_NAME (PARAMS) : EFFECT = admit()" *)
   F.pp_close_box fmt ();
   (* Close the box for the whole definition *)
@@ -2176,9 +2189,9 @@ let extract_termination_and_decreasing (ctx: extraction_ctx) (fmt: F.formatter)
   F.pp_open_hovbox fmt 0;
   F.pp_print_string fmt "| `(tactic| ";
   F.pp_print_string fmt def_name;
-  F.pp_print_space fmt ();
-  Collections.List.iter_link (F.pp_print_space fmt)
+  List.iter
     (fun v ->
+      F.pp_print_space fmt ();
       F.pp_print_string fmt "$";
       F.pp_print_string fmt (ctx_get_var v ctx_body))
     vars;
@@ -2230,10 +2243,9 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (* *)
   let qualif = ctx.fmt.fun_decl_kind_to_qualif kind in
   (* For Lean: we generate a record of assumed functions *)
-  if not (!backend = Lean && (kind = Assumed || kind = Declared)) then begin
+  if not (!backend = Lean && (kind = Assumed || kind = Declared)) then (
     F.pp_print_string fmt qualif;
-    F.pp_print_space fmt ()
-  end;
+    F.pp_print_space fmt ());
   F.pp_print_string fmt def_name;
   F.pp_print_space fmt ();
   if use_forall then (
@@ -2271,10 +2283,9 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
     (* [Tot] *)
     if has_decreases_clause then (
       assert_backend_supports_decreases_clauses ();
-      if !backend = FStar then begin
+      if !backend = FStar then (
         F.pp_print_string fmt "Tot";
-        F.pp_print_space fmt ()
-      end);
+        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 ();
@@ -2355,26 +2366,28 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Close the outer box for the definition *)
   F.pp_close_box fmt ();
   (* Termination clause *)
-  if has_decreases_clause && !backend = Lean then begin
+  if has_decreases_clause && !backend = Lean then (
     let def_body = Option.get def.body in
-    let all_vars = List.map (fun (v: var) -> v.id) def_body.inputs in
+    let all_vars = List.map (fun (v : var) -> v.id) def_body.inputs in
     let num_fwd_inputs =
       def.signature.info.num_fwd_inputs_with_fuel_with_state
     in
     let vars = Collections.List.prefix num_fwd_inputs all_vars in
 
     (* terminates_by *)
-    let terminates_name = ctx_get_terminates_clause def.def_id def.loop_id ctx in
+    let terminates_name =
+      ctx_get_terminates_clause def.def_id def.loop_id ctx
+    in
     F.pp_print_break fmt 0 0;
     F.pp_open_hovbox fmt ctx.indent_incr;
     F.pp_print_string fmt "termination_by";
     F.pp_open_hovbox fmt 0;
     F.pp_print_space fmt ();
     F.pp_print_string fmt def_name;
-    F.pp_print_space fmt ();
-    Collections.List.iter_link
-      (F.pp_print_space fmt)
-      (fun v -> F.pp_print_string fmt (ctx_get_var v ctx_body))
+    List.iter
+      (fun v ->
+        F.pp_print_space fmt ();
+        F.pp_print_string fmt (ctx_get_var v ctx_body))
       all_vars;
     F.pp_print_space fmt ();
     F.pp_print_string fmt "=>";
@@ -2382,17 +2395,16 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
     F.pp_open_hovbox fmt 0;
     F.pp_print_space fmt ();
     F.pp_print_string fmt terminates_name;
-    F.pp_print_space 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 ())
+        F.pp_print_space fmt ();
+        F.pp_print_string fmt pname)
       def.signature.type_params;
     List.iter
       (fun v ->
-        F.pp_print_string fmt (ctx_get_var v ctx_body);
-        F.pp_print_space fmt ())
+        F.pp_print_space fmt ();
+        F.pp_print_string fmt (ctx_get_var v ctx_body))
       vars;
     F.pp_close_box fmt ();
     F.pp_close_box fmt ();
@@ -2404,14 +2416,13 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
     F.pp_print_space fmt ();
     F.pp_open_hvbox fmt ctx.indent_incr;
     F.pp_print_string fmt decreases_name;
-    F.pp_print_space fmt ();
-    Collections.List.iter_link
-      (F.pp_print_space fmt)
-      (fun v -> F.pp_print_string fmt (ctx_get_var v ctx_body))
+    List.iter
+      (fun v ->
+        F.pp_print_space fmt ();
+        F.pp_print_string fmt (ctx_get_var v ctx_body))
       vars;
     F.pp_close_box fmt ();
-    F.pp_close_box fmt ()
-  end;
+    F.pp_close_box fmt ());
   (* Add breaks to insert new lines between definitions *)
   F.pp_print_break fmt 0 0
 
@@ -2561,7 +2572,8 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
     (* Add a break before *)
     F.pp_print_break fmt 0 0;
     (* Print a comment *)
-    extract_comment fmt ("Unit test for [" ^ Print.fun_name_to_string def.basename ^ "]");
+    extract_comment 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;
@@ -2613,8 +2625,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
         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 ^ " ())")
-    );
+        F.pp_print_string fmt ("." ^ success ^ " ())"));
     (* Close the box for the test *)
     F.pp_close_box fmt ();
     (* Add a break after *)
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 4c4a9959..e96a80f9 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -51,7 +51,7 @@ type decl_kind =
       (** The first definition of a group of mutually-recursive definitions.
 
           F*:  [type x0 = ... and x1 = ...]
-          Coq: [Fixpoing x0 := ... with x1 := ...]
+          Coq: [Fixpoint x0 := ... with x1 := ...]
        *)
   | MutRecInner
       (** An inner definition in a group of mutually-recursive definitions. *)
@@ -217,7 +217,6 @@ type formatter = {
             the same purpose as in {!field:fun_name}.
           - loop identifier, if this is for a loop
        *)
-
   var_basename : StringSet.t -> string option -> ty -> string;
       (** Generates a variable basename.
 
@@ -471,8 +470,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
   | GlobalId gid ->
       let name = (A.GlobalDeclId.Map.find gid global_decls).name in
       "global name: " ^ Print.global_name_to_string name
-  | DeclaredId fid
-  | FunId fid -> (
+  | DeclaredId fid | FunId fid -> (
       match fid with
       | FromLlbc (fid, lp_id, rg_id) ->
           let fun_name =
@@ -781,12 +779,12 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation)
     ctx.fmt.fun_name def.basename def.num_loops def.loop_id num_rgs rg_info
       (keep_fwd, num_backs)
   in
-  let ctx = if def.body = None && !Config.backend = Lean then
-    ctx_add
-      (DeclaredId (FromLlbc (A.Regular def_id, def.loop_id, def.back_id)))
-      ("opaque_defs." ^ name) ctx
-  else
-    ctx
+  let ctx =
+    if def.body = None && !Config.backend = Lean then
+      ctx_add
+        (DeclaredId (FromLlbc (A.Regular def_id, def.loop_id, def.back_id)))
+        ("opaque_defs." ^ name) ctx
+    else ctx
   in
   ctx_add
     (FunId (FromLlbc (A.Regular def_id, def.loop_id, def.back_id)))
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index df7a750d..1c0bcf73 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -466,10 +466,9 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
 
   let is_opaque = Option.is_none body.Pure.body in
   if
-    config.extract_globals && (
-      ((not is_opaque) && config.extract_transparent)
-      || (is_opaque && config.extract_opaque)
-    )
+    config.extract_globals
+    && (((not is_opaque) && config.extract_transparent)
+       || (is_opaque && config.extract_opaque))
   then
     Extract.extract_global_decl ctx.extract_ctx fmt global body config.interface
 
@@ -564,7 +563,8 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
           let has_decr_clause = has_decreases_clause decl in
           if has_decr_clause then
             if !Config.backend = Lean then
-              Extract.extract_termination_and_decreasing ctx.extract_ctx fmt decl
+              Extract.extract_termination_and_decreasing ctx.extract_ctx fmt
+                decl
             else
               Extract.extract_template_decreases_clause ctx.extract_ctx fmt decl
         in
@@ -661,24 +661,22 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
    *)
   if config.extract_state_type && config.extract_fun_decls then
     export_state_type ();
-  if config.extract_opaque && config.extract_fun_decls && !Config.backend = Lean then begin
+  if config.extract_opaque && config.extract_fun_decls && !Config.backend = Lean
+  then (
     Format.pp_print_break fmt 0 0;
     Format.pp_open_vbox fmt ctx.extract_ctx.indent_incr;
     Format.pp_print_string fmt "structure OpaqueDefs where";
-    Format.pp_print_break fmt 0 0
-  end;
+    Format.pp_print_break fmt 0 0);
   List.iter export_decl_group ctx.crate.declarations;
-  if config.extract_opaque && !Config.backend = Lean then begin
-    Format.pp_close_box fmt ()
-  end;
+  if config.extract_opaque && !Config.backend = Lean then
+    Format.pp_close_box fmt ();
   if config.extract_state_type && not config.extract_fun_decls then
     export_state_type ()
 
 let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
     (rust_module_name : string) (module_name : string) (custom_msg : string)
-    ?(custom_variables: string list = [])
-    (custom_imports : string list) (custom_includes : string list)
-    : unit =
+    ?(custom_variables : string list = []) (custom_imports : string list)
+    (custom_includes : string list) : unit =
   (* Open the file and create the formatter *)
   let out = open_out filename in
   let fmt = Format.formatter_of_out_channel out in
@@ -691,14 +689,14 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
    * internal count is consistent with the state of the file.
    *)
   (* Create the header *)
-  begin match !Config.backend with
+  (match !Config.backend with
   | Lean ->
       Printf.fprintf out "-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS\n";
-      Printf.fprintf out "-- [%s]%s\n" rust_module_name custom_msg;
+      Printf.fprintf out "-- [%s]%s\n" rust_module_name custom_msg
   | Coq | FStar ->
-      Printf.fprintf out "(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)\n";
-      Printf.fprintf out "(** [%s]%s *)\n" rust_module_name custom_msg
-  end;
+      Printf.fprintf out
+        "(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)\n";
+      Printf.fprintf out "(** [%s]%s *)\n" rust_module_name custom_msg);
   (match !Config.backend with
   | FStar ->
       Printf.fprintf out "module %s\n" module_name;
@@ -732,11 +730,9 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
       List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_imports;
       (* Add the custom includes *)
       List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_includes;
-      if custom_variables <> [] then begin
+      if custom_variables <> [] then (
         Printf.fprintf out "\n";
-        List.iter (fun m -> Printf.fprintf out "%s\n" m) custom_variables
-      end
-  );
+        List.iter (fun m -> Printf.fprintf out "%s\n" m) custom_variables));
   (* From now onwards, we use the formatter *)
   (* Set the margin *)
   Format.pp_set_margin fmt 80;
@@ -885,13 +881,11 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
 
   (* Lean reflects the module hierarchy within the filesystem, so we need to
      create more directories *)
-  if !Config.backend = Lean then begin
-    let (^^) = Filename.concat in
+  if !Config.backend = Lean then (
+    let ( ^^ ) = Filename.concat in
     mkdir_if (dest_dir ^^ "Base");
     mkdir_if (dest_dir ^^ module_name);
-    if needs_clauses_module then
-      mkdir_if (dest_dir ^^ module_name ^^ "Clauses");
-  end;
+    if needs_clauses_module then mkdir_if (dest_dir ^^ module_name ^^ "Clauses"));
 
   (* Copy the "Primitives" file *)
   let _ =
@@ -936,7 +930,17 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
   let file_delimiter =
     if !Config.backend = Lean then "/" else module_delimiter
   in
-  let ext = match !Config.backend with FStar -> ".fst" | Coq -> ".v" | Lean -> ".lean" in
+  (* File extension for the "regular" modules *)
+  let ext =
+    match !Config.backend with FStar -> ".fst" | Coq -> ".v" | Lean -> ".lean"
+  in
+  (* File extension for the opaque module *)
+  let opaque_ext =
+    match !Config.backend with
+    | FStar -> ".fsti"
+    | Coq -> ".v"
+    | Lean -> ".lean"
+  in
 
   (* Extract one or several files, depending on the configuration *)
   if !Config.split_files then (
@@ -985,20 +989,28 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
       ": type definitions" [] [];
 
     (* Extract the template clauses *)
-    if needs_clauses_module && !Config.extract_template_decreases_clauses then (
-      let clauses_filename = extract_filebasename ^ file_delimiter ^ "Clauses" ^ file_delimiter ^ "Template" ^ ext in
-      let clauses_module = module_name ^ module_delimiter ^ "Clauses" ^ module_delimiter ^ "Template" in
-      let clauses_config =
-        { base_gen_config with extract_template_decreases_clauses = true }
-      in
-      extract_file clauses_config gen_ctx clauses_filename crate.A.name
-        clauses_module ": templates for the decreases clauses" [ types_module ]
-        []);
+    (if needs_clauses_module && !Config.extract_template_decreases_clauses then
+     let template_clauses_filename =
+       extract_filebasename ^ file_delimiter ^ "Clauses" ^ file_delimiter
+       ^ "Template" ^ ext
+     in
+     let template_clauses_module =
+       module_name ^ module_delimiter ^ "Clauses" ^ module_delimiter
+       ^ "Template"
+     in
+     let template_clauses_config =
+       { base_gen_config with extract_template_decreases_clauses = true }
+     in
+     extract_file template_clauses_config gen_ctx template_clauses_filename
+       crate.A.name template_clauses_module
+       ": templates for the decreases clauses" [ types_module ] []);
 
     (* Extract the opaque functions, if needed *)
     let opaque_funs_module =
       if has_opaque_funs then (
-        let opaque_filename = extract_filebasename ^ file_delimiter ^ "Opaque" ^ ext in
+        let opaque_filename =
+          extract_filebasename ^ file_delimiter ^ "Opaque" ^ opaque_ext
+        in
         let opaque_module = module_name ^ module_delimiter ^ "Opaque" in
         let opaque_config =
           {
@@ -1028,13 +1040,18 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
     in
     let clauses_module =
       if needs_clauses_module then
-        [ module_name ^ module_delimiter ^ "Clauses" ^ module_delimiter ^ "Template"]
+        let clauses_submodule =
+          if !Config.backend = Lean then module_delimiter ^ "Clauses" else ""
+        in
+        [ module_name ^ clauses_submodule ^ module_delimiter ^ "Clauses" ]
+      else []
+    in
+    let custom_variables =
+      if has_opaque_funs then [ "section variable (opaque_defs: OpaqueDefs)" ]
       else []
     in
-    let custom_variables = if has_opaque_funs then [ "section variable (opaque_defs: OpaqueDefs)" ] else [] in
     extract_file fun_config gen_ctx fun_filename crate.A.name fun_module
-      ": function definitions" []
-      ~custom_variables
+      ": function definitions" [] ~custom_variables
       ([ types_module ] @ opaque_funs_module @ clauses_module))
   else
     let gen_config =