use crate::prelude::*;
use std::collections::HashMap;
fn fn_set_equality_fact(left: &FnSet, right: &FnSet, line_file: LineFile) -> Fact {
Fact::AtomicFact(AtomicFact::EqualFact(EqualFact::new(
Obj::FnSet(left.clone()),
Obj::FnSet(right.clone()),
line_file,
)))
}
fn fn_set_equality_verify_error(
left: &FnSet,
right: &FnSet,
line_file: LineFile,
message: String,
cause: Option<RuntimeError>,
) -> RuntimeError {
RuntimeError::new_verify_error_with_fact_msg_position_previous_error(
fn_set_equality_fact(left, right, line_file.clone()),
message,
line_file,
cause,
)
}
fn fn_set_equality_verified_by_builtin_rules_result(
left: &FnSet,
right: &FnSet,
line_file: LineFile,
) -> StmtResult {
let stmt = fn_set_equality_fact(left, right, line_file);
StmtResult::FactualStmtSuccess(
FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
stmt,
"fnset equality: mutual implication of param sets, dom facts, and ret set".to_string(),
Vec::new(),
),
)
}
impl Runtime {
pub(crate) fn verify_fn_set_with_params_equality_by_builtin_rules(
&mut self,
left: &FnSet,
right: &FnSet,
line_file: LineFile,
verify_state: &VerifyState,
) -> Result<StmtResult, RuntimeError> {
if ParamGroupWithSet::number_of_params(&left.params_def_with_set)
!= ParamGroupWithSet::number_of_params(&right.params_def_with_set)
{
return Ok((StmtUnknown::new()).into());
}
let left_implies_right = self.verify_fn_set_with_params_directionally_in_local_env(
left,
right,
line_file.clone(),
verify_state,
)?;
if !left_implies_right {
return Ok((StmtUnknown::new()).into());
}
let right_implies_left = self.verify_fn_set_with_params_directionally_in_local_env(
right,
left,
line_file.clone(),
verify_state,
)?;
if !right_implies_left {
return Ok((StmtUnknown::new()).into());
}
Ok(fn_set_equality_verified_by_builtin_rules_result(
left, right, line_file,
))
}
fn verify_fn_set_with_params_directionally_in_local_env(
&mut self,
source: &FnSet,
target: &FnSet,
line_file: LineFile,
verify_state: &VerifyState,
) -> Result<bool, RuntimeError> {
self.run_in_local_env(|rt| {
rt.verify_fn_set_with_params_directionally_in_local_env_body(
source,
target,
line_file,
verify_state,
)
})
}
fn verify_fn_set_with_params_directionally_in_local_env_body(
&mut self,
source: &FnSet,
target: &FnSet,
line_file: LineFile,
verify_state: &VerifyState,
) -> Result<bool, RuntimeError> {
let target_flat_param_names =
ParamGroupWithSet::collect_param_names(&target.params_def_with_set);
let generated_param_names =
self.generate_random_unused_names(target_flat_param_names.len());
let source_param_to_generated_arg_map = self
.define_directional_source_fn_set_params_in_local_env(
source,
&generated_param_names,
target,
line_file.clone(),
)?;
let target_param_to_generated_arg_map = Self::build_param_to_generated_arg_map(
&target_flat_param_names,
&generated_param_names,
);
self.assume_directional_source_fn_set_dom_facts_in_local_env(
source,
&source_param_to_generated_arg_map,
target,
line_file.clone(),
)?;
if !self.verify_directional_target_fn_set_param_membership_facts(
source,
target,
&target_param_to_generated_arg_map,
line_file.clone(),
verify_state,
)? {
return Ok(false);
}
if !self.verify_directional_target_fn_set_dom_facts(
source,
target,
line_file.clone(),
&target_param_to_generated_arg_map,
verify_state,
)? {
return Ok(false);
}
let source_ret_set = self
.inst_obj(&source.ret_set, &source_param_to_generated_arg_map)
.map_err(|e| {
fn_set_equality_verify_error(
source,
target,
line_file.clone(),
"failed to instantiate source ret set for fnset equality check".to_string(),
Some(e),
)
})?;
let target_ret_set = self
.inst_obj(&target.ret_set, &target_param_to_generated_arg_map)
.map_err(|e| {
fn_set_equality_verify_error(
source,
target,
line_file.clone(),
"failed to instantiate target ret set for fnset equality check".to_string(),
Some(e),
)
})?;
let ret_equal_fact = EqualFact::new(source_ret_set, target_ret_set, line_file);
let ret_equal_result = self.verify_equal_fact(&ret_equal_fact, verify_state)?;
Ok(ret_equal_result.is_true())
}
fn build_param_to_generated_arg_map(
flat_param_names: &[String],
generated_param_names: &[String],
) -> HashMap<String, Obj> {
let mut param_to_generated_arg_map: HashMap<String, Obj> =
HashMap::with_capacity(flat_param_names.len());
for (param_name, generated_param_name) in
flat_param_names.iter().zip(generated_param_names.iter())
{
param_to_generated_arg_map.insert(
param_name.clone(),
Obj::Identifier(Identifier::new(generated_param_name.clone())),
);
}
param_to_generated_arg_map
}
fn define_directional_source_fn_set_params_in_local_env(
&mut self,
source: &FnSet,
generated_param_names: &[String],
target: &FnSet,
line_file: LineFile,
) -> Result<HashMap<String, Obj>, RuntimeError> {
let mut source_param_to_generated_arg_map: HashMap<String, Obj> =
HashMap::with_capacity(generated_param_names.len());
let mut flat_index: usize = 0;
for param_def_with_set in source.params_def_with_set.iter() {
let next_flat_index = flat_index + param_def_with_set.params.len();
let generated_names_for_current_group =
generated_param_names[flat_index..next_flat_index].to_vec();
let instantiated_param_set = self
.inst_obj(¶m_def_with_set.set, &source_param_to_generated_arg_map)
.map_err(|e| {
fn_set_equality_verify_error(
source,
target,
line_file.clone(),
"failed to instantiate source fnset param set".to_string(),
Some(e),
)
})?;
let generated_param_def = ParamGroupWithSet::new(
generated_names_for_current_group.clone(),
instantiated_param_set,
);
self.define_params_with_set(&generated_param_def)
.map_err(|e| {
fn_set_equality_verify_error(
source,
target,
line_file.clone(),
"failed to define fresh params for directional fnset equality verification"
.to_string(),
Some(e),
)
})?;
for (source_param_name, generated_param_name) in param_def_with_set
.params
.iter()
.zip(generated_names_for_current_group.iter())
{
source_param_to_generated_arg_map.insert(
source_param_name.clone(),
Obj::Identifier(Identifier::new(generated_param_name.clone())),
);
}
flat_index = next_flat_index;
}
Ok(source_param_to_generated_arg_map)
}
fn assume_directional_source_fn_set_dom_facts_in_local_env(
&mut self,
source: &FnSet,
source_param_to_generated_arg_map: &HashMap<String, Obj>,
target: &FnSet,
line_file: LineFile,
) -> Result<(), RuntimeError> {
for dom_fact in source.dom_facts.iter() {
let instantiated_dom_fact = self
.inst_or_and_chain_atomic_fact(dom_fact, source_param_to_generated_arg_map)
.map_err(|e| {
fn_set_equality_verify_error(
source,
target,
line_file.clone(),
"failed to instantiate source fnset dom fact".to_string(),
Some(e),
)
})?;
self.store_exist_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(
instantiated_dom_fact.to_exist_or_and_chain_atomic_fact(),
)
.map_err(|e| {
fn_set_equality_verify_error(
source,
target,
line_file.clone(),
"failed to assume source fnset dom fact in local equality environment"
.to_string(),
Some(e.into()),
)
})?;
}
Ok(())
}
fn verify_directional_target_fn_set_param_membership_facts(
&mut self,
source: &FnSet,
target: &FnSet,
target_param_to_generated_arg_map: &HashMap<String, Obj>,
line_file: LineFile,
verify_state: &VerifyState,
) -> Result<bool, RuntimeError> {
for param_def_with_set in target.params_def_with_set.iter() {
let instantiated_param_set = self
.inst_obj(¶m_def_with_set.set, target_param_to_generated_arg_map)
.map_err(|e| {
fn_set_equality_verify_error(
source,
target,
line_file.clone(),
"failed to instantiate target fnset param set".to_string(),
Some(e),
)
})?;
for param_name in param_def_with_set.params.iter() {
let Some(generated_param_obj) =
target_param_to_generated_arg_map.get(param_name).cloned()
else {
return Err(fn_set_equality_verify_error(
source,
target,
line_file.clone(),
"internal error: missing generated param while verifying fnset equality"
.to_string(),
None,
));
};
let param_in_target_set_fact = AtomicFact::InFact(InFact::new(
generated_param_obj,
instantiated_param_set.clone(),
line_file.clone(),
));
let verify_result =
self.verify_atomic_fact(¶m_in_target_set_fact, verify_state)?;
if !verify_result.is_true() {
return Ok(false);
}
}
}
Ok(true)
}
fn verify_directional_target_fn_set_dom_facts(
&mut self,
source: &FnSet,
target: &FnSet,
line_file: LineFile,
target_param_to_generated_arg_map: &HashMap<String, Obj>,
verify_state: &VerifyState,
) -> Result<bool, RuntimeError> {
for dom_fact in target.dom_facts.iter() {
let instantiated_dom_fact = self
.inst_or_and_chain_atomic_fact(dom_fact, target_param_to_generated_arg_map)
.map_err(|e| {
fn_set_equality_verify_error(
source,
target,
line_file.clone(),
"failed to instantiate target fnset dom fact".to_string(),
Some(e),
)
})?;
let verify_result =
self.verify_or_and_chain_atomic_fact(&instantiated_dom_fact, verify_state)?;
if !verify_result.is_true() {
return Ok(false);
}
}
Ok(true)
}
}