From 84a505ed9f193885175308ecc837922a41176b5b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 22 Nov 2023 09:11:06 +0100 Subject: Regenerate the test files --- tests/coq/traits/Traits.v | 107 ++++++++++++++++++++++++------------------ tests/fstar/traits/Traits.fst | 106 ++++++++++++++++++++++++----------------- tests/lean/Traits.lean | 104 +++++++++++++++++++++++----------------- 3 files changed, 186 insertions(+), 131 deletions(-) diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v index 93ff9fe3..0952a1df 100644 --- a/tests/coq/traits/Traits.v +++ b/tests/coq/traits/Traits.v @@ -67,8 +67,8 @@ Definition test_bool_trait_option (T : Type) (x : option T) : result bool := (** [traits::test_bool_trait]: forward function Source: 'src/traits.rs', lines 35:0-35:50 *) Definition test_bool_trait - (T : Type) (inst : BoolTrait_t T) (x : T) : result bool := - inst.(BoolTrait_t_get_bool) x + (T : Type) (boolTraitTInst : BoolTrait_t T) (x : T) : result bool := + boolTraitTInst.(BoolTrait_t_get_bool) x . (** Trait declaration: [traits::ToU64] @@ -94,30 +94,31 @@ Definition traits_ToU64U64Inst : ToU64_t u64 := {| (** [traits::{(A, A)#3}::to_u64]: forward function Source: 'src/traits.rs', lines 50:4-50:26 *) Definition pair_to_u64 - (A : Type) (inst : ToU64_t A) (self : (A * A)) : result u64 := + (A : Type) (toU64AInst : ToU64_t A) (self : (A * A)) : result u64 := let (t, t0) := self in - i <- inst.(ToU64_t_to_u64) t; - i0 <- inst.(ToU64_t_to_u64) t0; + i <- toU64AInst.(ToU64_t_to_u64) t; + i0 <- toU64AInst.(ToU64_t_to_u64) t0; u64_add i i0 . (** Trait implementation: [traits::{(A, A)#3}] Source: 'src/traits.rs', lines 49:0-49:31 *) -Definition traits_ToU64TupleAAInst (A : Type) (inst : ToU64_t A) : ToU64_t (A * - A) := {| - ToU64_t_to_u64 := pair_to_u64 A inst; +Definition traits_ToU64TupleAAInst (A : Type) (toU64AInst : ToU64_t A) : + ToU64_t (A * A) := {| + ToU64_t_to_u64 := pair_to_u64 A toU64AInst; |}. (** [traits::f]: forward function Source: 'src/traits.rs', lines 55:0-55:36 *) -Definition f (T : Type) (inst : ToU64_t T) (x : (T * T)) : result u64 := - pair_to_u64 T inst x +Definition f (T : Type) (toU64TInst : ToU64_t T) (x : (T * T)) : result u64 := + pair_to_u64 T toU64TInst x . (** [traits::g]: forward function Source: 'src/traits.rs', lines 59:0-61:18 *) -Definition g (T : Type) (inst : ToU64_t (T * T)) (x : (T * T)) : result u64 := - inst.(ToU64_t_to_u64) x +Definition g + (T : Type) (toU64TupleTTInst : ToU64_t (T * T)) (x : (T * T)) : result u64 := + toU64TupleTTInst.(ToU64_t_to_u64) x . (** [traits::h0]: forward function @@ -135,15 +136,15 @@ Arguments wrapper_x { _ }. (** [traits::{traits::Wrapper#4}::to_u64]: forward function Source: 'src/traits.rs', lines 75:4-75:26 *) Definition wrapper_to_u64 - (T : Type) (inst : ToU64_t T) (self : Wrapper_t T) : result u64 := - inst.(ToU64_t_to_u64) self.(wrapper_x) + (T : Type) (toU64TInst : ToU64_t T) (self : Wrapper_t T) : result u64 := + toU64TInst.(ToU64_t_to_u64) self.(wrapper_x) . (** Trait implementation: [traits::{traits::Wrapper#4}] Source: 'src/traits.rs', lines 74:0-74:35 *) -Definition traits_ToU64traitsWrapperTInst (T : Type) (inst : ToU64_t T) : +Definition traits_ToU64traitsWrapperTInst (T : Type) (toU64TInst : ToU64_t T) : ToU64_t (Wrapper_t T) := {| - ToU64_t_to_u64 := wrapper_to_u64 T inst; + ToU64_t_to_u64 := wrapper_to_u64 T toU64TInst; |}. (** [traits::h1]: forward function @@ -154,8 +155,9 @@ Definition h1 (x : Wrapper_t u64) : result u64 := (** [traits::h2]: forward function Source: 'src/traits.rs', lines 84:0-84:41 *) -Definition h2 (T : Type) (inst : ToU64_t T) (x : Wrapper_t T) : result u64 := - wrapper_to_u64 T inst x +Definition h2 + (T : Type) (toU64TInst : ToU64_t T) (x : Wrapper_t T) : result u64 := + wrapper_to_u64 T toU64TInst x . (** Trait declaration: [traits::ToType] @@ -181,8 +183,8 @@ Definition traits_ToTypeU64BoolInst : ToType_t u64 bool := {| (** Trait declaration: [traits::OfType] Source: 'src/traits.rs', lines 98:0-98:16 *) Record OfType_t (Self : Type) := mkOfType_t { - OfType_t_of_type : forall (T : Type) (inst : ToType_t T Self), T -> result - Self; + OfType_t_of_type : forall (T : Type) (toTypeTSelfInst : ToType_t T Self), T + -> result Self; }. Arguments mkOfType_t { _ }. @@ -191,10 +193,11 @@ Arguments OfType_t_of_type { _ }. (** [traits::h3]: forward function Source: 'src/traits.rs', lines 104:0-104:50 *) Definition h3 - (T1 T2 : Type) (inst : OfType_t T1) (inst0 : ToType_t T2 T1) (y : T2) : + (T1 T2 : Type) (ofTypeT1Inst : OfType_t T1) (toTypeT2T1Inst : ToType_t T2 T1) + (y : T2) : result T1 := - inst.(OfType_t_of_type) T2 inst0 y + ofTypeT1Inst.(OfType_t_of_type) T2 toTypeT2T1Inst y . (** Trait declaration: [traits::OfTypeBis] @@ -211,10 +214,11 @@ Arguments OfTypeBis_t_of_type { _ _ }. (** [traits::h4]: forward function Source: 'src/traits.rs', lines 118:0-118:57 *) Definition h4 - (T1 T2 : Type) (inst : OfTypeBis_t T1 T2) (inst0 : ToType_t T2 T1) (y : T2) : + (T1 T2 : Type) (ofTypeBisT1T2Inst : OfTypeBis_t T1 T2) (toTypeT2T1Inst : + ToType_t T2 T1) (y : T2) : result T1 := - inst.(OfTypeBis_t_of_type) y + ofTypeBisT1T2Inst.(OfTypeBis_t_of_type) y . (** [traits::TestType] @@ -258,8 +262,10 @@ Definition traits_TestType_test_TestTraittraitstraitsTestTypeTtestTestType1Inst (** [traits::{traits::TestType#6}::test]: forward function Source: 'src/traits.rs', lines 126:4-126:36 *) Definition testType_test - (T : Type) (inst : ToU64_t T) (self : TestType_t T) (x : T) : result bool := - x0 <- inst.(ToU64_t_to_u64) x; + (T : Type) (toU64TInst : ToU64_t T) (self : TestType_t T) (x : T) : + result bool + := + x0 <- toU64TInst.(ToU64_t_to_u64) x; if x0 s> 0%u64 then testType_test_TestType1_test {| testType_test_TestType1_0 := 0%u64 |} else Return false @@ -272,15 +278,17 @@ Record BoolWrapper_t := mkBoolWrapper_t { boolWrapper_0 : bool; }. (** [traits::{traits::BoolWrapper#7}::to_type]: forward function Source: 'src/traits.rs', lines 156:4-156:25 *) Definition boolWrapper_to_type - (T : Type) (inst : ToType_t bool T) (self : BoolWrapper_t) : result T := - inst.(ToType_t_to_type) self.(boolWrapper_0) + (T : Type) (toTypeBoolTInst : ToType_t bool T) (self : BoolWrapper_t) : + result T + := + toTypeBoolTInst.(ToType_t_to_type) self.(boolWrapper_0) . (** Trait implementation: [traits::{traits::BoolWrapper#7}] Source: 'src/traits.rs', lines 152:0-152:33 *) -Definition traits_ToTypetraitsBoolWrapperTInst (T : Type) (inst : ToType_t bool - T) : ToType_t BoolWrapper_t T := {| - ToType_t_to_type := boolWrapper_to_type T inst; +Definition traits_ToTypetraitsBoolWrapperTInst (T : Type) (toTypeBoolTInst : + ToType_t bool T) : ToType_t BoolWrapper_t T := {| + ToType_t_to_type := boolWrapper_to_type T toTypeBoolTInst; |}. (** [traits::WithConstTy::LEN2] @@ -333,15 +341,17 @@ Definition traits_WithConstTyBool32Inst : WithConstTy_t bool 32%usize := {| (** [traits::use_with_const_ty1]: forward function Source: 'src/traits.rs', lines 183:0-183:75 *) Definition use_with_const_ty1 - (H : Type) (LEN : usize) (inst : WithConstTy_t H LEN) : result usize := - let i := inst.(WithConstTy_tWithConstTy_t_LEN1) in Return i + (H : Type) (LEN : usize) (withConstTyHLENInst : WithConstTy_t H LEN) : + result usize + := + let i := withConstTyHLENInst.(WithConstTy_tWithConstTy_t_LEN1) in Return i . (** [traits::use_with_const_ty2]: forward function Source: 'src/traits.rs', lines 187:0-187:73 *) Definition use_with_const_ty2 - (H : Type) (LEN : usize) (inst : WithConstTy_t H LEN) - (w : inst.(WithConstTy_tWithConstTy_t_W)) : + (H : Type) (LEN : usize) (withConstTyHLENInst : WithConstTy_t H LEN) + (w : withConstTyHLENInst.(WithConstTy_tWithConstTy_t_W)) : result unit := Return tt @@ -350,11 +360,12 @@ Definition use_with_const_ty2 (** [traits::use_with_const_ty3]: forward function Source: 'src/traits.rs', lines 189:0-189:80 *) Definition use_with_const_ty3 - (H : Type) (LEN : usize) (inst : WithConstTy_t H LEN) - (x : inst.(WithConstTy_tWithConstTy_t_W)) : + (H : Type) (LEN : usize) (withConstTyHLENInst : WithConstTy_t H LEN) + (x : withConstTyHLENInst.(WithConstTy_tWithConstTy_t_W)) : result u64 := - inst.(WithConstTy_tWithConstTy_t_W_clause_0).(ToU64_t_to_u64) x + withConstTyHLENInst.(WithConstTy_tWithConstTy_t_W_clause_0).(ToU64_t_to_u64) + x . (** [traits::test_where1]: forward function @@ -365,7 +376,9 @@ Definition test_where1 (T : Type) (_x : T) : result unit := (** [traits::test_where2]: forward function Source: 'src/traits.rs', lines 194:0-194:57 *) Definition test_where2 - (T : Type) (inst : WithConstTy_t T 32%usize) (_x : u32) : result unit := + (T : Type) (withConstTyT32Inst : WithConstTy_t T 32%usize) (_x : u32) : + result unit + := Return tt . @@ -406,25 +419,29 @@ Arguments ChildTrait_tChildTrait_t_ParentTrait1SelfInst { _ }. (** [traits::test_child_trait1]: forward function Source: 'src/traits.rs', lines 209:0-209:56 *) Definition test_child_trait1 - (T : Type) (inst : ChildTrait_t T) (x : T) : result alloc_string_String_t := - inst.(ChildTrait_tChildTrait_t_ParentTrait0SelfInst).(ParentTrait0_t_get_name) + (T : Type) (childTraitTInst : ChildTrait_t T) (x : T) : + result alloc_string_String_t + := + childTraitTInst.(ChildTrait_tChildTrait_t_ParentTrait0SelfInst).(ParentTrait0_t_get_name) x . (** [traits::test_child_trait2]: forward function Source: 'src/traits.rs', lines 213:0-213:54 *) Definition test_child_trait2 - (T : Type) (inst : ChildTrait_t T) (x : T) : + (T : Type) (childTraitTInst : ChildTrait_t T) (x : T) : result - inst.(ChildTrait_tChildTrait_t_ParentTrait0SelfInst).(ParentTrait0_tParentTrait0_t_W) + childTraitTInst.(ChildTrait_tChildTrait_t_ParentTrait0SelfInst).(ParentTrait0_tParentTrait0_t_W) := - inst.(ChildTrait_tChildTrait_t_ParentTrait0SelfInst).(ParentTrait0_t_get_w) x + childTraitTInst.(ChildTrait_tChildTrait_t_ParentTrait0SelfInst).(ParentTrait0_t_get_w) + x . (** [traits::order1]: forward function Source: 'src/traits.rs', lines 219:0-219:59 *) Definition order1 - (T U : Type) (inst : ParentTrait0_t T) (inst0 : ParentTrait0_t U) : + (T U : Type) (parentTrait0TInst : ParentTrait0_t T) (parentTrait0UInst : + ParentTrait0_t U) : result unit := Return tt diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst index 63ac307f..4cb9fbf1 100644 --- a/tests/fstar/traits/Traits.fst +++ b/tests/fstar/traits/Traits.fst @@ -54,8 +54,9 @@ let test_bool_trait_option (t : Type0) (x : option t) : result bool = (** [traits::test_bool_trait]: forward function Source: 'src/traits.rs', lines 35:0-35:50 *) -let test_bool_trait (t : Type0) (inst : boolTrait_t t) (x : t) : result bool = - inst.get_bool x +let test_bool_trait + (t : Type0) (boolTraitTInst : boolTrait_t t) (x : t) : result bool = + boolTraitTInst.get_bool x (** Trait declaration: [traits::ToU64] Source: 'src/traits.rs', lines 39:0-39:15 *) @@ -72,28 +73,30 @@ let traits_ToU64U64Inst : toU64_t u64 = { to_u64 = u64_to_u64; } (** [traits::{(A, A)#3}::to_u64]: forward function Source: 'src/traits.rs', lines 50:4-50:26 *) -let pair_to_u64 (a : Type0) (inst : toU64_t a) (self : (a & a)) : result u64 = +let pair_to_u64 + (a : Type0) (toU64AInst : toU64_t a) (self : (a & a)) : result u64 = let (x, x0) = self in - let* i = inst.to_u64 x in - let* i0 = inst.to_u64 x0 in + let* i = toU64AInst.to_u64 x in + let* i0 = toU64AInst.to_u64 x0 in u64_add i i0 (** Trait implementation: [traits::{(A, A)#3}] Source: 'src/traits.rs', lines 49:0-49:31 *) -let traits_ToU64TupleAAInst (a : Type0) (inst : toU64_t a) : toU64_t (a & a) - = { - to_u64 = pair_to_u64 a inst; +let traits_ToU64TupleAAInst (a : Type0) (toU64AInst : toU64_t a) : toU64_t (a & + a) = { + to_u64 = pair_to_u64 a toU64AInst; } (** [traits::f]: forward function Source: 'src/traits.rs', lines 55:0-55:36 *) -let f (t : Type0) (inst : toU64_t t) (x : (t & t)) : result u64 = - pair_to_u64 t inst x +let f (t : Type0) (toU64TInst : toU64_t t) (x : (t & t)) : result u64 = + pair_to_u64 t toU64TInst x (** [traits::g]: forward function Source: 'src/traits.rs', lines 59:0-61:18 *) -let g (t : Type0) (inst : toU64_t (t & t)) (x : (t & t)) : result u64 = - inst.to_u64 x +let g + (t : Type0) (toU64TupleTTInst : toU64_t (t & t)) (x : (t & t)) : result u64 = + toU64TupleTTInst.to_u64 x (** [traits::h0]: forward function Source: 'src/traits.rs', lines 66:0-66:24 *) @@ -107,14 +110,14 @@ type wrapper_t (t : Type0) = { x : t; } (** [traits::{traits::Wrapper#4}::to_u64]: forward function Source: 'src/traits.rs', lines 75:4-75:26 *) let wrapper_to_u64 - (t : Type0) (inst : toU64_t t) (self : wrapper_t t) : result u64 = - inst.to_u64 self.x + (t : Type0) (toU64TInst : toU64_t t) (self : wrapper_t t) : result u64 = + toU64TInst.to_u64 self.x (** Trait implementation: [traits::{traits::Wrapper#4}] Source: 'src/traits.rs', lines 74:0-74:35 *) -let traits_ToU64traitsWrapperTInst (t : Type0) (inst : toU64_t t) : toU64_t - (wrapper_t t) = { - to_u64 = wrapper_to_u64 t inst; +let traits_ToU64traitsWrapperTInst (t : Type0) (toU64TInst : toU64_t t) : + toU64_t (wrapper_t t) = { + to_u64 = wrapper_to_u64 t toU64TInst; } (** [traits::h1]: forward function @@ -124,8 +127,8 @@ let h1 (x : wrapper_t u64) : result u64 = (** [traits::h2]: forward function Source: 'src/traits.rs', lines 84:0-84:41 *) -let h2 (t : Type0) (inst : toU64_t t) (x : wrapper_t t) : result u64 = - wrapper_to_u64 t inst x +let h2 (t : Type0) (toU64TInst : toU64_t t) (x : wrapper_t t) : result u64 = + wrapper_to_u64 t toU64TInst x (** Trait declaration: [traits::ToType] Source: 'src/traits.rs', lines 88:0-88:19 *) @@ -143,16 +146,18 @@ let traits_ToTypeU64BoolInst : toType_t u64 bool = { to_type = u64_to_type; } (** Trait declaration: [traits::OfType] Source: 'src/traits.rs', lines 98:0-98:16 *) noeq type ofType_t (self : Type0) = { - of_type : (t : Type0) -> (inst : toType_t t self) -> t -> result self; + of_type : (t : Type0) -> (toTypeTSelfInst : toType_t t self) -> t -> result + self; } (** [traits::h3]: forward function Source: 'src/traits.rs', lines 104:0-104:50 *) let h3 - (t1 t2 : Type0) (inst : ofType_t t1) (inst0 : toType_t t2 t1) (y : t2) : + (t1 t2 : Type0) (ofTypeT1Inst : ofType_t t1) (toTypeT2T1Inst : toType_t t2 + t1) (y : t2) : result t1 = - inst.of_type t2 inst0 y + ofTypeT1Inst.of_type t2 toTypeT2T1Inst y (** Trait declaration: [traits::OfTypeBis] Source: 'src/traits.rs', lines 109:0-109:36 *) @@ -164,11 +169,11 @@ noeq type ofTypeBis_t (self t : Type0) = { (** [traits::h4]: forward function Source: 'src/traits.rs', lines 118:0-118:57 *) let h4 - (t1 t2 : Type0) (inst : ofTypeBis_t t1 t2) (inst0 : toType_t t2 t1) - (y : t2) : + (t1 t2 : Type0) (ofTypeBisT1T2Inst : ofTypeBis_t t1 t2) (toTypeT2T1Inst : + toType_t t2 t1) (y : t2) : result t1 = - inst.of_type y + ofTypeBisT1T2Inst.of_type y (** [traits::TestType] Source: 'src/traits.rs', lines 122:0-122:22 *) @@ -200,8 +205,10 @@ let traits_TestType_test_TestTraittraitstraitsTestTypeTtestTestType1Inst : (** [traits::{traits::TestType#6}::test]: forward function Source: 'src/traits.rs', lines 126:4-126:36 *) let testType_test - (t : Type0) (inst : toU64_t t) (self : testType_t t) (x : t) : result bool = - let* x0 = inst.to_u64 x in + (t : Type0) (toU64TInst : toU64_t t) (self : testType_t t) (x : t) : + result bool + = + let* x0 = toU64TInst.to_u64 x in if x0 > 0 then testType_test_TestType1_test { _0 = 0 } else Return false (** [traits::BoolWrapper] @@ -211,14 +218,16 @@ type boolWrapper_t = { _0 : bool; } (** [traits::{traits::BoolWrapper#7}::to_type]: forward function Source: 'src/traits.rs', lines 156:4-156:25 *) let boolWrapper_to_type - (t : Type0) (inst : toType_t bool t) (self : boolWrapper_t) : result t = - inst.to_type self._0 + (t : Type0) (toTypeBoolTInst : toType_t bool t) (self : boolWrapper_t) : + result t + = + toTypeBoolTInst.to_type self._0 (** Trait implementation: [traits::{traits::BoolWrapper#7}] Source: 'src/traits.rs', lines 152:0-152:33 *) -let traits_ToTypetraitsBoolWrapperTInst (t : Type0) (inst : toType_t bool t) : - toType_t boolWrapper_t t = { - to_type = boolWrapper_to_type t inst; +let traits_ToTypetraitsBoolWrapperTInst (t : Type0) (toTypeBoolTInst : toType_t + bool t) : toType_t boolWrapper_t t = { + to_type = boolWrapper_to_type t toTypeBoolTInst; } (** [traits::WithConstTy::LEN2] @@ -262,13 +271,16 @@ let traits_WithConstTyBool32Inst : withConstTy_t bool 32 = { (** [traits::use_with_const_ty1]: forward function Source: 'src/traits.rs', lines 183:0-183:75 *) let use_with_const_ty1 - (h : Type0) (len : usize) (inst : withConstTy_t h len) : result usize = - let i = inst.cLEN1 in Return i + (h : Type0) (len : usize) (withConstTyHLENInst : withConstTy_t h len) : + result usize + = + let i = withConstTyHLENInst.cLEN1 in Return i (** [traits::use_with_const_ty2]: forward function Source: 'src/traits.rs', lines 187:0-187:73 *) let use_with_const_ty2 - (h : Type0) (len : usize) (inst : withConstTy_t h len) (w : inst.tW) : + (h : Type0) (len : usize) (withConstTyHLENInst : withConstTy_t h len) + (w : withConstTyHLENInst.tW) : result unit = Return () @@ -276,10 +288,11 @@ let use_with_const_ty2 (** [traits::use_with_const_ty3]: forward function Source: 'src/traits.rs', lines 189:0-189:80 *) let use_with_const_ty3 - (h : Type0) (len : usize) (inst : withConstTy_t h len) (x : inst.tW) : + (h : Type0) (len : usize) (withConstTyHLENInst : withConstTy_t h len) + (x : withConstTyHLENInst.tW) : result u64 = - inst.tW_clause_0.to_u64 x + withConstTyHLENInst.tW_clause_0.to_u64 x (** [traits::test_where1]: forward function Source: 'src/traits.rs', lines 193:0-193:40 *) @@ -289,7 +302,9 @@ let test_where1 (t : Type0) (_x : t) : result unit = (** [traits::test_where2]: forward function Source: 'src/traits.rs', lines 194:0-194:57 *) let test_where2 - (t : Type0) (inst : withConstTy_t t 32) (_x : u32) : result unit = + (t : Type0) (withConstTyT32Inst : withConstTy_t t 32) (_x : u32) : + result unit + = Return () (** [alloc::string::String] @@ -318,21 +333,24 @@ noeq type childTrait_t (self : Type0) = { (** [traits::test_child_trait1]: forward function Source: 'src/traits.rs', lines 209:0-209:56 *) let test_child_trait1 - (t : Type0) (inst : childTrait_t t) (x : t) : result alloc_string_String_t = - inst.parentTrait0SelfInst.get_name x + (t : Type0) (childTraitTInst : childTrait_t t) (x : t) : + result alloc_string_String_t + = + childTraitTInst.parentTrait0SelfInst.get_name x (** [traits::test_child_trait2]: forward function Source: 'src/traits.rs', lines 213:0-213:54 *) let test_child_trait2 - (t : Type0) (inst : childTrait_t t) (x : t) : - result inst.parentTrait0SelfInst.tW + (t : Type0) (childTraitTInst : childTrait_t t) (x : t) : + result childTraitTInst.parentTrait0SelfInst.tW = - inst.parentTrait0SelfInst.get_w x + childTraitTInst.parentTrait0SelfInst.get_w x (** [traits::order1]: forward function Source: 'src/traits.rs', lines 219:0-219:59 *) let order1 - (t u : Type0) (inst : parentTrait0_t t) (inst0 : parentTrait0_t u) : + (t u : Type0) (parentTrait0TInst : parentTrait0_t t) (parentTrait0UInst : + parentTrait0_t u) : result unit = Return () diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean index 0aa68c5e..9ac4736c 100644 --- a/tests/lean/Traits.lean +++ b/tests/lean/Traits.lean @@ -61,8 +61,9 @@ def test_bool_trait_option (T : Type) (x : Option T) : Result Bool := /- [traits::test_bool_trait]: forward function Source: 'src/traits.rs', lines 35:0-35:50 -/ -def test_bool_trait (T : Type) (inst : BoolTrait T) (x : T) : Result Bool := - inst.get_bool x +def test_bool_trait + (T : Type) (BoolTraitTInst : BoolTrait T) (x : T) : Result Bool := + BoolTraitTInst.get_bool x /- Trait declaration: [traits::ToU64] Source: 'src/traits.rs', lines 39:0-39:15 -/ @@ -82,28 +83,31 @@ def traits.ToU64U64Inst : ToU64 U64 := { /- [traits::{(A, A)#3}::to_u64]: forward function Source: 'src/traits.rs', lines 50:4-50:26 -/ -def Pair.to_u64 (A : Type) (inst : ToU64 A) (self : (A × A)) : Result U64 := +def Pair.to_u64 + (A : Type) (ToU64AInst : ToU64 A) (self : (A × A)) : Result U64 := do let (t, t0) := self - let i ← inst.to_u64 t - let i0 ← inst.to_u64 t0 + let i ← ToU64AInst.to_u64 t + let i0 ← ToU64AInst.to_u64 t0 i + i0 /- Trait implementation: [traits::{(A, A)#3}] Source: 'src/traits.rs', lines 49:0-49:31 -/ -def traits.ToU64TupleAAInst (A : Type) (inst : ToU64 A) : ToU64 (A × A) := { - to_u64 := Pair.to_u64 A inst +def traits.ToU64TupleAAInst (A : Type) (ToU64AInst : ToU64 A) : ToU64 (A × A) + := { + to_u64 := Pair.to_u64 A ToU64AInst } /- [traits::f]: forward function Source: 'src/traits.rs', lines 55:0-55:36 -/ -def f (T : Type) (inst : ToU64 T) (x : (T × T)) : Result U64 := - Pair.to_u64 T inst x +def f (T : Type) (ToU64TInst : ToU64 T) (x : (T × T)) : Result U64 := + Pair.to_u64 T ToU64TInst x /- [traits::g]: forward function Source: 'src/traits.rs', lines 59:0-61:18 -/ -def g (T : Type) (inst : ToU64 (T × T)) (x : (T × T)) : Result U64 := - inst.to_u64 x +def g + (T : Type) (ToU64TupleTTInst : ToU64 (T × T)) (x : (T × T)) : Result U64 := + ToU64TupleTTInst.to_u64 x /- [traits::h0]: forward function Source: 'src/traits.rs', lines 66:0-66:24 -/ @@ -118,14 +122,14 @@ structure Wrapper (T : Type) where /- [traits::{traits::Wrapper#4}::to_u64]: forward function Source: 'src/traits.rs', lines 75:4-75:26 -/ def Wrapper.to_u64 - (T : Type) (inst : ToU64 T) (self : Wrapper T) : Result U64 := - inst.to_u64 self.x + (T : Type) (ToU64TInst : ToU64 T) (self : Wrapper T) : Result U64 := + ToU64TInst.to_u64 self.x /- Trait implementation: [traits::{traits::Wrapper#4}] Source: 'src/traits.rs', lines 74:0-74:35 -/ -def traits.ToU64traitsWrapperTInst (T : Type) (inst : ToU64 T) : ToU64 (Wrapper - T) := { - to_u64 := Wrapper.to_u64 T inst +def traits.ToU64traitsWrapperTInst (T : Type) (ToU64TInst : ToU64 T) : ToU64 + (Wrapper T) := { + to_u64 := Wrapper.to_u64 T ToU64TInst } /- [traits::h1]: forward function @@ -135,8 +139,8 @@ def h1 (x : Wrapper U64) : Result U64 := /- [traits::h2]: forward function Source: 'src/traits.rs', lines 84:0-84:41 -/ -def h2 (T : Type) (inst : ToU64 T) (x : Wrapper T) : Result U64 := - Wrapper.to_u64 T inst x +def h2 (T : Type) (ToU64TInst : ToU64 T) (x : Wrapper T) : Result U64 := + Wrapper.to_u64 T ToU64TInst x /- Trait declaration: [traits::ToType] Source: 'src/traits.rs', lines 88:0-88:19 -/ @@ -157,15 +161,17 @@ def traits.ToTypeU64BoolInst : ToType U64 Bool := { /- Trait declaration: [traits::OfType] Source: 'src/traits.rs', lines 98:0-98:16 -/ structure OfType (Self : Type) where - of_type : forall (T : Type) (inst : ToType T Self), T → Result Self + of_type : forall (T : Type) (ToTypeTSelfInst : ToType T Self), T → Result + Self /- [traits::h3]: forward function Source: 'src/traits.rs', lines 104:0-104:50 -/ def h3 - (T1 T2 : Type) (inst : OfType T1) (inst0 : ToType T2 T1) (y : T2) : + (T1 T2 : Type) (OfTypeT1Inst : OfType T1) (ToTypeT2T1Inst : ToType T2 T1) + (y : T2) : Result T1 := - inst.of_type T2 inst0 y + OfTypeT1Inst.of_type T2 ToTypeT2T1Inst y /- Trait declaration: [traits::OfTypeBis] Source: 'src/traits.rs', lines 109:0-109:36 -/ @@ -176,10 +182,11 @@ structure OfTypeBis (Self T : Type) where /- [traits::h4]: forward function Source: 'src/traits.rs', lines 118:0-118:57 -/ def h4 - (T1 T2 : Type) (inst : OfTypeBis T1 T2) (inst0 : ToType T2 T1) (y : T2) : + (T1 T2 : Type) (OfTypeBisT1T2Inst : OfTypeBis T1 T2) (ToTypeT2T1Inst : ToType + T2 T1) (y : T2) : Result T1 := - inst.of_type y + OfTypeBisT1T2Inst.of_type y /- [traits::TestType] Source: 'src/traits.rs', lines 122:0-122:22 -/ @@ -212,9 +219,11 @@ def traits.TestType.test.TestTraittraitstraitsTestTypeTtestTestType1Inst : /- [traits::{traits::TestType#6}::test]: forward function Source: 'src/traits.rs', lines 126:4-126:36 -/ def TestType.test - (T : Type) (inst : ToU64 T) (self : TestType T) (x : T) : Result Bool := + (T : Type) (ToU64TInst : ToU64 T) (self : TestType T) (x : T) : + Result Bool + := do - let x0 ← inst.to_u64 x + let x0 ← ToU64TInst.to_u64 x if x0 > 0#u64 then TestType.test.TestType1.test { _0 := 0#u64 } else Result.ret false @@ -227,14 +236,16 @@ structure BoolWrapper where /- [traits::{traits::BoolWrapper#7}::to_type]: forward function Source: 'src/traits.rs', lines 156:4-156:25 -/ def BoolWrapper.to_type - (T : Type) (inst : ToType Bool T) (self : BoolWrapper) : Result T := - inst.to_type self._0 + (T : Type) (ToTypeBoolTInst : ToType Bool T) (self : BoolWrapper) : + Result T + := + ToTypeBoolTInst.to_type self._0 /- Trait implementation: [traits::{traits::BoolWrapper#7}] Source: 'src/traits.rs', lines 152:0-152:33 -/ -def traits.ToTypetraitsBoolWrapperTInst (T : Type) (inst : ToType Bool T) : - ToType BoolWrapper T := { - to_type := BoolWrapper.to_type T inst +def traits.ToTypetraitsBoolWrapperTInst (T : Type) (ToTypeBoolTInst : ToType + Bool T) : ToType BoolWrapper T := { + to_type := BoolWrapper.to_type T ToTypeBoolTInst } /- [traits::WithConstTy::LEN2] @@ -278,14 +289,17 @@ def traits.WithConstTyBool32Inst : WithConstTy Bool 32#usize := { /- [traits::use_with_const_ty1]: forward function Source: 'src/traits.rs', lines 183:0-183:75 -/ def use_with_const_ty1 - (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) : Result Usize := - let i := inst.LEN1 + (H : Type) (LEN : Usize) (WithConstTyHLENInst : WithConstTy H LEN) : + Result Usize + := + let i := WithConstTyHLENInst.LEN1 Result.ret i /- [traits::use_with_const_ty2]: forward function Source: 'src/traits.rs', lines 187:0-187:73 -/ def use_with_const_ty2 - (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) (w : inst.W) : + (H : Type) (LEN : Usize) (WithConstTyHLENInst : WithConstTy H LEN) + (w : WithConstTyHLENInst.W) : Result Unit := Result.ret () @@ -293,10 +307,11 @@ def use_with_const_ty2 /- [traits::use_with_const_ty3]: forward function Source: 'src/traits.rs', lines 189:0-189:80 -/ def use_with_const_ty3 - (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) (x : inst.W) : + (H : Type) (LEN : Usize) (WithConstTyHLENInst : WithConstTy H LEN) + (x : WithConstTyHLENInst.W) : Result U64 := - inst.W_clause_0.to_u64 x + WithConstTyHLENInst.W_clause_0.to_u64 x /- [traits::test_where1]: forward function Source: 'src/traits.rs', lines 193:0-193:40 -/ @@ -306,7 +321,9 @@ def test_where1 (T : Type) (_x : T) : Result Unit := /- [traits::test_where2]: forward function Source: 'src/traits.rs', lines 194:0-194:57 -/ def test_where2 - (T : Type) (inst : WithConstTy T 32#usize) (_x : U32) : Result Unit := + (T : Type) (WithConstTyT32Inst : WithConstTy T 32#usize) (_x : U32) : + Result Unit + := Result.ret () /- [alloc::string::String] @@ -333,21 +350,24 @@ structure ChildTrait (Self : Type) where /- [traits::test_child_trait1]: forward function Source: 'src/traits.rs', lines 209:0-209:56 -/ def test_child_trait1 - (T : Type) (inst : ChildTrait T) (x : T) : Result alloc.string.String := - inst.ParentTrait0SelfInst.get_name x + (T : Type) (ChildTraitTInst : ChildTrait T) (x : T) : + Result alloc.string.String + := + ChildTraitTInst.ParentTrait0SelfInst.get_name x /- [traits::test_child_trait2]: forward function Source: 'src/traits.rs', lines 213:0-213:54 -/ def test_child_trait2 - (T : Type) (inst : ChildTrait T) (x : T) : - Result inst.ParentTrait0SelfInst.W + (T : Type) (ChildTraitTInst : ChildTrait T) (x : T) : + Result ChildTraitTInst.ParentTrait0SelfInst.W := - inst.ParentTrait0SelfInst.get_w x + ChildTraitTInst.ParentTrait0SelfInst.get_w x /- [traits::order1]: forward function Source: 'src/traits.rs', lines 219:0-219:59 -/ def order1 - (T U : Type) (inst : ParentTrait0 T) (inst0 : ParentTrait0 U) : + (T U : Type) (ParentTrait0TInst : ParentTrait0 T) (ParentTrait0UInst : + ParentTrait0 U) : Result Unit := Result.ret () -- cgit v1.2.3