5 use chalk_engine::fallible::Fallible;
13 use chalk_engine::forest::Forest;
14 use rustc::infer::{InferCtxt, LateBoundRegionConversionTime};
15 use rustc::infer::canonical::{
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;
42 use std::fmt::{self, Debug};
43 use std::marker::PhantomData;
47 #[derive(Copy, Clone, Debug)]
48 crate struct ChalkArenas<'gcx> {
49 _phantom: PhantomData<&'gcx ()>,
52 #[derive(Copy, Clone)]
53 crate struct ChalkContext<'cx, 'gcx: 'cx> {
54 _arenas: ChalkArenas<'gcx>,
55 tcx: TyCtxt<'cx, 'gcx, 'gcx>,
58 #[derive(Copy, Clone)]
59 crate struct ChalkInferenceContext<'cx, 'gcx: 'tcx, 'tcx: 'cx> {
60 infcx: &'cx InferCtxt<'cx, 'gcx, 'tcx>,
63 #[derive(Copy, Clone, Debug)]
64 crate struct UniverseMap;
66 crate type RegionConstraint<'tcx> = ty::OutlivesPredicate<Kind<'tcx>, ty::Region<'tcx>>;
68 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
69 crate struct ConstrainedSubst<'tcx> {
70 subst: CanonicalVarValues<'tcx>,
71 constraints: Vec<RegionConstraint<'tcx>>,
74 BraceStructTypeFoldableImpl! {
75 impl<'tcx> TypeFoldable<'tcx> for ConstrainedSubst<'tcx> {
80 impl context::Context for ChalkArenas<'tcx> {
81 type CanonicalExClause = Canonical<'tcx, ChalkExClause<'tcx>>;
83 type CanonicalGoalInEnvironment = Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>>;
85 // u-canonicalization not yet implemented
86 type UCanonicalGoalInEnvironment = Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>>;
88 type CanonicalConstrainedSubst = Canonical<'tcx, ConstrainedSubst<'tcx>>;
90 // u-canonicalization not yet implemented
91 type UniverseMap = UniverseMap;
93 type Solution = Canonical<'tcx, QueryResponse<'tcx, ()>>;
95 type InferenceNormalizedSubst = CanonicalVarValues<'tcx>;
97 type GoalInEnvironment = InEnvironment<'tcx, Goal<'tcx>>;
99 type RegionConstraint = RegionConstraint<'tcx>;
101 type Substitution = CanonicalVarValues<'tcx>;
103 type Environment = Environment<'tcx>;
105 type Goal = Goal<'tcx>;
107 type DomainGoal = DomainGoal<'tcx>;
109 type BindersGoal = ty::Binder<Goal<'tcx>>;
111 type Parameter = Kind<'tcx>;
113 type ProgramClause = Clause<'tcx>;
115 type ProgramClauses = Vec<Clause<'tcx>>;
117 type UnificationResult = UnificationResult<'tcx>;
119 type Variance = ty::Variance;
121 fn goal_in_environment(
122 env: &Environment<'tcx>,
124 ) -> InEnvironment<'tcx, Goal<'tcx>> {
129 impl context::AggregateOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
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;
137 debug!("make_solution(root_goal = {:?})", root_goal);
139 if simplified_answers.peek_answer().is_none() {
143 let SimplifiedAnswer { subst: constrained_subst, ambiguous } = simplified_answers
147 debug!("make_solution: ambiguous flag = {}", ambiguous);
149 let ambiguous = simplified_answers.peek_answer().is_some() || ambiguous;
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,
159 false => QueryResponse {
160 var_values: cs.subst,
161 region_constraints: Vec::new(),
163 // FIXME: restore this later once we get better at handling regions
164 // region_constraints: cs.constraints
166 // .map(|c| ty::Binder::bind(c))
168 certainty: Certainty::Proven,
173 debug!("make_solution: solution = {:?}", solution);
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.
184 goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>
186 use rustc::traits::{WellFormed, WhereClause};
188 let mut goal = goal.value.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());
199 GoalKind::Quantified(_, bound_goal) => goal = *bound_goal.skip_binder(),
205 /// Creates an inference table for processing a new goal and instantiate that goal
206 /// in that context, returning "all the pieces".
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
215 /// - the substitution `S`,
216 /// - the environment and goal found by substitution `S` into `arg`.
217 fn instantiate_ucanonical_goal<R>(
219 arg: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
220 op: impl context::WithInstantiatedUCanonicalGoal<ChalkArenas<'gcx>, Output = R>,
222 self.tcx.infer_ctxt().enter_with_canonical(DUMMY_SP, arg, |ref infcx, arg, subst| {
223 let chalk_infcx = &mut ChalkInferenceContext {
226 op.with(chalk_infcx, subst, arg.environment, arg.goal)
230 fn instantiate_ex_clause<R>(
232 _num_universes: usize,
233 arg: &Canonical<'gcx, ChalkExClause<'gcx>>,
234 op: impl context::WithInstantiatedExClause<ChalkArenas<'gcx>, Output = R>,
236 self.tcx.infer_ctxt().enter_with_canonical(DUMMY_SP, &arg.upcast(), |ref infcx, arg, _| {
237 let chalk_infcx = &mut ChalkInferenceContext {
240 op.with(chalk_infcx,arg)
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()
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
255 fn inference_normalized_subst_from_subst(
256 canon_subst: &'a Canonical<'gcx, ConstrainedSubst<'gcx>>,
257 ) -> &'a CanonicalVarValues<'gcx> {
258 &canon_subst.value.subst
262 u_canon: &'a Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
263 ) -> &'a Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>> {
267 fn is_trivial_substitution(
268 u_canon: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
269 canonical_subst: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
271 let subst = &canonical_subst.value.subst;
272 assert_eq!(u_canon.variables.len(), subst.var_values.len());
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()
283 UnpackedKind::Type(ty) => match ty.sty {
284 ty::Bound(debruijn, bound_ty) => {
285 debug_assert_eq!(debruijn, ty::INNERMOST);
290 UnpackedKind::Const(ct) => match ct.val {
291 ConstValue::Infer(InferConst::Canonical(debruijn, bound_ct)) => {
292 debug_assert_eq!(debruijn, ty::INNERMOST);
300 fn num_universes(canon: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>) -> usize {
301 canon.max_universe.index() + 1
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(
309 value: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
310 ) -> Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>> {
311 *value // FIXME universe maps not implemented yet
314 fn map_subst_from_canonical(
316 value: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
317 ) -> Canonical<'gcx, ConstrainedSubst<'gcx>> {
318 value.clone() // FIXME universe maps not implemented yet
322 impl context::InferenceTable<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
323 for ChalkInferenceContext<'cx, 'gcx, 'tcx>
325 fn into_goal(&self, domain_goal: DomainGoal<'tcx>) -> Goal<'tcx> {
326 self.infcx.tcx.mk_goal(GoalKind::DomainGoal(domain_goal))
329 fn cannot_prove(&self) -> Goal<'tcx> {
330 self.infcx.tcx.mk_goal(GoalKind::CannotProve)
333 fn into_hh_goal(&mut self, goal: Goal<'tcx>) -> ChalkHhGoal<'tcx> {
335 GoalKind::Implies(hypotheses, goal) => HhGoal::Implies(
336 hypotheses.iter().cloned().collect(),
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,
349 GoalKind::CannotProve => HhGoal::CannotProve,
355 env: &Environment<'tcx>,
356 clauses: Vec<Clause<'tcx>>,
357 ) -> Environment<'tcx> {
359 clauses: self.infcx.tcx.mk_clauses(
360 env.clauses.iter().cloned().chain(clauses.into_iter())
366 impl context::TruncateOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
367 for ChalkInferenceContext<'cx, 'gcx, 'tcx>
371 _subgoal: &InEnvironment<'tcx, Goal<'tcx>>,
372 ) -> Option<InEnvironment<'tcx, Goal<'tcx>>> {
373 None // FIXME we should truncate at some point!
378 _subst: &CanonicalVarValues<'tcx>,
379 ) -> Option<CanonicalVarValues<'tcx>> {
380 None // FIXME we should truncate at some point!
384 impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
385 for ChalkInferenceContext<'cx, 'gcx, 'tcx>
389 environment: &Environment<'tcx>,
390 goal: &DomainGoal<'tcx>,
391 ) -> Vec<Clause<'tcx>> {
392 self.program_clauses_impl(environment, goal)
395 fn instantiate_binders_universally(
397 arg: &ty::Binder<Goal<'tcx>>,
399 self.infcx.replace_bound_vars_with_placeholders(arg).0
402 fn instantiate_binders_existentially(
404 arg: &ty::Binder<Goal<'tcx>>,
406 self.infcx.replace_bound_vars_with_fresh_vars(
408 LateBoundRegionConversionTime::HigherRankedType,
413 fn debug_ex_clause(&mut self, value: &'v ChalkExClause<'tcx>) -> Box<dyn Debug + 'v> {
414 let string = format!("{:?}", self.infcx.resolve_vars_if_possible(value));
418 fn canonicalize_goal(
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)
426 fn canonicalize_ex_clause(
428 value: &ChalkExClause<'tcx>,
429 ) -> Canonical<'gcx, ChalkExClause<'gcx>> {
430 self.infcx.canonicalize_response(value)
433 fn canonicalize_constrained_subst(
435 subst: CanonicalVarValues<'tcx>,
436 constraints: Vec<RegionConstraint<'tcx>>,
437 ) -> Canonical<'gcx, ConstrainedSubst<'gcx>> {
438 self.infcx.canonicalize_response(&ConstrainedSubst { subst, constraints })
441 fn u_canonicalize_goal(
443 value: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
445 Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
448 (value.clone(), UniverseMap)
453 _value: &InEnvironment<'tcx, Goal<'tcx>>,
454 ) -> Option<InEnvironment<'tcx, Goal<'tcx>>> {
455 panic!("goal inversion not yet implemented")
460 environment: &Environment<'tcx>,
461 variance: ty::Variance,
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)
471 fn sink_answer_subset(
473 value: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
474 ) -> Canonical<'tcx, ConstrainedSubst<'tcx>> {
478 fn lift_delayed_literal(
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),
490 result: UnificationResult<'tcx>,
491 ex_clause: &mut ChalkExClause<'tcx>
493 into_ex_clause(result, ex_clause);
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)
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);
507 type ChalkHhGoal<'tcx> = HhGoal<ChalkArenas<'tcx>>;
509 type ChalkExClause<'tcx> = ExClause<ChalkArenas<'tcx>>;
511 impl Debug for ChalkContext<'cx, 'gcx> {
512 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
513 write!(f, "ChalkContext")
517 impl Debug for ChalkInferenceContext<'cx, 'gcx, 'tcx> {
518 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
519 write!(f, "ChalkInferenceContext")
523 impl ChalkContextLift<'tcx> for ChalkArenas<'a> {
524 type LiftedExClause = ChalkExClause<'tcx>;
525 type LiftedDelayedLiteral = DelayedLiteral<ChalkArenas<'tcx>>;
526 type LiftedLiteral = Literal<ChalkArenas<'tcx>>;
528 fn lift_ex_clause_to_tcx(
529 ex_clause: &ChalkExClause<'a>,
530 tcx: TyCtxt<'_, 'gcx, 'tcx>
531 ) -> Option<Self::LiftedExClause> {
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)?,
540 fn lift_delayed_literal_to_tcx(
541 literal: &DelayedLiteral<ChalkArenas<'a>>,
542 tcx: TyCtxt<'_, 'gcx, 'tcx>
543 ) -> Option<Self::LiftedDelayedLiteral> {
545 DelayedLiteral::CannotProve(()) => DelayedLiteral::CannotProve(()),
546 DelayedLiteral::Negative(index) => DelayedLiteral::Negative(*index),
547 DelayedLiteral::Positive(index, subst) => DelayedLiteral::Positive(
554 fn lift_literal_to_tcx(
555 literal: &Literal<ChalkArenas<'a>>,
556 tcx: TyCtxt<'_, 'gcx, 'tcx>,
557 ) -> Option<Self::LiftedLiteral> {
559 Literal::Negative(goal) => Literal::Negative(tcx.lift(goal)?),
560 Literal::Positive(goal) => Literal::Positive(tcx.lift(goal)?),
565 impl ExClauseFold<'tcx> for ChalkArenas<'tcx> {
566 fn fold_ex_clause_with<'gcx: 'tcx, F: TypeFolder<'gcx, 'tcx>>(
567 ex_clause: &ChalkExClause<'tcx>,
569 ) -> ChalkExClause<'tcx> {
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),
578 fn visit_ex_clause_with<V: TypeVisitor<'tcx>>(
579 ex_clause: &ExClause<Self>,
588 subst.visit_with(visitor)
589 || delayed_literals.visit_with(visitor)
590 || constraints.visit_with(visitor)
591 || subgoals.visit_with(visitor)
595 BraceStructLiftImpl! {
596 impl<'a, 'tcx> Lift<'tcx> for ConstrainedSubst<'a> {
597 type Lifted = ConstrainedSubst<'tcx>;
603 trait Upcast<'tcx, 'gcx: 'tcx>: 'gcx {
606 fn upcast(&self) -> Self::Upcasted;
609 impl<'tcx, 'gcx: 'tcx> Upcast<'tcx, 'gcx> for DelayedLiteral<ChalkArenas<'gcx>> {
610 type Upcasted = DelayedLiteral<ChalkArenas<'tcx>>;
612 fn upcast(&self) -> Self::Upcasted {
614 &DelayedLiteral::CannotProve(..) => DelayedLiteral::CannotProve(()),
615 &DelayedLiteral::Negative(index) => DelayedLiteral::Negative(index),
616 DelayedLiteral::Positive(index, subst) => DelayedLiteral::Positive(
624 impl<'tcx, 'gcx: 'tcx> Upcast<'tcx, 'gcx> for Literal<ChalkArenas<'gcx>> {
625 type Upcasted = Literal<ChalkArenas<'tcx>>;
627 fn upcast(&self) -> Self::Upcasted {
629 &Literal::Negative(goal) => Literal::Negative(goal),
630 &Literal::Positive(goal) => Literal::Positive(goal),
635 impl<'tcx, 'gcx: 'tcx> Upcast<'tcx, 'gcx> for ExClause<ChalkArenas<'gcx>> {
636 type Upcasted = ExClause<ChalkArenas<'tcx>>;
638 fn upcast(&self) -> Self::Upcasted {
640 subst: self.subst.clone(),
641 delayed_literals: self.delayed_literals
645 constraints: self.constraints.clone(),
646 subgoals: self.subgoals
654 impl<'tcx, 'gcx: 'tcx, T> Upcast<'tcx, 'gcx> for Canonical<'gcx, T>
655 where T: Upcast<'tcx, 'gcx>
657 type Upcasted = Canonical<'tcx, T::Upcasted>;
659 fn upcast(&self) -> Self::Upcasted {
661 max_universe: self.max_universe,
662 value: self.value.upcast(),
663 variables: self.variables,
668 crate fn provide(p: &mut Providers<'_>) {
675 crate fn evaluate_goal<'a, 'tcx>(
676 tcx: TyCtxt<'a, 'tcx, 'tcx>,
677 goal: ChalkCanonicalGoal<'tcx>
679 &'tcx Canonical<'tcx, QueryResponse<'tcx, ()>>,
680 traits::query::NoSolution
682 use crate::lowering::Lower;
683 use rustc::traits::WellFormed;
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)))
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)))
699 other => tcx.mk_goal(
700 GoalKind::from_poly_domain_goal(other.lower(), tcx)
706 debug!("evaluate_goal(goal = {:?})", goal);
708 let context = ChalkContext {
709 _arenas: ChalkArenas {
710 _phantom: PhantomData,
715 let mut forest = Forest::new(context);
716 let solution = forest.solve(&goal);
718 debug!("evaluate_goal: solution = {:?}", solution);
720 solution.map(|ok| Ok(&*tcx.arena.alloc(ok)))
721 .unwrap_or(Err(traits::query::NoSolution))