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::Sum(p) => {
52 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
53 }
54 FnObjHead::Product(p) => {
55 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
56 }
57 FnObjHead::DefHeader(_)
58 | FnObjHead::Exist(_)
59 | FnObjHead::SetBuilder(_)
60 | FnObjHead::FnSet(_)
61 | FnObjHead::Induc(_)
62 | FnObjHead::DefAlgo(_) => {}
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.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.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.ret_set.as_ref(), coverage_by_forall_param);
199 }
200 Obj::Cart(cart) => {
201 for boxed_arg in cart.args.iter() {
202 mark_forall_param_coverage_in_obj(boxed_arg.as_ref(), coverage_by_forall_param);
203 }
204 }
205 Obj::CartDim(cart_dim) => {
206 mark_forall_param_coverage_in_obj(cart_dim.set.as_ref(), coverage_by_forall_param);
207 }
208 Obj::Proj(proj) => {
209 mark_forall_param_coverage_in_obj(proj.set.as_ref(), coverage_by_forall_param);
210 mark_forall_param_coverage_in_obj(proj.dim.as_ref(), coverage_by_forall_param);
211 }
212 Obj::TupleDim(tuple_dim) => {
213 mark_forall_param_coverage_in_obj(tuple_dim.arg.as_ref(), coverage_by_forall_param);
214 }
215 Obj::Tuple(tuple_obj) => {
216 for boxed_arg in tuple_obj.args.iter() {
217 mark_forall_param_coverage_in_obj(boxed_arg.as_ref(), coverage_by_forall_param);
218 }
219 }
220 Obj::Count(count) => {
221 mark_forall_param_coverage_in_obj(count.set.as_ref(), coverage_by_forall_param);
222 }
223 Obj::Range(range) => {
224 mark_forall_param_coverage_in_obj(range.start.as_ref(), coverage_by_forall_param);
225 mark_forall_param_coverage_in_obj(range.end.as_ref(), coverage_by_forall_param);
226 }
227 Obj::ClosedRange(closed_range) => {
228 mark_forall_param_coverage_in_obj(
229 closed_range.start.as_ref(),
230 coverage_by_forall_param,
231 );
232 mark_forall_param_coverage_in_obj(closed_range.end.as_ref(), coverage_by_forall_param);
233 }
234 Obj::FiniteSeqSet(fs) => {
235 mark_forall_param_coverage_in_obj(fs.set.as_ref(), coverage_by_forall_param);
236 mark_forall_param_coverage_in_obj(fs.n.as_ref(), coverage_by_forall_param);
237 }
238 Obj::SeqSet(ss) => {
239 mark_forall_param_coverage_in_obj(ss.set.as_ref(), coverage_by_forall_param);
240 }
241 Obj::FiniteSeqListObj(v) => {
242 for o in v.objs.iter() {
243 mark_forall_param_coverage_in_obj(o.as_ref(), coverage_by_forall_param);
244 }
245 }
246 Obj::MatrixSet(ms) => {
247 mark_forall_param_coverage_in_obj(ms.set.as_ref(), coverage_by_forall_param);
248 mark_forall_param_coverage_in_obj(ms.row_len.as_ref(), coverage_by_forall_param);
249 mark_forall_param_coverage_in_obj(ms.col_len.as_ref(), coverage_by_forall_param);
250 }
251 Obj::MatrixListObj(v) => {
252 for row in v.rows.iter() {
253 for o in row.iter() {
254 mark_forall_param_coverage_in_obj(o.as_ref(), coverage_by_forall_param);
255 }
256 }
257 }
258 Obj::Choose(choose) => {
259 mark_forall_param_coverage_in_obj(choose.set.as_ref(), coverage_by_forall_param);
260 }
261 Obj::ObjAtIndex(obj_at_index) => {
262 mark_forall_param_coverage_in_obj(obj_at_index.obj.as_ref(), coverage_by_forall_param);
263 mark_forall_param_coverage_in_obj(
264 obj_at_index.index.as_ref(),
265 coverage_by_forall_param,
266 );
267 }
268 Obj::FamilyObj(family) => {
269 for o in family.params.iter() {
270 mark_forall_param_coverage_in_obj(o, coverage_by_forall_param);
271 }
272 }
273 Obj::Sum(sum) => {
274 mark_forall_param_coverage_in_obj(sum.start.as_ref(), coverage_by_forall_param);
275 mark_forall_param_coverage_in_obj(sum.end.as_ref(), coverage_by_forall_param);
276 mark_forall_param_coverage_in_obj(sum.body.as_ref(), coverage_by_forall_param);
277 }
278 Obj::Product(product) => {
279 mark_forall_param_coverage_in_obj(product.start.as_ref(), coverage_by_forall_param);
280 mark_forall_param_coverage_in_obj(product.end.as_ref(), coverage_by_forall_param);
281 mark_forall_param_coverage_in_obj(product.body.as_ref(), coverage_by_forall_param);
282 }
283 Obj::Atom(AtomObj::Forall(p)) => {
284 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
285 }
286 Obj::Atom(AtomObj::Def(p)) => {
287 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
288 }
289 Obj::Atom(AtomObj::Exist(p)) => {
290 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
291 }
292 Obj::Atom(AtomObj::SetBuilder(p)) => {
293 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
294 }
295 Obj::Atom(AtomObj::FnSet(p)) => {
296 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
297 }
298 Obj::Atom(AtomObj::Induc(p)) => {
299 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
300 }
301 Obj::Atom(AtomObj::DefAlgo(p)) => {
302 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
303 }
304 Obj::Atom(AtomObj::Sum(p)) => {
305 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
306 }
307 Obj::Atom(AtomObj::Product(p)) => {
308 mark_forall_param_name_if_tracked(coverage_by_forall_param, &p.name);
309 }
310 }
311}
312
313fn mark_forall_param_coverage_in_atomic_fact(
314 atomic_fact: &AtomicFact,
315 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
316) {
317 match atomic_fact {
318 AtomicFact::NormalAtomicFact(fact) => {
319 for body_obj in fact.body.iter() {
320 mark_forall_param_coverage_in_obj(body_obj, coverage_by_forall_param);
321 }
322 }
323 AtomicFact::NotNormalAtomicFact(fact) => {
324 for body_obj in fact.body.iter() {
325 mark_forall_param_coverage_in_obj(body_obj, coverage_by_forall_param);
326 }
327 }
328 AtomicFact::EqualFact(fact) => {
329 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
330 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
331 }
332 AtomicFact::LessFact(fact) => {
333 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
334 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
335 }
336 AtomicFact::GreaterFact(fact) => {
337 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
338 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
339 }
340 AtomicFact::LessEqualFact(fact) => {
341 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
342 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
343 }
344 AtomicFact::GreaterEqualFact(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::NotEqualFact(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::NotLessFact(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::NotGreaterFact(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::NotLessEqualFact(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::NotGreaterEqualFact(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::IsSetFact(fact) => {
369 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
370 }
371 AtomicFact::NotIsSetFact(fact) => {
372 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
373 }
374 AtomicFact::IsNonemptySetFact(fact) => {
375 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
376 }
377 AtomicFact::NotIsNonemptySetFact(fact) => {
378 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
379 }
380 AtomicFact::IsFiniteSetFact(fact) => {
381 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
382 }
383 AtomicFact::NotIsFiniteSetFact(fact) => {
384 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
385 }
386 AtomicFact::InFact(fact) => {
387 mark_forall_param_coverage_in_obj(&fact.element, coverage_by_forall_param);
388 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
389 }
390 AtomicFact::NotInFact(fact) => {
391 mark_forall_param_coverage_in_obj(&fact.element, coverage_by_forall_param);
392 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
393 }
394 AtomicFact::IsCartFact(fact) => {
395 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
396 }
397 AtomicFact::NotIsCartFact(fact) => {
398 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
399 }
400 AtomicFact::IsTupleFact(fact) => {
401 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
402 }
403 AtomicFact::NotIsTupleFact(fact) => {
404 mark_forall_param_coverage_in_obj(&fact.set, coverage_by_forall_param);
405 }
406 AtomicFact::SubsetFact(fact) => {
407 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
408 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
409 }
410 AtomicFact::SupersetFact(fact) => {
411 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
412 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
413 }
414 AtomicFact::NotSubsetFact(fact) => {
415 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
416 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
417 }
418 AtomicFact::NotSupersetFact(fact) => {
419 mark_forall_param_coverage_in_obj(&fact.left, coverage_by_forall_param);
420 mark_forall_param_coverage_in_obj(&fact.right, coverage_by_forall_param);
421 }
422 AtomicFact::RestrictFact(fact) => {
423 mark_forall_param_coverage_in_obj(&fact.obj, coverage_by_forall_param);
424 mark_forall_param_coverage_in_obj(
425 &fact.obj_can_restrict_to_fn_set,
426 coverage_by_forall_param,
427 );
428 }
429 AtomicFact::NotRestrictFact(fact) => {
430 mark_forall_param_coverage_in_obj(&fact.obj, coverage_by_forall_param);
431 mark_forall_param_coverage_in_obj(
432 &fact.obj_cannot_restrict_to_fn_set,
433 coverage_by_forall_param,
434 );
435 }
436 }
437}
438
439fn mark_forall_param_coverage_in_and_chain_atomic_fact(
440 parent_fact: &AndChainAtomicFact,
441 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
442) {
443 match parent_fact {
444 AndChainAtomicFact::AtomicFact(atomic_fact) => {
445 mark_forall_param_coverage_in_atomic_fact(atomic_fact, coverage_by_forall_param);
446 }
447 AndChainAtomicFact::AndFact(and_fact) => {
448 for inner_atomic in and_fact.facts.iter() {
449 mark_forall_param_coverage_in_atomic_fact(inner_atomic, coverage_by_forall_param);
450 }
451 }
452 AndChainAtomicFact::ChainFact(chain_fact) => {
453 for chain_obj in chain_fact.objs.iter() {
454 mark_forall_param_coverage_in_obj(chain_obj, coverage_by_forall_param);
455 }
456 }
457 }
458}
459
460fn mark_forall_param_coverage_in_or_and_chain_atomic_fact(
461 parent_fact: &OrAndChainAtomicFact,
462 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
463) {
464 match parent_fact {
465 OrAndChainAtomicFact::AtomicFact(atomic_fact) => {
466 mark_forall_param_coverage_in_atomic_fact(atomic_fact, coverage_by_forall_param);
467 }
468 OrAndChainAtomicFact::AndFact(and_fact) => {
469 for inner_atomic in and_fact.facts.iter() {
470 mark_forall_param_coverage_in_atomic_fact(inner_atomic, coverage_by_forall_param);
471 }
472 }
473 OrAndChainAtomicFact::ChainFact(chain_fact) => {
474 for chain_obj in chain_fact.objs.iter() {
475 mark_forall_param_coverage_in_obj(chain_obj, coverage_by_forall_param);
476 }
477 }
478 OrAndChainAtomicFact::OrFact(or_fact) => {
479 for branch in or_fact.facts.iter() {
480 mark_forall_param_coverage_in_and_chain_atomic_fact(
481 branch,
482 coverage_by_forall_param,
483 );
484 }
485 }
486 }
487}
488
489fn mark_forall_param_coverage_in_exist_fact(
490 exist_fact: &ExistFactEnum,
491 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
492) {
493 for param_def_with_type in exist_fact.params_def_with_type().groups.iter() {
494 mark_forall_param_coverage_in_param_type(
495 ¶m_def_with_type.param_type,
496 coverage_by_forall_param,
497 );
498 }
499 for inner_fact in exist_fact.facts().iter() {
500 mark_forall_param_coverage_in_or_and_chain_atomic_fact(
501 inner_fact,
502 coverage_by_forall_param,
503 );
504 }
505}
506
507fn mark_forall_param_coverage_in_exist_or_and_chain_atomic_fact(
508 parent_fact: &ExistOrAndChainAtomicFact,
509 coverage_by_forall_param: &mut HashMap<IdentifierName, bool>,
510) {
511 match parent_fact {
512 ExistOrAndChainAtomicFact::AtomicFact(atomic_fact) => {
513 mark_forall_param_coverage_in_atomic_fact(atomic_fact, coverage_by_forall_param);
514 }
515 ExistOrAndChainAtomicFact::AndFact(and_fact) => {
516 for inner_atomic in and_fact.facts.iter() {
517 mark_forall_param_coverage_in_atomic_fact(inner_atomic, coverage_by_forall_param);
518 }
519 }
520 ExistOrAndChainAtomicFact::ChainFact(chain_fact) => {
521 for chain_obj in chain_fact.objs.iter() {
522 mark_forall_param_coverage_in_obj(chain_obj, coverage_by_forall_param);
523 }
524 }
525 ExistOrAndChainAtomicFact::OrFact(or_fact) => {
526 for branch in or_fact.facts.iter() {
527 mark_forall_param_coverage_in_and_chain_atomic_fact(
528 branch,
529 coverage_by_forall_param,
530 );
531 }
532 }
533 ExistOrAndChainAtomicFact::ExistFact(exist_fact) => {
534 mark_forall_param_coverage_in_exist_fact(exist_fact, coverage_by_forall_param);
535 }
536 }
537}
538
539impl ForallFact {
540 pub fn error_messages_if_forall_param_missing_in_some_then_clause(
541 &self,
542 ) -> Vec<(usize, String)> {
543 let forall_param_names = self.params_def_with_type.collect_param_names();
544 if forall_param_names.is_empty() {
545 return Vec::new();
546 }
547 let mut error_messages = Vec::new();
548 let mut then_index: usize = 0;
549 while then_index < self.then_facts.len() {
550 let then_fact = &self.then_facts[then_index];
551 let mut coverage_by_forall_param: HashMap<IdentifierName, bool> = HashMap::new();
552 for param_name in forall_param_names.iter() {
553 coverage_by_forall_param.insert(param_name.clone(), false);
554 }
555 mark_forall_param_coverage_in_exist_or_and_chain_atomic_fact(
556 then_fact,
557 &mut coverage_by_forall_param,
558 );
559 let mut missing_param_names = Vec::new();
560 for param_name in forall_param_names.iter() {
561 let is_mentioned_in_then_clause = match coverage_by_forall_param.get(param_name) {
562 Some(flag) => *flag,
563 None => false,
564 };
565 if !is_mentioned_in_then_clause {
566 missing_param_names.push(param_name.clone());
567 }
568 }
569 if !missing_param_names.is_empty() {
570 let missing_list = missing_param_names.join(", ");
571 error_messages.push((
572 then_index,
573 format!(
574 "then-clause `{}` does not mention forall parameter(s) {{{}}}",
575 then_fact, missing_list,
576 ),
577 ));
578 }
579 then_index += 1;
580 }
581 error_messages
582 }
583}
584
585impl ForallFactWithIff {
586 pub fn error_messages_if_forall_param_missing_in_forall_then_clause(
588 &self,
589 ) -> Vec<(usize, String)> {
590 self.forall_fact
591 .error_messages_if_forall_param_missing_in_some_then_clause()
592 }
593}