diff options
Diffstat (limited to 'tests/coq/betree')
| -rw-r--r-- | tests/coq/betree/BetreeMain_Funs.v | 24 | ||||
| -rw-r--r-- | tests/coq/betree/BetreeMain_FunsExternal.v | 6 | ||||
| -rw-r--r-- | tests/coq/betree/Primitives.v | 7 |
3 files changed, 18 insertions, 19 deletions
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v index 80518eab..c31713be 100644 --- a/tests/coq/betree/BetreeMain_Funs.v +++ b/tests/coq/betree/BetreeMain_Funs.v @@ -275,8 +275,8 @@ Fixpoint betree_Node_lookup_in_bindings Source: 'src/betree.rs', lines 819:4-819:90 *) Fixpoint betree_Node_apply_upserts (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64) - (key : u64) (st : state) : - result (state * (u64 * (betree_List_t (u64 * betree_Message_t)))) + (key : u64) : + result (u64 * (betree_List_t (u64 * betree_Message_t))) := match n with | O => Fail_ OutOfFuel @@ -292,15 +292,14 @@ 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 st + betree_Node_apply_upserts n1 msgs1 (Some v) key end) else ( - p <- core_option_Option_unwrap u64 prev st; - let (st1, v) := p in + v <- core_option_Option_unwrap u64 prev; msgs1 <- betree_List_push_front (u64 * betree_Message_t) msgs (key, Betree_Message_Insert v); - Ok (st1, (v, msgs1))) + Ok (v, msgs1)) end . @@ -371,14 +370,13 @@ with betree_Node_lookup let (v, node1) := p4 in p5 <- betree_Node_apply_upserts n1 (Betree_List_Cons (k, - Betree_Message_Upsert ufs) l) v key st2; - let (st3, p6) := p5 in - let (v1, pending1) := p6 in + Betree_Message_Upsert ufs) l) v key; + let (v1, pending1) := p5 in msgs1 <- lookup_first_message_for_key_back pending1; - p7 <- - betree_store_internal_node node1.(betree_Internal_id) msgs1 st3; - let (st4, _) := p7 in - Ok (st4, (Some v1, Betree_Node_Internal node1)) + p6 <- + betree_store_internal_node node1.(betree_Internal_id) msgs1 st2; + let (st3, _) := p6 in + Ok (st3, (Some v1, Betree_Node_Internal node1)) end | Betree_List_Nil => p2 <- betree_Internal_lookup_in_children n1 node key st1; diff --git a/tests/coq/betree/BetreeMain_FunsExternal.v b/tests/coq/betree/BetreeMain_FunsExternal.v index 2d77c4ed..099a2e8f 100644 --- a/tests/coq/betree/BetreeMain_FunsExternal.v +++ b/tests/coq/betree/BetreeMain_FunsExternal.v @@ -36,10 +36,4 @@ Axiom betree_utils_store_leaf_node : u64 -> betree_List_t (u64 * u64) -> state -> result (state * unit) . -(** [core::option::{core::option::Option<T>}::unwrap]: forward function - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *) -Axiom core_option_Option_unwrap : - forall(T : Type), option T -> state -> result (state * T) -. - End BetreeMain_FunsExternal. diff --git a/tests/coq/betree/Primitives.v b/tests/coq/betree/Primitives.v index 5ffda12f..b29fce43 100644 --- a/tests/coq/betree/Primitives.v +++ b/tests/coq/betree/Primitives.v @@ -564,6 +564,13 @@ Definition core_clone_CloneI128 : core_clone_Clone i128 := {| clone := fun x => Ok (core_clone_impls_CloneI128_clone x) |}. +(** [core::option::{core::option::Option<T>}::unwrap] *) +Definition core_option_Option_unwrap (T : Type) (x : option T) : result T := + match x with + | None => Fail_ Failure + | Some x => Ok x + end. + (*** core::ops *) (* Trait declaration: [core::ops::index::Index] *) |