Skip to content

Commit

Permalink
Merge pull request #272 from jackh726/coinductive
Browse files Browse the repository at this point in the history 
Fix coinductive unsoundness
  • Loading branch information
@nikomatsakis
nikomatsakis committed Dec 23, 2019
2 parents ff65b5a + 6e68a41 commit 44106c0
Show file tree
Hide file tree
Showing 13 changed files with 631 additions and 195 deletions.
67 changes: 50 additions & 17 deletions chalk-engine/src/context.rs
View file
Expand Up @@ -7,7 +7,7 @@

use crate::fallible::Fallible;
use crate::hh::HhGoal;
use crate::{Answer, ExClause};
use crate::{CompleteAnswer, ExClause};
use std::fmt::Debug;
use std::hash::Hash;

Expand Down Expand Up @@ -61,12 +61,15 @@ pub trait Context: Clone + Debug {
/// `make_solution`.
type Solution;

/// Part of an answer: represents a canonicalized substitution,
/// combined with region constraints. See [the rustc-guide] for more information.
///
/// [the rustc-guide]: https://rust-lang.github.io/rustc-guide/traits/canonicalization.html#canonicalizing-the-query-result
/// Part of a complete answer: the canonical version of a
/// substitution and region constraints but without any delayed
/// literals.
type CanonicalConstrainedSubst: Clone + Debug + Eq + Hash;

/// Part of an answer: the canonical version of a substitution,
/// region constraints, and delayed literals.
type CanonicalAnswerSubst: Clone + Debug + Eq + Hash;

/// Represents a substitution from the "canonical variables" found
/// in a canonical goal to specific values.
type Substitution: Clone + Debug;
Expand Down Expand Up @@ -132,21 +135,27 @@ pub trait Context: Clone + Debug {

/// Extracts the inner normalized substitution from a canonical constraint subst.
fn inference_normalized_subst_from_subst(
canon_ex_clause: &Self::CanonicalConstrainedSubst,
canon_ex_clause: &Self::CanonicalAnswerSubst,
) -> &Self::InferenceNormalizedSubst;

/// True if this solution has no region constraints.
fn empty_constraints(ccs: &Self::CanonicalConstrainedSubst) -> bool;
fn empty_constraints(ccs: &Self::CanonicalAnswerSubst) -> bool;

fn canonical(u_canon: &Self::UCanonicalGoalInEnvironment) -> &Self::CanonicalGoalInEnvironment;

fn is_trivial_substitution(
u_canon: &Self::UCanonicalGoalInEnvironment,
canonical_subst: &Self::CanonicalConstrainedSubst,
canonical_subst: &Self::CanonicalAnswerSubst,
) -> bool;

fn has_delayed_subgoals(canonical_subst: &Self::CanonicalAnswerSubst) -> bool;

fn num_universes(_: &Self::UCanonicalGoalInEnvironment) -> usize;

fn canonical_constrained_subst_from_canonical_constrained_answer(
canonical_subst: &Self::CanonicalAnswerSubst,
) -> Self::CanonicalConstrainedSubst;

/// Convert a goal G *from* the canonical universes *into* our
/// local universes. This will yield a goal G' that is the same
/// but for the universes of universally quantified names.
Expand All @@ -161,8 +170,10 @@ pub trait Context: Clone + Debug {
/// names.
fn map_subst_from_canonical(
_: &Self::UniverseMap,
value: &Self::CanonicalConstrainedSubst,
) -> Self::CanonicalConstrainedSubst;
value: &Self::CanonicalAnswerSubst,
) -> Self::CanonicalAnswerSubst;

fn goal_from_goal_in_environment(goal: &Self::GoalInEnvironment) -> &Self::Goal;
}

pub trait ContextOps<C: Context>: Sized + Clone + Debug + AggregateOps<C> {
Expand Down Expand Up @@ -201,20 +212,34 @@ pub trait ContextOps<C: Context>: Sized + Clone + Debug + AggregateOps<C> {
/// - the table `T`
/// - the substitution `S`
/// - the environment and goal found by substitution `S` into `arg`
fn instantiate_ucanonical_goal<R>(
fn instantiate_ucanonical_goal(
&self,
arg: &C::UCanonicalGoalInEnvironment,
op: impl FnOnce(C::InferenceTable, C::Substitution, C::Environment, C::Goal) -> R,
) -> R;
) -> (C::InferenceTable, C::Substitution, C::Environment, C::Goal);

fn instantiate_ex_clause(
&self,
num_universes: usize,
canonical_ex_clause: &C::CanonicalExClause,
) -> (C::InferenceTable, ExClause<C>);

// Used by: logic
fn instantiate_answer_subst(
&self,
num_universes: usize,
answer: &C::CanonicalAnswerSubst,
) -> (
C::InferenceTable,
C::Substitution,
Vec<C::RegionConstraint>,
Vec<C::GoalInEnvironment>,
);

/// returns unique solution from answer
fn constrained_subst_from_answer(&self, answer: Answer<C>) -> C::CanonicalConstrainedSubst;
fn constrained_subst_from_answer(
&self,
answer: CompleteAnswer<C>,
) -> C::CanonicalConstrainedSubst;
}

/// Methods for combining solutions to yield an aggregate solution.
Expand Down Expand Up @@ -282,6 +307,14 @@ pub trait UnificationOps<C: Context> {
constraints: Vec<C::RegionConstraint>,
) -> C::CanonicalConstrainedSubst;

// Used by: logic
fn canonicalize_answer_subst(
&mut self,
subst: C::Substitution,
constraints: Vec<C::RegionConstraint>,
delayed_subgoals: Vec<C::GoalInEnvironment>,
) -> C::CanonicalAnswerSubst;

// Used by: logic
fn invert_goal(&mut self, value: &C::GoalInEnvironment) -> Option<C::GoalInEnvironment>;

Expand Down Expand Up @@ -343,13 +376,13 @@ pub trait ResolventOps<C: Context> {
ex_clause: &mut ExClause<C>,
selected_goal: &C::GoalInEnvironment,
answer_table_goal: &C::CanonicalGoalInEnvironment,
canonical_answer_subst: &C::CanonicalConstrainedSubst,
canonical_answer_subst: &C::CanonicalAnswerSubst,
) -> Fallible<()>;
}

pub trait AnswerStream<C: Context> {
fn peek_answer(&mut self) -> Option<Answer<C>>;
fn next_answer(&mut self) -> Option<Answer<C>>;
fn peek_answer(&mut self) -> Option<CompleteAnswer<C>>;
fn next_answer(&mut self) -> Option<CompleteAnswer<C>>;

/// Invokes `test` with each possible future answer, returning true immediately
/// if we find any answer for which `test` returns true.
Expand Down
23 changes: 15 additions & 8 deletions chalk-engine/src/forest.rs
View file
Expand Up @@ -4,7 +4,7 @@ use crate::logic::RootSearchFail;
use crate::stack::{Stack, StackIndex};
use crate::table::AnswerIndex;
use crate::tables::Tables;
use crate::{Answer, TableIndex};
use crate::{CompleteAnswer, TableIndex};

pub struct Forest<C: Context> {
context: C,
Expand Down Expand Up @@ -45,17 +45,20 @@ impl<C: Context> Forest<C> {
context: &impl ContextOps<C>,
goal: C::UCanonicalGoalInEnvironment,
num_answers: usize,
) -> Option<Vec<Answer<C>>> {
) -> Option<Vec<CompleteAnswer<C>>> {
let table = self.get_or_create_table_for_ucanonical_goal(context, goal);
let mut answers = Vec::with_capacity(num_answers);
for i in 0..num_answers {
let i = AnswerIndex::from(i);
let mut count = 0;
for _ in 0..num_answers {
loop {
match self.root_answer(context, table, i) {
match self.root_answer(context, table, AnswerIndex::from(count)) {
Ok(answer) => {
answers.push(answer.clone());
break;
}
Err(RootSearchFail::InvalidAnswer) => {
count += 1;
}
Err(RootSearchFail::Floundered) => return None,
Err(RootSearchFail::QuantumExceeded) => continue,
Err(RootSearchFail::NoMoreSolutions) => return Some(answers),
Expand All @@ -69,6 +72,7 @@ impl<C: Context> Forest<C> {
}
}
}
count += 1;
}

Some(answers)
Expand Down Expand Up @@ -181,7 +185,7 @@ impl<'me, C: Context, CO: ContextOps<C>> AnswerStream<C> for ForestSolver<'me, C
/// # Panics
///
/// Panics if a negative cycle was detected.
fn peek_answer(&mut self) -> Option<Answer<C>> {
fn peek_answer(&mut self) -> Option<CompleteAnswer<C>> {
loop {
match self
.forest
Expand All @@ -191,9 +195,12 @@ impl<'me, C: Context, CO: ContextOps<C>> AnswerStream<C> for ForestSolver<'me, C
return Some(answer.clone());
}

Err(RootSearchFail::InvalidAnswer) => {
self.answer.increment();
}
Err(RootSearchFail::Floundered) => {
let table_goal = &self.forest.tables[self.table].table_goal;
return Some(Answer {
return Some(CompleteAnswer {
subst: self.context.identity_constrained_subst(table_goal),
ambiguous: true,
});
Expand All @@ -217,7 +224,7 @@ impl<'me, C: Context, CO: ContextOps<C>> AnswerStream<C> for ForestSolver<'me, C
}
}

fn next_answer(&mut self) -> Option<Answer<C>> {
fn next_answer(&mut self) -> Option<CompleteAnswer<C>> {
self.peek_answer().map(|answer| {
self.answer.increment();
answer
Expand Down
29 changes: 21 additions & 8 deletions chalk-engine/src/lib.rs
View file
Expand Up @@ -112,6 +112,9 @@ pub struct ExClause<C: Context> {
/// Subgoals: literals that must be proven
pub subgoals: Vec<Literal<C>>,

/// We assume that negative literals cannot have coinductive cycles.
pub delayed_subgoals: Vec<C::GoalInEnvironment>,

/// Time stamp that is incremented each time we find an answer to
/// some subgoal. This is used to figure out whether any of the
/// floundered subgoals may no longer be floundered: we record the
Expand Down Expand Up @@ -185,18 +188,28 @@ pub struct FlounderedSubgoal<C: Context> {
pub floundered_time: TimeStamp,
}

#[derive(Clone, Debug, PartialEq, Eq, Hash)]
struct Answers<C: Context> {
answers: Vec<Answer<C>>,
}

/// An "answer" in the on-demand solver corresponds to a fully solved
/// goal for a particular table (modulo delayed literals). It contains
/// a substitution
#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
#[derive(Clone, Debug)]
pub struct Answer<C: Context> {
/// A fully instantiated version of the goal for which the query
/// is true (including region constraints).
/// Contains values for the unbound inference variables for which
/// the table is true, along with any delayed subgoals (Which must
/// still be proven) and region constrained (which must still be
/// proven, but not by chalk).
pub subst: C::CanonicalAnswerSubst,

/// If this flag is set, then the answer could be neither proven
/// nor disproven. This could be the size of the answer exceeded
/// `max_size` or because of a negative loop (e.g., `P :- not { P }`).
pub ambiguous: bool,
}

#[derive(Clone, Debug)]
pub struct CompleteAnswer<C: Context> {
/// Contains values for the unbound inference variables for which
/// the table is true, along with any region constrained (which must still be
/// proven, but not by chalk).
pub subst: C::CanonicalConstrainedSubst,

/// If this flag is set, then the answer could be neither proven
Expand Down

0 comments on commit 44106c0

Please sign in to comment.