Merge pull request #46 from AeneasVerif/son_improves

Minor improvements for the extraction

26 files changed, 256 insertions, 129 deletions

diff --git a/compiler/Config.ml b/compiler/Config.ml
index fe110ee4..364ef748 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -35,11 +35,11 @@ let backend = ref FStar
 
 (** {1 Interpreter} *)
 
-(** Check that invariants are maintained whenever we execute a statement
-
-    TODO: rename to sanity_checks.
+(** Activate the sanity checks, and in particular the invariant checks
+    that are performed at every evaluation step. This is very expensive
+    (~100x slow down) but very efficient to catch mistakes early.
  *)
-let check_invariants = ref true
+let sanity_checks = ref false
 
 (** Expand all symbolic values containing borrows upon introduction - allows
     to use restrict ourselves to a simpler model for the projectors over
@@ -52,7 +52,8 @@ let greedy_expand_symbolics_with_borrows = true
 
 (** Experimental.
 
-    TODO: remove (always true now)
+    TODO: remove (always true now), but check that when we panic/call a function
+    there is no bottom below a borrow.
 
     We sometimes want to temporarily break the invariant that there is no
     bottom value below a borrow. If this value is true, we don't check
@@ -288,7 +289,7 @@ let unfold_monadic_let_bindings = ref false
     we later filter the useless *forward* calls in the micro-passes, where it is
     more natural to do.
 
-    See the comments for {!val:PureMicroPasses.expression_contains_child_call_in_all_paths}
+    See the comments for {!PureMicroPasses.expression_contains_child_call_in_all_paths}
     for additional explanations.
  *)
 let filter_useless_monadic_calls = ref true
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index a2ae4f16..c93bb213 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -112,7 +112,7 @@ let reset_global_counters () =
   fun_call_id_counter := FunCallId.generator_zero;
   dummy_var_id_counter := DummyVarId.generator_zero
 
-(** Ancestor for {!env} iter visitor *)
+(** Ancestor for {!type:env} iter visitor *)
 class ['self] iter_env_base =
   object (_self : 'self)
     inherit [_] iter_abs
@@ -120,7 +120,7 @@ class ['self] iter_env_base =
     method visit_dummy_var_id : 'env -> dummy_var_id -> unit = fun _ _ -> ()
   end
 
-(** Ancestor for {!env} map visitor *)
+(** Ancestor for {!type:env} map visitor *)
 class ['self] map_env_base =
   object (_self : 'self)
     inherit [_] map_abs
@@ -423,11 +423,11 @@ let erase_regions (ty : ty) : ty =
   in
   v#visit_ty () ty
 
-(** Push an uninitialized variable (which thus maps to {!constructor:Values.value.Bottom}) *)
+(** Push an uninitialized variable (which thus maps to {!constructor:Values.value.VBottom}) *)
 let ctx_push_uninitialized_var (ctx : eval_ctx) (var : var) : eval_ctx =
   ctx_push_var ctx var (mk_bottom (erase_regions var.var_ty))
 
-(** Push a list of uninitialized variables (which thus map to {!constructor:Values.value.Bottom}) *)
+(** Push a list of uninitialized variables (which thus map to {!constructor:Values.value.VBottom}) *)
 let ctx_push_uninitialized_vars (ctx : eval_ctx) (vars : var list) : eval_ctx =
   let vars = List.map (fun v -> (v, mk_bottom (erase_regions v.var_ty))) vars in
   ctx_push_vars ctx vars
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index c8c16c08..e48e6ae6 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -173,12 +173,7 @@ let extract_adt_g_value
          *)
         let cons =
           match variant_id with
-          | Some vid -> (
-              (* In the case of Lean, we might have to add the type name as a prefix *)
-              match (!backend, adt_id) with
-              | Lean, TAssumed _ ->
-                  ctx_get_type adt_id ctx ^ "." ^ ctx_get_variant adt_id vid ctx
-              | _ -> ctx_get_variant adt_id vid ctx)
+          | Some vid -> ctx_get_variant adt_id vid ctx
           | None -> ctx_get_struct adt_id ctx
         in
         let use_parentheses = inside && field_values <> [] in
@@ -2723,7 +2718,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 (TAssumed TResult) result_return_id ctx in
-        F.pp_print_string fmt ("." ^ success ^ " ())")
+        F.pp_print_string fmt (success ^ " ())")
     | HOL4 ->
         F.pp_print_string fmt "val _ = assert_return (";
         F.pp_print_string fmt "“";
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index c6158847..85ab1112 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -311,7 +311,7 @@ let names_map_add (id_to_string : id -> string) (id : id) (name : string)
     the same name because Lean uses the typing information to resolve the
     ambiguities.
 
-    This map complements the {!names_map}, which checks for collisions.
+    This map complements the {!type:names_map}, which checks for collisions.
   *)
 type unsafe_names_map = { id_to_name : string IdMap.t }
 
@@ -634,11 +634,13 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
   | TypeId id -> "type name: " ^ type_id_to_string ctx id
   | StructId id -> "struct constructor of: " ^ type_id_to_string ctx id
   | VariantId (id, variant_id) ->
+      let type_name = type_id_to_string ctx id in
       let variant_name = adt_variant_to_string ctx id (Some variant_id) in
-      "variant name: " ^ variant_name
+      "type name: " ^ type_name ^ ", variant name: " ^ variant_name
   | FieldId (id, field_id) ->
+      let type_name = type_id_to_string ctx id in
       let field_name = adt_field_to_string ctx id field_id in
-      "field name: " ^ field_name
+      "type name: " ^ type_name ^ ", field name: " ^ field_name
   | UnknownId -> "keyword"
   | TypeVarId id -> "type_var_id: " ^ TypeVarId.to_string id
   | ConstGenericVarId id ->
@@ -958,31 +960,40 @@ let keywords () =
   List.concat [ named_unops; named_binops; misc ]
 
 let assumed_adts () : (assumed_ty * string) list =
-  match !backend with
-  | Lean ->
-      [
-        (TState, "State");
-        (TResult, "Result");
-        (TError, "Error");
-        (TFuel, "Nat");
-        (TArray, "Array");
-        (TSlice, "Slice");
-        (TStr, "Str");
-        (TRawPtr Mut, "MutRawPtr");
-        (TRawPtr Const, "ConstRawPtr");
-      ]
-  | Coq | FStar | HOL4 ->
-      [
-        (TState, "state");
-        (TResult, "result");
-        (TError, "error");
-        (TFuel, if !backend = HOL4 then "num" else "nat");
-        (TArray, "array");
-        (TSlice, "slice");
-        (TStr, "str");
-        (TRawPtr Mut, "mut_raw_ptr");
-        (TRawPtr Const, "const_raw_ptr");
-      ]
+  let state =
+    if !use_state then
+      match !backend with
+      | Lean -> [ (TState, "State") ]
+      | Coq | FStar | HOL4 -> [ (TState, "state") ]
+    else []
+  in
+  (* We voluntarily omit the type [Error]: it is never directly
+     referenced in the generated translation, and easily collides
+     with user-defined types *)
+  let adts =
+    match !backend with
+    | Lean ->
+        [
+          (TResult, "Result");
+          (TFuel, "Nat");
+          (TArray, "Array");
+          (TSlice, "Slice");
+          (TStr, "Str");
+          (TRawPtr Mut, "MutRawPtr");
+          (TRawPtr Const, "ConstRawPtr");
+        ]
+    | Coq | FStar | HOL4 ->
+        [
+          (TResult, "result");
+          (TFuel, if !backend = HOL4 then "num" else "nat");
+          (TArray, "array");
+          (TSlice, "slice");
+          (TStr, "str");
+          (TRawPtr Mut, "mut_raw_ptr");
+          (TRawPtr Const, "const_raw_ptr");
+        ]
+  in
+  state @ adts
 
 let assumed_struct_constructors () : (assumed_ty * string) list =
   match !backend with
@@ -1013,9 +1024,12 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
       ]
   | Lean ->
       [
-        (TResult, result_return_id, "ret");
-        (TResult, result_fail_id, "fail");
-        (TError, error_failure_id, "panic");
+        (TResult, result_return_id, "Result.ret");
+        (TResult, result_fail_id, "Result.fail");
+        (* For panic: we omit the prefix "Error." because the type is always
+           clear from the context. Also, "Error" is often used by user-defined
+           types (when we omit the crate as a prefix). *)
+        (TError, error_failure_id, ".panic");
         (* No Fuel::Zero on purpose *)
         (* No Fuel::Succ on purpose *)
       ]
@@ -1095,8 +1109,9 @@ let initialize_names_maps () : names_maps =
   let init = names_map_init () in
   let int_names = List.map int_name T.all_int_types in
   let keywords =
-    List.concat
-      [ [ bool_name (); char_name (); str_name () ]; int_names; init.keywords ]
+    (* Remark: we don't put "str_name()" below because it clashes with
+       "alloc::string::String", which we register elsewhere. *)
+    List.concat [ [ bool_name (); char_name () ]; int_names; init.keywords ]
   in
   let names_set = StringSet.empty in
   let name_to_id = StringMap.empty in
@@ -1405,9 +1420,10 @@ let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option)
        - we add "_fwd"
      - [rg] is [None]: this is a backward function:
        - this function has one extracted backward function:
-         - if the forward function has been filtered, we add "_fwd_back":
+         - if the forward function has been filtered, we add nothing:
            the forward function is useless, so the unique backward function
-           takes its place, in a way
+           takes its place, in a way (in effect, we "merge" the forward
+           and the backward functions).
          - otherwise we add "_back"
        - this function has several backward functions: we add "_back" and an
          additional suffix to identify the precise backward function
@@ -1623,7 +1639,7 @@ let ctx_compute_trait_type_clause_name (ctx : extraction_ctx)
       function is an assumed function or a local function
     - function basename
     - the number of loops in the parent function. This is used for
-      the same purpose as in {!field:llbc_name}.
+      the same purpose as in [llbc_name].
     - loop identifier, if this is for a loop
  *)
 let ctx_compute_termination_measure_name (ctx : extraction_ctx)
@@ -1652,7 +1668,7 @@ let ctx_compute_termination_measure_name (ctx : extraction_ctx)
       function is an assumed function or a local function
     - function basename
     - the number of loops in the parent function. This is used for
-      the same purpose as in {!field:llbc_name}.
+      the same purpose as in [llbc_name].
     - loop identifier, if this is for a loop
  *)
 let ctx_compute_decreases_proof_name (ctx : extraction_ctx)
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 30ec7c19..24d16dca 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -127,9 +127,15 @@ let mk_struct_constructor (type_name : string) : string =
     a type parameter for the allocator to use, which we want to filter.
  *)
 let builtin_types () : builtin_type_info list =
