1
1
use crate :: fallible:: Fallible ;
2
2
use crate :: hh:: HhGoal ;
3
- use crate :: { ExClause , SimplifiedAnswer } ;
3
+ use crate :: { DelayedLiteral , ExClause , SimplifiedAnswer } ;
4
4
use std:: fmt:: Debug ;
5
5
use std:: hash:: Hash ;
6
6
7
7
crate mod prelude;
8
8
9
- /// The "context" in which the SLG solver operates.
10
- // FIXME(leodasvacas): Clone and Debug bounds are just for easy derive,
11
- // they are not actually necessary.
9
+ /// The "context" in which the SLG solver operates. It defines all the
10
+ /// types that the SLG solver may need to refer to, as well as a few
11
+ /// very simple interconversion methods.
12
+ ///
13
+ /// At any given time, the SLG solver may have more than one context
14
+ /// active. First, there is always the *global* context, but when we
15
+ /// are in the midst of pursuing some particular strand, we will
16
+ /// instantiate a second context just for that work, via the
17
+ /// `instantiate_ucanonical_goal` and `instantiate_ex_clause` methods.
18
+ ///
19
+ /// In the chalk implementation, these two contexts are mapped to the
20
+ /// same type. But in the rustc implementation, this second context
21
+ /// corresponds to a fresh arena, and data allocated in that second
22
+ /// context will be freed once the work is done. (The "canonicalizing"
23
+ /// steps offer a way to convert data from the inference context back
24
+ /// into the global context.)
25
+ ///
26
+ /// FIXME: Clone and Debug bounds are just for easy derive, they are
27
+ /// not actually necessary. But dang are they convenient.
12
28
pub trait Context : Clone + Debug {
13
29
type CanonicalExClause : Debug ;
14
30
@@ -17,12 +33,6 @@ pub trait Context: Clone + Debug {
17
33
/// the universes from the original.
18
34
type UniverseMap : Clone + Debug ;
19
35
20
- /// Part of an answer: represents a canonicalized substitution,
21
- /// combined with region constraints. See [the rustc-guide] for more information.
22
- ///
23
- /// [the rustc-guide]: https://rust-lang-nursery.github.io/rustc-guide/traits-canonicalization.html#canonicalizing-the-query-result
24
- type CanonicalConstrainedSubst : Clone + Debug + Eq + Hash ;
25
-
26
36
/// Extracted from a canonicalized substitution or canonicalized ex clause, this is the type of
27
37
/// substitution that is fully normalized with respect to inference variables.
28
38
type InferenceNormalizedSubst : Debug ;
@@ -43,9 +53,13 @@ pub trait Context: Clone + Debug {
43
53
/// completely opaque to the SLG solver; it is produced by
44
54
/// `make_solution`.
45
55
type Solution ;
46
- }
47
56
48
- pub trait ExClauseContext < C : Context > : Sized + Debug {
57
+ /// Part of an answer: represents a canonicalized substitution,
58
+ /// combined with region constraints. See [the rustc-guide] for more information.
59
+ ///
60
+ /// [the rustc-guide]: https://rust-lang-nursery.github.io/rustc-guide/traits-canonicalization.html#canonicalizing-the-query-result
61
+ type CanonicalConstrainedSubst : Clone + Debug + Eq + Hash ;
62
+
49
63
/// Represents a substitution from the "canonical variables" found
50
64
/// in a canonical goal to specific values.
51
65
type Substitution : Debug ;
@@ -56,12 +70,7 @@ pub trait ExClauseContext<C: Context>: Sized + Debug {
56
70
57
71
/// Represents a goal along with an environment.
58
72
type GoalInEnvironment : Debug + Clone + Eq + Hash ;
59
- }
60
73
61
- /// The set of types belonging to an "inference context"; in rustc,
62
- /// these types are tied to the lifetime of the arena within which an
63
- /// inference context operates.
64
- pub trait InferenceContext < C : Context > : ExClauseContext < C > {
65
74
/// Represents a set of hypotheses that are assumed to be true.
66
75
type Environment : Debug + Clone ;
67
76
@@ -91,10 +100,15 @@ pub trait InferenceContext<C: Context>: ExClauseContext<C> {
91
100
/// goal we are trying to solve to produce an ex-clause.
92
101
type ProgramClause : Debug ;
93
102
103
+ /// A vector of program clauses.
104
+ type ProgramClauses : Debug ;
105
+
94
106
/// The successful result from unification: contains new subgoals
95
107
/// and things that can be attached to an ex-clause.
96
108
type UnificationResult ;
97
109
110
+ /// Given an environment and a goal, glue them together to create
111
+ /// a `GoalInEnvironment`.
98
112
fn goal_in_environment (
99
113
environment : & Self :: Environment ,
100
114
goal : Self :: Goal ,
@@ -105,26 +119,6 @@ pub trait InferenceContext<C: Context>: ExClauseContext<C> {
105
119
106
120
/// Create a "cannot prove" goal (see `HhGoal::CannotProve`).
107
121
fn cannot_prove ( ) -> Self :: Goal ;
108
-
109
- /// Convert the context's goal type into the `HhGoal` type that
110
- /// the SLG solver understands. The expectation is that the
111
- /// context's goal type has the same set of variants, but with
112
- /// different names and a different setup. If you inspect
113
- /// `HhGoal`, you will see that this is a "shallow" or "lazy"
114
- /// conversion -- that is, we convert the outermost goal into an
115
- /// `HhGoal`, but the goals contained within are left as context
116
- /// goals.
117
- fn into_hh_goal ( goal : Self :: Goal ) -> HhGoal < C , Self > ;
118
-
119
- /// Add the residual subgoals as new subgoals of the ex-clause.
120
- /// Also add region constraints.
121
- fn into_ex_clause ( result : Self :: UnificationResult , ex_clause : & mut ExClause < C , Self > ) ;
122
-
123
- // Used by: simplify
124
- fn add_clauses (
125
- env : & Self :: Environment ,
126
- clauses : impl IntoIterator < Item = Self :: ProgramClause > ,
127
- ) -> Self :: Environment ;
128
122
}
129
123
130
124
pub trait ContextOps < C : Context > : Sized + Clone + Debug + AggregateOps < C > {
@@ -201,7 +195,7 @@ pub trait ContextOps<C: Context>: Sized + Clone + Debug + AggregateOps<C> {
201
195
pub trait WithInstantiatedUCanonicalGoal < C : Context > {
202
196
type Output ;
203
197
204
- fn with < I : InferenceContext < C > > (
198
+ fn with < I : Context > (
205
199
self ,
206
200
infer : & mut dyn InferenceTable < C , I > ,
207
201
subst : I :: Substitution ,
@@ -219,10 +213,10 @@ pub trait WithInstantiatedUCanonicalGoal<C: Context> {
219
213
pub trait WithInstantiatedExClause < C : Context > {
220
214
type Output ;
221
215
222
- fn with < I : InferenceContext < C > > (
216
+ fn with < I : Context > (
223
217
self ,
224
218
infer : & mut dyn InferenceTable < C , I > ,
225
- ex_clause : ExClause < C , I > ,
219
+ ex_clause : ExClause < I > ,
226
220
) -> Self :: Output ;
227
221
}
228
222
@@ -237,13 +231,29 @@ pub trait AggregateOps<C: Context> {
237
231
238
232
/// An "inference table" contains the state to support unification and
239
233
/// other operations on terms.
240
- pub trait InferenceTable < C : Context , I : InferenceContext < C > > :
234
+ pub trait InferenceTable < C : Context , I : Context > :
241
235
ResolventOps < C , I > + TruncateOps < C , I > + UnificationOps < C , I >
242
236
{
237
+ /// Convert the context's goal type into the `HhGoal` type that
238
+ /// the SLG solver understands. The expectation is that the
239
+ /// context's goal type has the same set of variants, but with
240
+ /// different names and a different setup. If you inspect
241
+ /// `HhGoal`, you will see that this is a "shallow" or "lazy"
242
+ /// conversion -- that is, we convert the outermost goal into an
243
+ /// `HhGoal`, but the goals contained within are left as context
244
+ /// goals.
245
+ fn into_hh_goal ( & mut self , goal : I :: Goal ) -> HhGoal < I > ;
246
+
247
+ // Used by: simplify
248
+ fn add_clauses (
249
+ & mut self ,
250
+ env : & I :: Environment ,
251
+ clauses : I :: ProgramClauses ,
252
+ ) -> I :: Environment ;
243
253
}
244
254
245
255
/// Methods for unifying and manipulating terms and binders.
246
- pub trait UnificationOps < C : Context , I : InferenceContext < C > > {
256
+ pub trait UnificationOps < C : Context , I : Context > {
247
257
/// Returns the set of program clauses that might apply to
248
258
/// `goal`. (This set can be over-approximated, naturally.)
249
259
fn program_clauses (
@@ -259,13 +269,13 @@ pub trait UnificationOps<C: Context, I: InferenceContext<C>> {
259
269
fn instantiate_binders_existentially ( & mut self , arg : & I :: BindersGoal ) -> I :: Goal ;
260
270
261
271
// Used by: logic (but for debugging only)
262
- fn debug_ex_clause ( & mut self , value : & ' v ExClause < C , I > ) -> Box < dyn Debug + ' v > ;
272
+ fn debug_ex_clause ( & mut self , value : & ' v ExClause < I > ) -> Box < dyn Debug + ' v > ;
263
273
264
274
// Used by: logic
265
275
fn canonicalize_goal ( & mut self , value : & I :: GoalInEnvironment ) -> C :: CanonicalGoalInEnvironment ;
266
276
267
277
// Used by: logic
268
- fn canonicalize_ex_clause ( & mut self , value : & ExClause < C , I > ) -> C :: CanonicalExClause ;
278
+ fn canonicalize_ex_clause ( & mut self , value : & ExClause < I > ) -> C :: CanonicalExClause ;
269
279
270
280
// Used by: logic
271
281
fn canonicalize_constrained_subst (
@@ -280,6 +290,16 @@ pub trait UnificationOps<C: Context, I: InferenceContext<C>> {
280
290
value : & C :: CanonicalGoalInEnvironment ,
281
291
) -> ( C :: UCanonicalGoalInEnvironment , C :: UniverseMap ) ;
282
292
293
+ fn sink_answer_subset (
294
+ & self ,
295
+ value : & C :: CanonicalConstrainedSubst ,
296
+ ) -> I :: CanonicalConstrainedSubst ;
297
+
298
+ fn lift_delayed_literal (
299
+ & self ,
300
+ value : DelayedLiteral < I > ,
301
+ ) -> DelayedLiteral < C > ;
302
+
283
303
// Used by: logic
284
304
fn invert_goal ( & mut self , value : & I :: GoalInEnvironment ) -> Option < I :: GoalInEnvironment > ;
285
305
@@ -290,6 +310,10 @@ pub trait UnificationOps<C: Context, I: InferenceContext<C>> {
290
310
a : & I :: Parameter ,
291
311
b : & I :: Parameter ,
292
312
) -> Fallible < I :: UnificationResult > ;
313
+
314
+ /// Add the residual subgoals as new subgoals of the ex-clause.
315
+ /// Also add region constraints.
316
+ fn into_ex_clause ( & mut self , result : I :: UnificationResult , ex_clause : & mut ExClause < I > ) ;
293
317
}
294
318
295
319
/// "Truncation" (called "abstraction" in the papers referenced below)
@@ -304,7 +328,7 @@ pub trait UnificationOps<C: Context, I: InferenceContext<C>> {
304
328
/// - Riguzzi and Swift; ACM Transactions on Computational Logic 2013
305
329
/// - Radial Restraint
306
330
/// - Grosof and Swift; 2013
307
- pub trait TruncateOps < C : Context , I : InferenceContext < C > > {
331
+ pub trait TruncateOps < C : Context , I : Context > {
308
332
/// If `subgoal` is too large, return a truncated variant (else
309
333
/// return `None`).
310
334
fn truncate_goal ( & mut self , subgoal : & I :: GoalInEnvironment ) -> Option < I :: GoalInEnvironment > ;
@@ -314,7 +338,7 @@ pub trait TruncateOps<C: Context, I: InferenceContext<C>> {
314
338
fn truncate_answer ( & mut self , subst : & I :: Substitution ) -> Option < I :: Substitution > ;
315
339
}
316
340
317
- pub trait ResolventOps < C : Context , I : InferenceContext < C > > {
341
+ pub trait ResolventOps < C : Context , I : Context > {
318
342
/// Combines the `goal` (instantiated within `infer`) with the
319
343
/// given program clause to yield the start of a new strand (a
320
344
/// canonical ex-clause).
@@ -330,11 +354,11 @@ pub trait ResolventOps<C: Context, I: InferenceContext<C>> {
330
354
331
355
fn apply_answer_subst (
332
356
& mut self ,
333
- ex_clause : ExClause < C , I > ,
357
+ ex_clause : ExClause < I > ,
334
358
selected_goal : & I :: GoalInEnvironment ,
335
359
answer_table_goal : & C :: CanonicalGoalInEnvironment ,
336
360
canonical_answer_subst : & C :: CanonicalConstrainedSubst ,
337
- ) -> Fallible < ExClause < C , I > > ;
361
+ ) -> Fallible < ExClause < I > > ;
338
362
}
339
363
340
364
pub trait AnswerStream < C : Context > {
0 commit comments