Skip to content
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

Improve coinduction handling in recursive solver #457

Closed
wants to merge 1 commit into from
Closed

Improve coinduction handling in recursive solver #457

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
144 changes: 117 additions & 27 deletions chalk-solve/src/recursive.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,10 +16,37 @@ use rustc_hash::FxHashMap;

type UCanonicalGoal<I> = UCanonical<InEnvironment<Goal<I>>>;

#[derive(Clone, Debug, PartialEq, Eq)]
Copy link
Contributor

Choose a reason for hiding this comment

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

We should add a comment to this struct clarifying its role

pub struct Answer<I: Interner> {
pub solution: Solution<I>,
pub delayed_goals: Vec<UCanonicalGoal<I>>,
Copy link
Contributor

Choose a reason for hiding this comment

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

...and we should comment this field especially

}

impl<I: Interner> Answer<I> {
pub fn new(solution: Solution<I>, delayed_goals: Vec<UCanonicalGoal<I>>) -> Self {
Self {
solution,
delayed_goals,
}
}

pub fn needs_refinement(&self) -> bool {
Copy link
Contributor

Choose a reason for hiding this comment

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

We should comment this =)

!self.delayed_goals.is_empty()
}

pub fn combine(self, other: Answer<I>, interner: &I) -> Self {
Copy link
Contributor

Choose a reason for hiding this comment

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

Similarly an example would be great here

let mut goals = vec![];
let combined_solution = self.solution.combine(other.solution, interner);
goals.extend(self.delayed_goals);
goals.extend(other.delayed_goals);
Answer::new(combined_solution, goals)
}
}

pub(crate) struct RecursiveContext<I: Interner> {
stack: Stack,
search_graph: SearchGraph<I>,
cache: FxHashMap<UCanonicalGoal<I>, Fallible<Solution<I>>>,
cache: FxHashMap<UCanonicalGoal<I>, Fallible<Answer<I>>>,

caching_enabled: bool,
}
Expand Down Expand Up @@ -105,7 +132,35 @@ impl<'me, I: Interner> Solver<'me, I> {
debug!("solve_root_goal(canonical_goal={:?})", canonical_goal);
assert!(self.context.stack.is_empty());
let minimums = &mut Minimums::new();
self.solve_goal(canonical_goal.clone(), minimums)
self.solve_goal(canonical_goal.clone(), minimums).map(|a| {
assert!(a.delayed_goals.is_empty()); // at this point there should be no delayed goals
Copy link
Contributor

Choose a reason for hiding this comment

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

Is this true? In some of the more extreme examples I found that you had to have delayed goals that required iteration even at the root level I think, but maybe that is hapenning in the solve_goal routine...

a.solution
})
}

fn refine_answer(
Copy link
Contributor

Choose a reason for hiding this comment

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

Comment: when is this invoked in the process of solving, and what is an example input/output?

Copy link
Contributor

Choose a reason for hiding this comment

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

What is goal and what is answer?

&mut self,
goal: UCanonicalGoal<I>,
answer: Answer<I>,
minimums: &mut Minimums,
) -> Fallible<Answer<I>> {
debug_heading!("refine_answer(goal = {:?}, answer = {:?})", goal, answer);
let mut cur_solution = answer.solution.clone();
let mut delayed_goals = vec![];

for subgoal in answer.delayed_goals {
if goal == subgoal {
debug!("encountered trivial cycle");
} else {
debug!("solving delayed goal(subgoal={:?})", subgoal);
let answer = self.solve_goal(subgoal, minimums)?;
cur_solution = cur_solution.combine(answer.solution, self.program.interner());
delayed_goals.extend(answer.delayed_goals);
}
}
let refined_answer = Answer::new(cur_solution, delayed_goals);
debug!("refined_answer={:?}", refined_answer);
Ok(refined_answer)
}