-  let mk_type (rust_name : string) ?(keep_params : bool list option = None)
+  let mk_type (rust_name : string) ?(custom_name : string option = None)
+      ?(keep_params : bool list option = None)
       ?(kind : type_variant_kind = KOpaque) () : builtin_type_info =
-    let extract_name = flatten_name (split_on_separator rust_name) in
+    let rust_name = parse_pattern rust_name in
+    let extract_name =
+      match custom_name with
+      | None -> flatten_name (pattern_to_type_extract_name rust_name)
+      | Some name -> flatten_name (split_on_separator name)
+    in
     let body_info : builtin_type_body_info option =
       match kind with
       | KOpaque -> None
@@ -147,13 +153,16 @@ let builtin_types () : builtin_type_info list =
           Some (Struct (constructor, fields))
       | KEnum -> raise (Failure "TODO")
     in
-    let rust_name = parse_pattern rust_name in
     { rust_name; extract_name; keep_params; body_info }
   in
 
   [
     (* Alloc *)
     mk_type "alloc::alloc::Global" ();
+    (* String *)
+    mk_type "alloc::string::String"
+      ~custom_name:(Some (backend_choice "string" "String"))
+      ();
     (* Vec *)
     mk_type "alloc::vec::Vec" ~keep_params:(Some [ true; false ]) ();
     (* Range *)
diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index 41c81207..a916bffb 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -61,7 +61,10 @@ let pattern_to_extract_name (is_trait_impl : bool) (name : pattern) :
               | TArray -> "Array"
               | TSlice -> "Slice"
             else expr_to_string c ty
-        | ERef _ | EVar _ -> raise (Failure ""))
+        | ERef _ | EVar _ ->
+            (* We simply convert the pattern to a string. This is not very
+               satisfying but we should rarely get there. *)
+            expr_to_string c ty)
   in
   let rec pattern_to_string (n : pattern) : string list =
     match n with
