summaryrefslogtreecommitdiff
path: root/tests/coq
diff options
context:
space:
mode:
Diffstat (limited to 'tests/coq')
-rw-r--r--tests/coq/arrays/Primitives.v7
-rw-r--r--tests/coq/betree/BetreeMain_Funs.v24
-rw-r--r--tests/coq/betree/BetreeMain_FunsExternal.v6
-rw-r--r--tests/coq/betree/BetreeMain_FunsExternal_Template.v7
-rw-r--r--tests/coq/betree/Primitives.v7
-rw-r--r--tests/coq/demo/Primitives.v7
-rw-r--r--tests/coq/hashmap/Primitives.v7
-rw-r--r--tests/coq/hashmap_on_disk/Primitives.v7
-rw-r--r--tests/coq/misc/Primitives.v7
-rw-r--r--tests/coq/traits/Primitives.v7
10 files changed, 60 insertions, 26 deletions
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] *)
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 04:28:25 +0000