diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/lean/BetreeMain/Funs.lean | 1158 |
1 files changed, 408 insertions, 750 deletions
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean index 0d7cb984..4e64d217 100644 --- a/tests/lean/BetreeMain/Funs.lean +++ b/tests/lean/BetreeMain/Funs.lean @@ -7,7 +7,7 @@ open Primitives namespace betree_main -/- [betree_main::betree::load_internal_node]: forward function +/- [betree_main::betree::load_internal_node]: Source: 'src/betree.rs', lines 36:0-36:52 -/ def betree.load_internal_node (id : U64) (st : State) : @@ -15,65 +15,53 @@ def betree.load_internal_node := betree_utils.load_internal_node id st -/- [betree_main::betree::store_internal_node]: forward function +/- [betree_main::betree::store_internal_node]: Source: 'src/betree.rs', lines 41:0-41:60 -/ def betree.store_internal_node (id : U64) (content : betree.List (U64 × betree.Message)) (st : State) : Result (State × Unit) := do - let (st0, _) ← betree_utils.store_internal_node id content st - Result.ret (st0, ()) + let (st1, _) ← betree_utils.store_internal_node id content st + Result.ret (st1, ()) -/- [betree_main::betree::load_leaf_node]: forward function +/- [betree_main::betree::load_leaf_node]: Source: 'src/betree.rs', lines 46:0-46:44 -/ def betree.load_leaf_node (id : U64) (st : State) : Result (State × (betree.List (U64 × U64))) := betree_utils.load_leaf_node id st -/- [betree_main::betree::store_leaf_node]: forward function +/- [betree_main::betree::store_leaf_node]: Source: 'src/betree.rs', lines 51:0-51:52 -/ def betree.store_leaf_node (id : U64) (content : betree.List (U64 × U64)) (st : State) : Result (State × Unit) := do - let (st0, _) ← betree_utils.store_leaf_node id content st - Result.ret (st0, ()) + let (st1, _) ← betree_utils.store_leaf_node id content st + Result.ret (st1, ()) -/- [betree_main::betree::fresh_node_id]: forward function +/- [betree_main::betree::fresh_node_id]: Source: 'src/betree.rs', lines 55:0-55:48 -/ -def betree.fresh_node_id (counter : U64) : Result U64 := +def betree.fresh_node_id (counter : U64) : Result (U64 × U64) := do - let _ ← counter + 1#u64 - Result.ret counter + let counter1 ← counter + 1#u64 + Result.ret (counter, counter1) -/- [betree_main::betree::fresh_node_id]: backward function 0 - Source: 'src/betree.rs', lines 55:0-55:48 -/ -def betree.fresh_node_id_back (counter : U64) : Result U64 := - counter + 1#u64 - -/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: forward function +/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: Source: 'src/betree.rs', lines 206:4-206:20 -/ def betree.NodeIdCounter.new : Result betree.NodeIdCounter := Result.ret { next_node_id := 0#u64 } -/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: forward function +/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: Source: 'src/betree.rs', lines 210:4-210:36 -/ -def betree.NodeIdCounter.fresh_id (self : betree.NodeIdCounter) : Result U64 := +def betree.NodeIdCounter.fresh_id + (self : betree.NodeIdCounter) : Result (U64 × betree.NodeIdCounter) := do - let _ ← self.next_node_id + 1#u64 - Result.ret self.next_node_id + let i ← self.next_node_id + 1#u64 + Result.ret (self.next_node_id, { next_node_id := i }) -/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: backward function 0 - Source: 'src/betree.rs', lines 210:4-210:36 -/ -def betree.NodeIdCounter.fresh_id_back - (self : betree.NodeIdCounter) : Result betree.NodeIdCounter := - do - let i ← self.next_node_id + 1#u64 - Result.ret { next_node_id := i } - -/- [betree_main::betree::upsert_update]: forward function +/- [betree_main::betree::upsert_update]: Source: 'src/betree.rs', lines 234:0-234:70 -/ def betree.upsert_update (prev : Option U64) (st : betree.UpsertFunState) : Result U64 := @@ -81,30 +69,30 @@ def betree.upsert_update | none => match st with | betree.UpsertFunState.Add v => Result.ret v - | betree.UpsertFunState.Sub i => Result.ret 0#u64 - | some prev0 => + | betree.UpsertFunState.Sub _ => Result.ret 0#u64 + | some prev1 => match st with | betree.UpsertFunState.Add v => do - let margin ← core_u64_max - prev0 - if margin >= v - then prev0 + v - else Result.ret core_u64_max + let margin ← core_u64_max - prev1 + if margin >= v + then prev1 + v + else Result.ret core_u64_max | betree.UpsertFunState.Sub v => - if prev0 >= v - then prev0 - v + if prev1 >= v + then prev1 - v else Result.ret 0#u64 -/- [betree_main::betree::{betree_main::betree::List<T>#1}::len]: forward function +/- [betree_main::betree::{betree_main::betree::List<T>#1}::len]: Source: 'src/betree.rs', lines 276:4-276:24 -/ divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 := match self with - | betree.List.Cons t tl => do - let i ← betree.List.len T tl - 1#u64 + i + | betree.List.Cons _ tl => do + let i ← betree.List.len T tl + 1#u64 + i | betree.List.Nil => Result.ret 0#u64 -/- [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: forward function +/- [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: Source: 'src/betree.rs', lines 284:4-284:51 -/ divergent def betree.List.split_at (T : Type) (self : betree.List T) (n : U64) : @@ -116,56 +104,47 @@ divergent def betree.List.split_at match self with | betree.List.Cons hd tl => do - let i ← n - 1#u64 - let p ← betree.List.split_at T tl i - let (ls0, ls1) := p - let l := ls0 - Result.ret (betree.List.Cons hd l, ls1) + let i ← n - 1#u64 + let p ← betree.List.split_at T tl i + let (ls0, ls1) := p + let l := ls0 + Result.ret (betree.List.Cons hd l, ls1) | betree.List.Nil => Result.fail .panic -/- [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: Source: 'src/betree.rs', lines 299:4-299:34 -/ def betree.List.push_front (T : Type) (self : betree.List T) (x : T) : Result (betree.List T) := - let tl := core.mem.replace (betree.List T) self betree.List.Nil + let (tl, _) := core.mem.replace (betree.List T) self betree.List.Nil let l := tl Result.ret (betree.List.Cons x l) -/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: forward function - Source: 'src/betree.rs', lines 306:4-306:32 -/ -def betree.List.pop_front (T : Type) (self : betree.List T) : Result T := - let ls := core.mem.replace (betree.List T) self betree.List.Nil - match ls with - | betree.List.Cons x tl => Result.ret x - | betree.List.Nil => Result.fail .panic - -/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0 +/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: Source: 'src/betree.rs', lines 306:4-306:32 -/ -def betree.List.pop_front_back - (T : Type) (self : betree.List T) : Result (betree.List T) := - let ls := core.mem.replace (betree.List T) self betree.List.Nil +def betree.List.pop_front + (T : Type) (self : betree.List T) : Result (T × (betree.List T)) := + let (ls, _) := core.mem.replace (betree.List T) self betree.List.Nil match ls with - | betree.List.Cons x tl => Result.ret tl + | betree.List.Cons x tl => Result.ret (x, tl) | betree.List.Nil => Result.fail .panic -/- [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function +/- [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: Source: 'src/betree.rs', lines 318:4-318:22 -/ def betree.List.hd (T : Type) (self : betree.List T) : Result T := match self with - | betree.List.Cons hd l => Result.ret hd + | betree.List.Cons hd _ => Result.ret hd | betree.List.Nil => Result.fail .panic -/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function +/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: Source: 'src/betree.rs', lines 327:4-327:44 -/ def betree.ListTupleU64T.head_has_key (T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool := match self with - | betree.List.Cons hd l => let (i, _) := hd + | betree.List.Cons hd _ => let (i, _) := hd Result.ret (i = key) | betree.List.Nil => Result.ret false -/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: forward function +/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: Source: 'src/betree.rs', lines 339:4-339:73 -/ divergent def betree.ListTupleU64T.partition_at_pivot (T : Type) (self : betree.List (U64 × T)) (pivot : U64) : @@ -178,334 +157,191 @@ divergent def betree.ListTupleU64T.partition_at_pivot then Result.ret (betree.List.Nil, betree.List.Cons (i, t) tl) else do - let p ← betree.ListTupleU64T.partition_at_pivot T tl pivot - let (ls0, ls1) := p - let l := ls0 - Result.ret (betree.List.Cons (i, t) l, ls1) + let p ← betree.ListTupleU64T.partition_at_pivot T tl pivot + let (ls0, ls1) := p + let l := ls0 + Result.ret (betree.List.Cons (i, t) l, ls1) | betree.List.Nil => Result.ret (betree.List.Nil, betree.List.Nil) -/- [betree_main::betree::{betree_main::betree::Leaf#3}::split]: forward function +/- [betree_main::betree::{betree_main::betree::Leaf#3}::split]: Source: 'src/betree.rs', lines 359:4-364:17 -/ def betree.Leaf.split (self : betree.Leaf) (content : betree.List (U64 × U64)) (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) : - Result (State × betree.Internal) + Result (State × (betree.Internal × betree.NodeIdCounter)) := do - let p ← betree.List.split_at (U64 × U64) content params.split_size - let (content0, content1) := p - let p0 ← betree.List.hd (U64 × U64) content1 - let (pivot, _) := p0 - let id0 ← betree.NodeIdCounter.fresh_id node_id_cnt - let node_id_cnt0 ← betree.NodeIdCounter.fresh_id_back node_id_cnt - let id1 ← betree.NodeIdCounter.fresh_id node_id_cnt0 - let (st0, _) ← betree.store_leaf_node id0 content0 st - let (st1, _) ← betree.store_leaf_node id1 content1 st0 - let n := betree.Node.Leaf { id := id0, size := params.split_size } - let n0 := betree.Node.Leaf { id := id1, size := params.split_size } - Result.ret (st1, betree.Internal.mk self.id pivot n n0) - -/- [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 2 - Source: 'src/betree.rs', lines 359:4-364:17 -/ -def betree.Leaf.split_back - (self : betree.Leaf) (content : betree.List (U64 × U64)) - (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) : - Result betree.NodeIdCounter - := - do - let p ← betree.List.split_at (U64 × U64) content params.split_size - let (content0, content1) := p - let _ ← betree.List.hd (U64 × U64) content1 - let id0 ← betree.NodeIdCounter.fresh_id node_id_cnt - let node_id_cnt0 ← betree.NodeIdCounter.fresh_id_back node_id_cnt - let id1 ← betree.NodeIdCounter.fresh_id node_id_cnt0 - let (st0, _) ← betree.store_leaf_node id0 content0 st - let _ ← betree.store_leaf_node id1 content1 st0 - betree.NodeIdCounter.fresh_id_back node_id_cnt0 - -/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: forward function + let p ← betree.List.split_at (U64 × U64) content params.split_size + let (content0, content1) := p + let p1 ← betree.List.hd (U64 × U64) content1 + let (pivot, _) := p1 + let (id0, nic) ← betree.NodeIdCounter.fresh_id node_id_cnt + let (id1, nic1) ← betree.NodeIdCounter.fresh_id nic + let (st1, _) ← betree.store_leaf_node id0 content0 st + let (st2, _) ← betree.store_leaf_node id1 content1 st1 + let n := betree.Node.Leaf { id := id0, size := params.split_size } + let n1 := betree.Node.Leaf { id := id1, size := params.split_size } + Result.ret (st2, (betree.Internal.mk self.id pivot n n1, nic1)) + +/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: Source: 'src/betree.rs', lines 789:4-792:34 -/ divergent def betree.Node.lookup_first_message_for_key (key : U64) (msgs : betree.List (U64 × betree.Message)) : - Result (betree.List (U64 × betree.Message)) + Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 × + betree.Message) → Result (betree.List (U64 × betree.Message)))) := match msgs with | betree.List.Cons x next_msgs => let (i, m) := x if i >= key - then Result.ret (betree.List.Cons (i, m) next_msgs) - else betree.Node.lookup_first_message_for_key key next_msgs - | betree.List.Nil => Result.ret betree.List.Nil - -/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: backward function 0 - Source: 'src/betree.rs', lines 789:4-792:34 -/ -divergent def betree.Node.lookup_first_message_for_key_back - (key : U64) (msgs : betree.List (U64 × betree.Message)) - (ret : betree.List (U64 × betree.Message)) : - Result (betree.List (U64 × betree.Message)) - := - match msgs with - | betree.List.Cons x next_msgs => - let (i, m) := x - if i >= key - then Result.ret ret + then + let back_'a := fun ret => Result.ret ret + Result.ret (betree.List.Cons (i, m) next_msgs, back_'a) else do - let next_msgs0 ← - betree.Node.lookup_first_message_for_key_back key next_msgs ret - Result.ret (betree.List.Cons (i, m) next_msgs0) - | betree.List.Nil => Result.ret ret - -/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function + let (l, lookup_first_message_for_key_back) ← + betree.Node.lookup_first_message_for_key key next_msgs + let back_'a := + fun ret => + do + let next_msgs1 ← lookup_first_message_for_key_back ret + Result.ret (betree.List.Cons (i, m) next_msgs1) + Result.ret (l, back_'a) + | betree.List.Nil => + let back_'a := fun ret => Result.ret ret + Result.ret (betree.List.Nil, back_'a) + +/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: Source: 'src/betree.rs', lines 636:4-636:80 -/ divergent def betree.Node.lookup_in_bindings (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) := match bindings with | betree.List.Cons hd tl => - let (i, i0) := hd + let (i, i1) := hd if i = key - then Result.ret (some i0) + then Result.ret (some i1) else if i > key then Result.ret none else betree.Node.lookup_in_bindings key tl | betree.List.Nil => Result.ret none -/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function +/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: Source: 'src/betree.rs', lines 819:4-819:90 -/ divergent def betree.Node.apply_upserts (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64) (st : State) : - Result (State × U64) + Result (State × (U64 × (betree.List (U64 × betree.Message)))) := do - let b ← betree.ListTupleU64T.head_has_key betree.Message msgs key - if b - then - do - let msg ← betree.List.pop_front (U64 × betree.Message) msgs - let (_, m) := msg - match m with - | betree.Message.Insert i => Result.fail .panic - | betree.Message.Delete => Result.fail .panic - | betree.Message.Upsert s => - do - let v ← betree.upsert_update prev s - let msgs0 ← - betree.List.pop_front_back (U64 × betree.Message) msgs - betree.Node.apply_upserts msgs0 (some v) key st - else - do - let (st0, v) ← core.option.Option.unwrap U64 prev st - let _ ← - betree.List.push_front (U64 × betree.Message) msgs (key, - betree.Message.Insert v) - Result.ret (st0, v) - -/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: backward function 0 - Source: 'src/betree.rs', lines 819:4-819:90 -/ -divergent def betree.Node.apply_upserts_back - (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64) - (st : State) : - Result (betree.List (U64 × betree.Message)) - := - do - let b ← betree.ListTupleU64T.head_has_key betree.Message msgs key - if b - then - do - let msg ← betree.List.pop_front (U64 × betree.Message) msgs - let (_, m) := msg - match m with - | betree.Message.Insert i => Result.fail .panic - | betree.Message.Delete => Result.fail .panic - | betree.Message.Upsert s => - do - let v ← betree.upsert_update prev s - let msgs0 ← - betree.List.pop_front_back (U64 × betree.Message) msgs - betree.Node.apply_upserts_back msgs0 (some v) key st - else + let b ← betree.ListTupleU64T.head_has_key betree.Message msgs key + if b + then + do + let (msg, l) ← betree.List.pop_front (U64 × betree.Message) msgs + let (_, m) := msg + match m with + | betree.Message.Insert _ => Result.fail .panic + | betree.Message.Delete => Result.fail .panic + | betree.Message.Upsert s => do - let (_, v) ← core.option.Option.unwrap U64 prev st - betree.List.push_front (U64 × betree.Message) msgs (key, - betree.Message.Insert v) + let v ← betree.upsert_update prev s + betree.Node.apply_upserts l (some v) key st + else + do + let (st1, v) ← core.option.Option.unwrap U64 prev st + let l ← + betree.List.push_front (U64 × betree.Message) msgs (key, + betree.Message.Insert v) + Result.ret (st1, (v, l)) -/- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: forward function +/- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: Source: 'src/betree.rs', lines 395:4-395:63 -/ mutual divergent def betree.Internal.lookup_in_children (self : betree.Internal) (key : U64) (st : State) : - Result (State × (Option U64)) + Result (State × ((Option U64) × betree.Internal)) := - let ⟨ _, i, n, n0 ⟩ := self - if key < i - then betree.Node.lookup n key st - else betree.Node.lookup n0 key st - -/- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: backward function 0 - Source: 'src/betree.rs', lines 395:4-395:63 -/ -divergent def betree.Internal.lookup_in_children_back - (self : betree.Internal) (key : U64) (st : State) : Result betree.Internal := - let ⟨ i, i0, n, n0 ⟩ := self - if key < i0 + let ⟨ i, i1, n, n1 ⟩ := self + if key < i1 then do - let n1 ← betree.Node.lookup_back n key st - Result.ret (betree.Internal.mk i i0 n1 n0) + let (st1, (o, n2)) ← betree.Node.lookup n key st + Result.ret (st1, (o, betree.Internal.mk i i1 n2 n1)) else do - let n1 ← betree.Node.lookup_back n0 key st - Result.ret (betree.Internal.mk i i0 n n1) + let (st1, (o, n2)) ← betree.Node.lookup n1 key st + Result.ret (st1, (o, betree.Internal.mk i i1 n n2)) -/- [betree_main::betree::{betree_main::betree::Node#5}::lookup]: forward function +/- [betree_main::betree::{betree_main::betree::Node#5}::lookup]: Source: 'src/betree.rs', lines 709:4-709:58 -/ divergent def betree.Node.lookup (self : betree.Node) (key : U64) (st : State) : - Result (State × (Option U64)) + Result (State × ((Option U64) × betree.Node)) := match self with | betree.Node.Internal node => do - let ⟨ i, i0, n, n0 ⟩ := node - let (st0, msgs) ← betree.load_internal_node i st - let pending ← betree.Node.lookup_first_message_for_key key msgs - match pending with - | betree.List.Cons p l => - let (k, msg) := p - if k != key - then - do - let (st1, o) ← - betree.Internal.lookup_in_children (betree.Internal.mk i i0 n n0) - key st0 - let _ ← - betree.Node.lookup_first_message_for_key_back key msgs - (betree.List.Cons (k, msg) l) - Result.ret (st1, o) - else - match msg with - | betree.Message.Insert v => - do - let _ ← - betree.Node.lookup_first_message_for_key_back key msgs - (betree.List.Cons (k, betree.Message.Insert v) l) - Result.ret (st0, some v) - | betree.Message.Delete => - do - let _ ← - betree.Node.lookup_first_message_for_key_back key msgs - (betree.List.Cons (k, betree.Message.Delete) l) - Result.ret (st0, none) - | betree.Message.Upsert ufs => - do - let (st1, v) ← - betree.Internal.lookup_in_children (betree.Internal.mk i i0 n - n0) key st0 - let (st2, v0) ← - betree.Node.apply_upserts (betree.List.Cons (k, - betree.Message.Upsert ufs) l) v key st1 - let node0 ← - betree.Internal.lookup_in_children_back (betree.Internal.mk i - i0 n n0) key st0 - let ⟨ i1, _, _, _ ⟩ := node0 - let pending0 ← - betree.Node.apply_upserts_back (betree.List.Cons (k, - betree.Message.Upsert ufs) l) v key st1 - let msgs0 ← - betree.Node.lookup_first_message_for_key_back key msgs pending0 - let (st3, _) ← betree.store_internal_node i1 msgs0 st2 - Result.ret (st3, some v0) - | betree.List.Nil => + let ⟨ i, i1, n, n1 ⟩ := node + let (st1, msgs) ← betree.load_internal_node i st + let (pending, lookup_first_message_for_key_back) ← + betree.Node.lookup_first_message_for_key key msgs + match pending with + | betree.List.Cons p l => + let (k, msg) := p + if k != key + then do - let (st1, o) ← - betree.Internal.lookup_in_children (betree.Internal.mk i i0 n n0) - key st0 + let (st2, (o, i2)) ← + betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key + st1 + let _ ← + lookup_first_message_for_key_back (betree.List.Cons (k, msg) l) + Result.ret (st2, (o, betree.Node.Internal i2)) + else + match msg with + | betree.Message.Insert v => + do let _ ← - betree.Node.lookup_first_message_for_key_back key msgs - betree.List.Nil - Result.ret (st1, o) - | betree.Node.Leaf node => - do - let (st0, bindings) ← betree.load_leaf_node node.id st - let o ← betree.Node.lookup_in_bindings key bindings - Result.ret (st0, o) - -/- [betree_main::betree::{betree_main::betree::Node#5}::lookup]: backward function 0 - Source: 'src/betree.rs', lines 709:4-709:58 -/ -divergent def betree.Node.lookup_back - (self : betree.Node) (key : U64) (st : State) : Result betree.Node := - match self with - | betree.Node.Internal node => - do - let ⟨ i, i0, n, n0 ⟩ := node - let (st0, msgs) ← betree.load_internal_node i st - let pending ← betree.Node.lookup_first_message_for_key key msgs - match pending with - | betree.List.Cons p l => - let (k, msg) := p - if k != key - then + lookup_first_message_for_key_back (betree.List.Cons (k, + betree.Message.Insert v) l) + Result.ret (st1, (some v, betree.Node.Internal (betree.Internal.mk i + i1 n n1))) + | betree.Message.Delete => do - let _ ← - betree.Node.lookup_first_message_for_key_back key msgs - (betree.List.Cons (k, msg) l) - let node0 ← - betree.Internal.lookup_in_children_back (betree.Internal.mk i i0 - n n0) key st0 - Result.ret (betree.Node.Internal node0) - else - match msg with - | betree.Message.Insert v => - do - let _ ← - betree.Node.lookup_first_message_for_key_back key msgs - (betree.List.Cons (k, betree.Message.Insert v) l) - Result.ret (betree.Node.Internal (betree.Internal.mk i i0 n n0)) - | betree.Message.Delete => - do - let _ ← - betree.Node.lookup_first_message_for_key_back key msgs - (betree.List.Cons (k, betree.Message.Delete) l) - Result.ret (betree.Node.Internal (betree.Internal.mk i i0 n n0)) - | betree.Message.Upsert ufs => - do - let (st1, v) ← - betree.Internal.lookup_in_children (betree.Internal.mk i i0 n - n0) key st0 - let (st2, _) ← - betree.Node.apply_upserts (betree.List.Cons (k, - betree.Message.Upsert ufs) l) v key st1 - let node0 ← - betree.Internal.lookup_in_children_back (betree.Internal.mk i - i0 n n0) key st0 - let ⟨ i1, i2, n1, n2 ⟩ := node0 - let pending0 ← - betree.Node.apply_upserts_back (betree.List.Cons (k, - betree.Message.Upsert ufs) l) v key st1 - let msgs0 ← - betree.Node.lookup_first_message_for_key_back key msgs pending0 - let _ ← betree.store_internal_node i1 msgs0 st2 - Result.ret (betree.Node.Internal (betree.Internal.mk i1 i2 n1 - n2)) - | betree.List.Nil => - do let _ ← - betree.Node.lookup_first_message_for_key_back key msgs - betree.List.Nil - let node0 ← - betree.Internal.lookup_in_children_back (betree.Internal.mk i i0 n - n0) key st0 - Result.ret (betree.Node.Internal node0) + lookup_first_message_for_key_back (betree.List.Cons (k, + betree.Message.Delete) l) + Result.ret (st1, (none, betree.Node.Internal (betree.Internal.mk i i1 + n n1))) + | betree.Message.Upsert ufs => + do + let (st2, (v, i2)) ← + betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) + key st1 + let (st3, (v1, l1)) ← + betree.Node.apply_upserts (betree.List.Cons (k, + betree.Message.Upsert ufs) l) v key st2 + let ⟨ i3, i4, n2, n3 ⟩ := i2 + let msgs1 ← lookup_first_message_for_key_back l1 + let (st4, _) ← betree.store_internal_node i3 msgs1 st3 + Result.ret (st4, (some v1, betree.Node.Internal (betree.Internal.mk + i3 i4 n2 n3))) + | betree.List.Nil => + do + let (st2, (o, i2)) ← + betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key + st1 + let _ ← lookup_first_message_for_key_back betree.List.Nil + Result.ret (st2, (o, betree.Node.Internal i2)) | betree.Node.Leaf node => do - let (_, bindings) ← betree.load_leaf_node node.id st - let _ ← betree.Node.lookup_in_bindings key bindings - Result.ret (betree.Node.Leaf node) + let (st1, bindings) ← betree.load_leaf_node node.id st + let o ← betree.Node.lookup_in_bindings key bindings + Result.ret (st1, (o, betree.Node.Leaf node)) end -/- [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: Source: 'src/betree.rs', lines 674:4-674:77 -/ divergent def betree.Node.filter_messages_for_key (key : U64) (msgs : betree.List (U64 × betree.Message)) : @@ -517,33 +353,19 @@ divergent def betree.Node.filter_messages_for_key if k = key then do - let msgs0 ← - betree.List.pop_front_back (U64 × betree.Message) (betree.List.Cons - (k, m) l) - betree.Node.filter_messages_for_key key msgs0 + let (_, l1) ← + betree.List.pop_front (U64 × betree.Message) (betree.List.Cons (k, m) + l) + betree.Node.filter_messages_for_key key l1 else Result.ret (betree.List.Cons (k, m) l) | betree.List.Nil => Result.ret betree.List.Nil -/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: forward function +/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: Source: 'src/betree.rs', lines 689:4-692:34 -/ divergent def betree.Node.lookup_first_message_after_key (key : U64) (msgs : betree.List (U64 × betree.Message)) : - Result (betree.List (U64 × betree.Message)) - := - match msgs with - | betree.List.Cons p next_msgs => - let (k, m) := p - if k = key - then betree.Node.lookup_first_message_after_key key next_msgs - else Result.ret (betree.List.Cons (k, m) next_msgs) - | betree.List.Nil => Result.ret betree.List.Nil - -/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: backward function 0 - Source: 'src/betree.rs', lines 689:4-692:34 -/ -divergent def betree.Node.lookup_first_message_after_key_back - (key : U64) (msgs : betree.List (U64 × betree.Message)) - (ret : betree.List (U64 × betree.Message)) : - Result (betree.List (U64 × betree.Message)) + Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 × + betree.Message) → Result (betree.List (U64 × betree.Message)))) := match msgs with | betree.List.Cons p next_msgs => @@ -551,14 +373,22 @@ divergent def betree.Node.lookup_first_message_after_key_back if k = key then do - let next_msgs0 ← - betree.Node.lookup_first_message_after_key_back key next_msgs ret - Result.ret (betree.List.Cons (k, m) next_msgs0) - else Result.ret ret - | betree.List.Nil => Result.ret ret + let (l, lookup_first_message_after_key_back) ← + betree.Node.lookup_first_message_after_key key next_msgs + let back_'a := + fun ret => + do + let next_msgs1 ← lookup_first_message_after_key_back ret + Result.ret (betree.List.Cons (k, m) next_msgs1) + Result.ret (l, back_'a) + else + let back_'a := fun ret => Result.ret ret + Result.ret (betree.List.Cons (k, m) next_msgs, back_'a) + | betree.List.Nil => + let back_'a := fun ret => Result.ret ret + Result.ret (betree.List.Nil, back_'a) -/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: Source: 'src/betree.rs', lines 521:4-521:89 -/ def betree.Node.apply_to_internal (msgs : betree.List (U64 × betree.Message)) (key : U64) @@ -566,66 +396,63 @@ def betree.Node.apply_to_internal Result (betree.List (U64 × betree.Message)) := do - let msgs0 ← betree.Node.lookup_first_message_for_key key msgs - let b ← betree.ListTupleU64T.head_has_key betree.Message msgs0 key - if b - then - match new_msg with - | betree.Message.Insert i => + let (msgs1, lookup_first_message_for_key_back) ← + betree.Node.lookup_first_message_for_key key msgs + let b ← betree.ListTupleU64T.head_has_key betree.Message msgs1 key + if b + then + match new_msg with + | betree.Message.Insert i => + do + let l ← betree.Node.filter_messages_for_key key msgs1 + let l1 ← + betree.List.push_front (U64 × betree.Message) l (key, + betree.Message.Insert i) + lookup_first_message_for_key_back l1 + | betree.Message.Delete => + do + let l ← betree.Node.filter_messages_for_key key msgs1 + let l1 ← + betree.List.push_front (U64 × betree.Message) l (key, + betree.Message.Delete) + lookup_first_message_for_key_back l1 + | betree.Message.Upsert s => + do + let p ← betree.List.hd (U64 × betree.Message) msgs1 + let (_, m) := p + match m with + | betree.Message.Insert prev => do - let msgs1 ← betree.Node.filter_messages_for_key key msgs0 - let msgs2 ← - betree.List.push_front (U64 × betree.Message) msgs1 (key, - betree.Message.Insert i) - betree.Node.lookup_first_message_for_key_back key msgs msgs2 + let v ← betree.upsert_update (some prev) s + let (_, l) ← betree.List.pop_front (U64 × betree.Message) msgs1 + let l1 ← + betree.List.push_front (U64 × betree.Message) l (key, + betree.Message.Insert v) + lookup_first_message_for_key_back l1 | betree.Message.Delete => do - let msgs1 ← betree.Node.filter_messages_for_key key msgs0 - let msgs2 ← - betree.List.push_front (U64 × betree.Message) msgs1 (key, - betree.Message.Delete) - betree.Node.lookup_first_message_for_key_back key msgs msgs2 - | betree.Message.Upsert s => + let (_, l) ← betree.List.pop_front (U64 × betree.Message) msgs1 + let v ← betree.upsert_update none s + let l1 ← + betree.List.push_front (U64 × betree.Message) l (key, + betree.Message.Insert v) + lookup_first_message_for_key_back l1 + | betree.Message.Upsert _ => do - let p ← betree.List.hd (U64 × betree.Message) msgs0 - let (_, m) := p - match m with - | betree.Message.Insert prev => - do - let v ← betree.upsert_update (some prev) s - let msgs1 ← - betree.List.pop_front_back (U64 × betree.Message) msgs0 - let msgs2 ← - betree.List.push_front (U64 × betree.Message) msgs1 (key, - betree.Message.Insert v) - betree.Node.lookup_first_message_for_key_back key msgs msgs2 - | betree.Message.Delete => - do - let v ← betree.upsert_update none s - let msgs1 ← - betree.List.pop_front_back (U64 × betree.Message) msgs0 - let msgs2 ← - betree.List.push_front (U64 × betree.Message) msgs1 (key, - betree.Message.Insert v) - betree.Node.lookup_first_message_for_key_back key msgs msgs2 - | betree.Message.Upsert ufs => - do - let msgs1 ← - betree.Node.lookup_first_message_after_key key msgs0 - let msgs2 ← - betree.List.push_front (U64 × betree.Message) msgs1 (key, - betree.Message.Upsert s) - let msgs3 ← - betree.Node.lookup_first_message_after_key_back key msgs0 msgs2 - betree.Node.lookup_first_message_for_key_back key msgs msgs3 - else - do - let msgs1 ← - betree.List.push_front (U64 × betree.Message) msgs0 (key, new_msg) - betree.Node.lookup_first_message_for_key_back key msgs msgs1 + let (msgs2, lookup_first_message_after_key_back) ← + betree.Node.lookup_first_message_after_key key msgs1 + let l ← + betree.List.push_front (U64 × betree.Message) msgs2 (key, + betree.Message.Upsert s) + let msgs3 ← lookup_first_message_after_key_back l + lookup_first_message_for_key_back msgs3 + else + do + let l ← + betree.List.push_front (U64 × betree.Message) msgs1 (key, new_msg) + lookup_first_message_for_key_back l -/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: Source: 'src/betree.rs', lines 502:4-505:5 -/ divergent def betree.Node.apply_messages_to_internal (msgs : betree.List (U64 × betree.Message)) @@ -635,45 +462,40 @@ divergent def betree.Node.apply_messages_to_internal match new_msgs with | betree.List.Cons new_msg new_msgs_tl => do - let (i, m) := new_msg - let msgs0 ← betree.Node.apply_to_internal msgs i m - betree.Node.apply_messages_to_internal msgs0 new_msgs_tl + let (i, m) := new_msg + let l ← betree.Node.apply_to_internal msgs i m + betree.Node.apply_messages_to_internal l new_msgs_tl | betree.List.Nil => Result.ret msgs -/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: forward function +/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: Source: 'src/betree.rs', lines 653:4-656:32 -/ divergent def betree.Node.lookup_mut_in_bindings (key : U64) (bindings : betree.List (U64 × U64)) : - Result (betree.List (U64 × U64)) + Result ((betree.List (U64 × U64)) × (betree.List (U64 × U64) → Result + (betree.List (U64 × U64)))) := match bindings with | betree.List.Cons hd tl => - let (i, i0) := hd + let (i, i1) := hd if i >= key - then Result.ret (betree.List.Cons (i, i0) tl) - else betree.Node.lookup_mut_in_bindings key tl - | betree.List.Nil => Result.ret betree.List.Nil - -/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: backward function 0 - Source: 'src/betree.rs', lines 653:4-656:32 -/ -divergent def betree.Node.lookup_mut_in_bindings_back - (key : U64) (bindings : betree.List (U64 × U64)) - (ret : betree.List (U64 × U64)) : - Result (betree.List (U64 × U64)) - := - match bindings with - | betree.List.Cons hd tl => - let (i, i0) := hd - if i >= key - then Result.ret ret + then + let back_'a := fun ret => Result.ret ret + Result.ret (betree.List.Cons (i, i1) tl, back_'a) else do - let tl0 ← betree.Node.lookup_mut_in_bindings_back key tl ret - Result.ret (betree.List.Cons (i, i0) tl0) - | betree.List.Nil => Result.ret ret - -/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) + let (l, lookup_mut_in_bindings_back) ← + betree.Node.lookup_mut_in_bindings key tl + let back_'a := + fun ret => + do + let tl1 ← lookup_mut_in_bindings_back ret + Result.ret (betree.List.Cons (i, i1) tl1) + Result.ret (l, back_'a) + | betree.List.Nil => + let back_'a := fun ret => Result.ret ret + Result.ret (betree.List.Nil, back_'a) + +/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: Source: 'src/betree.rs', lines 460:4-460:87 -/ def betree.Node.apply_to_leaf (bindings : betree.List (U64 × U64)) (key : U64) (new_msg : betree.Message) @@ -681,49 +503,39 @@ def betree.Node.apply_to_leaf Result (betree.List (U64 × U64)) := do - let bindings0 ← betree.Node.lookup_mut_in_bindings key bindings - let b ← betree.ListTupleU64T.head_has_key U64 bindings0 key - if b - then + let (bindings1, lookup_mut_in_bindings_back) ← + betree.Node.lookup_mut_in_bindings key bindings + let b ← betree.ListTupleU64T.head_has_key U64 bindings1 key + if b + then + do + let (hd, l) ← betree.List.pop_front (U64 × U64) bindings1 + match new_msg with + | betree.Message.Insert v => do - let hd ← betree.List.pop_front (U64 × U64) bindings0 - match new_msg with - | betree.Message.Insert v => - do - let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0 - let bindings2 ← - betree.List.push_front (U64 × U64) bindings1 (key, v) - betree.Node.lookup_mut_in_bindings_back key bindings bindings2 - | betree.Message.Delete => - do - let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0 - betree.Node.lookup_mut_in_bindings_back key bindings bindings1 - | betree.Message.Upsert s => - do - let (_, i) := hd - let v ← betree.upsert_update (some i) s - let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0 - let bindings2 ← - betree.List.push_front (U64 × U64) bindings1 (key, v) - betree.Node.lookup_mut_in_bindings_back key bindings bindings2 - else - match new_msg with - | betree.Message.Insert v => - do - let bindings1 ← - betree.List.push_front (U64 × U64) bindings0 (key, v) - betree.Node.lookup_mut_in_bindings_back key bindings bindings1 - | betree.Message.Delete => - betree.Node.lookup_mut_in_bindings_back key bindings bindings0 - | betree.Message.Upsert s => - do - let v ← betree.upsert_update none s - let bindings1 ← - betree.List.push_front (U64 × U64) bindings0 (key, v) - betree.Node.lookup_mut_in_bindings_back key bindings bindings1 + let l1 ← betree.List.push_front (U64 × U64) l (key, v) + lookup_mut_in_bindings_back l1 + | betree.Message.Delete => lookup_mut_in_bindings_back l + | betree.Message.Upsert s => + do + let (_, i) := hd + let v ← betree.upsert_update (some i) s + let l1 ← betree.List.push_front (U64 × U64) l (key, v) + lookup_mut_in_bindings_back l1 + else + match new_msg with + | betree.Message.Insert v => + do + let l ← betree.List.push_front (U64 × U64) bindings1 (key, v) + lookup_mut_in_bindings_back l + | betree.Message.Delete => lookup_mut_in_bindings_back bindings1 + | betree.Message.Upsert s => + do + let v ← betree.upsert_update none s + let l ← betree.List.push_front (U64 × U64) bindings1 (key, v) + lookup_mut_in_bindings_back l -/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: Source: 'src/betree.rs', lines 444:4-447:5 -/ divergent def betree.Node.apply_messages_to_leaf (bindings : betree.List (U64 × U64)) @@ -733,337 +545,183 @@ divergent def betree.Node.apply_messages_to_leaf match new_msgs with | betree.List.Cons new_msg new_msgs_tl => do - let (i, m) := new_msg - let bindings0 ← betree.Node.apply_to_leaf bindings i m - betree.Node.apply_messages_to_leaf bindings0 new_msgs_tl + let (i, m) := new_msg + let l ← betree.Node.apply_to_leaf bindings i m + betree.Node.apply_messages_to_leaf l new_msgs_tl | betree.List.Nil => Result.ret bindings -/- [betree_main::betree::{betree_main::betree::Internal#4}::flush]: forward function +/- [betree_main::betree::{betree_main::betree::Internal#4}::flush]: Source: 'src/betree.rs', lines 410:4-415:26 -/ mutual divergent def betree.Internal.flush (self : betree.Internal) (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (content : betree.List (U64 × betree.Message)) (st : State) : - Result (State × (betree.List (U64 × betree.Message))) - := - do - let ⟨ _, i, n, n0 ⟩ := self - let p ← betree.ListTupleU64T.partition_at_pivot betree.Message content i - let (msgs_left, msgs_right) := p - let len_left ← betree.List.len (U64 × betree.Message) msgs_left - if len_left >= params.min_flush_size - then - do - let (st0, _) ← - betree.Node.apply_messages n params node_id_cnt msgs_left st - let (_, node_id_cnt0) ← - betree.Node.apply_messages_back n params node_id_cnt msgs_left st - let len_right ← betree.List.len (U64 × betree.Message) msgs_right - if len_right >= params.min_flush_size - then - do - let (st1, _) ← - betree.Node.apply_messages n0 params node_id_cnt0 msgs_right st0 - let _ ← - betree.Node.apply_messages_back n0 params node_id_cnt0 msgs_right - st0 - Result.ret (st1, betree.List.Nil) - else Result.ret (st0, msgs_right) - else - do - let (st0, _) ← - betree.Node.apply_messages n0 params node_id_cnt msgs_right st - let _ ← - betree.Node.apply_messages_back n0 params node_id_cnt msgs_right st - Result.ret (st0, msgs_left) - -/- [betree_main::betree::{betree_main::betree::Internal#4}::flush]: backward function 0 - Source: 'src/betree.rs', lines 410:4-415:26 -/ -divergent def betree.Internal.flush_back - (self : betree.Internal) (params : betree.Params) - (node_id_cnt : betree.NodeIdCounter) - (content : betree.List (U64 × betree.Message)) (st : State) : - Result (betree.Internal × betree.NodeIdCounter) + Result (State × ((betree.List (U64 × betree.Message)) × (betree.Internal + × betree.NodeIdCounter))) := do - let ⟨ i, i0, n, n0 ⟩ := self - let p ← betree.ListTupleU64T.partition_at_pivot betree.Message content i0 - let (msgs_left, msgs_right) := p - let len_left ← betree.List.len (U64 × betree.Message) msgs_left - if len_left >= params.min_flush_size + let ⟨ i, i1, n, n1 ⟩ := self + let p ← betree.ListTupleU64T.partition_at_pivot betree.Message content i1 + let (msgs_left, msgs_right) := p + let len_left ← betree.List.len (U64 × betree.Message) msgs_left + if len_left >= params.min_flush_size + then + do + let (st1, p1) ← + betree.Node.apply_messages n params node_id_cnt msgs_left st + let (n2, node_id_cnt1) := p1 + let len_right ← betree.List.len (U64 × betree.Message) msgs_right + if len_right >= params.min_flush_size then do - let (st0, _) ← - betree.Node.apply_messages 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 (U64 × betree.Message) msgs_right - if len_right >= params.min_flush_size - then - do - let (n2, node_id_cnt1) ← - betree.Node.apply_messages_back n0 params node_id_cnt0 msgs_right - st0 - Result.ret (betree.Internal.mk i i0 n1 n2, node_id_cnt1) - else Result.ret (betree.Internal.mk i i0 n1 n0, node_id_cnt0) + let (st2, p2) ← + betree.Node.apply_messages n1 params node_id_cnt1 msgs_right st1 + let (n3, node_id_cnt2) := p2 + Result.ret (st2, (betree.List.Nil, (betree.Internal.mk i i1 n2 n3, + node_id_cnt2))) else - do - let (n1, node_id_cnt0) ← - betree.Node.apply_messages_back n0 params node_id_cnt msgs_right st - Result.ret (betree.Internal.mk i i0 n n1, node_id_cnt0) - -/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: forward function - Source: 'src/betree.rs', lines 588:4-593:5 -/ -divergent def betree.Node.apply_messages - (self : betree.Node) (params : betree.Params) - (node_id_cnt : betree.NodeIdCounter) - (msgs : betree.List (U64 × betree.Message)) (st : State) : - Result (State × Unit) - := - match self with - | betree.Node.Internal node => - do - let ⟨ i, i0, n, n0 ⟩ := node - let (st0, content) ← betree.load_internal_node i st - let content0 ← betree.Node.apply_messages_to_internal content msgs - let num_msgs ← betree.List.len (U64 × betree.Message) content0 - if num_msgs >= params.min_flush_size - then - do - let (st1, content1) ← - betree.Internal.flush (betree.Internal.mk i i0 n n0) params - node_id_cnt content0 st0 - let (node0, _) ← - betree.Internal.flush_back (betree.Internal.mk i i0 n n0) params - node_id_cnt content0 st0 - let ⟨ i1, _, _, _ ⟩ := node0 - let (st2, _) ← betree.store_internal_node i1 content1 st1 - Result.ret (st2, ()) - else - do - let (st1, _) ← betree.store_internal_node i content0 st0 - Result.ret (st1, ()) - | betree.Node.Leaf node => + Result.ret (st1, (msgs_right, (betree.Internal.mk i i1 n2 n1, + node_id_cnt1))) + else do - let (st0, content) ← betree.load_leaf_node node.id st - let content0 ← betree.Node.apply_messages_to_leaf content msgs - let len ← betree.List.len (U64 × U64) content0 - let i ← 2#u64 * params.split_size - if len >= i - then - do - let (st1, _) ← - betree.Leaf.split node content0 params node_id_cnt st0 - let (st2, _) ← betree.store_leaf_node node.id betree.List.Nil st1 - Result.ret (st2, ()) - else - do - let (st1, _) ← betree.store_leaf_node node.id content0 st0 - Result.ret (st1, ()) + let (st1, p1) ← + betree.Node.apply_messages n1 params node_id_cnt msgs_right st + let (n2, node_id_cnt1) := p1 + Result.ret (st1, (msgs_left, (betree.Internal.mk i i1 n n2, node_id_cnt1))) -/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: backward function 0 +/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: Source: 'src/betree.rs', lines 588:4-593:5 -/ -divergent def betree.Node.apply_messages_back +divergent def betree.Node.apply_messages (self : betree.Node) (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (msgs : betree.List (U64 × betree.Message)) (st : State) : - Result (betree.Node × betree.NodeIdCounter) + Result (State × (betree.Node × betree.NodeIdCounter)) := match self with | betree.Node.Internal node => do - let ⟨ i, i0, n, n0 ⟩ := node - let (st0, content) ← betree.load_internal_node i st - let content0 ← betree.Node.apply_messages_to_internal content msgs - let num_msgs ← betree.List.len (U64 × betree.Message) content0 - if num_msgs >= params.min_flush_size - then - do - let (st1, content1) ← - betree.Internal.flush (betree.Internal.mk i i0 n n0) params - node_id_cnt content0 st0 - let (node0, node_id_cnt0) ← - betree.Internal.flush_back (betree.Internal.mk i i0 n n0) params - node_id_cnt content0 st0 - let ⟨ i1, i2, n1, n2 ⟩ := node0 - let _ ← betree.store_internal_node i1 content1 st1 - Result.ret (betree.Node.Internal (betree.Internal.mk i1 i2 n1 n2), - node_id_cnt0) - else - do - let _ ← betree.store_internal_node i content0 st0 - Result.ret (betree.Node.Internal (betree.Internal.mk i i0 n n0), - node_id_cnt) + let ⟨ i, i1, n, n1 ⟩ := node + let (st1, content) ← betree.load_internal_node i st + let l ← betree.Node.apply_messages_to_internal content msgs + let num_msgs ← betree.List.len (U64 × betree.Message) l + if num_msgs >= params.min_flush_size + then + do + let (st2, (content1, p)) ← + betree.Internal.flush (betree.Internal.mk i i1 n n1) params node_id_cnt + l st1 + let (node1, node_id_cnt1) := p + let ⟨ i2, i3, n2, n3 ⟩ := node1 + let (st3, _) ← betree.store_internal_node i2 content1 st2 + Result.ret (st3, (betree.Node.Internal (betree.Internal.mk i2 i3 n2 n3), + node_id_cnt1)) + else + do + let (st2, _) ← betree.store_internal_node i l st1 + Result.ret (st2, (betree.Node.Internal (betree.Internal.mk i i1 n n1), + node_id_cnt)) | betree.Node.Leaf node => do - let (st0, content) ← betree.load_leaf_node node.id st - let content0 ← betree.Node.apply_messages_to_leaf content msgs - let len ← betree.List.len (U64 × U64) content0 - let i ← 2#u64 * params.split_size - if len >= i - then - do - let (st1, new_node) ← - betree.Leaf.split node content0 params node_id_cnt st0 - let _ ← betree.store_leaf_node node.id betree.List.Nil st1 - let node_id_cnt0 ← - betree.Leaf.split_back node content0 params node_id_cnt st0 - Result.ret (betree.Node.Internal new_node, node_id_cnt0) - else - do - let _ ← betree.store_leaf_node node.id content0 st0 - Result.ret (betree.Node.Leaf { node with size := len }, node_id_cnt) + let (st1, content) ← betree.load_leaf_node node.id st + let l ← betree.Node.apply_messages_to_leaf content msgs + let len ← betree.List.len (U64 × U64) l + let i ← 2#u64 * params.split_size + if len >= i + then + do + let (st2, (new_node, nic)) ← + betree.Leaf.split node l params node_id_cnt st1 + let (st3, _) ← betree.store_leaf_node node.id betree.List.Nil st2 + Result.ret (st3, (betree.Node.Internal new_node, nic)) + else + do + let (st2, _) ← betree.store_leaf_node node.id l st1 + Result.ret (st2, (betree.Node.Leaf { node with size := len }, + node_id_cnt)) end -/- [betree_main::betree::{betree_main::betree::Node#5}::apply]: forward function +/- [betree_main::betree::{betree_main::betree::Node#5}::apply]: Source: 'src/betree.rs', lines 576:4-582:5 -/ def betree.Node.apply (self : betree.Node) (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (key : U64) (new_msg : betree.Message) (st : State) : - Result (State × Unit) + Result (State × (betree.Node × betree.NodeIdCounter)) := do - let l := betree.List.Nil - let (st0, _) ← - betree.Node.apply_messages self params node_id_cnt (betree.List.Cons - (key, new_msg) l) st - let _ ← - betree.Node.apply_messages_back self params node_id_cnt (betree.List.Cons - (key, new_msg) l) st - Result.ret (st0, ()) - -/- [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0 - Source: 'src/betree.rs', lines 576:4-582:5 -/ -def betree.Node.apply_back - (self : betree.Node) (params : betree.Params) - (node_id_cnt : betree.NodeIdCounter) (key : U64) (new_msg : betree.Message) - (st : State) : - Result (betree.Node × betree.NodeIdCounter) - := let l := betree.List.Nil - betree.Node.apply_messages_back self params node_id_cnt (betree.List.Cons - (key, new_msg) l) st + let (st1, p) ← + betree.Node.apply_messages self params node_id_cnt (betree.List.Cons (key, + new_msg) l) st + let (self1, node_id_cnt1) := p + Result.ret (st1, (self1, node_id_cnt1)) -/- [betree_main::betree::{betree_main::betree::BeTree#6}::new]: forward function +/- [betree_main::betree::{betree_main::betree::BeTree#6}::new]: Source: 'src/betree.rs', lines 849:4-849:60 -/ def betree.BeTree.new (min_flush_size : U64) (split_size : U64) (st : State) : Result (State × betree.BeTree) := do - let node_id_cnt ← betree.NodeIdCounter.new - let id ← betree.NodeIdCounter.fresh_id node_id_cnt - let (st0, _) ← betree.store_leaf_node id betree.List.Nil st - let node_id_cnt0 ← betree.NodeIdCounter.fresh_id_back node_id_cnt - Result.ret (st0, - { - params := - { min_flush_size := min_flush_size, split_size := split_size }, - node_id_cnt := node_id_cnt0, - root := (betree.Node.Leaf { id := id, size := 0#u64 }) - }) - -/- [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: forward function + let node_id_cnt ← betree.NodeIdCounter.new + let (id, nic) ← betree.NodeIdCounter.fresh_id node_id_cnt + let (st1, _) ← betree.store_leaf_node id betree.List.Nil st + Result.ret (st1, + { + params := { min_flush_size := min_flush_size, split_size := split_size }, + node_id_cnt := nic, + root := (betree.Node.Leaf { id := id, size := 0#u64 }) + }) + +/- [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: Source: 'src/betree.rs', lines 868:4-868:47 -/ def betree.BeTree.apply (self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) : - Result (State × Unit) - := - do - let (st0, _) ← - betree.Node.apply self.root self.params self.node_id_cnt key msg st - let _ ← - betree.Node.apply_back self.root self.params self.node_id_cnt key msg st - Result.ret (st0, ()) - -/- [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: backward function 0 - Source: 'src/betree.rs', lines 868:4-868:47 -/ -def betree.BeTree.apply_back - (self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) : - Result betree.BeTree + Result (State × betree.BeTree) := do - let (n, nic) ← - betree.Node.apply_back self.root self.params self.node_id_cnt key msg st - Result.ret { self with node_id_cnt := nic, root := n } + let (st1, p) ← + betree.Node.apply self.root self.params self.node_id_cnt key msg st + let (n, nic) := p + Result.ret (st1, { self with node_id_cnt := nic, root := n }) -/- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: forward function +/- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: Source: 'src/betree.rs', lines 874:4-874:52 -/ def betree.BeTree.insert (self : betree.BeTree) (key : U64) (value : U64) (st : State) : - Result (State × Unit) - := - do - let (st0, _) ← - betree.BeTree.apply self key (betree.Message.Insert value) st - let _ ← - betree.BeTree.apply_back self key (betree.Message.Insert value) st - Result.ret (st0, ()) - -/- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: backward function 0 - Source: 'src/betree.rs', lines 874:4-874:52 -/ -def betree.BeTree.insert_back - (self : betree.BeTree) (key : U64) (value : U64) (st : State) : - Result betree.BeTree + Result (State × betree.BeTree) := - betree.BeTree.apply_back self key (betree.Message.Insert value) st + betree.BeTree.apply self key (betree.Message.Insert value) st -/- [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: forward function +/- [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: Source: 'src/betree.rs', lines 880:4-880:38 -/ def betree.BeTree.delete - (self : betree.BeTree) (key : U64) (st : State) : Result (State × Unit) := - do - let (st0, _) ← betree.BeTree.apply self key betree.Message.Delete st - let _ ← betree.BeTree.apply_back self key betree.Message.Delete st - Result.ret (st0, ()) - -/- [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: backward function 0 - Source: 'src/betree.rs', lines 880:4-880:38 -/ -def betree.BeTree.delete_back - (self : betree.BeTree) (key : U64) (st : State) : Result betree.BeTree := - betree.BeTree.apply_back self key betree.Message.Delete st - -/- [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: forward function - Source: 'src/betree.rs', lines 886:4-886:59 -/ -def betree.BeTree.upsert - (self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State) - : - Result (State × Unit) + (self : betree.BeTree) (key : U64) (st : State) : + Result (State × betree.BeTree) := - do - let (st0, _) ← - betree.BeTree.apply self key (betree.Message.Upsert upd) st - let _ ← betree.BeTree.apply_back self key (betree.Message.Upsert upd) st - Result.ret (st0, ()) + betree.BeTree.apply self key betree.Message.Delete st -/- [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: backward function 0 +/- [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: Source: 'src/betree.rs', lines 886:4-886:59 -/ -def betree.BeTree.upsert_back +def betree.BeTree.upsert (self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State) : - Result betree.BeTree + Result (State × betree.BeTree) := - betree.BeTree.apply_back self key (betree.Message.Upsert upd) st + betree.BeTree.apply self key (betree.Message.Upsert upd) st -/- [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: forward function +/- [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: Source: 'src/betree.rs', lines 895:4-895:62 -/ def betree.BeTree.lookup (self : betree.BeTree) (key : U64) (st : State) : - Result (State × (Option U64)) + Result (State × ((Option U64) × betree.BeTree)) := - betree.Node.lookup self.root key st - -/- [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: backward function 0 - Source: 'src/betree.rs', lines 895:4-895:62 -/ -def betree.BeTree.lookup_back - (self : betree.BeTree) (key : U64) (st : State) : Result betree.BeTree := do - let n ← betree.Node.lookup_back self.root key st - Result.ret { self with root := n } + let (st1, (o, n)) ← betree.Node.lookup self.root key st + Result.ret (st1, (o, { self with root := n })) -/- [betree_main::main]: forward function +/- [betree_main::main]: Source: 'src/betree_main.rs', lines 5:0-5:9 -/ def main : Result Unit := Result.ret () |