@@ -197,8 +197,7 @@ where
197
197
let interner = gb. interner ( ) ;
198
198
199
199
// struct is well-formed in terms of Sized
200
- let sized_constraint_goal =
201
- WellKnownConstraints :: struct_sized_constraint ( gb. db ( ) , fields) ;
200
+ let sized_constraint_goal = WfWellKnownGoals :: struct_sized_constraint ( gb. db ( ) , fields) ;
202
201
203
202
// (FromEnv(T: Eq) => ...)
204
203
gb. implies (
@@ -292,7 +291,7 @@ fn impl_header_wf_goal<I: Interner>(
292
291
let well_formed_goal = gb. forall ( & impl_fields, ( ) , |gb, _, ( trait_ref, where_clauses) , ( ) | {
293
292
let interner = gb. interner ( ) ;
294
293
295
- let trait_constraint_goal = WellKnownConstraints :: inside_impl ( gb. db ( ) , & trait_ref) ;
294
+ let trait_constraint_goal = WfWellKnownGoals :: inside_impl ( gb. db ( ) , & trait_ref) ;
296
295
297
296
// if (WC && input types are well formed) { ... }
298
297
gb. implies (
@@ -326,7 +325,7 @@ fn impl_header_wf_goal<I: Interner>(
326
325
Some (
327
326
gb. all (
328
327
iter:: once ( well_formed_goal)
329
- . chain ( WellKnownConstraints :: outside_impl ( db, & impl_datum) . into_iter ( ) ) ,
328
+ . chain ( WfWellKnownGoals :: outside_impl ( db, & impl_datum) . into_iter ( ) ) ,
330
329
) ,
331
330
)
332
331
}
@@ -492,9 +491,13 @@ fn compute_assoc_ty_goal<I: Interner>(
492
491
) )
493
492
}
494
493
495
- struct WellKnownConstraints { }
494
+ /// Defines methods to compute well-formedness goals for well-known
495
+ /// traits (e.g. a goal for all fields of struct in a Copy impl to be Copy)
496
+ struct WfWellKnownGoals { }
496
497
497
- impl WellKnownConstraints {
498
+ impl WfWellKnownGoals {
499
+ /// A convenience method to compute the goal assuming `trait_ref`
500
+ /// well-formedness requirements are in the environment.
498
501
pub fn inside_impl < I : Interner > (
499
502
db : & dyn RustIrDatabase < I > ,
500
503
trait_ref : & TraitRef < I > ,
@@ -507,6 +510,9 @@ impl WellKnownConstraints {
507
510
}
508
511
}
509
512
513
+ /// Computes well-formedness goals without any assumptions about the environment.
514
+ /// Note that `outside_impl` does not call `inside_impl`, one needs to call both
515
+ /// in order to get the full set of goals to be proven.
510
516
pub fn outside_impl < I : Interner > (
511
517
db : & dyn RustIrDatabase < I > ,
512
518
impl_datum : & ImplDatum < I > ,
@@ -573,6 +579,7 @@ impl WellKnownConstraints {
573
579
_ => return None ,
574
580
} ;
575
581
582
+ // not { Implemented(ImplSelfTy: Drop) }
576
583
let neg_drop_goal =
577
584
db. well_known_trait_id ( WellKnownTrait :: DropTrait )
578
585
. map ( |drop_trait_id| {
@@ -592,6 +599,7 @@ impl WellKnownConstraints {
592
599
. substitute ( interner, substitution)
593
600
. into_iter ( )
594
601
. map ( |f| {
602
+ // Implemented(FieldTy: Copy)
595
603
TraitRef {
596
604
trait_id : trait_ref. trait_id ,
597
605
substitution : Substitution :: from1 ( interner, f) ,
@@ -668,16 +676,19 @@ impl WellKnownConstraints {
668
676
. binders
669
677
. map_ref ( |v| ( & v. trait_ref , & v. where_clauses ) ) ;
670
678
679
+ // forall<ImplP1...ImplPn> { .. }
671
680
let implied_by_struct_def_goal =
672
681
gb. forall ( & impl_fields, ( ) , |gb, _, ( trait_ref, where_clauses) , ( ) | {
673
682
let interner = gb. interner ( ) ;
674
683
684
+ // FromEnv(ImplSelfType) => ...
675
685
gb. implies (
676
686
iter:: once (
677
687
FromEnv :: Ty ( trait_ref. self_type_parameter ( interner) )
678
688
. cast :: < DomainGoal < I > > ( interner) ,
679
689
) ,
680
690
|gb| {
691
+ // All(ImplWhereClauses)
681
692
gb. all (
682
693
where_clauses
683
694
. iter ( )
@@ -691,6 +702,7 @@ impl WellKnownConstraints {
691
702
. binders
692
703
. map_ref ( |b| b. trait_ref . self_type_parameter ( interner) ) ;
693
704
705
+ // forall<StructP1..StructPN> {...}
694
706
let eq_goal = gb. forall (
695
707
& struct_datum. binders ,
696
708
( struct_name, impl_self_ty) ,
@@ -704,11 +716,14 @@ impl WellKnownConstraints {
704
716
. cast ( interner)
705
717
. intern ( interner) ;
706
718
719
+ // exists<ImplP1...ImplPn> { .. }
707
720
gb. exists (
708
721
& impl_self_ty,
709
722
def_struct,
710
723
|gb, _, impl_struct, def_struct| {
711
724
let interner = gb. interner ( ) ;
725
+
726
+ // StructName<StructP1..StructPn> = ImplSelfType
712
727
GoalData :: EqGoal ( EqGoal {
713
728
a : ParameterData :: Ty ( def_struct) . intern ( interner) ,
714
729
b : ParameterData :: Ty ( impl_struct. clone ( ) ) . intern ( interner) ,
0 commit comments