Merge pull request #123 from AeneasVerif/son/clean

Cleanup the code in preparation of the nested loops

2 files changed, 47 insertions, 49 deletions

diff --git a/tests/coq/traits/Primitives.v b/tests/coq/traits/Primitives.v
index 990e27e4..e84d65ce 100644
--- a/tests/coq/traits/Primitives.v
+++ b/tests/coq/traits/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 *)
diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
index 0e942c7d..fb37a507 100644
--- a/tests/coq/traits/Traits.v
+++ b/tests/coq/traits/Traits.v
@@ -20,7 +20,7 @@ Arguments BoolTrait_t_get_bool { _ }.
 (** [traits::{(traits::BoolTrait for bool)}::get_bool]:
     Source: 'src/traits.rs', lines 12:4-12:30 *)
 Definition boolTraitBool_get_bool (self : bool) : result bool :=
-  Return self.
+  Ok self.
 
 (** Trait implementation: [traits::{(traits::BoolTrait for bool)}]
     Source: 'src/traits.rs', lines 11:0-11:23 *)
@@ -32,21 +32,21 @@ Definition BoolTraitBool : BoolTrait_t bool := {|
     Source: 'src/traits.rs', lines 6:4-6:30 *)
 Definition boolTrait_ret_true
   {Self : Type} (self_clause : BoolTrait_t Self) (self : Self) : result bool :=
-  Return true
+  Ok true
 .
 
 (** [traits::test_bool_trait_bool]:
     Source: 'src/traits.rs', lines 17:0-17:44 *)
 Definition test_bool_trait_bool (x : bool) : result bool :=
   b <- boolTraitBool_get_bool x;
