Skip to content

Add CannotProve solution #45

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 3 commits into from
Jun 13, 2017
Merged

Add CannotProve solution #45

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
11d7040
Add `CannotProve` solution
scalexm Jun 13, 2017
722ecfb
Put back a missing debug message
scalexm Jun 13, 2017
faae05a
Add some comments
scalexm Jun 13, 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
46 changes: 28 additions & 18 deletions src/solve/fulfill.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,10 +23,6 @@ impl Outcome {
}
}

pub struct UnifyOutcome {
pub ambiguous: bool,
}

/// A goal that must be resolved
#[derive(Clone, Debug, PartialEq, Eq)]
enum Obligation {
Expand All @@ -53,6 +49,7 @@ struct PositiveSolution {
enum NegativeSolution {
Refuted,
Ambiguous,
CannotProve,
}

/// A `Fulfill` is where we actually break down complex goals, instantiate
Expand All @@ -77,8 +74,9 @@ pub struct Fulfill<'s> {
constraints: HashSet<InEnvironment<Constraint>>,

/// Record that a goal has been processed that can neither be proved nor
/// refuted, and thus the overall solution cannot be `Unique`
ambiguous: bool,
/// refuted. In such a case the solution will be either `CannotProve`, or `Err`
/// in the case where some other goal leads to an error.
cannot_prove: bool,
}

impl<'s> Fulfill<'s> {
Expand All @@ -88,7 +86,7 @@ impl<'s> Fulfill<'s> {
infer: InferenceTable::new(),
obligations: vec![],
constraints: HashSet::new(),
ambiguous: false,
cannot_prove: false,
}
}

Expand Down Expand Up @@ -119,19 +117,19 @@ impl<'s> Fulfill<'s> {
///
/// Wraps `InferenceTable::unify`; any resulting normalizations are added
/// into our list of pending obligations with the given environment.
pub fn unify<T>(&mut self, environment: &Arc<Environment>, a: &T, b: &T) -> Result<UnifyOutcome>
pub fn unify<T>(&mut self, environment: &Arc<Environment>, a: &T, b: &T) -> Result<()>
where T: ?Sized + Zip + Debug
{
let UnificationResult { goals, constraints, ambiguous } =
let UnificationResult { goals, constraints, cannot_prove } =
self.infer.unify(environment, a, b)?;
debug!("unify({:?}, {:?}) succeeded", a, b);
debug!("unify: goals={:?}", goals);
debug!("unify: constraints={:?}", constraints);
debug!("unify: ambiguous={:?}", ambiguous);
debug!("unify: cannot_prove={:?}", cannot_prove);
self.constraints.extend(constraints);
self.obligations.extend(goals.into_iter().map(Obligation::Prove));
self.ambiguous = self.ambiguous || ambiguous;
Ok(UnifyOutcome { ambiguous })
self.cannot_prove = self.cannot_prove || cannot_prove;
Ok(())
}

/// Create obligations for the given goal in the given environment. This may
Expand Down Expand Up @@ -223,10 +221,11 @@ impl<'s> Fulfill<'s> {
}

// Negate the result
if let Ok(solution) = self.solver.solve_closed_goal(canonicalized.quantified.value) {
if let Ok(solution) = self.solver.solve_closed_goal(canonicalized.quantified.value) {
match solution {
Solution::Unique(_) => Err("refutation failed")?,
Solution::Ambig(_) => Ok(NegativeSolution::Ambiguous),
Solution::CannotProve => Ok(NegativeSolution::CannotProve),
}
} else {
Ok(NegativeSolution::Refuted)
Expand Down Expand Up @@ -301,7 +300,7 @@ impl<'s> Fulfill<'s> {
// directly.
assert!(obligations.is_empty());
while let Some(obligation) = self.obligations.pop() {
let ambiguous = match obligation {
let (ambiguous, cannot_prove) = match obligation {
Obligation::Prove(ref wc) => {
let PositiveSolution { free_vars, solution } = self.prove(wc)?;

Expand All @@ -312,24 +311,30 @@ impl<'s> Fulfill<'s> {
}
}

solution.is_ambig()
(solution.is_ambig(), solution.cannot_be_proven())
}
Obligation::Refute(ref goal) => {
self.refute(goal)? == NegativeSolution::Ambiguous
let answer = self.refute(goal)?;
(answer == NegativeSolution::Ambiguous, answer == NegativeSolution::CannotProve)
}
};

if ambiguous {
debug!("ambiguous result: {:?}", obligation);
obligations.push(obligation);
}

// If one of the obligations cannot be proven then the whole goal
// cannot be proven either, unless another obligation leads to an error
// in which case the function will bail out normally.
self.cannot_prove = self.cannot_prove || cannot_prove;
}

self.obligations.extend(obligations.drain(..));
debug!("end of round, {} obligations left", self.obligations.len());
}

// At the end of this process, `self.to_prove` should have
// At the end of this process, `self.obligations` should have
// all of the ambiguous obligations, and `obligations` should
// be empty.
assert!(obligations.is_empty());
Expand All @@ -346,7 +351,12 @@ impl<'s> Fulfill<'s> {
/// the outcome of type inference by updating the replacements it provides.
pub fn solve(mut self, subst: Substitution) -> Result<Solution> {
let outcome = self.fulfill()?;
if outcome.is_complete() && !self.ambiguous {

if self.cannot_prove {
Copy link
Contributor

@nikomatsakis nikomatsakis Jun 13, 2017 •
edited
Loading

Choose a reason for hiding this comment

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

Instead of having a cannot_prove field, can we use a local variable in fulfill() and extend the Outcome enum? In that case, I think we would replace these two ifs with something like:

match outcome {
    Outcome::CannotProve => return Ok(Solution::CannotProve),
    Outcome::Complete => {
        // No obligations remain, so we have definitively solved our goals,
        ...
        return ...; // as before
    }
    Outcome::Incomplete => { /* fallthrough to figure out some good suggestions */ }
}

Copy link
Contributor

Choose a reason for hiding this comment

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

Ah, I see that in this case unify would have to return Outcome (or UnifyOutcome). This way is ok too. It feels a bit less direct to me somehow, but maybe some comments would suffice to clear it up.

Copy link
Member Author

Choose a reason for hiding this comment

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

Yes and moreover unify is called outside of Fulfill (see previous comment) so unify would still have to change an internal state somehow, so I thought that a flag was lighter.

return Ok(Solution::CannotProve);
}

if outcome.is_complete() {
// No obligations remain, so we have definitively solved our goals,
// and the current inference state is the unique way to solve them.

Expand Down
18 changes: 9 additions & 9 deletions src/solve/infer/unify.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ struct Unifier<'t> {
snapshot: InferenceSnapshot,
goals: Vec<InEnvironment<LeafGoal>>,
constraints: Vec<InEnvironment<Constraint>>,
ambiguous: bool,
cannot_prove: bool,
}

#[derive(Debug)]
Expand All @@ -46,7 +46,7 @@ pub struct UnificationResult {
/// neither confirm nor deny their equality, since we interpret the
/// unification request as talking about *all possible
/// substitutions*. Instead, we return an ambiguous result.
pub ambiguous: bool,
pub cannot_prove: bool,
}

impl<'t> Unifier<'t> {
Expand All @@ -58,7 +58,7 @@ impl<'t> Unifier<'t> {
snapshot: snapshot,
goals: vec![],
constraints: vec![],
ambiguous: false,
cannot_prove: false,
}
}

Expand All @@ -67,7 +67,7 @@ impl<'t> Unifier<'t> {
Ok(UnificationResult {
goals: self.goals,
constraints: self.constraints,
ambiguous: self.ambiguous,
cannot_prove: self.cannot_prove,
})
}

Expand Down Expand Up @@ -118,13 +118,13 @@ impl<'t> Unifier<'t> {
if apply1.name.is_for_all() || apply2.name.is_for_all() {
// we're being asked to prove something like `!0 = !1`
// or `!0 = i32`. We interpret this as being asked
// whether that holds *for all subtitutions*. Thus, the
// answer is always *maybe* (ambiguous). That means we get:
// whether that holds *for all subtitutions*. Thus, we
// cannot prove the goal. That means we get:
//
// forall<T, U> { T = U } // Ambig
// forall<T, U> { not { T = U } } // Ambig
// forall<T, U> { T = U } // CannotProve
// forall<T, U> { not { T = U } } // CannotProve

self.ambiguous = true;
self.cannot_prove = true;
return Ok(())
} else {
bail!("cannot equate `{:?}` and `{:?}`", apply1.name, apply2.name);
Expand Down
34 changes: 21 additions & 13 deletions src/solve/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,11 +16,16 @@ pub enum Solution {
/// which must also hold for the goal to be valid.
Unique(Canonical<ConstrainedSubst>),

/// The goal may or may not hold, but regardless we may have some guidance
/// The goal may be provable in multiple ways, but regardless we may have some guidance
/// for type inference. In this case, we don't return any lifetime
/// constraints, since we have not "committed" to any particular solution
/// yet.
Ambig(Guidance),

/// There is no instantiation of the existentials for which we could prove this goal
/// to be true. Nonetheless, the goal may yet be true for some instantiations of the
/// universals. In other words, this goal is neither true nor false.
CannotProve,
}

#[derive(Clone, Debug, PartialEq, Eq)]
Expand Down Expand Up @@ -66,8 +71,8 @@ impl Solution {
use self::Guidance::*;

if self == other { return self }
if self.is_empty_unique() { return self }
if other.is_empty_unique() { return other }
if other.cannot_be_proven() { return self }
if self.cannot_be_proven() { return other }

// Otherwise, always downgrade to Ambig:

Expand All @@ -93,8 +98,8 @@ impl Solution {
use self::Guidance::*;

if self == other { return self }
if self.is_empty_unique() { return self }
if other.is_empty_unique() { return other }
if other.cannot_be_proven() { return self }
if self.cannot_be_proven() { return other }

// Otherwise, always downgrade to Ambig:

Expand All @@ -113,6 +118,9 @@ impl Solution {
use self::Guidance::*;

if self == other { return self }
if other.cannot_be_proven() { return self }
if self.cannot_be_proven() { return other }

if let Solution::Ambig(guidance) = self {
match guidance {
Definite(subst) | Suggested(subst) => Solution::Ambig(Suggested(subst)),
Expand All @@ -132,7 +140,8 @@ impl Solution {
binders: constrained.binders,
})
}
Solution::Ambig(guidance) => guidance
Solution::Ambig(guidance) => guidance,
Solution::CannotProve => Guidance::Unknown,
}
}

Expand All @@ -148,7 +157,7 @@ impl Solution {
};
Some(Canonical { value, binders: canonical.binders.clone() })
}
Solution::Ambig(_) => None,
Solution::Ambig(_) | Solution::CannotProve => None,
}
}

Expand All @@ -169,13 +178,9 @@ impl Solution {
}
}

/// We use emptiness, rather than triviality, to deduce that alternative
/// solutions **cannot meaningfully differ**
pub fn is_empty_unique(&self) -> bool {
pub fn cannot_be_proven(&self) -> bool {
match *self {
Solution::Unique(ref subst) => {
subst.binders.is_empty() && subst.value.subst.is_empty()
}
Solution::CannotProve => true,
_ => false,
}
}
Expand All @@ -198,6 +203,9 @@ impl fmt::Display for Solution {
Solution::Ambig(Guidance::Unknown) => {
write!(f, "Ambiguous; no inference guidance")
}
Solution::CannotProve => {
write!(f, "CannotProve")
}
}
}
}
Expand Down
51 changes: 7 additions & 44 deletions src/solve/solver.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -115,21 +115,21 @@ impl Solver {
.environment
.elaborated_clauses(&self.program)
.map(DomainGoal::into_program_clause);
let env_solution = self.solve_from_clauses(&binders, &value, env_clauses, true);
let env_solution = self.solve_from_clauses(&binders, &value, env_clauses);

let prog_clauses: Vec<_> = self.program.program_clauses.iter()
.cloned()
.filter(|clause| !clause.fallback_clause)
.collect();
let prog_solution = self.solve_from_clauses(&binders, &value, prog_clauses, false);
let prog_solution = self.solve_from_clauses(&binders, &value, prog_clauses);

// These fallback clauses are used when we're sure we'll never
// reach Unique via another route
let fallback: Vec<_> = self.program.program_clauses.iter()
.cloned()
.filter(|clause| clause.fallback_clause)
.collect();
let fallback_solution = self.solve_from_clauses(&binders, &value, fallback, false);
let fallback_solution = self.solve_from_clauses(&binders, &value, fallback);

// Now that we have all the outcomes, we attempt to combine
// them. Here, we apply a heuristic (also found in rustc): if we
Expand Down Expand Up @@ -172,8 +172,7 @@ impl Solver {
&mut self,
binders: &[ParameterKind<UniverseIndex>],
goal: &InEnvironment<DomainGoal>,
clauses: C,
from_env: bool,
clauses: C
) -> Result<Solution>
where
C: IntoIterator<Item = ProgramClause>,
Expand All @@ -182,7 +181,7 @@ impl Solver {
for ProgramClause { implication, .. } in clauses {
debug_heading!("clause={:?}", implication);

let res = self.solve_via_implication(binders, goal.clone(), implication, from_env);
let res = self.solve_via_implication(binders, goal.clone(), implication);
if let Ok(solution) = res {
debug!("ok: solution={:?}", solution);
cur_solution = Some(
Expand All @@ -203,8 +202,7 @@ impl Solver {
&mut self,
binders: &[ParameterKind<UniverseIndex>],
goal: InEnvironment<DomainGoal>,
clause: Binders<ProgramClauseImplication>,
from_env: bool,
clause: Binders<ProgramClauseImplication>
) -> Result<Solution> {
let mut fulfill = Fulfill::new(self);
let subst = Substitution::from_binders(&binders);
Expand All @@ -213,42 +211,7 @@ impl Solver {
let ProgramClauseImplication { consequence, conditions} =
fulfill.instantiate_in(goal.environment.universe, clause.binders, &clause.value);

// first, see if the implication's conclusion might solve our goal
if fulfill.unify(&goal.environment, &goal.goal, &consequence)?.ambiguous && from_env {
// here, using this environmental assumption would require unifying a skolemized
// variable, which can only appear in an *environment*, never the
// program. We view the program as providing a "closed world" of
// possible types and impls, and thus we can safely abandon this
// route of proving our goal.
//
// You can see this at work in the following example, where the
// assumption in the `if` is ignored since it cannot actually be applied.
//
// ```
// program {
// struct i32 { }
// struct u32 { }
//
// trait Foo<T> { }
//
// impl<T> Foo<i32> for T { }
// }
//
// goal {
// forall<T> {
// exists<U> {
// if (i32: Foo<T>) {
// T: Foo<U>
// }
// }
// }
// } yields {
// "Unique"
// }
// ```

Err("using the implication would require changing a forall variable")?;
}
fulfill.unify(&goal.environment, &goal.goal, &consequence)?;

// if so, toss in all of its premises
for condition in conditions {
Expand Down
Loading