summaryrefslogtreecommitdiff
path: root/tests/coq
diff options
context:
space:
mode:
Diffstat (limited to 'tests/coq')
-rw-r--r--tests/coq/misc/External__Funs.v2
-rw-r--r--tests/coq/misc/NoNestedBorrows.v72
-rw-r--r--tests/coq/misc/Paper.v14
-rw-r--r--tests/coq/misc/Primitives.v42
4 files changed, 71 insertions, 59 deletions
diff --git a/tests/coq/misc/External__Funs.v b/tests/coq/misc/External__Funs.v
index cd03ae3d..cc9e9461 100644
--- a/tests/coq/misc/External__Funs.v
+++ b/tests/coq/misc/External__Funs.v
@@ -107,7 +107,7 @@ Definition test_swap_non_zero_fwd
p0 <- swap_back u32 x (0 %u32) st st0;
let (st1, p1) := p0 in
let (x0, _) := p1 in
- if x0 s= 0 %u32 then Fail_ else Return (st1, x0)
+ if x0 s= 0 %u32 then Fail_ Failure else Return (st1, x0)
.
End External__Funs .
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 774b8a1e..6d7f7987 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -95,7 +95,7 @@ Definition test3_fwd : result unit :=
x <- get_max_fwd (4 %u32) (3 %u32);
y <- get_max_fwd (10 %u32) (11 %u32);
z <- u32_add x y;
- if negb (z s= 15 %u32) then Fail_ else Return tt
+ if negb (z s= 15 %u32) then Fail_ Failure else Return tt
.
(** Unit test for [no_nested_borrows::test3] *)
@@ -103,14 +103,16 @@ Check (test3_fwd )%return.
(** [no_nested_borrows::test_neg1] *)
Definition test_neg1_fwd : result unit :=
- y <- i32_neg (3 %i32); if negb (y s= (-3) %i32) then Fail_ else Return tt .
+ y <- i32_neg (3 %i32);
+ if negb (y s= (-3) %i32) then Fail_ Failure else Return tt
+ .
(** Unit test for [no_nested_borrows::test_neg1] *)
Check (test_neg1_fwd )%return.
(** [no_nested_borrows::refs_test1] *)
Definition refs_test1_fwd : result unit :=
- if negb (1 %i32 s= 1 %i32) then Fail_ else Return tt .
+ if negb (1 %i32 s= 1 %i32) then Fail_ Failure else Return tt .
(** Unit test for [no_nested_borrows::refs_test1] *)
Check (refs_test1_fwd )%return.
@@ -118,14 +120,14 @@ Check (refs_test1_fwd )%return.
(** [no_nested_borrows::refs_test2] *)
Definition refs_test2_fwd : result unit :=
if negb (2 %i32 s= 2 %i32)
- then Fail_
+ then Fail_ Failure
else
if negb (0 %i32 s= 0 %i32)
- then Fail_
+ then Fail_ Failure
else
if negb (2 %i32 s= 2 %i32)
- then Fail_
- else if negb (2 %i32 s= 2 %i32) then Fail_ else Return tt
+ then Fail_ Failure
+ else if negb (2 %i32 s= 2 %i32) then Fail_ Failure else Return tt
.
(** Unit test for [no_nested_borrows::refs_test2] *)
@@ -141,7 +143,7 @@ Check (test_list1_fwd )%return.
Definition test_box1_fwd : result unit :=
let b := 1 %i32 in
let x := b in
- if negb (x s= 1 %i32) then Fail_ else Return tt
+ if negb (x s= 1 %i32) then Fail_ Failure else Return tt
.
(** Unit test for [no_nested_borrows::test_box1] *)
@@ -152,15 +154,17 @@ Definition copy_int_fwd (x : i32) : result i32 := Return x .
(** [no_nested_borrows::test_unreachable] *)
Definition test_unreachable_fwd (b : bool) : result unit :=
- if b then Fail_ else Return tt .
+ if b then Fail_ Failure else Return tt .
(** [no_nested_borrows::test_panic] *)
Definition test_panic_fwd (b : bool) : result unit :=
- if b then Fail_ else Return tt .
+ if b then Fail_ Failure else Return tt .
(** [no_nested_borrows::test_copy_int] *)
Definition test_copy_int_fwd : result unit :=
- y <- copy_int_fwd (0 %i32); if negb (0 %i32 s= y) then Fail_ else Return tt .
+ y <- copy_int_fwd (0 %i32);
+ if negb (0 %i32 s= y) then Fail_ Failure else Return tt
+ .
(** Unit test for [no_nested_borrows::test_copy_int] *)
Check (test_copy_int_fwd )%return.
@@ -173,7 +177,7 @@ Definition is_cons_fwd (T : Type) (l : List_t T) : result bool :=
Definition test_is_cons_fwd : result unit :=
let l := ListNil in
b <- is_cons_fwd i32 (ListCons (0 %i32) l);
- if negb b then Fail_ else Return tt
+ if negb b then Fail_ Failure else Return tt
.
(** Unit test for [no_nested_borrows::test_is_cons] *)
@@ -182,14 +186,18 @@ Check (test_is_cons_fwd )%return.
(** [no_nested_borrows::split_list] *)
Definition split_list_fwd
(T : Type) (l : List_t T) : result (T * (List_t T)) :=
- match l with | ListCons hd tl => Return (hd, tl) | ListNil => Fail_ end .
+ match l with
+ | ListCons hd tl => Return (hd, tl)
+ | ListNil => Fail_ Failure
+ end
+ .
(** [no_nested_borrows::test_split_list] *)
Definition test_split_list_fwd : result unit :=
let l := ListNil in
p <- split_list_fwd i32 (ListCons (0 %i32) l);
let (hd, _) := p in
- if negb (hd s= 0 %i32) then Fail_ else Return tt
+ if negb (hd s= 0 %i32) then Fail_ Failure else Return tt
.
(** Unit test for [no_nested_borrows::test_split_list] *)
@@ -209,13 +217,13 @@ Definition choose_test_fwd : result unit :=
z <- choose_fwd i32 true (0 %i32) (0 %i32);
z0 <- i32_add z 1 %i32;
if negb (z0 s= 1 %i32)
- then Fail_
+ then Fail_ Failure
else (
p <- choose_back i32 true (0 %i32) (0 %i32) z0;
let (x, y) := p in
if negb (x s= 1 %i32)
- then Fail_
- else if negb (y s= 0 %i32) then Fail_ else Return tt)
+ then Fail_ Failure
+ else if negb (y s= 0 %i32) then Fail_ Failure else Return tt)
.
(** Unit test for [no_nested_borrows::choose_test] *)
@@ -258,7 +266,7 @@ Fixpoint list_nth_shared_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
if i s= 0 %u32
then Return x
else (i0 <- u32_sub i 1 %u32; t <- list_nth_shared_fwd T tl i0; Return t)
- | ListNil => Fail_
+ | ListNil => Fail_ Failure
end
.
@@ -269,7 +277,7 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
if i s= 0 %u32
then Return x
else (i0 <- u32_sub i 1 %u32; t <- list_nth_mut_fwd T tl i0; Return t)
- | ListNil => Fail_
+ | ListNil => Fail_ Failure
end
.
@@ -284,7 +292,7 @@ Fixpoint list_nth_mut_back
i0 <- u32_sub i 1 %u32;
tl0 <- list_nth_mut_back T tl i0 ret;
Return (ListCons x tl0))
- | ListNil => Fail_
+ | ListNil => Fail_ Failure
end
.
@@ -311,31 +319,31 @@ Definition test_list_functions_fwd : result unit :=
let l1 := ListCons (1 %i32) l0 in
i <- list_length_fwd i32 (ListCons (0 %i32) l1);
if negb (i s= 3 %u32)
- then Fail_
+ then Fail_ Failure
else (
i0 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (0 %u32);
if negb (i0 s= 0 %i32)
- then Fail_
+ then Fail_ Failure
else (
i1 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (1 %u32);
if negb (i1 s= 1 %i32)
- then Fail_
+ then Fail_ Failure
else (
i2 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (2 %u32);
if negb (i2 s= 2 %i32)
- then Fail_
+ then Fail_ Failure
else (
ls <- list_nth_mut_back i32 (ListCons (0 %i32) l1) (1 %u32) (3 %i32);
i3 <- list_nth_shared_fwd i32 ls (0 %u32);
if negb (i3 s= 0 %i32)
- then Fail_
+ then Fail_ Failure
else (
i4 <- list_nth_shared_fwd i32 ls (1 %u32);
if negb (i4 s= 3 %i32)
- then Fail_
+ then Fail_ Failure
else (
i5 <- list_nth_shared_fwd i32 ls (2 %u32);
- if negb (i5 s= 2 %i32) then Fail_ else Return tt))))))
+ if negb (i5 s= 2 %i32) then Fail_ Failure else Return tt))))))
.
(** Unit test for [no_nested_borrows::test_list_functions] *)
@@ -436,28 +444,28 @@ Definition test_constants_fwd : result unit :=
| mkStruct_with_tuple_t p =>
let (i, _) := p in
if negb (i s= 1 %u32)
- then Fail_
+ then Fail_ Failure
else (
swt0 <- new_tuple2_fwd;
match swt0 with
| mkStruct_with_tuple_t p0 =>
let (i0, _) := p0 in
if negb (i0 s= 1 %i16)
- then Fail_
+ then Fail_ Failure
else (
swt1 <- new_tuple3_fwd;
match swt1 with
| mkStruct_with_tuple_t p1 =>
let (i1, _) := p1 in
if negb (i1 s= 1 %u64)
- then Fail_
+ then Fail_ Failure
else (
swp <- new_pair1_fwd;
match swp with
| mkStruct_with_pair_t p2 =>
match p2 with
| mkPair_t i2 i3 =>
- if negb (i2 s= 1 %u32) then Fail_ else Return tt
+ if negb (i2 s= 1 %u32) then Fail_ Failure else Return tt
end
end)
end)
@@ -477,7 +485,7 @@ Check (test_weird_borrows1_fwd )%return.
(** [no_nested_borrows::test_mem_replace] *)
Definition test_mem_replace_fwd_back (px : u32) : result u32 :=
let y := mem_replace_fwd u32 px (1 %u32) in
- if negb (y s= 0 %u32) then Fail_ else Return (2 %u32)
+ if negb (y s= 0 %u32) then Fail_ Failure else Return (2 %u32)
.
(** [no_nested_borrows::test_shared_borrow_bool1] *)
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index 25c01d7b..d0c99883 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -13,7 +13,7 @@ Definition ref_incr_fwd_back (x : i32) : result i32 :=
(** [paper::test_incr] *)
Definition test_incr_fwd : result unit :=
x <- ref_incr_fwd_back (0 %i32);
- if negb (x s= 1 %i32) then Fail_ else Return tt
+ if negb (x s= 1 %i32) then Fail_ Failure else Return tt
.
(** Unit test for [paper::test_incr] *)
@@ -33,13 +33,13 @@ Definition test_choose_fwd : result unit :=
z <- choose_fwd i32 true (0 %i32) (0 %i32);
z0 <- i32_add z 1 %i32;
if negb (z0 s= 1 %i32)
- then Fail_
+ then Fail_ Failure
else (
p <- choose_back i32 true (0 %i32) (0 %i32) z0;
let (x, y) := p in
if negb (x s= 1 %i32)
- then Fail_
- else if negb (y s= 0 %i32) then Fail_ else Return tt)
+ then Fail_ Failure
+ else if negb (y s= 0 %i32) then Fail_ Failure else Return tt)
.
(** Unit test for [paper::test_choose] *)
@@ -61,7 +61,7 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
if i s= 0 %u32
then Return x
else (i0 <- u32_sub i 1 %u32; t <- list_nth_mut_fwd T tl i0; Return t)
- | ListNil => Fail_
+ | ListNil => Fail_ Failure
end
.
@@ -76,7 +76,7 @@ Fixpoint list_nth_mut_back
i0 <- u32_sub i 1 %u32;
tl0 <- list_nth_mut_back T tl i0 ret;
Return (ListCons x tl0))
- | ListNil => Fail_
+ | ListNil => Fail_ Failure
end
.
@@ -97,7 +97,7 @@ Definition test_nth_fwd : result unit :=
x0 <- i32_add x 1 %i32;
l2 <- list_nth_mut_back i32 (ListCons (1 %i32) l1) (2 %u32) x0;
i <- sum_fwd l2;
- if negb (i s= 7 %i32) then Fail_ else Return tt
+ if negb (i s= 7 %i32) then Fail_ Failure else Return tt
.
(** Unit test for [paper::test_nth] *)
diff --git a/tests/coq/misc/Primitives.v b/tests/coq/misc/Primitives.v
index c27b8aed..9a97d6c7 100644
--- a/tests/coq/misc/Primitives.v
+++ b/tests/coq/misc/Primitives.v
@@ -13,40 +13,44 @@ Module Primitives.
Declare Scope Primitives_scope.
(*** Result *)
-
+
+Inductive error :=
+ | Failure
+ | OutOfFuel.
+
Inductive result A :=
| Return : A -> result A
- | Fail_ : result A.
+ | Fail_ : error -> result A.
Arguments Return {_} a.
Arguments Fail_ {_}.
Definition bind {A B} (m: result A) (f: A -> result B) : result B :=
match m with
- | Fail_ => Fail_
+ | Fail_ e => Fail_ e
| Return x => f x
end.
-Definition return_ {A: Type} (x: A) : result A := Return x .
-Definition fail_ {A: Type} : result A := Fail_ .
+Definition return_ {A: Type} (x: A) : result A := Return x.
+Definition fail_ {A: Type} (e: error) : result A := Fail_ e.
Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
(at level 61, c1 at next level, right associativity).
(** Monadic assert *)
Definition massert (b: bool) : result unit :=
- if b then Return tt else Fail_.
+ if b then Return 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'
- | Fail_ => fun p' =>
- False_rect _ (eq_ind Fail_
+ | Fail_ e => fun p' =>
+ False_rect _ (eq_ind (Fail_ e)
(fun e : result A =>
match e with
| Return _ => False
- | Fail_ => True
+ | Fail_ e => True
end)
I (Return x) p')
end p.
@@ -55,7 +59,7 @@ 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_)%global = 3.
+Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3.
(*** Misc *)
@@ -232,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))
- | right _ => Fail_
+ | right _ => Fail_ Failure
end.
Definition scalar_add {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (to_Z x + to_Z y).
@@ -242,7 +246,7 @@ Definition scalar_sub {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty
Definition scalar_mul {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (to_Z x * to_Z y).
Definition scalar_div {ty} (x y: scalar ty) : result (scalar ty) :=
- if to_Z y =? 0 then Fail_ else
+ if to_Z y =? 0 then Fail_ Failure else
mk_scalar ty (to_Z x / to_Z y).
Definition scalar_rem {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (Z.rem (to_Z x) (to_Z y)).
@@ -433,7 +437,7 @@ Definition vec_bind {A B} (v: vec A) (f: list A -> result (list B)) : result (ve
l <- f (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))
- | right _ => Fail_
+ | right _ => Fail_ Failure
end.
(* The **forward** function shouldn't be used *)
@@ -444,35 +448,35 @@ Definition vec_push_back (T: Type) (v: vec T) (x: T) : result (vec T) :=
(* The **forward** function shouldn't be used *)
Definition vec_insert_fwd (T: Type) (v: vec T) (i: usize) (x: T) : result unit :=
- if to_Z i <? vec_length v then Return tt else Fail_.
+ if to_Z i <? vec_length v then Return tt else Fail_ Failure.
Definition vec_insert_back (T: Type) (v: vec T) (i: usize) (x: T) : result (vec T) :=
vec_bind v (fun l =>
if to_Z i <? Z.of_nat (length l)
then Return (list_update l (usize_to_nat i) x)
- else Fail_).
+ else Fail_ Failure).
(* The **backward** function shouldn't be used *)
Definition vec_index_fwd (T: Type) (v: vec T) (i: usize) : result T :=
match nth_error (vec_to_list v) (usize_to_nat i) with
| Some n => Return n
- | None => Fail_
+ | None => Fail_ Failure
end.
Definition vec_index_back (T: Type) (v: vec T) (i: usize) (x: T) : result unit :=
- if to_Z i <? vec_length v then Return tt else Fail_.
+ if to_Z i <? vec_length v then Return tt else Fail_ Failure.
(* The **backward** function shouldn't be used *)
Definition vec_index_mut_fwd (T: Type) (v: vec T) (i: usize) : result T :=
match nth_error (vec_to_list v) (usize_to_nat i) with
| Some n => Return n
- | None => Fail_
+ | None => Fail_ Failure
end.
Definition vec_index_mut_back (T: Type) (v: vec T) (i: usize) (x: T) : result (vec T) :=
vec_bind v (fun l =>
if to_Z i <? Z.of_nat (length l)
then Return (list_update l (usize_to_nat i) x)
- else Fail_).
+ else Fail_ Failure).
End Primitives.
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 15:29:59 +0000