Skip to content

Commit 55dea16

Browse files
authored
Merge pull request #110 from leodasvacas/deref-first-class-domain-goal
Deref domain goal
2 parents 5e26056 + d1895b9 commit 55dea16

File tree

11 files changed

+153
-4
lines changed

11 files changed

+153
-4
lines changed

chalk-parse/src/ast.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,7 @@ pub struct TraitFlags {
4848
pub auto: bool,
4949
pub marker: bool,
5050
pub external: bool,
51+
pub deref: bool,
5152
}
5253

5354
pub struct AssocTyDefn {
@@ -192,6 +193,7 @@ pub enum WhereClause {
192193
UnifyTys { a: Ty, b: Ty },
193194
UnifyLifetimes { a: Lifetime, b: Lifetime },
194195
TraitInScope { trait_name: Identifier },
196+
Derefs { source: Ty, target: Ty },
195197
}
196198

197199
pub struct QuantifiedWhereClause {

chalk-parse/src/parser.lalrpop

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,7 @@ Goal1: Box<Goal> = {
3838
ExternalKeyword: () = "extern";
3939
AutoKeyword: () = "#" "[" "auto" "]";
4040
MarkerKeyword: () = "#" "[" "marker" "]";
41+
DerefLangItem: () = "#" "[" "lang_deref" "]";
4142

4243
StructDefn: StructDefn = {
4344
<external:ExternalKeyword?> "struct" <n:Id><p:Angle<ParameterKind>>
@@ -54,7 +55,7 @@ StructDefn: StructDefn = {
5455
};
5556

5657
TraitDefn: TraitDefn = {
57-
<external:ExternalKeyword?> <auto:AutoKeyword?> <marker:MarkerKeyword?> "trait" <n:Id><p:Angle<ParameterKind>>
58+
<external:ExternalKeyword?> <auto:AutoKeyword?> <marker:MarkerKeyword?> <deref:DerefLangItem?> "trait" <n:Id><p:Angle<ParameterKind>>
5859
<w:QuantifiedWhereClauses> "{" <a:AssocTyDefn*> "}" => TraitDefn
5960
{
6061
name: n,
@@ -65,6 +66,7 @@ TraitDefn: TraitDefn = {
6566
auto: auto.is_some(),
6667
marker: marker.is_some(),
6768
external: external.is_some(),
69+
deref: deref.is_some(),
6870
},
6971
}
7072
};
@@ -239,6 +241,7 @@ WhereClause: WhereClause = {
239241
},
240242

241243
"InScope" "(" <t:Id> ")" => WhereClause::TraitInScope { trait_name: t },
244+
"Derefs" "(" <source:Ty> "," <target:Ty> ")" => WhereClause::Derefs { source, target },
242245
};
243246

244247
QuantifiedWhereClause: QuantifiedWhereClause = {

src/errors.rs

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,5 +50,10 @@ error_chain! {
5050
description("could not match")
5151
display("could not match")
5252
}
53+
54+
DuplicateLangItem(item: ir::LangItem) {
55+
description("Duplicate lang item")
56+
display("Duplicate lang item `{:?}`", item)
57+
}
5358
}
5459
}

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), Derefs(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!(Derefs { 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::Derefs(n) => write!(fmt, "Derefs({:?})", n),
208209
}
209210
}
210211
}

src/ir/mod.rs

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,9 @@ pub struct Program {
3838

3939
/// For each user-specified clause
4040
crate custom_clauses: Vec<ProgramClause>,
41+
42+
/// Special types and traits.
43+
crate lang_items: BTreeMap<LangItem, ItemId>,
4144
}
4245

4346
impl Program {
@@ -71,6 +74,11 @@ pub struct ProgramEnvironment {
7174
crate program_clauses: Vec<ProgramClause>,
7275
}
7376

77+
#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
78+
pub enum LangItem {
79+
DerefTrait,
80+
}
81+
7482
#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
7583
/// The set of assumptions we've made so far, and the current number of
7684
/// universal (forall) quantifiers we're within.
@@ -244,6 +252,7 @@ pub struct TraitFlags {
244252
crate auto: bool,
245253
crate marker: bool,
246254
crate external: bool,
255+
pub deref: bool,
247256
}
248257

249258
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
@@ -454,6 +463,12 @@ pub enum WhereClauseAtom {
454463
ProjectionEq(ProjectionEq),
455464
}
456465

466+
#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)]
467+
pub struct Derefs {
468+
pub source: Ty,
469+
pub target: Ty,
470+
}
471+
457472
/// A "domain goal" is a goal that is directly about Rust, rather than a pure
458473
/// logical statement. As much as possible, the Chalk solver should avoid
459474
/// decomposing this enum, and instead treat its values opaquely.
@@ -516,6 +531,13 @@ pub enum DomainGoal {
516531
FromEnvTy(Ty),
517532

518533
InScope(ItemId),
534+
535+
/// Whether a type can deref into another. Right now this is just:
536+
/// ```notrust
537+
/// Derefs(T, U) :- Implemented(T: Deref<Target = U>)
538+
/// ```
539+
/// In Rust there are also raw pointers which can be deref'd but do not implement Deref.
540+
Derefs(Derefs)
519541
}
520542

521543
pub type QuantifiedDomainGoal = Binders<DomainGoal>;

src/lower/mod.rs

Lines changed: 46 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -172,6 +172,7 @@ impl LowerProgram for Program {
172172
let mut impl_data = BTreeMap::new();
173173
let mut associated_ty_data = BTreeMap::new();
174174
let mut custom_clauses = Vec::new();
175+
let mut lang_items = BTreeMap::new();
175176
for (item, &item_id) in self.items.iter().zip(&item_ids) {
176177
let empty_env = Env {
177178
type_ids: &type_ids,
@@ -204,6 +205,16 @@ impl LowerProgram for Program {
204205
},
205206
);
206207
}
208+
209+
if d.flags.deref {
210+
use std::collections::btree_map::Entry::*;
211+
match lang_items.entry(ir::LangItem::DerefTrait) {
212+
Vacant(entry) => { entry.insert(item_id); },
213+
Occupied(_) => {
214+
bail!(ErrorKind::DuplicateLangItem(ir::LangItem::DerefTrait))
215+
}
216+
}
217+
}
207218
}
208219
Item::Impl(ref d) => {
209220
impl_data.insert(item_id, d.lower_impl(&empty_env)?);
@@ -222,6 +233,7 @@ impl LowerProgram for Program {
222233
impl_data,
223234
associated_ty_data,
224235
custom_clauses,
236+
lang_items,
225237
default_impl_data: Vec::new(),
226238
};
227239
program.add_default_impls();
@@ -472,6 +484,12 @@ impl LowerWhereClause<ir::DomainGoal> for WhereClause {
472484

473485
ir::DomainGoal::InScope(id)
474486
}
487+
WhereClause::Derefs { source, target } => {
488+
ir::DomainGoal::Derefs(ir::Derefs {
489+
source: source.lower(env)?,
490+
target: target.lower(env)?
491+
})
492+
}
475493
})
476494
}
477495
}
@@ -499,7 +517,8 @@ impl LowerWhereClause<ir::LeafGoal> for WhereClause {
499517
| WhereClause::TyWellFormed { .. }
500518
| WhereClause::TraitRefWellFormed { .. }
501519
| WhereClause::TyFromEnv { .. }
502-
| WhereClause::TraitRefFromEnv { .. } => {
520+
| WhereClause::TraitRefFromEnv { .. }
521+
| WhereClause::Derefs { .. } => {
503522
let g: ir::DomainGoal = self.lower(env)?;
504523
g.cast()
505524
}
@@ -903,6 +922,7 @@ impl LowerTrait for TraitDefn {
903922
auto: self.flags.auto,
904923
marker: self.flags.marker,
905924
external: self.flags.external,
925+
deref: self.flags.deref,
906926
},
907927
})
908928
})?;
@@ -1026,6 +1046,31 @@ impl ir::Program {
10261046
);
10271047
program_clauses.extend(self.default_impl_data.iter().map(|d| d.to_program_clause()));
10281048

