summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-11-27 10:29:25 +0100
committerSon Ho2023-11-27 10:29:25 +0100
commitbef2bd34fcb0817f1b7d16b95122bcc3c6f05c72 (patch)
treeb491462e77665dceb44b4899f97508d440c57d6a
parent959d6fce38c8d8ca6eaed3ad6f458b87f91a9abc (diff)
Generate a dedicated file for the external types
-rw-r--r--compiler/Translate.ml114
-rw-r--r--tests/coq/array/Array.v2
-rw-r--r--tests/coq/betree/BetreeMain_Funs.v10
-rw-r--r--tests/coq/betree/BetreeMain_FunsExternal_Template.v6
-rw-r--r--tests/coq/betree/BetreeMain_Types.v7
-rw-r--r--tests/coq/betree/BetreeMain_TypesExternal.v15
-rw-r--r--tests/coq/betree/BetreeMain_TypesExternal_Template.v15
-rw-r--r--tests/coq/betree/_CoqProject2
-rw-r--r--tests/coq/hashmap/Hashmap_Funs.v6
-rw-r--r--tests/coq/hashmap/Hashmap_Types.v2
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Funs.v10
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v6
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Types.v7
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v15
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_TypesExternal_Template.v15
-rw-r--r--tests/coq/hashmap_on_disk/_CoqProject2
-rw-r--r--tests/coq/misc/Constants.v2
-rw-r--r--tests/coq/misc/External_Funs.v10
-rw-r--r--tests/coq/misc/External_FunsExternal.v2
-rw-r--r--tests/coq/misc/External_FunsExternal_Template.v6
-rw-r--r--tests/coq/misc/External_Types.v11
-rw-r--r--tests/coq/misc/External_TypesExternal.v19
-rw-r--r--tests/coq/misc/External_TypesExternal_Template.v19
-rw-r--r--tests/coq/misc/Loops.v2
-rw-r--r--tests/coq/misc/NoNestedBorrows.v2
-rw-r--r--tests/coq/misc/Paper.v2
-rw-r--r--tests/coq/misc/PoloniusList.v2
-rw-r--r--tests/coq/misc/_CoqProject6
-rw-r--r--tests/coq/traits/Traits.v2
-rw-r--r--tests/fstar/betree/BetreeMain.Types.fst (renamed from tests/fstar/betree/BetreeMain.Types.fsti)4
-rw-r--r--tests/fstar/betree/BetreeMain.TypesExternal.fsti10
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.Types.fst (renamed from tests/fstar/betree_back_stateful/BetreeMain.Types.fsti)4
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti10
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Types.fst (renamed from tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti)4
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti10
-rw-r--r--tests/fstar/misc/External.Types.fst8
-rw-r--r--tests/fstar/misc/External.TypesExternal.fsti (renamed from tests/fstar/misc/External.Types.fsti)4
-rw-r--r--tests/lean/BetreeMain/Types.lean4
-rw-r--r--tests/lean/BetreeMain/TypesExternal.lean7
-rw-r--r--tests/lean/BetreeMain/TypesExternal_Template.lean9
-rw-r--r--tests/lean/External/Types.lean8
-rw-r--r--tests/lean/External/TypesExternal.lean11
-rw-r--r--tests/lean/External/TypesExternal_Template.lean13
-rw-r--r--tests/lean/HashmapMain/Types.lean4
-rw-r--r--tests/lean/HashmapMain/TypesExternal.lean7
-rw-r--r--tests/lean/HashmapMain/TypesExternal_Template.lean9
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
+