summaryrefslogtreecommitdiff
path: root/tests/coq
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/coq/arrays/Arrays.v67
-rw-r--r--tests/coq/arrays/Primitives.v46
-rw-r--r--tests/coq/betree/BetreeMain_Funs.v124
-rw-r--r--tests/coq/betree/Primitives.v46
-rw-r--r--tests/coq/demo/Demo.v40
-rw-r--r--tests/coq/demo/Primitives.v46
-rw-r--r--tests/coq/hashmap/Hashmap_Funs.v65
-rw-r--r--tests/coq/hashmap/Primitives.v46
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Funs.v64
-rw-r--r--tests/coq/hashmap_on_disk/Primitives.v46
-rw-r--r--tests/coq/misc/Bitwise.v6
-rw-r--r--tests/coq/misc/Constants.v35
-rw-r--r--tests/coq/misc/External_Funs.v10
-rw-r--r--tests/coq/misc/External_FunsExternal.v2
-rw-r--r--tests/coq/misc/Loops.v120
-rw-r--r--tests/coq/misc/NoNestedBorrows.v102
-rw-r--r--tests/coq/misc/Paper.v23
-rw-r--r--tests/coq/misc/PoloniusList.v8
-rw-r--r--tests/coq/misc/Primitives.v46
-rw-r--r--tests/coq/traits/Primitives.v46
-rw-r--r--tests/coq/traits/Traits.v50
21 files changed, 502 insertions, 536 deletions
diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v
index 049d63cb..c9696147 100644
--- a/tests/coq/arrays/Arrays.v
+++ b/tests/coq/arrays/Arrays.v
@@ -36,19 +36,19 @@ Definition array_to_mut_slice_
(** [arrays::array_len]:
Source: 'src/arrays.rs', lines 25:0-25:40 *)
Definition array_len (T : Type) (s : array T 32%usize) : result usize :=
- s1 <- array_to_slice T 32%usize s; Return (slice_len T s1)
+ s1 <- array_to_slice T 32%usize s; Ok (slice_len T s1)
.
(** [arrays::shared_array_len]:
Source: 'src/arrays.rs', lines 29:0-29:48 *)
Definition shared_array_len (T : Type) (s : array T 32%usize) : result usize :=
- s1 <- array_to_slice T 32%usize s; Return (slice_len T s1)
+ s1 <- array_to_slice T 32%usize s; Ok (slice_len T s1)
.
(** [arrays::shared_slice_len]:
Source: 'src/arrays.rs', lines 33:0-33:44 *)
Definition shared_slice_len (T : Type) (s : slice T) : result usize :=
- Return (slice_len T s)
+ Ok (slice_len T s)
.
(** [arrays::index_array_shared]:
@@ -114,7 +114,7 @@ Definition slice_subslice_mut_
(core_slice_index_SliceIndexRangeUsizeSliceTInst u32) x
{| core_ops_range_Range_start := y; core_ops_range_Range_end_ := z |};
let (s, index_mut_back) := p in
- Return (s, index_mut_back)
+ Ok (s, index_mut_back)
.
(** [arrays::array_to_slice_shared_]:
@@ -155,7 +155,7 @@ Definition array_subslice_mut_
(core_slice_index_SliceIndexRangeUsizeSliceTInst u32)) x
{| core_ops_range_Range_start := y; core_ops_range_Range_end_ := z |};
let (s, index_mut_back) := p in
- Return (s, index_mut_back)
+ Ok (s, index_mut_back)
.
(** [arrays::index_slice_0]:
@@ -192,47 +192,46 @@ Definition update_update_array
let (_, index_mut_back1) := p1 in
a1 <- index_mut_back1 0%u32;
_ <- index_mut_back a1;
- Return tt
+ Ok tt
.
(** [arrays::array_local_deep_copy]:
Source: 'src/arrays.rs', lines 118:0-118:43 *)
Definition array_local_deep_copy (x : array u32 32%usize) : result unit :=
- Return tt
+ Ok tt
.
(** [arrays::take_array]:
Source: 'src/arrays.rs', lines 122:0-122:30 *)
Definition take_array (a : array u32 2%usize) : result unit :=
- Return tt.
+ Ok tt.
(** [arrays::take_array_borrow]:
Source: 'src/arrays.rs', lines 123:0-123:38 *)
Definition take_array_borrow (a : array u32 2%usize) : result unit :=
- Return tt
-.
+ Ok tt.
(** [arrays::take_slice]:
Source: 'src/arrays.rs', lines 124:0-124:28 *)
Definition take_slice (s : slice u32) : result unit :=
- Return tt.
+ Ok tt.
(** [arrays::take_mut_slice]:
Source: 'src/arrays.rs', lines 125:0-125:36 *)
Definition take_mut_slice (s : slice u32) : result (slice u32) :=
- Return s.
+ Ok s.
(** [arrays::const_array]:
Source: 'src/arrays.rs', lines 127:0-127:32 *)
Definition const_array : result (array u32 2%usize) :=
- Return (mk_array u32 2%usize [ 0%u32; 0%u32 ])
+ Ok (mk_array u32 2%usize [ 0%u32; 0%u32 ])
.
(** [arrays::const_slice]:
Source: 'src/arrays.rs', lines 131:0-131:20 *)
Definition const_slice : result unit :=
_ <- array_to_slice u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]);
- Return tt
+ Ok tt
.
(** [arrays::take_all]:
@@ -247,7 +246,7 @@ Definition take_all : result unit :=
let (s1, to_slice_mut_back) := p in
s2 <- take_mut_slice s1;
_ <- to_slice_mut_back s2;
- Return tt
+ Ok tt
.
(** [arrays::index_array]:
@@ -272,7 +271,7 @@ Definition index_slice_u32_0 (x : slice u32) : result u32 :=
Source: 'src/arrays.rs', lines 166:0-166:50 *)
Definition index_mut_slice_u32_0
(x : slice u32) : result (u32 * (slice u32)) :=
- i <- slice_index_usize u32 x 0%usize; Return (i, x)
+ i <- slice_index_usize u32 x 0%usize; Ok (i, x)
.
(** [arrays::index_all]:
@@ -292,7 +291,7 @@ Definition index_all : result u32 :=
let (i7, s2) := p1 in
i8 <- u32_add i6 i7;
_ <- to_slice_mut_back s2;
- Return i8
+ Ok i8
.
(** [arrays::update_array]:
@@ -301,7 +300,7 @@ Definition update_array (x : array u32 2%usize) : result unit :=
p <- array_index_mut_usize u32 2%usize x 0%usize;
let (_, index_mut_back) := p in
_ <- index_mut_back 1%u32;
- Return tt
+ Ok tt
.
(** [arrays::update_array_mut_borrow]:
@@ -331,7 +330,7 @@ Definition update_all : result unit :=
let (s, to_slice_mut_back) := p in
s1 <- update_mut_slice s;
_ <- to_slice_mut_back s1;
- Return tt
+ Ok tt
.
(** [arrays::range_all]:
@@ -349,7 +348,7 @@ Definition range_all : result unit :=
let (s, index_mut_back) := p in
s1 <- update_mut_slice s;
_ <- index_mut_back s1;
- Return tt
+ Ok tt
.
(** [arrays::deref_array_borrow]:
@@ -362,13 +361,13 @@ Definition deref_array_borrow (x : array u32 2%usize) : result u32 :=
Source: 'src/arrays.rs', lines 219:0-219:54 *)
Definition deref_array_mut_borrow
(x : array u32 2%usize) : result (u32 * (array u32 2%usize)) :=
- i <- array_index_usize u32 2%usize x 0%usize; Return (i, x)
+ i <- array_index_usize u32 2%usize x 0%usize; Ok (i, x)
.
(** [arrays::take_array_t]:
Source: 'src/arrays.rs', lines 227:0-227:31 *)
Definition take_array_t (a : array AB_t 2%usize) : result unit :=
- Return tt.
+ Ok tt.
(** [arrays::non_copyable_array]:
Source: 'src/arrays.rs', lines 229:0-229:27 *)
@@ -390,7 +389,7 @@ Fixpoint sum_loop
sum3 <- u32_add sum1 i2;
i3 <- usize_add i 1%usize;
sum_loop n1 s sum3 i3)
- else Return sum1
+ else Ok sum1
end
.
@@ -418,7 +417,7 @@ Fixpoint sum2_loop
sum3 <- u32_add sum1 i4;
i5 <- usize_add i 1%usize;
sum2_loop n1 s s2 sum3 i5)
- else Return sum1
+ else Ok sum1
end
.
@@ -439,7 +438,7 @@ Definition f0 : result unit :=
let (_, index_mut_back) := p1 in
s1 <- index_mut_back 1%u32;
_ <- to_slice_mut_back s1;
- Return tt
+ Ok tt
.
(** [arrays::f1]:
@@ -450,13 +449,13 @@ Definition f1 : result unit :=
0%usize;
let (_, index_mut_back) := p in
_ <- index_mut_back 1%u32;
- Return tt
+ Ok tt
.
(** [arrays::f2]:
Source: 'src/arrays.rs', lines 273:0-273:17 *)
Definition f2 (i : u32) : result unit :=
- Return tt.
+ Ok tt.
(** [arrays::f4]:
Source: 'src/arrays.rs', lines 282:0-282:54 *)
@@ -483,7 +482,7 @@ Definition f3 (n : nat) : result u32 :=
(** [arrays::SZ]
Source: 'src/arrays.rs', lines 286:0-286:19 *)
-Definition sz_body : result usize := Return 32%usize.
+Definition sz_body : result usize := Ok 32%usize.
Definition sz : usize := sz_body%global.
(** [arrays::f5]:
@@ -505,7 +504,7 @@ Definition ite : result unit :=
let (_, s3) := p3 in
_ <- to_slice_mut_back1 s3;
_ <- to_slice_mut_back s1;
- Return tt
+ Ok tt
.
(** [arrays::zero_slice]: loop 0:
@@ -522,7 +521,7 @@ Fixpoint zero_slice_loop
i1 <- usize_add i 1%usize;
a1 <- index_mut_back 0%u8;
zero_slice_loop n1 a1 i1 len)
- else Return a
+ else Ok a
end
.
@@ -541,14 +540,14 @@ Fixpoint iter_mut_slice_loop
| S n1 =>
if i s< len
then (i1 <- usize_add i 1%usize; iter_mut_slice_loop n1 len i1)
- else Return tt
+ else Ok tt
end
.
(** [arrays::iter_mut_slice]:
Source: 'src/arrays.rs', lines 312:0-312:35 *)
Definition iter_mut_slice (n : nat) (a : slice u8) : result (slice u8) :=
- let len := slice_len u8 a in _ <- iter_mut_slice_loop n len 0%usize; Return a
+ let len := slice_len u8 a in _ <- iter_mut_slice_loop n len 0%usize; Ok a
.
(** [arrays::sum_mut_slice]: loop 0:
@@ -565,7 +564,7 @@ Fixpoint sum_mut_slice_loop
s1 <- u32_add s i2;
i3 <- usize_add i 1%usize;
sum_mut_slice_loop n1 a i3 s1)
- else Return s
+ else Ok s
end
.
@@ -573,7 +572,7 @@ Fixpoint sum_mut_slice_loop
Source: 'src/arrays.rs', lines 320:0-320:42 *)
Definition sum_mut_slice
(n : nat) (a : slice u32) : result (u32 * (slice u32)) :=
- i <- sum_mut_slice_loop n a 0%usize 0%u32; Return (i, a)
+ i <- sum_mut_slice_loop n a 0%usize 0%u32; Ok (i, a)
.
End Arrays.
diff --git a/tests/coq/arrays/Primitives.v b/tests/coq/arrays/Primitives.v
index 990e27e4..e84d65ce 100644
--- a/tests/coq/arrays/Primitives.v
+++ b/tests/coq/arrays/Primitives.v
@@ -19,19 +19,19 @@ Inductive error :=
| OutOfFuel.
Inductive result A :=
- | Return : A -> result A
+ | Ok : A -> result A
| Fail_ : error -> result A.
-Arguments Return {_} a.
+Arguments Ok {_} a.
Arguments Fail_ {_}.
Definition bind {A B} (m: result A) (f: A -> result B) : result B :=
match m with
| Fail_ e => Fail_ e
- | Return x => f x
+ | Ok x => f x
end.
-Definition return_ {A: Type} (x: A) : result A := Return x.
+Definition return_ {A: Type} (x: A) : result A := Ok x.
Definition fail_ {A: Type} (e: error) : result A := Fail_ e.
Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
@@ -39,27 +39,27 @@ Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
(** Monadic assert *)
Definition massert (b: bool) : result unit :=
- if b then Return tt else Fail_ Failure.
+ if b then Ok tt else Fail_ Failure.
(** Normalize and unwrap a successful result (used for globals) *)
-Definition eval_result_refl {A} {x} (a: result A) (p: a = Return x) : A :=
- match a as r return (r = Return x -> A) with
- | Return a' => fun _ => a'
+Definition eval_result_refl {A} {x} (a: result A) (p: a = Ok x) : A :=
+ match a as r return (r = Ok x -> A) with
+ | Ok a' => fun _ => a'
| Fail_ e => fun p' =>
False_rect _ (eq_ind (Fail_ e)
(fun e : result A =>
match e with
- | Return _ => False
+ | Ok _ => False
| Fail_ e => True
end)
- I (Return x) p')
+ I (Ok x) p')
end p.
Notation "x %global" := (eval_result_refl x eq_refl) (at level 40).
Notation "x %return" := (eval_result_refl x eq_refl) (at level 40).
(* Sanity check *)
-Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3.
+Check (if true then Ok (1 + 2) else Fail_ Failure)%global = 3.
(*** Misc *)
@@ -236,7 +236,7 @@ Import Sumbool.
Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) :=
match sumbool_of_bool (scalar_in_bounds ty x) with
- | left H => Return (exist _ x (scalar_in_bounds_valid _ _ H))
+ | left H => Ok (exist _ x (scalar_in_bounds_valid _ _ H))
| right _ => Fail_ Failure
end.
@@ -544,9 +544,9 @@ Arguments core_ops_range_Range_end_ {_}.
(*** [alloc] *)
-Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Return x.
+Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Ok x.
Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result (T * (T -> result T)) :=
- Return (x, fun x => Return x).
+ Ok (x, fun x => Ok x).
(* Trait instance *)
Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {|
@@ -589,7 +589,7 @@ Definition array_index_mut_usize (T : Type) (n : usize) (a : array T n) (i : usi
result (T * (T -> result (array T n))) :=
match array_index_usize T n a i with
| Fail_ e => Fail_ e
- | Return x => Return (x, array_update_usize T n a i)
+ | Ok x => Ok (x, array_update_usize T n a i)
end.
(*** Slice *)
@@ -603,7 +603,7 @@ Definition slice_index_mut_usize (T : Type) (s : slice T) (i : usize) :
result (T * (T -> result (slice T))) :=
match slice_index_usize T s i with
| Fail_ e => Fail_ e
- | Return x => Return (x, slice_update_usize T s i)
+ | Ok x => Ok (x, slice_update_usize T s i)
end.
(*** Subslices *)
@@ -615,7 +615,7 @@ Definition array_to_slice_mut (T : Type) (n : usize) (a : array T n) :
result (slice T * (slice T -> result (array T n))) :=
match array_to_slice T n a with
| Fail_ e => Fail_ e
- | Return x => Return (x, array_from_slice T n a)
+ | Ok x => Ok (x, array_from_slice T n a)
end.
Axiom array_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize), result (slice T).
@@ -657,17 +657,17 @@ end end.
Definition alloc_vec_Vec_bind {A B} (v: alloc_vec_Vec A) (f: list A -> result (list B)) : result (alloc_vec_Vec B) :=
l <- f (alloc_vec_Vec_to_list v) ;
match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with
- | left H => Return (exist _ l (scalar_le_max_valid _ _ H))
+ | left H => Ok (exist _ l (scalar_le_max_valid _ _ H))
| right _ => Fail_ Failure
end.
Definition alloc_vec_Vec_push (T: Type) (v: alloc_vec_Vec T) (x: T) : result (alloc_vec_Vec T) :=
- alloc_vec_Vec_bind v (fun l => Return (l ++ [x])).
+ alloc_vec_Vec_bind v (fun l => Ok (l ++ [x])).
Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result (alloc_vec_Vec T) :=
alloc_vec_Vec_bind v (fun l =>
if to_Z i <? Z.of_nat (length l)
- then Return (list_update l (usize_to_nat i) x)
+ then Ok (list_update l (usize_to_nat i) x)
else Fail_ Failure).
(* Helper *)
@@ -679,8 +679,8 @@ Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i :
Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usize) :
result (T * (T -> result (alloc_vec_Vec T))) :=
match alloc_vec_Vec_index_usize v i with
- | Return x =>
- Return (x, alloc_vec_Vec_update_usize v i)
+ | Ok x =>
+ Ok (x, alloc_vec_Vec_update_usize v i)
| Fail_ e => Fail_ e
end.
@@ -717,7 +717,7 @@ Definition core_slice_index_Slice_index
x <- inst.(core_slice_index_SliceIndex_get) i s;
match x with
| None => Fail_ Failure
- | Some x => Return x
+ | Some x => Ok x
end.
(* [core::slice::index::Range:::get]: forward function *)
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 9256b149..80518eab 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -49,13 +49,13 @@ Definition betree_store_leaf_node
(** [betree_main::betree::fresh_node_id]:
Source: 'src/betree.rs', lines 55:0-55:48 *)
Definition betree_fresh_node_id (counter : u64) : result (u64 * u64) :=
- counter1 <- u64_add counter 1%u64; Return (counter, counter1)
+ counter1 <- u64_add counter 1%u64; Ok (counter, counter1)
.
(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]:
Source: 'src/betree.rs', lines 206:4-206:20 *)
Definition betree_NodeIdCounter_new : result betree_NodeIdCounter_t :=
- Return {| betree_NodeIdCounter_next_node_id := 0%u64 |}
+ Ok {| betree_NodeIdCounter_next_node_id := 0%u64 |}
.
(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]:
@@ -63,7 +63,7 @@ Definition betree_NodeIdCounter_new : result betree_NodeIdCounter_t :=
Definition betree_NodeIdCounter_fresh_id
(self : betree_NodeIdCounter_t) : result (u64 * betree_NodeIdCounter_t) :=
i <- u64_add self.(betree_NodeIdCounter_next_node_id) 1%u64;
- Return (self.(betree_NodeIdCounter_next_node_id),
+ Ok (self.(betree_NodeIdCounter_next_node_id),
{| betree_NodeIdCounter_next_node_id := i |})
.
@@ -74,16 +74,16 @@ Definition betree_upsert_update
match prev with
| None =>
match st with
- | Betree_UpsertFunState_Add v => Return v
- | Betree_UpsertFunState_Sub _ => Return 0%u64
+ | Betree_UpsertFunState_Add v => Ok v
+ | Betree_UpsertFunState_Sub _ => Ok 0%u64
end
| Some prev1 =>
match st with
| Betree_UpsertFunState_Add v =>
margin <- u64_sub core_u64_max prev1;
- if margin s>= v then u64_add prev1 v else Return core_u64_max
+ if margin s>= v then u64_add prev1 v else Ok core_u64_max
| Betree_UpsertFunState_Sub v =>
- if prev1 s>= v then u64_sub prev1 v else Return 0%u64
+ if prev1 s>= v then u64_sub prev1 v else Ok 0%u64
end
end
.
@@ -97,7 +97,7 @@ Fixpoint betree_List_len
| S n1 =>
match self with
| Betree_List_Cons _ tl => i <- betree_List_len T n1 tl; u64_add 1%u64 i
- | Betree_List_Nil => Return 0%u64
+ | Betree_List_Nil => Ok 0%u64
end
end
.
@@ -112,14 +112,14 @@ Fixpoint betree_List_split_at
| O => Fail_ OutOfFuel
| S n2 =>
if n1 s= 0%u64
- then Return (Betree_List_Nil, self)
+ then Ok (Betree_List_Nil, self)
else
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
- Return (Betree_List_Cons hd ls0, ls1)
+ Ok (Betree_List_Cons hd ls0, ls1)
| Betree_List_Nil => Fail_ Failure
end
end
@@ -130,7 +130,7 @@ Fixpoint betree_List_split_at
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
- Return (Betree_List_Cons x tl)
+ Ok (Betree_List_Cons x tl)
.
(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]:
@@ -139,7 +139,7 @@ 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
match ls with
- | Betree_List_Cons x tl => Return (x, tl)
+ | Betree_List_Cons x tl => Ok (x, tl)
| Betree_List_Nil => Fail_ Failure
end
.
@@ -148,7 +148,7 @@ Definition betree_List_pop_front
Source: 'src/betree.rs', lines 318:4-318:22 *)
Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T :=
match self with
- | Betree_List_Cons hd _ => Return hd
+ | Betree_List_Cons hd _ => Ok hd
| Betree_List_Nil => Fail_ Failure
end
.
@@ -158,8 +158,8 @@ Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T :=
Definition betree_ListPairU64T_head_has_key
(T : Type) (self : betree_List_t (u64 * T)) (key : u64) : result bool :=
match self with
- | Betree_List_Cons hd _ => let (i, _) := hd in Return (i s= key)
- | Betree_List_Nil => Return false
+ | Betree_List_Cons hd _ => let (i, _) := hd in Ok (i s= key)
+ | Betree_List_Nil => Ok false
end
.
@@ -176,12 +176,12 @@ Fixpoint betree_ListPairU64T_partition_at_pivot
| Betree_List_Cons hd tl =>
let (i, t) := hd in
if i s>= pivot
- then Return (Betree_List_Nil, Betree_List_Cons (i, t) tl)
+ 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
- Return (Betree_List_Cons (i, t) ls0, ls1))
- | Betree_List_Nil => Return (Betree_List_Nil, Betree_List_Nil)
+ Ok (Betree_List_Cons (i, t) ls0, ls1))
+ | Betree_List_Nil => Ok (Betree_List_Nil, Betree_List_Nil)
end
end
.
@@ -218,7 +218,7 @@ Definition betree_Leaf_split
betree_Leaf_id := id1;
betree_Leaf_size := params.(betree_Params_split_size)
|} in
- Return (st2, (mkbetree_Internal_t self.(betree_Leaf_id) pivot n1 n2,
+ Ok (st2, (mkbetree_Internal_t self.(betree_Leaf_id) pivot n1 n2,
node_id_cnt2))
.
@@ -236,16 +236,16 @@ Fixpoint betree_Node_lookup_first_message_for_key
| Betree_List_Cons x next_msgs =>
let (i, m) := x in
if i s>= key
- then Return (Betree_List_Cons (i, m) next_msgs, Return)
+ 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 :=
fun (ret : betree_List_t (u64 * betree_Message_t)) =>
next_msgs1 <- lookup_first_message_for_key_back ret;
- Return (Betree_List_Cons (i, m) next_msgs1) in
- Return (l, back))
- | Betree_List_Nil => Return (Betree_List_Nil, Return)
+ Ok (Betree_List_Cons (i, m) next_msgs1) in
+ Ok (l, back))
+ | Betree_List_Nil => Ok (Betree_List_Nil, Ok)
end
end
.
@@ -263,12 +263,10 @@ Fixpoint betree_Node_lookup_in_bindings
| Betree_List_Cons hd tl =>
let (i, i1) := hd in
if i s= key
- then Return (Some i1)
+ then Ok (Some i1)
else
- if i s> key
- then Return None
- else betree_Node_lookup_in_bindings n1 key tl
- | Betree_List_Nil => Return None
+ if i s> key then Ok None else betree_Node_lookup_in_bindings n1 key tl
+ | Betree_List_Nil => Ok None
end
end
.
@@ -302,7 +300,7 @@ Fixpoint betree_Node_apply_upserts
msgs1 <-
betree_List_push_front (u64 * betree_Message_t) msgs (key,
Betree_Message_Insert v);
- Return (st1, (v, msgs1)))
+ Ok (st1, (v, msgs1)))
end
.
@@ -320,13 +318,13 @@ Fixpoint betree_Internal_lookup_in_children
p <- betree_Node_lookup n1 self.(betree_Internal_left) key st;
let (st1, p1) := p in
let (o, n2) := p1 in
- Return (st1, (o, mkbetree_Internal_t self.(betree_Internal_id)
+ Ok (st1, (o, mkbetree_Internal_t self.(betree_Internal_id)
self.(betree_Internal_pivot) n2 self.(betree_Internal_right))))
else (
p <- betree_Node_lookup n1 self.(betree_Internal_right) key st;
let (st1, p1) := p in
let (o, n2) := p1 in
- Return (st1, (o, mkbetree_Internal_t self.(betree_Internal_id)
+ Ok (st1, (o, mkbetree_Internal_t self.(betree_Internal_id)
self.(betree_Internal_pivot) self.(betree_Internal_left) n2)))
end
@@ -354,19 +352,19 @@ with betree_Node_lookup
let (st2, p4) := p3 in
let (o, node1) := p4 in
_ <- lookup_first_message_for_key_back (Betree_List_Cons (k, msg) l);
- Return (st2, (o, Betree_Node_Internal node1)))
+ Ok (st2, (o, Betree_Node_Internal node1)))
else
match msg with
| Betree_Message_Insert v =>
_ <-
lookup_first_message_for_key_back (Betree_List_Cons (k,
Betree_Message_Insert v) l);
- Return (st1, (Some v, Betree_Node_Internal node))
+ Ok (st1, (Some v, Betree_Node_Internal node))
| Betree_Message_Delete =>
_ <-
lookup_first_message_for_key_back (Betree_List_Cons (k,
Betree_Message_Delete) l);
- Return (st1, (None, Betree_Node_Internal node))
+ Ok (st1, (None, Betree_Node_Internal node))
| Betree_Message_Upsert ufs =>
p3 <- betree_Internal_lookup_in_children n1 node key st1;
let (st2, p4) := p3 in
@@ -380,20 +378,20 @@ with betree_Node_lookup
p7 <-
betree_store_internal_node node1.(betree_Internal_id) msgs1 st3;
let (st4, _) := p7 in
- Return (st4, (Some v1, Betree_Node_Internal node1))
+ Ok (st4, (Some v1, Betree_Node_Internal node1))
end
| Betree_List_Nil =>
p2 <- betree_Internal_lookup_in_children n1 node key st1;
let (st2, p3) := p2 in
let (o, node1) := p3 in
_ <- lookup_first_message_for_key_back Betree_List_Nil;
- Return (st2, (o, Betree_Node_Internal node1))
+ Ok (st2, (o, Betree_Node_Internal node1))
end
| Betree_Node_Leaf node =>
p <- betree_load_leaf_node node.(betree_Leaf_id) st;
let (st1, bindings) := p in
o <- betree_Node_lookup_in_bindings n1 key bindings;
- Return (st1, (o, Betree_Node_Leaf node))
+ Ok (st1, (o, Betree_Node_Leaf node))
end
end
.
@@ -417,8 +415,8 @@ Fixpoint betree_Node_filter_messages_for_key
m) l);
let (_, msgs1) := p1 in
betree_Node_filter_messages_for_key n1 key msgs1)
- else Return (Betree_List_Cons (k, m) l)
- | Betree_List_Nil => Return Betree_List_Nil
+ else Ok (Betree_List_Cons (k, m) l)
+ | Betree_List_Nil => Ok Betree_List_Nil
end
end
.
@@ -443,10 +441,10 @@ Fixpoint betree_Node_lookup_first_message_after_key
let back :=
fun (ret : betree_List_t (u64 * betree_Message_t)) =>
next_msgs1 <- lookup_first_message_after_key_back ret;
- Return (Betree_List_Cons (k, m) next_msgs1) in
- Return (l, back))
- else Return (Betree_List_Cons (k, m) next_msgs, Return)
- | Betree_List_Nil => Return (Betree_List_Nil, Return)
+ Ok (Betree_List_Cons (k, m) next_msgs1) in
+ Ok (l, back))
+ else Ok (Betree_List_Cons (k, m) next_msgs, Ok)
+ | Betree_List_Nil => Ok (Betree_List_Nil, Ok)
end
end
.
@@ -527,7 +525,7 @@ Fixpoint betree_Node_apply_messages_to_internal
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_List_Nil => Return msgs
+ | Betree_List_Nil => Ok msgs
end
end
.
@@ -546,16 +544,16 @@ Fixpoint betree_Node_lookup_mut_in_bindings
| Betree_List_Cons hd tl =>
let (i, i1) := hd in
if i s>= key
- then Return (Betree_List_Cons (i, i1) tl, Return)
+ 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 :=
fun (ret : betree_List_t (u64 * u64)) =>
tl1 <- lookup_mut_in_bindings_back ret;
- Return (Betree_List_Cons (i, i1) tl1) in
- Return (l, back))
- | Betree_List_Nil => Return (Betree_List_Nil, Return)
+ Ok (Betree_List_Cons (i, i1) tl1) in
+ Ok (l, back))
+ | Betree_List_Nil => Ok (Betree_List_Nil, Ok)
end
end
.
@@ -613,7 +611,7 @@ Fixpoint betree_Node_apply_messages_to_leaf
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_List_Nil => Return bindings
+ | Betree_List_Nil => Ok bindings
end
end
.
@@ -650,20 +648,20 @@ Fixpoint betree_Internal_flush
node_id_cnt1 msgs_right st1;
let (st2, p4) := p3 in
let (n3, node_id_cnt2) := p4 in
- Return (st2, (Betree_List_Nil, (mkbetree_Internal_t
+ Ok (st2, (Betree_List_Nil, (mkbetree_Internal_t
self.(betree_Internal_id) self.(betree_Internal_pivot) n2 n3,
node_id_cnt2))))
else
- Return (st1, (msgs_right, (mkbetree_Internal_t
- self.(betree_Internal_id) self.(betree_Internal_pivot) n2
- self.(betree_Internal_right), node_id_cnt1))))
+ Ok (st1, (msgs_right, (mkbetree_Internal_t self.(betree_Internal_id)
+ self.(betree_Internal_pivot) n2 self.(betree_Internal_right),
+ node_id_cnt1))))
else (
p1 <-
betree_Node_apply_messages n1 self.(betree_Internal_right) params
node_id_cnt msgs_right st;
let (st1, p2) := p1 in
let (n2, node_id_cnt1) := p2 in
- Return (st1, (msgs_left, (mkbetree_Internal_t self.(betree_Internal_id)
+ Ok (st1, (msgs_left, (mkbetree_Internal_t self.(betree_Internal_id)
self.(betree_Internal_pivot) self.(betree_Internal_left) n2,
node_id_cnt1))))
end
@@ -694,12 +692,12 @@ with betree_Node_apply_messages
p4 <-
betree_store_internal_node node1.(betree_Internal_id) content2 st2;
let (st3, _) := p4 in
- Return (st3, (Betree_Node_Internal node1, node_id_cnt1)))
+ Ok (st3, (Betree_Node_Internal node1, node_id_cnt1)))
else (
p1 <-
betree_store_internal_node node.(betree_Internal_id) content1 st1;
let (st2, _) := p1 in
- Return (st2, (Betree_Node_Internal node, node_id_cnt)))
+ Ok (st2, (Betree_Node_Internal node, node_id_cnt)))
| Betree_Node_Leaf node =>
p <- betree_load_leaf_node node.(betree_Leaf_id) st;
let (st1, content) := p in
@@ -713,11 +711,11 @@ with betree_Node_apply_messages
let (new_node, node_id_cnt1) := p2 in
p3 <- betree_store_leaf_node node.(betree_Leaf_id) Betree_List_Nil st2;
let (st3, _) := p3 in
- Return (st3, (Betree_Node_Internal new_node, node_id_cnt1)))
+ Ok (st3, (Betree_Node_Internal new_node, node_id_cnt1)))
else (
p1 <- betree_store_leaf_node node.(betree_Leaf_id) content1 st1;
let (st2, _) := p1 in
- Return (st2, (Betree_Node_Leaf
+ Ok (st2, (Betree_Node_Leaf
{| betree_Leaf_id := node.(betree_Leaf_id); betree_Leaf_size := len
|}, node_id_cnt)))
end
@@ -737,7 +735,7 @@ Definition betree_Node_apply
(key, new_msg) Betree_List_Nil) st;
let (st1, p1) := p in
let (self1, node_id_cnt1) := p1 in
- Return (st1, (self1, node_id_cnt1))
+ Ok (st1, (self1, node_id_cnt1))
.
(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]:
@@ -751,7 +749,7 @@ Definition betree_BeTree_new
let (id, node_id_cnt1) := p in
p1 <- betree_store_leaf_node id Betree_List_Nil st;
let (st1, _) := p1 in
- Return (st1,
+ Ok (st1,
{|
betree_BeTree_params :=
{|
@@ -777,7 +775,7 @@ Definition betree_BeTree_apply
self.(betree_BeTree_node_id_cnt) key msg st;
let (st1, p1) := p in
let (n1, nic) := p1 in
- Return (st1,
+ Ok (st1,
{|
betree_BeTree_params := self.(betree_BeTree_params);
betree_BeTree_node_id_cnt := nic;
@@ -822,7 +820,7 @@ Definition betree_BeTree_lookup
p <- betree_Node_lookup n self.(betree_BeTree_root) key st;
let (st1, p1) := p in
let (o, n1) := p1 in
- Return (st1, (o,
+ Ok (st1, (o,
{|
betree_BeTree_params := self.(betree_BeTree_params);
betree_BeTree_node_id_cnt := self.(betree_BeTree_node_id_cnt);
@@ -833,7 +831,7 @@ Definition betree_BeTree_lookup
(** [betree_main::main]:
Source: 'src/betree_main.rs', lines 5:0-5:9 *)
Definition main : result unit :=
- Return tt.
+ Ok tt.
(** Unit test for [betree_main::main] *)
Check (main )%return.
diff --git a/tests/coq/betree/Primitives.v b/tests/coq/betree/Primitives.v
index 990e27e4..e84d65ce 100644
--- a/tests/coq/betree/Primitives.v
+++ b/tests/coq/betree/Primitives.v
@@ -19,19 +19,19 @@ Inductive error :=
| OutOfFuel.
Inductive result A :=
- | Return : A -> result A
+ | Ok : A -> result A
| Fail_ : error -> result A.
-Arguments Return {_} a.
+Arguments Ok {_} a.
Arguments Fail_ {_}.
Definition bind {A B} (m: result A) (f: A -> result B) : result B :=
match m with
| Fail_ e => Fail_ e
- | Return x => f x
+ | Ok x => f x
end.
-Definition return_ {A: Type} (x: A) : result A := Return x.
+Definition return_ {A: Type} (x: A) : result A := Ok x.
Definition fail_ {A: Type} (e: error) : result A := Fail_ e.
Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
@@ -39,27 +39,27 @@ Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
(** Monadic assert *)
Definition massert (b: bool) : result unit :=
- if b then Return tt else Fail_ Failure.
+ if b then Ok tt else Fail_ Failure.
(** Normalize and unwrap a successful result (used for globals) *)
-Definition eval_result_refl {A} {x} (a: result A) (p: a = Return x) : A :=
- match a as r return (r = Return x -> A) with
- | Return a' => fun _ => a'
+Definition eval_result_refl {A} {x} (a: result A) (p: a = Ok x) : A :=
+ match a as r return (r = Ok x -> A) with
+ | Ok a' => fun _ => a'
| Fail_ e => fun p' =>
False_rect _ (eq_ind (Fail_ e)
(fun e : result A =>
match e with
- | Return _ => False
+ | Ok _ => False
| Fail_ e => True
end)
- I (Return x) p')
+ I (Ok x) p')
end p.
Notation "x %global" := (eval_result_refl x eq_refl) (at level 40).
Notation "x %return" := (eval_result_refl x eq_refl) (at level 40).
(* Sanity check *)
-Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3.
+Check (if true then Ok (1 + 2) else Fail_ Failure)%global = 3.
(*** Misc *)
@@ -236,7 +236,7 @@ Import Sumbool.
Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) :=
match sumbool_of_bool (scalar_in_bounds ty x) with
- | left H => Return (exist _ x (scalar_in_bounds_valid _ _ H))
+ | left H => Ok (exist _ x (scalar_in_bounds_valid _ _ H))
| right _ => Fail_ Failure
end.
@@ -544,9 +544,9 @@ Arguments core_ops_range_Range_end_ {_}.
(*** [alloc] *)
-Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Return x.
+Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Ok x.
Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result (T * (T -> result T)) :=
- Return (x, fun x => Return x).
+ Ok (x, fun x => Ok x).
(* Trait instance *)
Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {|
@@ -589,7 +589,7 @@ Definition array_index_mut_usize (T : Type) (n : usize) (a : array T n) (i : usi
result (T * (T -> result (array T n))) :=
match array_index_usize T n a i with
| Fail_ e => Fail_ e
- | Return x => Return (x, array_update_usize T n a i)
+ | Ok x => Ok (x, array_update_usize T n a i)
end.
(*** Slice *)
@@ -603,7 +603,7 @@ Definition slice_index_mut_usize (T : Type) (s : slice T) (i : usize) :
result (T * (T -> result (slice T))) :=
match slice_index_usize T s i with
| Fail_ e => Fail_ e
- | Return x => Return (x, slice_update_usize T s i)
+ | Ok x => Ok (x, slice_update_usize T s i)
end.
(*** Subslices *)
@@ -615,7 +615,7 @@ Definition array_to_slice_mut (T : Type) (n : usize) (a : array T n) :
result (slice T * (slice T -> result (array T n))) :=
match array_to_slice T n a with
| Fail_ e => Fail_ e
- | Return x => Return (x, array_from_slice T n a)
+ | Ok x => Ok (x, array_from_slice T n a)
end.
Axiom array_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize), result (slice T).
@@ -657,17 +657,17 @@ end end.
Definition alloc_vec_Vec_bind {A B} (v: alloc_vec_Vec A) (f: list A -> result (list B)) : result (alloc_vec_Vec B) :=
l <- f (alloc_vec_Vec_to_list v) ;
match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with
- | left H => Return (exist _ l (scalar_le_max_valid _ _ H))
+ | left H => Ok (exist _ l (scalar_le_max_valid _ _ H))
| right _ => Fail_ Failure
end.
Definition alloc_vec_Vec_push (T: Type) (v: alloc_vec_Vec T) (x: T) : result (alloc_vec_Vec T) :=
- alloc_vec_Vec_bind v (fun l => Return (l ++ [x])).
+ alloc_vec_Vec_bind v (fun l => Ok (l ++ [x])).
Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result (alloc_vec_Vec T) :=
alloc_vec_Vec_bind v (fun l =>
if to_Z i <? Z.of_nat (length l)
- then Return (list_update l (usize_to_nat i) x)
+ then Ok (list_update l (usize_to_nat i) x)
else Fail_ Failure).
(* Helper *)
@@ -679,8 +679,8 @@ Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i :
Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usize) :
result (T * (T -> result (alloc_vec_Vec T))) :=
match alloc_vec_Vec_index_usize v i with
- | Return x =>
- Return (x, alloc_vec_Vec_update_usize v i)
+ | Ok x =>
+ Ok (x, alloc_vec_Vec_update_usize v i)
| Fail_ e => Fail_ e
end.
@@ -717,7 +717,7 @@ Definition core_slice_index_Slice_index
x <- inst.(core_slice_index_SliceIndex_get) i s;
match x with
| None => Fail_ Failure
- | Some x => Return x
+ | Some x => Ok x
end.
(* [core::slice::index::Range:::get]: forward function *)
diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index abec8e88..00b9b889 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -13,8 +13,8 @@ Module Demo.
Definition choose
(T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) :=
if b
- then let back := fun (ret : T) => Return (ret, y) in Return (x, back)
- else let back := fun (ret : T) => Return (x, ret) in Return (y, back)
+ then let back := fun (ret : T) => Ok (ret, y) in Ok (x, back)
+ else let back := fun (ret : T) => Ok (x, ret) in Ok (y, back)
.
(** [demo::mul2_add1]:
@@ -37,7 +37,7 @@ Definition incr (x : u32) : result u32 :=
(** [demo::use_incr]:
Source: 'src/demo.rs', lines 25:0-25:17 *)
Definition use_incr : result unit :=
- x <- incr 0%u32; x1 <- incr x; _ <- incr x1; Return tt
+ x <- incr 0%u32; x1 <- incr x; _ <- incr x1; Ok tt
.
(** [demo::CList]
@@ -58,9 +58,7 @@ Fixpoint list_nth (T : Type) (n : nat) (l : CList_t T) (i : u32) : result T :=
| S n1 =>
match l with
| CList_CCons x tl =>
- if i s= 0%u32
- then Return x
- else (i1 <- u32_sub i 1%u32; list_nth T n1 tl i1)
+ if i s= 0%u32 then Ok x else (i1 <- u32_sub i 1%u32; list_nth T n1 tl i1)
| CList_CNil => Fail_ Failure
end
end
@@ -78,17 +76,15 @@ Fixpoint list_nth_mut
match l with
| CList_CCons x tl =>
if i s= 0%u32
- then
- let back := fun (ret : T) => Return (CList_CCons ret tl) in
- Return (x, back)
+ then let back := fun (ret : T) => Ok (CList_CCons ret tl) in Ok (x, back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_mut T n1 tl i1;
let (t, list_nth_mut_back) := p in
let back :=
- fun (ret : T) =>
- tl1 <- list_nth_mut_back ret; Return (CList_CCons x tl1) in
- Return (t, back))
+ fun (ret : T) => tl1 <- list_nth_mut_back ret; Ok (CList_CCons x tl1)
+ in
+ Ok (t, back))
| CList_CNil => Fail_ Failure
end
end
@@ -106,16 +102,14 @@ Fixpoint list_nth_mut1_loop
match l with
| CList_CCons x tl =>
if i s= 0%u32
- then
- let back := fun (ret : T) => Return (CList_CCons ret tl) in
- Return (x, back)
+ then let back := fun (ret : T) => Ok (CList_CCons ret tl) in Ok (x, back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_mut1_loop T n1 tl i1;
let (t, back) := p in
- let back1 :=
- fun (ret : T) => tl1 <- back ret; Return (CList_CCons x tl1) in
- Return (t, back1))
+ let back1 := fun (ret : T) => tl1 <- back ret; Ok (CList_CCons x tl1)
+ in
+ Ok (t, back1))
| CList_CNil => Fail_ Failure
end
end
@@ -137,7 +131,7 @@ Fixpoint i32_id (n : nat) (i : i32) : result i32 :=
| O => Fail_ OutOfFuel
| S n1 =>
if i s= 0%i32
- then Return 0%i32
+ then Ok 0%i32
else (i1 <- i32_sub i 1%i32; i2 <- i32_id n1 i1; i32_add i2 1%i32)
end
.
@@ -157,9 +151,9 @@ Fixpoint list_tail
let (c, list_tail_back) := p in
let back :=
fun (ret : CList_t T) =>
- tl1 <- list_tail_back ret; Return (CList_CCons t tl1) in
- Return (c, back)
- | CList_CNil => Return (CList_CNil, Return)
+ tl1 <- list_tail_back ret; Ok (CList_CCons t tl1) in
+ Ok (c, back)
+ | CList_CNil => Ok (CList_CNil, Ok)
end
end
.
@@ -176,7 +170,7 @@ Arguments Counter_t_incr { _ }.
(** [demo::{(demo::Counter for usize)}::incr]:
Source: 'src/demo.rs', lines 102:4-102:31 *)
Definition counterUsize_incr (self : usize) : result (usize * usize) :=
- self1 <- usize_add self 1%usize; Return (self, self1)
+ self1 <- usize_add self 1%usize; Ok (self, self1)
.
(** Trait implementation: [demo::{(demo::Counter for usize)}]
diff --git a/tests/coq/demo/Primitives.v b/tests/coq/demo/Primitives.v
index 990e27e4..e84d65ce 100644
--- a/tests/coq/demo/Primitives.v
+++ b/tests/coq/demo/Primitives.v
@@ -19,19 +19,19 @@ Inductive error :=
| OutOfFuel.
Inductive result A :=
- | Return : A -> result A
+ | Ok : A -> result A
| Fail_ : error -> result A.
-Arguments Return {_} a.
+Arguments Ok {_} a.
Arguments Fail_ {_}.
Definition bind {A B} (m: result A) (f: A -> result B) : result B :=
match m with
| Fail_ e => Fail_ e
- | Return x => f x
+ | Ok x => f x
end.
-Definition return_ {A: Type} (x: A) : result A := Return x.
+Definition return_ {A: Type} (x: A) : result A := Ok x.
Definition fail_ {A: Type} (e: error) : result A := Fail_ e.
Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
@@ -39,27 +39,27 @@ Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
(** Monadic assert *)
Definition massert (b: bool) : result unit :=
- if b then Return tt else Fail_ Failure.
+ if b then Ok tt else Fail_ Failure.
(** Normalize and unwrap a successful result (used for globals) *)
-Definition eval_result_refl {A} {x} (a: result A) (p: a = Return x) : A :=
- match a as r return (r = Return x -> A) with
- | Return a' => fun _ => a'
+Definition eval_result_refl {A} {x} (a: result A) (p: a = Ok x) : A :=
+ match a as r return (r = Ok x -> A) with
+ | Ok a' => fun _ => a'
| Fail_ e => fun p' =>
False_rect _ (eq_ind (Fail_ e)
(fun e : result A =>
match e with
- | Return _ => False
+ | Ok _ => False
| Fail_ e => True
end)
- I (Return x) p')
+ I (Ok x) p')
end p.
Notation "x %global" := (eval_result_refl x eq_refl) (at level 40).
Notation "x %return" := (eval_result_refl x eq_refl) (at level 40).
(* Sanity check *)
-Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3.
+Check (if true then Ok (1 + 2) else Fail_ Failure)%global = 3.
(*** Misc *)
@@ -236,7 +236,7 @@ Import Sumbool.
Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) :=
match sumbool_of_bool (scalar_in_bounds ty x) with
- | left H => Return (exist _ x (scalar_in_bounds_valid _ _ H))
+ | left H => Ok (exist _ x (scalar_in_bounds_valid _ _ H))
| right _ => Fail_ Failure
end.
@@ -544,9 +544,9 @@ Arguments core_ops_range_Range_end_ {_}.
(*** [alloc] *)
-Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Return x.
+Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Ok x.
Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result (T * (T -> result T)) :=
- Return (x, fun x => Return x).
+ Ok (x, fun x => Ok x).
(* Trait instance *)
Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {|
@@ -589,7 +589,7 @@ Definition array_index_mut_usize (T : Type) (n : usize) (a : array T n) (i : usi
result (T * (T -> result (array T n))) :=
match array_index_usize T n a i with
| Fail_ e => Fail_ e
- | Return x => Return (x, array_update_usize T n a i)
+ | Ok x => Ok (x, array_update_usize T n a i)
end.
(*** Slice *)
@@ -603,7 +603,7 @@ Definition slice_index_mut_usize (T : Type) (s : slice T) (i : usize) :
result (T * (T -> result (slice T))) :=
match slice_index_usize T s i with
| Fail_ e => Fail_ e
- | Return x => Return (x, slice_update_usize T s i)
+ | Ok x => Ok (x, slice_update_usize T s i)
end.
(*** Subslices *)
@@ -615,7 +615,7 @@ Definition array_to_slice_mut (T : Type) (n : usize) (a : array T n) :
result (slice T * (slice T -> result (array T n))) :=
match array_to_slice T n a with
| Fail_ e => Fail_ e
- | Return x => Return (x, array_from_slice T n a)
+ | Ok x => Ok (x, array_from_slice T n a)
end.
Axiom array_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize), result (slice T).
@@ -657,17 +657,17 @@ end end.
Definition alloc_vec_Vec_bind {A B} (v: alloc_vec_Vec A) (f: list A -> result (list B)) : result (alloc_vec_Vec B) :=
l <- f (alloc_vec_Vec_to_list v) ;
match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with
- | left H => Return (exist _ l (scalar_le_max_valid _ _ H))
+ | left H => Ok (exist _ l (scalar_le_max_valid _ _ H))
| right _ => Fail_ Failure
end.
Definition alloc_vec_Vec_push (T: Type) (v: alloc_vec_Vec T) (x: T) : result (alloc_vec_Vec T) :=
- alloc_vec_Vec_bind v (fun l => Return (l ++ [x])).
+ alloc_vec_Vec_bind v (fun l => Ok (l ++ [x])).
Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result (alloc_vec_Vec T) :=
alloc_vec_Vec_bind v (fun l =>
if to_Z i <? Z.of_nat (length l)
- then Return (list_update l (usize_to_nat i) x)
+ then Ok (list_update l (usize_to_nat i) x)
else Fail_ Failure).
(* Helper *)
@@ -679,8 +679,8 @@ Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i :
Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usize) :
result (T * (T -> result (alloc_vec_Vec T))) :=
match alloc_vec_Vec_index_usize v i with
- | Return x =>
- Return (x, alloc_vec_Vec_update_usize v i)
+ | Ok x =>
+ Ok (x, alloc_vec_Vec_update_usize v i)
| Fail_ e => Fail_ e
end.
@@ -717,7 +717,7 @@ Definition core_slice_index_Slice_index
x <- inst.(core_slice_index_SliceIndex_get) i s;
match x with
| None => Fail_ Failure
- | Some x => Return x
+ | Some x => Ok x
end.
(* [core::slice::index::Range:::get]: forward function *)
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index c0cde78d..ebb7897d 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -13,7 +13,7 @@ Module Hashmap_Funs.
(** [hashmap::hash_key]:
Source: 'src/hashmap.rs', lines 27:0-27:32 *)
Definition hash_key (k : usize) : result usize :=
- Return k.
+ Ok k.
(** [hashmap::{hashmap::HashMap<T>}::allocate_slots]: loop 0:
Source: 'src/hashmap.rs', lines 50:4-56:5 *)
@@ -29,7 +29,7 @@ Fixpoint hashMap_allocate_slots_loop
slots1 <- alloc_vec_Vec_push (List_t T) slots List_Nil;
n3 <- usize_sub n1 1%usize;
hashMap_allocate_slots_loop T n2 slots1 n3)
- else Return slots
+ else Ok slots
end
.
@@ -52,7 +52,7 @@ Definition hashMap_new_with_capacity
slots <- hashMap_allocate_slots T n (alloc_vec_Vec_new (List_t T)) capacity;
i <- usize_mul capacity max_load_dividend;
i1 <- usize_div i max_load_divisor;
- Return
+ Ok
{|
hashMap_num_entries := 0%usize;
hashMap_max_load_factor := (max_load_dividend, max_load_divisor);
@@ -86,7 +86,7 @@ Fixpoint hashMap_clear_loop
i2 <- usize_add i 1%usize;
slots1 <- index_mut_back List_Nil;
hashMap_clear_loop T n1 slots1 i2)
- else Return slots
+ else Ok slots
end
.
@@ -95,7 +95,7 @@ Fixpoint hashMap_clear_loop
Definition hashMap_clear
(T : Type) (n : nat) (self : HashMap_t T) : result (HashMap_t T) :=
hm <- hashMap_clear_loop T n self.(hashMap_slots) 0%usize;
- Return
+ Ok
{|
hashMap_num_entries := 0%usize;
hashMap_max_load_factor := self.(hashMap_max_load_factor);
@@ -107,7 +107,7 @@ Definition hashMap_clear
(** [hashmap::{hashmap::HashMap<T>}::len]:
Source: 'src/hashmap.rs', lines 90:4-90:30 *)
Definition hashMap_len (T : Type) (self : HashMap_t T) : result usize :=
- Return self.(hashMap_num_entries)
+ Ok self.(hashMap_num_entries)
.
(** [hashmap::{hashmap::HashMap<T>}::insert_in_list]: loop 0:
@@ -122,12 +122,12 @@ Fixpoint hashMap_insert_in_list_loop
match ls with
| List_Cons ckey cvalue tl =>
if ckey s= key
- then Return (false, List_Cons ckey value tl)
+ then Ok (false, List_Cons ckey value tl)
else (
p <- hashMap_insert_in_list_loop T n1 key value tl;
let (b, tl1) := p in
- Return (b, List_Cons ckey cvalue tl1))
- | List_Nil => Return (true, List_Cons key value List_Nil)
+ Ok (b, List_Cons ckey cvalue tl1))
+ | List_Nil => Ok (true, List_Cons key value List_Nil)
end
end
.
@@ -161,7 +161,7 @@ Definition hashMap_insert_no_resize
then (
i1 <- usize_add self.(hashMap_num_entries) 1%usize;
v <- index_mut_back l1;
- Return
+ Ok
{|
hashMap_num_entries := i1;
hashMap_max_load_factor := self.(hashMap_max_load_factor);
@@ -170,7 +170,7 @@ Definition hashMap_insert_no_resize
|})
else (
v <- index_mut_back l1;
- Return
+ Ok
{|
hashMap_num_entries := self.(hashMap_num_entries);
hashMap_max_load_factor := self.(hashMap_max_load_factor);
@@ -192,7 +192,7 @@ Fixpoint hashMap_move_elements_from_list_loop
| List_Cons k v tl =>
ntable1 <- hashMap_insert_no_resize T n1 ntable k v;
hashMap_move_elements_from_list_loop T n1 ntable1 tl
- | List_Nil => Return ntable
+ | List_Nil => Ok ntable
end
end
.
@@ -228,7 +228,7 @@ Fixpoint hashMap_move_elements_loop
i2 <- usize_add i 1%usize;
slots1 <- index_mut_back l1;
hashMap_move_elements_loop T n1 ntable1 slots1 i2)
- else Return (ntable, slots)
+ else Ok (ntable, slots)
end
.
@@ -257,7 +257,7 @@ Definition hashMap_try_resize
ntable <- hashMap_new_with_capacity T n i3 i i1;
p <- hashMap_move_elements T n ntable self.(hashMap_slots) 0%usize;
let (ntable1, _) := p in
- Return
+ Ok
{|
hashMap_num_entries := self.(hashMap_num_entries);
hashMap_max_load_factor := (i, i1);
@@ -265,7 +265,7 @@ Definition hashMap_try_resize
hashMap_slots := ntable1.(hashMap_slots)
|})
else
- Return
+ Ok
{|
hashMap_num_entries := self.(hashMap_num_entries);
hashMap_max_load_factor := (i, i1);
@@ -284,7 +284,7 @@ Definition hashMap_insert
i <- hashMap_len T self1;
if i s> self1.(hashMap_max_load)
then hashMap_try_resize T n self1
- else Return self1
+ else Ok self1
.
(** [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
@@ -297,9 +297,9 @@ Fixpoint hashMap_contains_key_in_list_loop
match ls with
| List_Cons ckey _ tl =>
if ckey s= key
- then Return true
+ then Ok true
else hashMap_contains_key_in_list_loop T n1 key tl
- | List_Nil => Return false
+ | List_Nil => Ok false
end
end
.
@@ -334,9 +334,7 @@ Fixpoint hashMap_get_in_list_loop
| S n1 =>
match ls with
| List_Cons ckey cvalue tl =>
- if ckey s= key
- then Return cvalue
- else hashMap_get_in_list_loop T n1 key tl
+ if ckey s= key then Ok cvalue else hashMap_get_in_list_loop T n1 key tl
| List_Nil => Fail_ Failure
end
end
@@ -376,15 +374,14 @@ Fixpoint hashMap_get_mut_in_list_loop
| List_Cons ckey cvalue tl =>
if ckey s= key
then
- let back := fun (ret : T) => Return (List_Cons ckey ret tl) in
- Return (cvalue, back)
+ let back := fun (ret : T) => Ok (List_Cons ckey ret tl) in
+ Ok (cvalue, back)
else (
p <- hashMap_get_mut_in_list_loop T n1 tl key;
let (t, back) := p in
let back1 :=
- fun (ret : T) => tl1 <- back ret; Return (List_Cons ckey cvalue tl1)
- in
- Return (t, back1))
+ fun (ret : T) => tl1 <- back ret; Ok (List_Cons ckey cvalue tl1) in
+ Ok (t, back1))
| List_Nil => Fail_ Failure
end
end
@@ -419,14 +416,14 @@ Definition hashMap_get_mut
fun (ret : T) =>
l1 <- get_mut_in_list_back ret;
v <- index_mut_back l1;
- Return
+ Ok
{|
hashMap_num_entries := self.(hashMap_num_entries);
hashMap_max_load_factor := self.(hashMap_max_load_factor);
hashMap_max_load := self.(hashMap_max_load);
hashMap_slots := v
|} in
- Return (t, back)
+ Ok (t, back)
.
(** [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0:
@@ -445,14 +442,14 @@ Fixpoint hashMap_remove_from_list_loop
let (mv_ls, _) :=
core_mem_replace (List_t T) (List_Cons ckey t tl) List_Nil in
match mv_ls with
- | List_Cons _ cvalue tl1 => Return (Some cvalue, tl1)
+ | List_Cons _ cvalue tl1 => Ok (Some cvalue, tl1)
| List_Nil => Fail_ Failure
end
else (
p <- hashMap_remove_from_list_loop T n1 key tl;
let (o, tl1) := p in
- Return (o, List_Cons ckey t tl1))
- | List_Nil => Return (None, List_Nil)
+ Ok (o, List_Cons ckey t tl1))
+ | List_Nil => Ok (None, List_Nil)
end
end
.
@@ -485,7 +482,7 @@ Definition hashMap_remove
match x with
| None =>
v <- index_mut_back l1;
- Return (None,
+ Ok (None,
{|
hashMap_num_entries := self.(hashMap_num_entries);
hashMap_max_load_factor := self.(hashMap_max_load_factor);
@@ -495,7 +492,7 @@ Definition hashMap_remove
| Some x1 =>
i1 <- usize_sub self.(hashMap_num_entries) 1%usize;
v <- index_mut_back l1;
- Return (Some x1,
+ Ok (Some x1,
{|
hashMap_num_entries := i1;
hashMap_max_load_factor := self.(hashMap_max_load_factor);
@@ -541,7 +538,7 @@ Definition test1 (n : nat) : result unit :=
then Fail_ Failure
else (
i4 <- hashMap_get u64 n hm6 1056%usize;
- if negb (i4 s= 256%u64) then Fail_ Failure else Return tt)))
+ if negb (i4 s= 256%u64) then Fail_ Failure else Ok tt)))
end))
.
diff --git a/tests/coq/hashmap/Primitives.v b/tests/coq/hashmap/Primitives.v
index 990e27e4..e84d65ce 100644
--- a/tests/coq/hashmap/Primitives.v
+++ b/tests/coq/hashmap/Primitives.v
@@ -19,19 +19,19 @@ Inductive error :=
| OutOfFuel.
Inductive result A :=
- | Return : A -> result A
+ | Ok : A -> result A
| Fail_ : error -> result A.
-Arguments Return {_} a.
+Arguments Ok {_} a.
Arguments Fail_ {_}.
Definition bind {A B} (m: result A) (f: A -> result B) : result B :=
match m with
| Fail_ e => Fail_ e
- | Return x => f x
+ | Ok x => f x
end.
-Definition return_ {A: Type} (x: A) : result A := Return x.
+Definition return_ {A: Type} (x: A) : result A := Ok x.
Definition fail_ {A: Type} (e: error) : result A := Fail_ e.
Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
@@ -39,27 +39,27 @@ Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
(** Monadic assert *)
Definition massert (b: bool) : result unit :=
- if b then Return tt else Fail_ Failure.
+ if b then Ok tt else Fail_ Failure.
(** Normalize and unwrap a successful result (used for globals) *)
-Definition eval_result_refl {A} {x} (a: result A) (p: a = Return x) : A :=
- match a as r return (r = Return x -> A) with
- | Return a' => fun _ => a'
+Definition eval_result_refl {A} {x} (a: result A) (p: a = Ok x) : A :=
+ match a as r return (r = Ok x -> A) with
+ | Ok a' => fun _ => a'
| Fail_ e => fun p' =>
False_rect _ (eq_ind (Fail_ e)
(fun e : result A =>
match e with
- | Return _ => False
+ | Ok _ => False
| Fail_ e => True
end)
- I (Return x) p')
+ I (Ok x) p')
end p.
Notation "x %global" := (eval_result_refl x eq_refl) (at level 40).
Notation "x %return" := (eval_result_refl x eq_refl) (at level 40).
(* Sanity check *)
-Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3.
+Check (if true then Ok (1 + 2) else Fail_ Failure)%global = 3.
(*** Misc *)
@@ -236,7 +236,7 @@ Import Sumbool.
Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) :=
match sumbool_of_bool (scalar_in_bounds ty x) with
- | left H => Return (exist _ x (scalar_in_bounds_valid _ _ H))
+ | left H => Ok (exist _ x (scalar_in_bounds_valid _ _ H))
| right _ => Fail_ Failure
end.
@@ -544,9 +544,9 @@ Arguments core_ops_range_Range_end_ {_}.
(*** [alloc] *)
-Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Return x.
+Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Ok x.
Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result (T * (T -> result T)) :=
- Return (x, fun x => Return x).
+ Ok (x, fun x => Ok x).
(* Trait instance *)
Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {|
@@ -589,7 +589,7 @@ Definition array_index_mut_usize (T : Type) (n : usize) (a : array T n) (i : usi
result (T * (T -> result (array T n))) :=
match array_index_usize T n a i with
| Fail_ e => Fail_ e
- | Return x => Return (x, array_update_usize T n a i)
+ | Ok x => Ok (x, array_update_usize T n a i)
end.
(*** Slice *)
@@ -603,7 +603,7 @@ Definition slice_index_mut_usize (T : Type) (s : slice T) (i : usize) :
result (T * (T -> result (slice T))) :=
match slice_index_usize T s i with
| Fail_ e => Fail_ e
- | Return x => Return (x, slice_update_usize T s i)
+ | Ok x => Ok (x, slice_update_usize T s i)
end.
(*** Subslices *)
@@ -615,7 +615,7 @@ Definition array_to_slice_mut (T : Type) (n : usize) (a : array T n) :
result (slice T * (slice T -> result (array T n))) :=
match array_to_slice T n a with
| Fail_ e => Fail_ e
- | Return x => Return (x, array_from_slice T n a)
+ | Ok x => Ok (x, array_from_slice T n a)
end.
Axiom array_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize), result (slice T).
@@ -657,17 +657,17 @@ end end.
Definition alloc_vec_Vec_bind {A B} (v: alloc_vec_Vec A) (f: list A -> result (list B)) : result (alloc_vec_Vec B) :=
l <- f (alloc_vec_Vec_to_list v) ;
match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with
- | left H => Return (exist _ l (scalar_le_max_valid _ _ H))
+ | left H => Ok (exist _ l (scalar_le_max_valid _ _ H))
| right _ => Fail_ Failure
end.
Definition alloc_vec_Vec_push (T: Type) (v: alloc_vec_Vec T) (x: T) : result (alloc_vec_Vec T) :=
- alloc_vec_Vec_bind v (fun l => Return (l ++ [x])).
+ alloc_vec_Vec_bind v (fun l => Ok (l ++ [x])).
Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result (alloc_vec_Vec T) :=
alloc_vec_Vec_bind v (fun l =>
if to_Z i <? Z.of_nat (length l)
- then Return (list_update l (usize_to_nat i) x)
+ then Ok (list_update l (usize_to_nat i) x)
else Fail_ Failure).
(* Helper *)
@@ -679,8 +679,8 @@ Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i :
Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usize) :
result (T * (T -> result (alloc_vec_Vec T))) :=
match alloc_vec_Vec_index_usize v i with
- | Return x =>
- Return (x, alloc_vec_Vec_update_usize v i)
+ | Ok x =>
+ Ok (x, alloc_vec_Vec_update_usize v i)
| Fail_ e => Fail_ e
end.
@@ -717,7 +717,7 @@ Definition core_slice_index_Slice_index
x <- inst.(core_slice_index_SliceIndex_get) i s;
match x with
| None => Fail_ Failure
- | Some x => Return x
+ | Some x => Ok x
end.
(* [core::slice::index::Range:::get]: forward function *)
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 8e299800..79da6e80 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -15,7 +15,7 @@ Module HashmapMain_Funs.
(** [hashmap_main::hashmap::hash_key]:
Source: 'src/hashmap.rs', lines 27:0-27:32 *)
Definition hashmap_hash_key (k : usize) : result usize :=
- Return k.
+ Ok k.
(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]: loop 0:
Source: 'src/hashmap.rs', lines 50:4-56:5 *)
@@ -32,7 +32,7 @@ Fixpoint hashmap_HashMap_allocate_slots_loop
slots1 <- alloc_vec_Vec_push (hashmap_List_t T) slots Hashmap_List_Nil;
n3 <- usize_sub n1 1%usize;
hashmap_HashMap_allocate_slots_loop T n2 slots1 n3)
- else Return slots
+ else Ok slots
end
.
@@ -58,7 +58,7 @@ Definition hashmap_HashMap_new_with_capacity
capacity;
i <- usize_mul capacity max_load_dividend;
i1 <- usize_div i max_load_divisor;
- Return
+ Ok
{|
hashmap_HashMap_num_entries := 0%usize;
hashmap_HashMap_max_load_factor := (max_load_dividend, max_load_divisor);
@@ -94,7 +94,7 @@ Fixpoint hashmap_HashMap_clear_loop
i2 <- usize_add i 1%usize;
slots1 <- index_mut_back Hashmap_List_Nil;
hashmap_HashMap_clear_loop T n1 slots1 i2)
- else Return slots
+ else Ok slots
end
.
@@ -105,7 +105,7 @@ Definition hashmap_HashMap_clear
result (hashmap_HashMap_t T)
:=
hm <- hashmap_HashMap_clear_loop T n self.(hashmap_HashMap_slots) 0%usize;
- Return
+ Ok
{|
hashmap_HashMap_num_entries := 0%usize;
hashmap_HashMap_max_load_factor := self.(hashmap_HashMap_max_load_factor);
@@ -118,7 +118,7 @@ Definition hashmap_HashMap_clear
Source: 'src/hashmap.rs', lines 90:4-90:30 *)
Definition hashmap_HashMap_len
(T : Type) (self : hashmap_HashMap_t T) : result usize :=
- Return self.(hashmap_HashMap_num_entries)
+ Ok self.(hashmap_HashMap_num_entries)
.
(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_in_list]: loop 0:
@@ -133,13 +133,13 @@ Fixpoint hashmap_HashMap_insert_in_list_loop
match ls with
| Hashmap_List_Cons ckey cvalue tl =>
if ckey s= key
- then Return (false, Hashmap_List_Cons ckey value tl)
+ then Ok (false, Hashmap_List_Cons ckey value tl)
else (
p <- hashmap_HashMap_insert_in_list_loop T n1 key value tl;
let (b, tl1) := p in
- Return (b, Hashmap_List_Cons ckey cvalue tl1))
+ Ok (b, Hashmap_List_Cons ckey cvalue tl1))
| Hashmap_List_Nil =>
- Return (true, Hashmap_List_Cons key value Hashmap_List_Nil)
+ Ok (true, Hashmap_List_Cons key value Hashmap_List_Nil)
end
end
.
@@ -173,7 +173,7 @@ Definition hashmap_HashMap_insert_no_resize
then (
i1 <- usize_add self.(hashmap_HashMap_num_entries) 1%usize;
v <- index_mut_back l1;
- Return
+ Ok
{|
hashmap_HashMap_num_entries := i1;
hashmap_HashMap_max_load_factor :=
@@ -183,7 +183,7 @@ Definition hashmap_HashMap_insert_no_resize
|})
else (
v <- index_mut_back l1;
- Return
+ Ok
{|
hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries);
hashmap_HashMap_max_load_factor :=
@@ -206,7 +206,7 @@ Fixpoint hashmap_HashMap_move_elements_from_list_loop
| Hashmap_List_Cons k v tl =>
ntable1 <- hashmap_HashMap_insert_no_resize T n1 ntable k v;
hashmap_HashMap_move_elements_from_list_loop T n1 ntable1 tl
- | Hashmap_List_Nil => Return ntable
+ | Hashmap_List_Nil => Ok ntable
end
end
.
@@ -243,7 +243,7 @@ Fixpoint hashmap_HashMap_move_elements_loop
i2 <- usize_add i 1%usize;
slots1 <- index_mut_back l1;
hashmap_HashMap_move_elements_loop T n1 ntable1 slots1 i2)
- else Return (ntable, slots)
+ else Ok (ntable, slots)
end
.
@@ -277,7 +277,7 @@ Definition hashmap_HashMap_try_resize
hashmap_HashMap_move_elements T n ntable self.(hashmap_HashMap_slots)
0%usize;
let (ntable1, _) := p in
- Return
+ Ok
{|
hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries);
hashmap_HashMap_max_load_factor := (i, i1);
@@ -285,7 +285,7 @@ Definition hashmap_HashMap_try_resize
hashmap_HashMap_slots := ntable1.(hashmap_HashMap_slots)
|})
else
- Return
+ Ok
{|
hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries);
hashmap_HashMap_max_load_factor := (i, i1);
@@ -304,7 +304,7 @@ Definition hashmap_HashMap_insert
i <- hashmap_HashMap_len T self1;
if i s> self1.(hashmap_HashMap_max_load)
then hashmap_HashMap_try_resize T n self1
- else Return self1
+ else Ok self1
.
(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
@@ -317,9 +317,9 @@ Fixpoint hashmap_HashMap_contains_key_in_list_loop
match ls with
| Hashmap_List_Cons ckey _ tl =>
if ckey s= key
- then Return true
+ then Ok true
else hashmap_HashMap_contains_key_in_list_loop T n1 key tl
- | Hashmap_List_Nil => Return false
+ | Hashmap_List_Nil => Ok false
end
end
.
@@ -357,7 +357,7 @@ Fixpoint hashmap_HashMap_get_in_list_loop
match ls with
| Hashmap_List_Cons ckey cvalue tl =>
if ckey s= key
- then Return cvalue
+ then Ok cvalue
else hashmap_HashMap_get_in_list_loop T n1 key tl
| Hashmap_List_Nil => Fail_ Failure
end
@@ -398,15 +398,15 @@ Fixpoint hashmap_HashMap_get_mut_in_list_loop
| Hashmap_List_Cons ckey cvalue tl =>
if ckey s= key
then
- let back := fun (ret : T) => Return (Hashmap_List_Cons ckey ret tl) in
- Return (cvalue, back)
+ let back := fun (ret : T) => Ok (Hashmap_List_Cons ckey ret tl) in
+ Ok (cvalue, back)
else (
p <- hashmap_HashMap_get_mut_in_list_loop T n1 tl key;
let (t, back) := p in
let back1 :=
fun (ret : T) =>
- tl1 <- back ret; Return (Hashmap_List_Cons ckey cvalue tl1) in
- Return (t, back1))
+ tl1 <- back ret; Ok (Hashmap_List_Cons ckey cvalue tl1) in
+ Ok (t, back1))
| Hashmap_List_Nil => Fail_ Failure
end
end
@@ -441,7 +441,7 @@ Definition hashmap_HashMap_get_mut
fun (ret : T) =>
l1 <- get_mut_in_list_back ret;
v <- index_mut_back l1;
- Return
+ Ok
{|
hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries);
hashmap_HashMap_max_load_factor :=
@@ -449,7 +449,7 @@ Definition hashmap_HashMap_get_mut
hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load);
hashmap_HashMap_slots := v
|} in
- Return (t, back)
+ Ok (t, back)
.
(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0:
@@ -469,14 +469,14 @@ Fixpoint hashmap_HashMap_remove_from_list_loop
core_mem_replace (hashmap_List_t T) (Hashmap_List_Cons ckey t tl)
Hashmap_List_Nil in
match mv_ls with
- | Hashmap_List_Cons _ cvalue tl1 => Return (Some cvalue, tl1)
+ | Hashmap_List_Cons _ cvalue tl1 => Ok (Some cvalue, tl1)
| Hashmap_List_Nil => Fail_ Failure
end
else (
p <- hashmap_HashMap_remove_from_list_loop T n1 key tl;
let (o, tl1) := p in
- Return (o, Hashmap_List_Cons ckey t tl1))
- | Hashmap_List_Nil => Return (None, Hashmap_List_Nil)
+ Ok (o, Hashmap_List_Cons ckey t tl1))
+ | Hashmap_List_Nil => Ok (None, Hashmap_List_Nil)
end
end
.
@@ -509,7 +509,7 @@ Definition hashmap_HashMap_remove
match x with
| None =>
v <- index_mut_back l1;
- Return (None,
+ Ok (None,
{|
hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries);
hashmap_HashMap_max_load_factor :=
@@ -520,7 +520,7 @@ Definition hashmap_HashMap_remove
| Some x1 =>
i1 <- usize_sub self.(hashmap_HashMap_num_entries) 1%usize;
v <- index_mut_back l1;
- Return (Some x1,
+ Ok (Some x1,
{|
hashmap_HashMap_num_entries := i1;
hashmap_HashMap_max_load_factor :=
@@ -567,7 +567,7 @@ Definition hashmap_test1 (n : nat) : result unit :=
then Fail_ Failure
else (
i4 <- hashmap_HashMap_get u64 n hm6 1056%usize;
- if negb (i4 s= 256%u64) then Fail_ Failure else Return tt)))
+ if negb (i4 s= 256%u64) then Fail_ Failure else Ok tt)))
end))
.
@@ -584,6 +584,6 @@ Definition insert_on_disk
(** [hashmap_main::main]:
Source: 'src/hashmap_main.rs', lines 16:0-16:13 *)
Definition main : result unit :=
- Return tt.
+ Ok tt.
End HashmapMain_Funs.
diff --git a/tests/coq/hashmap_on_disk/Primitives.v b/tests/coq/hashmap_on_disk/Primitives.v
index 990e27e4..e84d65ce 100644
--- a/tests/coq/hashmap_on_disk/Primitives.v
+++ b/tests/coq/hashmap_on_disk/Primitives.v
@@ -19,19 +19,19 @@ Inductive error :=
| OutOfFuel.
Inductive result A :=
- | Return : A -> result A
+ | Ok : A -> result A
| Fail_ : error -> result A.
-Arguments Return {_} a.
+Arguments Ok {_} a.
Arguments Fail_ {_}.
Definition bind {A B} (m: result A) (f: A -> result B) : result B :=
match m with
| Fail_ e => Fail_ e
- | Return x => f x
+ | Ok x => f x
end.
-Definition return_ {A: Type} (x: A) : result A := Return x.
+Definition return_ {A: Type} (x: A) : result A := Ok x.
Definition fail_ {A: Type} (e: error) : result A := Fail_ e.
Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
@@ -39,27 +39,27 @@ Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
(** Monadic assert *)
Definition massert (b: bool) : result unit :=
- if b then Return tt else Fail_ Failure.
+ if b then Ok tt else Fail_ Failure.
(** Normalize and unwrap a successful result (used for globals) *)
-Definition eval_result_refl {A} {x} (a: result A) (p: a = Return x) : A :=
- match a as r return (r = Return x -> A) with
- | Return a' => fun _ => a'
+Definition eval_result_refl {A} {x} (a: result A) (p: a = Ok x) : A :=
+ match a as r return (r = Ok x -> A) with
+ | Ok a' => fun _ => a'
| Fail_ e => fun p' =>
False_rect _ (eq_ind (Fail_ e)
(fun e : result A =>
match e with
- | Return _ => False
+ | Ok _ => False
| Fail_ e => True
end)
- I (Return x) p')
+ I (Ok x) p')
end p.
Notation "x %global" := (eval_result_refl x eq_refl) (at level 40).
Notation "x %return" := (eval_result_refl x eq_refl) (at level 40).
(* Sanity check *)
-Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3.
+Check (if true then Ok (1 + 2) else Fail_ Failure)%global = 3.
(*** Misc *)
@@ -236,7 +236,7 @@ Import Sumbool.
Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) :=
match sumbool_of_bool (scalar_in_bounds ty x) with
- | left H => Return (exist _ x (scalar_in_bounds_valid _ _ H))
+ | left H => Ok (exist _ x (scalar_in_bounds_valid _ _ H))
| right _ => Fail_ Failure
end.
@@ -544,9 +544,9 @@ Arguments core_ops_range_Range_end_ {_}.
(*** [alloc] *)
-Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Return x.
+Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Ok x.
Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result (T * (T -> result T)) :=
- Return (x, fun x => Return x).
+ Ok (x, fun x => Ok x).
(* Trait instance *)
Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {|
@@ -589,7 +589,7 @@ Definition array_index_mut_usize (T : Type) (n : usize) (a : array T n) (i : usi
result (T * (T -> result (array T n))) :=
match array_index_usize T n a i with
| Fail_ e => Fail_ e
- | Return x => Return (x, array_update_usize T n a i)
+ | Ok x => Ok (x, array_update_usize T n a i)
end.
(*** Slice *)
@@ -603,7 +603,7 @@ Definition slice_index_mut_usize (T : Type) (s : slice T) (i : usize) :
result (T * (T -> result (slice T))) :=
match slice_index_usize T s i with
| Fail_ e => Fail_ e
- | Return x => Return (x, slice_update_usize T s i)
+ | Ok x => Ok (x, slice_update_usize T s i)
end.
(*** Subslices *)
@@ -615,7 +615,7 @@ Definition array_to_slice_mut (T : Type) (n : usize) (a : array T n) :
result (slice T * (slice T -> result (array T n))) :=
match array_to_slice T n a with
| Fail_ e => Fail_ e
- | Return x => Return (x, array_from_slice T n a)
+ | Ok x => Ok (x, array_from_slice T n a)
end.
Axiom array_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize), result (slice T).
@@ -657,17 +657,17 @@ end end.
Definition alloc_vec_Vec_bind {A B} (v: alloc_vec_Vec A) (f: list A -> result (list B)) : result (alloc_vec_Vec B) :=
l <- f (alloc_vec_Vec_to_list v) ;
match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with
- | left H => Return (exist _ l (scalar_le_max_valid _ _ H))
+ | left H => Ok (exist _ l (scalar_le_max_valid _ _ H))
| right _ => Fail_ Failure
end.
Definition alloc_vec_Vec_push (T: Type) (v: alloc_vec_Vec T) (x: T) : result (alloc_vec_Vec T) :=
- alloc_vec_Vec_bind v (fun l => Return (l ++ [x])).
+ alloc_vec_Vec_bind v (fun l => Ok (l ++ [x])).
Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result (alloc_vec_Vec T) :=
alloc_vec_Vec_bind v (fun l =>
if to_Z i <? Z.of_nat (length l)
- then Return (list_update l (usize_to_nat i) x)
+ then Ok (list_update l (usize_to_nat i) x)
else Fail_ Failure).
(* Helper *)
@@ -679,8 +679,8 @@ Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i :
Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usize) :
result (T * (T -> result (alloc_vec_Vec T))) :=
match alloc_vec_Vec_index_usize v i with
- | Return x =>
- Return (x, alloc_vec_Vec_update_usize v i)
+ | Ok x =>
+ Ok (x, alloc_vec_Vec_update_usize v i)
| Fail_ e => Fail_ e
end.
@@ -717,7 +717,7 @@ Definition core_slice_index_Slice_index
x <- inst.(core_slice_index_SliceIndex_get) i s;
match x with
| None => Fail_ Failure
- | Some x => Return x
+ | Some x => Ok x
end.
(* [core::slice::index::Range:::get]: forward function *)
diff --git a/tests/coq/misc/Bitwise.v b/tests/coq/misc/Bitwise.v
index b04c95f2..b2339c58 100644
--- a/tests/coq/misc/Bitwise.v
+++ b/tests/coq/misc/Bitwise.v
@@ -23,16 +23,16 @@ Definition shift_i32 (a : i32) : result i32 :=
(** [bitwise::xor_u32]:
Source: 'src/bitwise.rs', lines 17:0-17:37 *)
Definition xor_u32 (a : u32) (b : u32) : result u32 :=
- Return (u32_xor a b).
+ Ok (u32_xor a b).
(** [bitwise::or_u32]:
Source: 'src/bitwise.rs', lines 21:0-21:36 *)
Definition or_u32 (a : u32) (b : u32) : result u32 :=
- Return (u32_or a b).
+ Ok (u32_or a b).
(** [bitwise::and_u32]:
Source: 'src/bitwise.rs', lines 25:0-25:37 *)
Definition and_u32 (a : u32) (b : u32) : result u32 :=
- Return (u32_and a b).
+ Ok (u32_and a b).
End Bitwise.
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v
index fcafed53..71185975 100644
--- a/tests/coq/misc/Constants.v
+++ b/tests/coq/misc/Constants.v
@@ -10,17 +10,17 @@ Module Constants.
(** [constants::X0]
Source: 'src/constants.rs', lines 5:0-5:17 *)
-Definition x0_body : result u32 := Return 0%u32.
+Definition x0_body : result u32 := Ok 0%u32.
Definition x0 : u32 := x0_body%global.
(** [constants::X1]
Source: 'src/constants.rs', lines 7:0-7:17 *)
-Definition x1_body : result u32 := Return core_u32_max.
+Definition x1_body : result u32 := Ok core_u32_max.
Definition x1 : u32 := x1_body%global.
(** [constants::X2]
Source: 'src/constants.rs', lines 10:0-10:17 *)
-Definition x2_body : result u32 := Return 3%u32.
+Definition x2_body : result u32 := Ok 3%u32.
Definition x2 : u32 := x2_body%global.
(** [constants::incr]:
@@ -36,8 +36,7 @@ Definition x3 : u32 := x3_body%global.
(** [constants::mk_pair0]:
Source: 'src/constants.rs', lines 23:0-23:51 *)
Definition mk_pair0 (x : u32) (y1 : u32) : result (u32 * u32) :=
- Return (x, y1)
-.
+ Ok (x, y1).
(** [constants::Pair]
Source: 'src/constants.rs', lines 36:0-36:23 *)
@@ -50,7 +49,7 @@ Arguments pair_y { _ _ }.
(** [constants::mk_pair1]:
Source: 'src/constants.rs', lines 27:0-27:55 *)
Definition mk_pair1 (x : u32) (y1 : u32) : result (Pair_t u32 u32) :=
- Return {| pair_x := x; pair_y := y1 |}
+ Ok {| pair_x := x; pair_y := y1 |}
.
(** [constants::P0]
@@ -65,13 +64,13 @@ Definition p1 : Pair_t u32 u32 := p1_body%global.
(** [constants::P2]
Source: 'src/constants.rs', lines 33:0-33:24 *)
-Definition p2_body : result (u32 * u32) := Return (0%u32, 1%u32).
+Definition p2_body : result (u32 * u32) := Ok (0%u32, 1%u32).
Definition p2 : (u32 * u32) := p2_body%global.
(** [constants::P3]
Source: 'src/constants.rs', lines 34:0-34:28 *)
Definition p3_body : result (Pair_t u32 u32) :=
- Return {| pair_x := 0%u32; pair_y := 1%u32 |}
+ Ok {| pair_x := 0%u32; pair_y := 1%u32 |}
.
Definition p3 : Pair_t u32 u32 := p3_body%global.
@@ -85,7 +84,7 @@ Arguments wrap_value { _ }.
(** [constants::{constants::Wrap<T>}::new]:
Source: 'src/constants.rs', lines 54:4-54:41 *)
Definition wrap_new (T : Type) (value : T) : result (Wrap_t T) :=
- Return {| wrap_value := value |}
+ Ok {| wrap_value := value |}
.
(** [constants::Y]
@@ -96,7 +95,7 @@ Definition y : Wrap_t i32 := y_body%global.
(** [constants::unwrap_y]:
Source: 'src/constants.rs', lines 43:0-43:30 *)
Definition unwrap_y : result i32 :=
- Return y.(wrap_value).
+ Ok y.(wrap_value).
(** [constants::YVAL]
Source: 'src/constants.rs', lines 47:0-47:19 *)
@@ -105,13 +104,13 @@ Definition yval : i32 := yval_body%global.
(** [constants::get_z1::Z1]
Source: 'src/constants.rs', lines 62:4-62:17 *)
-Definition get_z1_z1_body : result i32 := Return 3%i32.
+Definition get_z1_z1_body : result i32 := Ok 3%i32.
Definition get_z1_z1 : i32 := get_z1_z1_body%global.
(** [constants::get_z1]:
Source: 'src/constants.rs', lines 61:0-61:28 *)
Definition get_z1 : result i32 :=
- Return get_z1_z1.
+ Ok get_z1_z1.
(** [constants::add]:
Source: 'src/constants.rs', lines 66:0-66:39 *)
@@ -120,12 +119,12 @@ Definition add (a : i32) (b : i32) : result i32 :=
(** [constants::Q1]
Source: 'src/constants.rs', lines 74:0-74:17 *)
-Definition q1_body : result i32 := Return 5%i32.
+Definition q1_body : result i32 := Ok 5%i32.
Definition q1 : i32 := q1_body%global.
(** [constants::Q2]
Source: 'src/constants.rs', lines 75:0-75:17 *)
-Definition q2_body : result i32 := Return q1.
+Definition q2_body : result i32 := Ok q1.
Definition q2 : i32 := q2_body%global.
(** [constants::Q3]
@@ -140,7 +139,7 @@ Definition get_z2 : result i32 :=
(** [constants::S1]
Source: 'src/constants.rs', lines 80:0-80:18 *)
-Definition s1_body : result u32 := Return 6%u32.
+Definition s1_body : result u32 := Ok 6%u32.
Definition s1 : u32 := s1_body%global.
(** [constants::S2]
@@ -150,7 +149,7 @@ Definition s2 : u32 := s2_body%global.
(** [constants::S3]
Source: 'src/constants.rs', lines 82:0-82:29 *)
-Definition s3_body : result (Pair_t u32 u32) := Return p3.
+Definition s3_body : result (Pair_t u32 u32) := Ok p3.
Definition s3 : Pair_t u32 u32 := s3_body%global.
(** [constants::S4]
@@ -167,12 +166,12 @@ Arguments v_x { _ _ }.
(** [constants::{constants::V<T, N>#1}::LEN]
Source: 'src/constants.rs', lines 91:4-91:24 *)
-Definition v_len_body (T : Type) (N : usize) : result usize := Return N.
+Definition v_len_body (T : Type) (N : usize) : result usize := Ok N.
Definition v_len (T : Type) (N : usize) : usize := (v_len_body T N)%global.
(** [constants::use_v]:
Source: 'src/constants.rs', lines 94:0-94:42 *)
Definition use_v (T : Type) (N : usize) : result usize :=
- Return (v_len T N).
+ Ok (v_len T N).
End Constants.
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index a6832854..41d4a7bd 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -31,7 +31,7 @@ Definition test_new_non_zero_u32
(** [external::test_vec]:
Source: 'src/external.rs', lines 17:0-17:17 *)
Definition test_vec : result unit :=
- _ <- alloc_vec_Vec_push u32 (alloc_vec_Vec_new u32) 0%u32; Return tt
+ _ <- alloc_vec_Vec_push u32 (alloc_vec_Vec_new u32) 0%u32; Ok tt
.
(** Unit test for [external::test_vec] *)
@@ -46,8 +46,8 @@ Definition custom_swap
p <- core_mem_swap T x y st;
let (st1, p1) := p in
let (x1, y1) := p1 in
- let back := fun (ret : T) (st2 : state) => Return (st2, (ret, y1)) in
- Return (st1, (x1, back))
+ let back := fun (ret : T) (st2 : state) => Ok (st2, (ret, y1)) in
+ Ok (st1, (x1, back))
.
(** [external::test_custom_swap]:
@@ -60,7 +60,7 @@ Definition test_custom_swap
p2 <- custom_swap_back 1%u32 st1;
let (_, p3) := p2 in
let (x1, y1) := p3 in
- Return (st1, (x1, y1))
+ Ok (st1, (x1, y1))
.
(** [external::test_swap_non_zero]:
@@ -69,7 +69,7 @@ Definition test_swap_non_zero (x : u32) (st : state) : result (state * u32) :=
p <- swap u32 x 0%u32 st;
let (st1, p1) := p in
let (x1, _) := p1 in
- if x1 s= 0%u32 then Fail_ Failure else Return (st1, x1)
+ if x1 s= 0%u32 then Fail_ Failure else Ok (st1, x1)
.
End External_Funs.
diff --git a/tests/coq/misc/External_FunsExternal.v b/tests/coq/misc/External_FunsExternal.v
index e9655f57..130b48a2 100644
--- a/tests/coq/misc/External_FunsExternal.v
+++ b/tests/coq/misc/External_FunsExternal.v
@@ -13,7 +13,7 @@ Module External_FunsExternal.
(** [core::mem::swap]:
Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
Definition core_mem_swap (T : Type) (x : T) (y : T) (s : state) :=
- Return (s, (y, x))
+ Ok (s, (y, x))
.
(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index ae529cf8..f396f16f 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -83,7 +83,7 @@ Fixpoint sum_array_loop
s1 <- u32_add s i1;
i2 <- usize_add i 1%usize;
sum_array_loop N n1 a i2 s1)
- else Return s
+ else Ok s
end
.
@@ -110,7 +110,7 @@ Fixpoint clear_loop
i2 <- usize_add i 1%usize;
v1 <- index_mut_back 0%u32;
clear_loop n1 v1 i2)
- else Return v
+ else Ok v
end
.
@@ -138,8 +138,8 @@ Fixpoint list_mem_loop (n : nat) (x : u32) (ls : List_t u32) : result bool :=
| O => Fail_ OutOfFuel
| S n1 =>
match ls with
- | List_Cons y tl => if y s= x then Return true else list_mem_loop n1 x tl
- | List_Nil => Return false
+ | List_Cons y tl => if y s= x then Ok true else list_mem_loop n1 x tl
+ | List_Nil => Ok false
end
end
.
@@ -162,16 +162,13 @@ Fixpoint list_nth_mut_loop_loop
match ls with
| List_Cons x tl =>
if i s= 0%u32
- then
- let back := fun (ret : T) => Return (List_Cons ret tl) in
- Return (x, back)
+ then let back := fun (ret : T) => Ok (List_Cons ret tl) in Ok (x, back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_mut_loop_loop T n1 tl i1;
let (t, back) := p in
- let back1 := fun (ret : T) => tl1 <- back ret; Return (List_Cons x tl1)
- in
- Return (t, back1))
+ let back1 := fun (ret : T) => tl1 <- back ret; Ok (List_Cons x tl1) in
+ Ok (t, back1))
| List_Nil => Fail_ Failure
end
end
@@ -196,7 +193,7 @@ Fixpoint list_nth_shared_loop_loop
match ls with
| List_Cons x tl =>
if i s= 0%u32
- then Return x
+ then Ok x
else (i1 <- u32_sub i 1%u32; list_nth_shared_loop_loop T n1 tl i1)
| List_Nil => Fail_ Failure
end
@@ -223,14 +220,13 @@ Fixpoint get_elem_mut_loop
| List_Cons y tl =>
if y s= x
then
- let back := fun (ret : usize) => Return (List_Cons ret tl) in
- Return (y, back)
+ let back := fun (ret : usize) => Ok (List_Cons ret tl) in Ok (y, back)
else (
p <- get_elem_mut_loop n1 x tl;
let (i, back) := p in
- let back1 :=
- fun (ret : usize) => tl1 <- back ret; Return (List_Cons y tl1) in
- Return (i, back1))
+ let back1 := fun (ret : usize) => tl1 <- back ret; Ok (List_Cons y tl1)
+ in
+ Ok (i, back1))
| List_Nil => Fail_ Failure
end
end
@@ -249,7 +245,7 @@ Definition get_elem_mut
p1 <- get_elem_mut_loop n x ls;
let (i, back) := p1 in
let back1 := fun (ret : usize) => l <- back ret; index_mut_back l in
- Return (i, back1)
+ Ok (i, back1)
.
(** [loops::get_elem_shared]: loop 0:
@@ -260,8 +256,7 @@ Fixpoint get_elem_shared_loop
| O => Fail_ OutOfFuel
| S n1 =>
match ls with
- | List_Cons y tl =>
- if y s= x then Return y else get_elem_shared_loop n1 x tl
+ | List_Cons y tl => if y s= x then Ok y else get_elem_shared_loop n1 x tl
| List_Nil => Fail_ Failure
end
end
@@ -285,14 +280,13 @@ Definition id_mut
(T : Type) (ls : List_t T) :
result ((List_t T) * (List_t T -> result (List_t T)))
:=
- Return (ls, Return)
+ Ok (ls, Ok)
.
(** [loops::id_shared]:
Source: 'src/loops.rs', lines 149:0-149:45 *)
Definition id_shared (T : Type) (ls : List_t T) : result (List_t T) :=
- Return ls
-.
+ Ok ls.
(** [loops::list_nth_mut_loop_with_id]: loop 0:
Source: 'src/loops.rs', lines 154:0-165:1 *)
@@ -306,16 +300,13 @@ Fixpoint list_nth_mut_loop_with_id_loop
match ls with
| List_Cons x tl =>
if i s= 0%u32
- then
- let back := fun (ret : T) => Return (List_Cons ret tl) in
- Return (x, back)
+ then let back := fun (ret : T) => Ok (List_Cons ret tl) in Ok (x, back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_mut_loop_with_id_loop T n1 i1 tl;
let (t, back) := p in
- let back1 := fun (ret : T) => tl1 <- back ret; Return (List_Cons x tl1)
- in
- Return (t, back1))
+ let back1 := fun (ret : T) => tl1 <- back ret; Ok (List_Cons x tl1) in
+ Ok (t, back1))
| List_Nil => Fail_ Failure
end
end
@@ -332,7 +323,7 @@ Definition list_nth_mut_loop_with_id
p1 <- list_nth_mut_loop_with_id_loop T n i ls1;
let (t, back) := p1 in
let back1 := fun (ret : T) => l <- back ret; id_mut_back l in
- Return (t, back1)
+ Ok (t, back1)
.
(** [loops::list_nth_shared_loop_with_id]: loop 0:
@@ -345,7 +336,7 @@ Fixpoint list_nth_shared_loop_with_id_loop
match ls with
| List_Cons x tl =>
if i s= 0%u32
- then Return x
+ then Ok x
else (
i1 <- u32_sub i 1%u32; list_nth_shared_loop_with_id_loop T n1 i1 tl)
| List_Nil => Fail_ Failure
@@ -375,18 +366,18 @@ Fixpoint list_nth_mut_loop_pair_loop
| List_Cons x1 tl1 =>
if i s= 0%u32
then
- let back'a := fun (ret : T) => Return (List_Cons ret tl0) in
- let back'b := fun (ret : T) => Return (List_Cons ret tl1) in
- Return ((x0, x1), back'a, back'b)
+ let back'a := fun (ret : T) => Ok (List_Cons ret tl0) in
+ let back'b := fun (ret : T) => Ok (List_Cons ret tl1) in
+ Ok ((x0, x1), back'a, back'b)
else (
i1 <- u32_sub i 1%u32;
t <- list_nth_mut_loop_pair_loop T n1 tl0 tl1 i1;
let '(p, back'a, back'b) := t in
let back'a1 :=
- fun (ret : T) => tl01 <- back'a ret; Return (List_Cons x0 tl01) in
+ fun (ret : T) => tl01 <- back'a ret; Ok (List_Cons x0 tl01) in
let back'b1 :=
- fun (ret : T) => tl11 <- back'b ret; Return (List_Cons x1 tl11) in
- Return (p, back'a1, back'b1))
+ fun (ret : T) => tl11 <- back'b ret; Ok (List_Cons x1 tl11) in
+ Ok (p, back'a1, back'b1))
| List_Nil => Fail_ Failure
end
| List_Nil => Fail_ Failure
@@ -417,7 +408,7 @@ Fixpoint list_nth_shared_loop_pair_loop
match ls1 with
| List_Cons x1 tl1 =>
if i s= 0%u32
- then Return (x0, x1)
+ then Ok (x0, x1)
else (
i1 <- u32_sub i 1%u32; list_nth_shared_loop_pair_loop T n1 tl0 tl1 i1)
| List_Nil => Fail_ Failure
@@ -453,9 +444,8 @@ Fixpoint list_nth_mut_loop_pair_merge_loop
then
let back :=
fun (ret : (T * T)) =>
- let (t, t1) := ret in Return (List_Cons t tl0, List_Cons t1 tl1)
- in
- Return ((x0, x1), back)
+ let (t, t1) := ret in Ok (List_Cons t tl0, List_Cons t1 tl1) in
+ Ok ((x0, x1), back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_mut_loop_pair_merge_loop T n1 tl0 tl1 i1;
@@ -464,8 +454,8 @@ Fixpoint list_nth_mut_loop_pair_merge_loop
fun (ret : (T * T)) =>
p2 <- back ret;
let (tl01, tl11) := p2 in
- Return (List_Cons x0 tl01, List_Cons x1 tl11) in
- Return (p1, back1))
+ Ok (List_Cons x0 tl01, List_Cons x1 tl11) in
+ Ok (p1, back1))
| List_Nil => Fail_ Failure
end
| List_Nil => Fail_ Failure
@@ -496,7 +486,7 @@ Fixpoint list_nth_shared_loop_pair_merge_loop
match ls1 with
| List_Cons x1 tl1 =>
if i s= 0%u32
- then Return (x0, x1)
+ then Ok (x0, x1)
else (
i1 <- u32_sub i 1%u32;
list_nth_shared_loop_pair_merge_loop T n1 tl0 tl1 i1)
@@ -531,15 +521,15 @@ Fixpoint list_nth_mut_shared_loop_pair_loop
| List_Cons x1 tl1 =>
if i s= 0%u32
then
- let back := fun (ret : T) => Return (List_Cons ret tl0) in
- Return ((x0, x1), back)
+ let back := fun (ret : T) => Ok (List_Cons ret tl0) in
+ Ok ((x0, x1), back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_mut_shared_loop_pair_loop T n1 tl0 tl1 i1;
let (p1, back) := p in
let back1 :=
- fun (ret : T) => tl01 <- back ret; Return (List_Cons x0 tl01) in
- Return (p1, back1))
+ fun (ret : T) => tl01 <- back ret; Ok (List_Cons x0 tl01) in
+ Ok (p1, back1))
| List_Nil => Fail_ Failure
end
| List_Nil => Fail_ Failure
@@ -571,15 +561,15 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop
| List_Cons x1 tl1 =>
if i s= 0%u32
then
- let back := fun (ret : T) => Return (List_Cons ret tl0) in
- Return ((x0, x1), back)
+ let back := fun (ret : T) => Ok (List_Cons ret tl0) in
+ Ok ((x0, x1), back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_mut_shared_loop_pair_merge_loop T n1 tl0 tl1 i1;
let (p1, back) := p in
let back1 :=
- fun (ret : T) => tl01 <- back ret; Return (List_Cons x0 tl01) in
- Return (p1, back1))
+ fun (ret : T) => tl01 <- back ret; Ok (List_Cons x0 tl01) in
+ Ok (p1, back1))
| List_Nil => Fail_ Failure
end
| List_Nil => Fail_ Failure
@@ -611,15 +601,15 @@ Fixpoint list_nth_shared_mut_loop_pair_loop
| List_Cons x1 tl1 =>
if i s= 0%u32
then
- let back := fun (ret : T) => Return (List_Cons ret tl1) in
- Return ((x0, x1), back)
+ let back := fun (ret : T) => Ok (List_Cons ret tl1) in
+ Ok ((x0, x1), back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_shared_mut_loop_pair_loop T n1 tl0 tl1 i1;
let (p1, back) := p in
let back1 :=
- fun (ret : T) => tl11 <- back ret; Return (List_Cons x1 tl11) in
- Return (p1, back1))
+ fun (ret : T) => tl11 <- back ret; Ok (List_Cons x1 tl11) in
+ Ok (p1, back1))
| List_Nil => Fail_ Failure
end
| List_Nil => Fail_ Failure
@@ -651,15 +641,15 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop
| List_Cons x1 tl1 =>
if i s= 0%u32
then
- let back := fun (ret : T) => Return (List_Cons ret tl1) in
- Return ((x0, x1), back)
+ let back := fun (ret : T) => Ok (List_Cons ret tl1) in
+ Ok ((x0, x1), back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_shared_mut_loop_pair_merge_loop T n1 tl0 tl1 i1;
let (p1, back) := p in
let back1 :=
- fun (ret : T) => tl11 <- back ret; Return (List_Cons x1 tl11) in
- Return (p1, back1))
+ fun (ret : T) => tl11 <- back ret; Ok (List_Cons x1 tl11) in
+ Ok (p1, back1))
| List_Nil => Fail_ Failure
end
| List_Nil => Fail_ Failure
@@ -684,7 +674,7 @@ Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
| S n1 =>
if i s> 0%u32
then (i1 <- u32_sub i 1%u32; ignore_input_mut_borrow_loop n1 i1)
- else Return tt
+ else Ok tt
end
.
@@ -692,7 +682,7 @@ Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
Source: 'src/loops.rs', lines 345:0-345:56 *)
Definition ignore_input_mut_borrow
(n : nat) (_a : u32) (i : u32) : result u32 :=
- _ <- ignore_input_mut_borrow_loop n i; Return _a
+ _ <- ignore_input_mut_borrow_loop n i; Ok _a
.
(** [loops::incr_ignore_input_mut_borrow]: loop 0:
@@ -703,7 +693,7 @@ Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
| S n1 =>
if i s> 0%u32
then (i1 <- u32_sub i 1%u32; incr_ignore_input_mut_borrow_loop n1 i1)
- else Return tt
+ else Ok tt
end
.
@@ -711,7 +701,7 @@ Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
Source: 'src/loops.rs', lines 353:0-353:60 *)
Definition incr_ignore_input_mut_borrow
(n : nat) (a : u32) (i : u32) : result u32 :=
- a1 <- u32_add a 1%u32; _ <- incr_ignore_input_mut_borrow_loop n i; Return a1
+ a1 <- u32_add a 1%u32; _ <- incr_ignore_input_mut_borrow_loop n i; Ok a1
.
(** [loops::ignore_input_shared_borrow]: loop 0:
@@ -722,7 +712,7 @@ Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit :=
| S n1 =>
if i s> 0%u32
then (i1 <- u32_sub i 1%u32; ignore_input_shared_borrow_loop n1 i1)
- else Return tt
+ else Ok tt
end
.
@@ -730,7 +720,7 @@ Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit :=
Source: 'src/loops.rs', lines 362:0-362:59 *)
Definition ignore_input_shared_borrow
(n : nat) (_a : u32) (i : u32) : result u32 :=
- _ <- ignore_input_shared_borrow_loop n i; Return _a
+ _ <- ignore_input_shared_borrow_loop n i; Ok _a
.
End Loops.
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index d4035104..ecdfb281 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -170,12 +170,12 @@ Definition cast_bool_to_i32 (x : bool) : result i32 :=
(** [no_nested_borrows::cast_bool_to_bool]:
Source: 'src/no_nested_borrows.rs', lines 137:0-137:41 *)
Definition cast_bool_to_bool (x : bool) : result bool :=
- Return x.
+ Ok x.
(** [no_nested_borrows::test2]:
Source: 'src/no_nested_borrows.rs', lines 142:0-142:14 *)
Definition test2 : result unit :=
- _ <- u32_add 23%u32 44%u32; Return tt.
+ _ <- u32_add 23%u32 44%u32; Ok tt.
(** Unit test for [no_nested_borrows::test2] *)
Check (test2 )%return.
@@ -183,7 +183,7 @@ Check (test2 )%return.
(** [no_nested_borrows::get_max]:
Source: 'src/no_nested_borrows.rs', lines 154:0-154:37 *)
Definition get_max (x : u32) (y : u32) : result u32 :=
- if x s>= y then Return x else Return y
+ if x s>= y then Ok x else Ok y
.
(** [no_nested_borrows::test3]:
@@ -192,7 +192,7 @@ Definition test3 : result unit :=
x <- get_max 4%u32 3%u32;
y <- get_max 10%u32 11%u32;
z <- u32_add x y;
- if negb (z s= 15%u32) then Fail_ Failure else Return tt
+ if negb (z s= 15%u32) then Fail_ Failure else Ok tt
.
(** Unit test for [no_nested_borrows::test3] *)
@@ -201,7 +201,7 @@ Check (test3 )%return.
(** [no_nested_borrows::test_neg1]:
Source: 'src/no_nested_borrows.rs', lines 169:0-169:18 *)
Definition test_neg1 : result unit :=
- y <- i32_neg 3%i32; if negb (y s= (-3)%i32) then Fail_ Failure else Return tt
+ y <- i32_neg 3%i32; if negb (y s= (-3)%i32) then Fail_ Failure else Ok tt
.
(** Unit test for [no_nested_borrows::test_neg1] *)
@@ -210,7 +210,7 @@ Check (test_neg1 )%return.
(** [no_nested_borrows::refs_test1]:
Source: 'src/no_nested_borrows.rs', lines 176:0-176:19 *)
Definition refs_test1 : result unit :=
- if negb (1%i32 s= 1%i32) then Fail_ Failure else Return tt
+ if negb (1%i32 s= 1%i32) then Fail_ Failure else Ok tt
.
(** Unit test for [no_nested_borrows::refs_test1] *)
@@ -227,7 +227,7 @@ Definition refs_test2 : result unit :=
else
if negb (2%i32 s= 2%i32)
then Fail_ Failure
- else if negb (2%i32 s= 2%i32) then Fail_ Failure else Return tt
+ else if negb (2%i32 s= 2%i32) then Fail_ Failure else Ok tt
.
(** Unit test for [no_nested_borrows::refs_test2] *)
@@ -236,7 +236,7 @@ Check (refs_test2 )%return.
(** [no_nested_borrows::test_list1]:
Source: 'src/no_nested_borrows.rs', lines 203:0-203:19 *)
Definition test_list1 : result unit :=
- Return tt.
+ Ok tt.
(** Unit test for [no_nested_borrows::test_list1] *)
Check (test_list1 )%return.
@@ -248,7 +248,7 @@ Definition test_box1 : result unit :=
let (_, deref_mut_back) := p in
b <- deref_mut_back 1%i32;
x <- alloc_boxed_Box_deref i32 b;
- if negb (x s= 1%i32) then Fail_ Failure else Return tt
+ if negb (x s= 1%i32) then Fail_ Failure else Ok tt
.
(** Unit test for [no_nested_borrows::test_box1] *)
@@ -257,24 +257,24 @@ Check (test_box1 )%return.
(** [no_nested_borrows::copy_int]:
Source: 'src/no_nested_borrows.rs', lines 218:0-218:30 *)
Definition copy_int (x : i32) : result i32 :=
- Return x.
+ Ok x.
(** [no_nested_borrows::test_unreachable]:
Source: 'src/no_nested_borrows.rs', lines 224:0-224:32 *)
Definition test_unreachable (b : bool) : result unit :=
- if b then Fail_ Failure else Return tt
+ if b then Fail_ Failure else Ok tt
.
(** [no_nested_borrows::test_panic]:
Source: 'src/no_nested_borrows.rs', lines 232:0-232:26 *)
Definition test_panic (b : bool) : result unit :=
- if b then Fail_ Failure else Return tt
+ if b then Fail_ Failure else Ok tt
.
(** [no_nested_borrows::test_copy_int]:
Source: 'src/no_nested_borrows.rs', lines 239:0-239:22 *)
Definition test_copy_int : result unit :=
- y <- copy_int 0%i32; if negb (0%i32 s= y) then Fail_ Failure else Return tt
+ y <- copy_int 0%i32; if negb (0%i32 s= y) then Fail_ Failure else Ok tt
.
(** Unit test for [no_nested_borrows::test_copy_int] *)
@@ -283,14 +283,14 @@ Check (test_copy_int )%return.
(** [no_nested_borrows::is_cons]:
Source: 'src/no_nested_borrows.rs', lines 246:0-246:38 *)
Definition is_cons (T : Type) (l : List_t T) : result bool :=
- match l with | List_Cons _ _ => Return true | List_Nil => Return false end
+ match l with | List_Cons _ _ => Ok true | List_Nil => Ok false end
.
(** [no_nested_borrows::test_is_cons]:
Source: 'src/no_nested_borrows.rs', lines 253:0-253:21 *)
Definition test_is_cons : result unit :=
b <- is_cons i32 (List_Cons 0%i32 List_Nil);
- if negb b then Fail_ Failure else Return tt
+ if negb b then Fail_ Failure else Ok tt
.
(** Unit test for [no_nested_borrows::test_is_cons] *)
@@ -299,10 +299,7 @@ Check (test_is_cons )%return.
(** [no_nested_borrows::split_list]:
Source: 'src/no_nested_borrows.rs', lines 259:0-259:48 *)
Definition split_list (T : Type) (l : List_t T) : result (T * (List_t T)) :=
- match l with
- | List_Cons hd tl => Return (hd, tl)
- | List_Nil => Fail_ Failure
- end
+ match l with | List_Cons hd tl => Ok (hd, tl) | List_Nil => Fail_ Failure end
.
(** [no_nested_borrows::test_split_list]:
@@ -310,7 +307,7 @@ Definition split_list (T : Type) (l : List_t T) : result (T * (List_t T)) :=
Definition test_split_list : result unit :=
p <- split_list i32 (List_Cons 0%i32 List_Nil);
let (hd, _) := p in
- if negb (hd s= 0%i32) then Fail_ Failure else Return tt
+ if negb (hd s= 0%i32) then Fail_ Failure else Ok tt
.
(** Unit test for [no_nested_borrows::test_split_list] *)
@@ -321,8 +318,8 @@ Check (test_split_list )%return.
Definition choose
(T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) :=
if b
- then let back := fun (ret : T) => Return (ret, y) in Return (x, back)
- else let back := fun (ret : T) => Return (x, ret) in Return (y, back)
+ then let back := fun (ret : T) => Ok (ret, y) in Ok (x, back)
+ else let back := fun (ret : T) => Ok (x, ret) in Ok (y, back)
.
(** [no_nested_borrows::choose_test]:
@@ -338,7 +335,7 @@ Definition choose_test : result unit :=
let (x, y) := p1 in
if negb (x s= 1%i32)
then Fail_ Failure
- else if negb (y s= 0%i32) then Fail_ Failure else Return tt)
+ else if negb (y s= 0%i32) then Fail_ Failure else Ok tt)
.
(** Unit test for [no_nested_borrows::choose_test] *)
@@ -347,7 +344,7 @@ Check (choose_test )%return.
(** [no_nested_borrows::test_char]:
Source: 'src/no_nested_borrows.rs', lines 294:0-294:26 *)
Definition test_char : result char :=
- Return (char_of_byte Coq.Init.Byte.x61).
+ Ok (char_of_byte Coq.Init.Byte.x61).
(** [no_nested_borrows::Tree]
Source: 'src/no_nested_borrows.rs', lines 299:0-299:16 *)
@@ -373,7 +370,7 @@ Arguments NodeElem_Nil { _ }.
Fixpoint list_length (T : Type) (l : List_t T) : result u32 :=
match l with
| List_Cons _ l1 => i <- list_length T l1; u32_add 1%u32 i
- | List_Nil => Return 0%u32
+ | List_Nil => Ok 0%u32
end
.
@@ -383,7 +380,7 @@ Fixpoint list_nth_shared (T : Type) (l : List_t T) (i : u32) : result T :=
match l with
| List_Cons x tl =>
if i s= 0%u32
- then Return x
+ then Ok x
else (i1 <- u32_sub i 1%u32; list_nth_shared T tl i1)
| List_Nil => Fail_ Failure
end
@@ -398,17 +395,14 @@ Fixpoint list_nth_mut
match l with
| List_Cons x tl =>
if i s= 0%u32
- then
- let back := fun (ret : T) => Return (List_Cons ret tl) in
- Return (x, back)
+ then let back := fun (ret : T) => Ok (List_Cons ret tl) in Ok (x, back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_mut T tl i1;
let (t, list_nth_mut_back) := p in
let back :=
- fun (ret : T) => tl1 <- list_nth_mut_back ret; Return (List_Cons x tl1)
- in
- Return (t, back))
+ fun (ret : T) => tl1 <- list_nth_mut_back ret; Ok (List_Cons x tl1) in
+ Ok (t, back))
| List_Nil => Fail_ Failure
end
.
@@ -419,7 +413,7 @@ Fixpoint list_rev_aux
(T : Type) (li : List_t T) (lo : List_t T) : result (List_t T) :=
match li with
| List_Cons hd tl => list_rev_aux T tl (List_Cons hd lo)
- | List_Nil => Return lo
+ | List_Nil => Ok lo
end
.
@@ -463,7 +457,7 @@ Definition test_list_functions : result unit :=
then Fail_ Failure
else (
i6 <- list_nth_shared i32 ls 2%u32;
- if negb (i6 s= 2%i32) then Fail_ Failure else Return tt))))))
+ if negb (i6 s= 2%i32) then Fail_ Failure else Ok tt))))))
.
(** Unit test for [no_nested_borrows::test_list_functions] *)
@@ -475,7 +469,7 @@ Definition id_mut_pair1
(T1 T2 : Type) (x : T1) (y : T2) :
result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2)))
:=
- Return ((x, y), Return)
+ Ok ((x, y), Ok)
.
(** [no_nested_borrows::id_mut_pair2]:
@@ -484,7 +478,7 @@ Definition id_mut_pair2
(T1 T2 : Type) (p : (T1 * T2)) :
result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2)))
:=
- let (t, t1) := p in Return ((t, t1), Return)
+ let (t, t1) := p in Ok ((t, t1), Ok)
.
(** [no_nested_borrows::id_mut_pair3]:
@@ -493,7 +487,7 @@ Definition id_mut_pair3
(T1 T2 : Type) (x : T1) (y : T2) :
result ((T1 * T2) * (T1 -> result T1) * (T2 -> result T2))
:=
- Return ((x, y), Return, Return)
+ Ok ((x, y), Ok, Ok)
.
(** [no_nested_borrows::id_mut_pair4]:
@@ -502,7 +496,7 @@ Definition id_mut_pair4
(T1 T2 : Type) (p : (T1 * T2)) :
result ((T1 * T2) * (T1 -> result T1) * (T2 -> result T2))
:=
- let (t, t1) := p in Return ((t, t1), Return, Return)
+ let (t, t1) := p in Ok ((t, t1), Ok, Ok)
.
(** [no_nested_borrows::StructWithTuple]
@@ -519,19 +513,19 @@ Arguments structWithTuple_p { _ _ }.
(** [no_nested_borrows::new_tuple1]:
Source: 'src/no_nested_borrows.rs', lines 437:0-437:48 *)
Definition new_tuple1 : result (StructWithTuple_t u32 u32) :=
- Return {| structWithTuple_p := (1%u32, 2%u32) |}
+ Ok {| structWithTuple_p := (1%u32, 2%u32) |}
.
(** [no_nested_borrows::new_tuple2]:
Source: 'src/no_nested_borrows.rs', lines 441:0-441:48 *)
Definition new_tuple2 : result (StructWithTuple_t i16 i16) :=
- Return {| structWithTuple_p := (1%i16, 2%i16) |}
+ Ok {| structWithTuple_p := (1%i16, 2%i16) |}
.
(** [no_nested_borrows::new_tuple3]:
Source: 'src/no_nested_borrows.rs', lines 445:0-445:48 *)
Definition new_tuple3 : result (StructWithTuple_t u64 i64) :=
- Return {| structWithTuple_p := (1%u64, 2%i64) |}
+ Ok {| structWithTuple_p := (1%u64, 2%i64) |}
.
(** [no_nested_borrows::StructWithPair]
@@ -548,7 +542,7 @@ Arguments structWithPair_p { _ _ }.
(** [no_nested_borrows::new_pair1]:
Source: 'src/no_nested_borrows.rs', lines 454:0-454:46 *)
Definition new_pair1 : result (StructWithPair_t u32 u32) :=
- Return {| structWithPair_p := {| pair_x := 1%u32; pair_y := 2%u32 |} |}
+ Ok {| structWithPair_p := {| pair_x := 1%u32; pair_y := 2%u32 |} |}
.
(** [no_nested_borrows::test_constants]:
@@ -572,7 +566,7 @@ Definition test_constants : result unit :=
swp <- new_pair1;
if negb (swp.(structWithPair_p).(pair_x) s= 1%u32)
then Fail_ Failure
- else Return tt)))
+ else Ok tt)))
.
(** Unit test for [no_nested_borrows::test_constants] *)
@@ -581,7 +575,7 @@ Check (test_constants )%return.
(** [no_nested_borrows::test_weird_borrows1]:
Source: 'src/no_nested_borrows.rs', lines 471:0-471:28 *)
Definition test_weird_borrows1 : result unit :=
- Return tt.
+ Ok tt.
(** Unit test for [no_nested_borrows::test_weird_borrows1] *)
Check (test_weird_borrows1 )%return.
@@ -590,30 +584,30 @@ Check (test_weird_borrows1 )%return.
Source: 'src/no_nested_borrows.rs', lines 481:0-481:37 *)
Definition test_mem_replace (px : u32) : result u32 :=
let (y, _) := core_mem_replace u32 px 1%u32 in
- if negb (y s= 0%u32) then Fail_ Failure else Return 2%u32
+ if negb (y s= 0%u32) then Fail_ Failure else Ok 2%u32
.
(** [no_nested_borrows::test_shared_borrow_bool1]:
Source: 'src/no_nested_borrows.rs', lines 488:0-488:47 *)
Definition test_shared_borrow_bool1 (b : bool) : result u32 :=
- if b then Return 0%u32 else Return 1%u32
+ if b then Ok 0%u32 else Ok 1%u32
.
(** [no_nested_borrows::test_shared_borrow_bool2]:
Source: 'src/no_nested_borrows.rs', lines 501:0-501:40 *)
Definition test_shared_borrow_bool2 : result u32 :=
- Return 0%u32.
+ Ok 0%u32.
(** [no_nested_borrows::test_shared_borrow_enum1]:
Source: 'src/no_nested_borrows.rs', lines 516:0-516:52 *)
Definition test_shared_borrow_enum1 (l : List_t u32) : result u32 :=
- match l with | List_Cons _ _ => Return 1%u32 | List_Nil => Return 0%u32 end
+ match l with | List_Cons _ _ => Ok 1%u32 | List_Nil => Ok 0%u32 end
.
(** [no_nested_borrows::test_shared_borrow_enum2]:
Source: 'src/no_nested_borrows.rs', lines 528:0-528:40 *)
Definition test_shared_borrow_enum2 : result u32 :=
- Return 0%u32.
+ Ok 0%u32.
(** [no_nested_borrows::incr]:
Source: 'src/no_nested_borrows.rs', lines 539:0-539:24 *)
@@ -628,7 +622,7 @@ Definition call_incr (x : u32) : result u32 :=
(** [no_nested_borrows::read_then_incr]:
Source: 'src/no_nested_borrows.rs', lines 548:0-548:41 *)
Definition read_then_incr (x : u32) : result (u32 * u32) :=
- x1 <- u32_add x 1%u32; Return (x, x1)
+ x1 <- u32_add x 1%u32; Ok (x, x1)
.
(** [no_nested_borrows::Tuple]
@@ -638,14 +632,14 @@ Definition Tuple_t (T1 T2 : Type) : Type := T1 * T2.
(** [no_nested_borrows::use_tuple_struct]:
Source: 'src/no_nested_borrows.rs', lines 556:0-556:48 *)
Definition use_tuple_struct (x : Tuple_t u32 u32) : result (Tuple_t u32 u32) :=
- let (_, i) := x in Return (1%u32, i)
+ let (_, i) := x in Ok (1%u32, i)
.
(** [no_nested_borrows::create_tuple_struct]:
Source: 'src/no_nested_borrows.rs', lines 560:0-560:61 *)
Definition create_tuple_struct
(x : u32) (y : u64) : result (Tuple_t u32 u64) :=
- Return (x, y)
+ Ok (x, y)
.
(** [no_nested_borrows::IdType]
@@ -655,11 +649,11 @@ Definition IdType_t (T : Type) : Type := T.
(** [no_nested_borrows::use_id_type]:
Source: 'src/no_nested_borrows.rs', lines 567:0-567:40 *)
Definition use_id_type (T : Type) (x : IdType_t T) : result T :=
- Return x.
+ Ok x.
(** [no_nested_borrows::create_id_type]:
Source: 'src/no_nested_borrows.rs', lines 571:0-571:43 *)
Definition create_id_type (T : Type) (x : T) : result (IdType_t T) :=
- Return x.
+ Ok x.
End NoNestedBorrows.
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index 77276223..5995de15 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -16,7 +16,7 @@ Definition ref_incr (x : i32) : result i32 :=
(** [paper::test_incr]:
Source: 'src/paper.rs', lines 8:0-8:18 *)
Definition test_incr : result unit :=
- x <- ref_incr 0%i32; if negb (x s= 1%i32) then Fail_ Failure else Return tt
+ x <- ref_incr 0%i32; if negb (x s= 1%i32) then Fail_ Failure else Ok tt
.
(** Unit test for [paper::test_incr] *)
@@ -27,8 +27,8 @@ Check (test_incr )%return.
Definition choose
(T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) :=
if b
- then let back := fun (ret : T) => Return (ret, y) in Return (x, back)
- else let back := fun (ret : T) => Return (x, ret) in Return (y, back)
+ then let back := fun (ret : T) => Ok (ret, y) in Ok (x, back)
+ else let back := fun (ret : T) => Ok (x, ret) in Ok (y, back)
.
(** [paper::test_choose]:
@@ -44,7 +44,7 @@ Definition test_choose : result unit :=
let (x, y) := p1 in
if negb (x s= 1%i32)
then Fail_ Failure
- else if negb (y s= 0%i32) then Fail_ Failure else Return tt)
+ else if negb (y s= 0%i32) then Fail_ Failure else Ok tt)
.
(** Unit test for [paper::test_choose] *)
@@ -69,17 +69,14 @@ Fixpoint list_nth_mut
match l with
| List_Cons x tl =>
if i s= 0%u32
- then
- let back := fun (ret : T) => Return (List_Cons ret tl) in
- Return (x, back)
+ then let back := fun (ret : T) => Ok (List_Cons ret tl) in Ok (x, back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_mut T tl i1;
let (t, list_nth_mut_back) := p in
let back :=
- fun (ret : T) => tl1 <- list_nth_mut_back ret; Return (List_Cons x tl1)
- in
- Return (t, back))
+ fun (ret : T) => tl1 <- list_nth_mut_back ret; Ok (List_Cons x tl1) in
+ Ok (t, back))
| List_Nil => Fail_ Failure
end
.
@@ -89,7 +86,7 @@ Fixpoint list_nth_mut
Fixpoint sum (l : List_t i32) : result i32 :=
match l with
| List_Cons x tl => i <- sum tl; i32_add x i
- | List_Nil => Return 0%i32
+ | List_Nil => Ok 0%i32
end
.
@@ -103,7 +100,7 @@ Definition test_nth : result unit :=
x1 <- i32_add x 1%i32;
l2 <- list_nth_mut_back x1;
i <- sum l2;
- if negb (i s= 7%i32) then Fail_ Failure else Return tt
+ if negb (i s= 7%i32) then Fail_ Failure else Ok tt
.
(** Unit test for [paper::test_nth] *)
@@ -118,7 +115,7 @@ Definition call_choose (p : (u32 * u32)) : result u32 :=
pz1 <- u32_add pz 1%u32;
p2 <- choose_back pz1;
let (px1, _) := p2 in
- Return px1
+ Ok px1
.
End Paper.
diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v
index dfa09328..8af7f69c 100644
--- a/tests/coq/misc/PoloniusList.v
+++ b/tests/coq/misc/PoloniusList.v
@@ -27,15 +27,15 @@ Fixpoint get_list_at_x
match ls with
| List_Cons hd tl =>
if hd s= x
- then Return (List_Cons hd tl, Return)
+ then Ok (List_Cons hd tl, Ok)
else (
p <- get_list_at_x tl x;
let (l, get_list_at_x_back) := p in
let back :=
fun (ret : List_t u32) =>
- tl1 <- get_list_at_x_back ret; Return (List_Cons hd tl1) in
- Return (l, back))
- | List_Nil => Return (List_Nil, Return)
+ tl1 <- get_list_at_x_back ret; Ok (List_Cons hd tl1) in
+ Ok (l, back))
+ | List_Nil => Ok (List_Nil, Ok)
end
.
diff --git a/tests/coq/misc/Primitives.v b/tests/coq/misc/Primitives.v
index 990e27e4..e84d65ce 100644
--- a/tests/coq/misc/Primitives.v
+++ b/tests/coq/misc/Primitives.v
@@ -19,19 +19,19 @@ Inductive error :=
| OutOfFuel.
Inductive result A :=
- | Return : A -> result A
+ | Ok : A -> result A
| Fail_ : error -> result A.
-Arguments Return {_} a.
+Arguments Ok {_} a.
Arguments Fail_ {_}.
Definition bind {A B} (m: result A) (f: A -> result B) : result B :=
match m with
| Fail_ e => Fail_ e
- | Return x => f x
+ | Ok x => f x
end.
-Definition return_ {A: Type} (x: A) : result A := Return x.
+Definition return_ {A: Type} (x: A) : result A := Ok x.
Definition fail_ {A: Type} (e: error) : result A := Fail_ e.
Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
@@ -39,27 +39,27 @@ Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
(** Monadic assert *)
Definition massert (b: bool) : result unit :=
- if b then Return tt else Fail_ Failure.
+ if b then Ok tt else Fail_ Failure.
(** Normalize and unwrap a successful result (used for globals) *)
-Definition eval_result_refl {A} {x} (a: result A) (p: a = Return x) : A :=
- match a as r return (r = Return x -> A) with
- | Return a' => fun _ => a'
+Definition eval_result_refl {A} {x} (a: result A) (p: a = Ok x) : A :=
+ match a as r return (r = Ok x -> A) with
+ | Ok a' => fun _ => a'
| Fail_ e => fun p' =>
False_rect _ (eq_ind (Fail_ e)
(fun e : result A =>
match e with
- | Return _ => False
+ | Ok _ => False
| Fail_ e => True
end)
- I (Return x) p')
+ I (Ok x) p')
end p.
Notation "x %global" := (eval_result_refl x eq_refl) (at level 40).
Notation "x %return" := (eval_result_refl x eq_refl) (at level 40).
(* Sanity check *)
-Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3.
+Check (if true then Ok (1 + 2) else Fail_ Failure)%global = 3.
(*** Misc *)
@@ -236,7 +236,7 @@ Import Sumbool.
Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) :=
match sumbool_of_bool (scalar_in_bounds ty x) with
- | left H => Return (exist _ x (scalar_in_bounds_valid _ _ H))
+ | left H => Ok (exist _ x (scalar_in_bounds_valid _ _ H))
| right _ => Fail_ Failure
end.
@@ -544,9 +544,9 @@ Arguments core_ops_range_Range_end_ {_}.
(*** [alloc] *)
-Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Return x.
+Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Ok x.
Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result (T * (T -> result T)) :=
- Return (x, fun x => Return x).
+ Ok (x, fun x => Ok x).
(* Trait instance *)
Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {|
@@ -589,7 +589,7 @@ Definition array_index_mut_usize (T : Type) (n : usize) (a : array T n) (i : usi
result (T * (T -> result (array T n))) :=
match array_index_usize T n a i with
| Fail_ e => Fail_ e
- | Return x => Return (x, array_update_usize T n a i)
+ | Ok x => Ok (x, array_update_usize T n a i)
end.
(*** Slice *)
@@ -603,7 +603,7 @@ Definition slice_index_mut_usize (T : Type) (s : slice T) (i : usize) :
result (T * (T -> result (slice T))) :=
match slice_index_usize T s i with
| Fail_ e => Fail_ e
- | Return x => Return (x, slice_update_usize T s i)
+ | Ok x => Ok (x, slice_update_usize T s i)
end.
(*** Subslices *)
@@ -615,7 +615,7 @@ Definition array_to_slice_mut (T : Type) (n : usize) (a : array T n) :
result (slice T * (slice T -> result (array T n))) :=
match array_to_slice T n a with
| Fail_ e => Fail_ e
- | Return x => Return (x, array_from_slice T n a)
+ | Ok x => Ok (x, array_from_slice T n a)
end.
Axiom array_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize), result (slice T).
@@ -657,17 +657,17 @@ end end.
Definition alloc_vec_Vec_bind {A B} (v: alloc_vec_Vec A) (f: list A -> result (list B)) : result (alloc_vec_Vec B) :=
l <- f (alloc_vec_Vec_to_list v) ;
match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with
- | left H => Return (exist _ l (scalar_le_max_valid _ _ H))
+ | left H => Ok (exist _ l (scalar_le_max_valid _ _ H))
| right _ => Fail_ Failure
end.
Definition alloc_vec_Vec_push (T: Type) (v: alloc_vec_Vec T) (x: T) : result (alloc_vec_Vec T) :=
- alloc_vec_Vec_bind v (fun l => Return (l ++ [x])).
+ alloc_vec_Vec_bind v (fun l => Ok (l ++ [x])).
Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result (alloc_vec_Vec T) :=
alloc_vec_Vec_bind v (fun l =>
if to_Z i <? Z.of_nat (length l)
- then Return (list_update l (usize_to_nat i) x)
+ then Ok (list_update l (usize_to_nat i) x)
else Fail_ Failure).
(* Helper *)
@@ -679,8 +679,8 @@ Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i :
Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usize) :
result (T * (T -> result (alloc_vec_Vec T))) :=
match alloc_vec_Vec_index_usize v i with
- | Return x =>
- Return (x, alloc_vec_Vec_update_usize v i)
+ | Ok x =>
+ Ok (x, alloc_vec_Vec_update_usize v i)
| Fail_ e => Fail_ e
end.
@@ -717,7 +717,7 @@ Definition core_slice_index_Slice_index
x <- inst.(core_slice_index_SliceIndex_get) i s;
match x with
| None => Fail_ Failure
- | Some x => Return x
+ | Some x => Ok x
end.
(* [core::slice::index::Range:::get]: forward function *)
diff --git a/tests/coq/traits/Primitives.v b/tests/coq/traits/Primitives.v
index 990e27e4..e84d65ce 100644
--- a/tests/coq/traits/Primitives.v
+++ b/tests/coq/traits/Primitives.v
@@ -19,19 +19,19 @@ Inductive error :=
| OutOfFuel.
Inductive result A :=
- | Return : A -> result A
+ | Ok : A -> result A
| Fail_ : error -> result A.
-Arguments Return {_} a.
+Arguments Ok {_} a.
Arguments Fail_ {_}.
Definition bind {A B} (m: result A) (f: A -> result B) : result B :=
match m with
| Fail_ e => Fail_ e
- | Return x => f x
+ | Ok x => f x
end.
-Definition return_ {A: Type} (x: A) : result A := Return x.
+Definition return_ {A: Type} (x: A) : result A := Ok x.
Definition fail_ {A: Type} (e: error) : result A := Fail_ e.
Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
@@ -39,27 +39,27 @@ Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
(** Monadic assert *)
Definition massert (b: bool) : result unit :=
- if b then Return tt else Fail_ Failure.
+ if b then Ok tt else Fail_ Failure.
(** Normalize and unwrap a successful result (used for globals) *)
-Definition eval_result_refl {A} {x} (a: result A) (p: a = Return x) : A :=
- match a as r return (r = Return x -> A) with
- | Return a' => fun _ => a'
+Definition eval_result_refl {A} {x} (a: result A) (p: a = Ok x) : A :=
+ match a as r return (r = Ok x -> A) with
+ | Ok a' => fun _ => a'
| Fail_ e => fun p' =>
False_rect _ (eq_ind (Fail_ e)
(fun e : result A =>
match e with
- | Return _ => False
+ | Ok _ => False
| Fail_ e => True
end)
- I (Return x) p')
+ I (Ok x) p')
end p.
Notation "x %global" := (eval_result_refl x eq_refl) (at level 40).
Notation "x %return" := (eval_result_refl x eq_refl) (at level 40).
(* Sanity check *)
-Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3.
+Check (if true then Ok (1 + 2) else Fail_ Failure)%global = 3.
(*** Misc *)
@@ -236,7 +236,7 @@ Import Sumbool.
Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) :=
match sumbool_of_bool (scalar_in_bounds ty x) with
- | left H => Return (exist _ x (scalar_in_bounds_valid _ _ H))
+ | left H => Ok (exist _ x (scalar_in_bounds_valid _ _ H))
| right _ => Fail_ Failure
end.
@@ -544,9 +544,9 @@ Arguments core_ops_range_Range_end_ {_}.
(*** [alloc] *)
-Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Return x.
+Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Ok x.
Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result (T * (T -> result T)) :=
- Return (x, fun x => Return x).
+ Ok (x, fun x => Ok x).
(* Trait instance *)
Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {|
@@ -589,7 +589,7 @@ Definition array_index_mut_usize (T : Type) (n : usize) (a : array T n) (i : usi
result (T * (T -> result (array T n))) :=
match array_index_usize T n a i with
| Fail_ e => Fail_ e
- | Return x => Return (x, array_update_usize T n a i)
+ | Ok x => Ok (x, array_update_usize T n a i)
end.
(*** Slice *)
@@ -603,7 +603,7 @@ Definition slice_index_mut_usize (T : Type) (s : slice T) (i : usize) :
result (T * (T -> result (slice T))) :=
match slice_index_usize T s i with
| Fail_ e => Fail_ e
- | Return x => Return (x, slice_update_usize T s i)
+ | Ok x => Ok (x, slice_update_usize T s i)
end.
(*** Subslices *)
@@ -615,7 +615,7 @@ Definition array_to_slice_mut (T : Type) (n : usize) (a : array T n) :
result (slice T * (slice T -> result (array T n))) :=
match array_to_slice T n a with
| Fail_ e => Fail_ e
- | Return x => Return (x, array_from_slice T n a)
+ | Ok x => Ok (x, array_from_slice T n a)
end.
Axiom array_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize), result (slice T).
@@ -657,17 +657,17 @@ end end.
Definition alloc_vec_Vec_bind {A B} (v: alloc_vec_Vec A) (f: list A -> result (list B)) : result (alloc_vec_Vec B) :=
l <- f (alloc_vec_Vec_to_list v) ;
match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with
- | left H => Return (exist _ l (scalar_le_max_valid _ _ H))
+ | left H => Ok (exist _ l (scalar_le_max_valid _ _ H))
| right _ => Fail_ Failure
end.
Definition alloc_vec_Vec_push (T: Type) (v: alloc_vec_Vec T) (x: T) : result (alloc_vec_Vec T) :=
- alloc_vec_Vec_bind v (fun l => Return (l ++ [x])).
+ alloc_vec_Vec_bind v (fun l => Ok (l ++ [x])).
Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result (alloc_vec_Vec T) :=
alloc_vec_Vec_bind v (fun l =>
if to_Z i <? Z.of_nat (length l)
- then Return (list_update l (usize_to_nat i) x)
+ then Ok (list_update l (usize_to_nat i) x)
else Fail_ Failure).
(* Helper *)
@@ -679,8 +679,8 @@ Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i :
Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usize) :
result (T * (T -> result (alloc_vec_Vec T))) :=
match alloc_vec_Vec_index_usize v i with
- | Return x =>
- Return (x, alloc_vec_Vec_update_usize v i)
+ | Ok x =>
+ Ok (x, alloc_vec_Vec_update_usize v i)
| Fail_ e => Fail_ e
end.
@@ -717,7 +717,7 @@ Definition core_slice_index_Slice_index
x <- inst.(core_slice_index_SliceIndex_get) i s;
match x with
| None => Fail_ Failure
- | Some x => Return x
+ | Some x => Ok x
end.
(* [core::slice::index::Range:::get]: forward function *)
diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
index 0e942c7d..fb37a507 100644
--- a/tests/coq/traits/Traits.v
+++ b/tests/coq/traits/Traits.v
@@ -20,7 +20,7 @@ Arguments BoolTrait_t_get_bool { _ }.
(** [traits::{(traits::BoolTrait for bool)}::get_bool]:
Source: 'src/traits.rs', lines 12:4-12:30 *)
Definition boolTraitBool_get_bool (self : bool) : result bool :=
- Return self.
+ Ok self.
(** Trait implementation: [traits::{(traits::BoolTrait for bool)}]
Source: 'src/traits.rs', lines 11:0-11:23 *)
@@ -32,21 +32,21 @@ Definition BoolTraitBool : BoolTrait_t bool := {|
Source: 'src/traits.rs', lines 6:4-6:30 *)
Definition boolTrait_ret_true
{Self : Type} (self_clause : BoolTrait_t Self) (self : Self) : result bool :=
- Return true
+ Ok true
.
(** [traits::test_bool_trait_bool]:
Source: 'src/traits.rs', lines 17:0-17:44 *)
Definition test_bool_trait_bool (x : bool) : result bool :=
b <- boolTraitBool_get_bool x;
- if b then boolTrait_ret_true BoolTraitBool x else Return false
+ if b then boolTrait_ret_true BoolTraitBool x else Ok false
.
(** [traits::{(traits::BoolTrait for core::option::Option<T>)#1}::get_bool]:
Source: 'src/traits.rs', lines 23:4-23:30 *)
Definition boolTraitOption_get_bool
(T : Type) (self : option T) : result bool :=
- match self with | None => Return false | Some _ => Return true end
+ match self with | None => Ok false | Some _ => Ok true end
.
(** Trait implementation: [traits::{(traits::BoolTrait for core::option::Option<T>)#1}]
@@ -59,7 +59,7 @@ Definition BoolTraitOption (T : Type) : BoolTrait_t (option T) := {|
Source: 'src/traits.rs', lines 31:0-31:54 *)
Definition test_bool_trait_option (T : Type) (x : option T) : result bool :=
b <- boolTraitOption_get_bool T x;
- if b then boolTrait_ret_true (BoolTraitOption T) x else Return false
+ if b then boolTrait_ret_true (BoolTraitOption T) x else Ok false
.
(** [traits::test_bool_trait]:
@@ -81,7 +81,7 @@ Arguments ToU64_t_to_u64 { _ }.
(** [traits::{(traits::ToU64 for u64)#2}::to_u64]:
Source: 'src/traits.rs', lines 44:4-44:26 *)
Definition toU64U64_to_u64 (self : u64) : result u64 :=
- Return self.
+ Ok self.
(** Trait implementation: [traits::{(traits::ToU64 for u64)#2}]
Source: 'src/traits.rs', lines 43:0-43:18 *)
@@ -167,7 +167,7 @@ Arguments ToType_t_to_type { _ _ }.
(** [traits::{(traits::ToType<bool> for u64)#5}::to_type]:
Source: 'src/traits.rs', lines 93:4-93:28 *)
Definition toTypeU64Bool_to_type (self : u64) : result bool :=
- Return (self s> 0%u64)
+ Ok (self s> 0%u64)
.
(** Trait implementation: [traits::{(traits::ToType<bool> for u64)#5}]
@@ -238,7 +238,7 @@ Arguments TestType_test_TestTrait_t_test { _ }.
Source: 'src/traits.rs', lines 139:12-139:34 *)
Definition testType_test_TestTraittraitsTestTypetestTestType1_test
(self : TestType_test_TestType1_t) : result bool :=
- Return (self s> 1%u64)
+ Ok (self s> 1%u64)
.
(** Trait implementation: [traits::{traits::TestType<T>#6}::test::{(traits::{traits::TestType<T>#6}::test::TestTrait for traits::{traits::TestType<T>#6}::test::TestType1)}]
@@ -258,7 +258,7 @@ Definition testType_test
x1 <- toU64Inst.(ToU64_t_to_u64) x;
if x1 s> 0%u64
then testType_test_TestTraittraitsTestTypetestTestType1_test 0%u64
- else Return false
+ else Ok false
.
(** [traits::BoolWrapper]
@@ -285,7 +285,7 @@ Definition ToTypetraitsBoolWrapperT (T : Type) (toTypeBoolTInst : ToType_t bool
Source: 'src/traits.rs', lines 164:4-164:21 *)
Definition with_const_ty_len2_default_body (Self : Type) (LEN : usize)
: result usize :=
- Return 32%usize
+ Ok 32%usize
.
Definition with_const_ty_len2_default (Self : Type) (LEN : usize) : usize :=
(with_const_ty_len2_default_body Self LEN)%global
@@ -313,7 +313,7 @@ Arguments WithConstTy_t_f { _ _ }.
(** [traits::{(traits::WithConstTy<32: usize> for bool)#8}::LEN1]
Source: 'src/traits.rs', lines 175:4-175:21 *)
-Definition with_const_ty_bool32_len1_body : result usize := Return 12%usize.
+Definition with_const_ty_bool32_len1_body : result usize := Ok 12%usize.
Definition with_const_ty_bool32_len1 : usize :=
with_const_ty_bool32_len1_body%global
.
@@ -322,7 +322,7 @@ Definition with_const_ty_bool32_len1 : usize :=
Source: 'src/traits.rs', lines 180:4-180:39 *)
Definition withConstTyBool32_f
(i : u64) (a : array u8 32%usize) : result u64 :=
- Return i
+ Ok i
.
(** Trait implementation: [traits::{(traits::WithConstTy<32: usize> for bool)#8}]
@@ -342,7 +342,7 @@ Definition use_with_const_ty1
(H : Type) (LEN : usize) (withConstTyInst : WithConstTy_t H LEN) :
result usize
:=
- Return withConstTyInst.(WithConstTy_tWithConstTy_t_LEN1)
+ Ok withConstTyInst.(WithConstTy_tWithConstTy_t_LEN1)
.
(** [traits::use_with_const_ty2]:
@@ -352,7 +352,7 @@ Definition use_with_const_ty2
(w : withConstTyInst.(WithConstTy_tWithConstTy_t_W)) :
result unit
:=
- Return tt
+ Ok tt
.
(** [traits::use_with_const_ty3]:
@@ -368,7 +368,7 @@ Definition use_with_const_ty3
(** [traits::test_where1]:
Source: 'src/traits.rs', lines 193:0-193:40 *)
Definition test_where1 (T : Type) (_x : T) : result unit :=
- Return tt.
+ Ok tt.
(** [traits::test_where2]:
Source: 'src/traits.rs', lines 194:0-194:57 *)
@@ -376,7 +376,7 @@ Definition test_where2
(T : Type) (withConstTyT32Inst : WithConstTy_t T 32%usize) (_x : u32) :
result unit
:=
- Return tt
+ Ok tt
.
(** Trait declaration: [traits::ParentTrait0]
@@ -435,7 +435,7 @@ Definition order1
ParentTrait0_t U) :
result unit
:=
- Return tt
+ Ok tt
.
(** Trait declaration: [traits::ChildTrait1]
@@ -552,7 +552,7 @@ Definition ParentTrait2U32 : ParentTrait2_t u32 := {|
(** [traits::{(traits::ChildTrait2 for u32)#13}::convert]:
Source: 'src/traits.rs', lines 273:4-273:29 *)
Definition childTrait2U32_convert (x : u32) : result u32 :=
- Return x.
+ Ok x.
(** Trait implementation: [traits::{(traits::ChildTrait2 for u32)#13}]
Source: 'src/traits.rs', lines 272:0-272:24 *)
@@ -625,9 +625,7 @@ Arguments Trait_tTrait_t_LEN { _ }.
(** [traits::{(traits::Trait for @Array<T, N>)#14}::LEN]
Source: 'src/traits.rs', lines 315:4-315:20 *)
-Definition trait_array_len_body (T : Type) (N : usize) : result usize :=
- Return N
-.
+Definition trait_array_len_body (T : Type) (N : usize) : result usize := Ok N.
Definition trait_array_len (T : Type) (N : usize) : usize :=
(trait_array_len_body T N)%global
.
@@ -642,7 +640,7 @@ Definition TraitArray (T : Type) (N : usize) : Trait_t (array T N) := {|
Source: 'src/traits.rs', lines 319:4-319:20 *)
Definition traittraits_wrapper_len_body (T : Type) (traitInst : Trait_t T)
: result usize :=
- Return 0%usize
+ Ok 0%usize
.
Definition traittraits_wrapper_len (T : Type) (traitInst : Trait_t T)
: usize :=
@@ -659,7 +657,7 @@ Definition TraittraitsWrapper (T : Type) (traitInst : Trait_t T) : Trait_t
(** [traits::use_wrapper_len]:
Source: 'src/traits.rs', lines 322:0-322:43 *)
Definition use_wrapper_len (T : Type) (traitInst : Trait_t T) : result usize :=
- Return (TraittraitsWrapper T traitInst).(Trait_tTrait_t_LEN)
+ Ok (TraittraitsWrapper T traitInst).(Trait_tTrait_t_LEN)
.
(** [traits::Foo]
@@ -685,7 +683,7 @@ Arguments Core_result_Result_Err { _ _ }.
Source: 'src/traits.rs', lines 332:4-332:33 *)
Definition foo_foo_body (T U : Type) (traitInst : Trait_t T)
: result (core_result_Result_t T i32) :=
- Return (Core_result_Result_Err 0%i32)
+ Ok (Core_result_Result_Err 0%i32)
.
Definition foo_foo (T U : Type) (traitInst : Trait_t T)
: core_result_Result_t T i32 :=
@@ -696,14 +694,14 @@ Definition foo_foo (T U : Type) (traitInst : Trait_t T)
Source: 'src/traits.rs', lines 335:0-335:48 *)
Definition use_foo1
(T U : Type) (traitInst : Trait_t T) : result (core_result_Result_t T i32) :=
- Return (foo_foo T U traitInst)
+ Ok (foo_foo T U traitInst)
.
(** [traits::use_foo2]:
Source: 'src/traits.rs', lines 339:0-339:48 *)
Definition use_foo2
(T U : Type) (traitInst : Trait_t U) : result (core_result_Result_t U i32) :=
- Return (foo_foo U T traitInst)
+ Ok (foo_foo U T traitInst)
.
End Traits.
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 06:02:21 +0000