vendor/chalk-solve-0.14.0/src/solve/slg.rs

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