Merge pull request #123 from AeneasVerif/son/clean

Cleanup the code in preparation of the nested loops

2 files changed, 55 insertions, 55 deletions

diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 8e299800..79da6e80 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -15,7 +15,7 @@ Module HashmapMain_Funs.
 (** [hashmap_main::hashmap::hash_key]:
     Source: 'src/hashmap.rs', lines 27:0-27:32 *)
 Definition hashmap_hash_key (k : usize) : result usize :=
-  Return k.
+  Ok k.
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]: loop 0:
     Source: 'src/hashmap.rs', lines 50:4-56:5 *)
@@ -32,7 +32,7 @@ Fixpoint hashmap_HashMap_allocate_slots_loop
       slots1 <- alloc_vec_Vec_push (hashmap_List_t T) slots Hashmap_List_Nil;
       n3 <- usize_sub n1 1%usize;
       hashmap_HashMap_allocate_slots_loop T n2 slots1 n3)
-    else Return slots
+    else Ok slots
   end
 .
 
@@ -58,7 +58,7 @@ Definition hashmap_HashMap_new_with_capacity
       capacity;
   i <- usize_mul capacity max_load_dividend;
   i1 <- usize_div i max_load_divisor;
-  Return
+  Ok
     {|
       hashmap_HashMap_num_entries := 0%usize;
       hashmap_HashMap_max_load_factor := (max_load_dividend, max_load_divisor);
@@ -94,7 +94,7 @@ Fixpoint hashmap_HashMap_clear_loop
       i2 <- usize_add i 1%usize;
       slots1 <- index_mut_back Hashmap_List_Nil;
       hashmap_HashMap_clear_loop T n1 slots1 i2)
-    else Return slots
+    else Ok slots
   end
 .
 
@@ -105,7 +105,7 @@ Definition hashmap_HashMap_clear
   result (hashmap_HashMap_t T)
   :=
   hm <- hashmap_HashMap_clear_loop T n self.(hashmap_HashMap_slots) 0%usize;
-  Return
+  Ok
     {|
       hashmap_HashMap_num_entries := 0%usize;
       hashmap_HashMap_max_load_factor := self.(hashmap_HashMap_max_load_factor);
@@ -118,7 +118,7 @@ Definition hashmap_HashMap_clear
     Source: 'src/hashmap.rs', lines 90:4-90:30 *)
 Definition hashmap_HashMap_len
   (T : Type) (self : hashmap_HashMap_t T) : result usize :=
-  Return self.(hashmap_HashMap_num_entries)
+  Ok self.(hashmap_HashMap_num_entries)
 .
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_in_list]: loop 0:
@@ -133,13 +133,13 @@ Fixpoint hashmap_HashMap_insert_in_list_loop
     match ls with
     | Hashmap_List_Cons ckey cvalue tl =>
       if ckey s= key
-      then Return (false, Hashmap_List_Cons ckey value tl)
+      then Ok (false, Hashmap_List_Cons ckey value tl)
       else (
         p <- hashmap_HashMap_insert_in_list_loop T n1 key value tl;
         let (b, tl1) := p in
-        Return (b, Hashmap_List_Cons ckey cvalue tl1))
+        Ok (b, Hashmap_List_Cons ckey cvalue tl1))
     | Hashmap_List_Nil =>
-      Return (true, Hashmap_List_Cons key value Hashmap_List_Nil)
+      Ok (true, Hashmap_List_Cons key value Hashmap_List_Nil)
     end
   end
 .
@@ -173,7 +173,7 @@ Definition hashmap_HashMap_insert_no_resize
   then (
     i1 <- usize_add self.(hashmap_HashMap_num_entries) 1%usize;
     v <- index_mut_back l1;
-    Return
+    Ok
       {|
         hashmap_HashMap_num_entries := i1;
         hashmap_HashMap_max_load_factor :=
@@ -183,7 +183,7 @@ Definition hashmap_HashMap_insert_no_resize
       |})
   else (
     v <- index_mut_back l1;
-    Return
+    Ok
       {|
         hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries);
         hashmap_HashMap_max_load_factor :=
@@ -206,7 +206,7 @@ Fixpoint hashmap_HashMap_move_elements_from_list_loop
     | Hashmap_List_Cons k v tl =>
       ntable1 <- hashmap_HashMap_insert_no_resize T n1 ntable k v;
       hashmap_HashMap_move_elements_from_list_loop T n1 ntable1 tl
-    | Hashmap_List_Nil => Return ntable
+    | Hashmap_List_Nil => Ok ntable
     end
   end
 .
@@ -243,7 +243,7 @@ Fixpoint hashmap_HashMap_move_elements_loop
       i2 <- usize_add i 1%usize;
       slots1 <- index_mut_back l1;
       hashmap_HashMap_move_elements_loop T n1 ntable1 slots1 i2)
