-
Notifications
You must be signed in to change notification settings - Fork 180
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.
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
Add CannotProve
solution
#45
Changes from 2 commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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 { | ||
|
@@ -53,6 +49,7 @@ struct PositiveSolution { | |
enum NegativeSolution { | ||
Refuted, | ||
Ambiguous, | ||
CannotProve, | ||
} | ||
|
||
/// A `Fulfill` is where we actually break down complex goals, instantiate | ||
|
@@ -75,10 +72,7 @@ pub struct Fulfill<'s> { | |
/// Lifetime constraints that must be fulfilled for a solution to be fully | ||
/// validated. | ||
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, | ||
cannot_prove: bool, | ||
} | ||
|
||
impl<'s> Fulfill<'s> { | ||
|
@@ -88,7 +82,7 @@ impl<'s> Fulfill<'s> { | |
infer: InferenceTable::new(), | ||
obligations: vec![], | ||
constraints: HashSet::new(), | ||
ambiguous: false, | ||
cannot_prove: false, | ||
} | ||
} | ||
|
||
|
@@ -119,19 +113,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 | ||
|
@@ -223,10 +217,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) | ||
|
@@ -301,7 +296,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)?; | ||
|
||
|
@@ -312,24 +307,29 @@ 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. | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. To make sure I understand: We don't stop immediately here because if we were to encounter a hard error somewhere else, that would "override" this cannot prove result, right? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Yeah exactly. I'm adding a bit of documentation here too. Notice that for the same reason, in the case where the unification set |
||
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()); | ||
|
@@ -346,7 +346,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 { | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Instead of having a 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 */ }
} There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Ah, I see that in this case There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Yes and moreover |
||
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. | ||
|
||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nit: comment would be good
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Right, I'm changing that.