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