From b643bd00747e75d69b6066c55a1798b61277c4b6 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 4 Jul 2023 18:09:36 +0200 Subject: Regenerate the Lean test files --- tests/lean/BetreeMain/ExternalFuns.lean | 9 ++ tests/lean/BetreeMain/Funs.lean | 147 ++++++++++++++++--------------- tests/lean/BetreeMain/Opaque.lean | 16 ++-- tests/lean/BetreeMain/Types.lean | 24 +++-- tests/lean/Constants.lean | 3 + tests/lean/External/ExternalFuns.lean | 9 ++ tests/lean/External/Funs.lean | 3 + tests/lean/External/Opaque.lean | 14 +-- tests/lean/External/Types.lean | 3 + tests/lean/Hashmap/Funs.lean | 31 ++++--- tests/lean/Hashmap/Types.lean | 5 +- tests/lean/HashmapMain/ExternalFuns.lean | 9 ++ tests/lean/HashmapMain/Funs.lean | 31 ++++--- tests/lean/HashmapMain/Opaque.lean | 7 +- tests/lean/HashmapMain/Types.lean | 5 +- tests/lean/Loops/Funs.lean | 83 ++++++++--------- tests/lean/Loops/Types.lean | 5 +- tests/lean/NoNestedBorrows.lean | 33 +++---- tests/lean/Paper.lean | 11 ++- tests/lean/PoloniusList.lean | 9 +- tests/lean/lake-manifest.json | 2 +- tests/lean/lakefile.lean | 8 ++ 22 files changed, 275 insertions(+), 192 deletions(-) create mode 100644 tests/lean/BetreeMain/ExternalFuns.lean create mode 100644 tests/lean/External/ExternalFuns.lean create mode 100644 tests/lean/HashmapMain/ExternalFuns.lean 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 -- cgit v1.2.3