From d84040e000333d6d2a212fb849a38fb73a65eb48 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 24 Nov 2023 17:41:42 +0100
Subject: Regenerate the files
---
tests/fstar/traits/Traits.fst | 10 ++--------
1 file changed, 2 insertions(+), 8 deletions(-)
(limited to 'tests/fstar')
diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst
index 4cb9fbf1..895a1cac 100644
--- a/tests/fstar/traits/Traits.fst
+++ b/tests/fstar/traits/Traits.fst
@@ -307,15 +307,11 @@ let test_where2
=
Return ()
-(** [alloc::string::String]
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/string.rs', lines 365:0-365:17 *)
-assume type alloc_string_String_t : Type0
-
(** Trait declaration: [traits::ParentTrait0]
Source: 'src/traits.rs', lines 200:0-200:22 *)
noeq type parentTrait0_t (self : Type0) = {
tW : Type0;
- get_name : self -> result alloc_string_String_t;
+ get_name : self -> result string;
get_w : self -> result tW;
}
@@ -333,9 +329,7 @@ noeq type childTrait_t (self : Type0) = {
(** [traits::test_child_trait1]: forward function
Source: 'src/traits.rs', lines 209:0-209:56 *)
let test_child_trait1
- (t : Type0) (childTraitTInst : childTrait_t t) (x : t) :
- result alloc_string_String_t
- =
+ (t : Type0) (childTraitTInst : childTrait_t t) (x : t) : result string =
childTraitTInst.parentTrait0SelfInst.get_name x
(** [traits::test_child_trait2]: forward function
--
cgit v1.2.3
From 959d6fce38c8d8ca6eaed3ad6f458b87f91a9abc Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 27 Nov 2023 09:37:31 +0100
Subject: Update the generation of files for external definitions and
regenerate the tests
---
tests/fstar/betree/BetreeMain.Funs.fst | 2 +-
tests/fstar/betree/BetreeMain.FunsExternal.fsti | 35 ++++++++++++++++++++++
tests/fstar/betree/BetreeMain.Opaque.fsti | 35 ----------------------
.../fstar/betree_back_stateful/BetreeMain.Funs.fst | 2 +-
.../BetreeMain.FunsExternal.fsti | 35 ++++++++++++++++++++++
.../betree_back_stateful/BetreeMain.Opaque.fsti | 35 ----------------------
tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 2 +-
.../hashmap_on_disk/HashmapMain.FunsExternal.fsti | 18 +++++++++++
.../fstar/hashmap_on_disk/HashmapMain.Opaque.fsti | 18 -----------
tests/fstar/misc/External.Funs.fst | 2 +-
tests/fstar/misc/External.FunsExternal.fsti | 32 ++++++++++++++++++++
tests/fstar/misc/External.Opaque.fsti | 32 --------------------
12 files changed, 124 insertions(+), 124 deletions(-)
create mode 100644 tests/fstar/betree/BetreeMain.FunsExternal.fsti
delete mode 100644 tests/fstar/betree/BetreeMain.Opaque.fsti
create mode 100644 tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
delete mode 100644 tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti
create mode 100644 tests/fstar/hashmap_on_disk/HashmapMain.FunsExternal.fsti
delete mode 100644 tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti
create mode 100644 tests/fstar/misc/External.FunsExternal.fsti
delete mode 100644 tests/fstar/misc/External.Opaque.fsti
(limited to 'tests/fstar')
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index 537ec32e..fef8a8e1 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -3,7 +3,7 @@
module BetreeMain.Funs
open Primitives
include BetreeMain.Types
-include BetreeMain.Opaque
+include BetreeMain.FunsExternal
include BetreeMain.Clauses
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
diff --git a/tests/fstar/betree/BetreeMain.FunsExternal.fsti b/tests/fstar/betree/BetreeMain.FunsExternal.fsti
new file mode 100644
index 00000000..cd2f956f
--- /dev/null
+++ b/tests/fstar/betree/BetreeMain.FunsExternal.fsti
@@ -0,0 +1,35 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: external function declarations *)
+module BetreeMain.FunsExternal
+open Primitives
+include BetreeMain.Types
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [betree_main::betree_utils::load_internal_node]: forward function
+ Source: 'src/betree_utils.rs', lines 98:0-98:63 *)
+val betree_utils_load_internal_node
+ : u64 -> state -> result (state & (betree_List_t (u64 & betree_Message_t)))
+
+(** [betree_main::betree_utils::store_internal_node]: forward function
+ Source: 'src/betree_utils.rs', lines 115:0-115:71 *)
+val betree_utils_store_internal_node
+ :
+ u64 -> betree_List_t (u64 & betree_Message_t) -> state -> result (state &
+ unit)
+
+(** [betree_main::betree_utils::load_leaf_node]: forward function
+ Source: 'src/betree_utils.rs', lines 132:0-132:55 *)
+val betree_utils_load_leaf_node
+ : u64 -> state -> result (state & (betree_List_t (u64 & u64)))
+
+(** [betree_main::betree_utils::store_leaf_node]: forward function
+ Source: 'src/betree_utils.rs', lines 145:0-145:63 *)
+val betree_utils_store_leaf_node
+ : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit)
+
+(** [core::option::{core::option::Option<T>}::unwrap]: forward function
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+val core_option_Option_unwrap
+ (t : Type0) : option t -> state -> result (state & t)
+
diff --git a/tests/fstar/betree/BetreeMain.Opaque.fsti b/tests/fstar/betree/BetreeMain.Opaque.fsti
deleted file mode 100644
index b89c8718..00000000
--- a/tests/fstar/betree/BetreeMain.Opaque.fsti
+++ /dev/null
@@ -1,35 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: external function declarations *)
-module BetreeMain.Opaque
-open Primitives
-include BetreeMain.Types
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [betree_main::betree_utils::load_internal_node]: forward function
- Source: 'src/betree_utils.rs', lines 98:0-98:63 *)
-val betree_utils_load_internal_node
- : u64 -> state -> result (state & (betree_List_t (u64 & betree_Message_t)))
-
-(** [betree_main::betree_utils::store_internal_node]: forward function
- Source: 'src/betree_utils.rs', lines 115:0-115:71 *)
-val betree_utils_store_internal_node
- :
- u64 -> betree_List_t (u64 & betree_Message_t) -> state -> result (state &
- unit)
-
-(** [betree_main::betree_utils::load_leaf_node]: forward function
- Source: 'src/betree_utils.rs', lines 132:0-132:55 *)
-val betree_utils_load_leaf_node
- : u64 -> state -> result (state & (betree_List_t (u64 & u64)))
-
-(** [betree_main::betree_utils::store_leaf_node]: forward function
- Source: 'src/betree_utils.rs', lines 145:0-145:63 *)
-val betree_utils_store_leaf_node
- : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit)
-
-(** [core::option::{core::option::Option<T>}::unwrap]: forward function
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
-val core_option_Option_unwrap
- (t : Type0) : option t -> state -> result (state & t)
-
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index a2586431..b912a316 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -3,7 +3,7 @@
module BetreeMain.Funs
open Primitives
include BetreeMain.Types
-include BetreeMain.Opaque
+include BetreeMain.FunsExternal
include BetreeMain.Clauses
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
new file mode 100644
index 00000000..cd2f956f
--- /dev/null
+++ b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
@@ -0,0 +1,35 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: external function declarations *)
+module BetreeMain.FunsExternal
+open Primitives
+include BetreeMain.Types
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [betree_main::betree_utils::load_internal_node]: forward function
+ Source: 'src/betree_utils.rs', lines 98:0-98:63 *)
+val betree_utils_load_internal_node
+ : u64 -> state -> result (state & (betree_List_t (u64 & betree_Message_t)))
+
+(** [betree_main::betree_utils::store_internal_node]: forward function
+ Source: 'src/betree_utils.rs', lines 115:0-115:71 *)
+val betree_utils_store_internal_node
+ :
+ u64 -> betree_List_t (u64 & betree_Message_t) -> state -> result (state &
+ unit)
+
+(** [betree_main::betree_utils::load_leaf_node]: forward function
+ Source: 'src/betree_utils.rs', lines 132:0-132:55 *)
+val betree_utils_load_leaf_node
+ : u64 -> state -> result (state & (betree_List_t (u64 & u64)))
+
+(** [betree_main::betree_utils::store_leaf_node]: forward function
+ Source: 'src/betree_utils.rs', lines 145:0-145:63 *)
+val betree_utils_store_leaf_node
+ : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit)
+
+(** [core::option::{core::option::Option<T>}::unwrap]: forward function
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+val core_option_Option_unwrap
+ (t : Type0) : option t -> state -> result (state & t)
+
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti b/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti
deleted file mode 100644
index b89c8718..00000000
--- a/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti
+++ /dev/null
@@ -1,35 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: external function declarations *)
-module BetreeMain.Opaque
-open Primitives
-include BetreeMain.Types
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [betree_main::betree_utils::load_internal_node]: forward function
- Source: 'src/betree_utils.rs', lines 98:0-98:63 *)
-val betree_utils_load_internal_node
- : u64 -> state -> result (state & (betree_List_t (u64 & betree_Message_t)))
-
-(** [betree_main::betree_utils::store_internal_node]: forward function
- Source: 'src/betree_utils.rs', lines 115:0-115:71 *)
-val betree_utils_store_internal_node
- :
- u64 -> betree_List_t (u64 & betree_Message_t) -> state -> result (state &
- unit)
-
-(** [betree_main::betree_utils::load_leaf_node]: forward function
- Source: 'src/betree_utils.rs', lines 132:0-132:55 *)
-val betree_utils_load_leaf_node
- : u64 -> state -> result (state & (betree_List_t (u64 & u64)))
-
-(** [betree_main::betree_utils::store_leaf_node]: forward function
- Source: 'src/betree_utils.rs', lines 145:0-145:63 *)
-val betree_utils_store_leaf_node
- : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit)
-
-(** [core::option::{core::option::Option<T>}::unwrap]: forward function
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
-val core_option_Option_unwrap
- (t : Type0) : option t -> state -> result (state & t)
-
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index fa570309..f2d09a38 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -3,7 +3,7 @@
module HashmapMain.Funs
open Primitives
include HashmapMain.Types
-include HashmapMain.Opaque
+include HashmapMain.FunsExternal
include HashmapMain.Clauses
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.FunsExternal.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.FunsExternal.fsti
new file mode 100644
index 00000000..b00bbcde
--- /dev/null
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.FunsExternal.fsti
@@ -0,0 +1,18 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: external function declarations *)
+module HashmapMain.FunsExternal
+open Primitives
+include HashmapMain.Types
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [hashmap_main::hashmap_utils::deserialize]: forward function
+ Source: 'src/hashmap_utils.rs', lines 10:0-10:43 *)
+val 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 *)
+val hashmap_utils_serialize
+ : hashmap_HashMap_t u64 -> state -> result (state & unit)
+
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti
deleted file mode 100644
index 1f47eb33..00000000
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti
+++ /dev/null
@@ -1,18 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [hashmap_main]: external function declarations *)
-module HashmapMain.Opaque
-open Primitives
-include HashmapMain.Types
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [hashmap_main::hashmap_utils::deserialize]: forward function
- Source: 'src/hashmap_utils.rs', lines 10:0-10:43 *)
-val 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 *)
-val hashmap_utils_serialize
- : hashmap_HashMap_t u64 -> state -> result (state & unit)
-
diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst
index 4d13fb71..00995634 100644
--- a/tests/fstar/misc/External.Funs.fst
+++ b/tests/fstar/misc/External.Funs.fst
@@ -3,7 +3,7 @@
module External.Funs
open Primitives
include External.Types
-include External.Opaque
+include External.FunsExternal
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
diff --git a/tests/fstar/misc/External.FunsExternal.fsti b/tests/fstar/misc/External.FunsExternal.fsti
new file mode 100644
index 00000000..923a1101
--- /dev/null
+++ b/tests/fstar/misc/External.FunsExternal.fsti
@@ -0,0 +1,32 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: external function declarations *)
+module External.FunsExternal
+open Primitives
+include External.Types
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [core::mem::swap]: forward function
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+val core_mem_swap (t : Type0) : t -> t -> state -> result (state & unit)
+
+(** [core::mem::swap]: backward function 0
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+val core_mem_swap_back0
+ (t : Type0) : t -> t -> state -> state -> result (state & t)
+
+(** [core::mem::swap]: backward function 1
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+val core_mem_swap_back1
+ (t : Type0) : t -> t -> state -> state -> result (state & t)
+
+(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *)
+val core_num_nonzero_NonZeroU32_new
+ : u32 -> state -> result (state & (option core_num_nonzero_NonZeroU32_t))
+
+(** [core::option::{core::option::Option<T>}::unwrap]: forward function
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+val core_option_Option_unwrap
+ (t : Type0) : option t -> state -> result (state & t)
+
diff --git a/tests/fstar/misc/External.Opaque.fsti b/tests/fstar/misc/External.Opaque.fsti
deleted file mode 100644
index ea1a70c2..00000000
--- a/tests/fstar/misc/External.Opaque.fsti
+++ /dev/null
@@ -1,32 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [external]: external function declarations *)
-module External.Opaque
-open Primitives
-include External.Types
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [core::mem::swap]: forward function
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
-val core_mem_swap (t : Type0) : t -> t -> state -> result (state & unit)
-
-(** [core::mem::swap]: backward function 0
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
-val core_mem_swap_back0
- (t : Type0) : t -> t -> state -> state -> result (state & t)
-
-(** [core::mem::swap]: backward function 1
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
-val core_mem_swap_back1
- (t : Type0) : t -> t -> state -> state -> result (state & t)
-
-(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *)
-val core_num_nonzero_NonZeroU32_new
- : u32 -> state -> result (state & (option core_num_nonzero_NonZeroU32_t))
-
-(** [core::option::{core::option::Option<T>}::unwrap]: forward function
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
-val core_option_Option_unwrap
- (t : Type0) : option t -> state -> result (state & t)
-
--
cgit v1.2.3
From bef2bd34fcb0817f1b7d16b95122bcc3c6f05c72 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 27 Nov 2023 10:29:25 +0100
Subject: Generate a dedicated file for the external types
---
tests/fstar/betree/BetreeMain.Types.fst | 61 +++++++++++++++++++++
tests/fstar/betree/BetreeMain.Types.fsti | 63 ----------------------
tests/fstar/betree/BetreeMain.TypesExternal.fsti | 10 ++++
.../betree_back_stateful/BetreeMain.Types.fst | 61 +++++++++++++++++++++
.../betree_back_stateful/BetreeMain.Types.fsti | 63 ----------------------
.../BetreeMain.TypesExternal.fsti | 10 ++++
tests/fstar/hashmap_on_disk/HashmapMain.Types.fst | 24 +++++++++
tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti | 26 ---------
.../hashmap_on_disk/HashmapMain.TypesExternal.fsti | 10 ++++
tests/fstar/misc/External.Types.fst | 8 +++
tests/fstar/misc/External.Types.fsti | 14 -----
tests/fstar/misc/External.TypesExternal.fsti | 14 +++++
12 files changed, 198 insertions(+), 166 deletions(-)
create mode 100644 tests/fstar/betree/BetreeMain.Types.fst
delete mode 100644 tests/fstar/betree/BetreeMain.Types.fsti
create mode 100644 tests/fstar/betree/BetreeMain.TypesExternal.fsti
create mode 100644 tests/fstar/betree_back_stateful/BetreeMain.Types.fst
delete mode 100644 tests/fstar/betree_back_stateful/BetreeMain.Types.fsti
create mode 100644 tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti
create mode 100644 tests/fstar/hashmap_on_disk/HashmapMain.Types.fst
delete mode 100644 tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti
create mode 100644 tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti
create mode 100644 tests/fstar/misc/External.Types.fst
delete mode 100644 tests/fstar/misc/External.Types.fsti
create mode 100644 tests/fstar/misc/External.TypesExternal.fsti
(limited to 'tests/fstar')
diff --git a/tests/fstar/betree/BetreeMain.Types.fst b/tests/fstar/betree/BetreeMain.Types.fst
new file mode 100644
index 00000000..b87219b2
--- /dev/null
+++ b/tests/fstar/betree/BetreeMain.Types.fst
@@ -0,0 +1,61 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: type definitions *)
+module BetreeMain.Types
+open Primitives
+include BetreeMain.TypesExternal
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [betree_main::betree::List]
+ Source: 'src/betree.rs', lines 17:0-17:23 *)
+type betree_List_t (t : Type0) =
+| Betree_List_Cons : t -> betree_List_t t -> betree_List_t t
+| Betree_List_Nil : betree_List_t t
+
+(** [betree_main::betree::UpsertFunState]
+ Source: 'src/betree.rs', lines 63:0-63:23 *)
+type betree_UpsertFunState_t =
+| Betree_UpsertFunState_Add : u64 -> betree_UpsertFunState_t
+| Betree_UpsertFunState_Sub : u64 -> betree_UpsertFunState_t
+
+(** [betree_main::betree::Message]
+ Source: 'src/betree.rs', lines 69:0-69:23 *)
+type betree_Message_t =
+| Betree_Message_Insert : u64 -> betree_Message_t
+| Betree_Message_Delete : betree_Message_t
+| Betree_Message_Upsert : betree_UpsertFunState_t -> betree_Message_t
+
+(** [betree_main::betree::Leaf]
+ Source: 'src/betree.rs', lines 167:0-167:11 *)
+type betree_Leaf_t = { id : u64; size : u64; }
+
+(** [betree_main::betree::Internal]
+ Source: 'src/betree.rs', lines 156:0-156:15 *)
+type betree_Internal_t =
+{
+ id : u64; pivot : u64; left : betree_Node_t; right : betree_Node_t;
+}
+
+(** [betree_main::betree::Node]
+ Source: 'src/betree.rs', lines 179:0-179:9 *)
+and betree_Node_t =
+| Betree_Node_Internal : betree_Internal_t -> betree_Node_t
+| Betree_Node_Leaf : betree_Leaf_t -> betree_Node_t
+
+(** [betree_main::betree::Params]
+ Source: 'src/betree.rs', lines 187:0-187:13 *)
+type betree_Params_t = { min_flush_size : u64; split_size : u64; }
+
+(** [betree_main::betree::NodeIdCounter]
+ Source: 'src/betree.rs', lines 201:0-201:20 *)
+type betree_NodeIdCounter_t = { next_node_id : u64; }
+
+(** [betree_main::betree::BeTree]
+ Source: 'src/betree.rs', lines 218:0-218:17 *)
+type betree_BeTree_t =
+{
+ params : betree_Params_t;
+ node_id_cnt : betree_NodeIdCounter_t;
+ root : betree_Node_t;
+}
+
diff --git a/tests/fstar/betree/BetreeMain.Types.fsti b/tests/fstar/betree/BetreeMain.Types.fsti
deleted file mode 100644
index a098ec19..00000000
--- a/tests/fstar/betree/BetreeMain.Types.fsti
+++ /dev/null
@@ -1,63 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: type definitions *)
-module BetreeMain.Types
-open Primitives
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [betree_main::betree::List]
- Source: 'src/betree.rs', lines 17:0-17:23 *)
-type betree_List_t (t : Type0) =
-| Betree_List_Cons : t -> betree_List_t t -> betree_List_t t
-| Betree_List_Nil : betree_List_t t
-
-(** [betree_main::betree::UpsertFunState]
- Source: 'src/betree.rs', lines 63:0-63:23 *)
-type betree_UpsertFunState_t =
-| Betree_UpsertFunState_Add : u64 -> betree_UpsertFunState_t
-| Betree_UpsertFunState_Sub : u64 -> betree_UpsertFunState_t
-
-(** [betree_main::betree::Message]
- Source: 'src/betree.rs', lines 69:0-69:23 *)
-type betree_Message_t =
-| Betree_Message_Insert : u64 -> betree_Message_t
-| Betree_Message_Delete : betree_Message_t
-| Betree_Message_Upsert : betree_UpsertFunState_t -> betree_Message_t
-
-(** [betree_main::betree::Leaf]
- Source: 'src/betree.rs', lines 167:0-167:11 *)
-type betree_Leaf_t = { id : u64; size : u64; }
-
-(** [betree_main::betree::Internal]
- Source: 'src/betree.rs', lines 156:0-156:15 *)
-type betree_Internal_t =
-{
- id : u64; pivot : u64; left : betree_Node_t; right : betree_Node_t;
-}
-
-(** [betree_main::betree::Node]
- Source: 'src/betree.rs', lines 179:0-179:9 *)
-and betree_Node_t =
-| Betree_Node_Internal : betree_Internal_t -> betree_Node_t
-| Betree_Node_Leaf : betree_Leaf_t -> betree_Node_t
-
-(** [betree_main::betree::Params]
- Source: 'src/betree.rs', lines 187:0-187:13 *)
-type betree_Params_t = { min_flush_size : u64; split_size : u64; }
-
-(** [betree_main::betree::NodeIdCounter]
- Source: 'src/betree.rs', lines 201:0-201:20 *)
-type betree_NodeIdCounter_t = { next_node_id : u64; }
-
-(** [betree_main::betree::BeTree]
- Source: 'src/betree.rs', lines 218:0-218:17 *)
-type betree_BeTree_t =
-{
- params : betree_Params_t;
- node_id_cnt : betree_NodeIdCounter_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.fst b/tests/fstar/betree_back_stateful/BetreeMain.Types.fst
new file mode 100644
index 00000000..b87219b2
--- /dev/null
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Types.fst
@@ -0,0 +1,61 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: type definitions *)
+module BetreeMain.Types
+open Primitives
+include BetreeMain.TypesExternal
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [betree_main::betree::List]
+ Source: 'src/betree.rs', lines 17:0-17:23 *)
+type betree_List_t (t : Type0) =
+| Betree_List_Cons : t -> betree_List_t t -> betree_List_t t
+| Betree_List_Nil : betree_List_t t
+
+(** [betree_main::betree::UpsertFunState]
+ Source: 'src/betree.rs', lines 63:0-63:23 *)
+type betree_UpsertFunState_t =
+| Betree_UpsertFunState_Add : u64 -> betree_UpsertFunState_t
+| Betree_UpsertFunState_Sub : u64 -> betree_UpsertFunState_t
+
+(** [betree_main::betree::Message]
+ Source: 'src/betree.rs', lines 69:0-69:23 *)
+type betree_Message_t =
+| Betree_Message_Insert : u64 -> betree_Message_t
+| Betree_Message_Delete : betree_Message_t
+| Betree_Message_Upsert : betree_UpsertFunState_t -> betree_Message_t
+
+(** [betree_main::betree::Leaf]
+ Source: 'src/betree.rs', lines 167:0-167:11 *)
+type betree_Leaf_t = { id : u64; size : u64; }
+
+(** [betree_main::betree::Internal]
+ Source: 'src/betree.rs', lines 156:0-156:15 *)
+type betree_Internal_t =
+{
+ id : u64; pivot : u64; left : betree_Node_t; right : betree_Node_t;
+}
+
+(** [betree_main::betree::Node]
+ Source: 'src/betree.rs', lines 179:0-179:9 *)
+and betree_Node_t =
+| Betree_Node_Internal : betree_Internal_t -> betree_Node_t
+| Betree_Node_Leaf : betree_Leaf_t -> betree_Node_t
+
+(** [betree_main::betree::Params]
+ Source: 'src/betree.rs', lines 187:0-187:13 *)
+type betree_Params_t = { min_flush_size : u64; split_size : u64; }
+
+(** [betree_main::betree::NodeIdCounter]
+ Source: 'src/betree.rs', lines 201:0-201:20 *)
+type betree_NodeIdCounter_t = { next_node_id : u64; }
+
+(** [betree_main::betree::BeTree]
+ Source: 'src/betree.rs', lines 218:0-218:17 *)
+type betree_BeTree_t =
+{
+ params : betree_Params_t;
+ node_id_cnt : betree_NodeIdCounter_t;
+ root : betree_Node_t;
+}
+
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti b/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti
deleted file mode 100644
index a098ec19..00000000
--- a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti
+++ /dev/null
@@ -1,63 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_main]: type definitions *)
-module BetreeMain.Types
-open Primitives
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [betree_main::betree::List]
- Source: 'src/betree.rs', lines 17:0-17:23 *)
-type betree_List_t (t : Type0) =
-| Betree_List_Cons : t -> betree_List_t t -> betree_List_t t
-| Betree_List_Nil : betree_List_t t
-
-(** [betree_main::betree::UpsertFunState]
- Source: 'src/betree.rs', lines 63:0-63:23 *)
-type betree_UpsertFunState_t =
-| Betree_UpsertFunState_Add : u64 -> betree_UpsertFunState_t
-| Betree_UpsertFunState_Sub : u64 -> betree_UpsertFunState_t
-
-(** [betree_main::betree::Message]
- Source: 'src/betree.rs', lines 69:0-69:23 *)
-type betree_Message_t =
-| Betree_Message_Insert : u64 -> betree_Message_t
-| Betree_Message_Delete : betree_Message_t
-| Betree_Message_Upsert : betree_UpsertFunState_t -> betree_Message_t
-
-(** [betree_main::betree::Leaf]
- Source: 'src/betree.rs', lines 167:0-167:11 *)
-type betree_Leaf_t = { id : u64; size : u64; }
-
-(** [betree_main::betree::Internal]
- Source: 'src/betree.rs', lines 156:0-156:15 *)
-type betree_Internal_t =
-{
- id : u64; pivot : u64; left : betree_Node_t; right : betree_Node_t;
-}
-
-(** [betree_main::betree::Node]
- Source: 'src/betree.rs', lines 179:0-179:9 *)
-and betree_Node_t =
-| Betree_Node_Internal : betree_Internal_t -> betree_Node_t
-| Betree_Node_Leaf : betree_Leaf_t -> betree_Node_t
-
-(** [betree_main::betree::Params]
- Source: 'src/betree.rs', lines 187:0-187:13 *)
-type betree_Params_t = { min_flush_size : u64; split_size : u64; }
-
-(** [betree_main::betree::NodeIdCounter]
- Source: 'src/betree.rs', lines 201:0-201:20 *)
-type betree_NodeIdCounter_t = { next_node_id : u64; }
-
-(** [betree_main::betree::BeTree]
- Source: 'src/betree.rs', lines 218:0-218:17 *)
-type betree_BeTree_t =
-{
- params : betree_Params_t;
- node_id_cnt : betree_NodeIdCounter_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.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Types.fst
new file mode 100644
index 00000000..afebcde3
--- /dev/null
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Types.fst
@@ -0,0 +1,24 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap_main]: type definitions *)
+module HashmapMain.Types
+open Primitives
+include HashmapMain.TypesExternal
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [hashmap_main::hashmap::List]
+ Source: 'src/hashmap.rs', lines 19:0-19:16 *)
+type hashmap_List_t (t : Type0) =
+| Hashmap_List_Cons : usize -> t -> hashmap_List_t t -> hashmap_List_t t
+| Hashmap_List_Nil : hashmap_List_t t
+
+(** [hashmap_main::hashmap::HashMap]
+ Source: 'src/hashmap.rs', lines 35:0-35:21 *)
+type hashmap_HashMap_t (t : Type0) =
+{
+ num_entries : usize;
+ max_load_factor : (usize & usize);
+ max_load : usize;
+ slots : alloc_vec_Vec (hashmap_List_t t);
+}
+
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti
deleted file mode 100644
index e77954ad..00000000
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti
+++ /dev/null
@@ -1,26 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [hashmap_main]: type definitions *)
-module HashmapMain.Types
-open Primitives
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [hashmap_main::hashmap::List]
- Source: 'src/hashmap.rs', lines 19:0-19:16 *)
-type hashmap_List_t (t : Type0) =
-| Hashmap_List_Cons : usize -> t -> hashmap_List_t t -> hashmap_List_t t
-| Hashmap_List_Nil : hashmap_List_t t
-
-(** [hashmap_main::hashmap::HashMap]
- Source: 'src/hashmap.rs', lines 35:0-35:21 *)
-type hashmap_HashMap_t (t : Type0) =
-{
- num_entries : usize;
- max_load_factor : (usize & usize);
- max_load : usize;
- 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.Types.fsti
deleted file mode 100644
index 0cb9fd0e..00000000
--- a/tests/fstar/misc/External.Types.fsti
+++ /dev/null
@@ -1,14 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [external]: type definitions *)
-module External.Types
-open Primitives
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [core::num::nonzero::NonZeroU32]
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
-val core_num_nonzero_NonZeroU32_t : Type0
-
-(** The state type used in the state-error monad *)
-val state : Type0
-
diff --git a/tests/fstar/misc/External.TypesExternal.fsti b/tests/fstar/misc/External.TypesExternal.fsti
new file mode 100644
index 00000000..4bfbe0c5
--- /dev/null
+++ b/tests/fstar/misc/External.TypesExternal.fsti
@@ -0,0 +1,14 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: external type declarations *)
+module External.TypesExternal
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [core::num::nonzero::NonZeroU32]
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
+val core_num_nonzero_NonZeroU32_t : Type0
+
+(** The state type used in the state-error monad *)
+val state : Type0
+
--
cgit v1.2.3