Skip to content

Commit 4a30113

Browse files
nikomatsakisnikomatsakis
authored
Merge pull request #150 from sunjay/implallowed-traitrefs
Complete Implementation of LocalImplAllowed(T: Trait)
2 parents 3d881b7 + 955ca69 commit 4a30113

File tree

9 files changed

+354
-27
lines changed

9 files changed

+354
-27
lines changed

‎chalk-parse/src/ast.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -243,6 +243,9 @@ pub enum DomainGoal {
243243
TraitInScope { trait_name: Identifier },
244244
Derefs { source: Ty, target: Ty },
245245
IsLocal { ty: Ty },
246+
IsExternal { ty: Ty },
247+
IsDeeplyExternal { ty: Ty },
248+
LocalImplAllowed { trait_ref: TraitRef },
246249
}
247250

248251
#[derive(Clone, PartialEq, Eq, Debug)]

‎chalk-parse/src/parser.lalrpop

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -287,6 +287,10 @@ DomainGoal: DomainGoal = {
287287
"Derefs" "(" <source:Ty> "," <target:Ty> ")" => DomainGoal::Derefs { source, target },
288288

289289
"IsLocal" "(" <ty:Ty> ")" => DomainGoal::IsLocal { ty },
290+
"IsExternal" "(" <ty:Ty> ")" => DomainGoal::IsExternal { ty },
291+
"IsDeeplyExternal" "(" <ty:Ty> ")" => DomainGoal::IsDeeplyExternal { ty },
292+
293+
"LocalImplAllowed" "(" <trait_ref:TraitRef<":">> ")" => DomainGoal::LocalImplAllowed { trait_ref },
290294
};
291295

