use crate::prelude::*;
use std::fmt;
#[derive(Clone)]
pub struct ForallFact {
pub params_def_with_type: ParamDefWithType,
pub dom_facts: Vec<Fact>,
pub then_facts: Vec<ExistOrAndChainAtomicFact>,
pub line_file: LineFile,
}
impl ForallFact {
pub fn new(
params_def_with_type: ParamDefWithType,
dom_facts: Vec<Fact>,
then_facts: Vec<ExistOrAndChainAtomicFact>,
line_file: LineFile,
) -> Result<Self, RuntimeError> {
let forall_fact = ForallFact {
params_def_with_type,
dom_facts,
then_facts,
line_file,
};
check_forall_fact_has_no_duplicate_forall_free_parameter(&forall_fact)?;
Ok(forall_fact)
}
pub fn expand_then_facts_with_order_chain_closure(&mut self) -> Result<(), RuntimeError> {
let mut new_then: Vec<ExistOrAndChainAtomicFact> =
Vec::with_capacity(self.then_facts.len().saturating_mul(2));
for tf in std::mem::take(&mut self.then_facts) {
match tf {
ExistOrAndChainAtomicFact::ChainFact(c) => {
let atomics = c.facts_with_order_transitive_closure()?;
new_then.push(ExistOrAndChainAtomicFact::ChainFact(c));
for af in atomics {
new_then.push(ExistOrAndChainAtomicFact::AtomicFact(af));
}
}
other => new_then.push(other),
}
}
self.then_facts = new_then;
Ok(())
}
}
impl fmt::Display for ForallFact {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
match self.dom_facts.len() {
0 => write!(
f,
"{} {}{}\n{}",
FORALL,
self.params_def_with_type.to_string(),
COLON,
vec_to_string_add_four_spaces_at_beginning_of_each_line(&self.then_facts, 1)
),
_ => write!(
f,
"{} {}{}\n{}\n{}{}\n{}",
FORALL,
self.params_def_with_type.to_string(),
COLON,
vec_to_string_add_four_spaces_at_beginning_of_each_line(&self.dom_facts, 1),
to_string_and_add_four_spaces_at_beginning_of_each_line(&RIGHT_ARROW, 1),
COLON,
vec_to_string_add_four_spaces_at_beginning_of_each_line(&self.then_facts, 2)
),
}
}
}