-  if b then boolTrait_ret_true BoolTraitBool x else Return false
+  if b then boolTrait_ret_true BoolTraitBool x else Ok false
 .
 
 (** [traits::{(traits::BoolTrait for core::option::Option<T>)#1}::get_bool]:
     Source: 'src/traits.rs', lines 23:4-23:30 *)
 Definition boolTraitOption_get_bool
   (T : Type) (self : option T) : result bool :=
-  match self with | None => Return false | Some _ => Return true end
+  match self with | None => Ok false | Some _ => Ok true end
 .
 
 (** Trait implementation: [traits::{(traits::BoolTrait for core::option::Option<T>)#1}]
@@ -59,7 +59,7 @@ Definition BoolTraitOption (T : Type) : BoolTrait_t (option T) := {|
     Source: 'src/traits.rs', lines 31:0-31:54 *)
 Definition test_bool_trait_option (T : Type) (x : option T) : result bool :=
   b <- boolTraitOption_get_bool T x;
-  if b then boolTrait_ret_true (BoolTraitOption T) x else Return false
+  if b then boolTrait_ret_true (BoolTraitOption T) x else Ok false
 .
 
 (** [traits::test_bool_trait]:
@@ -81,7 +81,7 @@ Arguments ToU64_t_to_u64 { _ }.
 (** [traits::{(traits::ToU64 for u64)#2}::to_u64]:
     Source: 'src/traits.rs', lines 44:4-44:26 *)
 Definition toU64U64_to_u64 (self : u64) : result u64 :=
-  Return self.
+  Ok self.
 
 (** Trait implementation: [traits::{(traits::ToU64 for u64)#2}]
     Source: 'src/traits.rs', lines 43:0-43:18 *)
@@ -167,7 +167,7 @@ Arguments ToType_t_to_type { _ _ }.
 (** [traits::{(traits::ToType<bool> for u64)#5}::to_type]:
     Source: 'src/traits.rs', lines 93:4-93:28 *)
 Definition toTypeU64Bool_to_type (self : u64) : result bool :=
-  Return (self s> 0%u64)
+  Ok (self s> 0%u64)
 .
 
 (** Trait implementation: [traits::{(traits::ToType<bool> for u64)#5}]
@@ -238,7 +238,7 @@ Arguments TestType_test_TestTrait_t_test { _ }.
     Source: 'src/traits.rs', lines 139:12-139:34 *)
 Definition testType_test_TestTraittraitsTestTypetestTestType1_test
   (self : TestType_test_TestType1_t) : result bool :=
-  Return (self s> 1%u64)
+  Ok (self s> 1%u64)
 .
 
 (** Trait implementation: [traits::{traits::TestType<T>#6}::test::{(traits::{traits::TestType<T>#6}::test::TestTrait for traits::{traits::TestType<T>#6}::test::TestType1)}]
@@ -258,7 +258,7 @@ Definition testType_test
   x1 <- toU64Inst.(ToU64_t_to_u64) x;
   if x1 s> 0%u64
   then testType_test_TestTraittraitsTestTypetestTestType1_test 0%u64
-  else Return false
+  else Ok false
 .
 
 (** [traits::BoolWrapper]
@@ -285,7 +285,7 @@ Definition ToTypetraitsBoolWrapperT (T : Type) (toTypeBoolTInst : ToType_t bool
     Source: 'src/traits.rs', lines 164:4-164:21 *)
 Definition with_const_ty_len2_default_body (Self : Type) (LEN : usize)
   : result usize :=
-  Return 32%usize
+  Ok 32%usize
 .
 Definition with_const_ty_len2_default (Self : Type) (LEN : usize) : usize :=
   (with_const_ty_len2_default_body Self LEN)%global
@@ -313,7 +313,7 @@ Arguments WithConstTy_t_f { _ _ }.
 
 (** [traits::{(traits::WithConstTy<32: usize> for bool)#8}::LEN1]
     Source: 'src/traits.rs', lines 175:4-175:21 *)
-Definition with_const_ty_bool32_len1_body : result usize := Return 12%usize.
+Definition with_const_ty_bool32_len1_body : result usize := Ok 12%usize.
 Definition with_const_ty_bool32_len1 : usize :=
   with_const_ty_bool32_len1_body%global
 .
@@ -322,7 +322,7 @@ Definition with_const_ty_bool32_len1 : usize :=
     Source: 'src/traits.rs', lines 180:4-180:39 *)
 Definition withConstTyBool32_f
   (i : u64) (a : array u8 32%usize) : result u64 :=
-  Return i
+  Ok i
 .
 
 (** Trait implementation: [traits::{(traits::WithConstTy<32: usize> for bool)#8}]
@@ -342,7 +342,7 @@ Definition use_with_const_ty1
   (H : Type) (LEN : usize) (withConstTyInst : WithConstTy_t H LEN) :
   result usize
   :=
-  Return withConstTyInst.(WithConstTy_tWithConstTy_t_LEN1)
+  Ok withConstTyInst.(WithConstTy_tWithConstTy_t_LEN1)
 .
 
 (** [traits::use_with_const_ty2]:
@@ -352,7 +352,7 @@ Definition use_with_const_ty2
   (w : withConstTyInst.(WithConstTy_tWithConstTy_t_W)) :
   result unit
   :=
-  Return tt
+  Ok tt
 .
 
 (** [traits::use_with_const_ty3]:
@@ -368,7 +368,7 @@ Definition use_with_const_ty3
 (** [traits::test_where1]:
     Source: 'src/traits.rs', lines 193:0-193:40 *)
 Definition test_where1 (T : Type) (_x : T) : result unit :=
-  Return tt.
+  Ok tt.
 
 (** [traits::test_where2]:
     Source: 'src/traits.rs', lines 194:0-194:57 *)
@@ -376,7 +376,7 @@ Definition test_where2
   (T : Type) (withConstTyT32Inst : WithConstTy_t T 32%usize) (_x : u32) :
   result unit
   :=
-  Return tt
+  Ok tt
 .
 
 (** Trait declaration: [traits::ParentTrait0]
@@ -435,7 +435,7 @@ Definition order1
   ParentTrait0_t U) :
   result unit
   :=
-  Return tt
+  Ok tt
 .
 
 (** Trait declaration: [traits::ChildTrait1]
@@ -552,7 +552,7 @@ Definition ParentTrait2U32 : ParentTrait2_t u32 := {|
 (** [traits::{(traits::ChildTrait2 for u32)#13}::convert]:
     Source: 'src/traits.rs', lines 273:4-273:29 *)
 Definition childTrait2U32_convert (x : u32) : result u32 :=
-  Return x.
+  Ok x.
 
 (** Trait implementation: [traits::{(traits::ChildTrait2 for u32)#13}]
     Source: 'src/traits.rs', lines 272:0-272:24 *)
@@ -625,9 +625,7 @@ Arguments Trait_tTrait_t_LEN { _ }.
 
 (** [traits::{(traits::Trait for @Array<T, N>)#14}::LEN]
     Source: 'src/traits.rs', lines 315:4-315:20 *)
-Definition trait_array_len_body (T : Type) (N : usize) : result usize :=
-  Return N
-.
+Definition trait_array_len_body (T : Type) (N : usize) : result usize := Ok N.
 Definition trait_array_len (T : Type) (N : usize) : usize :=
   (trait_array_len_body T N)%global
 .
@@ -642,7 +640,7 @@ Definition TraitArray (T : Type) (N : usize) : Trait_t (array T N) := {|
     Source: 'src/traits.rs', lines 319:4-319:20 *)
 Definition traittraits_wrapper_len_body (T : Type) (traitInst : Trait_t T)
   : result usize :=
-  Return 0%usize
+  Ok 0%usize
 .
 Definition traittraits_wrapper_len (T : Type) (traitInst : Trait_t T)
   : usize :=
@@ -659,7 +657,7 @@ Definition TraittraitsWrapper (T : Type) (traitInst : Trait_t T) : Trait_t
 (** [traits::use_wrapper_len]:
     Source: 'src/traits.rs', lines 322:0-322:43 *)
 Definition use_wrapper_len (T : Type) (traitInst : Trait_t T) : result usize :=
-  Return (TraittraitsWrapper T traitInst).(Trait_tTrait_t_LEN)
+  Ok (TraittraitsWrapper T traitInst).(Trait_tTrait_t_LEN)
 .
 
 (** [traits::Foo]
@@ -685,7 +683,7 @@ Arguments Core_result_Result_Err { _ _ }.
     Source: 'src/traits.rs', lines 332:4-332:33 *)
 Definition foo_foo_body (T U : Type) (traitInst : Trait_t T)
   : result (core_result_Result_t T i32) :=
-  Return (Core_result_Result_Err 0%i32)
+  Ok (Core_result_Result_Err 0%i32)
 .
 Definition foo_foo (T U : Type) (traitInst : Trait_t T)
   : core_result_Result_t T i32 :=
@@ -696,14 +694,14 @@ Definition foo_foo (T U : Type) (traitInst : Trait_t T)
     Source: 'src/traits.rs', lines 335:0-335:48 *)
 Definition use_foo1
   (T U : Type) (traitInst : Trait_t T) : result (core_result_Result_t T i32) :=
-  Return (foo_foo T U traitInst)
+  Ok (foo_foo T U traitInst)
 .
 
 (** [traits::use_foo2]:
     Source: 'src/traits.rs', lines 339:0-339:48 *)
 Definition use_foo2
   (T U : Type) (traitInst : Trait_t U) : result (core_result_Result_t U i32) :=
-  Return (foo_foo U T traitInst)
+  Ok (foo_foo U T traitInst)
 .
 
 End Traits.