summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2024-06-05 17:51:36 +0200
committerSon Ho2024-06-05 17:51:36 +0200
commita4dd9fe0598328976862868097f59207846d865c (patch)
tree80cc3d5db32d7198adbdf89e516484dc01e58186
parente6d04cf1a73533ae80a68d9ef5f34a9e832e77a3 (diff)
Regenerate the Coq and Lean betrees
Diffstat (limited to '')
-rw-r--r--tests/coq/betree/Betree_Funs.v310
-rw-r--r--tests/lean/Betree/Funs.lean291
2 files changed, 423 insertions, 178 deletions
diff --git a/tests/coq/betree/Betree_Funs.v b/tests/coq/betree/Betree_Funs.v
index b965d423..1c6092ba 100644
--- a/tests/coq/betree/Betree_Funs.v
+++ b/tests/coq/betree/Betree_Funs.v
@@ -88,45 +88,85 @@ Definition betree_upsert_update
end
.
+(** [betree::betree::{betree::betree::List<T>#1}::len]: loop 0:
+ Source: 'src/betree.rs', lines 276:4-284:5 *)
+Fixpoint betree_List_len_loop
+ (T : Type) (n : nat) (self : betree_List_t T) (len : u64) : result u64 :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n1 =>
+ match self with
+ | Betree_List_Cons _ tl =>
+ len1 <- u64_add len 1%u64; betree_List_len_loop T n1 tl len1
+ | Betree_List_Nil => Ok len
+ end
+ end
+.
+
(** [betree::betree::{betree::betree::List<T>#1}::len]:
Source: 'src/betree.rs', lines 276:4-276:24 *)
-Fixpoint betree_List_len
+Definition betree_List_len
(T : Type) (n : nat) (self : betree_List_t T) : result u64 :=
+ betree_List_len_loop T n self 0%u64
+.
+
+(** [betree::betree::{betree::betree::List<T>#1}::reverse]: loop 0:
+ Source: 'src/betree.rs', lines 304:4-312:5 *)
+Fixpoint betree_List_reverse_loop
+ (T : Type) (n : nat) (self : betree_List_t T) (out : betree_List_t T) :
+ result (betree_List_t T)
+ :=
match n with
| O => Fail_ OutOfFuel
| S n1 =>
match self with
- | Betree_List_Cons _ tl => i <- betree_List_len T n1 tl; u64_add 1%u64 i
- | Betree_List_Nil => Ok 0%u64
+ | Betree_List_Cons hd tl =>
+ betree_List_reverse_loop T n1 tl (Betree_List_Cons hd out)
+ | Betree_List_Nil => Ok out
end
end
.
-(** [betree::betree::{betree::betree::List<T>#1}::split_at]:
- Source: 'src/betree.rs', lines 284:4-284:51 *)
-Fixpoint betree_List_split_at
- (T : Type) (n : nat) (self : betree_List_t T) (n1 : u64) :
+(** [betree::betree::{betree::betree::List<T>#1}::reverse]:
+ Source: 'src/betree.rs', lines 304:4-304:32 *)
+Definition betree_List_reverse
+ (T : Type) (n : nat) (self : betree_List_t T) : result (betree_List_t T) :=
+ betree_List_reverse_loop T n self Betree_List_Nil
+.
+
+(** [betree::betree::{betree::betree::List<T>#1}::split_at]: loop 0:
+ Source: 'src/betree.rs', lines 287:4-302:5 *)
+Fixpoint betree_List_split_at_loop
+ (T : Type) (n : nat) (n1 : u64) (beg : betree_List_t T)
+ (self : betree_List_t T) :
result ((betree_List_t T) * (betree_List_t T))
:=
match n with
| O => Fail_ OutOfFuel
| S n2 =>
- if n1 s= 0%u64
- then Ok (Betree_List_Nil, self)
- else
+ if n1 s> 0%u64
+ then
match self with
| Betree_List_Cons hd tl =>
- i <- u64_sub n1 1%u64;
- p <- betree_List_split_at T n2 tl i;
- let (ls0, ls1) := p in
- Ok (Betree_List_Cons hd ls0, ls1)
+ n3 <- u64_sub n1 1%u64;
+ betree_List_split_at_loop T n2 n3 (Betree_List_Cons hd beg) tl
| Betree_List_Nil => Fail_ Failure
end
+ else (l <- betree_List_reverse T n2 beg; Ok (l, self))
end
.
+(** [betree::betree::{betree::betree::List<T>#1}::split_at]:
+ Source: 'src/betree.rs', lines 287:4-287:55 *)
+Definition betree_List_split_at
+ (T : Type) (n : nat) (self : betree_List_t T) (n1 : u64) :
+ result ((betree_List_t T) * (betree_List_t T))
+ :=
+ betree_List_split_at_loop T n n1 Betree_List_Nil self
+.
+
(** [betree::betree::{betree::betree::List<T>#1}::push_front]:
- Source: 'src/betree.rs', lines 299:4-299:34 *)
+ Source: 'src/betree.rs', lines 315:4-315:34 *)
Definition betree_List_push_front
(T : Type) (self : betree_List_t T) (x : T) : result (betree_List_t T) :=
let (tl, _) := core_mem_replace (betree_List_t T) self Betree_List_Nil in
@@ -134,7 +174,7 @@ Definition betree_List_push_front
.
(** [betree::betree::{betree::betree::List<T>#1}::pop_front]:
- Source: 'src/betree.rs', lines 306:4-306:32 *)
+ Source: 'src/betree.rs', lines 322:4-322:32 *)
Definition betree_List_pop_front
(T : Type) (self : betree_List_t T) : result (T * (betree_List_t T)) :=
let (ls, _) := core_mem_replace (betree_List_t T) self Betree_List_Nil in
@@ -145,7 +185,7 @@ Definition betree_List_pop_front
.
(** [betree::betree::{betree::betree::List<T>#1}::hd]:
- Source: 'src/betree.rs', lines 318:4-318:22 *)
+ Source: 'src/betree.rs', lines 334:4-334:22 *)
Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T :=
match self with
| Betree_List_Cons hd _ => Ok hd
@@ -154,7 +194,7 @@ Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T :=
.
(** [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]:
- Source: 'src/betree.rs', lines 327:4-327:44 *)
+ Source: 'src/betree.rs', lines 343:4-343:44 *)
Definition betree_ListPairU64T_head_has_key
(T : Type) (self : betree_List_t (u64 * T)) (key : u64) : result bool :=
match self with
@@ -163,10 +203,11 @@ Definition betree_ListPairU64T_head_has_key
end
.
-(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]:
- Source: 'src/betree.rs', lines 339:4-339:73 *)
-Fixpoint betree_ListPairU64T_partition_at_pivot
- (T : Type) (n : nat) (self : betree_List_t (u64 * T)) (pivot : u64) :
+(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: loop 0:
+ Source: 'src/betree.rs', lines 355:4-370:5 *)
+Fixpoint betree_ListPairU64T_partition_at_pivot_loop
+ (T : Type) (n : nat) (pivot : u64) (beg : betree_List_t (u64 * T))
+ (end1 : betree_List_t (u64 * T)) (self : betree_List_t (u64 * T)) :
result ((betree_List_t (u64 * T)) * (betree_List_t (u64 * T)))
:=
match n with
@@ -176,18 +217,32 @@ Fixpoint betree_ListPairU64T_partition_at_pivot
| Betree_List_Cons hd tl =>
let (i, t) := hd in
if i s>= pivot
- then Ok (Betree_List_Nil, Betree_List_Cons (i, t) tl)
- else (
- p <- betree_ListPairU64T_partition_at_pivot T n1 tl pivot;
- let (ls0, ls1) := p in
- Ok (Betree_List_Cons (i, t) ls0, ls1))
- | Betree_List_Nil => Ok (Betree_List_Nil, Betree_List_Nil)
+ then
+ betree_ListPairU64T_partition_at_pivot_loop T n1 pivot beg
+ (Betree_List_Cons (i, t) end1) tl
+ else
+ betree_ListPairU64T_partition_at_pivot_loop T n1 pivot
+ (Betree_List_Cons (i, t) beg) end1 tl
+ | Betree_List_Nil =>
+ l <- betree_List_reverse (u64 * T) n1 beg;
+ l1 <- betree_List_reverse (u64 * T) n1 end1;
+ Ok (l, l1)
end
end
.
+(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]:
+ Source: 'src/betree.rs', lines 355:4-355:73 *)
+Definition betree_ListPairU64T_partition_at_pivot
+ (T : Type) (n : nat) (self : betree_List_t (u64 * T)) (pivot : u64) :
+ result ((betree_List_t (u64 * T)) * (betree_List_t (u64 * T)))
+ :=
+ betree_ListPairU64T_partition_at_pivot_loop T n pivot Betree_List_Nil
+ Betree_List_Nil self
+.
+
(** [betree::betree::{betree::betree::Leaf#3}::split]:
- Source: 'src/betree.rs', lines 359:4-364:17 *)
+ Source: 'src/betree.rs', lines 378:4-383:17 *)
Definition betree_Leaf_split
(n : nat) (self : betree_Leaf_t) (content : betree_List_t (u64 * u64))
(params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -222,9 +277,9 @@ Definition betree_Leaf_split
node_id_cnt2))
.
-(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]:
- Source: 'src/betree.rs', lines 789:4-792:34 *)
-Fixpoint betree_Node_lookup_first_message_for_key
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: loop 0:
+ Source: 'src/betree.rs', lines 792:4-810:5 *)
+Fixpoint betree_Node_lookup_first_message_for_key_loop
(n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 *
betree_Message_t) -> result (betree_List_t (u64 * betree_Message_t))))
@@ -238,21 +293,30 @@ Fixpoint betree_Node_lookup_first_message_for_key
if i s>= key
then Ok (Betree_List_Cons (i, m) next_msgs, Ok)
else (
- p <- betree_Node_lookup_first_message_for_key n1 key next_msgs;
- let (l, lookup_first_message_for_key_back) := p in
- let back :=
+ p <- betree_Node_lookup_first_message_for_key_loop n1 key next_msgs;
+ let (l, back) := p in
+ let back1 :=
fun (ret : betree_List_t (u64 * betree_Message_t)) =>
- next_msgs1 <- lookup_first_message_for_key_back ret;
- Ok (Betree_List_Cons (i, m) next_msgs1) in
- Ok (l, back))
+ next_msgs1 <- back ret; Ok (Betree_List_Cons (i, m) next_msgs1) in
+ Ok (l, back1))
| Betree_List_Nil => Ok (Betree_List_Nil, Ok)
end
end
.
-(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]:
- Source: 'src/betree.rs', lines 636:4-636:80 *)
-Fixpoint betree_Node_lookup_in_bindings
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]:
+ Source: 'src/betree.rs', lines 792:4-795:34 *)
+Definition betree_Node_lookup_first_message_for_key
+ (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
+ result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 *
+ betree_Message_t) -> result (betree_List_t (u64 * betree_Message_t))))
+ :=
+ betree_Node_lookup_first_message_for_key_loop n key msgs
+.
+
+(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: loop 0:
+ Source: 'src/betree.rs', lines 649:4-660:5 *)
+Fixpoint betree_Node_lookup_in_bindings_loop
(n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
result (option u64)
:=
@@ -265,15 +329,26 @@ Fixpoint betree_Node_lookup_in_bindings
if i s= key
then Ok (Some i1)
else
- if i s> key then Ok None else betree_Node_lookup_in_bindings n1 key tl
+ if i s> key
+ then Ok None
+ else betree_Node_lookup_in_bindings_loop n1 key tl
| Betree_List_Nil => Ok None
end
end
.
-(** [betree::betree::{betree::betree::Node#5}::apply_upserts]:
- Source: 'src/betree.rs', lines 819:4-819:90 *)
-Fixpoint betree_Node_apply_upserts
+(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]:
+ Source: 'src/betree.rs', lines 649:4-649:84 *)
+Definition betree_Node_lookup_in_bindings
+ (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
+ result (option u64)
+ :=
+ betree_Node_lookup_in_bindings_loop n key bindings
+.
+
+(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: loop 0:
+ Source: 'src/betree.rs', lines 820:4-844:5 *)
+Fixpoint betree_Node_apply_upserts_loop
(n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64)
(key : u64) :
result (u64 * (betree_List_t (u64 * betree_Message_t)))
@@ -292,7 +367,7 @@ Fixpoint betree_Node_apply_upserts
| Betree_Message_Delete => Fail_ Failure
| Betree_Message_Upsert s =>
v <- betree_upsert_update prev s;
- betree_Node_apply_upserts n1 msgs1 (Some v) key
+ betree_Node_apply_upserts_loop n1 msgs1 (Some v) key
end)
else (
v <- core_option_Option_unwrap u64 prev;
@@ -303,8 +378,18 @@ Fixpoint betree_Node_apply_upserts
end
.
+(** [betree::betree::{betree::betree::Node#5}::apply_upserts]:
+ Source: 'src/betree.rs', lines 820:4-820:94 *)
+Definition betree_Node_apply_upserts
+ (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64)
+ (key : u64) :
+ result (u64 * (betree_List_t (u64 * betree_Message_t)))
+ :=
+ betree_Node_apply_upserts_loop n msgs prev key
+.
+
(** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]:
- Source: 'src/betree.rs', lines 395:4-395:63 *)
+ Source: 'src/betree.rs', lines 414:4-414:63 *)
Fixpoint betree_Internal_lookup_in_children
(n : nat) (self : betree_Internal_t) (key : u64) (st : state) :
result (state * ((option u64) * betree_Internal_t))
@@ -328,7 +413,7 @@ Fixpoint betree_Internal_lookup_in_children
end
(** [betree::betree::{betree::betree::Node#5}::lookup]:
- Source: 'src/betree.rs', lines 709:4-709:58 *)
+ Source: 'src/betree.rs', lines 712:4-712:58 *)
with betree_Node_lookup
(n : nat) (self : betree_Node_t) (key : u64) (st : state) :
result (state * ((option u64) * betree_Node_t))
@@ -394,9 +479,9 @@ with betree_Node_lookup
end
.
-(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]:
- Source: 'src/betree.rs', lines 674:4-674:77 *)
-Fixpoint betree_Node_filter_messages_for_key
+(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: loop 0:
+ Source: 'src/betree.rs', lines 683:4-692:5 *)
+Fixpoint betree_Node_filter_messages_for_key_loop
(n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
result (betree_List_t (u64 * betree_Message_t))
:=
@@ -412,16 +497,25 @@ Fixpoint betree_Node_filter_messages_for_key
betree_List_pop_front (u64 * betree_Message_t) (Betree_List_Cons (k,
m) l);
let (_, msgs1) := p1 in
- betree_Node_filter_messages_for_key n1 key msgs1)
+ betree_Node_filter_messages_for_key_loop n1 key msgs1)
else Ok (Betree_List_Cons (k, m) l)
| Betree_List_Nil => Ok Betree_List_Nil
end
end
.
-(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]:
- Source: 'src/betree.rs', lines 689:4-692:34 *)
-Fixpoint betree_Node_lookup_first_message_after_key
+(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]:
+ Source: 'src/betree.rs', lines 683:4-683:77 *)
+Definition betree_Node_filter_messages_for_key
+ (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
+ result (betree_List_t (u64 * betree_Message_t))
+ :=
+ betree_Node_filter_messages_for_key_loop n key msgs
+.
+
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: loop 0:
+ Source: 'src/betree.rs', lines 694:4-706:5 *)
+Fixpoint betree_Node_lookup_first_message_after_key_loop
(n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 *
betree_Message_t) -> result (betree_List_t (u64 * betree_Message_t))))
@@ -434,21 +528,30 @@ Fixpoint betree_Node_lookup_first_message_after_key
let (k, m) := p in
if k s= key
then (
- p1 <- betree_Node_lookup_first_message_after_key n1 key next_msgs;
- let (l, lookup_first_message_after_key_back) := p1 in
- let back :=
+ p1 <- betree_Node_lookup_first_message_after_key_loop n1 key next_msgs;
+ let (l, back) := p1 in
+ let back1 :=
fun (ret : betree_List_t (u64 * betree_Message_t)) =>
- next_msgs1 <- lookup_first_message_after_key_back ret;
- Ok (Betree_List_Cons (k, m) next_msgs1) in
- Ok (l, back))
+ next_msgs1 <- back ret; Ok (Betree_List_Cons (k, m) next_msgs1) in
+ Ok (l, back1))
else Ok (Betree_List_Cons (k, m) next_msgs, Ok)
| Betree_List_Nil => Ok (Betree_List_Nil, Ok)
end
end
.
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]:
+ Source: 'src/betree.rs', lines 694:4-697:34 *)
+Definition betree_Node_lookup_first_message_after_key
+ (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
+ result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 *
+ betree_Message_t) -> result (betree_List_t (u64 * betree_Message_t))))
+ :=
+ betree_Node_lookup_first_message_after_key_loop n key msgs
+.
+
(** [betree::betree::{betree::betree::Node#5}::apply_to_internal]:
- Source: 'src/betree.rs', lines 521:4-521:89 *)
+ Source: 'src/betree.rs', lines 534:4-534:89 *)
Definition betree_Node_apply_to_internal
(n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (key : u64)
(new_msg : betree_Message_t) :
@@ -508,9 +611,9 @@ Definition betree_Node_apply_to_internal
lookup_first_message_for_key_back msgs2)
.
-(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]:
- Source: 'src/betree.rs', lines 502:4-505:5 *)
-Fixpoint betree_Node_apply_messages_to_internal
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: loop 0:
+ Source: 'src/betree.rs', lines 518:4-526:5 *)
+Fixpoint betree_Node_apply_messages_to_internal_loop
(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))
@@ -522,15 +625,25 @@ Fixpoint betree_Node_apply_messages_to_internal
| Betree_List_Cons new_msg new_msgs_tl =>
let (i, m) := new_msg in
msgs1 <- betree_Node_apply_to_internal n1 msgs i m;
- betree_Node_apply_messages_to_internal n1 msgs1 new_msgs_tl
+ betree_Node_apply_messages_to_internal_loop n1 msgs1 new_msgs_tl
| Betree_List_Nil => Ok msgs
end
end
.
-(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]:
- Source: 'src/betree.rs', lines 653:4-656:32 *)
-Fixpoint betree_Node_lookup_mut_in_bindings
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]:
+ Source: 'src/betree.rs', lines 518:4-521:5 *)
+Definition betree_Node_apply_messages_to_internal
+ (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))
+ :=
+ betree_Node_apply_messages_to_internal_loop n msgs new_msgs
+.
+
+(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: loop 0:
+ Source: 'src/betree.rs', lines 664:4-677:5 *)
+Fixpoint betree_Node_lookup_mut_in_bindings_loop
(n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
result ((betree_List_t (u64 * u64)) * (betree_List_t (u64 * u64) -> result
(betree_List_t (u64 * u64))))
@@ -544,20 +657,29 @@ Fixpoint betree_Node_lookup_mut_in_bindings
if i s>= key
then Ok (Betree_List_Cons (i, i1) tl, Ok)
else (
- p <- betree_Node_lookup_mut_in_bindings n1 key tl;
- let (l, lookup_mut_in_bindings_back) := p in
- let back :=
+ p <- betree_Node_lookup_mut_in_bindings_loop n1 key tl;
+ let (l, back) := p in
+ let back1 :=
fun (ret : betree_List_t (u64 * u64)) =>
- tl1 <- lookup_mut_in_bindings_back ret;
- Ok (Betree_List_Cons (i, i1) tl1) in
- Ok (l, back))
+ tl1 <- back ret; Ok (Betree_List_Cons (i, i1) tl1) in
+ Ok (l, back1))
| Betree_List_Nil => Ok (Betree_List_Nil, Ok)
end
end
.
+(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]:
+ Source: 'src/betree.rs', lines 664:4-667:32 *)
+Definition betree_Node_lookup_mut_in_bindings
+ (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
+ result ((betree_List_t (u64 * u64)) * (betree_List_t (u64 * u64) -> result
+ (betree_List_t (u64 * u64))))
+ :=
+ betree_Node_lookup_mut_in_bindings_loop n key bindings
+.
+
(** [betree::betree::{betree::betree::Node#5}::apply_to_leaf]:
- Source: 'src/betree.rs', lines 460:4-460:87 *)
+ Source: 'src/betree.rs', lines 476:4-476:87 *)
Definition betree_Node_apply_to_leaf
(n : nat) (bindings : betree_List_t (u64 * u64)) (key : u64)
(new_msg : betree_Message_t) :
@@ -594,9 +716,9 @@ Definition betree_Node_apply_to_leaf
end
.
-(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]:
- Source: 'src/betree.rs', lines 444:4-447:5 *)
-Fixpoint betree_Node_apply_messages_to_leaf
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: loop 0:
+ Source: 'src/betree.rs', lines 463:4-471:5 *)
+Fixpoint betree_Node_apply_messages_to_leaf_loop
(n : nat) (bindings : betree_List_t (u64 * u64))
(new_msgs : betree_List_t (u64 * betree_Message_t)) :
result (betree_List_t (u64 * u64))
@@ -608,14 +730,24 @@ Fixpoint betree_Node_apply_messages_to_leaf
| Betree_List_Cons new_msg new_msgs_tl =>
let (i, m) := new_msg in
bindings1 <- betree_Node_apply_to_leaf n1 bindings i m;
- betree_Node_apply_messages_to_leaf n1 bindings1 new_msgs_tl
+ betree_Node_apply_messages_to_leaf_loop n1 bindings1 new_msgs_tl
| Betree_List_Nil => Ok bindings
end
end
.
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]:
+ Source: 'src/betree.rs', lines 463:4-466:5 *)
+Definition betree_Node_apply_messages_to_leaf
+ (n : nat) (bindings : betree_List_t (u64 * u64))
+ (new_msgs : betree_List_t (u64 * betree_Message_t)) :
+ result (betree_List_t (u64 * u64))
+ :=
+ betree_Node_apply_messages_to_leaf_loop n bindings new_msgs
+.
+
(** [betree::betree::{betree::betree::Internal#4}::flush]:
- Source: 'src/betree.rs', lines 410:4-415:26 *)
+ Source: 'src/betree.rs', lines 429:4-434:26 *)
Fixpoint betree_Internal_flush
(n : nat) (self : betree_Internal_t) (params : betree_Params_t)
(node_id_cnt : betree_NodeIdCounter_t)
@@ -665,7 +797,7 @@ Fixpoint betree_Internal_flush
end
(** [betree::betree::{betree::betree::Node#5}::apply_messages]:
- Source: 'src/betree.rs', lines 588:4-593:5 *)
+ Source: 'src/betree.rs', lines 601:4-606:5 *)
with betree_Node_apply_messages
(n : nat) (self : betree_Node_t) (params : betree_Params_t)
(node_id_cnt : betree_NodeIdCounter_t)
@@ -721,7 +853,7 @@ with betree_Node_apply_messages
.
(** [betree::betree::{betree::betree::Node#5}::apply]:
- Source: 'src/betree.rs', lines 576:4-582:5 *)
+ Source: 'src/betree.rs', lines 589:4-595:5 *)
Definition betree_Node_apply
(n : nat) (self : betree_Node_t) (params : betree_Params_t)
(node_id_cnt : betree_NodeIdCounter_t) (key : u64)
@@ -737,7 +869,7 @@ Definition betree_Node_apply
.
(** [betree::betree::{betree::betree::BeTree#6}::new]:
- Source: 'src/betree.rs', lines 849:4-849:60 *)
+ Source: 'src/betree.rs', lines 848:4-848:60 *)
Definition betree_BeTree_new
(min_flush_size : u64) (split_size : u64) (st : state) :
result (state * betree_BeTree_t)
@@ -762,7 +894,7 @@ Definition betree_BeTree_new
.
(** [betree::betree::{betree::betree::BeTree#6}::apply]:
- Source: 'src/betree.rs', lines 868:4-868:47 *)
+ Source: 'src/betree.rs', lines 867:4-867:47 *)
Definition betree_BeTree_apply
(n : nat) (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t)
(st : state) :
@@ -782,7 +914,7 @@ Definition betree_BeTree_apply
.
(** [betree::betree::{betree::betree::BeTree#6}::insert]:
- Source: 'src/betree.rs', lines 874:4-874:52 *)
+ Source: 'src/betree.rs', lines 873:4-873:52 *)
Definition betree_BeTree_insert
(n : nat) (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) :
result (state * betree_BeTree_t)
@@ -791,7 +923,7 @@ Definition betree_BeTree_insert
.
(** [betree::betree::{betree::betree::BeTree#6}::delete]:
- Source: 'src/betree.rs', lines 880:4-880:38 *)
+ Source: 'src/betree.rs', lines 879:4-879:38 *)
Definition betree_BeTree_delete
(n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
result (state * betree_BeTree_t)
@@ -800,7 +932,7 @@ Definition betree_BeTree_delete
.
(** [betree::betree::{betree::betree::BeTree#6}::upsert]:
- Source: 'src/betree.rs', lines 886:4-886:59 *)
+ Source: 'src/betree.rs', lines 885:4-885:59 *)
Definition betree_BeTree_upsert
(n : nat) (self : betree_BeTree_t) (key : u64)
(upd : betree_UpsertFunState_t) (st : state) :
@@ -810,7 +942,7 @@ Definition betree_BeTree_upsert
.
(** [betree::betree::{betree::betree::BeTree#6}::lookup]:
- Source: 'src/betree.rs', lines 895:4-895:62 *)
+ Source: 'src/betree.rs', lines 894:4-894:62 *)
Definition betree_BeTree_lookup
(n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
result (state * ((option u64) * betree_BeTree_t))
diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean
index 8612ccbc..7d8b4714 100644
--- a/tests/lean/Betree/Funs.lean
+++ b/tests/lean/Betree/Funs.lean
@@ -79,42 +79,74 @@ def betree.upsert_update
then prev1 - v
else Result.ok 0#u64
+/- [betree::betree::{betree::betree::List<T>#1}::len]: loop 0:
+ Source: 'src/betree.rs', lines 276:4-284:5 -/
+divergent def betree.List.len_loop
+ (T : Type) (self : betree.List T) (len : U64) : Result U64 :=
+ match self with
+ | betree.List.Cons _ tl =>
+ do
+ let len1 ← len + 1#u64
+ betree.List.len_loop T tl len1
+ | betree.List.Nil => Result.ok len
+
/- [betree::betree::{betree::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 :=
+def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
+ betree.List.len_loop T self 0#u64
+
+/- [betree::betree::{betree::betree::List<T>#1}::reverse]: loop 0:
+ Source: 'src/betree.rs', lines 304:4-312:5 -/
+divergent def betree.List.reverse_loop
+ (T : Type) (self : betree.List T) (out : betree.List T) :
+ Result (betree.List T)
+ :=
match self with
- | betree.List.Cons _ tl => do
- let i ← betree.List.len T tl
- 1#u64 + i
- | betree.List.Nil => Result.ok 0#u64
-
-/- [betree::betree::{betree::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) :
+ | betree.List.Cons hd tl =>
+ betree.List.reverse_loop T tl (betree.List.Cons hd out)
+ | betree.List.Nil => Result.ok out
+
+/- [betree::betree::{betree::betree::List<T>#1}::reverse]:
+ Source: 'src/betree.rs', lines 304:4-304:32 -/
+def betree.List.reverse
+ (T : Type) (self : betree.List T) : Result (betree.List T) :=
+ betree.List.reverse_loop T self betree.List.Nil
+
+/- [betree::betree::{betree::betree::List<T>#1}::split_at]: loop 0:
+ Source: 'src/betree.rs', lines 287:4-302:5 -/
+divergent def betree.List.split_at_loop
+ (T : Type) (n : U64) (beg : betree.List T) (self : betree.List T) :
Result ((betree.List T) × (betree.List T))
:=
- if n = 0#u64
- then Result.ok (betree.List.Nil, self)
- else
+ if n > 0#u64
+ then
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
- Result.ok (betree.List.Cons hd ls0, ls1)
+ let n1 ← n - 1#u64
+ betree.List.split_at_loop T n1 (betree.List.Cons hd beg) tl
| betree.List.Nil => Result.fail .panic
+ else do
+ let l ← betree.List.reverse T beg
+ Result.ok (l, self)
+
+/- [betree::betree::{betree::betree::List<T>#1}::split_at]:
+ Source: 'src/betree.rs', lines 287:4-287:55 -/
+def betree.List.split_at
+ (T : Type) (self : betree.List T) (n : U64) :
+ Result ((betree.List T) × (betree.List T))
+ :=
+ betree.List.split_at_loop T n betree.List.Nil self
/- [betree::betree::{betree::betree::List<T>#1}::push_front]:
- Source: 'src/betree.rs', lines 299:4-299:34 -/
+ Source: 'src/betree.rs', lines 315:4-315: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
Result.ok (betree.List.Cons x tl)
/- [betree::betree::{betree::betree::List<T>#1}::pop_front]:
- Source: 'src/betree.rs', lines 306:4-306:32 -/
+ Source: 'src/betree.rs', lines 322:4-322:32 -/
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
@@ -123,14 +155,14 @@ def betree.List.pop_front
| betree.List.Nil => Result.fail .panic
/- [betree::betree::{betree::betree::List<T>#1}::hd]:
- Source: 'src/betree.rs', lines 318:4-318:22 -/
+ Source: 'src/betree.rs', lines 334:4-334:22 -/
def betree.List.hd (T : Type) (self : betree.List T) : Result T :=
match self with
| betree.List.Cons hd _ => Result.ok hd
| betree.List.Nil => Result.fail .panic
/- [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]:
- Source: 'src/betree.rs', lines 327:4-327:44 -/
+ Source: 'src/betree.rs', lines 343:4-343:44 -/
def betree.ListPairU64T.head_has_key
(T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool :=
match self with
@@ -138,26 +170,40 @@ def betree.ListPairU64T.head_has_key
Result.ok (i = key)
| betree.List.Nil => Result.ok false
-/- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]:
- Source: 'src/betree.rs', lines 339:4-339:73 -/
-divergent def betree.ListPairU64T.partition_at_pivot
- (T : Type) (self : betree.List (U64 × T)) (pivot : U64) :
+/- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: loop 0:
+ Source: 'src/betree.rs', lines 355:4-370:5 -/
+divergent def betree.ListPairU64T.partition_at_pivot_loop
+ (T : Type) (pivot : U64) (beg : betree.List (U64 × T))
+ (end1 : betree.List (U64 × T)) (self : betree.List (U64 × T)) :
Result ((betree.List (U64 × T)) × (betree.List (U64 × T)))
:=
match self with
| betree.List.Cons hd tl =>
let (i, t) := hd
if i >= pivot
- then Result.ok (betree.List.Nil, betree.List.Cons (i, t) tl)
+ then
+ betree.ListPairU64T.partition_at_pivot_loop T pivot beg (betree.List.Cons
+ (i, t) end1) tl
else
- do
- let p ← betree.ListPairU64T.partition_at_pivot T tl pivot
- let (ls0, ls1) := p
- Result.ok (betree.List.Cons (i, t) ls0, ls1)
- | betree.List.Nil => Result.ok (betree.List.Nil, betree.List.Nil)
+ betree.ListPairU64T.partition_at_pivot_loop T pivot (betree.List.Cons (i,
+ t) beg) end1 tl
+ | betree.List.Nil =>
+ do
+ let l ← betree.List.reverse (U64 × T) beg
+ let l1 ← betree.List.reverse (U64 × T) end1
+ Result.ok (l, l1)
+
+/- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]:
+ Source: 'src/betree.rs', lines 355:4-355:73 -/
+def betree.ListPairU64T.partition_at_pivot
+ (T : Type) (self : betree.List (U64 × T)) (pivot : U64) :
+ Result ((betree.List (U64 × T)) × (betree.List (U64 × T)))
+ :=
+ betree.ListPairU64T.partition_at_pivot_loop T pivot betree.List.Nil
+ betree.List.Nil self
/- [betree::betree::{betree::betree::Leaf#3}::split]:
- Source: 'src/betree.rs', lines 359:4-364:17 -/
+ Source: 'src/betree.rs', lines 378:4-383:17 -/
def betree.Leaf.split
(self : betree.Leaf) (content : betree.List (U64 × U64))
(params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) :
@@ -176,9 +222,9 @@ def betree.Leaf.split
let n1 := betree.Node.Leaf { id := id1, size := params.split_size }
Result.ok (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2))
-/- [betree::betree::{betree::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
+/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: loop 0:
+ Source: 'src/betree.rs', lines 792:4-810:5 -/
+divergent def betree.Node.lookup_first_message_for_key_loop
(key : U64) (msgs : betree.List (U64 × betree.Message)) :
Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 ×
betree.Message) → Result (betree.List (U64 × betree.Message))))
@@ -190,19 +236,28 @@ divergent def betree.Node.lookup_first_message_for_key
then Result.ok (betree.List.Cons (i, m) next_msgs, Result.ok)
else
do
- let (l, lookup_first_message_for_key_back) ←
- betree.Node.lookup_first_message_for_key key next_msgs
- let back :=
+ let (l, back) ←
+ betree.Node.lookup_first_message_for_key_loop key next_msgs
+ let back1 :=
fun ret =>
do
- let next_msgs1 ← lookup_first_message_for_key_back ret
+ let next_msgs1 ← back ret
Result.ok (betree.List.Cons (i, m) next_msgs1)
- Result.ok (l, back)
+ Result.ok (l, back1)
| betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
-/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]:
- Source: 'src/betree.rs', lines 636:4-636:80 -/
-divergent def betree.Node.lookup_in_bindings
+/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]:
+ Source: 'src/betree.rs', lines 792:4-795:34 -/
+def betree.Node.lookup_first_message_for_key
+ (key : U64) (msgs : betree.List (U64 × betree.Message)) :
+ Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 ×
+ betree.Message) → Result (betree.List (U64 × betree.Message))))
+ :=
+ betree.Node.lookup_first_message_for_key_loop key msgs
+
+/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: loop 0:
+ Source: 'src/betree.rs', lines 649:4-660:5 -/
+divergent def betree.Node.lookup_in_bindings_loop
(key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
match bindings with
| betree.List.Cons hd tl =>
@@ -212,12 +267,18 @@ divergent def betree.Node.lookup_in_bindings
else
if i > key
then Result.ok none
- else betree.Node.lookup_in_bindings key tl
+ else betree.Node.lookup_in_bindings_loop key tl
| betree.List.Nil => Result.ok none
-/- [betree::betree::{betree::betree::Node#5}::apply_upserts]:
- Source: 'src/betree.rs', lines 819:4-819:90 -/
-divergent def betree.Node.apply_upserts
+/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]:
+ Source: 'src/betree.rs', lines 649:4-649:84 -/
+def betree.Node.lookup_in_bindings
+ (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
+ betree.Node.lookup_in_bindings_loop key bindings
+
+/- [betree::betree::{betree::betree::Node#5}::apply_upserts]: loop 0:
+ Source: 'src/betree.rs', lines 820:4-844:5 -/
+divergent def betree.Node.apply_upserts_loop
(msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64)
:
Result (U64 × (betree.List (U64 × betree.Message)))
@@ -235,7 +296,7 @@ divergent def betree.Node.apply_upserts
| betree.Message.Upsert s =>
do
let v ← betree.upsert_update prev s
- betree.Node.apply_upserts msgs1 (some v) key
+ betree.Node.apply_upserts_loop msgs1 (some v) key
else
do
let v ← core.option.Option.unwrap U64 prev
@@ -244,8 +305,17 @@ divergent def betree.Node.apply_upserts
betree.Message.Insert v)
Result.ok (v, msgs1)
+/- [betree::betree::{betree::betree::Node#5}::apply_upserts]:
+ Source: 'src/betree.rs', lines 820:4-820:94 -/
+def betree.Node.apply_upserts
+ (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64)
+ :
+ Result (U64 × (betree.List (U64 × betree.Message)))
+ :=
+ betree.Node.apply_upserts_loop msgs prev key
+
/- [betree::betree::{betree::betree::Internal#4}::lookup_in_children]:
- Source: 'src/betree.rs', lines 395:4-395:63 -/
+ Source: 'src/betree.rs', lines 414:4-414:63 -/
mutual divergent def betree.Internal.lookup_in_children
(self : betree.Internal) (key : U64) (st : State) :
Result (State × ((Option U64) × betree.Internal))
@@ -261,7 +331,7 @@ mutual divergent def betree.Internal.lookup_in_children
Result.ok (st1, (o, betree.Internal.mk self.id self.pivot self.left n))
/- [betree::betree::{betree::betree::Node#5}::lookup]:
- Source: 'src/betree.rs', lines 709:4-709:58 -/
+ Source: 'src/betree.rs', lines 712:4-712:58 -/
divergent def betree.Node.lookup
(self : betree.Node) (key : U64) (st : State) :
Result (State × ((Option U64) × betree.Node))
@@ -320,9 +390,9 @@ divergent def betree.Node.lookup
end
-/- [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]:
- Source: 'src/betree.rs', lines 674:4-674:77 -/
-divergent def betree.Node.filter_messages_for_key
+/- [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: loop 0:
+ Source: 'src/betree.rs', lines 683:4-692:5 -/
+divergent def betree.Node.filter_messages_for_key_loop
(key : U64) (msgs : betree.List (U64 × betree.Message)) :
Result (betree.List (U64 × betree.Message))
:=
@@ -335,13 +405,21 @@ divergent def betree.Node.filter_messages_for_key
let (_, msgs1) ←
betree.List.pop_front (U64 × betree.Message) (betree.List.Cons (k, m)
l)
- betree.Node.filter_messages_for_key key msgs1
+ betree.Node.filter_messages_for_key_loop key msgs1
else Result.ok (betree.List.Cons (k, m) l)
| betree.List.Nil => Result.ok betree.List.Nil
-/- [betree::betree::{betree::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
+/- [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]:
+ Source: 'src/betree.rs', lines 683:4-683:77 -/
+def betree.Node.filter_messages_for_key
+ (key : U64) (msgs : betree.List (U64 × betree.Message)) :
+ Result (betree.List (U64 × betree.Message))
+ :=
+ betree.Node.filter_messages_for_key_loop key msgs
+
+/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: loop 0:
+ Source: 'src/betree.rs', lines 694:4-706:5 -/
+divergent def betree.Node.lookup_first_message_after_key_loop
(key : U64) (msgs : betree.List (U64 × betree.Message)) :
Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 ×
betree.Message) → Result (betree.List (U64 × betree.Message))))
@@ -352,19 +430,28 @@ divergent def betree.Node.lookup_first_message_after_key
if k = key
then
do
- let (l, lookup_first_message_after_key_back) ←
- betree.Node.lookup_first_message_after_key key next_msgs
- let back :=
+ let (l, back) ←
+ betree.Node.lookup_first_message_after_key_loop key next_msgs
+ let back1 :=
fun ret =>
do
- let next_msgs1 ← lookup_first_message_after_key_back ret
+ let next_msgs1 ← back ret
Result.ok (betree.List.Cons (k, m) next_msgs1)
- Result.ok (l, back)
+ Result.ok (l, back1)
else Result.ok (betree.List.Cons (k, m) next_msgs, Result.ok)
| betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
+/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]:
+ Source: 'src/betree.rs', lines 694:4-697:34 -/
+def betree.Node.lookup_first_message_after_key
+ (key : U64) (msgs : betree.List (U64 × betree.Message)) :
+ Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 ×
+ betree.Message) → Result (betree.List (U64 × betree.Message))))
+ :=
+ betree.Node.lookup_first_message_after_key_loop key msgs
+
/- [betree::betree::{betree::betree::Node#5}::apply_to_internal]:
- Source: 'src/betree.rs', lines 521:4-521:89 -/
+ Source: 'src/betree.rs', lines 534:4-534:89 -/
def betree.Node.apply_to_internal
(msgs : betree.List (U64 × betree.Message)) (key : U64)
(new_msg : betree.Message) :
@@ -427,9 +514,9 @@ def betree.Node.apply_to_internal
betree.List.push_front (U64 × betree.Message) msgs1 (key, new_msg)
lookup_first_message_for_key_back msgs2
-/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]:
- Source: 'src/betree.rs', lines 502:4-505:5 -/
-divergent def betree.Node.apply_messages_to_internal
+/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: loop 0:
+ Source: 'src/betree.rs', lines 518:4-526:5 -/
+divergent def betree.Node.apply_messages_to_internal_loop
(msgs : betree.List (U64 × betree.Message))
(new_msgs : betree.List (U64 × betree.Message)) :
Result (betree.List (U64 × betree.Message))
@@ -439,12 +526,21 @@ divergent def betree.Node.apply_messages_to_internal
do
let (i, m) := new_msg
let msgs1 ← betree.Node.apply_to_internal msgs i m
- betree.Node.apply_messages_to_internal msgs1 new_msgs_tl
+ betree.Node.apply_messages_to_internal_loop msgs1 new_msgs_tl
| betree.List.Nil => Result.ok msgs
-/- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]:
- Source: 'src/betree.rs', lines 653:4-656:32 -/
-divergent def betree.Node.lookup_mut_in_bindings
+/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]:
+ Source: 'src/betree.rs', lines 518:4-521:5 -/
+def betree.Node.apply_messages_to_internal
+ (msgs : betree.List (U64 × betree.Message))
+ (new_msgs : betree.List (U64 × betree.Message)) :
+ Result (betree.List (U64 × betree.Message))
+ :=
+ betree.Node.apply_messages_to_internal_loop msgs new_msgs
+
+/- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: loop 0:
+ Source: 'src/betree.rs', lines 664:4-677:5 -/
+divergent def betree.Node.lookup_mut_in_bindings_loop
(key : U64) (bindings : betree.List (U64 × U64)) :
Result ((betree.List (U64 × U64)) × (betree.List (U64 × U64) → Result
(betree.List (U64 × U64))))
@@ -456,18 +552,26 @@ divergent def betree.Node.lookup_mut_in_bindings
then Result.ok (betree.List.Cons (i, i1) tl, Result.ok)
else
do
- let (l, lookup_mut_in_bindings_back) ←
- betree.Node.lookup_mut_in_bindings key tl
- let back :=
+ let (l, back) ← betree.Node.lookup_mut_in_bindings_loop key tl
+ let back1 :=
fun ret =>
do
- let tl1 ← lookup_mut_in_bindings_back ret
+ let tl1 ← back ret
Result.ok (betree.List.Cons (i, i1) tl1)
- Result.ok (l, back)
+ Result.ok (l, back1)
| betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
+/- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]:
+ Source: 'src/betree.rs', lines 664:4-667:32 -/
+def betree.Node.lookup_mut_in_bindings
+ (key : U64) (bindings : betree.List (U64 × U64)) :
+ Result ((betree.List (U64 × U64)) × (betree.List (U64 × U64) → Result
+ (betree.List (U64 × U64))))
+ :=
+ betree.Node.lookup_mut_in_bindings_loop key bindings
+
/- [betree::betree::{betree::betree::Node#5}::apply_to_leaf]:
- Source: 'src/betree.rs', lines 460:4-460:87 -/
+ Source: 'src/betree.rs', lines 476:4-476:87 -/
def betree.Node.apply_to_leaf
(bindings : betree.List (U64 × U64)) (key : U64) (new_msg : betree.Message)
:
@@ -506,9 +610,9 @@ def betree.Node.apply_to_leaf
let bindings2 ← betree.List.push_front (U64 × U64) bindings1 (key, v)
lookup_mut_in_bindings_back bindings2
-/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]:
- Source: 'src/betree.rs', lines 444:4-447:5 -/
-divergent def betree.Node.apply_messages_to_leaf
+/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: loop 0:
+ Source: 'src/betree.rs', lines 463:4-471:5 -/
+divergent def betree.Node.apply_messages_to_leaf_loop
(bindings : betree.List (U64 × U64))
(new_msgs : betree.List (U64 × betree.Message)) :
Result (betree.List (U64 × U64))
@@ -518,11 +622,20 @@ divergent def betree.Node.apply_messages_to_leaf
do
let (i, m) := new_msg
let bindings1 ← betree.Node.apply_to_leaf bindings i m
- betree.Node.apply_messages_to_leaf bindings1 new_msgs_tl
+ betree.Node.apply_messages_to_leaf_loop bindings1 new_msgs_tl
| betree.List.Nil => Result.ok bindings
+/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]:
+ Source: 'src/betree.rs', lines 463:4-466:5 -/
+def betree.Node.apply_messages_to_leaf
+ (bindings : betree.List (U64 × U64))
+ (new_msgs : betree.List (U64 × betree.Message)) :
+ Result (betree.List (U64 × U64))
+ :=
+ betree.Node.apply_messages_to_leaf_loop bindings new_msgs
+
/- [betree::betree::{betree::betree::Internal#4}::flush]:
- Source: 'src/betree.rs', lines 410:4-415:26 -/
+ Source: 'src/betree.rs', lines 429:4-434:26 -/
mutual divergent def betree.Internal.flush
(self : betree.Internal) (params : betree.Params)
(node_id_cnt : betree.NodeIdCounter)
@@ -563,7 +676,7 @@ mutual divergent def betree.Internal.flush
self.left n, node_id_cnt1)))
/- [betree::betree::{betree::betree::Node#5}::apply_messages]:
- Source: 'src/betree.rs', lines 588:4-593:5 -/
+ Source: 'src/betree.rs', lines 601:4-606:5 -/
divergent def betree.Node.apply_messages
(self : betree.Node) (params : betree.Params)
(node_id_cnt : betree.NodeIdCounter)
@@ -610,7 +723,7 @@ divergent def betree.Node.apply_messages
end
/- [betree::betree::{betree::betree::Node#5}::apply]:
- Source: 'src/betree.rs', lines 576:4-582:5 -/
+ Source: 'src/betree.rs', lines 589:4-595:5 -/
def betree.Node.apply
(self : betree.Node) (params : betree.Params)
(node_id_cnt : betree.NodeIdCounter) (key : U64) (new_msg : betree.Message)
@@ -625,7 +738,7 @@ def betree.Node.apply
Result.ok (st1, (self1, node_id_cnt1))
/- [betree::betree::{betree::betree::BeTree#6}::new]:
- Source: 'src/betree.rs', lines 849:4-849:60 -/
+ Source: 'src/betree.rs', lines 848:4-848:60 -/
def betree.BeTree.new
(min_flush_size : U64) (split_size : U64) (st : State) :
Result (State × betree.BeTree)
@@ -642,7 +755,7 @@ def betree.BeTree.new
})
/- [betree::betree::{betree::betree::BeTree#6}::apply]:
- Source: 'src/betree.rs', lines 868:4-868:47 -/
+ Source: 'src/betree.rs', lines 867:4-867:47 -/
def betree.BeTree.apply
(self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) :
Result (State × betree.BeTree)
@@ -654,7 +767,7 @@ def betree.BeTree.apply
Result.ok (st1, { self with node_id_cnt := nic, root := n })
/- [betree::betree::{betree::betree::BeTree#6}::insert]:
- Source: 'src/betree.rs', lines 874:4-874:52 -/
+ Source: 'src/betree.rs', lines 873:4-873:52 -/
def betree.BeTree.insert
(self : betree.BeTree) (key : U64) (value : U64) (st : State) :
Result (State × betree.BeTree)
@@ -662,7 +775,7 @@ def betree.BeTree.insert
betree.BeTree.apply self key (betree.Message.Insert value) st
/- [betree::betree::{betree::betree::BeTree#6}::delete]:
- Source: 'src/betree.rs', lines 880:4-880:38 -/
+ Source: 'src/betree.rs', lines 879:4-879:38 -/
def betree.BeTree.delete
(self : betree.BeTree) (key : U64) (st : State) :
Result (State × betree.BeTree)
@@ -670,7 +783,7 @@ def betree.BeTree.delete
betree.BeTree.apply self key betree.Message.Delete st
/- [betree::betree::{betree::betree::BeTree#6}::upsert]:
- Source: 'src/betree.rs', lines 886:4-886:59 -/
+ Source: 'src/betree.rs', lines 885:4-885:59 -/
def betree.BeTree.upsert
(self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State)
:
@@ -679,7 +792,7 @@ def betree.BeTree.upsert
betree.BeTree.apply self key (betree.Message.Upsert upd) st
/- [betree::betree::{betree::betree::BeTree#6}::lookup]:
- Source: 'src/betree.rs', lines 895:4-895:62 -/
+ Source: 'src/betree.rs', lines 894:4-894:62 -/
def betree.BeTree.lookup
(self : betree.BeTree) (key : U64) (st : State) :
Result (State × ((Option U64) × betree.BeTree))