src/librustc_traits/chalk_context/mod.rs

   1 mod program_clauses;
   2 mod resolvent_ops;
   3 mod unify;
   4
   5 use chalk_engine::fallible::Fallible;
   6 use chalk_engine::{
   7     context,
   8     hh::HhGoal,
   9     DelayedLiteral,
  10     Literal,
  11     ExClause,
  12 };
  13 use chalk_engine::forest::Forest;
  14 use rustc::infer::{InferCtxt, LateBoundRegionConversionTime};
  15 use rustc::infer::canonical::{
  16     Canonical,
  17     CanonicalVarValues,
  18     OriginalQueryValues,
  19     QueryResponse,
  20     Certainty,
  21 };
  22 use rustc::traits::{
  23     self,
  24     DomainGoal,
  25     ExClauseFold,
  26     ChalkContextLift,
  27     Goal,
  28     GoalKind,
  29     Clause,
  30     QuantifierKind,
  31     Environment,
  32     InEnvironment,
  33     ChalkCanonicalGoal,
  34 };
  35 use rustc::ty::{self, TyCtxt, InferConst};
  36 use rustc::ty::fold::{TypeFoldable, TypeFolder, TypeVisitor};
  37 use rustc::ty::query::Providers;
  38 use rustc::ty::subst::{Kind, UnpackedKind};
  39 use rustc::mir::interpret::ConstValue;
  40 use syntax_pos::DUMMY_SP;
  41
  42 use std::fmt::{self, Debug};
  43 use std::marker::PhantomData;
  44
  45 use self::unify::*;
  46
  47 #[derive(Copy, Clone, Debug)]
  48 crate struct ChalkArenas<'gcx> {
  49     _phantom: PhantomData<&'gcx ()>,
  50 }
  51
  52 #[derive(Copy, Clone)]
  53 crate struct ChalkContext<'cx, 'gcx: 'cx> {
  54     _arenas: ChalkArenas<'gcx>,
  55     tcx: TyCtxt<'cx, 'gcx, 'gcx>,
  56 }
  57
  58 #[derive(Copy, Clone)]
  59 crate struct ChalkInferenceContext<'cx, 'gcx: 'tcx, 'tcx: 'cx> {
  60     infcx: &'cx InferCtxt<'cx, 'gcx, 'tcx>,
  61 }
  62
  63 #[derive(Copy, Clone, Debug)]
  64 crate struct UniverseMap;
  65
  66 crate type RegionConstraint<'tcx> = ty::OutlivesPredicate<Kind<'tcx>, ty::Region<'tcx>>;
  67
  68 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
  69 crate struct ConstrainedSubst<'tcx> {
  70     subst: CanonicalVarValues<'tcx>,
  71     constraints: Vec<RegionConstraint<'tcx>>,
  72 }
  73
  74 BraceStructTypeFoldableImpl! {
  75     impl<'tcx> TypeFoldable<'tcx> for ConstrainedSubst<'tcx> {
  76         subst, constraints
  77     }
  78 }
  79
  80 impl context::Context for ChalkArenas<'tcx> {
  81     type CanonicalExClause = Canonical<'tcx, ChalkExClause<'tcx>>;
  82
  83     type CanonicalGoalInEnvironment = Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>>;
  84
  85     // u-canonicalization not yet implemented
  86     type UCanonicalGoalInEnvironment = Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>>;
  87
  88     type CanonicalConstrainedSubst = Canonical<'tcx, ConstrainedSubst<'tcx>>;
  89
  90     // u-canonicalization not yet implemented
  91     type UniverseMap = UniverseMap;
  92
  93     type Solution = Canonical<'tcx, QueryResponse<'tcx, ()>>;
  94
  95     type InferenceNormalizedSubst = CanonicalVarValues<'tcx>;
  96
  97     type GoalInEnvironment = InEnvironment<'tcx, Goal<'tcx>>;
  98
  99     type RegionConstraint = RegionConstraint<'tcx>;
 100
 101     type Substitution = CanonicalVarValues<'tcx>;
 102
 103     type Environment = Environment<'tcx>;
 104
 105     type Goal = Goal<'tcx>;
 106
 107     type DomainGoal = DomainGoal<'tcx>;
 108
 109     type BindersGoal = ty::Binder<Goal<'tcx>>;
 110
 111     type Parameter = Kind<'tcx>;
 112
 113     type ProgramClause = Clause<'tcx>;
 114
 115     type ProgramClauses = Vec<Clause<'tcx>>;
 116
 117     type UnificationResult = UnificationResult<'tcx>;
 118
 119     type Variance = ty::Variance;
 120
 121     fn goal_in_environment(
 122         env: &Environment<'tcx>,
 123         goal: Goal<'tcx>,
 124     ) -> InEnvironment<'tcx, Goal<'tcx>> {
 125         env.with(goal)
 126     }
 127 }
 128
 129 impl context::AggregateOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
 130     fn make_solution(
 131         &self,
 132         root_goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
 133         mut simplified_answers: impl context::AnswerStream<ChalkArenas<'gcx>>,
 134     ) -> Option<Canonical<'gcx, QueryResponse<'gcx, ()>>> {
 135         use chalk_engine::SimplifiedAnswer;
 136
 137         debug!("make_solution(root_goal = {:?})", root_goal);
 138
 139         if simplified_answers.peek_answer().is_none() {
 140             return None;
 141         }
 142
 143         let SimplifiedAnswer { subst: constrained_subst, ambiguous } = simplified_answers
 144             .next_answer()
 145             .unwrap();
 146
 147         debug!("make_solution: ambiguous flag = {}", ambiguous);
 148
 149         let ambiguous = simplified_answers.peek_answer().is_some() || ambiguous;
 150
 151         let solution = constrained_subst.unchecked_map(|cs| match ambiguous {
 152             true => QueryResponse {
 153                 var_values: cs.subst.make_identity(self.tcx),
 154                 region_constraints: Vec::new(),
 155                 certainty: Certainty::Ambiguous,
 156                 value: (),
 157             },
 158
 159             false => QueryResponse {
 160                 var_values: cs.subst,
 161                 region_constraints: Vec::new(),
 162
 163                 // FIXME: restore this later once we get better at handling regions
 164                 // region_constraints: cs.constraints
 165                 //     .into_iter()
 166                 //     .map(|c| ty::Binder::bind(c))
 167                 //     .collect(),
 168                 certainty: Certainty::Proven,
 169                 value: (),
 170             },
 171         });
 172
 173         debug!("make_solution: solution = {:?}", solution);
 174
 175         Some(solution)
 176     }
 177 }
 178
 179 impl context::ContextOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
 180     /// Returns `true` if this is a coinductive goal: basically proving that an auto trait
 181     /// is implemented or proving that a trait reference is well-formed.
 182     fn is_coinductive(
 183         &self,
 184         goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>
 185     ) -> bool {
 186         use rustc::traits::{WellFormed, WhereClause};
 187
 188         let mut goal = goal.value.goal;
 189         loop {
 190             match goal {
 191                 GoalKind::DomainGoal(domain_goal) => match domain_goal {
 192                     DomainGoal::WellFormed(WellFormed::Trait(..)) => return true,
 193                     DomainGoal::Holds(WhereClause::Implemented(trait_predicate)) => {
 194                         return self.tcx.trait_is_auto(trait_predicate.def_id());
 195                     }
 196                     _ => return false,
 197                 }
 198
 199                 GoalKind::Quantified(_, bound_goal) => goal = *bound_goal.skip_binder(),
 200                 _ => return false,
 201             }
 202         }
 203     }
 204
 205     /// Creates an inference table for processing a new goal and instantiate that goal
 206     /// in that context, returning "all the pieces".
 207     ///
 208     /// More specifically: given a u-canonical goal `arg`, creates a
 209     /// new inference table `T` and populates it with the universes
 210     /// found in `arg`. Then, creates a substitution `S` that maps
 211     /// each bound variable in `arg` to a fresh inference variable
 212     /// from T. Returns:
 213     ///
 214     /// - the table `T`,
 215     /// - the substitution `S`,
 216     /// - the environment and goal found by substitution `S` into `arg`.
 217     fn instantiate_ucanonical_goal<R>(
 218         &self,
 219         arg: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
 220         op: impl context::WithInstantiatedUCanonicalGoal<ChalkArenas<'gcx>, Output = R>,
 221     ) -> R {
 222         self.tcx.infer_ctxt().enter_with_canonical(DUMMY_SP, arg, |ref infcx, arg, subst| {
 223             let chalk_infcx = &mut ChalkInferenceContext {
 224                 infcx,
 225             };
 226             op.with(chalk_infcx, subst, arg.environment, arg.goal)
 227         })
 228     }
 229
 230     fn instantiate_ex_clause<R>(
 231         &self,
 232         _num_universes: usize,
 233         arg: &Canonical<'gcx, ChalkExClause<'gcx>>,
 234         op: impl context::WithInstantiatedExClause<ChalkArenas<'gcx>, Output = R>,
 235     ) -> R {
 236         self.tcx.infer_ctxt().enter_with_canonical(DUMMY_SP, &arg.upcast(), |ref infcx, arg, _| {
 237             let chalk_infcx = &mut ChalkInferenceContext {
 238                 infcx,
 239             };
 240             op.with(chalk_infcx,arg)
 241         })
 242     }
 243
 244     /// Returns `true` if this solution has no region constraints.
 245     fn empty_constraints(ccs: &Canonical<'gcx, ConstrainedSubst<'gcx>>) -> bool {
 246         ccs.value.constraints.is_empty()
 247     }
 248
 249     fn inference_normalized_subst_from_ex_clause(
 250         canon_ex_clause: &'a Canonical<'gcx, ChalkExClause<'gcx>>,
 251     ) -> &'a CanonicalVarValues<'gcx> {
 252         &canon_ex_clause.value.subst
 253     }
 254
 255     fn inference_normalized_subst_from_subst(
 256         canon_subst: &'a Canonical<'gcx, ConstrainedSubst<'gcx>>,
 257     ) -> &'a CanonicalVarValues<'gcx> {
 258         &canon_subst.value.subst
 259     }
 260
 261     fn canonical(
 262         u_canon: &'a Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
 263     ) -> &'a Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>> {
 264         u_canon
 265     }
 266
 267     fn is_trivial_substitution(
 268         u_canon: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
 269         canonical_subst: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
 270     ) -> bool {
 271         let subst = &canonical_subst.value.subst;
 272         assert_eq!(u_canon.variables.len(), subst.var_values.len());
 273         subst.var_values
 274             .iter_enumerated()
 275             .all(|(cvar, kind)| match kind.unpack() {
 276                 UnpackedKind::Lifetime(r) => match r {
 277                     &ty::ReLateBound(debruijn, br) => {
 278                         debug_assert_eq!(debruijn, ty::INNERMOST);
 279                         cvar == br.assert_bound_var()
 280                     }
 281                     _ => false,
 282                 },
 283                 UnpackedKind::Type(ty) => match ty.sty {
 284                     ty::Bound(debruijn, bound_ty) => {
 285                         debug_assert_eq!(debruijn, ty::INNERMOST);
 286                         cvar == bound_ty.var
 287                     }
 288                     _ => false,
 289                 },
 290                 UnpackedKind::Const(ct) => match ct.val {
 291                     ConstValue::Infer(InferConst::Canonical(debruijn, bound_ct)) => {
 292                         debug_assert_eq!(debruijn, ty::INNERMOST);
 293                         cvar == bound_ct
 294                     }
 295                     _ => false,
 296                 }
 297             })
 298     }
 299
 300     fn num_universes(canon: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>) -> usize {
 301         canon.max_universe.index() + 1
 302     }
 303
 304     /// Convert a goal G *from* the canonical universes *into* our
 305     /// local universes. This will yield a goal G' that is the same
 306     /// but for the universes of universally quantified names.
 307     fn map_goal_from_canonical(
 308         _map: &UniverseMap,
 309         value: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
 310     ) -> Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>> {
 311         *value // FIXME universe maps not implemented yet
 312     }
 313
 314     fn map_subst_from_canonical(
 315         _map: &UniverseMap,
 316         value: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
 317     ) -> Canonical<'gcx, ConstrainedSubst<'gcx>> {
 318         value.clone() // FIXME universe maps not implemented yet
 319     }
 320 }
 321
 322 impl context::InferenceTable<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
 323     for ChalkInferenceContext<'cx, 'gcx, 'tcx>
 324 {
 325     fn into_goal(&self, domain_goal: DomainGoal<'tcx>) -> Goal<'tcx> {
 326         self.infcx.tcx.mk_goal(GoalKind::DomainGoal(domain_goal))
 327     }
 328
 329     fn cannot_prove(&self) -> Goal<'tcx> {
 330         self.infcx.tcx.mk_goal(GoalKind::CannotProve)
 331     }
 332
 333     fn into_hh_goal(&mut self, goal: Goal<'tcx>) -> ChalkHhGoal<'tcx> {
 334         match *goal {
 335             GoalKind::Implies(hypotheses, goal) => HhGoal::Implies(
 336                 hypotheses.iter().cloned().collect(),
 337                 goal
 338             ),
 339             GoalKind::And(left, right) => HhGoal::And(left, right),
 340             GoalKind::Not(subgoal) => HhGoal::Not(subgoal),
 341             GoalKind::DomainGoal(d) => HhGoal::DomainGoal(d),
 342             GoalKind::Quantified(QuantifierKind::Universal, binder) => HhGoal::ForAll(binder),
 343             GoalKind::Quantified(QuantifierKind::Existential, binder) => HhGoal::Exists(binder),
 344             GoalKind::Subtype(a, b) => HhGoal::Unify(
 345                 ty::Variance::Covariant,
 346                 a.into(),
 347                 b.into()
 348             ),
 349             GoalKind::CannotProve => HhGoal::CannotProve,
 350         }
 351     }
 352
 353     fn add_clauses(
 354         &mut self,
 355         env: &Environment<'tcx>,
 356         clauses: Vec<Clause<'tcx>>,
 357     ) -> Environment<'tcx> {
 358         Environment {
 359             clauses: self.infcx.tcx.mk_clauses(
 360                 env.clauses.iter().cloned().chain(clauses.into_iter())
 361             )
 362         }
 363     }
 364 }
 365
 366 impl context::TruncateOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
 367     for ChalkInferenceContext<'cx, 'gcx, 'tcx>
 368 {
 369     fn truncate_goal(
 370         &mut self,
 371         _subgoal: &InEnvironment<'tcx, Goal<'tcx>>,
 372     ) -> Option<InEnvironment<'tcx, Goal<'tcx>>> {
 373         None // FIXME we should truncate at some point!
 374     }
 375
 376     fn truncate_answer(
 377         &mut self,
 378         _subst: &CanonicalVarValues<'tcx>,
 379     ) -> Option<CanonicalVarValues<'tcx>> {
 380         None // FIXME we should truncate at some point!
 381     }
 382 }
 383
 384 impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
 385     for ChalkInferenceContext<'cx, 'gcx, 'tcx>
 386 {
 387     fn program_clauses(
 388         &self,
 389         environment: &Environment<'tcx>,
 390         goal: &DomainGoal<'tcx>,
 391     ) -> Vec<Clause<'tcx>> {
 392         self.program_clauses_impl(environment, goal)
 393     }
 394
 395     fn instantiate_binders_universally(
 396         &mut self,
 397         arg: &ty::Binder<Goal<'tcx>>,
 398     ) -> Goal<'tcx> {
 399         self.infcx.replace_bound_vars_with_placeholders(arg).0
 400     }
 401
 402     fn instantiate_binders_existentially(
 403         &mut self,
 404         arg: &ty::Binder<Goal<'tcx>>,
 405     ) -> Goal<'tcx> {
 406         self.infcx.replace_bound_vars_with_fresh_vars(
 407             DUMMY_SP,
 408             LateBoundRegionConversionTime::HigherRankedType,
 409             arg
 410         ).0
 411     }
 412
 413     fn debug_ex_clause(&mut self, value: &'v ChalkExClause<'tcx>) -> Box<dyn Debug + 'v> {
 414         let string = format!("{:?}", self.infcx.resolve_type_vars_if_possible(value));
 415         Box::new(string)
 416     }
 417
 418     fn canonicalize_goal(
 419         &mut self,
 420         value: &InEnvironment<'tcx, Goal<'tcx>>,
 421     ) -> Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>> {
 422         let mut _orig_values = OriginalQueryValues::default();
 423         self.infcx.canonicalize_query(value, &mut _orig_values)
 424     }
 425
 426     fn canonicalize_ex_clause(
 427         &mut self,
 428         value: &ChalkExClause<'tcx>,
 429     ) -> Canonical<'gcx, ChalkExClause<'gcx>> {
 430         self.infcx.canonicalize_response(value)
 431     }
 432
 433     fn canonicalize_constrained_subst(
 434         &mut self,
 435         subst: CanonicalVarValues<'tcx>,
 436         constraints: Vec<RegionConstraint<'tcx>>,
 437     ) -> Canonical<'gcx, ConstrainedSubst<'gcx>> {
 438         self.infcx.canonicalize_response(&ConstrainedSubst { subst, constraints })
 439     }
 440
 441     fn u_canonicalize_goal(
 442         &mut self,
 443         value: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
 444     ) -> (
 445         Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
 446         UniverseMap,
 447     ) {
 448         (value.clone(), UniverseMap)
 449     }
 450
 451     fn invert_goal(
 452         &mut self,
 453         _value: &InEnvironment<'tcx, Goal<'tcx>>,
 454     ) -> Option<InEnvironment<'tcx, Goal<'tcx>>> {
 455         panic!("goal inversion not yet implemented")
 456     }
 457
 458     fn unify_parameters(
 459         &mut self,
 460         environment: &Environment<'tcx>,
 461         variance: ty::Variance,
 462         a: &Kind<'tcx>,
 463         b: &Kind<'tcx>,
 464     ) -> Fallible<UnificationResult<'tcx>> {
 465         self.infcx.commit_if_ok(|_| {
 466             unify(self.infcx, *environment, variance, a, b)
 467                 .map_err(|_| chalk_engine::fallible::NoSolution)
 468         })
 469     }
 470
 471     fn sink_answer_subset(
 472         &self,
 473         value: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
 474     ) -> Canonical<'tcx, ConstrainedSubst<'tcx>> {
 475         value.clone()
 476     }
 477
 478     fn lift_delayed_literal(
 479         &self,
 480         value: DelayedLiteral<ChalkArenas<'tcx>>,
 481     ) -> DelayedLiteral<ChalkArenas<'gcx>> {
 482         match self.infcx.tcx.lift_to_global(&value) {
 483             Some(literal) => literal,
 484             None => bug!("cannot lift {:?}", value),
 485         }
 486     }
 487
 488     fn into_ex_clause(
 489         &mut self,
 490         result: UnificationResult<'tcx>,
 491         ex_clause: &mut ChalkExClause<'tcx>
 492     ) {
 493         into_ex_clause(result, ex_clause);
 494     }
 495 }
 496
 497 crate fn into_ex_clause(result: UnificationResult<'tcx>, ex_clause: &mut ChalkExClause<'tcx>) {
 498     ex_clause.subgoals.extend(
 499         result.goals.into_iter().map(Literal::Positive)
 500     );
 501
 502     // FIXME: restore this later once we get better at handling regions
 503     let _ = result.constraints.len(); // trick `-D dead-code`
 504     // ex_clause.constraints.extend(result.constraints);
 505 }
 506
 507 type ChalkHhGoal<'tcx> = HhGoal<ChalkArenas<'tcx>>;
 508
 509 type ChalkExClause<'tcx> = ExClause<ChalkArenas<'tcx>>;
 510
 511 impl Debug for ChalkContext<'cx, 'gcx> {
 512     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
 513         write!(f, "ChalkContext")
 514     }
 515 }
 516
 517 impl Debug for ChalkInferenceContext<'cx, 'gcx, 'tcx> {
 518     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
 519         write!(f, "ChalkInferenceContext")
 520     }
 521 }
 522
 523 impl ChalkContextLift<'tcx> for ChalkArenas<'a> {
 524     type LiftedExClause = ChalkExClause<'tcx>;
 525     type LiftedDelayedLiteral = DelayedLiteral<ChalkArenas<'tcx>>;
 526     type LiftedLiteral = Literal<ChalkArenas<'tcx>>;
 527
 528     fn lift_ex_clause_to_tcx(
 529         ex_clause: &ChalkExClause<'a>,
 530         tcx: TyCtxt<'_, 'gcx, 'tcx>
 531     ) -> Option<Self::LiftedExClause> {
 532         Some(ChalkExClause {
 533             subst: tcx.lift(&ex_clause.subst)?,
 534             delayed_literals: tcx.lift(&ex_clause.delayed_literals)?,
 535             constraints: tcx.lift(&ex_clause.constraints)?,
 536             subgoals: tcx.lift(&ex_clause.subgoals)?,
 537         })
 538     }
 539
 540     fn lift_delayed_literal_to_tcx(
 541         literal: &DelayedLiteral<ChalkArenas<'a>>,
 542         tcx: TyCtxt<'_, 'gcx, 'tcx>
 543     ) -> Option<Self::LiftedDelayedLiteral> {
 544         Some(match literal {
 545             DelayedLiteral::CannotProve(()) => DelayedLiteral::CannotProve(()),
 546             DelayedLiteral::Negative(index) => DelayedLiteral::Negative(*index),
 547             DelayedLiteral::Positive(index, subst) => DelayedLiteral::Positive(
 548                 *index,
 549                 tcx.lift(subst)?
 550             )
 551         })
 552     }
 553
 554     fn lift_literal_to_tcx(
 555         literal: &Literal<ChalkArenas<'a>>,
 556         tcx: TyCtxt<'_, 'gcx, 'tcx>,
 557     ) -> Option<Self::LiftedLiteral> {
 558         Some(match literal {
 559             Literal::Negative(goal) => Literal::Negative(tcx.lift(goal)?),
 560             Literal::Positive(goal) =>  Literal::Positive(tcx.lift(goal)?),
 561         })
 562     }
 563 }
 564
 565 impl ExClauseFold<'tcx> for ChalkArenas<'tcx> {
 566     fn fold_ex_clause_with<'gcx: 'tcx, F: TypeFolder<'gcx, 'tcx>>(
 567         ex_clause: &ChalkExClause<'tcx>,
 568         folder: &mut F,
 569     ) -> ChalkExClause<'tcx> {
 570         ExClause {
 571             subst: ex_clause.subst.fold_with(folder),
 572             delayed_literals: ex_clause.delayed_literals.fold_with(folder),
 573             constraints: ex_clause.constraints.fold_with(folder),
 574             subgoals: ex_clause.subgoals.fold_with(folder),
 575         }
 576     }
 577
 578     fn visit_ex_clause_with<'gcx: 'tcx, V: TypeVisitor<'tcx>>(
 579         ex_clause: &ExClause<Self>,
 580         visitor: &mut V,
 581     ) -> bool {
 582         let ExClause {
 583             subst,
 584             delayed_literals,
 585             constraints,
 586             subgoals,
 587         } = ex_clause;
 588         subst.visit_with(visitor)
 589             || delayed_literals.visit_with(visitor)
 590             || constraints.visit_with(visitor)
 591             || subgoals.visit_with(visitor)
 592     }
 593 }
 594
 595 BraceStructLiftImpl! {
 596     impl<'a, 'tcx> Lift<'tcx> for ConstrainedSubst<'a> {
 597         type Lifted = ConstrainedSubst<'tcx>;
 598
 599         subst, constraints
 600     }
 601 }
 602
 603 trait Upcast<'tcx, 'gcx: 'tcx>: 'gcx {
 604     type Upcasted: 'tcx;
 605
 606     fn upcast(&self) -> Self::Upcasted;
 607 }
 608
 609 impl<'tcx, 'gcx: 'tcx> Upcast<'tcx, 'gcx> for DelayedLiteral<ChalkArenas<'gcx>> {
 610     type Upcasted = DelayedLiteral<ChalkArenas<'tcx>>;
 611
 612     fn upcast(&self) -> Self::Upcasted {
 613         match self {
 614             &DelayedLiteral::CannotProve(..) => DelayedLiteral::CannotProve(()),
 615             &DelayedLiteral::Negative(index) => DelayedLiteral::Negative(index),
 616             DelayedLiteral::Positive(index, subst) => DelayedLiteral::Positive(
 617                 *index,
 618                 subst.clone()
 619             ),
 620         }
 621     }
 622 }
 623
 624 impl<'tcx, 'gcx: 'tcx> Upcast<'tcx, 'gcx> for Literal<ChalkArenas<'gcx>> {
 625     type Upcasted = Literal<ChalkArenas<'tcx>>;
 626
 627     fn upcast(&self) -> Self::Upcasted {
 628         match self {
 629             &Literal::Negative(goal) => Literal::Negative(goal),
 630             &Literal::Positive(goal) => Literal::Positive(goal),
 631         }
 632     }
 633 }
 634
 635 impl<'tcx, 'gcx: 'tcx> Upcast<'tcx, 'gcx> for ExClause<ChalkArenas<'gcx>> {
 636     type Upcasted = ExClause<ChalkArenas<'tcx>>;
 637
 638     fn upcast(&self) -> Self::Upcasted {
 639         ExClause {
 640             subst: self.subst.clone(),
 641             delayed_literals: self.delayed_literals
 642                 .iter()
 643                 .map(|l| l.upcast())
 644                 .collect(),
 645             constraints: self.constraints.clone(),
 646             subgoals: self.subgoals
 647                 .iter()
 648                 .map(|g| g.upcast())
 649                 .collect(),
 650         }
 651     }
 652 }
 653
 654 impl<'tcx, 'gcx: 'tcx, T> Upcast<'tcx, 'gcx> for Canonical<'gcx, T>
 655     where T: Upcast<'tcx, 'gcx>
 656 {
 657     type Upcasted = Canonical<'tcx, T::Upcasted>;
 658
 659     fn upcast(&self) -> Self::Upcasted {
 660         Canonical {
 661             max_universe: self.max_universe,
 662             value: self.value.upcast(),
 663             variables: self.variables,
 664         }
 665     }
 666 }
 667
 668 crate fn provide(p: &mut Providers<'_>) {
 669     *p = Providers {
 670         evaluate_goal,
 671         ..*p
 672     };
 673 }
 674
 675 crate fn evaluate_goal<'a, 'tcx>(
 676     tcx: TyCtxt<'a, 'tcx, 'tcx>,
 677     goal: ChalkCanonicalGoal<'tcx>
 678 ) -> Result<
 679     &'tcx Canonical<'tcx, QueryResponse<'tcx, ()>>,
 680     traits::query::NoSolution
 681 > {
 682     use crate::lowering::Lower;
 683     use rustc::traits::WellFormed;
 684
 685     let goal = goal.unchecked_map(|goal| InEnvironment {
 686         environment: goal.environment,
 687         goal: match goal.goal {
 688             ty::Predicate::WellFormed(ty) => tcx.mk_goal(
 689                 GoalKind::DomainGoal(DomainGoal::WellFormed(WellFormed::Ty(ty)))
 690             ),
 691
 692             ty::Predicate::Subtype(predicate) => tcx.mk_goal(
 693                 GoalKind::Quantified(
 694                     QuantifierKind::Universal,
 695                     predicate.map_bound(|pred| tcx.mk_goal(GoalKind::Subtype(pred.a, pred.b)))
 696                 )
 697             ),
 698
 699             other => tcx.mk_goal(
 700                 GoalKind::from_poly_domain_goal(other.lower(), tcx)
 701             ),
 702         },
 703     });
 704
 705
 706     debug!("evaluate_goal(goal = {:?})", goal);
 707
 708     let context = ChalkContext {
 709         _arenas: ChalkArenas {
 710             _phantom: PhantomData,
 711         },
 712         tcx,
 713     };
 714
 715     let mut forest = Forest::new(context);
 716     let solution = forest.solve(&goal);
 717
 718     debug!("evaluate_goal: solution = {:?}", solution);
 719
 720     solution.map(|ok| Ok(&*tcx.arena.alloc(ok)))
 721             .unwrap_or(Err(traits::query::NoSolution))
 722 }