1 // Copyright 2014 The Rust Project Developers. See the COPYRIGHT
2 // file at the top-level directory of this distribution and at
3 // http://rust-lang.org/COPYRIGHT.
5 // Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
6 // http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
7 // <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
8 // option. This file may not be copied, modified, or distributed
9 // except according to those terms.
11 use chalk_engine::fallible::Fallible as ChalkEngineFallible;
12 use chalk_engine::{context, hh::HhGoal, DelayedLiteral, ExClause};
13 use rustc::infer::canonical::{
14 Canonical, CanonicalVarValues, Canonicalize, QueryRegionConstraint, QueryResult,
16 use rustc::infer::{InferCtxt, InferOk, LateBoundRegionConversionTime};
27 use rustc::ty::fold::{TypeFoldable, TypeFolder, TypeVisitor};
28 use rustc::ty::subst::Kind;
29 use rustc::ty::{self, TyCtxt};
31 use std::fmt::{self, Debug};
32 use std::marker::PhantomData;
34 use syntax_pos::DUMMY_SP;
36 #[derive(Copy, Clone, Debug)]
37 crate struct ChalkArenas<'gcx> {
38 _phantom: PhantomData<&'gcx ()>,
41 #[derive(Copy, Clone)]
42 crate struct ChalkContext<'cx, 'gcx: 'cx> {
43 _arenas: ChalkArenas<'gcx>,
44 _tcx: TyCtxt<'cx, 'gcx, 'gcx>,
47 #[derive(Copy, Clone)]
48 crate struct ChalkInferenceContext<'cx, 'gcx: 'tcx, 'tcx: 'cx> {
49 infcx: &'cx InferCtxt<'cx, 'gcx, 'tcx>,
52 #[derive(Copy, Clone, Debug)]
53 crate struct UniverseMap;
55 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
56 crate struct ConstrainedSubst<'tcx> {
57 subst: CanonicalVarValues<'tcx>,
58 constraints: Vec<QueryRegionConstraint<'tcx>>,
61 BraceStructTypeFoldableImpl! {
62 impl<'tcx> TypeFoldable<'tcx> for ConstrainedSubst<'tcx> {
67 impl context::Context for ChalkArenas<'tcx> {
68 type CanonicalExClause = Canonical<'tcx, ExClause<Self>>;
70 type CanonicalGoalInEnvironment = Canonical<'tcx, ty::ParamEnvAnd<'tcx, Goal<'tcx>>>;
72 // u-canonicalization not yet implemented
73 type UCanonicalGoalInEnvironment = Canonical<'tcx, ty::ParamEnvAnd<'tcx, Goal<'tcx>>>;
75 type CanonicalConstrainedSubst = Canonical<'tcx, ConstrainedSubst<'tcx>>;
77 // u-canonicalization not yet implemented
78 type UniverseMap = UniverseMap;
80 type Solution = Canonical<'tcx, QueryResult<'tcx, ()>>;
82 type InferenceNormalizedSubst = CanonicalVarValues<'tcx>;
84 type GoalInEnvironment = ty::ParamEnvAnd<'tcx, Goal<'tcx>>;
86 type RegionConstraint = QueryRegionConstraint<'tcx>;
88 type Substitution = CanonicalVarValues<'tcx>;
90 type Environment = ty::ParamEnv<'tcx>;
92 type Goal = Goal<'tcx>;
94 type DomainGoal = DomainGoal<'tcx>;
96 type BindersGoal = ty::Binder<&'tcx Goal<'tcx>>;
98 type Parameter = Kind<'tcx>;
100 type ProgramClause = ProgramClause<'tcx>;
102 type ProgramClauses = Vec<ProgramClause<'tcx>>;
104 type UnificationResult = InferOk<'tcx, ()>;
106 fn into_goal(domain_goal: DomainGoal<'tcx>) -> Goal<'tcx> {
107 Goal::DomainGoal(domain_goal)
110 fn cannot_prove() -> Goal<'tcx> {
114 fn goal_in_environment(
115 env: &ty::ParamEnv<'tcx>,
117 ) -> ty::ParamEnvAnd<'tcx, Goal<'tcx>> {
122 impl context::AggregateOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
125 _root_goal: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
126 _simplified_answers: impl context::AnswerStream<ChalkArenas<'gcx>>,
127 ) -> Option<Canonical<'gcx, QueryResult<'gcx, ()>>> {
132 impl context::ContextOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
133 /// True if this is a coinductive goal -- e.g., proving an auto trait.
134 fn is_coinductive(&self, _goal: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>) -> bool {
138 /// Create an inference table for processing a new goal and instantiate that goal
139 /// in that context, returning "all the pieces".
141 /// More specifically: given a u-canonical goal `arg`, creates a
142 /// new inference table `T` and populates it with the universes
143 /// found in `arg`. Then, creates a substitution `S` that maps
144 /// each bound variable in `arg` to a fresh inference variable
148 /// - the substitution `S`
149 /// - the environment and goal found by substitution `S` into `arg`
150 fn instantiate_ucanonical_goal<R>(
152 _arg: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
153 _op: impl context::WithInstantiatedUCanonicalGoal<ChalkArenas<'gcx>, Output = R>,
158 fn instantiate_ex_clause<R>(
160 _num_universes: usize,
161 _canonical_ex_clause: &Canonical<'gcx, ChalkExClause<'gcx>>,
162 _op: impl context::WithInstantiatedExClause<ChalkArenas<'gcx>, Output = R>,
167 /// True if this solution has no region constraints.
168 fn empty_constraints(ccs: &Canonical<'gcx, ConstrainedSubst<'gcx>>) -> bool {
169 ccs.value.constraints.is_empty()
172 fn inference_normalized_subst_from_ex_clause(
173 canon_ex_clause: &'a Canonical<'gcx, ChalkExClause<'gcx>>,
174 ) -> &'a CanonicalVarValues<'gcx> {
175 &canon_ex_clause.value.subst
178 fn inference_normalized_subst_from_subst(
179 canon_subst: &'a Canonical<'gcx, ConstrainedSubst<'gcx>>,
180 ) -> &'a CanonicalVarValues<'gcx> {
181 &canon_subst.value.subst
185 u_canon: &'a Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
186 ) -> &'a Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>> {
190 fn is_trivial_substitution(
191 _u_canon: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
192 _canonical_subst: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
197 fn num_universes(_: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>) -> usize {
201 /// Convert a goal G *from* the canonical universes *into* our
202 /// local universes. This will yield a goal G' that is the same
203 /// but for the universes of universally quantified names.
204 fn map_goal_from_canonical(
206 value: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
207 ) -> Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>> {
208 *value // FIXME universe maps not implemented yet
211 fn map_subst_from_canonical(
213 value: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
214 ) -> Canonical<'gcx, ConstrainedSubst<'gcx>> {
215 value.clone() // FIXME universe maps not implemented yet
219 //impl context::UCanonicalGoalInEnvironment<ChalkContext<'cx, 'gcx>>
220 // for Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>
222 // fn canonical(&self) -> &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>> {
226 // fn is_trivial_substitution(
228 // canonical_subst: &Canonical<'tcx, ConstrainedSubst<'tcx>>,
230 // let subst = &canonical_subst.value.subst;
231 // assert_eq!(self.canonical.variables.len(), subst.var_values.len());
234 // .iter_enumerated()
235 // .all(|(cvar, kind)| match kind.unpack() {
236 // Kind::Lifetime(r) => match r {
237 // ty::ReCanonical(cvar1) => cvar == cvar1,
240 // Kind::Type(ty) => match ty.sty {
241 // ty::TyInfer(ty::InferTy::CanonicalTy(cvar1)) => cvar == cvar1,
247 // fn num_universes(&self) -> usize {
252 impl context::InferenceTable<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
253 for ChalkInferenceContext<'cx, 'gcx, 'tcx>
255 fn into_hh_goal(&mut self, goal: Goal<'tcx>) -> ChalkHhGoal<'tcx> {
257 Goal::Implies(..) => panic!("FIXME rust-lang-nursery/chalk#94"),
258 Goal::And(left, right) => HhGoal::And(*left, *right),
259 Goal::Not(subgoal) => HhGoal::Not(*subgoal),
260 Goal::DomainGoal(d) => HhGoal::DomainGoal(d),
261 Goal::Quantified(QuantifierKind::Universal, binder) => HhGoal::ForAll(binder),
262 Goal::Quantified(QuantifierKind::Existential, binder) => HhGoal::Exists(binder),
263 Goal::CannotProve => HhGoal::CannotProve,
269 _env: &ty::ParamEnv<'tcx>,
270 _clauses: Vec<ProgramClause<'tcx>>,
271 ) -> ty::ParamEnv<'tcx> {
272 panic!("FIXME no method to add clauses to ParamEnv yet")
276 impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
277 for ChalkInferenceContext<'cx, 'gcx, 'tcx>
281 _environment: &ty::ParamEnv<'tcx>,
282 _goal: &DomainGoal<'tcx>,
283 _subst: &CanonicalVarValues<'tcx>,
284 _clause: &ProgramClause<'tcx>,
285 ) -> chalk_engine::fallible::Fallible<Canonical<'gcx, ChalkExClause<'gcx>>> {
289 fn apply_answer_subst(
291 _ex_clause: ChalkExClause<'tcx>,
292 _selected_goal: &ty::ParamEnvAnd<'tcx, Goal<'tcx>>,
293 _answer_table_goal: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
294 _canonical_answer_subst: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
295 ) -> chalk_engine::fallible::Fallible<ChalkExClause<'tcx>> {
300 impl context::TruncateOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
301 for ChalkInferenceContext<'cx, 'gcx, 'tcx>
305 subgoal: &ty::ParamEnvAnd<'tcx, Goal<'tcx>>,
306 ) -> Option<ty::ParamEnvAnd<'tcx, Goal<'tcx>>> {
307 Some(*subgoal) // FIXME we should truncate at some point!
312 subst: &CanonicalVarValues<'tcx>,
313 ) -> Option<CanonicalVarValues<'tcx>> {
314 Some(subst.clone()) // FIXME we should truncate at some point!
318 impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
319 for ChalkInferenceContext<'cx, 'gcx, 'tcx>
323 _environment: &ty::ParamEnv<'tcx>,
324 goal: &DomainGoal<'tcx>,
325 ) -> Vec<ProgramClause<'tcx>> {
326 use rustc::traits::WhereClause::*;
329 DomainGoal::Holds(Implemented(_trait_predicate)) => {
332 // - Trait definitions (implied bounds)
333 // - Implementations of the trait itself
337 DomainGoal::Holds(ProjectionEq(_projection_predicate)) => {
342 DomainGoal::Holds(RegionOutlives(_region_outlives)) => {
346 DomainGoal::Holds(TypeOutlives(_type_outlives)) => {
350 DomainGoal::WellFormed(WellFormed::Trait(_trait_predicate)) => {
351 // These come from -- the trait decl.
355 DomainGoal::WellFormed(WellFormed::Ty(_ty)) => panic!(),
357 DomainGoal::FromEnv(FromEnv::Trait(_trait_predicate)) => panic!(),
359 DomainGoal::FromEnv(FromEnv::Ty(_ty)) => panic!(),
361 DomainGoal::Normalize(_) => panic!(),
365 fn instantiate_binders_universally(
367 _arg: &ty::Binder<&'tcx Goal<'tcx>>,
369 panic!("FIXME -- universal instantiation needs sgrif's branch")
372 fn instantiate_binders_existentially(
374 arg: &ty::Binder<&'tcx Goal<'tcx>>,
376 let (value, _map) = self.infcx.replace_late_bound_regions_with_fresh_var(
378 LateBoundRegionConversionTime::HigherRankedType,
384 fn debug_ex_clause(&mut self, value: &'v ChalkExClause<'tcx>) -> Box<dyn Debug + 'v> {
385 let string = format!("{:?}", self.infcx.resolve_type_vars_if_possible(value));
389 fn canonicalize_goal(
391 value: &ty::ParamEnvAnd<'tcx, Goal<'tcx>>,
392 ) -> Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>> {
393 self.infcx.canonicalize_query(value).0
396 fn canonicalize_ex_clause(
398 value: &ChalkExClause<'tcx>,
399 ) -> Canonical<'gcx, ChalkExClause<'gcx>> {
400 self.infcx.canonicalize_response(value).0
403 fn canonicalize_constrained_subst(
405 subst: CanonicalVarValues<'tcx>,
406 constraints: Vec<QueryRegionConstraint<'tcx>>,
407 ) -> Canonical<'gcx, ConstrainedSubst<'gcx>> {
409 .canonicalize_response(&ConstrainedSubst { subst, constraints })
413 fn u_canonicalize_goal(
415 value: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
417 Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
420 (value.clone(), UniverseMap)
425 _value: &ty::ParamEnvAnd<'tcx, Goal<'tcx>>,
426 ) -> Option<ty::ParamEnvAnd<'tcx, Goal<'tcx>>> {
427 panic!("goal inversion not yet implemented")
432 _environment: &ty::ParamEnv<'tcx>,
435 ) -> ChalkEngineFallible<InferOk<'tcx, ()>> {
439 fn sink_answer_subset(
441 value: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
442 ) -> Canonical<'tcx, ConstrainedSubst<'tcx>> {
446 fn lift_delayed_literal(
448 _value: DelayedLiteral<ChalkArenas<'tcx>>,
449 ) -> DelayedLiteral<ChalkArenas<'gcx>> {
453 fn into_ex_clause(&mut self, _result: InferOk<'tcx, ()>, _ex_clause: &mut ChalkExClause<'tcx>) {
458 type ChalkHhGoal<'tcx> = HhGoal<ChalkArenas<'tcx>>;
460 type ChalkExClause<'tcx> = ExClause<ChalkArenas<'tcx>>;
462 impl Debug for ChalkContext<'cx, 'gcx> {
463 fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
464 write!(f, "ChalkContext")
468 impl Debug for ChalkInferenceContext<'cx, 'gcx, 'tcx> {
469 fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
470 write!(f, "ChalkInferenceContext")
474 impl ExClauseLift<'gcx> for ChalkArenas<'a> {
475 type LiftedExClause = ChalkExClause<'gcx>;
477 fn lift_ex_clause_to_tcx(
478 _ex_clause: &ChalkExClause<'a>,
479 _tcx: TyCtxt<'_, '_, 'tcx>,
480 ) -> Option<Self::LiftedExClause> {
485 impl ExClauseFold<'tcx> for ChalkArenas<'tcx> {
486 fn fold_ex_clause_with<'gcx: 'tcx, F: TypeFolder<'gcx, 'tcx>>(
487 ex_clause: &ChalkExClause<'tcx>,
489 ) -> ChalkExClause<'tcx> {
491 subst: ex_clause.subst.fold_with(folder),
492 delayed_literals: ex_clause.delayed_literals.fold_with(folder),
493 constraints: ex_clause.constraints.fold_with(folder),
494 subgoals: ex_clause.subgoals.fold_with(folder),
498 fn visit_ex_clause_with<'gcx: 'tcx, V: TypeVisitor<'tcx>>(
499 ex_clause: &ExClause<Self>,
508 subst.visit_with(visitor)
509 && delayed_literals.visit_with(visitor)
510 && constraints.visit_with(visitor)
511 && subgoals.visit_with(visitor)
515 BraceStructLiftImpl! {
516 impl<'a, 'tcx> Lift<'tcx> for ConstrainedSubst<'a> {
517 type Lifted = ConstrainedSubst<'tcx>;
523 impl<'gcx: 'tcx, 'tcx> Canonicalize<'gcx, 'tcx> for ConstrainedSubst<'tcx> {
524 type Canonicalized = Canonical<'gcx, ConstrainedSubst<'gcx>>;
527 _gcx: TyCtxt<'_, 'gcx, 'gcx>,
528 value: Canonical<'gcx, ConstrainedSubst<'gcx>>,
529 ) -> Self::Canonicalized {