@@ -73,6 +76,7 @@ let pattern_to_extract_name (is_trait_impl : bool) (name : pattern) :
   in
   pattern_to_string name
 
+let pattern_to_type_extract_name = pattern_to_extract_name false
 let pattern_to_fun_extract_name = pattern_to_extract_name false
 let pattern_to_trait_impl_extract_name = pattern_to_extract_name true
 
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index c6212d31..ca9984be 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -213,7 +213,7 @@ let is_empty_record_type_decl_group (dg : Pure.type_decl list) : bool =
     - in Lean, groups of mutually recursive definitions must end with "end"
     - in HOL4 (in most situations) the whole group must be within a `Define` command
 
-    Calls to {!extract_fun_decl} should be inserted between calls to
+    Calls to {!Extract.extract_fun_decl} should be inserted between calls to
     {!start_fun_decl_group} and {!end_fun_decl_group}.
 
     TODO: maybe those [{start/end}_decl_group] functions are not that much a good
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 8c9c0e72..2f793f4a 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -2155,7 +2155,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
      ^ "\n\n- abs1:\n" ^ abs_to_string ctx abs1));
 
   (* Check that the abstractions are destructured *)
-  if !Config.check_invariants then (
+  if !Config.sanity_checks then (
     let destructure_shared_values = true in
     assert (abs_is_destructured destructure_shared_values ctx abs0);
     assert (abs_is_destructured destructure_shared_values ctx abs1));
@@ -2487,7 +2487,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool)
   in
 
   (* Sanity check *)
