summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorSon Ho2023-03-08 00:39:05 +0100
committerSon HO2023-06-04 21:44:33 +0200
commit14aed083b850c2d8a77cfe394827aeecce06514b (patch)
tree8486ce9eb6ca80668d34c3422ef89e29018ec269 /tests
parentc00d77052e8cb778e5311a4344cf8449dd3726b6 (diff)
Improve the generation of variant names for Lean
Diffstat (limited to 'tests')
-rw-r--r--tests/lean/betree/BetreeMain/Funs.lean324
-rw-r--r--tests/lean/betree/BetreeMain/Types.lean18
-rw-r--r--tests/lean/hashmap/Hashmap/Funs.lean69
-rw-r--r--tests/lean/hashmap/Hashmap/Types.lean4
-rw-r--r--tests/lean/hashmap_on_disk/HashmapMain/Funs.lean102
-rw-r--r--tests/lean/hashmap_on_disk/HashmapMain/Types.lean4
-rw-r--r--tests/lean/misc-loops/Loops/Funs.lean200
-rw-r--r--tests/lean/misc-loops/Loops/Types.lean4
-rw-r--r--tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean90
-rw-r--r--tests/lean/misc-paper/Paper.lean39
-rw-r--r--tests/lean/misc-polonius_list/PoloniusList.lean16
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