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::{Canonical, CanonicalVarValues, QueryRegionConstraint, QueryResult};
  14 use rustc::infer::{InferCtxt, InferOk, LateBoundRegionConversionTime};
  15 use rustc::traits::{
  16     WellFormed,
  17     FromEnv,
  18     DomainGoal,
  19     ExClauseFold,
  20     ExClauseLift,
  21     Goal,
  22     ProgramClause,
  23     QuantifierKind
  24 };
  25 use rustc::ty::fold::{TypeFoldable, TypeFolder, TypeVisitor};
  26 use rustc::ty::subst::Kind;
  27 use rustc::ty::{self, TyCtxt};
  28 use smallvec::SmallVec;
  29
  30 use std::fmt::{self, Debug};
  31 use std::marker::PhantomData;
  32
  33 use syntax_pos::DUMMY_SP;
  34
  35 #[derive(Copy, Clone, Debug)]
  36 crate struct ChalkArenas<'gcx> {
  37     _phantom: PhantomData<&'gcx ()>,
  38 }
  39
  40 #[derive(Copy, Clone)]
  41 crate struct ChalkContext<'cx, 'gcx: 'cx> {
  42     _arenas: ChalkArenas<'gcx>,
  43     _tcx: TyCtxt<'cx, 'gcx, 'gcx>,
  44 }
  45
  46 #[derive(Copy, Clone)]
  47 crate struct ChalkInferenceContext<'cx, 'gcx: 'tcx, 'tcx: 'cx> {
  48     infcx: &'cx InferCtxt<'cx, 'gcx, 'tcx>,
  49 }
  50
  51 #[derive(Copy, Clone, Debug)]
  52 crate struct UniverseMap;
  53
  54 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
  55 crate struct ConstrainedSubst<'tcx> {
  56     subst: CanonicalVarValues<'tcx>,
  57     constraints: Vec<QueryRegionConstraint<'tcx>>,
  58 }
  59
  60 BraceStructTypeFoldableImpl! {
  61     impl<'tcx> TypeFoldable<'tcx> for ConstrainedSubst<'tcx> {
  62         subst, constraints
  63     }
  64 }
  65
  66 impl context::Context for ChalkArenas<'tcx> {
  67     type CanonicalExClause = Canonical<'tcx, ExClause<Self>>;
  68
  69     type CanonicalGoalInEnvironment = Canonical<'tcx, ty::ParamEnvAnd<'tcx, Goal<'tcx>>>;
  70
  71     // u-canonicalization not yet implemented
  72     type UCanonicalGoalInEnvironment = Canonical<'tcx, ty::ParamEnvAnd<'tcx, Goal<'tcx>>>;
  73
  74     type CanonicalConstrainedSubst = Canonical<'tcx, ConstrainedSubst<'tcx>>;
  75
  76     // u-canonicalization not yet implemented
  77     type UniverseMap = UniverseMap;
  78
  79     type Solution = Canonical<'tcx, QueryResult<'tcx, ()>>;
  80
  81     type InferenceNormalizedSubst = CanonicalVarValues<'tcx>;
  82
  83     type GoalInEnvironment = ty::ParamEnvAnd<'tcx, Goal<'tcx>>;
  84
  85     type RegionConstraint = QueryRegionConstraint<'tcx>;
  86
  87     type Substitution = CanonicalVarValues<'tcx>;
  88
  89     type Environment = ty::ParamEnv<'tcx>;
  90
  91     type Goal = Goal<'tcx>;
  92
  93     type DomainGoal = DomainGoal<'tcx>;
  94
  95     type BindersGoal = ty::Binder<&'tcx Goal<'tcx>>;
  96
  97     type Parameter = Kind<'tcx>;
  98
  99     type ProgramClause = ProgramClause<'tcx>;
 100
 101     type ProgramClauses = Vec<ProgramClause<'tcx>>;
 102
 103     type UnificationResult = InferOk<'tcx, ()>;
 104
 105     fn into_goal(domain_goal: DomainGoal<'tcx>) -> Goal<'tcx> {
 106         Goal::DomainGoal(domain_goal)
 107     }
 108
 109     fn cannot_prove() -> Goal<'tcx> {
 110         Goal::CannotProve
 111     }
 112
 113     fn goal_in_environment(
 114         env: &ty::ParamEnv<'tcx>,
 115         goal: Goal<'tcx>,
 116     ) -> ty::ParamEnvAnd<'tcx, Goal<'tcx>> {
 117         env.and(goal)
 118     }
 119 }
 120
 121 impl context::AggregateOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
 122     fn make_solution(
 123         &self,
 124         _root_goal: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
 125         _simplified_answers: impl context::AnswerStream<ChalkArenas<'gcx>>,
 126     ) -> Option<Canonical<'gcx, QueryResult<'gcx, ()>>> {
 127         unimplemented!()
 128     }
 129 }
 130
 131 impl context::ContextOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
 132     /// True if this is a coinductive goal -- e.g., proving an auto trait.
 133     fn is_coinductive(&self, _goal: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>) -> bool {
 134         unimplemented!()
 135     }
 136
 137     /// Create an inference table for processing a new goal and instantiate that goal
 138     /// in that context, returning "all the pieces".
 139     ///
 140     /// More specifically: given a u-canonical goal `arg`, creates a
 141     /// new inference table `T` and populates it with the universes
 142     /// found in `arg`. Then, creates a substitution `S` that maps
 143     /// each bound variable in `arg` to a fresh inference variable
 144     /// from T. Returns:
 145     ///
 146     /// - the table `T`
 147     /// - the substitution `S`
 148     /// - the environment and goal found by substitution `S` into `arg`
 149     fn instantiate_ucanonical_goal<R>(
 150         &self,
 151         _arg: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
 152         _op: impl context::WithInstantiatedUCanonicalGoal<ChalkArenas<'gcx>, Output = R>,
 153     ) -> R {
 154         unimplemented!()
 155     }
 156
 157     fn instantiate_ex_clause<R>(
 158         &self,
 159         _num_universes: usize,
 160         _canonical_ex_clause: &Canonical<'gcx, ChalkExClause<'gcx>>,
 161         _op: impl context::WithInstantiatedExClause<ChalkArenas<'gcx>, Output = R>,
 162     ) -> R {
 163         unimplemented!()
 164     }
 165
 166     /// True if this solution has no region constraints.
 167     fn empty_constraints(ccs: &Canonical<'gcx, ConstrainedSubst<'gcx>>) -> bool {
 168         ccs.value.constraints.is_empty()
 169     }
 170
 171     fn inference_normalized_subst_from_ex_clause(
 172         canon_ex_clause: &'a Canonical<'gcx, ChalkExClause<'gcx>>,
 173     ) -> &'a CanonicalVarValues<'gcx> {
 174         &canon_ex_clause.value.subst
 175     }
 176
 177     fn inference_normalized_subst_from_subst(
 178         canon_subst: &'a Canonical<'gcx, ConstrainedSubst<'gcx>>,
 179     ) -> &'a CanonicalVarValues<'gcx> {
 180         &canon_subst.value.subst
 181     }
 182
 183     fn canonical(
 184         u_canon: &'a Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
 185     ) -> &'a Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>> {
 186         u_canon
 187     }
 188
 189     fn is_trivial_substitution(
 190         _u_canon: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
 191         _canonical_subst: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
 192     ) -> bool {
 193         unimplemented!()
 194     }
 195
 196     fn num_universes(_: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>) -> usize {
 197         0 // FIXME
 198     }
 199
 200     /// Convert a goal G *from* the canonical universes *into* our
 201     /// local universes. This will yield a goal G' that is the same
 202     /// but for the universes of universally quantified names.
 203     fn map_goal_from_canonical(
 204         _map: &UniverseMap,
 205         value: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
 206     ) -> Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>> {
 207         *value // FIXME universe maps not implemented yet
 208     }
 209
 210     fn map_subst_from_canonical(
 211         _map: &UniverseMap,
 212         value: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
 213     ) -> Canonical<'gcx, ConstrainedSubst<'gcx>> {
 214         value.clone() // FIXME universe maps not implemented yet
 215     }
 216 }
 217
 218 //impl context::UCanonicalGoalInEnvironment<ChalkContext<'cx, 'gcx>>
 219 //    for Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>
 220 //{
 221 //    fn canonical(&self) -> &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>> {
 222 //        self
 223 //    }
 224 //
 225 //    fn is_trivial_substitution(
 226 //        &self,
 227 //        canonical_subst: &Canonical<'tcx, ConstrainedSubst<'tcx>>,
 228 //    ) -> bool {
 229 //        let subst = &canonical_subst.value.subst;
 230 //        assert_eq!(self.canonical.variables.len(), subst.var_values.len());
 231 //        subst
 232 //            .var_values
 233 //            .iter_enumerated()
 234 //            .all(|(cvar, kind)| match kind.unpack() {
 235 //                Kind::Lifetime(r) => match r {
 236 //                    ty::ReCanonical(cvar1) => cvar == cvar1,
 237 //                    _ => false,
 238 //                },
 239 //                Kind::Type(ty) => match ty.sty {
 240 //                    ty::Infer(ty::InferTy::CanonicalTy(cvar1)) => cvar == cvar1,
 241 //                    _ => false,
 242 //                },
 243 //            })
 244 //    }
 245 //
 246 //    fn num_universes(&self) -> usize {
 247 //        0 // FIXME
 248 //    }
 249 //}
 250
 251 impl context::InferenceTable<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
 252     for ChalkInferenceContext<'cx, 'gcx, 'tcx>
 253 {
 254     fn into_hh_goal(&mut self, goal: Goal<'tcx>) -> ChalkHhGoal<'tcx> {
 255         match goal {
 256             Goal::Implies(..) => panic!("FIXME rust-lang-nursery/chalk#94"),
 257             Goal::And(left, right) => HhGoal::And(*left, *right),
 258             Goal::Not(subgoal) => HhGoal::Not(*subgoal),
 259             Goal::DomainGoal(d) => HhGoal::DomainGoal(d),
 260             Goal::Quantified(QuantifierKind::Universal, binder) => HhGoal::ForAll(binder),
 261             Goal::Quantified(QuantifierKind::Existential, binder) => HhGoal::Exists(binder),
 262             Goal::CannotProve => HhGoal::CannotProve,
 263         }
 264     }
 265
 266     fn add_clauses(
 267         &mut self,
 268         _env: &ty::ParamEnv<'tcx>,
 269         _clauses: Vec<ProgramClause<'tcx>>,
 270     ) -> ty::ParamEnv<'tcx> {
 271         panic!("FIXME no method to add clauses to ParamEnv yet")
 272     }
 273 }
 274
 275 impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
 276     for ChalkInferenceContext<'cx, 'gcx, 'tcx>
 277 {
 278     fn resolvent_clause(
 279         &mut self,
 280         _environment: &ty::ParamEnv<'tcx>,
 281         _goal: &DomainGoal<'tcx>,
 282         _subst: &CanonicalVarValues<'tcx>,
 283         _clause: &ProgramClause<'tcx>,
 284     ) -> chalk_engine::fallible::Fallible<Canonical<'gcx, ChalkExClause<'gcx>>> {
 285         panic!()
 286     }
 287
 288     fn apply_answer_subst(
 289         &mut self,
 290         _ex_clause: ChalkExClause<'tcx>,
 291         _selected_goal: &ty::ParamEnvAnd<'tcx, Goal<'tcx>>,
 292         _answer_table_goal: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
 293         _canonical_answer_subst: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
 294     ) -> chalk_engine::fallible::Fallible<ChalkExClause<'tcx>> {
 295         panic!()
 296     }
 297 }
 298
 299 impl context::TruncateOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
 300     for ChalkInferenceContext<'cx, 'gcx, 'tcx>
 301 {
 302     fn truncate_goal(
 303         &mut self,
 304         subgoal: &ty::ParamEnvAnd<'tcx, Goal<'tcx>>,
 305     ) -> Option<ty::ParamEnvAnd<'tcx, Goal<'tcx>>> {
 306         Some(*subgoal) // FIXME we should truncate at some point!
 307     }
 308
 309     fn truncate_answer(
 310         &mut self,
 311         subst: &CanonicalVarValues<'tcx>,
 312     ) -> Option<CanonicalVarValues<'tcx>> {
 313         Some(subst.clone()) // FIXME we should truncate at some point!
 314     }
 315 }
 316
 317 impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
 318     for ChalkInferenceContext<'cx, 'gcx, 'tcx>
 319 {
 320     fn program_clauses(
 321         &self,
 322         _environment: &ty::ParamEnv<'tcx>,
 323         goal: &DomainGoal<'tcx>,
 324     ) -> Vec<ProgramClause<'tcx>> {
 325         use rustc::traits::WhereClause::*;
 326
 327         match goal {
 328             DomainGoal::Holds(Implemented(_trait_predicate)) => {
 329                 // These come from:
 330                 //
 331                 // - Trait definitions (implied bounds)
 332                 // - Implementations of the trait itself
 333                 panic!()
 334             }
 335
 336             DomainGoal::Holds(ProjectionEq(_projection_predicate)) => {
 337                 // These come from:
 338                 panic!()
 339             }
 340
 341             DomainGoal::Holds(RegionOutlives(_region_outlives)) => {
 342                 panic!()
 343             }
 344
 345             DomainGoal::Holds(TypeOutlives(_type_outlives)) => {
 346                 panic!()
 347             }
 348
 349             DomainGoal::WellFormed(WellFormed::Trait(_trait_predicate)) => {
 350                 // These come from -- the trait decl.
 351                 panic!()
 352             }
 353
 354             DomainGoal::WellFormed(WellFormed::Ty(_ty)) => panic!(),
 355
 356             DomainGoal::FromEnv(FromEnv::Trait(_trait_predicate)) => panic!(),
 357
 358             DomainGoal::FromEnv(FromEnv::Ty(_ty)) => panic!(),
 359
 360             DomainGoal::Normalize(_) => panic!(),
 361         }
 362     }
 363
 364     fn instantiate_binders_universally(
 365         &mut self,
 366         _arg: &ty::Binder<&'tcx Goal<'tcx>>,
 367     ) -> Goal<'tcx> {
 368         panic!("FIXME -- universal instantiation needs sgrif's branch")
 369     }
 370
 371     fn instantiate_binders_existentially(
 372         &mut self,
 373         arg: &ty::Binder<&'tcx Goal<'tcx>>,
 374     ) -> Goal<'tcx> {
 375         let (value, _map) = self.infcx.replace_late_bound_regions_with_fresh_var(
 376             DUMMY_SP,
 377             LateBoundRegionConversionTime::HigherRankedType,
 378             arg,
 379         );
 380         *value
 381     }
 382
 383     fn debug_ex_clause(&mut self, value: &'v ChalkExClause<'tcx>) -> Box<dyn Debug + 'v> {
 384         let string = format!("{:?}", self.infcx.resolve_type_vars_if_possible(value));
 385         Box::new(string)
 386     }
 387
 388     fn canonicalize_goal(
 389         &mut self,
 390         value: &ty::ParamEnvAnd<'tcx, Goal<'tcx>>,
 391     ) -> Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>> {
 392         let mut _orig_values = SmallVec::new();
 393         self.infcx.canonicalize_query(value, &mut _orig_values)
 394     }
 395
 396     fn canonicalize_ex_clause(
 397         &mut self,
 398         value: &ChalkExClause<'tcx>,
 399     ) -> Canonical<'gcx, ChalkExClause<'gcx>> {
 400         self.infcx.canonicalize_response(value)
 401     }
 402
 403     fn canonicalize_constrained_subst(
 404         &mut self,
 405         subst: CanonicalVarValues<'tcx>,
 406         constraints: Vec<QueryRegionConstraint<'tcx>>,
 407     ) -> Canonical<'gcx, ConstrainedSubst<'gcx>> {
 408         self.infcx.canonicalize_response(&ConstrainedSubst { subst, constraints })
 409     }
 410
 411     fn u_canonicalize_goal(
 412         &mut self,
 413         value: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
 414     ) -> (
 415         Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
 416         UniverseMap,
 417     ) {
 418         (value.clone(), UniverseMap)
 419     }
 420
 421     fn invert_goal(
 422         &mut self,
 423         _value: &ty::ParamEnvAnd<'tcx, Goal<'tcx>>,
 424     ) -> Option<ty::ParamEnvAnd<'tcx, Goal<'tcx>>> {
 425         panic!("goal inversion not yet implemented")
 426     }
 427
 428     fn unify_parameters(
 429         &mut self,
 430         _environment: &ty::ParamEnv<'tcx>,
 431         _a: &Kind<'tcx>,
 432         _b: &Kind<'tcx>,
 433     ) -> ChalkEngineFallible<InferOk<'tcx, ()>> {
 434         panic!()
 435     }
 436
 437     fn sink_answer_subset(
 438         &self,
 439         value: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
 440     ) -> Canonical<'tcx, ConstrainedSubst<'tcx>> {
 441         value.clone()
 442     }
 443
 444     fn lift_delayed_literal(
 445         &self,
 446         _value: DelayedLiteral<ChalkArenas<'tcx>>,
 447     ) -> DelayedLiteral<ChalkArenas<'gcx>> {
 448         panic!("lift")
 449     }
 450
 451     fn into_ex_clause(&mut self, _result: InferOk<'tcx, ()>, _ex_clause: &mut ChalkExClause<'tcx>) {
 452         panic!("TBD")
 453     }
 454 }
 455
 456 type ChalkHhGoal<'tcx> = HhGoal<ChalkArenas<'tcx>>;
 457
 458 type ChalkExClause<'tcx> = ExClause<ChalkArenas<'tcx>>;
 459
 460 impl Debug for ChalkContext<'cx, 'gcx> {
 461     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
 462         write!(f, "ChalkContext")
 463     }
 464 }
 465
 466 impl Debug for ChalkInferenceContext<'cx, 'gcx, 'tcx> {
 467     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
 468         write!(f, "ChalkInferenceContext")
 469     }
 470 }
 471
 472 impl ExClauseLift<'gcx> for ChalkArenas<'a> {
 473     type LiftedExClause = ChalkExClause<'gcx>;
 474
 475     fn lift_ex_clause_to_tcx(
 476         _ex_clause: &ChalkExClause<'a>,
 477         _tcx: TyCtxt<'_, '_, 'tcx>,
 478     ) -> Option<Self::LiftedExClause> {
 479         panic!()
 480     }
 481 }
 482
 483 impl ExClauseFold<'tcx> for ChalkArenas<'tcx> {
 484     fn fold_ex_clause_with<'gcx: 'tcx, F: TypeFolder<'gcx, 'tcx>>(
 485         ex_clause: &ChalkExClause<'tcx>,
 486         folder: &mut F,
 487     ) -> ChalkExClause<'tcx> {
 488         ExClause {
 489             subst: ex_clause.subst.fold_with(folder),
 490             delayed_literals: ex_clause.delayed_literals.fold_with(folder),
 491             constraints: ex_clause.constraints.fold_with(folder),
 492             subgoals: ex_clause.subgoals.fold_with(folder),
 493         }
 494     }
 495
 496     fn visit_ex_clause_with<'gcx: 'tcx, V: TypeVisitor<'tcx>>(
 497         ex_clause: &ExClause<Self>,
 498         visitor: &mut V,
 499     ) -> bool {
 500         let ExClause {
 501             subst,
 502             delayed_literals,
 503             constraints,
 504             subgoals,
 505         } = ex_clause;
 506         subst.visit_with(visitor)
 507             && delayed_literals.visit_with(visitor)
 508             && constraints.visit_with(visitor)
 509             && subgoals.visit_with(visitor)
 510     }
 511 }
 512
 513 BraceStructLiftImpl! {
 514     impl<'a, 'tcx> Lift<'tcx> for ConstrainedSubst<'a> {
 515         type Lifted = ConstrainedSubst<'tcx>;
 516
 517         subst, constraints
 518     }
 519 }