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::GenericArg;
  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: GenericArg<'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 param_env(&self) -> ty::ParamEnv<'tcx> {
 178         // FIXME(oli-obk): learn chalk and create param envs
 179         ty::ParamEnv::empty()
 180     }
 181
 182     fn tag(&self) -> &'static str {
 183         "chalk_context::answer_substitutor"
 184     }
 185
 186     fn a_is_expected(&self) -> bool {
 187         true
 188     }
 189
 190     fn relate_with_variance<T: Relate<'tcx>>(
 191         &mut self,
 192         _variance: ty::Variance,
 193         a: &T,
 194         b: &T,
 195     ) -> RelateResult<'tcx, T> {
 196         // We don't care about variance.
 197         self.relate(a, b)
 198     }
 199
 200     fn binders<T: Relate<'tcx>>(
 201         &mut self,
 202         a: &ty::Binder<T>,
 203         b: &ty::Binder<T>,
 204     ) -> RelateResult<'tcx, ty::Binder<T>> {
 205         self.binder_index.shift_in(1);
 206         let result = self.relate(a.skip_binder(), b.skip_binder())?;
 207         self.binder_index.shift_out(1);
 208         Ok(ty::Binder::bind(result))
 209     }
 210
 211     fn tys(&mut self, a: Ty<'tcx>, b: Ty<'tcx>) -> RelateResult<'tcx, Ty<'tcx>> {
 212         let b = self.infcx.shallow_resolve(b);
 213         debug!("AnswerSubstitutor::tys(a = {:?}, b = {:?})", a, b);
 214
 215         if let &ty::Bound(debruijn, bound_ty) = &a.kind {
 216             // Free bound var
 217             if debruijn == self.binder_index {
 218                 self.unify_free_answer_var(bound_ty.var, b.into())?;
 219                 return Ok(b);
 220             }
 221         }
 222
 223         match (&a.kind, &b.kind) {
 224             (&ty::Bound(a_debruijn, a_bound), &ty::Bound(b_debruijn, b_bound)) => {
 225                 assert_eq!(a_debruijn, b_debruijn);
 226                 assert_eq!(a_bound.var, b_bound.var);
 227                 Ok(a)
 228             }
 229
 230             // Those should have been canonicalized away.
 231             (ty::Placeholder(..), _) => {
 232                 bug!("unexpected placeholder ty in `AnswerSubstitutor`: {:?} ", a);
 233             }
 234
 235             // Everything else should just be a perfect match as well,
 236             // and we forbid inference variables.
 237             _ => match ty::relate::super_relate_tys(self, a, b) {
 238                 Ok(ty) => Ok(ty),
 239                 Err(err) => bug!("type mismatch in `AnswerSubstitutor`: {}", err),
 240             }
 241         }
 242     }
 243
 244     fn regions(
 245         &mut self,
 246         a: ty::Region<'tcx>,
 247         b: ty::Region<'tcx>,
 248     ) -> RelateResult<'tcx, ty::Region<'tcx>> {
 249         let b = match b {
 250             &ty::ReVar(vid) => self.infcx
 251                 .borrow_region_constraints()
 252                 .opportunistic_resolve_var(self.infcx.tcx, vid),
 253
 254             other => other,
 255         };
 256
 257         if let &ty::ReLateBound(debruijn, bound) = a {
 258             // Free bound region
 259             if debruijn == self.binder_index {
 260                 self.unify_free_answer_var(bound.assert_bound_var(), b.into())?;
 261                 return Ok(b);
 262             }
 263         }
 264
 265         match (a, b) {
 266             (&ty::ReLateBound(a_debruijn, a_bound), &ty::ReLateBound(b_debruijn, b_bound)) => {
 267                 assert_eq!(a_debruijn, b_debruijn);
 268                 assert_eq!(a_bound.assert_bound_var(), b_bound.assert_bound_var());
 269             }
 270
 271             (ty::ReStatic, ty::ReStatic) |
 272             (ty::ReErased, ty::ReErased) |
 273             (ty::ReEmpty, ty::ReEmpty) => (),
 274
 275             (&ty::ReFree(a_free), &ty::ReFree(b_free)) => {
 276                 assert_eq!(a_free, b_free);
 277             }
 278
 279             _ => bug!("unexpected regions in `AnswerSubstitutor`: {:?}, {:?}", a, b),
 280         }
 281
 282         Ok(a)
 283     }
 284
 285     fn consts(
 286         &mut self,
 287         a: &'tcx ty::Const<'tcx>,
 288         b: &'tcx ty::Const<'tcx>,
 289     ) -> RelateResult<'tcx, &'tcx ty::Const<'tcx>> {
 290         if let ty::Const { val: ConstValue::Bound(debruijn, bound_ct), .. } = a {
 291             if *debruijn == self.binder_index {
 292                 self.unify_free_answer_var(*bound_ct, b.into())?;
 293                 return Ok(b);
 294             }
 295         }
 296
 297         match (a, b) {
 298             (
 299                 ty::Const { val: ConstValue::Bound(a_debruijn, a_bound), .. },
 300                 ty::Const { val: ConstValue::Bound(b_debruijn, b_bound), .. },
 301             ) => {
 302                 assert_eq!(a_debruijn, b_debruijn);
 303                 assert_eq!(a_bound, b_bound);
 304                 Ok(a)
 305             }
 306
 307             // Everything else should just be a perfect match as well,
 308             // and we forbid inference variables.
 309             _ => match ty::relate::super_relate_consts(self, a, b) {
 310                 Ok(ct) => Ok(ct),
 311                 Err(err) => bug!("const mismatch in `AnswerSubstitutor`: {}", err),
 312             }
 313         }
 314     }
 315 }