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