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