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