use crate::prelude::*;
impl Runtime {
fn store_inferred_fact_and_record_result(
&mut self,
inferred_fact: Fact,
equal_fact: &EqualFact,
infer_result: &mut InferResult,
infer_step_description: &str,
) -> Result<(), RuntimeError> {
infer_result.new_fact(&inferred_fact);
self.store_fact_without_well_defined_verified_and_infer(inferred_fact)
.map_err(|previous_error| {
RuntimeError::new_infer_error_with_msg_position_previous_error(
format!(
"failed to store inferred {} while inferring `{}`",
infer_step_description, equal_fact
),
equal_fact.line_file.clone(),
Some(previous_error.into()),
)
})?;
Ok(())
}
fn infer_equal_fact_cart_from_known_side(
&mut self,
known_cart_obj: &crate::obj::Cart,
known_cart_obj_as_symbol: &Obj,
target_obj: &Obj,
equal_fact: &EqualFact,
infer_result: &mut InferResult,
) -> Result<(), RuntimeError> {
let target_is_cart_fact = Fact::AtomicFact(AtomicFact::IsCartFact(IsCartFact::new(
target_obj.clone(),
equal_fact.line_file.clone(),
)));
self.store_inferred_fact_and_record_result(
target_is_cart_fact,
equal_fact,
infer_result,
"cart fact",
)?;
let target_cart_dim_obj = Obj::CartDim(CartDim::new(target_obj.clone()));
let known_cart_dim_obj = Obj::Number(crate::obj::Number::new(
known_cart_obj.args.len().to_string(),
));
let cart_dim_equal_fact = Fact::AtomicFact(AtomicFact::EqualFact(EqualFact::new(
target_cart_dim_obj,
known_cart_dim_obj,
equal_fact.line_file.clone(),
)));
self.store_inferred_fact_and_record_result(
cart_dim_equal_fact,
equal_fact,
infer_result,
"cart_dim fact",
)?;
self.store_known_cart_obj(
&known_cart_obj_as_symbol.to_string(),
known_cart_obj.clone(),
equal_fact.line_file.clone(),
);
self.store_known_cart_obj(
&target_obj.to_string(),
known_cart_obj.clone(),
equal_fact.line_file.clone(),
);
Ok(())
}
fn infer_equal_fact_tuple_from_known_side(
&mut self,
known_tuple_obj: &crate::obj::Tuple,
target_obj: &Obj,
equal_fact: &EqualFact,
infer_result: &mut InferResult,
) -> Result<(), RuntimeError> {
if known_tuple_obj.args.len() < 2 {
return Ok(());
}
let target_is_tuple_fact = Fact::AtomicFact(AtomicFact::IsTupleFact(IsTupleFact::new(
target_obj.clone(),
equal_fact.line_file.clone(),
)));
self.store_inferred_fact_and_record_result(
target_is_tuple_fact,
equal_fact,
infer_result,
"tuple fact",
)?;
let target_tuple_dim_obj = Obj::TupleDim(TupleDim::new(target_obj.clone()));
let known_tuple_dim_obj = Obj::Number(crate::obj::Number::new(
known_tuple_obj.args.len().to_string(),
));
let tuple_dim_equal_fact = Fact::AtomicFact(AtomicFact::EqualFact(EqualFact::new(
target_tuple_dim_obj,
known_tuple_dim_obj,
equal_fact.line_file.clone(),
)));
self.store_inferred_fact_and_record_result(
tuple_dim_equal_fact,
equal_fact,
infer_result,
"tuple_dim fact",
)?;
self.store_tuple_obj_and_cart(
&target_obj.to_string(),
Some(known_tuple_obj.clone()),
None,
equal_fact.line_file.clone(),
);
Ok(())
}
pub(crate) fn infer_equal_fact(
&mut self,
equal_fact: &EqualFact,
) -> Result<InferResult, RuntimeError> {
let mut infer_result = InferResult::new();
infer_result
.new_infer_result_inside(self.infer_equal_fact_and_give_value_to_obj(equal_fact)?);
infer_result.new_infer_result_inside(self.infer_equal_fact_by_cart(equal_fact)?);
infer_result.new_infer_result_inside(self.infer_equal_fact_by_tuple(equal_fact)?);
Ok(infer_result)
}
fn infer_equal_fact_by_cart(
&mut self,
equal_fact: &EqualFact,
) -> Result<InferResult, RuntimeError> {
let mut infer_result = InferResult::new();
if let Obj::Cart(cart) = &equal_fact.left {
self.infer_equal_fact_cart_from_known_side(
cart,
&equal_fact.left,
&equal_fact.right,
equal_fact,
&mut infer_result,
)?;
}
if let Obj::Cart(cart) = &equal_fact.right {
self.infer_equal_fact_cart_from_known_side(
cart,
&equal_fact.right,
&equal_fact.left,
equal_fact,
&mut infer_result,
)?;
}
Ok(infer_result)
}
fn infer_equal_fact_by_tuple(
&mut self,
equal_fact: &EqualFact,
) -> Result<InferResult, RuntimeError> {
let mut infer_result = InferResult::new();
if let Obj::Tuple(tuple) = &equal_fact.left {
self.infer_equal_fact_tuple_from_known_side(
tuple,
&equal_fact.right,
equal_fact,
&mut infer_result,
)?;
}
if let Obj::Tuple(tuple) = &equal_fact.right {
self.infer_equal_fact_tuple_from_known_side(
tuple,
&equal_fact.left,
equal_fact,
&mut infer_result,
)?;
}
Ok(infer_result)
}
fn infer_equal_fact_and_give_value_to_obj(
&mut self,
equal_fact: &EqualFact,
) -> Result<InferResult, RuntimeError> {
if let Some(right_calculated_value) = self.resolve_obj_to_number(&equal_fact.right) {
self.top_level_env()
.known_objs_equal_to_normalized_decimal_number
.insert(equal_fact.left.to_string(), right_calculated_value);
}
if let Some(left_calculated_value) = self.resolve_obj_to_number(&equal_fact.left) {
self.top_level_env()
.known_objs_equal_to_normalized_decimal_number
.insert(equal_fact.right.to_string(), left_calculated_value);
}
Ok(InferResult::new())
}
pub(crate) fn infer_normal_atomic_fact(
&mut self,
normal_atomic_fact: &NormalAtomicFact,
) -> Result<InferResult, RuntimeError> {
let predicate_name = normal_atomic_fact.predicate.to_string();
let predicate_definition = match self.get_prop_definition_by_name(&predicate_name) {
Some(predicate_definition) => predicate_definition.clone(),
None => return Ok(InferResult::new()),
};
let mut infer_result = InferResult::new();
let param_type_infer = self
.store_args_satisfy_param_type_when_not_defining_new_identifiers(
&predicate_definition.params_def_with_type,
&normal_atomic_fact.body,
normal_atomic_fact.line_file.clone(),
)
.map_err(|previous_error| {
RuntimeError::new_infer_error_with_msg_position_previous_error(
format!(
"failed to verify parameter types for `{}`",
normal_atomic_fact
),
normal_atomic_fact.line_file.clone(),
Some(previous_error),
)
})?;
infer_result.new_infer_result_inside(param_type_infer);
let param_to_arg_map = self.params_to_arg_map(
&predicate_definition.params_def_with_type,
&normal_atomic_fact.body,
)?;
for iff_fact in predicate_definition.iff_facts.iter() {
let instantiated_iff_fact =
self.inst_fact(iff_fact, ¶m_to_arg_map).map_err(|e| {
RuntimeError::new_infer_error_with_msg_position_previous_error(
format!(
"failed to instantiate iff fact while inferring `{}`",
normal_atomic_fact
),
normal_atomic_fact.line_file.clone(),
Some(e),
)
})?;
let fact_to_store =
instantiated_iff_fact.with_new_line_file(normal_atomic_fact.line_file.clone());
infer_result.new_fact(&fact_to_store);
self.store_fact_without_well_defined_verified_and_infer(fact_to_store)
.map_err(|previous_error| {
RuntimeError::new_infer_error_with_msg_position_previous_error(
format!(
"failed to store instantiated iff fact while inferring `{}`",
normal_atomic_fact
),
normal_atomic_fact.line_file.clone(),
Some(previous_error.into()),
)
})?;
}
Ok(infer_result)
}
}