summaryrefslogtreecommitdiff
path: root/tests/coq/misc
diff options
context:
space:
mode:
Diffstat (limited to 'tests/coq/misc')
-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/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
8 files changed, 165 insertions, 185 deletions
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/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 *)
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 02:32:57 +0000