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};
  20 use rustc::ty::subst::Kind;
  21 use rustc::ty::relate::{Relate, RelateResult, TypeRelation};
  22 use syntax_pos::DUMMY_SP;
  23
  24 use super::{ChalkInferenceContext, ChalkArenas, ChalkExClause, ConstrainedSubst};
  25 use super::unify::*;
  26
  27 impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
  28     for ChalkInferenceContext<'cx, 'gcx, 'tcx>
  29 {
  30     fn resolvent_clause(
  31         &mut self,
  32         environment: &Environment<'tcx>,
  33         goal: &DomainGoal<'tcx>,
  34         subst: &CanonicalVarValues<'tcx>,
  35         clause: &Clause<'tcx>,
  36     ) -> Fallible<Canonical<'gcx, ChalkExClause<'gcx>>> {
  37         use chalk_engine::context::UnificationOps;
  38
  39         debug!("resolvent_clause(goal = {:?}, clause = {:?})", goal, clause);
  40
  41         let result = self.infcx.probe(|_| {
  42             let ProgramClause {
  43                 goal: consequence,
  44                 hypotheses,
  45                 ..
  46             } = match clause {
  47                 Clause::Implies(program_clause) => *program_clause,
  48                 Clause::ForAll(program_clause) => self.infcx.replace_bound_vars_with_fresh_vars(
  49                     DUMMY_SP,
  50                     LateBoundRegionConversionTime::HigherRankedType,
  51                     program_clause
  52                 ).0,
  53             };
  54
  55             let result = unify(
  56                 self.infcx,
  57                 *environment,
  58                 ty::Variance::Invariant,
  59                 goal,
  60                 &consequence
  61             ).map_err(|_| NoSolution)?;
  62
  63             let mut ex_clause = ExClause {
  64                 subst: subst.clone(),
  65                 delayed_literals: vec![],
  66                 constraints: vec![],
  67                 subgoals: vec![],
  68             };
  69
  70             self.into_ex_clause(result, &mut ex_clause);
  71
  72             ex_clause.subgoals.extend(
  73                 hypotheses.iter().map(|g| match g {
  74                     GoalKind::Not(g) => Literal::Negative(environment.with(*g)),
  75                     g => Literal::Positive(environment.with(*g)),
  76                 })
  77             );
  78
  79             // If we have a goal of the form `T: 'a` or `'a: 'b`, then just
  80             // assume it is true (no subgoals) and register it as a constraint
  81             // instead.
  82             match goal {
  83                 DomainGoal::Holds(WhereClause::RegionOutlives(pred)) => {
  84                     assert_eq!(ex_clause.subgoals.len(), 0);
  85                     ex_clause.constraints.push(ty::OutlivesPredicate(pred.0.into(), pred.1));
  86                 }
  87
  88                 DomainGoal::Holds(WhereClause::TypeOutlives(pred)) => {
  89                     assert_eq!(ex_clause.subgoals.len(), 0);
  90                     ex_clause.constraints.push(ty::OutlivesPredicate(pred.0.into(), pred.1));
  91                 }
  92
  93                 _ => (),
  94             };
  95
  96             let canonical_ex_clause = self.canonicalize_ex_clause(&ex_clause);
  97             Ok(canonical_ex_clause)
  98         });
  99
 100         debug!("resolvent_clause: result = {:?}", result);
 101         result
 102     }
 103
 104     fn apply_answer_subst(
 105         &mut self,
 106         ex_clause: ChalkExClause<'tcx>,
 107         selected_goal: &InEnvironment<'tcx, Goal<'tcx>>,
 108         answer_table_goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
 109         canonical_answer_subst: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
 110     ) -> Fallible<ChalkExClause<'tcx>> {
 111         debug!(
 112             "apply_answer_subst(ex_clause = {:?}, selected_goal = {:?})",
 113             self.infcx.resolve_type_vars_if_possible(&ex_clause),
 114             self.infcx.resolve_type_vars_if_possible(selected_goal)
 115         );
 116
 117         let (answer_subst, _) = self.infcx.instantiate_canonical_with_fresh_inference_vars(
 118             DUMMY_SP,
 119             canonical_answer_subst
 120         );
 121
 122         let mut substitutor = AnswerSubstitutor {
 123             infcx: self.infcx,
 124             environment: selected_goal.environment,
 125             answer_subst: answer_subst.subst,
 126             binder_index: ty::INNERMOST,
 127             ex_clause,
 128         };
 129
 130         substitutor.relate(&answer_table_goal.value, &selected_goal)
 131             .map_err(|_| NoSolution)?;
 132
 133         let mut ex_clause = substitutor.ex_clause;
 134         ex_clause.constraints.extend(answer_subst.constraints);
 135
 136         debug!("apply_answer_subst: ex_clause = {:?}", ex_clause);
 137         Ok(ex_clause)
 138     }
 139 }
 140
 141 struct AnswerSubstitutor<'cx, 'gcx: 'tcx, 'tcx: 'cx> {
 142     infcx: &'cx InferCtxt<'cx, 'gcx, 'tcx>,
 143     environment: Environment<'tcx>,
 144     answer_subst: CanonicalVarValues<'tcx>,
 145     binder_index: ty::DebruijnIndex,
 146     ex_clause: ChalkExClause<'tcx>,
 147 }
 148
 149 impl AnswerSubstitutor<'cx, 'gcx, 'tcx> {
 150     fn unify_free_answer_var(
 151         &mut self,
 152         answer_var: ty::BoundVar,
 153         pending: Kind<'tcx>
 154     ) -> RelateResult<'tcx, ()> {
 155         let answer_param = &self.answer_subst.var_values[answer_var];
 156         let pending = &ty::fold::shift_out_vars(
 157             self.infcx.tcx,
 158             &pending,
 159             self.binder_index.as_u32()
 160         );
 161
 162         super::into_ex_clause(
 163             unify(self.infcx, self.environment, ty::Variance::Invariant, answer_param, pending)?,
 164             &mut self.ex_clause
 165         );
 166
 167         Ok(())
 168     }
 169 }
 170
 171 impl TypeRelation<'cx, 'gcx, 'tcx> for AnswerSubstitutor<'cx, 'gcx, 'tcx> {
 172     fn tcx(&self) -> TyCtxt<'cx, 'gcx, 'tcx> {
 173         self.infcx.tcx
 174     }
 175
 176     fn tag(&self) -> &'static str {
 177         "chalk_context::answer_substitutor"
 178     }
 179
 180     fn a_is_expected(&self) -> bool {
 181         true
 182     }
 183
 184     fn relate_with_variance<T: Relate<'tcx>>(
 185         &mut self,
 186         _variance: ty::Variance,
 187         a: &T,
 188         b: &T,
 189     ) -> RelateResult<'tcx, T> {
 190         // We don't care about variance.
 191         self.relate(a, b)
 192     }
 193
 194     fn binders<T: Relate<'tcx>>(
 195         &mut self,
 196         a: &ty::Binder<T>,
 197         b: &ty::Binder<T>,
 198     ) -> RelateResult<'tcx, ty::Binder<T>> {
 199         self.binder_index.shift_in(1);
 200         let result = self.relate(a.skip_binder(), b.skip_binder())?;
 201         self.binder_index.shift_out(1);
 202         Ok(ty::Binder::bind(result))
 203     }
 204
 205     fn tys(&mut self, a: Ty<'tcx>, b: Ty<'tcx>) -> RelateResult<'tcx, Ty<'tcx>> {
 206         let b = self.infcx.shallow_resolve(b);
 207         debug!("AnswerSubstitutor::tys(a = {:?}, b = {:?})", a, b);
 208
 209         if let &ty::Bound(debruijn, bound_ty) = &a.sty {
 210             // Free bound var
 211             if debruijn == self.binder_index {
 212                 self.unify_free_answer_var(bound_ty.var, b.into())?;
 213                 return Ok(b);
 214             }
 215         }
 216
 217         match (&a.sty, &b.sty) {
 218             (&ty::Bound(a_debruijn, a_bound), &ty::Bound(b_debruijn, b_bound)) => {
 219                 assert_eq!(a_debruijn, b_debruijn);
 220                 assert_eq!(a_bound.var, b_bound.var);
 221                 Ok(a)
 222             }
 223
 224             // Those should have been canonicalized away.
 225             (ty::Placeholder(..), _) => {
 226                 bug!("unexpected placeholder ty in `AnswerSubstitutor`: {:?} ", a);
 227             }
 228
 229             // Everything else should just be a perfect match as well,
 230             // and we forbid inference variables.
 231             _ => match ty::relate::super_relate_tys(self, a, b) {
 232                 Ok(ty) => Ok(ty),
 233                 Err(err) => bug!("type mismatch in `AnswerSubstitutor`: {}", err),
 234             }
 235         }
 236     }
 237
 238     fn regions(
 239         &mut self,
 240         a: ty::Region<'tcx>,
 241         b: ty::Region<'tcx>,
 242     ) -> RelateResult<'tcx, ty::Region<'tcx>> {
 243         let b = match b {
 244             &ty::ReVar(vid) => self.infcx
 245                 .borrow_region_constraints()
 246                 .opportunistic_resolve_var(self.infcx.tcx, vid),
 247
 248             other => other,
 249         };
 250
 251         if let &ty::ReLateBound(debruijn, bound) = a {
 252             // Free bound region
 253             if debruijn == self.binder_index {
 254                 self.unify_free_answer_var(bound.assert_bound_var(), b.into())?;
 255                 return Ok(b);
 256             }
 257         }
 258
 259         match (a, b) {
 260             (&ty::ReLateBound(a_debruijn, a_bound), &ty::ReLateBound(b_debruijn, b_bound)) => {
 261                 assert_eq!(a_debruijn, b_debruijn);
 262                 assert_eq!(a_bound.assert_bound_var(), b_bound.assert_bound_var());
 263             }
 264
 265             (ty::ReStatic, ty::ReStatic) |
 266             (ty::ReErased, ty::ReErased) |
 267             (ty::ReEmpty, ty::ReEmpty) => (),
 268
 269             (&ty::ReFree(a_free), &ty::ReFree(b_free)) => {
 270                 assert_eq!(a_free, b_free);
 271             }
 272
 273             _ => bug!("unexpected regions in `AnswerSubstitutor`: {:?}, {:?}", a, b),
 274         }
 275
 276         Ok(a)
 277     }
 278 }