use crate::common::helper::is_number_string_literally_integer_without_dot;
use crate::prelude::*;
impl Runtime {
pub fn exec_by_closed_range_as_cases_stmt(
&mut self,
stmt: &ByClosedRangeAsCasesStmt,
) -> Result<StmtResult, RuntimeError> {
let set_obj: Obj = stmt.closed_range.clone().into();
let element = stmt.element.clone();
let in_fact = InFact::new(element, set_obj, stmt.line_file.clone());
let in_atomic: AtomicFact = in_fact.clone().into();
let verify_state = VerifyState::new(0, false);
let membership = self.verify_atomic_fact(&in_atomic, &verify_state)?;
if membership.is_unknown() {
return Err(short_exec_error(
stmt.clone().into(),
format!(
"by closed_range as cases: membership `{}` is not known",
in_fact
),
None,
vec![],
));
}
let z_set: Obj = StandardSet::Z.into();
let lf = stmt.line_file.clone();
for (side, endpoint) in [
("left", stmt.closed_range.start.as_ref().clone()),
("right", stmt.closed_range.end.as_ref().clone()),
] {
let in_z: AtomicFact = InFact::new(endpoint, z_set.clone(), lf.clone()).into();
let in_z_ok = self.verify_atomic_fact(&in_z, &verify_state)?;
if in_z_ok.is_unknown() {
return Err(short_exec_error(
stmt.clone().into(),
format!(
"by closed_range as cases: range {} endpoint must be known in Z (`{}`)",
side, in_z
),
None,
vec![],
));
}
}
let branches = match or_branches_integer_closed_range_equalities(
stmt.element.clone(),
&stmt.closed_range,
&stmt.line_file,
) {
Ok(b) => {
if b.is_empty() {
return Err(short_exec_error(
stmt.clone().into(),
"by closed_range as cases: integer range is empty (end < start)"
.to_string(),
None,
vec![],
));
}
b
}
Err(literal_err) => match or_branches_closed_range_start_plus_offset_equalities(
stmt.element.clone(),
&stmt.closed_range,
&stmt.line_file,
) {
Ok(b) => b,
Err(offset_err) => {
return Err(short_exec_error(
stmt.clone().into(),
format!("{} ({})", offset_err, literal_err),
None,
vec![],
));
}
},
};
let generated_fact: Fact = if branches.len() == 1 {
branches[0].clone().into()
} else {
OrFact::new(branches, stmt.line_file.clone()).into()
};
let infer_after_store = self
.verify_well_defined_and_store_and_infer_with_default_verify_state(
generated_fact.clone(),
)
.map_err(|e| exec_stmt_error_with_stmt_and_cause(stmt.clone().into(), e))?;
let mut infer_result = InferResult::new();
infer_result.new_fact(&generated_fact);
infer_result.new_infer_result_inside(infer_after_store);
Ok(NonFactualStmtSuccess::new(stmt.clone().into(), infer_result, vec![]).into())
}
}
fn closed_range_endpoint_integer_string(obj: &Obj) -> Result<String, String> {
let Obj::Number(n) = obj else {
return Err(
"by closed_range as cases: range endpoints must be integer literals".to_string(),
);
};
let s = n.normalized_value.clone();
if !is_number_string_literally_integer_without_dot(s.clone()) {
return Err(
"by closed_range as cases: range endpoints must be integers (no decimal point)"
.to_string(),
);
}
Ok(s)
}
fn or_branches_integer_closed_range_equalities(
element: Obj,
closed: &ClosedRange,
line_file: &LineFile,
) -> Result<Vec<AndChainAtomicFact>, String> {
let start_s = closed_range_endpoint_integer_string(closed.start.as_ref())?;
let end_s = closed_range_endpoint_integer_string(closed.end.as_ref())?;
let start_i: i128 = start_s
.parse()
.map_err(|_| format!("by closed_range as cases: invalid integer `{}`", start_s))?;
let end_i: i128 = end_s
.parse()
.map_err(|_| format!("by closed_range as cases: invalid integer `{}`", end_s))?;
let mut branches: Vec<AndChainAtomicFact> = Vec::new();
let mut v = start_i;
while v <= end_i {
let eq = EqualFact::new(
element.clone(),
Number::new(v.to_string()).into(),
line_file.clone(),
);
branches.push(AndChainAtomicFact::AtomicFact(eq.into()));
v += 1;
}
Ok(branches)
}
fn or_branches_closed_range_start_plus_offset_equalities(
element: Obj,
closed: &ClosedRange,
line_file: &LineFile,
) -> Result<Vec<AndChainAtomicFact>, String> {
let start = closed.start.as_ref();
let end = closed.end.as_ref();
let Obj::Add(add) = end else {
return Err(
"by closed_range as cases: when start is not an integer literal, end must be start + N"
.to_string(),
);
};
if add.left.as_ref().to_string() != start.to_string() {
return Err(
"by closed_range as cases: end must be start + N (left addend equals range start)"
.to_string(),
);
}
let Obj::Number(n) = add.right.as_ref() else {
return Err(
"by closed_range as cases: N in start + N must be an integer literal".to_string(),
);
};
let s = n.normalized_value.clone();
if !is_number_string_literally_integer_without_dot(s.clone()) {
return Err(
"by closed_range as cases: N in start + N must be an integer (no decimal point)"
.to_string(),
);
}
let k: i128 = s
.parse()
.map_err(|_| format!("by closed_range as cases: invalid integer offset `{}`", s))?;
if k < 0 {
return Err(
"by closed_range as cases: offset N in start + N must be non-negative".to_string(),
);
}
let mut branches: Vec<AndChainAtomicFact> = Vec::new();
let mut i = 0_i128;
while i <= k {
let rhs = if i == 0 {
start.clone()
} else {
Add::new(start.clone(), Number::new(i.to_string()).into()).into()
};
let eq = EqualFact::new(element.clone(), rhs, line_file.clone());
branches.push(AndChainAtomicFact::AtomicFact(eq.into()));
i += 1;
}
Ok(branches)
}