1use crate::prelude::*;
2use std::collections::HashMap;
3
4fn mark_forall_param_name_if_tracked(
8 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
9 name: &IdentifierName,
10) {
11 match coverage_by_forall_param.get_mut(name) {
12 Some(is_mentioned) => {
13 *is_mentioned = true;
14 }
15 None => {}
16 }
17}
18
19fn mark_forall_param_coverage_in_param_type(
20 param_type: &ParamType,
21 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
22) {
23 match param_type {
24 ParamType::Obj(obj) => {
25 mark_forall_param_coverage_in_obj(obj, coverage_by_forall_param);
26 }
27 ParamType::Restrictive(fs) => {
28 mark_forall_param_coverage_in_obj(&Obj::FnSet(fs.clone()), coverage_by_forall_param);
29 }
30 ParamType::Set(_) | ParamType::NonemptySet(_) | ParamType::FiniteSet(_) => {}
31 }
32}
33
34fn mark_forall_param_coverage_in_fn_obj_head(
35 head: &FnObjHead,
36 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
37) {
38 match head {
39 FnObjHead::Identifier(i) => {
40 mark_forall_param_coverage_in_obj(
41 &Obj::Atom(AtomObj::Identifier(i.clone())),
42 coverage_by_forall_param,
43 );
44 }
45 FnObjHead::IdentifierWithMod(m) => {
46 mark_forall_param_coverage_in_obj(
47 &Obj::Atom(AtomObj::IdentifierWithMod(m.clone())),
48 coverage_by_forall_param,
49 );
50 }
51 FnObjHead::Forall(p) => {
52 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
53 }
54 FnObjHead::DefHeader(_)
55 | FnObjHead::Exist(_)
56 | FnObjHead::SetBuilder(_)
57 | FnObjHead::FnSet(_)
58 | FnObjHead::Induc(_)
59 | FnObjHead::DefAlgo(_) => {}
60 FnObjHead::AnonymousFnLiteral(a) => {
61 mark_forall_param_coverage_in_obj(
62 &Obj::AnonymousFn((**a).clone()),
63 coverage_by_forall_param,
64 );
65 }
66 }
67}
68
69fn mark_forall_param_coverage_in_obj(
70 obj: &Obj,
71 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
72) {
73 match obj {
74 Obj::Atom(AtomObj::Identifier(identifier)) => {
75 mark_forall_param_name_if_tracked(coverage_by_forall_param, &identifier.name);
76 }
77 Obj::Atom(AtomObj::IdentifierWithMod(_)) => {}
78 Obj::FnObj(fn_obj) => {
79 mark_forall_param_coverage_in_fn_obj_head(fn_obj.head.as_ref(), coverage_by_forall_param);
80 for group in fn_obj.body.iter() {
81 for boxed_obj in group.iter() {
82 mark_forall_param_coverage_in_obj(boxed_obj.as_ref(), coverage_by_forall_param);
83 }
84 }
85 }
86 Obj::Number(_) | Obj::StandardSet(_) => {}
87 Obj::Add(binary) => {
88 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
89 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
90 }
91 Obj::Sub(binary) => {
92 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
93 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
94 }
95 Obj::Mul(binary) => {
96 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
97 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
98 }
99 Obj::Div(binary) => {
100 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
101 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
102 }
103 Obj::Mod(binary) => {
104 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
105 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
106 }
107 Obj::Pow(binary) => {
108 mark_forall_param_coverage_in_obj(binary.base.as_ref(), coverage_by_forall_param);
109 mark_forall_param_coverage_in_obj(binary.exponent.as_ref(), coverage_by_forall_param);
110 }
111 Obj::MatrixAdd(binary) => {
112 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
113 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
114 }
115 Obj::MatrixSub(binary) => {
116 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
117 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
118 }
119 Obj::MatrixMul(binary) => {
120 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
121 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
122 }
123 Obj::MatrixScalarMul(binary) => {
124 mark_forall_param_coverage_in_obj(binary.scalar.as_ref(), coverage_by_forall_param);
125 mark_forall_param_coverage_in_obj(binary.matrix.as_ref(), coverage_by_forall_param);
126 }
127 Obj::MatrixPow(binary) => {
128 mark_forall_param_coverage_in_obj(binary.base.as_ref(), coverage_by_forall_param);
129 mark_forall_param_coverage_in_obj(binary.exponent.as_ref(), coverage_by_forall_param);
130 }
131 Obj::Abs(unary) => {
132 mark_forall_param_coverage_in_obj(unary.arg.as_ref(), coverage_by_forall_param);
133 }
134 Obj::Log(binary) => {
135 mark_forall_param_coverage_in_obj(binary.base.as_ref(), coverage_by_forall_param);
136 mark_forall_param_coverage_in_obj(binary.arg.as_ref(), coverage_by_forall_param);
137 }
138 Obj::Max(binary) => {
139 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
140 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
141 }
142 Obj::Min(binary) => {
143 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
144 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
145 }
146 Obj::Union(binary) => {
147 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
148 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
149 }
150 Obj::Intersect(binary) => {
151 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
152 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
153 }
154 Obj::SetMinus(binary) => {
155 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
156 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
157 }
158 Obj::SetDiff(binary) => {
159 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
160 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
161 }
162 Obj::Cup(unary) => {
163 mark_forall_param_coverage_in_obj(unary.left.as_ref(), coverage_by_forall_param);
164 }
165 Obj::Cap(unary) => {
166 mark_forall_param_coverage_in_obj(unary.left.as_ref(), coverage_by_forall_param);
167 }
168 Obj::PowerSet(unary) => {
169 mark_forall_param_coverage_in_obj(unary.set.as_ref(), coverage_by_forall_param);
170 }
171 Obj::ListSet(list_set) => {
172 for boxed_obj in list_set.list.iter() {
173 mark_forall_param_coverage_in_obj(boxed_obj.as_ref(), coverage_by_forall_param);
174 }
175 }
176 Obj::SetBuilder(set_builder) => {
177 mark_forall_param_coverage_in_obj(
178 set_builder.param_set.as_ref(),
179 coverage_by_forall_param,
180 );
181 for inner_fact in set_builder.facts.iter() {
182 mark_forall_param_coverage_in_or_and_chain_atomic_fact(
183 inner_fact,
184 coverage_by_forall_param,
185 );
186 }
187 }
188 Obj::FnSet(fn_set) => {
189 for param_def_with_set in fn_set.body.params_def_with_set.iter() {
190 mark_forall_param_coverage_in_obj(
191 ¶m_def_with_set.set,
192 coverage_by_forall_param,
193 );
194 }
195 for dom_fact in fn_set.body.dom_facts.iter() {
196 mark_forall_param_coverage_in_or_and_chain_atomic_fact(
197 dom_fact,
198 coverage_by_forall_param,
199 );
200 }
201 mark_forall_param_coverage_in_obj(fn_set.body.ret_set.as_ref(), coverage_by_forall_param);
202 }
203 Obj::AnonymousFn(anon) => {
204 for param_def_with_set in anon.body.params_def_with_set.iter() {
205 mark_forall_param_coverage_in_obj(
206 ¶m_def_with_set.set,
207 coverage_by_forall_param,
208 );
209 }
210 for dom_fact in anon.body.dom_facts.iter() {
211 mark_forall_param_coverage_in_or_and_chain_atomic_fact(
212 dom_fact,
213 coverage_by_forall_param,
214 );
215 }
216 mark_forall_param_coverage_in_obj(anon.body.ret_set.as_ref(), coverage_by_forall_param);
217 mark_forall_param_coverage_in_obj(anon.equal_to.as_ref(), coverage_by_forall_param);
218 }
219 Obj::Cart(cart) => {
220 for boxed_arg in cart.args.iter() {
221 mark_forall_param_coverage_in_obj(boxed_arg.as_ref(), coverage_by_forall_param);
222 }
223 }
224 Obj::CartDim(cart_dim) => {
225 mark_forall_param_coverage_in_obj(cart_dim.set.as_ref(), coverage_by_forall_param);
226 }
227 Obj::Proj(proj) => {
228 mark_forall_param_coverage_in_obj(proj.set.as_ref(), coverage_by_forall_param);
229 mark_forall_param_coverage_in_obj(proj.dim.as_ref(), coverage_by_forall_param);
230 }
231 Obj::TupleDim(tuple_dim) => {
232 mark_forall_param_coverage_in_obj(tuple_dim.arg.as_ref(), coverage_by_forall_param);
233 }
234 Obj::Tuple(tuple_obj) => {
235 for boxed_arg in tuple_obj.args.iter() {
236 mark_forall_param_coverage_in_obj(boxed_arg.as_ref(), coverage_by_forall_param);
237 }
238 }
239 Obj::Count(count) => {
240 mark_forall_param_coverage_in_obj(count.set.as_ref(), coverage_by_forall_param);
241 }
242 Obj::Sum(s) => {
243 mark_forall_param_coverage_in_obj(s.start.as_ref(), coverage_by_forall_param);
244 mark_forall_param_coverage_in_obj(s.end.as_ref(), coverage_by_forall_param);
245 mark_forall_param_coverage_in_obj(s.func.as_ref(), coverage_by_forall_param);
246 }
247 Obj::Product(s) => {
248 mark_forall_param_coverage_in_obj(s.start.as_ref(), coverage_by_forall_param);
249 mark_forall_param_coverage_in_obj(s.end.as_ref(), coverage_by_forall_param);
250 mark_forall_param_coverage_in_obj(s.func.as_ref(), coverage_by_forall_param);
251 }
252 Obj::Range(range) => {
253 mark_forall_param_coverage_in_obj(range.start.as_ref(), coverage_by_forall_param);
254 mark_forall_param_coverage_in_obj(range.end.as_ref(), coverage_by_forall_param);
255 }
256 Obj::ClosedRange(closed_range) => {
257 mark_forall_param_coverage_in_obj(
258 closed_range.start.as_ref(),
259 coverage_by_forall_param,
260 );
261 mark_forall_param_coverage_in_obj(closed_range.end.as_ref(), coverage_by_forall_param);
262 }
263 Obj::FiniteSeqSet(fs) => {
264 mark_forall_param_coverage_in_obj(fs.set.as_ref(), coverage_by_forall_param);
265 mark_forall_param_coverage_in_obj(fs.n.as_ref(), coverage_by_forall_param);
266 }
267 Obj::SeqSet(ss) => {
268 mark_forall_param_coverage_in_obj(ss.set.as_ref(), coverage_by_forall_param);
269 }
270 Obj::FiniteSeqListObj(v) => {
271 for o in v.objs.iter() {
272 mark_forall_param_coverage_in_obj(o.as_ref(), coverage_by_forall_param);
273 }
274 }
275 Obj::MatrixSet(ms) => {
276 mark_forall_param_coverage_in_obj(ms.set.as_ref(), coverage_by_forall_param);
277 mark_forall_param_coverage_in_obj(ms.row_len.as_ref(), coverage_by_forall_param);
278 mark_forall_param_coverage_in_obj(ms.col_len.as_ref(), coverage_by_forall_param);
279 }
280 Obj::MatrixListObj(v) => {
281 for row in v.rows.iter() {
282 for o in row.iter() {
283 mark_forall_param_coverage_in_obj(o.as_ref(), coverage_by_forall_param);
284 }
285 }
286 }
287 Obj::Choose(choose) => {
288 mark_forall_param_coverage_in_obj(choose.set.as_ref(), coverage_by_forall_param);
289 }
290 Obj::ObjAtIndex(obj_at_index) => {
291 mark_forall_param_coverage_in_obj(obj_at_index.obj.as_ref(), coverage_by_forall_param);
292 mark_forall_param_coverage_in_obj(
293 obj_at_index.index.as_ref(),
294 coverage_by_forall_param,
295 );
296 }
297 Obj::FamilyObj(family) => {
298 for o in family.params.iter() {
299 mark_forall_param_coverage_in_obj(o, coverage_by_forall_param);
300 }
301 }
302 Obj::Atom(AtomObj::Forall(p)) => {
303 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
304 }
305 Obj::Atom(AtomObj::Def(p)) => {
306 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
307 }
308 Obj::Atom(AtomObj::Exist(p)) => {
309 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
310 }
311 Obj::Atom(AtomObj::SetBuilder(p)) => {
312 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
313 }
314 Obj::Atom(AtomObj::FnSet(p)) => {
315 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
316 }
317 Obj::Atom(AtomObj::Induc(p)) => {
318 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
319 }
320 Obj::Atom(AtomObj::DefAlgo(p)) => {
321 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
322 }
323 }
324}
325
326fn mark_forall_param_coverage_in_atomic_fact(
327 atomic_fact: &AtomicFact,
328 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
329) {
330 match atomic_fact {
331 AtomicFact::NormalAtomicFact(fact) => {
332 for body_obj in fact.body.iter() {
333 mark_forall_param_coverage_in_obj(body_obj, coverage_by_forall_param);
334 }
335 }
336 AtomicFact::NotNormalAtomicFact(fact) => {
337 for body_obj in fact.body.iter() {
338 mark_forall_param_coverage_in_obj(body_obj, coverage_by_forall_param);
339 }
340 }
341 AtomicFact::EqualFact(fact) => {
342 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
343 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
344 }
345 AtomicFact::LessFact(fact) => {
346 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
347 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
348 }
349 AtomicFact::GreaterFact(fact) => {
350 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
351 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
352 }
353 AtomicFact::LessEqualFact(fact) => {
354 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
355 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
356 }
357 AtomicFact::GreaterEqualFact(fact) => {
358 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
359 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
360 }
361 AtomicFact::NotEqualFact(fact) => {
362 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
363 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
364 }
365 AtomicFact::NotLessFact(fact) => {
366 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
367 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
368 }
369 AtomicFact::NotGreaterFact(fact) => {
370 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
371 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
372 }
373 AtomicFact::NotLessEqualFact(fact) => {
374 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
375 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
376 }
377 AtomicFact::NotGreaterEqualFact(fact) => {
378 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
379 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
380 }
381 AtomicFact::IsSetFact(fact) => {
382 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
383 }
384 AtomicFact::NotIsSetFact(fact) => {
385 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
386 }
387 AtomicFact::IsNonemptySetFact(fact) => {
388 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
389 }
390 AtomicFact::NotIsNonemptySetFact(fact) => {
391 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
392 }
393 AtomicFact::IsFiniteSetFact(fact) => {
394 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
395 }
396 AtomicFact::NotIsFiniteSetFact(fact) => {
397 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
398 }
399 AtomicFact::InFact(fact) => {
400 mark_forall_param_coverage_in_obj(&fact.element, coverage_by_forall_param);
401 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
402 }
403 AtomicFact::NotInFact(fact) => {
404 mark_forall_param_coverage_in_obj(&fact.element, coverage_by_forall_param);
405 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
406 }
407 AtomicFact::IsCartFact(fact) => {
408 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
409 }
410 AtomicFact::NotIsCartFact(fact) => {
411 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
412 }
413 AtomicFact::IsTupleFact(fact) => {
414 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
415 }
416 AtomicFact::NotIsTupleFact(fact) => {
417 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
418 }
419 AtomicFact::SubsetFact(fact) => {
420 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
421 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
422 }
423 AtomicFact::SupersetFact(fact) => {
424 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
425 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
426 }
427 AtomicFact::NotSubsetFact(fact) => {
428 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
429 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
430 }
431 AtomicFact::NotSupersetFact(fact) => {
432 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
433 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
434 }
435 AtomicFact::RestrictFact(fact) => {
436 mark_forall_param_coverage_in_obj(&fact.obj, coverage_by_forall_param);
437 mark_forall_param_coverage_in_obj(
438 &fact.obj_can_restrict_to_fn_set,
439 coverage_by_forall_param,
440 );
441 }
442 AtomicFact::NotRestrictFact(fact) => {
443 mark_forall_param_coverage_in_obj(&fact.obj, coverage_by_forall_param);
444 mark_forall_param_coverage_in_obj(
445 &fact.obj_cannot_restrict_to_fn_set,
446 coverage_by_forall_param,
447 );
448 }
449 AtomicFact::FnEqualInFact(fact) => {
450 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
451 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
452 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
453 }
454 AtomicFact::FnEqualFact(fact) => {
455 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
456 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
457 }
458 }
459}
460
461fn mark_forall_param_coverage_in_and_chain_atomic_fact(
462 parent_fact: &AndChainAtomicFact,
463 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
464) {
465 match parent_fact {
466 AndChainAtomicFact::AtomicFact(atomic_fact) => {
467 mark_forall_param_coverage_in_atomic_fact(atomic_fact, coverage_by_forall_param);
468 }
469 AndChainAtomicFact::AndFact(and_fact) => {
470 for inner_atomic in and_fact.facts.iter() {
471 mark_forall_param_coverage_in_atomic_fact(inner_atomic, coverage_by_forall_param);
472 }
473 }
474 AndChainAtomicFact::ChainFact(chain_fact) => {
475 for chain_obj in chain_fact.objs.iter() {
476 mark_forall_param_coverage_in_obj(chain_obj, coverage_by_forall_param);
477 }
478 }
479 }
480}
481
482fn mark_forall_param_coverage_in_or_and_chain_atomic_fact(
483 parent_fact: &OrAndChainAtomicFact,
484 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
485) {
486 match parent_fact {
487 OrAndChainAtomicFact::AtomicFact(atomic_fact) => {
488 mark_forall_param_coverage_in_atomic_fact(atomic_fact, coverage_by_forall_param);
489 }
490 OrAndChainAtomicFact::AndFact(and_fact) => {
491 for inner_atomic in and_fact.facts.iter() {
492 mark_forall_param_coverage_in_atomic_fact(inner_atomic, coverage_by_forall_param);
493 }
494 }
495 OrAndChainAtomicFact::ChainFact(chain_fact) => {
496 for chain_obj in chain_fact.objs.iter() {
497 mark_forall_param_coverage_in_obj(chain_obj, coverage_by_forall_param);
498 }
499 }
500 OrAndChainAtomicFact::OrFact(or_fact) => {
501 for branch in or_fact.facts.iter() {
502 mark_forall_param_coverage_in_and_chain_atomic_fact(
503 branch,
504 coverage_by_forall_param,
505 );
506 }
507 }
508 }
509}
510
511fn mark_forall_param_coverage_in_exist_fact(
512 exist_fact: &ExistFactEnum,
513 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
514) {
515 for param_def_with_type in exist_fact.params_def_with_type().groups.iter() {
516 mark_forall_param_coverage_in_param_type(
517 ¶m_def_with_type.param_type,
518 coverage_by_forall_param,
519 );
520 }
521 for inner_fact in exist_fact.facts().iter() {
522 mark_forall_param_coverage_in_or_and_chain_atomic_fact(
523 inner_fact,
524 coverage_by_forall_param,
525 );
526 }
527}
528
529fn mark_forall_param_coverage_in_exist_or_and_chain_atomic_fact(
530 parent_fact: &ExistOrAndChainAtomicFact,
531 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
532) {
533 match parent_fact {
534 ExistOrAndChainAtomicFact::AtomicFact(atomic_fact) => {
535 mark_forall_param_coverage_in_atomic_fact(atomic_fact, coverage_by_forall_param);
536 }
537 ExistOrAndChainAtomicFact::AndFact(and_fact) => {
538 for inner_atomic in and_fact.facts.iter() {
539 mark_forall_param_coverage_in_atomic_fact(inner_atomic, coverage_by_forall_param);
540 }
541 }
542 ExistOrAndChainAtomicFact::ChainFact(chain_fact) => {
543 for chain_obj in chain_fact.objs.iter() {
544 mark_forall_param_coverage_in_obj(chain_obj, coverage_by_forall_param);
545 }
546 }
547 ExistOrAndChainAtomicFact::OrFact(or_fact) => {
548 for branch in or_fact.facts.iter() {
549 mark_forall_param_coverage_in_and_chain_atomic_fact(
550 branch,
551 coverage_by_forall_param,
552 );
553 }
554 }
555 ExistOrAndChainAtomicFact::ExistFact(exist_fact) => {
556 mark_forall_param_coverage_in_exist_fact(exist_fact, coverage_by_forall_param);
557 }
558 }
559}
560
561impl ForallFact {
562 pub fn error_messages_if_forall_param_missing_in_some_then_clause(
563 &self,
564 ) -> Vec<(usize, String)> {
565 let forall_param_names = self.params_def_with_type.collect_param_names();
566 if forall_param_names.is_empty() {
567 return Vec::new();
568 }
569 let mut error_messages = Vec::new();
570 let mut then_index: usize = 0;
571 while then_index < self.then_facts.len() {
572 let then_fact = &self.then_facts[then_index];
573 let mut coverage_by_forall_param: HashMap<IdentifierName, bool> = HashMap::new();
574 for param_name in forall_param_names.iter() {
575 coverage_by_forall_param.insert(param_name.clone(), false);
576 }
577 mark_forall_param_coverage_in_exist_or_and_chain_atomic_fact(
578 then_fact,
579 &mut coverage_by_forall_param,
580 );
581 let mut missing_param_names = Vec::new();
582 for param_name in forall_param_names.iter() {
583 let is_mentioned_in_then_clause = match coverage_by_forall_param.get(param_name) {
584 Some(flag) => *flag,
585 None => false,
586 };
587 if !is_mentioned_in_then_clause {
588 missing_param_names.push(param_name.clone());
589 }
590 }
591 if !missing_param_names.is_empty() {
592 let missing_list = missing_param_names.join(", ");
593 error_messages.push((
594 then_index,
595 format!(
596 "then-clause `{}` does not mention forall parameter(s) {{{}}}",
597 then_fact, missing_list,
598 ),
599 ));
600 }
601 then_index += 1;
602 }
603 error_messages
604 }
605}
606
607impl ForallFactWithIff {
608 pub fn error_messages_if_forall_param_missing_in_forall_then_clause(
610 &self,
611 ) -> Vec<(usize, String)> {
612 self.forall_fact
613 .error_messages_if_forall_param_missing_in_some_then_clause()
614 }
615}