1use crate::prelude::*;
2use std::rc::Rc;
3
4impl Runtime {
5 pub fn verify_equal_fact(
6 &mut self,
7 equal_fact: &EqualFact,
8 verify_state: &VerifyState,
9 ) -> Result<StmtResult, RuntimeError> {
10 self.verify_objs_are_equal(
11 &equal_fact.left,
12 &equal_fact.right,
13 equal_fact.line_file.clone(),
14 verify_state,
15 )
16 }
17
18 pub fn verify_objs_are_equal(
19 &mut self,
20 left: &Obj,
21 right: &Obj,
22 line_file: LineFile,
23 verify_state: &VerifyState,
24 ) -> Result<StmtResult, RuntimeError> {
25 let mut result =
26 self.verify_equality_by_builtin_rules(left, right, line_file.clone(), verify_state)?;
27 if result.is_true() {
28 return Ok(result);
29 }
30
31 result = self.verify_equality_with_known_equalities(
32 left,
33 right,
34 line_file.clone(),
35 verify_state,
36 )?;
37 if result.is_true() {
38 return Ok(result);
39 }
40
41 let verified_by_arg_to_arg = self
42 .verify_objs_are_equal_when_they_have_same_builtin_shape_and_equal_args_recursively(
43 left,
44 right,
45 verify_state,
46 line_file.clone(),
47 )?;
48 if verified_by_arg_to_arg {
49 return Ok(
50 (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
51 EqualFact::new(left.clone(), right.clone(), line_file.clone()).into(),
52 same_shape_and_equal_args_reason(left, right),
53 Vec::new(),
54 ))
55 .into(),
56 );
57 }
58
59 if verify_state.is_round_0() {
60 let verify_state_add_one_round = verify_state.new_state_with_round_increased();
61 result = self.verify_atomic_fact_with_known_forall(
62 &EqualFact::new(left.clone(), right.clone(), line_file.clone()).into(),
63 &verify_state_add_one_round,
64 )?;
65 if result.is_true() {
66 return Ok(result);
67 }
68 }
69
70 Ok((StmtUnknown::new()).into())
71 }
72
73 fn verify_equality_with_known_equalities(
74 &mut self,
75 left: &Obj,
76 right: &Obj,
77 line_file: LineFile,
78 verify_state: &VerifyState,
79 ) -> Result<StmtResult, RuntimeError> {
80 let left_string = left.to_string();
81 let right_string = right.to_string();
82
83 let known_pairs = self.collect_known_equality_pairs_from_envs(&left_string, &right_string);
84 for (known_left, known_right) in known_pairs {
85 if let Some(result) = self
86 .try_verify_equality_with_known_equalities_by_builtin_rules_only(
87 left,
88 right,
89 line_file.clone(),
90 verify_state,
91 known_left.as_ref(),
92 known_right.as_ref(),
93 )?
94 {
95 return Ok(result);
96 }
97 }
98
99 if let Some(done) = self.try_verify_objs_equal_via_user_defined_fn_definition_substitution(
100 left,
101 right,
102 line_file.clone(),
103 verify_state,
104 )? {
105 return Ok(done);
106 }
107
108 Ok((StmtUnknown::new()).into())
109 }
110
111 fn try_verify_objs_equal_via_user_defined_fn_definition_substitution(
113 &mut self,
114 left: &Obj,
115 right: &Obj,
116 line_file: LineFile,
117 verify_state: &VerifyState,
118 ) -> Result<Option<StmtResult>, RuntimeError> {
119 if let Some(done) = self.try_one_side_user_defined_fn_app_equals_other_side(
120 left,
121 right,
122 left,
123 right,
124 line_file.clone(),
125 verify_state,
126 )? {
127 return Ok(Some(done));
128 }
129 if let Some(done) = self.try_one_side_user_defined_fn_app_equals_other_side(
130 left,
131 right,
132 right,
133 left,
134 line_file.clone(),
135 verify_state,
136 )? {
137 return Ok(Some(done));
138 }
139 Ok(None)
140 }
141
142 fn try_one_side_user_defined_fn_app_equals_other_side(
143 &mut self,
144 statement_left: &Obj,
145 statement_right: &Obj,
146 application_side: &Obj,
147 other_side: &Obj,
148 line_file: LineFile,
149 verify_state: &VerifyState,
150 ) -> Result<Option<StmtResult>, RuntimeError> {
151 let Obj::FnObj(fn_obj) = application_side else {
152 return Ok(None);
153 };
154 if fn_obj.body.is_empty() {
155 return Ok(None);
156 }
157 let key = match fn_obj.head.as_ref() {
158 FnObjHead::Identifier(i) => i.to_string(),
159 FnObjHead::IdentifierWithMod(i) => i.to_string(),
160 _ => return Ok(None),
161 };
162 let Some((fn_set_body, equal_to_expr, _)) =
163 self.get_known_fn_body_and_equal_to_for_key(key.as_str())
164 else {
165 return Ok(None);
166 };
167 let param_defs = &fn_set_body.params_def_with_set;
168 let n_params = ParamGroupWithSet::number_of_params(param_defs);
169 if n_params == 0 {
170 return Ok(None);
171 }
172 let mut args: Vec<Obj> = Vec::new();
173 for g in fn_obj.body.iter() {
174 for b in g.iter() {
175 args.push((**b).clone());
176 }
177 }
178 if args.len() != n_params {
179 return Ok(None);
180 }
181 let param_to_arg_map =
182 ParamGroupWithSet::param_defs_and_args_to_param_to_arg_map(param_defs, &args);
183 let reduced = self.inst_obj(&equal_to_expr, ¶m_to_arg_map, ParamObjType::FnSet)?;
184 let inner =
185 self.verify_objs_are_equal(&reduced, other_side, line_file.clone(), verify_state)?;
186 if !inner.is_true() {
187 return Ok(None);
188 }
189 let fact: Fact = EqualFact::new(
190 statement_left.clone(),
191 statement_right.clone(),
192 line_file.clone(),
193 )
194 .into();
195 let msg = format!(
196 "according to user-defined function `{}` = `{}`",
197 application_side, reduced
198 );
199 let cited = fact.clone();
200 let verified_by = VerifiedByResult::cited_fact(fact.clone(), cited, Some(msg));
201 Ok(Some(
202 FactualStmtSuccess::new_with_verified_by_known_fact(fact, verified_by, Vec::new())
203 .into(),
204 ))
205 }
206
207 fn collect_known_equality_pairs_from_envs(
209 &self,
210 left_string: &str,
211 right_string: &str,
212 ) -> Vec<(Option<Rc<Vec<Obj>>>, Option<Rc<Vec<Obj>>>)> {
213 let mut pairs = Vec::with_capacity(self.environment_stack.len());
214 for env in self.iter_environments_from_top() {
215 let known_left = env
216 .known_equality
217 .get(left_string)
218 .map(|(_, equiv_class_rc)| Rc::clone(equiv_class_rc));
219 let known_right = env
220 .known_equality
221 .get(right_string)
222 .map(|(_, equiv_class_rc)| Rc::clone(equiv_class_rc));
223 pairs.push((known_left, known_right));
224 }
225 pairs
226 }
227
228 fn verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
229 &mut self,
230 left_left: &Obj,
231 left_right: &Obj,
232 right_left: &Obj,
233 right_right: &Obj,
234 verify_state: &VerifyState,
235 equality_line_file: LineFile,
236 ) -> Result<bool, RuntimeError> {
237 let result = self.verify_two_objs_equal_by_builtin_rules_and_known_equalities(
238 left_left,
239 right_left,
240 verify_state,
241 equality_line_file.clone(),
242 )?;
243 if result.is_unknown() {
244 return Ok(false);
245 }
246 let result = self.verify_two_objs_equal_by_builtin_rules_and_known_equalities(
247 left_right,
248 right_right,
249 verify_state,
250 equality_line_file.clone(),
251 )?;
252 if result.is_unknown() {
253 return Ok(false);
254 }
255 Ok(true)
256 }
257
258 fn verify_unary_objs_are_equal_when_their_only_args_are_equal(
259 &mut self,
260 left_value: &Obj,
261 right_value: &Obj,
262 verify_state: &VerifyState,
263 equality_line_file: LineFile,
264 ) -> Result<bool, RuntimeError> {
265 let result = self.verify_two_objs_equal_by_builtin_rules_and_known_equalities(
266 left_value,
267 right_value,
268 verify_state,
269 equality_line_file.clone(),
270 )?;
271 if result.is_true() {
272 return Ok(true);
273 }
274 Ok(false)
275 }
276
277 fn verify_obj_vec_are_equal_when_all_corresponding_args_are_equal(
278 &mut self,
279 left_values: &Vec<Box<Obj>>,
280 right_values: &Vec<Box<Obj>>,
281 verify_state: &VerifyState,
282 equality_line_file: LineFile,
283 ) -> Result<bool, RuntimeError> {
284 if left_values.len() != right_values.len() {
285 return Ok(false);
286 }
287
288 let mut current_index = 0;
289 while current_index < left_values.len() {
290 let result = self.verify_two_objs_equal_by_builtin_rules_and_known_equalities(
291 &left_values[current_index],
292 &right_values[current_index],
293 verify_state,
294 equality_line_file.clone(),
295 )?;
296 if result.is_unknown() {
297 return Ok(false);
298 }
299 current_index += 1;
300 }
301 Ok(true)
302 }
303
304 fn verify_matrix_list_objs_equal_when_all_cells_equal(
305 &mut self,
306 left: &MatrixListObj,
307 right: &MatrixListObj,
308 verify_state: &VerifyState,
309 equality_line_file: LineFile,
310 ) -> Result<bool, RuntimeError> {
311 if left.rows.len() != right.rows.len() {
312 return Ok(false);
313 }
314 for (lr, rr) in left.rows.iter().zip(right.rows.iter()) {
315 if !self.verify_obj_vec_are_equal_when_all_corresponding_args_are_equal(
316 lr,
317 rr,
318 verify_state,
319 equality_line_file.clone(),
320 )? {
321 return Ok(false);
322 }
323 }
324 Ok(true)
325 }
326
327 fn verify_fn_objs_equal_when_they_have_same_head_and_equal_args(
328 &mut self,
329 left_fn_obj: &FnObj,
330 right_fn_obj: &FnObj,
331 verify_state: &VerifyState,
332 equality_line_file: LineFile,
333 ) -> Result<bool, RuntimeError> {
334 if left_fn_obj.body.len() != right_fn_obj.body.len() {
335 return Ok(false);
336 }
337
338 if left_fn_obj.head.to_string() != right_fn_obj.head.to_string() {
339 return Ok(false);
340 }
341
342 for (left_group, right_group) in left_fn_obj.body.iter().zip(right_fn_obj.body.iter()) {
343 let result = self.verify_obj_vec_are_equal_when_all_corresponding_args_are_equal(
344 left_group,
345 right_group,
346 verify_state,
347 equality_line_file.clone(),
348 )?;
349 if !result {
350 return Ok(false);
351 }
352 }
353
354 Ok(true)
355 }
356
357 fn verify_fn_objs_are_equal_when_their_body_groups_match_from_right_to_left(
358 &mut self,
359 left_fn_obj: &FnObj,
360 right_fn_obj: &FnObj,
361 verify_state: &VerifyState,
362 equality_line_file: LineFile,
363 ) -> Result<bool, RuntimeError> {
364 let mut remaining_left_group_count = left_fn_obj.body.len();
365 let mut remaining_right_group_count = right_fn_obj.body.len();
366
367 while remaining_left_group_count > 0 && remaining_right_group_count > 0 {
368 let left_group = &left_fn_obj.body[remaining_left_group_count - 1];
369 let right_group = &right_fn_obj.body[remaining_right_group_count - 1];
370 if !self.verify_obj_vec_are_equal_when_all_corresponding_args_are_equal(
371 left_group,
372 right_group,
373 verify_state,
374 equality_line_file.clone(),
375 )? {
376 return Ok(false);
377 }
378 remaining_left_group_count -= 1;
379 remaining_right_group_count -= 1;
380 }
381
382 let remaining_left_obj = fn_obj_prefix_to_obj(left_fn_obj, remaining_left_group_count);
383 let remaining_right_obj = fn_obj_prefix_to_obj(right_fn_obj, remaining_right_group_count);
384 let remaining_equality_result = self
385 .verify_two_objs_equal_by_builtin_rules_and_known_equalities(
386 &remaining_left_obj,
387 &remaining_right_obj,
388 verify_state,
389 equality_line_file.clone(),
390 )?;
391 Ok(remaining_equality_result.is_true())
392 }
393
394 fn verify_objs_are_equal_when_they_have_same_builtin_shape_and_equal_args_recursively(
395 &mut self,
396 left_obj: &Obj,
397 right_obj: &Obj,
398 verify_state: &VerifyState,
399 equality_line_file: LineFile,
400 ) -> Result<bool, RuntimeError> {
401 match (left_obj, right_obj) {
402 (Obj::FnObj(left_fn_obj), Obj::FnObj(right_fn_obj)) => {
403 if left_fn_obj.body.len() == right_fn_obj.body.len()
404 && left_fn_obj.head.to_string() == right_fn_obj.head.to_string()
405 {
406 self.verify_fn_objs_equal_when_they_have_same_head_and_equal_args(
407 left_fn_obj,
408 right_fn_obj,
409 verify_state,
410 equality_line_file,
411 )
412 } else {
413 self.verify_fn_objs_are_equal_when_their_body_groups_match_from_right_to_left(
414 left_fn_obj,
415 right_fn_obj,
416 verify_state,
417 equality_line_file,
418 )
419 }
420 }
421 (Obj::Add(left_add), Obj::Add(right_add)) => self
422 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
423 &left_add.left,
424 &left_add.right,
425 &right_add.left,
426 &right_add.right,
427 verify_state,
428 equality_line_file,
429 ),
430 (Obj::Sub(left_sub), Obj::Sub(right_sub)) => self
431 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
432 &left_sub.left,
433 &left_sub.right,
434 &right_sub.left,
435 &right_sub.right,
436 verify_state,
437 equality_line_file,
438 ),
439 (Obj::Mul(left_mul), Obj::Mul(right_mul)) => self
440 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
441 &left_mul.left,
442 &left_mul.right,
443 &right_mul.left,
444 &right_mul.right,
445 verify_state,
446 equality_line_file,
447 ),
448 (Obj::Div(left_div), Obj::Div(right_div)) => self
449 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
450 &left_div.left,
451 &left_div.right,
452 &right_div.left,
453 &right_div.right,
454 verify_state,
455 equality_line_file,
456 ),
457 (Obj::Mod(left_mod), Obj::Mod(right_mod)) => self
458 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
459 &left_mod.left,
460 &left_mod.right,
461 &right_mod.left,
462 &right_mod.right,
463 verify_state,
464 equality_line_file,
465 ),
466 (Obj::Pow(left_pow), Obj::Pow(right_pow)) => self
467 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
468 &left_pow.base,
469 &left_pow.exponent,
470 &right_pow.base,
471 &right_pow.exponent,
472 verify_state,
473 equality_line_file,
474 ),
475 (Obj::Log(left_log), Obj::Log(right_log)) => self
476 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
477 &left_log.base,
478 &left_log.arg,
479 &right_log.base,
480 &right_log.arg,
481 verify_state,
482 equality_line_file,
483 ),
484 (Obj::MatrixAdd(left_m), Obj::MatrixAdd(right_m)) => self
485 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
486 &left_m.left,
487 &left_m.right,
488 &right_m.left,
489 &right_m.right,
490 verify_state,
491 equality_line_file,
492 ),
493 (Obj::MatrixSub(left_m), Obj::MatrixSub(right_m)) => self
494 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
495 &left_m.left,
496 &left_m.right,
497 &right_m.left,
498 &right_m.right,
499 verify_state,
500 equality_line_file,
501 ),
502 (Obj::MatrixMul(left_m), Obj::MatrixMul(right_m)) => self
503 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
504 &left_m.left,
505 &left_m.right,
506 &right_m.left,
507 &right_m.right,
508 verify_state,
509 equality_line_file,
510 ),
511 (Obj::MatrixScalarMul(left_m), Obj::MatrixScalarMul(right_m)) => self
512 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
513 &left_m.scalar,
514 &left_m.matrix,
515 &right_m.scalar,
516 &right_m.matrix,
517 verify_state,
518 equality_line_file,
519 ),
520 (Obj::MatrixPow(left_m), Obj::MatrixPow(right_m)) => self
521 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
522 &left_m.base,
523 &left_m.exponent,
524 &right_m.base,
525 &right_m.exponent,
526 verify_state,
527 equality_line_file,
528 ),
529 (Obj::Max(left_max), Obj::Max(right_max)) => self
530 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
531 &left_max.left,
532 &left_max.right,
533 &right_max.left,
534 &right_max.right,
535 verify_state,
536 equality_line_file,
537 ),
538 (Obj::Min(left_min), Obj::Min(right_min)) => self
539 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
540 &left_min.left,
541 &left_min.right,
542 &right_min.left,
543 &right_min.right,
544 verify_state,
545 equality_line_file,
546 ),
547 (Obj::Union(left_union), Obj::Union(right_union)) => self
548 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
549 &left_union.left,
550 &left_union.right,
551 &right_union.left,
552 &right_union.right,
553 verify_state,
554 equality_line_file,
555 ),
556 (Obj::Intersect(left_intersect), Obj::Intersect(right_intersect)) => self
557 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
558 &left_intersect.left,
559 &left_intersect.right,
560 &right_intersect.left,
561 &right_intersect.right,
562 verify_state,
563 equality_line_file,
564 ),
565 (Obj::SetMinus(left_set_minus), Obj::SetMinus(right_set_minus)) => self
566 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
567 &left_set_minus.left,
568 &left_set_minus.right,
569 &right_set_minus.left,
570 &right_set_minus.right,
571 verify_state,
572 equality_line_file,
573 ),
574 (Obj::SetDiff(left_set_diff), Obj::SetDiff(right_set_diff)) => self
575 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
576 &left_set_diff.left,
577 &left_set_diff.right,
578 &right_set_diff.left,
579 &right_set_diff.right,
580 verify_state,
581 equality_line_file,
582 ),
583 (Obj::Cup(left_cup), Obj::Cup(right_cup)) => self
584 .verify_unary_objs_are_equal_when_their_only_args_are_equal(
585 &left_cup.left,
586 &right_cup.left,
587 verify_state,
588 equality_line_file,
589 ),
590 (Obj::Cap(left_cap), Obj::Cap(right_cap)) => self
591 .verify_unary_objs_are_equal_when_their_only_args_are_equal(
592 &left_cap.left,
593 &right_cap.left,
594 verify_state,
595 equality_line_file,
596 ),
597 (Obj::PowerSet(left_power_set), Obj::PowerSet(right_power_set)) => self
598 .verify_unary_objs_are_equal_when_their_only_args_are_equal(
599 &left_power_set.set,
600 &right_power_set.set,
601 verify_state,
602 equality_line_file,
603 ),
604 (Obj::Choose(left_choose), Obj::Choose(right_choose)) => self
605 .verify_unary_objs_are_equal_when_their_only_args_are_equal(
606 &left_choose.set,
607 &right_choose.set,
608 verify_state,
609 equality_line_file,
610 ),
611 (Obj::CartDim(left_cart_dim), Obj::CartDim(right_cart_dim)) => self
612 .verify_unary_objs_are_equal_when_their_only_args_are_equal(
613 &left_cart_dim.set,
614 &right_cart_dim.set,
615 verify_state,
616 equality_line_file,
617 ),
618 (Obj::TupleDim(left_dim), Obj::TupleDim(right_dim)) => self
619 .verify_unary_objs_are_equal_when_their_only_args_are_equal(
620 &left_dim.arg,
621 &right_dim.arg,
622 verify_state,
623 equality_line_file,
624 ),
625 (Obj::Count(left_count), Obj::Count(right_count)) => self
626 .verify_unary_objs_are_equal_when_their_only_args_are_equal(
627 &left_count.set,
628 &right_count.set,
629 verify_state,
630 equality_line_file,
631 ),
632 (Obj::Range(left_range), Obj::Range(right_range)) => self
633 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
634 &left_range.start,
635 &left_range.end,
636 &right_range.start,
637 &right_range.end,
638 verify_state,
639 equality_line_file,
640 ),
641 (Obj::Sum(ls), Obj::Sum(rs)) => {
642 if !self.verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
643 &ls.start,
644 &ls.end,
645 &rs.start,
646 &rs.end,
647 verify_state,
648 equality_line_file.clone(),
649 )? {
650 return Ok(false);
651 }
652 self.verify_unary_objs_are_equal_when_their_only_args_are_equal(
653 ls.func.as_ref(),
654 rs.func.as_ref(),
655 verify_state,
656 equality_line_file,
657 )
658 }
659 (Obj::Product(ls), Obj::Product(rs)) => {
660 if !self.verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
661 &ls.start,
662 &ls.end,
663 &rs.start,
664 &rs.end,
665 verify_state,
666 equality_line_file.clone(),
667 )? {
668 return Ok(false);
669 }
670 self.verify_unary_objs_are_equal_when_their_only_args_are_equal(
671 ls.func.as_ref(),
672 rs.func.as_ref(),
673 verify_state,
674 equality_line_file,
675 )
676 }
677 (Obj::ClosedRange(left_closed_range), Obj::ClosedRange(right_closed_range)) => self
678 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
679 &left_closed_range.start,
680 &left_closed_range.end,
681 &right_closed_range.start,
682 &right_closed_range.end,
683 verify_state,
684 equality_line_file,
685 ),
686 (Obj::FiniteSeqSet(left_fs), Obj::FiniteSeqSet(right_fs)) => self
687 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
688 &left_fs.set,
689 &left_fs.n,
690 &right_fs.set,
691 &right_fs.n,
692 verify_state,
693 equality_line_file,
694 ),
695 (Obj::SeqSet(left_s), Obj::SeqSet(right_s)) => self
696 .verify_unary_objs_are_equal_when_their_only_args_are_equal(
697 left_s.set.as_ref(),
698 right_s.set.as_ref(),
699 verify_state,
700 equality_line_file,
701 ),
702 (Obj::FiniteSeqListObj(left_v), Obj::FiniteSeqListObj(right_v)) => self
703 .verify_obj_vec_are_equal_when_all_corresponding_args_are_equal(
704 &left_v.objs,
705 &right_v.objs,
706 verify_state,
707 equality_line_file,
708 ),
709 (Obj::MatrixSet(left_m), Obj::MatrixSet(right_m)) => {
710 if !self.verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
711 &left_m.set,
712 &left_m.row_len,
713 &right_m.set,
714 &right_m.row_len,
715 verify_state,
716 equality_line_file.clone(),
717 )? {
718 return Ok(false);
719 }
720 let result = self.verify_two_objs_equal_by_builtin_rules_and_known_equalities(
721 &left_m.col_len,
722 &right_m.col_len,
723 verify_state,
724 equality_line_file,
725 )?;
726 if result.is_unknown() {
727 return Ok(false);
728 }
729 Ok(true)
730 }
731 (Obj::MatrixListObj(left_m), Obj::MatrixListObj(right_m)) => self
732 .verify_matrix_list_objs_equal_when_all_cells_equal(
733 left_m,
734 right_m,
735 verify_state,
736 equality_line_file,
737 ),
738 (Obj::Proj(left_proj), Obj::Proj(right_proj)) => self
739 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
740 &left_proj.set,
741 &left_proj.dim,
742 &right_proj.set,
743 &right_proj.dim,
744 verify_state,
745 equality_line_file,
746 ),
747 (Obj::ObjAtIndex(left_obj_at_index), Obj::ObjAtIndex(right_obj_at_index)) => self
748 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
749 &left_obj_at_index.obj,
750 &left_obj_at_index.index,
751 &right_obj_at_index.obj,
752 &right_obj_at_index.index,
753 verify_state,
754 equality_line_file,
755 ),
756 (Obj::Tuple(left_tuple), Obj::Tuple(right_tuple)) => self
757 .verify_obj_vec_are_equal_when_all_corresponding_args_are_equal(
758 &left_tuple.args,
759 &right_tuple.args,
760 verify_state,
761 equality_line_file,
762 ),
763 (Obj::ListSet(left_list_set), Obj::ListSet(right_list_set)) => self
764 .verify_obj_vec_are_equal_when_all_corresponding_args_are_equal(
765 &left_list_set.list,
766 &right_list_set.list,
767 verify_state,
768 equality_line_file,
769 ),
770 (Obj::Cart(left_cart), Obj::Cart(right_cart)) => self
771 .verify_obj_vec_are_equal_when_all_corresponding_args_are_equal(
772 &left_cart.args,
773 &right_cart.args,
774 verify_state,
775 equality_line_file,
776 ),
777 _ => Ok(false),
778 }
779 }
780
781 fn verify_two_objs_equal_by_builtin_rules_and_known_equalities(
782 &mut self,
783 left_obj: &Obj,
784 right_obj: &Obj,
785 verify_state: &VerifyState,
786 equality_line_file: LineFile,
787 ) -> Result<StmtResult, RuntimeError> {
788 let mut result = self.verify_equality_by_builtin_rules(
789 left_obj,
790 right_obj,
791 equality_line_file.clone(),
792 verify_state,
793 )?;
794 if result.is_true() {
795 return Ok(
796 (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
797 EqualFact::new(
798 left_obj.clone(),
799 right_obj.clone(),
800 equality_line_file.clone(),
801 )
802 .into(),
803 "builtin rules".to_string(),
804 Vec::new(),
805 ))
806 .into(),
807 );
808 }
809
810 result = self.verify_equality_with_known_equalities(
811 left_obj,
812 right_obj,
813 equality_line_file.clone(),
814 verify_state,
815 )?;
816 if result.is_true() {
817 return Ok(result);
818 }
819
820 let verified_by_arg_to_arg = self
821 .verify_objs_are_equal_when_they_have_same_builtin_shape_and_equal_args_recursively(
822 left_obj,
823 right_obj,
824 verify_state,
825 equality_line_file.clone(),
826 )?;
827 if verified_by_arg_to_arg {
828 return Ok(
829 (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
830 EqualFact::new(left_obj.clone(), right_obj.clone(), equality_line_file).into(),
831 same_shape_and_equal_args_reason(left_obj, right_obj),
832 Vec::new(),
833 ))
834 .into(),
835 );
836 }
837
838 Ok((StmtUnknown::new()).into())
839 }
840}
841
842fn fn_obj_prefix_to_obj(fn_obj: &FnObj, number_of_body_groups_to_keep: usize) -> Obj {
843 if number_of_body_groups_to_keep == 0 {
844 return fn_obj.head.as_ref().clone().into();
845 }
846
847 let mut kept_body_groups: Vec<Vec<Box<Obj>>> = Vec::new();
848 let mut current_group_index = 0;
849 while current_group_index < number_of_body_groups_to_keep {
850 kept_body_groups.push(fn_obj.body[current_group_index].clone());
851 current_group_index += 1;
852 }
853
854 FnObj::new(fn_obj.head.as_ref().clone(), kept_body_groups).into()
855}
856
857fn same_shape_and_equal_args_reason(left_obj: &Obj, right_obj: &Obj) -> String {
858 match (left_obj, right_obj) {
859 (Obj::FnObj(_), Obj::FnObj(_)) => {
860 "the function parts are equal, and the function arguments are equal one by one"
861 .to_string()
862 }
863 _ => "the corresponding builtin-object arguments are equal one by one".to_string(),
864 }
865}