vendor/chalk-engine/src/slg.rs

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