use crate::prelude::*;
use std::collections::HashMap;
impl Runtime {
pub fn verify_restrict_fact_using_its_definition(
&mut self,
restrict_fact: &RestrictFact,
verify_state: &VerifyState,
) -> Result<Option<StmtResult>, RuntimeError> {
let function = &restrict_fact.obj;
let original_fn_set =
match self.get_cloned_object_in_fn_set(function) {
Some(fn_set) => fn_set,
None => {
return Err(RuntimeError::new_verify_error_with_fact_msg_position_previous_error(
Fact::AtomicFact(AtomicFact::RestrictFact(restrict_fact.clone())),
String::new(),
restrict_fact.line_file.clone(),
Some(RuntimeError::new_well_defined_error_with_msg_previous_error_position(
format!(
"function `{}` belongs to what function set is unknown",
function.to_string()
),
None,
default_line_file(),
)),
));
}
};
self.verify_restrict_to_fn_set_with_params_against_original_with_params(
restrict_fact,
&original_fn_set,
verify_state,
)
}
fn verify_restrict_to_fn_set_with_params_against_original_with_params(
&mut self,
restrict_fact: &RestrictFact,
original_fn_set: &FnSet,
verify_state: &VerifyState,
) -> Result<Option<StmtResult>, RuntimeError> {
let restrict_to_ref = match &restrict_fact.obj_can_restrict_to_fn_set {
Obj::FnSet(r) => r,
_ => return Ok(None),
};
let mut restrict_flat_param_names: Vec<String> = Vec::new();
for param_def_with_set in &restrict_to_ref.params_def_with_set {
for param_name in param_def_with_set.params.iter() {
restrict_flat_param_names.push(param_name.clone());
}
}
let mut original_flat_param_names: Vec<String> = Vec::new();
for param_def_with_set in &original_fn_set.params_def_with_set {
for param_name in param_def_with_set.params.iter() {
original_flat_param_names.push(param_name.clone());
}
}
if restrict_flat_param_names.len() != original_flat_param_names.len() {
return Ok(None);
}
let original_to_restrict_param_map = Self::build_original_to_restrict_param_map(
&original_flat_param_names,
&restrict_flat_param_names,
);
let mut forall_params: Vec<ParamGroupWithParamType> = Vec::new();
for param_def_with_set in &restrict_to_ref.params_def_with_set {
forall_params.push(ParamGroupWithParamType::new(
param_def_with_set.params.clone(),
ParamType::Obj(param_def_with_set.set.clone()),
));
}
let mut forall_dom_facts: Vec<ExistOrAndChainAtomicFact> = Vec::new();
for dom_fact in &restrict_to_ref.dom_facts {
forall_dom_facts.push(dom_fact.clone().to_exist_or_and_chain_atomic_fact());
}
let then_facts = Self::build_then_facts_for_original_with_params(
self,
original_fn_set,
&original_to_restrict_param_map,
&restrict_flat_param_names,
restrict_fact.line_file.clone(),
)
.map_err(|e| {
RuntimeError::new_verify_error_with_fact_msg_position_previous_error(
Fact::AtomicFact(AtomicFact::RestrictFact(restrict_fact.clone())),
String::new(),
restrict_fact.line_file.clone(),
Some(e),
)
})?;
self.verify_forall_and_return_restrict_success(
restrict_fact,
forall_params,
forall_dom_facts,
then_facts,
&(*restrict_to_ref.ret_set).clone(),
&(*original_fn_set.ret_set).clone(),
verify_state,
)
}
fn build_original_to_restrict_param_map(
original_flat_param_names: &Vec<String>,
restrict_flat_param_names: &Vec<String>,
) -> HashMap<String, Obj> {
let mut original_to_restrict_param_map: HashMap<String, Obj> = HashMap::new();
let mut mapping_index: usize = 0;
while mapping_index < original_flat_param_names.len() {
original_to_restrict_param_map.insert(
original_flat_param_names[mapping_index].clone(),
Obj::Identifier(Identifier::new(
restrict_flat_param_names[mapping_index].clone(),
)),
);
mapping_index += 1;
}
original_to_restrict_param_map
}
fn build_then_facts_for_original_with_params(
runtime: &Runtime,
original_fn_set: &FnSet,
original_to_restrict_param_map: &HashMap<String, Obj>,
restrict_flat_param_names: &Vec<String>,
line_file: LineFile,
) -> Result<Vec<ExistOrAndChainAtomicFact>, RuntimeError> {
let mut then_facts: Vec<ExistOrAndChainAtomicFact> = Vec::new();
let mut index: usize = 0;
for param_def_with_set in &original_fn_set.params_def_with_set {
let instantiated_original_set =
runtime.inst_obj(¶m_def_with_set.set, original_to_restrict_param_map)?;
for _param_name in param_def_with_set.params.iter() {
let restrict_param_name = restrict_flat_param_names[index].clone();
then_facts.push(ExistOrAndChainAtomicFact::AtomicFact(AtomicFact::InFact(
InFact::new(
Obj::Identifier(Identifier::new(restrict_param_name)),
instantiated_original_set.clone(),
line_file.clone(),
),
)));
index += 1;
}
}
for dom_fact in &original_fn_set.dom_facts {
let instantiated_dom_fact =
runtime.inst_or_and_chain_atomic_fact(dom_fact, original_to_restrict_param_map)?;
then_facts.push(instantiated_dom_fact.to_exist_or_and_chain_atomic_fact());
}
Ok(then_facts)
}
fn verify_forall_and_return_restrict_success(
&mut self,
restrict_fact: &RestrictFact,
forall_params: Vec<ParamGroupWithParamType>,
forall_dom_facts: Vec<ExistOrAndChainAtomicFact>,
then_facts: Vec<ExistOrAndChainAtomicFact>,
restrict_ret_set: &Obj,
original_ret_set: &Obj,
verify_state: &VerifyState,
) -> Result<Option<StmtResult>, RuntimeError> {
let params_in_original_sets_forall = ForallFact::new(
forall_params,
forall_dom_facts,
then_facts,
restrict_fact.line_file.clone(),
);
let forall_result =
self.verify_forall_fact(¶ms_in_original_sets_forall, verify_state)?;
if !forall_result.is_true() {
return Ok(None);
}
let ret_equal_fact = EqualFact::new(
restrict_ret_set.clone(),
original_ret_set.clone(),
restrict_fact.line_file.clone(),
);
let ret_equal_result = self.verify_equal_fact(&ret_equal_fact, verify_state)?;
if !ret_equal_result.is_true() {
return Ok(None);
}
Ok(Some(
(FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
Fact::AtomicFact(AtomicFact::RestrictFact(restrict_fact.clone())),
"restrict by definition (forall param sets narrower, same ret set)".to_string(),
Vec::new(),
))
.into(),
))
}
}