diff options
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 + |