/
fulfill.rs
266 lines (238 loc) · 11.1 KB
/
fulfill.rs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
use errors::*;
use fold::Fold;
use ir::*;
use solve::Successful;
use solve::infer::{InferenceTable, UnificationResult, ParameterInferenceVariable};
use solve::solver::Solver;
use std::collections::HashSet;
use std::fmt::Debug;
use std::sync::Arc;
use zip::Zip;
pub struct Fulfill<'s> {
solver: &'s mut Solver,
infer: InferenceTable,
obligations: Vec<InEnvironment<WhereClauseGoal>>,
constraints: HashSet<InEnvironment<Constraint>>,
}
impl<'s> Fulfill<'s> {
pub fn new(solver: &'s mut Solver) -> Self {
Fulfill {
solver,
infer: InferenceTable::new(),
obligations: vec![],
constraints: HashSet::new(),
}
}
pub fn program(&self) -> Arc<ProgramEnvironment> {
self.solver.program.clone()
}
/// Wraps `InferenceTable::instantiate`
pub fn instantiate<U, T>(&mut self, universes: U, arg: &T) -> T::Result
where T: Fold,
U: IntoIterator<Item = ParameterKind<UniverseIndex>>
{
self.infer.instantiate(universes, arg)
}
/// Instantiates `arg` with fresh existential variables in the
/// given universe; the kinds of the variables are implied by
/// `binders`. This is used to apply a universally quantified
/// clause like `forall X, 'Y. P => Q`. Here the `binders`
/// argument is referring to `X, 'Y`.
pub fn instantiate_in<U, T>(&mut self,
universe: UniverseIndex,
binders: U,
arg: &T) -> T::Result
where T: Fold,
U: IntoIterator<Item = ParameterKind<()>>
{
self.instantiate(binders.into_iter().map(|pk| pk.map(|_| universe)), arg)
}
/// Unifies `a` and `b` in the given environment.
///
/// Wraps `InferenceTable::unify`; any resulting normalzations are
/// added into our list of pending obligations with the given
/// environment.
pub fn unify<T>(&mut self, environment: &Arc<Environment>, a: &T, b: &T) -> Result<()>
where T: ?Sized + Zip + Debug
{
let UnificationResult { goals, constraints } = self.infer.unify(environment, a, b)?;
debug!("unify({:?}, {:?}) succeeded", a, b);
debug!("unify: goals={:?}", goals);
debug!("unify: constraints={:?}", constraints);
self.constraints.extend(constraints);
self.extend(goals);
Ok(())
}
/// Wraps `InferenceTable::new_parameter_variable`
pub fn new_parameter_variable(&mut self, ui: ParameterKind<UniverseIndex>)
-> ParameterInferenceVariable {
self.infer.new_parameter_variable(ui)
}
/// Adds the given where-clauses to the internal list of
/// obligations that must be solved.
pub fn extend<WC>(&mut self, wc: WC)
where WC: IntoIterator<Item=InEnvironment<WhereClauseGoal>>
{
self.obligations.extend(wc);
}
/// Return current list of pending obligations; used for unit testing primarily
pub fn pending_obligations(&self) -> &[InEnvironment<WhereClauseGoal>] {
&self.obligations
}
/// Create obligations for the given goal in the given
/// environment. This may ultimately create any number of
/// obligations.
pub fn push_goal(&mut self, goal: Goal, environment: &Arc<Environment>) {
debug!("push_goal({:?}, {:?})", goal, environment);
match goal {
Goal::Quantified(QuantifierKind::ForAll, subgoal) => {
let mut new_environment = environment.clone();
let parameters: Vec<_> =
subgoal.binders
.iter()
.map(|pk| {
new_environment = new_environment.new_universe();
match *pk {
ParameterKind::Lifetime(()) =>
ParameterKind::Lifetime(Lifetime::ForAll(new_environment.universe)),
ParameterKind::Ty(()) =>
ParameterKind::Ty(Ty::Apply(ApplicationTy {
name: TypeName::ForAll(new_environment.universe),
parameters: vec![]
})),
}
})
.collect();
let subgoal = subgoal.value.subst(¶meters);
self.push_goal(subgoal, &new_environment);
}
Goal::Quantified(QuantifierKind::Exists, subgoal) => {
let subgoal = self.instantiate_in(environment.universe,
subgoal.binders.iter().cloned(),
&subgoal.value);
self.push_goal(*subgoal, environment);
}
Goal::Implies(wc, subgoal) => {
let new_environment = &environment.add_clauses(wc);
self.push_goal(*subgoal, new_environment);
}
Goal::And(subgoal1, subgoal2) => {
self.push_goal(*subgoal1, environment);
self.push_goal(*subgoal2, environment);
}
Goal::Leaf(wc) => {
self.obligations.push(InEnvironment::new(environment, wc));
}
}
}
/// As the final step in process a goal, we always have to deliver
/// back a "refined goal" that shows what we learned. This refined
/// goal combines any lifetime constraints with the final results
/// of inference. It is produced by this method.
pub fn refine_goal<G: Fold>(mut self, goal: G) -> Query<Constrained<G::Result>> {
let mut constraints: Vec<_> = self.constraints.into_iter().collect();
constraints.sort();
debug!("refine_goal: constraints = {:?}", constraints);
let constrained_goal = Constrained {
value: goal,
constraints: constraints,
};
self.infer.make_query(&constrained_goal)
}
/// Try to solve all `obligations`, which may contain inference variables
/// registered in the table `infer`. This can have side-effects on the
/// inference state (regardless of whether it returns success, failure, or
/// ambiguity). But, in all cases, the side-effects are only things that
/// must be true for `obligations` to be true.
pub fn solve_all(&mut self) -> Result<Successful> {
debug_heading!("solve_all(where_clauses={:#?})", self.obligations);
// Try to solve all the obligations. We do this via a fixed-point
// iteration. We try to solve each obligation in turn. Anything which is
// successful, we drop; anything ambiguous, we retain in the
// `obligations` array. This process is repeated so long as we are
// learning new things about our inference state.
let mut obligations = Vec::with_capacity(self.obligations.len());
let mut progress = true;
while progress {
progress = false;
debug_heading!("start of round, {:?} obligations", self.obligations.len());
// Take the list of `obligations` to solve this round and replace it
// with an empty vector. Iterate through each obligation to solve
// and solve it if we can. If not (because of ambiguity), then push
// it back onto `self.obligations` for next round. Note that
// `solve_one` may also push onto the `self.obligations` list
// directly.
assert!(obligations.is_empty());
while let Some(wc) = self.obligations.pop() {
match self.solve_one(&wc, &mut progress)? {
Successful::Yes => (),
Successful::Maybe => {
debug!("ambiguous result: {:?}", wc);
obligations.push(wc);
}
}
}
self.obligations.extend(obligations.drain(..));
debug!("end of round, {:?} obligations left", self.obligations.len());
}
// At the end of this process, `self.obligations` should have
// all of the ambiguous obligations, and `obligations` should
// be empty.
assert!(obligations.is_empty());
// If we still have ambiguous obligations, then we have an
// ambiguous overall result.
if self.obligations.is_empty() {
Ok(Successful::Yes)
} else {
debug!("still have {} ambiguous obligations: {:#?}",
self.obligations.len(), self.obligations);
Ok(Successful::Maybe)
}
}
fn solve_one(&mut self,
wc: &InEnvironment<WhereClauseGoal>,
inference_progress: &mut bool)
-> Result<Successful> {
debug!("fulfill::solve_one(wc={:?})", wc);
let quantified_wc = self.infer.make_query(&wc);
let solution = self.solver.solve(quantified_wc.clone())?;
// Regardless of whether the result is ambiguous or not,
// solving the where-clause may have yielded a refined
// goal. For example, if the original where-clause was
// something like `Foo<?4>: Borrow<?3>`, we would have
// "quantified" that to yield `exists ?0, ?1. Foo<?0>: Borrow<?1>`.
// We may now have gotten back a refined goal like `exists ?0. Foo<?0>:
// Borrow<Foo<?0>>`. In that case, we can unify `?3` with `Foo<?4>`.
//
// To make that unification happen, we first instantiate all
// the variables on the goal we got back with new inference
// variables. So we would thus convert `exists ?0. Foo<?0>:
// Borrow<Foo<?0>>` into `Foo<?5>: Borrow<Foo<?5>>`. We would
// then unify this with our original goal (`Foo<?4>:
// Borrow<?3>`). This will result in the equations `?4 = ?5`
// and `?3 = Foo<?5>`.
//
// As a potential efficiency improvement, one could imagine a
// more algorithm written just for this case instead of
// instantiating with variables and applying the standard
// unification algorithm. But this is good enough for now.
let new_type_info = {
solution.refined_goal.binders != quantified_wc.binders ||
solution.refined_goal.value.value != quantified_wc.value
};
debug!("fulfill::solve_one: new_type_info={}", new_type_info);
if new_type_info || !solution.refined_goal.value.constraints.is_empty() {
let Constrained { constraints, value: refined_goal } =
self.instantiate(solution.refined_goal.binders.iter().cloned(),
&solution.refined_goal.value);
debug!("fulfill::solve_one: adding constraints {:?}", constraints);
self.constraints.extend(constraints);
debug!("fulfill::solve_one: unifying original and refined goal");
self.unify(&wc.environment, wc, &refined_goal)?;
if new_type_info {
*inference_progress = true;
}
}
Ok(solution.successful)
}
}