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