summaryrefslogtreecommitdiff
path: root/tests/coq/traits
diff options
context:
space:
mode:
Diffstat (limited to 'tests/coq/traits')
-rw-r--r--tests/coq/traits/Primitives.v46
-rw-r--r--tests/coq/traits/Traits.v53
2 files changed, 49 insertions, 50 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 a861c114..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]
@@ -671,7 +669,8 @@ Arguments foo_x { _ _ }.
Arguments foo_y { _ _ }.
(** [core::result::Result]
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21 *)
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21
+ Name pattern: core::result::Result *)
Inductive core_result_Result_t (T E : Type) :=
| Core_result_Result_Ok : T -> core_result_Result_t T E
| Core_result_Result_Err : E -> core_result_Result_t T E
@@ -684,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 :=
@@ -695,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.
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 12:40:32 +0000