-    else Return (ntable, slots)
+    else Ok (ntable, slots)
   end
 .
 
@@ -277,7 +277,7 @@ Definition hashmap_HashMap_try_resize
       hashmap_HashMap_move_elements T n ntable self.(hashmap_HashMap_slots)
         0%usize;
     let (ntable1, _) := p in
-    Return
+    Ok
       {|
         hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries);
         hashmap_HashMap_max_load_factor := (i, i1);
@@ -285,7 +285,7 @@ Definition hashmap_HashMap_try_resize
         hashmap_HashMap_slots := ntable1.(hashmap_HashMap_slots)
       |})
   else
-    Return
+    Ok
       {|
         hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries);
         hashmap_HashMap_max_load_factor := (i, i1);
@@ -304,7 +304,7 @@ Definition hashmap_HashMap_insert
   i <- hashmap_HashMap_len T self1;
   if i s> self1.(hashmap_HashMap_max_load)
   then hashmap_HashMap_try_resize T n self1
-  else Return self1
+  else Ok self1
 .
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
@@ -317,9 +317,9 @@ Fixpoint hashmap_HashMap_contains_key_in_list_loop
     match ls with
     | Hashmap_List_Cons ckey _ tl =>
       if ckey s= key
-      then Return true
+      then Ok true
       else hashmap_HashMap_contains_key_in_list_loop T n1 key tl
-    | Hashmap_List_Nil => Return false
+    | Hashmap_List_Nil => Ok false
     end
   end
 .
@@ -357,7 +357,7 @@ Fixpoint hashmap_HashMap_get_in_list_loop
     match ls with
     | Hashmap_List_Cons ckey cvalue tl =>
       if ckey s= key
-      then Return cvalue
+      then Ok cvalue
       else hashmap_HashMap_get_in_list_loop T n1 key tl
     | Hashmap_List_Nil => Fail_ Failure
     end
@@ -398,15 +398,15 @@ Fixpoint hashmap_HashMap_get_mut_in_list_loop
     | Hashmap_List_Cons ckey cvalue tl =>
       if ckey s= key
       then
-        let back := fun (ret : T) => Return (Hashmap_List_Cons ckey ret tl) in
-        Return (cvalue, back)
+        let back := fun (ret : T) => Ok (Hashmap_List_Cons ckey ret tl) in
+        Ok (cvalue, back)
       else (
         p <- hashmap_HashMap_get_mut_in_list_loop T n1 tl key;
         let (t, back) := p in
         let back1 :=
           fun (ret : T) =>
-            tl1 <- back ret; Return (Hashmap_List_Cons ckey cvalue tl1) in
-        Return (t, back1))
+            tl1 <- back ret; Ok (Hashmap_List_Cons ckey cvalue tl1) in
+        Ok (t, back1))
     | Hashmap_List_Nil => Fail_ Failure
     end
   end
@@ -441,7 +441,7 @@ Definition hashmap_HashMap_get_mut
     fun (ret : T) =>
       l1 <- get_mut_in_list_back ret;
       v <- index_mut_back l1;
-      Return
+      Ok
         {|
           hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries);
           hashmap_HashMap_max_load_factor :=
@@ -449,7 +449,7 @@ Definition hashmap_HashMap_get_mut
           hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load);
           hashmap_HashMap_slots := v
         |} in
-  Return (t, back)
+  Ok (t, back)
 .
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0:
@@ -469,14 +469,14 @@ Fixpoint hashmap_HashMap_remove_from_list_loop
           core_mem_replace (hashmap_List_t T) (Hashmap_List_Cons ckey t tl)
             Hashmap_List_Nil in
         match mv_ls with
