1use crate::prelude::*;
2use std::collections::HashMap;
3use std::rc::Rc;
4use std::result::Result;
5
6impl Runtime {
7 pub fn verify_atomic_fact_with_known_forall(
8 &mut self,
9 atomic_fact: &AtomicFact,
10 verify_state: &VerifyState,
11 ) -> Result<StmtResult, RuntimeError> {
12 if let Some(fact_verified) =
13 self.try_verify_with_known_forall_facts_in_envs(atomic_fact, verify_state)?
14 {
15 return Ok((fact_verified).into());
16 }
17
18 if let AtomicFact::EqualFact(equal_fact) = atomic_fact {
19 let fact_with_reversed_args = EqualFact::new(
20 equal_fact.right.clone(),
21 equal_fact.left.clone(),
22 equal_fact.line_file.clone(),
23 );
24 if let Some(fact_verified) = self.try_verify_with_known_forall_facts_in_envs(
25 &fact_with_reversed_args.into(),
26 verify_state,
27 )? {
28 return Ok((fact_verified).into());
29 }
30 }
31
32 Ok((StmtUnknown::new()).into())
33 }
34
35 fn get_matched_atomic_fact_in_known_forall_fact_in_envs(
36 &mut self,
37 iterate_from_env_index: usize,
38 iterate_from_known_forall_fact_index: usize,
39 given_fact: &AtomicFact,
40 ) -> Result<
41 (
42 (usize, usize),
43 Option<HashMap<String, Obj>>,
44 Option<(AtomicFact, Rc<KnownForallFactParamsAndDom>)>,
45 ),
46 RuntimeError,
47 > {
48 let key = given_fact.key();
49 let is_true = given_fact.is_true();
50
51 let envs_count = self.environment_stack.len();
52 let lookup_key = (key.clone(), is_true);
53 for i in iterate_from_env_index..envs_count {
54 let stack_idx = envs_count - 1 - i;
55 let known_forall_facts_count = {
56 let env = &self.environment_stack[stack_idx];
57 match env.known_atomic_facts_in_forall_facts.get(&lookup_key) {
58 Some(v) => v.len(),
59 None => continue,
60 }
61 };
62 for j in iterate_from_known_forall_fact_index..known_forall_facts_count {
63 let entry_idx = known_forall_facts_count - 1 - j;
64 let (atomic_fact_args_in_known_forall, current_known_forall) = {
65 let env = &self.environment_stack[stack_idx];
66 let Some(known_forall_facts_in_env) =
67 env.known_atomic_facts_in_forall_facts.get(&lookup_key)
68 else {
69 continue;
70 };
71 let Some(current_known_forall) = known_forall_facts_in_env.get(entry_idx)
72 else {
73 continue;
74 };
75 (current_known_forall.0.args(), current_known_forall.clone())
76 };
77 let match_result = self.match_atomic_fact_args_against_known_forall_ordered_args(
78 &atomic_fact_args_in_known_forall,
79 given_fact,
80 )?;
81 if let Some(arg_map) = match_result {
82 return Ok(((i, j), Some(arg_map), Some(current_known_forall)));
83 }
84 }
85 }
86
87 Ok(((0, 0), None, None))
88 }
89
90 fn try_verify_with_known_forall_facts_in_envs(
91 &mut self,
92 atomic_fact: &AtomicFact,
93 verify_state: &VerifyState,
94 ) -> Result<Option<FactualStmtSuccess>, RuntimeError> {
95 let mut iterate_from_env_index = 0;
96 let mut iterate_from_known_forall_fact_index = 0;
97
98 loop {
99 let result = self.get_matched_atomic_fact_in_known_forall_fact_in_envs(
100 iterate_from_env_index,
101 iterate_from_known_forall_fact_index,
102 atomic_fact,
103 )?;
104 let ((i, j), arg_map_opt, known_forall_opt) = result;
105 match (arg_map_opt, known_forall_opt) {
106 (Some(arg_map), Some((atomic_fact_in_known_forall_fact, forall_rc))) => {
107 if let Some(fact_verified) = self.verify_args_satisfy_forall_requirements(
108 &atomic_fact_in_known_forall_fact,
109 &forall_rc,
110 arg_map,
111 atomic_fact,
112 verify_state,
113 )? {
114 return Ok(Some(fact_verified));
115 }
116 iterate_from_env_index = i;
117 iterate_from_known_forall_fact_index = j + 1;
118 }
119 _ => return Ok(None),
120 }
121 }
122 }
123
124 fn verify_args_satisfy_forall_requirements(
125 &mut self,
126 atomic_fact_in_known_forall_fact: &AtomicFact,
127 known_forall: &Rc<KnownForallFactParamsAndDom>,
128 arg_map: HashMap<String, Obj>,
129 given_atomic_fact: &AtomicFact,
130 verify_state: &VerifyState,
131 ) -> Result<Option<FactualStmtSuccess>, RuntimeError> {
132 let param_names = known_forall.params_def.collect_param_names();
133
134 if !param_names
135 .iter()
136 .all(|param_name| arg_map.contains_key(param_name))
137 {
138 return Ok(None);
139 }
140
141 let mut args_for_params: Vec<Obj> = Vec::new();
143
144 for param_name in param_names.iter() {
145 let obj = match arg_map.get(param_name) {
146 Some(v) => v,
147 None => return Ok(None),
148 };
149
150 args_for_params.push(obj.clone());
151 }
152
153 let args_param_types = self
154 .verify_args_satisfy_param_def_flat_types(
155 &known_forall.params_def,
156 &args_for_params,
157 verify_state,
158 ParamObjType::Forall,
159 )
160 .map_err(|e| {
161 {
162 RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
163 Some(Fact::from(given_atomic_fact.clone()).into_stmt()),
164 String::new(),
165 given_atomic_fact.line_file(),
166 Some(e),
167 vec![],
168 )))
169 }
170 })?;
171 if args_param_types.is_unknown() {
172 return Ok(None);
173 }
174
175 let param_to_arg_map = match known_forall
176 .params_def
177 .param_def_params_to_arg_map(&arg_map)
178 {
179 Some(m) => m,
180 None => return Ok(None),
181 };
182
183 for dom_fact in known_forall.dom.iter() {
184 let instantiated_dom_fact = self
185 .inst_fact(dom_fact, ¶m_to_arg_map, ParamObjType::Forall, None)
186 .map_err(|e| {
187 {
188 RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
189 Some(Fact::from(given_atomic_fact.clone()).into_stmt()),
190 String::new(),
191 given_atomic_fact.line_file(),
192 Some(e),
193 vec![],
194 )))
195 }
196 })?;
197 let result = self
198 .verify_fact(&instantiated_dom_fact, verify_state)
199 .map_err(|e| {
200 {
201 RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
202 Some(Fact::from(given_atomic_fact.clone()).into_stmt()),
203 String::new(),
204 given_atomic_fact.line_file(),
205 Some(e),
206 vec![],
207 )))
208 }
209 })?;
210 if result.is_unknown() {
211 return Ok(None);
212 }
213 }
214
215 let verified_by_known_forall_fact = ForallFact::new(
216 known_forall.params_def.clone(),
217 known_forall.dom.clone(),
218 vec![atomic_fact_in_known_forall_fact.clone().into()],
219 known_forall.line_file.clone(),
220 )?;
221 let fact_verified = FactualStmtSuccess::new_with_verified_by_known_fact(
222 given_atomic_fact.clone().into(),
223 VerifiedByResult::Fact(
224 verified_by_known_forall_fact.clone().into(),
225 verified_by_known_forall_fact.to_string(),
226 ),
227 Vec::new(),
228 );
229 Ok(Some(fact_verified))
230 }
231
232 fn match_atomic_fact_args_against_known_forall_ordered_args(
233 &mut self,
234 atomic_fact_args_in_known_forall: &Vec<Obj>,
235 given_fact: &AtomicFact,
236 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
237 let given_args = given_fact.args();
238 let forward = self.match_args_in_fact_in_known_forall_fact_with_given_args(
239 atomic_fact_args_in_known_forall,
240 &given_args,
241 )?;
242 return Ok(forward);
243 }
244
245 pub fn match_args_in_fact_in_known_forall_fact_with_given_args(
246 &mut self,
247 fact_args_in_known_forall: &Vec<Obj>,
248 given_fact_args: &Vec<Obj>,
249 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
250 if fact_args_in_known_forall.len() != given_fact_args.len() {
251 return Ok(None);
252 }
253
254 let mut atom_in_known_atomic_fact_to_matched_objs_in_given_fact_map: HashMap<String, Obj> =
255 HashMap::new();
256
257 for (arg_in_atomic_fact_in_known_forall, arg_in_given) in
258 fact_args_in_known_forall.iter().zip(given_fact_args.iter())
259 {
260 let sub_map_option = self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
261 arg_in_atomic_fact_in_known_forall,
262 arg_in_given,
263 )?;
264 let sub_map = match sub_map_option {
265 Some(m) => m,
266 None => return Ok(None),
267 };
268 if !self.merge_arg_match_map_into(
269 &mut atom_in_known_atomic_fact_to_matched_objs_in_given_fact_map,
270 sub_map,
271 ) {
272 return Ok(None);
273 }
274 }
275
276 Ok(Some(
277 atom_in_known_atomic_fact_to_matched_objs_in_given_fact_map,
278 ))
279 }
280
281 fn match_arg_in_atomic_fact_in_known_forall_with_given_arg(
284 &mut self,
285 known_arg: &Obj,
286 given_arg: &Obj,
287 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
288 match known_arg {
289 Obj::Atom(AtomObj::Identifier(ref id_known)) => {
291 if id_known.to_string() != given_arg.to_string() {
292 return Ok(None);
293 }
294 Ok(Some(HashMap::new()))
295 }
296 Obj::Atom(AtomObj::IdentifierWithMod(_)) => {
297 self.match_arg_when_left_is_identifier_with_mod(given_arg)
298 }
299 Obj::FnObj(ref f) => self.match_arg_when_left_is_fn_obj(f, given_arg),
300 Obj::Number(ref left) => self.match_arg_when_left_is_number(left, given_arg),
301 Obj::Add(ref a) => self.match_arg_when_left_is_add(&a.left, &a.right, given_arg),
302 Obj::MatrixAdd(ref a) => {
303 self.match_arg_when_left_is_matrix_add(&a.left, &a.right, given_arg)
304 }
305 Obj::MatrixSub(ref a) => {
306 self.match_arg_when_left_is_matrix_sub(&a.left, &a.right, given_arg)
307 }
308 Obj::MatrixMul(ref a) => {
309 self.match_arg_when_left_is_matrix_mul(&a.left, &a.right, given_arg)
310 }
311 Obj::MatrixScalarMul(ref a) => {
312 self.match_arg_when_left_is_matrix_scalar_mul(&a.scalar, &a.matrix, given_arg)
313 }
314 Obj::MatrixPow(ref a) => {
315 self.match_arg_when_left_is_matrix_pow(&a.base, &a.exponent, given_arg)
316 }
317 Obj::Sub(ref a) => self.match_arg_when_left_is_sub(&a.left, &a.right, given_arg),
318 Obj::Mul(ref a) => self.match_arg_when_left_is_mul(&a.left, &a.right, given_arg),
319 Obj::Div(ref a) => self.match_arg_when_left_is_div(&a.left, &a.right, given_arg),
320 Obj::Mod(ref a) => self.match_arg_when_left_is_mod(&a.left, &a.right, given_arg),
321 Obj::Pow(ref a) => self.match_arg_when_left_is_pow(&a.base, &a.exponent, given_arg),
322 Obj::Abs(ref a) => self.match_arg_when_left_is_abs(a.arg.as_ref(), given_arg),
323 Obj::Log(ref a) => self.match_arg_when_left_is_log(&a.base, &a.arg, given_arg),
324 Obj::Max(ref a) => self.match_arg_when_left_is_max(&a.left, &a.right, given_arg),
325 Obj::Min(ref a) => self.match_arg_when_left_is_min(&a.left, &a.right, given_arg),
326 Obj::Union(ref a) => self.match_arg_when_left_is_union(&a.left, &a.right, given_arg),
327 Obj::Intersect(ref a) => {
328 self.match_arg_when_left_is_intersect(&a.left, &a.right, given_arg)
329 }
330 Obj::SetMinus(ref a) => {
331 self.match_arg_when_left_is_set_minus(&a.left, &a.right, given_arg)
332 }
333 Obj::SetDiff(ref a) => {
334 self.match_arg_when_left_is_set_diff(&a.left, &a.right, given_arg)
335 }
336 Obj::Cup(ref a) => self.match_arg_when_left_is_cup(&a.left, given_arg),
337 Obj::Cap(ref a) => self.match_arg_when_left_is_cap(&a.left, given_arg),
338 Obj::ListSet(ref left) => self.match_arg_when_left_is_list_set(&left.list, given_arg),
339 Obj::SetBuilder(ref left) => self.match_arg_when_left_is_set_builder(left, given_arg),
340 Obj::FnSet(ref left) => self.match_arg_when_left_is_fn_set_with_params(left, given_arg),
341 Obj::AnonymousFn(ref left) => {
342 self.match_arg_when_left_is_anonymous_fn_with_params(left, given_arg)
343 }
344 Obj::StandardSet(StandardSet::NPos) => self.match_arg_when_left_is_n_pos_obj(given_arg),
345 Obj::StandardSet(StandardSet::N) => self.match_arg_when_left_is_n_obj(given_arg),
346 Obj::StandardSet(StandardSet::Q) => self.match_arg_when_left_is_q_obj(given_arg),
347 Obj::StandardSet(StandardSet::Z) => self.match_arg_when_left_is_z_obj(given_arg),
348 Obj::StandardSet(StandardSet::R) => self.match_arg_when_left_is_r_obj(given_arg),
349 Obj::Cart(ref left) => self.match_arg_when_left_is_cart(&left.args, given_arg),
350 Obj::CartDim(ref left) => {
351 self.match_arg_when_left_is_cart_dim(left.set.as_ref(), given_arg)
352 }
353 Obj::Proj(ref left) => {
354 self.match_arg_when_left_is_proj(left.set.as_ref(), left.dim.as_ref(), given_arg)
355 }
356 Obj::TupleDim(ref left) => {
357 self.match_arg_when_left_is_dim(left.arg.as_ref(), given_arg)
358 }
359 Obj::Tuple(ref left) => self.match_arg_when_left_is_tuple(&left.args, given_arg),
360 Obj::FiniteSeqListObj(ref left) => {
361 self.match_arg_when_left_is_finite_seq_list(&left.objs, given_arg)
362 }
363 Obj::Count(ref left) => self.match_arg_when_left_is_count(left.set.as_ref(), given_arg),
364 Obj::Sum(ref left) => self.match_arg_when_left_is_sum(
365 left.start.as_ref(),
366 left.end.as_ref(),
367 left.func.as_ref(),
368 given_arg,
369 ),
370 Obj::Product(ref left) => self.match_arg_when_left_is_product(
371 left.start.as_ref(),
372 left.end.as_ref(),
373 left.func.as_ref(),
374 given_arg,
375 ),
376 Obj::Range(ref left) => {
377 self.match_arg_when_left_is_range(left.start.as_ref(), left.end.as_ref(), given_arg)
378 }
379 Obj::ClosedRange(ref left) => self.match_arg_when_left_is_closed_range(
380 left.start.as_ref(),
381 left.end.as_ref(),
382 given_arg,
383 ),
384 Obj::FiniteSeqSet(ref left) => self.match_arg_when_left_is_finite_seq_set(
385 left.set.as_ref(),
386 left.n.as_ref(),
387 given_arg,
388 ),
389 Obj::SeqSet(ref left) => {
390 self.match_arg_when_left_is_seq_set(left.set.as_ref(), given_arg)
391 }
392 Obj::MatrixListObj(ref left) => {
393 self.match_arg_when_left_is_matrix_list(&left.rows, given_arg)
394 }
395 Obj::MatrixSet(ref left) => self.match_arg_when_left_is_matrix_set(
396 left.set.as_ref(),
397 left.row_len.as_ref(),
398 left.col_len.as_ref(),
399 given_arg,
400 ),
401 Obj::PowerSet(ref left) => {
402 self.match_arg_when_left_is_power_set(left.set.as_ref(), given_arg)
403 }
404 Obj::Choose(ref left) => {
405 self.match_arg_when_left_is_choose(left.set.as_ref(), given_arg)
406 }
407 Obj::ObjAtIndex(ref left) => self.match_arg_when_left_is_obj_at_index(
408 left.obj.as_ref(),
409 left.index.as_ref(),
410 given_arg,
411 ),
412 Obj::StandardSet(StandardSet::QPos) => self.match_arg_when_left_is_q_pos(given_arg),
413 Obj::StandardSet(StandardSet::RPos) => self.match_arg_when_left_is_r_pos(given_arg),
414 Obj::StandardSet(StandardSet::QNeg) => self.match_arg_when_left_is_q_neg(given_arg),
415 Obj::StandardSet(StandardSet::ZNeg) => self.match_arg_when_left_is_z_neg(given_arg),
416 Obj::StandardSet(StandardSet::RNeg) => self.match_arg_when_left_is_r_neg(given_arg),
417 Obj::StandardSet(StandardSet::QNz) => self.match_arg_when_left_is_q_nz(given_arg),
418 Obj::StandardSet(StandardSet::ZNz) => self.match_arg_when_left_is_z_nz(given_arg),
419 Obj::StandardSet(StandardSet::RNz) => self.match_arg_when_left_is_r_nz(given_arg),
420 Obj::FamilyObj(known) => match given_arg {
421 Obj::FamilyObj(given) => {
422 if known.name.to_string() != given.name.to_string() {
423 return Ok(None);
424 }
425 self.match_arg_vec_then_merge(&known.params, &given.params)
426 }
427 _ => Ok(None),
428 },
429 Obj::Atom(AtomObj::Forall(ref p)) => {
430 self.match_arg_when_left_is_forall_param(p, given_arg)
431 }
432 Obj::Atom(AtomObj::Def(ref p)) => {
433 if p.to_string() != given_arg.to_string() {
434 return Ok(None);
435 }
436 Ok(Some(HashMap::new()))
437 }
438 Obj::Atom(AtomObj::Exist(ref p)) => match given_arg {
439 Obj::Atom(AtomObj::Exist(_)) => {
440 let mut m = HashMap::new();
441 m.insert(p.name.clone(), given_arg.clone());
442 Ok(Some(m))
443 }
444 _ => {
445 if p.to_string() != given_arg.to_string() {
446 return Ok(None);
447 }
448 Ok(Some(HashMap::new()))
449 }
450 },
451 Obj::Atom(AtomObj::SetBuilder(ref p)) => {
452 if p.to_string() != given_arg.to_string() {
453 return Ok(None);
454 }
455 Ok(Some(HashMap::new()))
456 }
457 Obj::Atom(AtomObj::FnSet(ref p)) => {
458 if p.to_string() != given_arg.to_string() {
459 return Ok(None);
460 }
461 Ok(Some(HashMap::new()))
462 }
463 Obj::Atom(AtomObj::Induc(ref p)) => {
464 if p.to_string() != given_arg.to_string() {
465 return Ok(None);
466 }
467 Ok(Some(HashMap::new()))
468 }
469 Obj::Atom(AtomObj::DefAlgo(ref p)) => {
470 if p.to_string() != given_arg.to_string() {
471 return Ok(None);
472 }
473 Ok(Some(HashMap::new()))
474 }
475 }
476 }
477
478 fn match_arg_when_left_is_forall_param(
479 &mut self,
480 id_known: &ForallFreeParamObj,
481 given_arg: &Obj,
482 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
483 let mut map = HashMap::new();
484 map.insert(id_known.name.clone(), given_arg.clone());
485 Ok(Some(map))
486 }
487
488 fn match_arg_when_left_is_identifier_with_mod(
489 &mut self,
490 given_arg: &Obj,
491 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
492 match given_arg {
493 Obj::Atom(AtomObj::IdentifierWithMod(_)) => {
494 self.match_arg_type_not_implemented("IdentifierWithMod")
495 }
496 _ => Ok(None),
497 }
498 }
499
500 fn match_arg_when_left_is_fn_obj(
501 &mut self,
502 left: &FnObj,
503 right: &Obj,
504 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
505 match right {
506 Obj::FnObj(ref right_fn) => {
507 if left.body.len() != right_fn.body.len() {
509 return Ok(None);
510 }
511
512 let left_head: Obj = left.head.as_ref().clone().into();
513 let right_head: Obj = right_fn.head.as_ref().clone().into();
514
515 let head_match = self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
517 &left_head,
518 &right_head,
519 )?;
520 let mut head_map = match head_match {
521 Some(m) => m,
522 None => return Ok(None),
523 };
524
525 for (left_row, right_row) in left.body.iter().zip(right_fn.body.iter()) {
526 if left_row.len() != right_row.len() {
527 return Ok(None);
528 }
529 for (left_arg, right_arg) in left_row.iter().zip(right_row.iter()) {
530 let sub_map = match self
531 .match_arg_in_atomic_fact_in_known_forall_with_given_arg(
532 left_arg.as_ref(),
533 right_arg.as_ref(),
534 )? {
535 Some(m) => m,
536 None => return Ok(None),
537 };
538 if !self.merge_arg_match_map_into(&mut head_map, sub_map) {
539 return Ok(None);
540 }
541 }
542 }
543
544 Ok(Some(head_map))
545 }
546 _ => Ok(None),
547 }
548 }
549
550 fn match_arg_when_left_is_number(
551 &mut self,
552 left: &Number,
553 given_arg: &Obj,
554 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
555 if !given_arg.evaluate_to_normalized_decimal_number().is_some() {
556 return Ok(None);
557 }
558 let left_obj: Obj = left.clone().into();
559 if left_obj.two_objs_can_be_calculated_and_equal_by_calculation(given_arg) {
560 Ok(Some(HashMap::new()))
561 } else {
562 Ok(None)
563 }
564 }
565
566 fn match_arg_when_left_is_matrix_add(
567 &mut self,
568 left_left: &Obj,
569 left_right: &Obj,
570 given_arg: &Obj,
571 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
572 match given_arg {
573 Obj::MatrixAdd(ref g) => {
574 self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
575 }
576 _ => Ok(None),
577 }
578 }
579
580 fn match_arg_when_left_is_matrix_sub(
581 &mut self,
582 left_left: &Obj,
583 left_right: &Obj,
584 given_arg: &Obj,
585 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
586 match given_arg {
587 Obj::MatrixSub(ref g) => {
588 self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
589 }
590 _ => Ok(None),
591 }
592 }
593
594 fn match_arg_when_left_is_matrix_mul(
595 &mut self,
596 left_left: &Obj,
597 left_right: &Obj,
598 given_arg: &Obj,
599 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
600 match given_arg {
601 Obj::MatrixMul(ref g) => {
602 self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
603 }
604 _ => Ok(None),
605 }
606 }
607
608 fn match_arg_when_left_is_matrix_scalar_mul(
609 &mut self,
610 left_scalar: &Obj,
611 left_matrix: &Obj,
612 given_arg: &Obj,
613 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
614 match given_arg {
615 Obj::MatrixScalarMul(ref g) => {
616 self.match_arg_binary_then_merge(left_scalar, left_matrix, &g.scalar, &g.matrix)
617 }
618 _ => Ok(None),
619 }
620 }
621
622 fn match_arg_when_left_is_matrix_pow(
623 &mut self,
624 left_base: &Obj,
625 left_exp: &Obj,
626 given_arg: &Obj,
627 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
628 match given_arg {
629 Obj::MatrixPow(ref g) => {
630 self.match_arg_binary_then_merge(left_base, left_exp, &g.base, &g.exponent)
631 }
632 _ => Ok(None),
633 }
634 }
635
636 fn match_arg_when_left_is_add(
637 &mut self,
638 left_left: &Obj,
639 left_right: &Obj,
640 given_arg: &Obj,
641 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
642 match given_arg {
643 Obj::Add(ref g) => {
644 self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
645 }
646 _ => {
647 if let Obj::Number(left_left_number) = left_left {
648 let new_given = Sub::new(given_arg.clone(), left_left_number.clone().into());
649 return self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
650 left_right,
651 &new_given.into(),
652 );
653 } else if let Obj::Number(left_right_number) = left_right {
654 let new_given = Sub::new(given_arg.clone(), left_right_number.clone().into());
655 return self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
656 left_left,
657 &new_given.into(),
658 );
659 } else {
660 return Ok(None);
661 }
662 }
663 }
664 }
665
666 fn match_arg_when_left_is_sub(
667 &mut self,
668 left_left: &Obj,
669 left_right: &Obj,
670 given_arg: &Obj,
671 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
672 match given_arg {
673 Obj::Sub(ref g) => {
674 self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
675 }
676 _ => {
677 if let Obj::Number(right_number) = left_right {
678 let new_given = Add::new(right_number.clone().into(), given_arg.clone());
679 return self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
680 left_left,
681 &new_given.into(),
682 );
683 } else if let Obj::Number(left_left_number) = left_left {
684 let new_given = Sub::new(left_left_number.clone().into(), given_arg.clone());
685 return self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
686 left_right,
687 &new_given.into(),
688 );
689 } else {
690 return Ok(None);
691 }
692 }
693 }
694 }
695
696 fn match_arg_when_left_is_mul(
697 &mut self,
698 left_left: &Obj,
699 left_right: &Obj,
700 given_arg: &Obj,
701 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
702 match given_arg {
703 Obj::Mul(ref g) => {
704 self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
705 }
706 _ => {
707 let neg_one: Obj = Number::new("-1".to_string()).into();
708 let known_left_is_neg_one = match left_left {
709 Obj::Number(n) => {
710 let left_obj: Obj = n.clone().into();
711 "-1".to_string() == left_obj.to_string()
712 }
713 _ => false,
714 };
715 if known_left_is_neg_one {
716 let synthetic: Obj = Mul::new(neg_one, given_arg.clone()).into();
717 return self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
718 left_right, &synthetic,
719 );
720 } else {
721 if let Obj::Number(n) = left_left {
722 if n.normalized_value == "0".to_string() {
723 return Ok(None);
724 } else {
725 let synthetic: Obj =
726 Div::new(given_arg.clone(), n.clone().into()).into();
727 return self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
728 left_right, &synthetic,
729 );
730 }
731 } else if let Obj::Number(left_right_number) = left_right {
732 let new_given =
733 Div::new(given_arg.clone(), left_right_number.clone().into());
734 return self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
735 left_left,
736 &new_given.into(),
737 );
738 } else {
739 return Ok(None);
740 }
741 }
742 }
743 }
744 }
745
746 fn match_arg_when_left_is_div(
747 &mut self,
748 left_left: &Obj,
749 left_right: &Obj,
750 given_arg: &Obj,
751 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
752 match given_arg {
753 Obj::Div(ref g) => {
754 self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
755 }
756 _ => {
757 if let Obj::Number(left_right_number) = left_right {
758 let new_given = Mul::new(left_right_number.clone().into(), given_arg.clone());
759 return self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
760 left_left,
761 &new_given.into(),
762 );
763 } else {
764 return Ok(None);
765 }
766 }
767 }
768 }
769
770 fn match_arg_when_left_is_mod(
771 &mut self,
772 left_left: &Obj,
773 left_right: &Obj,
774 given_arg: &Obj,
775 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
776 match given_arg {
777 Obj::Mod(ref g) => {
778 self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
779 }
780 _ => Ok(None),
781 }
782 }
783
784 fn match_arg_when_left_is_pow(
785 &mut self,
786 left_left: &Obj,
787 left_right: &Obj,
788 given_arg: &Obj,
789 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
790 match given_arg {
791 Obj::Pow(ref g) => {
792 self.match_arg_binary_then_merge(left_left, left_right, &g.base, &g.exponent)
793 }
794 _ => Ok(None),
795 }
796 }
797
798 fn match_arg_when_left_is_abs(
799 &mut self,
800 left_arg: &Obj,
801 given_arg: &Obj,
802 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
803 match given_arg {
804 Obj::Abs(ref g) => {
805 self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(left_arg, &g.arg)
806 }
807 _ => Ok(None),
808 }
809 }
810
811 fn match_arg_when_left_is_log(
812 &mut self,
813 left_base: &Obj,
814 left_arg: &Obj,
815 given_arg: &Obj,
816 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
817 match given_arg {
818 Obj::Log(ref g) => {
819 self.match_arg_binary_then_merge(left_base, left_arg, &g.base, &g.arg)
820 }
821 _ => Ok(None),
822 }
823 }
824
825 fn match_arg_when_left_is_max(
826 &mut self,
827 left_left: &Obj,
828 left_right: &Obj,
829 given_arg: &Obj,
830 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
831 match given_arg {
832 Obj::Max(ref g) => {
833 self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
834 }
835 _ => Ok(None),
836 }
837 }
838
839 fn match_arg_when_left_is_min(
840 &mut self,
841 left_left: &Obj,
842 left_right: &Obj,
843 given_arg: &Obj,
844 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
845 match given_arg {
846 Obj::Min(ref g) => {
847 self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
848 }
849 _ => Ok(None),
850 }
851 }
852
853 fn match_arg_when_left_is_union(
854 &mut self,
855 left_left: &Obj,
856 left_right: &Obj,
857 given_arg: &Obj,
858 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
859 match given_arg {
860 Obj::Union(ref g) => {
861 self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
862 }
863 _ => Ok(None),
864 }
865 }
866
867 fn match_arg_when_left_is_intersect(
868 &mut self,
869 left_left: &Obj,
870 left_right: &Obj,
871 given_arg: &Obj,
872 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
873 match given_arg {
874 Obj::Intersect(ref g) => {
875 self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
876 }
877 _ => Ok(None),
878 }
879 }
880
881 fn match_arg_when_left_is_set_minus(
882 &mut self,
883 left_left: &Obj,
884 left_right: &Obj,
885 given_arg: &Obj,
886 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
887 match given_arg {
888 Obj::SetMinus(ref g) => {
889 self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
890 }
891 _ => Ok(None),
892 }
893 }
894
895 fn match_arg_when_left_is_set_diff(
896 &mut self,
897 left_left: &Obj,
898 left_right: &Obj,
899 given_arg: &Obj,
900 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
901 match given_arg {
902 Obj::SetDiff(ref g) => {
903 self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
904 }
905 _ => Ok(None),
906 }
907 }
908
909 fn match_arg_when_left_is_cup(
910 &mut self,
911 left_left: &Obj,
912 given_arg: &Obj,
913 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
914 match given_arg {
915 Obj::Cup(ref g) => {
916 self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(left_left, &g.left)
917 }
918 _ => Ok(None),
919 }
920 }
921
922 fn match_arg_when_left_is_cap(
923 &mut self,
924 left_left: &Obj,
925 given_arg: &Obj,
926 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
927 match given_arg {
928 Obj::Cap(ref g) => {
929 self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(left_left, &g.left)
930 }
931 _ => Ok(None),
932 }
933 }
934
935 fn match_arg_binary_then_merge(
937 &mut self,
938 left_left: &Obj,
939 left_right: &Obj,
940 given_left: &Obj,
941 given_right: &Obj,
942 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
943 let left_res =
944 self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(left_left, given_left)?;
945 let map1 = match left_res {
946 Some(m) => m,
947 None => return Ok(None),
948 };
949 let right_res =
950 self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(left_right, given_right)?;
951 let map2 = match right_res {
952 Some(m) => m,
953 None => return Ok(None),
954 };
955 let merged = self.merge_arg_match_maps(map1, map2);
956 Ok(merged)
957 }
958
959 fn match_arg_ternary_then_merge(
960 &mut self,
961 a1: &Obj,
962 a2: &Obj,
963 a3: &Obj,
964 b1: &Obj,
965 b2: &Obj,
966 b3: &Obj,
967 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
968 let m12 = self.match_arg_binary_then_merge(a1, a2, b1, b2)?;
969 let map12 = match m12 {
970 Some(m) => m,
971 None => return Ok(None),
972 };
973 let m3 = self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(a3, b3)?;
974 let map3 = match m3 {
975 Some(m) => m,
976 None => return Ok(None),
977 };
978 Ok(self.merge_arg_match_maps(map12, map3))
979 }
980
981 fn merge_arg_match_map_into(
983 &mut self,
984 into: &mut HashMap<String, Obj>,
985 from: HashMap<String, Obj>,
986 ) -> bool {
987 for (k, v) in from {
988 if let Some(existing) = into.get(&k) {
989 if existing.to_string() != v.to_string() {
990 return false;
991 }
992 }
993 into.insert(k, v);
994 }
995 true
996 }
997
998 fn merge_arg_match_maps(
999 &mut self,
1000 mut map1: HashMap<String, Obj>,
1001 map2: HashMap<String, Obj>,
1002 ) -> Option<HashMap<String, Obj>> {
1003 if !self.merge_arg_match_map_into(&mut map1, map2) {
1004 return None;
1005 }
1006 Some(map1)
1007 }
1008
1009 fn match_arg_pairs_then_merge<'a>(
1011 &mut self,
1012 pairs: impl Iterator<Item = (&'a Obj, &'a Obj)>,
1013 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1014 let mut merged: HashMap<String, Obj> = HashMap::new();
1015 for (left_elem, given_elem) in pairs {
1016 let sub_map = match self
1017 .match_arg_in_atomic_fact_in_known_forall_with_given_arg(left_elem, given_elem)?
1018 {
1019 Some(m) => m,
1020 None => return Ok(None),
1021 };
1022 if !self.merge_arg_match_map_into(&mut merged, sub_map) {
1023 return Ok(None);
1024 }
1025 }
1026 Ok(Some(merged))
1027 }
1028
1029 fn match_boxed_arg_vec_then_merge(
1030 &mut self,
1031 left_elements: &[Box<Obj>],
1032 given_elements: &[Box<Obj>],
1033 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1034 if left_elements.len() != given_elements.len() {
1035 return Ok(None);
1036 }
1037 self.match_arg_pairs_then_merge(
1038 left_elements
1039 .iter()
1040 .zip(given_elements.iter())
1041 .map(|(l, g)| (l.as_ref(), g.as_ref())),
1042 )
1043 }
1044
1045 fn match_arg_vec_then_merge(
1046 &mut self,
1047 left: &[Obj],
1048 given: &[Obj],
1049 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1050 if left.len() != given.len() {
1051 return Ok(None);
1052 }
1053 self.match_arg_pairs_then_merge(left.iter().zip(given.iter()).map(|(l, g)| (l, g)))
1054 }
1055
1056 fn match_arg_matrix_rows_then_merge(
1057 &mut self,
1058 left_rows: &[Vec<Box<Obj>>],
1059 given_rows: &[Vec<Box<Obj>>],
1060 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1061 if left_rows.len() != given_rows.len() {
1062 return Ok(None);
1063 }
1064 let mut merged: HashMap<String, Obj> = HashMap::new();
1065 for (lr, gr) in left_rows.iter().zip(given_rows.iter()) {
1066 let sub_map = match self.match_boxed_arg_vec_then_merge(lr, gr)? {
1067 Some(m) => m,
1068 None => return Ok(None),
1069 };
1070 if !self.merge_arg_match_map_into(&mut merged, sub_map) {
1071 return Ok(None);
1072 }
1073 }
1074 Ok(Some(merged))
1075 }
1076
1077 fn match_arg_when_left_is_list_set(
1078 &mut self,
1079 left_list: &[Box<Obj>],
1080 given_arg: &Obj,
1081 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1082 match given_arg {
1083 Obj::ListSet(ref given) => self.match_boxed_arg_vec_then_merge(left_list, &given.list),
1084 _ => Ok(None),
1085 }
1086 }
1087
1088 fn match_arg_or_and_chain_atomic_fact_in_known_forall(
1089 &mut self,
1090 left: &OrAndChainAtomicFact,
1091 given: &OrAndChainAtomicFact,
1092 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1093 let Some(pairs) =
1094 Self::_verify_or_and_chain_atomic_facts_the_same_type_and_return_matched_args(
1095 left, given,
1096 )?
1097 else {
1098 return Ok(None);
1099 };
1100 self.match_arg_pairs_then_merge(pairs.iter().map(|(l, g)| (l, g)))
1101 }
1102
1103 fn match_arg_when_left_is_set_builder(
1104 &mut self,
1105 left: &SetBuilder,
1106 given_arg: &Obj,
1107 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1108 let Obj::SetBuilder(given) = given_arg else {
1109 return Ok(None);
1110 };
1111 if left.param != given.param {
1112 return Ok(None);
1113 }
1114 let Some(mut merged) = self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
1115 left.param_set.as_ref(),
1116 given.param_set.as_ref(),
1117 )?
1118 else {
1119 return Ok(None);
1120 };
1121 if left.facts.len() != given.facts.len() {
1122 return Ok(None);
1123 }
1124 for (lf, gf) in left.facts.iter().zip(given.facts.iter()) {
1125 let Some(fact_map) = self.match_arg_or_and_chain_atomic_fact_in_known_forall(lf, gf)?
1126 else {
1127 return Ok(None);
1128 };
1129 if !self.merge_arg_match_map_into(&mut merged, fact_map) {
1130 return Ok(None);
1131 }
1132 }
1133 let verify_state = VerifyState::new_with_final_round(false);
1134 for value in merged.values() {
1135 if self
1136 .verify_obj_well_defined_and_store_cache(value, &verify_state)
1137 .is_err()
1138 {
1139 return Ok(None);
1140 }
1141 }
1142 Ok(Some(merged))
1143 }
1144
1145 fn match_arg_when_left_is_fn_set_with_params(
1146 &mut self,
1147 left: &FnSet,
1148 given_arg: &Obj,
1149 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1150 let Obj::FnSet(given) = given_arg else {
1151 return Ok(None);
1152 };
1153 if left.body.params_def_with_set.len() != given.body.params_def_with_set.len() {
1154 return Ok(None);
1155 }
1156 let mut merged: HashMap<String, Obj> = HashMap::new();
1157 for (lg, gg) in left
1158 .body
1159 .params_def_with_set
1160 .iter()
1161 .zip(given.body.params_def_with_set.iter())
1162 {
1163 if lg.params != gg.params {
1164 return Ok(None);
1165 }
1166 let Some(m) =
1167 self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(&lg.set, &gg.set)?
1168 else {
1169 return Ok(None);
1170 };
1171 if !self.merge_arg_match_map_into(&mut merged, m) {
1172 return Ok(None);
1173 }
1174 }
1175 if left.body.dom_facts.len() != given.body.dom_facts.len() {
1176 return Ok(None);
1177 }
1178 for (lf, gf) in left.body.dom_facts.iter().zip(given.body.dom_facts.iter()) {
1179 let Some(fact_map) = self.match_arg_or_and_chain_atomic_fact_in_known_forall(lf, gf)?
1180 else {
1181 return Ok(None);
1182 };
1183 if !self.merge_arg_match_map_into(&mut merged, fact_map) {
1184 return Ok(None);
1185 }
1186 }
1187 let Some(ret_map) = self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
1188 left.body.ret_set.as_ref(),
1189 given.body.ret_set.as_ref(),
1190 )?
1191 else {
1192 return Ok(None);
1193 };
1194 if !self.merge_arg_match_map_into(&mut merged, ret_map) {
1195 return Ok(None);
1196 }
1197 let verify_state = VerifyState::new_with_final_round(false);
1198 for value in merged.values() {
1199 if self
1200 .verify_obj_well_defined_and_store_cache(value, &verify_state)
1201 .is_err()
1202 {
1203 return Ok(None);
1204 }
1205 }
1206 Ok(Some(merged))
1207 }
1208
1209 fn match_arg_when_left_is_anonymous_fn_with_params(
1210 &mut self,
1211 left: &AnonymousFn,
1212 given_arg: &Obj,
1213 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1214 let Obj::AnonymousFn(given) = given_arg else {
1215 return Ok(None);
1216 };
1217 if left.body.params_def_with_set.len() != given.body.params_def_with_set.len() {
1218 return Ok(None);
1219 }
1220 let mut merged: HashMap<String, Obj> = HashMap::new();
1221 for (lg, gg) in left
1222 .body
1223 .params_def_with_set
1224 .iter()
1225 .zip(given.body.params_def_with_set.iter())
1226 {
1227 if lg.params != gg.params {
1228 return Ok(None);
1229 }
1230 let Some(m) =
1231 self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(&lg.set, &gg.set)?
1232 else {
1233 return Ok(None);
1234 };
1235 if !self.merge_arg_match_map_into(&mut merged, m) {
1236 return Ok(None);
1237 }
1238 }
1239 if left.body.dom_facts.len() != given.body.dom_facts.len() {
1240 return Ok(None);
1241 }
1242 for (lf, gf) in left.body.dom_facts.iter().zip(given.body.dom_facts.iter()) {
1243 let Some(fact_map) = self.match_arg_or_and_chain_atomic_fact_in_known_forall(lf, gf)?
1244 else {
1245 return Ok(None);
1246 };
1247 if !self.merge_arg_match_map_into(&mut merged, fact_map) {
1248 return Ok(None);
1249 }
1250 }
1251 let Some(ret_map) = self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
1252 left.body.ret_set.as_ref(),
1253 given.body.ret_set.as_ref(),
1254 )?
1255 else {
1256 return Ok(None);
1257 };
1258 if !self.merge_arg_match_map_into(&mut merged, ret_map) {
1259 return Ok(None);
1260 }
1261 let Some(eq_map) = self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
1262 left.equal_to.as_ref(),
1263 given.equal_to.as_ref(),
1264 )?
1265 else {
1266 return Ok(None);
1267 };
1268 if !self.merge_arg_match_map_into(&mut merged, eq_map) {
1269 return Ok(None);
1270 }
1271 let verify_state = VerifyState::new_with_final_round(false);
1272 for value in merged.values() {
1273 if self
1274 .verify_obj_well_defined_and_store_cache(value, &verify_state)
1275 .is_err()
1276 {
1277 return Ok(None);
1278 }
1279 }
1280 Ok(Some(merged))
1281 }
1282
1283 fn match_arg_when_left_is_n_pos_obj(
1284 &mut self,
1285 given_arg: &Obj,
1286 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1287 match given_arg {
1288 Obj::StandardSet(StandardSet::NPos) => self.match_arg_same_type(given_arg),
1289 _ => Ok(None),
1290 }
1291 }
1292
1293 fn match_arg_when_left_is_n_obj(
1294 &mut self,
1295 given_arg: &Obj,
1296 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1297 match given_arg {
1298 Obj::StandardSet(StandardSet::N) => self.match_arg_same_type(given_arg),
1299 _ => Ok(None),
1300 }
1301 }
1302
1303 fn match_arg_when_left_is_q_obj(
1304 &mut self,
1305 given_arg: &Obj,
1306 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1307 match given_arg {
1308 Obj::StandardSet(StandardSet::Q) => self.match_arg_same_type(given_arg),
1309 _ => Ok(None),
1310 }
1311 }
1312
1313 fn match_arg_when_left_is_z_obj(
1314 &mut self,
1315 given_arg: &Obj,
1316 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1317 match given_arg {
1318 Obj::StandardSet(StandardSet::Z) => self.match_arg_same_type(given_arg),
1319 _ => Ok(None),
1320 }
1321 }
1322
1323 fn match_arg_when_left_is_r_obj(
1324 &mut self,
1325 given_arg: &Obj,
1326 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1327 match given_arg {
1328 Obj::StandardSet(StandardSet::R) => self.match_arg_same_type(given_arg),
1329 _ => Ok(None),
1330 }
1331 }
1332
1333 fn match_arg_when_left_is_cart(
1334 &mut self,
1335 left_args: &[Box<Obj>],
1336 given_arg: &Obj,
1337 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1338 match given_arg {
1339 Obj::Cart(ref given) => self.match_boxed_arg_vec_then_merge(left_args, &given.args),
1340 _ => Ok(None),
1341 }
1342 }
1343
1344 fn match_arg_when_left_is_cart_dim(
1345 &mut self,
1346 left_set: &Obj,
1347 given_arg: &Obj,
1348 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1349 match given_arg {
1350 Obj::CartDim(ref given) => self
1351 .match_arg_in_atomic_fact_in_known_forall_with_given_arg(
1352 left_set,
1353 given.set.as_ref(),
1354 ),
1355 _ => Ok(None),
1356 }
1357 }
1358
1359 fn match_arg_when_left_is_proj(
1360 &mut self,
1361 left_set: &Obj,
1362 left_dim: &Obj,
1363 given_arg: &Obj,
1364 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1365 match given_arg {
1366 Obj::Proj(ref given) => self.match_arg_binary_then_merge(
1367 left_set,
1368 left_dim,
1369 given.set.as_ref(),
1370 given.dim.as_ref(),
1371 ),
1372 _ => Ok(None),
1373 }
1374 }
1375
1376 fn match_arg_when_left_is_dim(
1377 &mut self,
1378 left_dim: &Obj,
1379 given_arg: &Obj,
1380 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1381 match given_arg {
1382 Obj::TupleDim(ref given) => self
1383 .match_arg_in_atomic_fact_in_known_forall_with_given_arg(
1384 left_dim,
1385 given.arg.as_ref(),
1386 ),
1387 _ => Ok(None),
1388 }
1389 }
1390
1391 fn match_arg_when_left_is_tuple(
1392 &mut self,
1393 left_elements: &[Box<Obj>],
1394 given_arg: &Obj,
1395 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1396 match given_arg {
1397 Obj::Tuple(ref given) => {
1398 self.match_boxed_arg_vec_then_merge(left_elements, &given.args)
1399 }
1400 _ => Ok(None),
1401 }
1402 }
1403
1404 fn match_arg_when_left_is_finite_seq_list(
1405 &mut self,
1406 left_elements: &[Box<Obj>],
1407 given_arg: &Obj,
1408 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1409 match given_arg {
1410 Obj::FiniteSeqListObj(ref given) => {
1411 self.match_boxed_arg_vec_then_merge(left_elements, &given.objs)
1412 }
1413 _ => Ok(None),
1414 }
1415 }
1416
1417 fn match_arg_when_left_is_count(
1418 &mut self,
1419 left_set: &Obj,
1420 given_arg: &Obj,
1421 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1422 match given_arg {
1423 Obj::Count(ref given) => self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
1424 left_set,
1425 given.set.as_ref(),
1426 ),
1427 _ => Ok(None),
1428 }
1429 }
1430
1431 fn match_arg_when_left_is_range(
1432 &mut self,
1433 left_start: &Obj,
1434 left_end: &Obj,
1435 given_arg: &Obj,
1436 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1437 match given_arg {
1438 Obj::Range(ref given) => self.match_arg_binary_then_merge(
1439 left_start,
1440 left_end,
1441 given.start.as_ref(),
1442 given.end.as_ref(),
1443 ),
1444 _ => Ok(None),
1445 }
1446 }
1447
1448 fn match_arg_when_left_is_sum(
1449 &mut self,
1450 left_start: &Obj,
1451 left_end: &Obj,
1452 left_func: &Obj,
1453 given_arg: &Obj,
1454 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1455 match given_arg {
1456 Obj::Sum(ref g) => self.match_arg_ternary_then_merge(
1457 left_start,
1458 left_end,
1459 left_func,
1460 g.start.as_ref(),
1461 g.end.as_ref(),
1462 g.func.as_ref(),
1463 ),
1464 _ => Ok(None),
1465 }
1466 }
1467
1468 fn match_arg_when_left_is_product(
1469 &mut self,
1470 left_start: &Obj,
1471 left_end: &Obj,
1472 left_func: &Obj,
1473 given_arg: &Obj,
1474 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1475 match given_arg {
1476 Obj::Product(ref g) => self.match_arg_ternary_then_merge(
1477 left_start,
1478 left_end,
1479 left_func,
1480 g.start.as_ref(),
1481 g.end.as_ref(),
1482 g.func.as_ref(),
1483 ),
1484 _ => Ok(None),
1485 }
1486 }
1487
1488 fn match_arg_when_left_is_closed_range(
1489 &mut self,
1490 left_start: &Obj,
1491 left_end: &Obj,
1492 given_arg: &Obj,
1493 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1494 match given_arg {
1495 Obj::ClosedRange(ref given) => self.match_arg_binary_then_merge(
1496 left_start,
1497 left_end,
1498 given.start.as_ref(),
1499 given.end.as_ref(),
1500 ),
1501 _ => Ok(None),
1502 }
1503 }
1504
1505 fn match_arg_when_left_is_finite_seq_set(
1506 &mut self,
1507 left_set: &Obj,
1508 left_n: &Obj,
1509 given_arg: &Obj,
1510 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1511 match given_arg {
1512 Obj::FiniteSeqSet(ref given) => self.match_arg_binary_then_merge(
1513 left_set,
1514 left_n,
1515 given.set.as_ref(),
1516 given.n.as_ref(),
1517 ),
1518 _ => Ok(None),
1519 }
1520 }
1521
1522 fn match_arg_when_left_is_seq_set(
1523 &mut self,
1524 left_set: &Obj,
1525 given_arg: &Obj,
1526 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1527 match given_arg {
1528 Obj::SeqSet(ref given) => self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
1529 left_set,
1530 given.set.as_ref(),
1531 ),
1532 _ => Ok(None),
1533 }
1534 }
1535
1536 fn match_arg_when_left_is_matrix_list(
1537 &mut self,
1538 left_rows: &[Vec<Box<Obj>>],
1539 given_arg: &Obj,
1540 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1541 match given_arg {
1542 Obj::MatrixListObj(ref given) => {
1543 self.match_arg_matrix_rows_then_merge(left_rows, &given.rows)
1544 }
1545 _ => Ok(None),
1546 }
1547 }
1548
1549 fn match_arg_when_left_is_matrix_set(
1550 &mut self,
1551 left_set: &Obj,
1552 left_row_len: &Obj,
1553 left_col_len: &Obj,
1554 given_arg: &Obj,
1555 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1556 match given_arg {
1557 Obj::MatrixSet(ref given) => self.match_arg_ternary_then_merge(
1558 left_set,
1559 left_row_len,
1560 left_col_len,
1561 given.set.as_ref(),
1562 given.row_len.as_ref(),
1563 given.col_len.as_ref(),
1564 ),
1565 _ => Ok(None),
1566 }
1567 }
1568
1569 fn match_arg_when_left_is_power_set(
1570 &mut self,
1571 left_set: &Obj,
1572 given_arg: &Obj,
1573 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1574 match given_arg {
1575 Obj::PowerSet(ref given) => self
1576 .match_arg_in_atomic_fact_in_known_forall_with_given_arg(
1577 left_set,
1578 given.set.as_ref(),
1579 ),
1580 _ => Ok(None),
1581 }
1582 }
1583
1584 fn match_arg_when_left_is_choose(
1585 &mut self,
1586 left_set: &Obj,
1587 given_arg: &Obj,
1588 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1589 match given_arg {
1590 Obj::Choose(ref given) => self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
1591 left_set,
1592 given.set.as_ref(),
1593 ),
1594 _ => Ok(None),
1595 }
1596 }
1597
1598 fn match_arg_when_left_is_obj_at_index(
1599 &mut self,
1600 left_obj: &Obj,
1601 left_index: &Obj,
1602 given_arg: &Obj,
1603 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1604 match given_arg {
1605 Obj::ObjAtIndex(ref given) => self.match_arg_binary_then_merge(
1606 left_obj,
1607 left_index,
1608 given.obj.as_ref(),
1609 given.index.as_ref(),
1610 ),
1611 _ => Ok(None),
1612 }
1613 }
1614
1615 fn match_arg_when_left_is_q_pos(
1616 &mut self,
1617 given_arg: &Obj,
1618 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1619 match given_arg {
1620 Obj::StandardSet(StandardSet::QPos) => self.match_arg_same_type(given_arg),
1621 _ => Ok(None),
1622 }
1623 }
1624
1625 fn match_arg_when_left_is_r_pos(
1626 &mut self,
1627 given_arg: &Obj,
1628 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1629 match given_arg {
1630 Obj::StandardSet(StandardSet::RPos) => self.match_arg_same_type(given_arg),
1631 _ => Ok(None),
1632 }
1633 }
1634
1635 fn match_arg_when_left_is_q_neg(
1636 &mut self,
1637 given_arg: &Obj,
1638 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1639 match given_arg {
1640 Obj::StandardSet(StandardSet::QNeg) => self.match_arg_same_type(given_arg),
1641 _ => Ok(None),
1642 }
1643 }
1644
1645 fn match_arg_when_left_is_z_neg(
1646 &mut self,
1647 given_arg: &Obj,
1648 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1649 match given_arg {
1650 Obj::StandardSet(StandardSet::ZNeg) => self.match_arg_same_type(given_arg),
1651 _ => Ok(None),
1652 }
1653 }
1654
1655 fn match_arg_when_left_is_r_neg(
1656 &mut self,
1657 given_arg: &Obj,
1658 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1659 match given_arg {
1660 Obj::StandardSet(StandardSet::RNeg) => self.match_arg_same_type(given_arg),
1661 _ => Ok(None),
1662 }
1663 }
1664
1665 fn match_arg_when_left_is_q_nz(
1666 &mut self,
1667 given_arg: &Obj,
1668 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1669 match given_arg {
1670 Obj::StandardSet(StandardSet::QNz) => self.match_arg_same_type(given_arg),
1671 _ => Ok(None),
1672 }
1673 }
1674
1675 fn match_arg_when_left_is_z_nz(
1676 &mut self,
1677 given_arg: &Obj,
1678 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1679 match given_arg {
1680 Obj::StandardSet(StandardSet::ZNz) => self.match_arg_same_type(given_arg),
1681 _ => Ok(None),
1682 }
1683 }
1684
1685 fn match_arg_when_left_is_r_nz(
1686 &mut self,
1687 given_arg: &Obj,
1688 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1689 match given_arg {
1690 Obj::StandardSet(StandardSet::RNz) => self.match_arg_same_type(given_arg),
1691 _ => Ok(None),
1692 }
1693 }
1694
1695 fn match_arg_same_type(
1696 &mut self,
1697 given_arg: &Obj,
1698 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1699 let mut map = HashMap::new();
1700 map.insert(given_arg.to_string(), given_arg.clone());
1701 Ok(Some(map))
1702 }
1703
1704 fn match_arg_type_not_implemented(
1705 &mut self,
1706 obj_type_name: &str,
1707 ) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
1708 let _ = obj_type_name;
1709 Ok(None)
1710 }
1711}