From b455f94c841b2423898f39bc9b6a4c35a3db56e3 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 4 Apr 2024 16:20:20 +0200 Subject: Regenerate the test files --- tests/coq/traits/Primitives.v | 46 +++++++++++++++++++-------------------- tests/coq/traits/Traits.v | 50 +++++++++++++++++++++---------------------- 2 files changed, 47 insertions(+), 49 deletions(-) (limited to 'tests/coq/traits') 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 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)#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)#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 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 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#6}::test::{(traits::{traits::TestType#6}::test::TestTrait for traits::{traits::TestType#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)#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. -- cgit v1.2.3