src/librustc_traits/chalk_context.rs

   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.
   4 //
   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.
  10
  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, OriginalQueryValues, QueryRegionConstraint, QueryResponse,
  15 };
  16 use rustc::infer::{InferCtxt, InferOk, LateBoundRegionConversionTime};
  17 use rustc::traits::{
  18     WellFormed,
  19     FromEnv,
  20     DomainGoal,
  21     ExClauseFold,
  22     ExClauseLift,
  23     Goal,
  24     GoalKind,
  25     Clause,
  26     ProgramClauseCategory,
  27     QuantifierKind,
  28     Environment,
  29     InEnvironment,
  30 };
  31 use rustc::ty::fold::{TypeFoldable, TypeFolder, TypeVisitor};
  32 use rustc::ty::subst::Kind;
  33 use rustc::ty::{self, TyCtxt};
  34 use rustc::hir::def_id::DefId;
  35
  36 use std::fmt::{self, Debug};
  37 use std::marker::PhantomData;
  38
  39 use syntax_pos::DUMMY_SP;
  40
  41 #[derive(Copy, Clone, Debug)]
  42 crate struct ChalkArenas<'gcx> {
  43     _phantom: PhantomData<&'gcx ()>,
  44 }
  45
  46 #[derive(Copy, Clone)]
  47 crate struct ChalkContext<'cx, 'gcx: 'cx> {
  48     _arenas: ChalkArenas<'gcx>,
  49     _tcx: TyCtxt<'cx, 'gcx, 'gcx>,
  50 }
  51
  52 #[derive(Copy, Clone)]
  53 crate struct ChalkInferenceContext<'cx, 'gcx: 'tcx, 'tcx: 'cx> {
  54     infcx: &'cx InferCtxt<'cx, 'gcx, 'tcx>,
  55 }
  56
  57 #[derive(Copy, Clone, Debug)]
  58 crate struct UniverseMap;
  59
  60 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
  61 crate struct ConstrainedSubst<'tcx> {
  62     subst: CanonicalVarValues<'tcx>,
  63     constraints: Vec<QueryRegionConstraint<'tcx>>,
  64 }
  65
  66 BraceStructTypeFoldableImpl! {
  67     impl<'tcx> TypeFoldable<'tcx> for ConstrainedSubst<'tcx> {
  68         subst, constraints
  69     }
  70 }
  71
  72 impl context::Context for ChalkArenas<'tcx> {
  73     type CanonicalExClause = Canonical<'tcx, ExClause<Self>>;
  74
  75     type CanonicalGoalInEnvironment = Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>>;
  76
  77     // u-canonicalization not yet implemented
  78     type UCanonicalGoalInEnvironment = Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>>;
  79
  80     type CanonicalConstrainedSubst = Canonical<'tcx, ConstrainedSubst<'tcx>>;
  81
  82     // u-canonicalization not yet implemented
  83     type UniverseMap = UniverseMap;
  84
  85     type Solution = Canonical<'tcx, QueryResponse<'tcx, ()>>;
  86
  87     type InferenceNormalizedSubst = CanonicalVarValues<'tcx>;
  88
  89     type GoalInEnvironment = InEnvironment<'tcx, Goal<'tcx>>;
  90
  91     type RegionConstraint = QueryRegionConstraint<'tcx>;
  92
  93     type Substitution = CanonicalVarValues<'tcx>;
  94
  95     type Environment = Environment<'tcx>;
  96
  97     type Goal = Goal<'tcx>;
  98
  99     type DomainGoal = DomainGoal<'tcx>;
 100
 101     type BindersGoal = ty::Binder<Goal<'tcx>>;
 102
 103     type Parameter = Kind<'tcx>;
 104
 105     type ProgramClause = Clause<'tcx>;
 106
 107     type ProgramClauses = Vec<Clause<'tcx>>;
 108
 109     type UnificationResult = InferOk<'tcx, ()>;
 110
 111     fn goal_in_environment(
 112         env: &Environment<'tcx>,
 113         goal: Goal<'tcx>,
 114     ) -> InEnvironment<'tcx, Goal<'tcx>> {
 115         env.with(goal)
 116     }
 117 }
 118
 119 impl context::AggregateOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
 120     fn make_solution(
 121         &self,
 122         _root_goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
 123         _simplified_answers: impl context::AnswerStream<ChalkArenas<'gcx>>,
 124     ) -> Option<Canonical<'gcx, QueryResponse<'gcx, ()>>> {
 125         unimplemented!()
 126     }
 127 }
 128
 129 impl context::ContextOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
 130     /// True if this is a coinductive goal -- e.g., proving an auto trait.
 131     fn is_coinductive(
 132         &self,
 133         _goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>
 134     ) -> bool {
 135         unimplemented!()
 136     }
 137
 138     /// Create an inference table for processing a new goal and instantiate that goal
 139     /// in that context, returning "all the pieces".
 140     ///
 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
 145     /// from T. Returns:
 146     ///
 147     /// - the table `T`
 148     /// - the substitution `S`
 149     /// - the environment and goal found by substitution `S` into `arg`
 150     fn instantiate_ucanonical_goal<R>(
 151         &self,
 152         _arg: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
 153         _op: impl context::WithInstantiatedUCanonicalGoal<ChalkArenas<'gcx>, Output = R>,
 154     ) -> R {
 155         unimplemented!()
 156     }
 157
 158     fn instantiate_ex_clause<R>(
 159         &self,
 160         _num_universes: usize,
 161         _canonical_ex_clause: &Canonical<'gcx, ChalkExClause<'gcx>>,
 162         _op: impl context::WithInstantiatedExClause<ChalkArenas<'gcx>, Output = R>,
 163     ) -> R {
 164         unimplemented!()
 165     }
 166
 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()
 170     }
 171
 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
 176     }
 177
 178     fn inference_normalized_subst_from_subst(
 179         canon_subst: &'a Canonical<'gcx, ConstrainedSubst<'gcx>>,
 180     ) -> &'a CanonicalVarValues<'gcx> {
 181         &canon_subst.value.subst
 182     }
 183
 184     fn canonical(
 185         u_canon: &'a Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
 186     ) -> &'a Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>> {
 187         u_canon
 188     }
 189
 190     fn is_trivial_substitution(
 191         _u_canon: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
 192         _canonical_subst: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
 193     ) -> bool {
 194         unimplemented!()
 195     }
 196
 197     fn num_universes(_: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>) -> usize {
 198         0 // FIXME
 199     }
 200
 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(
 205         _map: &UniverseMap,
 206         value: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
 207     ) -> Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>> {
 208         *value // FIXME universe maps not implemented yet
 209     }
 210
 211     fn map_subst_from_canonical(
 212         _map: &UniverseMap,
 213         value: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
 214     ) -> Canonical<'gcx, ConstrainedSubst<'gcx>> {
 215         value.clone() // FIXME universe maps not implemented yet
 216     }
 217 }
 218
 219 //impl context::UCanonicalGoalInEnvironment<ChalkContext<'cx, 'gcx>>
 220 //    for Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>
 221 //{
 222 //    fn canonical(&self) -> &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>> {
 223 //        self
 224 //    }
 225 //
 226 //    fn is_trivial_substitution(
 227 //        &self,
 228 //        canonical_subst: &Canonical<'tcx, ConstrainedSubst<'tcx>>,
 229 //    ) -> bool {
 230 //        let subst = &canonical_subst.value.subst;
 231 //        assert_eq!(self.canonical.variables.len(), subst.var_values.len());
 232 //        subst
 233 //            .var_values
 234 //            .iter_enumerated()
 235 //            .all(|(cvar, kind)| match kind.unpack() {
 236 //                Kind::Lifetime(r) => match r {
 237 //                    ty::ReCanonical(cvar1) => cvar == cvar1,
 238 //                    _ => false,
 239 //                },
 240 //                Kind::Type(ty) => match ty.sty {
 241 //                    ty::Infer(ty::InferTy::CanonicalTy(cvar1)) => cvar == cvar1,
 242 //                    _ => false,
 243 //                },
 244 //            })
 245 //    }
 246 //
 247 //    fn num_universes(&self) -> usize {
 248 //        0 // FIXME
 249 //    }
 250 //}
 251
 252 impl context::InferenceTable<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
 253     for ChalkInferenceContext<'cx, 'gcx, 'tcx>
 254 {
 255     fn into_goal(&self, domain_goal: DomainGoal<'tcx>) -> Goal<'tcx> {
 256         self.infcx.tcx.mk_goal(GoalKind::DomainGoal(domain_goal))
 257     }
 258
 259     fn cannot_prove(&self) -> Goal<'tcx> {
 260         self.infcx.tcx.mk_goal(GoalKind::CannotProve)
 261     }
 262
 263     fn into_hh_goal(&mut self, goal: Goal<'tcx>) -> ChalkHhGoal<'tcx> {
 264         match *goal {
 265             GoalKind::Implies(..) => panic!("FIXME rust-lang-nursery/chalk#94"),
 266             GoalKind::And(left, right) => HhGoal::And(left, right),
 267             GoalKind::Not(subgoal) => HhGoal::Not(subgoal),
 268             GoalKind::DomainGoal(d) => HhGoal::DomainGoal(d),
 269             GoalKind::Quantified(QuantifierKind::Universal, binder) => HhGoal::ForAll(binder),
 270             GoalKind::Quantified(QuantifierKind::Existential, binder) => HhGoal::Exists(binder),
 271             GoalKind::CannotProve => HhGoal::CannotProve,
 272         }
 273     }
 274
 275     fn add_clauses(
 276         &mut self,
 277         env: &Environment<'tcx>,
 278         clauses: Vec<Clause<'tcx>>,
 279     ) -> Environment<'tcx> {
 280         Environment {
 281             clauses: self.infcx.tcx.mk_clauses(
 282                 env.clauses.iter().cloned().chain(clauses.into_iter())
 283             )
 284         }
 285     }
 286 }
 287
 288 impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
 289     for ChalkInferenceContext<'cx, 'gcx, 'tcx>
 290 {
 291     fn resolvent_clause(
 292         &mut self,
 293         _environment: &Environment<'tcx>,
 294         _goal: &DomainGoal<'tcx>,
 295         _subst: &CanonicalVarValues<'tcx>,
 296         _clause: &Clause<'tcx>,
 297     ) -> chalk_engine::fallible::Fallible<Canonical<'gcx, ChalkExClause<'gcx>>> {
 298         panic!()
 299     }
 300
 301     fn apply_answer_subst(
 302         &mut self,
 303         _ex_clause: ChalkExClause<'tcx>,
 304         _selected_goal: &InEnvironment<'tcx, Goal<'tcx>>,
 305         _answer_table_goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
 306         _canonical_answer_subst: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
 307     ) -> chalk_engine::fallible::Fallible<ChalkExClause<'tcx>> {
 308         panic!()
 309     }
 310 }
 311
 312 impl context::TruncateOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
 313     for ChalkInferenceContext<'cx, 'gcx, 'tcx>
 314 {
 315     fn truncate_goal(
 316         &mut self,
 317         subgoal: &InEnvironment<'tcx, Goal<'tcx>>,
 318     ) -> Option<InEnvironment<'tcx, Goal<'tcx>>> {
 319         Some(*subgoal) // FIXME we should truncate at some point!
 320     }
 321
 322     fn truncate_answer(
 323         &mut self,
 324         subst: &CanonicalVarValues<'tcx>,
 325     ) -> Option<CanonicalVarValues<'tcx>> {
 326         Some(subst.clone()) // FIXME we should truncate at some point!
 327     }
 328 }
 329
 330 impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
 331     for ChalkInferenceContext<'cx, 'gcx, 'tcx>
 332 {
 333     fn program_clauses(
 334         &self,
 335         environment: &Environment<'tcx>,
 336         goal: &DomainGoal<'tcx>,
 337     ) -> Vec<Clause<'tcx>> {
 338         use rustc::traits::WhereClause::*;
 339
 340         fn assemble_clauses_from_impls<'tcx>(
 341             tcx: ty::TyCtxt<'_, '_, 'tcx>,
 342             trait_def_id: DefId,
 343             clauses: &mut Vec<Clause<'tcx>>
 344         ) {
 345             tcx.for_each_impl(trait_def_id, |impl_def_id| {
 346                 clauses.extend(
 347                     tcx.program_clauses_for(impl_def_id)
 348                         .into_iter()
 349                         .cloned()
 350                 );
 351             });
 352         }
 353
 354         fn assemble_clauses_from_assoc_ty_values<'tcx>(
 355             tcx: ty::TyCtxt<'_, '_, 'tcx>,
 356             trait_def_id: DefId,
 357             clauses: &mut Vec<Clause<'tcx>>
 358         ) {
 359             tcx.for_each_impl(trait_def_id, |impl_def_id| {
 360                 for def_id in tcx.associated_item_def_ids(impl_def_id).iter() {
 361                     clauses.extend(
 362                         tcx.program_clauses_for(*def_id)
 363                             .into_iter()
 364                             .cloned()
 365                     );
 366                 }
 367             });
 368         }
 369
 370         let mut clauses = match goal {
 371             DomainGoal::Holds(Implemented(trait_predicate)) => {
 372                 // These come from:
 373                 // * implementations of the trait itself (rule `Implemented-From-Impl`)
 374                 // * the trait decl (rule `Implemented-From-Env`)
 375
 376                 let mut clauses = vec![];
 377                 assemble_clauses_from_impls(
 378                     self.infcx.tcx,
 379                     trait_predicate.def_id(),
 380                     &mut clauses
 381                 );
 382
 383                 // FIXME: we need to add special rules for builtin impls:
 384                 // * `Copy` / `Clone`
 385                 // * `Sized`
 386                 // * `Unsize`
 387                 // * `Generator`
 388                 // * `FnOnce` / `FnMut` / `Fn`
 389                 // * trait objects
 390                 // * auto traits
 391
 392                 // Rule `Implemented-From-Env` will be computed from the environment.
 393                 clauses
 394             }
 395
 396             DomainGoal::Holds(ProjectionEq(projection_predicate)) => {
 397                 // These come from:
 398                 // * the assoc type definition (rule `ProjectionEq-Placeholder`)
 399                 // * normalization of the assoc ty values (rule `ProjectionEq-Normalize`)
 400                 // * implied bounds from trait definitions (rule `Implied-Bound-From-Trait`)
 401                 // * implied bounds from type definitions (rule `Implied-Bound-From-Type`)
 402
 403                 let clauses = self.infcx.tcx.program_clauses_for(
 404                     projection_predicate.projection_ty.item_def_id
 405                 ).into_iter()
 406
 407                     // only select `ProjectionEq-Placeholder` and `ProjectionEq-Normalize`
 408                     .filter(|clause| clause.category() == ProgramClauseCategory::Other)
 409
 410                     .cloned()
 411                     .collect::<Vec<_>>();
 412
 413                 // Rules `Implied-Bound-From-Trait` and `Implied-Bound-From-Type` will be computed
 414                 // from the environment.
 415                 clauses
 416             }
 417
 418             DomainGoal::Holds(RegionOutlives(..)) => {
 419                 // These come from:
 420                 // * implied bounds from trait definitions (rule `Implied-Bound-From-Trait`)
 421                 // * implied bounds from type definitions (rule `Implied-Bound-From-Type`)
 422
 423                 // All of these rules are computed in the environment.
 424                 vec![]
 425             }
 426
 427             DomainGoal::Holds(TypeOutlives(..)) => {
 428                 // These come from:
 429                 // * implied bounds from trait definitions (rule `Implied-Bound-From-Trait`)
 430                 // * implied bounds from type definitions (rule `Implied-Bound-From-Type`)
 431
 432                 // All of these rules are computed in the environment.
 433                 vec![]
 434             }
 435
 436             DomainGoal::WellFormed(WellFormed::Trait(trait_predicate)) => {
 437                 // These come from -- the trait decl (rule `WellFormed-TraitRef`).
 438                 self.infcx.tcx.program_clauses_for(trait_predicate.def_id())
 439                     .into_iter()
 440
 441                     // only select `WellFormed-TraitRef`
 442                     .filter(|clause| clause.category() == ProgramClauseCategory::WellFormed)
 443
 444                     .cloned()
 445                     .collect()
 446             }
 447
 448             DomainGoal::WellFormed(WellFormed::Ty(ty)) => {
 449                 // These come from:
 450                 // * the associated type definition if `ty` refers to an unnormalized
 451                 //   associated type (rule `WellFormed-AssocTy`)
 452                 // * custom rules for built-in types
 453                 // * the type definition otherwise (rule `WellFormed-Type`)
 454                 let clauses = match ty.sty {
 455                     ty::Projection(data) => {
 456                         self.infcx.tcx.program_clauses_for(data.item_def_id)
 457                     }
 458
 459                     // These types are always WF (recall that we do not check
 460                     // for parameters to be WF)
 461                     ty::Bool |
 462                     ty::Char |
 463                     ty::Int(..) |
 464                     ty::Uint(..) |
 465                     ty::Float(..) |
 466                     ty::Str |
 467                     ty::RawPtr(..) |
 468                     ty::FnPtr(..) |
 469                     ty::Param(..) |
 470                     ty::Never => {
 471                         ty::List::empty()
 472                     }
 473
 474                     // WF if inner type is `Sized`
 475                     ty::Slice(..) |
 476                     ty::Array(..) => {
 477                         ty::List::empty()
 478                     }
 479
 480                     ty::Tuple(..) => {
 481                         ty::List::empty()
 482                     }
 483
 484                     // WF if `sub_ty` outlives `region`
 485                     ty::Ref(..) => {
 486                         ty::List::empty()
 487                     }
 488
 489                     ty::Dynamic(..) => {
 490                         // FIXME: no rules yet for trait objects
 491                         ty::List::empty()
 492                     }
 493
 494                     ty::Adt(def, ..) => {
 495                         self.infcx.tcx.program_clauses_for(def.did)
 496                     }
 497
 498                     ty::Foreign(def_id) |
 499                     ty::FnDef(def_id, ..) |
 500                     ty::Closure(def_id, ..) |
 501                     ty::Generator(def_id, ..) |
 502                     ty::Opaque(def_id, ..) => {
 503                         self.infcx.tcx.program_clauses_for(def_id)
 504                     }
 505
 506                     ty::GeneratorWitness(..) |
 507                     ty::UnnormalizedProjection(..) |
 508                     ty::Infer(..) |
 509                     ty::Bound(..) |
 510                     ty::Error => {
 511                         bug!("unexpected type {:?}", ty)
 512                     }
 513                 };
 514
 515                 clauses.into_iter()
 516                     .filter(|clause| clause.category() == ProgramClauseCategory::WellFormed)
 517                     .cloned()
 518                     .collect()
 519             }
 520
 521             DomainGoal::FromEnv(FromEnv::Trait(..)) => {
 522                 // These come from:
 523                 // * implied bounds from trait definitions (rule `Implied-Bound-From-Trait`)
 524                 // * implied bounds from type definitions (rule `Implied-Bound-From-Type`)
 525                 // * implied bounds from assoc type defs (rules `Implied-Trait-From-AssocTy`,
 526                 //   `Implied-Bound-From-AssocTy` and `Implied-WC-From-AssocTy`)
 527
 528                 // All of these rules are computed in the environment.
 529                 vec![]
 530             }
 531
 532             DomainGoal::FromEnv(FromEnv::Ty(..)) => {
 533                 // There are no `FromEnv::Ty(..) :- ...` rules (this predicate only
 534                 // comes from the environment).
 535                 vec![]
 536             }
 537
 538             DomainGoal::Normalize(projection_predicate) => {
 539                 // These come from -- assoc ty values (rule `Normalize-From-Impl`).
 540                 let mut clauses = vec![];
 541
 542                 assemble_clauses_from_assoc_ty_values(
 543                     self.infcx.tcx,
 544                     projection_predicate.projection_ty.trait_ref(self.infcx.tcx).def_id,
 545                     &mut clauses
 546                 );
 547
 548                 clauses
 549             }
 550         };
 551
 552         let environment = self.infcx.tcx.lift_to_global(environment)
 553             .expect("environment is not global");
 554         clauses.extend(
 555             self.infcx.tcx.program_clauses_for_env(environment)
 556                 .into_iter()
 557                 .cloned()
 558         );
 559         clauses
 560     }
 561
 562     fn instantiate_binders_universally(
 563         &mut self,
 564         _arg: &ty::Binder<Goal<'tcx>>,
 565     ) -> Goal<'tcx> {
 566         panic!("FIXME -- universal instantiation needs sgrif's branch")
 567     }
 568
 569     fn instantiate_binders_existentially(
 570         &mut self,
 571         arg: &ty::Binder<Goal<'tcx>>,
 572     ) -> Goal<'tcx> {
 573         let (value, _map) = self.infcx.replace_late_bound_regions_with_fresh_var(
 574             DUMMY_SP,
 575             LateBoundRegionConversionTime::HigherRankedType,
 576             arg,
 577         );
 578         value
 579     }
 580
 581     fn debug_ex_clause(&mut self, value: &'v ChalkExClause<'tcx>) -> Box<dyn Debug + 'v> {
 582         let string = format!("{:?}", self.infcx.resolve_type_vars_if_possible(value));
 583         Box::new(string)
 584     }
 585
 586     fn canonicalize_goal(
 587         &mut self,
 588         value: &InEnvironment<'tcx, Goal<'tcx>>,
 589     ) -> Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>> {
 590         let mut _orig_values = OriginalQueryValues::default();
 591         self.infcx.canonicalize_query(value, &mut _orig_values)
 592     }
 593
 594     fn canonicalize_ex_clause(
 595         &mut self,
 596         value: &ChalkExClause<'tcx>,
 597     ) -> Canonical<'gcx, ChalkExClause<'gcx>> {
 598         self.infcx.canonicalize_response(value)
 599     }
 600
 601     fn canonicalize_constrained_subst(
 602         &mut self,
 603         subst: CanonicalVarValues<'tcx>,
 604         constraints: Vec<QueryRegionConstraint<'tcx>>,
 605     ) -> Canonical<'gcx, ConstrainedSubst<'gcx>> {
 606         self.infcx.canonicalize_response(&ConstrainedSubst { subst, constraints })
 607     }
 608
 609     fn u_canonicalize_goal(
 610         &mut self,
 611         value: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
 612     ) -> (
 613         Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
 614         UniverseMap,
 615     ) {
 616         (value.clone(), UniverseMap)
 617     }
 618
 619     fn invert_goal(
 620         &mut self,
 621         _value: &InEnvironment<'tcx, Goal<'tcx>>,
 622     ) -> Option<InEnvironment<'tcx, Goal<'tcx>>> {
 623         panic!("goal inversion not yet implemented")
 624     }
 625
 626     fn unify_parameters(
 627         &mut self,
 628         _environment: &Environment<'tcx>,
 629         _a: &Kind<'tcx>,
 630         _b: &Kind<'tcx>,
 631     ) -> ChalkEngineFallible<InferOk<'tcx, ()>> {
 632         panic!()
 633     }
 634
 635     fn sink_answer_subset(
 636         &self,
 637         value: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
 638     ) -> Canonical<'tcx, ConstrainedSubst<'tcx>> {
 639         value.clone()
 640     }
 641
 642     fn lift_delayed_literal(
 643         &self,
 644         _value: DelayedLiteral<ChalkArenas<'tcx>>,
 645     ) -> DelayedLiteral<ChalkArenas<'gcx>> {
 646         panic!("lift")
 647     }
 648
 649     fn into_ex_clause(&mut self, _result: InferOk<'tcx, ()>, _ex_clause: &mut ChalkExClause<'tcx>) {
 650         panic!("TBD")
 651     }
 652 }
 653
 654 type ChalkHhGoal<'tcx> = HhGoal<ChalkArenas<'tcx>>;
 655
 656 type ChalkExClause<'tcx> = ExClause<ChalkArenas<'tcx>>;
 657
 658 impl Debug for ChalkContext<'cx, 'gcx> {
 659     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
 660         write!(f, "ChalkContext")
 661     }
 662 }
 663
 664 impl Debug for ChalkInferenceContext<'cx, 'gcx, 'tcx> {
 665     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
 666         write!(f, "ChalkInferenceContext")
 667     }
 668 }
 669
 670 impl ExClauseLift<'gcx> for ChalkArenas<'a> {
 671     type LiftedExClause = ChalkExClause<'gcx>;
 672
 673     fn lift_ex_clause_to_tcx(
 674         _ex_clause: &ChalkExClause<'a>,
 675         _tcx: TyCtxt<'_, '_, 'tcx>,
 676     ) -> Option<Self::LiftedExClause> {
 677         panic!()
 678     }
 679 }
 680
 681 impl ExClauseFold<'tcx> for ChalkArenas<'tcx> {
 682     fn fold_ex_clause_with<'gcx: 'tcx, F: TypeFolder<'gcx, 'tcx>>(
 683         ex_clause: &ChalkExClause<'tcx>,
 684         folder: &mut F,
 685     ) -> ChalkExClause<'tcx> {
 686         ExClause {
 687             subst: ex_clause.subst.fold_with(folder),
 688             delayed_literals: ex_clause.delayed_literals.fold_with(folder),
 689             constraints: ex_clause.constraints.fold_with(folder),
 690             subgoals: ex_clause.subgoals.fold_with(folder),
 691         }
 692     }
 693
 694     fn visit_ex_clause_with<'gcx: 'tcx, V: TypeVisitor<'tcx>>(
 695         ex_clause: &ExClause<Self>,
 696         visitor: &mut V,
 697     ) -> bool {
 698         let ExClause {
 699             subst,
 700             delayed_literals,
 701             constraints,
 702             subgoals,
 703         } = ex_clause;
 704         subst.visit_with(visitor)
 705             && delayed_literals.visit_with(visitor)
 706             && constraints.visit_with(visitor)
 707             && subgoals.visit_with(visitor)
 708     }
 709 }
 710
 711 BraceStructLiftImpl! {
 712     impl<'a, 'tcx> Lift<'tcx> for ConstrainedSubst<'a> {
 713         type Lifted = ConstrainedSubst<'tcx>;
 714
 715         subst, constraints
 716     }
 717 }