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::Fold;
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::Result) -> G,
) -> Goal<I>
where
B: HasInterner<Interner = I>,
P: Fold<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::Result) -> G,
) -> Goal<I>
where
B: HasInterner<Interner = I>,
P: Fold<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::Result) -> G,
) -> Goal<I>
where
B: HasInterner<Interner = I>,
P: Fold<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)
}
}