From f5cb41ca90f77d25b1e9bc145d43805e16a6d513 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Mon, 19 Nov 2018 18:28:10 -0600 Subject: [PATCH] SLG: Add links and mark-i-m's suggestions --- src/traits/slg.md | 111 +++++++++++++++++++++++++++------------------- 1 file changed, 65 insertions(+), 46 deletions(-) diff --git a/src/traits/slg.md b/src/traits/slg.md index 812afd1e..dcddd01f 100644 --- a/src/traits/slg.md +++ b/src/traits/slg.md @@ -16,10 +16,10 @@ a set of region constraints, which we'll ignore in this introduction. There are often many, or even infinitely many, solutions to a query. For example, say we want to prove that `exists { Vec: Debug }` for _some_ -type `?T`. Our solver should be capable of iterating over each answer one at -a time, say `?T = u32`, then `?T = i32`, and so on, rather than iterating -over every type in the type system. If we need more answers, we can request -more until we are done. This is similar to how Prolog works. +type `?T`. Our solver should be capable of yielding one answer at a time, say +`?T = u32`, then `?T = i32`, and so on, rather than iterating over every type +in the type system. If we need more answers, we can request more until we are +done. This is similar to how Prolog works. *See also: [The traditional, interactive Prolog query][pq]* @@ -27,32 +27,34 @@ more until we are done. This is similar to how Prolog works. ### Breadth-first -`Vec: Debug` is true if `?T: Debug`. This leads to a cycle: `[Vec , +`Vec: Debug` is true if `?T: Debug`. This leads to a cycle: `[Vec, Vec>, Vec>>]`, and so on all implement `Debug`. Our solver ought to be breadth first and consider answers like `[Vec: Debug, Vec: Debug, ...]` before it recurses, or we may never find the answer we're looking for. -### Cache friendly +### Cachable To speed up compilation, we need to cache results, including partial results left over from past solver queries. ## Description of how it works -The basis of the solver is the `Forest` type. A *forest* stores a +The basis of the solver is the [`Forest`] type. A *forest* stores a collection of *tables* as well as a *stack*. Each *table* represents the stored results of a particular query that is being performed, as well as the various *strands*, which are basically suspended computations that may be used to find more answers. Tables are interdependent: solving one query may require solving others. +[`Forest`]: https://rust-lang-nursery.github.io/chalk/doc/chalk_engine/forest/struct.Forest.html + ### Walkthrough Perhaps the easiest way to explain how the solver works is to walk through an example. Let's imagine that we have the following program: -```rust +```rust,ignore trait Debug { } struct u32 { } @@ -65,19 +67,22 @@ struct Vec { } impl Debug for Vec { } ``` -Now imagine that we want to find answers for the query `exists { -Rc: Debug }`. The first step would be to u-canonicalize this query; this -is the act of giving canonical names to all the unbound inference variables based on the -order of their left-most appearance, as well as canonicalizing the universes of any -universally bound names (e.g., the `T` in `forall { ... }`). In this case, there are no -universally bound names, but the canonical form Q of the query might look something like: +Now imagine that we want to find answers for the query `exists { Rc: +Debug }`. The first step would be to u-canonicalize this query; this is the +act of giving canonical names to all the unbound inference variables based on +the order of their left-most appearance, as well as canonicalizing the +universes of any universally bound names (e.g., the `T` in `forall { ... +}`). In this case, there are no universally bound names, but the canonical +form Q of the query might look something like: + +```text +Rc: Debug +``` - Rc: Debug - where `?0` is a variable in the root universe U0. We would then go and -look for a table with this as the key: since the forest is empty, this -lookup will fail, and we will create a new table T0, corresponding to -the u-canonical goal Q. +look for a table with this canonical query as the key: since the forest is +empty, this lookup will fail, and we will create a new table T0, +corresponding to the u-canonical goal Q. **Ignoring negative reasoning and regions.** To start, we'll ignore the possibility of negative goals like `not { Foo }`. We'll phase them @@ -93,7 +98,7 @@ where-clauses that are in scope. In the case of our example, there would be three clauses, each coming from the program. Using a Prolog-like notation, these look like: -``` +```text (u32: Debug). (Rc: Debug) :- (T: Debug). (Vec: Debug) :- (T: Debug). @@ -105,9 +110,9 @@ clauses are inapplicable because `u32` and `Vec` cannot be unified with `Rc`. The second clause, however, will work. **What is a strand?** Let's talk a bit more about what a strand *is*. In the code, a strand -is the combination of an inference table, an X-clause, and (possibly) +is the combination of an inference table, an _X-clause_, and (possibly) a selected subgoal from that X-clause. But what is an X-clause -(`ExClause`, in the code)? An X-clause pulls together a few things: +([`ExClause`], in the code)? An X-clause pulls together a few things: - The current state of the goal we are trying to prove; - A set of subgoals that have yet to be proven; @@ -118,7 +123,9 @@ The general form of an X-clause is written much like a Prolog clause, but with somewhat different semantics. Since we're ignoring delayed literals and region constraints, an X-clause just looks like this: - G :- L +```text +G :- L +``` where G is a goal and L is a set of subgoals that must be proven. (The L stands for *literal* -- when we address negative reasoning, a @@ -128,7 +135,9 @@ that if we are able to prove L then the goal G can be considered true. In the case of our example, we would wind up creating one strand, with an X-clause like so: - (Rc: Debug) :- (?T: Debug) +```text +(Rc: Debug) :- (?T: Debug) +``` Here, the `?T` refers to one of the inference variables created in the inference table that accompanies the strand. (I'll use named variables @@ -141,37 +150,45 @@ is the subgoal after the turnstile (`:-`) that we are currently trying to prove in this strand. Initally, when a strand is first created, there is no selected subgoal. +[`ExClause`]: https://rust-lang-nursery.github.io/chalk/doc/chalk_engine/struct.ExClause.html + **Activating a strand.** Now that we have created the table T0 and -initialized it with strands, we have to actually try and produce an -answer. We do this by invoking the `ensure_answer` operation on the -table: specifically, we say `ensure_answer(T0, A0)`, meaning "ensure -that there is a 0th answer". +initialized it with strands, we have to actually try and produce an answer. +We do this by invoking the [`ensure_root_answer`] operation on the table: +specifically, we say `ensure_root_answer(T0, A0)`, meaning "ensure that there +is a 0th answer A0 to query T0". -Remember that tables store not only strands, but also a vector of -cached answers. The first thing that `ensure_answer` does is to check -whether answer 0 is in this vector. If so, we can just return -immediately. In this case, the vector will be empty, and hence that -does not apply (this becomes important for cyclic checks later on). +Remember that tables store not only strands, but also a vector of cached +answers. The first thing that [`ensure_root_answer`] does is to check whether +answer A0 is in this vector. If so, we can just return immediately. In this +case, the vector will be empty, and hence that does not apply (this becomes +important for cyclic checks later on). -When there is no cached answer, `ensure_answer` will try to produce -one. It does this by selecting a strand from the set of active -strands -- the strands are stored in a `VecDeque` and hence processed -in a round-robin fashion. Right now, we have only one strand, storing -the following X-clause with no selected subgoal: +When there is no cached answer, [`ensure_root_answer`] will try to produce one. +It does this by selecting a strand from the set of active strands -- the +strands are stored in a `VecDeque` and hence processed in a round-robin +fashion. Right now, we have only one strand, storing the following X-clause +with no selected subgoal: - (Rc: Debug) :- (?T: Debug) +```text +(Rc: Debug) :- (?T: Debug) +``` When we activate the strand, we see that we have no selected subgoal, and so we first pick one of the subgoals to process. Here, there is only one (`?T: Debug`), so that becomes the selected subgoal, changing the state of the strand to: - (Rc: Debug) :- selected(?T: Debug, A0) +```text +(Rc: Debug) :- selected(?T: Debug, A0) +``` Here, we write `selected(L, An)` to indicate that (a) the literal `L` is the selected subgoal and (b) which answer `An` we are looking for. We start out looking for `A0`. +[`ensure_root_answer`]: https://rust-lang-nursery.github.io/chalk/doc/chalk_engine/forest/struct.Forest.html#method.ensure_root_answer + **Processing the selected subgoal.** Next, we have to try and find an answer to this selected goal. To do that, we will u-canonicalize it and try to find an associated table. In this case, the u-canonical @@ -189,7 +206,7 @@ will be: We can thus summarize the state of the whole forest at this point as follows: -``` +```text Table T0 [Rc: Debug] Strands: (Rc: Debug) :- selected(?T: Debug, A0) @@ -215,7 +232,7 @@ answer). The strand is then removed from the list of strands. The state of table T1 is therefore: -``` +```text Table T1 [?0: Debug] Answers: A0 = [?0 = u32] @@ -227,8 +244,10 @@ Table T1 [?0: Debug] Note that I am writing out the answer A0 as a substitution that can be applied to the table goal; actually, in the code, the goals for each X-clause are also represented as substitutions, but in this exposition -I've chosen to write them as full goals, following NFTD. - +I've chosen to write them as full goals, following [NFTD]. + +[NFTD]: ./bibliography.html#slg + Since we now have an answer, `ensure_answer(T1, A0)` will return `Ok` to the table T0, indicating that answer A0 is available. T0 now has the job of incorporating that result into its active strand. It does @@ -236,7 +255,7 @@ this in two ways. First, it creates a new strand that is looking for the next possible answer of T1. Next, it incorpoates the answer from A0 and removes the subgoal. The resulting state of table T0 is: -``` +```text Table T0 [Rc: Debug] Strands: (Rc: Debug) :- selected(?T: Debug, A1) @@ -250,7 +269,7 @@ then be returned up to our caller, and the whole forest goes quiescent at this point (remember, we only do enough work to generate *one* answer). The ending state of the forest at this point will be: -``` +```text Table T0 [Rc: Debug] Answer: A0 = [?0 = u32]