]>
Commit | Line | Data |
---|---|---|
f035d41b XL |
1 | use std::marker::PhantomData; |
2 | ||
f9f354fc XL |
3 | use crate::cast::{Cast, CastTo}; |
4 | use crate::RustIrDatabase; | |
f035d41b | 5 | use chalk_ir::fold::{Fold, Shift}; |
f9f354fc XL |
6 | use chalk_ir::interner::{HasInterner, Interner}; |
7 | use chalk_ir::*; | |
f035d41b | 8 | use tracing::{debug, instrument}; |
f9f354fc XL |
9 | |
10 | /// The "clause builder" is a useful tool for building up sets of | |
11 | /// program clauses. It takes ownership of the output vector while it | |
12 | /// lasts, and offers methods like `push_clause` and so forth to | |
13 | /// append to it. | |
14 | pub struct ClauseBuilder<'me, I: Interner> { | |
15 | pub db: &'me dyn RustIrDatabase<I>, | |
16 | clauses: &'me mut Vec<ProgramClause<I>>, | |
f035d41b XL |
17 | binders: Vec<VariableKind<I>>, |
18 | parameters: Vec<GenericArg<I>>, | |
f9f354fc XL |
19 | } |
20 | ||
21 | impl<'me, I: Interner> ClauseBuilder<'me, I> { | |
22 | pub fn new(db: &'me dyn RustIrDatabase<I>, clauses: &'me mut Vec<ProgramClause<I>>) -> Self { | |
23 | Self { | |
24 | db, | |
25 | clauses, | |
26 | binders: vec![], | |
27 | parameters: vec![], | |
28 | } | |
29 | } | |
30 | ||
31 | /// Pushes a "fact" `forall<..> { consequence }` into the set of | |
32 | /// program clauses, meaning something that we can assume to be | |
33 | /// true unconditionally. The `forall<..>` binders will be | |
34 | /// whichever binders have been pushed (see `push_binders`). | |
35 | pub fn push_fact(&mut self, consequence: impl CastTo<DomainGoal<I>>) { | |
36 | self.push_clause(consequence, None::<Goal<_>>); | |
37 | } | |
38 | ||
39 | /// Pushes a "fact" `forall<..> { consequence }` into the set of | |
40 | /// program clauses, meaning something that we can assume to be | |
41 | /// true unconditionally. The `forall<..>` binders will be | |
42 | /// whichever binders have been pushed (see `push_binders`). | |
43 | pub fn push_fact_with_priority( | |
44 | &mut self, | |
45 | consequence: impl CastTo<DomainGoal<I>>, | |
3dfed10e | 46 | constraints: impl IntoIterator<Item = InEnvironment<Constraint<I>>>, |
f9f354fc XL |
47 | priority: ClausePriority, |
48 | ) { | |
3dfed10e | 49 | self.push_clause_with_priority(consequence, None::<Goal<_>>, constraints, priority); |
f9f354fc XL |
50 | } |
51 | ||
52 | /// Pushes a clause `forall<..> { consequence :- conditions }` | |
53 | /// into the set of program clauses, meaning that `consequence` | |
54 | /// can be proven if `conditions` are all true. The `forall<..>` | |
55 | /// binders will be whichever binders have been pushed (see `push_binders`). | |
56 | pub fn push_clause( | |
57 | &mut self, | |
58 | consequence: impl CastTo<DomainGoal<I>>, | |
59 | conditions: impl IntoIterator<Item = impl CastTo<Goal<I>>>, | |
60 | ) { | |
3dfed10e | 61 | self.push_clause_with_priority(consequence, conditions, None, ClausePriority::High) |
f9f354fc XL |
62 | } |
63 | ||
3dfed10e XL |
64 | pub fn push_fact_with_constraints( |
65 | &mut self, | |
66 | consequence: impl CastTo<DomainGoal<I>>, | |
67 | constraints: impl IntoIterator<Item = InEnvironment<Constraint<I>>>, | |
68 | ) { | |
69 | self.push_fact_with_priority(consequence, constraints, ClausePriority::High) | |
70 | } | |
71 | ||
72 | /// Pushes a clause `forall<..> { consequence :- conditions ; constraints }` | |
f9f354fc | 73 | /// into the set of program clauses, meaning that `consequence` |
3dfed10e XL |
74 | /// can be proven if `conditions` are all true and `constraints` |
75 | /// are proven to hold. The `forall<..>` binders will be whichever binders | |
76 | /// have been pushed (see `push_binders`). | |
f9f354fc XL |
77 | pub fn push_clause_with_priority( |
78 | &mut self, | |
79 | consequence: impl CastTo<DomainGoal<I>>, | |
80 | conditions: impl IntoIterator<Item = impl CastTo<Goal<I>>>, | |
3dfed10e | 81 | constraints: impl IntoIterator<Item = InEnvironment<Constraint<I>>>, |
f9f354fc XL |
82 | priority: ClausePriority, |
83 | ) { | |
84 | let interner = self.db.interner(); | |
85 | let clause = ProgramClauseImplication { | |
86 | consequence: consequence.cast(interner), | |
3dfed10e XL |
87 | conditions: Goals::from_iter(interner, conditions), |
88 | constraints: Constraints::from_iter(interner, constraints), | |
f9f354fc XL |
89 | priority, |
90 | }; | |
91 | ||
f035d41b XL |
92 | let clause = if self.binders.is_empty() { |
93 | // Compensate for the added empty binder | |
94 | clause.shifted_in(interner) | |
f9f354fc | 95 | } else { |
f035d41b XL |
96 | clause |
97 | }; | |
98 | ||
99 | self.clauses.push( | |
100 | ProgramClauseData(Binders::new( | |
3dfed10e | 101 | VariableKinds::from_iter(interner, self.binders.clone()), |
f035d41b XL |
102 | clause, |
103 | )) | |
104 | .intern(interner), | |
105 | ); | |
f9f354fc XL |
106 | |
107 | debug!("pushed clause {:?}", self.clauses.last()); | |
108 | } | |
109 | ||
110 | /// Accesses the placeholders for the current list of parameters in scope. | |
f035d41b | 111 | pub fn placeholders_in_scope(&self) -> &[GenericArg<I>] { |
f9f354fc XL |
112 | &self.parameters |
113 | } | |
114 | ||
115 | /// Accesses the placeholders for the current list of parameters in scope, | |
116 | /// in the form of a `Substitution`. | |
117 | pub fn substitution_in_scope(&self) -> Substitution<I> { | |
3dfed10e | 118 | Substitution::from_iter( |
f9f354fc XL |
119 | self.db.interner(), |
120 | self.placeholders_in_scope().iter().cloned(), | |
121 | ) | |
122 | } | |
123 | ||
124 | /// Executes `op` with the `binders` in-scope; `op` is invoked | |
125 | /// with the bound value `v` as a parameter. After `op` finishes, | |
126 | /// the binders are popped from scope. | |
127 | /// | |
128 | /// The new binders are always pushed onto the end of the internal | |
129 | /// list of binders; this means that any extant values where were | |
130 | /// created referencing the *old* list of binders are still valid. | |
f035d41b XL |
131 | #[instrument(level = "debug", skip(self, op))] |
132 | pub fn push_binders<R, V>( | |
133 | &mut self, | |
5869c6ff | 134 | binders: Binders<V>, |
f035d41b XL |
135 | op: impl FnOnce(&mut Self, V::Result) -> R, |
136 | ) -> R | |
f9f354fc XL |
137 | where |
138 | V: Fold<I> + HasInterner<Interner = I>, | |
139 | V::Result: std::fmt::Debug, | |
140 | { | |
f9f354fc XL |
141 | let old_len = self.binders.len(); |
142 | let interner = self.interner(); | |
143 | self.binders.extend(binders.binders.iter(interner).cloned()); | |
144 | self.parameters.extend( | |
145 | binders | |
146 | .binders | |
147 | .iter(interner) | |
148 | .zip(old_len..) | |
f035d41b | 149 | .map(|(pk, i)| (i, pk).to_generic_arg(interner)), |
f9f354fc | 150 | ); |
f9f354fc | 151 | let value = binders.substitute(self.interner(), &self.parameters[old_len..]); |
3dfed10e | 152 | debug!(?value); |
f035d41b | 153 | let res = op(self, value); |
f9f354fc XL |
154 | |
155 | self.binders.truncate(old_len); | |
156 | self.parameters.truncate(old_len); | |
f035d41b | 157 | res |
f9f354fc XL |
158 | } |
159 | ||
160 | /// Push a single binder, for a type, at the end of the binder | |
161 | /// list. The indices of previously bound variables are | |
162 | /// unaffected and hence the context remains usable. Invokes `op`, | |
163 | /// passing a type representing this new type variable in as an | |
164 | /// argument. | |
f9f354fc XL |
165 | pub fn push_bound_ty(&mut self, op: impl FnOnce(&mut Self, Ty<I>)) { |
166 | let interner = self.interner(); | |
167 | let binders = Binders::new( | |
29967ef6 | 168 | VariableKinds::from1(interner, VariableKind::Ty(TyVariableKind::General)), |
f9f354fc XL |
169 | PhantomData::<I>, |
170 | ); | |
5869c6ff | 171 | self.push_binders(binders, |this, PhantomData| { |
f9f354fc XL |
172 | let ty = this |
173 | .placeholders_in_scope() | |
174 | .last() | |
175 | .unwrap() | |
176 | .assert_ty_ref(interner) | |
177 | .clone(); | |
178 | op(this, ty) | |
179 | }); | |
180 | } | |
181 | ||
3dfed10e XL |
182 | /// Push a single binder, for a lifetime, at the end of the binder |
183 | /// list. The indices of previously bound variables are | |
184 | /// unaffected and hence the context remains usable. Invokes `op`, | |
185 | /// passing a lifetime representing this new lifetime variable in as an | |
186 | /// argument. | |
187 | pub fn push_bound_lifetime(&mut self, op: impl FnOnce(&mut Self, Lifetime<I>)) { | |
188 | let interner = self.interner(); | |
189 | let binders = Binders::new( | |
190 | VariableKinds::from1(interner, VariableKind::Lifetime), | |
191 | PhantomData::<I>, | |
192 | ); | |
5869c6ff | 193 | self.push_binders(binders, |this, PhantomData| { |
3dfed10e XL |
194 | let lifetime = this |
195 | .placeholders_in_scope() | |
196 | .last() | |
197 | .unwrap() | |
198 | .assert_lifetime_ref(interner) | |
199 | .clone(); | |
200 | op(this, lifetime) | |
201 | }); | |
202 | } | |
203 | ||
f9f354fc XL |
204 | pub fn interner(&self) -> &'me I { |
205 | self.db.interner() | |
206 | } | |
207 | } |