vendor/chalk-solve/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 }
 363
 364 trait SubstitutionExt<I: Interner> {
 365     fn may_invalidate(&self, interner: &I, subst: &Canonical<Substitution<I>>) -> bool;
 366 }
 367
 368 impl<I: Interner> SubstitutionExt<I> for Substitution<I> {
 369     fn may_invalidate(&self, interner: &I, subst: &Canonical<Substitution<I>>) -> bool {
 370         self.iter(interner)
 371             .zip(subst.value.iter(interner))
 372             .any(|(new, current)| MayInvalidate { interner }.aggregate_generic_args(new, current))
 373     }
 374 }
 375
 376 // This is a struct in case we need to add state at any point like in AntiUnifier
 377 struct MayInvalidate<'i, I> {
 378     interner: &'i I,
 379 }
 380
 381 impl<I: Interner> MayInvalidate<'_, I> {
 382     fn aggregate_generic_args(&mut self, new: &GenericArg<I>, current: &GenericArg<I>) -> bool {
 383         let interner = self.interner;
 384         match (new.data(interner), current.data(interner)) {
 385             (GenericArgData::Ty(ty1), GenericArgData::Ty(ty2)) => self.aggregate_tys(ty1, ty2),
 386             (GenericArgData::Lifetime(l1), GenericArgData::Lifetime(l2)) => {
 387                 self.aggregate_lifetimes(l1, l2)
 388             }
 389             (GenericArgData::Const(c1), GenericArgData::Const(c2)) => self.aggregate_consts(c1, c2),
 390             (GenericArgData::Ty(_), _)
 391             | (GenericArgData::Lifetime(_), _)
 392             | (GenericArgData::Const(_), _) => panic!(
 393                 "mismatched parameter kinds: new={:?} current={:?}",
 394                 new, current
 395             ),
 396         }
 397     }
 398
 399     /// Returns true if the two types could be unequal.
 400     fn aggregate_tys(&mut self, new: &Ty<I>, current: &Ty<I>) -> bool {
 401         let interner = self.interner;
 402         match (new.data(interner), current.data(interner)) {
 403             (_, TyData::BoundVar(_)) => {
 404                 // If the aggregate solution already has an inference
 405                 // variable here, then no matter what type we produce,
 406                 // the aggregate cannot get 'more generalized' than it
 407                 // already is. So return false, we cannot invalidate.
 408                 //
 409                 // (Note that "inference variables" show up as *bound
 410                 // variables* here, because we are looking at the
 411                 // canonical form.)
 412                 false
 413             }
 414
 415             (TyData::BoundVar(_), _) => {
 416                 // If we see a type variable in the potential future
 417                 // solution, we have to be conservative. We don't know
 418                 // what type variable will wind up being! Remember
 419                 // that the future solution could be any instantiation
 420                 // of `ty0` -- or it could leave this variable
 421                 // unbound, if the result is true for all types.
 422                 //
 423                 // (Note that "inference variables" show up as *bound
 424                 // variables* here, because we are looking at the
 425                 // canonical form.)
 426                 true
 427             }
 428
 429             (TyData::InferenceVar(_, _), _) | (_, TyData::InferenceVar(_, _)) => {
 430                 panic!(
 431                     "unexpected free inference variable in may-invalidate: {:?} vs {:?}",
 432                     new, current,
 433                 );
 434             }
 435
 436             (TyData::Apply(apply1), TyData::Apply(apply2)) => {
 437                 self.aggregate_application_tys(apply1, apply2)
 438             }
 439
 440             (TyData::Placeholder(p1), TyData::Placeholder(p2)) => {
 441                 self.aggregate_placeholders(p1, p2)
 442             }
 443
 444             (
 445                 TyData::Alias(AliasTy::Projection(proj1)),
 446                 TyData::Alias(AliasTy::Projection(proj2)),
 447             ) => self.aggregate_projection_tys(proj1, proj2),
 448
 449             (
 450                 TyData::Alias(AliasTy::Opaque(opaque_ty1)),
 451                 TyData::Alias(AliasTy::Opaque(opaque_ty2)),
 452             ) => self.aggregate_opaque_ty_tys(opaque_ty1, opaque_ty2),
 453
 454             // For everything else, be conservative here and just say we may invalidate.
 455             (TyData::Function(_), _)
 456             | (TyData::Dyn(_), _)
 457             | (TyData::Apply(_), _)
 458             | (TyData::Placeholder(_), _)
 459             | (TyData::Alias(_), _) => true,
 460         }
 461     }
 462
 463     /// Returns true if the two consts could be unequal.
 464     fn aggregate_lifetimes(&mut self, _: &Lifetime<I>, _: &Lifetime<I>) -> bool {
 465         true
 466     }
 467
 468     /// Returns true if the two consts could be unequal.
 469     fn aggregate_consts(&mut self, new: &Const<I>, current: &Const<I>) -> bool {
 470         let interner = self.interner;
 471         let ConstData {
 472             ty: new_ty,
 473             value: new_value,
 474         } = new.data(interner);
 475         let ConstData {
 476             ty: current_ty,
 477             value: current_value,
 478         } = current.data(interner);
 479
 480         if self.aggregate_tys(new_ty, current_ty) {
 481             return true;
 482         }
 483
 484         match (new_value, current_value) {
 485             (_, ConstValue::BoundVar(_)) => {
 486                 // see comment in aggregate_tys
 487                 false
 488             }
 489
 490             (ConstValue::BoundVar(_), _) => {
 491                 // see comment in aggregate_tys
 492                 true
 493             }
 494
 495             (ConstValue::InferenceVar(_), _) | (_, ConstValue::InferenceVar(_)) => {
 496                 panic!(
 497                     "unexpected free inference variable in may-invalidate: {:?} vs {:?}",
 498                     new, current,
 499                 );
 500             }
 501
 502             (ConstValue::Placeholder(p1), ConstValue::Placeholder(p2)) => {
 503                 self.aggregate_placeholders(p1, p2)
 504             }
 505
 506             (ConstValue::Concrete(c1), ConstValue::Concrete(c2)) => {
 507                 !c1.const_eq(new_ty, c2, interner)
 508             }
 509
 510             // Only variants left are placeholder = concrete, which always fails
 511             (ConstValue::Placeholder(_), _) | (ConstValue::Concrete(_), _) => true,
 512         }
 513     }
 514
 515     fn aggregate_application_tys(
 516         &mut self,
 517         new: &ApplicationTy<I>,
 518         current: &ApplicationTy<I>,
 519     ) -> bool {
 520         let ApplicationTy {
 521             name: new_name,
 522             substitution: new_substitution,
 523         } = new;
 524         let ApplicationTy {
 525             name: current_name,
 526             substitution: current_substitution,
 527         } = current;
 528
 529         self.aggregate_name_and_substs(
 530             new_name,
 531             new_substitution,
 532             current_name,
 533             current_substitution,
 534         )
 535     }
 536
 537     fn aggregate_placeholders(
 538         &mut self,
 539         new: &PlaceholderIndex,
 540         current: &PlaceholderIndex,
 541     ) -> bool {
 542         new != current
 543     }
 544
 545     fn aggregate_projection_tys(
 546         &mut self,
 547         new: &ProjectionTy<I>,
 548         current: &ProjectionTy<I>,
 549     ) -> bool {
 550         let ProjectionTy {
 551             associated_ty_id: new_name,
 552             substitution: new_substitution,
 553         } = new;
 554         let ProjectionTy {
 555             associated_ty_id: current_name,
 556             substitution: current_substitution,
 557         } = current;
 558
 559         self.aggregate_name_and_substs(
 560             new_name,
 561             new_substitution,
 562             current_name,
 563             current_substitution,
 564         )
 565     }
 566
 567     fn aggregate_opaque_ty_tys(&mut self, new: &OpaqueTy<I>, current: &OpaqueTy<I>) -> bool {
 568         let OpaqueTy {
 569             opaque_ty_id: new_name,
 570             substitution: new_substitution,
 571         } = new;
 572         let OpaqueTy {
 573             opaque_ty_id: current_name,
 574             substitution: current_substitution,
 575         } = current;
 576
 577         self.aggregate_name_and_substs(
 578             new_name,
 579             new_substitution,
 580             current_name,
 581             current_substitution,
 582         )
 583     }
 584
 585     fn aggregate_name_and_substs<N>(
 586         &mut self,
 587         new_name: N,
 588         new_substitution: &Substitution<I>,
 589         current_name: N,
 590         current_substitution: &Substitution<I>,
 591     ) -> bool
 592     where
 593         N: Copy + Eq + Debug,
 594     {
 595         let interner = self.interner;
 596         if new_name != current_name {
 597             return true;
 598         }
 599
 600         let name = new_name;
 601
 602         assert_eq!(
 603             new_substitution.len(interner),
 604             current_substitution.len(interner),
 605             "does {:?} take {} substitution or {}? can't both be right",
 606             name,
 607             new_substitution.len(interner),
 608             current_substitution.len(interner)
 609         );
 610
 611         new_substitution
 612             .iter(interner)
 613             .zip(current_substitution.iter(interner))
 614             .any(|(new, current)| self.aggregate_generic_args(new, current))
 615     }
 616 }