parent
a3d20a768d
commit
470f24aae9
|
|
@ -205,8 +205,8 @@ TODO
|
||||||
TODO: maybe something about macros 2.0?
|
TODO: maybe something about macros 2.0?
|
||||||
|
|
||||||
|
|
||||||
[code_dir]: https://github.com/rust-lang/rust/tree/master/src/libsyntax/ext/tt
|
[code_dir]: https://github.com/rust-lang/rust/tree/master/src/libsyntax/ext/mbe
|
||||||
[code_mp]: https://doc.rust-lang.org/nightly/nightly-rustc/syntax/ext/tt/macro_parser/
|
[code_mp]: https://doc.rust-lang.org/nightly/nightly-rustc/syntax/ext/mbe/macro_parser
|
||||||
[code_mr]: https://doc.rust-lang.org/nightly/nightly-rustc/syntax/ext/tt/macro_rules/
|
[code_mr]: https://doc.rust-lang.org/nightly/nightly-rustc/syntax/ext/mbe/macro_rules
|
||||||
[code_parse_int]: https://doc.rust-lang.org/nightly/nightly-rustc/syntax/ext/tt/macro_parser/fn.parse.html
|
[code_parse_int]: https://doc.rust-lang.org/nightly/nightly-rustc/syntax/ext/mbe/macro_parser/fn.parse.html
|
||||||
[parsing]: ./the-parser.html
|
[parsing]: ./the-parser.html
|
||||||
|
|
|
||||||
|
|
@ -229,28 +229,28 @@ Likewise, lowering tests use the [`lowering_success!` and
|
||||||
[rustc-issues]: https://github.com/rust-lang/rustc-guide/issues
|
[rustc-issues]: https://github.com/rust-lang/rustc-guide/issues
|
||||||
[universal quantification]: https://en.wikipedia.org/wiki/Universal_quantification
|
[universal quantification]: https://en.wikipedia.org/wiki/Universal_quantification
|
||||||
|
|
||||||
[`ProgramClause`]: https://rust-lang.github.io/chalk/doc/chalk_ir/enum.ProgramClause.html
|
[`ProgramClause`]: https://rust-lang.github.io/chalk/chalk_ir/enum.ProgramClause.html
|
||||||
[`ProgramEnvironment`]: https://rust-lang.github.io/chalk/doc/chalk/program_environment/struct.ProgramEnvironment.html
|
[`ProgramEnvironment`]: https://rust-lang.github.io/chalk/chalk/program_environment/struct.ProgramEnvironment.html
|
||||||
[chalk_engine]: https://rust-lang.github.io/chalk/doc/chalk_engine/index.html
|
[chalk_engine]: https://rust-lang.github.io/chalk/chalk_engine
|
||||||
[chalk_ir]: https://rust-lang.github.io/chalk/doc/chalk_ir/index.html
|
[chalk_ir]: https://rust-lang.github.io/chalk/chalk_ir/index.html
|
||||||
[chalk_parse]: https://rust-lang.github.io/chalk/doc/chalk_parse/index.html
|
[chalk_parse]: https://rust-lang.github.io/chalk/chalk_parse/index.html
|
||||||
[chalk_solve]: https://rust-lang.github.io/chalk/doc/chalk_solve/index.html
|
[chalk_solve]: https://rust-lang.github.io/chalk/chalk_solve/index.html
|
||||||
[chalk_rust_ir]: https://rust-lang.github.io/chalk/doc/chalk_rust_ir/index.html
|
[chalk_rust_ir]: https://rust-lang.github.io/chalk/chalk_rust_ir/index.html
|
||||||
[doc-chalk]: https://rust-lang.github.io/chalk/doc/chalk/index.html
|
[doc-chalk]: https://rust-lang.github.io/chalk/chalk/index.html
|
||||||
[engine-context]: https://rust-lang.github.io/chalk/doc/chalk_engine/context/index.html
|
[engine-context]: https://rust-lang.github.io/chalk/chalk_engine/context/index.html
|
||||||
[chalk-program]: https://rust-lang.github.io/chalk/doc/chalk/program/struct.Program.html
|
[chalk-program]: https://rust-lang.github.io/chalk/chalk/program/struct.Program.html
|
||||||
|
|
||||||
[binders-struct]: https://rust-lang.github.io/chalk/doc/chalk_ir/struct.Binders.html
|
[binders-struct]: https://rust-lang.github.io/chalk/chalk_ir/struct.Binders.html
|
||||||
[chalk-ast]: https://rust-lang.github.io/chalk/doc/chalk_parse/ast/index.html
|
[chalk-ast]: https://rust-lang.github.io/chalk/chalk_parse/ast/index.html
|
||||||
[chalk-test-example]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L115
|
[chalk-test-example]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L115
|
||||||
[chalk-test-lowering-example]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rust_ir/lowering/test.rs#L8-L31
|
[chalk-test-lowering-example]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rust_ir/lowering/test.rs#L8-L31
|
||||||
[chalk-test-lowering]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rust_ir/lowering/test.rs
|
[chalk-test-lowering]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rust_ir/lowering/test.rs
|
||||||
[chalk-test-wf]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules/wf/test.rs#L1
|
[chalk-test-wf]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules/wf/test.rs#L1
|
||||||
[chalki]: https://rust-lang.github.io/chalk/doc/chalki/index.html
|
[chalki]: https://rust-lang.github.io/chalk/chalki/index.html
|
||||||
[clause]: https://github.com/rust-lang/chalk/blob/master/GLOSSARY.md#clause
|
[clause]: https://github.com/rust-lang/chalk/blob/master/GLOSSARY.md#clause
|
||||||
[coherence-src]: https://rust-lang.github.io/chalk/doc/chalk_solve/coherence/index.html
|
[coherence-src]: https://rust-lang.github.io/chalk/chalk_solve/coherence/index.html
|
||||||
[ir-code]: https://rust-lang.github.io/chalk/doc/chalk_rust_ir/
|
[ir-code]: https://rust-lang.github.io/chalk/chalk_rust_ir/
|
||||||
[solve-wf-src]: https://rust-lang.github.io/chalk/doc/chalk_solve/wf/index.html
|
[solve-wf-src]: https://rust-lang.github.io/chalk/chalk_solve/wf/index.html
|
||||||
[solve_goal]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L85
|
[solve_goal]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L85
|
||||||
[test-lowering-macros]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test_util.rs#L21-L54
|
[test-lowering-macros]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test_util.rs#L21-L54
|
||||||
[test-macro]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L33
|
[test-macro]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L33
|
||||||
|
|
|
||||||
|
|
@ -47,7 +47,7 @@ well as the various *strands*, which are basically suspended
|
||||||
computations that may be used to find more answers. Tables are
|
computations that may be used to find more answers. Tables are
|
||||||
interdependent: solving one query may require solving others.
|
interdependent: solving one query may require solving others.
|
||||||
|
|
||||||
[`Forest`]: https://rust-lang.github.io/chalk/doc/chalk_engine/forest/struct.Forest.html
|
[`Forest`]: https://rust-lang.github.io/chalk/chalk_engine/forest/struct.Forest.html
|
||||||
|
|
||||||
### Walkthrough
|
### Walkthrough
|
||||||
|
|
||||||
|
|
@ -126,7 +126,7 @@ literals and region constraints, an X-clause just looks like this:
|
||||||
```text
|
```text
|
||||||
G :- L
|
G :- L
|
||||||
```
|
```
|
||||||
|
|
||||||
where G is a goal and L is a set of subgoals that must be proven.
|
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
|
(The L stands for *literal* -- when we address negative reasoning, a
|
||||||
literal will be either a positive or negative subgoal.) The idea is
|
literal will be either a positive or negative subgoal.) The idea is
|
||||||
|
|
@ -150,7 +150,7 @@ is the subgoal after the turnstile (`:-`) that we are currently trying
|
||||||
to prove in this strand. Initially, when a strand is first created,
|
to prove in this strand. Initially, when a strand is first created,
|
||||||
there is no selected subgoal.
|
there is no selected subgoal.
|
||||||
|
|
||||||
[`ExClause`]: https://rust-lang.github.io/chalk/doc/chalk_engine/struct.ExClause.html
|
[`ExClause`]: https://rust-lang.github.io/chalk/chalk_engine/struct.ExClause.html
|
||||||
|
|
||||||
**Activating a strand.** Now that we have created the table T0 and
|
**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.
|
initialized it with strands, we have to actually try and produce an answer.
|
||||||
|
|
@ -182,12 +182,12 @@ the state of the strand to:
|
||||||
```text
|
```text
|
||||||
(Rc<?T>: Debug) :- selected(?T: Debug, A0)
|
(Rc<?T>: Debug) :- selected(?T: Debug, A0)
|
||||||
```
|
```
|
||||||
|
|
||||||
Here, we write `selected(L, An)` to indicate that (a) the literal `L`
|
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
|
is the selected subgoal and (b) which answer `An` we are looking for. We
|
||||||
start out looking for `A0`.
|
start out looking for `A0`.
|
||||||
|
|
||||||
[`ensure_root_answer`]: https://rust-lang.github.io/chalk/doc/chalk_engine/forest/struct.Forest.html#method.ensure_root_answer
|
[`ensure_root_answer`]: https://rust-lang.github.io/chalk/chalk_engine/forest/struct.Forest.html#method.ensure_root_answer
|
||||||
|
|
||||||
**Processing the selected subgoal.** Next, we have to try and find an
|
**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
|
answer to this selected goal. To do that, we will u-canonicalize it
|
||||||
|
|
@ -210,14 +210,14 @@ follows:
|
||||||
Table T0 [Rc<?0>: Debug]
|
Table T0 [Rc<?0>: Debug]
|
||||||
Strands:
|
Strands:
|
||||||
(Rc<?T>: Debug) :- selected(?T: Debug, A0)
|
(Rc<?T>: Debug) :- selected(?T: Debug, A0)
|
||||||
|
|
||||||
Table T1 [?0: Debug]
|
Table T1 [?0: Debug]
|
||||||
Strands:
|
Strands:
|
||||||
(u32: Debug) :-
|
(u32: Debug) :-
|
||||||
(Vec<?U>: Debug) :- (?U: Debug)
|
(Vec<?U>: Debug) :- (?U: Debug)
|
||||||
(Rc<?V>: Debug) :- (?V: Debug)
|
(Rc<?V>: Debug) :- (?V: Debug)
|
||||||
```
|
```
|
||||||
|
|
||||||
**Delegation between tables.** Now that the active strand from T0 has
|
**Delegation between tables.** Now that the active strand from T0 has
|
||||||
created the table T1, it can try to extract an answer. It does this
|
created the table T1, it can try to extract an answer. It does this
|
||||||
via that same `ensure_answer` operation we saw before. In this case,
|
via that same `ensure_answer` operation we saw before. In this case,
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue