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