diff options
Diffstat (limited to 'tests')
-rw-r--r-- | tests/coq/traits/Traits.v | 58 | ||||
-rw-r--r-- | tests/fstar/traits/Traits.fst | 36 | ||||
-rw-r--r-- | tests/lean/Traits.lean | 38 |
3 files changed, 71 insertions, 61 deletions
diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v index f0875a29..93ff9fe3 100644 --- a/tests/coq/traits/Traits.v +++ b/tests/coq/traits/Traits.v @@ -200,12 +200,12 @@ Definition h3 (** Trait declaration: [traits::OfTypeBis] Source: 'src/traits.rs', lines 109:0-109:36 *) Record OfTypeBis_t (Self T : Type) := mkOfTypeBis_t { - OfTypeBis_tOfTypeBis_t_parent_clause_0 : ToType_t T Self; + OfTypeBis_tOfTypeBis_t_ToTypeTSelfInst : ToType_t T Self; OfTypeBis_t_of_type : T -> result Self; }. Arguments mkOfTypeBis_t { _ _ }. -Arguments OfTypeBis_tOfTypeBis_t_parent_clause_0 { _ _ }. +Arguments OfTypeBis_tOfTypeBis_t_ToTypeTSelfInst { _ _ }. Arguments OfTypeBis_t_of_type { _ _ }. (** [traits::h4]: forward function @@ -395,19 +395,20 @@ Arguments mkParentTrait1_t { _ }. (** Trait declaration: [traits::ChildTrait] Source: 'src/traits.rs', lines 206:0-206:49 *) Record ChildTrait_t (Self : Type) := mkChildTrait_t { - ChildTrait_tChildTrait_t_parent_clause_0 : ParentTrait0_t Self; - ChildTrait_tChildTrait_t_parent_clause_1 : ParentTrait1_t Self; + ChildTrait_tChildTrait_t_ParentTrait0SelfInst : ParentTrait0_t Self; + ChildTrait_tChildTrait_t_ParentTrait1SelfInst : ParentTrait1_t Self; }. Arguments mkChildTrait_t { _ }. -Arguments ChildTrait_tChildTrait_t_parent_clause_0 { _ }. -Arguments ChildTrait_tChildTrait_t_parent_clause_1 { _ }. +Arguments ChildTrait_tChildTrait_t_ParentTrait0SelfInst { _ }. +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_parent_clause_0).(ParentTrait0_t_get_name) x + inst.(ChildTrait_tChildTrait_t_ParentTrait0SelfInst).(ParentTrait0_t_get_name) + x . (** [traits::test_child_trait2]: forward function @@ -415,9 +416,9 @@ Definition test_child_trait1 Definition test_child_trait2 (T : Type) (inst : ChildTrait_t T) (x : T) : result - inst.(ChildTrait_tChildTrait_t_parent_clause_0).(ParentTrait0_tParentTrait0_t_W) + inst.(ChildTrait_tChildTrait_t_ParentTrait0SelfInst).(ParentTrait0_tParentTrait0_t_W) := - inst.(ChildTrait_tChildTrait_t_parent_clause_0).(ParentTrait0_t_get_w) x + inst.(ChildTrait_tChildTrait_t_ParentTrait0SelfInst).(ParentTrait0_t_get_w) x . (** [traits::order1]: forward function @@ -432,11 +433,11 @@ Definition order1 (** Trait declaration: [traits::ChildTrait1] Source: 'src/traits.rs', lines 222:0-222:35 *) Record ChildTrait1_t (Self : Type) := mkChildTrait1_t { - ChildTrait1_tChildTrait1_t_parent_clause_0 : ParentTrait1_t Self; + ChildTrait1_tChildTrait1_t_ParentTrait1SelfInst : ParentTrait1_t Self; }. Arguments mkChildTrait1_t { _ }. -Arguments ChildTrait1_tChildTrait1_t_parent_clause_0 { _ }. +Arguments ChildTrait1_tChildTrait1_t_ParentTrait1SelfInst { _ }. (** Trait implementation: [traits::{usize#9}] Source: 'src/traits.rs', lines 224:0-224:27 *) @@ -446,7 +447,8 @@ Definition traits_ParentTrait1UsizeInst : ParentTrait1_t usize (** Trait implementation: [traits::{usize#10}] Source: 'src/traits.rs', lines 225:0-225:26 *) Definition traits_ChildTrait1UsizeInst : ChildTrait1_t usize := {| - ChildTrait1_tChildTrait1_t_parent_clause_0 := traits_ParentTrait1UsizeInst; + ChildTrait1_tChildTrait1_t_ParentTrait1SelfInst := + traits_ParentTrait1UsizeInst; |}. (** Trait declaration: [traits::Iterator] @@ -485,12 +487,13 @@ Arguments mkFromResidual_t { _ _ }. Source: 'src/traits.rs', lines 246:0-246:48 *) Record Try_t (Self : Type) := mkTry_t { Try_tTry_t_Residual : Type; - Try_tTry_t_parent_clause_0 : FromResidual_t Self Try_tTry_t_Residual; + Try_tTry_t_FromResidualSelftraitsTrySelfResidualInst : FromResidual_t Self + Try_tTry_t_Residual; }. Arguments mkTry_t { _ }. Arguments Try_tTry_t_Residual { _ }. -Arguments Try_tTry_t_parent_clause_0 { _ }. +Arguments Try_tTry_t_FromResidualSelftraitsTrySelfResidualInst { _ }. (** Trait declaration: [traits::WithTarget] Source: 'src/traits.rs', lines 252:0-252:20 *) @@ -516,15 +519,15 @@ Arguments ParentTrait2_tParentTrait2_t_U_clause_0 { _ }. (** Trait declaration: [traits::ChildTrait2] Source: 'src/traits.rs', lines 260:0-260:35 *) Record ChildTrait2_t (Self : Type) := mkChildTrait2_t { - ChildTrait2_tChildTrait2_t_parent_clause_0 : ParentTrait2_t Self; + ChildTrait2_tChildTrait2_t_ParentTrait2SelfInst : ParentTrait2_t Self; ChildTrait2_t_convert : - (ChildTrait2_tChildTrait2_t_parent_clause_0).(ParentTrait2_tParentTrait2_t_U) + (ChildTrait2_tChildTrait2_t_ParentTrait2SelfInst).(ParentTrait2_tParentTrait2_t_U) -> result - (ChildTrait2_tChildTrait2_t_parent_clause_0).(ParentTrait2_tParentTrait2_t_U_clause_0).(WithTarget_tWithTarget_t_Target); + (ChildTrait2_tChildTrait2_t_ParentTrait2SelfInst).(ParentTrait2_tParentTrait2_t_U_clause_0).(WithTarget_tWithTarget_t_Target); }. Arguments mkChildTrait2_t { _ }. -Arguments ChildTrait2_tChildTrait2_t_parent_clause_0 { _ }. +Arguments ChildTrait2_tChildTrait2_t_ParentTrait2SelfInst { _ }. Arguments ChildTrait2_t_convert { _ }. (** Trait implementation: [traits::{u32#11}] @@ -548,7 +551,8 @@ Definition u32_convert (x : u32) : result u32 := (** Trait implementation: [traits::{u32#13}] Source: 'src/traits.rs', lines 272:0-272:24 *) Definition traits_ChildTrait2U32Inst : ChildTrait2_t u32 := {| - ChildTrait2_tChildTrait2_t_parent_clause_0 := traits_ParentTrait2U32Inst; + ChildTrait2_tChildTrait2_t_ParentTrait2SelfInst := + traits_ParentTrait2U32Inst; ChildTrait2_t_convert := u32_convert; |}. @@ -566,29 +570,29 @@ Arguments CFnOnce_t_call_once { _ _ }. (** Trait declaration: [traits::CFnMut] Source: 'src/traits.rs', lines 292:0-292:37 *) Record CFnMut_t (Self Args : Type) := mkCFnMut_t { - CFnMut_tCFnMut_t_parent_clause_0 : CFnOnce_t Self Args; + CFnMut_tCFnMut_t_CFnOnceSelfArgsInst : CFnOnce_t Self Args; CFnMut_t_call_mut : Self -> Args -> result - (CFnMut_tCFnMut_t_parent_clause_0).(CFnOnce_tCFnOnce_t_Output); + (CFnMut_tCFnMut_t_CFnOnceSelfArgsInst).(CFnOnce_tCFnOnce_t_Output); CFnMut_t_call_mut_back : Self -> Args -> - (CFnMut_tCFnMut_t_parent_clause_0).(CFnOnce_tCFnOnce_t_Output) -> result - Self; + (CFnMut_tCFnMut_t_CFnOnceSelfArgsInst).(CFnOnce_tCFnOnce_t_Output) -> + result Self; }. Arguments mkCFnMut_t { _ _ }. -Arguments CFnMut_tCFnMut_t_parent_clause_0 { _ _ }. +Arguments CFnMut_tCFnMut_t_CFnOnceSelfArgsInst { _ _ }. Arguments CFnMut_t_call_mut { _ _ }. Arguments CFnMut_t_call_mut_back { _ _ }. (** Trait declaration: [traits::CFn] Source: 'src/traits.rs', lines 296:0-296:33 *) Record CFn_t (Self Args : Type) := mkCFn_t { - CFn_tCFn_t_parent_clause_0 : CFnMut_t Self Args; + CFn_tCFn_t_CFnMutSelfArgsInst : CFnMut_t Self Args; CFn_t_call_mut : Self -> Args -> result - (CFn_tCFn_t_parent_clause_0).(CFnMut_tCFnMut_t_parent_clause_0).(CFnOnce_tCFnOnce_t_Output); + (CFn_tCFn_t_CFnMutSelfArgsInst).(CFnMut_tCFnMut_t_CFnOnceSelfArgsInst).(CFnOnce_tCFnOnce_t_Output); }. Arguments mkCFn_t { _ _ }. -Arguments CFn_tCFn_t_parent_clause_0 { _ _ }. +Arguments CFn_tCFn_t_CFnMutSelfArgsInst { _ _ }. Arguments CFn_t_call_mut { _ _ }. (** [traits::incr_u32]: forward function diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst index 669c1dff..63ac307f 100644 --- a/tests/fstar/traits/Traits.fst +++ b/tests/fstar/traits/Traits.fst @@ -157,7 +157,7 @@ let h3 (** Trait declaration: [traits::OfTypeBis] Source: 'src/traits.rs', lines 109:0-109:36 *) noeq type ofTypeBis_t (self t : Type0) = { - parent_clause_0 : toType_t t self; + toTypeTSelfInst : toType_t t self; of_type : t -> result self; } @@ -311,23 +311,23 @@ type parentTrait1_t (self : Type0) = unit (** Trait declaration: [traits::ChildTrait] Source: 'src/traits.rs', lines 206:0-206:49 *) noeq type childTrait_t (self : Type0) = { - parent_clause_0 : parentTrait0_t self; - parent_clause_1 : parentTrait1_t self; + parentTrait0SelfInst : parentTrait0_t self; + parentTrait1SelfInst : parentTrait1_t self; } (** [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.parent_clause_0.get_name x + inst.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.parent_clause_0.tW + result inst.parentTrait0SelfInst.tW = - inst.parent_clause_0.get_w x + inst.parentTrait0SelfInst.get_w x (** [traits::order1]: forward function Source: 'src/traits.rs', lines 219:0-219:59 *) @@ -340,7 +340,7 @@ let order1 (** Trait declaration: [traits::ChildTrait1] Source: 'src/traits.rs', lines 222:0-222:35 *) noeq type childTrait1_t (self : Type0) = { - parent_clause_0 : parentTrait1_t self; + parentTrait1SelfInst : parentTrait1_t self; } (** Trait implementation: [traits::{usize#9}] @@ -350,7 +350,7 @@ let traits_ParentTrait1UsizeInst : parentTrait1_t usize = () (** Trait implementation: [traits::{usize#10}] Source: 'src/traits.rs', lines 225:0-225:26 *) let traits_ChildTrait1UsizeInst : childTrait1_t usize = { - parent_clause_0 = traits_ParentTrait1UsizeInst; + parentTrait1SelfInst = traits_ParentTrait1UsizeInst; } (** Trait declaration: [traits::Iterator] @@ -374,7 +374,7 @@ type fromResidual_t (self t : Type0) = unit Source: 'src/traits.rs', lines 246:0-246:48 *) noeq type try_t (self : Type0) = { tResidual : Type0; - parent_clause_0 : fromResidual_t self tResidual; + fromResidualSelftraitsTrySelfResidualInst : fromResidual_t self tResidual; } (** Trait declaration: [traits::WithTarget] @@ -391,8 +391,9 @@ noeq type parentTrait2_t (self : Type0) = { (** Trait declaration: [traits::ChildTrait2] Source: 'src/traits.rs', lines 260:0-260:35 *) noeq type childTrait2_t (self : Type0) = { - parent_clause_0 : parentTrait2_t self; - convert : parent_clause_0.tU -> result parent_clause_0.tU_clause_0.tTarget; + parentTrait2SelfInst : parentTrait2_t self; + convert : parentTrait2SelfInst.tU -> result + parentTrait2SelfInst.tU_clause_0.tTarget; } (** Trait implementation: [traits::{u32#11}] @@ -414,7 +415,7 @@ let u32_convert (x : u32) : result u32 = (** Trait implementation: [traits::{u32#13}] Source: 'src/traits.rs', lines 272:0-272:24 *) let traits_ChildTrait2U32Inst : childTrait2_t u32 = { - parent_clause_0 = traits_ParentTrait2U32Inst; + parentTrait2SelfInst = traits_ParentTrait2U32Inst; convert = u32_convert; } @@ -428,16 +429,17 @@ noeq type cFnOnce_t (self args : Type0) = { (** Trait declaration: [traits::CFnMut] Source: 'src/traits.rs', lines 292:0-292:37 *) noeq type cFnMut_t (self args : Type0) = { - parent_clause_0 : cFnOnce_t self args; - call_mut : self -> args -> result parent_clause_0.tOutput; - call_mut_back : self -> args -> parent_clause_0.tOutput -> result self; + cFnOnceSelfArgsInst : cFnOnce_t self args; + call_mut : self -> args -> result cFnOnceSelfArgsInst.tOutput; + call_mut_back : self -> args -> cFnOnceSelfArgsInst.tOutput -> result self; } (** Trait declaration: [traits::CFn] Source: 'src/traits.rs', lines 296:0-296:33 *) noeq type cFn_t (self args : Type0) = { - parent_clause_0 : cFnMut_t self args; - call_mut : self -> args -> result parent_clause_0.parent_clause_0.tOutput; + cFnMutSelfArgsInst : cFnMut_t self args; + call_mut : self -> args -> result + cFnMutSelfArgsInst.cFnOnceSelfArgsInst.tOutput; } (** [traits::incr_u32]: forward function diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean index f854da76..0aa68c5e 100644 --- a/tests/lean/Traits.lean +++ b/tests/lean/Traits.lean @@ -170,7 +170,7 @@ def h3 /- Trait declaration: [traits::OfTypeBis] Source: 'src/traits.rs', lines 109:0-109:36 -/ structure OfTypeBis (Self T : Type) where - parent_clause_0 : ToType T Self + ToTypeTSelfInst : ToType T Self of_type : T → Result Self /- [traits::h4]: forward function @@ -327,20 +327,22 @@ structure ParentTrait1 (Self : Type) where /- Trait declaration: [traits::ChildTrait] Source: 'src/traits.rs', lines 206:0-206:49 -/ structure ChildTrait (Self : Type) where - parent_clause_0 : ParentTrait0 Self - parent_clause_1 : ParentTrait1 Self + ParentTrait0SelfInst : ParentTrait0 Self + ParentTrait1SelfInst : ParentTrait1 Self /- [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.parent_clause_0.get_name x + inst.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.parent_clause_0.W := - inst.parent_clause_0.get_w x + (T : Type) (inst : ChildTrait T) (x : T) : + Result inst.ParentTrait0SelfInst.W + := + inst.ParentTrait0SelfInst.get_w x /- [traits::order1]: forward function Source: 'src/traits.rs', lines 219:0-219:59 -/ @@ -353,7 +355,7 @@ def order1 /- Trait declaration: [traits::ChildTrait1] Source: 'src/traits.rs', lines 222:0-222:35 -/ structure ChildTrait1 (Self : Type) where - parent_clause_0 : ParentTrait1 Self + ParentTrait1SelfInst : ParentTrait1 Self /- Trait implementation: [traits::{usize#9}] Source: 'src/traits.rs', lines 224:0-224:27 -/ @@ -363,7 +365,7 @@ def traits.ParentTrait1UsizeInst : ParentTrait1 Usize := { /- Trait implementation: [traits::{usize#10}] Source: 'src/traits.rs', lines 225:0-225:26 -/ def traits.ChildTrait1UsizeInst : ChildTrait1 Usize := { - parent_clause_0 := traits.ParentTrait1UsizeInst + ParentTrait1SelfInst := traits.ParentTrait1UsizeInst } /- Trait declaration: [traits::Iterator] @@ -387,7 +389,7 @@ structure FromResidual (Self T : Type) where Source: 'src/traits.rs', lines 246:0-246:48 -/ structure Try (Self : Type) where Residual : Type - parent_clause_0 : FromResidual Self Residual + FromResidualSelftraitsTrySelfResidualInst : FromResidual Self Residual /- Trait declaration: [traits::WithTarget] Source: 'src/traits.rs', lines 252:0-252:20 -/ @@ -403,8 +405,9 @@ structure ParentTrait2 (Self : Type) where /- Trait declaration: [traits::ChildTrait2] Source: 'src/traits.rs', lines 260:0-260:35 -/ structure ChildTrait2 (Self : Type) where - parent_clause_0 : ParentTrait2 Self - convert : parent_clause_0.U → Result parent_clause_0.U_clause_0.Target + ParentTrait2SelfInst : ParentTrait2 Self + convert : ParentTrait2SelfInst.U → Result + ParentTrait2SelfInst.U_clause_0.Target /- Trait implementation: [traits::{u32#11}] Source: 'src/traits.rs', lines 264:0-264:23 -/ @@ -427,7 +430,7 @@ def U32.convert (x : U32) : Result U32 := /- Trait implementation: [traits::{u32#13}] Source: 'src/traits.rs', lines 272:0-272:24 -/ def traits.ChildTrait2U32Inst : ChildTrait2 U32 := { - parent_clause_0 := traits.ParentTrait2U32Inst + ParentTrait2SelfInst := traits.ParentTrait2U32Inst convert := U32.convert } @@ -440,15 +443,16 @@ structure CFnOnce (Self Args : Type) where /- Trait declaration: [traits::CFnMut] Source: 'src/traits.rs', lines 292:0-292:37 -/ structure CFnMut (Self Args : Type) where - parent_clause_0 : CFnOnce Self Args - call_mut : Self → Args → Result parent_clause_0.Output - call_mut_back : Self → Args → parent_clause_0.Output → Result Self + CFnOnceSelfArgsInst : CFnOnce Self Args + call_mut : Self → Args → Result CFnOnceSelfArgsInst.Output + call_mut_back : Self → Args → CFnOnceSelfArgsInst.Output → Result Self /- Trait declaration: [traits::CFn] Source: 'src/traits.rs', lines 296:0-296:33 -/ structure CFn (Self Args : Type) where - parent_clause_0 : CFnMut Self Args - call_mut : Self → Args → Result parent_clause_0.parent_clause_0.Output + CFnMutSelfArgsInst : CFnMut Self Args + call_mut : Self → Args → Result + CFnMutSelfArgsInst.CFnOnceSelfArgsInst.Output /- [traits::incr_u32]: forward function Source: 'src/traits.rs', lines 300:0-300:30 -/ |