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 Strands, 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 Answers are found for the selected Table, entries on the stack are poped. 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 Answers to Goals may actually have delayed subgoals (see ExClause and Coinduction and refinement strands), whereas CompleteAnswers 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 Answers 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 Answers 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 Strands 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 Answers 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