diff options
Diffstat (limited to 'tests/lean')
| -rw-r--r-- | tests/lean/BetreeMain/Funs.lean | 614 | ||||
| -rw-r--r-- | tests/lean/BetreeMain/FunsExternal.lean | 8 | ||||
| -rw-r--r-- | tests/lean/BetreeMain/FunsExternal_Template.lean | 11 | ||||
| -rw-r--r-- | tests/lean/BetreeMain/Types.lean | 44 | ||||
| -rw-r--r-- | tests/lean/Constants.lean | 28 | ||||
| -rw-r--r-- | tests/lean/External/Funs.lean | 4 | ||||
| -rw-r--r-- | tests/lean/External/FunsExternal_Template.lean | 3 | ||||
| -rw-r--r-- | tests/lean/External/Types.lean | 2 | ||||
| -rw-r--r-- | tests/lean/Hashmap/Funs.lean | 203 | ||||
| -rw-r--r-- | tests/lean/Hashmap/Types.lean | 10 | ||||
| -rw-r--r-- | tests/lean/HashmapMain/Funs.lean | 232 | ||||
| -rw-r--r-- | tests/lean/HashmapMain/FunsExternal.lean | 4 | ||||
| -rw-r--r-- | tests/lean/HashmapMain/FunsExternal_Template.lean | 4 | ||||
| -rw-r--r-- | tests/lean/HashmapMain/Types.lean | 10 | ||||
| -rw-r--r-- | tests/lean/Loops/Funs.lean | 355 | ||||
| -rw-r--r-- | tests/lean/Loops/Types.lean | 6 | ||||
| -rw-r--r-- | tests/lean/NoNestedBorrows.lean | 143 | ||||
| -rw-r--r-- | tests/lean/Paper.lean | 43 | ||||
| -rw-r--r-- | tests/lean/PoloniusList.lean | 22 |
19 files changed, 857 insertions, 889 deletions
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean index 78e14146..3a678c71 100644 --- a/tests/lean/BetreeMain/Funs.lean +++ b/tests/lean/BetreeMain/Funs.lean @@ -9,13 +9,13 @@ namespace betree_main /- [betree_main::betree::load_internal_node] -/ def betree.load_internal_node_fwd (id : U64) (st : State) : - Result (State × (betree_list_t (U64 × betree_message_t))) + Result (State × (betree.List (U64 × betree.Message))) := betree_utils.load_internal_node_fwd id st /- [betree_main::betree::store_internal_node] -/ def betree.store_internal_node_fwd - (id : U64) (content : betree_list_t (U64 × betree_message_t)) (st : State) : + (id : U64) (content : betree.List (U64 × betree.Message)) (st : State) : Result (State × Unit) := do @@ -24,12 +24,12 @@ def betree.store_internal_node_fwd /- [betree_main::betree::load_leaf_node] -/ def betree.load_leaf_node_fwd - (id : U64) (st : State) : Result (State × (betree_list_t (U64 × U64))) := + (id : U64) (st : State) : Result (State × (betree.List (U64 × U64))) := betree_utils.load_leaf_node_fwd id st /- [betree_main::betree::store_leaf_node] -/ def betree.store_leaf_node_fwd - (id : U64) (content : betree_list_t (U64 × U64)) (st : State) : + (id : U64) (content : betree.List (U64 × U64)) (st : State) : Result (State × Unit) := do @@ -47,13 +47,13 @@ def betree.fresh_node_id_back (counter : U64) : Result U64 := counter + (U64.ofInt 1 (by intlit)) /- [betree_main::betree::NodeIdCounter::{0}::new] -/ -def betree.NodeIdCounter.new_fwd : Result betree_node_id_counter_t := +def betree.NodeIdCounter.new_fwd : Result betree.NodeIdCounter := Result.ret { betree_node_id_counter_next_node_id := (U64.ofInt 0 (by intlit)) } /- [betree_main::betree::NodeIdCounter::{0}::fresh_id] -/ def betree.NodeIdCounter.fresh_id_fwd - (self : betree_node_id_counter_t) : Result U64 := + (self : betree.NodeIdCounter) : Result U64 := do let _ ← self.betree_node_id_counter_next_node_id + (U64.ofInt 1 (by intlit)) @@ -61,7 +61,7 @@ def betree.NodeIdCounter.fresh_id_fwd /- [betree_main::betree::NodeIdCounter::{0}::fresh_id] -/ def betree.NodeIdCounter.fresh_id_back - (self : betree_node_id_counter_t) : Result betree_node_id_counter_t := + (self : betree.NodeIdCounter) : Result betree.NodeIdCounter := do let i ← self.betree_node_id_counter_next_node_id + (U64.ofInt 1 (by intlit)) @@ -74,113 +74,112 @@ 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 := + (prev : Option U64) (st : betree.UpsertFunState) : Result U64 := match prev with | Option.none => 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)) + | betree.UpsertFunState.Add v => Result.ret v + | betree.UpsertFunState.Sub i => Result.ret (U64.ofInt 0 (by intlit)) | Option.some prev0 => match st with - | betree_upsert_fun_state_t.Add v => + | betree.UpsertFunState.Add v => do let margin ← core_num_u64_max_c - prev0 if margin >= v then prev0 + v else Result.ret core_num_u64_max_c - | betree_upsert_fun_state_t.Sub v => + | betree.UpsertFunState.Sub v => if prev0 >= v then prev0 - v else Result.ret (U64.ofInt 0 (by intlit)) /- [betree_main::betree::List::{1}::len] -/ divergent def betree.List.len_fwd - (T : Type) (self : betree_list_t T) : Result U64 := + (T : Type) (self : betree.List T) : Result U64 := match self with - | betree_list_t.Cons t tl => + | betree.List.Cons t tl => do let i ← betree.List.len_fwd T tl (U64.ofInt 1 (by intlit)) + i - | betree_list_t.Nil => Result.ret (U64.ofInt 0 (by intlit)) + | betree.List.Nil => Result.ret (U64.ofInt 0 (by intlit)) /- [betree_main::betree::List::{1}::split_at] -/ divergent def betree.List.split_at_fwd - (T : Type) (self : betree_list_t T) (n : U64) : - Result ((betree_list_t T) × (betree_list_t T)) + (T : Type) (self : betree.List T) (n : U64) : + Result ((betree.List T) × (betree.List T)) := if n = (U64.ofInt 0 (by intlit)) - then Result.ret (betree_list_t.Nil, self) + then Result.ret (betree.List.Nil, self) else match self with - | betree_list_t.Cons hd tl => + | betree.List.Cons hd tl => do let i ← n - (U64.ofInt 1 (by intlit)) let p ← betree.List.split_at_fwd T tl i let (ls0, ls1) := p let l := ls0 - Result.ret (betree_list_t.Cons hd l, ls1) - | betree_list_t.Nil => Result.fail Error.panic + Result.ret (betree.List.Cons hd l, ls1) + | betree.List.Nil => Result.fail Error.panic /- [betree_main::betree::List::{1}::push_front] -/ def betree.List.push_front_fwd_back - (T : Type) (self : betree_list_t T) (x : T) : Result (betree_list_t T) := - let tl := mem_replace_fwd (betree_list_t T) self betree_list_t.Nil + (T : Type) (self : betree.List T) (x : T) : Result (betree.List T) := + let tl := mem_replace_fwd (betree.List T) self betree.List.Nil let l := tl - Result.ret (betree_list_t.Cons x l) + Result.ret (betree.List.Cons x l) /- [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 +def betree.List.pop_front_fwd (T : Type) (self : betree.List T) : Result T := + let ls := mem_replace_fwd (betree.List T) self betree.List.Nil match ls with - | betree_list_t.Cons x tl => Result.ret x - | betree_list_t.Nil => Result.fail Error.panic + | betree.List.Cons x tl => Result.ret x + | betree.List.Nil => Result.fail Error.panic /- [betree_main::betree::List::{1}::pop_front] -/ 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 + (T : Type) (self : betree.List T) : Result (betree.List T) := + let ls := mem_replace_fwd (betree.List T) self betree.List.Nil match ls with - | betree_list_t.Cons x tl => Result.ret tl - | betree_list_t.Nil => Result.fail Error.panic + | betree.List.Cons x tl => Result.ret tl + | betree.List.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 := +def betree.List.hd_fwd (T : Type) (self : betree.List T) : Result T := match self with - | betree_list_t.Cons hd l => Result.ret hd - | betree_list_t.Nil => Result.fail Error.panic + | betree.List.Cons hd l => Result.ret hd + | betree.List.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 := + (T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool := match self with - | betree_list_t.Cons hd l => let (i, _) := hd - Result.ret (i = key) - | betree_list_t.Nil => Result.ret false + | betree.List.Cons hd l => let (i, _) := hd + Result.ret (i = key) + | betree.List.Nil => Result.ret false /- [betree_main::betree::List::{2}::partition_at_pivot] -/ 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))) + (T : Type) (self : betree.List (U64 × T)) (pivot : U64) : + Result ((betree.List (U64 × T)) × (betree.List (U64 × T))) := match self with - | betree_list_t.Cons hd tl => + | betree.List.Cons hd tl => let (i, t) := hd if i >= pivot - then Result.ret (betree_list_t.Nil, betree_list_t.Cons (i, t) tl) + then Result.ret (betree.List.Nil, betree.List.Cons (i, t) tl) else do let p ← betree.List.partition_at_pivot_fwd T tl pivot let (ls0, ls1) := p let l := ls0 - Result.ret (betree_list_t.Cons (i, t) l, ls1) - | betree_list_t.Nil => Result.ret (betree_list_t.Nil, betree_list_t.Nil) + Result.ret (betree.List.Cons (i, t) l, ls1) + | betree.List.Nil => Result.ret (betree.List.Nil, betree.List.Nil) /- [betree_main::betree::Leaf::{3}::split] -/ def betree.Leaf.split_fwd - (self : betree_leaf_t) (content : betree_list_t (U64 × U64)) - (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) - (st : State) : - Result (State × betree_internal_t) + (self : betree.Leaf) (content : betree.List (U64 × U64)) + (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) : + Result (State × betree.Internal) := do let p ← @@ -194,24 +193,23 @@ def betree.Leaf.split_fwd let id1 ← betree.NodeIdCounter.fresh_id_fwd node_id_cnt0 let (st0, _) ← betree.store_leaf_node_fwd id0 content0 st let (st1, _) ← betree.store_leaf_node_fwd id1 content1 st0 - let n := betree_node_t.Leaf + let n := betree.Node.Leaf { betree_leaf_id := id0, betree_leaf_size := params.betree_params_split_size } - let n0 := betree_node_t.Leaf + let n0 := betree.Node.Leaf { betree_leaf_id := id1, betree_leaf_size := params.betree_params_split_size } - Result.ret (st1, betree_internal_t.mk self.betree_leaf_id pivot n n0) + Result.ret (st1, betree.Internal.mk self.betree_leaf_id pivot n n0) /- [betree_main::betree::Leaf::{3}::split] -/ def betree.Leaf.split_back - (self : betree_leaf_t) (content : betree_list_t (U64 × U64)) - (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) - (st : State) : - Result betree_node_id_counter_t + (self : betree.Leaf) (content : betree.List (U64 × U64)) + (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) : + Result betree.NodeIdCounter := do let p ← @@ -228,9 +226,9 @@ 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) := + (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) := match bindings with - | betree_list_t.Cons hd tl => + | betree.List.Cons hd tl => let (i, i0) := hd if i = key then Result.ret (Option.some i0) @@ -238,29 +236,29 @@ divergent def betree.Node.lookup_in_bindings_fwd if i > key then Result.ret Option.none else betree.Node.lookup_in_bindings_fwd key tl - | betree_list_t.Nil => Result.ret Option.none + | betree.List.Nil => Result.ret Option.none /- [betree_main::betree::Node::{5}::lookup_first_message_for_key] -/ 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)) + (key : U64) (msgs : betree.List (U64 × betree.Message)) : + Result (betree.List (U64 × betree.Message)) := match msgs with - | betree_list_t.Cons x next_msgs => + | betree.List.Cons x next_msgs => let (i, m) := x if i >= key - then Result.ret (betree_list_t.Cons (i, m) next_msgs) + then Result.ret (betree.List.Cons (i, m) next_msgs) else betree.Node.lookup_first_message_for_key_fwd key next_msgs - | betree_list_t.Nil => Result.ret betree_list_t.Nil + | betree.List.Nil => Result.ret betree.List.Nil /- [betree_main::betree::Node::{5}::lookup_first_message_for_key] -/ divergent def betree.Node.lookup_first_message_for_key_back - (key : U64) (msgs : betree_list_t (U64 × betree_message_t)) - (ret0 : betree_list_t (U64 × betree_message_t)) : - Result (betree_list_t (U64 × betree_message_t)) + (key : U64) (msgs : betree.List (U64 × betree.Message)) + (ret0 : betree.List (U64 × betree.Message)) : + Result (betree.List (U64 × betree.Message)) := match msgs with - | betree_list_t.Cons x next_msgs => + | betree.List.Cons x next_msgs => let (i, m) := x if i >= key then Result.ret ret0 @@ -268,134 +266,134 @@ divergent def betree.Node.lookup_first_message_for_key_back do let next_msgs0 ← betree.Node.lookup_first_message_for_key_back key next_msgs ret0 - Result.ret (betree_list_t.Cons (i, m) next_msgs0) - | betree_list_t.Nil => Result.ret ret0 + Result.ret (betree.List.Cons (i, m) next_msgs0) + | betree.List.Nil => Result.ret ret0 /- [betree_main::betree::Node::{5}::apply_upserts] -/ divergent def betree.Node.apply_upserts_fwd - (msgs : betree_list_t (U64 × betree_message_t)) (prev : Option U64) - (key : U64) (st : State) : + (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64) + (st : State) : Result (State × U64) := do - let b ← betree.List.head_has_key_fwd betree_message_t msgs key + let b ← betree.List.head_has_key_fwd betree.Message msgs key if b then do - let msg ← betree.List.pop_front_fwd (U64 × betree_message_t) msgs + let msg ← betree.List.pop_front_fwd (U64 × betree.Message) msgs let (_, m) := msg 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 => + | betree.Message.Insert i => Result.fail Error.panic + | betree.Message.Delete => Result.fail Error.panic + | betree.Message.Upsert s => do let v ← betree.upsert_update_fwd prev s let msgs0 ← - betree.List.pop_front_back (U64 × betree_message_t) msgs + betree.List.pop_front_back (U64 × betree.Message) msgs betree.Node.apply_upserts_fwd msgs0 (Option.some v) key st else do let (st0, v) ← core.option.Option.unwrap_fwd U64 prev st let _ ← - betree.List.push_front_fwd_back (U64 × betree_message_t) msgs (key, - betree_message_t.Insert v) + betree.List.push_front_fwd_back (U64 × betree.Message) msgs (key, + betree.Message.Insert v) Result.ret (st0, v) /- [betree_main::betree::Node::{5}::apply_upserts] -/ divergent def betree.Node.apply_upserts_back - (msgs : betree_list_t (U64 × betree_message_t)) (prev : Option U64) - (key : U64) (st : State) : - Result (betree_list_t (U64 × betree_message_t)) + (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64) + (st : State) : + Result (betree.List (U64 × betree.Message)) := do - let b ← betree.List.head_has_key_fwd betree_message_t msgs key + let b ← betree.List.head_has_key_fwd betree.Message msgs key if b then do - let msg ← betree.List.pop_front_fwd (U64 × betree_message_t) msgs + let msg ← betree.List.pop_front_fwd (U64 × betree.Message) msgs let (_, m) := msg 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 => + | betree.Message.Insert i => Result.fail Error.panic + | betree.Message.Delete => Result.fail Error.panic + | betree.Message.Upsert s => do let v ← betree.upsert_update_fwd prev s let msgs0 ← - betree.List.pop_front_back (U64 × betree_message_t) msgs + betree.List.pop_front_back (U64 × betree.Message) msgs betree.Node.apply_upserts_back msgs0 (Option.some v) key st else do let (_, v) ← core.option.Option.unwrap_fwd U64 prev st - betree.List.push_front_fwd_back (U64 × betree_message_t) msgs (key, - betree_message_t.Insert v) + betree.List.push_front_fwd_back (U64 × betree.Message) msgs (key, + betree.Message.Insert v) /- [betree_main::betree::Node::{5}::lookup] -/ mutual divergent def betree.Node.lookup_fwd - (self : betree_node_t) (key : U64) (st : State) : + (self : betree.Node) (key : U64) (st : State) : Result (State × (Option U64)) := match self with - | betree_node_t.Internal node => + | betree.Node.Internal node => do 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 pending with - | betree_list_t.Cons p l => + | betree.List.Cons p l => let (k, msg) := p if k != key then do let (st1, opt) ← - betree.Internal.lookup_in_children_fwd (betree_internal_t.mk i i0 - n n0) key st0 + betree.Internal.lookup_in_children_fwd (betree.Internal.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) + (betree.List.Cons (k, msg) l) Result.ret (st1, opt) else match msg with - | betree_message_t.Insert v => + | betree.Message.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) + (betree.List.Cons (k, betree.Message.Insert v) l) Result.ret (st0, Option.some v) - | betree_message_t.Delete => + | betree.Message.Delete => do let _ ← betree.Node.lookup_first_message_for_key_back key msgs - (betree_list_t.Cons (k, betree_message_t.Delete) l) + (betree.List.Cons (k, betree.Message.Delete) l) Result.ret (st0, Option.none) - | betree_message_t.Upsert ufs => + | betree.Message.Upsert ufs => do let (st1, v) ← - betree.Internal.lookup_in_children_fwd (betree_internal_t.mk i - i0 n n0) key st0 + betree.Internal.lookup_in_children_fwd (betree.Internal.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 + betree.Node.apply_upserts_fwd (betree.List.Cons (k, + betree.Message.Upsert ufs) l) v key st1 let node0 ← - betree.Internal.lookup_in_children_back (betree_internal_t.mk i + betree.Internal.lookup_in_children_back (betree.Internal.mk i i0 n n0) key st0 let ⟨ i1, _, _, _ ⟩ := node0 let pending0 ← - betree.Node.apply_upserts_back (betree_list_t.Cons (k, - betree_message_t.Upsert ufs) l) v key st1 + betree.Node.apply_upserts_back (betree.List.Cons (k, + betree.Message.Upsert ufs) l) v key st1 let msgs0 ← betree.Node.lookup_first_message_for_key_back key msgs pending0 let (st3, _) ← betree.store_internal_node_fwd i1 msgs0 st2 Result.ret (st3, Option.some v0) - | betree_list_t.Nil => + | betree.List.Nil => do let (st1, opt) ← - betree.Internal.lookup_in_children_fwd (betree_internal_t.mk i i0 n + betree.Internal.lookup_in_children_fwd (betree.Internal.mk i i0 n n0) key st0 let _ ← betree.Node.lookup_first_message_for_key_back key msgs - betree_list_t.Nil + betree.List.Nil Result.ret (st1, opt) - | betree_node_t.Leaf node => + | betree.Node.Leaf node => do let (st0, bindings) ← betree.load_leaf_node_fwd node.betree_leaf_id st let opt ← betree.Node.lookup_in_bindings_fwd key bindings @@ -403,80 +401,78 @@ 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 := + (self : betree.Node) (key : U64) (st : State) : Result betree.Node := match self with - | betree_node_t.Internal node => + | betree.Node.Internal node => do 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 pending with - | betree_list_t.Cons p l => + | betree.List.Cons p l => let (k, msg) := p if k != key then do let _ ← betree.Node.lookup_first_message_for_key_back key msgs - (betree_list_t.Cons (k, msg) l) + (betree.List.Cons (k, msg) l) let node0 ← - betree.Internal.lookup_in_children_back (betree_internal_t.mk i - i0 n n0) key st0 - Result.ret (betree_node_t.Internal node0) + betree.Internal.lookup_in_children_back (betree.Internal.mk i i0 + n n0) key st0 + Result.ret (betree.Node.Internal node0) else match msg with - | betree_message_t.Insert v => + | betree.Message.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 (betree_internal_t.mk i i0 n - n0)) - | betree_message_t.Delete => + (betree.List.Cons (k, betree.Message.Insert v) l) + Result.ret (betree.Node.Internal (betree.Internal.mk i i0 n n0)) + | betree.Message.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 (betree_internal_t.mk i i0 n - n0)) - | betree_message_t.Upsert ufs => + (betree.List.Cons (k, betree.Message.Delete) l) + Result.ret (betree.Node.Internal (betree.Internal.mk i i0 n n0)) + | betree.Message.Upsert ufs => do let (st1, v) ← - betree.Internal.lookup_in_children_fwd (betree_internal_t.mk i - i0 n n0) key st0 + betree.Internal.lookup_in_children_fwd (betree.Internal.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 + betree.Node.apply_upserts_fwd (betree.List.Cons (k, + betree.Message.Upsert ufs) l) v key st1 let node0 ← - betree.Internal.lookup_in_children_back (betree_internal_t.mk i + betree.Internal.lookup_in_children_back (betree.Internal.mk i i0 n n0) key st0 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 + betree.Node.apply_upserts_back (betree.List.Cons (k, + betree.Message.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 (betree_internal_t.mk i1 i2 n1 + Result.ret (betree.Node.Internal (betree.Internal.mk i1 i2 n1 n2)) - | betree_list_t.Nil => + | betree.List.Nil => do let _ ← betree.Node.lookup_first_message_for_key_back key msgs - betree_list_t.Nil + betree.List.Nil let node0 ← - 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 => + betree.Internal.lookup_in_children_back (betree.Internal.mk i i0 n + n0) key st0 + Result.ret (betree.Node.Internal node0) + | betree.Node.Leaf node => do let (_, bindings) ← betree.load_leaf_node_fwd node.betree_leaf_id st let _ ← betree.Node.lookup_in_bindings_fwd key bindings - Result.ret (betree_node_t.Leaf node) + Result.ret (betree.Node.Leaf node) /- [betree_main::betree::Internal::{4}::lookup_in_children] -/ divergent def betree.Internal.lookup_in_children_fwd - (self : betree_internal_t) (key : U64) (st : State) : + (self : betree.Internal) (key : U64) (st : State) : Result (State × (Option U64)) := let ⟨ _, i, n, n0 ⟩ := self @@ -486,57 +482,55 @@ divergent def betree.Internal.lookup_in_children_fwd /- [betree_main::betree::Internal::{4}::lookup_in_children] -/ divergent def betree.Internal.lookup_in_children_back - (self : betree_internal_t) (key : U64) (st : State) : - Result betree_internal_t - := + (self : betree.Internal) (key : U64) (st : State) : Result betree.Internal := let ⟨ i, i0, n, n0 ⟩ := self if key < i0 then do let n1 ← betree.Node.lookup_back n key st - Result.ret (betree_internal_t.mk i i0 n1 n0) + Result.ret (betree.Internal.mk i i0 n1 n0) else do let n1 ← betree.Node.lookup_back n0 key st - Result.ret (betree_internal_t.mk i i0 n n1) + Result.ret (betree.Internal.mk i i0 n n1) end /- [betree_main::betree::Node::{5}::lookup_mut_in_bindings] -/ divergent def betree.Node.lookup_mut_in_bindings_fwd - (key : U64) (bindings : betree_list_t (U64 × U64)) : - Result (betree_list_t (U64 × U64)) + (key : U64) (bindings : betree.List (U64 × U64)) : + Result (betree.List (U64 × U64)) := match bindings with - | betree_list_t.Cons hd tl => + | betree.List.Cons hd tl => let (i, i0) := hd if i >= key - then Result.ret (betree_list_t.Cons (i, i0) tl) + then Result.ret (betree.List.Cons (i, i0) tl) else betree.Node.lookup_mut_in_bindings_fwd key tl - | betree_list_t.Nil => Result.ret betree_list_t.Nil + | betree.List.Nil => Result.ret betree.List.Nil /- [betree_main::betree::Node::{5}::lookup_mut_in_bindings] -/ divergent def betree.Node.lookup_mut_in_bindings_back - (key : U64) (bindings : betree_list_t (U64 × U64)) - (ret0 : betree_list_t (U64 × U64)) : - Result (betree_list_t (U64 × U64)) + (key : U64) (bindings : betree.List (U64 × U64)) + (ret0 : betree.List (U64 × U64)) : + Result (betree.List (U64 × U64)) := match bindings with - | betree_list_t.Cons hd tl => + | betree.List.Cons hd tl => let (i, i0) := hd if i >= key then Result.ret ret0 else do let tl0 ← betree.Node.lookup_mut_in_bindings_back key tl ret0 - Result.ret (betree_list_t.Cons (i, i0) tl0) - | betree_list_t.Nil => Result.ret ret0 + Result.ret (betree.List.Cons (i, i0) tl0) + | betree.List.Nil => Result.ret ret0 /- [betree_main::betree::Node::{5}::apply_to_leaf] -/ def betree.Node.apply_to_leaf_fwd_back - (bindings : betree_list_t (U64 × U64)) (key : U64) - (new_msg : betree_message_t) : - Result (betree_list_t (U64 × U64)) + (bindings : betree.List (U64 × U64)) (key : U64) (new_msg : betree.Message) + : + Result (betree.List (U64 × U64)) := do let bindings0 ← betree.Node.lookup_mut_in_bindings_fwd key bindings @@ -546,17 +540,17 @@ def betree.Node.apply_to_leaf_fwd_back do let hd ← betree.List.pop_front_fwd (U64 × U64) bindings0 match new_msg with - | betree_message_t.Insert v => + | betree.Message.Insert v => do let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0 let bindings2 ← betree.List.push_front_fwd_back (U64 × U64) bindings1 (key, v) betree.Node.lookup_mut_in_bindings_back key bindings bindings2 - | betree_message_t.Delete => + | betree.Message.Delete => do let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0 betree.Node.lookup_mut_in_bindings_back key bindings bindings1 - | betree_message_t.Upsert s => + | betree.Message.Upsert s => do let (_, i) := hd let v ← betree.upsert_update_fwd (Option.some i) s @@ -566,14 +560,14 @@ def betree.Node.apply_to_leaf_fwd_back betree.Node.lookup_mut_in_bindings_back key bindings bindings2 else match new_msg with - | betree_message_t.Insert v => + | betree.Message.Insert v => do let bindings1 ← betree.List.push_front_fwd_back (U64 × U64) bindings0 (key, v) betree.Node.lookup_mut_in_bindings_back key bindings bindings1 - | betree_message_t.Delete => + | betree.Message.Delete => betree.Node.lookup_mut_in_bindings_back key bindings bindings0 - | betree_message_t.Upsert s => + | betree.Message.Upsert s => do let v ← betree.upsert_update_fwd Option.none s let bindings1 ← @@ -582,170 +576,170 @@ def betree.Node.apply_to_leaf_fwd_back /- [betree_main::betree::Node::{5}::apply_messages_to_leaf] -/ divergent def betree.Node.apply_messages_to_leaf_fwd_back - (bindings : betree_list_t (U64 × U64)) - (new_msgs : betree_list_t (U64 × betree_message_t)) : - Result (betree_list_t (U64 × U64)) + (bindings : betree.List (U64 × U64)) + (new_msgs : betree.List (U64 × betree.Message)) : + Result (betree.List (U64 × U64)) := match new_msgs with - | betree_list_t.Cons new_msg new_msgs_tl => + | betree.List.Cons new_msg new_msgs_tl => do let (i, m) := new_msg let bindings0 ← betree.Node.apply_to_leaf_fwd_back bindings i m betree.Node.apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl - | betree_list_t.Nil => Result.ret bindings + | betree.List.Nil => Result.ret bindings /- [betree_main::betree::Node::{5}::filter_messages_for_key] -/ 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)) + (key : U64) (msgs : betree.List (U64 × betree.Message)) : + Result (betree.List (U64 × betree.Message)) := match msgs with - | betree_list_t.Cons p l => + | betree.List.Cons p l => let (k, m) := p if k = key then do let msgs0 ← - betree.List.pop_front_back (U64 × betree_message_t) - (betree_list_t.Cons (k, m) l) + betree.List.pop_front_back (U64 × betree.Message) (betree.List.Cons + (k, m) l) betree.Node.filter_messages_for_key_fwd_back key msgs0 - else Result.ret (betree_list_t.Cons (k, m) l) - | betree_list_t.Nil => Result.ret betree_list_t.Nil + else Result.ret (betree.List.Cons (k, m) l) + | betree.List.Nil => Result.ret betree.List.Nil /- [betree_main::betree::Node::{5}::lookup_first_message_after_key] -/ 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)) + (key : U64) (msgs : betree.List (U64 × betree.Message)) : + Result (betree.List (U64 × betree.Message)) := match msgs with - | betree_list_t.Cons p next_msgs => + | betree.List.Cons p next_msgs => let (k, m) := p if k = key then betree.Node.lookup_first_message_after_key_fwd key next_msgs - else Result.ret (betree_list_t.Cons (k, m) next_msgs) - | betree_list_t.Nil => Result.ret betree_list_t.Nil + else Result.ret (betree.List.Cons (k, m) next_msgs) + | betree.List.Nil => Result.ret betree.List.Nil /- [betree_main::betree::Node::{5}::lookup_first_message_after_key] -/ divergent def betree.Node.lookup_first_message_after_key_back - (key : U64) (msgs : betree_list_t (U64 × betree_message_t)) - (ret0 : betree_list_t (U64 × betree_message_t)) : - Result (betree_list_t (U64 × betree_message_t)) + (key : U64) (msgs : betree.List (U64 × betree.Message)) + (ret0 : betree.List (U64 × betree.Message)) : + Result (betree.List (U64 × betree.Message)) := match msgs with - | betree_list_t.Cons p next_msgs => + | betree.List.Cons p next_msgs => let (k, m) := p if k = key then do let next_msgs0 ← betree.Node.lookup_first_message_after_key_back key next_msgs ret0 - Result.ret (betree_list_t.Cons (k, m) next_msgs0) + Result.ret (betree.List.Cons (k, m) next_msgs0) else Result.ret ret0 - | betree_list_t.Nil => Result.ret ret0 + | betree.List.Nil => Result.ret ret0 /- [betree_main::betree::Node::{5}::apply_to_internal] -/ def betree.Node.apply_to_internal_fwd_back - (msgs : betree_list_t (U64 × betree_message_t)) (key : U64) - (new_msg : betree_message_t) : - Result (betree_list_t (U64 × betree_message_t)) + (msgs : betree.List (U64 × betree.Message)) (key : U64) + (new_msg : betree.Message) : + Result (betree.List (U64 × betree.Message)) := do let msgs0 ← betree.Node.lookup_first_message_for_key_fwd key msgs - let b ← betree.List.head_has_key_fwd betree_message_t msgs0 key + let b ← betree.List.head_has_key_fwd betree.Message msgs0 key if b then match new_msg with - | betree_message_t.Insert i => + | betree.Message.Insert i => do let msgs1 ← betree.Node.filter_messages_for_key_fwd_back key msgs0 let msgs2 ← - betree.List.push_front_fwd_back (U64 × betree_message_t) msgs1 - (key, betree_message_t.Insert i) + betree.List.push_front_fwd_back (U64 × betree.Message) msgs1 (key, + betree.Message.Insert i) betree.Node.lookup_first_message_for_key_back key msgs msgs2 - | betree_message_t.Delete => + | betree.Message.Delete => do let msgs1 ← betree.Node.filter_messages_for_key_fwd_back key msgs0 let msgs2 ← - betree.List.push_front_fwd_back (U64 × betree_message_t) msgs1 - (key, betree_message_t.Delete) + betree.List.push_front_fwd_back (U64 × betree.Message) msgs1 (key, + betree.Message.Delete) betree.Node.lookup_first_message_for_key_back key msgs msgs2 - | betree_message_t.Upsert s => + | betree.Message.Upsert s => do - let p ← betree.List.hd_fwd (U64 × betree_message_t) msgs0 + let p ← betree.List.hd_fwd (U64 × betree.Message) msgs0 let (_, m) := p match m with - | betree_message_t.Insert prev => + | betree.Message.Insert prev => do let v ← betree.upsert_update_fwd (Option.some prev) s let msgs1 ← - betree.List.pop_front_back (U64 × betree_message_t) msgs0 + betree.List.pop_front_back (U64 × betree.Message) msgs0 let msgs2 ← - betree.List.push_front_fwd_back (U64 × betree_message_t) msgs1 - (key, betree_message_t.Insert v) + betree.List.push_front_fwd_back (U64 × betree.Message) msgs1 + (key, betree.Message.Insert v) betree.Node.lookup_first_message_for_key_back key msgs msgs2 - | betree_message_t.Delete => + | betree.Message.Delete => do let v ← betree.upsert_update_fwd Option.none s let msgs1 ← - betree.List.pop_front_back (U64 × betree_message_t) msgs0 + betree.List.pop_front_back (U64 × betree.Message) msgs0 let msgs2 ← - betree.List.push_front_fwd_back (U64 × betree_message_t) msgs1 - (key, betree_message_t.Insert v) + betree.List.push_front_fwd_back (U64 × betree.Message) msgs1 + (key, betree.Message.Insert v) betree.Node.lookup_first_message_for_key_back key msgs msgs2 - | betree_message_t.Upsert ufs => + | betree.Message.Upsert ufs => do let msgs1 ← betree.Node.lookup_first_message_after_key_fwd key msgs0 let msgs2 ← - betree.List.push_front_fwd_back (U64 × betree_message_t) msgs1 - (key, betree_message_t.Upsert s) + betree.List.push_front_fwd_back (U64 × betree.Message) msgs1 + (key, betree.Message.Upsert s) let msgs3 ← betree.Node.lookup_first_message_after_key_back key msgs0 msgs2 betree.Node.lookup_first_message_for_key_back key msgs msgs3 else do let msgs1 ← - betree.List.push_front_fwd_back (U64 × betree_message_t) msgs0 (key, + betree.List.push_front_fwd_back (U64 × betree.Message) msgs0 (key, new_msg) betree.Node.lookup_first_message_for_key_back key msgs msgs1 /- [betree_main::betree::Node::{5}::apply_messages_to_internal] -/ divergent def betree.Node.apply_messages_to_internal_fwd_back - (msgs : betree_list_t (U64 × betree_message_t)) - (new_msgs : betree_list_t (U64 × betree_message_t)) : - Result (betree_list_t (U64 × betree_message_t)) + (msgs : betree.List (U64 × betree.Message)) + (new_msgs : betree.List (U64 × betree.Message)) : + Result (betree.List (U64 × betree.Message)) := match new_msgs with - | betree_list_t.Cons new_msg new_msgs_tl => + | betree.List.Cons new_msg new_msgs_tl => do let (i, m) := new_msg let msgs0 ← betree.Node.apply_to_internal_fwd_back msgs i m betree.Node.apply_messages_to_internal_fwd_back msgs0 new_msgs_tl - | betree_list_t.Nil => Result.ret msgs + | betree.List.Nil => Result.ret msgs /- [betree_main::betree::Node::{5}::apply_messages] -/ mutual divergent def betree.Node.apply_messages_fwd - (self : betree_node_t) (params : betree_params_t) - (node_id_cnt : betree_node_id_counter_t) - (msgs : betree_list_t (U64 × betree_message_t)) (st : State) : + (self : betree.Node) (params : betree.Params) + (node_id_cnt : betree.NodeIdCounter) + (msgs : betree.List (U64 × betree.Message)) (st : State) : Result (State × Unit) := match self with - | betree_node_t.Internal node => + | betree.Node.Internal node => do 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 - let num_msgs ← betree.List.len_fwd (U64 × betree_message_t) content0 + let num_msgs ← betree.List.len_fwd (U64 × betree.Message) content0 if num_msgs >= params.betree_params_min_flush_size then do let (st1, content1) ← - betree.Internal.flush_fwd (betree_internal_t.mk i i0 n n0) params + betree.Internal.flush_fwd (betree.Internal.mk i i0 n n0) params node_id_cnt content0 st0 let (node0, _) ← - betree.Internal.flush_back (betree_internal_t.mk i i0 n n0) params + betree.Internal.flush_back (betree.Internal.mk i i0 n n0) params node_id_cnt content0 st0 let ⟨ i1, _, _, _ ⟩ := node0 let (st2, _) ← betree.store_internal_node_fwd i1 content1 st1 @@ -754,7 +748,7 @@ mutual divergent def betree.Node.apply_messages_fwd do let (st1, _) ← betree.store_internal_node_fwd i content0 st0 Result.ret (st1, ()) - | betree_node_t.Leaf node => + | betree.Node.Leaf node => do let (st0, content) ← betree.load_leaf_node_fwd node.betree_leaf_id st let content0 ← betree.Node.apply_messages_to_leaf_fwd_back content msgs @@ -766,8 +760,7 @@ mutual divergent def betree.Node.apply_messages_fwd let (st1, _) ← betree.Leaf.split_fwd node content0 params node_id_cnt st0 let (st2, _) ← - betree.store_leaf_node_fwd node.betree_leaf_id betree_list_t.Nil - st1 + betree.store_leaf_node_fwd node.betree_leaf_id betree.List.Nil st1 Result.ret (st2, ()) else do @@ -777,38 +770,38 @@ mutual divergent def betree.Node.apply_messages_fwd /- [betree_main::betree::Node::{5}::apply_messages] -/ divergent def betree.Node.apply_messages_back - (self : betree_node_t) (params : betree_params_t) - (node_id_cnt : betree_node_id_counter_t) - (msgs : betree_list_t (U64 × betree_message_t)) (st : State) : - Result (betree_node_t × betree_node_id_counter_t) + (self : betree.Node) (params : betree.Params) + (node_id_cnt : betree.NodeIdCounter) + (msgs : betree.List (U64 × betree.Message)) (st : State) : + Result (betree.Node × betree.NodeIdCounter) := match self with - | betree_node_t.Internal node => + | betree.Node.Internal node => do 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 - let num_msgs ← betree.List.len_fwd (U64 × betree_message_t) content0 + let num_msgs ← betree.List.len_fwd (U64 × betree.Message) content0 if num_msgs >= params.betree_params_min_flush_size then do let (st1, content1) ← - betree.Internal.flush_fwd (betree_internal_t.mk i i0 n n0) params + betree.Internal.flush_fwd (betree.Internal.mk i i0 n n0) params node_id_cnt content0 st0 let (node0, node_id_cnt0) ← - betree.Internal.flush_back (betree_internal_t.mk i i0 n n0) params + betree.Internal.flush_back (betree.Internal.mk i i0 n n0) params node_id_cnt content0 st0 let ⟨ i1, i2, n1, n2 ⟩ := node0 let _ ← betree.store_internal_node_fwd i1 content1 st1 - Result.ret (betree_node_t.Internal (betree_internal_t.mk i1 i2 n1 - n2), node_id_cnt0) + Result.ret (betree.Node.Internal (betree.Internal.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 (betree_internal_t.mk i i0 n n0), + Result.ret (betree.Node.Internal (betree.Internal.mk i i0 n n0), node_id_cnt) - | betree_node_t.Leaf node => + | betree.Node.Leaf node => do let (st0, content) ← betree.load_leaf_node_fwd node.betree_leaf_id st let content0 ← betree.Node.apply_messages_to_leaf_fwd_back content msgs @@ -820,29 +813,28 @@ divergent def betree.Node.apply_messages_back let (st1, new_node) ← betree.Leaf.split_fwd node content0 params node_id_cnt st0 let _ ← - betree.store_leaf_node_fwd node.betree_leaf_id betree_list_t.Nil - st1 + betree.store_leaf_node_fwd node.betree_leaf_id betree.List.Nil st1 let node_id_cnt0 ← betree.Leaf.split_back node content0 params node_id_cnt st0 - Result.ret (betree_node_t.Internal new_node, node_id_cnt0) + Result.ret (betree.Node.Internal new_node, node_id_cnt0) else do let _ ← betree.store_leaf_node_fwd node.betree_leaf_id content0 st0 - Result.ret (betree_node_t.Leaf { node with betree_leaf_size := len }, + Result.ret (betree.Node.Leaf { node with betree_leaf_size := len }, node_id_cnt) /- [betree_main::betree::Internal::{4}::flush] -/ divergent def betree.Internal.flush_fwd - (self : betree_internal_t) (params : betree_params_t) - (node_id_cnt : betree_node_id_counter_t) - (content : betree_list_t (U64 × betree_message_t)) (st : State) : - Result (State × (betree_list_t (U64 × betree_message_t))) + (self : betree.Internal) (params : betree.Params) + (node_id_cnt : betree.NodeIdCounter) + (content : betree.List (U64 × betree.Message)) (st : State) : + Result (State × (betree.List (U64 × betree.Message))) := do let ⟨ _, i, n, n0 ⟩ := self - let p ← betree.List.partition_at_pivot_fwd betree_message_t content i + let p ← betree.List.partition_at_pivot_fwd betree.Message content i let (msgs_left, msgs_right) := p - let len_left ← betree.List.len_fwd (U64 × betree_message_t) msgs_left + let len_left ← betree.List.len_fwd (U64 × betree.Message) msgs_left if len_left >= params.betree_params_min_flush_size then do @@ -851,7 +843,7 @@ divergent def betree.Internal.flush_fwd let (_, node_id_cnt0) ← betree.Node.apply_messages_back n params node_id_cnt msgs_left st let len_right ← - betree.List.len_fwd (U64 × betree_message_t) msgs_right + betree.List.len_fwd (U64 × betree.Message) msgs_right if len_right >= params.betree_params_min_flush_size then do @@ -861,7 +853,7 @@ divergent def betree.Internal.flush_fwd let _ ← betree.Node.apply_messages_back n0 params node_id_cnt0 msgs_right st0 - Result.ret (st1, betree_list_t.Nil) + Result.ret (st1, betree.List.Nil) else Result.ret (st0, msgs_right) else do @@ -873,16 +865,16 @@ divergent def betree.Internal.flush_fwd /- [betree_main::betree::Internal::{4}::flush] -/ divergent def betree.Internal.flush_back - (self : betree_internal_t) (params : betree_params_t) - (node_id_cnt : betree_node_id_counter_t) - (content : betree_list_t (U64 × betree_message_t)) (st : State) : - Result (betree_internal_t × betree_node_id_counter_t) + (self : betree.Internal) (params : betree.Params) + (node_id_cnt : betree.NodeIdCounter) + (content : betree.List (U64 × betree.Message)) (st : State) : + Result (betree.Internal × betree.NodeIdCounter) := do let ⟨ i, i0, n, n0 ⟩ := self - let p ← betree.List.partition_at_pivot_fwd betree_message_t content i0 + let p ← betree.List.partition_at_pivot_fwd betree.Message content i0 let (msgs_left, msgs_right) := p - let len_left ← betree.List.len_fwd (U64 × betree_message_t) msgs_left + let len_left ← betree.List.len_fwd (U64 × betree.Message) msgs_left if len_left >= params.betree_params_min_flush_size then do @@ -891,60 +883,60 @@ divergent def betree.Internal.flush_back let (n1, node_id_cnt0) ← betree.Node.apply_messages_back n params node_id_cnt msgs_left st let len_right ← - betree.List.len_fwd (U64 × betree_message_t) msgs_right + betree.List.len_fwd (U64 × betree.Message) msgs_right if len_right >= params.betree_params_min_flush_size then do let (n2, node_id_cnt1) ← betree.Node.apply_messages_back n0 params node_id_cnt0 msgs_right st0 - 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) + Result.ret (betree.Internal.mk i i0 n1 n2, node_id_cnt1) + else Result.ret (betree.Internal.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 (betree_internal_t.mk i i0 n n1, node_id_cnt0) + Result.ret (betree.Internal.mk i i0 n n1, node_id_cnt0) end /- [betree_main::betree::Node::{5}::apply] -/ def betree.Node.apply_fwd - (self : betree_node_t) (params : betree_params_t) - (node_id_cnt : betree_node_id_counter_t) (key : U64) - (new_msg : betree_message_t) (st : State) : + (self : betree.Node) (params : betree.Params) + (node_id_cnt : betree.NodeIdCounter) (key : U64) (new_msg : betree.Message) + (st : State) : Result (State × Unit) := do - let l := betree_list_t.Nil + let l := betree.List.Nil let (st0, _) ← - betree.Node.apply_messages_fwd self params node_id_cnt - (betree_list_t.Cons (key, new_msg) l) st + betree.Node.apply_messages_fwd self params node_id_cnt (betree.List.Cons + (key, new_msg) l) st let _ ← - betree.Node.apply_messages_back self params node_id_cnt - (betree_list_t.Cons (key, new_msg) l) st + betree.Node.apply_messages_back self params node_id_cnt (betree.List.Cons + (key, new_msg) l) st Result.ret (st0, ()) /- [betree_main::betree::Node::{5}::apply] -/ def betree.Node.apply_back - (self : betree_node_t) (params : betree_params_t) - (node_id_cnt : betree_node_id_counter_t) (key : U64) - (new_msg : betree_message_t) (st : State) : - Result (betree_node_t × betree_node_id_counter_t) + (self : betree.Node) (params : betree.Params) + (node_id_cnt : betree.NodeIdCounter) (key : U64) (new_msg : betree.Message) + (st : State) : + Result (betree.Node × betree.NodeIdCounter) := - let l := betree_list_t.Nil - betree.Node.apply_messages_back self params node_id_cnt (betree_list_t.Cons + let l := betree.List.Nil + betree.Node.apply_messages_back self params node_id_cnt (betree.List.Cons (key, new_msg) l) st /- [betree_main::betree::BeTree::{6}::new] -/ def betree.BeTree.new_fwd (min_flush_size : U64) (split_size : U64) (st : State) : - Result (State × betree_be_tree_t) + Result (State × betree.BeTree) := do let node_id_cnt ← betree.NodeIdCounter.new_fwd let id ← betree.NodeIdCounter.fresh_id_fwd node_id_cnt - let (st0, _) ← betree.store_leaf_node_fwd id betree_list_t.Nil st + let (st0, _) ← betree.store_leaf_node_fwd id betree.List.Nil st let node_id_cnt0 ← betree.NodeIdCounter.fresh_id_back node_id_cnt Result.ret (st0, { @@ -955,7 +947,7 @@ def betree.BeTree.new_fwd }, betree_be_tree_node_id_cnt := node_id_cnt0, betree_be_tree_root := - (betree_node_t.Leaf + (betree.Node.Leaf { betree_leaf_id := id, betree_leaf_size := (U64.ofInt 0 (by intlit)) @@ -964,7 +956,7 @@ def betree.BeTree.new_fwd /- [betree_main::betree::BeTree::{6}::apply] -/ def betree.BeTree.apply_fwd - (self : betree_be_tree_t) (key : U64) (msg : betree_message_t) (st : State) : + (self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) : Result (State × Unit) := do @@ -978,8 +970,8 @@ def betree.BeTree.apply_fwd /- [betree_main::betree::BeTree::{6}::apply] -/ def betree.BeTree.apply_back - (self : betree_be_tree_t) (key : U64) (msg : betree_message_t) (st : State) : - Result betree_be_tree_t + (self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) : + Result betree.BeTree := do let (n, nic) ← @@ -990,74 +982,66 @@ def betree.BeTree.apply_back /- [betree_main::betree::BeTree::{6}::insert] -/ def betree.BeTree.insert_fwd - (self : betree_be_tree_t) (key : U64) (value : U64) (st : State) : + (self : betree.BeTree) (key : U64) (value : U64) (st : State) : Result (State × Unit) := do let (st0, _) ← - betree.BeTree.apply_fwd self key (betree_message_t.Insert value) st + betree.BeTree.apply_fwd self key (betree.Message.Insert value) st let _ ← - betree.BeTree.apply_back self key (betree_message_t.Insert value) st + betree.BeTree.apply_back self key (betree.Message.Insert value) st Result.ret (st0, ()) /- [betree_main::betree::BeTree::{6}::insert] -/ def betree.BeTree.insert_back - (self : betree_be_tree_t) (key : U64) (value : U64) (st : State) : - Result betree_be_tree_t + (self : betree.BeTree) (key : U64) (value : U64) (st : State) : + Result betree.BeTree := - betree.BeTree.apply_back self key (betree_message_t.Insert value) st + betree.BeTree.apply_back self key (betree.Message.Insert value) st /- [betree_main::betree::BeTree::{6}::delete] -/ def betree.BeTree.delete_fwd - (self : betree_be_tree_t) (key : U64) (st : State) : - Result (State × Unit) - := + (self : betree.BeTree) (key : U64) (st : State) : Result (State × Unit) := do - let (st0, _) ← - betree.BeTree.apply_fwd self key betree_message_t.Delete st - let _ ← betree.BeTree.apply_back self key betree_message_t.Delete st + let (st0, _) ← betree.BeTree.apply_fwd self key betree.Message.Delete st + let _ ← betree.BeTree.apply_back self key betree.Message.Delete st Result.ret (st0, ()) /- [betree_main::betree::BeTree::{6}::delete] -/ def betree.BeTree.delete_back - (self : betree_be_tree_t) (key : U64) (st : State) : - Result betree_be_tree_t - := - betree.BeTree.apply_back self key betree_message_t.Delete st + (self : betree.BeTree) (key : U64) (st : State) : Result betree.BeTree := + betree.BeTree.apply_back self key betree.Message.Delete st /- [betree_main::betree::BeTree::{6}::upsert] -/ def betree.BeTree.upsert_fwd - (self : betree_be_tree_t) (key : U64) (upd : betree_upsert_fun_state_t) - (st : State) : + (self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State) + : Result (State × Unit) := do let (st0, _) ← - betree.BeTree.apply_fwd self key (betree_message_t.Upsert upd) st - let _ ← - betree.BeTree.apply_back self key (betree_message_t.Upsert upd) st + betree.BeTree.apply_fwd self key (betree.Message.Upsert upd) st + let _ ← betree.BeTree.apply_back self key (betree.Message.Upsert upd) st Result.ret (st0, ()) /- [betree_main::betree::BeTree::{6}::upsert] -/ def betree.BeTree.upsert_back - (self : betree_be_tree_t) (key : U64) (upd : betree_upsert_fun_state_t) - (st : State) : - Result betree_be_tree_t + (self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State) + : + Result betree.BeTree := - betree.BeTree.apply_back self key (betree_message_t.Upsert upd) st + betree.BeTree.apply_back self key (betree.Message.Upsert upd) st /- [betree_main::betree::BeTree::{6}::lookup] -/ def betree.BeTree.lookup_fwd - (self : betree_be_tree_t) (key : U64) (st : State) : + (self : betree.BeTree) (key : U64) (st : State) : Result (State × (Option U64)) := betree.Node.lookup_fwd self.betree_be_tree_root key st /- [betree_main::betree::BeTree::{6}::lookup] -/ def betree.BeTree.lookup_back - (self : betree_be_tree_t) (key : U64) (st : State) : - Result betree_be_tree_t - := + (self : betree.BeTree) (key : U64) (st : State) : Result betree.BeTree := do let n ← betree.Node.lookup_back self.betree_be_tree_root key st Result.ret { self with betree_be_tree_root := n } diff --git a/tests/lean/BetreeMain/FunsExternal.lean b/tests/lean/BetreeMain/FunsExternal.lean index 0c715ef9..7bcba380 100644 --- a/tests/lean/BetreeMain/FunsExternal.lean +++ b/tests/lean/BetreeMain/FunsExternal.lean @@ -9,24 +9,24 @@ open betree_main /- [betree_main::betree_utils::load_internal_node] -/ def betree_utils.load_internal_node_fwd : - U64 → State → Result (State × (betree_list_t (U64 × betree_message_t))) := + U64 → State → Result (State × (betree.List (U64 × betree.Message))) := fun _ _ => .fail .panic /- [betree_main::betree_utils::store_internal_node] -/ def betree_utils.store_internal_node_fwd : - U64 → betree_list_t (U64 × betree_message_t) → State → Result (State + U64 → betree.List (U64 × betree.Message) → State → Result (State × Unit) := fun _ _ _ => .fail .panic /- [betree_main::betree_utils::load_leaf_node] -/ def betree_utils.load_leaf_node_fwd - : U64 → State → Result (State × (betree_list_t (U64 × U64))) := + : U64 → State → Result (State × (betree.List (U64 × U64))) := fun _ _ => .fail .panic /- [betree_main::betree_utils::store_leaf_node] -/ def betree_utils.store_leaf_node_fwd - : U64 → betree_list_t (U64 × U64) → State → Result (State × Unit) := + : U64 → betree.List (U64 × U64) → State → Result (State × Unit) := fun _ _ _ => .fail .panic /- [core::option::Option::{0}::unwrap] -/ diff --git a/tests/lean/BetreeMain/FunsExternal_Template.lean b/tests/lean/BetreeMain/FunsExternal_Template.lean index 9b5a54e5..d768bb20 100644 --- a/tests/lean/BetreeMain/FunsExternal_Template.lean +++ b/tests/lean/BetreeMain/FunsExternal_Template.lean @@ -8,22 +8,21 @@ open betree_main /- [betree_main::betree_utils::load_internal_node] -/ axiom betree_utils.load_internal_node_fwd - : - U64 → State → Result (State × (betree_list_t (U64 × betree_message_t))) + : U64 → State → Result (State × (betree.List (U64 × betree.Message))) /- [betree_main::betree_utils::store_internal_node] -/ axiom betree_utils.store_internal_node_fwd : - U64 → betree_list_t (U64 × betree_message_t) → State → Result (State - × Unit) + U64 → betree.List (U64 × betree.Message) → State → Result (State × + Unit) /- [betree_main::betree_utils::load_leaf_node] -/ axiom betree_utils.load_leaf_node_fwd - : U64 → State → Result (State × (betree_list_t (U64 × U64))) + : U64 → State → Result (State × (betree.List (U64 × U64))) /- [betree_main::betree_utils::store_leaf_node] -/ axiom betree_utils.store_leaf_node_fwd - : U64 → betree_list_t (U64 × U64) → State → Result (State × Unit) + : U64 → betree.List (U64 × U64) → State → Result (State × Unit) /- [core::option::Option::{0}::unwrap] -/ axiom core.option.Option.unwrap_fwd diff --git a/tests/lean/BetreeMain/Types.lean b/tests/lean/BetreeMain/Types.lean index 3ecbd668..afbdac9a 100644 --- a/tests/lean/BetreeMain/Types.lean +++ b/tests/lean/BetreeMain/Types.lean @@ -5,53 +5,53 @@ open Primitives namespace betree_main /- [betree_main::betree::List] -/ -inductive betree_list_t (T : Type) := -| Cons : T → betree_list_t T → betree_list_t T -| Nil : betree_list_t T +inductive betree.List (T : Type) := +| Cons : T → betree.List T → betree.List T +| Nil : betree.List 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 +inductive betree.UpsertFunState := +| Add : U64 → betree.UpsertFunState +| Sub : U64 → betree.UpsertFunState /- [betree_main::betree::Message] -/ -inductive betree_message_t := -| Insert : U64 → betree_message_t -| Delete : betree_message_t -| Upsert : betree_upsert_fun_state_t → betree_message_t +inductive betree.Message := +| Insert : U64 → betree.Message +| Delete : betree.Message +| Upsert : betree.UpsertFunState → betree.Message /- [betree_main::betree::Leaf] -/ -structure betree_leaf_t where +structure betree.Leaf where betree_leaf_id : U64 betree_leaf_size : U64 mutual /- [betree_main::betree::Node] -/ -inductive betree_node_t := -| Internal : betree_internal_t → betree_node_t -| Leaf : betree_leaf_t → betree_node_t +inductive betree.Node := +| Internal : betree.Internal → betree.Node +| Leaf : betree.Leaf → betree.Node /- [betree_main::betree::Internal] -/ -inductive betree_internal_t := -| mk : U64 → U64 → betree_node_t → betree_node_t → betree_internal_t +inductive betree.Internal := +| mk : U64 → U64 → betree.Node → betree.Node → betree.Internal end /- [betree_main::betree::Params] -/ -structure betree_params_t where +structure betree.Params where betree_params_min_flush_size : U64 betree_params_split_size : U64 /- [betree_main::betree::NodeIdCounter] -/ -structure betree_node_id_counter_t where +structure betree.NodeIdCounter where betree_node_id_counter_next_node_id : U64 /- [betree_main::betree::BeTree] -/ -structure betree_be_tree_t where - betree_be_tree_params : betree_params_t - betree_be_tree_node_id_cnt : betree_node_id_counter_t - betree_be_tree_root : betree_node_t +structure betree.BeTree where + betree_be_tree_params : betree.Params + betree_be_tree_node_id_cnt : betree.NodeIdCounter + betree_be_tree_root : betree.Node /- The state type used in the state-error monad -/ axiom State : Type diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean index 39c270be..7014b0d8 100644 --- a/tests/lean/Constants.lean +++ b/tests/lean/Constants.lean @@ -34,12 +34,12 @@ def mk_pair0_fwd (x : U32) (y : U32) : Result (U32 × U32) := Result.ret (x, y) /- [constants::Pair] -/ -structure pair_t (T1 T2 : Type) where +structure Pair (T1 T2 : Type) where pair_x : T1 pair_y : T2 /- [constants::mk_pair1] -/ -def mk_pair1_fwd (x : U32) (y : U32) : Result (pair_t U32 U32) := +def mk_pair1_fwd (x : U32) (y : U32) : Result (Pair U32 U32) := Result.ret { pair_x := x, pair_y := y } /- [constants::P0] -/ @@ -48,9 +48,9 @@ def p0_body : Result (U32 × U32) := def p0_c : (U32 × U32) := eval_global p0_body (by simp) /- [constants::P1] -/ -def p1_body : Result (pair_t U32 U32) := +def p1_body : Result (Pair U32 U32) := mk_pair1_fwd (U32.ofInt 0 (by intlit)) (U32.ofInt 1 (by intlit)) -def p1_c : pair_t U32 U32 := eval_global p1_body (by simp) +def p1_c : Pair U32 U32 := eval_global p1_body (by simp) /- [constants::P2] -/ def p2_body : Result (U32 × U32) := @@ -58,22 +58,22 @@ def p2_body : Result (U32 × U32) := def p2_c : (U32 × U32) := eval_global p2_body (by simp) /- [constants::P3] -/ -def p3_body : Result (pair_t U32 U32) := +def p3_body : Result (Pair U32 U32) := Result.ret { pair_x := (U32.ofInt 0 (by intlit)), pair_y := (U32.ofInt 1 (by intlit)) } -def p3_c : pair_t U32 U32 := eval_global p3_body (by simp) +def p3_c : Pair U32 U32 := eval_global p3_body (by simp) /- [constants::Wrap] -/ -structure wrap_t (T : Type) where +structure Wrap (T : Type) where wrap_val : T /- [constants::Wrap::{0}::new] -/ -def Wrap.new_fwd (T : Type) (val : T) : Result (wrap_t T) := +def Wrap.new_fwd (T : Type) (val : T) : Result (Wrap T) := Result.ret { wrap_val := val } /- [constants::Y] -/ -def y_body : Result (wrap_t I32) := Wrap.new_fwd I32 (I32.ofInt 2 (by intlit)) -def y_c : wrap_t I32 := eval_global y_body (by simp) +def y_body : Result (Wrap I32) := Wrap.new_fwd I32 (I32.ofInt 2 (by intlit)) +def y_c : Wrap I32 := eval_global y_body (by simp) /- [constants::unwrap_y] -/ def unwrap_y_fwd : Result I32 := @@ -123,12 +123,12 @@ def s2_body : Result U32 := incr_fwd s1_c def s2_c : U32 := eval_global s2_body (by simp) /- [constants::S3] -/ -def s3_body : Result (pair_t U32 U32) := Result.ret p3_c -def s3_c : pair_t U32 U32 := eval_global s3_body (by simp) +def s3_body : Result (Pair U32 U32) := Result.ret p3_c +def s3_c : Pair U32 U32 := eval_global s3_body (by simp) /- [constants::S4] -/ -def s4_body : Result (pair_t U32 U32) := +def s4_body : Result (Pair 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) +def s4_c : Pair U32 U32 := eval_global s4_body (by simp) end constants diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean index 6bfffc33..10efc3db 100644 --- a/tests/lean/External/Funs.lean +++ b/tests/lean/External/Funs.lean @@ -28,10 +28,10 @@ def swap_back /- [external::test_new_non_zero_u32] -/ def test_new_non_zero_u32_fwd - (x : U32) (st : State) : Result (State × core_num_nonzero_non_zero_u32_t) := + (x : U32) (st : State) : Result (State × core.num.nonzero.NonZeroU32) := do let (st0, opt) ← core.num.nonzero.NonZeroU32.new_fwd x st - core.option.Option.unwrap_fwd core_num_nonzero_non_zero_u32_t opt st0 + core.option.Option.unwrap_fwd core.num.nonzero.NonZeroU32 opt st0 /- [external::test_vec] -/ def test_vec_fwd : Result Unit := diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean index d6c0eb1d..669fe91b 100644 --- a/tests/lean/External/FunsExternal_Template.lean +++ b/tests/lean/External/FunsExternal_Template.lean @@ -20,8 +20,7 @@ axiom core.mem.swap_back1 /- [core::num::nonzero::NonZeroU32::{14}::new] -/ axiom core.num.nonzero.NonZeroU32.new_fwd - : - U32 → State → Result (State × (Option core_num_nonzero_non_zero_u32_t)) + : U32 → State → Result (State × (Option core.num.nonzero.NonZeroU32)) /- [core::option::Option::{0}::unwrap] -/ axiom core.option.Option.unwrap_fwd diff --git a/tests/lean/External/Types.lean b/tests/lean/External/Types.lean index 316f6474..ba984e2a 100644 --- a/tests/lean/External/Types.lean +++ b/tests/lean/External/Types.lean @@ -5,7 +5,7 @@ open Primitives namespace external /- [core::num::nonzero::NonZeroU32] -/ -axiom core_num_nonzero_non_zero_u32_t : Type +axiom core.num.nonzero.NonZeroU32 : Type /- The state type used in the state-error monad -/ axiom State : Type diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index 8f54eca8..4f16688b 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -11,28 +11,28 @@ def hash_key_fwd (k : Usize) : Result Usize := /- [hashmap::HashMap::{0}::allocate_slots] -/ divergent def HashMap.allocate_slots_loop_fwd - (T : Type) (slots : Vec (list_t T)) (n : Usize) : Result (Vec (list_t T)) := + (T : Type) (slots : Vec (List T)) (n : Usize) : Result (Vec (List T)) := if n > (Usize.ofInt 0 (by intlit)) then do - let slots0 ← vec_push_back (list_t T) slots list_t.Nil + let slots0 ← vec_push_back (List T) slots List.Nil let n0 ← n - (Usize.ofInt 1 (by intlit)) HashMap.allocate_slots_loop_fwd T slots0 n0 else Result.ret slots /- [hashmap::HashMap::{0}::allocate_slots] -/ def HashMap.allocate_slots_fwd - (T : Type) (slots : Vec (list_t T)) (n : Usize) : Result (Vec (list_t T)) := + (T : Type) (slots : Vec (List T)) (n : Usize) : Result (Vec (List T)) := HashMap.allocate_slots_loop_fwd T slots n /- [hashmap::HashMap::{0}::new_with_capacity] -/ def HashMap.new_with_capacity_fwd (T : Type) (capacity : Usize) (max_load_dividend : Usize) (max_load_divisor : Usize) : - Result (hash_map_t T) + Result (HashMap T) := do - let v := vec_new (list_t T) + let v := vec_new (List T) let slots ← HashMap.allocate_slots_fwd T v capacity let i ← capacity * max_load_dividend let i0 ← i / max_load_divisor @@ -45,25 +45,25 @@ def HashMap.new_with_capacity_fwd } /- [hashmap::HashMap::{0}::new] -/ -def HashMap.new_fwd (T : Type) : Result (hash_map_t T) := +def HashMap.new_fwd (T : Type) : Result (HashMap T) := HashMap.new_with_capacity_fwd T (Usize.ofInt 32 (by intlit)) (Usize.ofInt 4 (by intlit)) (Usize.ofInt 5 (by intlit)) /- [hashmap::HashMap::{0}::clear] -/ divergent def HashMap.clear_loop_fwd_back - (T : Type) (slots : Vec (list_t T)) (i : Usize) : Result (Vec (list_t T)) := - let i0 := vec_len (list_t T) slots + (T : Type) (slots : Vec (List T)) (i : Usize) : Result (Vec (List T)) := + let i0 := vec_len (List T) slots if i < i0 then do let i1 ← i + (Usize.ofInt 1 (by intlit)) - let slots0 ← vec_index_mut_back (list_t T) slots i list_t.Nil + let slots0 ← vec_index_mut_back (List T) slots i List.Nil HashMap.clear_loop_fwd_back T slots0 i1 else Result.ret slots /- [hashmap::HashMap::{0}::clear] -/ def HashMap.clear_fwd_back - (T : Type) (self : hash_map_t T) : Result (hash_map_t T) := + (T : Type) (self : HashMap T) : Result (HashMap T) := do let v ← HashMap.clear_loop_fwd_back T self.hash_map_slots @@ -77,66 +77,66 @@ def HashMap.clear_fwd_back } /- [hashmap::HashMap::{0}::len] -/ -def HashMap.len_fwd (T : Type) (self : hash_map_t T) : Result Usize := +def HashMap.len_fwd (T : Type) (self : HashMap T) : Result Usize := Result.ret self.hash_map_num_entries /- [hashmap::HashMap::{0}::insert_in_list] -/ divergent def HashMap.insert_in_list_loop_fwd - (T : Type) (key : Usize) (value : T) (ls : list_t T) : Result Bool := + (T : Type) (key : Usize) (value : T) (ls : List T) : Result Bool := match ls with - | list_t.Cons ckey cvalue tl => + | List.Cons ckey cvalue tl => if ckey = key then Result.ret false else HashMap.insert_in_list_loop_fwd T key value tl - | list_t.Nil => Result.ret true + | List.Nil => Result.ret true /- [hashmap::HashMap::{0}::insert_in_list] -/ def HashMap.insert_in_list_fwd - (T : Type) (key : Usize) (value : T) (ls : list_t T) : Result Bool := + (T : Type) (key : Usize) (value : T) (ls : List T) : Result Bool := HashMap.insert_in_list_loop_fwd T key value ls /- [hashmap::HashMap::{0}::insert_in_list] -/ divergent def HashMap.insert_in_list_loop_back - (T : Type) (key : Usize) (value : T) (ls : list_t T) : Result (list_t T) := + (T : Type) (key : Usize) (value : T) (ls : List T) : Result (List T) := match ls with - | list_t.Cons ckey cvalue tl => + | List.Cons ckey cvalue tl => if ckey = key - then Result.ret (list_t.Cons ckey value tl) + then Result.ret (List.Cons ckey value tl) else do let tl0 ← HashMap.insert_in_list_loop_back T key value tl - Result.ret (list_t.Cons ckey cvalue tl0) - | list_t.Nil => let l := list_t.Nil - Result.ret (list_t.Cons key value l) + Result.ret (List.Cons ckey cvalue tl0) + | List.Nil => let l := List.Nil + Result.ret (List.Cons key value l) /- [hashmap::HashMap::{0}::insert_in_list] -/ def HashMap.insert_in_list_back - (T : Type) (key : Usize) (value : T) (ls : list_t T) : Result (list_t T) := + (T : Type) (key : Usize) (value : T) (ls : List T) : Result (List T) := HashMap.insert_in_list_loop_back T key value ls /- [hashmap::HashMap::{0}::insert_no_resize] -/ def HashMap.insert_no_resize_fwd_back - (T : Type) (self : hash_map_t T) (key : Usize) (value : T) : - Result (hash_map_t T) + (T : Type) (self : HashMap T) (key : Usize) (value : T) : + Result (HashMap T) := do let hash ← hash_key_fwd key - let i := vec_len (list_t T) self.hash_map_slots + let i := vec_len (List T) self.hash_map_slots let hash_mod ← hash % i - let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod + let l ← vec_index_mut_fwd (List T) self.hash_map_slots hash_mod let inserted ← HashMap.insert_in_list_fwd T key value l if inserted then do let i0 ← self.hash_map_num_entries + (Usize.ofInt 1 (by intlit)) let l0 ← HashMap.insert_in_list_back T key value l - let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 + let v ← vec_index_mut_back (List T) self.hash_map_slots hash_mod l0 Result.ret { self with hash_map_num_entries := i0, hash_map_slots := v } else do let l0 ← HashMap.insert_in_list_back T key value l - let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 + let v ← vec_index_mut_back (List T) self.hash_map_slots hash_mod l0 Result.ret { self with hash_map_slots := v } /- [core::num::u32::{9}::MAX] -/ @@ -146,50 +146,50 @@ 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 HashMap.move_elements_from_list_loop_fwd_back - (T : Type) (ntable : hash_map_t T) (ls : list_t T) : Result (hash_map_t T) := + (T : Type) (ntable : HashMap T) (ls : List T) : Result (HashMap T) := match ls with - | list_t.Cons k v tl => + | List.Cons k v tl => do let ntable0 ← HashMap.insert_no_resize_fwd_back T ntable k v HashMap.move_elements_from_list_loop_fwd_back T ntable0 tl - | list_t.Nil => Result.ret ntable + | List.Nil => Result.ret ntable /- [hashmap::HashMap::{0}::move_elements_from_list] -/ def HashMap.move_elements_from_list_fwd_back - (T : Type) (ntable : hash_map_t T) (ls : list_t T) : Result (hash_map_t T) := + (T : Type) (ntable : HashMap T) (ls : List T) : Result (HashMap T) := HashMap.move_elements_from_list_loop_fwd_back T ntable ls /- [hashmap::HashMap::{0}::move_elements] -/ divergent def HashMap.move_elements_loop_fwd_back - (T : Type) (ntable : hash_map_t T) (slots : Vec (list_t T)) (i : Usize) : - Result ((hash_map_t T) × (Vec (list_t T))) + (T : Type) (ntable : HashMap T) (slots : Vec (List T)) (i : Usize) : + Result ((HashMap T) × (Vec (List T))) := - let i0 := vec_len (list_t T) slots + let i0 := vec_len (List T) slots if i < i0 then do - let l ← vec_index_mut_fwd (list_t T) slots i - let ls := mem_replace_fwd (list_t T) l list_t.Nil + let l ← vec_index_mut_fwd (List T) slots i + let ls := mem_replace_fwd (List T) l List.Nil let ntable0 ← HashMap.move_elements_from_list_fwd_back T ntable ls let i1 ← i + (Usize.ofInt 1 (by intlit)) - let l0 := mem_replace_back (list_t T) l list_t.Nil - let slots0 ← vec_index_mut_back (list_t T) slots i l0 + let l0 := mem_replace_back (List T) l List.Nil + let slots0 ← vec_index_mut_back (List T) slots i l0 HashMap.move_elements_loop_fwd_back T ntable0 slots0 i1 else Result.ret (ntable, slots) /- [hashmap::HashMap::{0}::move_elements] -/ def HashMap.move_elements_fwd_back - (T : Type) (ntable : hash_map_t T) (slots : Vec (list_t T)) (i : Usize) : - Result ((hash_map_t T) × (Vec (list_t T))) + (T : Type) (ntable : HashMap T) (slots : Vec (List T)) (i : Usize) : + Result ((HashMap T) × (Vec (List T))) := HashMap.move_elements_loop_fwd_back T ntable slots i /- [hashmap::HashMap::{0}::try_resize] -/ def HashMap.try_resize_fwd_back - (T : Type) (self : hash_map_t T) : Result (hash_map_t T) := + (T : Type) (self : HashMap T) : Result (HashMap T) := do let max_usize ← Scalar.cast .Usize core_num_u32_max_c - let capacity := vec_len (list_t T) self.hash_map_slots + let capacity := vec_len (List T) self.hash_map_slots let n1 ← max_usize / (Usize.ofInt 2 (by intlit)) let (i, i0) := self.hash_map_max_load_factor let i1 ← n1 / i @@ -212,8 +212,8 @@ def HashMap.try_resize_fwd_back /- [hashmap::HashMap::{0}::insert] -/ def HashMap.insert_fwd_back - (T : Type) (self : hash_map_t T) (key : Usize) (value : T) : - Result (hash_map_t T) + (T : Type) (self : HashMap T) (key : Usize) (value : T) : + Result (HashMap T) := do let self0 ← HashMap.insert_no_resize_fwd_back T self key value @@ -224,162 +224,159 @@ def HashMap.insert_fwd_back /- [hashmap::HashMap::{0}::contains_key_in_list] -/ divergent def HashMap.contains_key_in_list_loop_fwd - (T : Type) (key : Usize) (ls : list_t T) : Result Bool := + (T : Type) (key : Usize) (ls : List T) : Result Bool := match ls with - | list_t.Cons ckey t tl => + | List.Cons ckey t tl => if ckey = key then Result.ret true else HashMap.contains_key_in_list_loop_fwd T key tl - | list_t.Nil => Result.ret false + | List.Nil => Result.ret false /- [hashmap::HashMap::{0}::contains_key_in_list] -/ def HashMap.contains_key_in_list_fwd - (T : Type) (key : Usize) (ls : list_t T) : Result Bool := + (T : Type) (key : Usize) (ls : List T) : Result Bool := HashMap.contains_key_in_list_loop_fwd T key ls /- [hashmap::HashMap::{0}::contains_key] -/ def HashMap.contains_key_fwd - (T : Type) (self : hash_map_t T) (key : Usize) : Result Bool := + (T : Type) (self : HashMap T) (key : Usize) : Result Bool := do let hash ← hash_key_fwd key - let i := vec_len (list_t T) self.hash_map_slots + let i := vec_len (List T) self.hash_map_slots let hash_mod ← hash % i - let l ← vec_index_fwd (list_t T) self.hash_map_slots hash_mod + let l ← vec_index_fwd (List T) self.hash_map_slots hash_mod HashMap.contains_key_in_list_fwd T key l /- [hashmap::HashMap::{0}::get_in_list] -/ divergent def HashMap.get_in_list_loop_fwd - (T : Type) (key : Usize) (ls : list_t T) : Result T := + (T : Type) (key : Usize) (ls : List T) : Result T := match ls with - | list_t.Cons ckey cvalue tl => + | List.Cons ckey cvalue tl => if ckey = key then Result.ret cvalue else HashMap.get_in_list_loop_fwd T key tl - | list_t.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [hashmap::HashMap::{0}::get_in_list] -/ def HashMap.get_in_list_fwd - (T : Type) (key : Usize) (ls : list_t T) : Result T := + (T : Type) (key : Usize) (ls : List T) : Result T := HashMap.get_in_list_loop_fwd T key ls /- [hashmap::HashMap::{0}::get] -/ -def HashMap.get_fwd - (T : Type) (self : hash_map_t T) (key : Usize) : Result T := +def HashMap.get_fwd (T : Type) (self : HashMap T) (key : Usize) : Result T := do let hash ← hash_key_fwd key - let i := vec_len (list_t T) self.hash_map_slots + let i := vec_len (List T) self.hash_map_slots let hash_mod ← hash % i - let l ← vec_index_fwd (list_t T) self.hash_map_slots hash_mod + let l ← vec_index_fwd (List T) self.hash_map_slots hash_mod HashMap.get_in_list_fwd T key l /- [hashmap::HashMap::{0}::get_mut_in_list] -/ divergent def HashMap.get_mut_in_list_loop_fwd - (T : Type) (ls : list_t T) (key : Usize) : Result T := + (T : Type) (ls : List T) (key : Usize) : Result T := match ls with - | list_t.Cons ckey cvalue tl => + | List.Cons ckey cvalue tl => if ckey = key then Result.ret cvalue else HashMap.get_mut_in_list_loop_fwd T tl key - | list_t.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [hashmap::HashMap::{0}::get_mut_in_list] -/ def HashMap.get_mut_in_list_fwd - (T : Type) (ls : list_t T) (key : Usize) : Result T := + (T : Type) (ls : List T) (key : Usize) : Result T := HashMap.get_mut_in_list_loop_fwd T ls key /- [hashmap::HashMap::{0}::get_mut_in_list] -/ divergent def HashMap.get_mut_in_list_loop_back - (T : Type) (ls : list_t T) (key : Usize) (ret0 : T) : Result (list_t T) := + (T : Type) (ls : List T) (key : Usize) (ret0 : T) : Result (List T) := match ls with - | list_t.Cons ckey cvalue tl => + | List.Cons ckey cvalue tl => if ckey = key - then Result.ret (list_t.Cons ckey ret0 tl) + then Result.ret (List.Cons ckey ret0 tl) else do let tl0 ← HashMap.get_mut_in_list_loop_back T tl key ret0 - Result.ret (list_t.Cons ckey cvalue tl0) - | list_t.Nil => Result.fail Error.panic + Result.ret (List.Cons ckey cvalue tl0) + | List.Nil => Result.fail Error.panic /- [hashmap::HashMap::{0}::get_mut_in_list] -/ def HashMap.get_mut_in_list_back - (T : Type) (ls : list_t T) (key : Usize) (ret0 : T) : Result (list_t T) := + (T : Type) (ls : List T) (key : Usize) (ret0 : T) : Result (List T) := HashMap.get_mut_in_list_loop_back T ls key ret0 /- [hashmap::HashMap::{0}::get_mut] -/ def HashMap.get_mut_fwd - (T : Type) (self : hash_map_t T) (key : Usize) : Result T := + (T : Type) (self : HashMap T) (key : Usize) : Result T := do let hash ← hash_key_fwd key - let i := vec_len (list_t T) self.hash_map_slots + let i := vec_len (List T) self.hash_map_slots let hash_mod ← hash % i - let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod + let l ← vec_index_mut_fwd (List T) self.hash_map_slots hash_mod HashMap.get_mut_in_list_fwd T l key /- [hashmap::HashMap::{0}::get_mut] -/ def HashMap.get_mut_back - (T : Type) (self : hash_map_t T) (key : Usize) (ret0 : T) : - Result (hash_map_t T) + (T : Type) (self : HashMap T) (key : Usize) (ret0 : T) : + Result (HashMap T) := do let hash ← hash_key_fwd key - let i := vec_len (list_t T) self.hash_map_slots + let i := vec_len (List T) self.hash_map_slots let hash_mod ← hash % i - let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod + let l ← vec_index_mut_fwd (List T) self.hash_map_slots hash_mod let l0 ← HashMap.get_mut_in_list_back T l key ret0 - let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 + let v ← vec_index_mut_back (List T) self.hash_map_slots hash_mod l0 Result.ret { self with hash_map_slots := v } /- [hashmap::HashMap::{0}::remove_from_list] -/ divergent def HashMap.remove_from_list_loop_fwd - (T : Type) (key : Usize) (ls : list_t T) : Result (Option T) := + (T : Type) (key : Usize) (ls : List T) : Result (Option T) := match ls with - | list_t.Cons ckey t tl => + | List.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 + let mv_ls := mem_replace_fwd (List T) (List.Cons ckey t tl) List.Nil match mv_ls with - | list_t.Cons i cvalue tl0 => Result.ret (Option.some cvalue) - | list_t.Nil => Result.fail Error.panic + | List.Cons i cvalue tl0 => Result.ret (Option.some cvalue) + | List.Nil => Result.fail Error.panic else HashMap.remove_from_list_loop_fwd T key tl - | list_t.Nil => Result.ret Option.none + | List.Nil => Result.ret Option.none /- [hashmap::HashMap::{0}::remove_from_list] -/ def HashMap.remove_from_list_fwd - (T : Type) (key : Usize) (ls : list_t T) : Result (Option T) := + (T : Type) (key : Usize) (ls : List T) : Result (Option T) := HashMap.remove_from_list_loop_fwd T key ls /- [hashmap::HashMap::{0}::remove_from_list] -/ divergent def HashMap.remove_from_list_loop_back - (T : Type) (key : Usize) (ls : list_t T) : Result (list_t T) := + (T : Type) (key : Usize) (ls : List T) : Result (List T) := match ls with - | list_t.Cons ckey t tl => + | List.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 + let mv_ls := mem_replace_fwd (List T) (List.Cons ckey t tl) List.Nil match mv_ls with - | list_t.Cons i cvalue tl0 => Result.ret tl0 - | list_t.Nil => Result.fail Error.panic + | List.Cons i cvalue tl0 => Result.ret tl0 + | List.Nil => Result.fail Error.panic else do let tl0 ← HashMap.remove_from_list_loop_back T key tl - Result.ret (list_t.Cons ckey t tl0) - | list_t.Nil => Result.ret list_t.Nil + Result.ret (List.Cons ckey t tl0) + | List.Nil => Result.ret List.Nil /- [hashmap::HashMap::{0}::remove_from_list] -/ def HashMap.remove_from_list_back - (T : Type) (key : Usize) (ls : list_t T) : Result (list_t T) := + (T : Type) (key : Usize) (ls : List T) : Result (List T) := HashMap.remove_from_list_loop_back T key ls /- [hashmap::HashMap::{0}::remove] -/ def HashMap.remove_fwd - (T : Type) (self : hash_map_t T) (key : Usize) : Result (Option T) := + (T : Type) (self : HashMap T) (key : Usize) : Result (Option T) := do let hash ← hash_key_fwd key - let i := vec_len (list_t T) self.hash_map_slots + let i := vec_len (List T) self.hash_map_slots let hash_mod ← hash % i - let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod + let l ← vec_index_mut_fwd (List T) self.hash_map_slots hash_mod let x ← HashMap.remove_from_list_fwd T key l match x with | Option.none => Result.ret Option.none @@ -390,24 +387,24 @@ def HashMap.remove_fwd /- [hashmap::HashMap::{0}::remove] -/ def HashMap.remove_back - (T : Type) (self : hash_map_t T) (key : Usize) : Result (hash_map_t T) := + (T : Type) (self : HashMap T) (key : Usize) : Result (HashMap T) := do let hash ← hash_key_fwd key - let i := vec_len (list_t T) self.hash_map_slots + let i := vec_len (List T) self.hash_map_slots let hash_mod ← hash % i - let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod + let l ← vec_index_mut_fwd (List T) self.hash_map_slots hash_mod let x ← HashMap.remove_from_list_fwd T key l match x with | Option.none => do let l0 ← HashMap.remove_from_list_back T key l - let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 + let v ← vec_index_mut_back (List T) self.hash_map_slots hash_mod l0 Result.ret { self with hash_map_slots := v } | Option.some x0 => do let i0 ← self.hash_map_num_entries - (Usize.ofInt 1 (by intlit)) let l0 ← HashMap.remove_from_list_back T key l - let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0 + let v ← vec_index_mut_back (List T) self.hash_map_slots hash_mod l0 Result.ret { self with hash_map_num_entries := i0, hash_map_slots := v } diff --git a/tests/lean/Hashmap/Types.lean b/tests/lean/Hashmap/Types.lean index 75a6500f..7530f3b9 100644 --- a/tests/lean/Hashmap/Types.lean +++ b/tests/lean/Hashmap/Types.lean @@ -5,15 +5,15 @@ open Primitives namespace hashmap /- [hashmap::List] -/ -inductive list_t (T : Type) := -| Cons : Usize → T → list_t T → list_t T -| Nil : list_t T +inductive List (T : Type) := +| Cons : Usize → T → List T → List T +| Nil : List T /- [hashmap::HashMap] -/ -structure hash_map_t (T : Type) where +structure HashMap (T : Type) where hash_map_num_entries : Usize hash_map_max_load_factor : (Usize × Usize) hash_map_max_load : Usize - hash_map_slots : Vec (list_t T) + hash_map_slots : Vec (List T) end hashmap diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean index 06929431..fd556878 100644 --- a/tests/lean/HashmapMain/Funs.lean +++ b/tests/lean/HashmapMain/Funs.lean @@ -12,21 +12,21 @@ def hashmap.hash_key_fwd (k : Usize) : Result Usize := /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ divergent def hashmap.HashMap.allocate_slots_loop_fwd - (T : Type) (slots : Vec (hashmap_list_t T)) (n : Usize) : - Result (Vec (hashmap_list_t T)) + (T : Type) (slots : Vec (hashmap.List T)) (n : Usize) : + Result (Vec (hashmap.List T)) := if n > (Usize.ofInt 0 (by intlit)) then do - let slots0 ← vec_push_back (hashmap_list_t T) slots hashmap_list_t.Nil + let slots0 ← vec_push_back (hashmap.List T) slots hashmap.List.Nil let n0 ← n - (Usize.ofInt 1 (by intlit)) hashmap.HashMap.allocate_slots_loop_fwd T slots0 n0 else Result.ret slots /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ def hashmap.HashMap.allocate_slots_fwd - (T : Type) (slots : Vec (hashmap_list_t T)) (n : Usize) : - Result (Vec (hashmap_list_t T)) + (T : Type) (slots : Vec (hashmap.List T)) (n : Usize) : + Result (Vec (hashmap.List T)) := hashmap.HashMap.allocate_slots_loop_fwd T slots n @@ -34,10 +34,10 @@ def hashmap.HashMap.allocate_slots_fwd def hashmap.HashMap.new_with_capacity_fwd (T : Type) (capacity : Usize) (max_load_dividend : Usize) (max_load_divisor : Usize) : - Result (hashmap_hash_map_t T) + Result (hashmap.HashMap T) := do - let v := vec_new (hashmap_list_t T) + let v := vec_new (hashmap.List T) let slots ← hashmap.HashMap.allocate_slots_fwd T v capacity let i ← capacity * max_load_dividend let i0 ← i / max_load_divisor @@ -51,28 +51,28 @@ def hashmap.HashMap.new_with_capacity_fwd } /- [hashmap_main::hashmap::HashMap::{0}::new] -/ -def hashmap.HashMap.new_fwd (T : Type) : Result (hashmap_hash_map_t T) := +def hashmap.HashMap.new_fwd (T : Type) : Result (hashmap.HashMap T) := hashmap.HashMap.new_with_capacity_fwd T (Usize.ofInt 32 (by intlit)) (Usize.ofInt 4 (by intlit)) (Usize.ofInt 5 (by intlit)) /- [hashmap_main::hashmap::HashMap::{0}::clear] -/ divergent def hashmap.HashMap.clear_loop_fwd_back - (T : Type) (slots : Vec (hashmap_list_t T)) (i : Usize) : - Result (Vec (hashmap_list_t T)) + (T : Type) (slots : Vec (hashmap.List T)) (i : Usize) : + Result (Vec (hashmap.List T)) := - let i0 := vec_len (hashmap_list_t T) slots + let i0 := vec_len (hashmap.List T) slots if i < i0 then do let i1 ← i + (Usize.ofInt 1 (by intlit)) let slots0 ← - vec_index_mut_back (hashmap_list_t T) slots i hashmap_list_t.Nil + vec_index_mut_back (hashmap.List T) slots i hashmap.List.Nil hashmap.HashMap.clear_loop_fwd_back T slots0 i1 else Result.ret slots /- [hashmap_main::hashmap::HashMap::{0}::clear] -/ def hashmap.HashMap.clear_fwd_back - (T : Type) (self : hashmap_hash_map_t T) : Result (hashmap_hash_map_t T) := + (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) := do let v ← hashmap.HashMap.clear_loop_fwd_back T self.hashmap_hash_map_slots @@ -87,59 +87,59 @@ def hashmap.HashMap.clear_fwd_back /- [hashmap_main::hashmap::HashMap::{0}::len] -/ def hashmap.HashMap.len_fwd - (T : Type) (self : hashmap_hash_map_t T) : Result Usize := + (T : Type) (self : hashmap.HashMap T) : Result Usize := Result.ret self.hashmap_hash_map_num_entries /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ divergent def hashmap.HashMap.insert_in_list_loop_fwd - (T : Type) (key : Usize) (value : T) (ls : hashmap_list_t T) : Result Bool := + (T : Type) (key : Usize) (value : T) (ls : hashmap.List T) : Result Bool := match ls with - | hashmap_list_t.Cons ckey cvalue tl => + | hashmap.List.Cons ckey cvalue tl => if ckey = key then Result.ret false else hashmap.HashMap.insert_in_list_loop_fwd T key value tl - | hashmap_list_t.Nil => Result.ret true + | hashmap.List.Nil => Result.ret true /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ def hashmap.HashMap.insert_in_list_fwd - (T : Type) (key : Usize) (value : T) (ls : hashmap_list_t T) : Result Bool := + (T : Type) (key : Usize) (value : T) (ls : hashmap.List T) : Result Bool := hashmap.HashMap.insert_in_list_loop_fwd T key value ls /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ divergent def hashmap.HashMap.insert_in_list_loop_back - (T : Type) (key : Usize) (value : T) (ls : hashmap_list_t T) : - Result (hashmap_list_t T) + (T : Type) (key : Usize) (value : T) (ls : hashmap.List T) : + Result (hashmap.List T) := match ls with - | hashmap_list_t.Cons ckey cvalue tl => + | hashmap.List.Cons ckey cvalue tl => if ckey = key - then Result.ret (hashmap_list_t.Cons ckey value tl) + then Result.ret (hashmap.List.Cons ckey value tl) else do let tl0 ← hashmap.HashMap.insert_in_list_loop_back T key value tl - Result.ret (hashmap_list_t.Cons ckey cvalue tl0) - | hashmap_list_t.Nil => - let l := hashmap_list_t.Nil - Result.ret (hashmap_list_t.Cons key value l) + Result.ret (hashmap.List.Cons ckey cvalue tl0) + | hashmap.List.Nil => + let l := hashmap.List.Nil + Result.ret (hashmap.List.Cons key value l) /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ def hashmap.HashMap.insert_in_list_back - (T : Type) (key : Usize) (value : T) (ls : hashmap_list_t T) : - Result (hashmap_list_t T) + (T : Type) (key : Usize) (value : T) (ls : hashmap.List T) : + Result (hashmap.List T) := hashmap.HashMap.insert_in_list_loop_back T key value ls /- [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] -/ def hashmap.HashMap.insert_no_resize_fwd_back - (T : Type) (self : hashmap_hash_map_t T) (key : Usize) (value : T) : - Result (hashmap_hash_map_t T) + (T : Type) (self : hashmap.HashMap T) (key : Usize) (value : T) : + Result (hashmap.HashMap T) := do let hash ← hashmap.hash_key_fwd key - let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let i := vec_len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + vec_index_mut_fwd (hashmap.List T) self.hashmap_hash_map_slots hash_mod let inserted ← hashmap.HashMap.insert_in_list_fwd T key value l if inserted then @@ -148,7 +148,7 @@ def hashmap.HashMap.insert_no_resize_fwd_back (Usize.ofInt 1 (by intlit)) let l0 ← hashmap.HashMap.insert_in_list_back T key value l let v ← - vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + vec_index_mut_back (hashmap.List T) self.hashmap_hash_map_slots hash_mod l0 Result.ret { @@ -160,7 +160,7 @@ def hashmap.HashMap.insert_no_resize_fwd_back do let l0 ← hashmap.HashMap.insert_in_list_back T key value l let v ← - vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + vec_index_mut_back (hashmap.List T) self.hashmap_hash_map_slots hash_mod l0 Result.ret { self with hashmap_hash_map_slots := v } @@ -171,57 +171,57 @@ def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp) /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ divergent def hashmap.HashMap.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) + (T : Type) (ntable : hashmap.HashMap T) (ls : hashmap.List T) : + Result (hashmap.HashMap T) := match ls with - | hashmap_list_t.Cons k v tl => + | hashmap.List.Cons k v tl => do let ntable0 ← hashmap.HashMap.insert_no_resize_fwd_back T ntable k v hashmap.HashMap.move_elements_from_list_loop_fwd_back T ntable0 tl - | hashmap_list_t.Nil => Result.ret ntable + | hashmap.List.Nil => Result.ret ntable /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ def hashmap.HashMap.move_elements_from_list_fwd_back - (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : - Result (hashmap_hash_map_t T) + (T : Type) (ntable : hashmap.HashMap T) (ls : hashmap.List T) : + Result (hashmap.HashMap T) := hashmap.HashMap.move_elements_from_list_loop_fwd_back T ntable ls /- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ divergent def hashmap.HashMap.move_elements_loop_fwd_back - (T : Type) (ntable : hashmap_hash_map_t T) (slots : Vec (hashmap_list_t T)) + (T : Type) (ntable : hashmap.HashMap T) (slots : Vec (hashmap.List T)) (i : Usize) : - Result ((hashmap_hash_map_t T) × (Vec (hashmap_list_t T))) + Result ((hashmap.HashMap T) × (Vec (hashmap.List T))) := - let i0 := vec_len (hashmap_list_t T) slots + let i0 := vec_len (hashmap.List T) slots if i < i0 then do - let l ← vec_index_mut_fwd (hashmap_list_t T) slots i - let ls := mem_replace_fwd (hashmap_list_t T) l hashmap_list_t.Nil + let l ← vec_index_mut_fwd (hashmap.List T) slots i + let ls := mem_replace_fwd (hashmap.List T) l hashmap.List.Nil let ntable0 ← hashmap.HashMap.move_elements_from_list_fwd_back T ntable ls let i1 ← i + (Usize.ofInt 1 (by intlit)) - let l0 := mem_replace_back (hashmap_list_t T) l hashmap_list_t.Nil - let slots0 ← vec_index_mut_back (hashmap_list_t T) slots i l0 + let l0 := mem_replace_back (hashmap.List T) l hashmap.List.Nil + let slots0 ← vec_index_mut_back (hashmap.List T) slots i l0 hashmap.HashMap.move_elements_loop_fwd_back T ntable0 slots0 i1 else Result.ret (ntable, slots) /- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ def hashmap.HashMap.move_elements_fwd_back - (T : Type) (ntable : hashmap_hash_map_t T) (slots : Vec (hashmap_list_t T)) + (T : Type) (ntable : hashmap.HashMap T) (slots : Vec (hashmap.List T)) (i : Usize) : - Result ((hashmap_hash_map_t T) × (Vec (hashmap_list_t T))) + Result ((hashmap.HashMap T) × (Vec (hashmap.List T))) := hashmap.HashMap.move_elements_loop_fwd_back T ntable slots i /- [hashmap_main::hashmap::HashMap::{0}::try_resize] -/ def hashmap.HashMap.try_resize_fwd_back - (T : Type) (self : hashmap_hash_map_t T) : Result (hashmap_hash_map_t T) := + (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) := do let max_usize ← Scalar.cast .Usize core_num_u32_max_c - let capacity := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let capacity := vec_len (hashmap.List T) self.hashmap_hash_map_slots let n1 ← max_usize / (Usize.ofInt 2 (by intlit)) let (i, i0) := self.hashmap_hash_map_max_load_factor let i1 ← n1 / i @@ -244,8 +244,8 @@ def hashmap.HashMap.try_resize_fwd_back /- [hashmap_main::hashmap::HashMap::{0}::insert] -/ def hashmap.HashMap.insert_fwd_back - (T : Type) (self : hashmap_hash_map_t T) (key : Usize) (value : T) : - Result (hashmap_hash_map_t T) + (T : Type) (self : hashmap.HashMap T) (key : Usize) (value : T) : + Result (hashmap.HashMap T) := do let self0 ← hashmap.HashMap.insert_no_resize_fwd_back T self key value @@ -256,179 +256,175 @@ def hashmap.HashMap.insert_fwd_back /- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ divergent def hashmap.HashMap.contains_key_in_list_loop_fwd - (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result Bool := + (T : Type) (key : Usize) (ls : hashmap.List T) : Result Bool := match ls with - | hashmap_list_t.Cons ckey t tl => + | hashmap.List.Cons ckey t tl => if ckey = key then Result.ret true else hashmap.HashMap.contains_key_in_list_loop_fwd T key tl - | hashmap_list_t.Nil => Result.ret false + | hashmap.List.Nil => Result.ret false /- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ def hashmap.HashMap.contains_key_in_list_fwd - (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result Bool := + (T : Type) (key : Usize) (ls : hashmap.List T) : Result Bool := hashmap.HashMap.contains_key_in_list_loop_fwd T key ls /- [hashmap_main::hashmap::HashMap::{0}::contains_key] -/ def hashmap.HashMap.contains_key_fwd - (T : Type) (self : hashmap_hash_map_t T) (key : Usize) : Result Bool := + (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result Bool := do let hash ← hashmap.hash_key_fwd key - let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let i := vec_len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← - vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + vec_index_fwd (hashmap.List T) self.hashmap_hash_map_slots hash_mod hashmap.HashMap.contains_key_in_list_fwd T key l /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ divergent def hashmap.HashMap.get_in_list_loop_fwd - (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result T := + (T : Type) (key : Usize) (ls : hashmap.List T) : Result T := match ls with - | hashmap_list_t.Cons ckey cvalue tl => + | hashmap.List.Cons ckey cvalue tl => if ckey = key then Result.ret cvalue else hashmap.HashMap.get_in_list_loop_fwd T key tl - | hashmap_list_t.Nil => Result.fail Error.panic + | hashmap.List.Nil => Result.fail Error.panic /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ def hashmap.HashMap.get_in_list_fwd - (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result T := + (T : Type) (key : Usize) (ls : hashmap.List T) : Result T := hashmap.HashMap.get_in_list_loop_fwd T key ls /- [hashmap_main::hashmap::HashMap::{0}::get] -/ def hashmap.HashMap.get_fwd - (T : Type) (self : hashmap_hash_map_t T) (key : Usize) : Result T := + (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result T := do let hash ← hashmap.hash_key_fwd key - let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let i := vec_len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← - vec_index_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + vec_index_fwd (hashmap.List T) self.hashmap_hash_map_slots hash_mod hashmap.HashMap.get_in_list_fwd T key l /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ divergent def hashmap.HashMap.get_mut_in_list_loop_fwd - (T : Type) (ls : hashmap_list_t T) (key : Usize) : Result T := + (T : Type) (ls : hashmap.List T) (key : Usize) : Result T := match ls with - | hashmap_list_t.Cons ckey cvalue tl => + | hashmap.List.Cons ckey cvalue tl => if ckey = key then Result.ret cvalue else hashmap.HashMap.get_mut_in_list_loop_fwd T tl key - | hashmap_list_t.Nil => Result.fail Error.panic + | hashmap.List.Nil => Result.fail Error.panic /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ def hashmap.HashMap.get_mut_in_list_fwd - (T : Type) (ls : hashmap_list_t T) (key : Usize) : Result T := + (T : Type) (ls : hashmap.List T) (key : Usize) : Result T := hashmap.HashMap.get_mut_in_list_loop_fwd T ls key /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ divergent def hashmap.HashMap.get_mut_in_list_loop_back - (T : Type) (ls : hashmap_list_t T) (key : Usize) (ret0 : T) : - Result (hashmap_list_t T) + (T : Type) (ls : hashmap.List T) (key : Usize) (ret0 : T) : + Result (hashmap.List T) := match ls with - | hashmap_list_t.Cons ckey cvalue tl => + | hashmap.List.Cons ckey cvalue tl => if ckey = key - then Result.ret (hashmap_list_t.Cons ckey ret0 tl) + then Result.ret (hashmap.List.Cons ckey ret0 tl) else do let tl0 ← hashmap.HashMap.get_mut_in_list_loop_back T tl key ret0 - Result.ret (hashmap_list_t.Cons ckey cvalue tl0) - | hashmap_list_t.Nil => Result.fail Error.panic + Result.ret (hashmap.List.Cons ckey cvalue tl0) + | hashmap.List.Nil => Result.fail Error.panic /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ def hashmap.HashMap.get_mut_in_list_back - (T : Type) (ls : hashmap_list_t T) (key : Usize) (ret0 : T) : - Result (hashmap_list_t T) + (T : Type) (ls : hashmap.List T) (key : Usize) (ret0 : T) : + Result (hashmap.List T) := hashmap.HashMap.get_mut_in_list_loop_back T ls key ret0 /- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ def hashmap.HashMap.get_mut_fwd - (T : Type) (self : hashmap_hash_map_t T) (key : Usize) : Result T := + (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result T := do let hash ← hashmap.hash_key_fwd key - let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let i := vec_len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + vec_index_mut_fwd (hashmap.List T) self.hashmap_hash_map_slots hash_mod hashmap.HashMap.get_mut_in_list_fwd T l key /- [hashmap_main::hashmap::HashMap::{0}::get_mut] -/ def hashmap.HashMap.get_mut_back - (T : Type) (self : hashmap_hash_map_t T) (key : Usize) (ret0 : T) : - Result (hashmap_hash_map_t T) + (T : Type) (self : hashmap.HashMap T) (key : Usize) (ret0 : T) : + Result (hashmap.HashMap T) := do let hash ← hashmap.hash_key_fwd key - let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let i := vec_len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + vec_index_mut_fwd (hashmap.List T) self.hashmap_hash_map_slots hash_mod let l0 ← hashmap.HashMap.get_mut_in_list_back T l key ret0 let v ← - vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots - hash_mod l0 + vec_index_mut_back (hashmap.List T) self.hashmap_hash_map_slots hash_mod + l0 Result.ret { self with hashmap_hash_map_slots := v } /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ divergent def hashmap.HashMap.remove_from_list_loop_fwd - (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result (Option T) := + (T : Type) (key : Usize) (ls : hashmap.List T) : Result (Option T) := match ls with - | hashmap_list_t.Cons ckey t tl => + | hashmap.List.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 + mem_replace_fwd (hashmap.List T) (hashmap.List.Cons ckey t tl) + hashmap.List.Nil match mv_ls with - | hashmap_list_t.Cons i cvalue tl0 => Result.ret (Option.some cvalue) - | hashmap_list_t.Nil => Result.fail Error.panic + | hashmap.List.Cons i cvalue tl0 => Result.ret (Option.some cvalue) + | hashmap.List.Nil => Result.fail Error.panic else hashmap.HashMap.remove_from_list_loop_fwd T key tl - | hashmap_list_t.Nil => Result.ret Option.none + | hashmap.List.Nil => Result.ret Option.none /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ def hashmap.HashMap.remove_from_list_fwd - (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result (Option T) := + (T : Type) (key : Usize) (ls : hashmap.List T) : Result (Option T) := hashmap.HashMap.remove_from_list_loop_fwd T key ls /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ divergent def hashmap.HashMap.remove_from_list_loop_back - (T : Type) (key : Usize) (ls : hashmap_list_t T) : - Result (hashmap_list_t T) - := + (T : Type) (key : Usize) (ls : hashmap.List T) : Result (hashmap.List T) := match ls with - | hashmap_list_t.Cons ckey t tl => + | hashmap.List.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 + mem_replace_fwd (hashmap.List T) (hashmap.List.Cons ckey t tl) + hashmap.List.Nil match mv_ls with - | hashmap_list_t.Cons i cvalue tl0 => Result.ret tl0 - | hashmap_list_t.Nil => Result.fail Error.panic + | hashmap.List.Cons i cvalue tl0 => Result.ret tl0 + | hashmap.List.Nil => Result.fail Error.panic else do let tl0 ← hashmap.HashMap.remove_from_list_loop_back T key tl - Result.ret (hashmap_list_t.Cons ckey t tl0) - | hashmap_list_t.Nil => Result.ret hashmap_list_t.Nil + Result.ret (hashmap.List.Cons ckey t tl0) + | hashmap.List.Nil => Result.ret hashmap.List.Nil /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ def hashmap.HashMap.remove_from_list_back - (T : Type) (key : Usize) (ls : hashmap_list_t T) : - Result (hashmap_list_t T) - := + (T : Type) (key : Usize) (ls : hashmap.List T) : Result (hashmap.List T) := hashmap.HashMap.remove_from_list_loop_back T key ls /- [hashmap_main::hashmap::HashMap::{0}::remove] -/ def hashmap.HashMap.remove_fwd - (T : Type) (self : hashmap_hash_map_t T) (key : Usize) : Result (Option T) := + (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result (Option T) := do let hash ← hashmap.hash_key_fwd key - let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let i := vec_len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + vec_index_mut_fwd (hashmap.List T) self.hashmap_hash_map_slots hash_mod let x ← hashmap.HashMap.remove_from_list_fwd T key l match x with | Option.none => Result.ret Option.none @@ -440,22 +436,22 @@ def hashmap.HashMap.remove_fwd /- [hashmap_main::hashmap::HashMap::{0}::remove] -/ def hashmap.HashMap.remove_back - (T : Type) (self : hashmap_hash_map_t T) (key : Usize) : - Result (hashmap_hash_map_t T) + (T : Type) (self : hashmap.HashMap T) (key : Usize) : + Result (hashmap.HashMap T) := do let hash ← hashmap.hash_key_fwd key - let i := vec_len (hashmap_list_t T) self.hashmap_hash_map_slots + let i := vec_len (hashmap.List T) self.hashmap_hash_map_slots let hash_mod ← hash % i let l ← - vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod + vec_index_mut_fwd (hashmap.List T) self.hashmap_hash_map_slots hash_mod let x ← hashmap.HashMap.remove_from_list_fwd T key l match x with | Option.none => do let l0 ← hashmap.HashMap.remove_from_list_back T key l let v ← - vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + vec_index_mut_back (hashmap.List T) self.hashmap_hash_map_slots hash_mod l0 Result.ret { self with hashmap_hash_map_slots := v } | Option.some x0 => @@ -464,7 +460,7 @@ def hashmap.HashMap.remove_back (Usize.ofInt 1 (by intlit)) let l0 ← hashmap.HashMap.remove_from_list_back T key l let v ← - vec_index_mut_back (hashmap_list_t T) self.hashmap_hash_map_slots + vec_index_mut_back (hashmap.List T) self.hashmap_hash_map_slots hash_mod l0 Result.ret { diff --git a/tests/lean/HashmapMain/FunsExternal.lean b/tests/lean/HashmapMain/FunsExternal.lean index d917b485..3689dd45 100644 --- a/tests/lean/HashmapMain/FunsExternal.lean +++ b/tests/lean/HashmapMain/FunsExternal.lean @@ -8,10 +8,10 @@ open hashmap_main /- [hashmap_main::hashmap_utils::deserialize] -/ def hashmap_utils.deserialize_fwd - : State → Result (State × (hashmap_hash_map_t U64)) := + : State → Result (State × (hashmap.HashMap U64)) := fun _ => .fail .panic /- [hashmap_main::hashmap_utils::serialize] -/ def hashmap_utils.serialize_fwd - : hashmap_hash_map_t U64 → State → Result (State × Unit) := + : hashmap.HashMap U64 → State → Result (State × Unit) := fun _ _ => .fail .panic diff --git a/tests/lean/HashmapMain/FunsExternal_Template.lean b/tests/lean/HashmapMain/FunsExternal_Template.lean index 86286373..8853b7fc 100644 --- a/tests/lean/HashmapMain/FunsExternal_Template.lean +++ b/tests/lean/HashmapMain/FunsExternal_Template.lean @@ -8,9 +8,9 @@ open hashmap_main /- [hashmap_main::hashmap_utils::deserialize] -/ axiom hashmap_utils.deserialize_fwd - : State → Result (State × (hashmap_hash_map_t U64)) + : State → Result (State × (hashmap.HashMap U64)) /- [hashmap_main::hashmap_utils::serialize] -/ axiom hashmap_utils.serialize_fwd - : hashmap_hash_map_t U64 → State → Result (State × Unit) + : hashmap.HashMap U64 → State → Result (State × Unit) diff --git a/tests/lean/HashmapMain/Types.lean b/tests/lean/HashmapMain/Types.lean index 16641146..ac195e3d 100644 --- a/tests/lean/HashmapMain/Types.lean +++ b/tests/lean/HashmapMain/Types.lean @@ -5,16 +5,16 @@ open Primitives namespace hashmap_main /- [hashmap_main::hashmap::List] -/ -inductive hashmap_list_t (T : Type) := -| Cons : Usize → T → hashmap_list_t T → hashmap_list_t T -| Nil : hashmap_list_t T +inductive hashmap.List (T : Type) := +| Cons : Usize → T → hashmap.List T → hashmap.List T +| Nil : hashmap.List T /- [hashmap_main::hashmap::HashMap] -/ -structure hashmap_hash_map_t (T : Type) where +structure hashmap.HashMap (T : Type) where hashmap_hash_map_num_entries : Usize hashmap_hash_map_max_load_factor : (Usize × Usize) hashmap_hash_map_max_load : Usize - hashmap_hash_map_slots : Vec (hashmap_list_t T) + hashmap_hash_map_slots : Vec (hashmap.List T) /- The state type used in the state-error monad -/ axiom State : Type diff --git a/tests/lean/Loops/Funs.lean b/tests/lean/Loops/Funs.lean index 694f5450..383bc819 100644 --- a/tests/lean/Loops/Funs.lean +++ b/tests/lean/Loops/Funs.lean @@ -68,179 +68,175 @@ def clear_fwd_back (v : Vec U32) : Result (Vec U32) := clear_loop_fwd_back v (Usize.ofInt 0 (by intlit)) /- [loops::list_mem] -/ -divergent def list_mem_loop_fwd (x : U32) (ls : list_t U32) : Result Bool := +divergent def list_mem_loop_fwd (x : U32) (ls : List U32) : Result Bool := match ls with - | list_t.Cons y tl => - if y = x - then Result.ret true - else list_mem_loop_fwd x tl - | list_t.Nil => Result.ret false + | List.Cons y tl => if y = x + then Result.ret true + else list_mem_loop_fwd x tl + | List.Nil => Result.ret false /- [loops::list_mem] -/ -def list_mem_fwd (x : U32) (ls : list_t U32) : Result Bool := +def list_mem_fwd (x : U32) (ls : List U32) : Result Bool := list_mem_loop_fwd x ls /- [loops::list_nth_mut_loop] -/ divergent def list_nth_mut_loop_loop_fwd - (T : Type) (ls : list_t T) (i : U32) : Result T := + (T : Type) (ls : List T) (i : U32) : Result T := match ls with - | list_t.Cons x tl => + | List.Cons x tl => if i = (U32.ofInt 0 (by intlit)) then Result.ret x else do let i0 ← i - (U32.ofInt 1 (by intlit)) list_nth_mut_loop_loop_fwd T tl i0 - | list_t.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [loops::list_nth_mut_loop] -/ -def list_nth_mut_loop_fwd (T : Type) (ls : list_t T) (i : U32) : Result T := +def list_nth_mut_loop_fwd (T : Type) (ls : List T) (i : U32) : Result T := list_nth_mut_loop_loop_fwd T ls i /- [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) := + (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) := match ls with - | list_t.Cons x tl => + | List.Cons x tl => if i = (U32.ofInt 0 (by intlit)) - then Result.ret (list_t.Cons ret0 tl) + then Result.ret (List.Cons ret0 tl) else do let i0 ← i - (U32.ofInt 1 (by intlit)) let tl0 ← list_nth_mut_loop_loop_back T tl i0 ret0 - Result.ret (list_t.Cons x tl0) - | list_t.Nil => Result.fail Error.panic + Result.ret (List.Cons x tl0) + | List.Nil => Result.fail Error.panic /- [loops::list_nth_mut_loop] -/ def list_nth_mut_loop_back - (T : Type) (ls : list_t T) (i : U32) (ret0 : T) : Result (list_t T) := + (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) := list_nth_mut_loop_loop_back T ls i ret0 /- [loops::list_nth_shared_loop] -/ divergent def list_nth_shared_loop_loop_fwd - (T : Type) (ls : list_t T) (i : U32) : Result T := + (T : Type) (ls : List T) (i : U32) : Result T := match ls with - | list_t.Cons x tl => + | List.Cons x tl => if i = (U32.ofInt 0 (by intlit)) then Result.ret x else do let i0 ← i - (U32.ofInt 1 (by intlit)) list_nth_shared_loop_loop_fwd T tl i0 - | list_t.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [loops::list_nth_shared_loop] -/ -def list_nth_shared_loop_fwd (T : Type) (ls : list_t T) (i : U32) : Result T := +def list_nth_shared_loop_fwd (T : Type) (ls : List T) (i : U32) : Result T := list_nth_shared_loop_loop_fwd T ls i /- [loops::get_elem_mut] -/ divergent def get_elem_mut_loop_fwd - (x : Usize) (ls : list_t Usize) : Result Usize := + (x : Usize) (ls : List Usize) : Result Usize := match ls with - | list_t.Cons y tl => + | List.Cons y tl => if y = x then Result.ret y else get_elem_mut_loop_fwd x tl - | list_t.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [loops::get_elem_mut] -/ -def get_elem_mut_fwd (slots : Vec (list_t Usize)) (x : Usize) : Result Usize := +def get_elem_mut_fwd (slots : Vec (List Usize)) (x : Usize) : Result Usize := do - let l ← - vec_index_mut_fwd (list_t Usize) slots (Usize.ofInt 0 (by intlit)) + let l ← vec_index_mut_fwd (List Usize) slots (Usize.ofInt 0 (by intlit)) get_elem_mut_loop_fwd x l /- [loops::get_elem_mut] -/ divergent def get_elem_mut_loop_back - (x : Usize) (ls : list_t Usize) (ret0 : Usize) : Result (list_t Usize) := + (x : Usize) (ls : List Usize) (ret0 : Usize) : Result (List Usize) := match ls with - | list_t.Cons y tl => + | List.Cons y tl => if y = x - then Result.ret (list_t.Cons ret0 tl) + then Result.ret (List.Cons ret0 tl) else do let tl0 ← get_elem_mut_loop_back x tl ret0 - Result.ret (list_t.Cons y tl0) - | list_t.Nil => Result.fail Error.panic + Result.ret (List.Cons y tl0) + | List.Nil => Result.fail Error.panic /- [loops::get_elem_mut] -/ def get_elem_mut_back - (slots : Vec (list_t Usize)) (x : Usize) (ret0 : Usize) : - Result (Vec (list_t Usize)) + (slots : Vec (List Usize)) (x : Usize) (ret0 : Usize) : + Result (Vec (List Usize)) := do - let l ← - vec_index_mut_fwd (list_t Usize) slots (Usize.ofInt 0 (by intlit)) + let l ← vec_index_mut_fwd (List Usize) slots (Usize.ofInt 0 (by intlit)) let l0 ← get_elem_mut_loop_back x l ret0 - vec_index_mut_back (list_t Usize) slots (Usize.ofInt 0 (by intlit)) l0 + vec_index_mut_back (List Usize) slots (Usize.ofInt 0 (by intlit)) l0 /- [loops::get_elem_shared] -/ divergent def get_elem_shared_loop_fwd - (x : Usize) (ls : list_t Usize) : Result Usize := + (x : Usize) (ls : List Usize) : Result Usize := match ls with - | list_t.Cons y tl => + | List.Cons y tl => if y = x then Result.ret y else get_elem_shared_loop_fwd x tl - | list_t.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [loops::get_elem_shared] -/ def get_elem_shared_fwd - (slots : Vec (list_t Usize)) (x : Usize) : Result Usize := + (slots : Vec (List Usize)) (x : Usize) : Result Usize := do - let l ← vec_index_fwd (list_t Usize) slots (Usize.ofInt 0 (by intlit)) + let l ← vec_index_fwd (List Usize) slots (Usize.ofInt 0 (by intlit)) get_elem_shared_loop_fwd x l /- [loops::id_mut] -/ -def id_mut_fwd (T : Type) (ls : list_t T) : Result (list_t T) := +def id_mut_fwd (T : Type) (ls : List T) : Result (List T) := Result.ret ls /- [loops::id_mut] -/ -def id_mut_back - (T : Type) (ls : list_t T) (ret0 : list_t T) : Result (list_t T) := +def id_mut_back (T : Type) (ls : List T) (ret0 : List T) : Result (List T) := Result.ret ret0 /- [loops::id_shared] -/ -def id_shared_fwd (T : Type) (ls : list_t T) : Result (list_t T) := +def id_shared_fwd (T : Type) (ls : List T) : Result (List T) := Result.ret ls /- [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 := + (T : Type) (i : U32) (ls : List T) : Result T := match ls with - | list_t.Cons x tl => + | List.Cons x tl => if i = (U32.ofInt 0 (by intlit)) then Result.ret x else do let i0 ← i - (U32.ofInt 1 (by intlit)) list_nth_mut_loop_with_id_loop_fwd T i0 tl - | list_t.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [loops::list_nth_mut_loop_with_id] -/ def list_nth_mut_loop_with_id_fwd - (T : Type) (ls : list_t T) (i : U32) : Result T := + (T : Type) (ls : List T) (i : U32) : Result T := do let ls0 ← id_mut_fwd T ls list_nth_mut_loop_with_id_loop_fwd T i ls0 /- [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) := + (T : Type) (i : U32) (ls : List T) (ret0 : T) : Result (List T) := match ls with - | list_t.Cons x tl => + | List.Cons x tl => if i = (U32.ofInt 0 (by intlit)) - then Result.ret (list_t.Cons ret0 tl) + then Result.ret (List.Cons ret0 tl) else do let i0 ← i - (U32.ofInt 1 (by intlit)) let tl0 ← list_nth_mut_loop_with_id_loop_back T i0 tl ret0 - Result.ret (list_t.Cons x tl0) - | list_t.Nil => Result.fail Error.panic + Result.ret (List.Cons x tl0) + | List.Nil => Result.fail Error.panic /- [loops::list_nth_mut_loop_with_id] -/ def list_nth_mut_loop_with_id_back - (T : Type) (ls : list_t T) (i : U32) (ret0 : T) : Result (list_t T) := + (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) := do let ls0 ← id_mut_fwd T ls let l ← list_nth_mut_loop_with_id_loop_back T i ls0 ret0 @@ -248,378 +244,377 @@ 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 := + (T : Type) (i : U32) (ls : List T) : Result T := match ls with - | list_t.Cons x tl => + | List.Cons x tl => if i = (U32.ofInt 0 (by intlit)) then Result.ret x else do let i0 ← i - (U32.ofInt 1 (by intlit)) list_nth_shared_loop_with_id_loop_fwd T i0 tl - | list_t.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [loops::list_nth_shared_loop_with_id] -/ def list_nth_shared_loop_with_id_fwd - (T : Type) (ls : list_t T) (i : U32) : Result T := + (T : Type) (ls : List T) (i : U32) : Result T := do let ls0 ← id_shared_fwd T ls list_nth_shared_loop_with_id_loop_fwd T i ls0 /- [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) := + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := match ls0 with - | list_t.Cons x0 tl0 => + | List.Cons x0 tl0 => match ls1 with - | list_t.Cons x1 tl1 => + | List.Cons x1 tl1 => if i = (U32.ofInt 0 (by intlit)) then Result.ret (x0, x1) else do let i0 ← i - (U32.ofInt 1 (by intlit)) list_nth_mut_loop_pair_loop_fwd T tl0 tl1 i0 - | list_t.Nil => Result.fail Error.panic - | list_t.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [loops::list_nth_mut_loop_pair] -/ def list_nth_mut_loop_pair_fwd - (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) := + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := list_nth_mut_loop_pair_loop_fwd T ls0 ls1 i /- [loops::list_nth_mut_loop_pair] -/ 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) + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) := match ls0 with - | list_t.Cons x0 tl0 => + | List.Cons x0 tl0 => match ls1 with - | list_t.Cons x1 tl1 => + | List.Cons x1 tl1 => if i = (U32.ofInt 0 (by intlit)) - then Result.ret (list_t.Cons ret0 tl0) + then Result.ret (List.Cons ret0 tl0) else do let i0 ← i - (U32.ofInt 1 (by intlit)) let tl00 ← list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret0 - Result.ret (list_t.Cons x0 tl00) - | list_t.Nil => Result.fail Error.panic - | list_t.Nil => Result.fail Error.panic + Result.ret (List.Cons x0 tl00) + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [loops::list_nth_mut_loop_pair] -/ def list_nth_mut_loop_pair_back'a - (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) : - Result (list_t T) + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) := list_nth_mut_loop_pair_loop_back'a T ls0 ls1 i ret0 /- [loops::list_nth_mut_loop_pair] -/ 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) + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) := match ls0 with - | list_t.Cons x0 tl0 => + | List.Cons x0 tl0 => match ls1 with - | list_t.Cons x1 tl1 => + | List.Cons x1 tl1 => if i = (U32.ofInt 0 (by intlit)) - then Result.ret (list_t.Cons ret0 tl1) + then Result.ret (List.Cons ret0 tl1) else do let i0 ← i - (U32.ofInt 1 (by intlit)) let tl10 ← list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret0 - Result.ret (list_t.Cons x1 tl10) - | list_t.Nil => Result.fail Error.panic - | list_t.Nil => Result.fail Error.panic + Result.ret (List.Cons x1 tl10) + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [loops::list_nth_mut_loop_pair] -/ def list_nth_mut_loop_pair_back'b - (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) : - Result (list_t T) + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) := list_nth_mut_loop_pair_loop_back'b T ls0 ls1 i ret0 /- [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) := + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := match ls0 with - | list_t.Cons x0 tl0 => + | List.Cons x0 tl0 => match ls1 with - | list_t.Cons x1 tl1 => + | List.Cons x1 tl1 => if i = (U32.ofInt 0 (by intlit)) then Result.ret (x0, x1) else do let i0 ← i - (U32.ofInt 1 (by intlit)) list_nth_shared_loop_pair_loop_fwd T tl0 tl1 i0 - | list_t.Nil => Result.fail Error.panic - | list_t.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [loops::list_nth_shared_loop_pair] -/ def list_nth_shared_loop_pair_fwd - (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) := + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := list_nth_shared_loop_pair_loop_fwd T ls0 ls1 i /- [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) := + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := match ls0 with - | list_t.Cons x0 tl0 => + | List.Cons x0 tl0 => match ls1 with - | list_t.Cons x1 tl1 => + | List.Cons x1 tl1 => if i = (U32.ofInt 0 (by intlit)) then Result.ret (x0, x1) else do let i0 ← i - (U32.ofInt 1 (by intlit)) list_nth_mut_loop_pair_merge_loop_fwd T tl0 tl1 i0 - | list_t.Nil => Result.fail Error.panic - | list_t.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [loops::list_nth_mut_loop_pair_merge] -/ def list_nth_mut_loop_pair_merge_fwd - (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) := + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := list_nth_mut_loop_pair_merge_loop_fwd T ls0 ls1 i /- [loops::list_nth_mut_loop_pair_merge] -/ 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)) + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) : + Result ((List T) × (List T)) := match ls0 with - | list_t.Cons x0 tl0 => + | List.Cons x0 tl0 => match ls1 with - | list_t.Cons x1 tl1 => + | List.Cons x1 tl1 => if i = (U32.ofInt 0 (by intlit)) - then - let (t, t0) := ret0 - Result.ret (list_t.Cons t tl0, list_t.Cons t0 tl1) + then let (t, t0) := ret0 + Result.ret (List.Cons t tl0, List.Cons t0 tl1) else do let i0 ← i - (U32.ofInt 1 (by intlit)) let (tl00, tl10) ← list_nth_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 - Result.ret (list_t.Cons x0 tl00, list_t.Cons x1 tl10) - | list_t.Nil => Result.fail Error.panic - | list_t.Nil => Result.fail Error.panic + Result.ret (List.Cons x0 tl00, List.Cons x1 tl10) + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [loops::list_nth_mut_loop_pair_merge] -/ def list_nth_mut_loop_pair_merge_back - (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : (T × T)) : - Result ((list_t T) × (list_t T)) + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) : + Result ((List T) × (List T)) := list_nth_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0 /- [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) := + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := match ls0 with - | list_t.Cons x0 tl0 => + | List.Cons x0 tl0 => match ls1 with - | list_t.Cons x1 tl1 => + | List.Cons x1 tl1 => if i = (U32.ofInt 0 (by intlit)) then Result.ret (x0, x1) else do let i0 ← i - (U32.ofInt 1 (by intlit)) list_nth_shared_loop_pair_merge_loop_fwd T tl0 tl1 i0 - | list_t.Nil => Result.fail Error.panic - | list_t.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [loops::list_nth_shared_loop_pair_merge] -/ def list_nth_shared_loop_pair_merge_fwd - (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) := + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := list_nth_shared_loop_pair_merge_loop_fwd T ls0 ls1 i /- [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) := + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := match ls0 with - | list_t.Cons x0 tl0 => + | List.Cons x0 tl0 => match ls1 with - | list_t.Cons x1 tl1 => + | List.Cons x1 tl1 => if i = (U32.ofInt 0 (by intlit)) then Result.ret (x0, x1) else do let i0 ← i - (U32.ofInt 1 (by intlit)) list_nth_mut_shared_loop_pair_loop_fwd T tl0 tl1 i0 - | list_t.Nil => Result.fail Error.panic - | list_t.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [loops::list_nth_mut_shared_loop_pair] -/ def list_nth_mut_shared_loop_pair_fwd - (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) := + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := list_nth_mut_shared_loop_pair_loop_fwd T ls0 ls1 i /- [loops::list_nth_mut_shared_loop_pair] -/ 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) + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) := match ls0 with - | list_t.Cons x0 tl0 => + | List.Cons x0 tl0 => match ls1 with - | list_t.Cons x1 tl1 => + | List.Cons x1 tl1 => if i = (U32.ofInt 0 (by intlit)) - then Result.ret (list_t.Cons ret0 tl0) + then Result.ret (List.Cons ret0 tl0) else do let i0 ← i - (U32.ofInt 1 (by intlit)) let tl00 ← list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret0 - Result.ret (list_t.Cons x0 tl00) - | list_t.Nil => Result.fail Error.panic - | list_t.Nil => Result.fail Error.panic + Result.ret (List.Cons x0 tl00) + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [loops::list_nth_mut_shared_loop_pair] -/ def list_nth_mut_shared_loop_pair_back - (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) : - Result (list_t T) + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) := list_nth_mut_shared_loop_pair_loop_back T ls0 ls1 i ret0 /- [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) := + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := match ls0 with - | list_t.Cons x0 tl0 => + | List.Cons x0 tl0 => match ls1 with - | list_t.Cons x1 tl1 => + | List.Cons x1 tl1 => if i = (U32.ofInt 0 (by intlit)) then Result.ret (x0, x1) else do let i0 ← i - (U32.ofInt 1 (by intlit)) list_nth_mut_shared_loop_pair_merge_loop_fwd T tl0 tl1 i0 - | list_t.Nil => Result.fail Error.panic - | list_t.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [loops::list_nth_mut_shared_loop_pair_merge] -/ def list_nth_mut_shared_loop_pair_merge_fwd - (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) := + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := list_nth_mut_shared_loop_pair_merge_loop_fwd T ls0 ls1 i /- [loops::list_nth_mut_shared_loop_pair_merge] -/ 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) + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) := match ls0 with - | list_t.Cons x0 tl0 => + | List.Cons x0 tl0 => match ls1 with - | list_t.Cons x1 tl1 => + | List.Cons x1 tl1 => if i = (U32.ofInt 0 (by intlit)) - then Result.ret (list_t.Cons ret0 tl0) + then Result.ret (List.Cons ret0 tl0) else do let i0 ← i - (U32.ofInt 1 (by intlit)) let tl00 ← list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 - Result.ret (list_t.Cons x0 tl00) - | list_t.Nil => Result.fail Error.panic - | list_t.Nil => Result.fail Error.panic + Result.ret (List.Cons x0 tl00) + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [loops::list_nth_mut_shared_loop_pair_merge] -/ def list_nth_mut_shared_loop_pair_merge_back - (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) : - Result (list_t T) + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) := list_nth_mut_shared_loop_pair_merge_loop_back T ls0 ls1 i ret0 /- [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) := + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := match ls0 with - | list_t.Cons x0 tl0 => + | List.Cons x0 tl0 => match ls1 with - | list_t.Cons x1 tl1 => + | List.Cons x1 tl1 => if i = (U32.ofInt 0 (by intlit)) then Result.ret (x0, x1) else do let i0 ← i - (U32.ofInt 1 (by intlit)) list_nth_shared_mut_loop_pair_loop_fwd T tl0 tl1 i0 - | list_t.Nil => Result.fail Error.panic - | list_t.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [loops::list_nth_shared_mut_loop_pair] -/ def list_nth_shared_mut_loop_pair_fwd - (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) := + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := list_nth_shared_mut_loop_pair_loop_fwd T ls0 ls1 i /- [loops::list_nth_shared_mut_loop_pair] -/ 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) + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) := match ls0 with - | list_t.Cons x0 tl0 => + | List.Cons x0 tl0 => match ls1 with - | list_t.Cons x1 tl1 => + | List.Cons x1 tl1 => if i = (U32.ofInt 0 (by intlit)) - then Result.ret (list_t.Cons ret0 tl1) + then Result.ret (List.Cons ret0 tl1) else do let i0 ← i - (U32.ofInt 1 (by intlit)) let tl10 ← list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret0 - Result.ret (list_t.Cons x1 tl10) - | list_t.Nil => Result.fail Error.panic - | list_t.Nil => Result.fail Error.panic + Result.ret (List.Cons x1 tl10) + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [loops::list_nth_shared_mut_loop_pair] -/ def list_nth_shared_mut_loop_pair_back - (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) : - Result (list_t T) + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) := list_nth_shared_mut_loop_pair_loop_back T ls0 ls1 i ret0 /- [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) := + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := match ls0 with - | list_t.Cons x0 tl0 => + | List.Cons x0 tl0 => match ls1 with - | list_t.Cons x1 tl1 => + | List.Cons x1 tl1 => if i = (U32.ofInt 0 (by intlit)) then Result.ret (x0, x1) else do let i0 ← i - (U32.ofInt 1 (by intlit)) list_nth_shared_mut_loop_pair_merge_loop_fwd T tl0 tl1 i0 - | list_t.Nil => Result.fail Error.panic - | list_t.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [loops::list_nth_shared_mut_loop_pair_merge] -/ def list_nth_shared_mut_loop_pair_merge_fwd - (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) := + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := list_nth_shared_mut_loop_pair_merge_loop_fwd T ls0 ls1 i /- [loops::list_nth_shared_mut_loop_pair_merge] -/ 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) + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) := match ls0 with - | list_t.Cons x0 tl0 => + | List.Cons x0 tl0 => match ls1 with - | list_t.Cons x1 tl1 => + | List.Cons x1 tl1 => if i = (U32.ofInt 0 (by intlit)) - then Result.ret (list_t.Cons ret0 tl1) + then Result.ret (List.Cons ret0 tl1) else do let i0 ← i - (U32.ofInt 1 (by intlit)) let tl10 ← list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 - Result.ret (list_t.Cons x1 tl10) - | list_t.Nil => Result.fail Error.panic - | list_t.Nil => Result.fail Error.panic + Result.ret (List.Cons x1 tl10) + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [loops::list_nth_shared_mut_loop_pair_merge] -/ def list_nth_shared_mut_loop_pair_merge_back - (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) : - Result (list_t T) + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) := list_nth_shared_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0 diff --git a/tests/lean/Loops/Types.lean b/tests/lean/Loops/Types.lean index 5b5ed31f..f8bc193b 100644 --- a/tests/lean/Loops/Types.lean +++ b/tests/lean/Loops/Types.lean @@ -5,8 +5,8 @@ open Primitives namespace loops /- [loops::List] -/ -inductive list_t (T : Type) := -| Cons : T → list_t T → list_t T -| Nil : list_t T +inductive List (T : Type) := +| Cons : T → List T → List T +| Nil : List T end loops diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean index 67abc8f6..cdbbcd67 100644 --- a/tests/lean/NoNestedBorrows.lean +++ b/tests/lean/NoNestedBorrows.lean @@ -5,35 +5,35 @@ open Primitives namespace no_nested_borrows /- [no_nested_borrows::Pair] -/ -structure pair_t (T1 T2 : Type) where +structure Pair (T1 T2 : Type) where pair_x : T1 pair_y : T2 /- [no_nested_borrows::List] -/ -inductive list_t (T : Type) := -| Cons : T → list_t T → list_t T -| Nil : list_t T +inductive List (T : Type) := +| Cons : T → List T → List T +| Nil : List T /- [no_nested_borrows::One] -/ -inductive one_t (T1 : Type) := -| One : T1 → one_t T1 +inductive One (T1 : Type) := +| One : T1 → One T1 /- [no_nested_borrows::EmptyEnum] -/ -inductive empty_enum_t := -| Empty : empty_enum_t +inductive EmptyEnum := +| Empty : EmptyEnum /- [no_nested_borrows::Enum] -/ -inductive enum_t := -| Variant1 : enum_t -| Variant2 : enum_t +inductive Enum := +| Variant1 : Enum +| Variant2 : Enum /- [no_nested_borrows::EmptyStruct] -/ -structure empty_struct_t where +structure EmptyStruct where /- [no_nested_borrows::Sum] -/ -inductive sum_t (T1 T2 : Type) := -| Left : T1 → sum_t T1 T2 -| Right : T2 → sum_t T1 T2 +inductive Sum (T1 T2 : Type) := +| Left : T1 → Sum T1 T2 +| Right : T2 → Sum T1 T2 /- [no_nested_borrows::neg_test] -/ def neg_test_fwd (x : I32) : Result I32 := @@ -175,16 +175,16 @@ def test_copy_int_fwd : Result Unit := #assert (test_copy_int_fwd == .ret ()) /- [no_nested_borrows::is_cons] -/ -def is_cons_fwd (T : Type) (l : list_t T) : Result Bool := +def is_cons_fwd (T : Type) (l : List T) : Result Bool := match l with - | list_t.Cons t l0 => Result.ret true - | list_t.Nil => Result.ret false + | List.Cons t l0 => Result.ret true + | List.Nil => Result.ret false /- [no_nested_borrows::test_is_cons] -/ def test_is_cons_fwd : Result Unit := do - let l := list_t.Nil - let b ← is_cons_fwd I32 (list_t.Cons (I32.ofInt 0 (by intlit)) l) + let l := List.Nil + let b ← is_cons_fwd I32 (List.Cons (I32.ofInt 0 (by intlit)) l) if not b then Result.fail Error.panic else Result.ret () @@ -193,16 +193,16 @@ def test_is_cons_fwd : Result Unit := #assert (test_is_cons_fwd == .ret ()) /- [no_nested_borrows::split_list] -/ -def split_list_fwd (T : Type) (l : list_t T) : Result (T × (list_t T)) := +def split_list_fwd (T : Type) (l : List T) : Result (T × (List T)) := match l with - | list_t.Cons hd tl => Result.ret (hd, tl) - | list_t.Nil => Result.fail Error.panic + | List.Cons hd tl => Result.ret (hd, tl) + | List.Nil => Result.fail Error.panic /- [no_nested_borrows::test_split_list] -/ def test_split_list_fwd : Result Unit := do - let l := list_t.Nil - let p ← split_list_fwd I32 (list_t.Cons (I32.ofInt 0 (by intlit)) l) + let l := List.Nil + let p ← split_list_fwd I32 (List.Cons (I32.ofInt 0 (by intlit)) l) let (hd, _) := p if not (hd = (I32.ofInt 0 (by intlit))) then Result.fail Error.panic @@ -254,111 +254,110 @@ def test_char_fwd : Result Char := mutual /- [no_nested_borrows::NodeElem] -/ -inductive node_elem_t (T : Type) := -| Cons : tree_t T → node_elem_t T → node_elem_t T -| Nil : node_elem_t T +inductive NodeElem (T : Type) := +| Cons : Tree T → NodeElem T → NodeElem T +| Nil : NodeElem 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 +inductive Tree (T : Type) := +| Leaf : T → Tree T +| Node : T → NodeElem T → Tree T → Tree T end /- [no_nested_borrows::list_length] -/ -divergent def list_length_fwd (T : Type) (l : list_t T) : Result U32 := +divergent def list_length_fwd (T : Type) (l : List T) : Result U32 := match l with - | list_t.Cons t l1 => + | List.Cons t l1 => do let i ← list_length_fwd T l1 (U32.ofInt 1 (by intlit)) + i - | list_t.Nil => Result.ret (U32.ofInt 0 (by intlit)) + | List.Nil => Result.ret (U32.ofInt 0 (by intlit)) /- [no_nested_borrows::list_nth_shared] -/ divergent def list_nth_shared_fwd - (T : Type) (l : list_t T) (i : U32) : Result T := + (T : Type) (l : List T) (i : U32) : Result T := match l with - | list_t.Cons x tl => + | List.Cons x tl => if i = (U32.ofInt 0 (by intlit)) then Result.ret x else do let i0 ← i - (U32.ofInt 1 (by intlit)) list_nth_shared_fwd T tl i0 - | list_t.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [no_nested_borrows::list_nth_mut] -/ -divergent def list_nth_mut_fwd - (T : Type) (l : list_t T) (i : U32) : Result T := +divergent def list_nth_mut_fwd (T : Type) (l : List T) (i : U32) : Result T := match l with - | list_t.Cons x tl => + | List.Cons x tl => if i = (U32.ofInt 0 (by intlit)) then Result.ret x else do let i0 ← i - (U32.ofInt 1 (by intlit)) list_nth_mut_fwd T tl i0 - | list_t.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [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) := + (T : Type) (l : List T) (i : U32) (ret0 : T) : Result (List T) := match l with - | list_t.Cons x tl => + | List.Cons x tl => if i = (U32.ofInt 0 (by intlit)) - then Result.ret (list_t.Cons ret0 tl) + then Result.ret (List.Cons ret0 tl) else do let i0 ← i - (U32.ofInt 1 (by intlit)) let tl0 ← list_nth_mut_back T tl i0 ret0 - Result.ret (list_t.Cons x tl0) - | list_t.Nil => Result.fail Error.panic + Result.ret (List.Cons x tl0) + | List.Nil => Result.fail Error.panic /- [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) := + (T : Type) (li : List T) (lo : List T) : Result (List T) := 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 + | List.Cons hd tl => list_rev_aux_fwd T tl (List.Cons hd lo) + | List.Nil => Result.ret lo /- [no_nested_borrows::list_rev] -/ -def list_rev_fwd_back (T : Type) (l : list_t T) : Result (list_t T) := - let li := mem_replace_fwd (list_t T) l list_t.Nil - list_rev_aux_fwd T li list_t.Nil +def list_rev_fwd_back (T : Type) (l : List T) : Result (List T) := + let li := mem_replace_fwd (List T) l List.Nil + list_rev_aux_fwd T li List.Nil /- [no_nested_borrows::test_list_functions] -/ def test_list_functions_fwd : Result Unit := do - let l := list_t.Nil - let l0 := list_t.Cons (I32.ofInt 2 (by intlit)) l - let l1 := list_t.Cons (I32.ofInt 1 (by intlit)) l0 - let i ← list_length_fwd I32 (list_t.Cons (I32.ofInt 0 (by intlit)) l1) + let l := List.Nil + let l0 := List.Cons (I32.ofInt 2 (by intlit)) l + let l1 := List.Cons (I32.ofInt 1 (by intlit)) l0 + let i ← list_length_fwd I32 (List.Cons (I32.ofInt 0 (by intlit)) l1) if not (i = (U32.ofInt 3 (by intlit))) then Result.fail Error.panic else do let i0 ← - list_nth_shared_fwd I32 (list_t.Cons (I32.ofInt 0 (by intlit)) l1) + list_nth_shared_fwd I32 (List.Cons (I32.ofInt 0 (by intlit)) l1) (U32.ofInt 0 (by intlit)) if not (i0 = (I32.ofInt 0 (by intlit))) then Result.fail Error.panic else do let i1 ← - list_nth_shared_fwd I32 (list_t.Cons (I32.ofInt 0 (by intlit)) - l1) (U32.ofInt 1 (by intlit)) + list_nth_shared_fwd I32 (List.Cons (I32.ofInt 0 (by intlit)) l1) + (U32.ofInt 1 (by intlit)) if not (i1 = (I32.ofInt 1 (by intlit))) then Result.fail Error.panic else do let i2 ← - list_nth_shared_fwd I32 (list_t.Cons - (I32.ofInt 0 (by intlit)) l1) (U32.ofInt 2 (by intlit)) + list_nth_shared_fwd I32 (List.Cons (I32.ofInt 0 (by intlit)) + l1) (U32.ofInt 2 (by intlit)) if not (i2 = (I32.ofInt 2 (by intlit))) then Result.fail Error.panic else do let ls ← - list_nth_mut_back I32 (list_t.Cons + list_nth_mut_back I32 (List.Cons (I32.ofInt 0 (by intlit)) l1) (U32.ofInt 1 (by intlit)) (I32.ofInt 3 (by intlit)) let i3 ← @@ -434,11 +433,11 @@ def id_mut_pair4_back'b Result.ret ret0 /- [no_nested_borrows::StructWithTuple] -/ -structure struct_with_tuple_t (T1 T2 : Type) where +structure StructWithTuple (T1 T2 : Type) where struct_with_tuple_p : (T1 × T2) /- [no_nested_borrows::new_tuple1] -/ -def new_tuple1_fwd : Result (struct_with_tuple_t U32 U32) := +def new_tuple1_fwd : Result (StructWithTuple U32 U32) := Result.ret { struct_with_tuple_p := @@ -446,7 +445,7 @@ def new_tuple1_fwd : Result (struct_with_tuple_t U32 U32) := } /- [no_nested_borrows::new_tuple2] -/ -def new_tuple2_fwd : Result (struct_with_tuple_t I16 I16) := +def new_tuple2_fwd : Result (StructWithTuple I16 I16) := Result.ret { struct_with_tuple_p := @@ -454,7 +453,7 @@ def new_tuple2_fwd : Result (struct_with_tuple_t I16 I16) := } /- [no_nested_borrows::new_tuple3] -/ -def new_tuple3_fwd : Result (struct_with_tuple_t U64 I64) := +def new_tuple3_fwd : Result (StructWithTuple U64 I64) := Result.ret { struct_with_tuple_p := @@ -462,11 +461,11 @@ def new_tuple3_fwd : Result (struct_with_tuple_t U64 I64) := } /- [no_nested_borrows::StructWithPair] -/ -structure struct_with_pair_t (T1 T2 : Type) where - struct_with_pair_p : pair_t T1 T2 +structure StructWithPair (T1 T2 : Type) where + struct_with_pair_p : Pair T1 T2 /- [no_nested_borrows::new_pair1] -/ -def new_pair1_fwd : Result (struct_with_pair_t U32 U32) := +def new_pair1_fwd : Result (StructWithPair U32 U32) := Result.ret { struct_with_pair_p := @@ -531,10 +530,10 @@ def test_shared_borrow_bool2_fwd : Result U32 := Result.ret (U32.ofInt 0 (by intlit)) /- [no_nested_borrows::test_shared_borrow_enum1] -/ -def test_shared_borrow_enum1_fwd (l : list_t U32) : Result U32 := +def test_shared_borrow_enum1_fwd (l : List U32) : Result U32 := 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)) + | List.Cons i l0 => Result.ret (U32.ofInt 1 (by intlit)) + | List.Nil => Result.ret (U32.ofInt 0 (by intlit)) /- [no_nested_borrows::test_shared_borrow_enum2] -/ def test_shared_borrow_enum2_fwd : Result U32 := diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean index c34941ef..9f63b460 100644 --- a/tests/lean/Paper.lean +++ b/tests/lean/Paper.lean @@ -56,56 +56,55 @@ def test_choose_fwd : Result Unit := #assert (test_choose_fwd == .ret ()) /- [paper::List] -/ -inductive list_t (T : Type) := -| Cons : T → list_t T → list_t T -| Nil : list_t T +inductive List (T : Type) := +| Cons : T → List T → List T +| Nil : List T /- [paper::list_nth_mut] -/ -divergent def list_nth_mut_fwd - (T : Type) (l : list_t T) (i : U32) : Result T := +divergent def list_nth_mut_fwd (T : Type) (l : List T) (i : U32) : Result T := match l with - | list_t.Cons x tl => + | List.Cons x tl => if i = (U32.ofInt 0 (by intlit)) then Result.ret x else do let i0 ← i - (U32.ofInt 1 (by intlit)) list_nth_mut_fwd T tl i0 - | list_t.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic /- [paper::list_nth_mut] -/ divergent def list_nth_mut_back - (T : Type) (l : list_t T) (i : U32) (ret0 : T) : Result (list_t T) := + (T : Type) (l : List T) (i : U32) (ret0 : T) : Result (List T) := match l with - | list_t.Cons x tl => + | List.Cons x tl => if i = (U32.ofInt 0 (by intlit)) - then Result.ret (list_t.Cons ret0 tl) + then Result.ret (List.Cons ret0 tl) else do let i0 ← i - (U32.ofInt 1 (by intlit)) let tl0 ← list_nth_mut_back T tl i0 ret0 - Result.ret (list_t.Cons x tl0) - | list_t.Nil => Result.fail Error.panic + Result.ret (List.Cons x tl0) + | List.Nil => Result.fail Error.panic /- [paper::sum] -/ -divergent def sum_fwd (l : list_t I32) : Result I32 := +divergent def sum_fwd (l : List I32) : Result I32 := match l with - | list_t.Cons x tl => do - let i ← sum_fwd tl - x + i - | list_t.Nil => Result.ret (I32.ofInt 0 (by intlit)) + | List.Cons x tl => do + let i ← sum_fwd tl + x + i + | List.Nil => Result.ret (I32.ofInt 0 (by intlit)) /- [paper::test_nth] -/ def test_nth_fwd : Result Unit := do - let l := list_t.Nil - let l0 := list_t.Cons (I32.ofInt 3 (by intlit)) l - let l1 := list_t.Cons (I32.ofInt 2 (by intlit)) l0 + let l := List.Nil + let l0 := List.Cons (I32.ofInt 3 (by intlit)) l + let l1 := List.Cons (I32.ofInt 2 (by intlit)) l0 let x ← - list_nth_mut_fwd I32 (list_t.Cons (I32.ofInt 1 (by intlit)) l1) + list_nth_mut_fwd I32 (List.Cons (I32.ofInt 1 (by intlit)) l1) (U32.ofInt 2 (by intlit)) let x0 ← x + (I32.ofInt 1 (by intlit)) let l2 ← - list_nth_mut_back I32 (list_t.Cons (I32.ofInt 1 (by intlit)) l1) + list_nth_mut_back I32 (List.Cons (I32.ofInt 1 (by intlit)) l1) (U32.ofInt 2 (by intlit)) x0 let i ← sum_fwd l2 if not (i = (I32.ofInt 7 (by intlit))) diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean index 0ff01b47..1d7ec99b 100644 --- a/tests/lean/PoloniusList.lean +++ b/tests/lean/PoloniusList.lean @@ -5,31 +5,31 @@ open Primitives namespace polonius_list /- [polonius_list::List] -/ -inductive list_t (T : Type) := -| Cons : T → list_t T → list_t T -| Nil : list_t T +inductive List (T : Type) := +| Cons : T → List T → List T +| Nil : List T /- [polonius_list::get_list_at_x] -/ divergent def get_list_at_x_fwd - (ls : list_t U32) (x : U32) : Result (list_t U32) := + (ls : List U32) (x : U32) : Result (List U32) := match ls with - | list_t.Cons hd tl => + | List.Cons hd tl => if hd = x - then Result.ret (list_t.Cons hd tl) + then Result.ret (List.Cons hd tl) else get_list_at_x_fwd tl x - | list_t.Nil => Result.ret list_t.Nil + | List.Nil => Result.ret List.Nil /- [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) := + (ls : List U32) (x : U32) (ret0 : List U32) : Result (List U32) := match ls with - | list_t.Cons hd tl => + | List.Cons hd tl => if hd = x then Result.ret ret0 else do let tl0 ← get_list_at_x_back tl x ret0 - Result.ret (list_t.Cons hd tl0) - | list_t.Nil => Result.ret ret0 + Result.ret (List.Cons hd tl0) + | List.Nil => Result.ret ret0 end polonius_list |