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::Set(_) | ParamType::NonemptySet(_) | ParamType::FiniteSet(_) => {}
28 }
29}
30
31fn mark_forall_param_coverage_in_fn_obj_head(
32 head: &FnObjHead,
33 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
34) {
35 match head {
36 FnObjHead::Identifier(i) => {
37 mark_forall_param_coverage_in_obj(
38 &Obj::Atom(AtomObj::Identifier(i.clone())),
39 coverage_by_forall_param,
40 );
41 }
42 FnObjHead::IdentifierWithMod(m) => {
43 mark_forall_param_coverage_in_obj(
44 &Obj::Atom(AtomObj::IdentifierWithMod(m.clone())),
45 coverage_by_forall_param,
46 );
47 }
48 FnObjHead::Forall(p) => {
49 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
50 }
51 FnObjHead::DefHeader(_)
52 | FnObjHead::Exist(_)
53 | FnObjHead::SetBuilder(_)
54 | FnObjHead::FnSet(_)
55 | FnObjHead::Induc(_)
56 | FnObjHead::DefAlgo(_) => {}
57 FnObjHead::AnonymousFnLiteral(a) => {
58 mark_forall_param_coverage_in_obj(
59 &Obj::AnonymousFn((**a).clone()),
60 coverage_by_forall_param,
61 );
62 }
63 }
64}
65
66fn mark_forall_param_coverage_in_obj(
67 obj: &Obj,
68 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
69) {
70 match obj {
71 Obj::Atom(AtomObj::Identifier(identifier)) => {
72 mark_forall_param_name_if_tracked(coverage_by_forall_param, &identifier.name);
73 }
74 Obj::Atom(AtomObj::IdentifierWithMod(_)) => {}
75 Obj::FnObj(fn_obj) => {
76 mark_forall_param_coverage_in_fn_obj_head(
77 fn_obj.head.as_ref(),
78 coverage_by_forall_param,
79 );
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(
202 fn_set.body.ret_set.as_ref(),
203 coverage_by_forall_param,
204 );
205 }
206 Obj::AnonymousFn(anon) => {
207 for param_def_with_set in anon.body.params_def_with_set.iter() {
208 mark_forall_param_coverage_in_obj(
209 ¶m_def_with_set.set,
210 coverage_by_forall_param,
211 );
212 }
213 for dom_fact in anon.body.dom_facts.iter() {
214 mark_forall_param_coverage_in_or_and_chain_atomic_fact(
215 dom_fact,
216 coverage_by_forall_param,
217 );
218 }
219 mark_forall_param_coverage_in_obj(anon.body.ret_set.as_ref(), coverage_by_forall_param);
220 mark_forall_param_coverage_in_obj(anon.equal_to.as_ref(), coverage_by_forall_param);
221 }
222 Obj::Cart(cart) => {
223 for boxed_arg in cart.args.iter() {
224 mark_forall_param_coverage_in_obj(boxed_arg.as_ref(), coverage_by_forall_param);
225 }
226 }
227 Obj::CartDim(cart_dim) => {
228 mark_forall_param_coverage_in_obj(cart_dim.set.as_ref(), coverage_by_forall_param);
229 }
230 Obj::Proj(proj) => {
231 mark_forall_param_coverage_in_obj(proj.set.as_ref(), coverage_by_forall_param);
232 mark_forall_param_coverage_in_obj(proj.dim.as_ref(), coverage_by_forall_param);
233 }
234 Obj::TupleDim(tuple_dim) => {
235 mark_forall_param_coverage_in_obj(tuple_dim.arg.as_ref(), coverage_by_forall_param);
236 }
237 Obj::Tuple(tuple_obj) => {
238 for boxed_arg in tuple_obj.args.iter() {
239 mark_forall_param_coverage_in_obj(boxed_arg.as_ref(), coverage_by_forall_param);
240 }
241 }
242 Obj::Count(count) => {
243 mark_forall_param_coverage_in_obj(count.set.as_ref(), coverage_by_forall_param);
244 }
245 Obj::Sum(s) => {
246 mark_forall_param_coverage_in_obj(s.start.as_ref(), coverage_by_forall_param);
247 mark_forall_param_coverage_in_obj(s.end.as_ref(), coverage_by_forall_param);
248 mark_forall_param_coverage_in_obj(s.func.as_ref(), coverage_by_forall_param);
249 }
250 Obj::Product(s) => {
251 mark_forall_param_coverage_in_obj(s.start.as_ref(), coverage_by_forall_param);
252 mark_forall_param_coverage_in_obj(s.end.as_ref(), coverage_by_forall_param);
253 mark_forall_param_coverage_in_obj(s.func.as_ref(), coverage_by_forall_param);
254 }
255 Obj::Range(range) => {
256 mark_forall_param_coverage_in_obj(range.start.as_ref(), coverage_by_forall_param);
257 mark_forall_param_coverage_in_obj(range.end.as_ref(), coverage_by_forall_param);
258 }
259 Obj::ClosedRange(closed_range) => {
260 mark_forall_param_coverage_in_obj(
261 closed_range.start.as_ref(),
262 coverage_by_forall_param,
263 );
264 mark_forall_param_coverage_in_obj(closed_range.end.as_ref(), coverage_by_forall_param);
265 }
266 Obj::FiniteSeqSet(fs) => {
267 mark_forall_param_coverage_in_obj(fs.set.as_ref(), coverage_by_forall_param);
268 mark_forall_param_coverage_in_obj(fs.n.as_ref(), coverage_by_forall_param);
269 }
270 Obj::SeqSet(ss) => {
271 mark_forall_param_coverage_in_obj(ss.set.as_ref(), coverage_by_forall_param);
272 }
273 Obj::FiniteSeqListObj(v) => {
274 for o in v.objs.iter() {
275 mark_forall_param_coverage_in_obj(o.as_ref(), coverage_by_forall_param);
276 }
277 }
278 Obj::MatrixSet(ms) => {
279 mark_forall_param_coverage_in_obj(ms.set.as_ref(), coverage_by_forall_param);
280 mark_forall_param_coverage_in_obj(ms.row_len.as_ref(), coverage_by_forall_param);
281 mark_forall_param_coverage_in_obj(ms.col_len.as_ref(), coverage_by_forall_param);
282 }
283 Obj::MatrixListObj(v) => {
284 for row in v.rows.iter() {
285 for o in row.iter() {
286 mark_forall_param_coverage_in_obj(o.as_ref(), coverage_by_forall_param);
287 }
288 }
289 }
290 Obj::Choose(choose) => {
291 mark_forall_param_coverage_in_obj(choose.set.as_ref(), coverage_by_forall_param);
292 }
293 Obj::ObjAtIndex(obj_at_index) => {
294 mark_forall_param_coverage_in_obj(obj_at_index.obj.as_ref(), coverage_by_forall_param);
295 mark_forall_param_coverage_in_obj(
296 obj_at_index.index.as_ref(),
297 coverage_by_forall_param,
298 );
299 }
300 Obj::FamilyObj(family) => {
301 for o in family.params.iter() {
302 mark_forall_param_coverage_in_obj(o, coverage_by_forall_param);
303 }
304 }
305 Obj::Atom(AtomObj::Forall(p)) => {
306 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
307 }
308 Obj::Atom(AtomObj::Def(p)) => {
309 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
310 }
311 Obj::Atom(AtomObj::Exist(p)) => {
312 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
313 }
314 Obj::Atom(AtomObj::SetBuilder(p)) => {
315 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
316 }
317 Obj::Atom(AtomObj::FnSet(p)) => {
318 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
319 }
320 Obj::Atom(AtomObj::Induc(p)) => {
321 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
322 }
323 Obj::Atom(AtomObj::DefAlgo(p)) => {
324 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
325 }
326 }
327}
328
329fn mark_forall_param_coverage_in_atomic_fact(
330 atomic_fact: &AtomicFact,
331 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
332) {
333 match atomic_fact {
334 AtomicFact::NormalAtomicFact(fact) => {
335 for body_obj in fact.body.iter() {
336 mark_forall_param_coverage_in_obj(body_obj, coverage_by_forall_param);
337 }
338 }
339 AtomicFact::NotNormalAtomicFact(fact) => {
340 for body_obj in fact.body.iter() {
341 mark_forall_param_coverage_in_obj(body_obj, coverage_by_forall_param);
342 }
343 }
344 AtomicFact::EqualFact(fact) => {
345 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
346 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
347 }
348 AtomicFact::LessFact(fact) => {
349 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
350 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
351 }
352 AtomicFact::GreaterFact(fact) => {
353 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
354 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
355 }
356 AtomicFact::LessEqualFact(fact) => {
357 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
358 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
359 }
360 AtomicFact::GreaterEqualFact(fact) => {
361 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
362 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
363 }
364 AtomicFact::NotEqualFact(fact) => {
365 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
366 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
367 }
368 AtomicFact::NotLessFact(fact) => {
369 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
370 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
371 }
372 AtomicFact::NotGreaterFact(fact) => {
373 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
374 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
375 }
376 AtomicFact::NotLessEqualFact(fact) => {
377 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
378 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
379 }
380 AtomicFact::NotGreaterEqualFact(fact) => {
381 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
382 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
383 }
384 AtomicFact::IsSetFact(fact) => {
385 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
386 }
387 AtomicFact::NotIsSetFact(fact) => {
388 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
389 }
390 AtomicFact::IsNonemptySetFact(fact) => {
391 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
392 }
393 AtomicFact::NotIsNonemptySetFact(fact) => {
394 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
395 }
396 AtomicFact::IsFiniteSetFact(fact) => {
397 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
398 }
399 AtomicFact::NotIsFiniteSetFact(fact) => {
400 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
401 }
402 AtomicFact::InFact(fact) => {
403 mark_forall_param_coverage_in_obj(&fact.element, coverage_by_forall_param);
404 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
405 }
406 AtomicFact::NotInFact(fact) => {
407 mark_forall_param_coverage_in_obj(&fact.element, coverage_by_forall_param);
408 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
409 }
410 AtomicFact::IsCartFact(fact) => {
411 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
412 }
413 AtomicFact::NotIsCartFact(fact) => {
414 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
415 }
416 AtomicFact::IsTupleFact(fact) => {
417 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
418 }
419 AtomicFact::NotIsTupleFact(fact) => {
420 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
421 }
422 AtomicFact::SubsetFact(fact) => {
423 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
424 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
425 }
426 AtomicFact::SupersetFact(fact) => {
427 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
428 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
429 }
430 AtomicFact::NotSubsetFact(fact) => {
431 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
432 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
433 }
434 AtomicFact::NotSupersetFact(fact) => {
435 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
436 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
437 }
438 AtomicFact::RestrictFact(fact) => {
439 mark_forall_param_coverage_in_obj(&fact.obj, coverage_by_forall_param);
440 mark_forall_param_coverage_in_obj(
441 &fact.obj_can_restrict_to_fn_set,
442 coverage_by_forall_param,
443 );
444 }
445 AtomicFact::NotRestrictFact(fact) => {
446 mark_forall_param_coverage_in_obj(&fact.obj, coverage_by_forall_param);
447 mark_forall_param_coverage_in_obj(
448 &fact.obj_cannot_restrict_to_fn_set,
449 coverage_by_forall_param,
450 );
451 }
452 AtomicFact::FnEqualInFact(fact) => {
453 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
454 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
455 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
456 }
457 AtomicFact::FnEqualFact(fact) => {
458 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
459 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
460 }
461 }
462}
463
464fn mark_forall_param_coverage_in_and_chain_atomic_fact(
465 parent_fact: &AndChainAtomicFact,
466 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
467) {
468 match parent_fact {
469 AndChainAtomicFact::AtomicFact(atomic_fact) => {
470 mark_forall_param_coverage_in_atomic_fact(atomic_fact, coverage_by_forall_param);
471 }
472 AndChainAtomicFact::AndFact(and_fact) => {
473 for inner_atomic in and_fact.facts.iter() {
474 mark_forall_param_coverage_in_atomic_fact(inner_atomic, coverage_by_forall_param);
475 }
476 }
477 AndChainAtomicFact::ChainFact(chain_fact) => {
478 for chain_obj in chain_fact.objs.iter() {
479 mark_forall_param_coverage_in_obj(chain_obj, coverage_by_forall_param);
480 }
481 }
482 }
483}
484
485fn mark_forall_param_coverage_in_or_and_chain_atomic_fact(
486 parent_fact: &OrAndChainAtomicFact,
487 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
488) {
489 match parent_fact {
490 OrAndChainAtomicFact::AtomicFact(atomic_fact) => {
491 mark_forall_param_coverage_in_atomic_fact(atomic_fact, coverage_by_forall_param);
492 }
493 OrAndChainAtomicFact::AndFact(and_fact) => {
494 for inner_atomic in and_fact.facts.iter() {
495 mark_forall_param_coverage_in_atomic_fact(inner_atomic, coverage_by_forall_param);
496 }
497 }
498 OrAndChainAtomicFact::ChainFact(chain_fact) => {
499 for chain_obj in chain_fact.objs.iter() {
500 mark_forall_param_coverage_in_obj(chain_obj, coverage_by_forall_param);
501 }
502 }
503 OrAndChainAtomicFact::OrFact(or_fact) => {
504 for branch in or_fact.facts.iter() {
505 mark_forall_param_coverage_in_and_chain_atomic_fact(
506 branch,
507 coverage_by_forall_param,
508 );
509 }
510 }
511 }
512}
513
514fn mark_forall_param_coverage_in_exist_body_fact(
515 parent_fact: &ExistBodyFact,
516 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
517) {
518 match parent_fact {
519 ExistBodyFact::AtomicFact(atomic_fact) => {
520 mark_forall_param_coverage_in_atomic_fact(atomic_fact, coverage_by_forall_param);
521 }
522 ExistBodyFact::AndFact(and_fact) => {
523 for inner_atomic in and_fact.facts.iter() {
524 mark_forall_param_coverage_in_atomic_fact(inner_atomic, coverage_by_forall_param);
525 }
526 }
527 ExistBodyFact::ChainFact(chain_fact) => {
528 for chain_obj in chain_fact.objs.iter() {
529 mark_forall_param_coverage_in_obj(chain_obj, coverage_by_forall_param);
530 }
531 }
532 ExistBodyFact::OrFact(or_fact) => {
533 for branch in or_fact.facts.iter() {
534 mark_forall_param_coverage_in_and_chain_atomic_fact(
535 branch,
536 coverage_by_forall_param,
537 );
538 }
539 }
540 ExistBodyFact::InlineForall(forall_fact) => {
541 for param_def_with_type in forall_fact.params_def_with_type.groups.iter() {
542 mark_forall_param_coverage_in_param_type(
543 ¶m_def_with_type.param_type,
544 coverage_by_forall_param,
545 );
546 }
547 for fact in forall_fact.dom_facts.iter() {
548 mark_forall_param_coverage_in_fact(fact, coverage_by_forall_param);
549 }
550 for fact in forall_fact.then_facts.iter() {
551 mark_forall_param_coverage_in_exist_or_and_chain_atomic_fact(
552 fact,
553 coverage_by_forall_param,
554 );
555 }
556 }
557 }
558}
559
560fn mark_forall_param_coverage_in_fact(
561 parent_fact: &Fact,
562 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
563) {
564 match parent_fact {
565 Fact::AtomicFact(atomic_fact) => {
566 mark_forall_param_coverage_in_atomic_fact(atomic_fact, coverage_by_forall_param);
567 }
568 Fact::ExistFact(exist_fact) => {
569 mark_forall_param_coverage_in_exist_fact(exist_fact, coverage_by_forall_param);
570 }
571 Fact::OrFact(or_fact) => {
572 for branch in or_fact.facts.iter() {
573 mark_forall_param_coverage_in_and_chain_atomic_fact(
574 branch,
575 coverage_by_forall_param,
576 );
577 }
578 }
579 Fact::AndFact(and_fact) => {
580 for atomic_fact in and_fact.facts.iter() {
581 mark_forall_param_coverage_in_atomic_fact(atomic_fact, coverage_by_forall_param);
582 }
583 }
584 Fact::ChainFact(chain_fact) => {
585 for chain_obj in chain_fact.objs.iter() {
586 mark_forall_param_coverage_in_obj(chain_obj, coverage_by_forall_param);
587 }
588 }
589 Fact::ForallFact(forall_fact) => {
590 for fact in forall_fact.dom_facts.iter() {
591 mark_forall_param_coverage_in_fact(fact, coverage_by_forall_param);
592 }
593 for fact in forall_fact.then_facts.iter() {
594 mark_forall_param_coverage_in_exist_or_and_chain_atomic_fact(
595 fact,
596 coverage_by_forall_param,
597 );
598 }
599 }
600 Fact::ForallFactWithIff(_) | Fact::NotForall(_) => {}
601 }
602}
603
604fn mark_forall_param_coverage_in_exist_fact(
605 exist_fact: &ExistFactEnum,
606 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
607) {
608 for param_def_with_type in exist_fact.params_def_with_type().groups.iter() {
609 mark_forall_param_coverage_in_param_type(
610 ¶m_def_with_type.param_type,
611 coverage_by_forall_param,
612 );
613 }
614 for inner_fact in exist_fact.facts().iter() {
615 mark_forall_param_coverage_in_exist_body_fact(inner_fact, coverage_by_forall_param);
616 }
617}
618
619fn mark_forall_param_coverage_in_exist_or_and_chain_atomic_fact(
620 parent_fact: &ExistOrAndChainAtomicFact,
621 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
622) {
623 match parent_fact {
624 ExistOrAndChainAtomicFact::AtomicFact(atomic_fact) => {
625 mark_forall_param_coverage_in_atomic_fact(atomic_fact, coverage_by_forall_param);
626 }
627 ExistOrAndChainAtomicFact::AndFact(and_fact) => {
628 for inner_atomic in and_fact.facts.iter() {
629 mark_forall_param_coverage_in_atomic_fact(inner_atomic, coverage_by_forall_param);
630 }
631 }
632 ExistOrAndChainAtomicFact::ChainFact(chain_fact) => {
633 for chain_obj in chain_fact.objs.iter() {
634 mark_forall_param_coverage_in_obj(chain_obj, coverage_by_forall_param);
635 }
636 }
637 ExistOrAndChainAtomicFact::OrFact(or_fact) => {
638 for branch in or_fact.facts.iter() {
639 mark_forall_param_coverage_in_and_chain_atomic_fact(
640 branch,
641 coverage_by_forall_param,
642 );
643 }
644 }
645 ExistOrAndChainAtomicFact::ExistFact(exist_fact) => {
646 mark_forall_param_coverage_in_exist_fact(exist_fact, coverage_by_forall_param);
647 }
648 }
649}
650
651impl ForallFact {
652 pub fn error_messages_if_forall_param_missing_in_some_then_clause(
653 &self,
654 ) -> Vec<(usize, String)> {
655 let forall_param_names = self.params_def_with_type.collect_param_names();
656 if forall_param_names.is_empty() {
657 return Vec::new();
658 }
659 let mut error_messages = Vec::new();
660 let mut then_index: usize = 0;
661 while then_index < self.then_facts.len() {
662 let then_fact = &self.then_facts[then_index];
663 let mut coverage_by_forall_param: HashMap<IdentifierName, bool> = HashMap::new();
664 for param_name in forall_param_names.iter() {
665 coverage_by_forall_param.insert(param_name.clone(), false);
666 }
667 mark_forall_param_coverage_in_exist_or_and_chain_atomic_fact(
668 then_fact,
669 &mut coverage_by_forall_param,
670 );
671 let mut missing_param_names = Vec::new();
672 for param_name in forall_param_names.iter() {
673 let is_mentioned_in_then_clause = match coverage_by_forall_param.get(param_name) {
674 Some(flag) => *flag,
675 None => false,
676 };
677 if !is_mentioned_in_then_clause {
678 missing_param_names.push(param_name.clone());
679 }
680 }
681 if !missing_param_names.is_empty() {
682 let missing_list = missing_param_names.join(", ");
683 error_messages.push((
684 then_index,
685 format!(
686 "then-clause `{}` does not mention forall parameter(s) {{{}}}",
687 then_fact, missing_list,
688 ),
689 ));
690 }
691 then_index += 1;
692 }
693 error_messages
694 }
695}
696
697impl ForallFactWithIff {
698 pub fn error_messages_if_forall_param_missing_in_forall_then_clause(
700 &self,
701 ) -> Vec<(usize, String)> {
702 self.forall_fact
703 .error_messages_if_forall_param_missing_in_some_then_clause()
704 }
705}