use super::helpers_by_stmt::impossible_proof_error_message;
use crate::prelude::*;
impl Runtime {
pub fn exec_by_cases_stmt(
&mut self,
stmt: &ByCasesStmt,
) -> Result<StmtResult, RuntimeError> {
for fact in stmt.then_facts.iter() {
self.verify_fact_well_defined(fact, &VerifyState::new(0, false))
.map_err(|verify_error| {
RuntimeError::from(RuntimeErrorStruct::exec_stmt_with_message_and_cause(
stmt.clone().into(),
format!("by cases: failed to prove `{}`", fact),
Some(verify_error.into()),
vec![],
))
})?;
}
self.exec_by_cases_stmt_verify_cases_cover_all_situations(stmt)
.map_err(RuntimeError::from)?;
let mut inside_results: Vec<StmtResult> = Vec::new();
for case_index in 0..stmt.cases.len() {
let one_case_result = self.run_in_local_env(|rt| {
rt.exec_by_cases_stmt_for_one_case(stmt, case_index)
});
match one_case_result {
Ok(mut one_case_inside_results) => {
inside_results.append(&mut one_case_inside_results);
}
Err(exec_stmt_error) => {
return Err(RuntimeError::from(exec_stmt_error));
}
}
}
let mut infer_result = InferResult::new();
for then_fact in stmt.then_facts.iter() {
let one_then_fact_infer_result = self
.store_fact_without_well_defined_verified_and_infer(then_fact.clone())
.map_err(|store_fact_error| {
RuntimeError::from(RuntimeErrorStruct::exec_stmt_with_message_and_cause(
stmt.clone().into(),
format!("by cases: failed to release `{}`", then_fact),
Some(store_fact_error.into()),
vec![],
))
})?;
infer_result.new_infer_result_inside(one_then_fact_infer_result);
}
Ok((NonFactualStmtSuccess::new(
stmt.clone().into(),
infer_result,
inside_results,
)).into())
}
fn exec_by_cases_stmt_verify_cases_cover_all_situations(
&mut self,
stmt: &ByCasesStmt,
) -> Result<(), RuntimeErrorStruct> {
let all_cases_or_fact =
Fact::OrFact(crate::fact::OrFact::new(stmt.cases.clone(), stmt.line_file.clone()));
self.verify_fact_return_err_if_not_true(&all_cases_or_fact, &VerifyState::new(0, false))
.map_err(|verify_error| {
RuntimeErrorStruct::exec_stmt_with_message_and_cause(
stmt.clone().into(),
"by cases: cannot verify that all cases cover all situations".to_string(),
Some(verify_error.into()),
vec![],
)
})?;
Ok(())
}
fn exec_by_cases_stmt_prove_then_facts_under_case(
&mut self,
stmt: &ByCasesStmt,
case_index: usize,
inside_results: &mut Vec<StmtResult>,
) -> Result<(), RuntimeErrorStruct> {
for then_fact in stmt.then_facts.iter() {
let exec_fact_result = self.exec_fact(then_fact).map_err(|statement_error| {
RuntimeErrorStruct::exec_stmt_with_message_and_cause(
stmt.clone().into(),
format!(
"by cases: failed to prove `{}` under case `{}`",
then_fact, stmt.cases[case_index]
),
Some(statement_error),
std::mem::take(inside_results),
)
})?;
inside_results.push(exec_fact_result);
}
Ok(())
}
fn exec_by_cases_stmt_for_one_case(
&mut self,
stmt: &ByCasesStmt,
case_index: usize,
) -> Result<Vec<StmtResult>, RuntimeErrorStruct> {
let case_fact = &stmt.cases[case_index];
let mut inside_results: Vec<StmtResult> = Vec::new();
self.store_and_chain_atomic_fact_without_well_defined_verified_and_infer(case_fact.clone())
.map_err(|store_fact_error| {
RuntimeErrorStruct::exec_stmt_with_message_and_cause(
stmt.clone().into(),
format!("by cases: failed to assume case `{}`", case_fact),
Some(store_fact_error.into()),
vec![],
)
})?;
for proof_stmt in stmt.proofs[case_index].iter() {
let exec_stmt_result = self.exec_stmt(proof_stmt);
match exec_stmt_result {
Ok(result) => inside_results.push(result),
Err(statement_error) => {
return Err(RuntimeErrorStruct::exec_stmt_with_message_and_cause(
stmt.clone().into(),
format!(
"by cases: failed while executing proof under case `{}`",
case_fact
),
Some(statement_error),
inside_results,
));
}
}
}
if let Some(impossible_fact) = &stmt.impossible_facts[case_index] {
let verify_state = VerifyState::new(0, false);
let verify_impossible_fact_result = self
.verify_atomic_fact(impossible_fact, &verify_state)
.map_err(|verify_error| {
RuntimeErrorStruct::exec_stmt_with_message_and_cause(
stmt.clone().into(),
impossible_proof_error_message(
impossible_fact,
Some(case_fact.to_string()),
),
Some(verify_error.into()),
vec![],
)
})?;
if verify_impossible_fact_result.is_unknown() {
return Err(RuntimeErrorStruct::exec_stmt_with_message_and_cause(
stmt.clone().into(),
impossible_proof_error_message(impossible_fact, Some(case_fact.to_string())),
None,
vec![],
));
}
let verify_reversed_impossible_fact_result = self
.verify_atomic_fact(&impossible_fact.make_reversed(), &verify_state)
.map_err(|verify_error| {
RuntimeErrorStruct::exec_stmt_with_message_and_cause(
stmt.clone().into(),
impossible_proof_error_message(
impossible_fact,
Some(case_fact.to_string()),
),
Some(verify_error.into()),
vec![],
)
})?;
if verify_reversed_impossible_fact_result.is_unknown() {
return Err(RuntimeErrorStruct::exec_stmt_with_message_and_cause(
stmt.clone().into(),
impossible_proof_error_message(impossible_fact, Some(case_fact.to_string())),
None,
vec![],
));
}
inside_results.push((NonFactualStmtSuccess::new(
stmt.clone().into(),
InferResult::new(),
vec![
verify_impossible_fact_result,
verify_reversed_impossible_fact_result,
],
)).into());
return Ok(inside_results);
}
self.exec_by_cases_stmt_prove_then_facts_under_case(
stmt,
case_index,
&mut inside_results,
)?;
Ok(inside_results)
}
}