use crate::prelude::*;
use std::collections::HashMap;
impl Runtime {
fn verify_obj_well_defined_from_cache_if_known(&self, obj: &Obj) -> Option<()> {
let key = obj.to_string();
if self.cache_well_defined_obj_contains(&key) {
Some(())
} else {
None
}
}
pub fn verify_obj_well_defined_and_store_cache(
&mut self,
obj: &Obj,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
if self
.verify_obj_well_defined_from_cache_if_known(obj)
.is_some()
{
return Ok(());
}
match obj {
Obj::Atom(AtomObj::Identifier(identifier)) => {
self.verify_identifier_well_defined(identifier)
}
Obj::Atom(AtomObj::IdentifierWithMod(x)) => {
self.verify_identifier_with_mod_well_defined(x)
}
Obj::FnObj(fn_obj) => self.verify_fn_obj_well_defined(fn_obj, verify_state),
Obj::Number(_) => Ok(()),
Obj::Add(add) => self.verify_add_well_defined(add, verify_state),
Obj::Sub(sub) => self.verify_sub_well_defined(sub, verify_state),
Obj::Mul(mul) => self.verify_mul_well_defined(mul, verify_state),
Obj::Div(div) => self.verify_div_well_defined(div, verify_state),
Obj::Mod(m) => self.verify_mod_well_defined(m, verify_state),
Obj::Pow(pow) => self.verify_pow_well_defined(pow, verify_state),
Obj::Abs(abs) => self.verify_abs_well_defined(abs, verify_state),
Obj::Log(log) => self.verify_log_well_defined(log, verify_state),
Obj::Max(max) => self.verify_max_well_defined(max, verify_state),
Obj::Min(min) => self.verify_min_well_defined(min, verify_state),
Obj::Union(x) => self.verify_union_well_defined(x, verify_state),
Obj::Intersect(x) => self.verify_intersect_well_defined(x, verify_state),
Obj::SetMinus(x) => self.verify_set_minus_well_defined(x, verify_state),
Obj::SetDiff(x) => self.verify_set_diff_well_defined(x, verify_state),
Obj::Cup(x) => self.verify_cup_well_defined(x, verify_state),
Obj::Cap(x) => self.verify_cap_well_defined(x, verify_state),
Obj::ListSet(x) => self.verify_list_set_well_defined(x, verify_state),
Obj::SetBuilder(x) => {
self.run_in_local_env(|rt| rt.verify_set_builder_well_defined(x, verify_state))
}
Obj::FnSet(x) => {
self.run_in_local_env(|rt| rt.verify_fn_set_well_defined(x, verify_state))
}
Obj::AnonymousFn(x) => self.verify_anonymous_fn_well_defined(x, verify_state),
Obj::StandardSet(StandardSet::NPos) => self.verify_n_pos_obj_well_defined(),
Obj::StandardSet(StandardSet::N) => self.verify_n_obj_well_defined(),
Obj::StandardSet(StandardSet::Q) => self.verify_q_obj_well_defined(),
Obj::StandardSet(StandardSet::Z) => self.verify_z_obj_well_defined(),
Obj::StandardSet(StandardSet::R) => self.verify_r_obj_well_defined(),
Obj::Cart(x) => self.verify_cart_well_defined(x, verify_state),
Obj::CartDim(x) => self.verify_cart_dim_well_defined(x, verify_state),
Obj::Proj(x) => self.verify_proj_well_defined(x, verify_state),
Obj::TupleDim(x) => self.verify_dim_well_defined(x, verify_state),
Obj::Tuple(x) => self.verify_tuple_well_defined(x, verify_state),
Obj::Count(x) => self.verify_count_well_defined(x, verify_state),
Obj::Sum(x) => self.verify_sum_obj_well_defined(x, verify_state),
Obj::Product(x) => self.verify_product_obj_well_defined(x, verify_state),
Obj::Range(x) => self.verify_range_well_defined(x, verify_state),
Obj::ClosedRange(x) => self.verify_closed_range_well_defined(x, verify_state),
Obj::FiniteSeqSet(x) => self.verify_finite_seq_set_well_defined(x, verify_state),
Obj::SeqSet(x) => self.verify_seq_set_well_defined(x, verify_state),
Obj::FiniteSeqListObj(x) => {
self.verify_finite_seq_list_obj_well_defined(x, verify_state)
}
Obj::MatrixSet(x) => self.verify_matrix_set_well_defined(x, verify_state),
Obj::MatrixListObj(x) => self.verify_matrix_list_obj_well_defined(x, verify_state),
Obj::MatrixAdd(x) => self.verify_matrix_add_well_defined(x, verify_state),
Obj::MatrixSub(x) => self.verify_matrix_sub_well_defined(x, verify_state),
Obj::MatrixMul(x) => self.verify_matrix_mul_well_defined(x, verify_state),
Obj::MatrixScalarMul(x) => self.verify_matrix_scalar_mul_well_defined(x, verify_state),
Obj::MatrixPow(x) => self.verify_matrix_pow_well_defined(x, verify_state),
Obj::PowerSet(x) => self.verify_power_set_well_defined(x, verify_state),
Obj::Choose(x) => self.verify_choose_well_defined(x, verify_state),
Obj::ObjAtIndex(x) => self.verify_obj_at_index_well_defined(x, verify_state),
Obj::StandardSet(StandardSet::QPos) => self.verify_q_pos_well_defined(),
Obj::StandardSet(StandardSet::RPos) => self.verify_r_pos_well_defined(),
Obj::StandardSet(StandardSet::QNeg) => self.verify_q_neg_well_defined(),
Obj::StandardSet(StandardSet::ZNeg) => self.verify_z_neg_well_defined(),
Obj::StandardSet(StandardSet::RNeg) => self.verify_r_neg_well_defined(),
Obj::StandardSet(StandardSet::QNz) => self.verify_q_nz_well_defined(),
Obj::StandardSet(StandardSet::ZNz) => self.verify_z_nz_well_defined(),
Obj::StandardSet(StandardSet::RNz) => self.verify_r_nz_well_defined(),
Obj::FamilyObj(family) => {
self.verify_param_type_family_well_defined(family, verify_state)
}
Obj::StructObj(struct_obj) => {
self.verify_struct_obj_well_defined(struct_obj, verify_state)
}
Obj::ObjAsStructInstanceWithFieldAccess(field_access) => self
.verify_obj_as_struct_instance_with_field_access_well_defined(
field_access,
verify_state,
),
Obj::Atom(AtomObj::Forall(_)) => Ok(()),
Obj::Atom(AtomObj::Def(_)) => Ok(()),
Obj::Atom(AtomObj::Exist(_)) => Ok(()),
Obj::Atom(AtomObj::SetBuilder(_)) => Ok(()),
Obj::Atom(AtomObj::FnSet(_)) => Ok(()),
Obj::Atom(AtomObj::Induc(_)) => Ok(()),
Obj::Atom(AtomObj::DefAlgo(_)) => Ok(()),
Obj::Atom(AtomObj::DefStructField(_)) => Ok(()),
}?;
self.store_well_defined_obj_cache(obj);
Ok(())
}
fn verify_identifier_well_defined(&self, identifier: &Identifier) -> Result<(), RuntimeError> {
if self.is_name_used_for_identifier(&identifier.name) {
Ok(())
} else if self
.get_struct_definition_by_name(&identifier.name)
.is_some()
{
Ok(())
} else {
Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"identifier `{}` not defined",
identifier.to_string()
)),
)))
}
}
fn verify_identifier_with_mod_well_defined(
&self,
x: &IdentifierWithMod,
) -> Result<(), RuntimeError> {
let _ = x;
unreachable!()
}
fn verify_fn_obj_well_defined(
&mut self,
fn_obj: &FnObj,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
let mut space = match fn_obj.head.as_ref() {
FnObjHead::AnonymousFnLiteral(a) => {
self.verify_anonymous_fn_well_defined(a.as_ref(), verify_state)
.map_err(|well_defined_error| {
RuntimeError::from(WellDefinedRuntimeError(RuntimeErrorStruct::new_with_msg_and_cause(format!(
"object {} is not well-defined: anonymous function head is not well-defined",
fn_obj.to_string()
), well_defined_error)))
})?;
FnSetSpace::Anon((**a).clone())
}
FnObjHead::FiniteSeqListObj(list) => {
for obj in list.objs.iter() {
self.verify_obj_well_defined_and_store_cache(obj, verify_state)?;
}
if fn_obj.body.len() != 1 || fn_obj.body[0].len() != 1 {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"finite sequence literal function {} expects one argument",
fn_obj.head
)),
)));
}
let index_obj = fn_obj.body[0][0].as_ref().clone();
self.verify_obj_well_defined_and_store_cache(&index_obj, verify_state)?;
let index_in_n_pos: AtomicFact = InFact::new(
index_obj.clone(),
StandardSet::NPos.into(),
default_line_file(),
)
.into();
let index_in_n_pos_result =
self.verify_atomic_fact(&index_in_n_pos, verify_state)?;
if index_in_n_pos_result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"index {} is not a positive integer",
index_obj
)),
)));
}
let list_len_obj: Obj = Number::new(list.objs.len().to_string()).into();
let index_not_larger_than_list_len: AtomicFact = LessEqualFact::new(
index_obj.clone(),
list_len_obj.clone(),
default_line_file(),
)
.into();
let index_not_larger_than_list_len_result =
self.verify_atomic_fact(&index_not_larger_than_list_len, verify_state)?;
if index_not_larger_than_list_len_result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"{} <= {} is unknown",
index_obj, list_len_obj
)),
)));
}
return Ok(());
}
_ => {
let function_name_obj: Obj = (*fn_obj.head).clone().into();
let body = self
.get_object_in_fn_set_or_restrict(&function_name_obj)
.ok_or_else(|| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(todo_error_message(format!(
"`{}` is not a defined function",
fn_obj.head.to_string()
))),
))
})?
.clone();
FnSetSpace::Set(FnSet::from_body(body)?)
}
};
for (i, args) in fn_obj.body.iter().enumerate() {
self.verify_fn_obj_well_defined_against_fn_like_space(
args,
space.params(),
space.dom(),
space.binding(),
verify_state,
)
.map_err(|well_defined_error| {
RuntimeError::from(WellDefinedRuntimeError(RuntimeErrorStruct::new_with_msg_and_cause(format!(
"object {} is not well-defined, failed to verify arguments satisfy function domain.",
fn_obj.to_string()
), well_defined_error)))
})?;
let set_where_the_next_fn_obj_is_in = space.ret_set_obj();
let fn_obj_prefix_body: Vec<Vec<Box<Obj>>> =
fn_obj.body[..=i].iter().cloned().collect();
let fn_obj_prefix_as_obj: Obj =
FnObj::new(*fn_obj.head.clone(), fn_obj_prefix_body).into();
let intermediate_in_fact = InFact::new(
fn_obj_prefix_as_obj,
set_where_the_next_fn_obj_is_in,
default_line_file(),
);
let intermediate_atomic_fact = AtomicFact::InFact(intermediate_in_fact);
let intermediate_line_file = intermediate_atomic_fact.line_file();
let intermediate_fact_string = intermediate_atomic_fact.to_string();
self.top_level_env()
.store_atomic_fact(intermediate_atomic_fact)
.map_err(|store_fact_error| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!(
"failed to store intermediate fn-obj membership fact while verifying `{}`",
fn_obj.to_string()
),
store_fact_error,
),
))
})?;
self.top_level_env()
.store_fact_to_cache_known_fact(intermediate_fact_string, intermediate_line_file)
.map_err(|store_fact_error| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!(
"failed to store intermediate fn-obj membership fact while verifying `{}`",
fn_obj.to_string()
),
store_fact_error,
),
))
})?;
if i == fn_obj.body.len() - 1 {
break;
}
space = FnSetSpace::from_ret_obj(space.ret_set_obj())?;
}
Ok(())
}
fn verify_fn_obj_well_defined_against_fn_like_space(
&mut self,
args: &Vec<Box<Obj>>,
params_def_with_set: &Vec<ParamGroupWithSet>,
dom_facts: &Vec<OrAndChainAtomicFact>,
param_binding: ParamObjType,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
let param_count = ParamGroupWithSet::number_of_params(params_def_with_set);
if args.len() != param_count {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"number of args ({}) does not match fn set with dom param count ({})",
args.len(),
param_count
)),
)));
}
for arg in args.iter() {
self.verify_obj_well_defined_and_store_cache(arg, verify_state)?;
}
let mut args_as_obj: Vec<Obj> = Vec::with_capacity(args.len());
for arg in args.iter() {
args_as_obj.push((**arg).clone());
}
self.verify_args_satisfy_fn_param_groups(
params_def_with_set,
&args_as_obj,
param_binding,
verify_state,
)?;
let param_to_arg_map = ParamGroupWithSet::param_defs_and_args_to_param_to_arg_map(
params_def_with_set,
&args_as_obj,
);
for dom_fact in dom_facts.iter() {
let instantiated_dom_fact = self
.inst_or_and_chain_atomic_fact(dom_fact, ¶m_to_arg_map, param_binding, None)
.map_err(|e| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!("failed to instantiate function domain fact: {}", e),
e,
),
))
})?;
let verify_result = self
.verify_or_and_chain_atomic_fact(&instantiated_dom_fact, verify_state)
.map_err(|verify_error| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!(
"failed to verify function domain fact:\n{}",
instantiated_dom_fact
),
verify_error,
),
))
})?;
if verify_result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"failed to verify function domain fact:\n{}",
instantiated_dom_fact
)),
)));
}
}
Ok(())
}
fn verify_args_satisfy_fn_param_groups(
&mut self,
params_def_with_set: &Vec<ParamGroupWithSet>,
args_as_obj: &Vec<Obj>,
param_binding: ParamObjType,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
let mut param_to_arg_map: HashMap<String, Obj> = HashMap::new();
let mut arg_index: usize = 0;
for param_def in params_def_with_set.iter() {
let param_type = if arg_index != 0 {
ParamType::Obj(self.inst_obj(
param_def.set_obj(),
¶m_to_arg_map,
param_binding,
)?)
} else {
ParamType::Obj(param_def.set_obj().clone())
};
for param_name in param_def.params.iter() {
let arg = args_as_obj[arg_index].clone();
let verify_result = self
.verify_obj_satisfies_param_type(arg.clone(), ¶m_type, verify_state)
.map_err(|verify_error| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!(
"failed to verify arg `{}` satisfy fn parameter type {}",
arg, param_type
),
verify_error,
),
))
})?;
if verify_result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"arg `{}` does not satisfy fn parameter type {}",
arg, param_type
)),
)));
}
param_to_arg_map.insert(param_name.clone(), arg);
arg_index += 1;
}
}
Ok(())
}
fn require_obj_in_r(
&mut self,
obj: &Obj,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
if let Obj::Abs(a) = obj {
return self.require_obj_in_r(&a.arg, verify_state);
}
if let Obj::Max(m) = obj {
self.require_obj_in_r(&m.left, verify_state)?;
return self.require_obj_in_r(&m.right, verify_state);
}
if let Obj::Min(m) = obj {
self.require_obj_in_r(&m.left, verify_state)?;
return self.require_obj_in_r(&m.right, verify_state);
}
if let Obj::Log(l) = obj {
self.require_obj_in_r(&l.base, verify_state)?;
return self.require_obj_in_r(&l.arg, verify_state);
}
let r_obj = StandardSet::R.into();
let element = obj.clone();
let in_fact = InFact::new(element, r_obj, default_line_file());
let atomic_fact = AtomicFact::InFact(in_fact);
let result = self.verify_atomic_fact(&atomic_fact, verify_state)?;
if result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"obj {} is not in r",
obj.to_string()
)),
)));
}
Ok(())
}
fn require_obj_in_z(
&mut self,
obj: &Obj,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
let z_obj = StandardSet::Z.into();
let element = obj.clone();
let in_fact = InFact::new(element, z_obj, default_line_file());
let atomic_fact = AtomicFact::InFact(in_fact);
let result = self.verify_atomic_fact(&atomic_fact, verify_state)?;
if result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"obj {} is not in z",
obj.to_string()
)),
)));
}
Ok(())
}
fn require_less_equal_verified(
&mut self,
left: &Obj,
right: &Obj,
verify_state: &VerifyState,
err_detail: String,
) -> Result<(), RuntimeError> {
let f: AtomicFact =
LessEqualFact::new(left.clone(), right.clone(), default_line_file()).into();
let r = self.verify_atomic_fact(&f, verify_state)?;
if r.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(err_detail),
)));
}
Ok(())
}
fn range_endpoints_are_numeric_for_interval_order_check(&self, start: &Obj, end: &Obj) -> bool {
self.resolve_obj_to_number(start).is_some() && self.resolve_obj_to_number(end).is_some()
}
fn verify_add_well_defined(
&mut self,
add: &Add,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&add.left, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&add.right, verify_state)?;
self.require_obj_in_r(&add.left, verify_state)?;
self.require_obj_in_r(&add.right, verify_state)?;
Ok(())
}
fn verify_sub_well_defined(
&mut self,
sub: &Sub,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&sub.left, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&sub.right, verify_state)?;
self.require_obj_in_r(&sub.left, verify_state)?;
self.require_obj_in_r(&sub.right, verify_state)?;
Ok(())
}
fn verify_mul_well_defined(
&mut self,
mul: &Mul,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&mul.left, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&mul.right, verify_state)?;
self.require_obj_in_r(&mul.left, verify_state)?;
self.require_obj_in_r(&mul.right, verify_state)?;
Ok(())
}
fn verify_div_well_defined(
&mut self,
div: &Div,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&div.left, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&div.right, verify_state)?;
let zero: Obj = Number::new("0".to_string()).into();
let not_equal_fact = NotEqualFact::new((*div.right).clone(), zero, default_line_file());
let atomic_fact = AtomicFact::NotEqualFact(not_equal_fact);
let result = self.verify_atomic_fact(&atomic_fact, verify_state)?;
if result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"divisor `{}` must be non-zero",
div.right.to_string()
)),
)));
}
self.require_obj_in_r(&div.left, verify_state)?;
self.require_obj_in_r(&div.right, verify_state)?;
Ok(())
}
fn verify_mod_well_defined(
&mut self,
m: &Mod,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&m.left, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&m.right, verify_state)?;
self.require_obj_in_z(&m.left, verify_state)?;
self.require_obj_in_z(&m.right, verify_state)?;
let zero: Obj = Number::new("0".to_string()).into();
let not_equal_fact = NotEqualFact::new((*m.right).clone(), zero, default_line_file());
let atomic_fact = AtomicFact::NotEqualFact(not_equal_fact);
let result = self.verify_atomic_fact(&atomic_fact, verify_state)?;
if result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"modulus `{}` must be non-zero",
m.right.to_string()
)),
)));
}
Ok(())
}
fn verify_abs_well_defined(
&mut self,
abs: &Abs,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&abs.arg, verify_state)?;
self.require_obj_in_r(&abs.arg, verify_state)?;
Ok(())
}
fn verify_log_well_defined(
&mut self,
log: &Log,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&log.base, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&log.arg, verify_state)?;
self.require_obj_in_r(&log.base, verify_state)?;
self.require_obj_in_r(&log.arg, verify_state)?;
let zero: Obj = Number::new("0".to_string()).into();
let one: Obj = Number::new("1".to_string()).into();
let lf = default_line_file();
let checks: [(&str, AtomicFact); 3] = [
(
"log: base must be > 0",
GreaterFact::new((*log.base).clone(), zero.clone(), lf.clone()).into(),
),
(
"log: argument must be > 0",
GreaterFact::new((*log.arg).clone(), zero.clone(), lf.clone()).into(),
),
(
"log: base must be != 1",
NotEqualFact::new((*log.base).clone(), one, lf.clone()).into(),
),
];
for (msg, atomic) in checks {
let result = self.verify_atomic_fact(&atomic, verify_state)?;
if result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_line_file(msg.to_string(), lf.clone()),
)));
}
}
Ok(())
}
fn verify_max_well_defined(
&mut self,
max: &Max,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&max.left, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&max.right, verify_state)?;
self.require_obj_in_r(&max.left, verify_state)?;
self.require_obj_in_r(&max.right, verify_state)?;
Ok(())
}
fn verify_min_well_defined(
&mut self,
min: &Min,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&min.left, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&min.right, verify_state)?;
self.require_obj_in_r(&min.left, verify_state)?;
self.require_obj_in_r(&min.right, verify_state)?;
Ok(())
}
fn verify_pow_well_defined(
&mut self,
pow: &Pow,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&pow.base, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&pow.exponent, verify_state)?;
let zero_obj: Obj = Number::new("0".to_string()).into();
let positive_base_and_real_exponent = AndChainAtomicFact::AndFact(AndFact::new(
vec![
GreaterFact::new((*pow.base).clone(), zero_obj.clone(), default_line_file()).into(),
InFact::new(
(*pow.exponent).clone(),
StandardSet::R.into(),
default_line_file(),
)
.into(),
],
default_line_file(),
));
let result =
self.verify_and_chain_atomic_fact(&positive_base_and_real_exponent, verify_state)?;
if result.is_true() {
return Ok(());
}
let zero_base_and_positive_real_exponent = AndChainAtomicFact::AndFact(AndFact::new(
vec![
EqualFact::new((*pow.base).clone(), zero_obj.clone(), default_line_file()).into(),
InFact::new(
(*pow.exponent).clone(),
StandardSet::R.into(),
default_line_file(),
)
.into(),
GreaterFact::new(
(*pow.exponent).clone(),
zero_obj.clone(),
default_line_file(),
)
.into(),
],
default_line_file(),
));
let result =
self.verify_and_chain_atomic_fact(&zero_base_and_positive_real_exponent, verify_state)?;
if result.is_true() {
return Ok(());
}
let nonzero_base_integer_exponent = AndChainAtomicFact::AndFact(AndFact::new(
vec![
InFact::new(
(*pow.exponent).clone(),
StandardSet::Z.into(),
default_line_file(),
)
.into(),
NotEqualFact::new((*pow.base).clone(), zero_obj.clone(), default_line_file())
.into(),
],
default_line_file(),
));
let exponent_in_n_pos = AndChainAtomicFact::AtomicFact(
InFact::new(
(*pow.exponent).clone(),
StandardSet::NPos.into(),
default_line_file(),
)
.into(),
);
let pow_domain_or_fact = OrFact::new(
vec![
positive_base_and_real_exponent,
zero_base_and_positive_real_exponent,
nonzero_base_integer_exponent,
exponent_in_n_pos,
],
default_line_file(),
);
let result = self.verify_or_fact(&pow_domain_or_fact, verify_state)?;
if result.is_true() {
return Ok(());
}
let pow_display = Obj::Pow(pow.clone()).to_string();
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"base and exponent do not satisfy the pow domain: {}",
pow_display
)),
)));
}
fn verify_union_well_defined(
&mut self,
x: &Union,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&x.left, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&x.right, verify_state)?;
Ok(())
}
fn verify_intersect_well_defined(
&mut self,
x: &Intersect,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&x.left, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&x.right, verify_state)?;
Ok(())
}
fn verify_set_minus_well_defined(
&mut self,
x: &SetMinus,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&x.left, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&x.right, verify_state)?;
Ok(())
}
fn verify_set_diff_well_defined(
&mut self,
x: &SetDiff,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&x.left, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&x.right, verify_state)?;
Ok(())
}
fn verify_cup_well_defined(
&mut self,
x: &Cup,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&x.left, verify_state)?;
Ok(())
}
fn verify_cap_well_defined(
&mut self,
x: &Cap,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&x.left, verify_state)?;
Ok(())
}
fn verify_list_set_well_defined(
&mut self,
x: &ListSet,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
for obj in &x.list {
self.verify_obj_well_defined_and_store_cache(obj, verify_state)?;
}
let next_verify_state = verify_state.make_state_with_req_ok_set_to_true();
let len = x.list.len();
let mut i = 0;
while i < len {
let left_obj = match x.list.get(i) {
Some(left_obj) => (**left_obj).clone(),
None => break,
};
let mut j = i + 1;
while j < len {
let right_obj = match x.list.get(j) {
Some(right_obj) => (**right_obj).clone(),
None => break,
};
let not_equal_atomic_fact =
NotEqualFact::new(left_obj.clone(), right_obj, default_line_file()).into();
let verify_result = self
.verify_atomic_fact(¬_equal_atomic_fact, &next_verify_state)
.map_err(|previous_error| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!(
"failed to verify list set elements are pairwise not equal: {}",
not_equal_atomic_fact
),
previous_error,
),
))
})?;
if verify_result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(RuntimeErrorStruct::new_with_just_msg(format!("list set elements must be pairwise not equal, but it is not provable: {}", not_equal_atomic_fact)))));
}
j += 1;
}
i += 1;
}
Ok(())
}
fn verify_set_builder_well_defined(
&mut self,
x: &SetBuilder,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.run_in_local_env(|rt| {
if let Err(well_defined_error) = rt
.verify_obj_well_defined_and_store_cache(&x.param_set, &VerifyState::new(0, false))
{
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!(
"failed to verify well-defined of set builder {}",
x.to_string()
),
well_defined_error,
),
)));
}
if let Err(e) =
rt.store_free_param_or_identifier_name(&x.param, ParamObjType::SetBuilder)
{
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!(
"failed to verify well-defined of set builder {}",
x.to_string()
),
e,
),
)));
}
let param_in_set: Fact = InFact::new(
obj_for_bound_param_in_scope(x.param.clone(), ParamObjType::SetBuilder),
(*x.param_set).clone(),
default_line_file(),
)
.into();
if let Err(e) =
rt.verify_well_defined_and_store_and_infer_with_default_verify_state(param_in_set)
{
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!(
"failed to verify well-defined of set builder {}",
x.to_string()
),
e,
),
)));
}
for fact in x.facts.iter() {
if let Err(e) = rt.verify_or_and_chain_atomic_fact_well_defined_and_store_and_infer(
fact,
verify_state,
) {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!(
"failed to verify well-defined of set builder {}",
x.to_string()
),
e,
),
)));
}
}
Ok(())
})
}
fn verify_fn_set_well_defined(
&mut self,
x: &FnSet,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
for param_def_with_set in x.body.params_def_with_set.iter() {
if let Err(e) = self.define_params_with_set(param_def_with_set) {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!(
"failed to verify well-defined of fn set with dom {}",
x.to_string()
),
e,
),
)));
}
}
for fact in x.body.dom_facts.iter() {
if let Err(e) = self.verify_or_and_chain_atomic_fact_well_defined_and_store_and_infer(
fact,
verify_state,
) {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!(
"failed to verify well-defined of fn set with dom {}",
x.to_string()
),
e,
),
)));
}
}
if let Err(e) = self.verify_obj_well_defined_and_store_cache(&x.body.ret_set, verify_state)
{
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!(
"failed to verify well-defined of fn set with dom {}",
x.to_string()
),
e,
),
)));
}
Ok(())
}
fn verify_anonymous_fn_well_defined(
&mut self,
x: &AnonymousFn,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.run_in_local_env(|rt| {
for param_def_with_set in x.body.params_def_with_set.iter() {
if let Err(e) =
rt.define_params_with_set_in_scope(param_def_with_set, ParamObjType::FnSet)
{
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!(
"failed to verify well-defined of anonymous fn {}",
x.to_string()
),
e,
),
)));
}
}
for fact in x.body.dom_facts.iter() {
if let Err(e) = rt.verify_or_and_chain_atomic_fact_well_defined_and_store_and_infer(
fact,
verify_state,
) {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!(
"failed to verify well-defined of anonymous fn {}",
x.to_string()
),
e,
),
)));
}
}
if let Err(e) =
rt.verify_obj_well_defined_and_store_cache(&x.body.ret_set, verify_state)
{
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!(
"failed to verify well-defined of anonymous fn {}",
x.to_string()
),
e,
),
)));
}
if let Err(e) = rt.verify_obj_well_defined_and_store_cache(&x.equal_to, verify_state) {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!(
"failed to verify well-defined of anonymous fn {}",
x.to_string()
),
e,
),
)));
}
Ok(())
})
}
fn verify_n_pos_obj_well_defined(&mut self) -> Result<(), RuntimeError> {
Ok(())
}
fn verify_n_obj_well_defined(&mut self) -> Result<(), RuntimeError> {
Ok(())
}
fn verify_q_obj_well_defined(&self) -> Result<(), RuntimeError> {
Ok(())
}
fn verify_z_obj_well_defined(&self) -> Result<(), RuntimeError> {
Ok(())
}
fn verify_r_obj_well_defined(&self) -> Result<(), RuntimeError> {
Ok(())
}
fn verify_cart_well_defined(
&mut self,
x: &Cart,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
for obj in &x.args {
self.verify_obj_well_defined_and_store_cache(obj, verify_state)?;
}
Ok(())
}
fn verify_cart_dim_well_defined(
&mut self,
x: &CartDim,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&x.set, verify_state)?;
let is_cart_fact = IsCartFact::new((*x.set).clone(), default_line_file()).into();
let result = self.verify_atomic_fact(&is_cart_fact, verify_state)?;
if result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"set {} is not a cart",
x.set.to_string()
)),
)));
}
Ok(())
}
fn verify_proj_well_defined(
&mut self,
x: &Proj,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&x.set, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&x.dim, verify_state)?;
let projection_dimension_number = self.resolve_obj_to_number(&x.dim).ok_or_else(|| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"projection dimension {} is not a number",
x.dim
)),
))
})?;
let projection_dimension_obj: Obj =
Number::new(projection_dimension_number.normalized_value).into();
let projection_dimension_is_positive_integer_fact = InFact::new(
projection_dimension_obj.clone(),
StandardSet::NPos.into(),
default_line_file(),
)
.into();
let projection_dimension_is_positive_integer_result =
self.verify_atomic_fact(&projection_dimension_is_positive_integer_fact, verify_state)?;
if projection_dimension_is_positive_integer_result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"projection dimension {} is not a positive integer",
projection_dimension_obj
)),
)));
}
let left_set_is_cart_fact = IsCartFact::new((*x.set).clone(), default_line_file()).into();
let left_set_is_cart_result =
self.verify_atomic_fact(&left_set_is_cart_fact, verify_state)?;
if left_set_is_cart_result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"projection left side {} is not a cart",
x.set
)),
)));
}
let left_set_cart_dim_obj: Obj = CartDim::new((*x.set).clone()).into();
let proj_index_not_larger_than_cart_dim = LessEqualFact::new(
projection_dimension_obj.clone(),
left_set_cart_dim_obj.clone(),
default_line_file(),
)
.into();
let left_set_cart_dim_less_equal_projection_dimension_result =
self.verify_atomic_fact(&proj_index_not_larger_than_cart_dim, verify_state)?;
if left_set_cart_dim_less_equal_projection_dimension_result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"{} <= {} is unknown",
projection_dimension_obj, left_set_cart_dim_obj
)),
)));
}
Ok(())
}
fn verify_dim_well_defined(
&mut self,
x: &TupleDim,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&x.arg, verify_state)?;
let is_tuple_fact = IsTupleFact::new((*x.arg).clone(), default_line_file()).into();
let result = self.verify_atomic_fact(&is_tuple_fact, verify_state)?;
if result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"`{}` is unknown, `dim` object requires its argument to be a tuple",
is_tuple_fact
)),
)));
}
Ok(())
}
fn verify_tuple_well_defined(
&mut self,
x: &Tuple,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
for obj in &x.args {
self.verify_obj_well_defined_and_store_cache(obj, verify_state)?;
}
Ok(())
}
fn verify_count_well_defined(
&mut self,
x: &Count,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
let is_finite_set_fact = IsFiniteSetFact::new((*x.set).clone(), default_line_file()).into();
let result = self.verify_atomic_fact(&is_finite_set_fact, verify_state)?;
if result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"set {} is not a finite set",
x.set.to_string()
)),
)));
}
Ok(())
}
fn verify_sum_obj_well_defined(
&mut self,
x: &Sum,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&x.start, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&x.end, verify_state)?;
self.require_obj_in_z(&x.start, verify_state)?;
self.require_obj_in_z(&x.end, verify_state)?;
if self.range_endpoints_are_numeric_for_interval_order_check(&x.start, &x.end) {
self.require_less_equal_verified(
&x.start,
&x.end,
verify_state,
"sum: cannot verify start <= end for the summation range".to_string(),
)?;
}
self.verify_obj_well_defined_and_store_cache(&x.func, verify_state)?;
self.verify_iterated_op_summand_under_integer_index_interval(
&x.func,
x.start.as_ref(),
x.end.as_ref(),
verify_state,
"sum",
)
}
fn verify_product_obj_well_defined(
&mut self,
x: &Product,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&x.start, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&x.end, verify_state)?;
self.require_obj_in_z(&x.start, verify_state)?;
self.require_obj_in_z(&x.end, verify_state)?;
if self.range_endpoints_are_numeric_for_interval_order_check(&x.start, &x.end) {
self.require_less_equal_verified(
&x.start,
&x.end,
verify_state,
"product: cannot verify start <= end for the product range".to_string(),
)?;
}
self.verify_obj_well_defined_and_store_cache(&x.func, verify_state)?;
self.verify_iterated_op_summand_under_integer_index_interval(
&x.func,
x.start.as_ref(),
x.end.as_ref(),
verify_state,
"product",
)
}
fn unary_param_set_from_params_def(
params_def: &[ParamGroupWithSet],
pname: &str,
) -> Option<Obj> {
for g in params_def {
if g.params.iter().any(|n| n == pname) {
return Some(g.set_obj().clone());
}
}
None
}
fn verify_closed_range_each_integer_satisfies_unary_param_set(
&mut self,
start: &Obj,
end: &Obj,
param_set: &Obj,
verify_state: &VerifyState,
op: &str,
) -> Result<(), RuntimeError> {
let Some(a_num) = self.resolve_obj_to_number(start) else {
return Ok(());
};
let Some(b_num) = self.resolve_obj_to_number(end) else {
return Ok(());
};
let as_ = a_num.normalized_value.trim();
let bs = b_num.normalized_value.trim();
if !is_number_string_literally_integer_without_dot(as_.to_string())
|| !is_number_string_literally_integer_without_dot(bs.to_string())
{
return Ok(());
}
let Some(ai) = as_.parse::<i128>().ok() else {
return Ok(());
};
let Some(bi) = bs.parse::<i128>().ok() else {
return Ok(());
};
if ai > bi {
return Ok(());
}
for k in ai..=bi {
let k_obj: Obj = Number::new(k.to_string()).into();
let in_fact = InFact::new(k_obj, param_set.clone(), default_line_file());
let atomic_fact = AtomicFact::InFact(in_fact);
let result = self.verify_atomic_fact(&atomic_fact, verify_state)?;
if result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"{op}: each integer in the closed range from {} to {} must belong to the index parameter's type; not satisfied at index {}",
start, end, k
)),
)));
}
}
Ok(())
}
fn verify_iterated_op_summand_with_stored_fn_set_body(
&mut self,
fs_body: FnSetBody,
start: &Obj,
end: &Obj,
verify_state: &VerifyState,
op: &str,
) -> Result<(), RuntimeError> {
if ParamGroupWithSet::number_of_params(&fs_body.params_def_with_set) != 1 {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"{op}: the function in the function set must be unary (one index)"
)),
)));
}
let param_names = ParamGroupWithSet::collect_param_names(&fs_body.params_def_with_set);
let pname = param_names[0].clone();
let Some(param_set_for_index) =
Self::unary_param_set_from_params_def(&fs_body.params_def_with_set, &pname)
else {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"{op}: could not find index parameter in params_def_with_set"
)),
)));
};
self.verify_closed_range_each_integer_satisfies_unary_param_set(
start,
end,
¶m_set_for_index,
verify_state,
op,
)?;
let start_c = start.clone();
let end_c = end.clone();
self.run_in_local_env(|rt| {
for g in fs_body.params_def_with_set.iter() {
rt.define_params_with_set_in_scope(g, ParamObjType::FnSet)
.map_err(|e| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!(
"{op}: could not bind index parameter in local well-defined check"
),
e,
),
))
})?;
}
let k: Obj = Identifier::new(pname).into();
let le_lo = OrAndChainAtomicFact::AtomicFact(
LessEqualFact::new(start_c.clone(), k.clone(), default_line_file()).into(),
);
let le_hi = OrAndChainAtomicFact::AtomicFact(
LessEqualFact::new(k, end_c.clone(), default_line_file()).into(),
);
rt.store_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(le_lo)
.map_err(|e| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!("{op}: could not add lower bound in local check"),
e,
),
))
})?;
rt.store_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(le_hi)
.map_err(|e| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!("{op}: could not add upper bound in local check"),
e,
),
))
})?;
for df in fs_body.dom_facts.iter() {
rt.verify_or_and_chain_atomic_fact_well_defined_and_store_and_infer(
df,
verify_state,
)
.map_err(|e| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!("{op}: function set dom in local check failed"),
e,
),
))
})?;
}
rt.verify_obj_well_defined_and_store_cache(&fs_body.ret_set, verify_state)
.map_err(|e| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!("{op}: return set not well-defined on the integer range"),
e,
),
))
})
})
}
fn verify_iterated_op_summand_under_integer_index_interval(
&mut self,
func: &Obj,
start: &Obj,
end: &Obj,
verify_state: &VerifyState,
op: &str,
) -> Result<(), RuntimeError> {
if let Some(af) = Self::summand_as_unary_anonymous_fn(func) {
return self.verify_unary_iterated_anonymous_in_interval(
af,
start,
end,
verify_state,
op,
);
}
if let Obj::FnObj(fo) = func {
if !fo.body.is_empty() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"{op}: expected a bare function as summand, not a function application"
)),
)));
}
let function_name_obj: Obj = (*fo.head).clone().into();
let Some(fs_body) = self
.get_object_in_fn_set_or_restrict(&function_name_obj)
.cloned()
else {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"{op}: summand must be a unary anonymous function, or a name with a stored function set; got {}",
func
)),
)));
};
return self.verify_iterated_op_summand_with_stored_fn_set_body(
fs_body,
start,
end,
verify_state,
op,
);
}
if let Some(fs_body) = self.get_cloned_object_in_fn_set_or_restrict(func) {
return self.verify_iterated_op_summand_with_stored_fn_set_body(
fs_body,
start,
end,
verify_state,
op,
);
}
Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"{op}: summand must be a unary anonymous function, or a defined unary function in a function set; got {}",
func
)),
)))
}
fn summand_as_unary_anonymous_fn(obj: &Obj) -> Option<&AnonymousFn> {
match obj {
Obj::AnonymousFn(af) => Some(af),
Obj::FnObj(fo) => {
if !fo.body.is_empty() {
return None;
}
match fo.head.as_ref() {
FnObjHead::AnonymousFnLiteral(a) => Some(a.as_ref()),
_ => None,
}
}
_ => None,
}
}
fn verify_unary_iterated_anonymous_in_interval(
&mut self,
af: &AnonymousFn,
start: &Obj,
end: &Obj,
verify_state: &VerifyState,
op: &str,
) -> Result<(), RuntimeError> {
if ParamGroupWithSet::number_of_params(&af.body.params_def_with_set) != 1 {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"{op}: summation/product index function must be unary (one parameter)"
)),
)));
}
let param_names = ParamGroupWithSet::collect_param_names(&af.body.params_def_with_set);
let pname = param_names[0].clone();
let Some(param_set_for_index) =
Self::unary_param_set_from_params_def(&af.body.params_def_with_set, &pname)
else {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"{op}: could not find index parameter in params_def_with_set"
)),
)));
};
self.verify_closed_range_each_integer_satisfies_unary_param_set(
start,
end,
¶m_set_for_index,
verify_state,
op,
)?;
self.run_in_local_env(|rt| {
for g in af.body.params_def_with_set.iter() {
rt.define_params_with_set_in_scope(g, ParamObjType::FnSet)
.map_err(|e| {
RuntimeError::from(WellDefinedRuntimeError(RuntimeErrorStruct::new_with_msg_and_cause(format!("{op}: could not bind index parameter in local well-defined check"), e)))
})?;
}
let k: Obj = Identifier::new(pname).into();
let le_lo = OrAndChainAtomicFact::AtomicFact(
LessEqualFact::new(start.clone(), k.clone(), default_line_file()).into(),
);
let le_hi = OrAndChainAtomicFact::AtomicFact(
LessEqualFact::new(k, end.clone(), default_line_file()).into(),
);
rt.store_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(le_lo)
.map_err(|e| {
RuntimeError::from(WellDefinedRuntimeError(RuntimeErrorStruct::new_with_msg_and_cause(format!("{op}: could not add lower bound in local check"), e)))
})?;
rt.store_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(le_hi)
.map_err(|e| {
RuntimeError::from(WellDefinedRuntimeError(RuntimeErrorStruct::new_with_msg_and_cause(format!("{op}: could not add upper bound in local check"), e)))
})?;
for df in af.body.dom_facts.iter() {
rt.verify_or_and_chain_atomic_fact_well_defined_and_store_and_infer(
df,
verify_state,
)
.map_err(|e| {
RuntimeError::from(WellDefinedRuntimeError(RuntimeErrorStruct::new_with_msg_and_cause(format!("{op}: local dom of anonymous summand in integer range check failed"), e)))
})?;
}
rt.verify_obj_well_defined_and_store_cache(&af.body.ret_set, verify_state)
.map_err(|e| {
RuntimeError::from(WellDefinedRuntimeError(RuntimeErrorStruct::new_with_msg_and_cause(format!("{op}: return set not well-defined on the integer range"), e)))
})?;
rt.verify_obj_well_defined_and_store_cache(&af.equal_to, verify_state)
.map_err(|e| {
RuntimeError::from(WellDefinedRuntimeError(RuntimeErrorStruct::new_with_msg_and_cause(format!("{op}: expression body not well-defined on the integer range"), e)))
})
})
}
fn verify_range_well_defined(
&mut self,
x: &Range,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&x.start, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&x.end, verify_state)?;
self.require_obj_in_z(&x.start, verify_state)?;
self.require_obj_in_z(&x.end, verify_state)?;
if self.range_endpoints_are_numeric_for_interval_order_check(&x.start, &x.end) {
self.require_less_equal_verified(
&x.start,
&x.end,
verify_state,
format!(
"range: cannot verify {} <= {} (numeric half-open interval needs lower <= upper)",
x.start, x.end
),
)?;
}
Ok(())
}
fn verify_closed_range_well_defined(
&mut self,
x: &ClosedRange,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&x.start, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&x.end, verify_state)?;
self.require_obj_in_z(&x.start, verify_state)?;
self.require_obj_in_z(&x.end, verify_state)?;
if self.range_endpoints_are_numeric_for_interval_order_check(&x.start, &x.end) {
self.require_less_equal_verified(
&x.start,
&x.end,
verify_state,
format!(
"closed_range: cannot verify {} <= {} (numeric closed interval needs lower <= upper)",
x.start, x.end
),
)?;
}
Ok(())
}
fn verify_finite_seq_set_well_defined(
&mut self,
x: &FiniteSeqSet,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&x.set, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&x.n, verify_state)?;
let is_set_fact = IsSetFact::new((*x.set).clone(), default_line_file()).into();
let set_ok = self.verify_atomic_fact(&is_set_fact, verify_state)?;
if set_ok.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"finite_seq_set: first argument {} is not a set",
x.set
)),
)));
}
let n_in_n_pos = InFact::new(
(*x.n).clone(),
StandardSet::NPos.into(),
default_line_file(),
)
.into();
let n_ok = self.verify_atomic_fact(&n_in_n_pos, verify_state)?;
if n_ok.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"finite_seq_set: length argument {} is not verified in N_pos",
x.n
)),
)));
}
Ok(())
}
fn verify_seq_set_well_defined(
&mut self,
x: &SeqSet,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&x.set, verify_state)?;
let is_set_fact = IsSetFact::new((*x.set).clone(), default_line_file()).into();
let set_ok = self.verify_atomic_fact(&is_set_fact, verify_state)?;
if set_ok.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"seq: argument {} is not a set",
x.set
)),
)));
}
Ok(())
}
fn verify_finite_seq_list_obj_well_defined(
&mut self,
x: &FiniteSeqListObj,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
for o in x.objs.iter() {
self.verify_obj_well_defined_and_store_cache(o, verify_state)?;
}
Ok(())
}
fn verify_matrix_set_well_defined(
&mut self,
x: &MatrixSet,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&x.set, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&x.row_len, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&x.col_len, verify_state)?;
let is_set_fact = IsSetFact::new((*x.set).clone(), default_line_file()).into();
let set_ok = self.verify_atomic_fact(&is_set_fact, verify_state)?;
if set_ok.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"matrix: first argument {} is not a set",
x.set
)),
)));
}
for (label, len_obj) in [("row_len", &x.row_len), ("col_len", &x.col_len)] {
let in_n_pos = InFact::new(
(**len_obj).clone(),
StandardSet::NPos.into(),
default_line_file(),
)
.into();
let ok = self.verify_atomic_fact(&in_n_pos, verify_state)?;
if ok.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"matrix: {} argument {} is not verified in N_pos",
label, len_obj
)),
)));
}
}
Ok(())
}
fn verify_matrix_list_obj_well_defined(
&mut self,
x: &MatrixListObj,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
if !x.rows.is_empty() {
let col_len = x.rows[0].len();
for row in x.rows.iter() {
if row.len() != col_len {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"matrix literal: row length {} differs from first row length {}",
row.len(),
col_len
)),
)));
}
}
}
for row in x.rows.iter() {
for o in row.iter() {
self.verify_obj_well_defined_and_store_cache(o, verify_state)?;
}
}
Ok(())
}
fn verify_matrix_add_well_defined(
&mut self,
ma: &MatrixAdd,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&ma.left, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&ma.right, verify_state)?;
let shape_left = Self::matrix_value_shape(self, &ma.left)?;
let shape_right = Self::matrix_value_shape(self, &ma.right)?;
if shape_left != shape_right {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"matrix ++: shape {:?} and {:?} do not match",
shape_left, shape_right
)),
)));
}
Ok(())
}
fn verify_matrix_sub_well_defined(
&mut self,
ms: &MatrixSub,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&ms.left, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&ms.right, verify_state)?;
let shape_left = Self::matrix_value_shape(self, &ms.left)?;
let shape_right = Self::matrix_value_shape(self, &ms.right)?;
if shape_left != shape_right {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"matrix --: shape {:?} and {:?} do not match",
shape_left, shape_right
)),
)));
}
Ok(())
}
fn verify_matrix_mul_well_defined(
&mut self,
mm: &MatrixMul,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&mm.left, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&mm.right, verify_state)?;
let shape_left = Self::matrix_value_shape(self, &mm.left)?;
let shape_right = Self::matrix_value_shape(self, &mm.right)?;
if shape_left.1 != shape_right.0 {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"matrix **: left columns {} != right rows {}",
shape_left.1, shape_right.0
)),
)));
}
Ok(())
}
fn verify_matrix_scalar_mul_well_defined(
&mut self,
m: &MatrixScalarMul,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&m.scalar, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&m.matrix, verify_state)?;
let _ = Self::matrix_value_shape(self, &m.matrix)?;
Ok(())
}
fn verify_matrix_pow_well_defined(
&mut self,
m: &MatrixPow,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&m.base, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&m.exponent, verify_state)?;
let shape_base = Self::matrix_value_shape(self, &m.base)?;
if shape_base.0 != shape_base.1 {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"matrix ^^: base must be square, got {}x{}",
shape_base.0, shape_base.1
)),
)));
}
let exp_in_n_pos = InFact::new(
(*m.exponent).clone(),
StandardSet::NPos.into(),
default_line_file(),
)
.into();
let ok = self.verify_atomic_fact(&exp_in_n_pos, verify_state)?;
if ok.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"matrix ^^: exponent {} is not verified in N_pos",
m.exponent
)),
)));
}
Ok(())
}
fn matrix_value_shape(rt: &Runtime, obj: &Obj) -> Result<(usize, usize), RuntimeError> {
match obj {
Obj::MatrixListObj(m) => Self::rectangular_shape_of_matrix_list_obj(m),
Obj::Atom(AtomObj::Identifier(id)) => {
Self::matrix_list_shape_for_name_known_as_matrix_list(rt, &id.name)
}
Obj::MatrixAdd(inner) => Self::matrix_value_shape(rt, &inner.left),
Obj::MatrixSub(inner) => Self::matrix_value_shape(rt, &inner.left),
Obj::MatrixMul(inner) => {
let sl = Self::matrix_value_shape(rt, &inner.left)?;
let sr = Self::matrix_value_shape(rt, &inner.right)?;
if sl.1 != sr.0 {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"matrix **: left columns {} != right rows {}",
sl.1, sr.0
)),
)));
}
Ok((sl.0, sr.1))
}
Obj::MatrixScalarMul(inner) => Self::matrix_value_shape(rt, &inner.matrix),
Obj::MatrixPow(inner) => {
let s = Self::matrix_value_shape(rt, &inner.base)?;
if s.0 != s.1 {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"matrix ^^: base must be square, got {}x{}",
s.0, s.1
)),
)));
}
Ok(s)
}
_ => Self::matrix_list_shape_for_name_known_as_matrix_list(rt, &obj.to_string()),
}
}
fn matrix_list_shape_for_name_known_as_matrix_list(
rt: &Runtime,
key: &str,
) -> Result<(usize, usize), RuntimeError> {
let Some(known) = rt.get_obj_equal_to_matrix_list(key) else {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"`{}` is not known as a matrix list value",
key
)),
)));
};
let shape = Self::rectangular_shape_of_matrix_list_obj(&known)?;
if let Some(ms) = rt.get_matrix_set_for_obj_equal_to_matrix_list(key) {
Self::ensure_matrix_list_matches_matrix_set(rt, &known, &ms)?;
}
Ok(shape)
}
fn ensure_matrix_list_matches_matrix_set(
rt: &Runtime,
m: &MatrixListObj,
ms: &MatrixSet,
) -> Result<(), RuntimeError> {
let (rows, cols) = Self::rectangular_shape_of_matrix_list_obj(m)?;
let row_expect = rt
.resolve_obj_to_number(ms.row_len.as_ref())
.ok_or_else(|| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"matrix: cannot resolve row_len {} of matrix type for list shape check",
ms.row_len
)),
))
})?;
let col_expect = rt
.resolve_obj_to_number(ms.col_len.as_ref())
.ok_or_else(|| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"matrix: cannot resolve col_len {} of matrix type for list shape check",
ms.col_len
)),
))
})?;
let r = row_expect.normalized_value.parse::<usize>().map_err(|_| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"matrix: row_len `{}` is not a valid size",
row_expect.normalized_value
)),
))
})?;
let c = col_expect.normalized_value.parse::<usize>().map_err(|_| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"matrix: col_len `{}` is not a valid size",
col_expect.normalized_value
)),
))
})?;
if r != rows || c != cols {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"matrix list has shape {}x{} but matrix type expects {}x{}",
rows, cols, r, c
)),
)));
}
Ok(())
}
fn rectangular_shape_of_matrix_list_obj(
m: &MatrixListObj,
) -> Result<(usize, usize), RuntimeError> {
let rows = m.rows.len();
let cols = if rows == 0 { 0 } else { m.rows[0].len() };
for row in m.rows.iter() {
if row.len() != cols {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(
"matrix list is not rectangular (row lengths differ)".to_string(),
),
)));
}
}
Ok((rows, cols))
}
fn verify_power_set_well_defined(
&mut self,
x: &PowerSet,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&x.set, verify_state)?;
Ok(())
}
fn verify_choose_well_defined(
&mut self,
_x: &Choose,
_verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
let choose_from = *_x.set.clone();
let choose_from_is_nonempty_set_fact = AtomicFact::IsNonemptySetFact(
IsNonemptySetFact::new(choose_from.clone(), default_line_file()),
);
let choose_from_is_nonempty_set_result =
self.verify_atomic_fact(&choose_from_is_nonempty_set_fact, _verify_state)?;
if choose_from_is_nonempty_set_result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"set {} is not a nonempty set",
choose_from.to_string()
)),
)));
}
let random_param = self.generate_random_unused_name();
let nonempty_set_fact = IsNonemptySetFact::new(
obj_for_bound_param_in_scope(random_param.clone(), ParamObjType::Forall),
default_line_file(),
);
let forall_x_in_choose_from_x_is_nonempty = ForallFact::new(
ParamDefWithType::new(vec![ParamGroupWithParamType::new(
vec![random_param.clone().to_string()],
ParamType::Obj(choose_from),
)]),
vec![],
vec![nonempty_set_fact.into()],
default_line_file(),
)?
.into();
self.verify_fact(&forall_x_in_choose_from_x_is_nonempty, _verify_state)?;
Ok(())
}
fn verify_obj_at_index_well_defined(
&mut self,
x: &ObjAtIndex,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_obj_well_defined_and_store_cache(&x.obj, verify_state)?;
self.verify_obj_well_defined_and_store_cache(&x.index, verify_state)?;
let index_calculated_number = self.resolve_obj_to_number(&x.index).ok_or_else(|| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"index {} is not a number",
x.index.to_string()
)),
))
})?;
let index_calculated_obj: Obj =
Number::new(index_calculated_number.normalized_value).into();
let index_is_positive_integer_in_z_pos_fact = InFact::new(
index_calculated_obj.clone(),
StandardSet::NPos.into(),
default_line_file(),
)
.into();
let index_is_positive_integer_result =
self.verify_atomic_fact(&index_is_positive_integer_in_z_pos_fact, verify_state)?;
if index_is_positive_integer_result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"index {} is not a positive integer",
index_calculated_obj
)),
)));
}
self.store_fn_obj_cart_return_facts_if_available(&x.obj, default_line_file())?;
let target_obj_is_tuple_fact =
IsTupleFact::new((*x.obj).clone(), default_line_file()).into();
let target_obj_is_tuple_result =
self.verify_atomic_fact(&target_obj_is_tuple_fact, verify_state)?;
if target_obj_is_tuple_result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"index target {} is not a tuple",
x.obj
)),
)));
}
let target_tuple_dim_obj: Obj = TupleDim::new((*x.obj).clone()).into();
let index_not_larger_than_tuple_dim_fact = LessEqualFact::new(
index_calculated_obj.clone(),
target_tuple_dim_obj.clone(),
default_line_file(),
)
.into();
let index_not_larger_than_tuple_dim_result =
self.verify_atomic_fact(&index_not_larger_than_tuple_dim_fact, verify_state)?;
if index_not_larger_than_tuple_dim_result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"{} <= {} is unknown",
index_calculated_obj, target_tuple_dim_obj
)),
)));
}
Ok(())
}
fn store_fn_obj_cart_return_facts_if_available(
&mut self,
obj: &Obj,
line_file: LineFile,
) -> Result<(), RuntimeError> {
let Obj::FnObj(fn_obj) = obj else {
return Ok(());
};
let Some(ret_set) = self.fn_obj_return_set_after_application(fn_obj)? else {
return Ok(());
};
let Obj::Cart(cart) = ret_set else {
return Ok(());
};
if cart.args.len() < 2 {
return Ok(());
}
self.store_tuple_obj_and_cart(
&obj.to_string(),
None,
Some(cart.clone()),
line_file.clone(),
);
let is_tuple_fact: AtomicFact = IsTupleFact::new(obj.clone(), line_file.clone()).into();
self.store_atomic_fact_without_well_defined_verified_and_infer(is_tuple_fact)?;
let tuple_dim_obj: Obj = TupleDim::new(obj.clone()).into();
let cart_arg_count_obj: Obj = Number::new(cart.args.len().to_string()).into();
let tuple_dim_fact: AtomicFact =
EqualFact::new(tuple_dim_obj, cart_arg_count_obj, line_file.clone()).into();
self.store_atomic_fact_without_well_defined_verified_and_infer(tuple_dim_fact)?;
for (factor_index, factor) in cart.args.iter().enumerate() {
let index = factor_index + 1;
let index_obj: Obj = Number::new(index.to_string()).into();
let index_bound_fact: AtomicFact = LessEqualFact::new(
index_obj.clone(),
TupleDim::new(obj.clone()).into(),
line_file.clone(),
)
.into();
self.store_atomic_fact_without_well_defined_verified_and_infer(index_bound_fact)?;
let projected_obj: Obj = ObjAtIndex::new(obj.clone(), index_obj).into();
let projected_in_factor_fact: AtomicFact =
InFact::new(projected_obj, (**factor).clone(), line_file.clone()).into();
self.store_atomic_fact_without_well_defined_verified_and_infer(
projected_in_factor_fact,
)?;
}
Ok(())
}
fn fn_obj_return_set_after_application(
&self,
fn_obj: &FnObj,
) -> Result<Option<Obj>, RuntimeError> {
if fn_obj.body.is_empty() {
return Ok(None);
}
let mut space = match fn_obj.head.as_ref() {
FnObjHead::AnonymousFnLiteral(a) => FnSetSpace::Anon((**a).clone()),
FnObjHead::FiniteSeqListObj(_) => return Ok(None),
_ => {
let function_name_obj: Obj = (*fn_obj.head).clone().into();
let Some(body) = self.get_object_in_fn_set_or_restrict(&function_name_obj) else {
return Ok(None);
};
FnSetSpace::Set(FnSet::from_body(body.clone())?)
}
};
for i in 0..fn_obj.body.len() {
let ret_set = space.ret_set_obj();
if i == fn_obj.body.len() - 1 {
return Ok(Some(ret_set));
}
space = FnSetSpace::from_ret_obj(ret_set)?;
}
Ok(None)
}
fn verify_q_pos_well_defined(&self) -> Result<(), RuntimeError> {
Ok(())
}
fn verify_r_pos_well_defined(&self) -> Result<(), RuntimeError> {
Ok(())
}
fn verify_q_neg_well_defined(&self) -> Result<(), RuntimeError> {
Ok(())
}
fn verify_z_neg_well_defined(&self) -> Result<(), RuntimeError> {
Ok(())
}
fn verify_r_neg_well_defined(&self) -> Result<(), RuntimeError> {
Ok(())
}
fn verify_q_nz_well_defined(&self) -> Result<(), RuntimeError> {
Ok(())
}
fn verify_z_nz_well_defined(&self) -> Result<(), RuntimeError> {
Ok(())
}
fn verify_r_nz_well_defined(&self) -> Result<(), RuntimeError> {
Ok(())
}
pub(crate) fn struct_header_param_to_arg_map(
&mut self,
struct_obj: &StructObj,
verify_state: &VerifyState,
) -> Result<(DefStructStmt, HashMap<String, Obj>), RuntimeError> {
let struct_name = struct_obj.name.to_name_string();
let def = self
.get_struct_definition_by_name(&struct_name)
.cloned()
.ok_or_else(|| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"struct `{}` is not defined",
struct_name
)),
))
})?;
let expected_count = def
.param_def_with_dom
.as_ref()
.map(|(param_def, _)| param_def.number_of_params())
.unwrap_or(0);
if struct_obj.params.len() != expected_count {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"struct `{}` expects {} parameter(s), got {}",
struct_name,
expected_count,
struct_obj.params.len()
)),
)));
}
for arg in struct_obj.params.iter() {
self.verify_obj_well_defined_and_store_cache(arg, verify_state)?;
}
let param_to_arg_map = if let Some((param_def, dom_facts)) = &def.param_def_with_dom {
let verify_args_result = self
.verify_args_satisfy_param_def_flat_types(
param_def,
&struct_obj.params,
verify_state,
ParamObjType::DefHeader,
)
.map_err(|runtime_error| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!(
"failed to verify struct `{}` arguments satisfy parameter types",
struct_name
),
runtime_error,
),
))
})?;
if verify_args_result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"failed to verify struct `{}` arguments satisfy parameter types",
struct_name
)),
)));
}
let param_to_arg_map =
param_def.param_defs_and_args_to_param_to_arg_map(&struct_obj.params);
for dom_fact in dom_facts.iter() {
let instantiated_dom_fact = self
.inst_or_and_chain_atomic_fact(
dom_fact,
¶m_to_arg_map,
ParamObjType::DefHeader,
None,
)
.map_err(|e| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!(
"failed to instantiate struct `{}` domain fact",
struct_name
),
e,
),
))
})?;
let verify_result =
self.verify_or_and_chain_atomic_fact(&instantiated_dom_fact, verify_state)?;
if verify_result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"failed to verify struct `{}` domain fact:\n{}",
struct_name, instantiated_dom_fact
)),
)));
}
}
param_to_arg_map
} else {
HashMap::new()
};
Ok((def, param_to_arg_map))
}
pub(crate) fn instantiated_struct_field_types(
&mut self,
struct_obj: &StructObj,
verify_state: &VerifyState,
) -> Result<Vec<Obj>, RuntimeError> {
let (def, param_to_arg_map) =
self.struct_header_param_to_arg_map(struct_obj, verify_state)?;
let mut fields = Vec::with_capacity(def.fields.len());
for (_, field_type) in def.fields.iter() {
fields.push(self.inst_obj(field_type, ¶m_to_arg_map, ParamObjType::DefHeader)?);
}
Ok(fields)
}
pub(crate) fn struct_field_index(
&self,
struct_obj: &StructObj,
field_name: &str,
) -> Result<usize, RuntimeError> {
let struct_name = struct_obj.name.to_name_string();
let def = self
.get_struct_definition_by_name(&struct_name)
.ok_or_else(|| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"struct `{}` is not defined",
struct_name
)),
))
})?;
def.fields
.iter()
.position(|(name, _)| name == field_name)
.map(|idx| idx + 1)
.ok_or_else(|| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"struct `{}` has no field `{}`",
struct_name, field_name
)),
))
})
}
pub(crate) fn struct_field_access_projection(
&self,
field_access: &ObjAsStructInstanceWithFieldAccess,
) -> Result<Obj, RuntimeError> {
let index = self.struct_field_index(&field_access.struct_obj, &field_access.field_name)?;
Ok(ObjAtIndex::new(
(*field_access.obj).clone(),
Number::new(index.to_string()).into(),
)
.into())
}
fn verify_struct_obj_well_defined(
&mut self,
struct_obj: &StructObj,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
let (def, param_to_arg_map) =
self.struct_header_param_to_arg_map(struct_obj, verify_state)?;
for (_, field_type) in def.fields.iter() {
let instantiated_field_type =
self.inst_obj(field_type, ¶m_to_arg_map, ParamObjType::DefHeader)?;
self.verify_obj_well_defined_and_store_cache(&instantiated_field_type, verify_state)?;
}
self.run_in_local_env(|rt| {
for (field_name, field_type) in def.fields.iter() {
let instantiated_field_type =
rt.inst_obj(field_type, ¶m_to_arg_map, ParamObjType::DefHeader)?;
let param_def =
ParamGroupWithSet::new(vec![field_name.clone()], instantiated_field_type);
rt.define_params_with_set_in_scope(¶m_def, ParamObjType::DefStructField)?;
}
for fact in def.equivalent_facts.iter() {
let instantiated_fact =
rt.inst_fact(fact, ¶m_to_arg_map, ParamObjType::DefHeader, None)?;
rt.verify_fact_well_defined(&instantiated_fact, verify_state)?;
}
Ok::<(), RuntimeError>(())
})?;
Ok(())
}
fn verify_obj_as_struct_instance_with_field_access_well_defined(
&mut self,
field_access: &ObjAsStructInstanceWithFieldAccess,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
self.verify_struct_obj_well_defined(&field_access.struct_obj, verify_state)?;
self.struct_field_index(&field_access.struct_obj, &field_access.field_name)?;
self.verify_obj_well_defined_and_store_cache(&field_access.obj, verify_state)?;
let membership_fact: AtomicFact = InFact::new(
(*field_access.obj).clone(),
(*field_access.struct_obj).clone().into(),
default_line_file(),
)
.into();
let result = self.verify_atomic_fact(&membership_fact, verify_state)?;
if result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"failed to verify `{}` is well-defined: cannot prove {}",
field_access, membership_fact
)),
)));
}
Ok(())
}
}
impl Runtime {
pub fn verify_param_type_well_defined(
&mut self,
param_type: &ParamType,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
match param_type {
ParamType::Set(_) => Ok(()),
ParamType::NonemptySet(_) => Ok(()),
ParamType::FiniteSet(_) => Ok(()),
ParamType::Obj(obj) => match obj {
Obj::FamilyObj(family) => {
self.verify_param_type_family_well_defined(family, verify_state)
}
_ => self.verify_obj_well_defined_and_store_cache(obj, verify_state),
},
}
}
fn verify_param_type_family_well_defined(
&mut self,
family_param_type: &FamilyObj,
verify_state: &VerifyState,
) -> Result<(), RuntimeError> {
let family_name = family_param_type.name.to_string();
let def = match self.get_cloned_family_definition_by_name(&family_name) {
Some(d) => d,
None => {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"family `{}` is not defined",
family_name
)),
)));
}
};
let expected_count = def.params_def_with_type.number_of_params();
if family_param_type.params.len() != expected_count {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"family `{}` expects {} parameter(s), got {}",
family_name,
expected_count,
family_param_type.params.len()
)),
)));
}
for arg in family_param_type.params.iter() {
self.verify_obj_well_defined_and_store_cache(arg, verify_state)?;
}
let args_param_types = self
.verify_args_satisfy_param_def_flat_types(
&def.params_def_with_type,
&family_param_type.params,
verify_state,
ParamObjType::DefHeader,
)
.map_err(|runtime_error| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!(
"failed to verify family `{}` arguments satisfy parameter types",
family_name
),
runtime_error,
),
))
})?;
if args_param_types.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"failed to verify family `{}` arguments satisfy parameter types",
family_name
)),
)));
}
let param_to_arg_map = def
.params_def_with_type
.param_defs_and_args_to_param_to_arg_map(family_param_type.params.as_slice());
for dom_fact in def.dom_facts.iter() {
let instantiated_dom_fact = self
.inst_or_and_chain_atomic_fact(
dom_fact,
¶m_to_arg_map,
ParamObjType::DefHeader,
None,
)
.map_err(|e| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!(
"failed to instantiate family `{}` domain fact: {}",
family_name, e
),
e,
),
))
})?;
let verify_result = self
.verify_or_and_chain_atomic_fact(&instantiated_dom_fact, verify_state)
.map_err(|verify_error| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!(
"failed to verify family `{}` domain fact:\n{}",
family_name, instantiated_dom_fact
),
verify_error,
),
))
})?;
if verify_result.is_unknown() {
return Err(RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_just_msg(format!(
"failed to verify family `{}` domain fact:\n{}",
family_name, instantiated_dom_fact
)),
)));
}
}
let instantiated_equal_to = self
.inst_obj(&def.equal_to, ¶m_to_arg_map, ParamObjType::DefHeader)
.map_err(|e| {
RuntimeError::from(WellDefinedRuntimeError(
RuntimeErrorStruct::new_with_msg_and_cause(
format!(
"failed to instantiate family `{}` member set: {}",
family_name, e
),
e,
),
))
})?;
self.verify_obj_well_defined_and_store_cache(&instantiated_equal_to, verify_state)?;
Ok(())
}
}