From eb9df19cedf5df47ddbfc13a0c5e969270c9082c Mon Sep 17 00:00:00 2001 From: Wilco Kusee Date: Sun, 4 Oct 2020 20:50:22 +0200 Subject: [PATCH] Fix mdbook links after chalk-engine changes This broke a while back in https://github.com/rust-lang/chalk/pull/611, but only now broke the build because the hosted docs were updated. --- book/src/engine/logic.md | 8 ++--- book/src/engine/major_concepts.md | 52 ++++++------------------------- 2 files changed, 14 insertions(+), 46 deletions(-) diff --git a/book/src/engine/logic.md b/book/src/engine/logic.md index 7c025153b39..787f645b623 100644 --- a/book/src/engine/logic.md +++ b/book/src/engine/logic.md @@ -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. @@ -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` @@ -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 @@ -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 diff --git a/book/src/engine/major_concepts.md b/book/src/engine/major_concepts.md index 4a4ea0895cf..7f44fc80f70 100644 --- a/book/src/engine/major_concepts.md +++ b/book/src/engine/major_concepts.md @@ -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: @@ -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.) @@ -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 @@ -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 \ No newline at end of file