use crate::prelude::*;
use std::collections::HashMap;
use std::rc::Rc;
use std::result::Result;
impl Runtime {
pub fn verify_atomic_fact_with_known_forall(
&mut self,
atomic_fact: &AtomicFact,
verify_state: &VerifyState,
) -> Result<StmtResult, RuntimeError> {
if let Some(fact_verified) =
self.try_verify_with_known_forall_facts_in_envs(atomic_fact, verify_state)?
{
return Ok((fact_verified).into());
}
if let AtomicFact::EqualFact(equal_fact) = atomic_fact {
let fact_with_reversed_args = EqualFact::new(
equal_fact.right.clone(),
equal_fact.left.clone(),
equal_fact.line_file.clone(),
);
if let Some(fact_verified) = self.try_verify_with_known_forall_facts_in_envs(
&fact_with_reversed_args.into(),
verify_state,
)? {
return Ok((fact_verified).into());
}
}
Ok((StmtUnknown::new()).into())
}
fn get_matched_atomic_fact_in_known_forall_fact_in_envs(
&mut self,
iterate_from_env_index: usize,
iterate_from_known_forall_fact_index: usize,
given_fact: &AtomicFact,
) -> Result<
(
(usize, usize),
Option<HashMap<String, Obj>>,
Option<(AtomicFact, Rc<KnownForallFactParamsAndDom>)>,
),
RuntimeError,
> {
let key = given_fact.key();
let is_true = given_fact.is_true();
let envs_count = self.environment_stack.len();
let lookup_key = (key.clone(), is_true);
for i in iterate_from_env_index..envs_count {
let stack_idx = envs_count - 1 - i;
let known_forall_facts_count = {
let env = &self.environment_stack[stack_idx];
match env.known_atomic_facts_in_forall_facts.get(&lookup_key) {
Some(v) => v.len(),
None => continue,
}
};
for j in iterate_from_known_forall_fact_index..known_forall_facts_count {
let entry_idx = known_forall_facts_count - 1 - j;
let (atomic_fact_args_in_known_forall, current_known_forall) = {
let env = &self.environment_stack[stack_idx];
let Some(known_forall_facts_in_env) =
env.known_atomic_facts_in_forall_facts.get(&lookup_key)
else {
continue;
};
let Some(current_known_forall) = known_forall_facts_in_env.get(entry_idx)
else {
continue;
};
(current_known_forall.0.args(), current_known_forall.clone())
};
let match_result = self.match_atomic_fact_args_against_known_forall_ordered_args(
&atomic_fact_args_in_known_forall,
given_fact,
)?;
if let Some(arg_map) = match_result {
return Ok(((i, j), Some(arg_map), Some(current_known_forall)));
}
}
}
Ok(((0, 0), None, None))
}
fn try_verify_with_known_forall_facts_in_envs(
&mut self,
atomic_fact: &AtomicFact,
verify_state: &VerifyState,
) -> Result<Option<FactualStmtSuccess>, RuntimeError> {
let mut iterate_from_env_index = 0;
let mut iterate_from_known_forall_fact_index = 0;
loop {
let result = self.get_matched_atomic_fact_in_known_forall_fact_in_envs(
iterate_from_env_index,
iterate_from_known_forall_fact_index,
atomic_fact,
)?;
let ((i, j), arg_map_opt, known_forall_opt) = result;
match (arg_map_opt, known_forall_opt) {
(Some(arg_map), Some((atomic_fact_in_known_forall_fact, forall_rc))) => {
if let Some(fact_verified) = self.verify_args_satisfy_forall_requirements(
&atomic_fact_in_known_forall_fact,
&forall_rc,
arg_map,
atomic_fact,
verify_state,
)? {
return Ok(Some(fact_verified));
}
iterate_from_env_index = i;
iterate_from_known_forall_fact_index = j + 1;
}
_ => return Ok(None),
}
}
}
fn verify_args_satisfy_forall_requirements(
&mut self,
atomic_fact_in_known_forall_fact: &AtomicFact,
known_forall: &Rc<KnownForallFactParamsAndDom>,
arg_map: HashMap<String, Obj>,
given_atomic_fact: &AtomicFact,
verify_state: &VerifyState,
) -> Result<Option<FactualStmtSuccess>, RuntimeError> {
let param_names = known_forall.params_def.collect_param_names();
if !param_names
.iter()
.all(|param_name| arg_map.contains_key(param_name))
{
return Ok(None);
}
let mut args_for_params: Vec<Obj> = Vec::new();
for param_name in param_names.iter() {
let obj = match arg_map.get(param_name) {
Some(v) => v,
None => return Ok(None),
};
args_for_params.push(obj.clone());
}
let args_param_types = self
.verify_args_satisfy_param_def_flat_types(
&known_forall.params_def,
&args_for_params,
verify_state,
ParamObjType::Forall,
)
.map_err(|e| {
{
RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
Some(Fact::from(given_atomic_fact.clone()).into_stmt()),
String::new(),
given_atomic_fact.line_file(),
Some(e),
vec![],
)))
}
})?;
if args_param_types.is_unknown() {
return Ok(None);
}
let param_to_arg_map = match known_forall
.params_def
.param_def_params_to_arg_map(&arg_map)
{
Some(m) => m,
None => return Ok(None),
};
for dom_fact in known_forall.dom.iter() {
let instantiated_dom_fact = self
.inst_fact(dom_fact, ¶m_to_arg_map, ParamObjType::Forall, None)
.map_err(|e| {
{
RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
Some(Fact::from(given_atomic_fact.clone()).into_stmt()),
String::new(),
given_atomic_fact.line_file(),
Some(e),
vec![],
)))
}
})?;
let result = self
.verify_fact(&instantiated_dom_fact, verify_state)
.map_err(|e| {
{
RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
Some(Fact::from(given_atomic_fact.clone()).into_stmt()),
String::new(),
given_atomic_fact.line_file(),
Some(e),
vec![],
)))
}
})?;
if result.is_unknown() {
return Ok(None);
}
}
let verified_by_known_forall_fact = ForallFact::new(
known_forall.params_def.clone(),
known_forall.dom.clone(),
vec![atomic_fact_in_known_forall_fact.clone().into()],
known_forall.line_file.clone(),
)?;
let fact_verified =
FactualStmtSuccess::new_with_verified_by_known_fact_source_recording_facts(
given_atomic_fact.clone().into(),
verified_by_known_forall_fact.to_string(),
Some(verified_by_known_forall_fact.clone().into()),
None,
Vec::new(),
);
Ok(Some(fact_verified))
}
fn match_atomic_fact_args_against_known_forall_ordered_args(
&mut self,
atomic_fact_args_in_known_forall: &Vec<Obj>,
given_fact: &AtomicFact,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
let given_args = given_fact.args();
let forward = self.match_args_in_fact_in_known_forall_fact_with_given_args(
atomic_fact_args_in_known_forall,
&given_args,
)?;
return Ok(forward);
}
pub fn match_args_in_fact_in_known_forall_fact_with_given_args(
&mut self,
fact_args_in_known_forall: &Vec<Obj>,
given_fact_args: &Vec<Obj>,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
if fact_args_in_known_forall.len() != given_fact_args.len() {
return Ok(None);
}
let mut atom_in_known_atomic_fact_to_matched_objs_in_given_fact_map: HashMap<String, Obj> =
HashMap::new();
for (arg_in_atomic_fact_in_known_forall, arg_in_given) in
fact_args_in_known_forall.iter().zip(given_fact_args.iter())
{
let sub_map_option = self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
arg_in_atomic_fact_in_known_forall,
arg_in_given,
)?;
let sub_map = match sub_map_option {
Some(m) => m,
None => return Ok(None),
};
if !self.merge_arg_match_map_into(
&mut atom_in_known_atomic_fact_to_matched_objs_in_given_fact_map,
sub_map,
) {
return Ok(None);
}
}
Ok(Some(
atom_in_known_atomic_fact_to_matched_objs_in_given_fact_map,
))
}
fn match_arg_in_atomic_fact_in_known_forall_with_given_arg(
&mut self,
known_arg: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match known_arg {
Obj::Atom(AtomObj::Identifier(ref id_known)) => {
if id_known.to_string() != given_arg.to_string() {
return Ok(None);
}
Ok(Some(HashMap::new()))
}
Obj::Atom(AtomObj::IdentifierWithMod(_)) => {
self.match_arg_when_left_is_identifier_with_mod(given_arg)
}
Obj::FnObj(ref f) => self.match_arg_when_left_is_fn_obj(f, given_arg),
Obj::Number(ref left) => self.match_arg_when_left_is_number(left, given_arg),
Obj::Add(ref a) => self.match_arg_when_left_is_add(&a.left, &a.right, given_arg),
Obj::MatrixAdd(ref a) => {
self.match_arg_when_left_is_matrix_add(&a.left, &a.right, given_arg)
}
Obj::MatrixSub(ref a) => {
self.match_arg_when_left_is_matrix_sub(&a.left, &a.right, given_arg)
}
Obj::MatrixMul(ref a) => {
self.match_arg_when_left_is_matrix_mul(&a.left, &a.right, given_arg)
}
Obj::MatrixScalarMul(ref a) => {
self.match_arg_when_left_is_matrix_scalar_mul(&a.scalar, &a.matrix, given_arg)
}
Obj::MatrixPow(ref a) => {
self.match_arg_when_left_is_matrix_pow(&a.base, &a.exponent, given_arg)
}
Obj::Sub(ref a) => self.match_arg_when_left_is_sub(&a.left, &a.right, given_arg),
Obj::Mul(ref a) => self.match_arg_when_left_is_mul(&a.left, &a.right, given_arg),
Obj::Div(ref a) => self.match_arg_when_left_is_div(&a.left, &a.right, given_arg),
Obj::Mod(ref a) => self.match_arg_when_left_is_mod(&a.left, &a.right, given_arg),
Obj::Pow(ref a) => self.match_arg_when_left_is_pow(&a.base, &a.exponent, given_arg),
Obj::Abs(ref a) => self.match_arg_when_left_is_abs(a.arg.as_ref(), given_arg),
Obj::Log(ref a) => self.match_arg_when_left_is_log(&a.base, &a.arg, given_arg),
Obj::Max(ref a) => self.match_arg_when_left_is_max(&a.left, &a.right, given_arg),
Obj::Min(ref a) => self.match_arg_when_left_is_min(&a.left, &a.right, given_arg),
Obj::Union(ref a) => self.match_arg_when_left_is_union(&a.left, &a.right, given_arg),
Obj::Intersect(ref a) => {
self.match_arg_when_left_is_intersect(&a.left, &a.right, given_arg)
}
Obj::SetMinus(ref a) => {
self.match_arg_when_left_is_set_minus(&a.left, &a.right, given_arg)
}
Obj::SetDiff(ref a) => {
self.match_arg_when_left_is_set_diff(&a.left, &a.right, given_arg)
}
Obj::Cup(ref a) => self.match_arg_when_left_is_cup(&a.left, given_arg),
Obj::Cap(ref a) => self.match_arg_when_left_is_cap(&a.left, given_arg),
Obj::ListSet(ref left) => self.match_arg_when_left_is_list_set(&left.list, given_arg),
Obj::SetBuilder(ref left) => self.match_arg_when_left_is_set_builder(left, given_arg),
Obj::FnSet(ref left) => self.match_arg_when_left_is_fn_set_with_params(left, given_arg),
Obj::AnonymousFn(ref left) => {
self.match_arg_when_left_is_anonymous_fn_with_params(left, given_arg)
}
Obj::StandardSet(StandardSet::NPos) => self.match_arg_when_left_is_n_pos_obj(given_arg),
Obj::StandardSet(StandardSet::N) => self.match_arg_when_left_is_n_obj(given_arg),
Obj::StandardSet(StandardSet::Q) => self.match_arg_when_left_is_q_obj(given_arg),
Obj::StandardSet(StandardSet::Z) => self.match_arg_when_left_is_z_obj(given_arg),
Obj::StandardSet(StandardSet::R) => self.match_arg_when_left_is_r_obj(given_arg),
Obj::Cart(ref left) => self.match_arg_when_left_is_cart(&left.args, given_arg),
Obj::CartDim(ref left) => {
self.match_arg_when_left_is_cart_dim(left.set.as_ref(), given_arg)
}
Obj::Proj(ref left) => {
self.match_arg_when_left_is_proj(left.set.as_ref(), left.dim.as_ref(), given_arg)
}
Obj::TupleDim(ref left) => {
self.match_arg_when_left_is_dim(left.arg.as_ref(), given_arg)
}
Obj::Tuple(ref left) => self.match_arg_when_left_is_tuple(&left.args, given_arg),
Obj::FiniteSeqListObj(ref left) => {
self.match_arg_when_left_is_finite_seq_list(&left.objs, given_arg)
}
Obj::Count(ref left) => self.match_arg_when_left_is_count(left.set.as_ref(), given_arg),
Obj::Sum(ref left) => self.match_arg_when_left_is_sum(
left.start.as_ref(),
left.end.as_ref(),
left.func.as_ref(),
given_arg,
),
Obj::Product(ref left) => self.match_arg_when_left_is_product(
left.start.as_ref(),
left.end.as_ref(),
left.func.as_ref(),
given_arg,
),
Obj::Range(ref left) => {
self.match_arg_when_left_is_range(left.start.as_ref(), left.end.as_ref(), given_arg)
}
Obj::ClosedRange(ref left) => self.match_arg_when_left_is_closed_range(
left.start.as_ref(),
left.end.as_ref(),
given_arg,
),
Obj::FiniteSeqSet(ref left) => self.match_arg_when_left_is_finite_seq_set(
left.set.as_ref(),
left.n.as_ref(),
given_arg,
),
Obj::SeqSet(ref left) => {
self.match_arg_when_left_is_seq_set(left.set.as_ref(), given_arg)
}
Obj::MatrixListObj(ref left) => {
self.match_arg_when_left_is_matrix_list(&left.rows, given_arg)
}
Obj::MatrixSet(ref left) => self.match_arg_when_left_is_matrix_set(
left.set.as_ref(),
left.row_len.as_ref(),
left.col_len.as_ref(),
given_arg,
),
Obj::PowerSet(ref left) => {
self.match_arg_when_left_is_power_set(left.set.as_ref(), given_arg)
}
Obj::Choose(ref left) => {
self.match_arg_when_left_is_choose(left.set.as_ref(), given_arg)
}
Obj::ObjAtIndex(ref left) => self.match_arg_when_left_is_obj_at_index(
left.obj.as_ref(),
left.index.as_ref(),
given_arg,
),
Obj::StandardSet(StandardSet::QPos) => self.match_arg_when_left_is_q_pos(given_arg),
Obj::StandardSet(StandardSet::RPos) => self.match_arg_when_left_is_r_pos(given_arg),
Obj::StandardSet(StandardSet::QNeg) => self.match_arg_when_left_is_q_neg(given_arg),
Obj::StandardSet(StandardSet::ZNeg) => self.match_arg_when_left_is_z_neg(given_arg),
Obj::StandardSet(StandardSet::RNeg) => self.match_arg_when_left_is_r_neg(given_arg),
Obj::StandardSet(StandardSet::QNz) => self.match_arg_when_left_is_q_nz(given_arg),
Obj::StandardSet(StandardSet::ZNz) => self.match_arg_when_left_is_z_nz(given_arg),
Obj::StandardSet(StandardSet::RNz) => self.match_arg_when_left_is_r_nz(given_arg),
Obj::FamilyObj(known) => match given_arg {
Obj::FamilyObj(given) => {
if known.name.to_string() != given.name.to_string() {
return Ok(None);
}
self.match_arg_vec_then_merge(&known.params, &given.params)
}
_ => Ok(None),
},
Obj::Atom(AtomObj::Forall(ref p)) => {
self.match_arg_when_left_is_forall_param(p, given_arg)
}
Obj::Atom(AtomObj::Def(ref p)) => {
if p.to_string() != given_arg.to_string() {
return Ok(None);
}
Ok(Some(HashMap::new()))
}
Obj::Atom(AtomObj::Exist(ref p)) => match given_arg {
Obj::Atom(AtomObj::Exist(_)) => {
let mut m = HashMap::new();
m.insert(p.name.clone(), given_arg.clone());
Ok(Some(m))
}
_ => {
if p.to_string() != given_arg.to_string() {
return Ok(None);
}
Ok(Some(HashMap::new()))
}
},
Obj::Atom(AtomObj::SetBuilder(ref p)) => {
if p.to_string() != given_arg.to_string() {
return Ok(None);
}
Ok(Some(HashMap::new()))
}
Obj::Atom(AtomObj::FnSet(ref p)) => {
if p.to_string() != given_arg.to_string() {
return Ok(None);
}
Ok(Some(HashMap::new()))
}
Obj::Atom(AtomObj::Induc(ref p)) => {
if p.to_string() != given_arg.to_string() {
return Ok(None);
}
Ok(Some(HashMap::new()))
}
Obj::Atom(AtomObj::DefAlgo(ref p)) => {
if p.to_string() != given_arg.to_string() {
return Ok(None);
}
Ok(Some(HashMap::new()))
}
}
}
fn match_arg_when_left_is_forall_param(
&mut self,
id_known: &ForallFreeParamObj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
let mut map = HashMap::new();
map.insert(id_known.name.clone(), given_arg.clone());
Ok(Some(map))
}
fn match_arg_when_left_is_identifier_with_mod(
&mut self,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::Atom(AtomObj::IdentifierWithMod(_)) => {
self.match_arg_type_not_implemented("IdentifierWithMod")
}
_ => Ok(None),
}
}
fn match_arg_when_left_is_fn_obj(
&mut self,
left: &FnObj,
right: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match right {
Obj::FnObj(ref right_fn) => {
if left.body.len() != right_fn.body.len() {
return Ok(None);
}
let left_head: Obj = left.head.as_ref().clone().into();
let right_head: Obj = right_fn.head.as_ref().clone().into();
let head_match = self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
&left_head,
&right_head,
)?;
let mut head_map = match head_match {
Some(m) => m,
None => return Ok(None),
};
for (left_row, right_row) in left.body.iter().zip(right_fn.body.iter()) {
if left_row.len() != right_row.len() {
return Ok(None);
}
for (left_arg, right_arg) in left_row.iter().zip(right_row.iter()) {
let sub_map = match self
.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
left_arg.as_ref(),
right_arg.as_ref(),
)? {
Some(m) => m,
None => return Ok(None),
};
if !self.merge_arg_match_map_into(&mut head_map, sub_map) {
return Ok(None);
}
}
}
Ok(Some(head_map))
}
_ => Ok(None),
}
}
fn match_arg_when_left_is_number(
&mut self,
left: &Number,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
if !given_arg.evaluate_to_normalized_decimal_number().is_some() {
return Ok(None);
}
let left_obj: Obj = left.clone().into();
if left_obj.two_objs_can_be_calculated_and_equal_by_calculation(given_arg) {
Ok(Some(HashMap::new()))
} else {
Ok(None)
}
}
fn match_arg_when_left_is_matrix_add(
&mut self,
left_left: &Obj,
left_right: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::MatrixAdd(ref g) => {
self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
}
_ => Ok(None),
}
}
fn match_arg_when_left_is_matrix_sub(
&mut self,
left_left: &Obj,
left_right: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::MatrixSub(ref g) => {
self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
}
_ => Ok(None),
}
}
fn match_arg_when_left_is_matrix_mul(
&mut self,
left_left: &Obj,
left_right: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::MatrixMul(ref g) => {
self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
}
_ => Ok(None),
}
}
fn match_arg_when_left_is_matrix_scalar_mul(
&mut self,
left_scalar: &Obj,
left_matrix: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::MatrixScalarMul(ref g) => {
self.match_arg_binary_then_merge(left_scalar, left_matrix, &g.scalar, &g.matrix)
}
_ => Ok(None),
}
}
fn match_arg_when_left_is_matrix_pow(
&mut self,
left_base: &Obj,
left_exp: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::MatrixPow(ref g) => {
self.match_arg_binary_then_merge(left_base, left_exp, &g.base, &g.exponent)
}
_ => Ok(None),
}
}
fn match_arg_when_left_is_add(
&mut self,
left_left: &Obj,
left_right: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::Add(ref g) => {
self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
}
_ => {
if let Obj::Number(left_left_number) = left_left {
let new_given = Sub::new(given_arg.clone(), left_left_number.clone().into());
return self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
left_right,
&new_given.into(),
);
} else if let Obj::Number(left_right_number) = left_right {
let new_given = Sub::new(given_arg.clone(), left_right_number.clone().into());
return self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
left_left,
&new_given.into(),
);
} else {
return Ok(None);
}
}
}
}
fn match_arg_when_left_is_sub(
&mut self,
left_left: &Obj,
left_right: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::Sub(ref g) => {
self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
}
_ => {
if let Obj::Number(right_number) = left_right {
let new_given = Add::new(right_number.clone().into(), given_arg.clone());
return self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
left_left,
&new_given.into(),
);
} else if let Obj::Number(left_left_number) = left_left {
let new_given = Sub::new(left_left_number.clone().into(), given_arg.clone());
return self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
left_right,
&new_given.into(),
);
} else {
return Ok(None);
}
}
}
}
fn match_arg_when_left_is_mul(
&mut self,
left_left: &Obj,
left_right: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::Mul(ref g) => {
self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
}
_ => {
let neg_one: Obj = Number::new("-1".to_string()).into();
let known_left_is_neg_one = match left_left {
Obj::Number(n) => {
let left_obj: Obj = n.clone().into();
"-1".to_string() == left_obj.to_string()
}
_ => false,
};
if known_left_is_neg_one {
let synthetic: Obj = Mul::new(neg_one, given_arg.clone()).into();
return self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
left_right, &synthetic,
);
} else {
if let Obj::Number(n) = left_left {
if n.normalized_value == "0".to_string() {
return Ok(None);
} else {
let synthetic: Obj =
Div::new(given_arg.clone(), n.clone().into()).into();
return self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
left_right, &synthetic,
);
}
} else if let Obj::Number(left_right_number) = left_right {
let new_given =
Div::new(given_arg.clone(), left_right_number.clone().into());
return self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
left_left,
&new_given.into(),
);
} else {
return Ok(None);
}
}
}
}
}
fn match_arg_when_left_is_div(
&mut self,
left_left: &Obj,
left_right: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::Div(ref g) => {
self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
}
_ => {
if let Obj::Number(left_right_number) = left_right {
let new_given = Mul::new(left_right_number.clone().into(), given_arg.clone());
return self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
left_left,
&new_given.into(),
);
} else {
return Ok(None);
}
}
}
}
fn match_arg_when_left_is_mod(
&mut self,
left_left: &Obj,
left_right: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::Mod(ref g) => {
self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
}
_ => Ok(None),
}
}
fn match_arg_when_left_is_pow(
&mut self,
left_left: &Obj,
left_right: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::Pow(ref g) => {
self.match_arg_binary_then_merge(left_left, left_right, &g.base, &g.exponent)
}
_ => Ok(None),
}
}
fn match_arg_when_left_is_abs(
&mut self,
left_arg: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::Abs(ref g) => {
self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(left_arg, &g.arg)
}
_ => Ok(None),
}
}
fn match_arg_when_left_is_log(
&mut self,
left_base: &Obj,
left_arg: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::Log(ref g) => {
self.match_arg_binary_then_merge(left_base, left_arg, &g.base, &g.arg)
}
_ => Ok(None),
}
}
fn match_arg_when_left_is_max(
&mut self,
left_left: &Obj,
left_right: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::Max(ref g) => {
self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
}
_ => Ok(None),
}
}
fn match_arg_when_left_is_min(
&mut self,
left_left: &Obj,
left_right: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::Min(ref g) => {
self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
}
_ => Ok(None),
}
}
fn match_arg_when_left_is_union(
&mut self,
left_left: &Obj,
left_right: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::Union(ref g) => {
self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
}
_ => Ok(None),
}
}
fn match_arg_when_left_is_intersect(
&mut self,
left_left: &Obj,
left_right: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::Intersect(ref g) => {
self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
}
_ => Ok(None),
}
}
fn match_arg_when_left_is_set_minus(
&mut self,
left_left: &Obj,
left_right: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::SetMinus(ref g) => {
self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
}
_ => Ok(None),
}
}
fn match_arg_when_left_is_set_diff(
&mut self,
left_left: &Obj,
left_right: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::SetDiff(ref g) => {
self.match_arg_binary_then_merge(left_left, left_right, &g.left, &g.right)
}
_ => Ok(None),
}
}
fn match_arg_when_left_is_cup(
&mut self,
left_left: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::Cup(ref g) => {
self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(left_left, &g.left)
}
_ => Ok(None),
}
}
fn match_arg_when_left_is_cap(
&mut self,
left_left: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::Cap(ref g) => {
self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(left_left, &g.left)
}
_ => Ok(None),
}
}
fn match_arg_binary_then_merge(
&mut self,
left_left: &Obj,
left_right: &Obj,
given_left: &Obj,
given_right: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
let left_res =
self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(left_left, given_left)?;
let map1 = match left_res {
Some(m) => m,
None => return Ok(None),
};
let right_res =
self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(left_right, given_right)?;
let map2 = match right_res {
Some(m) => m,
None => return Ok(None),
};
let merged = self.merge_arg_match_maps(map1, map2);
Ok(merged)
}
fn match_arg_ternary_then_merge(
&mut self,
a1: &Obj,
a2: &Obj,
a3: &Obj,
b1: &Obj,
b2: &Obj,
b3: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
let m12 = self.match_arg_binary_then_merge(a1, a2, b1, b2)?;
let map12 = match m12 {
Some(m) => m,
None => return Ok(None),
};
let m3 = self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(a3, b3)?;
let map3 = match m3 {
Some(m) => m,
None => return Ok(None),
};
Ok(self.merge_arg_match_maps(map12, map3))
}
fn merge_arg_match_map_into(
&mut self,
into: &mut HashMap<String, Obj>,
from: HashMap<String, Obj>,
) -> bool {
for (k, v) in from {
if let Some(existing) = into.get(&k) {
if existing.to_string() != v.to_string() {
return false;
}
}
into.insert(k, v);
}
true
}
fn merge_arg_match_maps(
&mut self,
mut map1: HashMap<String, Obj>,
map2: HashMap<String, Obj>,
) -> Option<HashMap<String, Obj>> {
if !self.merge_arg_match_map_into(&mut map1, map2) {
return None;
}
Some(map1)
}
fn match_arg_pairs_then_merge<'a>(
&mut self,
pairs: impl Iterator<Item = (&'a Obj, &'a Obj)>,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
let mut merged: HashMap<String, Obj> = HashMap::new();
for (left_elem, given_elem) in pairs {
let sub_map = match self
.match_arg_in_atomic_fact_in_known_forall_with_given_arg(left_elem, given_elem)?
{
Some(m) => m,
None => return Ok(None),
};
if !self.merge_arg_match_map_into(&mut merged, sub_map) {
return Ok(None);
}
}
Ok(Some(merged))
}
fn match_boxed_arg_vec_then_merge(
&mut self,
left_elements: &[Box<Obj>],
given_elements: &[Box<Obj>],
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
if left_elements.len() != given_elements.len() {
return Ok(None);
}
self.match_arg_pairs_then_merge(
left_elements
.iter()
.zip(given_elements.iter())
.map(|(l, g)| (l.as_ref(), g.as_ref())),
)
}
fn match_arg_vec_then_merge(
&mut self,
left: &[Obj],
given: &[Obj],
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
if left.len() != given.len() {
return Ok(None);
}
self.match_arg_pairs_then_merge(left.iter().zip(given.iter()).map(|(l, g)| (l, g)))
}
fn match_arg_matrix_rows_then_merge(
&mut self,
left_rows: &[Vec<Box<Obj>>],
given_rows: &[Vec<Box<Obj>>],
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
if left_rows.len() != given_rows.len() {
return Ok(None);
}
let mut merged: HashMap<String, Obj> = HashMap::new();
for (lr, gr) in left_rows.iter().zip(given_rows.iter()) {
let sub_map = match self.match_boxed_arg_vec_then_merge(lr, gr)? {
Some(m) => m,
None => return Ok(None),
};
if !self.merge_arg_match_map_into(&mut merged, sub_map) {
return Ok(None);
}
}
Ok(Some(merged))
}
fn match_arg_when_left_is_list_set(
&mut self,
left_list: &[Box<Obj>],
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::ListSet(ref given) => self.match_boxed_arg_vec_then_merge(left_list, &given.list),
_ => Ok(None),
}
}
fn match_arg_or_and_chain_atomic_fact_in_known_forall(
&mut self,
left: &OrAndChainAtomicFact,
given: &OrAndChainAtomicFact,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
let Some(pairs) =
Self::_verify_or_and_chain_atomic_facts_the_same_type_and_return_matched_args(
left, given,
)?
else {
return Ok(None);
};
self.match_arg_pairs_then_merge(pairs.iter().map(|(l, g)| (l, g)))
}
fn match_arg_when_left_is_set_builder(
&mut self,
left: &SetBuilder,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
let Obj::SetBuilder(given) = given_arg else {
return Ok(None);
};
if left.param != given.param {
return Ok(None);
}
let Some(mut merged) = self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
left.param_set.as_ref(),
given.param_set.as_ref(),
)?
else {
return Ok(None);
};
if left.facts.len() != given.facts.len() {
return Ok(None);
}
for (lf, gf) in left.facts.iter().zip(given.facts.iter()) {
let Some(fact_map) = self.match_arg_or_and_chain_atomic_fact_in_known_forall(lf, gf)?
else {
return Ok(None);
};
if !self.merge_arg_match_map_into(&mut merged, fact_map) {
return Ok(None);
}
}
let verify_state = VerifyState::new_with_final_round(false);
for value in merged.values() {
if self
.verify_obj_well_defined_and_store_cache(value, &verify_state)
.is_err()
{
return Ok(None);
}
}
Ok(Some(merged))
}
fn match_arg_when_left_is_fn_set_with_params(
&mut self,
left: &FnSet,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
let Obj::FnSet(given) = given_arg else {
return Ok(None);
};
if left.body.params_def_with_set.len() != given.body.params_def_with_set.len() {
return Ok(None);
}
let mut merged: HashMap<String, Obj> = HashMap::new();
for (lg, gg) in left
.body
.params_def_with_set
.iter()
.zip(given.body.params_def_with_set.iter())
{
if lg.params != gg.params {
return Ok(None);
}
let Some(m) =
self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(&lg.set, &gg.set)?
else {
return Ok(None);
};
if !self.merge_arg_match_map_into(&mut merged, m) {
return Ok(None);
}
}
if left.body.dom_facts.len() != given.body.dom_facts.len() {
return Ok(None);
}
for (lf, gf) in left.body.dom_facts.iter().zip(given.body.dom_facts.iter()) {
let Some(fact_map) = self.match_arg_or_and_chain_atomic_fact_in_known_forall(lf, gf)?
else {
return Ok(None);
};
if !self.merge_arg_match_map_into(&mut merged, fact_map) {
return Ok(None);
}
}
let Some(ret_map) = self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
left.body.ret_set.as_ref(),
given.body.ret_set.as_ref(),
)?
else {
return Ok(None);
};
if !self.merge_arg_match_map_into(&mut merged, ret_map) {
return Ok(None);
}
let verify_state = VerifyState::new_with_final_round(false);
for value in merged.values() {
if self
.verify_obj_well_defined_and_store_cache(value, &verify_state)
.is_err()
{
return Ok(None);
}
}
Ok(Some(merged))
}
fn match_arg_when_left_is_anonymous_fn_with_params(
&mut self,
left: &AnonymousFn,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
let Obj::AnonymousFn(given) = given_arg else {
return Ok(None);
};
if left.body.params_def_with_set.len() != given.body.params_def_with_set.len() {
return Ok(None);
}
let mut merged: HashMap<String, Obj> = HashMap::new();
for (lg, gg) in left
.body
.params_def_with_set
.iter()
.zip(given.body.params_def_with_set.iter())
{
if lg.params != gg.params {
return Ok(None);
}
let Some(m) =
self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(&lg.set, &gg.set)?
else {
return Ok(None);
};
if !self.merge_arg_match_map_into(&mut merged, m) {
return Ok(None);
}
}
if left.body.dom_facts.len() != given.body.dom_facts.len() {
return Ok(None);
}
for (lf, gf) in left.body.dom_facts.iter().zip(given.body.dom_facts.iter()) {
let Some(fact_map) = self.match_arg_or_and_chain_atomic_fact_in_known_forall(lf, gf)?
else {
return Ok(None);
};
if !self.merge_arg_match_map_into(&mut merged, fact_map) {
return Ok(None);
}
}
let Some(ret_map) = self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
left.body.ret_set.as_ref(),
given.body.ret_set.as_ref(),
)?
else {
return Ok(None);
};
if !self.merge_arg_match_map_into(&mut merged, ret_map) {
return Ok(None);
}
let Some(eq_map) = self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
left.equal_to.as_ref(),
given.equal_to.as_ref(),
)?
else {
return Ok(None);
};
if !self.merge_arg_match_map_into(&mut merged, eq_map) {
return Ok(None);
}
let verify_state = VerifyState::new_with_final_round(false);
for value in merged.values() {
if self
.verify_obj_well_defined_and_store_cache(value, &verify_state)
.is_err()
{
return Ok(None);
}
}
Ok(Some(merged))
}
fn match_arg_when_left_is_n_pos_obj(
&mut self,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::StandardSet(StandardSet::NPos) => self.match_arg_same_type(given_arg),
_ => Ok(None),
}
}
fn match_arg_when_left_is_n_obj(
&mut self,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::StandardSet(StandardSet::N) => self.match_arg_same_type(given_arg),
_ => Ok(None),
}
}
fn match_arg_when_left_is_q_obj(
&mut self,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::StandardSet(StandardSet::Q) => self.match_arg_same_type(given_arg),
_ => Ok(None),
}
}
fn match_arg_when_left_is_z_obj(
&mut self,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::StandardSet(StandardSet::Z) => self.match_arg_same_type(given_arg),
_ => Ok(None),
}
}
fn match_arg_when_left_is_r_obj(
&mut self,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::StandardSet(StandardSet::R) => self.match_arg_same_type(given_arg),
_ => Ok(None),
}
}
fn match_arg_when_left_is_cart(
&mut self,
left_args: &[Box<Obj>],
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::Cart(ref given) => self.match_boxed_arg_vec_then_merge(left_args, &given.args),
_ => Ok(None),
}
}
fn match_arg_when_left_is_cart_dim(
&mut self,
left_set: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::CartDim(ref given) => self
.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
left_set,
given.set.as_ref(),
),
_ => Ok(None),
}
}
fn match_arg_when_left_is_proj(
&mut self,
left_set: &Obj,
left_dim: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::Proj(ref given) => self.match_arg_binary_then_merge(
left_set,
left_dim,
given.set.as_ref(),
given.dim.as_ref(),
),
_ => Ok(None),
}
}
fn match_arg_when_left_is_dim(
&mut self,
left_dim: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::TupleDim(ref given) => self
.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
left_dim,
given.arg.as_ref(),
),
_ => Ok(None),
}
}
fn match_arg_when_left_is_tuple(
&mut self,
left_elements: &[Box<Obj>],
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::Tuple(ref given) => {
self.match_boxed_arg_vec_then_merge(left_elements, &given.args)
}
_ => Ok(None),
}
}
fn match_arg_when_left_is_finite_seq_list(
&mut self,
left_elements: &[Box<Obj>],
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::FiniteSeqListObj(ref given) => {
self.match_boxed_arg_vec_then_merge(left_elements, &given.objs)
}
_ => Ok(None),
}
}
fn match_arg_when_left_is_count(
&mut self,
left_set: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::Count(ref given) => self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
left_set,
given.set.as_ref(),
),
_ => Ok(None),
}
}
fn match_arg_when_left_is_range(
&mut self,
left_start: &Obj,
left_end: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::Range(ref given) => self.match_arg_binary_then_merge(
left_start,
left_end,
given.start.as_ref(),
given.end.as_ref(),
),
_ => Ok(None),
}
}
fn match_arg_when_left_is_sum(
&mut self,
left_start: &Obj,
left_end: &Obj,
left_func: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::Sum(ref g) => self.match_arg_ternary_then_merge(
left_start,
left_end,
left_func,
g.start.as_ref(),
g.end.as_ref(),
g.func.as_ref(),
),
_ => Ok(None),
}
}
fn match_arg_when_left_is_product(
&mut self,
left_start: &Obj,
left_end: &Obj,
left_func: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::Product(ref g) => self.match_arg_ternary_then_merge(
left_start,
left_end,
left_func,
g.start.as_ref(),
g.end.as_ref(),
g.func.as_ref(),
),
_ => Ok(None),
}
}
fn match_arg_when_left_is_closed_range(
&mut self,
left_start: &Obj,
left_end: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::ClosedRange(ref given) => self.match_arg_binary_then_merge(
left_start,
left_end,
given.start.as_ref(),
given.end.as_ref(),
),
_ => Ok(None),
}
}
fn match_arg_when_left_is_finite_seq_set(
&mut self,
left_set: &Obj,
left_n: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::FiniteSeqSet(ref given) => self.match_arg_binary_then_merge(
left_set,
left_n,
given.set.as_ref(),
given.n.as_ref(),
),
_ => Ok(None),
}
}
fn match_arg_when_left_is_seq_set(
&mut self,
left_set: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::SeqSet(ref given) => self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
left_set,
given.set.as_ref(),
),
_ => Ok(None),
}
}
fn match_arg_when_left_is_matrix_list(
&mut self,
left_rows: &[Vec<Box<Obj>>],
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::MatrixListObj(ref given) => {
self.match_arg_matrix_rows_then_merge(left_rows, &given.rows)
}
_ => Ok(None),
}
}
fn match_arg_when_left_is_matrix_set(
&mut self,
left_set: &Obj,
left_row_len: &Obj,
left_col_len: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::MatrixSet(ref given) => self.match_arg_ternary_then_merge(
left_set,
left_row_len,
left_col_len,
given.set.as_ref(),
given.row_len.as_ref(),
given.col_len.as_ref(),
),
_ => Ok(None),
}
}
fn match_arg_when_left_is_power_set(
&mut self,
left_set: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::PowerSet(ref given) => self
.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
left_set,
given.set.as_ref(),
),
_ => Ok(None),
}
}
fn match_arg_when_left_is_choose(
&mut self,
left_set: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::Choose(ref given) => self.match_arg_in_atomic_fact_in_known_forall_with_given_arg(
left_set,
given.set.as_ref(),
),
_ => Ok(None),
}
}
fn match_arg_when_left_is_obj_at_index(
&mut self,
left_obj: &Obj,
left_index: &Obj,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::ObjAtIndex(ref given) => self.match_arg_binary_then_merge(
left_obj,
left_index,
given.obj.as_ref(),
given.index.as_ref(),
),
_ => Ok(None),
}
}
fn match_arg_when_left_is_q_pos(
&mut self,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::StandardSet(StandardSet::QPos) => self.match_arg_same_type(given_arg),
_ => Ok(None),
}
}
fn match_arg_when_left_is_r_pos(
&mut self,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::StandardSet(StandardSet::RPos) => self.match_arg_same_type(given_arg),
_ => Ok(None),
}
}
fn match_arg_when_left_is_q_neg(
&mut self,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::StandardSet(StandardSet::QNeg) => self.match_arg_same_type(given_arg),
_ => Ok(None),
}
}
fn match_arg_when_left_is_z_neg(
&mut self,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::StandardSet(StandardSet::ZNeg) => self.match_arg_same_type(given_arg),
_ => Ok(None),
}
}
fn match_arg_when_left_is_r_neg(
&mut self,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::StandardSet(StandardSet::RNeg) => self.match_arg_same_type(given_arg),
_ => Ok(None),
}
}
fn match_arg_when_left_is_q_nz(
&mut self,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::StandardSet(StandardSet::QNz) => self.match_arg_same_type(given_arg),
_ => Ok(None),
}
}
fn match_arg_when_left_is_z_nz(
&mut self,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::StandardSet(StandardSet::ZNz) => self.match_arg_same_type(given_arg),
_ => Ok(None),
}
}
fn match_arg_when_left_is_r_nz(
&mut self,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
match given_arg {
Obj::StandardSet(StandardSet::RNz) => self.match_arg_same_type(given_arg),
_ => Ok(None),
}
}
fn match_arg_same_type(
&mut self,
given_arg: &Obj,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
let mut map = HashMap::new();
map.insert(given_arg.to_string(), given_arg.clone());
Ok(Some(map))
}
fn match_arg_type_not_implemented(
&mut self,
obj_type_name: &str,
) -> Result<Option<HashMap<String, Obj>>, RuntimeError> {
let _ = obj_type_name;
Ok(None)
}
}