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, Canonicalize, QueryRegionConstraint, QueryResult,
  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     ProgramClause,
  25     QuantifierKind
  26 };
  27 use rustc::ty::fold::{TypeFoldable, TypeFolder, TypeVisitor};
  28 use rustc::ty::subst::Kind;
  29 use rustc::ty::{self, TyCtxt};
  30
  31 use std::fmt::{self, Debug};
  32 use std::marker::PhantomData;
  33
  34 use syntax_pos::DUMMY_SP;
  35
  36 #[derive(Copy, Clone, Debug)]
  37 crate struct ChalkArenas<'gcx> {
  38     _phantom: PhantomData<&'gcx ()>,
  39 }
  40
  41 #[derive(Copy, Clone)]
  42 crate struct ChalkContext<'cx, 'gcx: 'cx> {
  43     _arenas: ChalkArenas<'gcx>,
  44     _tcx: TyCtxt<'cx, 'gcx, 'gcx>,
  45 }
  46
  47 #[derive(Copy, Clone)]
  48 crate struct ChalkInferenceContext<'cx, 'gcx: 'tcx, 'tcx: 'cx> {
  49     infcx: &'cx InferCtxt<'cx, 'gcx, 'tcx>,
  50 }
  51
  52 #[derive(Copy, Clone, Debug)]
  53 crate struct UniverseMap;
  54
  55 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
  56 crate struct ConstrainedSubst<'tcx> {
  57     subst: CanonicalVarValues<'tcx>,
  58     constraints: Vec<QueryRegionConstraint<'tcx>>,
  59 }
  60
  61 BraceStructTypeFoldableImpl! {
  62     impl<'tcx> TypeFoldable<'tcx> for ConstrainedSubst<'tcx> {
  63         subst, constraints
  64     }
  65 }
  66
  67 impl context::Context for ChalkArenas<'tcx> {
  68     type CanonicalExClause = Canonical<'tcx, ExClause<Self>>;
  69
  70     type CanonicalGoalInEnvironment = Canonical<'tcx, ty::ParamEnvAnd<'tcx, Goal<'tcx>>>;
  71
  72     // u-canonicalization not yet implemented
  73     type UCanonicalGoalInEnvironment = Canonical<'tcx, ty::ParamEnvAnd<'tcx, Goal<'tcx>>>;
  74
  75     type CanonicalConstrainedSubst = Canonical<'tcx, ConstrainedSubst<'tcx>>;
  76
  77     // u-canonicalization not yet implemented
  78     type UniverseMap = UniverseMap;
  79
  80     type Solution = Canonical<'tcx, QueryResult<'tcx, ()>>;
  81
  82     type InferenceNormalizedSubst = CanonicalVarValues<'tcx>;
  83
  84     type GoalInEnvironment = ty::ParamEnvAnd<'tcx, Goal<'tcx>>;
  85
  86     type RegionConstraint = QueryRegionConstraint<'tcx>;
  87
  88     type Substitution = CanonicalVarValues<'tcx>;
  89
  90     type Environment = ty::ParamEnv<'tcx>;
  91
  92     type Goal = Goal<'tcx>;
  93
  94     type DomainGoal = DomainGoal<'tcx>;
  95
  96     type BindersGoal = ty::Binder<&'tcx Goal<'tcx>>;
  97
  98     type Parameter = Kind<'tcx>;
  99
 100     type ProgramClause = ProgramClause<'tcx>;
 101
 102     type ProgramClauses = Vec<ProgramClause<'tcx>>;
 103
 104     type UnificationResult = InferOk<'tcx, ()>;
 105
 106     fn into_goal(domain_goal: DomainGoal<'tcx>) -> Goal<'tcx> {
 107         Goal::DomainGoal(domain_goal)
 108     }
 109
 110     fn cannot_prove() -> Goal<'tcx> {
 111         Goal::CannotProve
 112     }
 113
 114     fn goal_in_environment(
 115         env: &ty::ParamEnv<'tcx>,
 116         goal: Goal<'tcx>,
 117     ) -> ty::ParamEnvAnd<'tcx, Goal<'tcx>> {
 118         env.and(goal)
 119     }
 120 }
 121
 122 impl context::AggregateOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
 123     fn make_solution(
 124         &self,
 125         _root_goal: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
 126         _simplified_answers: impl context::AnswerStream<ChalkArenas<'gcx>>,
 127     ) -> Option<Canonical<'gcx, QueryResult<'gcx, ()>>> {
 128         unimplemented!()
 129     }
 130 }
 131
 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 {
 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, ty::ParamEnvAnd<'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, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
 186     ) -> &'a Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>> {
 187         u_canon
 188     }
 189
 190     fn is_trivial_substitution(
 191         _u_canon: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
 192         _canonical_subst: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
 193     ) -> bool {
 194         unimplemented!()
 195     }
 196
 197     fn num_universes(_: &Canonical<'gcx, ty::ParamEnvAnd<'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, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
 207     ) -> Canonical<'gcx, ty::ParamEnvAnd<'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::TyInfer(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_hh_goal(&mut self, goal: Goal<'tcx>) -> ChalkHhGoal<'tcx> {
 256         match goal {
 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,
 264         }
 265     }
 266
 267     fn add_clauses(
 268         &mut self,
 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")
 273     }
 274 }
 275
 276 impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
 277     for ChalkInferenceContext<'cx, 'gcx, 'tcx>
 278 {
 279     fn resolvent_clause(
 280         &mut self,
 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>>> {
 286         panic!()
 287     }
 288
 289     fn apply_answer_subst(
 290         &mut self,
 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>> {
 296         panic!()
 297     }
 298 }
 299
 300 impl context::TruncateOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
 301     for ChalkInferenceContext<'cx, 'gcx, 'tcx>
 302 {
 303     fn truncate_goal(
 304         &mut self,
 305         subgoal: &ty::ParamEnvAnd<'tcx, Goal<'tcx>>,
 306     ) -> Option<ty::ParamEnvAnd<'tcx, Goal<'tcx>>> {
 307         Some(*subgoal) // FIXME we should truncate at some point!
 308     }
 309
 310     fn truncate_answer(
 311         &mut self,
 312         subst: &CanonicalVarValues<'tcx>,
 313     ) -> Option<CanonicalVarValues<'tcx>> {
 314         Some(subst.clone()) // FIXME we should truncate at some point!
 315     }
 316 }
 317
 318 impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
 319     for ChalkInferenceContext<'cx, 'gcx, 'tcx>
 320 {
 321     fn program_clauses(
 322         &self,
 323         _environment: &ty::ParamEnv<'tcx>,
 324         goal: &DomainGoal<'tcx>,
 325     ) -> Vec<ProgramClause<'tcx>> {
 326         use rustc::traits::WhereClause::*;
 327
 328         match goal {
 329             DomainGoal::Holds(Implemented(_trait_predicate)) => {
 330                 // These come from:
 331                 //
 332                 // - Trait definitions (implied bounds)
 333                 // - Implementations of the trait itself
 334                 panic!()
 335             }
 336
 337             DomainGoal::Holds(ProjectionEq(_projection_predicate)) => {
 338                 // These come from:
 339                 panic!()
 340             }
 341
 342             DomainGoal::Holds(RegionOutlives(_region_outlives)) => {
 343                 panic!()
 344             }
 345
 346             DomainGoal::Holds(TypeOutlives(_type_outlives)) => {
 347                 panic!()
 348             }
 349
 350             DomainGoal::WellFormed(WellFormed::Trait(_trait_predicate)) => {
 351                 // These come from -- the trait decl.
 352                 panic!()
 353             }
 354
 355             DomainGoal::WellFormed(WellFormed::Ty(_ty)) => panic!(),
 356
 357             DomainGoal::FromEnv(FromEnv::Trait(_trait_predicate)) => panic!(),
 358
 359             DomainGoal::FromEnv(FromEnv::Ty(_ty)) => panic!(),
 360
 361             DomainGoal::Normalize(_) => panic!(),
 362         }
 363     }
 364
 365     fn instantiate_binders_universally(
 366         &mut self,
 367         _arg: &ty::Binder<&'tcx Goal<'tcx>>,
 368     ) -> Goal<'tcx> {
 369         panic!("FIXME -- universal instantiation needs sgrif's branch")
 370     }
 371
 372     fn instantiate_binders_existentially(
 373         &mut self,
 374         arg: &ty::Binder<&'tcx Goal<'tcx>>,
 375     ) -> Goal<'tcx> {
 376         let (value, _map) = self.infcx.replace_late_bound_regions_with_fresh_var(
 377             DUMMY_SP,
 378             LateBoundRegionConversionTime::HigherRankedType,
 379             arg,
 380         );
 381         *value
 382     }
 383
 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));
 386         Box::new(string)
 387     }
 388
 389     fn canonicalize_goal(
 390         &mut self,
 391         value: &ty::ParamEnvAnd<'tcx, Goal<'tcx>>,
 392     ) -> Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>> {
 393         self.infcx.canonicalize_query(value).0
 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).0
 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
 409             .canonicalize_response(&ConstrainedSubst { subst, constraints })
 410             .0
 411     }
 412
 413     fn u_canonicalize_goal(
 414         &mut self,
 415         value: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
 416     ) -> (
 417         Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
 418         UniverseMap,
 419     ) {
 420         (value.clone(), UniverseMap)
 421     }
 422
 423     fn invert_goal(
 424         &mut self,
 425         _value: &ty::ParamEnvAnd<'tcx, Goal<'tcx>>,
 426     ) -> Option<ty::ParamEnvAnd<'tcx, Goal<'tcx>>> {
 427         panic!("goal inversion not yet implemented")
 428     }
 429
 430     fn unify_parameters(
 431         &mut self,
 432         _environment: &ty::ParamEnv<'tcx>,
 433         _a: &Kind<'tcx>,
 434         _b: &Kind<'tcx>,
 435     ) -> ChalkEngineFallible<InferOk<'tcx, ()>> {
 436         panic!()
 437     }
 438
 439     fn sink_answer_subset(
 440         &self,
 441         value: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
 442     ) -> Canonical<'tcx, ConstrainedSubst<'tcx>> {
 443         value.clone()
 444     }
 445
 446     fn lift_delayed_literal(
 447         &self,
 448         _value: DelayedLiteral<ChalkArenas<'tcx>>,
 449     ) -> DelayedLiteral<ChalkArenas<'gcx>> {
 450         panic!("lift")
 451     }
 452
 453     fn into_ex_clause(&mut self, _result: InferOk<'tcx, ()>, _ex_clause: &mut ChalkExClause<'tcx>) {
 454         panic!("TBD")
 455     }
 456 }
 457
 458 type ChalkHhGoal<'tcx> = HhGoal<ChalkArenas<'tcx>>;
 459
 460 type ChalkExClause<'tcx> = ExClause<ChalkArenas<'tcx>>;
 461
 462 impl Debug for ChalkContext<'cx, 'gcx> {
 463     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
 464         write!(f, "ChalkContext")
 465     }
 466 }
 467
 468 impl Debug for ChalkInferenceContext<'cx, 'gcx, 'tcx> {
 469     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
 470         write!(f, "ChalkInferenceContext")
 471     }
 472 }
 473
 474 impl ExClauseLift<'gcx> for ChalkArenas<'a> {
 475     type LiftedExClause = ChalkExClause<'gcx>;
 476
 477     fn lift_ex_clause_to_tcx(
 478         _ex_clause: &ChalkExClause<'a>,
 479         _tcx: TyCtxt<'_, '_, 'tcx>,
 480     ) -> Option<Self::LiftedExClause> {
 481         panic!()
 482     }
 483 }
 484
 485 impl ExClauseFold<'tcx> for ChalkArenas<'tcx> {
 486     fn fold_ex_clause_with<'gcx: 'tcx, F: TypeFolder<'gcx, 'tcx>>(
 487         ex_clause: &ChalkExClause<'tcx>,
 488         folder: &mut F,
 489     ) -> ChalkExClause<'tcx> {
 490         ExClause {
 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),
 495         }
 496     }
 497
 498     fn visit_ex_clause_with<'gcx: 'tcx, V: TypeVisitor<'tcx>>(
 499         ex_clause: &ExClause<Self>,
 500         visitor: &mut V,
 501     ) -> bool {
 502         let ExClause {
 503             subst,
 504             delayed_literals,
 505             constraints,
 506             subgoals,
 507         } = ex_clause;
 508         subst.visit_with(visitor)
 509             && delayed_literals.visit_with(visitor)
 510             && constraints.visit_with(visitor)
 511             && subgoals.visit_with(visitor)
 512     }
 513 }
 514
 515 BraceStructLiftImpl! {
 516     impl<'a, 'tcx> Lift<'tcx> for ConstrainedSubst<'a> {
 517         type Lifted = ConstrainedSubst<'tcx>;
 518
 519         subst, constraints
 520     }
 521 }
 522
 523 impl<'gcx: 'tcx, 'tcx> Canonicalize<'gcx, 'tcx> for ConstrainedSubst<'tcx> {
 524     type Canonicalized = Canonical<'gcx, ConstrainedSubst<'gcx>>;
 525
 526     fn intern(
 527         _gcx: TyCtxt<'_, 'gcx, 'gcx>,
 528         value: Canonical<'gcx, ConstrainedSubst<'gcx>>,
 529     ) -> Self::Canonicalized {
 530         value
 531     }
 532 }