Skip to content

Commit 60554a9

Browse files
nikomatsakisnikomatsakis
authored
Merge pull request #160 from sunjay/isfullyvisible
Replacing IsDeeplyExternal with IsFullyVisible
2 parents ca82ca3 + 0b7b4a7 commit 60554a9

File tree

9 files changed

+174
-125
lines changed

9 files changed

+174
-125
lines changed

‎chalk-parse/src/ast.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -257,7 +257,7 @@ pub enum DomainGoal {
257257
Derefs { source: Ty, target: Ty },
258258
IsLocal { ty: Ty },
259259
IsUpstream { ty: Ty },
260-
IsDeeplyExternal { ty: Ty },
260+
IsFullyVisible { ty: Ty },
261261
LocalImplAllowed { trait_ref: TraitRef },
262262
}
263263

‎chalk-parse/src/parser.lalrpop

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -302,7 +302,7 @@ DomainGoal: DomainGoal = {
302302

303303
"IsLocal" "(" <ty:Ty> ")" => DomainGoal::IsLocal { ty },
304304
"IsUpstream" "(" <ty:Ty> ")" => DomainGoal::IsUpstream { ty },
305-
"IsDeeplyExternal" "(" <ty:Ty> ")" => DomainGoal::IsDeeplyExternal { ty },
305+
"IsFullyVisible" "(" <ty:Ty> ")" => DomainGoal::IsFullyVisible { ty },
306306

307307
"LocalImplAllowed" "(" <trait_ref:TraitRef<":">> ")" => DomainGoal::LocalImplAllowed { trait_ref },
308308
};

‎src/fold.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -427,7 +427,7 @@ 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), IsUpstream(a), IsDeeplyExternal(a),
430+
InScope(a), Derefs(a), IsLocal(a), IsUpstream(a), IsFullyVisible(a),
431431
LocalImplAllowed(a), Compatible(a), DownstreamType(a) });
432432
enum_fold!(LeafGoal[] { EqGoal(a), DomainGoal(a) });
433433
enum_fold!(Constraint[] { LifetimeEq(a, b) });

‎src/ir.rs