/// Attempt to solve a goal that has been fully broken down into leaf form
Expand All @@ -115,13 +170,19 @@ impl<'me, I: Interner> Solver<'me, I> {
&mut self,
goal: UCanonicalGoal<I>,
minimums: &mut Minimums,
) -> Fallible<Solution<I>> {
) -> Fallible<Answer<I>> {
info_heading!("solve_goal({:?})", goal);

// First check the cache.
if let Some(value) = self.context.cache.get(&goal) {
debug!("solve_reduced_goal: cache hit, value={:?}", value);
return value.clone();
return value.clone().and_then(|a| {
if a.needs_refinement() {
self.refine_answer(goal.clone(), a, minimums)
Copy link
Contributor

Choose a reason for hiding this comment

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

It seems like the main role of this routine is to remove "trivial" self-cycles, right? How can those come about here -- i.e., if we are retrieving a value from the cache, would it ever have trivial self-cycles?

} else {
Ok(a)
}
});
}

// Next, check if the goal is in the search tree already.
Expand All @@ -138,11 +199,15 @@ impl<'me, I: Interner> Solver<'me, I> {
subst: goal.trivial_substitution(self.program.interner()),
constraints: vec![],
};

debug!("applying coinductive semantics");
return Ok(Solution::Unique(Canonical {
value,
binders: goal.canonical.binders,
}));
return Ok(Answer::new(
Solution::Unique(Canonical {
value,
binders: goal.clone().canonical.binders,
}),
vec![goal],
));
Copy link
Contributor

Choose a reason for hiding this comment

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

So I was to think a bit about this -- in particular, I think the recursive solver can handle this case differently than the SLG solver. Unlike the SLG solver, it's ok for intermediate queries in the recursive solver to not get cached (and/or get cached at the end, along with everything else). I have to review how we handle caching and minimums, but I suspect that we want to work towards a setup where the cache itself never has delayed goals, they are always ephemeral things that exist on the stack during solving.

}

self.context.stack[depth].flag_cycle();
Expand All @@ -163,7 +228,7 @@ impl<'me, I: Interner> Solver<'me, I> {
// The initial result for this table is error.
let depth = self.context.stack.push(self.program, &goal);
let dfn = self.context.search_graph.insert(&goal, depth);
let subgoal_minimums = self.solve_new_subgoal(goal, depth, dfn);
let subgoal_minimums = self.solve_new_subgoal(goal.clone(), depth, dfn);
self.context.search_graph[dfn].links = subgoal_minimums;
self.context.search_graph[dfn].stack_depth = None;
self.context.stack.pop(depth);
Expand Down Expand Up @@ -191,7 +256,21 @@ impl<'me, I: Interner> Solver<'me, I> {
}
}

info!("solve_goal: solution = {:?} prio {:?}", result, priority);
info!(
"solve_goal: goal ={:?} solution_unrefined ={:?} prio ={:?}",
goal, result, priority
);
let result = result.and_then(|a| {
if a.needs_refinement() {
self.refine_answer(goal.clone(), a, minimums)
} else {
Ok(a)
}
});
info!(
"solve_goal: goal={:?} solution_refined={:?} prio={:?}",
goal, result, priority
);
result
}
}
Expand Down Expand Up @@ -258,9 +337,10 @@ impl<'me, I: Interner> Solver<'me, I> {
Ok(clauses) => {
self.solve_from_clauses(&canonical_goal, clauses, minimums)
}
Err(Floundered) => {
(Ok(Solution::Ambig(Guidance::Unknown)), ClausePriority::High)
}
Err(Floundered) => (
Ok(Answer::new(Solution::Ambig(Guidance::Unknown), vec![])),
ClausePriority::High,
),
}
};
debug!("prog_solution={:?}", prog_solution);
Expand Down Expand Up @@ -314,7 +394,7 @@ impl<'me, I: Interner> Solver<'me, I> {
}

let current_answer_is_ambig = match &current_answer {
Ok(s) => s.is_ambig(),
Ok(s) => s.solution.is_ambig(),
Err(_) => false,
};

