diff options
Diffstat (limited to 'tests/lean/betree/BetreeMain')
| -rw-r--r-- | tests/lean/betree/BetreeMain/Funs.lean | 227 |
1 files changed, 99 insertions, 128 deletions
diff --git a/tests/lean/betree/BetreeMain/Funs.lean b/tests/lean/betree/BetreeMain/Funs.lean index e40ca4ca..5d355677 100644 --- a/tests/lean/betree/BetreeMain/Funs.lean +++ b/tests/lean/betree/BetreeMain/Funs.lean @@ -223,13 +223,7 @@ def betree_leaf_split_fwd betree_leaf_id := id1, betree_leaf_size := params.betree_params_split_size } - Result.ret (st1, - { - betree_internal_id := self.betree_leaf_id, - betree_internal_pivot := pivot, - betree_internal_left := n, - betree_internal_right := n0 - }) + Result.ret (st1, mkbetree_internal_t self.betree_leaf_id pivot n n0) /- [betree_main::betree::Leaf::{3}::split] -/ def betree_leaf_split_back @@ -380,8 +374,8 @@ mutual def betree_node_lookup_fwd match h: self with | betree_node_t.BetreeNodeInternal node => do - let (st0, msgs) ← - betree_load_internal_node_fwd node.betree_internal_id st + 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 => @@ -390,7 +384,8 @@ mutual def betree_node_lookup_fwd then do let (st1, opt) ← - betree_internal_lookup_in_children_fwd node key st0 + 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.BetreeListCons (k, msg) l) @@ -414,25 +409,27 @@ mutual def betree_node_lookup_fwd | betree_message_t.BetreeMessageUpsert ufs => do let (st1, v) ← - betree_internal_lookup_in_children_fwd node key st0 + 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 let node0 ← - betree_internal_lookup_in_children_back node key st0 + 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 let msgs0 ← betree_node_lookup_first_message_for_key_back key msgs pending0 - let (st3, _) ← - betree_store_internal_node_fwd node0.betree_internal_id msgs0 - st2 + let (st3, _) ← betree_store_internal_node_fwd i1 msgs0 st2 Result.ret (st3, Option.some v0) | betree_list_t.BetreeListNil => do let (st1, opt) ← - betree_internal_lookup_in_children_fwd node key st0 + 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 @@ -454,8 +451,8 @@ def betree_node_lookup_back match h: self with | betree_node_t.BetreeNodeInternal node => do - let (st0, msgs) ← - betree_load_internal_node_fwd node.betree_internal_id st + 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 => @@ -466,7 +463,9 @@ def betree_node_lookup_back let _ ← betree_node_lookup_first_message_for_key_back key msgs (betree_list_t.BetreeListCons (k, msg) l) - let node0 ← betree_internal_lookup_in_children_back node key st0 + let node0 ← + betree_internal_lookup_in_children_back (mkbetree_internal_t i i0 + n n0) key st0 Result.ret (betree_node_t.BetreeNodeInternal node0) else match h: msg with @@ -476,38 +475,44 @@ def betree_node_lookup_back 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 node) + Result.ret (betree_node_t.BetreeNodeInternal (mkbetree_internal_t + i i0 n n0)) | betree_message_t.BetreeMessageDelete => 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 node) + Result.ret (betree_node_t.BetreeNodeInternal (mkbetree_internal_t + i i0 n n0)) | betree_message_t.BetreeMessageUpsert ufs => do let (st1, v) ← - betree_internal_lookup_in_children_fwd node key st0 + 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 let node0 ← - betree_internal_lookup_in_children_back node key st0 + 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 let msgs0 ← betree_node_lookup_first_message_for_key_back key msgs pending0 - let _ ← - betree_store_internal_node_fwd node0.betree_internal_id msgs0 - st2 - Result.ret (betree_node_t.BetreeNodeInternal node0) + 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 => do let _ ← betree_node_lookup_first_message_for_key_back key msgs betree_list_t.BetreeListNil - let node0 ← betree_internal_lookup_in_children_back node key st0 + 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 => do @@ -523,9 +528,10 @@ def betree_internal_lookup_in_children_fwd (self : betree_internal_t) (key : UInt64) (st : State) : (Result (State × (Option UInt64))) := - if h: key < self.betree_internal_pivot - then betree_node_lookup_fwd self.betree_internal_left key st - else betree_node_lookup_fwd self.betree_internal_right key st + let (mkbetree_internal_t _ i n n0) := self + if h: key < i + then betree_node_lookup_fwd n key st + else betree_node_lookup_fwd n0 key st termination_by betree_internal_lookup_in_children_fwd self key st => betree_internal_lookup_in_children_terminates self key st decreasing_by betree_internal_lookup_in_children_decreases self key st @@ -535,27 +541,16 @@ def betree_internal_lookup_in_children_back (self : betree_internal_t) (key : UInt64) (st : State) : (Result betree_internal_t) := - if h: key < self.betree_internal_pivot + let (mkbetree_internal_t i i0 n n0) := self + if h: key < i0 then do - let n ← betree_node_lookup_back self.betree_internal_left key st - Result.ret - { - betree_internal_id := self.betree_internal_id, - betree_internal_pivot := self.betree_internal_pivot, - betree_internal_left := n, - betree_internal_right := self.betree_internal_right - } + let n1 ← betree_node_lookup_back n key st + Result.ret (mkbetree_internal_t i i0 n1 n0) else do - let n ← betree_node_lookup_back self.betree_internal_right key st - Result.ret - { - betree_internal_id := self.betree_internal_id, - betree_internal_pivot := self.betree_internal_pivot, - betree_internal_left := self.betree_internal_left, - betree_internal_right := n - } + let n1 ← betree_node_lookup_back n0 key st + Result.ret (mkbetree_internal_t i i0 n n1) termination_by betree_internal_lookup_in_children_back self key st => betree_internal_lookup_in_children_terminates self key st decreasing_by betree_internal_lookup_in_children_decreases self key st @@ -819,8 +814,8 @@ mutual def betree_node_apply_messages_fwd match h: self with | betree_node_t.BetreeNodeInternal node => do - let (st0, content) ← - betree_load_internal_node_fwd node.betree_internal_id st + let (mkbetree_internal_t i i0 n n0) := node + let (st0, content) ← betree_load_internal_node_fwd i st let content0 ← betree_node_apply_messages_to_internal_fwd_back content msgs let num_msgs ← @@ -829,17 +824,17 @@ mutual def betree_node_apply_messages_fwd then do let (st1, content1) ← - betree_internal_flush_fwd node params node_id_cnt content0 st0 + betree_internal_flush_fwd (mkbetree_internal_t i i0 n n0) params + node_id_cnt content0 st0 let (node0, _) ← - betree_internal_flush_back node params node_id_cnt content0 st0 - let (st2, _) ← - betree_store_internal_node_fwd node0.betree_internal_id content1 - st1 + betree_internal_flush_back (mkbetree_internal_t i i0 n n0) params + node_id_cnt content0 st0 + let (mkbetree_internal_t i1 _ _ _) := node0 + let (st2, _) ← betree_store_internal_node_fwd i1 content1 st1 Result.ret (st2, ()) else do - let (st1, _) ← - betree_store_internal_node_fwd node.betree_internal_id content0 st0 + let (st1, _) ← betree_store_internal_node_fwd i content0 st0 Result.ret (st1, ()) | betree_node_t.BetreeNodeLeaf node => do @@ -878,8 +873,8 @@ def betree_node_apply_messages_back match h: self with | betree_node_t.BetreeNodeInternal node => do - let (st0, content) ← - betree_load_internal_node_fwd node.betree_internal_id st + let (mkbetree_internal_t i i0 n n0) := node + let (st0, content) ← betree_load_internal_node_fwd i st let content0 ← betree_node_apply_messages_to_internal_fwd_back content msgs let num_msgs ← @@ -888,18 +883,20 @@ def betree_node_apply_messages_back then do let (st1, content1) ← - betree_internal_flush_fwd node params node_id_cnt content0 st0 + betree_internal_flush_fwd (mkbetree_internal_t i i0 n n0) params + node_id_cnt content0 st0 let (node0, node_id_cnt0) ← - betree_internal_flush_back node params node_id_cnt content0 st0 - let _ ← - betree_store_internal_node_fwd node0.betree_internal_id content1 - st1 - Result.ret (betree_node_t.BetreeNodeInternal node0, node_id_cnt0) + betree_internal_flush_back (mkbetree_internal_t i i0 n n0) params + 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) else do - let _ ← - betree_store_internal_node_fwd node.betree_internal_id content0 st0 - Result.ret (betree_node_t.BetreeNodeInternal node, node_id_cnt) + 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 => do let (st0, content) ← betree_load_leaf_node_fwd node.betree_leaf_id st @@ -938,41 +935,36 @@ def betree_internal_flush_fwd (Result (State × (betree_list_t (UInt64 × betree_message_t)))) := do - let p ← - betree_list_partition_at_pivot_fwd betree_message_t content - self.betree_internal_pivot + let (mkbetree_internal_t _ i n n0) := self + let p ← betree_list_partition_at_pivot_fwd betree_message_t content i let (msgs_left, msgs_right) := p let len_left ← betree_list_len_fwd (UInt64 × betree_message_t) msgs_left if h: len_left >= params.betree_params_min_flush_size then do let (st0, _) ← - betree_node_apply_messages_fwd self.betree_internal_left params - node_id_cnt msgs_left st + betree_node_apply_messages_fwd n params node_id_cnt msgs_left st let (_, node_id_cnt0) ← - betree_node_apply_messages_back self.betree_internal_left params - node_id_cnt msgs_left st + betree_node_apply_messages_back n params node_id_cnt msgs_left st let len_right ← betree_list_len_fwd (UInt64 × betree_message_t) msgs_right if h: len_right >= params.betree_params_min_flush_size then do let (st1, _) ← - betree_node_apply_messages_fwd self.betree_internal_right params - node_id_cnt0 msgs_right st0 + betree_node_apply_messages_fwd n0 params node_id_cnt0 msgs_right + st0 let _ ← - betree_node_apply_messages_back self.betree_internal_right params - node_id_cnt0 msgs_right st0 + betree_node_apply_messages_back n0 params node_id_cnt0 msgs_right + st0 Result.ret (st1, betree_list_t.BetreeListNil) else Result.ret (st0, msgs_right) else do let (st0, _) ← - betree_node_apply_messages_fwd self.betree_internal_right params - node_id_cnt msgs_right st + betree_node_apply_messages_fwd n0 params node_id_cnt msgs_right st let _ ← - betree_node_apply_messages_back self.betree_internal_right params - node_id_cnt msgs_right st + betree_node_apply_messages_back n0 params node_id_cnt msgs_right st Result.ret (st0, msgs_left) termination_by betree_internal_flush_fwd self params node_id_cnt content st => betree_internal_flush_terminates self params node_id_cnt content st @@ -987,55 +979,32 @@ def betree_internal_flush_back (Result (betree_internal_t × betree_node_id_counter_t)) := do - let p ← - betree_list_partition_at_pivot_fwd betree_message_t content - self.betree_internal_pivot + let (mkbetree_internal_t i i0 n n0) := self + let p ← betree_list_partition_at_pivot_fwd betree_message_t content i0 let (msgs_left, msgs_right) := p let len_left ← betree_list_len_fwd (UInt64 × betree_message_t) msgs_left if h: len_left >= params.betree_params_min_flush_size then do let (st0, _) ← - betree_node_apply_messages_fwd self.betree_internal_left params - node_id_cnt msgs_left st - let (n, node_id_cnt0) ← - betree_node_apply_messages_back self.betree_internal_left params - node_id_cnt msgs_left st + betree_node_apply_messages_fwd n params node_id_cnt msgs_left st + let (n1, node_id_cnt0) ← + betree_node_apply_messages_back n params node_id_cnt msgs_left st let len_right ← betree_list_len_fwd (UInt64 × betree_message_t) msgs_right if h: len_right >= params.betree_params_min_flush_size then do - let (n0, node_id_cnt1) ← - betree_node_apply_messages_back self.betree_internal_right params - node_id_cnt0 msgs_right st0 - Result.ret - ({ - betree_internal_id := self.betree_internal_id, - betree_internal_pivot := self.betree_internal_pivot, - betree_internal_left := n, - betree_internal_right := n0 - }, node_id_cnt1) - else - Result.ret - ({ - betree_internal_id := self.betree_internal_id, - betree_internal_pivot := self.betree_internal_pivot, - betree_internal_left := n, - betree_internal_right := self.betree_internal_right - }, node_id_cnt0) + let (n2, node_id_cnt1) ← + betree_node_apply_messages_back n0 params node_id_cnt0 msgs_right + st0 + Result.ret (mkbetree_internal_t i i0 n1 n2, node_id_cnt1) + else Result.ret (mkbetree_internal_t i i0 n1 n0, node_id_cnt0) else do - let (n, node_id_cnt0) ← - betree_node_apply_messages_back self.betree_internal_right params - node_id_cnt msgs_right st - Result.ret - ({ - betree_internal_id := self.betree_internal_id, - betree_internal_pivot := self.betree_internal_pivot, - betree_internal_left := self.betree_internal_left, - betree_internal_right := n - }, node_id_cnt0) + let (n1, node_id_cnt0) ← + betree_node_apply_messages_back n0 params node_id_cnt msgs_right st + Result.ret (mkbetree_internal_t i i0 n n1, node_id_cnt0) termination_by betree_internal_flush_back self params node_id_cnt content st => betree_internal_flush_terminates self params node_id_cnt content st decreasing_by @@ -1082,16 +1051,18 @@ def betree_be_tree_new_fwd let node_id_cnt0 ← betree_node_id_counter_fresh_id_back node_id_cnt Result.ret (st0, { - betree_be_tree_params := { - betree_params_min_flush_size := min_flush_size, - betree_params_split_size := split_size - }, + betree_be_tree_params := + { + betree_params_min_flush_size := min_flush_size, + betree_params_split_size := split_size + }, betree_be_tree_node_id_cnt := node_id_cnt0, - betree_be_tree_root := (betree_node_t.BetreeNodeLeaf - { - betree_leaf_id := id, - betree_leaf_size := (UInt64.ofNatCore 0 (by intlit)) - }) + betree_be_tree_root := + (betree_node_t.BetreeNodeLeaf + { + betree_leaf_id := id, + betree_leaf_size := (UInt64.ofNatCore 0 (by intlit)) + }) }) /- [betree_main::betree::BeTree::{6}::apply] -/ |