use crate::prelude::*;
impl Runtime {
pub fn exec_witness_exist_fact(
&mut self,
stmt: &WitnessExistFact,
) -> Result<StmtResult, RuntimeError> {
let witness_stmt = stmt.clone().into();
let inside_results_when_verify = self.run_in_local_env(|rt| {
let witness_stmt = stmt.clone().into();
let verify_state_for_well_defined = VerifyState::new(0, false);
let expected_param_count = ParamGroupWithParamType::number_of_params(
&stmt.exist_fact_in_witness.params_def_with_type,
);
if expected_param_count != stmt.equal_tos.len() {
return Err(RuntimeError::from(
RuntimeErrorStruct::exec_stmt_with_message_and_cause(
witness_stmt,
"witness exist fact: parameter count mismatch".to_string(),
None,
vec![],
),
));
}
if let Err(well_defined_error) = rt.verify_exist_fact_well_defined(
&stmt.exist_fact_in_witness,
&verify_state_for_well_defined,
) {
return Err(RuntimeError::from(
RuntimeErrorStruct::exec_stmt_with_message_and_cause(
witness_stmt,
"witness exist fact: exist fact well-defined failed".to_string(),
Some(well_defined_error.into()),
vec![],
),
));
}
for equal_to_obj in stmt.equal_tos.iter() {
if let Err(well_defined_error) = rt.verify_obj_well_defined_and_store_cache(
equal_to_obj,
&verify_state_for_well_defined,
) {
return Err(RuntimeError::from(
RuntimeErrorStruct::exec_stmt_with_message_and_cause(
witness_stmt,
"witness exist fact: equal_to well-defined failed".to_string(),
Some(well_defined_error.into()),
vec![],
),
));
}
}
let have_obj_equal_stmt = HaveObjEqualStmt {
param_def: stmt.exist_fact_in_witness.params_def_with_type.clone(),
objs_equal_to: stmt.equal_tos.clone(),
line_file: stmt.line_file.clone(),
};
match rt.exec_have_obj_equal_stmt(&have_obj_equal_stmt) {
Ok(_binding_result) => {}
Err(exec_stmt_error) => {
return Err(RuntimeError::from(exec_stmt_error));
}
}
let mut inside_results: Vec<StmtResult> = Vec::new();
for proof_stmt in stmt.proof.iter() {
match rt.exec_stmt(proof_stmt) {
Ok(proof_result) => {
inside_results.push(proof_result);
}
Err(proof_exec_error) => {
return Err(RuntimeError::from(
RuntimeErrorStruct::exec_stmt_with_message_and_cause(
witness_stmt.clone(),
proof_stmt.to_string(),
Some(proof_exec_error),
inside_results,
),
));
}
}
}
let param_to_obj_map = ParamGroupWithParamType::param_defs_and_args_to_param_to_arg_map(
&stmt.exist_fact_in_witness.params_def_with_type,
&stmt.equal_tos,
);
let instantiated_exist_fact =
rt.inst_exist_fact(&stmt.exist_fact_in_witness, ¶m_to_obj_map)?;
let verify_state_for_proof_check = VerifyState::new(0, false);
for internal_fact_template in instantiated_exist_fact.facts.iter() {
let internal_fact = internal_fact_template.clone().to_fact();
let verification_result = rt
.verify_fact_return_err_if_not_true(&internal_fact, &verify_state_for_proof_check);
if let Err(verify_error) = verification_result {
return Err(RuntimeError::from(verify_error));
}
}
Ok(inside_results)
});
let inside_results = match inside_results_when_verify {
Ok(proof_inside_results) => proof_inside_results,
Err(inside_results_error) => return Err(RuntimeError::from(inside_results_error)),
};
let store_result = self.store_fact_without_well_defined_verified_and_infer(
Fact::ExistFact(stmt.exist_fact_in_witness.clone()),
);
match store_result {
Ok(infer_result) => Ok((NonFactualStmtSuccess::new(witness_stmt, infer_result, inside_results)).into()),
Err(store_error) => Err(RuntimeError::from(
RuntimeErrorStruct::exec_stmt_with_message_and_cause(
witness_stmt,
"witness exist fact: failed to store exist fact".to_string(),
Some(store_error.into()),
inside_results,
),
)),
}
}
pub fn exec_witness_nonempty_set(
&mut self,
stmt: &WitnessNonemptySet,
) -> Result<StmtResult, RuntimeError> {
let witness_stmt = stmt.clone().into();
let inside_results_when_verify = self.run_in_local_env(|rt| {
let witness_stmt = stmt.clone().into();
let verify_state_for_well_defined = VerifyState::new(0, false);
if let Err(well_defined_error) =
rt.verify_obj_well_defined_and_store_cache(&stmt.obj, &verify_state_for_well_defined)
{
return Err(RuntimeError::from(
RuntimeErrorStruct::exec_stmt_with_message_and_cause(
witness_stmt,
"witness nonempty set: obj well-defined failed".to_string(),
Some(well_defined_error.into()),
vec![],
),
));
}
if let Err(well_defined_error) =
rt.verify_obj_well_defined_and_store_cache(&stmt.set, &verify_state_for_well_defined)
{
return Err(RuntimeError::from(
RuntimeErrorStruct::exec_stmt_with_message_and_cause(
witness_stmt.clone(),
"witness nonempty set: set well-defined failed".to_string(),
Some(well_defined_error.into()),
vec![],
),
));
}
let mut inside_results: Vec<StmtResult> = Vec::new();
for proof_stmt in stmt.proof.iter() {
match rt.exec_stmt(proof_stmt) {
Ok(proof_result) => {
inside_results.push(proof_result);
}
Err(proof_exec_error) => {
return Err(RuntimeError::from(
RuntimeErrorStruct::exec_stmt_with_message_and_cause(
witness_stmt.clone(),
proof_stmt.to_string(),
Some(proof_exec_error),
inside_results,
),
));
}
}
}
let verify_state_for_proof_check = VerifyState::new(0, false);
if let Obj::FnSet(fn_set) = &stmt.set {
let ret_nonempty_fact = AtomicFact::IsNonemptySetFact(IsNonemptySetFact::new(
fn_set.ret_set.as_ref().clone(),
stmt.line_file.clone(),
));
let ret_check = rt.verify_non_equational_atomic_fact_with_builtin_rules(
&ret_nonempty_fact,
&verify_state_for_proof_check,
)?;
if ret_check.is_true() {
return Ok(inside_results);
}
}
let membership_fact = Fact::AtomicFact(AtomicFact::InFact(InFact::new(
stmt.obj.clone(),
stmt.set.clone(),
stmt.line_file.clone(),
)));
rt.verify_fact_return_err_if_not_true(&membership_fact, &verify_state_for_proof_check)?;
Ok(inside_results)
});
let inside_results = match inside_results_when_verify {
Ok(proof_inside_results) => proof_inside_results,
Err(inside_results_error) => return Err(RuntimeError::from(inside_results_error)),
};
let store_result = self.store_fact_without_well_defined_verified_and_infer(
Fact::AtomicFact(AtomicFact::IsNonemptySetFact(IsNonemptySetFact::new(
stmt.set.clone(),
stmt.line_file.clone(),
))),
);
match store_result {
Ok(infer_result) => Ok((NonFactualStmtSuccess::new(witness_stmt, infer_result, inside_results)).into()),
Err(store_error) => Err(RuntimeError::from(
RuntimeErrorStruct::exec_stmt_with_message_and_cause(
witness_stmt,
"witness nonempty set: failed to store nonempty set fact".to_string(),
Some(store_error.into()),
inside_results,
),
)),
}
}
}