1049+
// Adds clause that defines the Derefs domain goal:
1050+
// forall<T, U> { Derefs(T, U) :- ProjectionEq(<T as Deref>::Target = U>) }
1051+
if let Some(trait_id) = self.lang_items.get(&ir::LangItem::DerefTrait) {
1052+
// Find `Deref::Target`.
1053+
let associated_ty_id = self.associated_ty_data.values()
1054+
.find(|d| d.trait_id == *trait_id)
1055+
.expect("Deref has no assoc item")
1056+
.id;
1057+
let t = || ir::Ty::Var(0);
1058+
let u = || ir::Ty::Var(1);
1059+
program_clauses.push(ir::Binders {
1060+
binders: vec![ir::ParameterKind::Ty(()), ir::ParameterKind::Ty(())],
1061+
value: ir::ProgramClauseImplication {
1062+
consequence: ir::DomainGoal::Derefs(ir::Derefs { source: t(), target: u() }),
1063+
conditions: vec![ir::ProjectionEq {
1064+
projection: ir::ProjectionTy {
1065+
associated_ty_id,
1066+
parameters: vec![t().cast()]
1067+
},
1068+
ty: u(),
1069+
}.cast()]
1070+
},
1071+
}.cast());
1072+
}
1073+
10291074
for datum in self.impl_data.values() {
10301075
// If we encounter a negative impl, do not generate any rule. Negative impls
10311076
// are currently just there to deactivate default impls for auto traits.

src/lower/test.rs

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -850,3 +850,21 @@ fn higher_ranked_cyclic_requirements() {
850850
}
851851
}
852852
}
853+
854+
#[test]
855+
fn deref_trait() {
856+
lowering_success! {
857+
program {
858+
#[lang_deref] trait Deref { type Target; }
859+
}
860+
}
861+
862+
lowering_error! {
863+
program {
864+
#[lang_deref] trait Deref { }
865+
#[lang_deref] trait DerefDupe { }
866+
} error_msg {
867+
"Duplicate lang item `DerefTrait`"
868+
}
869+
}
870+
}

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::Derefs(..) => panic!("unexpected where clause"),
142143

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

