]> git.proxmox.com Git - rustc.git/blame - vendor/chalk-solve-0.55.0/src/clauses/builder.rs
Merge tag 'debian/1.52.1+dfsg1-1_exp2' into proxmox/buster
[rustc.git] / vendor / chalk-solve-0.55.0 / src / clauses / builder.rs
CommitLineData
f035d41b
XL
1use std::marker::PhantomData;
2
f9f354fc
XL
3use crate::cast::{Cast, CastTo};
4use crate::RustIrDatabase;
f035d41b 5use chalk_ir::fold::{Fold, Shift};
f9f354fc
XL
6use chalk_ir::interner::{HasInterner, Interner};
7use chalk_ir::*;
f035d41b 8use 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.
14pub 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
21impl<'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}