Merge pull request #46 from AeneasVerif/son_improves

Minor improvements for the extraction

9 files changed, 74 insertions, 16 deletions

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 46d3ee29..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_Opaque.
-Import HashmapMain_Opaque.
+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_Opaque.v b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v
index a0e9003d..a03dc407 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v
@@ -8,7 +8,7 @@ Import ListNotations.
 Local Open Scope Primitives_scope.
 Require Export HashmapMain_Types.
 Import HashmapMain_Types.
-Module HashmapMain_Opaque.
+Module HashmapMain_FunsExternal.
 
 (** [hashmap_main::hashmap_utils::deserialize]: forward function
     Source: 'src/hashmap_utils.rs', lines 10:0-10:43 *)
@@ -22,4 +22,4 @@ Axiom hashmap_utils_serialize
   : hashmap_HashMap_t u64 -> state -> result (state * unit)
 .
 
-End HashmapMain_Opaque .
+End HashmapMain_FunsExternal.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v
new file mode 100644
index 00000000..e10d02f6
--- /dev/null
+++ b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v
@@ -0,0 +1,26 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: external functions.
+-- This is a template file: rename it to "FunsExternal.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.
+Require Import HashmapMain_Types.
+Include HashmapMain_Types.
+Module HashmapMain_FunsExternal_Template.
+
+(** [hashmap_main::hashmap_utils::deserialize]: forward function
+    Source: 'src/hashmap_utils.rs', lines 10:0-10:43 *)
+Axiom hashmap_utils_deserialize
+  : state -> result (state * (hashmap_HashMap_t u64))
+.
+
+(** [hashmap_main::hashmap_utils::serialize]: forward function
+    Source: 'src/hashmap_utils.rs', lines 5:0-5:42 *)
+Axiom hashmap_utils_serialize
+  : hashmap_HashMap_t u64 -> state -> result (state * unit)
+.
+
+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 b78c7b5f..41945494 100644
--- a/tests/coq/hashmap_on_disk/_CoqProject
+++ b/tests/coq/hashmap_on_disk/_CoqProject
@@ -6,4 +6,7 @@
 HashmapMain_Types.v
 Primitives.v
 HashmapMain_Funs.v
-HashmapMain_Opaque.v
+HashmapMain_TypesExternal.v
+HashmapMain_FunsExternal_Template.v
+HashmapMain_FunsExternal.v
+HashmapMain_TypesExternal_Template.v