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