Skip to content

Commit 58365b7

Browse files
scalexmscalexm
committed
Elaborate where clauses in Implies goals
1 parent ae79dfd commit 58365b7

File tree

6 files changed

+80
-18
lines changed

6 files changed

+80
-18
lines changed

‎chalk-parse/src/ast.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -162,7 +162,7 @@ pub struct Field {
162162
pub enum Goal {
163163
ForAll(Vec<ParameterKind>, Box<Goal>),
164164
Exists(Vec<ParameterKind>, Box<Goal>),
165-
Implies(Vec<WhereClause>, Box<Goal>),
165+
Implies(Vec<WhereClause>, Box<Goal>, bool),
166166
And(Box<Goal>, Box<Goal>),
167167
Not(Box<Goal>),
168168

‎chalk-parse/src/parser.lalrpop

+2-1
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,8 @@ pub Goal: Box<Goal> = {
2828
Goal1: Box<Goal> = {
2929
"forall" "<" <p:Comma<ParameterKind>> ">" "{" <g:Goal> "}" => Box::new(Goal::ForAll(p, g)),
3030
"exists" "<" <p:Comma<ParameterKind>> ">" "{" <g:Goal> "}" => Box::new(Goal::Exists(p, g)),
31-
"if" "(" <w:Comma<WhereClause>> ")" "{" <g:Goal> "}" => Box::new(Goal::Implies(w, g)),
31+
"if" "(" <w:Comma<WhereClause>> ")" "{" <g:Goal> "}" => Box::new(Goal::Implies(w, g, true)),
32+
"if_raw" "(" <w:Comma<WhereClause>> ")" "{" <g:Goal> "}" => Box::new(Goal::Implies(w, g, false)),
3233
"not" "{" <g:Goal> "}" => Box::new(Goal::Not(g)),
3334
<w:WhereClause> => Box::new(Goal::Leaf(w)),
3435
};

‎src/cast.rs

+32-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
use ir::*;
2+
use std::marker::PhantomData;
23

34
pub trait Cast<T>: Sized {
45
fn cast(self) -> T;
@@ -130,7 +131,7 @@ impl<T, U> Cast<Vec<U>> for Vec<T>
130131
where T: Cast<U>
131132
{
132133
fn cast(self) -> Vec<U> {
133-
self.into_iter().map(|v| v.cast()).collect()
134+
self.into_iter().casted().collect()
134135
}
135136
}
136137

@@ -145,3 +146,33 @@ impl Cast<Parameter> for Lifetime {
145146
ParameterKind::Lifetime(self)
146147
}
147148
}
149+
150+
pub struct Casted<I, U> {
151+
iterator: I,
152+
_cast: PhantomData<U>,
153+
}
154+
155+
impl<I: Iterator, U> Iterator for Casted<I, U> where I::Item: Cast<U> {
156+
type Item = U;
157+
158+
fn next(&mut self) -> Option<Self::Item> {
159+
self.iterator.next().map(|item| item.cast())
160+
}
161+
162+
fn size_hint(&self) -> (usize, Option<usize>) {
163+
self.iterator.size_hint()
164+
}
165+
}
166+
167+
pub trait Caster<U>: Sized {
168+
fn casted(self) -> Casted<Self, U>;
169+
}
170+
171+
impl<I: Iterator, U> Caster<U> for I {
172+
fn casted(self) -> Casted<Self, U> {
173+
Casted {
174+
iterator: self,
175+
_cast: PhantomData,
176+
}
177+
}
178+
}

‎src/ir/mod.rs

+1-2
Original file line numberDiff line numberDiff line change
@@ -366,7 +366,7 @@ impl DomainGoal {
366366
}
367367

368368
/// A clause of the form (T: Foo) expands to (T: Foo), WF(T: Foo).
369-
/// A clause of the form (T: Foo<Item = U>) expands to (T: Foo<Item = U>), (T: Foo), WF(T: Foo).
369+
/// A clause of the form (T: Foo<Item = U>) expands to (T: Foo<Item = U>), WF(T: Foo).
370370
pub fn expanded(self, program: &Program) -> impl Iterator<Item = DomainGoal> {
371371
let mut expanded = vec![];
372372
match self {
@@ -379,7 +379,6 @@ impl DomainGoal {
379379
trait_id: associated_ty_data.trait_id,
380380
parameters: trait_params.to_owned()
381381
};
382-
expanded.push(trait_ref.clone().cast());
383382
expanded.push(WellFormed::TraitRef(trait_ref).cast());
384383
}
385384
_ => ()

‎src/lower/mod.rs

+21-8
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ use std::collections::HashMap;
33
use chalk_parse::ast::*;
44
use lalrpop_intern::intern;
55

6-
use cast::Cast;
6+
use cast::{Cast, Caster};
77
use errors::*;
88
use ir;
99

@@ -720,8 +720,19 @@ impl<'k> LowerGoal<Env<'k>> for Goal {
720720
g.lower_quantified(env, ir::QuantifierKind::ForAll, ids),
721721
Goal::Exists(ref ids, ref g) =>
722722
g.lower_quantified(env, ir::QuantifierKind::Exists, ids),
723-
Goal::Implies(ref wc, ref g) =>
724-
Ok(Box::new(ir::Goal::Implies(wc.lower(env)?, g.lower(env)?))),
723+
Goal::Implies(ref wc, ref g, ref elaborate) => {
724+
let mut where_clauses = wc.lower(env)?;
725+
if *elaborate {
726+
where_clauses = ir::with_current_program(|program| {
727+
let program = program.expect("cannot elaborate without a program");
728+
where_clauses.into_iter()
729+
.flat_map(|wc| wc.expanded(program))
730+
.casted()
731+
.collect()
732+
});
733+
}
734+
Ok(Box::new(ir::Goal::Implies(where_clauses, g.lower(env)?)))
735+
}
725736
Goal::And(ref g1, ref g2) =>
726737
Ok(Box::new(ir::Goal::And(g1.lower(env)?, g2.lower(env)?))),
727738
Goal::Not(ref g) =>
@@ -798,7 +809,7 @@ impl ir::ImplDatum {
798809
.iter()
799810
.cloned()
800811
.flat_map(|wc| wc.expanded(program))
801-
.map(|wc| wc.cast())
812+
.casted()
802813
.collect(),
803814
}
804815
}),
@@ -930,12 +941,13 @@ impl ir::StructDatum {
930941
.iter()
931942
.filter_map(|pk| pk.as_ref().ty())
932943
.cloned()
933-
.map(|ty| ir::WellFormed::Ty(ty).cast());
944+
.map(|ty| ir::WellFormed::Ty(ty))
945+
.casted();
934946

935947
let where_clauses = bound_datum.where_clauses.iter()
936948
.cloned()
937949
.flat_map(|wc| wc.expanded(program))
938-
.map(|wc| wc.cast());
950+
.casted();
939951

940952
tys.chain(where_clauses).collect()
941953
}
@@ -982,9 +994,10 @@ impl ir::TraitDatum {
982994
.iter()
983995
.filter_map(|pk| pk.as_ref().ty())
984996
.cloned()
985-
.map(|ty| ir::WellFormed::Ty(ty).cast());
997+
.map(|ty| ir::WellFormed::Ty(ty))
998+
.casted();
986999

987-
tys.chain(where_clauses.iter().cloned().map(|wc| wc.cast())).collect()
1000+
tys.chain(where_clauses.iter().cloned().casted()).collect()
9881001
}
9891002
}
9901003
}),

