diff options
author | Son HO | 2024-04-26 10:55:47 +0200 |
---|---|---|
committer | GitHub | 2024-04-26 10:55:47 +0200 |
commit | 5da597289c1723aa59bf87ad5075675820c18f73 (patch) | |
tree | d63e2f44c75634674a3e4eabb57ff08c0ae441ac | |
parent | 2df6dd65b84a2fd9aad4f716f323bf3f85bf82db (diff) | |
parent | fe8d14cd8b7ba907d5248d574619e93e6d1d253a (diff) |
Merge pull request #125 from zhassan-aws/core-option-unwrap
Add `core::option::unwrap` builtin
36 files changed, 173 insertions, 89 deletions
diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v index 5ffda12f..b29fce43 100644 --- a/backends/coq/Primitives.v +++ b/backends/coq/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] *) diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst index c7c9f9db..9951ccc3 100644 --- a/backends/fstar/Primitives.fst +++ b/backends/fstar/Primitives.fst @@ -540,6 +540,12 @@ let core_clone_CloneI128 : core_clone_Clone i128 = { clone = fun x -> Ok (core_clone_impls_CloneI128_clone x) } +(** [core::option::{core::option::Option<T>}::unwrap] *) +let core_option_Option_unwrap (t : Type0) (x : option t) : result t = + match x with + | None -> Fail Failure + | Some x -> Ok x + (*** core::ops *) // Trait declaration: [core::ops::index::Index] diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean index 94134d86..d682e926 100644 --- a/backends/lean/Base/Primitives/Base.lean +++ b/backends/lean/Base/Primitives/Base.lean @@ -76,6 +76,11 @@ def eval_global {α: Type u} (x: Result α) (_: ok? x := by prove_eval_global) : | fail _ | div => by contradiction | ok x => x +def Result.ofOption {a : Type u} (x : Option a) (e : Error) : Result a := + match x with + | some x => ok x + | none => fail e + /- DO-DSL SUPPORT -/ def bind {α : Type u} {β : Type v} (x: Result α) (f: α → Result β) : Result β := diff --git a/backends/lean/Base/Primitives/Core.lean b/backends/lean/Base/Primitives/Core.lean index 99f65985..14a51bc1 100644 --- a/backends/lean/Base/Primitives/Core.lean +++ b/backends/lean/Base/Primitives/Core.lean @@ -51,4 +51,12 @@ def clone.CloneBool : clone.Clone Bool := { clone := fun b => ok (clone.impls.CloneBool.clone b) } +namespace option -- core.option + +/- [core::option::{core::option::Option<T>}::unwrap] -/ +def Option.unwrap (T : Type) (x : Option T) : Result T := + Result.ofOption x Error.panic + +end option -- core.option + end core diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index 014decb1..2bee8a2f 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -364,11 +364,6 @@ def Scalar.tryMkOpt (ty : ScalarTy) (x : Int) : Option (Scalar ty) := some (Scalar.ofIntCore x (Scalar.check_bounds_imp_in_bounds h)) else none -def Result.ofOption {a : Type u} (x : Option a) (e : Error) : Result a := - match x with - | some x => ok x - | none => fail e - def Scalar.tryMk (ty : ScalarTy) (x : Int) : Result (Scalar ty) := Result.ofOption (tryMkOpt ty x) integerOverflow diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index c6827bbe..a7ab6da0 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -387,6 +387,8 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list = @A>>}::deref_mut" (Some "alloc.vec.DerefMutVec.deref_mut") (Some [ true; false ]); + mk_fun "core::option::{core::option::Option<@T>}::unwrap" + (Some "core.option.Option.unwrap") None; ] @ List.flatten (List.map @@ -552,14 +554,17 @@ let builtin_fun_effects = (fun n -> (n, { can_fail = false; stateful = false })) no_fail_no_state_funs in + (* TODO: all the functions registered in the [builtin_funs] above should + be considered as not using a state. There is a lot of redundancy + right now. *) let no_state_funs = [ - (* TODO: redundancy with the funs information above *) "alloc::vec::{alloc::vec::Vec<@T, @A>}::push"; "alloc::vec::{core::ops::index::Index<alloc::vec::Vec<@T, @A>, \ @I>}::index"; "alloc::vec::{core::ops::index::IndexMut<alloc::vec::Vec<@T, @A>, \ @I>}::index_mut"; + "core::option::{core::option::Option<@T>}::unwrap"; ] in let no_state_funs = diff --git a/tests/coq/arrays/Primitives.v b/tests/coq/arrays/Primitives.v index 5ffda12f..b29fce43 100644 --- a/tests/coq/arrays/Primitives.v +++ b/tests/coq/arrays/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] *) 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/BetreeMain_FunsExternal_Template.v b/tests/coq/betree/BetreeMain_FunsExternal_Template.v index 1367bac2..58be2733 100644 --- a/tests/coq/betree/BetreeMain_FunsExternal_Template.v +++ b/tests/coq/betree/BetreeMain_FunsExternal_Template.v @@ -37,11 +37,4 @@ Axiom betree_utils_store_leaf_node : u64 -> betree_List_t (u64 * u64) -> state -> result (state * unit) . -(** [core::option::{core::option::Option<T>}::unwrap]: - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 - Name pattern: core::option::{core::option::Option<@T>}::unwrap *) -Axiom core_option_Option_unwrap : - forall(T : Type), option T -> state -> result (state * T) -. - End BetreeMain_FunsExternal_Template. 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] *) diff --git a/tests/coq/demo/Primitives.v b/tests/coq/demo/Primitives.v index 5ffda12f..b29fce43 100644 --- a/tests/coq/demo/Primitives.v +++ b/tests/coq/demo/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] *) diff --git a/tests/coq/hashmap/Primitives.v b/tests/coq/hashmap/Primitives.v index 5ffda12f..b29fce43 100644 --- a/tests/coq/hashmap/Primitives.v +++ b/tests/coq/hashmap/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] *) diff --git a/tests/coq/hashmap_on_disk/Primitives.v b/tests/coq/hashmap_on_disk/Primitives.v index 5ffda12f..b29fce43 100644 --- a/tests/coq/hashmap_on_disk/Primitives.v +++ b/tests/coq/hashmap_on_disk/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] *) diff --git a/tests/coq/misc/Primitives.v b/tests/coq/misc/Primitives.v index 5ffda12f..b29fce43 100644 --- a/tests/coq/misc/Primitives.v +++ b/tests/coq/misc/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] *) diff --git a/tests/coq/traits/Primitives.v b/tests/coq/traits/Primitives.v index 5ffda12f..b29fce43 100644 --- a/tests/coq/traits/Primitives.v +++ b/tests/coq/traits/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] *) diff --git a/tests/fstar/arrays/Primitives.fst b/tests/fstar/arrays/Primitives.fst index c7c9f9db..9951ccc3 100644 --- a/tests/fstar/arrays/Primitives.fst +++ b/tests/fstar/arrays/Primitives.fst @@ -540,6 +540,12 @@ let core_clone_CloneI128 : core_clone_Clone i128 = { clone = fun x -> Ok (core_clone_impls_CloneI128_clone x) } +(** [core::option::{core::option::Option<T>}::unwrap] *) +let core_option_Option_unwrap (t : Type0) (x : option t) : result t = + match x with + | None -> Fail Failure + | Some x -> Ok x + (*** core::ops *) // Trait declaration: [core::ops::index::Index] diff --git a/tests/fstar/betree/BetreeMain.Clauses.Template.fst b/tests/fstar/betree/BetreeMain.Clauses.Template.fst index de56ba46..b317dca4 100644 --- a/tests/fstar/betree/BetreeMain.Clauses.Template.fst +++ b/tests/fstar/betree/BetreeMain.Clauses.Template.fst @@ -45,7 +45,7 @@ let betree_Node_lookup_in_bindings_decreases (key : u64) unfold let betree_Node_apply_upserts_decreases (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64) - (key : u64) (st : state) : nat = + (key : u64) : nat = admit () (** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: decreases clause diff --git a/tests/fstar/betree/BetreeMain.Clauses.fst b/tests/fstar/betree/BetreeMain.Clauses.fst index ed5c5069..b95d4c7e 100644 --- a/tests/fstar/betree/BetreeMain.Clauses.fst +++ b/tests/fstar/betree/BetreeMain.Clauses.fst @@ -134,7 +134,7 @@ let betree_Node_lookup_first_message_for_key_decreases (key : u64) unfold let betree_Node_apply_upserts_decreases (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64) - (key : u64) (st : state) : betree_List_t (u64 & betree_Message_t) = + (key : u64) : betree_List_t (u64 & betree_Message_t) = msgs (** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *) diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst index 8e64f43f..89396df0 100644 --- a/tests/fstar/betree/BetreeMain.Funs.fst +++ b/tests/fstar/betree/BetreeMain.Funs.fst @@ -223,9 +223,9 @@ let rec betree_Node_lookup_in_bindings Source: 'src/betree.rs', lines 819:4-819:90 *) let rec betree_Node_apply_upserts (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64) - (key : u64) (st : state) : - Tot (result (state & (u64 & (betree_List_t (u64 & betree_Message_t))))) - (decreases (betree_Node_apply_upserts_decreases msgs prev key st)) + (key : u64) : + Tot (result (u64 & (betree_List_t (u64 & betree_Message_t)))) + (decreases (betree_Node_apply_upserts_decreases msgs prev key)) = let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs key in if b @@ -237,14 +237,14 @@ let rec betree_Node_apply_upserts | Betree_Message_Delete -> Fail Failure | Betree_Message_Upsert s -> let* v = betree_upsert_update prev s in - betree_Node_apply_upserts msgs1 (Some v) key st + betree_Node_apply_upserts msgs1 (Some v) key end else - let* (st1, v) = core_option_Option_unwrap u64 prev st in + let* v = core_option_Option_unwrap u64 prev in let* msgs1 = betree_List_push_front (u64 & betree_Message_t) msgs (key, Betree_Message_Insert v) in - Ok (st1, (v, msgs1)) + Ok (v, msgs1) (** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: Source: 'src/betree.rs', lines 395:4-395:63 *) @@ -298,12 +298,12 @@ and betree_Node_lookup | Betree_Message_Upsert ufs -> let* (st2, (v, node1)) = betree_Internal_lookup_in_children node key st1 in - let* (st3, (v1, pending1)) = + let* (v1, pending1) = betree_Node_apply_upserts (Betree_List_Cons (k, - Betree_Message_Upsert ufs) l) v key st2 in + Betree_Message_Upsert ufs) l) v key in let* msgs1 = lookup_first_message_for_key_back pending1 in - let* (st4, _) = betree_store_internal_node node1.id msgs1 st3 in - Ok (st4, (Some v1, Betree_Node_Internal node1)) + let* (st3, _) = betree_store_internal_node node1.id msgs1 st2 in + Ok (st3, (Some v1, Betree_Node_Internal node1)) end | Betree_List_Nil -> let* (st2, (o, node1)) = betree_Internal_lookup_in_children node key st1 diff --git a/tests/fstar/betree/BetreeMain.FunsExternal.fsti b/tests/fstar/betree/BetreeMain.FunsExternal.fsti index 3aad9390..8be98acf 100644 --- a/tests/fstar/betree/BetreeMain.FunsExternal.fsti +++ b/tests/fstar/betree/BetreeMain.FunsExternal.fsti @@ -28,9 +28,3 @@ val betree_utils_load_leaf_node val betree_utils_store_leaf_node : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit) -(** [core::option::{core::option::Option<T>}::unwrap]: - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 - Name pattern: core::option::{core::option::Option<@T>}::unwrap *) -val core_option_Option_unwrap - (t : Type0) : option t -> state -> result (state & t) - diff --git a/tests/fstar/betree/Primitives.fst b/tests/fstar/betree/Primitives.fst index c7c9f9db..9951ccc3 100644 --- a/tests/fstar/betree/Primitives.fst +++ b/tests/fstar/betree/Primitives.fst @@ -540,6 +540,12 @@ let core_clone_CloneI128 : core_clone_Clone i128 = { clone = fun x -> Ok (core_clone_impls_CloneI128_clone x) } +(** [core::option::{core::option::Option<T>}::unwrap] *) +let core_option_Option_unwrap (t : Type0) (x : option t) : result t = + match x with + | None -> Fail Failure + | Some x -> Ok x + (*** core::ops *) // Trait declaration: [core::ops::index::Index] diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst index de56ba46..b317dca4 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst @@ -45,7 +45,7 @@ let betree_Node_lookup_in_bindings_decreases (key : u64) unfold let betree_Node_apply_upserts_decreases (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64) - (key : u64) (st : state) : nat = + (key : u64) : nat = admit () (** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: decreases clause diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst index ed5c5069..b95d4c7e 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst @@ -134,7 +134,7 @@ let betree_Node_lookup_first_message_for_key_decreases (key : u64) unfold let betree_Node_apply_upserts_decreases (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64) - (key : u64) (st : state) : betree_List_t (u64 & betree_Message_t) = + (key : u64) : betree_List_t (u64 & betree_Message_t) = msgs (** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *) diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst index 8e64f43f..89396df0 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst @@ -223,9 +223,9 @@ let rec betree_Node_lookup_in_bindings Source: 'src/betree.rs', lines 819:4-819:90 *) let rec betree_Node_apply_upserts (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64) - (key : u64) (st : state) : - Tot (result (state & (u64 & (betree_List_t (u64 & betree_Message_t))))) - (decreases (betree_Node_apply_upserts_decreases msgs prev key st)) + (key : u64) : + Tot (result (u64 & (betree_List_t (u64 & betree_Message_t)))) + (decreases (betree_Node_apply_upserts_decreases msgs prev key)) = let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs key in if b @@ -237,14 +237,14 @@ let rec betree_Node_apply_upserts | Betree_Message_Delete -> Fail Failure | Betree_Message_Upsert s -> let* v = betree_upsert_update prev s in - betree_Node_apply_upserts msgs1 (Some v) key st + betree_Node_apply_upserts msgs1 (Some v) key end else - let* (st1, v) = core_option_Option_unwrap u64 prev st in + let* v = core_option_Option_unwrap u64 prev in let* msgs1 = betree_List_push_front (u64 & betree_Message_t) msgs (key, Betree_Message_Insert v) in - Ok (st1, (v, msgs1)) + Ok (v, msgs1) (** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: Source: 'src/betree.rs', lines 395:4-395:63 *) @@ -298,12 +298,12 @@ and betree_Node_lookup | Betree_Message_Upsert ufs -> let* (st2, (v, node1)) = betree_Internal_lookup_in_children node key st1 in - let* (st3, (v1, pending1)) = + let* (v1, pending1) = betree_Node_apply_upserts (Betree_List_Cons (k, - Betree_Message_Upsert ufs) l) v key st2 in + Betree_Message_Upsert ufs) l) v key in let* msgs1 = lookup_first_message_for_key_back pending1 in - let* (st4, _) = betree_store_internal_node node1.id msgs1 st3 in - Ok (st4, (Some v1, Betree_Node_Internal node1)) + let* (st3, _) = betree_store_internal_node node1.id msgs1 st2 in + Ok (st3, (Some v1, Betree_Node_Internal node1)) end | Betree_List_Nil -> let* (st2, (o, node1)) = betree_Internal_lookup_in_children node key st1 diff --git a/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti index 3aad9390..8be98acf 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti +++ b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti @@ -28,9 +28,3 @@ val betree_utils_load_leaf_node val betree_utils_store_leaf_node : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit) -(** [core::option::{core::option::Option<T>}::unwrap]: - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 - Name pattern: core::option::{core::option::Option<@T>}::unwrap *) -val core_option_Option_unwrap - (t : Type0) : option t -> state -> result (state & t) - diff --git a/tests/fstar/betree_back_stateful/Primitives.fst b/tests/fstar/betree_back_stateful/Primitives.fst index c7c9f9db..9951ccc3 100644 --- a/tests/fstar/betree_back_stateful/Primitives.fst +++ b/tests/fstar/betree_back_stateful/Primitives.fst @@ -540,6 +540,12 @@ let core_clone_CloneI128 : core_clone_Clone i128 = { clone = fun x -> Ok (core_clone_impls_CloneI128_clone x) } +(** [core::option::{core::option::Option<T>}::unwrap] *) +let core_option_Option_unwrap (t : Type0) (x : option t) : result t = + match x with + | None -> Fail Failure + | Some x -> Ok x + (*** core::ops *) // Trait declaration: [core::ops::index::Index] diff --git a/tests/fstar/demo/Primitives.fst b/tests/fstar/demo/Primitives.fst index c7c9f9db..9951ccc3 100644 --- a/tests/fstar/demo/Primitives.fst +++ b/tests/fstar/demo/Primitives.fst @@ -540,6 +540,12 @@ let core_clone_CloneI128 : core_clone_Clone i128 = { clone = fun x -> Ok (core_clone_impls_CloneI128_clone x) } +(** [core::option::{core::option::Option<T>}::unwrap] *) +let core_option_Option_unwrap (t : Type0) (x : option t) : result t = + match x with + | None -> Fail Failure + | Some x -> Ok x + (*** core::ops *) // Trait declaration: [core::ops::index::Index] diff --git a/tests/fstar/hashmap/Primitives.fst b/tests/fstar/hashmap/Primitives.fst index c7c9f9db..9951ccc3 100644 --- a/tests/fstar/hashmap/Primitives.fst +++ b/tests/fstar/hashmap/Primitives.fst @@ -540,6 +540,12 @@ let core_clone_CloneI128 : core_clone_Clone i128 = { clone = fun x -> Ok (core_clone_impls_CloneI128_clone x) } +(** [core::option::{core::option::Option<T>}::unwrap] *) +let core_option_Option_unwrap (t : Type0) (x : option t) : result t = + match x with + | None -> Fail Failure + | Some x -> Ok x + (*** core::ops *) // Trait declaration: [core::ops::index::Index] diff --git a/tests/fstar/hashmap_on_disk/Primitives.fst b/tests/fstar/hashmap_on_disk/Primitives.fst index c7c9f9db..9951ccc3 100644 --- a/tests/fstar/hashmap_on_disk/Primitives.fst +++ b/tests/fstar/hashmap_on_disk/Primitives.fst @@ -540,6 +540,12 @@ let core_clone_CloneI128 : core_clone_Clone i128 = { clone = fun x -> Ok (core_clone_impls_CloneI128_clone x) } +(** [core::option::{core::option::Option<T>}::unwrap] *) +let core_option_Option_unwrap (t : Type0) (x : option t) : result t = + match x with + | None -> Fail Failure + | Some x -> Ok x + (*** core::ops *) // Trait declaration: [core::ops::index::Index] diff --git a/tests/fstar/misc/Primitives.fst b/tests/fstar/misc/Primitives.fst index c7c9f9db..9951ccc3 100644 --- a/tests/fstar/misc/Primitives.fst +++ b/tests/fstar/misc/Primitives.fst @@ -540,6 +540,12 @@ let core_clone_CloneI128 : core_clone_Clone i128 = { clone = fun x -> Ok (core_clone_impls_CloneI128_clone x) } +(** [core::option::{core::option::Option<T>}::unwrap] *) +let core_option_Option_unwrap (t : Type0) (x : option t) : result t = + match x with + | None -> Fail Failure + | Some x -> Ok x + (*** core::ops *) // Trait declaration: [core::ops::index::Index] diff --git a/tests/fstar/traits/Primitives.fst b/tests/fstar/traits/Primitives.fst index c7c9f9db..9951ccc3 100644 --- a/tests/fstar/traits/Primitives.fst +++ b/tests/fstar/traits/Primitives.fst @@ -540,6 +540,12 @@ let core_clone_CloneI128 : core_clone_Clone i128 = { clone = fun x -> Ok (core_clone_impls_CloneI128_clone x) } +(** [core::option::{core::option::Option<T>}::unwrap] *) +let core_option_Option_unwrap (t : Type0) (x : option t) : result t = + match x with + | None -> Fail Failure + | Some x -> Ok x + (*** core::ops *) // Trait declaration: [core::ops::index::Index] diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean index 0c31b9bc..f0032d51 100644 --- a/tests/lean/BetreeMain/Funs.lean +++ b/tests/lean/BetreeMain/Funs.lean @@ -219,8 +219,8 @@ divergent def betree.Node.lookup_in_bindings Source: 'src/betree.rs', lines 819:4-819:90 -/ divergent def betree.Node.apply_upserts (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64) - (st : State) : - Result (State × (U64 × (betree.List (U64 × betree.Message)))) + : + Result (U64 × (betree.List (U64 × betree.Message))) := do let b ← betree.ListPairU64T.head_has_key betree.Message msgs key @@ -235,14 +235,14 @@ 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 st + betree.Node.apply_upserts msgs1 (some v) key else do - let (st1, v) ← core.option.Option.unwrap U64 prev st + let v ← core.option.Option.unwrap U64 prev let msgs1 ← betree.List.push_front (U64 × betree.Message) msgs (key, betree.Message.Insert v) - Result.ok (st1, (v, msgs1)) + Result.ok (v, msgs1) /- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: Source: 'src/betree.rs', lines 395:4-395:63 -/ @@ -307,13 +307,13 @@ divergent def betree.Node.lookup let (st2, (v, node1)) ← betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key st1 - let (st3, (v1, pending1)) ← + let (v1, pending1) ← betree.Node.apply_upserts (betree.List.Cons (k, - betree.Message.Upsert ufs) l) v key st2 + betree.Message.Upsert ufs) l) v key let ⟨ i2, i3, n2, n3 ⟩ := node1 let msgs1 ← lookup_first_message_for_key_back pending1 - let (st4, _) ← betree.store_internal_node i2 msgs1 st3 - Result.ok (st4, (some v1, betree.Node.Internal (betree.Internal.mk i2 + let (st3, _) ← betree.store_internal_node i2 msgs1 st2 + Result.ok (st3, (some v1, betree.Node.Internal (betree.Internal.mk i2 i3 n2 n3))) | betree.List.Nil => do diff --git a/tests/lean/BetreeMain/FunsExternal.lean b/tests/lean/BetreeMain/FunsExternal.lean index 71d26da4..d26177fb 100644 --- a/tests/lean/BetreeMain/FunsExternal.lean +++ b/tests/lean/BetreeMain/FunsExternal.lean @@ -28,8 +28,3 @@ def betree_utils.load_leaf_node def betree_utils.store_leaf_node : U64 → betree.List (U64 × U64) → State → Result (State × Unit) := fun _ _ _ => .fail .panic - -/- [core::option::Option::{0}::unwrap] -/ -def core.option.Option.unwrap - (T : Type) : Option T → State → Result (State × T) := - fun _ _ => .fail .panic diff --git a/tests/lean/BetreeMain/FunsExternal_Template.lean b/tests/lean/BetreeMain/FunsExternal_Template.lean index 0b3e4ef4..0dcce5ca 100644 --- a/tests/lean/BetreeMain/FunsExternal_Template.lean +++ b/tests/lean/BetreeMain/FunsExternal_Template.lean @@ -28,9 +28,3 @@ axiom betree_utils.load_leaf_node axiom betree_utils.store_leaf_node : U64 → betree.List (U64 × U64) → State → Result (State × Unit) -/- [core::option::{core::option::Option<T>}::unwrap]: - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 - Name pattern: core::option::{core::option::Option<@T>}::unwrap -/ -axiom core.option.Option.unwrap - (T : Type) : Option T → State → Result (State × T) - diff --git a/tests/lean/External/FunsExternal.lean b/tests/lean/External/FunsExternal.lean index 28ba2077..c3e8dd79 100644 --- a/tests/lean/External/FunsExternal.lean +++ b/tests/lean/External/FunsExternal.lean @@ -14,4 +14,3 @@ def core.cell.Cell.get def core.cell.Cell.get_mut (T : Type) (c : core.cell.Cell T) (s : State) : Result (State × (T × (T → State → Result (State × (core.cell.Cell T))))) := sorry - |