use crate::prelude::*;
use std::collections::HashMap;
use std::result::Result;
impl Runtime {
pub fn verify_exist_fact(
&mut self,
exist_fact: &ExistFactEnum,
verify_state: &VerifyState,
) -> Result<StmtResult, RuntimeError> {
if let Some(cached_result) =
self.verify_fact_from_cache_using_display_string(&exist_fact.clone().into())
{
return Ok(cached_result);
}
if !verify_state.well_defined_already_verified {
if let Err(e) = self.verify_exist_fact_well_defined(exist_fact, verify_state) {
return Err({
VerifyRuntimeError(RuntimeErrorStruct::new(
Some(Fact::from(exist_fact.clone()).into_stmt()),
String::new(),
exist_fact.line_file(),
Some(e),
vec![],
))
.into()
});
}
}
let result = self.verify_exist_fact_with_known_exist_fact(exist_fact, exist_fact)?;
if result.is_true() {
return Ok(result);
}
if verify_state.is_round_0() {
let result = self.verify_exist_fact_with_known_forall(exist_fact, verify_state)?;
if result.is_true() {
return Ok(result);
}
if exist_fact.is_exist_unique() {
if let Some(proved) = self.try_verify_exist_unique_by_exist_and_uniqueness_forall(
exist_fact,
verify_state,
)? {
return Ok(proved);
}
}
}
Ok((StmtUnknown::new()).into())
}
pub(crate) fn build_exist_unique_uniqueness_forall_fact(
&self,
exist_fact: &ExistFactEnum,
) -> Result<ForallFact, RuntimeError> {
let lf = exist_fact.line_file();
let flat_orig = exist_fact.params_def_with_type().collect_param_names();
let n = flat_orig.len();
let flat_a: Vec<String> = flat_orig.iter().map(|name| format!("{}1", name)).collect();
let flat_b: Vec<String> = flat_orig.iter().map(|name| format!("{}2", name)).collect();
let mut map_running_a: HashMap<String, Obj> = HashMap::new();
let mut map_running_b: HashMap<String, Obj> = HashMap::new();
let mut forall_groups: Vec<ParamGroupWithParamType> = Vec::new();
for group in exist_fact.params_def_with_type().groups.iter() {
let chunk_a: Vec<String> = group
.params
.iter()
.map(|name| format!("{}1", name))
.collect();
for (orig, nm) in group.params.iter().zip(chunk_a.iter()) {
map_running_a.insert(
orig.clone(),
obj_for_bound_param_in_scope(nm.clone(), ParamObjType::Forall),
);
}
let pt_a =
self.inst_param_type(&group.param_type, &map_running_a, ParamObjType::Forall)?;
forall_groups.push(ParamGroupWithParamType::new(chunk_a, pt_a));
}
for group in exist_fact.params_def_with_type().groups.iter() {
let chunk_b: Vec<String> = group
.params
.iter()
.map(|name| format!("{}2", name))
.collect();
for (orig, nm) in group.params.iter().zip(chunk_b.iter()) {
map_running_b.insert(
orig.clone(),
obj_for_bound_param_in_scope(nm.clone(), ParamObjType::Forall),
);
}
let pt_b =
self.inst_param_type(&group.param_type, &map_running_b, ParamObjType::Forall)?;
forall_groups.push(ParamGroupWithParamType::new(chunk_b, pt_b));
}
let map_a: HashMap<String, Obj> = flat_orig
.iter()
.cloned()
.zip(
flat_a
.iter()
.cloned()
.map(|s| obj_for_bound_param_in_scope(s, ParamObjType::Forall)),
)
.collect();
let map_b: HashMap<String, Obj> = flat_orig
.iter()
.cloned()
.zip(
flat_b
.iter()
.cloned()
.map(|s| obj_for_bound_param_in_scope(s, ParamObjType::Forall)),
)
.collect();
let mut dom_facts: Vec<Fact> = Vec::new();
for inner in exist_fact.facts().iter() {
let f_a = self.inst_exist_body_fact(inner, &map_a, ParamObjType::Exist, None)?;
dom_facts.push(f_a.to_fact());
}
for inner in exist_fact.facts().iter() {
let f_b = self.inst_exist_body_fact(inner, &map_b, ParamObjType::Exist, None)?;
dom_facts.push(f_b.to_fact());
}
let mut then_facts: Vec<ExistOrAndChainAtomicFact> = Vec::new();
if n == 1 {
let eq = EqualFact::new(
obj_for_bound_param_in_scope(flat_a[0].clone(), ParamObjType::Forall),
obj_for_bound_param_in_scope(flat_b[0].clone(), ParamObjType::Forall),
lf.clone(),
);
then_facts.push(ExistOrAndChainAtomicFact::AtomicFact(eq.into()));
} else {
let left_tuple: Obj = Tuple::new(
flat_a
.iter()
.cloned()
.map(|s| obj_for_bound_param_in_scope(s, ParamObjType::Forall))
.collect::<Vec<Obj>>(),
)
.into();
let right_tuple: Obj = Tuple::new(
flat_b
.iter()
.cloned()
.map(|s| obj_for_bound_param_in_scope(s, ParamObjType::Forall))
.collect::<Vec<Obj>>(),
)
.into();
let eq = EqualFact::new(left_tuple, right_tuple, lf.clone());
then_facts.push(ExistOrAndChainAtomicFact::AtomicFact(eq.into()));
}
let forall_fact = ForallFact::new(
ParamDefWithType::new(forall_groups),
dom_facts,
then_facts,
lf,
)?;
let mut param_to_arg_map: HashMap<String, Obj> = HashMap::new();
for group in forall_fact.params_def_with_type.groups.iter() {
for param in group.params.iter() {
param_to_arg_map
.insert(param.clone(), ForallFreeParamObj::new(param.clone()).into());
}
}
let forall_fact = self.inst_fact(
&forall_fact.into(),
¶m_to_arg_map,
ParamObjType::Forall,
None,
)?;
match forall_fact {
Fact::ForallFact(x) => Ok(x.clone()),
_ => {
unreachable!();
}
}
}
fn try_verify_exist_unique_by_exist_and_uniqueness_forall(
&mut self,
exist_fact: &ExistFactEnum,
verify_state: &VerifyState,
) -> Result<Option<StmtResult>, RuntimeError> {
if exist_fact.params_def_with_type().number_of_params() == 0 {
return Ok(None);
}
let plain = ExistFactEnum::ExistFact(ExistFactBody::new(
exist_fact.params_def_with_type().clone(),
exist_fact.facts().clone(),
exist_fact.line_file(),
)?);
let wd_ok = verify_state.make_state_with_req_ok_set_to_true();
let plain_res = self.verify_exist_fact(&plain, &wd_ok)?;
if !plain_res.is_true() {
return Ok(None);
}
let uniqueness_forall = self.build_exist_unique_uniqueness_forall_fact(exist_fact)?;
let uniqueness_fact: Fact = uniqueness_forall.clone().into();
let uniq_res = self.verify_fact(&uniqueness_fact, &wd_ok)?;
if !uniq_res.is_true() {
return Ok(None);
}
let mut infers = InferResult::new();
infers.new_fact(&exist_fact.clone().into());
infers.new_infer_result_inside(stmt_result_infers(&plain_res));
infers.new_infer_result_inside(stmt_result_infers(&uniq_res));
infers.new_fact(&uniqueness_fact);
let out = FactualStmtSuccess::new_with_verified_by_known_fact_and_infer(
exist_fact.clone().into(),
infers,
VerifiedByResult::cited_fact(
exist_fact.clone().into(),
uniqueness_fact.clone(),
Some("exist!: witness exist and uniqueness forall verified".to_string()),
),
vec![],
);
Ok(Some(out.into()))
}
pub fn verify_exist_fact_with_known_exist_fact(
&mut self,
exist_fact: &ExistFactEnum,
known_exist_fact: &ExistFactEnum,
) -> Result<StmtResult, RuntimeError> {
for environment in self.iter_environments_from_top() {
let result = Self::verify_exist_fact_with_known_exist_fact_with_facts_in_environment(
self,
environment,
exist_fact,
known_exist_fact,
)?;
if result.is_true() {
return Ok(result);
}
}
Ok((StmtUnknown::new()).into())
}
pub fn verify_exist_fact_with_known_exist_fact_with_facts_in_environment(
runtime: &Runtime,
environment: &Environment,
exist_fact: &ExistFactEnum,
known_exist_fact: &ExistFactEnum,
) -> Result<StmtResult, RuntimeError> {
let goal_keys = Self::known_exist_lookup_keys(known_exist_fact);
let target_body_string = Self::exist_fact_normalized_body_string(runtime, exist_fact)
.map_err(|e| {
RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
Some(Fact::from(exist_fact.clone()).into_stmt()),
String::new(),
exist_fact.line_file(),
Some(e),
vec![],
)))
})?;
for key in goal_keys.iter() {
let Some(known_exist_facts) = environment.known_exist_facts.get(key) else {
continue;
};
for known_fact in known_exist_facts.iter() {
if !known_fact.can_be_used_to_verify_goal(exist_fact) {
continue;
}
let known_body_string =
Self::exist_fact_normalized_body_string(runtime, known_fact).map_err(|e| {
RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
Some(Fact::from(exist_fact.clone()).into_stmt()),
String::new(),
exist_fact.line_file(),
Some(e),
vec![],
)))
})?;
if target_body_string == known_body_string {
return Ok((FactualStmtSuccess::new_with_verified_by_known_fact(
exist_fact.clone().into(),
VerifiedByResult::cited_fact(
exist_fact.clone().into(),
known_fact.clone().into(),
None,
),
Vec::new(),
))
.into());
}
}
}
Ok((StmtUnknown::new()).into())
}
fn known_exist_lookup_keys(goal: &ExistFactEnum) -> Vec<String> {
let mut keys = vec![goal.key()];
if let ExistFactEnum::ExistFact(body) = goal {
keys.push(ExistFactEnum::ExistUniqueFact(body.clone()).key());
}
keys.sort();
keys.dedup();
keys
}
fn exist_fact_normalized_body_string(
runtime: &Runtime,
exist_fact: &ExistFactEnum,
) -> Result<String, RuntimeError> {
let mut param_to_arg_map: HashMap<String, Obj> = HashMap::new();
let mut normalized_params: Vec<ParamGroupWithParamType> = Vec::new();
let mut param_index: usize = 0;
for param_def_with_type in exist_fact.params_def_with_type().groups.iter() {
let mut new_param_names: Vec<String> = Vec::new();
for original_name in param_def_with_type.params.iter() {
let normalized_name = format!("#{}", param_index);
param_index += 1;
param_to_arg_map.insert(
original_name.clone(),
obj_for_bound_param_in_scope(normalized_name.clone(), ParamObjType::Exist),
);
new_param_names.push(normalized_name);
}
let instantiated_param_type = runtime.inst_param_type(
¶m_def_with_type.param_type,
¶m_to_arg_map,
ParamObjType::Exist,
)?;
normalized_params.push(ParamGroupWithParamType::new(
new_param_names,
instantiated_param_type,
));
}
let instantiated_exist_fact =
runtime.inst_exist_fact(exist_fact, ¶m_to_arg_map, ParamObjType::Exist, None)?;
let mut fact_strings: Vec<String> = Vec::new();
for fact in instantiated_exist_fact.facts().iter() {
let fact_as_fact = fact.from_ref_to_cloned_fact();
fact_strings.push(fact_as_fact.to_string());
}
let mut params_string_parts: Vec<String> = Vec::new();
for param_def_with_type in normalized_params.iter() {
params_string_parts.push(format!(
"{} {}",
param_def_with_type.params.join(","),
param_def_with_type.param_type
));
}
let params_string = params_string_parts.join("; ");
let facts_string = fact_strings.join("; ");
Ok(format!("{} || {}", params_string, facts_string))
}
}
fn stmt_result_infers(result: &StmtResult) -> InferResult {
match result {
StmtResult::FactualStmtSuccess(x) => x.infers.clone(),
StmtResult::NonFactualStmtSuccess(x) => x.infers.clone(),
StmtResult::StmtUnknown(_) => InferResult::new(),
}
}