use crate::prelude::*;
use std::collections::HashMap;
impl Runtime {
pub fn exec_have_fn_by_induc(
&mut self,
stmt: &HaveFnByInducStmt,
) -> Result<StmtResult, RuntimeError> {
self.run_in_local_env(|rt| rt.exec_have_fn_by_induc_verify_process(stmt))?;
let flat = stmt.to_have_fn_equal_case_by_case_stmt();
let fn_set_stored = self
.fn_set_from_fn_set_clause(&flat.fn_set_clause)
.map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
let infer_result = self
.store_have_fn_equal_case_by_case_stmt_facts(&flat, &fn_set_stored)
.map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
Ok((NonFactualStmtSuccess::new(stmt.clone().into(), infer_result, vec![])).into())
}
fn have_fn_by_induc_err(stmt: &HaveFnByInducStmt, cause: RuntimeError) -> RuntimeError {
exec_stmt_error_with_stmt_and_cause(stmt.clone().into(), cause)
}
fn exec_have_fn_by_induc_verify_process(
&mut self,
stmt: &HaveFnByInducStmt,
) -> Result<(), RuntimeError> {
self.define_have_fn_by_induc_current_params_and_domain(stmt)?;
self.verify_have_fn_by_induc_measure_lower_bound(stmt)?;
self.register_have_fn_by_induc_recursive_fn(stmt)?;
self.verify_have_fn_by_induc_case_list(stmt, &stmt.cases)
}
fn define_have_fn_by_induc_current_params_and_domain(
&mut self,
stmt: &HaveFnByInducStmt,
) -> Result<(), RuntimeError> {
for param_def_with_set in stmt.fn_set_clause.params_def_with_set.iter() {
self.define_params_with_set(param_def_with_set)
.map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
}
for dom_fact in stmt.fn_set_clause.dom_facts.iter() {
self.store_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(
dom_fact.clone(),
)
.map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
}
Ok(())
}
fn verify_have_fn_by_induc_measure_lower_bound(
&mut self,
stmt: &HaveFnByInducStmt,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&stmt.measure, &VerifyState::new(0, false))
.map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
self.verify_obj_well_defined_and_store_cache(
&stmt.lower_bound,
&VerifyState::new(0, false),
)
.map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
let lower_fact: AtomicFact = GreaterEqualFact::new(
stmt.measure.clone(),
stmt.lower_bound.clone(),
stmt.line_file.clone(),
)
.into();
let result = self
.verify_atomic_fact(&lower_fact, &VerifyState::new(0, false))
.map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
if result.is_unknown() {
return Err(short_exec_error(
stmt.clone().into(),
format!(
"have_fn_by_induc: failed to prove decreasing measure lower bound `{}`",
lower_fact
),
None,
vec![],
));
}
Ok(())
}
fn register_have_fn_by_induc_recursive_fn(
&mut self,
stmt: &HaveFnByInducStmt,
) -> Result<(), RuntimeError> {
self.store_free_param_or_identifier_name(&stmt.name, ParamObjType::Identifier)
.map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
let param_names = stmt.param_names();
let generated_names = self.generate_random_unused_names(param_names.len());
let mut param_to_generated_obj: HashMap<String, Obj> = HashMap::new();
for (param_name, generated_name) in param_names.iter().zip(generated_names.iter()) {
param_to_generated_obj.insert(
param_name.clone(),
obj_for_bound_param_in_scope(generated_name.clone(), ParamObjType::FnSet),
);
}
let mut generated_groups: Vec<ParamGroupWithSet> =
Vec::with_capacity(stmt.fn_set_clause.params_def_with_set.len());
let mut generated_index = 0;
for group in stmt.fn_set_clause.params_def_with_set.iter() {
let mut generated_group_names = Vec::with_capacity(group.params.len());
for _ in group.params.iter() {
generated_group_names.push(generated_names[generated_index].clone());
generated_index += 1;
}
let generated_set = self
.inst_obj(
group.set_obj(),
¶m_to_generated_obj,
ParamObjType::FnSet,
)
.map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
generated_groups.push(ParamGroupWithSet::new(generated_group_names, generated_set));
}
let mut recursive_dom_facts: Vec<OrAndChainAtomicFact> =
Vec::with_capacity(stmt.fn_set_clause.dom_facts.len() + 2);
for dom_fact in stmt.fn_set_clause.dom_facts.iter() {
recursive_dom_facts.push(
self.inst_or_and_chain_atomic_fact(
dom_fact,
¶m_to_generated_obj,
ParamObjType::FnSet,
None,
)
.map_err(|e| Self::have_fn_by_induc_err(stmt, e))?,
);
}
let generated_measure = self
.inst_obj(&stmt.measure, ¶m_to_generated_obj, ParamObjType::FnSet)
.map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
recursive_dom_facts.push(OrAndChainAtomicFact::AtomicFact(
LessFact::new(
generated_measure.clone(),
stmt.measure.clone(),
stmt.line_file.clone(),
)
.into(),
));
recursive_dom_facts.push(OrAndChainAtomicFact::AtomicFact(
GreaterEqualFact::new(
generated_measure,
stmt.lower_bound.clone(),
stmt.line_file.clone(),
)
.into(),
));
let generated_ret_set = self
.inst_obj(
&stmt.fn_set_clause.ret_set,
¶m_to_generated_obj,
ParamObjType::FnSet,
)
.map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
let recursive_fn_set = self
.new_fn_set(generated_groups, recursive_dom_facts, generated_ret_set)
.map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
let function_in_function_set_fact: Fact = InFact::new(
Identifier::new(stmt.name.clone()).into(),
recursive_fn_set.into(),
stmt.line_file.clone(),
)
.into();
self.verify_well_defined_and_store_and_infer_with_default_verify_state(
function_in_function_set_fact,
)
.map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
Ok(())
}
fn verify_have_fn_by_induc_case_list(
&mut self,
stmt: &HaveFnByInducStmt,
cases: &[HaveFnByInducCase],
) -> Result<(), RuntimeError> {
if cases.is_empty() {
return Err(short_exec_error(
stmt.clone().into(),
"have_fn_by_induc: case list must not be empty".to_string(),
None,
vec![],
));
}
let coverage_cases: Vec<AndChainAtomicFact> =
cases.iter().map(|c| c.case_fact.clone()).collect();
let coverage: Fact = OrFact::new(coverage_cases, stmt.line_file.clone()).into();
self.verify_fact_return_err_if_not_true(&coverage, &VerifyState::new(0, false))
.map_err(|e| {
short_exec_error(
stmt.clone().into(),
"have_fn_by_induc: cases do not cover all situations".to_string(),
Some(e),
vec![],
)
})?;
self.verify_have_fn_by_induc_cases_mutually_exclusive(stmt, cases)?;
for case in cases.iter() {
self.run_in_local_env(|rt| {
rt.verify_well_defined_and_store_and_infer_with_default_verify_state(Fact::from(
case.case_fact.clone(),
))
.map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
match &case.body {
HaveFnByInducCaseBody::EqualTo(equal_to) => {
rt.verify_have_fn_by_induc_equal_to(stmt, equal_to)
}
HaveFnByInducCaseBody::NestedCases(nested) => {
rt.verify_have_fn_by_induc_case_list(stmt, nested)
}
}
})?;
}
Ok(())
}
fn verify_have_fn_by_induc_equal_to(
&mut self,
stmt: &HaveFnByInducStmt,
equal_to: &Obj,
) -> Result<(), RuntimeError> {
let verify_state = VerifyState::new(0, false);
self.verify_obj_well_defined_and_store_cache(equal_to, &verify_state)
.map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
let equal_to_in_ret_set_atomic_fact: AtomicFact = InFact::new(
equal_to.clone(),
stmt.fn_set_clause.ret_set.clone(),
stmt.line_file.clone(),
)
.into();
let verify_result = self
.verify_atomic_fact(&equal_to_in_ret_set_atomic_fact, &verify_state)
.map_err(|e| Self::have_fn_by_induc_err(stmt, e))?;
if verify_result.is_unknown() {
return Err(short_exec_error(
stmt.clone().into(),
format!(
"have_fn_by_induc: {} is not in return set {}",
equal_to, stmt.fn_set_clause.ret_set
),
None,
vec![],
));
}
Ok(())
}
fn verify_have_fn_by_induc_cases_mutually_exclusive(
&mut self,
stmt: &HaveFnByInducStmt,
cases: &[HaveFnByInducCase],
) -> Result<(), RuntimeError> {
for i in 0..cases.len() {
for j in (i + 1)..cases.len() {
if !self
.have_fn_by_induc_cases_are_disjoint(&cases[i].case_fact, &cases[j].case_fact)?
{
return Err(short_exec_error(
stmt.clone().into(),
format!(
"have_fn_by_induc: cases overlap or cannot be proved mutually exclusive: `{}` and `{}`",
cases[i].case_fact, cases[j].case_fact
),
None,
vec![],
));
}
}
}
Ok(())
}
fn have_fn_by_induc_cases_are_disjoint(
&mut self,
left: &AndChainAtomicFact,
right: &AndChainAtomicFact,
) -> Result<bool, RuntimeError> {
if self.have_fn_by_induc_case_implies_not_other(left, right)? {
return Ok(true);
}
self.have_fn_by_induc_case_implies_not_other(right, left)
}
fn have_fn_by_induc_case_implies_not_other(
&mut self,
assumed: &AndChainAtomicFact,
other: &AndChainAtomicFact,
) -> Result<bool, RuntimeError> {
self.run_in_local_env(|rt| {
rt.verify_well_defined_and_store_and_infer_with_default_verify_state(Fact::from(
assumed.clone(),
))?;
for atom in flatten_have_fn_by_induc_and_chain_to_atomic_facts(other) {
let reversed = atom.make_reversed();
let result = rt.verify_atomic_fact(&reversed, &VerifyState::new(0, false))?;
if result.is_true() {
return Ok(true);
}
}
Ok(false)
})
}
pub fn exec_have_fn_by_induc_stmt(
&mut self,
stmt: &HaveFnByInducStmt,
) -> Result<StmtResult, RuntimeError> {
self.exec_have_fn_by_induc(stmt)
}
}
fn flatten_have_fn_by_induc_and_chain_to_atomic_facts(c: &AndChainAtomicFact) -> Vec<AtomicFact> {
match c {
AndChainAtomicFact::AtomicFact(a) => vec![a.clone()],
AndChainAtomicFact::AndFact(af) => af.facts.clone(),
AndChainAtomicFact::ChainFact(cf) => cf.facts().unwrap(),
}
}