@@ -41,8 +41,8 @@ define a kind of "minimal embedding" of chalk.
4141| The ` chalk-solve ` crate | |
4242| ---| --- |
4343| Purpose: | to solve a given goal |
44- | Depends on IR: | chalk-ir but not rust-ir |
45- | Context required: | ` ChalkSolveDatabase ` |
44+ | Depends on IR: | chalk-ir and rust-ir |
45+ | Context required: | ` RustIrDatabase ` |
4646
4747The ` chalk-solve ` crate exposes a key type called ` Solver ` . This is a
4848solver that, given a goal (expressed in chalk-ir) will solve the goal
@@ -51,12 +51,12 @@ invocations, so solving the same goal twice in a row (or solving goals
5151with common subgoals) is faster.
5252
5353The solver is configured by a type that implements the
54- ` ChalkSolveDatabase ` trait. This trait contains some callbacks that
54+ ` RustIrDatabase ` trait. This trait contains some callbacks that
5555provide needed context for the solver -- notably, the solver can ask:
5656
5757- ** What are the program clauses that might solve given rule?** This
58- is answered by the code in the chalk-rules crate.
59- - ** Is this trait coinductive?** This is answered by the rust -ir.
58+ is answered by the code in the chalk-solve crate.
59+ - ** Is this trait coinductive?** This is answered by the chalk -ir.
6060
6161
6262## The chalk-engine crate
@@ -70,66 +70,7 @@ provide needed context for the solver -- notably, the solver can ask:
7070For the purposes of chalk, the ` chalk-engine ` crate is effectively
7171encapsulated by ` chalk-solve ` . It defines the base SLG engine. It is
7272written in a very generic style that knows next to nothing about Rust
73- itself. In particular, it does not depend on any of the Chalk IRs,
74- which allows it to be used by rustc (which currently doesn't use
75- chalk-ir). The engine can be configured via the traits defined in
73+ itself. The engine can be configured via the traits defined in
7674` chalk_engine::context::Context ` , which contain (for example)
7775associated types that define what a goal or clause is, as well as
7876functions that operate on those things.
79-
80- ## The chalk-rules crate
81-
82- | The ` chalk-rules ` crate | |
83- | ---| --- |
84- | Purpose: | create chalk-ir goals/clauses given rust-ir |
85- | Depends on IR: | chalk-ir and rust-ir |
86- | Context required: | ` Context ` trait |
87-
88- The ` chalk-rules ` defines code that "lowers" rust-ir into chalk-ir,
89- producing both goals and clauses.
90-
91- - For example, the ` clauses ` module defines a trait
92- (` ToProgramClauses ` ) that is implemented for various bits of
93- rust-ir. It might (for example) lower an impl into a set of program
94- clauses.
95- - The coherence rules are defined in the ` coherence ` module; these
96- include code to check if an impl meets the orphan rules, and to
97- check for overlap between impls.
98- - These can also return information about the specialization tree
99- for a given trait.
100- - Finally, the well-formedness rules are defined in the ` wf ` module.
101-
102- The chalk-rules crate defines a ` ChalkRulesDatabase ` trait that contains
103- a number of callbacks that it needs. These callbacks are grouped into
104- two sub-traits:
105-
106- - The ` GoalSolver ` trait, which exposes a ` solve ` method for solving
107- goals. This solving is ultimately done by the code in the
108- ` chalk-solve ` crate.
109- - The ` RustIrDatabase ` trait, which offers a number of accessors to
110- fetch rust-ir. For example, the ` trait_datum ` method returns the
111- ` TraitDatum ` for a given ` TraitId ` .
112- - Note that -- by design -- this trait does not include any
113- "open-ended" methods that ask queries like "return all the impls
114- in the program" or "return all structs". These sorts of open-ended
115- walks are expected to be performed at an outer level (in our case,
116- in the chalk crate).
117-
118- ## The flow
119-
120- This section tries to document how the flow of information proceeds in
121- the main chalk testing harness. This can help give an idea how all the
122- parts of the system interact.
123-
124- - To begin with, the integration crate is asked to solve some goal
125- (via ` ChalkRulesDatabase::solve ` , for example).
126- - It will get access to its internal ` Solver ` (instantiating one, if
127- one does not already exist) and invoke the ` Solver::solve ` method.
128- - The solver may periodically request the set of applicable program clauses
129- for the main goal or some subgoal.
130- - The integration crate will examine the goal in question and use the code in the ` chalk-rules `
131- crate to instantiate program clauses.
132- - This may, in the case of specialization, require recursively solving goals.
133- - Once the program clauses are known, the solver can continue. It may
134- periodically ask the integration crate whether a given bit of IR is
135- coinductive.
0 commit comments