summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/coq/traits/Traits.v58
-rw-r--r--tests/fstar/traits/Traits.fst36
-rw-r--r--tests/lean/Traits.lean38
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 -/
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-20 01:26:02 +0000