1 use chalk_engine::fallible::{Fallible, NoSolution};
2 use chalk_engine::{context, ExClause, Literal};
3 use rustc::infer::canonical::{Canonical, CanonicalVarValues};
4 use rustc::infer::{InferCtxt, LateBoundRegionConversionTime};
6 Clause, DomainGoal, Environment, Goal, GoalKind, InEnvironment, ProgramClause, WhereClause,
8 use rustc::ty::relate::{Relate, RelateResult, TypeRelation};
9 use rustc::ty::subst::GenericArg;
10 use rustc::ty::{self, Ty, TyCtxt};
11 use rustc_span::DUMMY_SP;
14 use super::{ChalkArenas, ChalkExClause, ChalkInferenceContext, ConstrainedSubst};
16 impl context::ResolventOps<ChalkArenas<'tcx>, ChalkArenas<'tcx>>
17 for ChalkInferenceContext<'cx, 'tcx>
21 environment: &Environment<'tcx>,
22 goal: &DomainGoal<'tcx>,
23 subst: &CanonicalVarValues<'tcx>,
24 clause: &Clause<'tcx>,
25 ) -> Fallible<Canonical<'tcx, ChalkExClause<'tcx>>> {
26 use chalk_engine::context::UnificationOps;
28 debug!("resolvent_clause(goal = {:?}, clause = {:?})", goal, clause);
30 let result = self.infcx.probe(|_| {
31 let ProgramClause { goal: consequence, hypotheses, .. } = match clause {
32 Clause::Implies(program_clause) => *program_clause,
33 Clause::ForAll(program_clause) => {
35 .replace_bound_vars_with_fresh_vars(
37 LateBoundRegionConversionTime::HigherRankedType,
45 unify(self.infcx, *environment, ty::Variance::Invariant, goal, &consequence)
46 .map_err(|_| NoSolution)?;
48 let mut ex_clause = ExClause {
50 delayed_literals: vec![],
55 self.into_ex_clause(result, &mut ex_clause);
57 ex_clause.subgoals.extend(hypotheses.iter().map(|g| match g {
58 GoalKind::Not(g) => Literal::Negative(environment.with(*g)),
59 g => Literal::Positive(environment.with(*g)),
62 // If we have a goal of the form `T: 'a` or `'a: 'b`, then just
63 // assume it is true (no subgoals) and register it as a constraint
66 DomainGoal::Holds(WhereClause::RegionOutlives(pred)) => {
67 assert_eq!(ex_clause.subgoals.len(), 0);
68 ex_clause.constraints.push(ty::OutlivesPredicate(pred.0.into(), pred.1));
71 DomainGoal::Holds(WhereClause::TypeOutlives(pred)) => {
72 assert_eq!(ex_clause.subgoals.len(), 0);
73 ex_clause.constraints.push(ty::OutlivesPredicate(pred.0.into(), pred.1));
79 let canonical_ex_clause = self.canonicalize_ex_clause(&ex_clause);
80 Ok(canonical_ex_clause)
83 debug!("resolvent_clause: result = {:?}", result);
87 fn apply_answer_subst(
89 ex_clause: ChalkExClause<'tcx>,
90 selected_goal: &InEnvironment<'tcx, Goal<'tcx>>,
91 answer_table_goal: &Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>>,
92 canonical_answer_subst: &Canonical<'tcx, ConstrainedSubst<'tcx>>,
93 ) -> Fallible<ChalkExClause<'tcx>> {
95 "apply_answer_subst(ex_clause = {:?}, selected_goal = {:?})",
96 self.infcx.resolve_vars_if_possible(&ex_clause),
97 self.infcx.resolve_vars_if_possible(selected_goal)
100 let (answer_subst, _) = self
102 .instantiate_canonical_with_fresh_inference_vars(DUMMY_SP, canonical_answer_subst);
104 let mut substitutor = AnswerSubstitutor {
106 environment: selected_goal.environment,
107 answer_subst: answer_subst.subst,
108 binder_index: ty::INNERMOST,
112 substitutor.relate(&answer_table_goal.value, &selected_goal).map_err(|_| NoSolution)?;
114 let mut ex_clause = substitutor.ex_clause;
115 ex_clause.constraints.extend(answer_subst.constraints);
117 debug!("apply_answer_subst: ex_clause = {:?}", ex_clause);
122 struct AnswerSubstitutor<'cx, 'tcx> {
123 infcx: &'cx InferCtxt<'cx, 'tcx>,
124 environment: Environment<'tcx>,
125 answer_subst: CanonicalVarValues<'tcx>,
126 binder_index: ty::DebruijnIndex,
127 ex_clause: ChalkExClause<'tcx>,
130 impl AnswerSubstitutor<'cx, 'tcx> {
131 fn unify_free_answer_var(
133 answer_var: ty::BoundVar,
134 pending: GenericArg<'tcx>,
135 ) -> RelateResult<'tcx, ()> {
136 let answer_param = &self.answer_subst.var_values[answer_var];
138 &ty::fold::shift_out_vars(self.infcx.tcx, &pending, self.binder_index.as_u32());
140 super::into_ex_clause(
141 unify(self.infcx, self.environment, ty::Variance::Invariant, answer_param, pending)?,
149 impl TypeRelation<'tcx> for AnswerSubstitutor<'cx, 'tcx> {
150 fn tcx(&self) -> TyCtxt<'tcx> {
154 fn param_env(&self) -> ty::ParamEnv<'tcx> {
155 // FIXME(oli-obk): learn chalk and create param envs
156 ty::ParamEnv::empty()
159 fn tag(&self) -> &'static str {
160 "chalk_context::answer_substitutor"
163 fn a_is_expected(&self) -> bool {
167 fn relate_with_variance<T: Relate<'tcx>>(
169 _variance: ty::Variance,
172 ) -> RelateResult<'tcx, T> {
173 // We don't care about variance.
177 fn binders<T: Relate<'tcx>>(
181 ) -> RelateResult<'tcx, ty::Binder<T>> {
182 self.binder_index.shift_in(1);
183 let result = self.relate(a.skip_binder(), b.skip_binder())?;
184 self.binder_index.shift_out(1);
185 Ok(ty::Binder::bind(result))
188 fn tys(&mut self, a: Ty<'tcx>, b: Ty<'tcx>) -> RelateResult<'tcx, Ty<'tcx>> {
189 let b = self.infcx.shallow_resolve(b);
190 debug!("AnswerSubstitutor::tys(a = {:?}, b = {:?})", a, b);
192 if let &ty::Bound(debruijn, bound_ty) = &a.kind {
194 if debruijn == self.binder_index {
195 self.unify_free_answer_var(bound_ty.var, b.into())?;
200 match (&a.kind, &b.kind) {
201 (&ty::Bound(a_debruijn, a_bound), &ty::Bound(b_debruijn, b_bound)) => {
202 assert_eq!(a_debruijn, b_debruijn);
203 assert_eq!(a_bound.var, b_bound.var);
207 // Those should have been canonicalized away.
208 (ty::Placeholder(..), _) => {
209 bug!("unexpected placeholder ty in `AnswerSubstitutor`: {:?} ", a);
212 // Everything else should just be a perfect match as well,
213 // and we forbid inference variables.
214 _ => match ty::relate::super_relate_tys(self, a, b) {
216 Err(err) => bug!("type mismatch in `AnswerSubstitutor`: {}", err),
225 ) -> RelateResult<'tcx, ty::Region<'tcx>> {
227 &ty::ReVar(vid) => self
229 .borrow_region_constraints()
230 .opportunistic_resolve_var(self.infcx.tcx, vid),
235 if let &ty::ReLateBound(debruijn, bound) = a {
237 if debruijn == self.binder_index {
238 self.unify_free_answer_var(bound.assert_bound_var(), b.into())?;
244 (&ty::ReLateBound(a_debruijn, a_bound), &ty::ReLateBound(b_debruijn, b_bound)) => {
245 assert_eq!(a_debruijn, b_debruijn);
246 assert_eq!(a_bound.assert_bound_var(), b_bound.assert_bound_var());
249 (ty::ReStatic, ty::ReStatic)
250 | (ty::ReErased, ty::ReErased)
251 | (ty::ReEmpty, ty::ReEmpty) => (),
253 (&ty::ReFree(a_free), &ty::ReFree(b_free)) => {
254 assert_eq!(a_free, b_free);
257 _ => bug!("unexpected regions in `AnswerSubstitutor`: {:?}, {:?}", a, b),
265 a: &'tcx ty::Const<'tcx>,
266 b: &'tcx ty::Const<'tcx>,
267 ) -> RelateResult<'tcx, &'tcx ty::Const<'tcx>> {
268 if let ty::Const { val: ty::ConstKind::Bound(debruijn, bound_ct), .. } = a {
269 if *debruijn == self.binder_index {
270 self.unify_free_answer_var(*bound_ct, b.into())?;
277 ty::Const { val: ty::ConstKind::Bound(a_debruijn, a_bound), .. },
278 ty::Const { val: ty::ConstKind::Bound(b_debruijn, b_bound), .. },
280 assert_eq!(a_debruijn, b_debruijn);
281 assert_eq!(a_bound, b_bound);
285 // Everything else should just be a perfect match as well,
286 // and we forbid inference variables.
287 _ => match ty::relate::super_relate_consts(self, a, b) {
289 Err(err) => bug!("const mismatch in `AnswerSubstitutor`: {}", err),