|
| 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 | + clauses.into_iter().casted(self.interner()).collect(), |
| 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() |
| 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 | +} |
0 commit comments