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