src/librustc_traits/chalk_context/resolvent_ops.rs

   1 use chalk_engine::fallible::{Fallible, NoSolution};
   2 use chalk_engine::{
   3     context,
   4     Literal,
   5     ExClause
   6 };
   7 use rustc::infer::{InferCtxt, LateBoundRegionConversionTime};
   8 use rustc::infer::canonical::{Canonical, CanonicalVarValues};
   9 use rustc::traits::{
  10     DomainGoal,
  11     WhereClause,
  12     Goal,
  13     GoalKind,
  14     Clause,
  15     ProgramClause,
  16     Environment,
  17     InEnvironment,
  18 };
  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;
  24
  25 use super::{ChalkInferenceContext, ChalkArenas, ChalkExClause, ConstrainedSubst};
  26 use super::unify::*;
  27
  28 impl context::ResolventOps<ChalkArenas<'tcx>, ChalkArenas<'tcx>>
  29     for ChalkInferenceContext<'cx, 'tcx>
  30 {
  31     fn resolvent_clause(
  32         &mut self,
  33         environment: &Environment<'tcx>,
  34         goal: &DomainGoal<'tcx>,
  35         subst: &CanonicalVarValues<'tcx>,
  36         clause: &Clause<'tcx>,
  37     ) -> Fallible<Canonical<'tcx, ChalkExClause<'tcx>>> {
  38         use chalk_engine::context::UnificationOps;
  39
  40         debug!("resolvent_clause(goal = {:?}, clause = {:?})", goal, clause);
  41
  42         let result = self.infcx.probe(|_| {
  43             let ProgramClause {
  44                 goal: consequence,
  45                 hypotheses,
  46                 ..
  47             } = match clause {
  48                 Clause::Implies(program_clause) => *program_clause,
  49                 Clause::ForAll(program_clause) => self.infcx.replace_bound_vars_with_fresh_vars(
  50                     DUMMY_SP,
  51                     LateBoundRegionConversionTime::HigherRankedType,
  52                     program_clause
  53                 ).0,
  54             };
  55
  56             let result = unify(
  57                 self.infcx,
  58                 *environment,
  59                 ty::Variance::Invariant,
  60                 goal,
  61                 &consequence
  62             ).map_err(|_| NoSolution)?;
  63
  64             let mut ex_clause = ExClause {
  65                 subst: subst.clone(),
  66                 delayed_literals: vec![],
  67                 constraints: vec![],
  68                 subgoals: vec![],
  69             };
  70
  71             self.into_ex_clause(result, &mut ex_clause);
  72
  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)),
  77                 })
  78             );
  79
  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
  82             // instead.
  83             match goal {
  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));
  87                 }
  88
  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));
  92                 }
  93
  94                 _ => (),
  95             };
  96
  97             let canonical_ex_clause = self.canonicalize_ex_clause(&ex_clause);
  98             Ok(canonical_ex_clause)
  99         });
 100
 101         debug!("resolvent_clause: result = {:?}", result);
 102         result
 103     }
 104
 105     fn apply_answer_subst(
 106         &mut self,
 107         ex_clause: ChalkExClause<'tcx>,
 108         selected_goal: &InEnvironment<'tcx, Goal<'tcx>>,
 109         answer_table_goal: &Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>>,
 110         canonical_answer_subst: &Canonical<'tcx, ConstrainedSubst<'tcx>>,
 111     ) -> Fallible<ChalkExClause<'tcx>> {
 112         debug!(
 113             "apply_answer_subst(ex_clause = {:?}, selected_goal = {:?})",
 114             self.infcx.resolve_vars_if_possible(&ex_clause),
 115             self.infcx.resolve_vars_if_possible(selected_goal)
 116         );
 117
 118         let (answer_subst, _) = self.infcx.instantiate_canonical_with_fresh_inference_vars(
 119             DUMMY_SP,
 120             canonical_answer_subst
 121         );
 122
 123         let mut substitutor = AnswerSubstitutor {
 124             infcx: self.infcx,
 125             environment: selected_goal.environment,
 126             answer_subst: answer_subst.subst,
 127             binder_index: ty::INNERMOST,
 128             ex_clause,
 129         };
 130
 131         substitutor.relate(&answer_table_goal.value, &selected_goal)
 132             .map_err(|_| NoSolution)?;
 133
 134         let mut ex_clause = substitutor.ex_clause;
 135         ex_clause.constraints.extend(answer_subst.constraints);
 136
 137         debug!("apply_answer_subst: ex_clause = {:?}", ex_clause);
 138         Ok(ex_clause)
 139     }
 140 }
 141
 142 struct AnswerSubstitutor<'cx, 'tcx> {
 143     infcx: &'cx InferCtxt<'cx, 'tcx>,
 144     environment: Environment<'tcx>,
 145     answer_subst: CanonicalVarValues<'tcx>,
 146     binder_index: ty::DebruijnIndex,
 147     ex_clause: ChalkExClause<'tcx>,
 148 }
 149
 150 impl AnswerSubstitutor<'cx, 'tcx> {
 151     fn unify_free_answer_var(
 152         &mut self,
 153         answer_var: ty::BoundVar,
 154         pending: Kind<'tcx>
 155     ) -> RelateResult<'tcx, ()> {
 156         let answer_param = &self.answer_subst.var_values[answer_var];
 157         let pending = &ty::fold::shift_out_vars(
 158             self.infcx.tcx,
 159             &pending,
 160             self.binder_index.as_u32()
 161         );
 162
 163         super::into_ex_clause(
 164             unify(self.infcx, self.environment, ty::Variance::Invariant, answer_param, pending)?,
 165             &mut self.ex_clause
 166         );
 167
 168         Ok(())
 169     }
 170 }
 171
 172 impl TypeRelation<'tcx> for AnswerSubstitutor<'cx, 'tcx> {
 173     fn tcx(&self) -> TyCtxt<'tcx> {
 174         self.infcx.tcx
 175     }
 176
 177     fn tag(&self) -> &'static str {
 178         "chalk_context::answer_substitutor"
 179     }
 180
 181     fn a_is_expected(&self) -> bool {
 182         true
 183     }
 184
 185     fn relate_with_variance<T: Relate<'tcx>>(
 186         &mut self,
 187         _variance: ty::Variance,
 188         a: &T,
 189         b: &T,
 190     ) -> RelateResult<'tcx, T> {
 191         // We don't care about variance.
 192         self.relate(a, b)
 193     }
 194
 195     fn binders<T: Relate<'tcx>>(
 196         &mut self,
 197         a: &ty::Binder<T>,
 198         b: &ty::Binder<T>,
 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))
 204     }
 205
 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);
 209
 210         if let &ty::Bound(debruijn, bound_ty) = &a.sty {
 211             // Free bound var
 212             if debruijn == self.binder_index {
 213                 self.unify_free_answer_var(bound_ty.var, b.into())?;
 214                 return Ok(b);
 215             }
 216         }
 217
 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);
 222                 Ok(a)
 223             }
 224
 225             // Those should have been canonicalized away.
 226             (ty::Placeholder(..), _) => {
 227                 bug!("unexpected placeholder ty in `AnswerSubstitutor`: {:?} ", a);
 228             }
 229
 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) {
 233                 Ok(ty) => Ok(ty),
 234                 Err(err) => bug!("type mismatch in `AnswerSubstitutor`: {}", err),
 235             }
 236         }
 237     }
 238
 239     fn regions(
 240         &mut self,
 241         a: ty::Region<'tcx>,
 242         b: ty::Region<'tcx>,
 243     ) -> RelateResult<'tcx, ty::Region<'tcx>> {
 244         let b = match b {
 245             &ty::ReVar(vid) => self.infcx
 246                 .borrow_region_constraints()
 247                 .opportunistic_resolve_var(self.infcx.tcx, vid),
 248
 249             other => other,
 250         };
 251
 252         if let &ty::ReLateBound(debruijn, bound) = a {
 253             // Free bound region
 254             if debruijn == self.binder_index {
 255                 self.unify_free_answer_var(bound.assert_bound_var(), b.into())?;
 256                 return Ok(b);
 257             }
 258         }
 259
 260         match (a, b) {
 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());
 264             }
 265
 266             (ty::ReStatic, ty::ReStatic) |
 267             (ty::ReErased, ty::ReErased) |
 268             (ty::ReEmpty, ty::ReEmpty) => (),
 269
 270             (&ty::ReFree(a_free), &ty::ReFree(b_free)) => {
 271                 assert_eq!(a_free, b_free);
 272             }
 273
 274             _ => bug!("unexpected regions in `AnswerSubstitutor`: {:?}, {:?}", a, b),
 275         }
 276
 277         Ok(a)
 278     }
 279
 280     fn consts(
 281         &mut self,
 282         a: &'tcx ty::Const<'tcx>,
 283         b: &'tcx ty::Const<'tcx>,
 284     ) -> RelateResult<'tcx, &'tcx ty::Const<'tcx>> {
 285         if let ty::Const {
 286             val: ConstValue::Infer(InferConst::Canonical(debruijn, bound_ct)),
 287             ..
 288         } = a {
 289             if *debruijn == self.binder_index {
 290                 self.unify_free_answer_var(*bound_ct, b.into())?;
 291                 return Ok(b);
 292             }
 293         }
 294
 295         match (a, b) {
 296             (
 297                 ty::Const {
 298                     val: ConstValue::Infer(InferConst::Canonical(a_debruijn, a_bound)),
 299                     ..
 300                 },
 301                 ty::Const {
 302                     val: ConstValue::Infer(InferConst::Canonical(b_debruijn, b_bound)),
 303                     ..
 304                 },
 305             ) => {
 306                 assert_eq!(a_debruijn, b_debruijn);
 307                 assert_eq!(a_bound, b_bound);
 308                 Ok(a)
 309             }
 310
 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) {
 314                 Ok(ct) => Ok(ct),
 315                 Err(err) => bug!("const mismatch in `AnswerSubstitutor`: {}", err),
 316             }
 317         }
 318     }
 319 }