Skip to content

Commit

Permalink
Fix mdbook links after chalk-engine changes
Browse files Browse the repository at this point in the history
This broke a while back in #611,
but only now broke the build because the hosted docs were updated.
  • Loading branch information
detrumi committed Oct 4, 2020
1 parent c472e47 commit eb9df19
Show file tree
Hide file tree
Showing 2 changed files with 14 additions and 46 deletions.
8 changes: 4 additions & 4 deletions book/src/engine/logic.md
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
## 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 ask the [`Context`] to
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.
Expand Down Expand Up @@ -37,7 +37,7 @@ created to store current and future answers. First, the [`Goal`] is converted in
an `HhGoal`. 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`](https://rust-lang.github.io/chalk/chalk_engine/context/trait.ContextOps.html#tymethod.program_clauses)
[`program_clauses_for_goal`](https://rust-lang.github.io/chalk/chalk_solve/clauses/fn.program_clauses_for_goal.html)
is called and each clause is converted into a `Strand` and can be followed.

## `root_answer` and `ensure_root_answer`
Expand All @@ -58,7 +58,7 @@ into separate functions that branch out from `ensure_root_answer`.
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`](https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html#tymethod.next_subgoal_index)).
[`next_subgoal_index`](https://rust-lang.github.io/chalk/chalk_engine/slg/struct.SlgContext.html#method.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
Expand Down Expand Up @@ -126,6 +126,6 @@ For much more in-depth
[`Stack`]: https://rust-lang.github.io/chalk/chalk_engine/stack/struct.Stack.html
[`StackEntry`]: https://rust-lang.github.io/chalk/chalk_engine/stack/struct.StackEntry.html
[`Table`]: https://rust-lang.github.io/chalk/chalk_engine/table/struct.Table.html
[`Goal`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html#associatedtype.Goal
[`Goal`]: https://rust-lang.github.io/chalk/chalk_ir/struct.Goal.html
[`Answer`]: https://rust-lang.github.io/chalk/chalk_engine/struct.Answer.html
[`CompleteAnswer`]: https://rust-lang.github.io/chalk/chalk_engine/struct.CompleteAnswer.html
52 changes: 10 additions & 42 deletions book/src/engine/major_concepts.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,45 +4,14 @@ This section goes over a few different concepts that are crucial to
understanding how `chalk-engine` works, without going over the exact solving
logic.

## `Context`, `ContextOps`, and `InferenceTable`

### `Context`

The [`Context`] trait is the primary bridge between Chalk internal logic and
external types. In addition actually *defining* the types (via associated
types), it also contains associated functions to convert or extract
information from those types. Overall, this allows the types to be basically
opaque to the engine internals. Functions in the trait are agnostic to specific
program or environment details, since they lack a `&self` argument.

To give an example, there is an associated [`Goal`] type. However, Chalk doesn't
know how to solve this. Instead, it has to be converted an `HhGoal` via the
`Context::into_hh_goal` function. This will be coverted more in the `Goals`
section.

### `ContextOps`

The [`ContextOps`] trait contains functions that may specifically require
information a specific program or environment. For example, the
`program_clauses` function gives potential ways to prove a `Goal`, but obviously
it requires knowing the program (for example, what types, traits, and impls
there are). Functions in this trait all take a `&self` argument.

### `InferenceTable`

The [`InferenceTable`] is a super trait to the [`UnificationOps`], [`TruncateOps`],
and [`ResolventOps`]. Each of these contains functions that track the state of
specific parts of the program. Importantly, these operations can dynamically
change the state of the logic itself.

## Goals

A "goal" in Chalk can be thought of as "something we want to prove". The engine
itself understands `HhGoal`s. `HHGoal`s consist of the most basic logic,
such as introducing Binders (`Forall` or `Exists`) or combining goals (`All`).
On the other hand, `Context::Goal` represents an opaque goal generated
On the other hand, `Goal` represents an opaque goal generated
externally. As such, it may contain any extra information or may be interned.
When solving a logic predicate, Chalk will lazily convert `Context::Goal`s
When solving a logic predicate, Chalk will lazily convert `Goal`s
into `HHGoal`s.

There are three types of completely opaque `HhGoal`s that Chalk can solve:
Expand Down Expand Up @@ -77,11 +46,10 @@ goals that depend on this goal.

However, oftentimes, this is not what external crates want when solving for a
goal. Instead, the may want a *unique* solution to this goal. Indeed, when we
solve for a given root [`Goal`], we return a since [`Solution`]. It is up to the
implementation of [`Context`] to decide how a `Solution` is made, given a possibly
infinite set of answers. One of example of this is the
solve for a given root [`Goal`], we return a single [`Solution`]. The
[`AntiUnifier`](https://rust-lang.github.io/chalk/chalk_engine/slg/aggregate/struct.AntiUnifier.html)
from `chalk-solve`, which finds a minimal generalization of answers which don't
struct from `chalk-solve` then finds that solution, by finding a minimal
generalization of answers which don't
unify. (For the example above, it would return only `Ambiguous`, since `A` and
`B` can't unify.)

Expand All @@ -91,7 +59,7 @@ An [`ExClause`] is described in literature as `A :- D | G` or
`A holds given that G holds with D delayed goals`. In `chalk-engine`, an
`ExClause` stores the current state of proving a goal, including existing
substitutions already found, subgoals yet to be proven, or delayed subgoals. A
[`Strand`] wraps both an [`ExClause`] and an [`InferenceTable`] together.
[`Strand`] wraps both an [`ExClause`] and an [`TruncatingInferenceTable`] together.

## Tables and Forests

Expand All @@ -110,15 +78,15 @@ stack).

[`Context`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html
[`ContextOps`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.ContextOps.html
[`InferenceTable`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.InferenceTable.html
[`Solution`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html#associatedtype.Solution
[`TruncatingInferenceTable`]: https://rust-lang.github.io/chalk/chalk_engine/slg/struct.TruncatingInferenceTable.html
[`Solution`]: https://rust-lang.github.io/chalk/chalk_solve/solve/enum.Solution.html
[`ExClause`]: https://rust-lang.github.io/chalk/chalk_engine/struct.ExClause.html
[`Strand`]: https://rust-lang.github.io/chalk/chalk_engine/strand/struct.Strand.html
[`Table`]: https://rust-lang.github.io/chalk/chalk_engine/table/struct.Table.html
[`Forest`]: https://rust-lang.github.io/chalk/chalk_engine/forest/struct.Forest.html
[`Goal`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html#associatedtype.Goal
[`Goal`]: https://rust-lang.github.io/chalk/chalk_ir/struct.Goal.html
[`UnificationOps`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.UnificationOps.html
[`TruncateOps`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.TruncateOps.html
[`ResolventOps`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.ResolventOps.html
[`ProgramClause`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html#associatedtype.ProgramClause
[`ProgramClause`]: https://rust-lang.github.io/chalk/chalk_ir/struct.ProgramClause.html
[`Answer`]: https://rust-lang.github.io/chalk/chalk_engine/struct.Answer.html

0 comments on commit eb9df19

Please sign in to comment.