diff options
Diffstat (limited to 'tests/coq/betree/BetreeMain__Funs.v')
| -rw-r--r-- | tests/coq/betree/BetreeMain__Funs.v | 1397 |
1 files changed, 0 insertions, 1397 deletions
diff --git a/tests/coq/betree/BetreeMain__Funs.v b/tests/coq/betree/BetreeMain__Funs.v deleted file mode 100644 index 3ce86f6b..00000000 --- a/tests/coq/betree/BetreeMain__Funs.v +++ /dev/null @@ -1,1397 +0,0 @@ -(** 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 . |