Lines changed: 7 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -746,23 +746,20 @@ pub enum DomainGoal {
746746
/// fundamental types like `Box<T>`, it is true if `T` is upstream.
747747
IsUpstream(Ty),
748748

749-
/// True if a type both external and its type parameters are recursively external
749+
/// True if a type and its input types are fully visible, known types. That is, there are no
750+
/// unknown type parameters anywhere in this type.
750751
///
751-
/// More formally, for each non-fundamental struct S<P0..Pn> that is external:
752+
/// More formally, for each struct S<P0..Pn>:
752753
/// forall<P0..Pn> {
753-
/// IsDeeplyExternal(S<P0...Pn>) :-
754-
/// IsDeeplyExternal(P0),
754+
/// IsFullyVisible(S<P0...Pn>) :-
755+
/// IsFullyVisible(P0),
755756
/// ...
756-
/// IsDeeplyExternal(Pn)
757+
/// IsFullyVisible(Pn)
757758
/// }
758759
///
759-
/// For each fundamental struct S<P0>,
760-
///
761-
/// forall<P0> { IsDeeplyExternal(S<P0>) :- IsDeeplyExternal(P0) }
762-
///
763760
/// Note that any of these types can have lifetimes in their parameters too, but we only
764761
/// consider type parameters.
765-
IsDeeplyExternal(Ty),
762+
IsFullyVisible(Ty),
766763

767764
/// Used to dictate when trait impls are allowed in the current (local) crate based on the
768765
/// orphan rules.

‎src/ir/debug.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -214,7 +214,7 @@ impl Debug for DomainGoal {
214214
DomainGoal::Derefs(n) => write!(fmt, "Derefs({:?})", n),
215215
DomainGoal::IsLocal(n) => write!(fmt, "IsLocal({:?})", n),
216216
DomainGoal::IsUpstream(n) => write!(fmt, "IsUpstream({:?})", n),
217-
DomainGoal::IsDeeplyExternal(n) => write!(fmt, "IsDeeplyExternal({:?})", n),
217+
DomainGoal::IsFullyVisible(n) => write!(fmt, "IsFullyVisible({:?})", n),
218218
DomainGoal::LocalImplAllowed(tr) => write!(
219219
fmt,
220220
"LocalImplAllowed({:?}: {:?}{:?})",

‎src/ir/lowering.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -524,8 +524,8 @@ impl LowerDomainGoal for DomainGoal {
524524
DomainGoal::IsUpstream { ty } => vec![
525525
ir::DomainGoal::IsUpstream(ty.lower(env)?)
526526
],
527-
DomainGoal::IsDeeplyExternal { ty } => vec![
528-
ir::DomainGoal::IsDeeplyExternal(ty.lower(env)?)
527+
DomainGoal::IsFullyVisible { ty } => vec![
528+
ir::DomainGoal::IsFullyVisible(ty.lower(env)?)
529529
],
530530
DomainGoal::LocalImplAllowed { trait_ref } => vec![
531531
ir::DomainGoal::LocalImplAllowed(trait_ref.lower(env)?)

‎src/rules.rs

Lines changed: 18 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -295,15 +295,15 @@ impl StructDatum {
295295
//
296296
// struct Foo<T: Eq> { }
297297
//
298-
// we generate the following clause:
298+
// we generate the following clauses:
299299
//
300300
// forall<T> { WF(Foo<T>) :- (T: Eq). }
301301
// forall<T> { FromEnv(T: Eq) :- FromEnv(Foo<T>). }
302+
// forall<T> { IsFullyVisible(Foo<T>) :- IsFullyVisible(T) }
302303
//
303304
// If the type Foo is marked `#[upstream]`, we also generate:
304305
//
305306
// forall<T> { IsUpstream(Foo<T>) }
306-
// forall<T> { IsDeeplyExternal(Foo<T>) :- IsDeeplyExternal(T) }
307307
//
308308
// Otherwise, if the type Foo is not marked `#[upstream]`, we generate:
309309
//
@@ -319,7 +319,6 @@ impl StructDatum {
319319
//
320320
// forall<T> { IsLocal(Box<T>) :- IsLocal(T) }
321321
// forall<T> { IsUpstream(Box<T>) :- IsUpstream(T) }
322-
// forall<T> { IsDeeplyExternal(Box<T>) :- IsDeeplyExternal(T) }
323322

324323
let wf = self.binders.map_ref(|bound_datum| {
325324
ProgramClauseImplication {
@@ -335,7 +334,14 @@ impl StructDatum {
335334
}
336335
}).cast();
337336

338-
let mut clauses = vec![wf];
337+
let is_fully_visible = self.binders.map_ref(|bound_datum| ProgramClauseImplication {
338+
consequence: DomainGoal::IsFullyVisible(bound_datum.self_ty.clone().cast()),
339+
conditions: bound_datum.self_ty.type_parameters()
340+
.map(|ty| DomainGoal::IsFullyVisible(ty).cast())
341+
.collect(),
342+
}).cast();
343+
344+
let mut clauses = vec![wf, is_fully_visible];
339345

340346
// Types that are not marked `#[upstream]` satisfy IsLocal(TypeName)
341347
if !self.binders.value.flags.upstream {
@@ -378,7 +384,6 @@ impl StructDatum {
378384

379385
fundamental_rule!(IsLocal);
380386
fundamental_rule!(IsUpstream);
381-
fundamental_rule!(IsDeeplyExternal);
382387
} else {
383388
// The type is just upstream and not fundamental
384389

@@ -388,15 +393,6 @@ impl StructDatum {
388393
}).cast();
389394

390395
clauses.push(is_upstream);
391-
392-
let is_deeply_external = self.binders.map_ref(|bound_datum| ProgramClauseImplication {
393-
consequence: DomainGoal::IsDeeplyExternal(bound_datum.self_ty.clone().cast()),
394-
conditions: bound_datum.self_ty.type_parameters()
395-
.map(|ty| DomainGoal::IsDeeplyExternal(ty).cast())
396-
.collect(),
397-
}).cast();
398-
399-
clauses.push(is_deeply_external);
400396
}
401397

402398
let condition = DomainGoal::FromEnv(
@@ -457,7 +453,7 @@ impl TraitDatum {
457453
//
458454
// For traits that are `#[upstream]` (i.e. not in the current crate), the orphan rules dictate
459455
// that impls are allowed as long as at least one type parameter is local and each type
460-
// prior to that is *deeply* external. That means that each type prior to the first local
456+
// prior to that is fully visible. That means that each type prior to the first local
461457
// type cannot contain any of the type parameters of the impl.
462458
//
463459
// This rule is fairly complex, so we expand it and generate a program clause for each
@@ -469,20 +465,20 @@ impl TraitDatum {
469465
// }
470466
// forall<Self, T, U, V> {
471467
// LocalImplAllowed(Self: Foo<T, U, V>) :-
472-
// IsDeeplyExternal(Self),
468+
// IsFullyVisible(Self),
473469
// IsLocal(T)
474470
// }
475471
// forall<Self, T, U, V> {
476472
// LocalImplAllowed(Self: Foo<T, U, V>) :-
477-
// IsDeeplyExternal(Self),
478-
// IsDeeplyExternal(T),
473+
// IsFullyVisible(Self),
474+
// IsFullyVisible(T),
479475
// IsLocal(U)
480476
// }
481477
// forall<Self, T, U, V> {
482478
// LocalImplAllowed(Self: Foo<T, U, V>) :-
483-
// IsDeeplyExternal(Self),
484-
// IsDeeplyExternal(T),
485-
// IsDeeplyExternal(U),
479+
// IsFullyVisible(Self),
480+
// IsFullyVisible(T),
481+
// IsFullyVisible(U),
486482
// IsLocal(V)
487483
// }
488484

@@ -531,7 +527,7 @@ impl TraitDatum {
531527
ProgramClauseImplication {
532528
consequence: DomainGoal::LocalImplAllowed(bound_datum.trait_ref.clone()),
533529
conditions: (0..i)
534-
.map(|j| DomainGoal::IsDeeplyExternal(type_parameters[j].clone()).cast())
530+
.map(|j| DomainGoal::IsFullyVisible(type_parameters[j].clone()).cast())
535531
.chain(iter::once(DomainGoal::IsLocal(type_parameters[i].clone()).cast()))
536532
.collect(),
537533
}

0 commit comments

Comments
 (0)