-        | Hashmap_List_Cons _ cvalue tl1 => Return (Some cvalue, tl1)
+        | Hashmap_List_Cons _ cvalue tl1 => Ok (Some cvalue, tl1)
         | Hashmap_List_Nil => Fail_ Failure
         end
       else (
         p <- hashmap_HashMap_remove_from_list_loop T n1 key tl;
         let (o, tl1) := p in
-        Return (o, Hashmap_List_Cons ckey t tl1))
-    | Hashmap_List_Nil => Return (None, Hashmap_List_Nil)
+        Ok (o, Hashmap_List_Cons ckey t tl1))
+    | Hashmap_List_Nil => Ok (None, Hashmap_List_Nil)
     end
   end
 .
@@ -509,7 +509,7 @@ Definition hashmap_HashMap_remove
   match x with
   | None =>
     v <- index_mut_back l1;
-    Return (None,
+    Ok (None,
       {|
         hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries);
         hashmap_HashMap_max_load_factor :=
@@ -520,7 +520,7 @@ Definition hashmap_HashMap_remove
   | Some x1 =>
     i1 <- usize_sub self.(hashmap_HashMap_num_entries) 1%usize;
     v <- index_mut_back l1;
-    Return (Some x1,
+    Ok (Some x1,
       {|
         hashmap_HashMap_num_entries := i1;
         hashmap_HashMap_max_load_factor :=
@@ -567,7 +567,7 @@ Definition hashmap_test1 (n : nat) : result unit :=
             then Fail_ Failure
             else (
               i4 <- hashmap_HashMap_get u64 n hm6 1056%usize;
-              if negb (i4 s= 256%u64) then Fail_ Failure else Return tt)))
+              if negb (i4 s= 256%u64) then Fail_ Failure else Ok tt)))
       end))
 .
 
@@ -584,6 +584,6 @@ Definition insert_on_disk
 (** [hashmap_main::main]:
     Source: 'src/hashmap_main.rs', lines 16:0-16:13 *)
 Definition main : result unit :=
-  Return tt.
+  Ok tt.
 
 End HashmapMain_Funs.
diff --git a/tests/coq/hashmap_on_disk/Primitives.v b/tests/coq/hashmap_on_disk/Primitives.v
index 990e27e4..e84d65ce 100644
--- a/tests/coq/hashmap_on_disk/Primitives.v
+++ b/tests/coq/hashmap_on_disk/Primitives.v
@@ -19,19 +19,19 @@ Inductive error :=
   | OutOfFuel.
 
 Inductive result A :=
-  | Return : A -> result A
+  | Ok : A -> result A
   | Fail_ : error -> result A.
 
-Arguments Return {_} a.
+Arguments Ok {_} a.
 Arguments Fail_ {_}.
 
 Definition bind {A B} (m: result A) (f: A -> result B) : result B :=
   match m with
   | Fail_ e => Fail_ e
-  | Return x => f x
+  | Ok x => f x
   end.
 
-Definition return_ {A: Type} (x: A) : result A := Return x.
+Definition return_ {A: Type} (x: A) : result A := Ok x.
 Definition fail_ {A: Type} (e: error) : result A := Fail_ e.
 
 Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
@@ -39,27 +39,27 @@ Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
 
 (** Monadic assert *)
 Definition massert (b: bool) : result unit :=
-  if b then Return tt else Fail_ Failure.
+  if b then Ok tt else Fail_ Failure.
 
 (** Normalize and unwrap a successful result (used for globals) *)
-Definition eval_result_refl {A} {x} (a: result A) (p: a = Return x) : A :=
-  match a as r return (r = Return x -> A) with
-  | Return a' => fun _  => a'
+Definition eval_result_refl {A} {x} (a: result A) (p: a = Ok x) : A :=
+  match a as r return (r = Ok x -> A) with
+  | Ok a' => fun _  => a'
   | Fail_ e   => fun p' =>
       False_rect _ (eq_ind (Fail_ e)
           (fun e : result A =>
           match e with
-          | Return _ => False
+          | Ok _ => False
           | Fail_ e => True
           end)
-        I (Return x) p')
+        I (Ok x) p')
   end p.
 
 Notation "x %global" := (eval_result_refl x eq_refl) (at level 40).
 Notation "x %return" := (eval_result_refl x eq_refl) (at level 40).
 
 (* Sanity check *)
-Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3.
+Check (if true then Ok (1 + 2) else Fail_ Failure)%global = 3.
 
 (*** Misc *)
 
@@ -236,7 +236,7 @@ Import Sumbool.
 
 Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) :=
   match sumbool_of_bool (scalar_in_bounds ty x) with
