Merge pull request #123 from AeneasVerif/son/clean

Cleanup the code in preparation of the nested loops

2 files changed, 25 insertions, 25 deletions

diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index 6d9fef8e..3a3aeb96 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -12,10 +12,10 @@ def choose
   Result (T × (T → Result (T × T)))
   :=
   if b
-  then let back := fun ret => Result.ret (ret, y)
-       Result.ret (x, back)
-  else let back := fun ret => Result.ret (x, ret)
-       Result.ret (y, back)
+  then let back := fun ret => Result.ok (ret, y)
+       Result.ok (x, back)
+  else let back := fun ret => Result.ok (x, ret)
+       Result.ok (y, back)
 
 /- [demo::mul2_add1]:
    Source: 'src/demo.rs', lines 13:0-13:31 -/
@@ -43,7 +43,7 @@ def use_incr : Result Unit :=
   let x ← incr 0#u32
   let x1 ← incr x
   let _ ← incr x1
-  Result.ret ()
+  Result.ok ()
 
 /- [demo::CList]
    Source: 'src/demo.rs', lines 34:0-34:17 -/
@@ -57,7 +57,7 @@ divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
   match l with
   | CList.CCons x tl =>
     if i = 0#u32
-    then Result.ret x
+    then Result.ok x
     else do
          let i1 ← i - 1#u32
          list_nth T tl i1
@@ -73,8 +73,8 @@ divergent def list_nth_mut
   | CList.CCons x tl =>
     if i = 0#u32
     then
-      let back := fun ret => Result.ret (CList.CCons ret tl)
-      Result.ret (x, back)
+      let back := fun ret => Result.ok (CList.CCons ret tl)
+      Result.ok (x, back)
     else
       do
       let i1 ← i - 1#u32
@@ -83,8 +83,8 @@ divergent def list_nth_mut
         fun ret =>
           do
           let tl1 ← list_nth_mut_back ret
-          Result.ret (CList.CCons x tl1)
-      Result.ret (t, back)
+          Result.ok (CList.CCons x tl1)
+      Result.ok (t, back)
   | CList.CNil => Result.fail .panic
 
 /- [demo::list_nth_mut1]: loop 0:
@@ -97,8 +97,8 @@ divergent def list_nth_mut1_loop
   | CList.CCons x tl =>
     if i = 0#u32
     then
-      let back := fun ret => Result.ret (CList.CCons ret tl)
-      Result.ret (x, back)
+      let back := fun ret => Result.ok (CList.CCons ret tl)
+      Result.ok (x, back)
     else
       do
       let i1 ← i - 1#u32
@@ -106,8 +106,8 @@ divergent def list_nth_mut1_loop
       let back1 :=
         fun ret => do
                    let tl1 ← back ret
-                   Result.ret (CList.CCons x tl1)
-      Result.ret (t, back1)
+                   Result.ok (CList.CCons x tl1)
+      Result.ok (t, back1)
   | CList.CNil => Result.fail .panic
 
 /- [demo::list_nth_mut1]:
@@ -122,7 +122,7 @@ def list_nth_mut1
    Source: 'src/demo.rs', lines 80:0-80:28 -/
 divergent def i32_id (i : I32) : Result I32 :=
   if i = 0#i32
-  then Result.ret 0#i32
+  then Result.ok 0#i32
   else do
        let i1 ← i - 1#i32
        let i2 ← i32_id i1
@@ -142,9 +142,9 @@ divergent def list_tail
       fun ret =>
         do
         let tl1 ← list_tail_back ret
-        Result.ret (CList.CCons t tl1)
-    Result.ret (c, back)
-  | CList.CNil => Result.ret (CList.CNil, Result.ret)
+        Result.ok (CList.CCons t tl1)
+    Result.ok (c, back)
+  | CList.CNil => Result.ok (CList.CNil, Result.ok)
 
 /- Trait declaration: [demo::Counter]
    Source: 'src/demo.rs', lines 97:0-97:17 -/
@@ -156,7 +156,7 @@ structure Counter (Self : Type) where
 def CounterUsize.incr (self : Usize) : Result (Usize × Usize) :=
   do
   let self1 ← self + 1#usize
-  Result.ret (self, self1)
+  Result.ok (self, self1)
 
 /- Trait implementation: [demo::{(demo::Counter for usize)}]
    Source: 'src/demo.rs', lines 101:0-101:22 -/
diff --git a/tests/lean/Demo/Properties.lean b/tests/lean/Demo/Properties.lean
index e514ac3e..abdc2985 100644
--- a/tests/lean/Demo/Properties.lean
+++ b/tests/lean/Demo/Properties.lean
@@ -9,7 +9,7 @@ namespace demo
 
 -- @[pspec]
 theorem mul2_add1_spec (x : U32) (h : 2 * ↑x + 1 ≤ U32.max)
-  : ∃ y, mul2_add1 x = ret y ∧
+  : ∃ y, mul2_add1 x = ok y ∧
   ↑y = 2 * ↑x + (1 : Int)
   := by
   rw [mul2_add1]
@@ -18,7 +18,7 @@ theorem mul2_add1_spec (x : U32) (h : 2 * ↑x + 1 ≤ U32.max)
   simp; scalar_tac
 
 theorem use_mul2_add1_spec (x : U32) (y : U32) (h : 2 * ↑x + 1 + ↑y ≤ U32.max) :
-  ∃ z, use_mul2_add1 x y = ret z ∧
+  ∃ z, use_mul2_add1 x y = ok z ∧
   ↑z = 2 * ↑x + (1 : Int) + ↑y := by
   rw [use_mul2_add1]
   progress with mul2_add1_spec as ⟨ i ⟩
@@ -34,7 +34,7 @@ open CList
 
 theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
   (h : ↑i < l.to_list.len) :
-  ∃ x, list_nth T l i = ret x ∧
+  ∃ x, list_nth T l i = ok x ∧
   x = l.to_list.index ↑i
   := by
   rw [list_nth]
@@ -52,7 +52,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
       simp_all
 
 theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) :
-  ∃ y, i32_id x = ret y ∧ x.val = y.val := by
+  ∃ y, i32_id x = ok y ∧ x.val = y.val := by
   rw [i32_id]
   if hx : x = 0#i32 then
     simp_all
@@ -66,8 +66,8 @@ termination_by x.val.toNat
 decreasing_by scalar_decr_tac
 
 theorem list_tail_spec {T : Type} [Inhabited T] (l : CList T) :
-  ∃ back, list_tail T l = ret (CList.CNil, back) ∧
-  ∀ tl', ∃ l', back tl' = ret l' ∧ l'.to_list = l.to_list ++ tl'.to_list := by
+  ∃ back, list_tail T l = ok (CList.CNil, back) ∧
+  ∀ tl', ∃ l', back tl' = ok l' ∧ l'.to_list = l.to_list ++ tl'.to_list := by
   rw [list_tail]
   match l with
   | CNil =>