diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/lean/betree/BetreeMain/Funs.lean | 324 | ||||
| -rw-r--r-- | tests/lean/betree/BetreeMain/Types.lean | 18 | ||||
| -rw-r--r-- | tests/lean/hashmap/Hashmap/Funs.lean | 69 | ||||
| -rw-r--r-- | tests/lean/hashmap/Hashmap/Types.lean | 4 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 102 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Types.lean | 4 | ||||
| -rw-r--r-- | tests/lean/misc-loops/Loops/Funs.lean | 200 | ||||
| -rw-r--r-- | tests/lean/misc-loops/Loops/Types.lean | 4 | ||||
| -rw-r--r-- | tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean | 90 | ||||
| -rw-r--r-- | tests/lean/misc-paper/Paper.lean | 39 | ||||
| -rw-r--r-- | tests/lean/misc-polonius_list/PoloniusList.lean | 16 |
11 files changed, 419 insertions, 451 deletions
diff --git a/tests/lean/betree/BetreeMain/Funs.lean b/tests/lean/betree/BetreeMain/Funs.lean index e161e066..7177e2ec 100644 --- a/tests/lean/betree/BetreeMain/Funs.lean +++ b/tests/lean/betree/BetreeMain/Funs.lean @@ -83,18 +83,18 @@ def betree_upsert_update_fwd match h: prev with | Option.none => match h: st with - | betree_upsert_fun_state_t.BetreeUpsertFunStateAdd v => Result.ret v - | betree_upsert_fun_state_t.BetreeUpsertFunStateSub i => + | betree_upsert_fun_state_t.Add v => Result.ret v + | betree_upsert_fun_state_t.Sub i => Result.ret (UInt64.ofNatCore 0 (by intlit)) | Option.some prev0 => match h: st with - | betree_upsert_fun_state_t.BetreeUpsertFunStateAdd v => + | betree_upsert_fun_state_t.Add v => do let margin ← UInt64.checked_sub core_num_u64_max_c prev0 if h: margin >= v then UInt64.checked_add prev0 v else Result.ret core_num_u64_max_c - | betree_upsert_fun_state_t.BetreeUpsertFunStateSub v => + | betree_upsert_fun_state_t.Sub v => if h: prev0 >= v then UInt64.checked_sub prev0 v else Result.ret (UInt64.ofNatCore 0 (by intlit)) @@ -103,11 +103,11 @@ def betree_upsert_update_fwd def betree_list_len_fwd (T : Type) (self : betree_list_t T) : (Result UInt64) := match h: self with - | betree_list_t.BetreeListCons t tl => + | betree_list_t.Cons t tl => do let i ← betree_list_len_fwd T tl UInt64.checked_add (UInt64.ofNatCore 1 (by intlit)) i - | betree_list_t.BetreeListNil => Result.ret (UInt64.ofNatCore 0 (by intlit)) + | betree_list_t.Nil => Result.ret (UInt64.ofNatCore 0 (by intlit)) termination_by betree_list_len_fwd self => betree_list_len_terminates T self decreasing_by betree_list_len_decreases self @@ -117,17 +117,17 @@ def betree_list_split_at_fwd (Result ((betree_list_t T) × (betree_list_t T))) := if h: n = (UInt64.ofNatCore 0 (by intlit)) - then Result.ret (betree_list_t.BetreeListNil, self) + then Result.ret (betree_list_t.Nil, self) else match h: self with - | betree_list_t.BetreeListCons hd tl => + | betree_list_t.Cons hd tl => do let i ← UInt64.checked_sub n (UInt64.ofNatCore 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.BetreeListCons hd l, ls1) - | betree_list_t.BetreeListNil => Result.fail Error.panic + Result.ret (betree_list_t.Cons hd l, ls1) + | betree_list_t.Nil => Result.fail Error.panic termination_by betree_list_split_at_fwd self n => betree_list_split_at_terminates T self n decreasing_by betree_list_split_at_decreases self n @@ -135,30 +135,30 @@ decreasing_by betree_list_split_at_decreases self n /- [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.BetreeListNil + let tl := mem_replace_fwd (betree_list_t T) self betree_list_t.Nil let l := tl - Result.ret (betree_list_t.BetreeListCons x l) + Result.ret (betree_list_t.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.BetreeListNil + let ls := mem_replace_fwd (betree_list_t T) self betree_list_t.Nil match h: ls with - | betree_list_t.BetreeListCons x tl => Result.ret x - | betree_list_t.BetreeListNil => Result.fail Error.panic + | betree_list_t.Cons x tl => Result.ret x + | betree_list_t.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.BetreeListNil + let ls := mem_replace_fwd (betree_list_t T) self betree_list_t.Nil match h: ls with - | betree_list_t.BetreeListCons x tl => Result.ret tl - | betree_list_t.BetreeListNil => Result.fail Error.panic + | betree_list_t.Cons x tl => Result.ret tl + | betree_list_t.Nil => Result.fail Error.panic /- [betree_main::betree::List::{1}::hd] -/ def betree_list_hd_fwd (T : Type) (self : betree_list_t T) : Result T := match h: self with - | betree_list_t.BetreeListCons hd l => Result.ret hd - | betree_list_t.BetreeListNil => Result.fail Error.panic + | betree_list_t.Cons hd l => Result.ret hd + | betree_list_t.Nil => Result.fail Error.panic /- [betree_main::betree::List::{2}::head_has_key] -/ def betree_list_head_has_key_fwd @@ -166,9 +166,9 @@ def betree_list_head_has_key_fwd Result Bool := match h: self with - | betree_list_t.BetreeListCons hd l => let (i, _) := hd - Result.ret (i = key) - | betree_list_t.BetreeListNil => Result.ret false + | betree_list_t.Cons hd l => let (i, _) := hd + Result.ret (i = key) + | betree_list_t.Nil => Result.ret false /- [betree_main::betree::List::{2}::partition_at_pivot] -/ def betree_list_partition_at_pivot_fwd @@ -176,20 +176,17 @@ def betree_list_partition_at_pivot_fwd (Result ((betree_list_t (UInt64 × T)) × (betree_list_t (UInt64 × T)))) := match h: self with - | betree_list_t.BetreeListCons hd tl => + | betree_list_t.Cons hd tl => let (i, t) := hd if h: i >= pivot - then - Result.ret (betree_list_t.BetreeListNil, betree_list_t.BetreeListCons (i, - t) tl) + then Result.ret (betree_list_t.Nil, betree_list_t.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.BetreeListCons (i, t) l, ls1) - | betree_list_t.BetreeListNil => - Result.ret (betree_list_t.BetreeListNil, betree_list_t.BetreeListNil) + Result.ret (betree_list_t.Cons (i, t) l, ls1) + | betree_list_t.Nil => Result.ret (betree_list_t.Nil, betree_list_t.Nil) termination_by betree_list_partition_at_pivot_fwd self pivot => betree_list_partition_at_pivot_terminates T self pivot decreasing_by betree_list_partition_at_pivot_decreases self pivot @@ -213,12 +210,12 @@ def betree_leaf_split_fwd let id1 ← betree_node_id_counter_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.BetreeNodeLeaf + let n := betree_node_t.Leaf { betree_leaf_id := id0, betree_leaf_size := params.betree_params_split_size } - let n0 := betree_node_t.BetreeNodeLeaf + let n0 := betree_node_t.Leaf { betree_leaf_id := id1, betree_leaf_size := params.betree_params_split_size @@ -251,7 +248,7 @@ def betree_node_lookup_in_bindings_fwd (Result (Option UInt64)) := match h: bindings with - | betree_list_t.BetreeListCons hd tl => + | betree_list_t.Cons hd tl => let (i, i0) := hd if h: i = key then Result.ret (Option.some i0) @@ -259,7 +256,7 @@ def betree_node_lookup_in_bindings_fwd if h: i > key then Result.ret Option.none else betree_node_lookup_in_bindings_fwd key tl - | betree_list_t.BetreeListNil => Result.ret Option.none + | betree_list_t.Nil => Result.ret Option.none termination_by betree_node_lookup_in_bindings_fwd key bindings => betree_node_lookup_in_bindings_terminates key bindings decreasing_by betree_node_lookup_in_bindings_decreases key bindings @@ -270,12 +267,12 @@ def betree_node_lookup_first_message_for_key_fwd (Result (betree_list_t (UInt64 × betree_message_t))) := match h: msgs with - | betree_list_t.BetreeListCons x next_msgs => + | betree_list_t.Cons x next_msgs => let (i, m) := x if h: i >= key - then Result.ret (betree_list_t.BetreeListCons (i, m) next_msgs) + then Result.ret (betree_list_t.Cons (i, m) next_msgs) else betree_node_lookup_first_message_for_key_fwd key next_msgs - | betree_list_t.BetreeListNil => Result.ret betree_list_t.BetreeListNil + | betree_list_t.Nil => Result.ret betree_list_t.Nil termination_by betree_node_lookup_first_message_for_key_fwd key msgs => betree_node_lookup_first_message_for_key_terminates key msgs decreasing_by betree_node_lookup_first_message_for_key_decreases key msgs @@ -287,7 +284,7 @@ def betree_node_lookup_first_message_for_key_back (Result (betree_list_t (UInt64 × betree_message_t))) := match h: msgs with - | betree_list_t.BetreeListCons x next_msgs => + | betree_list_t.Cons x next_msgs => let (i, m) := x if h: i >= key then Result.ret ret0 @@ -295,8 +292,8 @@ 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.BetreeListCons (i, m) next_msgs0) - | betree_list_t.BetreeListNil => Result.ret ret0 + Result.ret (betree_list_t.Cons (i, m) next_msgs0) + | betree_list_t.Nil => Result.ret ret0 termination_by betree_node_lookup_first_message_for_key_back key msgs ret0 => betree_node_lookup_first_message_for_key_terminates key msgs decreasing_by betree_node_lookup_first_message_for_key_decreases key msgs @@ -315,9 +312,9 @@ def betree_node_apply_upserts_fwd let msg ← betree_list_pop_front_fwd (UInt64 × betree_message_t) msgs let (_, m) := msg match h: m with - | betree_message_t.BetreeMessageInsert i => Result.fail Error.panic - | betree_message_t.BetreeMessageDelete => Result.fail Error.panic - | betree_message_t.BetreeMessageUpsert s => + | betree_message_t.Insert i => Result.fail Error.panic + | betree_message_t.Delete => Result.fail Error.panic + | betree_message_t.Upsert s => do let v ← betree_upsert_update_fwd prev s let msgs0 ← @@ -329,7 +326,7 @@ def betree_node_apply_upserts_fwd opaque_defs.core_option_option_unwrap_fwd UInt64 prev st let _ ← betree_list_push_front_fwd_back (UInt64 × betree_message_t) msgs - (key, betree_message_t.BetreeMessageInsert v) + (key, betree_message_t.Insert v) Result.ret (st0, v) termination_by betree_node_apply_upserts_fwd msgs prev key st => betree_node_apply_upserts_terminates msgs prev key st @@ -349,9 +346,9 @@ def betree_node_apply_upserts_back let msg ← betree_list_pop_front_fwd (UInt64 × betree_message_t) msgs let (_, m) := msg match h: m with - | betree_message_t.BetreeMessageInsert i => Result.fail Error.panic - | betree_message_t.BetreeMessageDelete => Result.fail Error.panic - | betree_message_t.BetreeMessageUpsert s => + | betree_message_t.Insert i => Result.fail Error.panic + | betree_message_t.Delete => Result.fail Error.panic + | betree_message_t.Upsert s => do let v ← betree_upsert_update_fwd prev s let msgs0 ← @@ -361,7 +358,7 @@ def betree_node_apply_upserts_back do let (_, v) ← opaque_defs.core_option_option_unwrap_fwd UInt64 prev st betree_list_push_front_fwd_back (UInt64 × betree_message_t) msgs (key, - betree_message_t.BetreeMessageInsert v) + betree_message_t.Insert v) termination_by betree_node_apply_upserts_back msgs prev key st => betree_node_apply_upserts_terminates msgs prev key st decreasing_by betree_node_apply_upserts_decreases msgs prev key st @@ -372,13 +369,13 @@ mutual def betree_node_lookup_fwd (Result (State × (Option UInt64))) := match h: self with - | betree_node_t.BetreeNodeInternal node => + | betree_node_t.Internal node => do let (mkbetree_internal_t i i0 n n0) := node let (st0, msgs) ← betree_load_internal_node_fwd i st let pending ← betree_node_lookup_first_message_for_key_fwd key msgs match h: pending with - | betree_list_t.BetreeListCons p l => + | betree_list_t.Cons p l => let (k, msg) := p if h: k != key then @@ -388,53 +385,51 @@ mutual def betree_node_lookup_fwd n n0) key st0 let _ ← betree_node_lookup_first_message_for_key_back key msgs - (betree_list_t.BetreeListCons (k, msg) l) + (betree_list_t.Cons (k, msg) l) Result.ret (st1, opt) else match h: msg with - | betree_message_t.BetreeMessageInsert v => + | betree_message_t.Insert v => do let _ ← betree_node_lookup_first_message_for_key_back key msgs - (betree_list_t.BetreeListCons (k, - betree_message_t.BetreeMessageInsert v) l) + (betree_list_t.Cons (k, betree_message_t.Insert v) l) Result.ret (st0, Option.some v) - | betree_message_t.BetreeMessageDelete => + | betree_message_t.Delete => do let _ ← betree_node_lookup_first_message_for_key_back key msgs - (betree_list_t.BetreeListCons (k, - betree_message_t.BetreeMessageDelete) l) + (betree_list_t.Cons (k, betree_message_t.Delete) l) Result.ret (st0, Option.none) - | betree_message_t.BetreeMessageUpsert ufs => + | betree_message_t.Upsert ufs => do let (st1, v) ← betree_internal_lookup_in_children_fwd (mkbetree_internal_t i i0 n n0) key st0 let (st2, v0) ← - betree_node_apply_upserts_fwd (betree_list_t.BetreeListCons (k, - betree_message_t.BetreeMessageUpsert ufs) l) v key st1 + betree_node_apply_upserts_fwd (betree_list_t.Cons (k, + betree_message_t.Upsert ufs) l) v key st1 let node0 ← betree_internal_lookup_in_children_back (mkbetree_internal_t i i0 n n0) key st0 let (mkbetree_internal_t i1 _ _ _) := node0 let pending0 ← - betree_node_apply_upserts_back (betree_list_t.BetreeListCons - (k, betree_message_t.BetreeMessageUpsert ufs) l) v key st1 + betree_node_apply_upserts_back (betree_list_t.Cons (k, + betree_message_t.Upsert ufs) l) v key st1 let msgs0 ← betree_node_lookup_first_message_for_key_back key msgs pending0 let (st3, _) ← betree_store_internal_node_fwd i1 msgs0 st2 Result.ret (st3, Option.some v0) - | betree_list_t.BetreeListNil => + | betree_list_t.Nil => do let (st1, opt) ← betree_internal_lookup_in_children_fwd (mkbetree_internal_t i i0 n n0) key st0 let _ ← betree_node_lookup_first_message_for_key_back key msgs - betree_list_t.BetreeListNil + betree_list_t.Nil Result.ret (st1, opt) - | betree_node_t.BetreeNodeLeaf node => + | betree_node_t.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 @@ -449,76 +444,74 @@ def betree_node_lookup_back (Result betree_node_t) := match h: self with - | betree_node_t.BetreeNodeInternal node => + | betree_node_t.Internal node => do let (mkbetree_internal_t i i0 n n0) := node let (st0, msgs) ← betree_load_internal_node_fwd i st let pending ← betree_node_lookup_first_message_for_key_fwd key msgs match h: pending with - | betree_list_t.BetreeListCons p l => + | betree_list_t.Cons p l => let (k, msg) := p if h: k != key then do let _ ← betree_node_lookup_first_message_for_key_back key msgs - (betree_list_t.BetreeListCons (k, msg) l) + (betree_list_t.Cons (k, msg) l) let node0 ← betree_internal_lookup_in_children_back (mkbetree_internal_t i i0 n n0) key st0 - Result.ret (betree_node_t.BetreeNodeInternal node0) + Result.ret (betree_node_t.Internal node0) else match h: msg with - | betree_message_t.BetreeMessageInsert v => + | betree_message_t.Insert v => do let _ ← betree_node_lookup_first_message_for_key_back key msgs - (betree_list_t.BetreeListCons (k, - betree_message_t.BetreeMessageInsert v) l) - Result.ret (betree_node_t.BetreeNodeInternal (mkbetree_internal_t - i i0 n n0)) - | betree_message_t.BetreeMessageDelete => + (betree_list_t.Cons (k, betree_message_t.Insert v) l) + Result.ret (betree_node_t.Internal (mkbetree_internal_t i i0 n + n0)) + | betree_message_t.Delete => do let _ ← betree_node_lookup_first_message_for_key_back key msgs - (betree_list_t.BetreeListCons (k, - betree_message_t.BetreeMessageDelete) l) - Result.ret (betree_node_t.BetreeNodeInternal (mkbetree_internal_t - i i0 n n0)) - | betree_message_t.BetreeMessageUpsert ufs => + (betree_list_t.Cons (k, betree_message_t.Delete) l) + Result.ret (betree_node_t.Internal (mkbetree_internal_t i i0 n + n0)) + | betree_message_t.Upsert ufs => do let (st1, v) ← betree_internal_lookup_in_children_fwd (mkbetree_internal_t i i0 n n0) key st0 let (st2, _) ← - betree_node_apply_upserts_fwd (betree_list_t.BetreeListCons (k, - betree_message_t.BetreeMessageUpsert ufs) l) v key st1 + betree_node_apply_upserts_fwd (betree_list_t.Cons (k, + betree_message_t.Upsert ufs) l) v key st1 let node0 ← betree_internal_lookup_in_children_back (mkbetree_internal_t i i0 n n0) key st0 let (mkbetree_internal_t i1 i2 n1 n2) := node0 let pending0 ← - betree_node_apply_upserts_back (betree_list_t.BetreeListCons - (k, betree_message_t.BetreeMessageUpsert ufs) l) v key st1 + betree_node_apply_upserts_back (betree_list_t.Cons (k, + betree_message_t.Upsert ufs) l) v key st1 let msgs0 ← betree_node_lookup_first_message_for_key_back key msgs pending0 let _ ← betree_store_internal_node_fwd i1 msgs0 st2 - Result.ret (betree_node_t.BetreeNodeInternal (mkbetree_internal_t - i1 i2 n1 n2)) - | betree_list_t.BetreeListNil => + Result.ret (betree_node_t.Internal (mkbetree_internal_t i1 i2 n1 + n2)) + | betree_list_t.Nil => do let _ ← betree_node_lookup_first_message_for_key_back key msgs - betree_list_t.BetreeListNil + betree_list_t.Nil let node0 ← betree_internal_lookup_in_children_back (mkbetree_internal_t i i0 n n0) key st0 - Result.ret (betree_node_t.BetreeNodeInternal node0) - | betree_node_t.BetreeNodeLeaf node => + Result.ret (betree_node_t.Internal node0) + | betree_node_t.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.BetreeNodeLeaf node) + Result.ret (betree_node_t.Leaf node) termination_by betree_node_lookup_back self key st => betree_node_lookup_terminates self key st decreasing_by betree_node_lookup_decreases self key st @@ -561,12 +554,12 @@ def betree_node_lookup_mut_in_bindings_fwd (Result (betree_list_t (UInt64 × UInt64))) := match h: bindings with - | betree_list_t.BetreeListCons hd tl => + | betree_list_t.Cons hd tl => let (i, i0) := hd if h: i >= key - then Result.ret (betree_list_t.BetreeListCons (i, i0) tl) + then Result.ret (betree_list_t.Cons (i, i0) tl) else betree_node_lookup_mut_in_bindings_fwd key tl - | betree_list_t.BetreeListNil => Result.ret betree_list_t.BetreeListNil + | betree_list_t.Nil => Result.ret betree_list_t.Nil termination_by betree_node_lookup_mut_in_bindings_fwd key bindings => betree_node_lookup_mut_in_bindings_terminates key bindings decreasing_by betree_node_lookup_mut_in_bindings_decreases key bindings @@ -578,15 +571,15 @@ def betree_node_lookup_mut_in_bindings_back (Result (betree_list_t (UInt64 × UInt64))) := match h: bindings with - | betree_list_t.BetreeListCons hd tl => + | betree_list_t.Cons hd tl => let (i, i0) := hd if h: 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.BetreeListCons (i, i0) tl0) - | betree_list_t.BetreeListNil => Result.ret ret0 + Result.ret (betree_list_t.Cons (i, i0) tl0) + | betree_list_t.Nil => Result.ret ret0 termination_by betree_node_lookup_mut_in_bindings_back key bindings ret0 => betree_node_lookup_mut_in_bindings_terminates key bindings decreasing_by betree_node_lookup_mut_in_bindings_decreases key bindings @@ -605,7 +598,7 @@ def betree_node_apply_to_leaf_fwd_back do let hd ← betree_list_pop_front_fwd (UInt64 × UInt64) bindings0 match h: new_msg with - | betree_message_t.BetreeMessageInsert v => + | betree_message_t.Insert v => do let bindings1 ← betree_list_pop_front_back (UInt64 × UInt64) bindings0 @@ -613,12 +606,12 @@ def betree_node_apply_to_leaf_fwd_back betree_list_push_front_fwd_back (UInt64 × UInt64) bindings1 (key, v) betree_node_lookup_mut_in_bindings_back key bindings bindings2 - | betree_message_t.BetreeMessageDelete => + | betree_message_t.Delete => do let bindings1 ← betree_list_pop_front_back (UInt64 × UInt64) bindings0 betree_node_lookup_mut_in_bindings_back key bindings bindings1 - | betree_message_t.BetreeMessageUpsert s => + | betree_message_t.Upsert s => do let (_, i) := hd let v ← betree_upsert_update_fwd (Option.some i) s @@ -630,15 +623,15 @@ def betree_node_apply_to_leaf_fwd_back betree_node_lookup_mut_in_bindings_back key bindings bindings2 else match h: new_msg with - | betree_message_t.BetreeMessageInsert v => + | betree_message_t.Insert v => do let bindings1 ← betree_list_push_front_fwd_back (UInt64 × UInt64) bindings0 (key, v) betree_node_lookup_mut_in_bindings_back key bindings bindings1 - | betree_message_t.BetreeMessageDelete => + | betree_message_t.Delete => betree_node_lookup_mut_in_bindings_back key bindings bindings0 - | betree_message_t.BetreeMessageUpsert s => + | betree_message_t.Upsert s => do let v ← betree_upsert_update_fwd Option.none s let bindings1 ← @@ -653,12 +646,12 @@ def betree_node_apply_messages_to_leaf_fwd_back (Result (betree_list_t (UInt64 × UInt64))) := match h: new_msgs with - | betree_list_t.BetreeListCons new_msg new_msgs_tl => + | betree_list_t.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.BetreeListNil => Result.ret bindings + | betree_list_t.Nil => Result.ret bindings termination_by betree_node_apply_messages_to_leaf_fwd_back bindings new_msgs => betree_node_apply_messages_to_leaf_terminates bindings new_msgs decreasing_by betree_node_apply_messages_to_leaf_decreases bindings new_msgs @@ -669,17 +662,17 @@ def betree_node_filter_messages_for_key_fwd_back (Result (betree_list_t (UInt64 × betree_message_t))) := match h: msgs with - | betree_list_t.BetreeListCons p l => + | betree_list_t.Cons p l => let (k, m) := p if h: k = key then do let msgs0 ← betree_list_pop_front_back (UInt64 × betree_message_t) - (betree_list_t.BetreeListCons (k, m) l) + (betree_list_t.Cons (k, m) l) betree_node_filter_messages_for_key_fwd_back key msgs0 - else Result.ret (betree_list_t.BetreeListCons (k, m) l) - | betree_list_t.BetreeListNil => Result.ret betree_list_t.BetreeListNil + else Result.ret (betree_list_t.Cons (k, m) l) + | betree_list_t.Nil => Result.ret betree_list_t.Nil termination_by betree_node_filter_messages_for_key_fwd_back key msgs => betree_node_filter_messages_for_key_terminates key msgs decreasing_by betree_node_filter_messages_for_key_decreases key msgs @@ -690,12 +683,12 @@ def betree_node_lookup_first_message_after_key_fwd (Result (betree_list_t (UInt64 × betree_message_t))) := match h: msgs with - | betree_list_t.BetreeListCons p next_msgs => + | betree_list_t.Cons p next_msgs => let (k, m) := p if h: k = key then betree_node_lookup_first_message_after_key_fwd key next_msgs - else Result.ret (betree_list_t.BetreeListCons (k, m) next_msgs) - | betree_list_t.BetreeListNil => Result.ret betree_list_t.BetreeListNil + else Result.ret (betree_list_t.Cons (k, m) next_msgs) + | betree_list_t.Nil => Result.ret betree_list_t.Nil termination_by betree_node_lookup_first_message_after_key_fwd key msgs => betree_node_lookup_first_message_after_key_terminates key msgs decreasing_by betree_node_lookup_first_message_after_key_decreases key msgs @@ -707,16 +700,16 @@ def betree_node_lookup_first_message_after_key_back (Result (betree_list_t (UInt64 × betree_message_t))) := match h: msgs with - | betree_list_t.BetreeListCons p next_msgs => + | betree_list_t.Cons p next_msgs => let (k, m) := p if h: k = key then do let next_msgs0 ← betree_node_lookup_first_message_after_key_back key next_msgs ret0 - Result.ret (betree_list_t.BetreeListCons (k, m) next_msgs0) + Result.ret (betree_list_t.Cons (k, m) next_msgs0) else Result.ret ret0 - | betree_list_t.BetreeListNil => Result.ret ret0 + | betree_list_t.Nil => Result.ret ret0 termination_by betree_node_lookup_first_message_after_key_back key msgs ret0 => betree_node_lookup_first_message_after_key_terminates key msgs decreasing_by betree_node_lookup_first_message_after_key_decreases key msgs @@ -733,50 +726,50 @@ def betree_node_apply_to_internal_fwd_back if h: b then match h: new_msg with - | betree_message_t.BetreeMessageInsert i => + | betree_message_t.Insert i => do let msgs1 ← betree_node_filter_messages_for_key_fwd_back key msgs0 let msgs2 ← betree_list_push_front_fwd_back (UInt64 × betree_message_t) msgs1 - (key, betree_message_t.BetreeMessageInsert i) + (key, betree_message_t.Insert i) betree_node_lookup_first_message_for_key_back key msgs msgs2 - | betree_message_t.BetreeMessageDelete => + | betree_message_t.Delete => do let msgs1 ← betree_node_filter_messages_for_key_fwd_back key msgs0 let msgs2 ← betree_list_push_front_fwd_back (UInt64 × betree_message_t) msgs1 - (key, betree_message_t.BetreeMessageDelete) + (key, betree_message_t.Delete) betree_node_lookup_first_message_for_key_back key msgs msgs2 - | betree_message_t.BetreeMessageUpsert s => + | betree_message_t.Upsert s => do let p ← betree_list_hd_fwd (UInt64 × betree_message_t) msgs0 let (_, m) := p match h: m with - | betree_message_t.BetreeMessageInsert prev => + | betree_message_t.Insert prev => do let v ← betree_upsert_update_fwd (Option.some prev) s let msgs1 ← betree_list_pop_front_back (UInt64 × betree_message_t) msgs0 let msgs2 ← betree_list_push_front_fwd_back (UInt64 × betree_message_t) - msgs1 (key, betree_message_t.BetreeMessageInsert v) + msgs1 (key, betree_message_t.Insert v) betree_node_lookup_first_message_for_key_back key msgs msgs2 - | betree_message_t.BetreeMessageDelete => + | betree_message_t.Delete => do let v ← betree_upsert_update_fwd Option.none s let msgs1 ← betree_list_pop_front_back (UInt64 × betree_message_t) msgs0 let msgs2 ← betree_list_push_front_fwd_back (UInt64 × betree_message_t) - msgs1 (key, betree_message_t.BetreeMessageInsert v) + msgs1 (key, betree_message_t.Insert v) betree_node_lookup_first_message_for_key_back key msgs msgs2 - | betree_message_t.BetreeMessageUpsert ufs => + | betree_message_t.Upsert ufs => do let msgs1 ← betree_node_lookup_first_message_after_key_fwd key msgs0 let msgs2 ← betree_list_push_front_fwd_back (UInt64 × betree_message_t) - msgs1 (key, betree_message_t.BetreeMessageUpsert s) + msgs1 (key, betree_message_t.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 @@ -794,12 +787,12 @@ def betree_node_apply_messages_to_internal_fwd_back (Result (betree_list_t (UInt64 × betree_message_t))) := match h: new_msgs with - | betree_list_t.BetreeListCons new_msg new_msgs_tl => + | betree_list_t.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.BetreeListNil => Result.ret msgs + | betree_list_t.Nil => Result.ret msgs termination_by betree_node_apply_messages_to_internal_fwd_back msgs new_msgs => betree_node_apply_messages_to_internal_terminates msgs new_msgs decreasing_by betree_node_apply_messages_to_internal_decreases msgs new_msgs @@ -812,7 +805,7 @@ mutual def betree_node_apply_messages_fwd (Result (State × Unit)) := match h: self with - | betree_node_t.BetreeNodeInternal node => + | betree_node_t.Internal node => do let (mkbetree_internal_t i i0 n n0) := node let (st0, content) ← betree_load_internal_node_fwd i st @@ -836,7 +829,7 @@ mutual def betree_node_apply_messages_fwd do let (st1, _) ← betree_store_internal_node_fwd i content0 st0 Result.ret (st1, ()) - | betree_node_t.BetreeNodeLeaf node => + | betree_node_t.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 @@ -849,8 +842,8 @@ mutual 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.BetreeListNil st1 + betree_store_leaf_node_fwd node.betree_leaf_id betree_list_t.Nil + st1 Result.ret (st2, ()) else do @@ -871,7 +864,7 @@ def betree_node_apply_messages_back (Result (betree_node_t × betree_node_id_counter_t)) := match h: self with - | betree_node_t.BetreeNodeInternal node => + | betree_node_t.Internal node => do let (mkbetree_internal_t i i0 n n0) := node let (st0, content) ← betree_load_internal_node_fwd i st @@ -890,14 +883,14 @@ def betree_node_apply_messages_back node_id_cnt content0 st0 let (mkbetree_internal_t i1 i2 n1 n2) := node0 let _ ← betree_store_internal_node_fwd i1 content1 st1 - Result.ret (betree_node_t.BetreeNodeInternal (mkbetree_internal_t i1 - i2 n1 n2), node_id_cnt0) + Result.ret (betree_node_t.Internal (mkbetree_internal_t i1 i2 n1 n2), + node_id_cnt0) else do let _ ← betree_store_internal_node_fwd i content0 st0 - Result.ret (betree_node_t.BetreeNodeInternal (mkbetree_internal_t i - i0 n n0), node_id_cnt) - | betree_node_t.BetreeNodeLeaf node => + Result.ret (betree_node_t.Internal (mkbetree_internal_t i i0 n n0), + node_id_cnt) + | betree_node_t.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 @@ -910,16 +903,16 @@ 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.BetreeListNil st1 + betree_store_leaf_node_fwd node.betree_leaf_id betree_list_t.Nil + st1 let node_id_cnt0 ← betree_leaf_split_back node content0 params node_id_cnt st0 - Result.ret (betree_node_t.BetreeNodeInternal new_node, node_id_cnt0) + Result.ret (betree_node_t.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.BetreeNodeLeaf - { node with betree_leaf_size := len }, node_id_cnt) + Result.ret (betree_node_t.Leaf { node with betree_leaf_size := len }, + node_id_cnt) termination_by betree_node_apply_messages_back self params node_id_cnt msgs st => betree_node_apply_messages_terminates self params node_id_cnt msgs st @@ -956,7 +949,7 @@ 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.BetreeListNil) + Result.ret (st1, betree_list_t.Nil) else Result.ret (st0, msgs_right) else do @@ -1017,13 +1010,13 @@ def betree_node_apply_fwd Result (State × Unit) := do - let l := betree_list_t.BetreeListNil + let l := betree_list_t.Nil let (st0, _) ← betree_node_apply_messages_fwd self params node_id_cnt - (betree_list_t.BetreeListCons (key, new_msg) l) st + (betree_list_t.Cons (key, new_msg) l) st let _ ← betree_node_apply_messages_back self params node_id_cnt - (betree_list_t.BetreeListCons (key, new_msg) l) st + (betree_list_t.Cons (key, new_msg) l) st Result.ret (st0, ()) /- [betree_main::betree::Node::{5}::apply] -/ @@ -1033,9 +1026,9 @@ def betree_node_apply_back (new_msg : betree_message_t) (st : State) : Result (betree_node_t × betree_node_id_counter_t) := - let l := betree_list_t.BetreeListNil - betree_node_apply_messages_back self params node_id_cnt - (betree_list_t.BetreeListCons (key, new_msg) l) st + let l := betree_list_t.Nil + betree_node_apply_messages_back self params node_id_cnt (betree_list_t.Cons + (key, new_msg) l) st /- [betree_main::betree::BeTree::{6}::new] -/ def betree_be_tree_new_fwd @@ -1045,8 +1038,7 @@ def betree_be_tree_new_fwd do let node_id_cnt ← betree_node_id_counter_new_fwd let id ← betree_node_id_counter_fresh_id_fwd node_id_cnt - let (st0, _) ← - betree_store_leaf_node_fwd id betree_list_t.BetreeListNil st + let (st0, _) ← betree_store_leaf_node_fwd id betree_list_t.Nil st let node_id_cnt0 ← betree_node_id_counter_fresh_id_back node_id_cnt Result.ret (st0, { @@ -1057,7 +1049,7 @@ def betree_be_tree_new_fwd }, betree_be_tree_node_id_cnt := node_id_cnt0, betree_be_tree_root := - (betree_node_t.BetreeNodeLeaf + (betree_node_t.Leaf { betree_leaf_id := id, betree_leaf_size := (UInt64.ofNatCore 0 (by intlit)) @@ -1099,11 +1091,9 @@ def betree_be_tree_insert_fwd := do let (st0, _) ← - betree_be_tree_apply_fwd self key (betree_message_t.BetreeMessageInsert - value) st + betree_be_tree_apply_fwd self key (betree_message_t.Insert value) st let _ ← - betree_be_tree_apply_back self key (betree_message_t.BetreeMessageInsert - value) st + betree_be_tree_apply_back self key (betree_message_t.Insert value) st Result.ret (st0, ()) /- [betree_main::betree::BeTree::{6}::insert] -/ @@ -1111,8 +1101,7 @@ def betree_be_tree_insert_back (self : betree_be_tree_t) (key : UInt64) (value : UInt64) (st : State) : Result betree_be_tree_t := - betree_be_tree_apply_back self key (betree_message_t.BetreeMessageInsert - value) st + betree_be_tree_apply_back self key (betree_message_t.Insert value) st /- [betree_main::betree::BeTree::{6}::delete] -/ def betree_be_tree_delete_fwd @@ -1121,10 +1110,8 @@ def betree_be_tree_delete_fwd := do let (st0, _) ← - betree_be_tree_apply_fwd self key betree_message_t.BetreeMessageDelete st - let _ ← - betree_be_tree_apply_back self key betree_message_t.BetreeMessageDelete - st + betree_be_tree_apply_fwd self key betree_message_t.Delete st + let _ ← betree_be_tree_apply_back self key betree_message_t.Delete st Result.ret (st0, ()) /- [betree_main::betree::BeTree::{6}::delete] -/ @@ -1132,7 +1119,7 @@ def betree_be_tree_delete_back (self : betree_be_tree_t) (key : UInt64) (st : State) : Result betree_be_tree_t := - betree_be_tree_apply_back self key betree_message_t.BetreeMessageDelete st + betree_be_tree_apply_back self key betree_message_t.Delete st /- [betree_main::betree::BeTree::{6}::upsert] -/ def betree_be_tree_upsert_fwd @@ -1142,11 +1129,9 @@ def betree_be_tree_upsert_fwd := do let (st0, _) ← - betree_be_tree_apply_fwd self key (betree_message_t.BetreeMessageUpsert - upd) st + betree_be_tree_apply_fwd self key (betree_message_t.Upsert upd) st let _ ← - betree_be_tree_apply_back self key (betree_message_t.BetreeMessageUpsert - upd) st + betree_be_tree_apply_back self key (betree_message_t.Upsert upd) st Result.ret (st0, ()) /- [betree_main::betree::BeTree::{6}::upsert] -/ @@ -1155,8 +1140,7 @@ def betree_be_tree_upsert_back (st : State) : Result betree_be_tree_t := - betree_be_tree_apply_back self key (betree_message_t.BetreeMessageUpsert upd) - st + betree_be_tree_apply_back self key (betree_message_t.Upsert upd) st /- [betree_main::betree::BeTree::{6}::lookup] -/ def betree_be_tree_lookup_fwd diff --git a/tests/lean/betree/BetreeMain/Types.lean b/tests/lean/betree/BetreeMain/Types.lean index e2e6c867..32634e30 100644 --- a/tests/lean/betree/BetreeMain/Types.lean +++ b/tests/lean/betree/BetreeMain/Types.lean @@ -4,19 +4,19 @@ import Base.Primitives /- [betree_main::betree::List] -/ inductive betree_list_t (T : Type) := -| BetreeListCons : T -> betree_list_t T -> betree_list_t T -| BetreeListNil : betree_list_t T +| Cons : T -> betree_list_t T -> betree_list_t T +| Nil : betree_list_t T /- [betree_main::betree::UpsertFunState] -/ inductive betree_upsert_fun_state_t := -| BetreeUpsertFunStateAdd : UInt64 -> betree_upsert_fun_state_t -| BetreeUpsertFunStateSub : UInt64 -> betree_upsert_fun_state_t +| Add : UInt64 -> betree_upsert_fun_state_t +| Sub : UInt64 -> betree_upsert_fun_state_t /- [betree_main::betree::Message] -/ inductive betree_message_t := -| BetreeMessageInsert : UInt64 -> betree_message_t -| BetreeMessageDelete : betree_message_t -| BetreeMessageUpsert : betree_upsert_fun_state_t -> betree_message_t +| Insert : UInt64 -> betree_message_t +| Delete : betree_message_t +| Upsert : betree_upsert_fun_state_t -> betree_message_t /- [betree_main::betree::Leaf] -/ structure betree_leaf_t where @@ -25,8 +25,8 @@ structure betree_leaf_t where /- [betree_main::betree::Node] -/ mutual inductive betree_node_t := -| BetreeNodeInternal : betree_internal_t -> betree_node_t -| BetreeNodeLeaf : betree_leaf_t -> betree_node_t +| Internal : betree_internal_t -> betree_node_t +| Leaf : betree_leaf_t -> betree_node_t /- [betree_main::betree::Internal] -/ inductive betree_internal_t := diff --git a/tests/lean/hashmap/Hashmap/Funs.lean b/tests/lean/hashmap/Hashmap/Funs.lean index 0d83b04d..535ac9b2 100644 --- a/tests/lean/hashmap/Hashmap/Funs.lean +++ b/tests/lean/hashmap/Hashmap/Funs.lean @@ -16,7 +16,7 @@ def hash_map_allocate_slots_loop_fwd if h: n > (USize.ofNatCore 0 (by intlit)) then do - let slots0 ← vec_push_back (list_t T) slots list_t.ListNil + let slots0 ← vec_push_back (list_t T) slots list_t.Nil let n0 ← USize.checked_sub n (USize.ofNatCore 1 (by intlit)) hash_map_allocate_slots_loop_fwd T slots0 n0 else Result.ret slots @@ -63,7 +63,7 @@ def hash_map_clear_loop_fwd_back then do let i1 ← USize.checked_add i (USize.ofNatCore 1 (by intlit)) - let slots0 ← vec_index_mut_back (list_t T) slots i list_t.ListNil + let slots0 ← vec_index_mut_back (list_t T) slots i list_t.Nil hash_map_clear_loop_fwd_back T slots0 i1 else Result.ret slots termination_by hash_map_clear_loop_fwd_back slots i => @@ -93,11 +93,11 @@ def hash_map_len_fwd (T : Type) (self : hash_map_t T) : Result USize := def hash_map_insert_in_list_loop_fwd (T : Type) (key : USize) (value : T) (ls : list_t T) : (Result Bool) := match h: ls with - | list_t.ListCons ckey cvalue tl => + | list_t.Cons ckey cvalue tl => if h: ckey = key then Result.ret false else hash_map_insert_in_list_loop_fwd T key value tl - | list_t.ListNil => Result.ret true + | list_t.Nil => Result.ret true termination_by hash_map_insert_in_list_loop_fwd key value ls => hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hash_map_insert_in_list_loop_decreases key value ls @@ -111,16 +111,15 @@ def hash_map_insert_in_list_fwd def hash_map_insert_in_list_loop_back (T : Type) (key : USize) (value : T) (ls : list_t T) : (Result (list_t T)) := match h: ls with - | list_t.ListCons ckey cvalue tl => + | list_t.Cons ckey cvalue tl => if h: ckey = key - then Result.ret (list_t.ListCons ckey value tl) + then Result.ret (list_t.Cons ckey value tl) else do let tl0 ← hash_map_insert_in_list_loop_back T key value tl - Result.ret (list_t.ListCons ckey cvalue tl0) - | list_t.ListNil => - let l := list_t.ListNil - Result.ret (list_t.ListCons key value l) + Result.ret (list_t.Cons ckey cvalue tl0) + | list_t.Nil => let l := list_t.Nil + Result.ret (list_t.Cons key value l) termination_by hash_map_insert_in_list_loop_back key value ls => hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hash_map_insert_in_list_loop_decreases key value ls @@ -167,11 +166,11 @@ def hash_map_move_elements_from_list_loop_fwd_back (Result (hash_map_t T)) := match h: ls with - | list_t.ListCons k v tl => + | list_t.Cons k v tl => do let ntable0 ← hash_map_insert_no_resize_fwd_back T ntable k v hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl - | list_t.ListNil => Result.ret ntable + | list_t.Nil => Result.ret ntable termination_by hash_map_move_elements_from_list_loop_fwd_back ntable ls => hash_map_move_elements_from_list_loop_terminates T ntable ls decreasing_by hash_map_move_elements_from_list_loop_decreases ntable ls @@ -191,10 +190,10 @@ def hash_map_move_elements_loop_fwd_back then do let l ← vec_index_mut_fwd (list_t T) slots i - let ls := mem_replace_fwd (list_t T) l list_t.ListNil + let ls := mem_replace_fwd (list_t T) l list_t.Nil let ntable0 ← hash_map_move_elements_from_list_fwd_back T ntable ls let i1 ← USize.checked_add i (USize.ofNatCore 1 (by intlit)) - let l0 := mem_replace_back (list_t T) l list_t.ListNil + let l0 := mem_replace_back (list_t T) l list_t.Nil let slots0 ← vec_index_mut_back (list_t T) slots i l0 hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1 else Result.ret (ntable, slots) @@ -251,11 +250,11 @@ def hash_map_insert_fwd_back def hash_map_contains_key_in_list_loop_fwd (T : Type) (key : USize) (ls : list_t T) : (Result Bool) := match h: ls with - | list_t.ListCons ckey t tl => + | list_t.Cons ckey t tl => if h: ckey = key then Result.ret true else hash_map_contains_key_in_list_loop_fwd T key tl - | list_t.ListNil => Result.ret false + | list_t.Nil => Result.ret false termination_by hash_map_contains_key_in_list_loop_fwd key ls => hash_map_contains_key_in_list_loop_terminates T key ls decreasing_by hash_map_contains_key_in_list_loop_decreases key ls @@ -279,11 +278,11 @@ def hash_map_contains_key_fwd def hash_map_get_in_list_loop_fwd (T : Type) (key : USize) (ls : list_t T) : (Result T) := match h: ls with - | list_t.ListCons ckey cvalue tl => + | list_t.Cons ckey cvalue tl => if h: ckey = key then Result.ret cvalue else hash_map_get_in_list_loop_fwd T key tl - | list_t.ListNil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by hash_map_get_in_list_loop_fwd key ls => hash_map_get_in_list_loop_terminates T key ls decreasing_by hash_map_get_in_list_loop_decreases key ls @@ -307,11 +306,11 @@ def hash_map_get_fwd def hash_map_get_mut_in_list_loop_fwd (T : Type) (ls : list_t T) (key : USize) : (Result T) := match h: ls with - | list_t.ListCons ckey cvalue tl => + | list_t.Cons ckey cvalue tl => if h: ckey = key then Result.ret cvalue else hash_map_get_mut_in_list_loop_fwd T tl key - | list_t.ListNil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by hash_map_get_mut_in_list_loop_fwd ls key => hash_map_get_mut_in_list_loop_terminates T ls key decreasing_by hash_map_get_mut_in_list_loop_decreases ls key @@ -325,14 +324,14 @@ def hash_map_get_mut_in_list_fwd def hash_map_get_mut_in_list_loop_back (T : Type) (ls : list_t T) (key : USize) (ret0 : T) : (Result (list_t T)) := match h: ls with - | list_t.ListCons ckey cvalue tl => + | list_t.Cons ckey cvalue tl => if h: ckey = key - then Result.ret (list_t.ListCons ckey ret0 tl) + then Result.ret (list_t.Cons ckey ret0 tl) else do let tl0 ← hash_map_get_mut_in_list_loop_back T tl key ret0 - Result.ret (list_t.ListCons ckey cvalue tl0) - | list_t.ListNil => Result.fail Error.panic + Result.ret (list_t.Cons ckey cvalue tl0) + | list_t.Nil => Result.fail Error.panic termination_by hash_map_get_mut_in_list_loop_back ls key ret0 => hash_map_get_mut_in_list_loop_terminates T ls key decreasing_by hash_map_get_mut_in_list_loop_decreases ls key @@ -370,16 +369,16 @@ def hash_map_get_mut_back def hash_map_remove_from_list_loop_fwd (T : Type) (key : USize) (ls : list_t T) : (Result (Option T)) := match h: ls with - | list_t.ListCons ckey t tl => + | list_t.Cons ckey t tl => if h: ckey = key then let mv_ls := - mem_replace_fwd (list_t T) (list_t.ListCons ckey t tl) list_t.ListNil + mem_replace_fwd (list_t T) (list_t.Cons ckey t tl) list_t.Nil match h: mv_ls with - | list_t.ListCons i cvalue tl0 => Result.ret (Option.some cvalue) - | list_t.ListNil => Result.fail Error.panic + | list_t.Cons i cvalue tl0 => Result.ret (Option.some cvalue) + | list_t.Nil => Result.fail Error.panic else hash_map_remove_from_list_loop_fwd T key tl - | list_t.ListNil => Result.ret Option.none + | list_t.Nil => Result.ret Option.none termination_by hash_map_remove_from_list_loop_fwd key ls => hash_map_remove_from_list_loop_terminates T key ls decreasing_by hash_map_remove_from_list_loop_decreases key ls @@ -393,19 +392,19 @@ def hash_map_remove_from_list_fwd def hash_map_remove_from_list_loop_back (T : Type) (key : USize) (ls : list_t T) : (Result (list_t T)) := match h: ls with - | list_t.ListCons ckey t tl => + | list_t.Cons ckey t tl => if h: ckey = key then let mv_ls := - mem_replace_fwd (list_t T) (list_t.ListCons ckey t tl) list_t.ListNil + mem_replace_fwd (list_t T) (list_t.Cons ckey t tl) list_t.Nil match h: mv_ls with - | list_t.ListCons i cvalue tl0 => Result.ret tl0 - | list_t.ListNil => Result.fail Error.panic + | list_t.Cons i cvalue tl0 => Result.ret tl0 + | list_t.Nil => Result.fail Error.panic else do let tl0 ← hash_map_remove_from_list_loop_back T key tl - Result.ret (list_t.ListCons ckey t tl0) - | list_t.ListNil => Result.ret list_t.ListNil + Result.ret (list_t.Cons ckey t tl0) + | list_t.Nil => Result.ret list_t.Nil termination_by hash_map_remove_from_list_loop_back key ls => hash_map_remove_from_list_loop_terminates T key ls decreasing_by hash_map_remove_from_list_loop_decreases key ls diff --git a/tests/lean/hashmap/Hashmap/Types.lean b/tests/lean/hashmap/Hashmap/Types.lean index dd2be633..9e9e5c03 100644 --- a/tests/lean/hashmap/Hashmap/Types.lean +++ b/tests/lean/hashmap/Hashmap/Types.lean @@ -4,8 +4,8 @@ import Base.Primitives /- [hashmap::List] -/ inductive list_t (T : Type) := -| ListCons : USize -> T -> list_t T -> list_t T -| ListNil : list_t T +| Cons : USize -> T -> list_t T -> list_t T +| Nil : list_t T /- [hashmap::HashMap] -/ structure hash_map_t (T : Type) where diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index bf3a30e9..2be03d98 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -19,8 +19,7 @@ def hashmap_hash_map_allocate_slots_loop_fwd if h: n > (USize.ofNatCore 0 (by intlit)) then do - let slots0 ← - vec_push_back (hashmap_list_t T) slots hashmap_list_t.HashmapListNil + let slots0 ← vec_push_back (hashmap_list_t T) slots hashmap_list_t.Nil let n0 ← USize.checked_sub n (USize.ofNatCore 1 (by intlit)) hashmap_hash_map_allocate_slots_loop_fwd T slots0 n0 else Result.ret slots @@ -60,8 +59,8 @@ def hashmap_hash_map_new_fwd (T : Type) : Result (hashmap_hash_map_t T) := hashmap_hash_map_new_with_capacity_fwd T (USize.ofNatCore 32 (by intlit)) (USize.ofNatCore 4 (by intlit)) (USize.ofNatCore 5 (by intlit)) -/- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/ -def hashmap_hash_map_clear_slots_loop_fwd_back +/- [hashmap_main::hashmap::HashMap::{0}::clear] -/ +def hashmap_hash_map_clear_loop_fwd_back (T : Type) (slots : Vec (hashmap_list_t T)) (i : USize) : (Result (Vec (hashmap_list_t T))) := @@ -71,28 +70,20 @@ def hashmap_hash_map_clear_slots_loop_fwd_back do let i1 ← USize.checked_add i (USize.ofNatCore 1 (by intlit)) let slots0 ← - vec_index_mut_back (hashmap_list_t T) slots i - hashmap_list_t.HashmapListNil - hashmap_hash_map_clear_slots_loop_fwd_back T slots0 i1 + vec_index_mut_back (hashmap_list_t T) slots i hashmap_list_t.Nil + hashmap_hash_map_clear_loop_fwd_back T slots0 i1 else Result.ret slots -termination_by hashmap_hash_map_clear_slots_loop_fwd_back slots i => - hashmap_hash_map_clear_slots_loop_terminates T slots i -decreasing_by hashmap_hash_map_clear_slots_loop_decreases slots i - -/- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/ -def hashmap_hash_map_clear_slots_fwd_back - (T : Type) (slots : Vec (hashmap_list_t T)) : - Result (Vec (hashmap_list_t T)) - := - hashmap_hash_map_clear_slots_loop_fwd_back T slots - (USize.ofNatCore 0 (by intlit)) +termination_by hashmap_hash_map_clear_loop_fwd_back slots i => + hashmap_hash_map_clear_loop_terminates T slots i +decreasing_by hashmap_hash_map_clear_loop_decreases slots i /- [hashmap_main::hashmap::HashMap::{0}::clear] -/ def hashmap_hash_map_clear_fwd_back (T : Type) (self : hashmap_hash_map_t T) : Result (hashmap_hash_map_t T) := do let v ← - hashmap_hash_map_clear_slots_fwd_back T self.hashmap_hash_map_slots + hashmap_hash_map_clear_loop_fwd_back T self.hashmap_hash_map_slots + (USize.ofNatCore 0 (by intlit)) Result.ret { self @@ -112,11 +103,11 @@ def hashmap_hash_map_insert_in_list_loop_fwd (Result Bool) := match h: ls with - | hashmap_list_t.HashmapListCons ckey cvalue tl => + | hashmap_list_t.Cons ckey cvalue tl => if h: ckey = key then Result.ret false else hashmap_hash_map_insert_in_list_loop_fwd T key value tl - | hashmap_list_t.HashmapListNil => Result.ret true + | hashmap_list_t.Nil => Result.ret true termination_by hashmap_hash_map_insert_in_list_loop_fwd key value ls => hashmap_hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hashmap_hash_map_insert_in_list_loop_decreases key value ls @@ -132,16 +123,16 @@ def hashmap_hash_map_insert_in_list_loop_back (Result (hashmap_list_t T)) := match h: ls with - | hashmap_list_t.HashmapListCons ckey cvalue tl => + | hashmap_list_t.Cons ckey cvalue tl => if h: ckey = key - then Result.ret (hashmap_list_t.HashmapListCons ckey value tl) + then Result.ret (hashmap_list_t.Cons ckey value tl) else do let tl0 ← hashmap_hash_map_insert_in_list_loop_back T key value tl - Result.ret (hashmap_list_t.HashmapListCons ckey cvalue tl0) - | hashmap_list_t.HashmapListNil => - let l := hashmap_list_t.HashmapListNil - Result.ret (hashmap_list_t.HashmapListCons key value l) + 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) termination_by hashmap_hash_map_insert_in_list_loop_back key value ls => hashmap_hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hashmap_hash_map_insert_in_list_loop_decreases key value ls @@ -199,11 +190,11 @@ def hashmap_hash_map_move_elements_from_list_loop_fwd_back (Result (hashmap_hash_map_t T)) := match h: ls with - | hashmap_list_t.HashmapListCons k v tl => + | hashmap_list_t.Cons k v tl => do let ntable0 ← hashmap_hash_map_insert_no_resize_fwd_back T ntable k v hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl - | hashmap_list_t.HashmapListNil => Result.ret ntable + | hashmap_list_t.Nil => Result.ret ntable termination_by hashmap_hash_map_move_elements_from_list_loop_fwd_back ntable ls => hashmap_hash_map_move_elements_from_list_loop_terminates T ntable ls @@ -227,13 +218,11 @@ def hashmap_hash_map_move_elements_loop_fwd_back 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.HashmapListNil + let ls := mem_replace_fwd (hashmap_list_t T) l hashmap_list_t.Nil let ntable0 ← hashmap_hash_map_move_elements_from_list_fwd_back T ntable ls let i1 ← USize.checked_add i (USize.ofNatCore 1 (by intlit)) - let l0 := - mem_replace_back (hashmap_list_t T) l hashmap_list_t.HashmapListNil + 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 hashmap_hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1 else Result.ret (ntable, slots) @@ -291,11 +280,11 @@ def hashmap_hash_map_insert_fwd_back def hashmap_hash_map_contains_key_in_list_loop_fwd (T : Type) (key : USize) (ls : hashmap_list_t T) : (Result Bool) := match h: ls with - | hashmap_list_t.HashmapListCons ckey t tl => + | hashmap_list_t.Cons ckey t tl => if h: ckey = key then Result.ret true else hashmap_hash_map_contains_key_in_list_loop_fwd T key tl - | hashmap_list_t.HashmapListNil => Result.ret false + | hashmap_list_t.Nil => Result.ret false termination_by hashmap_hash_map_contains_key_in_list_loop_fwd key ls => hashmap_hash_map_contains_key_in_list_loop_terminates T key ls decreasing_by hashmap_hash_map_contains_key_in_list_loop_decreases key ls @@ -320,11 +309,11 @@ def hashmap_hash_map_contains_key_fwd def hashmap_hash_map_get_in_list_loop_fwd (T : Type) (key : USize) (ls : hashmap_list_t T) : (Result T) := match h: ls with - | hashmap_list_t.HashmapListCons ckey cvalue tl => + | hashmap_list_t.Cons ckey cvalue tl => if h: ckey = key then Result.ret cvalue else hashmap_hash_map_get_in_list_loop_fwd T key tl - | hashmap_list_t.HashmapListNil => Result.fail Error.panic + | hashmap_list_t.Nil => Result.fail Error.panic termination_by hashmap_hash_map_get_in_list_loop_fwd key ls => hashmap_hash_map_get_in_list_loop_terminates T key ls decreasing_by hashmap_hash_map_get_in_list_loop_decreases key ls @@ -349,11 +338,11 @@ def hashmap_hash_map_get_fwd def hashmap_hash_map_get_mut_in_list_loop_fwd (T : Type) (ls : hashmap_list_t T) (key : USize) : (Result T) := match h: ls with - | hashmap_list_t.HashmapListCons ckey cvalue tl => + | hashmap_list_t.Cons ckey cvalue tl => if h: ckey = key then Result.ret cvalue else hashmap_hash_map_get_mut_in_list_loop_fwd T tl key - | hashmap_list_t.HashmapListNil => Result.fail Error.panic + | hashmap_list_t.Nil => Result.fail Error.panic termination_by hashmap_hash_map_get_mut_in_list_loop_fwd ls key => hashmap_hash_map_get_mut_in_list_loop_terminates T ls key decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key @@ -369,14 +358,14 @@ def hashmap_hash_map_get_mut_in_list_loop_back (Result (hashmap_list_t T)) := match h: ls with - | hashmap_list_t.HashmapListCons ckey cvalue tl => + | hashmap_list_t.Cons ckey cvalue tl => if h: ckey = key - then Result.ret (hashmap_list_t.HashmapListCons ckey ret0 tl) + then Result.ret (hashmap_list_t.Cons ckey ret0 tl) else do let tl0 ← hashmap_hash_map_get_mut_in_list_loop_back T tl key ret0 - Result.ret (hashmap_list_t.HashmapListCons ckey cvalue tl0) - | hashmap_list_t.HashmapListNil => Result.fail Error.panic + Result.ret (hashmap_list_t.Cons ckey cvalue tl0) + | hashmap_list_t.Nil => Result.fail Error.panic termination_by hashmap_hash_map_get_mut_in_list_loop_back ls key ret0 => hashmap_hash_map_get_mut_in_list_loop_terminates T ls key decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key @@ -420,18 +409,17 @@ def hashmap_hash_map_get_mut_back def hashmap_hash_map_remove_from_list_loop_fwd (T : Type) (key : USize) (ls : hashmap_list_t T) : (Result (Option T)) := match h: ls with - | hashmap_list_t.HashmapListCons ckey t tl => + | hashmap_list_t.Cons ckey t tl => if h: ckey = key then let mv_ls := - mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.HashmapListCons ckey - t tl) hashmap_list_t.HashmapListNil + mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.Cons ckey t tl) + hashmap_list_t.Nil match h: mv_ls with - | hashmap_list_t.HashmapListCons i cvalue tl0 => - Result.ret (Option.some cvalue) - | hashmap_list_t.HashmapListNil => Result.fail Error.panic + | hashmap_list_t.Cons i cvalue tl0 => Result.ret (Option.some cvalue) + | hashmap_list_t.Nil => Result.fail Error.panic else hashmap_hash_map_remove_from_list_loop_fwd T key tl - | hashmap_list_t.HashmapListNil => Result.ret Option.none + | hashmap_list_t.Nil => Result.ret Option.none termination_by hashmap_hash_map_remove_from_list_loop_fwd key ls => hashmap_hash_map_remove_from_list_loop_terminates T key ls decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls @@ -447,20 +435,20 @@ def hashmap_hash_map_remove_from_list_loop_back (Result (hashmap_list_t T)) := match h: ls with - | hashmap_list_t.HashmapListCons ckey t tl => + | hashmap_list_t.Cons ckey t tl => if h: ckey = key then let mv_ls := - mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.HashmapListCons ckey - t tl) hashmap_list_t.HashmapListNil + mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.Cons ckey t tl) + hashmap_list_t.Nil match h: mv_ls with - | hashmap_list_t.HashmapListCons i cvalue tl0 => Result.ret tl0 - | hashmap_list_t.HashmapListNil => Result.fail Error.panic + | hashmap_list_t.Cons i cvalue tl0 => Result.ret tl0 + | hashmap_list_t.Nil => Result.fail Error.panic else do let tl0 ← hashmap_hash_map_remove_from_list_loop_back T key tl - Result.ret (hashmap_list_t.HashmapListCons ckey t tl0) - | hashmap_list_t.HashmapListNil => Result.ret hashmap_list_t.HashmapListNil + Result.ret (hashmap_list_t.Cons ckey t tl0) + | hashmap_list_t.Nil => Result.ret hashmap_list_t.Nil termination_by hashmap_hash_map_remove_from_list_loop_back key ls => hashmap_hash_map_remove_from_list_loop_terminates T key ls decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean index fbab1bcd..989dd2a9 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean @@ -4,8 +4,8 @@ import Base.Primitives /- [hashmap_main::hashmap::List] -/ inductive hashmap_list_t (T : Type) := -| HashmapListCons : USize -> T -> hashmap_list_t T -> hashmap_list_t T -| HashmapListNil : hashmap_list_t T +| Cons : USize -> T -> hashmap_list_t T -> hashmap_list_t T +| Nil : hashmap_list_t T /- [hashmap_main::hashmap::HashMap] -/ structure hashmap_hash_map_t (T : Type) where diff --git a/tests/lean/misc-loops/Loops/Funs.lean b/tests/lean/misc-loops/Loops/Funs.lean index 5a81ebff..f79a27a9 100644 --- a/tests/lean/misc-loops/Loops/Funs.lean +++ b/tests/lean/misc-loops/Loops/Funs.lean @@ -79,11 +79,11 @@ def clear_fwd_back (v : Vec UInt32) : Result (Vec UInt32) := /- [loops::list_mem] -/ def list_mem_loop_fwd (x : UInt32) (ls : list_t UInt32) : (Result Bool) := match h: ls with - | list_t.ListCons y tl => + | list_t.Cons y tl => if h: y = x then Result.ret true else list_mem_loop_fwd x tl - | list_t.ListNil => Result.ret false + | list_t.Nil => Result.ret false termination_by list_mem_loop_fwd x ls => list_mem_loop_terminates x ls decreasing_by list_mem_loop_decreases x ls @@ -95,14 +95,14 @@ def list_mem_fwd (x : UInt32) (ls : list_t UInt32) : Result Bool := def list_nth_mut_loop_loop_fwd (T : Type) (ls : list_t T) (i : UInt32) : (Result T) := match h: ls with - | list_t.ListCons x tl => + | list_t.Cons x tl => if h: i = (UInt32.ofNatCore 0 (by intlit)) then Result.ret x else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_mut_loop_loop_fwd T tl i0 - | list_t.ListNil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by list_nth_mut_loop_loop_fwd ls i => list_nth_mut_loop_loop_terminates T ls i decreasing_by list_nth_mut_loop_loop_decreases ls i @@ -115,15 +115,15 @@ def list_nth_mut_loop_fwd (T : Type) (ls : list_t T) (i : UInt32) : Result T := def list_nth_mut_loop_loop_back (T : Type) (ls : list_t T) (i : UInt32) (ret0 : T) : (Result (list_t T)) := match h: ls with - | list_t.ListCons x tl => + | list_t.Cons x tl => if h: i = (UInt32.ofNatCore 0 (by intlit)) - then Result.ret (list_t.ListCons ret0 tl) + then Result.ret (list_t.Cons ret0 tl) else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) let tl0 ← list_nth_mut_loop_loop_back T tl i0 ret0 - Result.ret (list_t.ListCons x tl0) - | list_t.ListNil => Result.fail Error.panic + Result.ret (list_t.Cons x tl0) + | list_t.Nil => Result.fail Error.panic termination_by list_nth_mut_loop_loop_back ls i ret0 => list_nth_mut_loop_loop_terminates T ls i decreasing_by list_nth_mut_loop_loop_decreases ls i @@ -137,14 +137,14 @@ def list_nth_mut_loop_back def list_nth_shared_loop_loop_fwd (T : Type) (ls : list_t T) (i : UInt32) : (Result T) := match h: ls with - | list_t.ListCons x tl => + | list_t.Cons x tl => if h: i = (UInt32.ofNatCore 0 (by intlit)) then Result.ret x else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_shared_loop_loop_fwd T tl i0 - | list_t.ListNil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by list_nth_shared_loop_loop_fwd ls i => list_nth_shared_loop_loop_terminates T ls i decreasing_by list_nth_shared_loop_loop_decreases ls i @@ -157,11 +157,11 @@ def list_nth_shared_loop_fwd /- [loops::get_elem_mut] -/ def get_elem_mut_loop_fwd (x : USize) (ls : list_t USize) : (Result USize) := match h: ls with - | list_t.ListCons y tl => + | list_t.Cons y tl => if h: y = x then Result.ret y else get_elem_mut_loop_fwd x tl - | list_t.ListNil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by get_elem_mut_loop_fwd x ls => get_elem_mut_loop_terminates x ls decreasing_by get_elem_mut_loop_decreases x ls @@ -176,14 +176,14 @@ def get_elem_mut_fwd (slots : Vec (list_t USize)) (x : USize) : Result USize := def get_elem_mut_loop_back (x : USize) (ls : list_t USize) (ret0 : USize) : (Result (list_t USize)) := match h: ls with - | list_t.ListCons y tl => + | list_t.Cons y tl => if h: y = x - then Result.ret (list_t.ListCons ret0 tl) + then Result.ret (list_t.Cons ret0 tl) else do let tl0 ← get_elem_mut_loop_back x tl ret0 - Result.ret (list_t.ListCons y tl0) - | list_t.ListNil => Result.fail Error.panic + Result.ret (list_t.Cons y tl0) + | list_t.Nil => Result.fail Error.panic termination_by get_elem_mut_loop_back x ls ret0 => get_elem_mut_loop_terminates x ls decreasing_by get_elem_mut_loop_decreases x ls @@ -203,11 +203,11 @@ def get_elem_mut_back def get_elem_shared_loop_fwd (x : USize) (ls : list_t USize) : (Result USize) := match h: ls with - | list_t.ListCons y tl => + | list_t.Cons y tl => if h: y = x then Result.ret y else get_elem_shared_loop_fwd x tl - | list_t.ListNil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by get_elem_shared_loop_fwd x ls => get_elem_shared_loop_terminates x ls decreasing_by get_elem_shared_loop_decreases x ls @@ -237,14 +237,14 @@ def id_shared_fwd (T : Type) (ls : list_t T) : Result (list_t T) := def list_nth_mut_loop_with_id_loop_fwd (T : Type) (i : UInt32) (ls : list_t T) : (Result T) := match h: ls with - | list_t.ListCons x tl => + | list_t.Cons x tl => if h: i = (UInt32.ofNatCore 0 (by intlit)) then Result.ret x else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_mut_loop_with_id_loop_fwd T i0 tl - | list_t.ListNil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by list_nth_mut_loop_with_id_loop_fwd i ls => list_nth_mut_loop_with_id_loop_terminates T i ls decreasing_by list_nth_mut_loop_with_id_loop_decreases i ls @@ -260,15 +260,15 @@ def list_nth_mut_loop_with_id_fwd def list_nth_mut_loop_with_id_loop_back (T : Type) (i : UInt32) (ls : list_t T) (ret0 : T) : (Result (list_t T)) := match h: ls with - | list_t.ListCons x tl => + | list_t.Cons x tl => if h: i = (UInt32.ofNatCore 0 (by intlit)) - then Result.ret (list_t.ListCons ret0 tl) + then Result.ret (list_t.Cons ret0 tl) else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) let tl0 ← list_nth_mut_loop_with_id_loop_back T i0 tl ret0 - Result.ret (list_t.ListCons x tl0) - | list_t.ListNil => Result.fail Error.panic + Result.ret (list_t.Cons x tl0) + | list_t.Nil => Result.fail Error.panic termination_by list_nth_mut_loop_with_id_loop_back i ls ret0 => list_nth_mut_loop_with_id_loop_terminates T i ls decreasing_by list_nth_mut_loop_with_id_loop_decreases i ls @@ -285,14 +285,14 @@ def list_nth_mut_loop_with_id_back def list_nth_shared_loop_with_id_loop_fwd (T : Type) (i : UInt32) (ls : list_t T) : (Result T) := match h: ls with - | list_t.ListCons x tl => + | list_t.Cons x tl => if h: i = (UInt32.ofNatCore 0 (by intlit)) then Result.ret x else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_shared_loop_with_id_loop_fwd T i0 tl - | list_t.ListNil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by list_nth_shared_loop_with_id_loop_fwd i ls => list_nth_shared_loop_with_id_loop_terminates T i ls decreasing_by list_nth_shared_loop_with_id_loop_decreases i ls @@ -310,17 +310,17 @@ def list_nth_mut_loop_pair_loop_fwd (Result (T × T)) := match h: ls0 with - | list_t.ListCons x0 tl0 => + | list_t.Cons x0 tl0 => match h: ls1 with - | list_t.ListCons x1 tl1 => + | list_t.Cons x1 tl1 => if h: i = (UInt32.ofNatCore 0 (by intlit)) then Result.ret (x0, x1) else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_mut_loop_pair_loop_fwd T tl0 tl1 i0 - | list_t.ListNil => Result.fail Error.panic - | list_t.ListNil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by list_nth_mut_loop_pair_loop_fwd ls0 ls1 i => list_nth_mut_loop_pair_loop_terminates T ls0 ls1 i decreasing_by list_nth_mut_loop_pair_loop_decreases ls0 ls1 i @@ -338,18 +338,18 @@ def list_nth_mut_loop_pair_loop_back'a (Result (list_t T)) := match h: ls0 with - | list_t.ListCons x0 tl0 => + | list_t.Cons x0 tl0 => match h: ls1 with - | list_t.ListCons x1 tl1 => + | list_t.Cons x1 tl1 => if h: i = (UInt32.ofNatCore 0 (by intlit)) - then Result.ret (list_t.ListCons ret0 tl0) + then Result.ret (list_t.Cons ret0 tl0) else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) let tl00 ← list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret0 - Result.ret (list_t.ListCons x0 tl00) - | list_t.ListNil => Result.fail Error.panic - | list_t.ListNil => Result.fail Error.panic + Result.ret (list_t.Cons x0 tl00) + | list_t.Nil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by list_nth_mut_loop_pair_loop_back'a ls0 ls1 i ret0 => list_nth_mut_loop_pair_loop_terminates T ls0 ls1 i decreasing_by list_nth_mut_loop_pair_loop_decreases ls0 ls1 i @@ -367,18 +367,18 @@ def list_nth_mut_loop_pair_loop_back'b (Result (list_t T)) := match h: ls0 with - | list_t.ListCons x0 tl0 => + | list_t.Cons x0 tl0 => match h: ls1 with - | list_t.ListCons x1 tl1 => + | list_t.Cons x1 tl1 => if h: i = (UInt32.ofNatCore 0 (by intlit)) - then Result.ret (list_t.ListCons ret0 tl1) + then Result.ret (list_t.Cons ret0 tl1) else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) let tl10 ← list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret0 - Result.ret (list_t.ListCons x1 tl10) - | list_t.ListNil => Result.fail Error.panic - | list_t.ListNil => Result.fail Error.panic + Result.ret (list_t.Cons x1 tl10) + | list_t.Nil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by list_nth_mut_loop_pair_loop_back'b ls0 ls1 i ret0 => list_nth_mut_loop_pair_loop_terminates T ls0 ls1 i decreasing_by list_nth_mut_loop_pair_loop_decreases ls0 ls1 i @@ -396,17 +396,17 @@ def list_nth_shared_loop_pair_loop_fwd (Result (T × T)) := match h: ls0 with - | list_t.ListCons x0 tl0 => + | list_t.Cons x0 tl0 => match h: ls1 with - | list_t.ListCons x1 tl1 => + | list_t.Cons x1 tl1 => if h: i = (UInt32.ofNatCore 0 (by intlit)) then Result.ret (x0, x1) else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_shared_loop_pair_loop_fwd T tl0 tl1 i0 - | list_t.ListNil => Result.fail Error.panic - | list_t.ListNil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by list_nth_shared_loop_pair_loop_fwd ls0 ls1 i => list_nth_shared_loop_pair_loop_terminates T ls0 ls1 i decreasing_by list_nth_shared_loop_pair_loop_decreases ls0 ls1 i @@ -424,17 +424,17 @@ def list_nth_mut_loop_pair_merge_loop_fwd (Result (T × T)) := match h: ls0 with - | list_t.ListCons x0 tl0 => + | list_t.Cons x0 tl0 => match h: ls1 with - | list_t.ListCons x1 tl1 => + | list_t.Cons x1 tl1 => if h: i = (UInt32.ofNatCore 0 (by intlit)) then Result.ret (x0, x1) else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_mut_loop_pair_merge_loop_fwd T tl0 tl1 i0 - | list_t.ListNil => Result.fail Error.panic - | list_t.ListNil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by list_nth_mut_loop_pair_merge_loop_fwd ls0 ls1 i => list_nth_mut_loop_pair_merge_loop_terminates T ls0 ls1 i decreasing_by list_nth_mut_loop_pair_merge_loop_decreases ls0 ls1 i @@ -452,21 +452,21 @@ def list_nth_mut_loop_pair_merge_loop_back (Result ((list_t T) × (list_t T))) := match h: ls0 with - | list_t.ListCons x0 tl0 => + | list_t.Cons x0 tl0 => match h: ls1 with - | list_t.ListCons x1 tl1 => + | list_t.Cons x1 tl1 => if h: i = (UInt32.ofNatCore 0 (by intlit)) then let (t, t0) := ret0 - Result.ret (list_t.ListCons t tl0, list_t.ListCons t0 tl1) + Result.ret (list_t.Cons t tl0, list_t.Cons t0 tl1) else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) let (tl00, tl10) ← list_nth_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 - Result.ret (list_t.ListCons x0 tl00, list_t.ListCons x1 tl10) - | list_t.ListNil => Result.fail Error.panic - | list_t.ListNil => Result.fail Error.panic + 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 termination_by list_nth_mut_loop_pair_merge_loop_back ls0 ls1 i ret0 => list_nth_mut_loop_pair_merge_loop_terminates T ls0 ls1 i decreasing_by list_nth_mut_loop_pair_merge_loop_decreases ls0 ls1 i @@ -484,17 +484,17 @@ def list_nth_shared_loop_pair_merge_loop_fwd (Result (T × T)) := match h: ls0 with - | list_t.ListCons x0 tl0 => + | list_t.Cons x0 tl0 => match h: ls1 with - | list_t.ListCons x1 tl1 => + | list_t.Cons x1 tl1 => if h: i = (UInt32.ofNatCore 0 (by intlit)) then Result.ret (x0, x1) else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_shared_loop_pair_merge_loop_fwd T tl0 tl1 i0 - | list_t.ListNil => Result.fail Error.panic - | list_t.ListNil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by list_nth_shared_loop_pair_merge_loop_fwd ls0 ls1 i => list_nth_shared_loop_pair_merge_loop_terminates T ls0 ls1 i decreasing_by list_nth_shared_loop_pair_merge_loop_decreases ls0 ls1 i @@ -512,17 +512,17 @@ def list_nth_mut_shared_loop_pair_loop_fwd (Result (T × T)) := match h: ls0 with - | list_t.ListCons x0 tl0 => + | list_t.Cons x0 tl0 => match h: ls1 with - | list_t.ListCons x1 tl1 => + | list_t.Cons x1 tl1 => if h: i = (UInt32.ofNatCore 0 (by intlit)) then Result.ret (x0, x1) else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_mut_shared_loop_pair_loop_fwd T tl0 tl1 i0 - | list_t.ListNil => Result.fail Error.panic - | list_t.ListNil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by list_nth_mut_shared_loop_pair_loop_fwd ls0 ls1 i => list_nth_mut_shared_loop_pair_loop_terminates T ls0 ls1 i decreasing_by list_nth_mut_shared_loop_pair_loop_decreases ls0 ls1 i @@ -540,19 +540,19 @@ def list_nth_mut_shared_loop_pair_loop_back (Result (list_t T)) := match h: ls0 with - | list_t.ListCons x0 tl0 => + | list_t.Cons x0 tl0 => match h: ls1 with - | list_t.ListCons x1 tl1 => + | list_t.Cons x1 tl1 => if h: i = (UInt32.ofNatCore 0 (by intlit)) - then Result.ret (list_t.ListCons ret0 tl0) + then Result.ret (list_t.Cons ret0 tl0) else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) let tl00 ← list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret0 - Result.ret (list_t.ListCons x0 tl00) - | list_t.ListNil => Result.fail Error.panic - | list_t.ListNil => Result.fail Error.panic + Result.ret (list_t.Cons x0 tl00) + | list_t.Nil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by list_nth_mut_shared_loop_pair_loop_back ls0 ls1 i ret0 => list_nth_mut_shared_loop_pair_loop_terminates T ls0 ls1 i decreasing_by list_nth_mut_shared_loop_pair_loop_decreases ls0 ls1 i @@ -570,17 +570,17 @@ def list_nth_mut_shared_loop_pair_merge_loop_fwd (Result (T × T)) := match h: ls0 with - | list_t.ListCons x0 tl0 => + | list_t.Cons x0 tl0 => match h: ls1 with - | list_t.ListCons x1 tl1 => + | list_t.Cons x1 tl1 => if h: i = (UInt32.ofNatCore 0 (by intlit)) then Result.ret (x0, x1) else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_mut_shared_loop_pair_merge_loop_fwd T tl0 tl1 i0 - | list_t.ListNil => Result.fail Error.panic - | list_t.ListNil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by list_nth_mut_shared_loop_pair_merge_loop_fwd ls0 ls1 i => list_nth_mut_shared_loop_pair_merge_loop_terminates T ls0 ls1 i decreasing_by list_nth_mut_shared_loop_pair_merge_loop_decreases ls0 ls1 i @@ -598,19 +598,19 @@ def list_nth_mut_shared_loop_pair_merge_loop_back (Result (list_t T)) := match h: ls0 with - | list_t.ListCons x0 tl0 => + | list_t.Cons x0 tl0 => match h: ls1 with - | list_t.ListCons x1 tl1 => + | list_t.Cons x1 tl1 => if h: i = (UInt32.ofNatCore 0 (by intlit)) - then Result.ret (list_t.ListCons ret0 tl0) + then Result.ret (list_t.Cons ret0 tl0) else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) let tl00 ← list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 - Result.ret (list_t.ListCons x0 tl00) - | list_t.ListNil => Result.fail Error.panic - | list_t.ListNil => Result.fail Error.panic + Result.ret (list_t.Cons x0 tl00) + | list_t.Nil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by list_nth_mut_shared_loop_pair_merge_loop_back ls0 ls1 i ret0 => list_nth_mut_shared_loop_pair_merge_loop_terminates T ls0 ls1 i decreasing_by list_nth_mut_shared_loop_pair_merge_loop_decreases ls0 ls1 i @@ -628,17 +628,17 @@ def list_nth_shared_mut_loop_pair_loop_fwd (Result (T × T)) := match h: ls0 with - | list_t.ListCons x0 tl0 => + | list_t.Cons x0 tl0 => match h: ls1 with - | list_t.ListCons x1 tl1 => + | list_t.Cons x1 tl1 => if h: i = (UInt32.ofNatCore 0 (by intlit)) then Result.ret (x0, x1) else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_shared_mut_loop_pair_loop_fwd T tl0 tl1 i0 - | list_t.ListNil => Result.fail Error.panic - | list_t.ListNil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by list_nth_shared_mut_loop_pair_loop_fwd ls0 ls1 i => list_nth_shared_mut_loop_pair_loop_terminates T ls0 ls1 i decreasing_by list_nth_shared_mut_loop_pair_loop_decreases ls0 ls1 i @@ -656,19 +656,19 @@ def list_nth_shared_mut_loop_pair_loop_back (Result (list_t T)) := match h: ls0 with - | list_t.ListCons x0 tl0 => + | list_t.Cons x0 tl0 => match h: ls1 with - | list_t.ListCons x1 tl1 => + | list_t.Cons x1 tl1 => if h: i = (UInt32.ofNatCore 0 (by intlit)) - then Result.ret (list_t.ListCons ret0 tl1) + then Result.ret (list_t.Cons ret0 tl1) else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) let tl10 ← list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret0 - Result.ret (list_t.ListCons x1 tl10) - | list_t.ListNil => Result.fail Error.panic - | list_t.ListNil => Result.fail Error.panic + Result.ret (list_t.Cons x1 tl10) + | list_t.Nil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by list_nth_shared_mut_loop_pair_loop_back ls0 ls1 i ret0 => list_nth_shared_mut_loop_pair_loop_terminates T ls0 ls1 i decreasing_by list_nth_shared_mut_loop_pair_loop_decreases ls0 ls1 i @@ -686,17 +686,17 @@ def list_nth_shared_mut_loop_pair_merge_loop_fwd (Result (T × T)) := match h: ls0 with - | list_t.ListCons x0 tl0 => + | list_t.Cons x0 tl0 => match h: ls1 with - | list_t.ListCons x1 tl1 => + | list_t.Cons x1 tl1 => if h: i = (UInt32.ofNatCore 0 (by intlit)) then Result.ret (x0, x1) else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_shared_mut_loop_pair_merge_loop_fwd T tl0 tl1 i0 - | list_t.ListNil => Result.fail Error.panic - | list_t.ListNil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by list_nth_shared_mut_loop_pair_merge_loop_fwd ls0 ls1 i => list_nth_shared_mut_loop_pair_merge_loop_terminates T ls0 ls1 i decreasing_by list_nth_shared_mut_loop_pair_merge_loop_decreases ls0 ls1 i @@ -714,19 +714,19 @@ def list_nth_shared_mut_loop_pair_merge_loop_back (Result (list_t T)) := match h: ls0 with - | list_t.ListCons x0 tl0 => + | list_t.Cons x0 tl0 => match h: ls1 with - | list_t.ListCons x1 tl1 => + | list_t.Cons x1 tl1 => if h: i = (UInt32.ofNatCore 0 (by intlit)) - then Result.ret (list_t.ListCons ret0 tl1) + then Result.ret (list_t.Cons ret0 tl1) else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) let tl10 ← list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 - Result.ret (list_t.ListCons x1 tl10) - | list_t.ListNil => Result.fail Error.panic - | list_t.ListNil => Result.fail Error.panic + Result.ret (list_t.Cons x1 tl10) + | list_t.Nil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic termination_by list_nth_shared_mut_loop_pair_merge_loop_back ls0 ls1 i ret0 => list_nth_shared_mut_loop_pair_merge_loop_terminates T ls0 ls1 i decreasing_by list_nth_shared_mut_loop_pair_merge_loop_decreases ls0 ls1 i diff --git a/tests/lean/misc-loops/Loops/Types.lean b/tests/lean/misc-loops/Loops/Types.lean index f4b6809e..ca43f4c8 100644 --- a/tests/lean/misc-loops/Loops/Types.lean +++ b/tests/lean/misc-loops/Loops/Types.lean @@ -4,6 +4,6 @@ import Base.Primitives /- [loops::List] -/ inductive list_t (T : Type) := -| ListCons : T -> list_t T -> list_t T -| ListNil : list_t T +| Cons : T -> list_t T -> list_t T +| Nil : list_t T diff --git a/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean b/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean index 12d4190c..e2697385 100644 --- a/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean +++ b/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean @@ -11,29 +11,29 @@ structure OpaqueDefs where /- [no_nested_borrows::List] -/ inductive list_t (T : Type) := - | ListCons : T -> list_t T -> list_t T - | ListNil : list_t T + | Cons : T -> list_t T -> list_t T + | Nil : list_t T /- [no_nested_borrows::One] -/ inductive one_t (T1 : Type) := - | OneOne : T1 -> one_t T1 + | One : T1 -> one_t T1 /- [no_nested_borrows::EmptyEnum] -/ inductive empty_enum_t := - | EmptyEnumEmpty : empty_enum_t + | Empty : empty_enum_t /- [no_nested_borrows::Enum] -/ inductive enum_t := - | EnumVariant1 : enum_t - | EnumVariant2 : enum_t + | Variant1 : enum_t + | Variant2 : enum_t /- [no_nested_borrows::EmptyStruct] -/ structure empty_struct_t where /- [no_nested_borrows::Sum] -/ inductive sum_t (T1 T2 : Type) := - | SumLeft : T1 -> sum_t T1 T2 - | SumRight : T2 -> sum_t T1 T2 + | Left : T1 -> sum_t T1 T2 + | Right : T2 -> sum_t T1 T2 /- [no_nested_borrows::neg_test] -/ def neg_test_fwd (x : Int32) : Result Int32 := @@ -187,15 +187,15 @@ structure OpaqueDefs where /- [no_nested_borrows::is_cons] -/ def is_cons_fwd (T : Type) (l : list_t T) : Result Bool := match h: l with - | list_t.ListCons t l0 => Result.ret true - | list_t.ListNil => Result.ret false + | list_t.Cons t l0 => Result.ret true + | list_t.Nil => Result.ret false /- [no_nested_borrows::test_is_cons] -/ def test_is_cons_fwd : Result Unit := do - let l := list_t.ListNil + let l := list_t.Nil let b ← - is_cons_fwd Int32 (list_t.ListCons (Int32.ofNatCore 0 (by intlit)) l) + is_cons_fwd Int32 (list_t.Cons (Int32.ofNatCore 0 (by intlit)) l) if h: not b then Result.fail Error.panic else Result.ret () @@ -206,16 +206,15 @@ structure OpaqueDefs where /- [no_nested_borrows::split_list] -/ def split_list_fwd (T : Type) (l : list_t T) : Result (T × (list_t T)) := match h: l with - | list_t.ListCons hd tl => Result.ret (hd, tl) - | list_t.ListNil => Result.fail Error.panic + | list_t.Cons hd tl => Result.ret (hd, tl) + | list_t.Nil => Result.fail Error.panic /- [no_nested_borrows::test_split_list] -/ def test_split_list_fwd : Result Unit := do - let l := list_t.ListNil + let l := list_t.Nil let p ← - split_list_fwd Int32 (list_t.ListCons (Int32.ofNatCore 0 (by intlit)) - l) + split_list_fwd Int32 (list_t.Cons (Int32.ofNatCore 0 (by intlit)) l) let (hd, _) := p if h: not (hd = (Int32.ofNatCore 0 (by intlit))) then Result.fail Error.panic @@ -267,88 +266,87 @@ structure OpaqueDefs where /- [no_nested_borrows::NodeElem] -/ mutual inductive node_elem_t (T : Type) := - | NodeElemCons : tree_t T -> node_elem_t T -> node_elem_t T - | NodeElemNil : node_elem_t T + | Cons : tree_t T -> node_elem_t T -> node_elem_t T + | Nil : node_elem_t T /- [no_nested_borrows::Tree] -/ inductive tree_t (T : Type) := - | TreeLeaf : T -> tree_t T - | TreeNode : T -> node_elem_t T -> tree_t T -> tree_t T + | Leaf : T -> tree_t T + | Node : T -> node_elem_t T -> tree_t T -> tree_t T /- [no_nested_borrows::list_length] -/ def list_length_fwd (T : Type) (l : list_t T) : Result UInt32 := match h: l with - | list_t.ListCons t l1 => + | list_t.Cons t l1 => do let i ← list_length_fwd T l1 UInt32.checked_add (UInt32.ofNatCore 1 (by intlit)) i - | list_t.ListNil => Result.ret (UInt32.ofNatCore 0 (by intlit)) + | list_t.Nil => Result.ret (UInt32.ofNatCore 0 (by intlit)) /- [no_nested_borrows::list_nth_shared] -/ def list_nth_shared_fwd (T : Type) (l : list_t T) (i : UInt32) : Result T := match h: l with - | list_t.ListCons x tl => + | list_t.Cons x tl => if h: i = (UInt32.ofNatCore 0 (by intlit)) then Result.ret x else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_shared_fwd T tl i0 - | list_t.ListNil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic /- [no_nested_borrows::list_nth_mut] -/ def list_nth_mut_fwd (T : Type) (l : list_t T) (i : UInt32) : Result T := match h: l with - | list_t.ListCons x tl => + | list_t.Cons x tl => if h: i = (UInt32.ofNatCore 0 (by intlit)) then Result.ret x else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_mut_fwd T tl i0 - | list_t.ListNil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic /- [no_nested_borrows::list_nth_mut] -/ def list_nth_mut_back (T : Type) (l : list_t T) (i : UInt32) (ret0 : T) : Result (list_t T) := match h: l with - | list_t.ListCons x tl => + | list_t.Cons x tl => if h: i = (UInt32.ofNatCore 0 (by intlit)) - then Result.ret (list_t.ListCons ret0 tl) + then Result.ret (list_t.Cons ret0 tl) else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) let tl0 ← list_nth_mut_back T tl i0 ret0 - Result.ret (list_t.ListCons x tl0) - | list_t.ListNil => Result.fail Error.panic + Result.ret (list_t.Cons x tl0) + | list_t.Nil => Result.fail Error.panic /- [no_nested_borrows::list_rev_aux] -/ def list_rev_aux_fwd (T : Type) (li : list_t T) (lo : list_t T) : Result (list_t T) := match h: li with - | list_t.ListCons hd tl => list_rev_aux_fwd T tl (list_t.ListCons hd lo) - | list_t.ListNil => Result.ret lo + | list_t.Cons hd tl => list_rev_aux_fwd T tl (list_t.Cons hd lo) + | list_t.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.ListNil - list_rev_aux_fwd T li list_t.ListNil + let li := mem_replace_fwd (list_t T) l list_t.Nil + list_rev_aux_fwd T li list_t.Nil /- [no_nested_borrows::test_list_functions] -/ def test_list_functions_fwd : Result Unit := do - let l := list_t.ListNil - let l0 := list_t.ListCons (Int32.ofNatCore 2 (by intlit)) l - let l1 := list_t.ListCons (Int32.ofNatCore 1 (by intlit)) l0 + let l := list_t.Nil + let l0 := list_t.Cons (Int32.ofNatCore 2 (by intlit)) l + let l1 := list_t.Cons (Int32.ofNatCore 1 (by intlit)) l0 let i ← - list_length_fwd Int32 (list_t.ListCons (Int32.ofNatCore 0 (by intlit)) - l1) + list_length_fwd Int32 (list_t.Cons (Int32.ofNatCore 0 (by intlit)) l1) if h: not (i = (UInt32.ofNatCore 3 (by intlit))) then Result.fail Error.panic else do let i0 ← - list_nth_shared_fwd Int32 (list_t.ListCons + list_nth_shared_fwd Int32 (list_t.Cons (Int32.ofNatCore 0 (by intlit)) l1) (UInt32.ofNatCore 0 (by intlit)) if h: not (i0 = (Int32.ofNatCore 0 (by intlit))) @@ -356,7 +354,7 @@ structure OpaqueDefs where else do let i1 ← - list_nth_shared_fwd Int32 (list_t.ListCons + list_nth_shared_fwd Int32 (list_t.Cons (Int32.ofNatCore 0 (by intlit)) l1) (UInt32.ofNatCore 1 (by intlit)) if h: not (i1 = (Int32.ofNatCore 1 (by intlit))) @@ -364,7 +362,7 @@ structure OpaqueDefs where else do let i2 ← - list_nth_shared_fwd Int32 (list_t.ListCons + list_nth_shared_fwd Int32 (list_t.Cons (Int32.ofNatCore 0 (by intlit)) l1) (UInt32.ofNatCore 2 (by intlit)) if h: not (i2 = (Int32.ofNatCore 2 (by intlit))) @@ -372,7 +370,7 @@ structure OpaqueDefs where else do let ls ← - list_nth_mut_back Int32 (list_t.ListCons + list_nth_mut_back Int32 (list_t.Cons (Int32.ofNatCore 0 (by intlit)) l1) (UInt32.ofNatCore 1 (by intlit)) (Int32.ofNatCore 3 (by intlit)) @@ -550,8 +548,8 @@ structure OpaqueDefs where /- [no_nested_borrows::test_shared_borrow_enum1] -/ def test_shared_borrow_enum1_fwd (l : list_t UInt32) : Result UInt32 := match h: l with - | list_t.ListCons i l0 => Result.ret (UInt32.ofNatCore 1 (by intlit)) - | list_t.ListNil => Result.ret (UInt32.ofNatCore 0 (by intlit)) + | list_t.Cons i l0 => Result.ret (UInt32.ofNatCore 1 (by intlit)) + | list_t.Nil => Result.ret (UInt32.ofNatCore 0 (by intlit)) /- [no_nested_borrows::test_shared_borrow_enum2] -/ def test_shared_borrow_enum2_fwd : Result UInt32 := diff --git a/tests/lean/misc-paper/Paper.lean b/tests/lean/misc-paper/Paper.lean index 4faf36ee..05fde52c 100644 --- a/tests/lean/misc-paper/Paper.lean +++ b/tests/lean/misc-paper/Paper.lean @@ -58,57 +58,56 @@ structure OpaqueDefs where /- [paper::List] -/ inductive list_t (T : Type) := - | ListCons : T -> list_t T -> list_t T - | ListNil : list_t T + | Cons : T -> list_t T -> list_t T + | Nil : list_t T /- [paper::list_nth_mut] -/ def list_nth_mut_fwd (T : Type) (l : list_t T) (i : UInt32) : Result T := match h: l with - | list_t.ListCons x tl => + | list_t.Cons x tl => if h: i = (UInt32.ofNatCore 0 (by intlit)) then Result.ret x else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) list_nth_mut_fwd T tl i0 - | list_t.ListNil => Result.fail Error.panic + | list_t.Nil => Result.fail Error.panic /- [paper::list_nth_mut] -/ def list_nth_mut_back (T : Type) (l : list_t T) (i : UInt32) (ret0 : T) : Result (list_t T) := match h: l with - | list_t.ListCons x tl => + | list_t.Cons x tl => if h: i = (UInt32.ofNatCore 0 (by intlit)) - then Result.ret (list_t.ListCons ret0 tl) + then Result.ret (list_t.Cons ret0 tl) else do let i0 ← UInt32.checked_sub i (UInt32.ofNatCore 1 (by intlit)) let tl0 ← list_nth_mut_back T tl i0 ret0 - Result.ret (list_t.ListCons x tl0) - | list_t.ListNil => Result.fail Error.panic + Result.ret (list_t.Cons x tl0) + | list_t.Nil => Result.fail Error.panic /- [paper::sum] -/ def sum_fwd (l : list_t Int32) : Result Int32 := match h: l with - | list_t.ListCons x tl => do - let i ← sum_fwd tl - Int32.checked_add x i - | list_t.ListNil => Result.ret (Int32.ofNatCore 0 (by intlit)) + | list_t.Cons x tl => do + let i ← sum_fwd tl + Int32.checked_add x i + | list_t.Nil => Result.ret (Int32.ofNatCore 0 (by intlit)) /- [paper::test_nth] -/ def test_nth_fwd : Result Unit := do - let l := list_t.ListNil - let l0 := list_t.ListCons (Int32.ofNatCore 3 (by intlit)) l - let l1 := list_t.ListCons (Int32.ofNatCore 2 (by intlit)) l0 + let l := list_t.Nil + let l0 := list_t.Cons (Int32.ofNatCore 3 (by intlit)) l + let l1 := list_t.Cons (Int32.ofNatCore 2 (by intlit)) l0 let x ← - list_nth_mut_fwd Int32 (list_t.ListCons (Int32.ofNatCore 1 (by intlit)) - l1) (UInt32.ofNatCore 2 (by intlit)) + list_nth_mut_fwd Int32 (list_t.Cons (Int32.ofNatCore 1 (by intlit)) l1) + (UInt32.ofNatCore 2 (by intlit)) let x0 ← Int32.checked_add x (Int32.ofNatCore 1 (by intlit)) let l2 ← - list_nth_mut_back Int32 (list_t.ListCons - (Int32.ofNatCore 1 (by intlit)) l1) (UInt32.ofNatCore 2 (by intlit)) - x0 + list_nth_mut_back Int32 (list_t.Cons (Int32.ofNatCore 1 (by intlit)) + l1) (UInt32.ofNatCore 2 (by intlit)) x0 let i ← sum_fwd l2 if h: not (i = (Int32.ofNatCore 7 (by intlit))) then Result.fail Error.panic diff --git a/tests/lean/misc-polonius_list/PoloniusList.lean b/tests/lean/misc-polonius_list/PoloniusList.lean index d679230d..a3bbfd0a 100644 --- a/tests/lean/misc-polonius_list/PoloniusList.lean +++ b/tests/lean/misc-polonius_list/PoloniusList.lean @@ -6,18 +6,18 @@ structure OpaqueDefs where /- [polonius_list::List] -/ inductive list_t (T : Type) := - | ListCons : T -> list_t T -> list_t T - | ListNil : list_t T + | Cons : T -> list_t T -> list_t T + | Nil : list_t T /- [polonius_list::get_list_at_x] -/ def get_list_at_x_fwd (ls : list_t UInt32) (x : UInt32) : Result (list_t UInt32) := match h: ls with - | list_t.ListCons hd tl => + | list_t.Cons hd tl => if h: hd = x - then Result.ret (list_t.ListCons hd tl) + then Result.ret (list_t.Cons hd tl) else get_list_at_x_fwd tl x - | list_t.ListNil => Result.ret list_t.ListNil + | list_t.Nil => Result.ret list_t.Nil /- [polonius_list::get_list_at_x] -/ def get_list_at_x_back @@ -25,12 +25,12 @@ structure OpaqueDefs where Result (list_t UInt32) := match h: ls with - | list_t.ListCons hd tl => + | list_t.Cons hd tl => if h: hd = x then Result.ret ret0 else do let tl0 ← get_list_at_x_back tl x ret0 - Result.ret (list_t.ListCons hd tl0) - | list_t.ListNil => Result.ret ret0 + Result.ret (list_t.Cons hd tl0) + | list_t.Nil => Result.ret ret0 |