1use crate::prelude::*;
2use crate::verify::verify_equality_by_builtin_rules::{
3 factual_equal_success_by_builtin_reason, verify_equality_by_they_are_the_same,
4};
5use std::rc::Rc;
6
7impl Runtime {
8 fn try_verify_equality_pair_by_the_same_then_calculation_then_fn_obj_same_head_known_args(
9 &mut self,
10 left: &Obj,
11 right: &Obj,
12 line_file: LineFile,
13 verify_state: &VerifyState,
14 ) -> Result<Option<StmtResult>, RuntimeError> {
15 if let Obj::ObjAsStructInstanceWithFieldAccess(field_access) = left {
16 let projected = self.struct_field_access_projection(field_access)?;
17 return self
18 .try_verify_equality_pair_by_the_same_then_calculation_then_fn_obj_same_head_known_args(
19 &projected,
20 right,
21 line_file,
22 verify_state,
23 );
24 }
25 if let Obj::ObjAsStructInstanceWithFieldAccess(field_access) = right {
26 let projected = self.struct_field_access_projection(field_access)?;
27 return self
28 .try_verify_equality_pair_by_the_same_then_calculation_then_fn_obj_same_head_known_args(
29 left,
30 &projected,
31 line_file,
32 verify_state,
33 );
34 }
35 let (result, _, _) = self.verify_equality_by_they_are_the_same_and_calculation(
36 left,
37 right,
38 line_file.clone(),
39 verify_state,
40 )?;
41 if result.is_true() {
42 return Ok(Some(result));
43 }
44 if let Some(shape_result) =
45 self.try_verify_equal_by_same_shape_and_known_equality_args(left, right, line_file)
46 {
47 if shape_result.is_true() {
48 return Ok(Some(shape_result));
49 }
50 }
51 Ok(None)
52 }
53
54 pub fn try_verify_equality_with_known_equalities_by_builtin_rules_only(
55 &mut self,
56 left: &Obj,
57 right: &Obj,
58 line_file: LineFile,
59 verify_state: &VerifyState,
60 known_objs_equal_to_left: Option<&Rc<Vec<Obj>>>,
61 known_objs_equal_to_right: Option<&Rc<Vec<Obj>>>,
62 ) -> Result<Option<StmtResult>, RuntimeError> {
63 match (known_objs_equal_to_left, known_objs_equal_to_right) {
64 (None, None) => Ok(None),
65 (Some(known_objs_equal_to_left), None) => {
66 for obj in known_objs_equal_to_left.iter() {
67 if let Some(result) = self
68 .try_verify_equality_pair_by_the_same_then_calculation_then_fn_obj_same_head_known_args(
69 obj,
70 right,
71 line_file.clone(),
72 verify_state,
73 )?
74 {
75 return Ok(Some(result));
76 }
77 }
78 Ok(None)
79 }
80 (None, Some(known_objs_equal_to_right)) => {
81 for obj in known_objs_equal_to_right.iter() {
82 if let Some(result) = self
83 .try_verify_equality_pair_by_the_same_then_calculation_then_fn_obj_same_head_known_args(
84 left,
85 obj,
86 line_file.clone(),
87 verify_state,
88 )?
89 {
90 return Ok(Some(result));
91 }
92 }
93 Ok(None)
94 }
95 (Some(known_objs_equal_to_left), Some(known_objs_equal_to_right)) => {
96 for obj1 in known_objs_equal_to_left.iter() {
97 for obj2 in known_objs_equal_to_right.iter() {
98 if let Some(result) = self
99 .try_verify_equality_pair_by_the_same_then_calculation_then_fn_obj_same_head_known_args(
100 obj1,
101 obj2,
102 line_file.clone(),
103 verify_state,
104 )?
105 {
106 return Ok(Some(result));
107 }
108 }
109 }
110 Ok(None)
111 }
112 }
113 }
114
115 pub fn objs_have_same_known_equality_rc_in_some_env(&self, left: &Obj, right: &Obj) -> bool {
116 let left_key: ObjString = left.to_string();
117 let right_key: ObjString = right.to_string();
118 for env in self.iter_environments_from_top() {
119 let left_entry = env.known_equality.get(&left_key);
120 let right_entry = env.known_equality.get(&right_key);
121 if let (Some((_, left_rc)), Some((_, right_rc))) = (left_entry, right_entry) {
122 if Rc::ptr_eq(left_rc, right_rc) {
123 return true;
124 }
125 }
126 }
127 false
128 }
129
130 fn arg_pairs_share_known_equality_class(&self, pairs: &[(&Obj, &Obj)]) -> bool {
131 pairs
132 .iter()
133 .all(|(a, b)| self.objs_have_same_known_equality_rc_in_some_env(a, b))
134 }
135
136 fn boxed_obj_vecs_share_known_equality_class(
137 &self,
138 left: &[Box<Obj>],
139 right: &[Box<Obj>],
140 ) -> bool {
141 if left.len() != right.len() {
142 return false;
143 }
144 left.iter()
145 .zip(right.iter())
146 .all(|(a, b)| self.objs_have_same_known_equality_rc_in_some_env(a, b))
147 }
148
149 pub fn try_verify_equal_by_same_shape_and_known_equality_args(
150 &self,
151 left: &Obj,
152 right: &Obj,
153 line_file: LineFile,
154 ) -> Option<StmtResult> {
155 let reason = "same shape and paired args share known equality class";
156 match (left, right) {
157 (Obj::FnObj(left_fn), Obj::FnObj(right_fn)) => {
158 let left_head_obj = left_fn.head.as_ref().clone().into();
159 let right_head_obj = right_fn.head.as_ref().clone().into();
160 if !verify_equality_by_they_are_the_same(&left_head_obj, &right_head_obj) {
161 return Some((StmtUnknown::new()).into());
162 }
163 if left_fn.body.len() != right_fn.body.len() {
164 return Some((StmtUnknown::new()).into());
165 }
166 for (left_group, right_group) in left_fn.body.iter().zip(right_fn.body.iter()) {
167 if !self.boxed_obj_vecs_share_known_equality_class(left_group, right_group) {
168 return Some((StmtUnknown::new()).into());
169 }
170 }
171 Some(factual_equal_success_by_builtin_reason(
172 left, right, line_file, reason,
173 ))
174 }
175 (Obj::Add(l), Obj::Add(r)) => {
176 if self.arg_pairs_share_known_equality_class(&[
177 (&l.left, &r.left),
178 (&l.right, &r.right),
179 ]) {
180 Some(factual_equal_success_by_builtin_reason(
181 left, right, line_file, reason,
182 ))
183 } else {
184 Some((StmtUnknown::new()).into())
185 }
186 }
187 (Obj::MatrixAdd(l), Obj::MatrixAdd(r)) => {
188 if self.arg_pairs_share_known_equality_class(&[
189 (&l.left, &r.left),
190 (&l.right, &r.right),
191 ]) {
192 Some(factual_equal_success_by_builtin_reason(
193 left, right, line_file, reason,
194 ))
195 } else {
196 Some((StmtUnknown::new()).into())
197 }
198 }
199 (Obj::MatrixSub(l), Obj::MatrixSub(r)) => {
200 if self.arg_pairs_share_known_equality_class(&[
201 (&l.left, &r.left),
202 (&l.right, &r.right),
203 ]) {
204 Some(factual_equal_success_by_builtin_reason(
205 left, right, line_file, reason,
206 ))
207 } else {
208 Some((StmtUnknown::new()).into())
209 }
210 }
211 (Obj::MatrixMul(l), Obj::MatrixMul(r)) => {
212 if self.arg_pairs_share_known_equality_class(&[
213 (&l.left, &r.left),
214 (&l.right, &r.right),
215 ]) {
216 Some(factual_equal_success_by_builtin_reason(
217 left, right, line_file, reason,
218 ))
219 } else {
220 Some((StmtUnknown::new()).into())
221 }
222 }
223 (Obj::MatrixScalarMul(l), Obj::MatrixScalarMul(r)) => {
224 if self.arg_pairs_share_known_equality_class(&[
225 (&l.scalar, &r.scalar),
226 (&l.matrix, &r.matrix),
227 ]) {
228 Some(factual_equal_success_by_builtin_reason(
229 left, right, line_file, reason,
230 ))
231 } else {
232 Some((StmtUnknown::new()).into())
233 }
234 }
235 (Obj::MatrixPow(l), Obj::MatrixPow(r)) => {
236 if self.arg_pairs_share_known_equality_class(&[
237 (&l.base, &r.base),
238 (&l.exponent, &r.exponent),
239 ]) {
240 Some(factual_equal_success_by_builtin_reason(
241 left, right, line_file, reason,
242 ))
243 } else {
244 Some((StmtUnknown::new()).into())
245 }
246 }
247 (Obj::Sub(l), Obj::Sub(r)) => {
248 if self.arg_pairs_share_known_equality_class(&[
249 (&l.left, &r.left),
250 (&l.right, &r.right),
251 ]) {
252 Some(factual_equal_success_by_builtin_reason(
253 left, right, line_file, reason,
254 ))
255 } else {
256 Some((StmtUnknown::new()).into())
257 }
258 }
259 (Obj::Mul(l), Obj::Mul(r)) => {
260 if self.arg_pairs_share_known_equality_class(&[
261 (&l.left, &r.left),
262 (&l.right, &r.right),
263 ]) {
264 Some(factual_equal_success_by_builtin_reason(
265 left, right, line_file, reason,
266 ))
267 } else {
268 Some((StmtUnknown::new()).into())
269 }
270 }
271 (Obj::Div(l), Obj::Div(r)) => {
272 if self.arg_pairs_share_known_equality_class(&[
273 (&l.left, &r.left),
274 (&l.right, &r.right),
275 ]) {
276 Some(factual_equal_success_by_builtin_reason(
277 left, right, line_file, reason,
278 ))
279 } else {
280 Some((StmtUnknown::new()).into())
281 }
282 }
283 (Obj::Mod(l), Obj::Mod(r)) => {
284 if self.arg_pairs_share_known_equality_class(&[
285 (&l.left, &r.left),
286 (&l.right, &r.right),
287 ]) {
288 Some(factual_equal_success_by_builtin_reason(
289 left, right, line_file, reason,
290 ))
291 } else {
292 Some((StmtUnknown::new()).into())
293 }
294 }
295 (Obj::Pow(l), Obj::Pow(r)) => {
296 if self.arg_pairs_share_known_equality_class(&[
297 (&l.base, &r.base),
298 (&l.exponent, &r.exponent),
299 ]) {
300 Some(factual_equal_success_by_builtin_reason(
301 left, right, line_file, reason,
302 ))
303 } else {
304 Some((StmtUnknown::new()).into())
305 }
306 }
307 (Obj::Log(l), Obj::Log(r)) => {
308 if self
309 .arg_pairs_share_known_equality_class(&[(&l.base, &r.base), (&l.arg, &r.arg)])
310 {
311 Some(factual_equal_success_by_builtin_reason(
312 left, right, line_file, reason,
313 ))
314 } else {
315 Some((StmtUnknown::new()).into())
316 }
317 }
318 (Obj::Max(l), Obj::Max(r)) => {
319 if self.arg_pairs_share_known_equality_class(&[
320 (&l.left, &r.left),
321 (&l.right, &r.right),
322 ]) {
323 Some(factual_equal_success_by_builtin_reason(
324 left, right, line_file, reason,
325 ))
326 } else {
327 Some((StmtUnknown::new()).into())
328 }
329 }
330 (Obj::Min(l), Obj::Min(r)) => {
331 if self.arg_pairs_share_known_equality_class(&[
332 (&l.left, &r.left),
333 (&l.right, &r.right),
334 ]) {
335 Some(factual_equal_success_by_builtin_reason(
336 left, right, line_file, reason,
337 ))
338 } else {
339 Some((StmtUnknown::new()).into())
340 }
341 }
342 (Obj::Union(l), Obj::Union(r)) => {
343 if self.arg_pairs_share_known_equality_class(&[
344 (&l.left, &r.left),
345 (&l.right, &r.right),
346 ]) {
347 Some(factual_equal_success_by_builtin_reason(
348 left, right, line_file, reason,
349 ))
350 } else {
351 Some((StmtUnknown::new()).into())
352 }
353 }
354 (Obj::Intersect(l), Obj::Intersect(r)) => {
355 if self.arg_pairs_share_known_equality_class(&[
356 (&l.left, &r.left),
357 (&l.right, &r.right),
358 ]) {
359 Some(factual_equal_success_by_builtin_reason(
360 left, right, line_file, reason,
361 ))
362 } else {
363 Some((StmtUnknown::new()).into())
364 }
365 }
366 (Obj::SetMinus(l), Obj::SetMinus(r)) => {
367 if self.arg_pairs_share_known_equality_class(&[
368 (&l.left, &r.left),
369 (&l.right, &r.right),
370 ]) {
371 Some(factual_equal_success_by_builtin_reason(
372 left, right, line_file, reason,
373 ))
374 } else {
375 Some((StmtUnknown::new()).into())
376 }
377 }
378 (Obj::SetDiff(l), Obj::SetDiff(r)) => {
379 if self.arg_pairs_share_known_equality_class(&[
380 (&l.left, &r.left),
381 (&l.right, &r.right),
382 ]) {
383 Some(factual_equal_success_by_builtin_reason(
384 left, right, line_file, reason,
385 ))
386 } else {
387 Some((StmtUnknown::new()).into())
388 }
389 }
390 (Obj::Cup(l), Obj::Cup(r)) => {
391 if self.objs_have_same_known_equality_rc_in_some_env(&l.left, &r.left) {
392 Some(factual_equal_success_by_builtin_reason(
393 left, right, line_file, reason,
394 ))
395 } else {
396 Some((StmtUnknown::new()).into())
397 }
398 }
399 (Obj::Cap(l), Obj::Cap(r)) => {
400 if self.objs_have_same_known_equality_rc_in_some_env(&l.left, &r.left) {
401 Some(factual_equal_success_by_builtin_reason(
402 left, right, line_file, reason,
403 ))
404 } else {
405 Some((StmtUnknown::new()).into())
406 }
407 }
408 (Obj::PowerSet(l), Obj::PowerSet(r)) => {
409 if self.objs_have_same_known_equality_rc_in_some_env(&l.set, &r.set) {
410 Some(factual_equal_success_by_builtin_reason(
411 left, right, line_file, reason,
412 ))
413 } else {
414 Some((StmtUnknown::new()).into())
415 }
416 }
417 (Obj::Choose(l), Obj::Choose(r)) => {
418 if self.objs_have_same_known_equality_rc_in_some_env(&l.set, &r.set) {
419 Some(factual_equal_success_by_builtin_reason(
420 left, right, line_file, reason,
421 ))
422 } else {
423 Some((StmtUnknown::new()).into())
424 }
425 }
426 (Obj::CartDim(l), Obj::CartDim(r)) => {
427 if self.objs_have_same_known_equality_rc_in_some_env(&l.set, &r.set) {
428 Some(factual_equal_success_by_builtin_reason(
429 left, right, line_file, reason,
430 ))
431 } else {
432 Some((StmtUnknown::new()).into())
433 }
434 }
435 (Obj::TupleDim(l), Obj::TupleDim(r)) => {
436 if self.objs_have_same_known_equality_rc_in_some_env(&l.arg, &r.arg) {
437 Some(factual_equal_success_by_builtin_reason(
438 left, right, line_file, reason,
439 ))
440 } else {
441 Some((StmtUnknown::new()).into())
442 }
443 }
444 (Obj::Count(l), Obj::Count(r)) => {
445 if self.objs_have_same_known_equality_rc_in_some_env(&l.set, &r.set) {
446 Some(factual_equal_success_by_builtin_reason(
447 left, right, line_file, reason,
448 ))
449 } else {
450 Some((StmtUnknown::new()).into())
451 }
452 }
453 (Obj::Range(l), Obj::Range(r)) => {
454 if self
455 .arg_pairs_share_known_equality_class(&[(&l.start, &r.start), (&l.end, &r.end)])
456 {
457 Some(factual_equal_success_by_builtin_reason(
458 left, right, line_file, reason,
459 ))
460 } else {
461 Some((StmtUnknown::new()).into())
462 }
463 }
464 (Obj::Sum(l), Obj::Sum(r)) => {
465 if self.arg_pairs_share_known_equality_class(&[
466 (&l.start, &r.start),
467 (&l.end, &r.end),
468 (&l.func, &r.func),
469 ]) {
470 Some(factual_equal_success_by_builtin_reason(
471 left, right, line_file, reason,
472 ))
473 } else {
474 Some((StmtUnknown::new()).into())
475 }
476 }
477 (Obj::Product(l), Obj::Product(r)) => {
478 if self.arg_pairs_share_known_equality_class(&[
479 (&l.start, &r.start),
480 (&l.end, &r.end),
481 (&l.func, &r.func),
482 ]) {
483 Some(factual_equal_success_by_builtin_reason(
484 left, right, line_file, reason,
485 ))
486 } else {
487 Some((StmtUnknown::new()).into())
488 }
489 }
490 (Obj::ClosedRange(l), Obj::ClosedRange(r)) => {
491 if self
492 .arg_pairs_share_known_equality_class(&[(&l.start, &r.start), (&l.end, &r.end)])
493 {
494 Some(factual_equal_success_by_builtin_reason(
495 left, right, line_file, reason,
496 ))
497 } else {
498 Some((StmtUnknown::new()).into())
499 }
500 }
501 (Obj::FiniteSeqSet(l), Obj::FiniteSeqSet(r)) => {
502 if self.arg_pairs_share_known_equality_class(&[(&l.set, &r.set), (&l.n, &r.n)]) {
503 Some(factual_equal_success_by_builtin_reason(
504 left, right, line_file, reason,
505 ))
506 } else {
507 Some((StmtUnknown::new()).into())
508 }
509 }
510 (Obj::SeqSet(l), Obj::SeqSet(r)) => {
511 if self.arg_pairs_share_known_equality_class(&[(&l.set, &r.set)]) {
512 Some(factual_equal_success_by_builtin_reason(
513 left, right, line_file, reason,
514 ))
515 } else {
516 Some((StmtUnknown::new()).into())
517 }
518 }
519 (Obj::MatrixSet(l), Obj::MatrixSet(r)) => {
520 if self.arg_pairs_share_known_equality_class(&[
521 (&l.set, &r.set),
522 (&l.row_len, &r.row_len),
523 (&l.col_len, &r.col_len),
524 ]) {
525 Some(factual_equal_success_by_builtin_reason(
526 left, right, line_file, reason,
527 ))
528 } else {
529 Some((StmtUnknown::new()).into())
530 }
531 }
532 (Obj::Proj(l), Obj::Proj(r)) => {
533 if self.arg_pairs_share_known_equality_class(&[(&l.set, &r.set), (&l.dim, &r.dim)])
534 {
535 Some(factual_equal_success_by_builtin_reason(
536 left, right, line_file, reason,
537 ))
538 } else {
539 Some((StmtUnknown::new()).into())
540 }
541 }
542 (Obj::ObjAtIndex(l), Obj::ObjAtIndex(r)) => {
543 if self
544 .arg_pairs_share_known_equality_class(&[(&l.obj, &r.obj), (&l.index, &r.index)])
545 {
546 Some(factual_equal_success_by_builtin_reason(
547 left, right, line_file, reason,
548 ))
549 } else {
550 Some((StmtUnknown::new()).into())
551 }
552 }
553 (Obj::Tuple(l), Obj::Tuple(r)) => {
554 if self.boxed_obj_vecs_share_known_equality_class(&l.args, &r.args) {
555 Some(factual_equal_success_by_builtin_reason(
556 left, right, line_file, reason,
557 ))
558 } else {
559 Some((StmtUnknown::new()).into())
560 }
561 }
562 (Obj::ListSet(l), Obj::ListSet(r)) => {
563 if self.boxed_obj_vecs_share_known_equality_class(&l.list, &r.list) {
564 Some(factual_equal_success_by_builtin_reason(
565 left, right, line_file, reason,
566 ))
567 } else {
568 Some((StmtUnknown::new()).into())
569 }
570 }
571 (Obj::Cart(l), Obj::Cart(r)) => {
572 if self.boxed_obj_vecs_share_known_equality_class(&l.args, &r.args) {
573 Some(factual_equal_success_by_builtin_reason(
574 left, right, line_file, reason,
575 ))
576 } else {
577 Some((StmtUnknown::new()).into())
578 }
579 }
580 _ => None,
581 }
582 }
583
584 pub fn verify_equality_by_they_are_the_same_and_calculation(
585 &mut self,
586 left: &Obj,
587 right: &Obj,
588 line_file: LineFile,
589 _verify_state: &VerifyState,
590 ) -> Result<(StmtResult, Obj, Obj), RuntimeError> {
591 if verify_equality_by_they_are_the_same(left, right) {
592 return Ok((
593 factual_equal_success_by_builtin_reason(
594 left,
595 right,
596 line_file,
597 "they are the same",
598 ),
599 left.clone(),
600 right.clone(),
601 ));
602 }
603
604 let left_resolved = self.resolve_obj(left);
605 let right_resolved = self.resolve_obj(right);
606
607 if left_resolved.two_objs_can_be_calculated_and_equal_by_calculation(&right_resolved) {
608 return Ok((
609 factual_equal_success_by_builtin_reason(left, right, line_file, "calculation"),
610 left_resolved,
611 right_resolved,
612 ));
613 }
614
615 Ok((
616 StmtResult::StmtUnknown(StmtUnknown::new()),
617 left_resolved,
618 right_resolved,
619 ))
620 }
621}