Skip to content

Commit 05f2322

Browse files
scalexmscalexm
committed
Add documentation
1 parent 762549f commit 05f2322

File tree

5 files changed

+148
-19
lines changed

5 files changed

+148
-19
lines changed

‎src/ir/mod.rs‎

Lines changed: 39 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -506,6 +506,10 @@ impl DomainGoal {
506506
}
507507
}
508508

509+
/// Turn a where clause into the WF version of it i.e.:
510+
/// * `T: Trait` maps to `WellFormed(T: Trait)`
511+
/// * `T: Trait<Item = Foo>` maps to `WellFormed(T: Trait<Item = Foo>)`
512+
/// * any other clause maps to itself
509513
pub fn into_well_formed_clause(self) -> DomainGoal {
510514
match self {
511515
DomainGoal::Implemented(tr) => DomainGoal::WellFormed(WellFormed::TraitRef(tr)),
@@ -514,6 +518,7 @@ impl DomainGoal {
514518
}
515519
}
516520

521+
/// Same as `into_well_formed_clause` but with the `FromEnv` predicate instead of `WellFormed`.
517522
pub fn into_from_env_clause(self) -> DomainGoal {
518523
match self {
519524
DomainGoal::Implemented(tr) => DomainGoal::FromEnv(FromEnv::TraitRef(tr)),
@@ -539,13 +544,43 @@ pub struct EqGoal {
539544
}
540545

541546
#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
547+
/// A predicate which is true is some object is well-formed, e.g. a type or a trait ref.
548+
/// For example, given the following type definition:
549+
///
550+
/// ```notrust
551+
/// struct Set<K> where K: Hash {
552+
/// ...
553+
/// }
554+
/// ```
555+
///
556+
/// then we have the following rule: `WellFormed(Set<K>) :- (K: Hash)`.
557+
/// See the complete rules in `lower.rs`.
542558
pub enum WellFormed {
543559
Ty(Ty),
544560
TraitRef(TraitRef),
545561
Normalize(Normalize),
546562
}
547563

548564
#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
565+
/// A predicate which enables deriving everything which should be true if we *know* that some object
566+
/// is well-formed. For example, given the following trait definitions:
567+
///
568+
/// ```notrust
569+
/// trait Clone { ... }
570+
/// trait Copy where Self: Clone { ... }
571+
/// ```
572+
///
573+
/// then we can use `FromEnv(T: Copy)` to derive that `T: Clone`, like in:
574+
///
575+
/// ```notrust
576+
/// forall<T> {
577+
/// if (FromEnv(T: Copy)) {
578+
/// T: Clone
579+
/// }
580+
/// }
581+
/// ```
582+
///
583+
/// See the complete rules in `lower.rs`.
549584
pub enum FromEnv {
550585
Ty(Ty),
551586
TraitRef(TraitRef),
@@ -755,7 +790,10 @@ impl<T> UCanonical<T> {
755790
}
756791

757792
impl UCanonical<InEnvironment<Goal>> {
758-
/// A goal has coinductive semantics if it is of the form `T: AutoTrait`.
793+
/// A goal has coinductive semantics if it is of the form `T: AutoTrait`, or if it is of the
794+
/// form `WellFormed(T: Trait)` where `Trait` is any trait. The latter is needed for dealing
795+
/// with WF requirements and cyclic traits, which generates cycles in the proof tree which must
796+
/// not be rejected but instead must be treated as a success.
759797
pub fn is_coinductive(&self, program: &ProgramEnvironment) -> bool {
760798
match &self.canonical.value.goal {
761799
Goal::Leaf(LeafGoal::DomainGoal(DomainGoal::Implemented(tr))) => {

‎src/lower/mod.rs‎

Lines changed: 36 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1247,8 +1247,8 @@ impl ir::StructDatum {
12471247
//
12481248
// we generate the following clause:
12491249
//
1250-
// for<?T> WF(Foo<?T>) :- (?T: Eq).
1251-
// for<?T> FromEnv(?T: Eq) :- FromEnv(Foo<?T>).
1250+
// forall<T> { WF(Foo<T>) :- (T: Eq). }
1251+
// forall<T> { FromEnv(T: Eq) :- FromEnv(Foo<T>). }
12521252

12531253
let wf = ir::ProgramClause {
12541254
implication: self.binders.map_ref(|bound_datum| {
@@ -1296,13 +1296,15 @@ impl ir::TraitDatum {
12961296
//
12971297
// trait Ord<T> where Self: Eq<T> { ... }
12981298
//
1299-
// we generate the following clauses:
1299+
// we generate the following clause:
13001300
//
1301-
// for<?Self, ?T> WF(?Self: Ord<?T>) :-
1302-
// (?Self: Ord<?T>), WF(?Self: Eq<?T>)
1301+
// forall<Self, T> {
1302+
// WF(Self: Ord<T>) :- (Self: Ord<T>), WF(Self: Eq<T>)
1303+
// }
13031304
//
1304-
// for<?Self, ?T> (?Self: Ord<T>) :- FromEnv(?Self: Ord<T>)
1305-
// for<?Self, ?T> FromEnv(?Self: Ord<?T>) :- FromEnv(?Self: Ord<T>)
1305+
// and the reverse rules:
1306+
// forall<Self, T> { (Self: Ord<T>) :- FromEnv(Self: Ord<T>) }
1307+
// forall<Self, T> { FromEnv(Self: Ord<T>) :- FromEnv(Self: Ord<T>) }
13061308

13071309
let trait_ref = self.binders.value.trait_ref.clone();
13081310

@@ -1387,6 +1389,9 @@ impl ir::AssociatedTyDatum {
13871389
// `ProjectionEq` to fallback *or* normalize it. So instead we
13881390
// handle this kind of reasoning by expanding "projection
13891391
// equality" predicates (see `DomainGoal::expanded`).
1392+
//
1393+
// We also generate rules specific to WF requirements and implied bounds,
1394+
// see below.
13901395

13911396
let binders: Vec<_> = self.parameter_kinds
13921397
.iter()
@@ -1434,6 +1439,12 @@ impl ir::AssociatedTyDatum {
14341439
},
14351440
});
14361441

1442+
// The above application type is always well-formed, and `<T as Foo>::Assoc` will
1443+
// unify with `(Foo::Assoc)<T>` only if `T: Foo`, because of the above rule, so we have:
1444+
//
1445+
// forall<T> {
1446+
// WellFormed((Foo::Assoc)<T>).
1447+
// }
14371448
clauses.push(ir::ProgramClause {
14381449
implication: ir::Binders {
14391450
binders: binders.clone(),
@@ -1470,6 +1481,14 @@ impl ir::AssociatedTyDatum {
14701481
});
14711482

14721483

1484+
// We generate a proxy rule for the well-formedness of `T: Foo<Assoc = U>` which really
1485+
// means two things: `T: Foo` and `Normalize(<T as Foo>::Assoc -> U)`. So we have the
1486+
// following rule:
1487+
//
1488+
// forall<T> {
1489+
// WellFormed(T: Foo<Assoc = U>) :-
1490+
// WellFormed(T: Foo), Normalize(<T as Foo>::Assoc -> U)
1491+
// }
14731492
clauses.push(ir::ProgramClause {
14741493
implication: ir::Binders {
14751494
binders: binders.clone(),
@@ -1483,6 +1502,11 @@ impl ir::AssociatedTyDatum {
14831502
}
14841503
});
14851504

1505+
// We also have two proxy reverse rules, the first one being:
1506+
//
1507+
// forall<T> {
1508+
// FromEnv(T: Foo) :- FromEnv(T: Foo<Assoc = U>)
1509+
// }
14861510
clauses.push(ir::ProgramClause {
14871511
implication: ir::Binders {
14881512
binders: binders.clone(),
@@ -1493,6 +1517,11 @@ impl ir::AssociatedTyDatum {
14931517
}
14941518
});
14951519

1520+
// And the other one being:
1521+
//
1522+
// forall<T> {
1523+
// Normalize(<T as Foo>::Assoc -> U) :- FromEnv(T: Foo<Assoc = U>)
1524+
// }
14961525
clauses.push(ir::ProgramClause {
14971526
implication: ir::Binders {
14981527
binders: binders,

‎src/lower/test.rs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,8 @@ macro_rules! lowering_error {
3232

3333

3434
fn parse_and_lower(text: &str) -> Result<Program> {
35+
// Use the on-demand SLG solver to avoid ambiguities on projection types encountered when
36+
// using the recursive solver.
3537
chalk_parse::parse_program(text)?.lower(SolverChoice::on_demand_slg())
3638
}
3739

‎src/lower/wf.rs‎

Lines changed: 68 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,7 @@ impl Program {
4141
}
4242
}
4343

44+
/// A trait for retrieving all types appearing in some Chalk construction.
4445
trait FoldInputTypes {
4546
fn fold(&self, accumulator: &mut Vec<Ty>);
4647
}
@@ -77,7 +78,10 @@ impl FoldInputTypes for Ty {
7778
accumulator.push(self.clone());
7879
proj.parameters.fold(accumulator);
7980
}
80-
_ => (),
81+
82+
// Type parameters and higher-kinded types do not carry any input types (so we can sort
83+
// of assume they are always WF).
84+
Ty::Var(..) | Ty::ForAll(..) => (),
8185
}
8286
}
8387
}
@@ -108,13 +112,15 @@ impl FoldInputTypes for DomainGoal {
108112
DomainGoal::Implemented(ref tr) => tr.fold(accumulator),
109113
DomainGoal::Normalize(ref n) => n.fold(accumulator),
110114
DomainGoal::UnselectedNormalize(ref n) => n.fold(accumulator),
115+
DomainGoal::WellFormed(..) | DomainGoal::FromEnv(..) => panic!("unexpected where clause"),
111116
_ => (),
112117
}
113118
}
114119
}
115120

116121
impl WfSolver {
117122
fn verify_struct_decl(&self, struct_datum: &StructDatum) -> bool {
123+
// We retrieve all the input types of the struct fields.
118124
let mut input_types = Vec::new();
119125
struct_datum.binders.value.fields.fold(&mut input_types);
120126
struct_datum.binders.value.where_clauses.fold(&mut input_types);
@@ -124,7 +130,6 @@ impl WfSolver {
124130
}
125131

126132
let goals = input_types.into_iter().map(|ty| WellFormed::Ty(ty).cast());
127-
128133
let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf)))
129134
.expect("at least one goal");
130135

@@ -137,6 +142,8 @@ impl WfSolver {
137142
.map(|wc| wc.into_from_env_clause())
138143
.collect();
139144

145+
// We ask that the above input types are well-formed provided that all the where-clauses
146+
// on the struct definition hold.
140147
let goal = Goal::Implies(hypotheses, Box::new(goal))
141148
.quantify(QuantifierKind::ForAll, struct_datum.binders.binders.clone());
142149

@@ -152,9 +159,62 @@ impl WfSolver {
152159
_ => return true
153160
};
154161

162+
// We retrieve all the input types of the where clauses appearing on the trait impl,
163+
// e.g. in:
164+
// ```
165+
// impl<T, K> Foo for (Set<K>, Vec<Box<T>>) { ... }
166+
// ```
167+
// we would retrieve `Set<K>`, `Box<T>`, `Vec<Box<T>>`, `(Set<K>, Vec<Box<T>>)`.
168+
// We will have to prove that these types are well-formed.
155169
let mut input_types = Vec::new();
156170
impl_datum.binders.value.where_clauses.fold(&mut input_types);
157171

172+
// We partition the input types of the type on which we implement the trait in two categories:
173+
// * projection types, e.g. `<T as Iterator>::Item`: we will have to prove that these types
174+
// are well-formed, e.g. that we can show that `T: Iterator` holds
175+
// * any other types, e.g. `HashSet<K>`: we will *assume* that these types are well-formed, e.g.
176+
// we will be able to derive that `K: Hash` holds without writing any where clause.
177+
//
178+
// Examples:
179+
// ```
180+
// struct HashSet<K> where K: Hash { ... }
181+
//
182+
// impl<K> Foo for HashSet<K> {
183+
// // Inside here, we can rely on the fact that `K: Hash` holds
184+
// }
185+
// ```
186+
//
187+
// ```
188+
// impl<T> Foo for <T as Iterator>::Item {
189+
// // The impl is not well-formed, as an exception we do not assume that
190+
// // `<T as Iterator>::Item` is well-formed and instead want to prove it.
191+
// }
192+
// ```
193+
//
194+
// ```
195+
// impl<T> Foo for <T as Iterator>::Item where T: Iterator {
196+
// // Now ok.
197+
// }
198+
// ```
199+
let mut header_input_types = Vec::new();
200+
trait_ref.fold(&mut header_input_types);
201+
let (header_projection_types, header_other_types): (Vec<_>, Vec<_>) =
202+
header_input_types.into_iter()
203+
.partition(|ty| ty.is_projection());
204+
205+
// Associated type values are special because they can be parametric (independently of
206+
// the impl), so we issue a special goal which is quantified using the binders of the
207+
// associated type value, for example in:
208+
// ```
209+
// trait Foo {
210+
// type Item<'a>
211+
// }
212+
//
213+
// impl<T> Foo for Box<T> {
214+
// type Item<'a> = Box<&'a T>;
215+
// }
216+
// ```
217+
// we would issue the following subgoal: `forall<'a> { WellFormed(Box<&'a T>) }`.
158218
let compute_assoc_ty_goal = |assoc_ty: &AssociatedTyValue| {
159219
let mut input_types = Vec::new();
160220
assoc_ty.value.value.ty.fold(&mut input_types);
@@ -176,12 +236,8 @@ impl WfSolver {
176236
.iter()
177237
.filter_map(compute_assoc_ty_goal);
178238

179-
let mut header_input_types = Vec::new();
180-
trait_ref.fold(&mut header_input_types);
181-
let (header_projection_types, header_other_types): (Vec<_>, Vec<_>) =
182-
header_input_types.into_iter()
183-
.partition(|ty| ty.is_projection());
184-
239+
// Things to prove well-formed: input types of the where-clauses, projection types
240+
// appearing in the header, associated type values, and of course the trait ref.
185241
let goals =
186242
input_types.into_iter()
187243
.chain(header_projection_types.into_iter())
@@ -191,6 +247,10 @@ impl WfSolver {
191247

192248
let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf)))
193249
.expect("at least one goal");
250+
251+
// Assumptions: types appearing in the header which are not projection types are
252+
// assumed to be well-formed, and where clauses declared on the impl are assumed
253+
// to hold.
194254
let hypotheses =
195255
impl_datum.binders
196256
.value

‎src/solve/test/mod.rs‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,8 @@ fn parse_and_lower_program(text: &str, solver_choice: SolverChoice, skip_coheren
1414
-> Result<ir::Program>
1515
{
1616
if skip_coherence {
17+
// We disable WF checks for the recursive solver, because of ambiguities appearing
18+
// with projection types.
1719
chalk_parse::parse_program(text)?.lower_without_coherence()
1820
} else {
1921
chalk_parse::parse_program(text)?.lower(solver_choice)
@@ -1543,11 +1545,9 @@ fn coinductive_semantics() {
15431545
} yields {
15441546
"No possible solution"
15451547
}
1546-
1547-
// `WellFormed(T)` because of the hand-written impl for `Ptr<T>`.
15481548
goal {
15491549
forall<T> {
1550-
if (WellFormed(T), T: Send) {
1550+
if (T: Send) {
15511551
List<T>: Send
15521552
}
15531553
}

0 commit comments

Comments
 (0)