src/librustc_traits/chalk_context/resolvent_ops.rs

   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};
   5 use rustc::traits::{
   6     Clause, DomainGoal, Environment, Goal, GoalKind, InEnvironment, ProgramClause, WhereClause,
   7 };
   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;
  12
  13 use super::unify::*;
  14 use super::{ChalkArenas, ChalkExClause, ChalkInferenceContext, ConstrainedSubst};
  15
  16 impl context::ResolventOps<ChalkArenas<'tcx>, ChalkArenas<'tcx>>
  17     for ChalkInferenceContext<'cx, 'tcx>
  18 {
  19     fn resolvent_clause(
  20         &mut self,
  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;
  27
  28         debug!("resolvent_clause(goal = {:?}, clause = {:?})", goal, clause);
  29
  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) => {
  34                     self.infcx
  35                         .replace_bound_vars_with_fresh_vars(
  36                             DUMMY_SP,
  37                             LateBoundRegionConversionTime::HigherRankedType,
  38                             program_clause,
  39                         )
  40                         .0
  41                 }
  42             };
  43
  44             let result =
  45                 unify(self.infcx, *environment, ty::Variance::Invariant, goal, &consequence)
  46                     .map_err(|_| NoSolution)?;
  47
  48             let mut ex_clause = ExClause {
  49                 subst: subst.clone(),
  50                 delayed_literals: vec![],
  51                 constraints: vec![],
  52                 subgoals: vec![],
  53             };
  54
  55             self.into_ex_clause(result, &mut ex_clause);
  56
  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)),
  60             }));
  61
  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
  64             // instead.
  65             match goal {
  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));
  69                 }
  70
  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));
  74                 }
  75
  76                 _ => (),
  77             };
  78
  79             let canonical_ex_clause = self.canonicalize_ex_clause(&ex_clause);
  80             Ok(canonical_ex_clause)
  81         });
  82
  83         debug!("resolvent_clause: result = {:?}", result);
  84         result
  85     }
  86
  87     fn apply_answer_subst(
  88         &mut self,
  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>> {
  94         debug!(
  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)
  98         );
  99
 100         let (answer_subst, _) = self
 101             .infcx
 102             .instantiate_canonical_with_fresh_inference_vars(DUMMY_SP, canonical_answer_subst);
 103
 104         let mut substitutor = AnswerSubstitutor {
 105             infcx: self.infcx,
 106             environment: selected_goal.environment,
 107             answer_subst: answer_subst.subst,
 108             binder_index: ty::INNERMOST,
 109             ex_clause,
 110         };
 111
 112         substitutor.relate(&answer_table_goal.value, &selected_goal).map_err(|_| NoSolution)?;
 113
 114         let mut ex_clause = substitutor.ex_clause;
 115         ex_clause.constraints.extend(answer_subst.constraints);
 116
 117         debug!("apply_answer_subst: ex_clause = {:?}", ex_clause);
 118         Ok(ex_clause)
 119     }
 120 }
 121
 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>,
 128 }
 129
 130 impl AnswerSubstitutor<'cx, 'tcx> {
 131     fn unify_free_answer_var(
 132         &mut self,
 133         answer_var: ty::BoundVar,
 134         pending: GenericArg<'tcx>,
 135     ) -> RelateResult<'tcx, ()> {
 136         let answer_param = &self.answer_subst.var_values[answer_var];
 137         let pending =
 138             &ty::fold::shift_out_vars(self.infcx.tcx, &pending, self.binder_index.as_u32());
 139
 140         super::into_ex_clause(
 141             unify(self.infcx, self.environment, ty::Variance::Invariant, answer_param, pending)?,
 142             &mut self.ex_clause,
 143         );
 144
 145         Ok(())
 146     }
 147 }
 148
 149 impl TypeRelation<'tcx> for AnswerSubstitutor<'cx, 'tcx> {
 150     fn tcx(&self) -> TyCtxt<'tcx> {
 151         self.infcx.tcx
 152     }
 153
 154     fn param_env(&self) -> ty::ParamEnv<'tcx> {
 155         // FIXME(oli-obk): learn chalk and create param envs
 156         ty::ParamEnv::empty()
 157     }
 158
 159     fn tag(&self) -> &'static str {
 160         "chalk_context::answer_substitutor"
 161     }
 162
 163     fn a_is_expected(&self) -> bool {
 164         true
 165     }
 166
 167     fn relate_with_variance<T: Relate<'tcx>>(
 168         &mut self,
 169         _variance: ty::Variance,
 170         a: &T,
 171         b: &T,
 172     ) -> RelateResult<'tcx, T> {
 173         // We don't care about variance.
 174         self.relate(a, b)
 175     }
 176
 177     fn binders<T: Relate<'tcx>>(
 178         &mut self,
 179         a: &ty::Binder<T>,
 180         b: &ty::Binder<T>,
 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))
 186     }
 187
 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);
 191
 192         if let &ty::Bound(debruijn, bound_ty) = &a.kind {
 193             // Free bound var
 194             if debruijn == self.binder_index {
 195                 self.unify_free_answer_var(bound_ty.var, b.into())?;
 196                 return Ok(b);
 197             }
 198         }
 199
 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);
 204                 Ok(a)
 205             }
 206
 207             // Those should have been canonicalized away.
 208             (ty::Placeholder(..), _) => {
 209                 bug!("unexpected placeholder ty in `AnswerSubstitutor`: {:?} ", a);
 210             }
 211
 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) {
 215                 Ok(ty) => Ok(ty),
 216                 Err(err) => bug!("type mismatch in `AnswerSubstitutor`: {}", err),
 217             },
 218         }
 219     }
 220
 221     fn regions(
 222         &mut self,
 223         a: ty::Region<'tcx>,
 224         b: ty::Region<'tcx>,
 225     ) -> RelateResult<'tcx, ty::Region<'tcx>> {
 226         let b = match b {
 227             &ty::ReVar(vid) => self
 228                 .infcx
 229                 .borrow_region_constraints()
 230                 .opportunistic_resolve_var(self.infcx.tcx, vid),
 231
 232             other => other,
 233         };
 234
 235         if let &ty::ReLateBound(debruijn, bound) = a {
 236             // Free bound region
 237             if debruijn == self.binder_index {
 238                 self.unify_free_answer_var(bound.assert_bound_var(), b.into())?;
 239                 return Ok(b);
 240             }
 241         }
 242
 243         match (a, b) {
 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());
 247             }
 248
 249             (ty::ReStatic, ty::ReStatic)
 250             | (ty::ReErased, ty::ReErased)
 251             | (ty::ReEmpty, ty::ReEmpty) => (),
 252
 253             (&ty::ReFree(a_free), &ty::ReFree(b_free)) => {
 254                 assert_eq!(a_free, b_free);
 255             }
 256
 257             _ => bug!("unexpected regions in `AnswerSubstitutor`: {:?}, {:?}", a, b),
 258         }
 259
 260         Ok(a)
 261     }
 262
 263     fn consts(
 264         &mut self,
 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())?;
 271                 return Ok(b);
 272             }
 273         }
 274
 275         match (a, b) {
 276             (
 277                 ty::Const { val: ty::ConstKind::Bound(a_debruijn, a_bound), .. },
 278                 ty::Const { val: ty::ConstKind::Bound(b_debruijn, b_bound), .. },
 279             ) => {
 280                 assert_eq!(a_debruijn, b_debruijn);
 281                 assert_eq!(a_bound, b_bound);
 282                 Ok(a)
 283             }
 284
 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) {
 288                 Ok(ct) => Ok(ct),
 289                 Err(err) => bug!("const mismatch in `AnswerSubstitutor`: {}", err),
 290             },
 291         }
 292     }
 293 }