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