summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/lean/BetreeMain/ExternalFuns.lean9
-rw-r--r--tests/lean/BetreeMain/Funs.lean147
-rw-r--r--tests/lean/BetreeMain/Opaque.lean16
-rw-r--r--tests/lean/BetreeMain/Types.lean24
-rw-r--r--tests/lean/Constants.lean3
-rw-r--r--tests/lean/External/ExternalFuns.lean9
-rw-r--r--tests/lean/External/Funs.lean3
-rw-r--r--tests/lean/External/Opaque.lean14
-rw-r--r--tests/lean/External/Types.lean3
-rw-r--r--tests/lean/Hashmap/Funs.lean31
-rw-r--r--tests/lean/Hashmap/Types.lean5
-rw-r--r--tests/lean/HashmapMain/ExternalFuns.lean9
-rw-r--r--tests/lean/HashmapMain/Funs.lean31
-rw-r--r--tests/lean/HashmapMain/Opaque.lean7
-rw-r--r--tests/lean/HashmapMain/Types.lean5
-rw-r--r--tests/lean/Loops/Funs.lean83
-rw-r--r--tests/lean/Loops/Types.lean5
-rw-r--r--tests/lean/NoNestedBorrows.lean33
-rw-r--r--tests/lean/Paper.lean11
-rw-r--r--tests/lean/PoloniusList.lean9
-rw-r--r--tests/lean/lake-manifest.json2
-rw-r--r--tests/lean/lakefile.lean8
22 files changed, 275 insertions, 192 deletions
diff --git a/tests/lean/BetreeMain/ExternalFuns.lean b/tests/lean/BetreeMain/ExternalFuns.lean
new file mode 100644
index 00000000..59beb514
--- /dev/null
+++ b/tests/lean/BetreeMain/ExternalFuns.lean
@@ -0,0 +1,9 @@
+import Base
+import BetreeMain.Types
+import BetreeMain.Opaque
+
+namespace BetreeMain
+
+def opaque_defs : OpaqueDefs := by sorry
+
+end BetreeMain
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index fb48b3a6..2eb7fa1f 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -5,6 +5,8 @@ import BetreeMain.Types
import BetreeMain.ExternalFuns
open Primitives
+namespace BetreeMain
+
/- [betree_main::betree::load_internal_node] -/
def betree_load_internal_node_fwd
(id : U64) (st : State) :
@@ -75,13 +77,13 @@ def core_num_u64_max_c : U64 := eval_global core_num_u64_max_body (by simp)
/- [betree_main::betree::upsert_update] -/
def betree_upsert_update_fwd
(prev : Option U64) (st : betree_upsert_fun_state_t) : Result U64 :=
- match h: prev with
+ match prev with
| Option.none =>
- match h: st with
+ match st with
| betree_upsert_fun_state_t.Add v => Result.ret v
| betree_upsert_fun_state_t.Sub i => Result.ret (U64.ofInt 0 (by intlit))
| Option.some prev0 =>
- match h: st with
+ match st with
| betree_upsert_fun_state_t.Add v =>
do
let margin ← core_num_u64_max_c - prev0
@@ -96,7 +98,7 @@ def betree_upsert_update_fwd
/- [betree_main::betree::List::{1}::len] -/
divergent def betree_list_len_fwd
(T : Type) (self : betree_list_t T) : Result U64 :=
- match h: self with
+ match self with
| betree_list_t.Cons t tl =>
do
let i ← betree_list_len_fwd T tl
@@ -111,7 +113,7 @@ divergent def betree_list_split_at_fwd
if n = (U64.ofInt 0 (by intlit))
then Result.ret (betree_list_t.Nil, self)
else
- match h: self with
+ match self with
| betree_list_t.Cons hd tl =>
do
let i ← n - (U64.ofInt 1 (by intlit))
@@ -131,7 +133,7 @@ def betree_list_push_front_fwd_back
/- [betree_main::betree::List::{1}::pop_front] -/
def betree_list_pop_front_fwd (T : Type) (self : betree_list_t T) : Result T :=
let ls := mem_replace_fwd (betree_list_t T) self betree_list_t.Nil
- match h: ls with
+ match ls with
| betree_list_t.Cons x tl => Result.ret x
| betree_list_t.Nil => Result.fail Error.panic
@@ -139,20 +141,20 @@ def betree_list_pop_front_fwd (T : Type) (self : betree_list_t T) : Result T :=
def betree_list_pop_front_back
(T : Type) (self : betree_list_t T) : Result (betree_list_t T) :=
let ls := mem_replace_fwd (betree_list_t T) self betree_list_t.Nil
- match h: ls with
+ match ls with
| betree_list_t.Cons x tl => Result.ret tl
| betree_list_t.Nil => Result.fail Error.panic
/- [betree_main::betree::List::{1}::hd] -/
def betree_list_hd_fwd (T : Type) (self : betree_list_t T) : Result T :=
- match h: self with
+ match self with
| betree_list_t.Cons hd l => Result.ret hd
| betree_list_t.Nil => Result.fail Error.panic
/- [betree_main::betree::List::{2}::head_has_key] -/
def betree_list_head_has_key_fwd
(T : Type) (self : betree_list_t (U64 × T)) (key : U64) : Result Bool :=
- match h: self with
+ match self with
| betree_list_t.Cons hd l => let (i, _) := hd
Result.ret (i = key)
| betree_list_t.Nil => Result.ret false
@@ -162,7 +164,7 @@ divergent def betree_list_partition_at_pivot_fwd
(T : Type) (self : betree_list_t (U64 × T)) (pivot : U64) :
Result ((betree_list_t (U64 × T)) × (betree_list_t (U64 × T)))
:=
- match h: self with
+ match self with
| betree_list_t.Cons hd tl =>
let (i, t) := hd
if i >= pivot
@@ -204,7 +206,7 @@ def betree_leaf_split_fwd
betree_leaf_id := id1,
betree_leaf_size := params.betree_params_split_size
}
- Result.ret (st1, mkbetree_internal_t self.betree_leaf_id pivot n n0)
+ Result.ret (st1, betree_internal_t.mk self.betree_leaf_id pivot n n0)
/- [betree_main::betree::Leaf::{3}::split] -/
def betree_leaf_split_back
@@ -229,7 +231,7 @@ def betree_leaf_split_back
/- [betree_main::betree::Node::{5}::lookup_in_bindings] -/
divergent def betree_node_lookup_in_bindings_fwd
(key : U64) (bindings : betree_list_t (U64 × U64)) : Result (Option U64) :=
- match h: bindings with
+ match bindings with
| betree_list_t.Cons hd tl =>
let (i, i0) := hd
if i = key
@@ -245,7 +247,7 @@ divergent def betree_node_lookup_first_message_for_key_fwd
(key : U64) (msgs : betree_list_t (U64 × betree_message_t)) :
Result (betree_list_t (U64 × betree_message_t))
:=
- match h: msgs with
+ match msgs with
| betree_list_t.Cons x next_msgs =>
let (i, m) := x
if i >= key
@@ -259,7 +261,7 @@ divergent def betree_node_lookup_first_message_for_key_back
(ret0 : betree_list_t (U64 × betree_message_t)) :
Result (betree_list_t (U64 × betree_message_t))
:=
- match h: msgs with
+ match msgs with
| betree_list_t.Cons x next_msgs =>
let (i, m) := x
if i >= key
@@ -284,7 +286,7 @@ divergent def betree_node_apply_upserts_fwd
do
let msg ← betree_list_pop_front_fwd (U64 × betree_message_t) msgs
let (_, m) := msg
- match h: m with
+ match m with
| betree_message_t.Insert i => Result.fail Error.panic
| betree_message_t.Delete => Result.fail Error.panic
| betree_message_t.Upsert s =>
@@ -314,7 +316,7 @@ divergent def betree_node_apply_upserts_back
do
let msg ← betree_list_pop_front_fwd (U64 × betree_message_t) msgs
let (_, m) := msg
- match h: m with
+ match m with
| betree_message_t.Insert i => Result.fail Error.panic
| betree_message_t.Delete => Result.fail Error.panic
| betree_message_t.Upsert s =>
@@ -334,27 +336,27 @@ mutual divergent def betree_node_lookup_fwd
(self : betree_node_t) (key : U64) (st : State) :
Result (State × (Option U64))
:=
- match h: self with
+ match self with
| betree_node_t.Internal node =>
do
- let (mkbetree_internal_t i i0 n n0) := node
+ let ⟨ i, i0, n, n0 ⟩ := node
let (st0, msgs) ← betree_load_internal_node_fwd i st
let pending ← betree_node_lookup_first_message_for_key_fwd key msgs
- match h: pending with
+ match pending with
| betree_list_t.Cons p l =>
let (k, msg) := p
if k != key
then
do
let (st1, opt) ←
- betree_internal_lookup_in_children_fwd (mkbetree_internal_t i i0
+ betree_internal_lookup_in_children_fwd (betree_internal_t.mk i i0
n n0) key st0
let _ ←
betree_node_lookup_first_message_for_key_back key msgs
(betree_list_t.Cons (k, msg) l)
Result.ret (st1, opt)
else
- match h: msg with
+ match msg with
| betree_message_t.Insert v =>
do
let _ ←
@@ -370,15 +372,15 @@ mutual divergent def betree_node_lookup_fwd
| betree_message_t.Upsert ufs =>
do
let (st1, v) ←
- betree_internal_lookup_in_children_fwd (mkbetree_internal_t i
+ betree_internal_lookup_in_children_fwd (betree_internal_t.mk i
i0 n n0) key st0
let (st2, v0) ←
betree_node_apply_upserts_fwd (betree_list_t.Cons (k,
betree_message_t.Upsert ufs) l) v key st1
let node0 ←
- betree_internal_lookup_in_children_back (mkbetree_internal_t i
+ betree_internal_lookup_in_children_back (betree_internal_t.mk i
i0 n n0) key st0
- let (mkbetree_internal_t i1 _ _ _) := node0
+ let ⟨ i1, _, _, _ ⟩ := node0
let pending0 ←
betree_node_apply_upserts_back (betree_list_t.Cons (k,
betree_message_t.Upsert ufs) l) v key st1
@@ -389,7 +391,7 @@ mutual divergent def betree_node_lookup_fwd
| betree_list_t.Nil =>
do
let (st1, opt) ←
- betree_internal_lookup_in_children_fwd (mkbetree_internal_t i i0 n
+ betree_internal_lookup_in_children_fwd (betree_internal_t.mk i i0 n
n0) key st0
let _ ←
betree_node_lookup_first_message_for_key_back key msgs
@@ -404,13 +406,13 @@ mutual divergent def betree_node_lookup_fwd
/- [betree_main::betree::Node::{5}::lookup] -/
divergent def betree_node_lookup_back
(self : betree_node_t) (key : U64) (st : State) : Result betree_node_t :=
- match h: self with
+ match self with
| betree_node_t.Internal node =>
do
- let (mkbetree_internal_t i i0 n n0) := node
+ let ⟨ i, i0, n, n0 ⟩ := node
let (st0, msgs) ← betree_load_internal_node_fwd i st
let pending ← betree_node_lookup_first_message_for_key_fwd key msgs
- match h: pending with
+ match pending with
| betree_list_t.Cons p l =>
let (k, msg) := p
if k != key
@@ -420,44 +422,44 @@ divergent def betree_node_lookup_back
betree_node_lookup_first_message_for_key_back key msgs
(betree_list_t.Cons (k, msg) l)
let node0 ←
- betree_internal_lookup_in_children_back (mkbetree_internal_t i i0
- n n0) key st0
+ betree_internal_lookup_in_children_back (betree_internal_t.mk i
+ i0 n n0) key st0
Result.ret (betree_node_t.Internal node0)
else
- match h: msg with
+ match msg with
| betree_message_t.Insert v =>
do
let _ ←
betree_node_lookup_first_message_for_key_back key msgs
(betree_list_t.Cons (k, betree_message_t.Insert v) l)
- Result.ret (betree_node_t.Internal (mkbetree_internal_t i i0 n
+ Result.ret (betree_node_t.Internal (betree_internal_t.mk i i0 n
n0))
| betree_message_t.Delete =>
do
let _ ←
betree_node_lookup_first_message_for_key_back key msgs
(betree_list_t.Cons (k, betree_message_t.Delete) l)
- Result.ret (betree_node_t.Internal (mkbetree_internal_t i i0 n
+ Result.ret (betree_node_t.Internal (betree_internal_t.mk i i0 n
n0))
| betree_message_t.Upsert ufs =>
do
let (st1, v) ←
- betree_internal_lookup_in_children_fwd (mkbetree_internal_t i
+ betree_internal_lookup_in_children_fwd (betree_internal_t.mk i
i0 n n0) key st0
let (st2, _) ←
betree_node_apply_upserts_fwd (betree_list_t.Cons (k,
betree_message_t.Upsert ufs) l) v key st1
let node0 ←
- betree_internal_lookup_in_children_back (mkbetree_internal_t i
+ betree_internal_lookup_in_children_back (betree_internal_t.mk i
i0 n n0) key st0
- let (mkbetree_internal_t i1 i2 n1 n2) := node0
+ let ⟨ i1, i2, n1, n2 ⟩ := node0
let pending0 ←
betree_node_apply_upserts_back (betree_list_t.Cons (k,
betree_message_t.Upsert ufs) l) v key st1
let msgs0 ←
betree_node_lookup_first_message_for_key_back key msgs pending0
let _ ← betree_store_internal_node_fwd i1 msgs0 st2
- Result.ret (betree_node_t.Internal (mkbetree_internal_t i1 i2 n1
+ Result.ret (betree_node_t.Internal (betree_internal_t.mk i1 i2 n1
n2))
| betree_list_t.Nil =>
do
@@ -465,8 +467,8 @@ divergent def betree_node_lookup_back
betree_node_lookup_first_message_for_key_back key msgs
betree_list_t.Nil
let node0 ←
- betree_internal_lookup_in_children_back (mkbetree_internal_t i i0 n
- n0) key st0
+ betree_internal_lookup_in_children_back (betree_internal_t.mk i i0
+ n n0) key st0
Result.ret (betree_node_t.Internal node0)
| betree_node_t.Leaf node =>
do
@@ -479,7 +481,7 @@ divergent def betree_internal_lookup_in_children_fwd
(self : betree_internal_t) (key : U64) (st : State) :
Result (State × (Option U64))
:=
- let (mkbetree_internal_t _ i n n0) := self
+ let ⟨ _, i, n, n0 ⟩ := self
if key < i
then betree_node_lookup_fwd n key st
else betree_node_lookup_fwd n0 key st
@@ -489,16 +491,16 @@ divergent def betree_internal_lookup_in_children_back
(self : betree_internal_t) (key : U64) (st : State) :
Result betree_internal_t
:=
- let (mkbetree_internal_t i i0 n n0) := self
+ let ⟨ i, i0, n, n0 ⟩ := self
if key < i0
then
do
let n1 ← betree_node_lookup_back n key st
- Result.ret (mkbetree_internal_t i i0 n1 n0)
+ Result.ret (betree_internal_t.mk i i0 n1 n0)
else
do
let n1 ← betree_node_lookup_back n0 key st
- Result.ret (mkbetree_internal_t i i0 n n1)
+ Result.ret (betree_internal_t.mk i i0 n n1)
end
@@ -507,7 +509,7 @@ divergent def betree_node_lookup_mut_in_bindings_fwd
(key : U64) (bindings : betree_list_t (U64 × U64)) :
Result (betree_list_t (U64 × U64))
:=
- match h: bindings with
+ match bindings with
| betree_list_t.Cons hd tl =>
let (i, i0) := hd
if i >= key
@@ -521,7 +523,7 @@ divergent def betree_node_lookup_mut_in_bindings_back
(ret0 : betree_list_t (U64 × U64)) :
Result (betree_list_t (U64 × U64))
:=
- match h: bindings with
+ match bindings with
| betree_list_t.Cons hd tl =>
let (i, i0) := hd
if i >= key
@@ -545,7 +547,7 @@ def betree_node_apply_to_leaf_fwd_back
then
do
let hd ← betree_list_pop_front_fwd (U64 × U64) bindings0
- match h: new_msg with
+ match new_msg with
| betree_message_t.Insert v =>
do
let bindings1 ← betree_list_pop_front_back (U64 × U64) bindings0
@@ -565,7 +567,7 @@ def betree_node_apply_to_leaf_fwd_back
betree_list_push_front_fwd_back (U64 × U64) bindings1 (key, v)
betree_node_lookup_mut_in_bindings_back key bindings bindings2
else
- match h: new_msg with
+ match new_msg with
| betree_message_t.Insert v =>
do
let bindings1 ←
@@ -586,7 +588,7 @@ divergent def betree_node_apply_messages_to_leaf_fwd_back
(new_msgs : betree_list_t (U64 × betree_message_t)) :
Result (betree_list_t (U64 × U64))
:=
- match h: new_msgs with
+ match new_msgs with
| betree_list_t.Cons new_msg new_msgs_tl =>
do
let (i, m) := new_msg
@@ -599,7 +601,7 @@ divergent def betree_node_filter_messages_for_key_fwd_back
(key : U64) (msgs : betree_list_t (U64 × betree_message_t)) :
Result (betree_list_t (U64 × betree_message_t))
:=
- match h: msgs with
+ match msgs with
| betree_list_t.Cons p l =>
let (k, m) := p
if k = key
@@ -617,7 +619,7 @@ divergent def betree_node_lookup_first_message_after_key_fwd
(key : U64) (msgs : betree_list_t (U64 × betree_message_t)) :
Result (betree_list_t (U64 × betree_message_t))
:=
- match h: msgs with
+ match msgs with
| betree_list_t.Cons p next_msgs =>
let (k, m) := p
if k = key
@@ -631,7 +633,7 @@ divergent def betree_node_lookup_first_message_after_key_back
(ret0 : betree_list_t (U64 × betree_message_t)) :
Result (betree_list_t (U64 × betree_message_t))
:=
- match h: msgs with
+ match msgs with
| betree_list_t.Cons p next_msgs =>
let (k, m) := p
if k = key
@@ -654,7 +656,7 @@ def betree_node_apply_to_internal_fwd_back
let b ← betree_list_head_has_key_fwd betree_message_t msgs0 key
if b
then
- match h: new_msg with
+ match new_msg with
| betree_message_t.Insert i =>
do
let msgs1 ← betree_node_filter_messages_for_key_fwd_back key msgs0
@@ -673,7 +675,7 @@ def betree_node_apply_to_internal_fwd_back
do
let p ← betree_list_hd_fwd (U64 × betree_message_t) msgs0
let (_, m) := p
- match h: m with
+ match m with
| betree_message_t.Insert prev =>
do
let v ← betree_upsert_update_fwd (Option.some prev) s
@@ -715,7 +717,7 @@ divergent def betree_node_apply_messages_to_internal_fwd_back
(new_msgs : betree_list_t (U64 × betree_message_t)) :
Result (betree_list_t (U64 × betree_message_t))
:=
- match h: new_msgs with
+ match new_msgs with
| betree_list_t.Cons new_msg new_msgs_tl =>
do
let (i, m) := new_msg
@@ -730,10 +732,10 @@ mutual divergent def betree_node_apply_messages_fwd
(msgs : betree_list_t (U64 × betree_message_t)) (st : State) :
Result (State × Unit)
:=
- match h: self with
+ match self with
| betree_node_t.Internal node =>
do
- let (mkbetree_internal_t i i0 n n0) := node
+ let ⟨ i, i0, n, n0 ⟩ := node
let (st0, content) ← betree_load_internal_node_fwd i st
let content0 ←
betree_node_apply_messages_to_internal_fwd_back content msgs
@@ -742,12 +744,12 @@ mutual divergent def betree_node_apply_messages_fwd
then
do
let (st1, content1) ←
- betree_internal_flush_fwd (mkbetree_internal_t i i0 n n0) params
+ betree_internal_flush_fwd (betree_internal_t.mk i i0 n n0) params
node_id_cnt content0 st0
let (node0, _) ←
- betree_internal_flush_back (mkbetree_internal_t i i0 n n0) params
+ betree_internal_flush_back (betree_internal_t.mk i i0 n n0) params
node_id_cnt content0 st0
- let (mkbetree_internal_t i1 _ _ _) := node0
+ let ⟨ i1, _, _, _ ⟩ := node0
let (st2, _) ← betree_store_internal_node_fwd i1 content1 st1
Result.ret (st2, ())
else
@@ -782,10 +784,10 @@ divergent def betree_node_apply_messages_back
(msgs : betree_list_t (U64 × betree_message_t)) (st : State) :
Result (betree_node_t × betree_node_id_counter_t)
:=
- match h: self with
+ match self with
| betree_node_t.Internal node =>
do
- let (mkbetree_internal_t i i0 n n0) := node
+ let ⟨ i, i0, n, n0 ⟩ := node
let (st0, content) ← betree_load_internal_node_fwd i st
let content0 ←
betree_node_apply_messages_to_internal_fwd_back content msgs
@@ -794,19 +796,19 @@ divergent def betree_node_apply_messages_back
then
do
let (st1, content1) ←
- betree_internal_flush_fwd (mkbetree_internal_t i i0 n n0) params
+ betree_internal_flush_fwd (betree_internal_t.mk i i0 n n0) params
node_id_cnt content0 st0
let (node0, node_id_cnt0) ←
- betree_internal_flush_back (mkbetree_internal_t i i0 n n0) params
+ betree_internal_flush_back (betree_internal_t.mk i i0 n n0) params
node_id_cnt content0 st0
- let (mkbetree_internal_t i1 i2 n1 n2) := node0
+ let ⟨ i1, i2, n1, n2 ⟩ := node0
let _ ← betree_store_internal_node_fwd i1 content1 st1
- Result.ret (betree_node_t.Internal (mkbetree_internal_t i1 i2 n1 n2),
- node_id_cnt0)
+ Result.ret (betree_node_t.Internal (betree_internal_t.mk i1 i2 n1
+ n2), node_id_cnt0)
else
do
let _ ← betree_store_internal_node_fwd i content0 st0
- Result.ret (betree_node_t.Internal (mkbetree_internal_t i i0 n n0),
+ Result.ret (betree_node_t.Internal (betree_internal_t.mk i i0 n n0),
node_id_cnt)
| betree_node_t.Leaf node =>
do
@@ -839,7 +841,7 @@ divergent def betree_internal_flush_fwd
Result (State × (betree_list_t (U64 × betree_message_t)))
:=
do
- let (mkbetree_internal_t _ i n n0) := self
+ let ⟨ _, i, n, n0 ⟩ := self
let p ← betree_list_partition_at_pivot_fwd betree_message_t content i
let (msgs_left, msgs_right) := p
let len_left ← betree_list_len_fwd (U64 × betree_message_t) msgs_left
@@ -879,7 +881,7 @@ divergent def betree_internal_flush_back
Result (betree_internal_t × betree_node_id_counter_t)
:=
do
- let (mkbetree_internal_t i i0 n n0) := self
+ let ⟨ i, i0, n, n0 ⟩ := self
let p ← betree_list_partition_at_pivot_fwd betree_message_t content i0
let (msgs_left, msgs_right) := p
let len_left ← betree_list_len_fwd (U64 × betree_message_t) msgs_left
@@ -898,13 +900,13 @@ divergent def betree_internal_flush_back
let (n2, node_id_cnt1) ←
betree_node_apply_messages_back n0 params node_id_cnt0 msgs_right
st0
- Result.ret (mkbetree_internal_t i i0 n1 n2, node_id_cnt1)
- else Result.ret (mkbetree_internal_t i i0 n1 n0, node_id_cnt0)
+ Result.ret (betree_internal_t.mk i i0 n1 n2, node_id_cnt1)
+ else Result.ret (betree_internal_t.mk i i0 n1 n0, node_id_cnt0)
else
do
let (n1, node_id_cnt0) ←
betree_node_apply_messages_back n0 params node_id_cnt msgs_right st
- Result.ret (mkbetree_internal_t i i0 n n1, node_id_cnt0)
+ Result.ret (betree_internal_t.mk i i0 n n1, node_id_cnt0)
end
@@ -1069,3 +1071,4 @@ def main_fwd : Result Unit :=
/- Unit test for [betree_main::main] -/
#assert (main_fwd == .ret ())
+end BetreeMain
diff --git a/tests/lean/BetreeMain/Opaque.lean b/tests/lean/BetreeMain/Opaque.lean
index c8226d4e..d043186b 100644
--- a/tests/lean/BetreeMain/Opaque.lean
+++ b/tests/lean/BetreeMain/Opaque.lean
@@ -4,28 +4,32 @@ import Base
import BetreeMain.Types
open Primitives
+namespace BetreeMain
+
structure OpaqueDefs where
/- [betree_main::betree_utils::load_internal_node] -/
betree_utils_load_internal_node_fwd
:
- U64 -> State -> Result (State × (betree_list_t (U64 × betree_message_t)))
+ U64 → State → Result (State × (betree_list_t (U64 ×
+ betree_message_t)))
/- [betree_main::betree_utils::store_internal_node] -/
betree_utils_store_internal_node_fwd
:
- U64 -> betree_list_t (U64 × betree_message_t) -> State -> Result (State ×
- Unit)
+ U64 → betree_list_t (U64 × betree_message_t) → State → Result (State
+ × Unit)
/- [betree_main::betree_utils::load_leaf_node] -/
betree_utils_load_leaf_node_fwd
- : U64 -> State -> Result (State × (betree_list_t (U64 × U64)))
+ : U64 → State → Result (State × (betree_list_t (U64 × U64)))
/- [betree_main::betree_utils::store_leaf_node] -/
betree_utils_store_leaf_node_fwd
- : U64 -> betree_list_t (U64 × U64) -> State -> Result (State × Unit)
+ : U64 → betree_list_t (U64 × U64) → State → Result (State × Unit)
/- [core::option::Option::{0}::unwrap] -/
core_option_option_unwrap_fwd
- (T : Type) : Option T -> State -> Result (State × T)
+ (T : Type) : Option T → State → Result (State × T)
+end BetreeMain
diff --git a/tests/lean/BetreeMain/Types.lean b/tests/lean/BetreeMain/Types.lean
index 4875a8ba..cfed6a28 100644
--- a/tests/lean/BetreeMain/Types.lean
+++ b/tests/lean/BetreeMain/Types.lean
@@ -3,21 +3,23 @@
import Base
open Primitives
+namespace BetreeMain
+
/- [betree_main::betree::List] -/
inductive betree_list_t (T : Type) :=
-| Cons : T -> betree_list_t T -> betree_list_t T
+| Cons : T → betree_list_t T → betree_list_t T
| Nil : betree_list_t T
/- [betree_main::betree::UpsertFunState] -/
inductive betree_upsert_fun_state_t :=
-| Add : U64 -> betree_upsert_fun_state_t
-| Sub : U64 -> betree_upsert_fun_state_t
+| Add : U64 → betree_upsert_fun_state_t
+| Sub : U64 → betree_upsert_fun_state_t
/- [betree_main::betree::Message] -/
inductive betree_message_t :=
-| Insert : U64 -> betree_message_t
+| Insert : U64 → betree_message_t
| Delete : betree_message_t
-| Upsert : betree_upsert_fun_state_t -> betree_message_t
+| Upsert : betree_upsert_fun_state_t → betree_message_t
/- [betree_main::betree::Leaf] -/
structure betree_leaf_t where
@@ -28,17 +30,12 @@ mutual
/- [betree_main::betree::Node] -/
inductive betree_node_t :=
-| Internal : betree_internal_t -> betree_node_t
-| Leaf : betree_leaf_t -> betree_node_t
+| Internal : betree_internal_t → betree_node_t
+| Leaf : betree_leaf_t → betree_node_t
/- [betree_main::betree::Internal] -/
inductive betree_internal_t :=
-| mkbetree_internal_t :
- U64 ->
- U64 ->
- betree_node_t ->
- betree_node_t ->
- betree_internal_t
+| mk : U64 → U64 → betree_node_t → betree_node_t → betree_internal_t
end
@@ -60,3 +57,4 @@ structure betree_be_tree_t where
/- The state type used in the state-error monad -/
axiom State : Type
+end BetreeMain
diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean
index cd2f88f5..9f6a47de 100644
--- a/tests/lean/Constants.lean
+++ b/tests/lean/Constants.lean
@@ -3,6 +3,8 @@
import Base
open Primitives
+namespace Constants
+
/- [constants::X0] -/
def x0_body : Result U32 := Result.ret (U32.ofInt 0 (by intlit))
def x0_c : U32 := eval_global x0_body (by simp)
@@ -130,3 +132,4 @@ def s4_body : Result (pair_t U32 U32) :=
mk_pair1_fwd (U32.ofInt 7 (by intlit)) (U32.ofInt 8 (by intlit))
def s4_c : pair_t U32 U32 := eval_global s4_body (by simp)
+end Constants
diff --git a/tests/lean/External/ExternalFuns.lean b/tests/lean/External/ExternalFuns.lean
new file mode 100644
index 00000000..d63db2ac
--- /dev/null
+++ b/tests/lean/External/ExternalFuns.lean
@@ -0,0 +1,9 @@
+import Base
+import External.Types
+import External.Opaque
+
+namespace External
+
+def opaque_defs : OpaqueDefs := sorry
+
+end External
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index 73e45938..e36987e0 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -5,6 +5,8 @@ import External.Types
import External.ExternalFuns
open Primitives
+namespace External
+
/- [external::swap] -/
def swap_fwd
(T : Type) (x : T) (y : T) (st : State) : Result (State × Unit) :=
@@ -86,3 +88,4 @@ def test_swap_non_zero_fwd (x : U32) (st : State) : Result (State × U32) :=
then Result.fail Error.panic
else Result.ret (st1, x0)
+end External
diff --git a/tests/lean/External/Opaque.lean b/tests/lean/External/Opaque.lean
index 5483c3a9..1c0db095 100644
--- a/tests/lean/External/Opaque.lean
+++ b/tests/lean/External/Opaque.lean
@@ -4,25 +4,29 @@ import Base
import External.Types
open Primitives
+namespace External
+
structure OpaqueDefs where
/- [core::mem::swap] -/
- core_mem_swap_fwd (T : Type) : T -> T -> State -> Result (State × Unit)
+ core_mem_swap_fwd (T : Type) : T → T → State → Result (State × Unit)
/- [core::mem::swap] -/
core_mem_swap_back0
- (T : Type) : T -> T -> State -> State -> Result (State × T)
+ (T : Type) : T → T → State → State → Result (State × T)
/- [core::mem::swap] -/
core_mem_swap_back1
- (T : Type) : T -> T -> State -> State -> Result (State × T)
+ (T : Type) : T → T → State → State → Result (State × T)
/- [core::num::nonzero::NonZeroU32::{14}::new] -/
core_num_nonzero_non_zero_u32_new_fwd
:
- U32 -> State -> Result (State × (Option core_num_nonzero_non_zero_u32_t))
+ U32 → State → Result (State × (Option
+ core_num_nonzero_non_zero_u32_t))
/- [core::option::Option::{0}::unwrap] -/
core_option_option_unwrap_fwd
- (T : Type) : Option T -> State -> Result (State × T)
+ (T : Type) : Option T → State → Result (State × T)
+end External
diff --git a/tests/lean/External/Types.lean b/tests/lean/External/Types.lean
index 25907da2..fda0670e 100644
--- a/tests/lean/External/Types.lean
+++ b/tests/lean/External/Types.lean
@@ -3,9 +3,12 @@
import Base
open Primitives
+namespace External
+
/- [core::num::nonzero::NonZeroU32] -/
axiom core_num_nonzero_non_zero_u32_t : Type
/- The state type used in the state-error monad -/
axiom State : Type
+end External
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 26742d5d..b4254726 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -4,6 +4,8 @@ import Base
import Hashmap.Types
open Primitives
+namespace Hashmap
+
/- [hashmap::hash_key] -/
def hash_key_fwd (k : Usize) : Result Usize :=
Result.ret k
@@ -82,7 +84,7 @@ def hash_map_len_fwd (T : Type) (self : hash_map_t T) : Result Usize :=
/- [hashmap::HashMap::{0}::insert_in_list] -/
divergent def hash_map_insert_in_list_loop_fwd
(T : Type) (key : Usize) (value : T) (ls : list_t T) : Result Bool :=
- match h: ls with
+ match ls with
| list_t.Cons ckey cvalue tl =>
if ckey = key
then Result.ret false
@@ -97,7 +99,7 @@ def hash_map_insert_in_list_fwd
/- [hashmap::HashMap::{0}::insert_in_list] -/
divergent def hash_map_insert_in_list_loop_back
(T : Type) (key : Usize) (value : T) (ls : list_t T) : Result (list_t T) :=
- match h: ls with
+ match ls with
| list_t.Cons ckey cvalue tl =>
if ckey = key
then Result.ret (list_t.Cons ckey value tl)
@@ -146,7 +148,7 @@ def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp)
/- [hashmap::HashMap::{0}::move_elements_from_list] -/
divergent def hash_map_move_elements_from_list_loop_fwd_back
(T : Type) (ntable : hash_map_t T) (ls : list_t T) : Result (hash_map_t T) :=
- match h: ls with
+ match ls with
| list_t.Cons k v tl =>
do
let ntable0 ← hash_map_insert_no_resize_fwd_back T ntable k v
@@ -224,7 +226,7 @@ def hash_map_insert_fwd_back
/- [hashmap::HashMap::{0}::contains_key_in_list] -/
divergent def hash_map_contains_key_in_list_loop_fwd
(T : Type) (key : Usize) (ls : list_t T) : Result Bool :=
- match h: ls with
+ match ls with
| list_t.Cons ckey t tl =>
if ckey = key
then Result.ret true
@@ -249,7 +251,7 @@ def hash_map_contains_key_fwd
/- [hashmap::HashMap::{0}::get_in_list] -/
divergent def hash_map_get_in_list_loop_fwd
(T : Type) (key : Usize) (ls : list_t T) : Result T :=
- match h: ls with
+ match ls with
| list_t.Cons ckey cvalue tl =>
if ckey = key
then Result.ret cvalue
@@ -274,7 +276,7 @@ def hash_map_get_fwd
/- [hashmap::HashMap::{0}::get_mut_in_list] -/
divergent def hash_map_get_mut_in_list_loop_fwd
(T : Type) (ls : list_t T) (key : Usize) : Result T :=
- match h: ls with
+ match ls with
| list_t.Cons ckey cvalue tl =>
if ckey = key
then Result.ret cvalue
@@ -289,7 +291,7 @@ def hash_map_get_mut_in_list_fwd
/- [hashmap::HashMap::{0}::get_mut_in_list] -/
divergent def hash_map_get_mut_in_list_loop_back
(T : Type) (ls : list_t T) (key : Usize) (ret0 : T) : Result (list_t T) :=
- match h: ls with
+ match ls with
| list_t.Cons ckey cvalue tl =>
if ckey = key
then Result.ret (list_t.Cons ckey ret0 tl)
@@ -331,13 +333,13 @@ def hash_map_get_mut_back
/- [hashmap::HashMap::{0}::remove_from_list] -/
divergent def hash_map_remove_from_list_loop_fwd
(T : Type) (key : Usize) (ls : list_t T) : Result (Option T) :=
- match h: ls with
+ match ls with
| list_t.Cons ckey t tl =>
if ckey = key
then
let mv_ls :=
mem_replace_fwd (list_t T) (list_t.Cons ckey t tl) list_t.Nil
- match h: mv_ls with
+ match mv_ls with
| list_t.Cons i cvalue tl0 => Result.ret (Option.some cvalue)
| list_t.Nil => Result.fail Error.panic
else hash_map_remove_from_list_loop_fwd T key tl
@@ -351,13 +353,13 @@ def hash_map_remove_from_list_fwd
/- [hashmap::HashMap::{0}::remove_from_list] -/
divergent def hash_map_remove_from_list_loop_back
(T : Type) (key : Usize) (ls : list_t T) : Result (list_t T) :=
- match h: ls with
+ match ls with
| list_t.Cons ckey t tl =>
if ckey = key
then
let mv_ls :=
mem_replace_fwd (list_t T) (list_t.Cons ckey t tl) list_t.Nil
- match h: mv_ls with
+ match mv_ls with
| list_t.Cons i cvalue tl0 => Result.ret tl0
| list_t.Nil => Result.fail Error.panic
else
@@ -380,7 +382,7 @@ def hash_map_remove_fwd
let hash_mod ← hash % i
let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod
let x ← hash_map_remove_from_list_fwd T key l
- match h: x with
+ match x with
| Option.none => Result.ret Option.none
| Option.some x0 =>
do
@@ -396,7 +398,7 @@ def hash_map_remove_back
let hash_mod ← hash % i
let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod
let x ← hash_map_remove_from_list_fwd T key l
- match h: x with
+ match x with
| Option.none =>
do
let l0 ← hash_map_remove_from_list_back T key l
@@ -441,7 +443,7 @@ def test1_fwd : Result Unit :=
do
let x ←
hash_map_remove_fwd U64 hm4 (Usize.ofInt 1024 (by intlit))
- match h: x with
+ match x with
| Option.none => Result.fail Error.panic
| Option.some x0 =>
if not (x0 = (U64.ofInt 56 (by intlit)))
@@ -472,3 +474,4 @@ def test1_fwd : Result Unit :=
/- Unit test for [hashmap::test1] -/
#assert (test1_fwd == .ret ())
+end Hashmap
diff --git a/tests/lean/Hashmap/Types.lean b/tests/lean/Hashmap/Types.lean
index af26f363..0aec6acf 100644
--- a/tests/lean/Hashmap/Types.lean
+++ b/tests/lean/Hashmap/Types.lean
@@ -3,9 +3,11 @@
import Base
open Primitives
+namespace Hashmap
+
/- [hashmap::List] -/
inductive list_t (T : Type) :=
-| Cons : Usize -> T -> list_t T -> list_t T
+| Cons : Usize → T → list_t T → list_t T
| Nil : list_t T
/- [hashmap::HashMap] -/
@@ -15,3 +17,4 @@ structure hash_map_t (T : Type) where
hash_map_max_load : Usize
hash_map_slots : Vec (list_t T)
+end Hashmap
diff --git a/tests/lean/HashmapMain/ExternalFuns.lean b/tests/lean/HashmapMain/ExternalFuns.lean
new file mode 100644
index 00000000..bc831158
--- /dev/null
+++ b/tests/lean/HashmapMain/ExternalFuns.lean
@@ -0,0 +1,9 @@
+import Base
+import HashmapMain.Types
+import HashmapMain.Opaque
+
+namespace HashmapMain
+
+def opaque_defs : OpaqueDefs := by sorry
+
+end HashmapMain
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index a59a9f26..34a0eca1 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -5,6 +5,8 @@ import HashmapMain.Types
import HashmapMain.ExternalFuns
open Primitives
+namespace HashmapMain
+
/- [hashmap_main::hashmap::hash_key] -/
def hashmap_hash_key_fwd (k : Usize) : Result Usize :=
Result.ret k
@@ -92,7 +94,7 @@ def hashmap_hash_map_len_fwd
/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/
divergent def hashmap_hash_map_insert_in_list_loop_fwd
(T : Type) (key : Usize) (value : T) (ls : hashmap_list_t T) : Result Bool :=
- match h: ls with
+ match ls with
| hashmap_list_t.Cons ckey cvalue tl =>
if ckey = key
then Result.ret false
@@ -109,7 +111,7 @@ divergent def hashmap_hash_map_insert_in_list_loop_back
(T : Type) (key : Usize) (value : T) (ls : hashmap_list_t T) :
Result (hashmap_list_t T)
:=
- match h: ls with
+ match ls with
| hashmap_list_t.Cons ckey cvalue tl =>
if ckey = key
then Result.ret (hashmap_list_t.Cons ckey value tl)
@@ -173,7 +175,7 @@ divergent def hashmap_hash_map_move_elements_from_list_loop_fwd_back
(T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) :
Result (hashmap_hash_map_t T)
:=
- match h: ls with
+ match ls with
| hashmap_list_t.Cons k v tl =>
do
let ntable0 ← hashmap_hash_map_insert_no_resize_fwd_back T ntable k v
@@ -256,7 +258,7 @@ def hashmap_hash_map_insert_fwd_back
/- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/
divergent def hashmap_hash_map_contains_key_in_list_loop_fwd
(T : Type) (key : Usize) (ls : hashmap_list_t T) : Result Bool :=
- match h: ls with
+ match ls with
| hashmap_list_t.Cons ckey t tl =>
if ckey = key
then Result.ret true
@@ -282,7 +284,7 @@ def hashmap_hash_map_contains_key_fwd
/- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/
divergent def hashmap_hash_map_get_in_list_loop_fwd
(T : Type) (key : Usize) (ls : hashmap_list_t T) : Result T :=
- match h: ls with
+ match ls with
| hashmap_list_t.Cons ckey cvalue tl =>
if ckey = key
then Result.ret cvalue
@@ -308,7 +310,7 @@ def hashmap_hash_map_get_fwd
/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/
divergent def hashmap_hash_map_get_mut_in_list_loop_fwd
(T : Type) (ls : hashmap_list_t T) (key : Usize) : Result T :=
- match h: ls with
+ match ls with
| hashmap_list_t.Cons ckey cvalue tl =>
if ckey = key
then Result.ret cvalue
@@ -325,7 +327,7 @@ divergent def hashmap_hash_map_get_mut_in_list_loop_back
(T : Type) (ls : hashmap_list_t T) (key : Usize) (ret0 : T) :
Result (hashmap_list_t T)
:=
- match h: ls with
+ match ls with
| hashmap_list_t.Cons ckey cvalue tl =>
if ckey = key
then Result.ret (hashmap_list_t.Cons ckey ret0 tl)
@@ -373,14 +375,14 @@ def hashmap_hash_map_get_mut_back
/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/
divergent def hashmap_hash_map_remove_from_list_loop_fwd
(T : Type) (key : Usize) (ls : hashmap_list_t T) : Result (Option T) :=
- match h: ls with
+ match ls with
| hashmap_list_t.Cons ckey t tl =>
if ckey = key
then
let mv_ls :=
mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.Cons ckey t tl)
hashmap_list_t.Nil
- match h: mv_ls with
+ match mv_ls with
| hashmap_list_t.Cons i cvalue tl0 => Result.ret (Option.some cvalue)
| hashmap_list_t.Nil => Result.fail Error.panic
else hashmap_hash_map_remove_from_list_loop_fwd T key tl
@@ -396,14 +398,14 @@ divergent def hashmap_hash_map_remove_from_list_loop_back
(T : Type) (key : Usize) (ls : hashmap_list_t T) :
Result (hashmap_list_t T)
:=
- match h: ls with
+ match ls with
| hashmap_list_t.Cons ckey t tl =>
if ckey = key
then
let mv_ls :=
mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.Cons ckey t tl)
hashmap_list_t.Nil
- match h: mv_ls with
+ match mv_ls with
| hashmap_list_t.Cons i cvalue tl0 => Result.ret tl0
| hashmap_list_t.Nil => Result.fail Error.panic
else
@@ -429,7 +431,7 @@ def hashmap_hash_map_remove_fwd
let l ←
vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod
let x ← hashmap_hash_map_remove_from_list_fwd T key l
- match h: x with
+ match x with
| Option.none => Result.ret Option.none
| Option.some x0 =>
do
@@ -449,7 +451,7 @@ def hashmap_hash_map_remove_back
let l ←
vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod
let x ← hashmap_hash_map_remove_from_list_fwd T key l
- match h: x with
+ match x with
| Option.none =>
do
let l0 ← hashmap_hash_map_remove_from_list_back T key l
@@ -505,7 +507,7 @@ def hashmap_test1_fwd : Result Unit :=
let x ←
hashmap_hash_map_remove_fwd U64 hm4
(Usize.ofInt 1024 (by intlit))
- match h: x with
+ match x with
| Option.none => Result.fail Error.panic
| Option.some x0 =>
if not (x0 = (U64.ofInt 56 (by intlit)))
@@ -555,3 +557,4 @@ def main_fwd : Result Unit :=
/- Unit test for [hashmap_main::main] -/
#assert (main_fwd == .ret ())
+end HashmapMain
diff --git a/tests/lean/HashmapMain/Opaque.lean b/tests/lean/HashmapMain/Opaque.lean
index bef4f3fb..10e4d8bd 100644
--- a/tests/lean/HashmapMain/Opaque.lean
+++ b/tests/lean/HashmapMain/Opaque.lean
@@ -4,13 +4,16 @@ import Base
import HashmapMain.Types
open Primitives
+namespace HashmapMain
+
structure OpaqueDefs where
/- [hashmap_main::hashmap_utils::deserialize] -/
hashmap_utils_deserialize_fwd
- : State -> Result (State × (hashmap_hash_map_t U64))
+ : State → Result (State × (hashmap_hash_map_t U64))
/- [hashmap_main::hashmap_utils::serialize] -/
hashmap_utils_serialize_fwd
- : hashmap_hash_map_t U64 -> State -> Result (State × Unit)
+ : hashmap_hash_map_t U64 → State → Result (State × Unit)
+end HashmapMain
diff --git a/tests/lean/HashmapMain/Types.lean b/tests/lean/HashmapMain/Types.lean
index 858e1c51..b91ff3a7 100644
--- a/tests/lean/HashmapMain/Types.lean
+++ b/tests/lean/HashmapMain/Types.lean
@@ -3,9 +3,11 @@
import Base
open Primitives
+namespace HashmapMain
+
/- [hashmap_main::hashmap::List] -/
inductive hashmap_list_t (T : Type) :=
-| Cons : Usize -> T -> hashmap_list_t T -> hashmap_list_t T
+| Cons : Usize → T → hashmap_list_t T → hashmap_list_t T
| Nil : hashmap_list_t T
/- [hashmap_main::hashmap::HashMap] -/
@@ -18,3 +20,4 @@ structure hashmap_hash_map_t (T : Type) where
/- The state type used in the state-error monad -/
axiom State : Type
+end HashmapMain
diff --git a/tests/lean/Loops/Funs.lean b/tests/lean/Loops/Funs.lean
index 7d5f7595..9e084327 100644
--- a/tests/lean/Loops/Funs.lean
+++ b/tests/lean/Loops/Funs.lean
@@ -4,6 +4,8 @@ import Base
import Loops.Types
open Primitives
+namespace Loops
+
/- [loops::sum] -/
divergent def sum_loop_fwd (max : U32) (i : U32) (s : U32) : Result U32 :=
if i < max
@@ -68,7 +70,7 @@ def clear_fwd_back (v : Vec U32) : Result (Vec U32) :=
/- [loops::list_mem] -/
divergent def list_mem_loop_fwd (x : U32) (ls : list_t U32) : Result Bool :=
- match h: ls with
+ match ls with
| list_t.Cons y tl =>
if y = x
then Result.ret true
@@ -82,7 +84,7 @@ def list_mem_fwd (x : U32) (ls : list_t U32) : Result Bool :=
/- [loops::list_nth_mut_loop] -/
divergent def list_nth_mut_loop_loop_fwd
(T : Type) (ls : list_t T) (i : U32) : Result T :=
- match h: ls with
+ match ls with
| list_t.Cons x tl =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret x
@@ -99,7 +101,7 @@ def list_nth_mut_loop_fwd (T : Type) (ls : list_t T) (i : U32) : Result T :=
/- [loops::list_nth_mut_loop] -/
divergent def list_nth_mut_loop_loop_back
(T : Type) (ls : list_t T) (i : U32) (ret0 : T) : Result (list_t T) :=
- match h: ls with
+ match ls with
| list_t.Cons x tl =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret (list_t.Cons ret0 tl)
@@ -118,7 +120,7 @@ def list_nth_mut_loop_back
/- [loops::list_nth_shared_loop] -/
divergent def list_nth_shared_loop_loop_fwd
(T : Type) (ls : list_t T) (i : U32) : Result T :=
- match h: ls with
+ match ls with
| list_t.Cons x tl =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret x
@@ -135,7 +137,7 @@ def list_nth_shared_loop_fwd (T : Type) (ls : list_t T) (i : U32) : Result T :=
/- [loops::get_elem_mut] -/
divergent def get_elem_mut_loop_fwd
(x : Usize) (ls : list_t Usize) : Result Usize :=
- match h: ls with
+ match ls with
| list_t.Cons y tl =>
if y = x
then Result.ret y
@@ -152,7 +154,7 @@ def get_elem_mut_fwd (slots : Vec (list_t Usize)) (x : Usize) : Result Usize :=
/- [loops::get_elem_mut] -/
divergent def get_elem_mut_loop_back
(x : Usize) (ls : list_t Usize) (ret0 : Usize) : Result (list_t Usize) :=
- match h: ls with
+ match ls with
| list_t.Cons y tl =>
if y = x
then Result.ret (list_t.Cons ret0 tl)
@@ -176,7 +178,7 @@ def get_elem_mut_back
/- [loops::get_elem_shared] -/
divergent def get_elem_shared_loop_fwd
(x : Usize) (ls : list_t Usize) : Result Usize :=
- match h: ls with
+ match ls with
| list_t.Cons y tl =>
if y = x
then Result.ret y
@@ -206,7 +208,7 @@ def id_shared_fwd (T : Type) (ls : list_t T) : Result (list_t T) :=
/- [loops::list_nth_mut_loop_with_id] -/
divergent def list_nth_mut_loop_with_id_loop_fwd
(T : Type) (i : U32) (ls : list_t T) : Result T :=
- match h: ls with
+ match ls with
| list_t.Cons x tl =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret x
@@ -226,7 +228,7 @@ def list_nth_mut_loop_with_id_fwd
/- [loops::list_nth_mut_loop_with_id] -/
divergent def list_nth_mut_loop_with_id_loop_back
(T : Type) (i : U32) (ls : list_t T) (ret0 : T) : Result (list_t T) :=
- match h: ls with
+ match ls with
| list_t.Cons x tl =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret (list_t.Cons ret0 tl)
@@ -248,7 +250,7 @@ def list_nth_mut_loop_with_id_back
/- [loops::list_nth_shared_loop_with_id] -/
divergent def list_nth_shared_loop_with_id_loop_fwd
(T : Type) (i : U32) (ls : list_t T) : Result T :=
- match h: ls with
+ match ls with
| list_t.Cons x tl =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret x
@@ -268,9 +270,9 @@ def list_nth_shared_loop_with_id_fwd
/- [loops::list_nth_mut_loop_pair] -/
divergent def list_nth_mut_loop_pair_loop_fwd
(T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
- match h: ls0 with
+ match ls0 with
| list_t.Cons x0 tl0 =>
- match h: ls1 with
+ match ls1 with
| list_t.Cons x1 tl1 =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret (x0, x1)
@@ -291,9 +293,9 @@ divergent def list_nth_mut_loop_pair_loop_back'a
(T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
Result (list_t T)
:=
- match h: ls0 with
+ match ls0 with
| list_t.Cons x0 tl0 =>
- match h: ls1 with
+ match ls1 with
| list_t.Cons x1 tl1 =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret (list_t.Cons ret0 tl0)
@@ -317,9 +319,9 @@ divergent def list_nth_mut_loop_pair_loop_back'b
(T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
Result (list_t T)
:=
- match h: ls0 with
+ match ls0 with
| list_t.Cons x0 tl0 =>
- match h: ls1 with
+ match ls1 with
| list_t.Cons x1 tl1 =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret (list_t.Cons ret0 tl1)
@@ -341,9 +343,9 @@ def list_nth_mut_loop_pair_back'b
/- [loops::list_nth_shared_loop_pair] -/
divergent def list_nth_shared_loop_pair_loop_fwd
(T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
- match h: ls0 with
+ match ls0 with
| list_t.Cons x0 tl0 =>
- match h: ls1 with
+ match ls1 with
| list_t.Cons x1 tl1 =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret (x0, x1)
@@ -362,9 +364,9 @@ def list_nth_shared_loop_pair_fwd
/- [loops::list_nth_mut_loop_pair_merge] -/
divergent def list_nth_mut_loop_pair_merge_loop_fwd
(T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
- match h: ls0 with
+ match ls0 with
| list_t.Cons x0 tl0 =>
- match h: ls1 with
+ match ls1 with
| list_t.Cons x1 tl1 =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret (x0, x1)
@@ -385,9 +387,9 @@ divergent def list_nth_mut_loop_pair_merge_loop_back
(T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : (T × T)) :
Result ((list_t T) × (list_t T))
:=
- match h: ls0 with
+ match ls0 with
| list_t.Cons x0 tl0 =>
- match h: ls1 with
+ match ls1 with
| list_t.Cons x1 tl1 =>
if i = (U32.ofInt 0 (by intlit))
then
@@ -412,9 +414,9 @@ def list_nth_mut_loop_pair_merge_back
/- [loops::list_nth_shared_loop_pair_merge] -/
divergent def list_nth_shared_loop_pair_merge_loop_fwd
(T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
- match h: ls0 with
+ match ls0 with
| list_t.Cons x0 tl0 =>
- match h: ls1 with
+ match ls1 with
| list_t.Cons x1 tl1 =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret (x0, x1)
@@ -433,9 +435,9 @@ def list_nth_shared_loop_pair_merge_fwd
/- [loops::list_nth_mut_shared_loop_pair] -/
divergent def list_nth_mut_shared_loop_pair_loop_fwd
(T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
- match h: ls0 with
+ match ls0 with
| list_t.Cons x0 tl0 =>
- match h: ls1 with
+ match ls1 with
| list_t.Cons x1 tl1 =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret (x0, x1)
@@ -456,9 +458,9 @@ divergent def list_nth_mut_shared_loop_pair_loop_back
(T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
Result (list_t T)
:=
- match h: ls0 with
+ match ls0 with
| list_t.Cons x0 tl0 =>
- match h: ls1 with
+ match ls1 with
| list_t.Cons x1 tl1 =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret (list_t.Cons ret0 tl0)
@@ -481,9 +483,9 @@ def list_nth_mut_shared_loop_pair_back
/- [loops::list_nth_mut_shared_loop_pair_merge] -/
divergent def list_nth_mut_shared_loop_pair_merge_loop_fwd
(T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
- match h: ls0 with
+ match ls0 with
| list_t.Cons x0 tl0 =>
- match h: ls1 with
+ match ls1 with
| list_t.Cons x1 tl1 =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret (x0, x1)
@@ -504,9 +506,9 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop_back
(T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
Result (list_t T)
:=
- match h: ls0 with
+ match ls0 with
| list_t.Cons x0 tl0 =>
- match h: ls1 with
+ match ls1 with
| list_t.Cons x1 tl1 =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret (list_t.Cons ret0 tl0)
@@ -529,9 +531,9 @@ def list_nth_mut_shared_loop_pair_merge_back
/- [loops::list_nth_shared_mut_loop_pair] -/
divergent def list_nth_shared_mut_loop_pair_loop_fwd
(T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
- match h: ls0 with
+ match ls0 with
| list_t.Cons x0 tl0 =>
- match h: ls1 with
+ match ls1 with
| list_t.Cons x1 tl1 =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret (x0, x1)
@@ -552,9 +554,9 @@ divergent def list_nth_shared_mut_loop_pair_loop_back
(T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
Result (list_t T)
:=
- match h: ls0 with
+ match ls0 with
| list_t.Cons x0 tl0 =>
- match h: ls1 with
+ match ls1 with
| list_t.Cons x1 tl1 =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret (list_t.Cons ret0 tl1)
@@ -577,9 +579,9 @@ def list_nth_shared_mut_loop_pair_back
/- [loops::list_nth_shared_mut_loop_pair_merge] -/
divergent def list_nth_shared_mut_loop_pair_merge_loop_fwd
(T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
- match h: ls0 with
+ match ls0 with
| list_t.Cons x0 tl0 =>
- match h: ls1 with
+ match ls1 with
| list_t.Cons x1 tl1 =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret (x0, x1)
@@ -600,9 +602,9 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop_back
(T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
Result (list_t T)
:=
- match h: ls0 with
+ match ls0 with
| list_t.Cons x0 tl0 =>
- match h: ls1 with
+ match ls1 with
| list_t.Cons x1 tl1 =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret (list_t.Cons ret0 tl1)
@@ -622,3 +624,4 @@ def list_nth_shared_mut_loop_pair_merge_back
:=
list_nth_shared_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0
+end Loops
diff --git a/tests/lean/Loops/Types.lean b/tests/lean/Loops/Types.lean
index e14f9766..ca0403e9 100644
--- a/tests/lean/Loops/Types.lean
+++ b/tests/lean/Loops/Types.lean
@@ -3,8 +3,11 @@
import Base
open Primitives
+namespace Loops
+
/- [loops::List] -/
inductive list_t (T : Type) :=
-| Cons : T -> list_t T -> list_t T
+| Cons : T → list_t T → list_t T
| Nil : list_t T
+end Loops
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 67ef4b20..769bb311 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -3,6 +3,8 @@
import Base
open Primitives
+namespace NoNestedBorrows
+
/- [no_nested_borrows::Pair] -/
structure pair_t (T1 T2 : Type) where
pair_x : T1
@@ -10,12 +12,12 @@ structure pair_t (T1 T2 : Type) where
/- [no_nested_borrows::List] -/
inductive list_t (T : Type) :=
-| Cons : T -> list_t T -> list_t T
+| Cons : T → list_t T → list_t T
| Nil : list_t T
/- [no_nested_borrows::One] -/
inductive one_t (T1 : Type) :=
-| One : T1 -> one_t T1
+| One : T1 → one_t T1
/- [no_nested_borrows::EmptyEnum] -/
inductive empty_enum_t :=
@@ -31,8 +33,8 @@ structure empty_struct_t where
/- [no_nested_borrows::Sum] -/
inductive sum_t (T1 T2 : Type) :=
-| Left : T1 -> sum_t T1 T2
-| Right : T2 -> sum_t T1 T2
+| Left : T1 → sum_t T1 T2
+| Right : T2 → sum_t T1 T2
/- [no_nested_borrows::neg_test] -/
def neg_test_fwd (x : I32) : Result I32 :=
@@ -175,7 +177,7 @@ def test_copy_int_fwd : Result Unit :=
/- [no_nested_borrows::is_cons] -/
def is_cons_fwd (T : Type) (l : list_t T) : Result Bool :=
- match h: l with
+ match l with
| list_t.Cons t l0 => Result.ret true
| list_t.Nil => Result.ret false
@@ -193,7 +195,7 @@ def test_is_cons_fwd : Result Unit :=
/- [no_nested_borrows::split_list] -/
def split_list_fwd (T : Type) (l : list_t T) : Result (T × (list_t T)) :=
- match h: l with
+ match l with
| list_t.Cons hd tl => Result.ret (hd, tl)
| list_t.Nil => Result.fail Error.panic
@@ -254,19 +256,19 @@ mutual
/- [no_nested_borrows::NodeElem] -/
inductive node_elem_t (T : Type) :=
-| Cons : tree_t T -> node_elem_t T -> node_elem_t T
+| Cons : tree_t T → node_elem_t T → node_elem_t T
| Nil : node_elem_t T
/- [no_nested_borrows::Tree] -/
inductive tree_t (T : Type) :=
-| Leaf : T -> tree_t T
-| Node : T -> node_elem_t T -> tree_t T -> tree_t T
+| Leaf : T → tree_t T
+| Node : T → node_elem_t T → tree_t T → tree_t T
end
/- [no_nested_borrows::list_length] -/
divergent def list_length_fwd (T : Type) (l : list_t T) : Result U32 :=
- match h: l with
+ match l with
| list_t.Cons t l1 =>
do
let i ← list_length_fwd T l1
@@ -276,7 +278,7 @@ divergent def list_length_fwd (T : Type) (l : list_t T) : Result U32 :=
/- [no_nested_borrows::list_nth_shared] -/
divergent def list_nth_shared_fwd
(T : Type) (l : list_t T) (i : U32) : Result T :=
- match h: l with
+ match l with
| list_t.Cons x tl =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret x
@@ -289,7 +291,7 @@ divergent def list_nth_shared_fwd
/- [no_nested_borrows::list_nth_mut] -/
divergent def list_nth_mut_fwd
(T : Type) (l : list_t T) (i : U32) : Result T :=
- match h: l with
+ match l with
| list_t.Cons x tl =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret x
@@ -301,7 +303,7 @@ divergent def list_nth_mut_fwd
/- [no_nested_borrows::list_nth_mut] -/
divergent def list_nth_mut_back
(T : Type) (l : list_t T) (i : U32) (ret0 : T) : Result (list_t T) :=
- match h: l with
+ match l with
| list_t.Cons x tl =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret (list_t.Cons ret0 tl)
@@ -315,7 +317,7 @@ divergent def list_nth_mut_back
/- [no_nested_borrows::list_rev_aux] -/
divergent def list_rev_aux_fwd
(T : Type) (li : list_t T) (lo : list_t T) : Result (list_t T) :=
- match h: li with
+ match li with
| list_t.Cons hd tl => list_rev_aux_fwd T tl (list_t.Cons hd lo)
| list_t.Nil => Result.ret lo
@@ -531,7 +533,7 @@ def test_shared_borrow_bool2_fwd : Result U32 :=
/- [no_nested_borrows::test_shared_borrow_enum1] -/
def test_shared_borrow_enum1_fwd (l : list_t U32) : Result U32 :=
- match h: l with
+ match l with
| list_t.Cons i l0 => Result.ret (U32.ofInt 1 (by intlit))
| list_t.Nil => Result.ret (U32.ofInt 0 (by intlit))
@@ -539,3 +541,4 @@ def test_shared_borrow_enum1_fwd (l : list_t U32) : Result U32 :=
def test_shared_borrow_enum2_fwd : Result U32 :=
Result.ret (U32.ofInt 0 (by intlit))
+end NoNestedBorrows
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index 9019b694..edcb5c1b 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -3,6 +3,8 @@
import Base
open Primitives
+namespace Paper
+
/- [paper::ref_incr] -/
def ref_incr_fwd_back (x : I32) : Result I32 :=
x + (I32.ofInt 1 (by intlit))
@@ -56,13 +58,13 @@ def test_choose_fwd : Result Unit :=
/- [paper::List] -/
inductive list_t (T : Type) :=
-| Cons : T -> list_t T -> list_t T
+| Cons : T → list_t T → list_t T
| Nil : list_t T
/- [paper::list_nth_mut] -/
divergent def list_nth_mut_fwd
(T : Type) (l : list_t T) (i : U32) : Result T :=
- match h: l with
+ match l with
| list_t.Cons x tl =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret x
@@ -74,7 +76,7 @@ divergent def list_nth_mut_fwd
/- [paper::list_nth_mut] -/
divergent def list_nth_mut_back
(T : Type) (l : list_t T) (i : U32) (ret0 : T) : Result (list_t T) :=
- match h: l with
+ match l with
| list_t.Cons x tl =>
if i = (U32.ofInt 0 (by intlit))
then Result.ret (list_t.Cons ret0 tl)
@@ -87,7 +89,7 @@ divergent def list_nth_mut_back
/- [paper::sum] -/
divergent def sum_fwd (l : list_t I32) : Result I32 :=
- match h: l with
+ match l with
| list_t.Cons x tl => do
let i ← sum_fwd tl
x + i
@@ -123,3 +125,4 @@ def call_choose_fwd (p : (U32 × U32)) : Result U32 :=
let (px0, _) ← choose_back U32 true px py pz0
Result.ret px0
+end Paper
diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean
index 671f54ea..0f2a05e3 100644
--- a/tests/lean/PoloniusList.lean
+++ b/tests/lean/PoloniusList.lean
@@ -3,15 +3,17 @@
import Base
open Primitives
+namespace PoloniusList
+
/- [polonius_list::List] -/
inductive list_t (T : Type) :=
-| Cons : T -> list_t T -> list_t T
+| Cons : T → list_t T → list_t T
| Nil : list_t T
/- [polonius_list::get_list_at_x] -/
divergent def get_list_at_x_fwd
(ls : list_t U32) (x : U32) : Result (list_t U32) :=
- match h: ls with
+ match ls with
| list_t.Cons hd tl =>
if hd = x
then Result.ret (list_t.Cons hd tl)
@@ -21,7 +23,7 @@ divergent def get_list_at_x_fwd
/- [polonius_list::get_list_at_x] -/
divergent def get_list_at_x_back
(ls : list_t U32) (x : U32) (ret0 : list_t U32) : Result (list_t U32) :=
- match h: ls with
+ match ls with
| list_t.Cons hd tl =>
if hd = x
then Result.ret ret0
@@ -31,3 +33,4 @@ divergent def get_list_at_x_back
Result.ret (list_t.Cons hd tl0)
| list_t.Nil => Result.ret ret0
+end PoloniusList
diff --git a/tests/lean/lake-manifest.json b/tests/lean/lake-manifest.json
index 1397c6f0..ccd6d61a 100644
--- a/tests/lean/lake-manifest.json
+++ b/tests/lean/lake-manifest.json
@@ -11,7 +11,7 @@
{"git":
{"url": "https://github.com/leanprover-community/mathlib4.git",
"subDir?": null,
- "rev": "cb02d09e1d5611d22efc2b406e7893f246b2f51e",
+ "rev": "409bee4eabf8072c4569950c3c2f310afd203abf",
"name": "mathlib",
"inputRev?": null}},
{"git":
diff --git a/tests/lean/lakefile.lean b/tests/lean/lakefile.lean
index da4293dd..217e533f 100644
--- a/tests/lean/lakefile.lean
+++ b/tests/lean/lakefile.lean
@@ -11,4 +11,12 @@ package «tests» {}
@[default_target]
lean_lib «Tests» {}
+lean_lib betreeMain
+lean_lib constants
+lean_lib external
lean_lib hashmap
+lean_lib hashmapMain
+lean_lib loops
+lean_lib noNestedBorrows
+lean_lib paper
+lean_lib poloniusList
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 20:26:15 +0000