Generate a dedicated file for the external types

46 files changed, 355 insertions, 90 deletions

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 31cb4b32..cc84b9fb 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 *)
@@ -1250,12 +1276,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 +1355,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 +1364,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 +1393,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,7 +1404,7 @@ 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 (
          (* For F*, we generate an .fsti, and let the user write the .fst.
@@ -1362,6 +1449,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;
@@ -1401,6 +1489,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;
@@ -1434,6 +1523,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/tests/coq/array/Array.v b/tests/coq/array/Array.v
index 99ff3b03..105ce21f 100644
--- a/tests/coq/array/Array.v
+++ b/tests/coq/array/Array.v
@@ -528,4 +528,4 @@ Definition ite : result unit :=
   Return tt
 .
 
-End Array .
+End Array.
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index ede82492..aadaa20d 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -6,10 +6,10 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
-Require Export BetreeMain_Types.
-Import BetreeMain_Types.
-Require Export BetreeMain_FunsExternal.
-Import BetreeMain_FunsExternal.
+Require Import BetreeMain_Types.
+Include BetreeMain_Types.
+Require Import BetreeMain_FunsExternal.
+Include BetreeMain_FunsExternal.
 Module BetreeMain_Funs.
 
 (** [betree_main::betree::load_internal_node]: forward function
@@ -1230,4 +1230,4 @@ Definition main : result unit :=
 (** Unit test for [betree_main::main] *)
 Check (main )%return.
 
-End BetreeMain_Funs .
+End BetreeMain_Funs.
diff --git a/tests/coq/betree/BetreeMain_FunsExternal_Template.v b/tests/coq/betree/BetreeMain_FunsExternal_Template.v
index 4898acd4..36022a20 100644
--- a/tests/coq/betree/BetreeMain_FunsExternal_Template.v
+++ b/tests/coq/betree/BetreeMain_FunsExternal_Template.v
@@ -7,8 +7,8 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
-Require Export BetreeMain_Types.
-Import BetreeMain_Types.
+Require Import BetreeMain_Types.
+Include BetreeMain_Types.
 Module BetreeMain_FunsExternal_Template.
 
 (** [betree_main::betree_utils::load_internal_node]: forward function
@@ -43,4 +43,4 @@ Axiom core_option_Option_unwrap :
   forall(T : Type), option T -> state -> result (state * T)
 .
 
-End BetreeMain_FunsExternal_Template .
+End BetreeMain_FunsExternal_Template.
diff --git a/tests/coq/betree/BetreeMain_Types.v b/tests/coq/betree/BetreeMain_Types.v
index b729d1c3..22989256 100644
--- a/tests/coq/betree/BetreeMain_Types.v
+++ b/tests/coq/betree/BetreeMain_Types.v
@@ -6,6 +6,8 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
+Require Import BetreeMain_TypesExternal.
+Include BetreeMain_TypesExternal.
 Module BetreeMain_Types.
 
 (** [betree_main::betree::List]
@@ -113,7 +115,4 @@ mkbetree_BeTree_t {
 }
 .
 
-(** The state type used in the state-error monad *)
-Axiom state : Type.
-
-End BetreeMain_Types .
+End BetreeMain_Types.
diff --git a/tests/coq/betree/BetreeMain_TypesExternal.v b/tests/coq/betree/BetreeMain_TypesExternal.v
new file mode 100644
index 00000000..50c4a4f8
--- /dev/null
+++ b/tests/coq/betree/BetreeMain_TypesExternal.v
@@ -0,0 +1,15 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module BetreeMain_TypesExternal.
+
+(** The state type used in the state-error monad *)
+Axiom state : Type.
+
+End BetreeMain_TypesExternal.
diff --git a/tests/coq/betree/BetreeMain_TypesExternal_Template.v b/tests/coq/betree/BetreeMain_TypesExternal_Template.v
new file mode 100644
index 00000000..651de2b7
--- /dev/null
+++ b/tests/coq/betree/BetreeMain_TypesExternal_Template.v
@@ -0,0 +1,15 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module BetreeMain_TypesExternal_Template.
+
+(** The state type used in the state-error monad *)
+Axiom state : Type.
+
+End BetreeMain_TypesExternal_Template.
diff --git a/tests/coq/betree/_CoqProject b/tests/coq/betree/_CoqProject
index 9ab8ea9f..13e4b9c1 100644
--- a/tests/coq/betree/_CoqProject
+++ b/tests/coq/betree/_CoqProject
@@ -4,7 +4,9 @@
 -arg all
 
 BetreeMain_Types.v
+BetreeMain_TypesExternal_Template.v
 Primitives.v
 BetreeMain_FunsExternal_Template.v
 BetreeMain_Funs.v
+BetreeMain_TypesExternal.v
 BetreeMain_FunsExternal.v
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index c08f7f7d..64de44a6 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -6,8 +6,8 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
-Require Export Hashmap_Types.
-Import Hashmap_Types.
+Require Import Hashmap_Types.
+Include Hashmap_Types.
 Module Hashmap_Funs.
 
 (** [hashmap::hash_key]: forward function
@@ -668,4 +668,4 @@ Definition test1 (n : nat) : result unit :=
       end))
 .
 
-End Hashmap_Funs .
+End Hashmap_Funs.
diff --git a/tests/coq/hashmap/Hashmap_Types.v b/tests/coq/hashmap/Hashmap_Types.v
index bfb5ae4b..80a43593 100644
--- a/tests/coq/hashmap/Hashmap_Types.v
+++ b/tests/coq/hashmap/Hashmap_Types.v
@@ -35,4 +35,4 @@ Arguments hashMap_max_load_factor { _ }.
 Arguments hashMap_max_load { _ }.
 Arguments hashMap_slots { _ }.
 
-End Hashmap_Types .
+End Hashmap_Types.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 188c98b3..faba0afe 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -6,10 +6,10 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
-Require Export HashmapMain_Types.
-Import HashmapMain_Types.
-Require Export HashmapMain_FunsExternal.
-Import HashmapMain_FunsExternal.
+Require Import HashmapMain_Types.
+Include HashmapMain_Types.
+Require Import HashmapMain_FunsExternal.
+Include HashmapMain_FunsExternal.
 Module HashmapMain_Funs.
 
 (** [hashmap_main::hashmap::hash_key]: forward function
@@ -717,4 +717,4 @@ Definition insert_on_disk
 Definition main : result unit :=
   Return tt.
 
-End HashmapMain_Funs .
+End HashmapMain_Funs.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v
index b5a4a101..e10d02f6 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v
@@ -7,8 +7,8 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
-Require Export HashmapMain_Types.
-Import HashmapMain_Types.
+Require Import HashmapMain_Types.
+Include HashmapMain_Types.
 Module HashmapMain_FunsExternal_Template.
 
 (** [hashmap_main::hashmap_utils::deserialize]: forward function
@@ -23,4 +23,4 @@ Axiom hashmap_utils_serialize
   : hashmap_HashMap_t u64 -> state -> result (state * unit)
 .
 
-End HashmapMain_FunsExternal_Template .
+End HashmapMain_FunsExternal_Template.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Types.v b/tests/coq/hashmap_on_disk/HashmapMain_Types.v
index 039b7e72..8d3d72aa 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Types.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Types.v
@@ -6,6 +6,8 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
+Require Import HashmapMain_TypesExternal.
+Include HashmapMain_TypesExternal.
 Module HashmapMain_Types.
 
 (** [hashmap_main::hashmap::List]
@@ -35,7 +37,4 @@ Arguments hashmap_HashMap_max_load_factor { _ }.
 Arguments hashmap_HashMap_max_load { _ }.
 Arguments hashmap_HashMap_slots { _ }.
 
-(** The state type used in the state-error monad *)
-Axiom state : Type.
-
-End HashmapMain_Types .
+End HashmapMain_Types.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v b/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v
new file mode 100644
index 00000000..87568232
--- /dev/null
+++ b/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v
@@ -0,0 +1,15 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module HashmapMain_TypesExternal.
+
+(** The state type used in the state-error monad *)
+Axiom state : Type.
+
+End HashmapMain_TypesExternal.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal_Template.v b/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal_Template.v
new file mode 100644
index 00000000..391b2775
--- /dev/null
+++ b/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal_Template.v
@@ -0,0 +1,15 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module HashmapMain_TypesExternal_Template.
+
+(** The state type used in the state-error monad *)
+Axiom state : Type.
+
+End HashmapMain_TypesExternal_Template.
diff --git a/tests/coq/hashmap_on_disk/_CoqProject b/tests/coq/hashmap_on_disk/_CoqProject
index a85fa1fe..41945494 100644
--- a/tests/coq/hashmap_on_disk/_CoqProject
+++ b/tests/coq/hashmap_on_disk/_CoqProject
@@ -6,5 +6,7 @@
 HashmapMain_Types.v
 Primitives.v
 HashmapMain_Funs.v
+HashmapMain_TypesExternal.v
 HashmapMain_FunsExternal_Template.v
 HashmapMain_FunsExternal.v
+HashmapMain_TypesExternal_Template.v
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v
index 20edb2b1..ad899f25 100644
--- a/tests/coq/misc/Constants.v
+++ b/tests/coq/misc/Constants.v
@@ -157,4 +157,4 @@ Definition s3_c : Pair_t u32 u32 := s3_body%global.
 Definition s4_body : result (Pair_t u32 u32) := mk_pair1 7%u32 8%u32.
 Definition s4_c : Pair_t u32 u32 := s4_body%global.
 
-End Constants .
+End Constants.
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index 8a3360bb..e9d39f66 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -6,10 +6,10 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
-Require Export External_Types.
-Import External_Types.
-Require Export External_FunsExternal.
-Import External_FunsExternal.
+Require Import External_Types.
+Include External_Types.
+Require Import External_FunsExternal.
+Include External_FunsExternal.
 Module External_Funs.
 
 (** [external::swap]: forward function
@@ -115,4 +115,4 @@ Definition test_swap_non_zero (x : u32) (st : state) : result (state * u32) :=
   if x0 s= 0%u32 then Fail_ Failure else Return (st1, x0)
 .
 
-End External_Funs .
+End External_Funs.
diff --git a/tests/coq/misc/External_FunsExternal.v b/tests/coq/misc/External_FunsExternal.v
index 07d43061..a8c5756a 100644
--- a/tests/coq/misc/External_FunsExternal.v
+++ b/tests/coq/misc/External_FunsExternal.v
@@ -7,7 +7,7 @@ Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
 Require Export External_Types.
-Import External_Types.
+Include External_Types.
 Module External_FunsExternal.
 
 (** [core::mem::swap]: forward function
diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v
index 0977c3ae..31e69c39 100644
--- a/tests/coq/misc/External_FunsExternal_Template.v
+++ b/tests/coq/misc/External_FunsExternal_Template.v
@@ -7,8 +7,8 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
-Require Export External_Types.
-Import External_Types.
+Require Import External_Types.
+Include External_Types.
 Module External_FunsExternal_Template.
 
 (** [core::mem::swap]: forward function
@@ -41,4 +41,4 @@ Axiom core_option_Option_unwrap :
   forall(T : Type), option T -> state -> result (state * T)
 .
 
-End External_FunsExternal_Template .
+End External_FunsExternal_Template.
diff --git a/tests/coq/misc/External_Types.v b/tests/coq/misc/External_Types.v
index c638670c..b42c2ecf 100644
--- a/tests/coq/misc/External_Types.v
+++ b/tests/coq/misc/External_Types.v
@@ -6,13 +6,8 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
+Require Import External_TypesExternal.
+Include External_TypesExternal.
 Module External_Types.
 
-(** [core::num::nonzero::NonZeroU32]
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
-Axiom core_num_nonzero_NonZeroU32_t : Type.
-
-(** The state type used in the state-error monad *)
-Axiom state : Type.
-
-End External_Types .
+End External_Types.
diff --git a/tests/coq/misc/External_TypesExternal.v b/tests/coq/misc/External_TypesExternal.v
new file mode 100644
index 00000000..3f02b839
--- /dev/null
+++ b/tests/coq/misc/External_TypesExternal.v
@@ -0,0 +1,19 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module External_TypesExternal.
+
+(** [core::num::nonzero::NonZeroU32]
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
+Axiom core_num_nonzero_NonZeroU32_t : Type.
+
+(** The state type used in the state-error monad *)
+Axiom state : Type.
+
+End External_TypesExternal.
diff --git a/tests/coq/misc/External_TypesExternal_Template.v b/tests/coq/misc/External_TypesExternal_Template.v
new file mode 100644
index 00000000..7ba79d8e
--- /dev/null
+++ b/tests/coq/misc/External_TypesExternal_Template.v
@@ -0,0 +1,19 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module External_TypesExternal_Template.
+
+(** [core::num::nonzero::NonZeroU32]
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
+Axiom core_num_nonzero_NonZeroU32_t : Type.
+
+(** The state type used in the state-error monad *)
+Axiom state : Type.
+
+End External_TypesExternal_Template.
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 4929ddd0..83c249c1 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -914,4 +914,4 @@ Definition list_nth_shared_mut_loop_pair_merge_back
   list_nth_shared_mut_loop_pair_merge_loop_back T n ls0 ls1 i ret
 .
 
-End Loops .
+End Loops.
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index b044d24f..16a2e816 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -586,4 +586,4 @@ Definition test_shared_borrow_enum1 (l : List_t u32) : result u32 :=
 Definition test_shared_borrow_enum2 : result u32 :=
   Return 0%u32.
 
-End NoNestedBorrows .
+End NoNestedBorrows.
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index 4a49096f..6b110193 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -128,4 +128,4 @@ Definition call_choose (p : (u32 * u32)) : result u32 :=
   Return px0
 .
 
-End Paper .
+End Paper.
diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v
index a0820e40..2371b1cc 100644
--- a/tests/coq/misc/PoloniusList.v
+++ b/tests/coq/misc/PoloniusList.v
@@ -41,4 +41,4 @@ Fixpoint get_list_at_x_back
   end
 .
 
-End PoloniusList .
+End PoloniusList.
diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject
index 6884d5d9..0828bced 100644
--- a/tests/coq/misc/_CoqProject
+++ b/tests/coq/misc/_CoqProject
@@ -4,12 +4,14 @@
 -arg all
 
 Loops.v
+External_Types.v
 Primitives.v
 External_Funs.v
+Paper.v
+External_TypesExternal.v
 Constants.v
 PoloniusList.v
-External_Types.v
 NoNestedBorrows.v
 External_FunsExternal.v
+External_TypesExternal_Template.v
 External_FunsExternal_Template.v
-Paper.v
diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
index 50eaf848..ebdca4ec 100644
--- a/tests/coq/traits/Traits.v
+++ b/tests/coq/traits/Traits.v
@@ -611,4 +611,4 @@ Arguments CFn_t_call_mut { _ _ }.
 Definition incr_u32 (x : u32) : result u32 :=
   u32_add x 1%u32.
 
-End Traits .
+End Traits.
diff --git a/tests/fstar/betree/BetreeMain.Types.fsti b/tests/fstar/betree/BetreeMain.Types.fst
index a098ec19..b87219b2 100644
--- a/tests/fstar/betree/BetreeMain.Types.fsti
+++ b/tests/fstar/betree/BetreeMain.Types.fst
@@ -2,6 +2,7 @@
 (** [betree_main]: type definitions *)
 module BetreeMain.Types
 open Primitives
+include BetreeMain.TypesExternal
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
@@ -58,6 +59,3 @@ type betree_BeTree_t =
   root : betree_Node_t;
 }
 
-(** The state type used in the state-error monad *)
-val state : Type0
-
diff --git a/tests/fstar/betree/BetreeMain.TypesExternal.fsti b/tests/fstar/betree/BetreeMain.TypesExternal.fsti
new file mode 100644
index 00000000..1b2c53a6
--- /dev/null
+++ b/tests/fstar/betree/BetreeMain.TypesExternal.fsti
@@ -0,0 +1,10 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: external type declarations *)
+module BetreeMain.TypesExternal
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** The state type used in the state-error monad *)
+val state : Type0
+
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti b/tests/fstar/betree_back_stateful/BetreeMain.Types.fst
index a098ec19..b87219b2 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Types.fst
@@ -2,6 +2,7 @@
 (** [betree_main]: type definitions *)
 module BetreeMain.Types
 open Primitives
+include BetreeMain.TypesExternal
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
@@ -58,6 +59,3 @@ type betree_BeTree_t =
   root : betree_Node_t;
 }
 
-(** The state type used in the state-error monad *)
-val state : Type0
-
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti b/tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti
new file mode 100644
index 00000000..1b2c53a6
--- /dev/null
+++ b/tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti
@@ -0,0 +1,10 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: external type declarations *)
+module BetreeMain.TypesExternal
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** The state type used in the state-error monad *)
+val state : Type0
+
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.Types.fst
index e77954ad..afebcde3 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Types.fst
@@ -2,6 +2,7 @@
 (** [hashmap_main]: type definitions *)
 module HashmapMain.Types
 open Primitives
+include HashmapMain.TypesExternal
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
@@ -21,6 +22,3 @@ type hashmap_HashMap_t (t : Type0) =
   slots : alloc_vec_Vec (hashmap_List_t t);
 }
 
-(** The state type used in the state-error monad *)
-val state : Type0
-
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti
new file mode 100644
index 00000000..75747408
--- /dev/null
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti
@@ -0,0 +1,10 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: external type declarations *)
+module HashmapMain.TypesExternal
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** The state type used in the state-error monad *)
+val state : Type0
+
diff --git a/tests/fstar/misc/External.Types.fst b/tests/fstar/misc/External.Types.fst
new file mode 100644
index 00000000..4fbcec47
--- /dev/null
+++ b/tests/fstar/misc/External.Types.fst
@@ -0,0 +1,8 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: type definitions *)
+module External.Types
+open Primitives
+include External.TypesExternal
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
diff --git a/tests/fstar/misc/External.Types.fsti b/tests/fstar/misc/External.TypesExternal.fsti
index 0cb9fd0e..4bfbe0c5 100644
--- a/tests/fstar/misc/External.Types.fsti
+++ b/tests/fstar/misc/External.TypesExternal.fsti
@@ -1,6 +1,6 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [external]: type definitions *)
-module External.Types
+(** [external]: external type declarations *)
+module External.TypesExternal
 open Primitives
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
diff --git a/tests/lean/BetreeMain/Types.lean b/tests/lean/BetreeMain/Types.lean
index 6e528437..877508f6 100644
--- a/tests/lean/BetreeMain/Types.lean
+++ b/tests/lean/BetreeMain/Types.lean
@@ -1,6 +1,7 @@
 -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
 -- [betree_main]: type definitions
 import Base
+import BetreeMain.TypesExternal
 open Primitives
 
 namespace betree_main
@@ -63,7 +64,4 @@ structure betree.BeTree where
   node_id_cnt : betree.NodeIdCounter
   root : betree.Node
 
-/- The state type used in the state-error monad -/
-axiom State : Type
-
 end betree_main
diff --git a/tests/lean/BetreeMain/TypesExternal.lean b/tests/lean/BetreeMain/TypesExternal.lean
new file mode 100644
index 00000000..1701eaaf
--- /dev/null
+++ b/tests/lean/BetreeMain/TypesExternal.lean
@@ -0,0 +1,7 @@
+-- [betree_main]: external types.
+import Base
+open Primitives
+
+/- The state type used in the state-error monad -/
+axiom State : Type
+
diff --git a/tests/lean/BetreeMain/TypesExternal_Template.lean b/tests/lean/BetreeMain/TypesExternal_Template.lean
new file mode 100644
index 00000000..bbac7e99
--- /dev/null
+++ b/tests/lean/BetreeMain/TypesExternal_Template.lean
@@ -0,0 +1,9 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [betree_main]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes.
+import Base
+open Primitives
+
+/- The state type used in the state-error monad -/
+axiom State : Type
+
diff --git a/tests/lean/External/Types.lean b/tests/lean/External/Types.lean
index 40f20cda..961f3e8a 100644
--- a/tests/lean/External/Types.lean
+++ b/tests/lean/External/Types.lean
@@ -1,15 +1,9 @@
 -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
 -- [external]: type definitions
 import Base
+import External.TypesExternal
 open Primitives
 
 namespace external
 
-/- [core::num::nonzero::NonZeroU32]
-   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 -/
-axiom core.num.nonzero.NonZeroU32 : Type
-
-/- The state type used in the state-error monad -/
-axiom State : Type
-
 end external
diff --git a/tests/lean/External/TypesExternal.lean b/tests/lean/External/TypesExternal.lean
new file mode 100644
index 00000000..7c30f792
--- /dev/null
+++ b/tests/lean/External/TypesExternal.lean
@@ -0,0 +1,11 @@
+-- [external]: external types.
+import Base
+open Primitives
+
+/- [core::num::nonzero::NonZeroU32]
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 -/
+axiom core.num.nonzero.NonZeroU32 : Type
+
+/- The state type used in the state-error monad -/
+axiom State : Type
+
diff --git a/tests/lean/External/TypesExternal_Template.lean b/tests/lean/External/TypesExternal_Template.lean
new file mode 100644
index 00000000..85fef236
--- /dev/null
+++ b/tests/lean/External/TypesExternal_Template.lean
@@ -0,0 +1,13 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [external]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes.
+import Base
+open Primitives
+
+/- [core::num::nonzero::NonZeroU32]
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 -/
+axiom core.num.nonzero.NonZeroU32 : Type
+
+/- The state type used in the state-error monad -/
+axiom State : Type
+
diff --git a/tests/lean/HashmapMain/Types.lean b/tests/lean/HashmapMain/Types.lean
index f7be6719..ae9ac999 100644
--- a/tests/lean/HashmapMain/Types.lean
+++ b/tests/lean/HashmapMain/Types.lean
@@ -1,6 +1,7 @@
 -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
 -- [hashmap_main]: type definitions
 import Base
+import HashmapMain.TypesExternal
 open Primitives
 
 namespace hashmap_main
@@ -19,7 +20,4 @@ structure hashmap.HashMap (T : Type) where
   max_load : Usize
   slots : alloc.vec.Vec (hashmap.List T)
 
-/- The state type used in the state-error monad -/
-axiom State : Type
-
 end hashmap_main
diff --git a/tests/lean/HashmapMain/TypesExternal.lean b/tests/lean/HashmapMain/TypesExternal.lean
new file mode 100644
index 00000000..4e1cdbe9
--- /dev/null
+++ b/tests/lean/HashmapMain/TypesExternal.lean
@@ -0,0 +1,7 @@
+-- [hashmap_main]: external types.
+import Base
+open Primitives
+
+/- The state type used in the state-error monad -/
+axiom State : Type
+
diff --git a/tests/lean/HashmapMain/TypesExternal_Template.lean b/tests/lean/HashmapMain/TypesExternal_Template.lean
new file mode 100644
index 00000000..cfa8bbb1
--- /dev/null
+++ b/tests/lean/HashmapMain/TypesExternal_Template.lean
@@ -0,0 +1,9 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [hashmap_main]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes.
+import Base
+open Primitives
+
+/- The state type used in the state-error monad -/
+axiom State : Type
+