diff options
Diffstat (limited to 'tests/coq/betree/BetreeMain__Funs.v')
| -rw-r--r-- | tests/coq/betree/BetreeMain__Funs.v | 1394 |
1 files changed, 1394 insertions, 0 deletions
diff --git a/tests/coq/betree/BetreeMain__Funs.v b/tests/coq/betree/BetreeMain__Funs.v new file mode 100644 index 00000000..a8bb9b74 --- /dev/null +++ b/tests/coq/betree/BetreeMain__Funs.v @@ -0,0 +1,1394 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree_main]: function definitions *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Local Open Scope Primitives_scope. +Require Export BetreeMain__Types . +Import BetreeMain__Types . +Require Export BetreeMain__Opaque . +Import BetreeMain__Opaque . +Module BetreeMain__Funs . + +(** [betree_main::betree::load_internal_node] *) +Definition betree_load_internal_node_fwd + (id : u64) (st : state) : + result (state * (Betree_list_t (u64 * Betree_message_t))) + := + p <- betree_utils_load_internal_node_fwd id st; + let (st0, l) := p in + Return (st0, l) + . + +(** [betree_main::betree::store_internal_node] *) +Definition betree_store_internal_node_fwd + (id : u64) (content : Betree_list_t (u64 * Betree_message_t)) (st : state) : + result (state * unit) + := + p <- betree_utils_store_internal_node_fwd id content st; + let (st0, _) := p in + Return (st0, tt) + . + +(** [betree_main::betree::load_leaf_node] *) +Definition betree_load_leaf_node_fwd + (id : u64) (st : state) : result (state * (Betree_list_t (u64 * u64))) := + p <- betree_utils_load_leaf_node_fwd id st; + let (st0, l) := p in + Return (st0, l) + . + +(** [betree_main::betree::store_leaf_node] *) +Definition betree_store_leaf_node_fwd + (id : u64) (content : Betree_list_t (u64 * u64)) (st : state) : + result (state * unit) + := + p <- betree_utils_store_leaf_node_fwd id content st; + let (st0, _) := p in + Return (st0, tt) + . + +(** [betree_main::betree::fresh_node_id] *) +Definition betree_fresh_node_id_fwd (counter : u64) : result u64 := + i <- u64_add counter 1 %u64; let _ := i in Return counter . + +(** [betree_main::betree::fresh_node_id] *) +Definition betree_fresh_node_id_back (counter : u64) : result u64 := + counter0 <- u64_add counter 1 %u64; Return counter0 . + +(** [betree_main::betree::NodeIdCounter::{0}::new] *) +Definition betree_node_id_counter_new_fwd : result Betree_node_id_counter_t := + Return (mkBetree_node_id_counter_t (0 %u64)) . + +(** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *) +Definition betree_node_id_counter_fresh_id_fwd + (self : Betree_node_id_counter_t) : result u64 := + match self with + | mkBetree_node_id_counter_t id => + i <- u64_add id 1 %u64; let _ := i in Return id + end + . + +(** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *) +Definition betree_node_id_counter_fresh_id_back + (self : Betree_node_id_counter_t) : result Betree_node_id_counter_t := + match self with + | mkBetree_node_id_counter_t id => + i <- u64_add id 1 %u64; Return (mkBetree_node_id_counter_t i) + end + . + +(** [core::num::u64::{10}::MAX] *) +Definition core_num_u64_max_body : result u64 := + Return (18446744073709551615 %u64) + . +Definition core_num_u64_max_c : u64 := core_num_u64_max_body%global . + +(** [betree_main::betree::upsert_update] *) +Definition betree_upsert_update_fwd + (prev : option u64) (st : Betree_upsert_fun_state_t) : result u64 := + match prev with + | None => + match st with + | BetreeUpsertFunStateAdd v => Return v + | BetreeUpsertFunStateSub i => Return (0 %u64) + end + | Some prev0 => + match st with + | BetreeUpsertFunStateAdd v => + margin <- u64_sub core_num_u64_max_c prev0; + if margin s>= v + then (i <- u64_add prev0 v; Return i) + else Return core_num_u64_max_c + | BetreeUpsertFunStateSub v => + if prev0 s>= v then (i <- u64_sub prev0 v; Return i) else Return (0 %u64) + end + end + . + +(** [betree_main::betree::List::{1}::len] *) +Fixpoint betree_list_len_fwd + (T : Type) (n : nat) (self : Betree_list_t T) : result u64 := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | BetreeListCons t tl => + i <- betree_list_len_fwd T n0 tl; i0 <- u64_add 1 %u64 i; Return i0 + | BetreeListNil => Return (0 %u64) + end + end + . + +(** [betree_main::betree::List::{1}::split_at] *) +Fixpoint betree_list_split_at_fwd + (T : Type) (n : nat) (self : Betree_list_t T) (n0 : u64) : + result ((Betree_list_t T) * (Betree_list_t T)) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + if n0 s= 0 %u64 + then Return (BetreeListNil, self) + else + match self with + | BetreeListCons hd tl => + i <- u64_sub n0 1 %u64; + p <- betree_list_split_at_fwd T n1 tl i; + let (ls0, ls1) := p in + let l := ls0 in + Return (BetreeListCons hd l, ls1) + | BetreeListNil => Fail_ Failure + end + end + . + +(** [betree_main::betree::List::{1}::push_front] *) +Definition 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 BetreeListNil in + let l := tl in + Return (BetreeListCons x l) + . + +(** [betree_main::betree::List::{1}::pop_front] *) +Definition betree_list_pop_front_fwd + (T : Type) (self : Betree_list_t T) : result T := + let ls := mem_replace_fwd (Betree_list_t T) self BetreeListNil in + match ls with + | BetreeListCons x tl => Return x + | BetreeListNil => Fail_ Failure + end + . + +(** [betree_main::betree::List::{1}::pop_front] *) +Definition 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 BetreeListNil in + match ls with + | BetreeListCons x tl => Return tl + | BetreeListNil => Fail_ Failure + end + . + +(** [betree_main::betree::List::{1}::hd] *) +Definition betree_list_hd_fwd (T : Type) (self : Betree_list_t T) : result T := + match self with + | BetreeListCons hd l => Return hd + | BetreeListNil => Fail_ Failure + end + . + +(** [betree_main::betree::List::{2}::head_has_key] *) +Definition betree_list_head_has_key_fwd + (T : Type) (self : Betree_list_t (u64 * T)) (key : u64) : result bool := + match self with + | BetreeListCons hd l => let (i, _) := hd in Return (i s= key) + | BetreeListNil => Return false + end + . + +(** [betree_main::betree::List::{2}::partition_at_pivot] *) +Fixpoint betree_list_partition_at_pivot_fwd + (T : Type) (n : nat) (self : Betree_list_t (u64 * T)) (pivot : u64) : + result ((Betree_list_t (u64 * T)) * (Betree_list_t (u64 * T))) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | BetreeListCons hd tl => + let (i, t) := hd in + if i s>= pivot + then Return (BetreeListNil, BetreeListCons (i, t) tl) + else ( + p <- betree_list_partition_at_pivot_fwd T n0 tl pivot; + let (ls0, ls1) := p in + let l := ls0 in + Return (BetreeListCons (i, t) l, ls1)) + | BetreeListNil => Return (BetreeListNil, BetreeListNil) + end + end + . + +(** [betree_main::betree::Leaf::{3}::split] *) +Definition betree_leaf_split_fwd + (n : nat) (self : Betree_leaf_t) (content : Betree_list_t (u64 * u64)) + (params : Betree_params_t) (node_id_cnt : Betree_node_id_counter_t) + (st : state) : + result (state * Betree_internal_t) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match params with + | mkBetree_params_t i i0 => + p <- betree_list_split_at_fwd (u64 * u64) n0 content i0; + let (content0, content1) := p in + p0 <- betree_list_hd_fwd (u64 * u64) content1; + let (pivot, _) := p0 in + id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt; + node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt; + id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0; + p1 <- betree_store_leaf_node_fwd id0 content0 st; + let (st0, _) := p1 in + p2 <- betree_store_leaf_node_fwd id1 content1 st0; + let (st1, _) := p2 in + match self with + | mkBetree_leaf_t i1 i2 => + let n1 := BetreeNodeLeaf (mkBetree_leaf_t id0 i0) in + let n2 := BetreeNodeLeaf (mkBetree_leaf_t id1 i0) in + Return (st1, mkBetree_internal_t i1 pivot n1 n2) + end + end + end + . + +(** [betree_main::betree::Leaf::{3}::split] *) +Definition betree_leaf_split_back + (n : nat) (self : Betree_leaf_t) (content : Betree_list_t (u64 * u64)) + (params : Betree_params_t) (node_id_cnt : Betree_node_id_counter_t) + (st : state) : + result Betree_node_id_counter_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match params with + | mkBetree_params_t i i0 => + p <- betree_list_split_at_fwd (u64 * u64) n0 content i0; + let (content0, content1) := p in + p0 <- betree_list_hd_fwd (u64 * u64) content1; + let _ := p0 in + id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt; + node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt; + id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0; + p1 <- betree_store_leaf_node_fwd id0 content0 st; + let (st0, _) := p1 in + p2 <- betree_store_leaf_node_fwd id1 content1 st0; + let (_, _) := p2 in + match self with + | mkBetree_leaf_t i1 i2 => + node_id_cnt1 <- betree_node_id_counter_fresh_id_back node_id_cnt0; + Return node_id_cnt1 + end + end + end + . + +(** [betree_main::betree::Node::{5}::lookup_in_bindings] *) +Fixpoint betree_node_lookup_in_bindings_fwd + (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) : + result (option u64) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match bindings with + | BetreeListCons hd tl => + let (i, i0) := hd in + if i s= key + then Return (Some i0) + else + if i s> key + then Return None + else (opt <- betree_node_lookup_in_bindings_fwd n0 key tl; Return opt) + | BetreeListNil => Return None + end + end + . + +(** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *) +Fixpoint betree_node_lookup_first_message_for_key_fwd + (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match msgs with + | BetreeListCons x next_msgs => + let (i, m) := x in + if i s>= key + then Return (BetreeListCons (i, m) next_msgs) + else ( + l <- betree_node_lookup_first_message_for_key_fwd n0 key next_msgs; + Return l) + | BetreeListNil => Return BetreeListNil + end + end + . + +(** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *) +Fixpoint betree_node_lookup_first_message_for_key_back + (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) + (ret : Betree_list_t (u64 * Betree_message_t)) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match msgs with + | BetreeListCons x next_msgs => + let (i, m) := x in + if i s>= key + then Return ret + else ( + next_msgs0 <- + betree_node_lookup_first_message_for_key_back n0 key next_msgs ret; + Return (BetreeListCons (i, m) next_msgs0)) + | BetreeListNil => Return ret + end + end + . + +(** [betree_main::betree::Node::{5}::apply_upserts] *) +Fixpoint betree_node_apply_upserts_fwd + (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t)) (prev : option u64) + (key : u64) (st : state) : + result (state * u64) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + b <- betree_list_head_has_key_fwd Betree_message_t msgs key; + if b + then ( + msg <- betree_list_pop_front_fwd (u64 * Betree_message_t) msgs; + let (_, m) := msg in + match m with + | BetreeMessageInsert i => Fail_ Failure + | BetreeMessageDelete => Fail_ Failure + | BetreeMessageUpsert s => + v <- betree_upsert_update_fwd prev s; + msgs0 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs; + p <- betree_node_apply_upserts_fwd n0 msgs0 (Some v) key st; + let (st0, i) := p in + Return (st0, i) + end) + else ( + p <- core_option_option_unwrap_fwd u64 prev st; + let (st0, v) := p in + l <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs (key, + BetreeMessageInsert v); + let _ := l in + Return (st0, v)) + end + . + +(** [betree_main::betree::Node::{5}::apply_upserts] *) +Fixpoint betree_node_apply_upserts_back + (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t)) (prev : option u64) + (key : u64) (st : state) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + b <- betree_list_head_has_key_fwd Betree_message_t msgs key; + if b + then ( + msg <- betree_list_pop_front_fwd (u64 * Betree_message_t) msgs; + let (_, m) := msg in + match m with + | BetreeMessageInsert i => Fail_ Failure + | BetreeMessageDelete => Fail_ Failure + | BetreeMessageUpsert s => + v <- betree_upsert_update_fwd prev s; + msgs0 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs; + msgs1 <- betree_node_apply_upserts_back n0 msgs0 (Some v) key st; + Return msgs1 + end) + else ( + p <- core_option_option_unwrap_fwd u64 prev st; + let (_, v) := p in + msgs0 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs (key, + BetreeMessageInsert v); + Return msgs0) + end + . + +(** [betree_main::betree::Node::{5}::lookup] *) +Fixpoint betree_node_lookup_fwd + (n : nat) (self : Betree_node_t) (key : u64) (st : state) : + result (state * (option u64)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | BetreeNodeInternal node => + match node with + | mkBetree_internal_t i i0 n1 n2 => + p <- betree_load_internal_node_fwd i st; + let (st0, msgs) := p in + pending <- betree_node_lookup_first_message_for_key_fwd n0 key msgs; + match pending with + | BetreeListCons p0 l => + let (k, msg) := p0 in + if k s<> key + then ( + p1 <- + betree_internal_lookup_in_children_fwd n0 (mkBetree_internal_t i + i0 n1 n2) key st0; + let (st1, opt) := p1 in + l0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + (BetreeListCons (k, msg) l); + let _ := l0 in + Return (st1, opt)) + else + match msg with + | BetreeMessageInsert v => + l0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + (BetreeListCons (k, BetreeMessageInsert v) l); + let _ := l0 in + Return (st0, Some v) + | BetreeMessageDelete => + l0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + (BetreeListCons (k, BetreeMessageDelete) l); + let _ := l0 in + Return (st0, None) + | BetreeMessageUpsert ufs => + p1 <- + betree_internal_lookup_in_children_fwd n0 (mkBetree_internal_t + i i0 n1 n2) key st0; + let (st1, v) := p1 in + p2 <- + betree_node_apply_upserts_fwd n0 (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st1; + let (st2, v0) := p2 in + node0 <- + betree_internal_lookup_in_children_back n0 (mkBetree_internal_t + i i0 n1 n2) key st0; + match node0 with + | mkBetree_internal_t i1 i2 n3 n4 => + pending0 <- + betree_node_apply_upserts_back n0 (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st1; + msgs0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + pending0; + p3 <- betree_store_internal_node_fwd i1 msgs0 st2; + let (st3, _) := p3 in + Return (st3, Some v0) + end + end + | BetreeListNil => + p0 <- + betree_internal_lookup_in_children_fwd n0 (mkBetree_internal_t i i0 + n1 n2) key st0; + let (st1, opt) := p0 in + l <- + betree_node_lookup_first_message_for_key_back n0 key msgs + BetreeListNil; + let _ := l in + Return (st1, opt) + end + end + | BetreeNodeLeaf node => + match node with + | mkBetree_leaf_t i i0 => + p <- betree_load_leaf_node_fwd i st; + let (st0, bindings) := p in + opt <- betree_node_lookup_in_bindings_fwd n0 key bindings; + Return (st0, opt) + end + end + end + +(** [betree_main::betree::Node::{5}::lookup] *) +with betree_node_lookup_back + (n : nat) (self : Betree_node_t) (key : u64) (st : state) : + result Betree_node_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | BetreeNodeInternal node => + match node with + | mkBetree_internal_t i i0 n1 n2 => + p <- betree_load_internal_node_fwd i st; + let (st0, msgs) := p in + pending <- betree_node_lookup_first_message_for_key_fwd n0 key msgs; + match pending with + | BetreeListCons p0 l => + let (k, msg) := p0 in + if k s<> key + then ( + l0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + (BetreeListCons (k, msg) l); + let _ := l0 in + node0 <- + betree_internal_lookup_in_children_back n0 (mkBetree_internal_t i + i0 n1 n2) key st0; + Return (BetreeNodeInternal node0)) + else + match msg with + | BetreeMessageInsert v => + l0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + (BetreeListCons (k, BetreeMessageInsert v) l); + let _ := l0 in + Return (BetreeNodeInternal (mkBetree_internal_t i i0 n1 n2)) + | BetreeMessageDelete => + l0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + (BetreeListCons (k, BetreeMessageDelete) l); + let _ := l0 in + Return (BetreeNodeInternal (mkBetree_internal_t i i0 n1 n2)) + | BetreeMessageUpsert ufs => + p1 <- + betree_internal_lookup_in_children_fwd n0 (mkBetree_internal_t + i i0 n1 n2) key st0; + let (st1, v) := p1 in + p2 <- + betree_node_apply_upserts_fwd n0 (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st1; + let (st2, _) := p2 in + node0 <- + betree_internal_lookup_in_children_back n0 (mkBetree_internal_t + i i0 n1 n2) key st0; + match node0 with + | mkBetree_internal_t i1 i2 n3 n4 => + pending0 <- + betree_node_apply_upserts_back n0 (BetreeListCons (k, + BetreeMessageUpsert ufs) l) v key st1; + msgs0 <- + betree_node_lookup_first_message_for_key_back n0 key msgs + pending0; + p3 <- betree_store_internal_node_fwd i1 msgs0 st2; + let (_, _) := p3 in + Return (BetreeNodeInternal (mkBetree_internal_t i1 i2 n3 n4)) + end + end + | BetreeListNil => + l <- + betree_node_lookup_first_message_for_key_back n0 key msgs + BetreeListNil; + let _ := l in + node0 <- + betree_internal_lookup_in_children_back n0 (mkBetree_internal_t i + i0 n1 n2) key st0; + Return (BetreeNodeInternal node0) + end + end + | BetreeNodeLeaf node => + match node with + | mkBetree_leaf_t i i0 => + p <- betree_load_leaf_node_fwd i st; + let (_, bindings) := p in + opt <- betree_node_lookup_in_bindings_fwd n0 key bindings; + let _ := opt in + Return (BetreeNodeLeaf (mkBetree_leaf_t i i0)) + end + end + end + +(** [betree_main::betree::Internal::{4}::lookup_in_children] *) +with betree_internal_lookup_in_children_fwd + (n : nat) (self : Betree_internal_t) (key : u64) (st : state) : + result (state * (option u64)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_internal_t i i0 n1 n2 => + if key s< i0 + then ( + p <- betree_node_lookup_fwd n0 n1 key st; + let (st0, opt) := p in + Return (st0, opt)) + else ( + p <- betree_node_lookup_fwd n0 n2 key st; + let (st0, opt) := p in + Return (st0, opt)) + end + end + +(** [betree_main::betree::Internal::{4}::lookup_in_children] *) +with betree_internal_lookup_in_children_back + (n : nat) (self : Betree_internal_t) (key : u64) (st : state) : + result Betree_internal_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_internal_t i i0 n1 n2 => + if key s< i0 + then ( + n3 <- betree_node_lookup_back n0 n1 key st; + Return (mkBetree_internal_t i i0 n3 n2)) + else ( + n3 <- betree_node_lookup_back n0 n2 key st; + Return (mkBetree_internal_t i i0 n1 n3)) + end + end + . + +(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *) +Fixpoint betree_node_lookup_mut_in_bindings_fwd + (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) : + result (Betree_list_t (u64 * u64)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match bindings with + | BetreeListCons hd tl => + let (i, i0) := hd in + if i s>= key + then Return (BetreeListCons (i, i0) tl) + else (l <- betree_node_lookup_mut_in_bindings_fwd n0 key tl; Return l) + | BetreeListNil => Return BetreeListNil + end + end + . + +(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *) +Fixpoint betree_node_lookup_mut_in_bindings_back + (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) + (ret : Betree_list_t (u64 * u64)) : + result (Betree_list_t (u64 * u64)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match bindings with + | BetreeListCons hd tl => + let (i, i0) := hd in + if i s>= key + then Return ret + else ( + tl0 <- betree_node_lookup_mut_in_bindings_back n0 key tl ret; + Return (BetreeListCons (i, i0) tl0)) + | BetreeListNil => Return ret + end + end + . + +(** [betree_main::betree::Node::{5}::apply_to_leaf] *) +Definition betree_node_apply_to_leaf_fwd_back + (n : nat) (bindings : Betree_list_t (u64 * u64)) (key : u64) + (new_msg : Betree_message_t) : + result (Betree_list_t (u64 * u64)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + bindings0 <- betree_node_lookup_mut_in_bindings_fwd n0 key bindings; + b <- betree_list_head_has_key_fwd u64 bindings0 key; + if b + then ( + hd <- betree_list_pop_front_fwd (u64 * u64) bindings0; + match new_msg with + | BetreeMessageInsert v => + bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0; + bindings2 <- + betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v); + bindings3 <- + betree_node_lookup_mut_in_bindings_back n0 key bindings bindings2; + Return bindings3 + | BetreeMessageDelete => + bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0; + bindings2 <- + betree_node_lookup_mut_in_bindings_back n0 key bindings bindings1; + Return bindings2 + | BetreeMessageUpsert s => + let (_, i) := hd in + v <- betree_upsert_update_fwd (Some i) s; + bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0; + bindings2 <- + betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v); + bindings3 <- + betree_node_lookup_mut_in_bindings_back n0 key bindings bindings2; + Return bindings3 + end) + else + match new_msg with + | BetreeMessageInsert v => + bindings1 <- + betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v); + bindings2 <- + betree_node_lookup_mut_in_bindings_back n0 key bindings bindings1; + Return bindings2 + | BetreeMessageDelete => + bindings1 <- + betree_node_lookup_mut_in_bindings_back n0 key bindings bindings0; + Return bindings1 + | BetreeMessageUpsert s => + v <- betree_upsert_update_fwd None s; + bindings1 <- + betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v); + bindings2 <- + betree_node_lookup_mut_in_bindings_back n0 key bindings bindings1; + Return bindings2 + end + end + . + +(** [betree_main::betree::Node::{5}::apply_messages_to_leaf] *) +Fixpoint betree_node_apply_messages_to_leaf_fwd_back + (n : nat) (bindings : Betree_list_t (u64 * u64)) + (new_msgs : Betree_list_t (u64 * Betree_message_t)) : + result (Betree_list_t (u64 * u64)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match new_msgs with + | BetreeListCons new_msg new_msgs_tl => + let (i, m) := new_msg in + bindings0 <- betree_node_apply_to_leaf_fwd_back n0 bindings i m; + bindings1 <- + betree_node_apply_messages_to_leaf_fwd_back n0 bindings0 new_msgs_tl; + Return bindings1 + | BetreeListNil => Return bindings + end + end + . + +(** [betree_main::betree::Node::{5}::filter_messages_for_key] *) +Fixpoint betree_node_filter_messages_for_key_fwd_back + (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match msgs with + | BetreeListCons p l => + let (k, m) := p in + if k s= key + then ( + msgs0 <- + betree_list_pop_front_back (u64 * Betree_message_t) (BetreeListCons + (k, m) l); + msgs1 <- betree_node_filter_messages_for_key_fwd_back n0 key msgs0; + Return msgs1) + else Return (BetreeListCons (k, m) l) + | BetreeListNil => Return BetreeListNil + end + end + . + +(** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *) +Fixpoint betree_node_lookup_first_message_after_key_fwd + (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match msgs with + | BetreeListCons p next_msgs => + let (k, m) := p in + if k s= key + then ( + l <- betree_node_lookup_first_message_after_key_fwd n0 key next_msgs; + Return l) + else Return (BetreeListCons (k, m) next_msgs) + | BetreeListNil => Return BetreeListNil + end + end + . + +(** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *) +Fixpoint betree_node_lookup_first_message_after_key_back + (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) + (ret : Betree_list_t (u64 * Betree_message_t)) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match msgs with + | BetreeListCons p next_msgs => + let (k, m) := p in + if k s= key + then ( + next_msgs0 <- + betree_node_lookup_first_message_after_key_back n0 key next_msgs ret; + Return (BetreeListCons (k, m) next_msgs0)) + else Return ret + | BetreeListNil => Return ret + end + end + . + +(** [betree_main::betree::Node::{5}::apply_to_internal] *) +Definition betree_node_apply_to_internal_fwd_back + (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t)) (key : u64) + (new_msg : Betree_message_t) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + msgs0 <- betree_node_lookup_first_message_for_key_fwd n0 key msgs; + b <- betree_list_head_has_key_fwd Betree_message_t msgs0 key; + if b + then + match new_msg with + | BetreeMessageInsert i => + msgs1 <- betree_node_filter_messages_for_key_fwd_back n0 key msgs0; + msgs2 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key, + BetreeMessageInsert i); + msgs3 <- + betree_node_lookup_first_message_for_key_back n0 key msgs msgs2; + Return msgs3 + | BetreeMessageDelete => + msgs1 <- betree_node_filter_messages_for_key_fwd_back n0 key msgs0; + msgs2 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 (key, + BetreeMessageDelete); + msgs3 <- + betree_node_lookup_first_message_for_key_back n0 key msgs msgs2; + Return msgs3 + | BetreeMessageUpsert s => + p <- betree_list_hd_fwd (u64 * Betree_message_t) msgs0; + let (_, m) := p in + match m with + | BetreeMessageInsert prev => + v <- betree_upsert_update_fwd (Some prev) s; + msgs1 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs0; + msgs2 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 + (key, BetreeMessageInsert v); + msgs3 <- + betree_node_lookup_first_message_for_key_back n0 key msgs msgs2; + Return msgs3 + | BetreeMessageDelete => + v <- betree_upsert_update_fwd None s; + msgs1 <- betree_list_pop_front_back (u64 * Betree_message_t) msgs0; + msgs2 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 + (key, BetreeMessageInsert v); + msgs3 <- + betree_node_lookup_first_message_for_key_back n0 key msgs msgs2; + Return msgs3 + | BetreeMessageUpsert ufs => + msgs1 <- betree_node_lookup_first_message_after_key_fwd n0 key msgs0; + msgs2 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs1 + (key, BetreeMessageUpsert s); + msgs3 <- + betree_node_lookup_first_message_after_key_back n0 key msgs0 msgs2; + msgs4 <- + betree_node_lookup_first_message_for_key_back n0 key msgs msgs3; + Return msgs4 + end + end + else ( + msgs1 <- + betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs0 (key, + new_msg); + msgs2 <- betree_node_lookup_first_message_for_key_back n0 key msgs msgs1; + Return msgs2) + end + . + +(** [betree_main::betree::Node::{5}::apply_messages_to_internal] *) +Fixpoint betree_node_apply_messages_to_internal_fwd_back + (n : nat) (msgs : Betree_list_t (u64 * Betree_message_t)) + (new_msgs : Betree_list_t (u64 * Betree_message_t)) : + result (Betree_list_t (u64 * Betree_message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match new_msgs with + | BetreeListCons new_msg new_msgs_tl => + let (i, m) := new_msg in + msgs0 <- betree_node_apply_to_internal_fwd_back n0 msgs i m; + msgs1 <- + betree_node_apply_messages_to_internal_fwd_back n0 msgs0 new_msgs_tl; + Return msgs1 + | BetreeListNil => Return msgs + end + end + . + +(** [betree_main::betree::Node::{5}::apply_messages] *) +Fixpoint betree_node_apply_messages_fwd + (n : nat) (self : Betree_node_t) (params : Betree_params_t) + (node_id_cnt : Betree_node_id_counter_t) + (msgs : Betree_list_t (u64 * Betree_message_t)) (st : state) : + result (state * unit) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | BetreeNodeInternal node => + match node with + | mkBetree_internal_t i i0 n1 n2 => + p <- betree_load_internal_node_fwd i st; + let (st0, content) := p in + content0 <- + betree_node_apply_messages_to_internal_fwd_back n0 content msgs; + num_msgs <- betree_list_len_fwd (u64 * Betree_message_t) n0 content0; + match params with + | mkBetree_params_t i1 i2 => + if num_msgs s>= i1 + then ( + p0 <- + betree_internal_flush_fwd n0 (mkBetree_internal_t i i0 n1 n2) + (mkBetree_params_t i1 i2) node_id_cnt content0 st0; + let (st1, content1) := p0 in + p1 <- + betree_internal_flush_back n0 (mkBetree_internal_t i i0 n1 n2) + (mkBetree_params_t i1 i2) node_id_cnt content0 st0; + let (node0, _) := p1 in + match node0 with + | mkBetree_internal_t i3 i4 n3 n4 => + p2 <- betree_store_internal_node_fwd i3 content1 st1; + let (st2, _) := p2 in + Return (st2, tt) + end) + else ( + p0 <- betree_store_internal_node_fwd i content0 st0; + let (st1, _) := p0 in + Return (st1, tt)) + end + end + | BetreeNodeLeaf node => + match node with + | mkBetree_leaf_t i i0 => + p <- betree_load_leaf_node_fwd i st; + let (st0, content) := p in + content0 <- + betree_node_apply_messages_to_leaf_fwd_back n0 content msgs; + len <- betree_list_len_fwd (u64 * u64) n0 content0; + match params with + | mkBetree_params_t i1 i2 => + i3 <- u64_mul 2 %u64 i2; + if len s>= i3 + then ( + p0 <- + betree_leaf_split_fwd n0 (mkBetree_leaf_t i i0) content0 + (mkBetree_params_t i1 i2) node_id_cnt st0; + let (st1, _) := p0 in + p1 <- betree_store_leaf_node_fwd i BetreeListNil st1; + let (st2, _) := p1 in + Return (st2, tt)) + else ( + p0 <- betree_store_leaf_node_fwd i content0 st0; + let (st1, _) := p0 in + Return (st1, tt)) + end + end + end + end + +(** [betree_main::betree::Node::{5}::apply_messages] *) +with betree_node_apply_messages_back + (n : nat) (self : Betree_node_t) (params : Betree_params_t) + (node_id_cnt : Betree_node_id_counter_t) + (msgs : Betree_list_t (u64 * Betree_message_t)) (st : state) : + result (Betree_node_t * Betree_node_id_counter_t) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | BetreeNodeInternal node => + match node with + | mkBetree_internal_t i i0 n1 n2 => + p <- betree_load_internal_node_fwd i st; + let (st0, content) := p in + content0 <- + betree_node_apply_messages_to_internal_fwd_back n0 content msgs; + num_msgs <- betree_list_len_fwd (u64 * Betree_message_t) n0 content0; + match params with + | mkBetree_params_t i1 i2 => + if num_msgs s>= i1 + then ( + p0 <- + betree_internal_flush_fwd n0 (mkBetree_internal_t i i0 n1 n2) + (mkBetree_params_t i1 i2) node_id_cnt content0 st0; + let (st1, content1) := p0 in + p1 <- + betree_internal_flush_back n0 (mkBetree_internal_t i i0 n1 n2) + (mkBetree_params_t i1 i2) node_id_cnt content0 st0; + let (node0, node_id_cnt0) := p1 in + match node0 with + | mkBetree_internal_t i3 i4 n3 n4 => + p2 <- betree_store_internal_node_fwd i3 content1 st1; + let (_, _) := p2 in + Return (BetreeNodeInternal (mkBetree_internal_t i3 i4 n3 n4), + node_id_cnt0) + end) + else ( + p0 <- betree_store_internal_node_fwd i content0 st0; + let (_, _) := p0 in + Return (BetreeNodeInternal (mkBetree_internal_t i i0 n1 n2), + node_id_cnt)) + end + end + | BetreeNodeLeaf node => + match node with + | mkBetree_leaf_t i i0 => + p <- betree_load_leaf_node_fwd i st; + let (st0, content) := p in + content0 <- + betree_node_apply_messages_to_leaf_fwd_back n0 content msgs; + len <- betree_list_len_fwd (u64 * u64) n0 content0; + match params with + | mkBetree_params_t i1 i2 => + i3 <- u64_mul 2 %u64 i2; + if len s>= i3 + then ( + p0 <- + betree_leaf_split_fwd n0 (mkBetree_leaf_t i i0) content0 + (mkBetree_params_t i1 i2) node_id_cnt st0; + let (st1, new_node) := p0 in + p1 <- betree_store_leaf_node_fwd i BetreeListNil st1; + let (_, _) := p1 in + node_id_cnt0 <- + betree_leaf_split_back n0 (mkBetree_leaf_t i i0) content0 + (mkBetree_params_t i1 i2) node_id_cnt st0; + Return (BetreeNodeInternal new_node, node_id_cnt0)) + else ( + p0 <- betree_store_leaf_node_fwd i content0 st0; + let (_, _) := p0 in + Return (BetreeNodeLeaf (mkBetree_leaf_t i len), node_id_cnt)) + end + end + end + end + +(** [betree_main::betree::Internal::{4}::flush] *) +with betree_internal_flush_fwd + (n : nat) (self : Betree_internal_t) (params : Betree_params_t) + (node_id_cnt : Betree_node_id_counter_t) + (content : Betree_list_t (u64 * Betree_message_t)) (st : state) : + result (state * (Betree_list_t (u64 * Betree_message_t))) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_internal_t i i0 n1 n2 => + p <- betree_list_partition_at_pivot_fwd Betree_message_t n0 content i0; + let (msgs_left, msgs_right) := p in + len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left; + match params with + | mkBetree_params_t i1 i2 => + if len_left s>= i1 + then ( + p0 <- + betree_node_apply_messages_fwd n0 n1 (mkBetree_params_t i1 i2) + node_id_cnt msgs_left st; + let (st0, _) := p0 in + p1 <- + betree_node_apply_messages_back n0 n1 (mkBetree_params_t i1 i2) + node_id_cnt msgs_left st; + let (_, node_id_cnt0) := p1 in + len_right <- + betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right; + if len_right s>= i1 + then ( + p2 <- + betree_node_apply_messages_fwd n0 n2 (mkBetree_params_t i1 i2) + node_id_cnt0 msgs_right st0; + let (st1, _) := p2 in + p3 <- + betree_node_apply_messages_back n0 n2 (mkBetree_params_t i1 i2) + node_id_cnt0 msgs_right st0; + let (_, _) := p3 in + Return (st1, BetreeListNil)) + else Return (st0, msgs_right)) + else ( + p0 <- + betree_node_apply_messages_fwd n0 n2 (mkBetree_params_t i1 i2) + node_id_cnt msgs_right st; + let (st0, _) := p0 in + p1 <- + betree_node_apply_messages_back n0 n2 (mkBetree_params_t i1 i2) + node_id_cnt msgs_right st; + let (_, _) := p1 in + Return (st0, msgs_left)) + end + end + end + +(** [betree_main::betree::Internal::{4}::flush] *) +with betree_internal_flush_back + (n : nat) (self : Betree_internal_t) (params : Betree_params_t) + (node_id_cnt : Betree_node_id_counter_t) + (content : Betree_list_t (u64 * Betree_message_t)) (st : state) : + result (Betree_internal_t * Betree_node_id_counter_t) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_internal_t i i0 n1 n2 => + p <- betree_list_partition_at_pivot_fwd Betree_message_t n0 content i0; + let (msgs_left, msgs_right) := p in + len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left; + match params with + | mkBetree_params_t i1 i2 => + if len_left s>= i1 + then ( + p0 <- + betree_node_apply_messages_fwd n0 n1 (mkBetree_params_t i1 i2) + node_id_cnt msgs_left st; + let (st0, _) := p0 in + p1 <- + betree_node_apply_messages_back n0 n1 (mkBetree_params_t i1 i2) + node_id_cnt msgs_left st; + let (n3, node_id_cnt0) := p1 in + len_right <- + betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right; + if len_right s>= i1 + then ( + p2 <- + betree_node_apply_messages_back n0 n2 (mkBetree_params_t i1 i2) + node_id_cnt0 msgs_right st0; + let (n4, node_id_cnt1) := p2 in + Return (mkBetree_internal_t i i0 n3 n4, node_id_cnt1)) + else Return (mkBetree_internal_t i i0 n3 n2, node_id_cnt0)) + else ( + p0 <- + betree_node_apply_messages_back n0 n2 (mkBetree_params_t i1 i2) + node_id_cnt msgs_right st; + let (n3, node_id_cnt0) := p0 in + Return (mkBetree_internal_t i i0 n1 n3, node_id_cnt0)) + end + end + end + . + +(** [betree_main::betree::Node::{5}::apply] *) +Definition betree_node_apply_fwd + (n : nat) (self : Betree_node_t) (params : Betree_params_t) + (node_id_cnt : Betree_node_id_counter_t) (key : u64) + (new_msg : Betree_message_t) (st : state) : + result (state * unit) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + let l := BetreeListNil in + p <- + betree_node_apply_messages_fwd n0 self params node_id_cnt (BetreeListCons + (key, new_msg) l) st; + let (st0, _) := p in + p0 <- + betree_node_apply_messages_back n0 self params node_id_cnt + (BetreeListCons (key, new_msg) l) st; + let (_, _) := p0 in + Return (st0, tt) + end + . + +(** [betree_main::betree::Node::{5}::apply] *) +Definition betree_node_apply_back + (n : nat) (self : Betree_node_t) (params : Betree_params_t) + (node_id_cnt : Betree_node_id_counter_t) (key : u64) + (new_msg : Betree_message_t) (st : state) : + result (Betree_node_t * Betree_node_id_counter_t) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + let l := BetreeListNil in + p <- + betree_node_apply_messages_back n0 self params node_id_cnt + (BetreeListCons (key, new_msg) l) st; + let (self0, node_id_cnt0) := p in + Return (self0, node_id_cnt0) + end + . + +(** [betree_main::betree::BeTree::{6}::new] *) +Definition betree_be_tree_new_fwd + (min_flush_size : u64) (split_size : u64) (st : state) : + result (state * Betree_be_tree_t) + := + node_id_cnt <- betree_node_id_counter_new_fwd; + id <- betree_node_id_counter_fresh_id_fwd node_id_cnt; + p <- betree_store_leaf_node_fwd id BetreeListNil st; + let (st0, _) := p in + node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt; + Return (st0, mkBetree_be_tree_t (mkBetree_params_t min_flush_size split_size) + node_id_cnt0 (BetreeNodeLeaf (mkBetree_leaf_t id (0 %u64)))) + . + +(** [betree_main::betree::BeTree::{6}::apply] *) +Definition betree_be_tree_apply_fwd + (n : nat) (self : Betree_be_tree_t) (key : u64) (msg : Betree_message_t) + (st : state) : + result (state * unit) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_be_tree_t p nic n1 => + p0 <- betree_node_apply_fwd n0 n1 p nic key msg st; + let (st0, _) := p0 in + p1 <- betree_node_apply_back n0 n1 p nic key msg st; + let (_, _) := p1 in + Return (st0, tt) + end + end + . + +(** [betree_main::betree::BeTree::{6}::apply] *) +Definition betree_be_tree_apply_back + (n : nat) (self : Betree_be_tree_t) (key : u64) (msg : Betree_message_t) + (st : state) : + result Betree_be_tree_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_be_tree_t p nic n1 => + p0 <- betree_node_apply_back n0 n1 p nic key msg st; + let (n2, nic0) := p0 in + Return (mkBetree_be_tree_t p nic0 n2) + end + end + . + +(** [betree_main::betree::BeTree::{6}::insert] *) +Definition betree_be_tree_insert_fwd + (n : nat) (self : Betree_be_tree_t) (key : u64) (value : u64) (st : state) : + result (state * unit) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + p <- betree_be_tree_apply_fwd n0 self key (BetreeMessageInsert value) st; + let (st0, _) := p in + bt <- betree_be_tree_apply_back n0 self key (BetreeMessageInsert value) st; + let _ := bt in + Return (st0, tt) + end + . + +(** [betree_main::betree::BeTree::{6}::insert] *) +Definition betree_be_tree_insert_back + (n : nat) (self : Betree_be_tree_t) (key : u64) (value : u64) (st : state) : + result Betree_be_tree_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + self0 <- + betree_be_tree_apply_back n0 self key (BetreeMessageInsert value) st; + Return self0 + end + . + +(** [betree_main::betree::BeTree::{6}::delete] *) +Definition betree_be_tree_delete_fwd + (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) : + result (state * unit) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + p <- betree_be_tree_apply_fwd n0 self key BetreeMessageDelete st; + let (st0, _) := p in + bt <- betree_be_tree_apply_back n0 self key BetreeMessageDelete st; + let _ := bt in + Return (st0, tt) + end + . + +(** [betree_main::betree::BeTree::{6}::delete] *) +Definition betree_be_tree_delete_back + (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) : + result Betree_be_tree_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + self0 <- betree_be_tree_apply_back n0 self key BetreeMessageDelete st; + Return self0 + end + . + +(** [betree_main::betree::BeTree::{6}::upsert] *) +Definition betree_be_tree_upsert_fwd + (n : nat) (self : Betree_be_tree_t) (key : u64) + (upd : Betree_upsert_fun_state_t) (st : state) : + result (state * unit) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + p <- betree_be_tree_apply_fwd n0 self key (BetreeMessageUpsert upd) st; + let (st0, _) := p in + bt <- betree_be_tree_apply_back n0 self key (BetreeMessageUpsert upd) st; + let _ := bt in + Return (st0, tt) + end + . + +(** [betree_main::betree::BeTree::{6}::upsert] *) +Definition betree_be_tree_upsert_back + (n : nat) (self : Betree_be_tree_t) (key : u64) + (upd : Betree_upsert_fun_state_t) (st : state) : + result Betree_be_tree_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + self0 <- + betree_be_tree_apply_back n0 self key (BetreeMessageUpsert upd) st; + Return self0 + end + . + +(** [betree_main::betree::BeTree::{6}::lookup] *) +Definition betree_be_tree_lookup_fwd + (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) : + result (state * (option u64)) + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_be_tree_t p nic n1 => + p0 <- betree_node_lookup_fwd n0 n1 key st; + let (st0, opt) := p0 in + Return (st0, opt) + end + end + . + +(** [betree_main::betree::BeTree::{6}::lookup] *) +Definition betree_be_tree_lookup_back + (n : nat) (self : Betree_be_tree_t) (key : u64) (st : state) : + result Betree_be_tree_t + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + match self with + | mkBetree_be_tree_t p nic n1 => + n2 <- betree_node_lookup_back n0 n1 key st; + Return (mkBetree_be_tree_t p nic n2) + end + end + . + +(** [betree_main::main] *) +Definition main_fwd : result unit := Return tt . + +End BetreeMain__Funs . |