vendor/chalk-engine/src/slg.rs

   1 use crate::context;
   2 use crate::normalize_deep::DeepNormalizer;
   3 use crate::{ExClause, Literal};
   4
   5 use chalk_derive::HasInterner;
   6 use chalk_ir::cast::Cast;
   7 use chalk_ir::cast::Caster;
   8 use chalk_ir::interner::Interner;
   9 use chalk_ir::*;
  10 use chalk_solve::clauses::program_clauses_for_goal;
  11 use chalk_solve::coinductive_goal::IsCoinductive;
  12 use chalk_solve::infer::ucanonicalize::UCanonicalized;
  13 use chalk_solve::infer::unify::UnificationResult;
  14 use chalk_solve::infer::InferenceTable;
  15 use chalk_solve::solve::truncate;
  16 use chalk_solve::RustIrDatabase;
  17
  18 use std::fmt::Debug;
  19 use std::marker::PhantomData;
  20
  21 pub(crate) mod aggregate;
  22 mod resolvent;
  23
  24 #[derive(Clone, Debug, HasInterner)]
  25 pub(crate) struct SlgContext<I: Interner> {
  26     phantom: PhantomData<I>,
  27 }
  28
  29 #[derive(Clone, Debug)]
  30 pub(crate) struct SlgContextOps<'me, I: Interner> {
  31     program: &'me dyn RustIrDatabase<I>,
  32     max_size: usize,
  33     expected_answers: Option<usize>,
  34 }
  35
  36 impl<I: Interner> SlgContextOps<'_, I> {
  37     pub(crate) fn new(
  38         program: &dyn RustIrDatabase<I>,
  39         max_size: usize,
  40         expected_answers: Option<usize>,
  41     ) -> SlgContextOps<'_, I> {
  42         SlgContextOps {
  43             program,
  44             max_size,
  45             expected_answers,
  46         }
  47     }
  48 }
  49
  50 #[derive(Clone)]
  51 pub struct TruncatingInferenceTable<I: Interner> {
  52     max_size: usize,
  53     infer: InferenceTable<I>,
  54 }
  55
  56 impl<I: Interner> context::Context<I> for SlgContext<I> {
  57     type InferenceTable = TruncatingInferenceTable<I>;
  58
  59     // Used by: logic
  60     fn next_subgoal_index(ex_clause: &ExClause<I>) -> usize {
  61         // For now, we always pick the last subgoal in the
  62         // list.
  63         //
  64         // FIXME(rust-lang-nursery/chalk#80) -- we should be more
  65         // selective. For example, we don't want to pick a
  66         // negative literal that will flounder, and we don't want
  67         // to pick things like `?T: Sized` if we can help it.
  68         ex_clause.subgoals.len() - 1
  69     }
  70 }
  71
  72 impl<'me, I: Interner> context::ContextOps<I, SlgContext<I>> for SlgContextOps<'me, I> {
  73     fn is_coinductive(&self, goal: &UCanonical<InEnvironment<Goal<I>>>) -> bool {
  74         goal.is_coinductive(self.program)
  75     }
  76
  77     fn map_goal_from_canonical(
  78         &self,
  79         map: &UniverseMap,
  80         value: &Canonical<InEnvironment<Goal<I>>>,
  81     ) -> Canonical<InEnvironment<Goal<I>>> {
  82         use chalk_solve::infer::ucanonicalize::UniverseMapExt;
  83         map.map_from_canonical(self.program.interner(), value)
  84     }
  85
  86     fn map_subst_from_canonical(
  87         &self,
  88         map: &UniverseMap,
  89         value: &Canonical<AnswerSubst<I>>,
  90     ) -> Canonical<AnswerSubst<I>> {
  91         use chalk_solve::infer::ucanonicalize::UniverseMapExt;
  92         map.map_from_canonical(self.program.interner(), value)
  93     }
  94
  95     fn program_clauses(
  96         &self,
  97         environment: &Environment<I>,
  98         goal: &DomainGoal<I>,
  99         _infer: &mut TruncatingInferenceTable<I>,
 100     ) -> Result<Vec<ProgramClause<I>>, Floundered> {
 101         let clauses: Vec<_> = program_clauses_for_goal(
 102             self.program,
 103             environment,
 104             goal,
 105             &CanonicalVarKinds::empty(self.program.interner()),
 106         )?;
 107
 108         Ok(clauses)
 109     }
 110
 111     // Used by: simplify
 112     fn add_clauses(&self, env: &Environment<I>, clauses: ProgramClauses<I>) -> Environment<I> {
 113         let interner = self.interner();
 114         env.add_clauses(interner, clauses.iter(interner).cloned())
 115     }
 116
 117     fn instantiate_ucanonical_goal(
 118         &self,
 119         arg: &UCanonical<InEnvironment<Goal<I>>>,
 120     ) -> (
 121         TruncatingInferenceTable<I>,
 122         Substitution<I>,
 123         Environment<I>,
 124         Goal<I>,
 125     ) {
 126         let (infer, subst, InEnvironment { environment, goal }) =
 127             InferenceTable::from_canonical(self.program.interner(), arg.universes, &arg.canonical);
 128         let infer_table = TruncatingInferenceTable::new(self.max_size, infer);
 129         (infer_table, subst, environment, goal)
 130     }
 131
 132     fn instantiate_ex_clause(
 133         &self,
 134         num_universes: usize,
 135         canonical_ex_clause: &Canonical<ExClause<I>>,
 136     ) -> (TruncatingInferenceTable<I>, ExClause<I>) {
 137         let (infer, _subst, ex_cluse) = InferenceTable::from_canonical(
 138             self.program.interner(),
 139             num_universes,
 140             canonical_ex_clause,
 141         );
 142         let infer_table = TruncatingInferenceTable::new(self.max_size, infer);
 143         (infer_table, ex_cluse)
 144     }
 145
 146     fn instantiate_answer_subst(
 147         &self,
 148         num_universes: usize,
 149         answer: &Canonical<AnswerSubst<I>>,
 150     ) -> (
 151         TruncatingInferenceTable<I>,
 152         Substitution<I>,
 153         Vec<InEnvironment<Constraint<I>>>,
 154         Vec<InEnvironment<Goal<I>>>,
 155     ) {
 156         let (
 157             infer,
 158             _subst,
 159             AnswerSubst {
 160                 subst,
 161                 constraints,
 162                 delayed_subgoals,
 163             },
 164         ) = InferenceTable::from_canonical(self.program.interner(), num_universes, answer);
 165         let infer_table = TruncatingInferenceTable::new(self.max_size, infer);
 166         (
 167             infer_table,
 168             subst,
 169             constraints.as_slice(self.interner()).to_vec(),
 170             delayed_subgoals,
 171         )
 172     }
 173
 174     fn identity_constrained_subst(
 175         &self,
 176         goal: &UCanonical<InEnvironment<Goal<I>>>,
 177     ) -> Canonical<ConstrainedSubst<I>> {
 178         let (mut infer, subst, _) = InferenceTable::from_canonical(
 179             self.program.interner(),
 180             goal.universes,
 181             &goal.canonical,
 182         );
 183         infer
 184             .canonicalize(
 185                 self.program.interner(),
 186                 &ConstrainedSubst {
 187                     subst,
 188                     constraints: Constraints::empty(self.program.interner()),
 189                 },
 190             )
 191             .quantified
 192     }
 193
 194     fn interner(&self) -> &I {
 195         self.program.interner()
 196     }
 197
 198     fn into_goal(&self, domain_goal: DomainGoal<I>) -> Goal<I> {
 199         domain_goal.cast(self.program.interner())
 200     }
 201
 202     fn is_trivial_constrained_substitution(
 203         &self,
 204         constrained_subst: &Canonical<ConstrainedSubst<I>>,
 205     ) -> bool {
 206         let interner = self.interner();
 207         constrained_subst.value.subst.is_identity_subst(interner)
 208     }
 209
 210     fn is_trivial_substitution(
 211         &self,
 212         u_canon: &UCanonical<InEnvironment<Goal<I>>>,
 213         canonical_subst: &Canonical<AnswerSubst<I>>,
 214     ) -> bool {
 215         let interner = self.interner();
 216         u_canon.is_trivial_substitution(interner, canonical_subst)
 217     }
 218 }
 219
 220 impl<I: Interner> TruncatingInferenceTable<I> {
 221     fn new(max_size: usize, infer: InferenceTable<I>) -> Self {
 222         Self { max_size, infer }
 223     }
 224 }
 225
 226 impl<I: Interner> context::TruncateOps<I, SlgContext<I>> for TruncatingInferenceTable<I> {
 227     fn goal_needs_truncation(&mut self, interner: &I, subgoal: &InEnvironment<Goal<I>>) -> bool {
 228         truncate::needs_truncation(interner, &mut self.infer, self.max_size, &subgoal)
 229     }
 230
 231     fn answer_needs_truncation(&mut self, interner: &I, subst: &Substitution<I>) -> bool {
 232         truncate::needs_truncation(interner, &mut self.infer, self.max_size, subst)
 233     }
 234 }
 235
 236 impl<I: Interner> context::InferenceTable<I, SlgContext<I>> for TruncatingInferenceTable<I> {}
 237
 238 impl<I: Interner> context::UnificationOps<I, SlgContext<I>> for TruncatingInferenceTable<I> {
 239     fn instantiate_binders_universally(&mut self, interner: &I, arg: &Binders<Goal<I>>) -> Goal<I> {
 240         self.infer.instantiate_binders_universally(interner, arg)
 241     }
 242
 243     fn instantiate_binders_existentially(
 244         &mut self,
 245         interner: &I,
 246         arg: &Binders<Goal<I>>,
 247     ) -> Goal<I> {
 248         self.infer.instantiate_binders_existentially(interner, arg)
 249     }
 250
 251     fn debug_ex_clause<'v>(&mut self, interner: &I, value: &'v ExClause<I>) -> Box<dyn Debug + 'v> {
 252         Box::new(DeepNormalizer::normalize_deep(
 253             &mut self.infer,
 254             interner,
 255             value,
 256         ))
 257     }
 258
 259     fn fully_canonicalize_goal(
 260         &mut self,
 261         interner: &I,
 262         value: &InEnvironment<Goal<I>>,
 263     ) -> (UCanonical<InEnvironment<Goal<I>>>, UniverseMap) {
 264         let canonicalized_goal = self.infer.canonicalize(interner, value).quantified;
 265         let UCanonicalized {
 266             quantified,
 267             universes,
 268         } = self.infer.u_canonicalize(interner, &canonicalized_goal);
 269         (quantified, universes)
 270     }
 271
 272     fn canonicalize_ex_clause(
 273         &mut self,
 274         interner: &I,
 275         value: &ExClause<I>,
 276     ) -> Canonical<ExClause<I>> {
 277         self.infer.canonicalize(interner, value).quantified
 278     }
 279
 280     fn canonicalize_constrained_subst(
 281         &mut self,
 282         interner: &I,
 283         subst: Substitution<I>,
 284         constraints: Vec<InEnvironment<Constraint<I>>>,
 285     ) -> Canonical<ConstrainedSubst<I>> {
 286         self.infer
 287             .canonicalize(
 288                 interner,
 289                 &ConstrainedSubst {
 290                     subst,
 291                     constraints: Constraints::from_iter(interner, constraints),
 292                 },
 293             )
 294             .quantified
 295     }
 296
 297     fn canonicalize_answer_subst(
 298         &mut self,
 299         interner: &I,
 300         subst: Substitution<I>,
 301         constraints: Vec<InEnvironment<Constraint<I>>>,
 302         delayed_subgoals: Vec<InEnvironment<Goal<I>>>,
 303     ) -> Canonical<AnswerSubst<I>> {
 304         self.infer
 305             .canonicalize(
 306                 interner,
 307                 &AnswerSubst {
 308                     subst,
 309                     constraints: Constraints::from_iter(interner, constraints),
 310                     delayed_subgoals,
 311                 },
 312             )
 313             .quantified
 314     }
 315
 316     fn invert_goal(
 317         &mut self,
 318         interner: &I,
 319         value: &InEnvironment<Goal<I>>,
 320     ) -> Option<InEnvironment<Goal<I>>> {
 321         self.infer.invert(interner, value)
 322     }
 323
 324     fn unify_generic_args_into_ex_clause(
 325         &mut self,
 326         interner: &I,
 327         environment: &Environment<I>,
 328         a: &GenericArg<I>,
 329         b: &GenericArg<I>,
 330         ex_clause: &mut ExClause<I>,
 331     ) -> Fallible<()> {
 332         let result = self.infer.unify(interner, environment, a, b)?;
 333         Ok(into_ex_clause(interner, result, ex_clause))
 334     }
 335 }
 336
 337 /// Helper function
 338 fn into_ex_clause<I: Interner>(
 339     interner: &I,
 340     result: UnificationResult<I>,
 341     ex_clause: &mut ExClause<I>,
 342 ) {
 343     ex_clause.subgoals.extend(
 344         result
 345             .goals
 346             .into_iter()
 347             .casted(interner)
 348             .map(Literal::Positive),
 349     );
 350 }
 351
 352 trait SubstitutionExt<I: Interner> {
 353     fn may_invalidate(&self, interner: &I, subst: &Canonical<Substitution<I>>) -> bool;
 354 }
 355
 356 impl<I: Interner> SubstitutionExt<I> for Substitution<I> {
 357     fn may_invalidate(&self, interner: &I, subst: &Canonical<Substitution<I>>) -> bool {
 358         self.iter(interner)
 359             .zip(subst.value.iter(interner))
 360             .any(|(new, current)| MayInvalidate { interner }.aggregate_generic_args(new, current))
 361     }
 362 }
 363
 364 // This is a struct in case we need to add state at any point like in AntiUnifier
 365 struct MayInvalidate<'i, I> {
 366     interner: &'i I,
 367 }
 368
 369 impl<I: Interner> MayInvalidate<'_, I> {
 370     fn aggregate_generic_args(&mut self, new: &GenericArg<I>, current: &GenericArg<I>) -> bool {
 371         let interner = self.interner;
 372         match (new.data(interner), current.data(interner)) {
 373             (GenericArgData::Ty(ty1), GenericArgData::Ty(ty2)) => self.aggregate_tys(ty1, ty2),
 374             (GenericArgData::Lifetime(l1), GenericArgData::Lifetime(l2)) => {
 375                 self.aggregate_lifetimes(l1, l2)
 376             }
 377             (GenericArgData::Const(c1), GenericArgData::Const(c2)) => self.aggregate_consts(c1, c2),
 378             (GenericArgData::Ty(_), _)
 379             | (GenericArgData::Lifetime(_), _)
 380             | (GenericArgData::Const(_), _) => panic!(
 381                 "mismatched parameter kinds: new={:?} current={:?}",
 382                 new, current
 383             ),
 384         }
 385     }
 386
 387     /// Returns true if the two types could be unequal.
 388     fn aggregate_tys(&mut self, new: &Ty<I>, current: &Ty<I>) -> bool {
 389         let interner = self.interner;
 390         match (new.data(interner), current.data(interner)) {
 391             (_, TyData::BoundVar(_)) => {
 392                 // If the aggregate solution already has an inference
 393                 // variable here, then no matter what type we produce,
 394                 // the aggregate cannot get 'more generalized' than it
 395                 // already is. So return false, we cannot invalidate.
 396                 //
 397                 // (Note that "inference variables" show up as *bound
 398                 // variables* here, because we are looking at the
 399                 // canonical form.)
 400                 false
 401             }
 402
 403             (TyData::BoundVar(_), _) => {
 404                 // If we see a type variable in the potential future
 405                 // solution, we have to be conservative. We don't know
 406                 // what type variable will wind up being! Remember
 407                 // that the future solution could be any instantiation
 408                 // of `ty0` -- or it could leave this variable
 409                 // unbound, if the result is true for all types.
 410                 //
 411                 // (Note that "inference variables" show up as *bound
 412                 // variables* here, because we are looking at the
 413                 // canonical form.)
 414                 true
 415             }
 416
 417             (TyData::InferenceVar(_, _), _) | (_, TyData::InferenceVar(_, _)) => {
 418                 panic!(
 419                     "unexpected free inference variable in may-invalidate: {:?} vs {:?}",
 420                     new, current,
 421                 );
 422             }
 423
 424             (TyData::Apply(apply1), TyData::Apply(apply2)) => {
 425                 self.aggregate_application_tys(apply1, apply2)
 426             }
 427
 428             (TyData::Placeholder(p1), TyData::Placeholder(p2)) => {
 429                 self.aggregate_placeholders(p1, p2)
 430             }
 431
 432             (
 433                 TyData::Alias(AliasTy::Projection(proj1)),
 434                 TyData::Alias(AliasTy::Projection(proj2)),
 435             ) => self.aggregate_projection_tys(proj1, proj2),
 436
 437             (
 438                 TyData::Alias(AliasTy::Opaque(opaque_ty1)),
 439                 TyData::Alias(AliasTy::Opaque(opaque_ty2)),
 440             ) => self.aggregate_opaque_ty_tys(opaque_ty1, opaque_ty2),
 441
 442             // For everything else, be conservative here and just say we may invalidate.
 443             (TyData::Function(_), _)
 444             | (TyData::Dyn(_), _)
 445             | (TyData::Apply(_), _)
 446             | (TyData::Placeholder(_), _)
 447             | (TyData::Alias(_), _) => true,
 448         }
 449     }
 450
 451     /// Returns true if the two consts could be unequal.
 452     fn aggregate_lifetimes(&mut self, _: &Lifetime<I>, _: &Lifetime<I>) -> bool {
 453         true
 454     }
 455
 456     /// Returns true if the two consts could be unequal.
 457     fn aggregate_consts(&mut self, new: &Const<I>, current: &Const<I>) -> bool {
 458         let interner = self.interner;
 459         let ConstData {
 460             ty: new_ty,
 461             value: new_value,
 462         } = new.data(interner);
 463         let ConstData {
 464             ty: current_ty,
 465             value: current_value,
 466         } = current.data(interner);
 467
 468         if self.aggregate_tys(new_ty, current_ty) {
 469             return true;
 470         }
 471
 472         match (new_value, current_value) {
 473             (_, ConstValue::BoundVar(_)) => {
 474                 // see comment in aggregate_tys
 475                 false
 476             }
 477
 478             (ConstValue::BoundVar(_), _) => {
 479                 // see comment in aggregate_tys
 480                 true
 481             }
 482
 483             (ConstValue::InferenceVar(_), _) | (_, ConstValue::InferenceVar(_)) => {
 484                 panic!(
 485                     "unexpected free inference variable in may-invalidate: {:?} vs {:?}",
 486                     new, current,
 487                 );
 488             }
 489
 490             (ConstValue::Placeholder(p1), ConstValue::Placeholder(p2)) => {
 491                 self.aggregate_placeholders(p1, p2)
 492             }
 493
 494             (ConstValue::Concrete(c1), ConstValue::Concrete(c2)) => {
 495                 !c1.const_eq(new_ty, c2, interner)
 496             }
 497
 498             // Only variants left are placeholder = concrete, which always fails
 499             (ConstValue::Placeholder(_), _) | (ConstValue::Concrete(_), _) => true,
 500         }
 501     }
 502
 503     fn aggregate_application_tys(
 504         &mut self,
 505         new: &ApplicationTy<I>,
 506         current: &ApplicationTy<I>,
 507     ) -> bool {
 508         let ApplicationTy {
 509             name: new_name,
 510             substitution: new_substitution,
 511         } = new;
 512         let ApplicationTy {
 513             name: current_name,
 514             substitution: current_substitution,
 515         } = current;
 516
 517         self.aggregate_name_and_substs(
 518             new_name,
 519             new_substitution,
 520             current_name,
 521             current_substitution,
 522         )
 523     }
 524
 525     fn aggregate_placeholders(
 526         &mut self,
 527         new: &PlaceholderIndex,
 528         current: &PlaceholderIndex,
 529     ) -> bool {
 530         new != current
 531     }
 532
 533     fn aggregate_projection_tys(
 534         &mut self,
 535         new: &ProjectionTy<I>,
 536         current: &ProjectionTy<I>,
 537     ) -> bool {
 538         let ProjectionTy {
 539             associated_ty_id: new_name,
 540             substitution: new_substitution,
 541         } = new;
 542         let ProjectionTy {
 543             associated_ty_id: current_name,
 544             substitution: current_substitution,
 545         } = current;
 546
 547         self.aggregate_name_and_substs(
 548             new_name,
 549             new_substitution,
 550             current_name,
 551             current_substitution,
 552         )
 553     }
 554
 555     fn aggregate_opaque_ty_tys(&mut self, new: &OpaqueTy<I>, current: &OpaqueTy<I>) -> bool {
 556         let OpaqueTy {
 557             opaque_ty_id: new_name,
 558             substitution: new_substitution,
 559         } = new;
 560         let OpaqueTy {
 561             opaque_ty_id: current_name,
 562             substitution: current_substitution,
 563         } = current;
 564
 565         self.aggregate_name_and_substs(
 566             new_name,
 567             new_substitution,
 568             current_name,
 569             current_substitution,
 570         )
 571     }
 572
 573     fn aggregate_name_and_substs<N>(
 574         &mut self,
 575         new_name: N,
 576         new_substitution: &Substitution<I>,
 577         current_name: N,
 578         current_substitution: &Substitution<I>,
 579     ) -> bool
 580     where
 581         N: Copy + Eq + Debug,
 582     {
 583         let interner = self.interner;
 584         if new_name != current_name {
 585             return true;
 586         }
 587
 588         let name = new_name;
 589
 590         assert_eq!(
 591             new_substitution.len(interner),
 592             current_substitution.len(interner),
 593             "does {:?} take {} substitution or {}? can't both be right",
 594             name,
 595             new_substitution.len(interner),
 596             current_substitution.len(interner)
 597         );
 598
 599         new_substitution
 600             .iter(interner)
 601             .zip(current_substitution.iter(interner))
 602             .any(|(new, current)| self.aggregate_generic_args(new, current))
 603     }
 604 }