1 use chalk_engine::fallible::{Fallible, NoSolution};
7 use rustc::infer::{InferCtxt, LateBoundRegionConversionTime};
8 use rustc::infer::canonical::{Canonical, CanonicalVarValues};
19 use rustc::ty::{self, Ty, TyCtxt, InferConst};
20 use rustc::ty::subst::Kind;
21 use rustc::ty::relate::{Relate, RelateResult, TypeRelation};
22 use rustc::mir::interpret::ConstValue;
23 use syntax_pos::DUMMY_SP;
25 use super::{ChalkInferenceContext, ChalkArenas, ChalkExClause, ConstrainedSubst};
28 impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
29 for ChalkInferenceContext<'cx, 'gcx, 'tcx>
33 environment: &Environment<'tcx>,
34 goal: &DomainGoal<'tcx>,
35 subst: &CanonicalVarValues<'tcx>,
36 clause: &Clause<'tcx>,
37 ) -> Fallible<Canonical<'gcx, ChalkExClause<'gcx>>> {
38 use chalk_engine::context::UnificationOps;
40 debug!("resolvent_clause(goal = {:?}, clause = {:?})", goal, clause);
42 let result = self.infcx.probe(|_| {
48 Clause::Implies(program_clause) => *program_clause,
49 Clause::ForAll(program_clause) => self.infcx.replace_bound_vars_with_fresh_vars(
51 LateBoundRegionConversionTime::HigherRankedType,
59 ty::Variance::Invariant,
62 ).map_err(|_| NoSolution)?;
64 let mut ex_clause = ExClause {
66 delayed_literals: vec![],
71 self.into_ex_clause(result, &mut ex_clause);
73 ex_clause.subgoals.extend(
74 hypotheses.iter().map(|g| match g {
75 GoalKind::Not(g) => Literal::Negative(environment.with(*g)),
76 g => Literal::Positive(environment.with(*g)),
80 // If we have a goal of the form `T: 'a` or `'a: 'b`, then just
81 // assume it is true (no subgoals) and register it as a constraint
84 DomainGoal::Holds(WhereClause::RegionOutlives(pred)) => {
85 assert_eq!(ex_clause.subgoals.len(), 0);
86 ex_clause.constraints.push(ty::OutlivesPredicate(pred.0.into(), pred.1));
89 DomainGoal::Holds(WhereClause::TypeOutlives(pred)) => {
90 assert_eq!(ex_clause.subgoals.len(), 0);
91 ex_clause.constraints.push(ty::OutlivesPredicate(pred.0.into(), pred.1));
97 let canonical_ex_clause = self.canonicalize_ex_clause(&ex_clause);
98 Ok(canonical_ex_clause)
101 debug!("resolvent_clause: result = {:?}", result);
105 fn apply_answer_subst(
107 ex_clause: ChalkExClause<'tcx>,
108 selected_goal: &InEnvironment<'tcx, Goal<'tcx>>,
109 answer_table_goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
110 canonical_answer_subst: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
111 ) -> Fallible<ChalkExClause<'tcx>> {
113 "apply_answer_subst(ex_clause = {:?}, selected_goal = {:?})",
114 self.infcx.resolve_type_vars_if_possible(&ex_clause),
115 self.infcx.resolve_type_vars_if_possible(selected_goal)
118 let (answer_subst, _) = self.infcx.instantiate_canonical_with_fresh_inference_vars(
120 canonical_answer_subst
123 let mut substitutor = AnswerSubstitutor {
125 environment: selected_goal.environment,
126 answer_subst: answer_subst.subst,
127 binder_index: ty::INNERMOST,
131 substitutor.relate(&answer_table_goal.value, &selected_goal)
132 .map_err(|_| NoSolution)?;
134 let mut ex_clause = substitutor.ex_clause;
135 ex_clause.constraints.extend(answer_subst.constraints);
137 debug!("apply_answer_subst: ex_clause = {:?}", ex_clause);
142 struct AnswerSubstitutor<'cx, 'gcx: 'tcx, 'tcx: 'cx> {
143 infcx: &'cx InferCtxt<'cx, 'gcx, 'tcx>,
144 environment: Environment<'tcx>,
145 answer_subst: CanonicalVarValues<'tcx>,
146 binder_index: ty::DebruijnIndex,
147 ex_clause: ChalkExClause<'tcx>,
150 impl AnswerSubstitutor<'cx, 'gcx, 'tcx> {
151 fn unify_free_answer_var(
153 answer_var: ty::BoundVar,
155 ) -> RelateResult<'tcx, ()> {
156 let answer_param = &self.answer_subst.var_values[answer_var];
157 let pending = &ty::fold::shift_out_vars(
160 self.binder_index.as_u32()
163 super::into_ex_clause(
164 unify(self.infcx, self.environment, ty::Variance::Invariant, answer_param, pending)?,
172 impl TypeRelation<'cx, 'gcx, 'tcx> for AnswerSubstitutor<'cx, 'gcx, 'tcx> {
173 fn tcx(&self) -> TyCtxt<'cx, 'gcx, 'tcx> {
177 fn tag(&self) -> &'static str {
178 "chalk_context::answer_substitutor"
181 fn a_is_expected(&self) -> bool {
185 fn relate_with_variance<T: Relate<'tcx>>(
187 _variance: ty::Variance,
190 ) -> RelateResult<'tcx, T> {
191 // We don't care about variance.
195 fn binders<T: Relate<'tcx>>(
199 ) -> RelateResult<'tcx, ty::Binder<T>> {
200 self.binder_index.shift_in(1);
201 let result = self.relate(a.skip_binder(), b.skip_binder())?;
202 self.binder_index.shift_out(1);
203 Ok(ty::Binder::bind(result))
206 fn tys(&mut self, a: Ty<'tcx>, b: Ty<'tcx>) -> RelateResult<'tcx, Ty<'tcx>> {
207 let b = self.infcx.shallow_resolve(b);
208 debug!("AnswerSubstitutor::tys(a = {:?}, b = {:?})", a, b);
210 if let &ty::Bound(debruijn, bound_ty) = &a.sty {
212 if debruijn == self.binder_index {
213 self.unify_free_answer_var(bound_ty.var, b.into())?;
218 match (&a.sty, &b.sty) {
219 (&ty::Bound(a_debruijn, a_bound), &ty::Bound(b_debruijn, b_bound)) => {
220 assert_eq!(a_debruijn, b_debruijn);
221 assert_eq!(a_bound.var, b_bound.var);
225 // Those should have been canonicalized away.
226 (ty::Placeholder(..), _) => {
227 bug!("unexpected placeholder ty in `AnswerSubstitutor`: {:?} ", a);
230 // Everything else should just be a perfect match as well,
231 // and we forbid inference variables.
232 _ => match ty::relate::super_relate_tys(self, a, b) {
234 Err(err) => bug!("type mismatch in `AnswerSubstitutor`: {}", err),
243 ) -> RelateResult<'tcx, ty::Region<'tcx>> {
245 &ty::ReVar(vid) => self.infcx
246 .borrow_region_constraints()
247 .opportunistic_resolve_var(self.infcx.tcx, vid),
252 if let &ty::ReLateBound(debruijn, bound) = a {
254 if debruijn == self.binder_index {
255 self.unify_free_answer_var(bound.assert_bound_var(), b.into())?;
261 (&ty::ReLateBound(a_debruijn, a_bound), &ty::ReLateBound(b_debruijn, b_bound)) => {
262 assert_eq!(a_debruijn, b_debruijn);
263 assert_eq!(a_bound.assert_bound_var(), b_bound.assert_bound_var());
266 (ty::ReStatic, ty::ReStatic) |
267 (ty::ReErased, ty::ReErased) |
268 (ty::ReEmpty, ty::ReEmpty) => (),
270 (&ty::ReFree(a_free), &ty::ReFree(b_free)) => {
271 assert_eq!(a_free, b_free);
274 _ => bug!("unexpected regions in `AnswerSubstitutor`: {:?}, {:?}", a, b),
282 a: &'tcx ty::Const<'tcx>,
283 b: &'tcx ty::Const<'tcx>,
284 ) -> RelateResult<'tcx, &'tcx ty::Const<'tcx>> {
286 val: ConstValue::Infer(InferConst::Canonical(debruijn, bound_ct)),
289 if *debruijn == self.binder_index {
290 self.unify_free_answer_var(*bound_ct, b.into())?;
298 val: ConstValue::Infer(InferConst::Canonical(a_debruijn, a_bound)),
302 val: ConstValue::Infer(InferConst::Canonical(b_debruijn, b_bound)),
306 assert_eq!(a_debruijn, b_debruijn);
307 assert_eq!(a_bound, b_bound);
311 // Everything else should just be a perfect match as well,
312 // and we forbid inference variables.
313 _ => match ty::relate::super_relate_consts(self, a, b) {
315 Err(err) => bug!("const mismatch in `AnswerSubstitutor`: {}", err),