292296
LeafGoal: LeafGoal = {

‎src/fold.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -427,7 +427,8 @@ enum_fold!(WhereClause[] { Implemented(a), ProjectionEq(a) });
427427
enum_fold!(WellFormed[] { Trait(a), Ty(a) });
428428
enum_fold!(FromEnv[] { Trait(a), Ty(a) });
429429
enum_fold!(DomainGoal[] { Holds(a), WellFormed(a), FromEnv(a), Normalize(a), UnselectedNormalize(a),
430-
InScope(a), Derefs(a), IsLocal(a), LocalImplAllowed(a) });
430+
InScope(a), Derefs(a), IsLocal(a), IsExternal(a), IsDeeplyExternal(a),
431+
LocalImplAllowed(a) });
431432
enum_fold!(LeafGoal[] { EqGoal(a), DomainGoal(a) });
432433
enum_fold!(Constraint[] { LifetimeEq(a, b) });
433434
enum_fold!(Goal[] { Quantified(qkind, subgoal), Implies(wc, subgoal), And(g1, g2), Not(g),

‎src/ir.rs

Lines changed: 37 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -453,13 +453,17 @@ pub struct ApplicationTy {
453453
}
454454

455455
impl ApplicationTy {
456-
crate fn first_type_parameter(&self) -> Option<Ty> {
456+
crate fn type_parameters<'a>(&'a self) -> impl Iterator<Item=Ty> + 'a {
457457
// This unwrap() is safe because is_ty ensures that we definitely have a Ty
458-
self.parameters.iter().find(|p| p.is_ty()).map(|p| p.clone().ty().unwrap())
458+
self.parameters.iter().filter(|p| p.is_ty()).map(|p| p.clone().ty().unwrap())
459+
}
460+
461+
crate fn first_type_parameter(&self) -> Option<Ty> {
462+
self.type_parameters().next()
459463
}
460464

461465
crate fn len_type_parameters(&self) -> usize {
462-
self.parameters.iter().filter(|p| p.is_ty()).count()
466+
self.type_parameters().count()
463467
}
464468
}
465469

@@ -592,6 +596,13 @@ pub struct TraitRef {
592596
crate parameters: Vec<Parameter>,
593597
}
594598

599+
impl TraitRef {
600+
crate fn type_parameters<'a>(&'a self) -> impl Iterator<Item=Ty> + 'a {
601+
// This unwrap() is safe because is_ty ensures that we definitely have a Ty
602+
self.parameters.iter().filter(|p| p.is_ty()).map(|p| p.clone().ty().unwrap())
603+
}
604+
}
605+
595606
#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)]
596607
pub enum PolarizedTraitRef {
597608
Positive(TraitRef),
@@ -709,6 +720,29 @@ pub enum DomainGoal {
709720
/// like `Box<T>`, it is true if `T` is local.
710721
IsLocal(Ty),
711722

723+
/// True if a type is *not* considered to have been "defined" by the current crate. This is
724+
/// false for a `struct Foo { }` but true for a `extern struct Foo { }`. However, for
725+
/// fundamental types like `Box<T>`, it is true if `T` is external.
726+
IsExternal(Ty),
727+
728+
/// True if a type both external and its type parameters are recursively external
729+
///
730+
/// More formally, for each non-fundamental struct S<P0..Pn> that is external:
731+
/// forall<P0..Pn> {
732+
/// IsDeeplyExternal(S<P0...Pn>) :-
733+
/// IsDeeplyExternal(P0),
734+
/// ...
735+
/// IsDeeplyExternal(Pn)
736+
/// }
737+
///
738+
/// For each fundamental struct S<P0>,
739+
///
740+
/// forall<P0> { IsDeeplyExternal(S<P0>) :- IsDeeplyExternal(P0) }
741+
///
742+
/// Note that any of these types can have lifetimes in their parameters too, but we only
743+
/// consider type parameters.
744+
IsDeeplyExternal(Ty),
745+
712746
/// Used to dictate when trait impls are allowed in the current (local) crate based on the
713747
/// orphan rules.
714748
///

‎src/ir/debug.rs

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -213,7 +213,15 @@ impl Debug for DomainGoal {
213213
DomainGoal::InScope(n) => write!(fmt, "InScope({:?})", n),
214214
DomainGoal::Derefs(n) => write!(fmt, "Derefs({:?})", n),
215215
DomainGoal::IsLocal(n) => write!(fmt, "IsLocal({:?})", n),
216-
DomainGoal::LocalImplAllowed(n) => write!(fmt, "LocalImplAllowed({:?})", n),
216+
DomainGoal::IsExternal(n) => write!(fmt, "IsExternal({:?})", n),
217+
DomainGoal::IsDeeplyExternal(n) => write!(fmt, "IsDeeplyExternal({:?})", n),
218+
DomainGoal::LocalImplAllowed(tr) => write!(
219+
fmt,
220+
"LocalImplAllowed({:?}: {:?}{:?})",
221+
tr.parameters[0],
222+
tr.trait_id,
223+
Angle(&tr.parameters[1..])
224+
),
217225
}
218226
}
219227
}

‎src/ir/lowering.rs

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -524,6 +524,15 @@ impl LowerDomainGoal for DomainGoal {
524524
DomainGoal::IsLocal { ty } => vec![
525525
ir::DomainGoal::IsLocal(ty.lower(env)?)
526526
],
527+
DomainGoal::IsExternal { ty } => vec![
528+
ir::DomainGoal::IsExternal(ty.lower(env)?)
529+
],
530+
DomainGoal::IsDeeplyExternal { ty } => vec![
531+
ir::DomainGoal::IsDeeplyExternal(ty.lower(env)?)
532+
],
533+
DomainGoal::LocalImplAllowed { trait_ref } => vec![
534+
ir::DomainGoal::LocalImplAllowed(trait_ref.lower(env)?)
535+
],
527536
};
528537
Ok(goals)
529538
}

‎src/rules.rs