Expand All @@ -337,7 +417,7 @@ impl<'me, I: Interner> Solver<'me, I> {
&mut self,
canonical_goal: &UCanonicalGoal<I>,
minimums: &mut Minimums,
) -> (Fallible<Solution<I>>, ClausePriority) {
) -> (Fallible<Answer<I>>, ClausePriority) {
debug_heading!("solve_via_simplification({:?})", canonical_goal);
let (mut fulfill, subst, goal) = Fulfill::new(self, canonical_goal);
if let Err(e) = fulfill.push_goal(&goal.environment, goal.goal) {
Expand All @@ -354,7 +434,7 @@ impl<'me, I: Interner> Solver<'me, I> {
canonical_goal: &UCanonical<InEnvironment<DomainGoal<I>>>,
clauses: C,
minimums: &mut Minimums,
) -> (Fallible<Solution<I>>, ClausePriority)
) -> (Fallible<Answer<I>>, ClausePriority)
where
C: IntoIterator<Item = ProgramClause<I>>,
{
Expand All @@ -363,8 +443,18 @@ impl<'me, I: Interner> Solver<'me, I> {
debug_heading!("clause={:?}", program_clause);

// If we have a completely ambiguous answer, it's not going to get better, so stop
if cur_solution == Some((Solution::Ambig(Guidance::Unknown), ClausePriority::High)) {
return (Ok(Solution::Ambig(Guidance::Unknown)), ClausePriority::High);
if let Some((
Answer {
solution: Solution::Ambig(Guidance::Unknown),
..
},
ClausePriority::High,
)) = cur_solution
{
return (
Ok(Answer::new(Solution::Ambig(Guidance::Unknown), vec![])),
ClausePriority::High,
);
}

match program_clause.data(self.program.interner()) {
Expand Down Expand Up @@ -424,7 +514,7 @@ impl<'me, I: Interner> Solver<'me, I> {
canonical_goal: &UCanonical<InEnvironment<DomainGoal<I>>>,
clause: &Binders<ProgramClauseImplication<I>>,
minimums: &mut Minimums,
) -> (Fallible<Solution<I>>, ClausePriority) {
) -> (Fallible<Answer<I>>, ClausePriority) {
info_heading!(
"solve_via_implication(\
\n canonical_goal={:?},\
Expand Down Expand Up @@ -485,11 +575,11 @@ fn calculate_inputs<I: Interner>(
fn combine_with_priorities_for_goal<I: Interner>(
interner: &I,
goal: &Goal<I>,
a: Fallible<Solution<I>>,
a: Fallible<Answer<I>>,
prio_a: ClausePriority,
b: Fallible<Solution<I>>,
b: Fallible<Answer<I>>,
prio_b: ClausePriority,
) -> (Fallible<Solution<I>>, ClausePriority) {
) -> (Fallible<Answer<I>>, ClausePriority) {
let domain_goal = match goal.data(interner) {
GoalData::DomainGoal(domain_goal) => domain_goal,
_ => {
Expand All @@ -512,11 +602,11 @@ fn combine_with_priorities_for_goal<I: Interner>(
fn combine_with_priorities<I: Interner>(
interner: &I,
domain_goal: &DomainGoal<I>,
a: Solution<I>,
a: Answer<I>,
prio_a: ClausePriority,
b: Solution<I>,
b: Answer<I>,
prio_b: ClausePriority,
) -> (Solution<I>, ClausePriority) {
) -> (Answer<I>, ClausePriority) {
match (prio_a, prio_b, a, b) {
(ClausePriority::High, ClausePriority::Low, higher, lower)
| (ClausePriority::Low, ClausePriority::High, lower, higher) => {
Expand All @@ -526,8 +616,8 @@ fn combine_with_priorities<I: Interner>(
// solution overriding a general low-priority one. Currently inputs
// only matter for projections; in a goal like `AliasEq(<?0 as
// Trait>::Type = ?1)`, ?0 is the input.
let inputs_higher = calculate_inputs(interner, domain_goal, &higher);
let inputs_lower = calculate_inputs(interner, domain_goal, &lower);
let inputs_higher = calculate_inputs(interner, domain_goal, &higher.solution);
let inputs_lower = calculate_inputs(interner, domain_goal, &lower.solution);
if inputs_higher == inputs_lower {
debug!(
"preferring solution: {:?} over {:?} because of higher prio",
Expand Down
Loading