-  if !Config.check_invariants then assert (abs_is_destructured true ctx abs);
+  if !Config.sanity_checks then assert (abs_is_destructured true ctx abs);
   (* Return *)
   abs
 
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index b13d545c..44f85d0a 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -924,7 +924,7 @@ let remove_intersecting_aproj_borrows_shared (regions : RegionId.Set.t)
         
     [subst]: takes as parameters the abstraction in which we perform the
     substitution and the list of given back values at the projector of
-    loans where we perform the substitution (see the fields in {!AProjLoans}).
+    loans where we perform the substitution (see the fields in {!Values.AProjLoans}).
     Note that the symbolic value at this place is necessarily equal to [sv],
     which is why we don't give it as parameters.
  *)
@@ -970,13 +970,13 @@ let update_intersecting_aproj_loans (proj_regions : RegionId.Set.t)
   (* Return *)
   ctx
 
-(** Helper function: lookup an {!AProjLoans} by using an abstraction id and a
+(** Helper function: lookup an {!constructor:Values.aproj.AProjLoans} by using an abstraction id and a
     symbolic value.
-    
+
     We return the information from the looked up projector of loans. See the
-    fields in {!AProjLoans} (we don't return the symbolic value, because it
+    fields in {!constructor:Values.aproj.AProjLoans} (we don't return the symbolic value, because it
     is equal to [sv]).
-    
+
     Sanity check: we check that there is exactly one projector which corresponds
     to the couple (abstraction id, symbolic value).
  *)
@@ -1115,7 +1115,7 @@ let update_aproj_borrows (abs_id : AbstractionId.id) (sv : symbolic_value)
 
 (** Helper function: might break invariants.
 
-    Converts an {!AProjLoans} to an {!AEndedProjLoans}. The projector is identified
+    Converts an {!Values.aproj.AProjLoans} to an {!Values.aproj.AEndedProjLoans}. The projector is identified
     by a symbolic value and an abstraction id.
  *)
 let update_aproj_loans_to_ended (abs_id : AbstractionId.id)
diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli
index 4be1fd24..b545f979 100644
--- a/compiler/InterpreterExpansion.mli
+++ b/compiler/InterpreterExpansion.mli
@@ -79,6 +79,6 @@ val expand_symbolic_int :
   m_fun
 
 (** If this mode is activated through the [config], greedily expand the symbolic
-    values which need to be expanded. See {!type:config} for more information.
+    values which need to be expanded. See {!type:Contexts.config} for more information.
  *)
 val greedy_expand_symbolic_values : config -> cm_fun
diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml
index d14230c6..ca1f8f31 100644
--- a/compiler/InterpreterLoopsCore.ml
+++ b/compiler/InterpreterLoopsCore.ml
@@ -41,10 +41,10 @@ type abs_borrows_loans_maps = {
   borrow_loan_to_abs : AbstractionId.Set.t BorrowId.Map.t;
 }
 
-(** See {!InterpreterLoopsMatchCtxs.MakeMatcher} and {!InterpreterLoopsCore.Matcher}.
+(** See {!module:Aeneas.InterpreterLoopsMatchCtxs.MakeMatcher} and [Matcher].
 
     This module contains primitive match functions to instantiate the generic
-    {!InterpreterLoopsMatchCtxs.MakeMatcher} functor.
+    {!module:Aeneas.InterpreterLoopsMatchCtxs.MakeMatcher} functor.
   *)
 module type PrimMatcher = sig
   val match_etys : ety -> ety -> ety
@@ -231,8 +231,8 @@ module type Matcher = sig
     eval_ctx -> typed_avalue -> typed_avalue -> typed_avalue
 end
 
-(** See {!InterpreterLoopsMatchCtxs.MakeCheckEquivMatcher} and
-    {!InterpreterLoopsCore.CheckEquivMatcher}.
+(** See {!module:InterpreterLoopsMatchCtxs.MakeCheckEquivMatcher} and
+    {!module-type:InterpreterLoopsCore.CheckEquivMatcher}.
 
     Very annoying: functors only take modules as inputs...
  *)
diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index 4cc74aae..8d485483 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -714,7 +714,7 @@ let loop_join_origin_with_continue_ctxs (config : config) (loop_id : LoopId.id)
         ^ eval_ctx_to_string !joined_ctx));
 
     (* Sanity check *)
-    if !Config.check_invariants then Invariants.check_invariants !joined_ctx;
+    if !Config.sanity_checks then Invariants.check_invariants !joined_ctx;
     (* Return *)
     ctx1
   in
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 74f9ba2c..bf459e41 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -1580,7 +1580,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id)
        ^ eval_ctx_to_string tgt_ctx));
 
     (* Sanity check *)
-    if !Config.check_invariants then
+    if !Config.sanity_checks then
       Invariants.check_borrowed_values_invariant tgt_ctx;
 
     (* End all the borrows which appear in the *new* abstractions *)
