From 49117ba254679f98938223711810191c3f7d788f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 27 Oct 2023 13:34:03 +0200
Subject: Regenerate the Coq test files

---
 tests/coq/misc/Paper.v | 67 +++++++++++++++++++++++++-------------------------
 1 file changed, 33 insertions(+), 34 deletions(-)

(limited to 'tests/coq/misc/Paper.v')

diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index 175a523d..d397995b 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 {T} _ _.
+Arguments List_Nil {T}.
 
 (** [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
-- 
cgit v1.2.3


From 49ffc966cfdbd71f8c83a3c72ab81e1bb101f420 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 9 Nov 2023 16:24:07 +0100
Subject: Regenerate the Coq test files

---
 tests/coq/misc/Paper.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tests/coq/misc/Paper.v')

diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index d397995b..d3852e6b 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -55,8 +55,8 @@ Inductive List_t (T : Type) :=
 | List_Nil : List_t T
 .
 
-Arguments List_Cons {T} _ _.
-Arguments List_Nil {T}.
+Arguments List_Cons { _ }.
+Arguments List_Nil { _ }.
 
 (** [paper::list_nth_mut]: forward function *)
 Fixpoint list_nth_mut (T : Type) (l : List_t T) (i : u32) : result T :=
-- 
cgit v1.2.3