‎src/solve/test.rs

+23-5
Original file line numberDiff line numberDiff line change
@@ -175,13 +175,23 @@ fn prove_forall() {
175175
// Here, we do know that `T: Clone`, so we can.
176176
goal {
177177
forall<T> {
178-
if (WellFormed(T: Clone), T: Clone) {
178+
if (T: Clone) {
179179
Vec<T>: Clone
180180
}
181181
}
182182
} yields {
183183
"Unique; substitution [], lifetime constraints []"
184184
}
185+
186+
goal {
187+
forall<T> {
188+
if_raw (T: Clone) {
189+
Vec<T>: Clone
190+
}
191+
}
192+
} yields {
193+
"CannotProve"
194+
}
185195
}
186196
}
187197

@@ -546,7 +556,7 @@ fn elaborate_eq() {
546556

547557
goal {
548558
forall<T> {
549-
if (WellFormed(T: Eq)) {
559+
if (T: Eq) {
550560
T: PartialEq
551561
}
552562
}
@@ -567,7 +577,7 @@ fn elaborate_transitive() {
567577

568578
goal {
569579
forall<T> {
570-
if (WellFormed(T: StrictEq)) {
580+
if (T: StrictEq) {
571581
T: PartialEq
572582
}
573583
}
@@ -596,7 +606,7 @@ fn elaborate_normalize() {
596606

597607
goal {
598608
forall<T, U> {
599-
if (WellFormed(T: Item), T: Item<Out = U>) {
609+
if (T: Item<Out = U>) {
600610
U: Eq
601611
}
602612
}
@@ -753,6 +763,8 @@ fn trait_wf() {
753763

754764
impl Ord<Int> for Int { }
755765
impl<T> Ord<Vec<T>> for Vec<T> where T: Ord<T> { }
766+
767+
impl<T> Ord<Slice<T>> for Slice<T> { }
756768
}
757769

758770
goal {
@@ -779,13 +791,19 @@ fn trait_wf() {
779791
"Unique; substitution [], lifetime constraints []"
780792
}
781793

794+
goal {
795+
Slice<Int>: Ord<Slice<Int>>
796+
} yields {
797+
"Unique"
798+
}
799+
782800
goal {
783801
Slice<Int>: Eq<Slice<Int>>
784802
} yields {
785803
"No possible solution"
786804
}
787805

788-
// not WF because previous equation doesn't hold
806+
// not WF because previous equation doesn't hold, despite Slice<Int> having an impl for Ord<Int>
789807
goal {
790808
WellFormed(Slice<Int>: Ord<Slice<Int>>)
791809
} yields {

0 commit comments

Comments
 (0)