diff options
Diffstat (limited to '')
3 files changed, 10 insertions, 10 deletions
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst index 537705c5..de56ba46 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst @@ -22,7 +22,7 @@ let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t) (** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause Source: 'src/betree.rs', lines 339:4-339:73 *) unfold -let betree_ListTupleU64T_partition_at_pivot_decreases (t : Type0) +let betree_ListPairU64T_partition_at_pivot_decreases (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) : nat = admit () diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst index 21f953d1..ed5c5069 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst @@ -114,7 +114,7 @@ let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t) (** [betree_main::betree::List::{2}::partition_at_pivot]: decreases clause *) unfold -let betree_ListTupleU64T_partition_at_pivot_decreases (t : Type0) +let betree_ListPairU64T_partition_at_pivot_decreases (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) : betree_List_t (u64 & t) = self diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst index 196f120c..ec042fb3 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst @@ -134,7 +134,7 @@ let betree_List_hd (t : Type0) (self : betree_List_t t) : result t = (** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: Source: 'src/betree.rs', lines 327:4-327:44 *) -let betree_ListTupleU64T_head_has_key +let betree_ListPairU64T_head_has_key (t : Type0) (self : betree_List_t (u64 & t)) (key : u64) : result bool = begin match self with | Betree_List_Cons hd _ -> let (i, _) = hd in Return (i = key) @@ -143,10 +143,10 @@ let betree_ListTupleU64T_head_has_key (** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: Source: 'src/betree.rs', lines 339:4-339:73 *) -let rec betree_ListTupleU64T_partition_at_pivot +let rec betree_ListPairU64T_partition_at_pivot (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) : Tot (result ((betree_List_t (u64 & t)) & (betree_List_t (u64 & t)))) - (decreases (betree_ListTupleU64T_partition_at_pivot_decreases t self pivot)) + (decreases (betree_ListPairU64T_partition_at_pivot_decreases t self pivot)) = begin match self with | Betree_List_Cons hd tl -> @@ -154,7 +154,7 @@ let rec betree_ListTupleU64T_partition_at_pivot if i >= pivot then Return (Betree_List_Nil, Betree_List_Cons (i, x) tl) else - let* p = betree_ListTupleU64T_partition_at_pivot t tl pivot in + let* p = betree_ListPairU64T_partition_at_pivot t tl pivot in let (ls0, ls1) = p in Return (Betree_List_Cons (i, x) ls0, ls1) | Betree_List_Nil -> Return (Betree_List_Nil, Betree_List_Nil) @@ -228,7 +228,7 @@ let rec betree_Node_apply_upserts Tot (result (state & (u64 & (betree_List_t (u64 & betree_Message_t))))) (decreases (betree_Node_apply_upserts_decreases msgs prev key st)) = - let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs key in + let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs key in if b then let* (msg, l) = betree_List_pop_front (u64 & betree_Message_t) msgs in @@ -369,7 +369,7 @@ let betree_Node_apply_to_internal = let* (msgs1, lookup_first_message_for_key_back) = betree_Node_lookup_first_message_for_key key msgs in - let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs1 key in + let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs1 key in if b then begin match new_msg with @@ -467,7 +467,7 @@ let betree_Node_apply_to_leaf = let* (bindings1, lookup_mut_in_bindings_back) = betree_Node_lookup_mut_in_bindings key bindings in - let* b = betree_ListTupleU64T_head_has_key u64 bindings1 key in + let* b = betree_ListPairU64T_head_has_key u64 bindings1 key in if b then let* (hd, l) = betree_List_pop_front (u64 & u64) bindings1 in @@ -522,7 +522,7 @@ let rec betree_Internal_flush betree_Internal_flush_decreases self params node_id_cnt content st)) = let* p = - betree_ListTupleU64T_partition_at_pivot betree_Message_t content self.pivot + betree_ListPairU64T_partition_at_pivot betree_Message_t content self.pivot in let (msgs_left, msgs_right) = p in let* len_left = betree_List_len (u64 & betree_Message_t) msgs_left in |