diff --git a/compiler/InterpreterLoopsMatchCtxs.mli b/compiler/InterpreterLoopsMatchCtxs.mli
index bf29af79..5f69b8d3 100644
--- a/compiler/InterpreterLoopsMatchCtxs.mli
+++ b/compiler/InterpreterLoopsMatchCtxs.mli
@@ -27,13 +27,13 @@ val compute_abs_borrows_loans_maps :
     We use it for joins, to check if two environments are convertible, etc.
     See for instance {!MakeJoinMatcher} and {!MakeCheckEquivMatcher}.
 
-    The functor is parameterized by a {!PrimMatcher}, which implements the
-    non-generic part of the match. More precisely, the role of {!PrimMatcher} is two
+    The functor is parameterized by a {!module-type:InterpreterLoopsCore.PrimMatcher}, which implements the
+    non-generic part of the match. More precisely, the role of {!module-type:InterpreterLoopsCore.PrimMatcher} is two
     provide generic functions which recursively match two values (by recursively
     matching the fields of ADT values for instance). When it does need to match
     values in a non-trivial manner (if two ADT values don't have the same
     variant for instance) it calls the corresponding specialized function from
-    {!PrimMatcher}.
+    {!module-type:InterpreterLoopsCore.PrimMatcher}.
  *)
 module MakeMatcher : functor (_ : PrimMatcher) -> Matcher
 
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 729a3577..999b8ab0 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -311,7 +311,7 @@ let try_read_place (access : access_kind) (p : place) (ctx : eval_ctx) :
       (* Note that we ignore the new environment: it should be the same as the
          original one.
       *)
-      if !Config.check_invariants then
+      if !Config.sanity_checks then
         if ctx1 <> ctx then (
           let msg =
             "Unexpected environment update:\nNew environment:\n"
diff --git a/compiler/InterpreterProjectors.mli b/compiler/InterpreterProjectors.mli
index 583c6907..9e4ebc20 100644
--- a/compiler/InterpreterProjectors.mli
+++ b/compiler/InterpreterProjectors.mli
@@ -6,7 +6,7 @@ open Contexts
 
     Apply a proj_borrows on a shared borrow.
     Note that when projecting over shared values, we generate
-    {!type:abstract_shared_borrows}, not {!type:avalue}s.
+    {!type:Aeneas.Values.abstract_shared_borrows}, not {!type:Aeneas.Values.avalue}s.
 
     Parameters:
     [regions]
diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli
index d84e8be6..3832d02f 100644
--- a/compiler/InterpreterStatements.mli
+++ b/compiler/InterpreterStatements.mli
@@ -10,7 +10,7 @@ open Cps
     dummy variables, after ending the proper borrows of course) but the return
     variable, move the return value out of the return variable, remove all the
     local variables (but preserve the abstractions!), remove the
-    {!constructor:env_elem.Frame} indicator delimiting the current frame and
+    {!constructor:Contexts.env_elem.EFrame} indicator delimiting the current frame and
     handle the return value to the continuation.
 
     If the boolean is false, we don't move the return value, and call the
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index ecd8f53f..bba88e9f 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -111,7 +111,7 @@ let mk_typed_value_from_symbolic_value (svalue : symbolic_value) : typed_value =
 (** Create a loans projector value from a symbolic value.
     
     Checks if the projector will actually project some regions. If not,
-    returns {!AIgnored} ([_]).
+    returns {!Values.AIgnored} ([_]).
     
     TODO: update to handle 'static
  *)
@@ -238,7 +238,7 @@ let symbolic_value_has_ended_regions (ended_regions : RegionId.Set.t)
   let regions = ty_regions s.sv_ty in
   not (RegionId.Set.disjoint regions ended_regions)
 
