Skip to content

Use substitutions and suggestions in Solution; implement negation #36

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 7 commits into from
Jun 1, 2017
Merged

Use substitutions and suggestions in Solution; implement negation #36

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
7b7124a
Use substitutions and suggestions in Solution
aturon May 23, 2017
8158847
Introduce negation
aturon May 28, 2017
05bdfce
Treat unification with unequal skolemized type variables as ambiguous…
aturon May 30, 2017
3bd7bf4
Implement normalization fallback via lowering
aturon May 31, 2017
1444a69
Address most review nits and questions
aturon May 31, 2017
f79f6dd
Revamp normalization fallback to follow Niko's review suggestion
aturon May 31, 2017
d3e941e
Test fixup
aturon May 31, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions chalk-parse/src/ast.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -164,6 +164,7 @@ pub enum Goal {
Exists(Vec<ParameterKind>, Box<Goal>),
Implies(Vec<WhereClause>, Box<Goal>),
And(Box<Goal>, Box<Goal>),
Not(Box<Goal>),

// Additional kinds of goals:
Leaf(WhereClause),
Expand Down
1 change: 1 addition & 0 deletions chalk-parse/src/parser.lalrpop
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@ Goal1: Box<Goal> = {
"forall" "<" <p:Comma<ParameterKind>> ">" "{" <g:Goal> "}" => Box::new(Goal::ForAll(p, g)),
"exists" "<" <p:Comma<ParameterKind>> ">" "{" <g:Goal> "}" => Box::new(Goal::Exists(p, g)),
"if" "(" <w:Comma<WhereClause>> ")" "{" <g:Goal> "}" => Box::new(Goal::Implies(w, g)),
"not" "{" <g:Goal> "}" => Box::new(Goal::Not(g)),
<w:WhereClause> => Box::new(Goal::Leaf(w)),
};

Expand Down
4,786 changes: 2,522 additions & 2,264 deletions chalk-parse/src/parser.rs
View file
Open in desktop

Large diffs are not rendered by default.

11 changes: 7 additions & 4 deletions src/bin/repl.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,6 @@ use std::sync::Arc;

use chalk::ir;
use chalk::lower::*;
use chalk::solve::prove::Prove;
use chalk::solve::solver::Solver;

use rustyline::error::ReadlineError;
Expand Down Expand Up @@ -121,9 +120,13 @@ fn goal(text: &str, prog: &Program) -> Result<()> {
let goal = chalk_parse::parse_goal(text)?.lower(&*prog.ir)?;
let overflow_depth = 10;
let mut solver = Solver::new(&prog.env, overflow_depth);
match Prove::new(&mut solver, goal).solve() {
Ok(v) => println!("{:#?}", v),
Err(e) => println!("{}", e),
let goal = ir::Canonical {
value: ir::InEnvironment::new(&ir::Environment::new(), *goal),
binders: vec![],
};
match solver.solve_goal(goal) {
Ok(v) => println!("{}\n", v),
Err(e) => println!("No possible solution: {}\n", e),
}
Ok(())
}
74 changes: 34 additions & 40 deletions src/cast.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
use ir::*;
use solve::Solution;

pub trait Cast<T>: Sized {
fn cast(self) -> T;
Expand All @@ -23,59 +22,62 @@ macro_rules! reflexive_impl {
}

reflexive_impl!(TraitRef);
reflexive_impl!(WhereClause);
reflexive_impl!(WhereClauseGoal);
reflexive_impl!(LeafGoal);
reflexive_impl!(DomainGoal);

impl Cast<WhereClause> for TraitRef {
fn cast(self) -> WhereClause {
WhereClause::Implemented(self)
impl Cast<DomainGoal> for TraitRef {
fn cast(self) -> DomainGoal {
DomainGoal::Implemented(self)
}
}

impl Cast<WhereClauseGoal> for TraitRef {
fn cast(self) -> WhereClauseGoal {
WhereClauseGoal::Implemented(self)
impl Cast<LeafGoal> for TraitRef {
fn cast(self) -> LeafGoal {
LeafGoal::DomainGoal(self.cast())
}
}

impl Cast<WhereClause> for Normalize {
fn cast(self) -> WhereClause {
WhereClause::Normalize(self)
impl Cast<DomainGoal> for Normalize {
fn cast(self) -> DomainGoal {
DomainGoal::Normalize(self)
}
}

impl Cast<WhereClauseGoal> for Normalize {
fn cast(self) -> WhereClauseGoal {
WhereClauseGoal::Normalize(self)
impl Cast<LeafGoal> for Normalize {
fn cast(self) -> LeafGoal {
LeafGoal::DomainGoal(self.cast())
}
}

impl Cast<WhereClauseGoal> for WellFormed {
fn cast(self) -> WhereClauseGoal {
WhereClauseGoal::WellFormed(self)
impl Cast<DomainGoal> for WellFormed {
fn cast(self) -> DomainGoal {
DomainGoal::WellFormed(self)
}
}

impl Cast<LeafGoal> for WellFormed {
fn cast(self) -> LeafGoal {
LeafGoal::DomainGoal(self.cast())
}
}

impl Cast<Goal> for WellFormed {
fn cast(self) -> Goal {
let wcg: WhereClauseGoal = self.cast();
let wcg: LeafGoal = self.cast();
wcg.cast()
}
}

impl Cast<Goal> for Normalize {
fn cast(self) -> Goal {
let wcg: WhereClauseGoal = self.cast();
let wcg: LeafGoal = self.cast();
wcg.cast()
}
}

impl Cast<WhereClauseGoal> for WhereClause {
fn cast(self) -> WhereClauseGoal {
match self {
WhereClause::Implemented(a) => a.cast(),
WhereClause::Normalize(a) => a.cast(),
}
impl Cast<LeafGoal> for DomainGoal {
fn cast(self) -> LeafGoal {
LeafGoal::DomainGoal(self)
}
}

Expand All @@ -85,27 +87,21 @@ impl Cast<Goal> for TraitRef {
}
}

impl Cast<Goal> for WhereClause {
impl Cast<Goal> for DomainGoal {
fn cast(self) -> Goal {
Goal::Leaf(self.cast())
}
}

impl Cast<Goal> for WhereClauseGoal {
impl Cast<Goal> for LeafGoal {
fn cast(self) -> Goal {
Goal::Leaf(self)
}
}

impl Cast<WhereClauseGoal> for Unify<Ty> {
fn cast(self) -> WhereClauseGoal {
WhereClauseGoal::UnifyTys(self)
}
}

impl Cast<WhereClauseGoal> for Unify<Lifetime> {
fn cast(self) -> WhereClauseGoal {
WhereClauseGoal::UnifyLifetimes(self)
impl Cast<LeafGoal> for EqGoal {
fn cast(self) -> LeafGoal {
LeafGoal::EqGoal(self)
}
}

Expand All @@ -126,10 +122,8 @@ macro_rules! map_impl {
}

map_impl!(impl[T: Cast<U>, U] Cast<Option<U>> for Option<T>);
map_impl!(impl[T: Cast<U>, U] Cast<Query<U>> for Query<T>);
map_impl!(impl[T: Cast<U>, U] Cast<Solution<U>> for Solution<T>);
map_impl!(impl[T: Cast<U>, U] Cast<Canonical<U>> for Canonical<T>);
map_impl!(impl[T: Cast<U>, U] Cast<InEnvironment<U>> for InEnvironment<T>);
map_impl!(impl[T: Cast<U>, U] Cast<Constrained<U>> for Constrained<T>);
map_impl!(impl[T: Cast<U>, U, E] Cast<Result<U, E>> for Result<T, E>);

impl<T, U> Cast<Vec<U>> for Vec<T>
Expand Down
29 changes: 23 additions & 6 deletions src/fold/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ use errors::*;
use ir::*;
use std::fmt::Debug;
use std::sync::Arc;
use std::collections::BTreeMap;

mod instantiate;
mod shifted;
Expand Down Expand Up @@ -139,6 +140,23 @@ impl Fold for Lifetime {
}
}

impl Fold for Substitution {
type Result = Substitution;
fn fold_with(&self, folder: &mut Folder, binders: usize) -> Result<Self::Result> {
let mut tys = BTreeMap::new();
let mut lifetimes = BTreeMap::new();

for (var, ty) in &self.tys {
tys.insert(*var, ty.fold_with(folder, binders)?);
Copy link
Contributor

@nikomatsakis nikomatsakis May 31, 2017 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit: can't we write this with some kind of fancy collect() call? ;) (don't feel obligated)

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The ? here is what seems to make the imperative more clear and nearly as concise, sadly.

Copy link
Contributor

@nikomatsakis nikomatsakis May 31, 2017 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe something like this?

let tys = self.tys.iter()
    .map(|(&var, ty)| (var, ty.fold_with(folder, binders)?))
    .collect::<Result<BTreemap<_, _>>>()?;

Anyway, doesn't matter. More readable this way =)

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Right, that's exactly what I mean -- I find this iterator-chained version much harder to read...

}
for (var, lt) in &self.lifetimes {
lifetimes.insert(*var, lt.fold_with(folder, binders)?);
}

Ok(Substitution { tys, lifetimes })
}
}

macro_rules! copy_fold {
($t:ty) => {
impl Fold for $t {
Expand Down Expand Up @@ -178,12 +196,11 @@ macro_rules! enum_fold {
}

enum_fold!(ParameterKind[T,L] { Ty(a), Lifetime(a) } where T: Fold, L: Fold);
enum_fold!(WhereClause[] { Implemented(a), Normalize(a) });
enum_fold!(DomainGoal[] { Implemented(a), RawNormalize(a), Normalize(a), WellFormed(a) });
enum_fold!(WellFormed[] { Ty(a), TraitRef(a) });
enum_fold!(WhereClauseGoal[] { Implemented(a), Normalize(a), UnifyTys(a),
UnifyLifetimes(a), WellFormed(a) });
enum_fold!(LeafGoal[] { EqGoal(a), DomainGoal(a) });
enum_fold!(Constraint[] { LifetimeEq(a, b) });
enum_fold!(Goal[] { Quantified(qkind, subgoal), Implies(wc, subgoal), And(g1, g2), Leaf(wc) });
enum_fold!(Goal[] { Quantified(qkind, subgoal), Implies(wc, subgoal), And(g1, g2), Not(g), Leaf(wc) });

macro_rules! struct_fold {
($s:ident $([$($n:ident),*])* { $($name:ident),* } $($w:tt)*) => {
Expand All @@ -206,6 +223,6 @@ struct_fold!(AssociatedTyValue { associated_ty_id, value });
struct_fold!(AssociatedTyValueBound { ty, where_clauses });
struct_fold!(Environment { universe, clauses });
struct_fold!(InEnvironment[F] { environment, goal } where F: Fold);
struct_fold!(Unify[T] { a, b } where T: Fold);
struct_fold!(Constrained[F] { value, constraints } where F: Fold);
struct_fold!(EqGoal { a, b });
struct_fold!(ProgramClauseImplication { consequence, conditions });
struct_fold!(ConstrainedSubst { subst, constraints });
1 change: 1 addition & 0 deletions src/fold/shifter.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@ up_shift_method!(Ty);
up_shift_method!(Parameter);
up_shift_method!(Lifetime);
up_shift_method!(TraitRef);
up_shift_method!(ProjectionTy);

impl Folder for Shifter {
fn fold_free_var(&mut self, depth: usize, binders: usize) -> Result<Ty> {
Expand Down
26 changes: 10 additions & 16 deletions src/ir/debug.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -145,35 +145,28 @@ impl Debug for Normalize {
}
}

impl Debug for WhereClause {
impl Debug for DomainGoal {
fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
match *self {
WhereClause::Normalize(ref n) => write!(fmt, "{:?}", n),
WhereClause::Implemented(ref n) => {
DomainGoal::Normalize(ref n) => write!(fmt, "{:?}", n),
DomainGoal::RawNormalize(ref n) => write!(fmt, "raw {{ {:?} }}", n),
DomainGoal::Implemented(ref n) => {
write!(fmt,
"{:?}: {:?}{:?}",
n.parameters[0],
n.trait_id,
Angle(&n.parameters[1..]))
}
DomainGoal::WellFormed(ref n) => write!(fmt, "{:?}", n),
}
}
}

impl Debug for WhereClauseGoal {
impl Debug for LeafGoal {
fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
match *self {
WhereClauseGoal::Normalize(ref n) => write!(fmt, "{:?}", n),
WhereClauseGoal::Implemented(ref n) => {
write!(fmt,
"{:?}: {:?}{:?}",
n.parameters[0],
n.trait_id,
Angle(&n.parameters[1..]))
}
WhereClauseGoal::UnifyTys(ref n) => write!(fmt, "{:?}", n),
WhereClauseGoal::UnifyLifetimes(ref n) => write!(fmt, "{:?}", n),
WhereClauseGoal::WellFormed(ref n) => write!(fmt, "{:?}", n),
LeafGoal::EqGoal(ref eq) => write!(fmt, "{:?}", eq),
LeafGoal::DomainGoal(ref dom) => write!(fmt, "{:?}", dom),
}
}
}
Expand All @@ -188,7 +181,7 @@ impl Debug for WellFormed {
}
}

impl<T: Debug> Debug for Unify<T> {
impl Debug for EqGoal {
fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
write!(fmt, "({:?} = {:?})", self.a, self.b)
}
Expand All @@ -212,6 +205,7 @@ impl Debug for Goal {
}
Goal::Implies(ref wc, ref g) => write!(fmt, "if ({:?}) {{ {:?} }}", wc, g),
Goal::And(ref g1, ref g2) => write!(fmt, "({:?}, {:?})", g1, g2),
Goal::Not(ref g) => write!(fmt, "not {{ {:?} }}", g),
Goal::Leaf(ref wc) => write!(fmt, "{:?}", wc),
}
}
Expand Down
Loading