Skip to content

Commit 61e90fd

Browse files
committed
Deref domain goal.
1 parent c0afedb commit 61e90fd

File tree

5 files changed

+21
-2
lines changed

5 files changed

+21
-2
lines changed

src/fold/mod.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -425,7 +425,7 @@ enum_fold!(PolarizedTraitRef[] { Positive(a), Negative(a) });
425425
enum_fold!(ParameterKind[T,L] { Ty(a), Lifetime(a) } where T: Fold, L: Fold);
426426
enum_fold!(WhereClauseAtom[] { Implemented(a), ProjectionEq(a) });
427427
enum_fold!(DomainGoal[] { Holds(a), WellFormed(a), FromEnv(a), Normalize(a), UnselectedNormalize(a),
428-
WellFormedTy(a), FromEnvTy(a), InScope(a) });
428+
WellFormedTy(a), FromEnvTy(a), InScope(a), Deref(a) });
429429
enum_fold!(LeafGoal[] { EqGoal(a), DomainGoal(a) });
430430
enum_fold!(Constraint[] { LifetimeEq(a, b) });
431431
enum_fold!(Goal[] { Quantified(qkind, subgoal), Implies(wc, subgoal), And(g1, g2), Not(g),
@@ -571,6 +571,7 @@ struct_fold!(AssociatedTyValueBound { ty, where_clauses });
571571
struct_fold!(Environment { clauses });
572572
struct_fold!(InEnvironment[F] { environment, goal } where F: Fold<Result = F>);
573573
struct_fold!(EqGoal { a, b });
574+
struct_fold!(Deref { source, target });
574575
struct_fold!(ProgramClauseImplication {
575576
consequence,
576577
conditions,

src/ir/debug.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -205,6 +205,7 @@ impl Debug for DomainGoal {
205205
DomainGoal::WellFormedTy(t) => write!(fmt, "WellFormed({:?})", t),
206206
DomainGoal::FromEnvTy(t) => write!(fmt, "FromEnv({:?})", t),
207207
DomainGoal::InScope(n) => write!(fmt, "InScope({:?})", n),
208+
DomainGoal::Deref(n) => write!(fmt, "Deref({:?})", n),
208209
}
209210
}
210211
}

src/ir/mod.rs

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -454,6 +454,12 @@ pub enum WhereClauseAtom {
454454
ProjectionEq(ProjectionEq),
455455
}
456456

457+
#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)]
458+
pub struct Deref {
459+
pub source: Ty,
460+
pub target: Ty,
461+
}
462+
457463
/// A "domain goal" is a goal that is directly about Rust, rather than a pure
458464
/// logical statement. As much as possible, the Chalk solver should avoid
459465
/// decomposing this enum, and instead treat its values opaquely.
@@ -516,6 +522,14 @@ pub enum DomainGoal {
516522
FromEnvTy(Ty),
517523

518524
InScope(ItemId),
525+
526+
/// Whether a type can Deref into another. Right now this is just:
527+
/// ```notrust
528+
/// Deref(T, U) :- Implemented(T: Deref<Target = U>)
529+
/// ```
530+
/// In Rust there are also raw pointers which can be deref'd
531+
/// but do not implement Deref.
532+
Deref(Deref)
519533
}
520534

521535
pub type QuantifiedDomainGoal = Binders<DomainGoal>;

src/lower/wf.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -138,7 +138,8 @@ impl FoldInputTypes for DomainGoal {
138138
DomainGoal::WellFormed(..) |
139139
DomainGoal::FromEnv(..) |
140140
DomainGoal::WellFormedTy(..) |
141-
DomainGoal::FromEnvTy(..) => panic!("unexpected where clause"),
141+
DomainGoal::FromEnvTy(..) |
142+
DomainGoal::Deref(..) => panic!("unexpected where clause"),
142143

143144
DomainGoal::InScope(..) => (),
144145
}

src/zip.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -182,6 +182,7 @@ struct_zip!(ProjectionEq { projection, ty });
182182
struct_zip!(UnselectedNormalize { projection, ty });
183183
struct_zip!(EqGoal { a, b });
184184
struct_zip!(ProgramClauseImplication { consequence, conditions });
185+
struct_zip!(Deref { source, target });
185186

186187
impl Zip for Environment {
187188
fn zip_with<Z: Zipper>(zipper: &mut Z, a: &Self, b: &Self) -> Fallible<()> {
@@ -225,6 +226,7 @@ enum_zip!(DomainGoal {
225226
WellFormedTy,
226227
FromEnvTy,
227228
InScope,
229+
Deref
228230
});
229231
enum_zip!(LeafGoal { DomainGoal, EqGoal });
230232
enum_zip!(ProgramClause { Implies, ForAll });

0 commit comments

Comments
 (0)