src/solve/test/mod.rs

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2058,3 +2058,52 @@ fn higher_ranked_implied_bounds() {
20582058
}
20592059
}
20602060
}
2061+
2062+
#[test]
2063+
fn deref_goal() {
2064+
test! {
2065+
program {
2066+
#[lang_deref]
2067+
trait Deref { type Target; }
2068+
struct Foo { }
2069+
struct Bar { }
2070+
struct Baz { }
2071+
impl Deref for Foo { type Target = Bar; }
2072+
}
2073+
2074+
goal {
2075+
Derefs(Foo, Bar)
2076+
} yields {
2077+
"Unique"
2078+
}
2079+
2080+
goal {
2081+
Derefs(Foo, Baz)
2082+
} yields {
2083+
"No possible solution"
2084+
}
2085+
}
2086+
2087+
test! {
2088+
program {
2089+
#[lang_deref]
2090+
trait Deref { type Target; }
2091+
struct Arc<T> { }
2092+
struct i32 { }
2093+
struct u64 { }
2094+
impl<T> Deref for Arc<T> { type Target = T; }
2095+
}
2096+
2097+
goal {
2098+
Derefs(Arc<i32>, i32)
2099+
} yields {
2100+
"Unique"
2101+
}
2102+
2103+
goal {
2104+
Derefs(Arc<i32>, u64)
2105+
} yields {
2106+
"No possible solution"
2107+
}
2108+
}
2109+
}

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!(Derefs { 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+
Derefs
228230
});
229231
enum_zip!(LeafGoal { DomainGoal, EqGoal });
230232
enum_zip!(ProgramClause { Implies, ForAll });

0 commit comments

Comments
 (0)