use crate::prelude::*;
use std::collections::HashMap;
fn param_defs_with_type_from_have_fn_clause(clause: &FnSetClause) -> Vec<ParamGroupWithParamType> {
let mut param_defs_with_type: Vec<ParamGroupWithParamType> =
Vec::with_capacity(clause.params_def_with_set.len());
for param_def_with_set in clause.params_def_with_set.iter() {
param_defs_with_type.push(ParamGroupWithParamType::new(
param_def_with_set.params.clone(),
ParamType::Obj(param_def_with_set.set.clone()),
));
}
param_defs_with_type
}
impl Runtime {
fn build_function_obj_with_param_names(
&self,
function_name: &str,
param_names: &[String],
) -> Obj {
let mut function_args: Vec<Box<Obj>> = Vec::with_capacity(param_names.len());
for param_name in param_names.iter() {
function_args.push(Box::new(Obj::Identifier(Identifier::new(
param_name.clone(),
))));
}
let fn_head_atom = Atom::Identifier(Identifier::new(function_name.to_string()));
let fn_body_groups = vec![function_args];
Obj::FnObj(FnObj::new(fn_head_atom, fn_body_groups))
}
pub fn exec_def_prop_stmt(
&mut self,
def_prop_stmt: &DefPropStmt,
) -> Result<StmtResult, RuntimeErrorStruct> {
self.run_in_local_env(|rt| rt.def_prop_stmt_check_well_defined(def_prop_stmt))
.map_err(|e| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
def_prop_stmt.clone().into(),
"".to_string(),
Some(e.into()),
vec![],
)
})?;
self.store_def_prop(def_prop_stmt)?;
Ok((NonFactualStmtSuccess::new(
def_prop_stmt.clone().into(),
InferResult::new(),
vec![],
)).into())
}
fn def_prop_stmt_check_well_defined(
&mut self,
def_prop_stmt: &DefPropStmt,
) -> Result<(), RuntimeErrorStruct> {
self.define_params_with_type(&def_prop_stmt.params_def_with_type, false)
.map_err(|e| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
def_prop_stmt.clone().into(),
"".to_string(),
Some(e.into()),
vec![],
)
})?;
for fact in def_prop_stmt.iff_facts.iter() {
self.verify_fact_well_defined_and_store_and_infer(
fact.clone(),
&VerifyState::new(0, false),
)
.map_err(|inner_exec_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
def_prop_stmt.clone().into(),
"".to_string(),
Some(RuntimeError::from(inner_exec_error)),
vec![],
)
})?;
}
Ok(())
}
pub fn exec_def_abstract_prop_stmt(
&mut self,
def_abstract_prop_stmt: &DefAbstractPropStmt,
) -> Result<StmtResult, RuntimeErrorStruct> {
self.store_def_abstract_prop(def_abstract_prop_stmt)
.map_err(|e| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
def_abstract_prop_stmt.clone().into(),
"".to_string(),
Some(e.into()),
vec![],
)
})?;
Ok((NonFactualStmtSuccess::new(
def_abstract_prop_stmt.clone().into(),
InferResult::new(),
vec![],
)).into())
}
pub fn exec_let_stmt(
&mut self,
def_let_stmt: &DefLetStmt,
) -> Result<StmtResult, RuntimeErrorStruct> {
let mut infer_result = self
.define_params_with_type(&def_let_stmt.param_def, false)
.map_err(|e| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
def_let_stmt.clone().into(),
"".to_string(),
Some(e.into()),
vec![],
)
})?;
for fact in def_let_stmt.facts.iter() {
let fact_infer_result = self
.verify_fact_well_defined_and_store_and_infer(
fact.clone(),
&VerifyState::new(0, false),
)
.map_err(|inner_exec_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
def_let_stmt.clone().into(),
"".to_string(),
Some(RuntimeError::from(inner_exec_error)),
vec![],
)
})?;
infer_result.new_infer_result_inside(fact_infer_result);
infer_result.new_fact(fact);
}
Ok((NonFactualStmtSuccess::new(
def_let_stmt.clone().into(),
infer_result,
vec![],
)).into())
}
pub fn exec_have_obj_in_nonempty_set_or_param_type_stmt(
&mut self,
stmt: &HaveObjInNonemptySetOrParamTypeStmt,
) -> Result<StmtResult, RuntimeErrorStruct> {
let infer_result = self
.define_params_with_type(&stmt.param_def, true)
.map_err(|define_params_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
stmt.clone().into(),
"".to_string(),
Some(define_params_error),
vec![],
)
})?;
Ok((NonFactualStmtSuccess::new(
stmt.clone().into(),
infer_result,
vec![],
)).into())
}
pub fn define_params_with_set(
&mut self,
param_def: &ParamGroupWithSet,
) -> Result<InferResult, RuntimeError> {
self.verify_obj_well_defined_and_store_cache(¶m_def.set, &VerifyState::new(0, false))
.map_err(|well_defined_error| {
let param_names_text = param_def.params.join(", ");
let error_line_file = well_defined_error.line_file().clone();
RuntimeError::new_define_params_error_with_msg_previous_error_position(
format!(
"define params with set: failed to verify set well-defined for params [{}] with set {}",
param_names_text, param_def.set
),
Some(well_defined_error.into()),
error_line_file,
)
})?;
let mut infer_result = InferResult::new();
let facts = param_def.facts();
for (name, fact) in param_def.params.iter().zip(facts.iter()) {
self.store_identifier_obj(name).map_err(|runtime_error| {
RuntimeError::new_define_params_error_with_msg_previous_error_position(
format!(
"define params with set: failed to declare parameter `{}`",
name
),
Some(RuntimeError::from(runtime_error)),
default_line_file(),
)
})?;
let fact_infer_result = self
.store_fact_without_well_defined_verified_and_infer(fact.clone())
.map_err(|store_fact_error| {
RuntimeError::new_define_params_error_with_msg_previous_error_position(
format!(
"define params with set: failed to store in-set fact for parameter `{}`",
name
),
Some(store_fact_error.into()),
default_line_file(),
)
})?;
infer_result.new_infer_result_inside(fact_infer_result);
}
Ok(infer_result)
}
pub fn exec_have_obj_equal_stmt(
&mut self,
have_obj_equal_stmt: &HaveObjEqualStmt,
) -> Result<StmtResult, RuntimeErrorStruct> {
if ParamGroupWithParamType::number_of_params(&have_obj_equal_stmt.param_def)
!= have_obj_equal_stmt.objs_equal_to.len()
{
return Err(RuntimeErrorStruct::exec_stmt_with_message_and_cause(
have_obj_equal_stmt.clone().into(),
"have_obj_equal_stmt: number of params in param_def does not match number of objs_equal_to".to_string(),
None,
vec![],
));
}
let mut current_index = 0;
let mut param_to_obj_map: HashMap<String, Obj> = HashMap::new();
for param_def in have_obj_equal_stmt.param_def.iter() {
let current_type_holder = self
.inst_param_type(¶m_def.param_type, ¶m_to_obj_map)
.map_err(|runtime_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
have_obj_equal_stmt.clone().into(),
"".to_string(),
Some(runtime_error),
vec![],
)
})?;
let current_type = ¤t_type_holder;
for name in param_def.params.iter() {
let current_param_equal_to = &have_obj_equal_stmt.objs_equal_to[current_index];
let verify_result = self
.verify_obj_satisfies_param_type(
current_param_equal_to.clone(),
current_type,
&VerifyState::new(0, false),
)
.map_err(|verify_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
have_obj_equal_stmt.clone().into(),
"".to_string(),
Some(verify_error.into()),
vec![],
)
})?;
if verify_result.is_unknown() {
let msg = format!(
"have_obj_equal_stmt: {} is not in type {}",
current_param_equal_to, current_type
);
return Err(RuntimeErrorStruct::exec_stmt_with_message_and_cause(
have_obj_equal_stmt.clone().into(),
msg,
None,
vec![],
));
}
param_to_obj_map.insert(name.clone(), current_param_equal_to.clone());
current_index += 1;
}
}
let mut infer_result = InferResult::new();
let param_infer_result = self
.define_params_with_type(&have_obj_equal_stmt.param_def, true)
.map_err(|define_params_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
have_obj_equal_stmt.clone().into(),
"".to_string(),
Some(define_params_error),
vec![],
)
})?;
infer_result.new_infer_result_inside(param_infer_result);
for (name, obj) in ParamType::get_all_param_names(&have_obj_equal_stmt.param_def)
.iter()
.zip(have_obj_equal_stmt.objs_equal_to.iter())
{
let equal_to_fact = AtomicFact::EqualFact(EqualFact::new(
Obj::Identifier(Identifier::new(name.clone())),
obj.clone(),
have_obj_equal_stmt.line_file.clone(),
));
let equal_to_fact_infer_result = self
.store_atomic_fact_without_well_defined_verified_and_infer(equal_to_fact)
.map_err(|store_fact_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
have_obj_equal_stmt.clone().into(),
"".to_string(),
Some(store_fact_error.into()),
vec![],
)
})?;
infer_result.new_infer_result_inside(equal_to_fact_infer_result);
}
return Ok((NonFactualStmtSuccess::new(
have_obj_equal_stmt.clone().into(),
infer_result,
vec![],
)).into());
}
pub fn exec_have_exist_obj_stmt(
&mut self,
have_exist_obj_stmt: &HaveByExistStmt,
) -> Result<StmtResult, RuntimeErrorStruct> {
let exist_fact_in_have_obj_stmt = &have_exist_obj_stmt.exist_fact_in_have_obj_st;
let verify_state = VerifyState::new(0, false);
let result = self
.verify_exist_fact(exist_fact_in_have_obj_stmt, &verify_state)
.map_err(|verify_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
have_exist_obj_stmt.clone().into(),
"".to_string(),
Some(verify_error.into()),
vec![],
)
})?;
if result.is_unknown() {
return Err(RuntimeErrorStruct::exec_stmt_with_message_and_cause(
have_exist_obj_stmt.clone().into(),
"have_exist_obj_stmt: exist fact is not verified".to_string(),
None,
vec![],
));
}
if ParamGroupWithParamType::number_of_params(
&exist_fact_in_have_obj_stmt.params_def_with_type,
) != have_exist_obj_stmt.equal_tos.len()
{
return Err(RuntimeErrorStruct::exec_stmt_with_message_and_cause(
have_exist_obj_stmt.clone().into(),
"have_exist_obj_stmt: number of params in exist does not match number of given objs".to_string(),
None,
vec![],
));
}
for obj in have_exist_obj_stmt.equal_tos.iter() {
self.store_identifier_obj(obj)?;
}
let new_obj_names_as_identifier_objs = have_exist_obj_stmt
.equal_tos
.iter()
.map(|s| Obj::Identifier(Identifier::new(s.clone())))
.collect();
let mut infer_result = self
.store_args_satisfy_param_type_when_not_defining_new_identifiers(
&exist_fact_in_have_obj_stmt.params_def_with_type,
&new_obj_names_as_identifier_objs,
have_exist_obj_stmt.line_file.clone(),
)
.map_err(|e| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
have_exist_obj_stmt.clone().into(),
"".to_string(),
Some(e),
vec![],
)
})?;
let param_to_obj_map = ParamGroupWithParamType::param_defs_and_args_to_param_to_arg_map(
&exist_fact_in_have_obj_stmt.params_def_with_type,
&new_obj_names_as_identifier_objs,
);
for fact in exist_fact_in_have_obj_stmt.facts.iter() {
let instantiated_fact = self
.inst_or_and_chain_atomic_fact(fact, ¶m_to_obj_map)
.map_err(|runtime_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
have_exist_obj_stmt.clone().into(),
"".to_string(),
Some(runtime_error),
vec![],
)
})?
.to_fact();
let fact_infer_result = self
.store_fact_without_well_defined_verified_and_infer(instantiated_fact)
.map_err(|store_fact_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
have_exist_obj_stmt.clone().into(),
"".to_string(),
Some(store_fact_error.into()),
vec![],
)
})?;
infer_result.new_infer_result_inside(fact_infer_result);
}
Ok((NonFactualStmtSuccess::new(
have_exist_obj_stmt.clone().into(),
infer_result,
vec![],
)).into())
}
pub fn exec_have_fn_equal_stmt(
&mut self,
have_fn_equal_stmt: &HaveFnEqualStmt,
) -> Result<StmtResult, RuntimeErrorStruct> {
let fn_set_stored = self
.add_mangled_prefix_to_fn_set_clause(
&have_fn_equal_stmt.fn_set_clause,
have_fn_equal_stmt.line_file.clone(),
)
.map_err(|e| {
RuntimeErrorStruct::exec_stmt_with_message_and_cause(
have_fn_equal_stmt.clone().into(),
"have_fn_equal_stmt: build fn set for storage failed".to_string(),
Some(e.into()),
vec![],
)
})?;
self.have_fn_equal_stmt_verify_well_defined(have_fn_equal_stmt, &fn_set_stored)
.map_err(|e| {
RuntimeErrorStruct::exec_stmt_with_message_and_cause(
have_fn_equal_stmt.clone().into(),
"have_fn_equal_stmt: verify well-defined failed".to_string(),
Some(e.into()),
vec![],
)
})?;
self.store_identifier_obj(&have_fn_equal_stmt.name)?;
let function_identifier_obj =
Obj::Identifier(Identifier::new(have_fn_equal_stmt.name.clone()));
let function_set_obj = Obj::FnSet(fn_set_stored.clone());
let function_in_function_set_fact = Fact::AtomicFact(AtomicFact::InFact(InFact::new(
function_identifier_obj,
function_set_obj,
have_fn_equal_stmt.line_file.clone(),
)));
let mut infer_result = self
.store_fact_without_well_defined_verified_and_infer(function_in_function_set_fact)
.map_err(|store_fact_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
have_fn_equal_stmt.clone().into(),
"".to_string(),
Some(store_fact_error.into()),
vec![],
)
})?;
let param_defs_with_type =
param_defs_with_type_from_have_fn_clause(&have_fn_equal_stmt.fn_set_clause);
let param_names = ParamGroupWithSet::collect_param_names(
&have_fn_equal_stmt.fn_set_clause.params_def_with_set,
);
let function_obj =
self.build_function_obj_with_param_names(&have_fn_equal_stmt.name, ¶m_names);
let function_equals_equal_to_fact = AtomicFact::EqualFact(EqualFact::new(
function_obj,
have_fn_equal_stmt.equal_to.clone(),
have_fn_equal_stmt.line_file.clone(),
));
let mut forall_dom_facts: Vec<ExistOrAndChainAtomicFact> =
Vec::with_capacity(have_fn_equal_stmt.fn_set_clause.dom_facts.len());
for dom_fact in have_fn_equal_stmt.fn_set_clause.dom_facts.iter() {
forall_dom_facts.push(dom_fact.clone().to_exist_or_and_chain_atomic_fact());
}
let forall_fact = ForallFact::new(
param_defs_with_type,
forall_dom_facts,
vec![crate::fact::ExistOrAndChainAtomicFact::AtomicFact(
function_equals_equal_to_fact,
)],
have_fn_equal_stmt.line_file.clone(),
);
let forall_as_fact = Fact::ForallFact(forall_fact);
let forall_infer_result = self
.store_fact_without_well_defined_verified_and_infer(forall_as_fact)
.map_err(|store_fact_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
have_fn_equal_stmt.clone().into(),
"".to_string(),
Some(store_fact_error.into()),
vec![],
)
})?;
infer_result.new_infer_result_inside(forall_infer_result);
Ok((NonFactualStmtSuccess::new(
have_fn_equal_stmt.clone().into(),
infer_result,
vec![],
)).into())
}
fn have_fn_equal_stmt_verify_well_defined(
&mut self,
have_fn_equal_stmt: &HaveFnEqualStmt,
fn_set_stored: &FnSet,
) -> Result<(), RuntimeErrorStruct> {
self.run_in_local_env(|rt| {
rt.have_fn_equal_stmt_verify_well_defined_body(have_fn_equal_stmt, fn_set_stored)
})
}
fn have_fn_equal_stmt_verify_well_defined_body(
&mut self,
have_fn_equal_stmt: &HaveFnEqualStmt,
fn_set_stored: &FnSet,
) -> Result<(), RuntimeErrorStruct> {
let verify_state = VerifyState::new(0, false);
let function_set_obj = Obj::FnSet(fn_set_stored.clone());
self.verify_obj_well_defined_and_store_cache(&function_set_obj, &verify_state)
.map_err(|well_defined_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
have_fn_equal_stmt.clone().into(),
"".to_string(),
Some(well_defined_error.into()),
vec![],
)
})?;
for param_def_with_set in have_fn_equal_stmt.fn_set_clause.params_def_with_set.iter() {
self.define_params_with_set(param_def_with_set)
.map_err(|define_params_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
have_fn_equal_stmt.clone().into(),
"".to_string(),
Some(define_params_error),
vec![],
)
})?;
}
for dom_fact in have_fn_equal_stmt.fn_set_clause.dom_facts.iter() {
let _ = self
.store_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(
dom_fact.clone(),
)
.map_err(|store_fact_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
have_fn_equal_stmt.clone().into(),
"".to_string(),
Some(store_fact_error.into()),
vec![],
)
})?;
}
let equal_to_in_ret_set_atomic_fact = AtomicFact::InFact(InFact::new(
have_fn_equal_stmt.equal_to.clone(),
have_fn_equal_stmt.fn_set_clause.ret_set.clone(),
have_fn_equal_stmt.line_file.clone(),
));
let verify_result = self
.verify_atomic_fact(&equal_to_in_ret_set_atomic_fact, &verify_state)
.map_err(|verify_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
have_fn_equal_stmt.clone().into(),
"".to_string(),
Some(verify_error.into()),
vec![],
)
})?;
if verify_result.is_unknown() {
let msg = format!(
"have_fn_equal_stmt: {} is not in return set {}",
have_fn_equal_stmt.equal_to, have_fn_equal_stmt.fn_set_clause.ret_set
);
return Err(RuntimeErrorStruct::exec_stmt_with_message_and_cause(
have_fn_equal_stmt.clone().into(),
msg,
None,
vec![],
));
}
Ok(())
}
pub fn exec_have_fn_equal_case_by_case_stmt(
&mut self,
have_fn_equal_case_by_case_stmt: &HaveFnEqualCaseByCaseStmt,
) -> Result<StmtResult, RuntimeErrorStruct> {
let fn_set_stored = self
.add_mangled_prefix_to_fn_set_clause(
&have_fn_equal_case_by_case_stmt.fn_set_clause,
have_fn_equal_case_by_case_stmt.line_file.clone(),
)
.map_err(|e| {
RuntimeErrorStruct::exec_stmt_with_message_and_cause(
have_fn_equal_case_by_case_stmt.clone().into(),
"have_fn_equal_case_by_case_stmt: build fn set for storage failed".to_string(),
Some(e.into()),
vec![],
)
})?;
self.verify_have_fn_equal_case_by_case_stmt(
have_fn_equal_case_by_case_stmt,
&fn_set_stored,
)
.map_err(|e| {
RuntimeErrorStruct::exec_stmt_with_message_and_cause(
have_fn_equal_case_by_case_stmt.clone().into(),
"have_fn_equal_case_by_case_stmt: verify well-defined failed".to_string(),
Some(e.into()),
vec![],
)
})?;
let infer_result =
self.store_have_fn_equal_case_by_case(have_fn_equal_case_by_case_stmt, &fn_set_stored)?;
Ok((NonFactualStmtSuccess::new(
have_fn_equal_case_by_case_stmt.clone().into(),
infer_result,
vec![],
)).into())
}
fn store_have_fn_equal_case_by_case(
&mut self,
have_fn_equal_case_by_case_stmt: &HaveFnEqualCaseByCaseStmt,
fn_set_stored: &FnSet,
) -> Result<InferResult, RuntimeErrorStruct> {
self.store_identifier_obj(&have_fn_equal_case_by_case_stmt.name)?;
let function_identifier_obj = Obj::Identifier(Identifier::new(
have_fn_equal_case_by_case_stmt.name.clone(),
));
let function_set_obj = Obj::FnSet(fn_set_stored.clone());
let function_in_function_set_fact = Fact::AtomicFact(AtomicFact::InFact(InFact::new(
function_identifier_obj,
function_set_obj,
have_fn_equal_case_by_case_stmt.line_file.clone(),
)));
let mut infer_result = self
.store_fact_without_well_defined_verified_and_infer(function_in_function_set_fact)
.map_err(|store_fact_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
have_fn_equal_case_by_case_stmt.clone().into(),
"".to_string(),
Some(store_fact_error.into()),
vec![],
)
})?;
let param_defs_with_type = param_defs_with_type_from_have_fn_clause(
&have_fn_equal_case_by_case_stmt.fn_set_clause,
);
let param_names = ParamGroupWithSet::collect_param_names(
&have_fn_equal_case_by_case_stmt
.fn_set_clause
.params_def_with_set,
);
let function_obj = self.build_function_obj_with_param_names(
&have_fn_equal_case_by_case_stmt.name,
¶m_names,
);
for case_index in 0..have_fn_equal_case_by_case_stmt.cases.len() {
let case_fact = &have_fn_equal_case_by_case_stmt.cases[case_index];
let equal_to = &have_fn_equal_case_by_case_stmt.equal_tos[case_index];
let mut forall_dom_facts: Vec<ExistOrAndChainAtomicFact> = Vec::with_capacity(
have_fn_equal_case_by_case_stmt
.fn_set_clause
.dom_facts
.len()
+ 1,
);
for dom_fact in have_fn_equal_case_by_case_stmt
.fn_set_clause
.dom_facts
.iter()
{
forall_dom_facts.push(dom_fact.clone().to_exist_or_and_chain_atomic_fact());
}
forall_dom_facts.push(case_fact.to_exist_or_and_chain_atomic_fact());
let function_equals_equal_to_fact = AtomicFact::EqualFact(EqualFact::new(
function_obj.clone(),
equal_to.clone(),
have_fn_equal_case_by_case_stmt.line_file.clone(),
));
let forall_fact = ForallFact::new(
param_defs_with_type.clone(),
forall_dom_facts,
vec![ExistOrAndChainAtomicFact::AtomicFact(
function_equals_equal_to_fact,
)],
have_fn_equal_case_by_case_stmt.line_file.clone(),
);
let forall_as_fact = Fact::ForallFact(forall_fact);
infer_result.new_fact(&forall_as_fact);
let forall_infer_result = self
.store_fact_without_well_defined_verified_and_infer(forall_as_fact)
.map_err(|store_fact_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
have_fn_equal_case_by_case_stmt.clone().into(),
"".to_string(),
Some(store_fact_error.into()),
vec![],
)
})?;
infer_result.new_infer_result_inside(forall_infer_result);
}
Ok(infer_result)
}
pub fn exec_have_fn_by_induc_stmt(
&mut self,
stmt: &HaveFnByInducStmt,
) -> Result<StmtResult, RuntimeErrorStruct> {
self.exec_have_fn_by_induc(stmt)
.map_err(|e| e.into_struct())
}
fn verify_have_fn_equal_case_by_case_stmt(
&mut self,
have_fn_equal_case_by_case_stmt: &HaveFnEqualCaseByCaseStmt,
fn_set_stored: &FnSet,
) -> Result<(), RuntimeErrorStruct> {
if have_fn_equal_case_by_case_stmt.cases.len()
!= have_fn_equal_case_by_case_stmt.equal_tos.len()
{
return Err(RuntimeErrorStruct::exec_stmt_with_message_and_cause(
have_fn_equal_case_by_case_stmt.clone().into(),
"have_fn_equal_case_by_case_stmt: number of cases does not match number of equal_tos".to_string(),
None,
vec![],
));
}
let function_set_obj = Obj::FnSet(fn_set_stored.clone());
self.verify_obj_well_defined_and_store_cache(
&function_set_obj,
&VerifyState::new(0, false),
)
.map_err(|well_defined_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
have_fn_equal_case_by_case_stmt.clone().into(),
"".to_string(),
Some(well_defined_error.into()),
vec![],
)
})?;
for case_index in 0..have_fn_equal_case_by_case_stmt.cases.len() {
let case_fact = &have_fn_equal_case_by_case_stmt.cases[case_index];
let equal_to = &have_fn_equal_case_by_case_stmt.equal_tos[case_index];
self.run_in_local_env(|rt| {
rt.have_fn_equal_case_by_case_stmt_verify_well_defined_body_for_one_case(
have_fn_equal_case_by_case_stmt,
case_fact,
equal_to,
)
})?;
}
Ok(())
}
fn have_fn_equal_case_by_case_stmt_verify_well_defined_body_for_one_case(
&mut self,
have_fn_equal_case_by_case_stmt: &HaveFnEqualCaseByCaseStmt,
case_fact: &AndChainAtomicFact,
equal_to: &Obj,
) -> Result<(), RuntimeErrorStruct> {
let verify_state = VerifyState::new(0, false);
let case_fact_as_fact = case_fact.to_fact();
for param_def_with_set in have_fn_equal_case_by_case_stmt
.fn_set_clause
.params_def_with_set
.iter()
{
self.define_params_with_set(param_def_with_set)
.map_err(|define_params_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
have_fn_equal_case_by_case_stmt.clone().into(),
"".to_string(),
Some(define_params_error),
vec![],
)
})?;
}
for dom_fact in have_fn_equal_case_by_case_stmt
.fn_set_clause
.dom_facts
.iter()
{
let _ = self
.store_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(
dom_fact.clone(),
)
.map_err(|store_fact_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
have_fn_equal_case_by_case_stmt.clone().into(),
"".to_string(),
Some(store_fact_error.into()),
vec![],
)
})?;
}
let _ = self
.store_fact_without_well_defined_verified_and_infer(case_fact_as_fact)
.map_err(|store_fact_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
have_fn_equal_case_by_case_stmt.clone().into(),
"".to_string(),
Some(store_fact_error.into()),
vec![],
)
})?;
self.verify_obj_well_defined_and_store_cache(equal_to, &verify_state)
.map_err(|well_defined_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
have_fn_equal_case_by_case_stmt.clone().into(),
"".to_string(),
Some(well_defined_error.into()),
vec![],
)
})?;
let equal_to_in_ret_set_atomic_fact = AtomicFact::InFact(InFact::new(
equal_to.clone(),
have_fn_equal_case_by_case_stmt
.fn_set_clause
.ret_set
.clone(),
have_fn_equal_case_by_case_stmt.line_file.clone(),
));
let verify_result = self
.verify_atomic_fact(&equal_to_in_ret_set_atomic_fact, &verify_state)
.map_err(|verify_error| {
RuntimeErrorStruct::exec_stmt_new_with_stmt(
have_fn_equal_case_by_case_stmt.clone().into(),
"".to_string(),
Some(verify_error.into()),
vec![],
)
})?;
if verify_result.is_unknown() {
let msg = format!(
"have_fn_equal_case_by_case_stmt: {} is not in return set {} under case {}",
equal_to, have_fn_equal_case_by_case_stmt.fn_set_clause.ret_set, case_fact,
);
return Err(RuntimeErrorStruct::exec_stmt_with_message_and_cause(
have_fn_equal_case_by_case_stmt.clone().into(),
msg,
None,
vec![],
));
}
Ok(())
}
}