@@ -41,8 +41,8 @@ define a kind of "minimal embedding" of chalk.
41
41
| The ` chalk-solve ` crate | |
42
42
| ---| --- |
43
43
| 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 ` |
46
46
47
47
The ` chalk-solve ` crate exposes a key type called ` Solver ` . This is a
48
48
solver 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
51
51
with common subgoals) is faster.
52
52
53
53
The 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
55
55
provide needed context for the solver -- notably, the solver can ask:
56
56
57
57
- ** 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.
60
60
61
61
62
62
## The chalk-engine crate
@@ -70,66 +70,7 @@ provide needed context for the solver -- notably, the solver can ask:
70
70
For the purposes of chalk, the ` chalk-engine ` crate is effectively
71
71
encapsulated by ` chalk-solve ` . It defines the base SLG engine. It is
72
72
written 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
76
74
` chalk_engine::context::Context ` , which contain (for example)
77
75
associated types that define what a goal or clause is, as well as
78
76
functions 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