vendor/chalk-solve/src/goal_builder.rs

   1 use crate::RustIrDatabase;
   2 use cast::CastTo;
   3 use chalk_ir::cast::Cast;
   4 use chalk_ir::cast::Caster;
   5 use chalk_ir::*;
   6 use chalk_rust_ir::ToParameter;
   7 use fold::shift::Shift;
   8 use fold::Fold;
   9 use interner::{HasInterner, Interner};
  10
  11 pub struct GoalBuilder<'i, I: Interner> {
  12     db: &'i dyn RustIrDatabase<I>,
  13 }
  14
  15 impl<'i, I: Interner> GoalBuilder<'i, I> {
  16     pub fn new(db: &'i dyn RustIrDatabase<I>) -> Self {
  17         GoalBuilder { db }
  18     }
  19
  20     /// Returns the database within the goal builder.
  21     pub fn db(&self) -> &'i dyn RustIrDatabase<I> {
  22         self.db
  23     }
  24
  25     /// Returns the interner within the goal builder.
  26     pub fn interner(&self) -> &'i I {
  27         self.db.interner()
  28     }
  29
  30     /// Creates a goal that ensures all of the goals from the `goals`
  31     /// iterator are met (e.g., `goals[0] && ... && goals[N]`).
  32     pub fn all<GS, G>(&mut self, goals: GS) -> Goal<I>
  33     where
  34         GS: IntoIterator<Item = G>,
  35         G: CastTo<Goal<I>>,
  36     {
  37         Goal::all(self.interner(), goals.into_iter().casted(self.interner()))
  38     }
  39
  40     /// Creates a goal `clauses => goal`. The clauses are given as an iterator
  41     /// and the goal is returned via the contained closure.
  42     pub fn implies<CS, C, G>(&mut self, clauses: CS, goal: impl FnOnce(&mut Self) -> G) -> Goal<I>
  43     where
  44         CS: IntoIterator<Item = C>,
  45         C: CastTo<ProgramClause<I>>,
  46         G: CastTo<Goal<I>>,
  47     {
  48         GoalData::Implies(
  49             ProgramClauses::from(self.interner(), clauses),
  50             goal(self).cast(self.interner()),
  51         )
  52         .intern(self.interner())
  53     }
  54
  55     /// Given a bound value `binders` like `<P0..Pn> V`,
  56     /// creates a goal `forall<Q0..Qn> { G }` where
  57     /// the goal `G` is created by invoking a helper
  58     /// function `body`.
  59     ///
  60     /// # Parameters to `body`
  61     ///
  62     /// `body` will be invoked with:
  63     ///
  64     /// * the goal builder `self`
  65     /// * the substitution `Q0..Qn`
  66     /// * the bound value `[P0..Pn => Q0..Qn] V` instantiated
  67     ///   with the substitution
  68     /// * the value `passthru`, appropriately shifted so that
  69     ///   any debruijn indices within account for the new binder
  70     ///
  71     /// # Why is `body` a function and not a closure?
  72     ///
  73     /// This is to ensure that `body` doesn't accidentally reference
  74     /// values from the environment whose debruijn indices do not
  75     /// account for the new binder being created.
  76     pub fn forall<G, B, P>(
  77         &mut self,
  78         binders: &Binders<B>,
  79         passthru: P,
  80         body: fn(&mut Self, Substitution<I>, &B, P::Result) -> G,
  81     ) -> Goal<I>
  82     where
  83         B: Fold<I> + HasInterner<Interner = I>,
  84         P: Fold<I>,
  85         B::Result: std::fmt::Debug,
  86         G: CastTo<Goal<I>>,
  87     {
  88         self.quantified(QuantifierKind::ForAll, binders, passthru, body)
  89     }
  90
  91     /// Like [`GoalBuilder::forall`], but for a `exists<Q0..Qn> { G }` goal.
  92     pub fn exists<G, B, P>(
  93         &mut self,
  94         binders: &Binders<B>,
  95         passthru: P,
  96         body: fn(&mut Self, Substitution<I>, &B, P::Result) -> G,
  97     ) -> Goal<I>
  98     where
  99         B: Fold<I> + HasInterner<Interner = I>,
 100         P: Fold<I>,
 101         B::Result: std::fmt::Debug,
 102         G: CastTo<Goal<I>>,
 103     {
 104         self.quantified(QuantifierKind::Exists, binders, passthru, body)
 105     }
 106
 107     /// A combined helper functon for the various methods
 108     /// to create `forall` and `exists` goals. See:
 109     ///
 110     /// * [`GoalBuilder::forall`]
 111     /// * [`GoalBuilder::exists`]
 112     ///
 113     /// for details.
 114     fn quantified<G, B, P>(
 115         &mut self,
 116         quantifier_kind: QuantifierKind,
 117         binders: &Binders<B>,
 118         passthru: P,
 119         body: fn(&mut Self, Substitution<I>, &B, P::Result) -> G,
 120     ) -> Goal<I>
 121     where
 122         B: Fold<I> + HasInterner<Interner = I>,
 123         P: Fold<I>,
 124         B::Result: std::fmt::Debug,
 125         G: CastTo<Goal<I>>,
 126     {
 127         let interner = self.interner();
 128
 129         // Make an identity mapping `[0 => ^0.0, 1 => ^0.1, ..]`
 130         // and so forth. This substitution is mapping from the `<P0..Pn>` variables
 131         // in `binders` to the corresponding `P0..Pn` variables we're about to
 132         // introduce in the form of a `forall<P0..Pn>` goal. Of course, it's
 133         // actually an identity mapping, since this `forall` will be the innermost
 134         // debruijn binder and so forth, so there's no actual reason to
 135         // *do* the substitution, since it would effectively just be a clone.
 136         let substitution: Substitution<I> = Substitution::from(
 137             interner,
 138             binders
 139                 .binders
 140                 .iter(interner)
 141                 .zip(0..)
 142                 .map(|p| p.to_parameter(interner)),
 143         );
 144
 145         // Shift passthru into one level of binder, to account for the `forall<P0..Pn>`
 146         // we are about to introduce.
 147         let passthru_shifted = passthru.shifted_in(self.interner());
 148
 149         // Invoke `body` function, which returns a goal, and wrap that goal in the binders
 150         // from `binders`, and finally a `forall` or `exists` goal.
 151         let bound_goal = binders.map_ref(|bound_value| {
 152             body(self, substitution, bound_value, passthru_shifted).cast(interner)
 153         });
 154         GoalData::Quantified(quantifier_kind, bound_goal).intern(interner)
 155     }
 156 }