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