summaryrefslogtreecommitdiff
path: root/tests/coq/misc/Paper.v
diff options
context:
space:
mode:
Diffstat (limited to 'tests/coq/misc/Paper.v')
-rw-r--r--tests/coq/misc/Paper.v67
1 files changed, 33 insertions, 34 deletions
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index 175a523d..d3852e6b 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -10,20 +10,19 @@ Module Paper.
(** [paper::ref_incr]: merged forward/backward function
(there is a single backward function, and the forward function returns ()) *)
-Definition ref_incr_fwd_back (x : i32) : result i32 :=
+Definition ref_incr (x : i32) : result i32 :=
i32_add x 1%i32.
(** [paper::test_incr]: forward function *)
-Definition test_incr_fwd : result unit :=
- x <- ref_incr_fwd_back 0%i32;
- if negb (x s= 1%i32) then Fail_ Failure else Return tt
+Definition test_incr : result unit :=
+ x <- ref_incr 0%i32; if negb (x s= 1%i32) then Fail_ Failure else Return tt
.
(** Unit test for [paper::test_incr] *)
-Check (test_incr_fwd )%return.
+Check (test_incr )%return.
(** [paper::choose]: forward function *)
-Definition choose_fwd (T : Type) (b : bool) (x : T) (y : T) : result T :=
+Definition choose (T : Type) (b : bool) (x : T) (y : T) : result T :=
if b then Return x else Return y
.
@@ -34,8 +33,8 @@ Definition choose_back
.
(** [paper::test_choose]: forward function *)
-Definition test_choose_fwd : result unit :=
- z <- choose_fwd i32 true 0%i32 0%i32;
+Definition test_choose : result unit :=
+ z <- choose i32 true 0%i32 0%i32;
z0 <- i32_add z 1%i32;
if negb (z0 s= 1%i32)
then Fail_ Failure
@@ -48,25 +47,25 @@ Definition test_choose_fwd : result unit :=
.
(** Unit test for [paper::test_choose] *)
-Check (test_choose_fwd )%return.
+Check (test_choose )%return.
(** [paper::List] *)
Inductive List_t (T : Type) :=
-| ListCons : T -> List_t T -> List_t T
-| ListNil : List_t T
+| List_Cons : T -> List_t T -> List_t T
+| List_Nil : List_t T
.
-Arguments ListCons {T} _ _.
-Arguments ListNil {T}.
+Arguments List_Cons { _ }.
+Arguments List_Nil { _ }.
(** [paper::list_nth_mut]: forward function *)
-Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
+Fixpoint list_nth_mut (T : Type) (l : List_t T) (i : u32) : result T :=
match l with
- | ListCons x tl =>
+ | List_Cons x tl =>
if i s= 0%u32
then Return x
- else (i0 <- u32_sub i 1%u32; list_nth_mut_fwd T tl i0)
- | ListNil => Fail_ Failure
+ else (i0 <- u32_sub i 1%u32; list_nth_mut T tl i0)
+ | List_Nil => Fail_ Failure
end
.
@@ -74,44 +73,44 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
Fixpoint list_nth_mut_back
(T : Type) (l : List_t T) (i : u32) (ret : T) : result (List_t T) :=
match l with
- | ListCons x tl =>
+ | List_Cons x tl =>
if i s= 0%u32
- then Return (ListCons ret tl)
+ then Return (List_Cons ret tl)
else (
i0 <- u32_sub i 1%u32;
tl0 <- list_nth_mut_back T tl i0 ret;
- Return (ListCons x tl0))
- | ListNil => Fail_ Failure
+ Return (List_Cons x tl0))
+ | List_Nil => Fail_ Failure
end
.
(** [paper::sum]: forward function *)
-Fixpoint sum_fwd (l : List_t i32) : result i32 :=
+Fixpoint sum (l : List_t i32) : result i32 :=
match l with
- | ListCons x tl => i <- sum_fwd tl; i32_add x i
- | ListNil => Return 0%i32
+ | List_Cons x tl => i <- sum tl; i32_add x i
+ | List_Nil => Return 0%i32
end
.
(** [paper::test_nth]: forward function *)
-Definition test_nth_fwd : result unit :=
- let l := ListNil in
- let l0 := ListCons 3%i32 l in
- let l1 := ListCons 2%i32 l0 in
- x <- list_nth_mut_fwd i32 (ListCons 1%i32 l1) 2%u32;
+Definition test_nth : result unit :=
+ let l := List_Nil in
+ let l0 := List_Cons 3%i32 l in
+ let l1 := List_Cons 2%i32 l0 in
+ x <- list_nth_mut i32 (List_Cons 1%i32 l1) 2%u32;
x0 <- i32_add x 1%i32;
- l2 <- list_nth_mut_back i32 (ListCons 1%i32 l1) 2%u32 x0;
- i <- sum_fwd l2;
+ l2 <- list_nth_mut_back i32 (List_Cons 1%i32 l1) 2%u32 x0;
+ i <- sum l2;
if negb (i s= 7%i32) then Fail_ Failure else Return tt
.
(** Unit test for [paper::test_nth] *)
-Check (test_nth_fwd )%return.
+Check (test_nth )%return.
(** [paper::call_choose]: forward function *)
-Definition call_choose_fwd (p : (u32 * u32)) : result u32 :=
+Definition call_choose (p : (u32 * u32)) : result u32 :=
let (px, py) := p in
- pz <- choose_fwd u32 true px py;
+ pz <- choose u32 true px py;
pz0 <- u32_add pz 1%u32;
p0 <- choose_back u32 true px py pz0;
let (px0, _) := p0 in