Merge branch 'main' into son_fixes2

1 files changed, 56 insertions, 46 deletions

diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index 175a523d..6b110193 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -9,33 +9,37 @@ Local Open Scope Primitives_scope.
 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 :=
+    (there is a single backward function, and the forward function returns ())
+    Source: 'src/paper.rs', lines 4:0-4:28 *)
+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
+(** [paper::test_incr]: forward function
+    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
 .
 
 (** 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 :=
+(** [paper::choose]: forward function
+    Source: 'src/paper.rs', lines 15:0-15:70 *)
+Definition choose (T : Type) (b : bool) (x : T) (y : T) : result T :=
   if b then Return x else Return y
 .
 
-(** [paper::choose]: backward function 0 *)
+(** [paper::choose]: backward function 0
+    Source: 'src/paper.rs', lines 15:0-15:70 *)
 Definition choose_back
   (T : Type) (b : bool) (x : T) (y : T) (ret : T) : result (T * T) :=
   if b then Return (ret, y) else Return (x, ret)
 .
 
-(** [paper::test_choose]: forward function *)
-Definition test_choose_fwd : result unit :=
-  z <- choose_fwd i32 true 0%i32 0%i32;
+(** [paper::test_choose]: forward function
+    Source: 'src/paper.rs', lines 23:0-23:20 *)
+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,74 +52,80 @@ Definition test_choose_fwd : result unit :=
 .
 
 (** Unit test for [paper::test_choose] *)
-Check (test_choose_fwd )%return.
+Check (test_choose )%return.
 
-(** [paper::List] *)
+(** [paper::List]
+    Source: 'src/paper.rs', lines 35:0-35:16 *)
 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 :=
+(** [paper::list_nth_mut]: forward function
+    Source: 'src/paper.rs', lines 42:0-42:67 *)
+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
 .
 
-(** [paper::list_nth_mut]: backward function 0 *)
+(** [paper::list_nth_mut]: backward function 0
+    Source: 'src/paper.rs', lines 42:0-42:67 *)
 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 :=
+(** [paper::sum]: forward function
+    Source: 'src/paper.rs', lines 57:0-57:32 *)
+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;
+(** [paper::test_nth]: forward function
+    Source: 'src/paper.rs', lines 68:0-68:17 *)
+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 :=
+(** [paper::call_choose]: forward function
+    Source: 'src/paper.rs', lines 76:0-76:44 *)
+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
   Return px0
 .
 
-End Paper .
+End Paper.