-(** Check if a {!type:value} contains [⊥].
+(** Check if a {!type:Values.value} contains [⊥].
 
     Note that this function is very general: it also checks wether
     symbolic values contain already ended regions.
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index e0e3f354..fa0d7436 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -804,7 +804,7 @@ let check_symbolic_values (ctx : eval_ctx) : unit =
   M.iter check_info !infos
 
 let check_invariants (ctx : eval_ctx) : unit =
-  if !Config.check_invariants then (
+  if !Config.sanity_checks then (
     log#ldebug (lazy ("Checking invariants:\n" ^ eval_ctx_to_string ctx));
     check_loans_borrows_relation_invariant ctx;
     check_borrowed_values_invariant ctx;
diff --git a/compiler/Main.ml b/compiler/Main.ml
index e350da8a..7f98f581 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -107,10 +107,10 @@ let () =
         Arg.Set split_files,
         " Split the definitions between different files for types, functions, \
          etc." );
-      ( "-no-check-inv",
-        Arg.Clear check_invariants,
-        " Deactivate the invariant sanity checks performed at every evaluation \
-         step. Dramatically increases speed." );
+      ( "-checks",
+        Arg.Set sanity_checks,
+        " Activate extensive sanity checks (warning: causes a ~100 times slow \
+         down)." );
       ( "-no-gen-lib-entry",
         Arg.Clear generate_lib_entry_point,
         " Do not generate the entry point file for the generated library (only \
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 50849df9..0ae83007 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -273,7 +273,7 @@ class virtual ['self] mapreduce_ty_base =
 
 type ty =
   | TAdt of type_id * generic_args
-      (** {!Adt} encodes ADTs and tuples and assumed types.
+      (** {!TAdt} encodes ADTs and tuples and assumed types.
 
           TODO: what about the ended regions? (ADTs may be parameterized
           with several region variables. When giving back an ADT value, we may
@@ -1064,7 +1064,7 @@ type trait_impl = {
   meta : meta;
   impl_trait : trait_decl_ref;
   llbc_impl_trait : Types.trait_decl_ref;
-      (** Same remark as for {llbc_generics}. *)
+      (** Same remark as for {!field:llbc_generics}. *)
   generics : generic_params;
   llbc_generics : Types.generic_params;
       (** We use the LLBC generics to generate "pretty" names, for instance
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 6b0deb73..a5143f3c 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -195,7 +195,7 @@ let fun_sig_substitute (subst : subst) (sg : fun_sig) : inst_fun_sig =
     We only look for outer monadic let-bindings.
     This is used when printing the branches of [if ... then ... else ...].
 
-    Rem.: this function will *fail* if there are {!constructor:Aeneas.Pure.expression.Loop}
+    Rem.: this function will *fail* if there are {!Pure.Loop}
     nodes (you should call it on an expression where those nodes have been eliminated).
  *)
 let rec let_group_requires_parentheses (e : texpression) : bool =
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index 73e7f71d..a05b2c5a 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -76,7 +76,7 @@ let erase_regions_subst : subst =
     tr_self = Self;
   }
 
-(** Convert an {!rty} to an {!ety} by erasing the region variables *)
+(** Erase the region variables in a type *)
 let erase_regions (ty : ty) : ty = ty_substitute erase_regions_subst ty
 
 let trait_ref_erase_regions (tr : trait_ref) : trait_ref =
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index a9f45926..53f99b7f 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -66,8 +66,8 @@ type 'a region_group_id_map = 'a RegionGroupId.Map.t [@@deriving show]
 
 (** Ancestor for {!expression} iter visitor.
 
-    We could make it inherit the visitor for {!eval_ctx}, but in all the uses
-    of this visitor we don't need to explore {!eval_ctx}, so we make it inherit
+    We could make it inherit the visitor for {!Contexts.eval_ctx}, but in all the uses
+    of this visitor we don't need to explore {!Contexts.eval_ctx}, so we make it inherit
     the abstraction visitors instead.
  *)
 class ['self] iter_expression_base =
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 05e48af5..37f58140 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -481,9 +481,19 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
       defs
   in
 
+  let dont_extract (d : Pure.type_decl) : bool =
+    match d.kind with
+    | Enum _ | Struct _ -> not config.extract_transparent
+    | Opaque -> not config.extract_opaque
+  in
+
   if List.exists (fun b -> b) builtin then
     (* Sanity check *)
     assert (List.for_all (fun b -> b) builtin)
+  else if List.exists dont_extract defs then
+    (* Check if we have to ignore declarations *)
+    (* Sanity check *)
+    assert (List.for_all dont_extract defs)
   else (
     (* Extract the type declarations.
 
@@ -873,6 +883,7 @@ type extract_file_info = {
   filename : string;
   namespace : string;
   in_namespace : bool;
+  open_namespace : bool;
   crate_name : string;
   rust_module_name : string;
   module_name : string;
@@ -931,8 +942,22 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
       (* Add the custom includes *)
       List.iter
         (fun m ->
-          Printf.fprintf out "Require Export %s.\n" m;
-          Printf.fprintf out "Import %s.\n" m)
+          (* TODO: I don't really understand how the "Require Export",
+             "Require Import", "Include" work.
+             I used to have:
+             {[
+               Require Export %s.
+               Import %s.
+             ]}
+
+             I now have:
+             {[
+               Require Import %s.
+               Include %s.
+             ]}
+          *)
+          Printf.fprintf out "Require Import %s.\n" m;
+          Printf.fprintf out "Include %s.\n" m)
         fi.custom_includes;
       Printf.fprintf out "Module %s.\n" fi.module_name
   | Lean ->
@@ -943,9 +968,10 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
       List.iter (fun m -> Printf.fprintf out "import %s\n" m) fi.custom_includes;
       (* Always open the Primitives namespace *)
       Printf.fprintf out "open Primitives\n";
-      (* If we are inside the namespace: declare it, otherwise: open it *)
-      if fi.in_namespace then Printf.fprintf out "\nnamespace %s\n" fi.namespace
-      else Printf.fprintf out "open %s\n" fi.namespace
+      (* If we are inside the namespace: declare it *)
+      if fi.in_namespace then Printf.fprintf out "\nnamespace %s\n" fi.namespace;
+      (* We might need to open the namespace *)
+      if fi.open_namespace then Printf.fprintf out "open %s\n" fi.namespace
   | HOL4 ->
       Printf.fprintf out "open primitivesLib divDefLib\n";
       (* Add the custom imports and includes *)
@@ -977,7 +1003,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
   | FStar -> ()
   | Lean -> if fi.in_namespace then Printf.fprintf out "end %s\n" fi.namespace
   | HOL4 -> Printf.fprintf out "val _ = export_theory ()\n"
-  | Coq -> Printf.fprintf out "End %s .\n" fi.module_name);
+  | Coq -> Printf.fprintf out "End %s.\n" fi.module_name);
 
   (* Some logging *)
   log#linfo (lazy ("Generated: " ^ fi.filename));
@@ -1180,20 +1206,27 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
     match primitives_src_dest with
     | None -> ()
     | Some (primitives_src, primitives_destname) -> (
-        let src = open_in (exe_dir ^ primitives_src) in
-        let tgt_filename = Filename.concat dest_dir primitives_destname in
-        let tgt = open_out tgt_filename in
-        (* Very annoying: I couldn't find a "cp" function in the OCaml libraries... *)
         try
-          while true do
-            (* We copy line by line *)
-            let line = input_line src in
-            Printf.fprintf tgt "%s\n" line
-          done
-        with End_of_file ->
-          close_in src;
-          close_out tgt;
-          log#linfo (lazy ("Copied:    " ^ tgt_filename)))
+          (* TODO: stop copying the primitives file *)
+          let src = open_in (exe_dir ^ primitives_src) in
+          let tgt_filename = Filename.concat dest_dir primitives_destname in
+          let tgt = open_out tgt_filename in
+          (* Very annoying: I couldn't find a "cp" function in the OCaml libraries... *)
+          try
+            while true do
+              (* We copy line by line *)
+              let line = input_line src in
+              Printf.fprintf tgt "%s\n" line
+            done
+          with End_of_file ->
+            close_in src;
+            close_out tgt;
+            log#linfo (lazy ("Copied:    " ^ tgt_filename))
+        with Sys_error _ ->
+          log#error
+            "Could not copy the primitives file: %s.\n\
+             You will have to copy it/set up the project by hand."
+            primitives_src)
   in
 
   (* Extract the file(s) *)
@@ -1250,12 +1283,72 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
      in
      let has_opaque_types = has_opaque_types || !Config.use_state in
 
-     (* Extract the types *)
+     (*
+      * Extract the types
+      *)
      (* If there are opaque types, we extract in an interface *)
-     (* TODO: for Lean and Coq: generate a template file *)
+     (* Extract the opaque type declarations, if needed *)
+     let opaque_types_module =
+       if has_opaque_types then (
+         (* For F*, we generate an .fsti, and let the user write the .fst.
+            For the other backends, we generate a template file as a model
+            for the file the user has to provide. *)
+         let module_suffix, opaque_imported_suffix, custom_msg =
+           match !Config.backend with
+           | FStar ->
+               ("TypesExternal", "TypesExternal", ": external type declarations")
+           | HOL4 | Coq | Lean ->
+               ( (* The name of the file we generate *)
+                 "TypesExternal_Template",
+                 (* The name of the file that will be imported by the Types
+                    module, and that the user has to provide. *)
+                 "TypesExternal",
+                 ": external types.\n\
+                  -- This is a template file: rename it to \
+                  \"TypesExternal.lean\" and fill the holes." )
+         in
+         let opaque_filename =
+           extract_filebasename ^ file_delimiter ^ module_suffix ^ opaque_ext
+         in
+         let opaque_module = crate_name ^ module_delimiter ^ module_suffix in
+         let opaque_imported_module =
+           crate_name ^ module_delimiter ^ opaque_imported_suffix
+         in
+         let opaque_config =
+           {
+             base_gen_config with
+             extract_opaque = true;
+             extract_transparent = false;
+             extract_types = true;
+             extract_trait_decls = true;
+             extract_state_type = !Config.use_state;
+             interface = true;
+           }
+         in
+         let file_info =
+           {
+             filename = opaque_filename;
+             namespace;
+             in_namespace = false;
+             open_namespace = false;
+             crate_name;
+             rust_module_name = crate.name;
+             module_name = opaque_module;
+             custom_msg;
+             custom_imports = [];
+             custom_includes = [];
+           }
+         in
+         extract_file opaque_config ctx file_info;
+         (* Return the additional dependencies *)
+         [ opaque_imported_module ])
+       else []
+     in
+
+     (* Extract the non opaque types *)
      let types_filename_ext =
        match !Config.backend with
-       | FStar -> if has_opaque_types then ".fsti" else ".fst"
+       | FStar -> ".fst"
        | Coq -> ".v"
        | Lean -> ".lean"
        | HOL4 -> "Script.sml"
@@ -1269,8 +1362,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
          base_gen_config with
          extract_types = true;
          extract_trait_decls = true;
-         extract_opaque = true;
-         extract_state_type = !Config.use_state;
+         extract_opaque = false;
          interface = has_opaque_types;
        }
      in
@@ -1279,12 +1371,13 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
          filename = types_filename;
          namespace;
          in_namespace = true;
+         open_namespace = false;
          crate_name;
          rust_module_name = crate.name;
          module_name = types_module;
          custom_msg = ": type definitions";
          custom_imports = [];
-         custom_includes = [];
+         custom_includes = opaque_types_module;
        }
      in
      extract_file types_config ctx file_info;
@@ -1307,6 +1400,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
             filename = template_clauses_filename;
             namespace;
             in_namespace = true;
+            open_namespace = false;
             crate_name;
             rust_module_name = crate.name;
             module_name = template_clauses_module;
@@ -1317,16 +1411,23 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
         in
         extract_file template_clauses_config ctx file_info);
 
-     (* Extract the opaque declarations, if needed *)
+     (* Extract the opaque fun declarations, if needed *)
      let opaque_funs_module =
        if has_opaque_funs then (
-         (* In the case of Lean we generate a template file *)
+         (* For F*, we generate an .fsti, and let the user write the .fst.
+            For the other backends, we generate a template file as a model
+            for the file the user has to provide. *)
          let module_suffix, opaque_imported_suffix, custom_msg =
            match !Config.backend with
-           | FStar | Coq | HOL4 ->
-               ("Opaque", "Opaque", ": external function declarations")
-           | Lean ->
-               ( "FunsExternal_Template",
+           | FStar ->
+               ( "FunsExternal",
+                 "FunsExternal",
+                 ": external function declarations" )
+           | HOL4 | Coq | Lean ->
+               ( (* The name of the file we generate *)
+                 "FunsExternal_Template",
+                 (* The name of the file that will be imported by the Funs
+                    module, and that the user has to provide. *)
                  "FunsExternal",
                  ": external functions.\n\
                   -- This is a template file: rename it to \
@@ -1337,9 +1438,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
          in
          let opaque_module = crate_name ^ module_delimiter ^ module_suffix in
          let opaque_imported_module =
-           if !Config.backend = Lean then
-             crate_name ^ module_delimiter ^ opaque_imported_suffix
-           else opaque_module
+           crate_name ^ module_delimiter ^ opaque_imported_suffix
          in
          let opaque_config =
            {
@@ -1357,6 +1456,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
              filename = opaque_filename;
              namespace;
              in_namespace = false;
+             open_namespace = true;
              crate_name;
              rust_module_name = crate.name;
              module_name = opaque_module;
@@ -1396,6 +1496,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
          filename = fun_filename;
          namespace;
          in_namespace = true;
+         open_namespace = false;
          crate_name;
          rust_module_name = crate.name;
          module_name = fun_module;
@@ -1429,6 +1530,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
          filename = extract_filebasename ^ ext;
          namespace;
          in_namespace = true;
+         open_namespace = false;
          crate_name;
          rust_module_name = crate.name;
          module_name = crate_name;
diff --git a/compiler/TypesUtils.ml b/compiler/TypesUtils.ml
index 52e12b9a..76cc710a 100644
--- a/compiler/TypesUtils.ml
+++ b/compiler/TypesUtils.ml
@@ -5,7 +5,7 @@ include Charon.TypesUtils
 (** Retuns true if the type contains borrows.
 
     Note that we can't simply explore the type and look for regions: sometimes
-    we erase the lists of regions (by replacing them with [[]] when using {!Types.ety},
+    we erase the lists of regions (by replacing them with [[]] when using {!type:Types.ty},
     and when a type uses 'static this region doesn't appear in the region parameters.
  *)
 let ty_has_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool =
@@ -15,7 +15,7 @@ let ty_has_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool =
 (** Retuns true if the type contains nested borrows.
 
     Note that we can't simply explore the type and look for regions: sometimes
-    we erase the lists of regions (by replacing them with [[]] when using {!Types.ety},
+    we erase the lists of regions (by replacing them with [[]] when using {!type:Types.ty},
     and when a type uses 'static this region doesn't appear in the region parameters.
  *)
 let ty_has_nested_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool =