use crate::prelude::*;
impl Runtime {
pub fn exec_by_commutative_prop_stmt(
&mut self,
stmt: &ByCommutativePropStmt,
) -> Result<StmtResult, RuntimeError> {
let (prop_name, gather) = stmt.commutative_prop_registration().map_err(|msg| {
RuntimeError::from(VerifyRuntimeError(
RuntimeErrorStruct::new_with_msg_and_line_file(msg, stmt.line_file.clone()),
))
})?;
let forall_arity = stmt
.forall_fact
.params_def_with_type
.collect_param_names()
.len();
let prop_definition = self.get_abstract_prop_definition_by_name(&prop_name);
match prop_definition {
Some(definition) => {
if definition.params.len() != forall_arity {
return Err(short_exec_error(
stmt.clone().into(),
format!(
"by commutative_prop: `{}` must have arity {} to match the forall",
prop_name, forall_arity
),
None,
vec![],
));
}
}
None => {
return Err(short_exec_error(
stmt.clone().into(),
format!(
"by commutative_prop: `{}` must be an abstract_prop",
prop_name
),
None,
vec![],
));
}
}
let inside_results = self.run_in_local_env(|rt| {
let verify_state = VerifyState::new(0, false);
let mut infer_result =
rt.forall_assume_params_and_dom_in_current_env(&stmt.forall_fact, &verify_state)?;
let mut inside_results: Vec<StmtResult> = Vec::new();
for proof_stmt in stmt.proof.iter() {
inside_results.push(rt.exec_stmt(proof_stmt)?);
}
let result = rt.forall_verify_then_facts_in_current_env(
&stmt.forall_fact,
&verify_state,
&mut infer_result,
None,
)?;
if result.is_unknown() {
return Err(short_exec_error(
stmt.clone().into(),
format!(
"by commutative_prop: failed to prove `{}`",
stmt.forall_fact
),
None,
inside_results,
));
}
inside_results.push(result);
Ok(inside_results)
})?;
self.top_level_env().store_commutative_prop_permutation(
prop_name.clone(),
gather.clone(),
stmt.line_file.clone(),
)?;
let mut infer_result = InferResult::new();
infer_result.new_with_msg(format!(
"registered commutative permutation {:?} for `{}`",
gather, prop_name
));
Ok(NonFactualStmtSuccess::new(stmt.clone().into(), infer_result, inside_results).into())
}
}