chalk has moved to rust-lang
This commit is contained in:
Mark Mansi
parent
be8685ab1f
commit
55856e4162
|
|
@ -172,7 +172,7 @@ Chalk's functionality is broken up into the following crates:
|
|||
- `coherence`, which implements coherence rules
|
||||
- Also includes [chalki][chalki], chalk's REPL.
|
||||
|
||||
[Browse source code on GitHub](https://github.com/rust-lang-nursery/chalk)
|
||||
[Browse source code on GitHub](https://github.com/rust-lang/chalk)
|
||||
|
||||
## Testing
|
||||
|
||||
|
|
@ -202,8 +202,8 @@ Likewise, lowering tests use the [`lowering_success!` and
|
|||
|
||||
## More Resources
|
||||
|
||||
* [Chalk Source Code](https://github.com/rust-lang-nursery/chalk)
|
||||
* [Chalk Glossary](https://github.com/rust-lang-nursery/chalk/blob/master/GLOSSARY.md)
|
||||
* [Chalk Source Code](https://github.com/rust-lang/chalk)
|
||||
* [Chalk Glossary](https://github.com/rust-lang/chalk/blob/master/GLOSSARY.md)
|
||||
|
||||
### Blog Posts
|
||||
|
||||
|
|
@ -224,34 +224,34 @@ Likewise, lowering tests use the [`lowering_success!` and
|
|||
[wf-checking]: ./wf.html
|
||||
|
||||
[ast]: https://en.wikipedia.org/wiki/Abstract_syntax_tree
|
||||
[chalk]: https://github.com/rust-lang-nursery/chalk
|
||||
[rustc-issues]: https://github.com/rust-lang-nursery/rustc-guide/issues
|
||||
[chalk]: https://github.com/rust-lang/chalk
|
||||
[rustc-issues]: https://github.com/rust-lang/rustc-guide/issues
|
||||
[universal quantification]: https://en.wikipedia.org/wiki/Universal_quantification
|
||||
|
||||
[`ProgramClause`]: https://rust-lang-nursery.github.io/chalk/doc/chalk_ir/enum.ProgramClause.html
|
||||
[`ProgramEnvironment`]: https://rust-lang-nursery.github.io/chalk/doc/chalk_ir/struct.ProgramEnvironment.html
|
||||
[chalk_engine]: https://rust-lang-nursery.github.io/chalk/doc/chalk_engine/index.html
|
||||
[chalk_ir]: https://rust-lang-nursery.github.io/chalk/doc/chalk_ir/index.html
|
||||
[chalk_parse]: https://rust-lang-nursery.github.io/chalk/doc/chalk_parse/index.html
|
||||
[chalk_solve]: https://rust-lang-nursery.github.io/chalk/doc/chalk_solve/index.html
|
||||
[doc-chalk]: https://rust-lang-nursery.github.io/chalk/doc/chalk/index.html
|
||||
[engine-context]: https://rust-lang-nursery.github.io/chalk/doc/chalk_engine/context/index.html
|
||||
[rust_ir-program]: https://rust-lang-nursery.github.io/chalk/doc/chalk/rust_ir/struct.Program.html
|
||||
[rust_ir]: https://rust-lang-nursery.github.io/chalk/doc/chalk/rust_ir/index.html
|
||||
[`ProgramClause`]: https://rust-lang.github.io/chalk/doc/chalk_ir/enum.ProgramClause.html
|
||||
[`ProgramEnvironment`]: https://rust-lang.github.io/chalk/doc/chalk_ir/struct.ProgramEnvironment.html
|
||||
[chalk_engine]: https://rust-lang.github.io/chalk/doc/chalk_engine/index.html
|
||||
[chalk_ir]: https://rust-lang.github.io/chalk/doc/chalk_ir/index.html
|
||||
[chalk_parse]: https://rust-lang.github.io/chalk/doc/chalk_parse/index.html
|
||||
[chalk_solve]: https://rust-lang.github.io/chalk/doc/chalk_solve/index.html
|
||||
[doc-chalk]: https://rust-lang.github.io/chalk/doc/chalk/index.html
|
||||
[engine-context]: https://rust-lang.github.io/chalk/doc/chalk_engine/context/index.html
|
||||
[rust_ir-program]: https://rust-lang.github.io/chalk/doc/chalk/rust_ir/struct.Program.html
|
||||
[rust_ir]: https://rust-lang.github.io/chalk/doc/chalk/rust_ir/index.html
|
||||
|
||||
[binders-struct]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/ir.rs#L661
|
||||
[chalk-ast]: https://github.com/rust-lang-nursery/chalk/blob/master/chalk-parse/src/ast.rs
|
||||
[chalk-test-example]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L115
|
||||
[chalk-test-lowering-example]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rust_ir/lowering/test.rs#L8-L31
|
||||
[chalk-test-lowering]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rust_ir/lowering/test.rs
|
||||
[chalk-test-wf]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules/wf/test.rs#L1
|
||||
[chalki]: https://rust-lang-nursery.github.io/chalk/doc/chalki/index.html
|
||||
[clause]: https://github.com/rust-lang-nursery/chalk/blob/master/GLOSSARY.md#clause
|
||||
[coherence-src]: https://github.com/rust-lang-nursery/chalk/blob/master/src/coherence.rs
|
||||
[ir-code]: https://github.com/rust-lang-nursery/chalk/blob/master/src/rust_ir.rs
|
||||
[rules-environment]: https://github.com/rust-lang-nursery/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/rules.rs#L9
|
||||
[rules-src]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules.rs
|
||||
[rules-wf-src]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules/wf.rs
|
||||
[solve_goal]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L85
|
||||
[test-lowering-macros]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test_util.rs#L21-L54
|
||||
[test-macro]: https://github.com/rust-lang-nursery/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L33
|
||||
[binders-struct]: https://github.com/rust-lang/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/ir.rs#L661
|
||||
[chalk-ast]: https://github.com/rust-lang/chalk/blob/master/chalk-parse/src/ast.rs
|
||||
[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]: 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
|
||||
[chalki]: https://rust-lang.github.io/chalk/doc/chalki/index.html
|
||||
[clause]: https://github.com/rust-lang/chalk/blob/master/GLOSSARY.md#clause
|
||||
[coherence-src]: https://github.com/rust-lang/chalk/blob/master/src/coherence.rs
|
||||
[ir-code]: https://github.com/rust-lang/chalk/blob/master/src/rust_ir.rs
|
||||
[rules-environment]: https://github.com/rust-lang/chalk/blob/94a1941a021842a5fcb35cd043145c8faae59f08/src/rules.rs#L9
|
||||
[rules-src]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules.rs
|
||||
[rules-wf-src]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules/wf.rs
|
||||
[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-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
|
||||
interdependent: solving one query may require solving others.
|
||||
|
||||
[`Forest`]: https://rust-lang-nursery.github.io/chalk/doc/chalk_engine/forest/struct.Forest.html
|
||||
[`Forest`]: https://rust-lang.github.io/chalk/doc/chalk_engine/forest/struct.Forest.html
|
||||
|
||||
### Walkthrough
|
||||
|
||||
|
|
@ -150,7 +150,7 @@ 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
|
||||
[`ExClause`]: https://rust-lang.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.
|
||||
|
|
@ -187,7 +187,7 @@ 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
|
||||
[`ensure_root_answer`]: https://rust-lang.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
|
||||
|
|
@ -297,6 +297,6 @@ more answers later on.
|
|||
- [Negative Reasoning in Chalk][negative-reasoning-blog] explains the need
|
||||
for negative reasoning, but not how the SLG solver does it
|
||||
|
||||
[readme]: https://github.com/rust-lang-nursery/chalk/blob/239e4ae4e69b2785b5f99e0f2b41fc16b0b4e65e/chalk-engine/src/README.md
|
||||
[readme]: https://github.com/rust-lang/chalk/blob/239e4ae4e69b2785b5f99e0f2b41fc16b0b4e65e/chalk-engine/src/README.md
|
||||
[slg-blog]: http://smallcultfollowing.com/babysteps/blog/2018/01/31/an-on-demand-slg-solver-for-chalk/
|
||||
[negative-reasoning-blog]: http://aturon.github.io/blog/2017/04/24/negative-chalk/
|
||||
|
|
|
|||
Loading…
Reference in New Issue