From ce8614be6bd96c51756bf5922b5dfd4c59650dd4 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz
Date: Thu, 30 May 2024 12:33:05 +0200
Subject: Implement two phases of loops join + collapse

---
 tests/coq/demo/Demo.v | 27 +--------------------------
 1 file changed, 1 insertion(+), 26 deletions(-)

(limited to 'tests/coq/demo')

diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index 8d8f840d..14b1ca9d 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -90,38 +90,13 @@ Fixpoint list_nth_mut
   end
 .
 
-(** [demo::list_nth_mut1]: loop 0:
-    Source: 'tests/src/demo.rs', lines 69:0-78:1 *)
-Fixpoint list_nth_mut1_loop
-  (T : Type) (n : nat) (l : CList_t T) (i : u32) :
-  result (T * (T -> result (CList_t T)))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n1 =>
-    match l with
-    | CList_CCons x tl =>
-      if i s= 0%u32
-      then let back := fun (ret : T) => Ok (CList_CCons ret tl) in Ok (x, back)
-      else (
-        i1 <- u32_sub i 1%u32;
-        p <- list_nth_mut1_loop T n1 tl i1;
-        let (t, back) := p in
-        let back1 := fun (ret : T) => tl1 <- back ret; Ok (CList_CCons x tl1)
-          in
-        Ok (t, back1))
-    | CList_CNil => Fail_ Failure
-    end
-  end
-.
-
 (** [demo::list_nth_mut1]:
     Source: 'tests/src/demo.rs', lines 69:0-69:77 *)
 Definition list_nth_mut1
   (T : Type) (n : nat) (l : CList_t T) (i : u32) :
   result (T * (T -> result (CList_t T)))
   :=
-  list_nth_mut1_loop T n l i
+  admit
 .
 
 (** [demo::i32_id]:
-- 
cgit v1.2.3


From 092dae81f5f90281b634e229102d2dff7f5c3fd7 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz
Date: Fri, 31 May 2024 13:09:37 +0200
Subject: Regenerate test output

---
 tests/coq/demo/Demo.v | 27 ++++++++++++++++++++++++++-
 1 file changed, 26 insertions(+), 1 deletion(-)

(limited to 'tests/coq/demo')

diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index 14b1ca9d..8d8f840d 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -90,13 +90,38 @@ Fixpoint list_nth_mut
   end
 .
 
+(** [demo::list_nth_mut1]: loop 0:
+    Source: 'tests/src/demo.rs', lines 69:0-78:1 *)
+Fixpoint list_nth_mut1_loop
+  (T : Type) (n : nat) (l : CList_t T) (i : u32) :
+  result (T * (T -> result (CList_t T)))
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    match l with
+    | CList_CCons x tl =>
+      if i s= 0%u32
+      then let back := fun (ret : T) => Ok (CList_CCons ret tl) in Ok (x, back)
+      else (
+        i1 <- u32_sub i 1%u32;
+        p <- list_nth_mut1_loop T n1 tl i1;
+        let (t, back) := p in
+        let back1 := fun (ret : T) => tl1 <- back ret; Ok (CList_CCons x tl1)
+          in
+        Ok (t, back1))
+    | CList_CNil => Fail_ Failure
+    end
+  end
+.
+
 (** [demo::list_nth_mut1]:
     Source: 'tests/src/demo.rs', lines 69:0-69:77 *)
 Definition list_nth_mut1
   (T : Type) (n : nat) (l : CList_t T) (i : u32) :
   result (T * (T -> result (CList_t T)))
   :=
-  admit
+  list_nth_mut1_loop T n l i
 .
 
 (** [demo::i32_id]:
-- 
cgit v1.2.3


From 2e3d1cdfde3e19af97e0d0fa47f92cfd66c688d9 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz
Date: Fri, 31 May 2024 14:25:23 +0200
Subject: Regenerate tests

---
 tests/coq/demo/_CoqProject | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tests/coq/demo')

diff --git a/tests/coq/demo/_CoqProject b/tests/coq/demo/_CoqProject
index 62554699..67e4f2a4 100644
--- a/tests/coq/demo/_CoqProject
+++ b/tests/coq/demo/_CoqProject
@@ -3,5 +3,5 @@
 -arg -w
 -arg all
 
-Demo.v
+Demo.v 
 Primitives.v
-- 
cgit v1.2.3