use crate::prelude::*;
use std::collections::HashSet;
impl Runtime {
pub fn store_fact_without_well_defined_verified_and_infer(
&mut self,
fact: Fact,
) -> Result<InferResult, RuntimeErrorStruct> {
match fact {
Fact::AtomicFact(_)
| Fact::ExistFact(_)
| Fact::OrFact(_)
| Fact::AndFact(_)
| Fact::ChainFact(_) => self.store_whole_fact_update_cache_known_fact_and_infer(fact),
Fact::ForallFact(forall_fact) => {
self.store_forall_fact_without_well_defined_verified_and_infer(forall_fact)
}
Fact::ForallFactWithIff(forall_fact_with_iff) => self
.store_forall_fact_with_iff_without_well_defined_verified_and_infer(
forall_fact_with_iff,
),
}
}
pub fn store_fact_without_forall_coverage_check_and_infer(
&mut self,
fact: Fact,
) -> Result<InferResult, RuntimeErrorStruct> {
self.store_whole_fact_update_cache_known_fact_and_infer(fact)
}
fn store_forall_fact_without_well_defined_verified_and_infer(
&mut self,
mut forall_fact: ForallFact,
) -> Result<InferResult, RuntimeErrorStruct> {
let coverage_error_detail_lines =
forall_fact.error_messages_if_forall_param_missing_in_some_then_clause();
if coverage_error_detail_lines.is_empty() {
return self
.store_whole_fact_update_cache_known_fact_and_infer(Fact::ForallFact(forall_fact));
}
let warning_msg = forall_fact_coverage_warn_after_drop_then(&coverage_error_detail_lines);
let then_drop: HashSet<usize> = coverage_error_detail_lines
.iter()
.map(|(i, _)| *i)
.collect();
forall_fact.then_facts = forall_fact
.then_facts
.into_iter()
.enumerate()
.filter(|(i, _)| !then_drop.contains(i))
.map(|(_, f)| f)
.collect();
if forall_fact.then_facts.is_empty() {
let mut infer_result = InferResult::new();
infer_result.new_with_msg(warning_msg);
return Ok(infer_result);
}
let mut infer_result = InferResult::new();
infer_result.new_with_msg(warning_msg);
infer_result.new_infer_result_inside(
self.store_whole_fact_update_cache_known_fact_and_infer(Fact::ForallFact(forall_fact))?,
);
Ok(infer_result)
}
fn store_forall_fact_with_iff_without_well_defined_verified_and_infer(
&mut self,
forall_fact_with_iff: ForallFactWithIff,
) -> Result<InferResult, RuntimeErrorStruct> {
let (forall_then_implies_iff, forall_iff_implies_then) =
forall_fact_with_iff.to_two_forall_facts();
let mut infer_result = self
.store_forall_fact_without_well_defined_verified_and_infer(forall_then_implies_iff)?;
infer_result.new_infer_result_inside(
self.store_forall_fact_without_well_defined_verified_and_infer(
forall_iff_implies_then,
)?,
);
Ok(infer_result)
}
fn store_whole_fact_update_cache_known_fact_and_infer(
&mut self,
fact: Fact,
) -> Result<InferResult, RuntimeErrorStruct> {
let line_file = fact.line_file();
let fact_string: FactString = fact.to_string();
let fact_for_infer = fact.clone();
self.top_level_env().store_fact(fact)?;
self.top_level_env()
.store_fact_to_cache_known_fact(fact_string, line_file)?;
let infer_result = self.infer(&fact_for_infer).map_err(|e| {
RuntimeErrorStruct::new_with_msg_previous_error(format!("infer error: {}", e), Some(e))
})?;
Ok(infer_result)
}
pub fn store_and_chain_atomic_fact_without_well_defined_verified_and_infer(
&mut self,
fact: AndChainAtomicFact,
) -> Result<InferResult, RuntimeErrorStruct> {
let line_file = fact.line_file();
let fact_string: FactString = fact.to_string();
let fact_for_infer = fact.to_fact();
self.top_level_env().store_and_chain_atomic_fact(fact)?;
self.top_level_env()
.store_fact_to_cache_known_fact(fact_string, line_file)?;
let infer_result = self.infer(&fact_for_infer).map_err(|e| {
RuntimeErrorStruct::new_with_msg_previous_error(format!("infer error: {}", e), Some(e))
})?;
Ok(infer_result)
}
pub fn store_atomic_fact_without_well_defined_verified_and_infer(
&mut self,
fact: AtomicFact,
) -> Result<InferResult, RuntimeErrorStruct> {
let line_file = fact.line_file();
let fact_string: FactString = fact.to_string();
let infer_wrapped_fact = Fact::AtomicFact(fact.clone());
self.top_level_env().store_atomic_fact(fact)?;
self.top_level_env()
.store_fact_to_cache_known_fact(fact_string, line_file)?;
let infer_result = self.infer(&infer_wrapped_fact).map_err(|e| {
RuntimeErrorStruct::new_with_msg_previous_error(format!("infer error: {}", e), Some(e))
})?;
Ok(infer_result)
}
pub fn store_exist_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(
&mut self,
fact: ExistOrAndChainAtomicFact,
) -> Result<InferResult, RuntimeErrorStruct> {
let line_file = fact.line_file();
let fact_string: FactString = fact.to_string();
let fact_for_infer = fact.clone();
self.top_level_env()
.store_exist_or_and_chain_atomic_fact(fact)?;
self.top_level_env()
.store_fact_to_cache_known_fact(fact_string, line_file)?;
let infer_result = self
.infer_exist_or_and_chain_atomic_fact(&fact_for_infer)
.map_err(|e| {
RuntimeErrorStruct::new_with_msg_previous_error(
format!("infer error: {}", e),
Some(e),
)
})?;
Ok(infer_result)
}
pub fn store_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(
&mut self,
fact: OrAndChainAtomicFact,
) -> Result<InferResult, RuntimeErrorStruct> {
let line_file = fact.line_file();
let fact_string: FactString = fact.to_string();
let fact_for_infer = fact.clone();
self.top_level_env().store_or_and_chain_atomic_fact(fact)?;
self.top_level_env()
.store_fact_to_cache_known_fact(fact_string, line_file)?;
let infer_result = self
.infer_or_and_chain_atomic_fact(&fact_for_infer)
.map_err(|e| {
RuntimeErrorStruct::new_with_msg_previous_error(
format!("infer error: {}", e),
Some(e),
)
})?;
Ok(infer_result)
}
}
fn forall_fact_coverage_warn_after_drop_then(
coverage_error_detail_lines: &[(usize, String)],
) -> String {
let body = coverage_error_detail_lines
.iter()
.map(|(idx, msg)| format!("at index {}: {}", idx, msg))
.collect::<Vec<_>>()
.join("\n");
format!(
"Warning: forall missing forall parameter(s) in some then clause(s); dropped problematic clause(s):\n{}",
body
)
}