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::FiniteSeqListObj(v) => {
58 mark_forall_param_coverage_in_obj(
59 &Obj::FiniteSeqListObj(v.clone()),
60 coverage_by_forall_param,
61 );
62 }
63 FnObjHead::AnonymousFnLiteral(a) => {
64 mark_forall_param_coverage_in_obj(
65 &Obj::AnonymousFn((**a).clone()),
66 coverage_by_forall_param,
67 );
68 }
69 }
70}
71
72fn mark_forall_param_coverage_in_obj(
73 obj: &Obj,
74 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
75) {
76 match obj {
77 Obj::Atom(AtomObj::Identifier(identifier)) => {
78 mark_forall_param_name_if_tracked(coverage_by_forall_param, &identifier.name);
79 }
80 Obj::Atom(AtomObj::IdentifierWithMod(_)) => {}
81 Obj::FnObj(fn_obj) => {
82 mark_forall_param_coverage_in_fn_obj_head(
83 fn_obj.head.as_ref(),
84 coverage_by_forall_param,
85 );
86 for group in fn_obj.body.iter() {
87 for boxed_obj in group.iter() {
88 mark_forall_param_coverage_in_obj(boxed_obj.as_ref(), coverage_by_forall_param);
89 }
90 }
91 }
92 Obj::Number(_) | Obj::StandardSet(_) => {}
93 Obj::Add(binary) => {
94 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
95 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
96 }
97 Obj::Sub(binary) => {
98 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
99 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
100 }
101 Obj::Mul(binary) => {
102 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
103 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
104 }
105 Obj::Div(binary) => {
106 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
107 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
108 }
109 Obj::Mod(binary) => {
110 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
111 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
112 }
113 Obj::Pow(binary) => {
114 mark_forall_param_coverage_in_obj(binary.base.as_ref(), coverage_by_forall_param);
115 mark_forall_param_coverage_in_obj(binary.exponent.as_ref(), coverage_by_forall_param);
116 }
117 Obj::MatrixAdd(binary) => {
118 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
119 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
120 }
121 Obj::MatrixSub(binary) => {
122 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
123 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
124 }
125 Obj::MatrixMul(binary) => {
126 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
127 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
128 }
129 Obj::MatrixScalarMul(binary) => {
130 mark_forall_param_coverage_in_obj(binary.scalar.as_ref(), coverage_by_forall_param);
131 mark_forall_param_coverage_in_obj(binary.matrix.as_ref(), coverage_by_forall_param);
132 }
133 Obj::MatrixPow(binary) => {
134 mark_forall_param_coverage_in_obj(binary.base.as_ref(), coverage_by_forall_param);
135 mark_forall_param_coverage_in_obj(binary.exponent.as_ref(), coverage_by_forall_param);
136 }
137 Obj::Abs(unary) => {
138 mark_forall_param_coverage_in_obj(unary.arg.as_ref(), coverage_by_forall_param);
139 }
140 Obj::Log(binary) => {
141 mark_forall_param_coverage_in_obj(binary.base.as_ref(), coverage_by_forall_param);
142 mark_forall_param_coverage_in_obj(binary.arg.as_ref(), coverage_by_forall_param);
143 }
144 Obj::Max(binary) => {
145 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
146 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
147 }
148 Obj::Min(binary) => {
149 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
150 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
151 }
152 Obj::Union(binary) => {
153 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
154 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
155 }
156 Obj::Intersect(binary) => {
157 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
158 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
159 }
160 Obj::SetMinus(binary) => {
161 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
162 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
163 }
164 Obj::SetDiff(binary) => {
165 mark_forall_param_coverage_in_obj(binary.left.as_ref(), coverage_by_forall_param);
166 mark_forall_param_coverage_in_obj(binary.right.as_ref(), coverage_by_forall_param);
167 }
168 Obj::Cup(unary) => {
169 mark_forall_param_coverage_in_obj(unary.left.as_ref(), coverage_by_forall_param);
170 }
171 Obj::Cap(unary) => {
172 mark_forall_param_coverage_in_obj(unary.left.as_ref(), coverage_by_forall_param);
173 }
174 Obj::PowerSet(unary) => {
175 mark_forall_param_coverage_in_obj(unary.set.as_ref(), coverage_by_forall_param);
176 }
177 Obj::ListSet(list_set) => {
178 for boxed_obj in list_set.list.iter() {
179 mark_forall_param_coverage_in_obj(boxed_obj.as_ref(), coverage_by_forall_param);
180 }
181 }
182 Obj::SetBuilder(set_builder) => {
183 mark_forall_param_coverage_in_obj(
184 set_builder.param_set.as_ref(),
185 coverage_by_forall_param,
186 );
187 for inner_fact in set_builder.facts.iter() {
188 mark_forall_param_coverage_in_or_and_chain_atomic_fact(
189 inner_fact,
190 coverage_by_forall_param,
191 );
192 }
193 }
194 Obj::FnSet(fn_set) => {
195 for param_def_with_set in fn_set.body.params_def_with_set.iter() {
196 mark_forall_param_coverage_in_obj(
197 param_def_with_set.set_obj(),
198 coverage_by_forall_param,
199 );
200 }
201 for dom_fact in fn_set.body.dom_facts.iter() {
202 mark_forall_param_coverage_in_or_and_chain_atomic_fact(
203 dom_fact,
204 coverage_by_forall_param,
205 );
206 }
207 mark_forall_param_coverage_in_obj(
208 fn_set.body.ret_set.as_ref(),
209 coverage_by_forall_param,
210 );
211 }
212 Obj::AnonymousFn(anon) => {
213 for param_def_with_set in anon.body.params_def_with_set.iter() {
214 mark_forall_param_coverage_in_obj(
215 param_def_with_set.set_obj(),
216 coverage_by_forall_param,
217 );
218 }
219 for dom_fact in anon.body.dom_facts.iter() {
220 mark_forall_param_coverage_in_or_and_chain_atomic_fact(
221 dom_fact,
222 coverage_by_forall_param,
223 );
224 }
225 mark_forall_param_coverage_in_obj(anon.body.ret_set.as_ref(), coverage_by_forall_param);
226 mark_forall_param_coverage_in_obj(anon.equal_to.as_ref(), coverage_by_forall_param);
227 }
228 Obj::Cart(cart) => {
229 for boxed_arg in cart.args.iter() {
230 mark_forall_param_coverage_in_obj(boxed_arg.as_ref(), coverage_by_forall_param);
231 }
232 }
233 Obj::CartDim(cart_dim) => {
234 mark_forall_param_coverage_in_obj(cart_dim.set.as_ref(), coverage_by_forall_param);
235 }
236 Obj::Proj(proj) => {
237 mark_forall_param_coverage_in_obj(proj.set.as_ref(), coverage_by_forall_param);
238 mark_forall_param_coverage_in_obj(proj.dim.as_ref(), coverage_by_forall_param);
239 }
240 Obj::TupleDim(tuple_dim) => {
241 mark_forall_param_coverage_in_obj(tuple_dim.arg.as_ref(), coverage_by_forall_param);
242 }
243 Obj::Tuple(tuple_obj) => {
244 for boxed_arg in tuple_obj.args.iter() {
245 mark_forall_param_coverage_in_obj(boxed_arg.as_ref(), coverage_by_forall_param);
246 }
247 }
248 Obj::Count(count) => {
249 mark_forall_param_coverage_in_obj(count.set.as_ref(), coverage_by_forall_param);
250 }
251 Obj::Sum(s) => {
252 mark_forall_param_coverage_in_obj(s.start.as_ref(), coverage_by_forall_param);
253 mark_forall_param_coverage_in_obj(s.end.as_ref(), coverage_by_forall_param);
254 mark_forall_param_coverage_in_obj(s.func.as_ref(), coverage_by_forall_param);
255 }
256 Obj::Product(s) => {
257 mark_forall_param_coverage_in_obj(s.start.as_ref(), coverage_by_forall_param);
258 mark_forall_param_coverage_in_obj(s.end.as_ref(), coverage_by_forall_param);
259 mark_forall_param_coverage_in_obj(s.func.as_ref(), coverage_by_forall_param);
260 }
261 Obj::Range(range) => {
262 mark_forall_param_coverage_in_obj(range.start.as_ref(), coverage_by_forall_param);
263 mark_forall_param_coverage_in_obj(range.end.as_ref(), coverage_by_forall_param);
264 }
265 Obj::ClosedRange(closed_range) => {
266 mark_forall_param_coverage_in_obj(
267 closed_range.start.as_ref(),
268 coverage_by_forall_param,
269 );
270 mark_forall_param_coverage_in_obj(closed_range.end.as_ref(), coverage_by_forall_param);
271 }
272 Obj::FiniteSeqSet(fs) => {
273 mark_forall_param_coverage_in_obj(fs.set.as_ref(), coverage_by_forall_param);
274 mark_forall_param_coverage_in_obj(fs.n.as_ref(), coverage_by_forall_param);
275 }
276 Obj::SeqSet(ss) => {
277 mark_forall_param_coverage_in_obj(ss.set.as_ref(), coverage_by_forall_param);
278 }
279 Obj::FiniteSeqListObj(v) => {
280 for o in v.objs.iter() {
281 mark_forall_param_coverage_in_obj(o.as_ref(), coverage_by_forall_param);
282 }
283 }
284 Obj::MatrixSet(ms) => {
285 mark_forall_param_coverage_in_obj(ms.set.as_ref(), coverage_by_forall_param);
286 mark_forall_param_coverage_in_obj(ms.row_len.as_ref(), coverage_by_forall_param);
287 mark_forall_param_coverage_in_obj(ms.col_len.as_ref(), coverage_by_forall_param);
288 }
289 Obj::MatrixListObj(v) => {
290 for row in v.rows.iter() {
291 for o in row.iter() {
292 mark_forall_param_coverage_in_obj(o.as_ref(), coverage_by_forall_param);
293 }
294 }
295 }
296 Obj::Choose(choose) => {
297 mark_forall_param_coverage_in_obj(choose.set.as_ref(), coverage_by_forall_param);
298 }
299 Obj::ObjAtIndex(obj_at_index) => {
300 mark_forall_param_coverage_in_obj(obj_at_index.obj.as_ref(), coverage_by_forall_param);
301 mark_forall_param_coverage_in_obj(
302 obj_at_index.index.as_ref(),
303 coverage_by_forall_param,
304 );
305 }
306 Obj::FamilyObj(family) => {
307 for o in family.params.iter() {
308 mark_forall_param_coverage_in_obj(o, coverage_by_forall_param);
309 }
310 }
311 Obj::StructObj(struct_obj) => {
312 for o in struct_obj.params.iter() {
313 mark_forall_param_coverage_in_obj(o, coverage_by_forall_param);
314 }
315 }
316 Obj::ObjAsStructInstanceWithFieldAccess(field_access) => {
317 for o in field_access.struct_obj.params.iter() {
318 mark_forall_param_coverage_in_obj(o, coverage_by_forall_param);
319 }
320 mark_forall_param_coverage_in_obj(field_access.obj.as_ref(), coverage_by_forall_param);
321 }
322 Obj::Atom(AtomObj::Forall(p)) => {
323 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
324 }
325 Obj::Atom(AtomObj::Def(p)) => {
326 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
327 }
328 Obj::Atom(AtomObj::Exist(p)) => {
329 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
330 }
331 Obj::Atom(AtomObj::SetBuilder(p)) => {
332 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
333 }
334 Obj::Atom(AtomObj::FnSet(p)) => {
335 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
336 }
337 Obj::Atom(AtomObj::Induc(p)) => {
338 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
339 }
340 Obj::Atom(AtomObj::DefAlgo(p)) => {
341 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
342 }
343 Obj::Atom(AtomObj::DefStructField(_)) => {}
344 }
345}
346
347fn mark_forall_param_coverage_in_atomic_fact(
348 atomic_fact: &AtomicFact,
349 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
350) {
351 match atomic_fact {
352 AtomicFact::NormalAtomicFact(fact) => {
353 for body_obj in fact.body.iter() {
354 mark_forall_param_coverage_in_obj(body_obj, coverage_by_forall_param);
355 }
356 }
357 AtomicFact::NotNormalAtomicFact(fact) => {
358 for body_obj in fact.body.iter() {
359 mark_forall_param_coverage_in_obj(body_obj, coverage_by_forall_param);
360 }
361 }
362 AtomicFact::EqualFact(fact) => {
363 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
364 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
365 }
366 AtomicFact::LessFact(fact) => {
367 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
368 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
369 }
370 AtomicFact::GreaterFact(fact) => {
371 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
372 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
373 }
374 AtomicFact::LessEqualFact(fact) => {
375 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
376 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
377 }
378 AtomicFact::GreaterEqualFact(fact) => {
379 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
380 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
381 }
382 AtomicFact::NotEqualFact(fact) => {
383 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
384 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
385 }
386 AtomicFact::NotLessFact(fact) => {
387 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
388 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
389 }
390 AtomicFact::NotGreaterFact(fact) => {
391 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
392 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
393 }
394 AtomicFact::NotLessEqualFact(fact) => {
395 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
396 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
397 }
398 AtomicFact::NotGreaterEqualFact(fact) => {
399 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
400 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
401 }
402 AtomicFact::IsSetFact(fact) => {
403 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
404 }
405 AtomicFact::NotIsSetFact(fact) => {
406 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
407 }
408 AtomicFact::IsNonemptySetFact(fact) => {
409 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
410 }
411 AtomicFact::NotIsNonemptySetFact(fact) => {
412 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
413 }
414 AtomicFact::IsFiniteSetFact(fact) => {
415 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
416 }
417 AtomicFact::NotIsFiniteSetFact(fact) => {
418 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
419 }
420 AtomicFact::InFact(fact) => {
421 mark_forall_param_coverage_in_obj(&fact.element, coverage_by_forall_param);
422 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
423 }
424 AtomicFact::NotInFact(fact) => {
425 mark_forall_param_coverage_in_obj(&fact.element, coverage_by_forall_param);
426 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
427 }
428 AtomicFact::IsCartFact(fact) => {
429 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
430 }
431 AtomicFact::NotIsCartFact(fact) => {
432 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
433 }
434 AtomicFact::IsTupleFact(fact) => {
435 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
436 }
437 AtomicFact::NotIsTupleFact(fact) => {
438 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
439 }
440 AtomicFact::SubsetFact(fact) => {
441 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
442 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
443 }
444 AtomicFact::SupersetFact(fact) => {
445 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
446 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
447 }
448 AtomicFact::NotSubsetFact(fact) => {
449 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
450 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
451 }
452 AtomicFact::NotSupersetFact(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 }
456 AtomicFact::RestrictFact(fact) => {
457 mark_forall_param_coverage_in_obj(&fact.obj, coverage_by_forall_param);
458 mark_forall_param_coverage_in_obj(
459 &fact.obj_can_restrict_to_fn_set,
460 coverage_by_forall_param,
461 );
462 }
463 AtomicFact::NotRestrictFact(fact) => {
464 mark_forall_param_coverage_in_obj(&fact.obj, coverage_by_forall_param);
465 mark_forall_param_coverage_in_obj(
466 &fact.obj_cannot_restrict_to_fn_set,
467 coverage_by_forall_param,
468 );
469 }
470 AtomicFact::FnEqualInFact(fact) => {
471 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
472 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
473 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
474 }
475 AtomicFact::FnEqualFact(fact) => {
476 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
477 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
478 }
479 }
480}
481
482fn mark_forall_param_coverage_in_and_chain_atomic_fact(
483 parent_fact: &AndChainAtomicFact,
484 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
485) {
486 match parent_fact {
487 AndChainAtomicFact::AtomicFact(atomic_fact) => {
488 mark_forall_param_coverage_in_atomic_fact(atomic_fact, coverage_by_forall_param);
489 }
490 AndChainAtomicFact::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 AndChainAtomicFact::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 }
501}
502
503fn mark_forall_param_coverage_in_or_and_chain_atomic_fact(
504 parent_fact: &OrAndChainAtomicFact,
505 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
506) {
507 match parent_fact {
508 OrAndChainAtomicFact::AtomicFact(atomic_fact) => {
509 mark_forall_param_coverage_in_atomic_fact(atomic_fact, coverage_by_forall_param);
510 }
511 OrAndChainAtomicFact::AndFact(and_fact) => {
512 for inner_atomic in and_fact.facts.iter() {
513 mark_forall_param_coverage_in_atomic_fact(inner_atomic, coverage_by_forall_param);
514 }
515 }
516 OrAndChainAtomicFact::ChainFact(chain_fact) => {
517 for chain_obj in chain_fact.objs.iter() {
518 mark_forall_param_coverage_in_obj(chain_obj, coverage_by_forall_param);
519 }
520 }
521 OrAndChainAtomicFact::OrFact(or_fact) => {
522 for branch in or_fact.facts.iter() {
523 mark_forall_param_coverage_in_and_chain_atomic_fact(
524 branch,
525 coverage_by_forall_param,
526 );
527 }
528 }
529 }
530}
531
532fn mark_forall_param_coverage_in_exist_body_fact(
533 parent_fact: &ExistBodyFact,
534 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
535) {
536 match parent_fact {
537 ExistBodyFact::AtomicFact(atomic_fact) => {
538 mark_forall_param_coverage_in_atomic_fact(atomic_fact, coverage_by_forall_param);
539 }
540 ExistBodyFact::AndFact(and_fact) => {
541 for inner_atomic in and_fact.facts.iter() {
542 mark_forall_param_coverage_in_atomic_fact(inner_atomic, coverage_by_forall_param);
543 }
544 }
545 ExistBodyFact::ChainFact(chain_fact) => {
546 for chain_obj in chain_fact.objs.iter() {
547 mark_forall_param_coverage_in_obj(chain_obj, coverage_by_forall_param);
548 }
549 }
550 ExistBodyFact::OrFact(or_fact) => {
551 for branch in or_fact.facts.iter() {
552 mark_forall_param_coverage_in_and_chain_atomic_fact(
553 branch,
554 coverage_by_forall_param,
555 );
556 }
557 }
558 ExistBodyFact::InlineForall(forall_fact) => {
559 for param_def_with_type in forall_fact.params_def_with_type.groups.iter() {
560 mark_forall_param_coverage_in_param_type(
561 ¶m_def_with_type.param_type,
562 coverage_by_forall_param,
563 );
564 }
565 for fact in forall_fact.dom_facts.iter() {
566 mark_forall_param_coverage_in_fact(fact, coverage_by_forall_param);
567 }
568 for fact in forall_fact.then_facts.iter() {
569 mark_forall_param_coverage_in_exist_or_and_chain_atomic_fact(
570 fact,
571 coverage_by_forall_param,
572 );
573 }
574 }
575 }
576}
577
578fn mark_forall_param_coverage_in_fact(
579 parent_fact: &Fact,
580 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
581) {
582 match parent_fact {
583 Fact::AtomicFact(atomic_fact) => {
584 mark_forall_param_coverage_in_atomic_fact(atomic_fact, coverage_by_forall_param);
585 }
586 Fact::ExistFact(exist_fact) => {
587 mark_forall_param_coverage_in_exist_fact(exist_fact, coverage_by_forall_param);
588 }
589 Fact::OrFact(or_fact) => {
590 for branch in or_fact.facts.iter() {
591 mark_forall_param_coverage_in_and_chain_atomic_fact(
592 branch,
593 coverage_by_forall_param,
594 );
595 }
596 }
597 Fact::AndFact(and_fact) => {
598 for atomic_fact in and_fact.facts.iter() {
599 mark_forall_param_coverage_in_atomic_fact(atomic_fact, coverage_by_forall_param);
600 }
601 }
602 Fact::ChainFact(chain_fact) => {
603 for chain_obj in chain_fact.objs.iter() {
604 mark_forall_param_coverage_in_obj(chain_obj, coverage_by_forall_param);
605 }
606 }
607 Fact::ForallFact(forall_fact) => {
608 for fact in forall_fact.dom_facts.iter() {
609 mark_forall_param_coverage_in_fact(fact, coverage_by_forall_param);
610 }
611 for fact in forall_fact.then_facts.iter() {
612 mark_forall_param_coverage_in_exist_or_and_chain_atomic_fact(
613 fact,
614 coverage_by_forall_param,
615 );
616 }
617 }
618 Fact::ForallFactWithIff(_) | Fact::NotForall(_) => {}
619 }
620}
621
622fn mark_forall_param_coverage_in_exist_fact(
623 exist_fact: &ExistFactEnum,
624 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
625) {
626 for param_def_with_type in exist_fact.params_def_with_type().groups.iter() {
627 mark_forall_param_coverage_in_param_type(
628 ¶m_def_with_type.param_type,
629 coverage_by_forall_param,
630 );
631 }
632 for inner_fact in exist_fact.facts().iter() {
633 mark_forall_param_coverage_in_exist_body_fact(inner_fact, coverage_by_forall_param);
634 }
635}
636
637fn mark_forall_param_coverage_in_exist_or_and_chain_atomic_fact(
638 parent_fact: &ExistOrAndChainAtomicFact,
639 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
640) {
641 match parent_fact {
642 ExistOrAndChainAtomicFact::AtomicFact(atomic_fact) => {
643 mark_forall_param_coverage_in_atomic_fact(atomic_fact, coverage_by_forall_param);
644 }
645 ExistOrAndChainAtomicFact::AndFact(and_fact) => {
646 for inner_atomic in and_fact.facts.iter() {
647 mark_forall_param_coverage_in_atomic_fact(inner_atomic, coverage_by_forall_param);
648 }
649 }
650 ExistOrAndChainAtomicFact::ChainFact(chain_fact) => {
651 for chain_obj in chain_fact.objs.iter() {
652 mark_forall_param_coverage_in_obj(chain_obj, coverage_by_forall_param);
653 }
654 }
655 ExistOrAndChainAtomicFact::OrFact(or_fact) => {
656 for branch in or_fact.facts.iter() {
657 mark_forall_param_coverage_in_and_chain_atomic_fact(
658 branch,
659 coverage_by_forall_param,
660 );
661 }
662 }
663 ExistOrAndChainAtomicFact::ExistFact(exist_fact) => {
664 mark_forall_param_coverage_in_exist_fact(exist_fact, coverage_by_forall_param);
665 }
666 }
667}
668
669impl ForallFact {
670 pub fn error_messages_if_forall_param_missing_in_some_then_clause(
671 &self,
672 ) -> Vec<(usize, String)> {
673 let forall_param_names = self.params_def_with_type.collect_param_names();
674 if forall_param_names.is_empty() {
675 return Vec::new();
676 }
677 let mut error_messages = Vec::new();
678 let mut then_index: usize = 0;
679 while then_index < self.then_facts.len() {
680 let then_fact = &self.then_facts[then_index];
681 let mut coverage_by_forall_param: HashMap<IdentifierName, bool> = HashMap::new();
682 for param_name in forall_param_names.iter() {
683 coverage_by_forall_param.insert(param_name.clone(), false);
684 }
685 mark_forall_param_coverage_in_exist_or_and_chain_atomic_fact(
686 then_fact,
687 &mut coverage_by_forall_param,
688 );
689 let mut missing_param_names = Vec::new();
690 for param_name in forall_param_names.iter() {
691 let is_mentioned_in_then_clause = match coverage_by_forall_param.get(param_name) {
692 Some(flag) => *flag,
693 None => false,
694 };
695 if !is_mentioned_in_then_clause {
696 missing_param_names.push(param_name.clone());
697 }
698 }
699 if !missing_param_names.is_empty() {
700 let missing_list = missing_param_names.join(", ");
701 error_messages.push((
702 then_index,
703 format!(
704 "then-clause `{}` does not mention forall parameter(s) {{{}}}",
705 then_fact, missing_list,
706 ),
707 ));
708 }
709 then_index += 1;
710 }
711 error_messages
712 }
713}
714
715impl ForallFactWithIff {
716 pub fn error_messages_if_forall_param_missing_in_forall_then_clause(
718 &self,
719 ) -> Vec<(usize, String)> {
720 self.forall_fact
721 .error_messages_if_forall_param_missing_in_some_then_clause()
722 }
723}