From 0a0445c72e005c328b4764f5fb0f8f38e7a55d60 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jul 2023 14:52:23 +0200
Subject: Start using namespaces in the Lean backend

---
 tests/lean/BetreeMain/FunsExternal.lean | 35 +++++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)
 create mode 100644 tests/lean/BetreeMain/FunsExternal.lean

(limited to 'tests/lean/BetreeMain/FunsExternal.lean')

diff --git a/tests/lean/BetreeMain/FunsExternal.lean b/tests/lean/BetreeMain/FunsExternal.lean
new file mode 100644
index 00000000..0c715ef9
--- /dev/null
+++ b/tests/lean/BetreeMain/FunsExternal.lean
@@ -0,0 +1,35 @@
+-- [betree_main]: external functions.
+import Base
+import BetreeMain.Types
+open Primitives
+open betree_main
+
+-- TODO: fill those bodies
+
+/- [betree_main::betree_utils::load_internal_node] -/
+def betree_utils.load_internal_node_fwd
+  :
+  U64 → State → Result (State × (betree_list_t (U64 × betree_message_t))) :=
+  fun _ _ => .fail .panic
+
+/- [betree_main::betree_utils::store_internal_node] -/
+def betree_utils.store_internal_node_fwd
+  :
+  U64 → betree_list_t (U64 × betree_message_t) → State → Result (State
+    × Unit) :=
+  fun _ _ _ => .fail .panic
+
+/- [betree_main::betree_utils::load_leaf_node] -/
+def betree_utils.load_leaf_node_fwd
+  : U64 → State → Result (State × (betree_list_t (U64 × U64))) :=
+  fun _ _ => .fail .panic
+
+/- [betree_main::betree_utils::store_leaf_node] -/
+def betree_utils.store_leaf_node_fwd
+  : U64 → betree_list_t (U64 × U64) → State → Result (State × Unit) :=
+  fun _ _ _ => .fail .panic
+
+/- [core::option::Option::{0}::unwrap] -/
+def core.option.Option.unwrap_fwd
+  (T : Type) : Option T → State → Result (State × T) :=
+  fun _ _ => .fail .panic
-- 
cgit v1.2.3


From c07721dedb2cfe4c726c42606e623395cdfe5b80 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jul 2023 15:09:07 +0200
Subject: Simplify the generated names for the types in Lean

---
 tests/lean/BetreeMain/FunsExternal.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'tests/lean/BetreeMain/FunsExternal.lean')

diff --git a/tests/lean/BetreeMain/FunsExternal.lean b/tests/lean/BetreeMain/FunsExternal.lean
index 0c715ef9..7bcba380 100644
--- a/tests/lean/BetreeMain/FunsExternal.lean
+++ b/tests/lean/BetreeMain/FunsExternal.lean
@@ -9,24 +9,24 @@ open betree_main
 /- [betree_main::betree_utils::load_internal_node] -/
 def betree_utils.load_internal_node_fwd
   :
-  U64 → State → Result (State × (betree_list_t (U64 × betree_message_t))) :=
+  U64 → State → Result (State × (betree.List (U64 × betree.Message))) :=
   fun _ _ => .fail .panic
 
 /- [betree_main::betree_utils::store_internal_node] -/
 def betree_utils.store_internal_node_fwd
   :
-  U64 → betree_list_t (U64 × betree_message_t) → State → Result (State
+  U64 → betree.List (U64 × betree.Message) → State → Result (State
     × Unit) :=
   fun _ _ _ => .fail .panic
 
 /- [betree_main::betree_utils::load_leaf_node] -/
 def betree_utils.load_leaf_node_fwd
-  : U64 → State → Result (State × (betree_list_t (U64 × U64))) :=
+  : U64 → State → Result (State × (betree.List (U64 × U64))) :=
   fun _ _ => .fail .panic
 
 /- [betree_main::betree_utils::store_leaf_node] -/
 def betree_utils.store_leaf_node_fwd
-  : U64 → betree_list_t (U64 × U64) → State → Result (State × Unit) :=
+  : U64 → betree.List (U64 × U64) → State → Result (State × Unit) :=
   fun _ _ _ => .fail .panic
 
 /- [core::option::Option::{0}::unwrap] -/
-- 
cgit v1.2.3


From 7c95800cefc87fad894f8bf855cfc047e713b3a7 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jul 2023 12:20:28 +0200
Subject: Improve the generated comments

---
 tests/lean/BetreeMain/FunsExternal.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'tests/lean/BetreeMain/FunsExternal.lean')

diff --git a/tests/lean/BetreeMain/FunsExternal.lean b/tests/lean/BetreeMain/FunsExternal.lean
index 7bcba380..71d26da4 100644
--- a/tests/lean/BetreeMain/FunsExternal.lean
+++ b/tests/lean/BetreeMain/FunsExternal.lean
@@ -7,29 +7,29 @@ open betree_main
 -- TODO: fill those bodies
 
 /- [betree_main::betree_utils::load_internal_node] -/
-def betree_utils.load_internal_node_fwd
+def betree_utils.load_internal_node
   :
   U64 → State → Result (State × (betree.List (U64 × betree.Message))) :=
   fun _ _ => .fail .panic
 
 /- [betree_main::betree_utils::store_internal_node] -/
-def betree_utils.store_internal_node_fwd
+def betree_utils.store_internal_node
   :
   U64 → betree.List (U64 × betree.Message) → State → Result (State
     × Unit) :=
   fun _ _ _ => .fail .panic
 
 /- [betree_main::betree_utils::load_leaf_node] -/
-def betree_utils.load_leaf_node_fwd
+def betree_utils.load_leaf_node
   : U64 → State → Result (State × (betree.List (U64 × U64))) :=
   fun _ _ => .fail .panic
 
 /- [betree_main::betree_utils::store_leaf_node] -/
-def betree_utils.store_leaf_node_fwd
+def betree_utils.store_leaf_node
   : U64 → betree.List (U64 × U64) → State → Result (State × Unit) :=
   fun _ _ _ => .fail .panic
 
 /- [core::option::Option::{0}::unwrap] -/
-def core.option.Option.unwrap_fwd
+def core.option.Option.unwrap
   (T : Type) : Option T → State → Result (State × T) :=
   fun _ _ => .fail .panic
-- 
cgit v1.2.3