use crate::prelude::*;
impl Runtime {
pub fn exec_claim_stmt(&mut self, stmt: &ClaimStmt) -> Result<StmtResult, RuntimeError> {
match &stmt.fact {
Fact::ForallFactWithIff(_) => unreachable!("claim forall with iff is not supported"),
Fact::ForallFact(forall_fact) => {
self.verify_fact_well_defined(&stmt.fact, &VerifyState::new(0, false))
.map_err(|e| {
RuntimeError::from(RuntimeErrorStruct::exec_stmt_with_message_and_cause(
stmt.clone().into(),
"claim: fact is not well defined".to_string(),
Some(e.into()),
vec![],
))
})?;
let body_exec_result = self.run_in_local_env(|rt| {
rt.define_params_with_type(&forall_fact.params_def_with_type, false)
.map_err(|define_params_error| {
RuntimeError::from(RuntimeErrorStruct::exec_stmt_new_with_stmt(
stmt.clone().into(),
"".to_string(),
Some(define_params_error),
vec![],
))
})?;
for dom_fact in forall_fact.dom_facts.iter() {
rt.store_exist_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(
dom_fact.clone(),
)?;
}
let mut inside_results = vec![];
for proof_stmt in stmt.proof.iter() {
let result = rt.exec_stmt(proof_stmt)?;
inside_results.push(result);
}
for then_fact in forall_fact.then_facts.iter() {
let result = rt.verify_exist_or_and_chain_atomic_fact(
then_fact,
&VerifyState::new(0, false),
)?;
if result.is_unknown() {
return Err(
RuntimeError::new_unknown_error_with_msg_position_optional_fact_previous_error(
format!("claim failed: cannot prove `{}`", stmt.fact),
stmt.line_file.clone(),
Some(stmt.fact.clone()),
None,
)
.into(),
);
}
inside_results.push(result);
}
Ok(NonFactualStmtSuccess::new(
stmt.clone().into(),
crate::infer::InferResult::new(),
inside_results,
)
.into())
});
let non_err_after_body: StmtResult = match body_exec_result {
Ok(non_err_stmt_exec_result) => non_err_stmt_exec_result,
Err(runtime_error) => return Err(runtime_error),
};
if non_err_after_body.is_unknown() {
return Err(RuntimeError::new_unknown_error_with_msg_position_optional_fact_previous_error(
format!("claim failed: cannot prove `{}`", stmt.fact),
stmt.line_file.clone(),
Some(stmt.fact.clone()),
None,
).into());
}
let infer_result_after_store =
self.store_fact_without_well_defined_verified_and_infer(stmt.fact.clone())?;
Ok(non_err_after_body.with_infers(infer_result_after_store))
}
_ => {
self.verify_fact_well_defined(&stmt.fact, &VerifyState::new(0, false))
.map_err(|e| {
RuntimeError::from(RuntimeErrorStruct::exec_stmt_with_message_and_cause(
stmt.clone().into(),
"claim: fact is not well defined".to_string(),
Some(e.into()),
vec![],
))
})?;
let body_exec_result = self.run_in_local_env(|rt| {
let mut inside_results: Vec<StmtResult> = Vec::new();
for proof_stmt in stmt.proof.iter() {
let proof_exec_result = rt.exec_stmt(proof_stmt)?;
inside_results.push(proof_exec_result);
}
rt.verify_fact_return_err_if_not_true(&stmt.fact, &VerifyState::new(0, false))?;
Ok(NonFactualStmtSuccess::new(
stmt.clone().into(),
crate::infer::InferResult::new(),
inside_results,
)
.into())
});
let non_err_after_body: StmtResult = match body_exec_result {
Ok(non_err_stmt_exec_result) => non_err_stmt_exec_result,
Err(runtime_error) => return Err(runtime_error),
};
let infer_result_after_store =
self.store_fact_without_well_defined_verified_and_infer(stmt.fact.clone())?;
Ok(non_err_after_body.with_infers(infer_result_after_store))
}
}
}
}