compiler/rustc_traits/src/chalk/mod.rs

   1 //! Calls `chalk-solve` to solve a `ty::Predicate`
   2 //!
   3 //! In order to call `chalk-solve`, this file must convert a `CanonicalChalkEnvironmentAndGoal` into
   4 //! a Chalk uncanonical goal. It then calls Chalk, and converts the answer back into rustc solution.
   5
   6 crate mod db;
   7 crate mod lowering;
   8
   9 use rustc_data_structures::fx::FxHashMap;
  10
  11 use rustc_index::vec::IndexVec;
  12
  13 use rustc_middle::infer::canonical::{CanonicalTyVarKind, CanonicalVarKind};
  14 use rustc_middle::traits::ChalkRustInterner;
  15 use rustc_middle::ty::query::Providers;
  16 use rustc_middle::ty::subst::GenericArg;
  17 use rustc_middle::ty::{self, BoundVar, ParamTy, TyCtxt, TypeFoldable};
  18
  19 use rustc_infer::infer::canonical::{
  20     Canonical, CanonicalVarValues, Certainty, QueryRegionConstraints, QueryResponse,
  21 };
  22 use rustc_infer::traits::{self, CanonicalChalkEnvironmentAndGoal};
  23
  24 use crate::chalk::db::RustIrDatabase as ChalkRustIrDatabase;
  25 use crate::chalk::lowering::{
  26     LowerInto, ParamsSubstitutor, PlaceholdersCollector, RegionsSubstitutor,
  27 };
  28
  29 use chalk_solve::Solution;
  30
  31 crate fn provide(p: &mut Providers) {
  32     *p = Providers { evaluate_goal, ..*p };
  33 }
  34
  35 crate fn evaluate_goal<'tcx>(
  36     tcx: TyCtxt<'tcx>,
  37     obligation: CanonicalChalkEnvironmentAndGoal<'tcx>,
  38 ) -> Result<&'tcx Canonical<'tcx, QueryResponse<'tcx, ()>>, traits::query::NoSolution> {
  39     let interner = ChalkRustInterner { tcx };
  40
  41     // Chalk doesn't have a notion of `Params`, so instead we use placeholders.
  42     let mut placeholders_collector = PlaceholdersCollector::new();
  43     obligation.visit_with(&mut placeholders_collector);
  44
  45     let reempty_placeholder = tcx.mk_region(ty::RegionKind::RePlaceholder(ty::Placeholder {
  46         universe: ty::UniverseIndex::ROOT,
  47         name: ty::BoundRegionKind::BrAnon(placeholders_collector.next_anon_region_placeholder + 1),
  48     }));
  49
  50     let mut params_substitutor =
  51         ParamsSubstitutor::new(tcx, placeholders_collector.next_ty_placeholder);
  52     let obligation = obligation.fold_with(&mut params_substitutor);
  53     // FIXME(chalk): we really should be substituting these back in the solution
  54     let _params: FxHashMap<usize, ParamTy> = params_substitutor.params;
  55
  56     let mut regions_substitutor = RegionsSubstitutor::new(tcx, reempty_placeholder);
  57     let obligation = obligation.fold_with(&mut regions_substitutor);
  58
  59     let max_universe = obligation.max_universe.index();
  60
  61     let lowered_goal: chalk_ir::UCanonical<
  62         chalk_ir::InEnvironment<chalk_ir::Goal<ChalkRustInterner<'tcx>>>,
  63     > = chalk_ir::UCanonical {
  64         canonical: chalk_ir::Canonical {
  65             binders: chalk_ir::CanonicalVarKinds::from_iter(
  66                 &interner,
  67                 obligation.variables.iter().map(|v| match v.kind {
  68                     CanonicalVarKind::PlaceholderTy(_ty) => unimplemented!(),
  69                     CanonicalVarKind::PlaceholderRegion(_ui) => unimplemented!(),
  70                     CanonicalVarKind::Ty(ty) => match ty {
  71                         CanonicalTyVarKind::General(ui) => chalk_ir::WithKind::new(
  72                             chalk_ir::VariableKind::Ty(chalk_ir::TyVariableKind::General),
  73                             chalk_ir::UniverseIndex { counter: ui.index() },
  74                         ),
  75                         CanonicalTyVarKind::Int => chalk_ir::WithKind::new(
  76                             chalk_ir::VariableKind::Ty(chalk_ir::TyVariableKind::Integer),
  77                             chalk_ir::UniverseIndex::root(),
  78                         ),
  79                         CanonicalTyVarKind::Float => chalk_ir::WithKind::new(
  80                             chalk_ir::VariableKind::Ty(chalk_ir::TyVariableKind::Float),
  81                             chalk_ir::UniverseIndex::root(),
  82                         ),
  83                     },
  84                     CanonicalVarKind::Region(ui) => chalk_ir::WithKind::new(
  85                         chalk_ir::VariableKind::Lifetime,
  86                         chalk_ir::UniverseIndex { counter: ui.index() },
  87                     ),
  88                     CanonicalVarKind::Const(_ui) => unimplemented!(),
  89                     CanonicalVarKind::PlaceholderConst(_pc) => unimplemented!(),
  90                 }),
  91             ),
  92             value: obligation.value.lower_into(&interner),
  93         },
  94         universes: max_universe + 1,
  95     };
  96
  97     use chalk_solve::Solver;
  98     let mut solver = chalk_engine::solve::SLGSolver::new(32, None);
  99     let db = ChalkRustIrDatabase { interner, reempty_placeholder };
 100     let solution = solver.solve(&db, &lowered_goal);
 101     debug!(?obligation, ?solution, "evaluate goal");
 102
 103     // Ideally, the code to convert *back* to rustc types would live close to
 104     // the code to convert *from* rustc types. Right now though, we don't
 105     // really need this and so it's really minimal.
 106     // Right now, we also treat a `Unique` solution the same as
 107     // `Ambig(Definite)`. This really isn't right.
 108     let make_solution = |subst: chalk_ir::Substitution<_>,
 109                          binders: chalk_ir::CanonicalVarKinds<_>| {
 110         use rustc_middle::infer::canonical::CanonicalVarInfo;
 111
 112         let mut var_values: IndexVec<BoundVar, GenericArg<'tcx>> = IndexVec::new();
 113         subst.as_slice(&interner).iter().for_each(|p| {
 114             var_values.push(p.lower_into(&interner));
 115         });
 116         let variables: Vec<_> = binders
 117             .iter(&interner)
 118             .map(|var| {
 119                 let kind = match var.kind {
 120                     chalk_ir::VariableKind::Ty(ty_kind) => CanonicalVarKind::Ty(match ty_kind {
 121                         chalk_ir::TyVariableKind::General => CanonicalTyVarKind::General(
 122                             ty::UniverseIndex::from_usize(var.skip_kind().counter),
 123                         ),
 124                         chalk_ir::TyVariableKind::Integer => CanonicalTyVarKind::Int,
 125                         chalk_ir::TyVariableKind::Float => CanonicalTyVarKind::Float,
 126                     }),
 127                     chalk_ir::VariableKind::Lifetime => CanonicalVarKind::Region(
 128                         ty::UniverseIndex::from_usize(var.skip_kind().counter),
 129                     ),
 130                     chalk_ir::VariableKind::Const(_) => CanonicalVarKind::Const(
 131                         ty::UniverseIndex::from_usize(var.skip_kind().counter),
 132                     ),
 133                 };
 134                 CanonicalVarInfo { kind }
 135             })
 136             .collect();
 137         let max_universe =
 138             binders.iter(&interner).map(|v| v.skip_kind().counter).max().unwrap_or(0);
 139         let sol = Canonical {
 140             max_universe: ty::UniverseIndex::from_usize(max_universe),
 141             variables: tcx.intern_canonical_var_infos(&variables),
 142             value: QueryResponse {
 143                 var_values: CanonicalVarValues { var_values },
 144                 region_constraints: QueryRegionConstraints::default(),
 145                 certainty: Certainty::Proven,
 146                 value: (),
 147             },
 148         };
 149         tcx.arena.alloc(sol)
 150     };
 151     solution
 152         .map(|s| match s {
 153             Solution::Unique(subst) => {
 154                 // FIXME(chalk): handle constraints
 155                 make_solution(subst.value.subst, subst.binders)
 156             }
 157             Solution::Ambig(guidance) => {
 158                 match guidance {
 159                     chalk_solve::Guidance::Definite(subst) => {
 160                         make_solution(subst.value, subst.binders)
 161                     }
 162                     chalk_solve::Guidance::Suggested(_) => unimplemented!(),
 163                     chalk_solve::Guidance::Unknown => {
 164                         // chalk_fulfill doesn't use the var_values here, so
 165                         // let's just ignore that
 166                         let sol = Canonical {
 167                             max_universe: ty::UniverseIndex::from_usize(0),
 168                             variables: obligation.variables,
 169                             value: QueryResponse {
 170                                 var_values: CanonicalVarValues { var_values: IndexVec::new() }
 171                                     .make_identity(tcx),
 172                                 region_constraints: QueryRegionConstraints::default(),
 173                                 certainty: Certainty::Ambiguous,
 174                                 value: (),
 175                             },
 176                         };
 177                         &*tcx.arena.alloc(sol)
 178                     }
 179                 }
 180             }
 181         })
 182         .ok_or(traits::query::NoSolution)
 183 }