Lines changed: 115 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -158,7 +158,7 @@ impl AssociatedTyValue {
158158
/// type IntoIter<'a>: 'a;
159159
/// }
160160
/// ```
161-
///
161+
///
162162
/// Then for the following impl:
163163
/// ```notrust
164164
/// impl<T> Iterable for Vec<T> {
@@ -300,7 +300,12 @@ impl StructDatum {
300300
// forall<T> { WF(Foo<T>) :- (T: Eq). }
301301
// forall<T> { FromEnv(T: Eq) :- FromEnv(Foo<T>). }
302302
//
303-
// If the type Foo is not marked `extern`, we also generate:
303+
// If the type Foo is marked `extern`, we also generate:
304+
//
305+
// forall<T> { IsExternal(Foo<T>) }
306+
// forall<T> { IsDeeplyExternal(Foo<T>) :- IsDeeplyExternal(T) }
307+
//
308+
// Otherwise, if the type Foo is not marked `extern`, we generate:
304309
//
305310
// forall<T> { IsLocal(Foo<T>) }
306311
//
@@ -312,6 +317,8 @@ impl StructDatum {
312317
// We generate the following clause:
313318
//
314319
// forall<T> { IsLocal(Box<T>) :- IsLocal(T) }
320+
// forall<T> { IsExternal(Box<T>) :- IsExternal(T) }
321+
// forall<T> { IsDeeplyExternal(Box<T>) :- IsDeeplyExternal(T) }
315322

316323
let wf = self.binders.map_ref(|bound_datum| {
317324
ProgramClauseImplication {
@@ -350,18 +357,45 @@ impl StructDatum {
350357
assert_eq!(self.binders.value.self_ty.len_type_parameters(), 1,
351358
"Only fundamental types with a single parameter are supported");
352359

353-
let local_fundamental = self.binders.map_ref(|bound_datum| ProgramClauseImplication {
354-
consequence: DomainGoal::IsLocal(bound_datum.self_ty.clone().cast()),
355-
conditions: vec![
356-
DomainGoal::IsLocal(
357-
// This unwrap is safe because we asserted above for the presence of a type
358-
// parameter
359-
bound_datum.self_ty.first_type_parameter().unwrap()
360-
).cast(),
361-
],
360+
// Fundamental types often have rules in the form of:
361+
// Goal(FundamentalType<T>) :- Goal(T)
362+
// This macro makes creating that kind of clause easy
363+
macro_rules! fundamental_rule {
364+
($goal:ident) => {
365+
clauses.push(self.binders.map_ref(|bound_datum| ProgramClauseImplication {
366+
consequence: DomainGoal::$goal(bound_datum.self_ty.clone().cast()),
367+
conditions: vec![
368+
DomainGoal::$goal(
369+
// This unwrap is safe because we asserted above for the presence of a type
370+
// parameter
371+
bound_datum.self_ty.first_type_parameter().unwrap()
372+
).cast(),
373+
],
374+
}).cast());
375+
};
376+
}
377+
378+
fundamental_rule!(IsLocal);
379+
fundamental_rule!(IsExternal);
380+
fundamental_rule!(IsDeeplyExternal);
381+
} else {
382+
// The type is just extern and not fundamental
383+
384+
let is_external = self.binders.map_ref(|bound_datum| ProgramClauseImplication {
385+
consequence: DomainGoal::IsExternal(bound_datum.self_ty.clone().cast()),
386+
conditions: Vec::new(),
362387
}).cast();
363388

364-
clauses.push(local_fundamental);
389+
clauses.push(is_external);
390+
391+
let is_deeply_external = self.binders.map_ref(|bound_datum| ProgramClauseImplication {
392+
consequence: DomainGoal::IsDeeplyExternal(bound_datum.self_ty.clone().cast()),
393+
conditions: bound_datum.self_ty.type_parameters()
394+
.map(|ty| DomainGoal::IsDeeplyExternal(ty).cast())
395+
.collect(),
396+
}).cast();
397+
398+
clauses.push(is_deeply_external);
365399
}
366400

367401
let condition = DomainGoal::FromEnv(
@@ -413,6 +447,43 @@ impl TraitDatum {
413447
//
414448
// forall<Self, T> { (Self: Ord<T>) :- FromEnv(Self: Ord<T>) }
415449
// forall<Self, T> { FromEnv(Self: Eq<T>) :- FromEnv(Self: Ord<T>) }
450+
//
451+
// As specified in the orphan rules, if a trait is not marked `extern`, the current crate
452+
// can implement it for any type. To represent that, we generate:
453+
//
454+
// // `Ord<T>` would not be `extern` when compiling `std`
455+
// forall<Self, T> { LocalImplAllowed(Self: Ord<T>) }
456+
//
457+
// For traits that are `extern` (i.e. not in the current crate), the orphan rules dictate
458+
// that impls are allowed as long as at least one type parameter is local and each type
459+
// prior to that is *deeply* external. That means that each type prior to the first local
460+
// type cannot contain any of the type parameters of the impl.
461+
//
462+
// This rule is fairly complex, so we expand it and generate a program clause for each
463+
// possible case. This is represented as follows:
464+
//
465+
// // for `extern trait Foo<T, U, V> where Self: Eq<T> { ... }`
466+
// forall<Self, T, U, V> {
467+
// LocalImplAllowed(Self: Foo<T, U, V>) :- IsLocal(Self)
468+
// }
469+
// forall<Self, T, U, V> {
470+
// LocalImplAllowed(Self: Foo<T, U, V>) :-
471+
// IsDeeplyExternal(Self),
472+
// IsLocal(T)
473+
// }
474+
// forall<Self, T, U, V> {
475+
// LocalImplAllowed(Self: Foo<T, U, V>) :-
476+
// IsDeeplyExternal(Self),
477+
// IsDeeplyExternal(T),
478+
// IsLocal(U)
479+
// }
480+
// forall<Self, T, U, V> {
481+
// LocalImplAllowed(Self: Foo<T, U, V>) :-
482+
// IsDeeplyExternal(Self),
483+
// IsDeeplyExternal(T),
484+
// IsDeeplyExternal(U),
485+
// IsLocal(V)
486+
// }
416487

417488
let trait_ref = self.binders.value.trait_ref.clone();
418489

@@ -437,6 +508,38 @@ impl TraitDatum {
437508
}).cast();
438509

439510
let mut clauses = vec![wf];
511+
512+
if !self.binders.value.flags.external {
513+
let impl_allowed = self.binders.map_ref(|bound_datum|
514+
ProgramClauseImplication {
515+
consequence: DomainGoal::LocalImplAllowed(bound_datum.trait_ref.clone()),
516+
conditions: Vec::new(),
517+
}
518+
).cast();
519+
520+
clauses.push(impl_allowed);
521+
} else {
522+
// The number of parameters will always be at least 1 because of the Self parameter
523+
// that is automatically added to every trait. This is important because otherwise
524+
// the added program clauses would not have any conditions.
525+
526+
let type_parameters: Vec<_> = self.binders.value.trait_ref.type_parameters().collect();
527+
528+
for i in 0..type_parameters.len() {
529+
let impl_maybe_allowed = self.binders.map_ref(|bound_datum|
530+
ProgramClauseImplication {
531+
consequence: DomainGoal::LocalImplAllowed(bound_datum.trait_ref.clone()),
532+
conditions: (0..i)
533+
.map(|j| DomainGoal::IsDeeplyExternal(type_parameters[j].clone()).cast())
534+
.chain(iter::once(DomainGoal::IsLocal(type_parameters[i].clone()).cast()))
535+
.collect(),
536+
}
537+
).cast();
538+
539+
clauses.push(impl_maybe_allowed);
540+
}
541+
}
542+
440543
let condition = DomainGoal::FromEnv(FromEnv::Trait(trait_ref.clone()));
441544

442545
for wc in self.binders

0 commit comments

Comments
 (0)