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