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 Ok(Some(
201 FactualStmtSuccess::new_with_verified_by_known_fact(
202 fact,
203 VerifiedByResult::Fact(cited, msg),
204 Vec::new(),
205 )
206 .into(),
207 ))
208 }
209
210 fn collect_known_equality_pairs_from_envs(
212 &self,
213 left_string: &str,
214 right_string: &str,
215 ) -> Vec<(Option<Rc<Vec<Obj>>>, Option<Rc<Vec<Obj>>>)> {
216 let mut pairs = Vec::with_capacity(self.environment_stack.len());
217 for env in self.iter_environments_from_top() {
218 let known_left = env
219 .known_equality
220 .get(left_string)
221 .map(|(_, equiv_class_rc)| Rc::clone(equiv_class_rc));
222 let known_right = env
223 .known_equality
224 .get(right_string)
225 .map(|(_, equiv_class_rc)| Rc::clone(equiv_class_rc));
226 pairs.push((known_left, known_right));
227 }
228 pairs
229 }
230
231 fn verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
232 &mut self,
233 left_left: &Obj,
234 left_right: &Obj,
235 right_left: &Obj,
236 right_right: &Obj,
237 verify_state: &VerifyState,
238 equality_line_file: LineFile,
239 ) -> Result<bool, RuntimeError> {
240 let result = self.verify_two_objs_equal_by_builtin_rules_and_known_equalities(
241 left_left,
242 right_left,
243 verify_state,
244 equality_line_file.clone(),
245 )?;
246 if result.is_unknown() {
247 return Ok(false);
248 }
249 let result = self.verify_two_objs_equal_by_builtin_rules_and_known_equalities(
250 left_right,
251 right_right,
252 verify_state,
253 equality_line_file.clone(),
254 )?;
255 if result.is_unknown() {
256 return Ok(false);
257 }
258 Ok(true)
259 }
260
261 fn verify_unary_objs_are_equal_when_their_only_args_are_equal(
262 &mut self,
263 left_value: &Obj,
264 right_value: &Obj,
265 verify_state: &VerifyState,
266 equality_line_file: LineFile,
267 ) -> Result<bool, RuntimeError> {
268 let result = self.verify_two_objs_equal_by_builtin_rules_and_known_equalities(
269 left_value,
270 right_value,
271 verify_state,
272 equality_line_file.clone(),
273 )?;
274 if result.is_true() {
275 return Ok(true);
276 }
277 Ok(false)
278 }
279
280 fn verify_obj_vec_are_equal_when_all_corresponding_args_are_equal(
281 &mut self,
282 left_values: &Vec<Box<Obj>>,
283 right_values: &Vec<Box<Obj>>,
284 verify_state: &VerifyState,
285 equality_line_file: LineFile,
286 ) -> Result<bool, RuntimeError> {
287 if left_values.len() != right_values.len() {
288 return Ok(false);
289 }
290
291 let mut current_index = 0;
292 while current_index < left_values.len() {
293 let result = self.verify_two_objs_equal_by_builtin_rules_and_known_equalities(
294 &left_values[current_index],
295 &right_values[current_index],
296 verify_state,
297 equality_line_file.clone(),
298 )?;
299 if result.is_unknown() {
300 return Ok(false);
301 }
302 current_index += 1;
303 }
304 Ok(true)
305 }
306
307 fn verify_matrix_list_objs_equal_when_all_cells_equal(
308 &mut self,
309 left: &MatrixListObj,
310 right: &MatrixListObj,
311 verify_state: &VerifyState,
312 equality_line_file: LineFile,
313 ) -> Result<bool, RuntimeError> {
314 if left.rows.len() != right.rows.len() {
315 return Ok(false);
316 }
317 for (lr, rr) in left.rows.iter().zip(right.rows.iter()) {
318 if !self.verify_obj_vec_are_equal_when_all_corresponding_args_are_equal(
319 lr,
320 rr,
321 verify_state,
322 equality_line_file.clone(),
323 )? {
324 return Ok(false);
325 }
326 }
327 Ok(true)
328 }
329
330 fn verify_fn_objs_equal_when_they_have_same_head_and_equal_args(
331 &mut self,
332 left_fn_obj: &FnObj,
333 right_fn_obj: &FnObj,
334 verify_state: &VerifyState,
335 equality_line_file: LineFile,
336 ) -> Result<bool, RuntimeError> {
337 if left_fn_obj.body.len() != right_fn_obj.body.len() {
338 return Ok(false);
339 }
340
341 if left_fn_obj.head.to_string() != right_fn_obj.head.to_string() {
342 return Ok(false);
343 }
344
345 for (left_group, right_group) in left_fn_obj.body.iter().zip(right_fn_obj.body.iter()) {
346 let result = self.verify_obj_vec_are_equal_when_all_corresponding_args_are_equal(
347 left_group,
348 right_group,
349 verify_state,
350 equality_line_file.clone(),
351 )?;
352 if !result {
353 return Ok(false);
354 }
355 }
356
357 Ok(true)
358 }
359
360 fn verify_fn_objs_are_equal_when_their_body_groups_match_from_right_to_left(
361 &mut self,
362 left_fn_obj: &FnObj,
363 right_fn_obj: &FnObj,
364 verify_state: &VerifyState,
365 equality_line_file: LineFile,
366 ) -> Result<bool, RuntimeError> {
367 let mut remaining_left_group_count = left_fn_obj.body.len();
368 let mut remaining_right_group_count = right_fn_obj.body.len();
369
370 while remaining_left_group_count > 0 && remaining_right_group_count > 0 {
371 let left_group = &left_fn_obj.body[remaining_left_group_count - 1];
372 let right_group = &right_fn_obj.body[remaining_right_group_count - 1];
373 if !self.verify_obj_vec_are_equal_when_all_corresponding_args_are_equal(
374 left_group,
375 right_group,
376 verify_state,
377 equality_line_file.clone(),
378 )? {
379 return Ok(false);
380 }
381 remaining_left_group_count -= 1;
382 remaining_right_group_count -= 1;
383 }
384
385 let remaining_left_obj = fn_obj_prefix_to_obj(left_fn_obj, remaining_left_group_count);
386 let remaining_right_obj = fn_obj_prefix_to_obj(right_fn_obj, remaining_right_group_count);
387 let remaining_equality_result = self
388 .verify_two_objs_equal_by_builtin_rules_and_known_equalities(
389 &remaining_left_obj,
390 &remaining_right_obj,
391 verify_state,
392 equality_line_file.clone(),
393 )?;
394 Ok(remaining_equality_result.is_true())
395 }
396
397 fn verify_objs_are_equal_when_they_have_same_builtin_shape_and_equal_args_recursively(
398 &mut self,
399 left_obj: &Obj,
400 right_obj: &Obj,
401 verify_state: &VerifyState,
402 equality_line_file: LineFile,
403 ) -> Result<bool, RuntimeError> {
404 match (left_obj, right_obj) {
405 (Obj::FnObj(left_fn_obj), Obj::FnObj(right_fn_obj)) => {
406 if left_fn_obj.body.len() == right_fn_obj.body.len()
407 && left_fn_obj.head.to_string() == right_fn_obj.head.to_string()
408 {
409 self.verify_fn_objs_equal_when_they_have_same_head_and_equal_args(
410 left_fn_obj,
411 right_fn_obj,
412 verify_state,
413 equality_line_file,
414 )
415 } else {
416 self.verify_fn_objs_are_equal_when_their_body_groups_match_from_right_to_left(
417 left_fn_obj,
418 right_fn_obj,
419 verify_state,
420 equality_line_file,
421 )
422 }
423 }
424 (Obj::Add(left_add), Obj::Add(right_add)) => self
425 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
426 &left_add.left,
427 &left_add.right,
428 &right_add.left,
429 &right_add.right,
430 verify_state,
431 equality_line_file,
432 ),
433 (Obj::Sub(left_sub), Obj::Sub(right_sub)) => self
434 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
435 &left_sub.left,
436 &left_sub.right,
437 &right_sub.left,
438 &right_sub.right,
439 verify_state,
440 equality_line_file,
441 ),
442 (Obj::Mul(left_mul), Obj::Mul(right_mul)) => self
443 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
444 &left_mul.left,
445 &left_mul.right,
446 &right_mul.left,
447 &right_mul.right,
448 verify_state,
449 equality_line_file,
450 ),
451 (Obj::Div(left_div), Obj::Div(right_div)) => self
452 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
453 &left_div.left,
454 &left_div.right,
455 &right_div.left,
456 &right_div.right,
457 verify_state,
458 equality_line_file,
459 ),
460 (Obj::Mod(left_mod), Obj::Mod(right_mod)) => self
461 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
462 &left_mod.left,
463 &left_mod.right,
464 &right_mod.left,
465 &right_mod.right,
466 verify_state,
467 equality_line_file,
468 ),
469 (Obj::Pow(left_pow), Obj::Pow(right_pow)) => self
470 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
471 &left_pow.base,
472 &left_pow.exponent,
473 &right_pow.base,
474 &right_pow.exponent,
475 verify_state,
476 equality_line_file,
477 ),
478 (Obj::Log(left_log), Obj::Log(right_log)) => self
479 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
480 &left_log.base,
481 &left_log.arg,
482 &right_log.base,
483 &right_log.arg,
484 verify_state,
485 equality_line_file,
486 ),
487 (Obj::MatrixAdd(left_m), Obj::MatrixAdd(right_m)) => self
488 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
489 &left_m.left,
490 &left_m.right,
491 &right_m.left,
492 &right_m.right,
493 verify_state,
494 equality_line_file,
495 ),
496 (Obj::MatrixSub(left_m), Obj::MatrixSub(right_m)) => self
497 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
498 &left_m.left,
499 &left_m.right,
500 &right_m.left,
501 &right_m.right,
502 verify_state,
503 equality_line_file,
504 ),
505 (Obj::MatrixMul(left_m), Obj::MatrixMul(right_m)) => self
506 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
507 &left_m.left,
508 &left_m.right,
509 &right_m.left,
510 &right_m.right,
511 verify_state,
512 equality_line_file,
513 ),
514 (Obj::MatrixScalarMul(left_m), Obj::MatrixScalarMul(right_m)) => self
515 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
516 &left_m.scalar,
517 &left_m.matrix,
518 &right_m.scalar,
519 &right_m.matrix,
520 verify_state,
521 equality_line_file,
522 ),
523 (Obj::MatrixPow(left_m), Obj::MatrixPow(right_m)) => self
524 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
525 &left_m.base,
526 &left_m.exponent,
527 &right_m.base,
528 &right_m.exponent,
529 verify_state,
530 equality_line_file,
531 ),
532 (Obj::Max(left_max), Obj::Max(right_max)) => self
533 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
534 &left_max.left,
535 &left_max.right,
536 &right_max.left,
537 &right_max.right,
538 verify_state,
539 equality_line_file,
540 ),
541 (Obj::Min(left_min), Obj::Min(right_min)) => self
542 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
543 &left_min.left,
544 &left_min.right,
545 &right_min.left,
546 &right_min.right,
547 verify_state,
548 equality_line_file,
549 ),
550 (Obj::Union(left_union), Obj::Union(right_union)) => self
551 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
552 &left_union.left,
553 &left_union.right,
554 &right_union.left,
555 &right_union.right,
556 verify_state,
557 equality_line_file,
558 ),
559 (Obj::Intersect(left_intersect), Obj::Intersect(right_intersect)) => self
560 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
561 &left_intersect.left,
562 &left_intersect.right,
563 &right_intersect.left,
564 &right_intersect.right,
565 verify_state,
566 equality_line_file,
567 ),
568 (Obj::SetMinus(left_set_minus), Obj::SetMinus(right_set_minus)) => self
569 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
570 &left_set_minus.left,
571 &left_set_minus.right,
572 &right_set_minus.left,
573 &right_set_minus.right,
574 verify_state,
575 equality_line_file,
576 ),
577 (Obj::SetDiff(left_set_diff), Obj::SetDiff(right_set_diff)) => self
578 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
579 &left_set_diff.left,
580 &left_set_diff.right,
581 &right_set_diff.left,
582 &right_set_diff.right,
583 verify_state,
584 equality_line_file,
585 ),
586 (Obj::Cup(left_cup), Obj::Cup(right_cup)) => self
587 .verify_unary_objs_are_equal_when_their_only_args_are_equal(
588 &left_cup.left,
589 &right_cup.left,
590 verify_state,
591 equality_line_file,
592 ),
593 (Obj::Cap(left_cap), Obj::Cap(right_cap)) => self
594 .verify_unary_objs_are_equal_when_their_only_args_are_equal(
595 &left_cap.left,
596 &right_cap.left,
597 verify_state,
598 equality_line_file,
599 ),
600 (Obj::PowerSet(left_power_set), Obj::PowerSet(right_power_set)) => self
601 .verify_unary_objs_are_equal_when_their_only_args_are_equal(
602 &left_power_set.set,
603 &right_power_set.set,
604 verify_state,
605 equality_line_file,
606 ),
607 (Obj::Choose(left_choose), Obj::Choose(right_choose)) => self
608 .verify_unary_objs_are_equal_when_their_only_args_are_equal(
609 &left_choose.set,
610 &right_choose.set,
611 verify_state,
612 equality_line_file,
613 ),
614 (Obj::CartDim(left_cart_dim), Obj::CartDim(right_cart_dim)) => self
615 .verify_unary_objs_are_equal_when_their_only_args_are_equal(
616 &left_cart_dim.set,
617 &right_cart_dim.set,
618 verify_state,
619 equality_line_file,
620 ),
621 (Obj::TupleDim(left_dim), Obj::TupleDim(right_dim)) => self
622 .verify_unary_objs_are_equal_when_their_only_args_are_equal(
623 &left_dim.arg,
624 &right_dim.arg,
625 verify_state,
626 equality_line_file,
627 ),
628 (Obj::Count(left_count), Obj::Count(right_count)) => self
629 .verify_unary_objs_are_equal_when_their_only_args_are_equal(
630 &left_count.set,
631 &right_count.set,
632 verify_state,
633 equality_line_file,
634 ),
635 (Obj::Range(left_range), Obj::Range(right_range)) => self
636 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
637 &left_range.start,
638 &left_range.end,
639 &right_range.start,
640 &right_range.end,
641 verify_state,
642 equality_line_file,
643 ),
644 (Obj::Sum(ls), Obj::Sum(rs)) => {
645 if !self.verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
646 &ls.start,
647 &ls.end,
648 &rs.start,
649 &rs.end,
650 verify_state,
651 equality_line_file.clone(),
652 )? {
653 return Ok(false);
654 }
655 self.verify_unary_objs_are_equal_when_their_only_args_are_equal(
656 ls.func.as_ref(),
657 rs.func.as_ref(),
658 verify_state,
659 equality_line_file,
660 )
661 }
662 (Obj::Product(ls), Obj::Product(rs)) => {
663 if !self.verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
664 &ls.start,
665 &ls.end,
666 &rs.start,
667 &rs.end,
668 verify_state,
669 equality_line_file.clone(),
670 )? {
671 return Ok(false);
672 }
673 self.verify_unary_objs_are_equal_when_their_only_args_are_equal(
674 ls.func.as_ref(),
675 rs.func.as_ref(),
676 verify_state,
677 equality_line_file,
678 )
679 }
680 (Obj::ClosedRange(left_closed_range), Obj::ClosedRange(right_closed_range)) => self
681 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
682 &left_closed_range.start,
683 &left_closed_range.end,
684 &right_closed_range.start,
685 &right_closed_range.end,
686 verify_state,
687 equality_line_file,
688 ),
689 (Obj::FiniteSeqSet(left_fs), Obj::FiniteSeqSet(right_fs)) => self
690 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
691 &left_fs.set,
692 &left_fs.n,
693 &right_fs.set,
694 &right_fs.n,
695 verify_state,
696 equality_line_file,
697 ),
698 (Obj::SeqSet(left_s), Obj::SeqSet(right_s)) => self
699 .verify_unary_objs_are_equal_when_their_only_args_are_equal(
700 left_s.set.as_ref(),
701 right_s.set.as_ref(),
702 verify_state,
703 equality_line_file,
704 ),
705 (Obj::FiniteSeqListObj(left_v), Obj::FiniteSeqListObj(right_v)) => self
706 .verify_obj_vec_are_equal_when_all_corresponding_args_are_equal(
707 &left_v.objs,
708 &right_v.objs,
709 verify_state,
710 equality_line_file,
711 ),
712 (Obj::MatrixSet(left_m), Obj::MatrixSet(right_m)) => {
713 if !self.verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
714 &left_m.set,
715 &left_m.row_len,
716 &right_m.set,
717 &right_m.row_len,
718 verify_state,
719 equality_line_file.clone(),
720 )? {
721 return Ok(false);
722 }
723 let result = self.verify_two_objs_equal_by_builtin_rules_and_known_equalities(
724 &left_m.col_len,
725 &right_m.col_len,
726 verify_state,
727 equality_line_file,
728 )?;
729 if result.is_unknown() {
730 return Ok(false);
731 }
732 Ok(true)
733 }
734 (Obj::MatrixListObj(left_m), Obj::MatrixListObj(right_m)) => self
735 .verify_matrix_list_objs_equal_when_all_cells_equal(
736 left_m,
737 right_m,
738 verify_state,
739 equality_line_file,
740 ),
741 (Obj::Proj(left_proj), Obj::Proj(right_proj)) => self
742 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
743 &left_proj.set,
744 &left_proj.dim,
745 &right_proj.set,
746 &right_proj.dim,
747 verify_state,
748 equality_line_file,
749 ),
750 (Obj::ObjAtIndex(left_obj_at_index), Obj::ObjAtIndex(right_obj_at_index)) => self
751 .verify_binary_objs_are_equal_when_both_corresponding_args_are_equal(
752 &left_obj_at_index.obj,
753 &left_obj_at_index.index,
754 &right_obj_at_index.obj,
755 &right_obj_at_index.index,
756 verify_state,
757 equality_line_file,
758 ),
759 (Obj::Tuple(left_tuple), Obj::Tuple(right_tuple)) => self
760 .verify_obj_vec_are_equal_when_all_corresponding_args_are_equal(
761 &left_tuple.args,
762 &right_tuple.args,
763 verify_state,
764 equality_line_file,
765 ),
766 (Obj::ListSet(left_list_set), Obj::ListSet(right_list_set)) => self
767 .verify_obj_vec_are_equal_when_all_corresponding_args_are_equal(
768 &left_list_set.list,
769 &right_list_set.list,
770 verify_state,
771 equality_line_file,
772 ),
773 (Obj::Cart(left_cart), Obj::Cart(right_cart)) => self
774 .verify_obj_vec_are_equal_when_all_corresponding_args_are_equal(
775 &left_cart.args,
776 &right_cart.args,
777 verify_state,
778 equality_line_file,
779 ),
780 _ => Ok(false),
781 }
782 }
783
784 fn verify_two_objs_equal_by_builtin_rules_and_known_equalities(
785 &mut self,
786 left_obj: &Obj,
787 right_obj: &Obj,
788 verify_state: &VerifyState,
789 equality_line_file: LineFile,
790 ) -> Result<StmtResult, RuntimeError> {
791 let mut result = self.verify_equality_by_builtin_rules(
792 left_obj,
793 right_obj,
794 equality_line_file.clone(),
795 verify_state,
796 )?;
797 if result.is_true() {
798 return Ok(
799 (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
800 EqualFact::new(
801 left_obj.clone(),
802 right_obj.clone(),
803 equality_line_file.clone(),
804 )
805 .into(),
806 "builtin rules".to_string(),
807 Vec::new(),
808 ))
809 .into(),
810 );
811 }
812
813 result = self.verify_equality_with_known_equalities(
814 left_obj,
815 right_obj,
816 equality_line_file.clone(),
817 verify_state,
818 )?;
819 if result.is_true() {
820 return Ok(result);
821 }
822
823 let verified_by_arg_to_arg = self
824 .verify_objs_are_equal_when_they_have_same_builtin_shape_and_equal_args_recursively(
825 left_obj,
826 right_obj,
827 verify_state,
828 equality_line_file.clone(),
829 )?;
830 if verified_by_arg_to_arg {
831 return Ok(
832 (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
833 EqualFact::new(left_obj.clone(), right_obj.clone(), equality_line_file).into(),
834 same_shape_and_equal_args_reason(left_obj, right_obj),
835 Vec::new(),
836 ))
837 .into(),
838 );
839 }
840
841 Ok((StmtUnknown::new()).into())
842 }
843}
844
845fn fn_obj_prefix_to_obj(fn_obj: &FnObj, number_of_body_groups_to_keep: usize) -> Obj {
846 if number_of_body_groups_to_keep == 0 {
847 return fn_obj.head.as_ref().clone().into();
848 }
849
850 let mut kept_body_groups: Vec<Vec<Box<Obj>>> = Vec::new();
851 let mut current_group_index = 0;
852 while current_group_index < number_of_body_groups_to_keep {
853 kept_body_groups.push(fn_obj.body[current_group_index].clone());
854 current_group_index += 1;
855 }
856
857 FnObj::new(fn_obj.head.as_ref().clone(), kept_body_groups).into()
858}
859
860fn same_shape_and_equal_args_reason(left_obj: &Obj, right_obj: &Obj) -> String {
861 match (left_obj, right_obj) {
862 (Obj::FnObj(_), Obj::FnObj(_)) => {
863 "the function parts are equal, and the function arguments are equal one by one"
864 .to_string()
865 }
866 _ => "the corresponding builtin-object arguments are equal one by one".to_string(),
867 }
868}