-  | left H => Return (exist _ x (scalar_in_bounds_valid _ _ H))
+  | left H => Ok (exist _ x (scalar_in_bounds_valid _ _ H))
   | right _ => Fail_ Failure
   end.
 
@@ -544,9 +544,9 @@ Arguments core_ops_range_Range_end_ {_}.
 
 (*** [alloc] *)
 
-Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Return x.
+Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Ok x.
 Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result (T * (T -> result T)) :=
-  Return (x, fun x => Return x).
+  Ok (x, fun x => Ok x).
 
 (* Trait instance *)
 Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {|
@@ -589,7 +589,7 @@ Definition array_index_mut_usize (T : Type) (n : usize) (a : array T n) (i : usi
   result (T * (T -> result (array T n))) :=
   match array_index_usize T n a i with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, array_update_usize T n a i)
+  | Ok x => Ok (x, array_update_usize T n a i)
   end.
 
 (*** Slice *)
@@ -603,7 +603,7 @@ Definition slice_index_mut_usize (T : Type) (s : slice T) (i : usize) :
   result (T * (T -> result (slice T))) :=
   match slice_index_usize T s i with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, slice_update_usize T s i)
+  | Ok x => Ok (x, slice_update_usize T s i)
   end.
 
 (*** Subslices *)
@@ -615,7 +615,7 @@ Definition array_to_slice_mut (T : Type) (n : usize) (a : array T n) :
   result (slice T * (slice T -> result (array T n))) :=
   match array_to_slice T n a with
   | Fail_ e => Fail_ e
-  | Return x => Return (x, array_from_slice T n a)
+  | Ok x => Ok (x, array_from_slice T n a)
   end.
 
 Axiom array_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize), result (slice T).
@@ -657,17 +657,17 @@ end end.
 Definition alloc_vec_Vec_bind {A B} (v: alloc_vec_Vec A) (f: list A -> result (list B)) : result (alloc_vec_Vec B) :=
   l <- f (alloc_vec_Vec_to_list v) ;
   match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with
-  | left H => Return (exist _ l (scalar_le_max_valid _ _ H))
+  | left H => Ok (exist _ l (scalar_le_max_valid _ _ H))
   | right _ => Fail_ Failure
   end.
 
 Definition alloc_vec_Vec_push (T: Type) (v: alloc_vec_Vec T) (x: T) : result (alloc_vec_Vec T) :=
-  alloc_vec_Vec_bind v (fun l => Return (l ++ [x])).
+  alloc_vec_Vec_bind v (fun l => Ok (l ++ [x])).
 
 Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result (alloc_vec_Vec T) :=
   alloc_vec_Vec_bind v (fun l =>
     if to_Z i <? Z.of_nat (length l)
-    then Return (list_update l (usize_to_nat i) x)
+    then Ok (list_update l (usize_to_nat i) x)
     else Fail_ Failure).
 
 (* Helper *)
@@ -679,8 +679,8 @@ Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i :
 Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usize) :
   result (T * (T -> result (alloc_vec_Vec T))) :=
   match alloc_vec_Vec_index_usize v i with
-  | Return x =>
-    Return (x, alloc_vec_Vec_update_usize v i)
+  | Ok x =>
+    Ok (x, alloc_vec_Vec_update_usize v i)
   | Fail_ e => Fail_ e
   end.
 
@@ -717,7 +717,7 @@ Definition core_slice_index_Slice_index
   x <- inst.(core_slice_index_SliceIndex_get) i s;
   match x with
   | None => Fail_ Failure
-  | Some x => Return x
+  | Some x => Ok x
   end.
 
 (* [core::slice::index::Range:::get]: forward function *)