use crate::prelude::*;
use std::collections::HashMap;
impl Runtime {
pub(crate) fn build_not_exist_demorgan_forall_fact(
&self,
not_exist: &ExistFactEnum,
) -> Result<ForallFact, RuntimeError> {
if !not_exist.is_not_exist() {
return Err(RuntimeError::from(NewFactRuntimeError(
RuntimeErrorStruct::new_with_just_msg(
"internal: build_not_exist_demorgan_forall_fact expects NotExistFact"
.to_string(),
),
)));
}
if not_exist.params_def_with_type().number_of_params() == 0 {
return Err(RuntimeError::from(NewFactRuntimeError(
RuntimeErrorStruct::new_with_msg_and_line_file(
"not exist: cannot derive forall (no parameters)".to_string(),
not_exist.line_file(),
),
)));
}
let facts = not_exist.facts();
if facts.is_empty() {
return Err(RuntimeError::from(NewFactRuntimeError(
RuntimeErrorStruct::new_with_msg_and_line_file(
"not exist: cannot derive forall (empty body)".to_string(),
not_exist.line_file(),
),
)));
}
let lf = not_exist.line_file();
let mut param_to_forall_obj: HashMap<String, Obj> = HashMap::new();
let mut forall_groups: Vec<ParamGroupWithParamType> = Vec::new();
for group in not_exist.params_def_with_type().groups.iter() {
for name in group.params.iter() {
param_to_forall_obj.insert(
name.clone(),
obj_for_bound_param_in_scope(name.clone(), ParamObjType::Forall),
);
}
let param_type =
self.inst_param_type(&group.param_type, ¶m_to_forall_obj, ParamObjType::Exist)?;
forall_groups.push(ParamGroupWithParamType::new(
group.params.clone(),
param_type,
));
}
let mut disjuncts: Vec<AndChainAtomicFact> = Vec::new();
for conjunct in facts.iter() {
let forall_conjunct = self.inst_exist_body_fact(
conjunct,
¶m_to_forall_obj,
ParamObjType::Exist,
None,
)?;
let Some(forall_conjunct) =
exist_body_fact_as_or_and_chain_atomic_fact(forall_conjunct)
else {
return Err(RuntimeError::from(NewFactRuntimeError(
RuntimeErrorStruct::new_with_msg_and_line_file(
format!(
"not exist: `{}` in body cannot be negated here",
FORALL_BANG
),
conjunct.line_file(),
),
)));
};
let mut part = Self::demorgan_negate_exist_body_conjunct(&forall_conjunct)?;
disjuncts.append(&mut part);
}
let then_fact = if disjuncts.len() == 1 {
disjuncts.remove(0).into()
} else {
ExistOrAndChainAtomicFact::OrFact(OrFact::new(disjuncts, lf.clone()))
};
Ok(ForallFact::new(
ParamDefWithType::new(forall_groups),
vec![],
vec![then_fact],
lf,
)?)
}
pub(crate) fn demorgan_negate_exist_body_conjunct(
conjunct: &OrAndChainAtomicFact,
) -> Result<Vec<AndChainAtomicFact>, RuntimeError> {
let lf = conjunct.line_file();
match conjunct {
OrAndChainAtomicFact::AtomicFact(a) => Ok(vec![AndChainAtomicFact::AtomicFact(
Self::demorgan_negate_atomic_or_err(a)?,
)]),
OrAndChainAtomicFact::AndFact(af) => {
if af.facts.is_empty() {
return Err(RuntimeError::from(NewFactRuntimeError(
RuntimeErrorStruct::new_with_msg_and_line_file(
"not exist: empty `and` in body".to_string(),
lf,
),
)));
}
let mut out = Vec::with_capacity(af.facts.len());
for a in af.facts.iter() {
out.push(AndChainAtomicFact::AtomicFact(
Self::demorgan_negate_atomic_or_err(a)?,
));
}
Ok(out)
}
OrAndChainAtomicFact::ChainFact(cf) => {
let atomics = cf
.facts()
.map_err(RuntimeError::wrap_new_fact_as_store_conflict)?;
if atomics.is_empty() {
return Err(RuntimeError::from(NewFactRuntimeError(
RuntimeErrorStruct::new_with_msg_and_line_file(
"not exist: empty chain in body".to_string(),
lf,
),
)));
}
let mut out = Vec::with_capacity(atomics.len());
for a in atomics.iter() {
out.push(AndChainAtomicFact::AtomicFact(
Self::demorgan_negate_atomic_or_err(a)?,
));
}
Ok(out)
}
OrAndChainAtomicFact::OrFact(_) => Err(RuntimeError::from(NewFactRuntimeError(
RuntimeErrorStruct::new_with_msg_and_line_file(
"not exist: automatic forall derivation does not support `or` inside a body conjunct"
.to_string(),
lf,
),
))),
}
}
fn demorgan_negate_atomic_or_err(a: &AtomicFact) -> Result<AtomicFact, RuntimeError> {
match a {
AtomicFact::FnEqualFact(_) | AtomicFact::FnEqualInFact(_) => Err(
RuntimeError::from(NewFactRuntimeError(
RuntimeErrorStruct::new_with_msg_and_line_file(
"not exist: automatic forall derivation does not support negating $fn_eq / $fn_eq_in here"
.to_string(),
a.line_file(),
),
)),
),
_ => Ok(a.make_reversed()),
}
}
}
fn exist_body_fact_as_or_and_chain_atomic_fact(
fact: ExistBodyFact,
) -> Option<OrAndChainAtomicFact> {
match fact {
ExistBodyFact::AtomicFact(f) => Some(OrAndChainAtomicFact::AtomicFact(f)),
ExistBodyFact::AndFact(f) => Some(OrAndChainAtomicFact::AndFact(f)),
ExistBodyFact::ChainFact(f) => Some(OrAndChainAtomicFact::ChainFact(f)),
ExistBodyFact::OrFact(f) => Some(OrAndChainAtomicFact::OrFact(f)),
ExistBodyFact::InlineForall(_) => None,
}
}