Logic
Overview
chalk-engine
solves a Goal
using a hybrid search strategy with elements of depth- and breadth-first search. When asked to solve a
particular Goal
it hasn't seen before, it will first try to
generate a set of program clauses, that get turned into Strand
s, that could
solve that goal. Otherwise, if asked to solve a Goal
it has seen before, it
will select the existing table.
Once a table is selected, it will pick a Strand
and a subgoal of that
Strand
, try to solve that Goal
, repeating the process.
When an Answer
is found for a Goal
, it is merged into the parent Strand
,
or returned if it was the root Goal
. It will then go on to pick the next
subgoal of the Strand
and continue on.
If at any point the solving stops being "successful" (i.e. we definitely found
something to be unsolvable), the solving is restarted at the root Goal
.
The stack
In order to detect cycles (talked more about later), as well as keep track of
the selected Strand
for each table, chalk-engine
stores a Stack
on the
Forest
. Whenever a new goal is selected, a StackEntry
is pushed onto the
Stack
, as well as the "time" (which also gets incremented) that it was pushed.
This "time" can be compared later to check if all the Strands
of a Table
have been checked in a single solve.
As either Answer
s are found for the selected Table
, entries on the stack are
pop
ed. If something is found to be unsolvable, the complete stack is unwound.
Table creation
As mentioned before, whenever a new Goal
is encountered, a new Table
is
created to store current and future answers. First, the Goal
is converted into
an GoalData
. If it can be simplified, then a Strand
with one or more
subgoals will be generated and can be followed as above. Otherwise, if it is a
DomainGoal
(see above), then
program_clauses_for_goal
is called and each clause is converted into a Strand
and can be followed.
root_answer
and ensure_root_answer
The root_answer
function is the entry point to solve a Goal
. Up until now,
the idea of Answer
versus CompleteAnswer
have been ignored. However, in
reality Answer
s to Goal
s may actually have delayed subgoals (see ExClause
and Coinduction and refinement strands), whereas CompleteAnswer
s may not.
root_answer
essentially just wraps ensure_root_answer
and converts the
Goal
's Answer
to a CompleteAnswer
.
The ensure_root_answer
function contains the core skeleton of the logic around
Strand
and subgoal selection. The majority of the logic, however, is split out
into separate functions that branch out from ensure_root_answer
.
Subgoal selection
Once a given Strand
for a table has been selected, a subgoal has to be
selected. If there are no subgoals left, then there is nothing to do. Otherwise,
if there are subgoals left, then a subgoal will attempt to be selected (from
next_subgoal_index
).
If the table for that subgoal had previously floundered (see next section), then
we mark that subgoal as floundered and try the next subgoal. If all subgoals are
marked as floundered, then this entire Strand
is marked as floundered. If a
subgoal is successfully selected, there is nothing left to do.
Floundering
There a couple cases where we "give up" - here called floundering - on trying to
solve a goal. The most easy to understand case is if the types for a Goal
or
Answer
are too large. (Side note, we could actually handle this - by
generalizing - but turns out to be quite buggy and probably unnecessary).
Another case where we flounder is if we try to solve a Goal
where we try to
enumerate non-enumerable types (like auto traits). In general, floundering
just means that we can't know any more answers about a Goal
, for some
reason. However, if there are other Strands
that don't flounder, there may
still be other Answer
s available.
Answers
After an answer has been found for a subgoal, it must be applied to the parent
Strand
. Specifically, it must be able to unify with any existing Answers
. If
the Answer
s are incompatible, the Strand
is dropped since it can't lead
anywhere.
Cycles
If while pursuing a Goal
, the engine encounters the same Table
twice, then a
cycle has occurred. If the cycle is not coinductive (see next), then there is
nothing that can be gained from taking this route. We mark how far up the stack
is in the cycle, and try the next Strand
. If all Strand
s for a table
encounter a cycle, then we know that the current selected Goal
has no more
answers.
Coinduction and refinement strands
Coinduction basically means that two statements can rely on each other being true, unless either is proven false.
For example with the following program:
#[coinductive]
trait C1<T> { }
forall<A, B> { A: C1<B> if B: C1<A> }
Then the goal exists<T, U> { T: C1<U> }
holds for all T
and U
. If the C1
trait was not coinductive, this would be a simple cycle.
To implement coinduction in the engine, delayed subgoals were introduced.
Essentially, if a cycle is found, and the Goal
is coinductive, then this is
"delayed" until the stack unwinds back to the top Goal
and all other
non-coinductive cycles have been proven. Then, Goal
has been proven itself. In
some cases, it is the root Goal
that has delayed coinductive subgoals (see
above example). In this case, we create another "Refinement Strand" where the
only subgoals are the delayed coinductive subgoals. If this new Strand
can be
proven, then any Answer
s from that are valid answers for the root Goal
.
However, since there are currently delayed coinductive subgoals, there are no
answers available yet.
For much more in-depth