use crate::prelude::*;
impl Runtime {
pub fn exec_by_enumerate_stmt(
&mut self,
stmt: &ByEnumerateStmt,
) -> Result<StmtResult, RuntimeError> {
let corresponding_forall_fact = stmt.to_corresponding_forall_fact().map_err(|msg| {
RuntimeError::from(RuntimeErrorStruct::exec_stmt_with_message_and_cause(
stmt.clone().into(),
msg,
None,
vec![],
))
})?;
self.verify_fact_well_defined(&corresponding_forall_fact, &VerifyState::new(0, false))
.map_err(|well_defined_error| {
RuntimeError::from(RuntimeErrorStruct::exec_stmt_with_message_and_cause(
stmt.clone().into(),
format!(
"by enumerate: corresponding forall `{}` is not well-defined",
corresponding_forall_fact
),
Some(well_defined_error.into()),
vec![],
))
})?;
let enumerate_cartesian_product_is_empty = stmt
.param_sets
.iter()
.any(|list_set_obj| list_set_obj.list.is_empty());
if enumerate_cartesian_product_is_empty {
let infer_result_from_stored_forall_fact = self
.store_fact_without_well_defined_verified_and_infer(
corresponding_forall_fact.clone(),
)
.map_err(|store_fact_error| {
RuntimeError::from(RuntimeErrorStruct::exec_stmt_with_message_and_cause(
stmt.clone().into(),
format!(
"by enumerate: failed to store corresponding forall `{}`",
corresponding_forall_fact
),
Some(store_fact_error.into()),
vec![],
))
})?;
let infer_result = Self::infer_result_with_generated_forall_and_store_infer(
&corresponding_forall_fact,
infer_result_from_stored_forall_fact,
);
return Ok((NonFactualStmtSuccess::new(
stmt.clone().into(),
infer_result,
vec![],
)).into());
}
let mut current_parameter_index_assignment = Self::by_enumerate_start_index_assignment(stmt);
loop {
self.exec_by_enumerate_stmt_for_one_assignment(
stmt,
¤t_parameter_index_assignment,
)?;
let next_parameter_index_assignment =
Self::by_enumerate_next_index_assignment(stmt, ¤t_parameter_index_assignment);
match next_parameter_index_assignment {
Some(next_parameter_index_assignment) => {
current_parameter_index_assignment = next_parameter_index_assignment;
}
None => break,
}
}
let infer_result_from_stored_forall_fact = self
.store_fact_without_well_defined_verified_and_infer(
corresponding_forall_fact.clone(),
)
.map_err(|store_fact_error| {
RuntimeError::from(RuntimeErrorStruct::exec_stmt_with_message_and_cause(
stmt.clone().into(),
format!(
"by enumerate: failed to store corresponding forall `{}`",
corresponding_forall_fact
),
Some(store_fact_error.into()),
vec![],
))
})?;
let infer_result = Self::infer_result_with_generated_forall_and_store_infer(
&corresponding_forall_fact,
infer_result_from_stored_forall_fact,
);
Ok((NonFactualStmtSuccess::new(
stmt.clone().into(),
infer_result,
vec![],
)).into())
}
fn infer_result_with_generated_forall_and_store_infer(
generated_forall_fact: &Fact,
infer_after_store: InferResult,
) -> InferResult {
let mut infer_result = InferResult::new();
infer_result.new_fact(generated_forall_fact);
infer_result.new_infer_result_inside(infer_after_store);
infer_result
}
fn by_enumerate_start_index_assignment(stmt: &ByEnumerateStmt) -> Vec<usize> {
let mut start_index_assignment: Vec<usize> = Vec::new();
for _ in stmt.param_sets.iter() {
start_index_assignment.push(0);
}
start_index_assignment
}
fn by_enumerate_next_index_assignment(
stmt: &ByEnumerateStmt,
current_parameter_index_assignment: &Vec<usize>,
) -> Option<Vec<usize>> {
let mut next_parameter_index_assignment = current_parameter_index_assignment.clone();
for reversed_position in 0..next_parameter_index_assignment.len() {
let position_from_right = next_parameter_index_assignment.len() - 1 - reversed_position;
let current_index = next_parameter_index_assignment[position_from_right];
let current_list_set_length = stmt.param_sets[position_from_right].list.len();
if current_index + 1 < current_list_set_length {
next_parameter_index_assignment[position_from_right] = current_index + 1;
return Some(next_parameter_index_assignment);
}
next_parameter_index_assignment[position_from_right] = 0;
}
None
}
fn exec_by_enumerate_stmt_for_one_assignment(
&mut self,
stmt: &ByEnumerateStmt,
parameter_index_assignment: &Vec<usize>,
) -> Result<(), RuntimeError> {
self.run_in_local_env(|rt| {
rt.exec_by_enumerate_stmt_for_one_assignment_body(stmt, parameter_index_assignment)
})
}
fn exec_by_enumerate_stmt_for_one_assignment_body(
&mut self,
stmt: &ByEnumerateStmt,
parameter_index_assignment: &Vec<usize>,
) -> Result<(), RuntimeError> {
for (parameter_position, parameter_name) in stmt.params.iter().enumerate() {
let assigned_obj = (*stmt.param_sets[parameter_position].list
[parameter_index_assignment[parameter_position]])
.clone();
self.store_identifier_obj(parameter_name)
.map_err(RuntimeError::from)?;
let parameter_equal_to_assigned_obj_atomic_fact =
AtomicFact::EqualFact(EqualFact::new(
Obj::Identifier(Identifier::new(parameter_name.to_string())),
assigned_obj.clone(),
stmt.line_file.clone(),
));
self.store_atomic_fact_without_well_defined_verified_and_infer(
parameter_equal_to_assigned_obj_atomic_fact,
)
.map_err(RuntimeError::from)?;
}
for proof_stmt in stmt.proof.iter() {
if let Err(statement_error) = self.exec_stmt(proof_stmt) {
return Err(RuntimeError::from(
RuntimeErrorStruct::exec_stmt_with_message_and_cause(
stmt.clone().into(),
proof_stmt.to_string(),
Some(statement_error),
vec![],
),
));
}
}
for fact_to_prove in stmt.to_prove.iter() {
let verified_result = self.verify_exist_or_and_chain_atomic_fact(
fact_to_prove,
&VerifyState::new(0, false),
)?;
if verified_result.is_unknown() {
return Err(RuntimeError::from(
RuntimeErrorStruct::exec_stmt_with_message_and_cause(
stmt.clone().into(),
format!("by enumerate: failed to prove `{}`", fact_to_prove),
None,
vec![],
),
));
}
}
Ok(())
}
}