1use crate::prelude::*;
2
3impl Runtime {
4 pub fn exec_by_for_stmt(&mut self, stmt: &ByForStmt) -> Result<StmtResult, RuntimeError> {
5 let (params, param_sets) = stmt
6 .expanded_range_params()
7 .map_err(|msg| short_exec_error(stmt.clone().into(), msg, None, vec![]))?;
8
9 let corresponding_forall_fact = stmt
10 .to_corresponding_forall_fact()
11 .map_err(|msg| short_exec_error(stmt.clone().into(), msg, None, vec![]))?;
12 self.verify_forall_fact_params_and_dom_well_defined(
13 &stmt.forall_fact,
14 &VerifyState::new(0, false),
15 )
16 .map_err(|well_defined_error| {
17 short_exec_error(
18 stmt.clone().into(),
19 format!(
20 "by for: forall parameters or domain is not well-defined (`{}`)",
21 stmt.forall_fact
22 ),
23 Some(well_defined_error),
24 vec![],
25 )
26 })?;
27
28 let param_value_strings_of_each_param = self
29 .by_for_param_value_strings_of_each_param(stmt, ¶m_sets)
30 .map_err(|msg| short_exec_error(stmt.clone().into(), msg, None, vec![]))?;
31 let for_cartesian_product_is_empty = param_value_strings_of_each_param
32 .iter()
33 .any(|one_param_value_strings| one_param_value_strings.is_empty());
34 if for_cartesian_product_is_empty {
35 let infer_result_from_stored_forall_fact = self
36 .verify_well_defined_and_store_and_infer_with_default_verify_state(
37 corresponding_forall_fact.clone(),
38 )
39 .map_err(|store_fact_error| {
40 short_exec_error(
41 stmt.clone().into(),
42 format!(
43 "by for: failed to store corresponding forall `{}`",
44 corresponding_forall_fact
45 ),
46 Some(store_fact_error),
47 vec![],
48 )
49 })?;
50 return Ok((NonFactualStmtSuccess::new(
51 stmt.clone().into(),
52 infer_result_from_stored_forall_fact,
53 vec![],
54 ))
55 .into());
56 }
57
58 let mut current_parameter_index_assignment =
59 Self::by_for_start_index_assignment(param_sets.len());
60 loop {
61 self.exec_by_for_stmt_for_one_assignment(
62 stmt,
63 ¶ms,
64 ¶m_sets,
65 ¤t_parameter_index_assignment,
66 ¶m_value_strings_of_each_param,
67 )?;
68 let next_parameter_index_assignment = Self::by_for_next_index_assignment(
69 ¤t_parameter_index_assignment,
70 ¶m_value_strings_of_each_param,
71 );
72 match next_parameter_index_assignment {
73 Some(next_parameter_index_assignment) => {
74 current_parameter_index_assignment = next_parameter_index_assignment;
75 }
76 None => break,
77 }
78 }
79
80 let infer_result_from_stored_forall_fact = self
81 .verify_well_defined_and_store_and_infer_with_default_verify_state(
82 corresponding_forall_fact.clone(),
83 )
84 .map_err(|store_fact_error| {
85 short_exec_error(
86 stmt.clone().into(),
87 format!(
88 "by for: failed to store corresponding forall `{}`",
89 corresponding_forall_fact
90 ),
91 Some(store_fact_error),
92 vec![],
93 )
94 })?;
95
96 Ok((NonFactualStmtSuccess::new(
97 stmt.clone().into(),
98 infer_result_from_stored_forall_fact,
99 vec![],
100 ))
101 .into())
102 }
103}
104
105impl Runtime {
106 pub(crate) fn negated_domain_fact_for_by_for_skip(dom: &Fact) -> Option<Fact> {
108 match dom {
109 Fact::AtomicFact(a) => Some(Fact::AtomicFact(a.make_reversed())),
110 Fact::AndFact(and_fact) => {
111 if and_fact.facts.is_empty() {
112 return None;
113 }
114 let branches: Vec<AndChainAtomicFact> = and_fact
115 .facts
116 .iter()
117 .map(|f| AndChainAtomicFact::AtomicFact(f.make_reversed()))
118 .collect();
119 Some(OrFact::new(branches, and_fact.line_file()).into())
120 }
121 Fact::ChainFact(_)
122 | Fact::OrFact(_)
123 | Fact::ExistFact(_)
124 | Fact::ForallFact(_)
125 | Fact::ForallFactWithIff(_)
126 | Fact::NotForall(_) => None,
127 }
128 }
129
130 fn integer_string_from_number_like_obj_for_for(
131 self: &Self,
132 number_like_obj: &Obj,
133 line_file: LineFile,
134 ) -> Result<String, RuntimeError> {
135 let calculated_string = {
136 let value = self.resolve_obj_to_number(number_like_obj);
137
138 match value {
139 Some(number) => number.normalized_value,
140 _ => {
141 return Err(UnknownRuntimeError(
142 RuntimeErrorStruct::new_with_msg_and_line_file(
143 format!(
144 "by for: range boundary `{}` must be a calculable number expression",
145 number_like_obj
146 ),
147 line_file,
148 ),
149 )
150 .into());
151 }
152 }
153 };
154
155 if !is_number_string_literally_integer_without_dot(calculated_string.clone()) {
156 return Err(
157 UnknownRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(
158 format!(
159 "by for: range boundary `{}` is not an integer number",
160 number_like_obj
161 ),
162 line_file,
163 ))
164 .into(),
165 );
166 }
167 Ok(calculated_string)
168 }
169
170 fn by_for_param_value_strings_of_each_param(
171 self: &Self,
172 stmt: &ByForStmt,
173 param_sets: &[ClosedRangeOrRange],
174 ) -> Result<Vec<Vec<String>>, String> {
175 let mut param_value_strings_of_each_param: Vec<Vec<String>> = Vec::new();
176 for param_set in param_sets.iter() {
177 let (start_obj, end_obj, is_closed_range) = match param_set {
178 ClosedRangeOrRange::ClosedRange(closed_range) => {
179 (closed_range.start.as_ref(), closed_range.end.as_ref(), true)
180 }
181 ClosedRangeOrRange::Range(range) => {
182 (range.start.as_ref(), range.end.as_ref(), false)
183 }
184 };
185 let start_integer_string = self
186 .integer_string_from_number_like_obj_for_for(start_obj, stmt.line_file.clone())
187 .map_err(|e| e.to_string())?;
188 let end_integer_string = self
189 .integer_string_from_number_like_obj_for_for(end_obj, stmt.line_file.clone())
190 .map_err(|e| e.to_string())?;
191 let start_integer_i128 = start_integer_string.parse::<i128>().map_err(|_| {
192 format!(
193 "by for: failed to parse start boundary `{}` as integer",
194 start_integer_string
195 )
196 })?;
197 let end_integer_i128 = end_integer_string.parse::<i128>().map_err(|_| {
198 format!(
199 "by for: failed to parse end boundary `{}` as integer",
200 end_integer_string
201 )
202 })?;
203
204 let mut one_param_value_strings: Vec<String> = Vec::new();
205 if start_integer_i128 <= end_integer_i128 {
206 let right_boundary = if is_closed_range {
207 end_integer_i128
208 } else {
209 end_integer_i128 - 1
210 };
211 if start_integer_i128 <= right_boundary {
212 let mut current_value_i128 = start_integer_i128;
213 while current_value_i128 <= right_boundary {
214 one_param_value_strings.push(current_value_i128.to_string());
215 current_value_i128 += 1;
216 }
217 }
218 }
219 param_value_strings_of_each_param.push(one_param_value_strings);
220 }
221 Ok(param_value_strings_of_each_param)
222 }
223
224 fn by_for_start_index_assignment(param_count: usize) -> Vec<usize> {
225 vec![0; param_count]
226 }
227
228 fn by_for_next_index_assignment(
229 current_parameter_index_assignment: &Vec<usize>,
230 param_value_strings_of_each_param: &Vec<Vec<String>>,
231 ) -> Option<Vec<usize>> {
232 let mut next_parameter_index_assignment = current_parameter_index_assignment.clone();
233 for reversed_position in 0..next_parameter_index_assignment.len() {
234 let position_from_right = next_parameter_index_assignment.len() - 1 - reversed_position;
235 let current_index = next_parameter_index_assignment[position_from_right];
236 let current_range_length = param_value_strings_of_each_param[position_from_right].len();
237 if current_index + 1 < current_range_length {
238 next_parameter_index_assignment[position_from_right] = current_index + 1;
239 return Some(next_parameter_index_assignment);
240 }
241 next_parameter_index_assignment[position_from_right] = 0;
242 }
243 None
244 }
245
246 fn exec_by_for_stmt_for_one_assignment(
247 &mut self,
248 stmt: &ByForStmt,
249 params: &[String],
250 param_sets: &[ClosedRangeOrRange],
251 parameter_index_assignment: &Vec<usize>,
252 param_value_strings_of_each_param: &Vec<Vec<String>>,
253 ) -> Result<(), RuntimeError> {
254 self.run_in_local_env(|rt| {
255 rt.exec_by_for_stmt_for_one_assignment_body(
256 stmt,
257 params,
258 param_sets,
259 parameter_index_assignment,
260 param_value_strings_of_each_param,
261 )
262 })
263 }
264
265 fn exec_by_for_stmt_for_one_assignment_body(
266 &mut self,
267 stmt: &ByForStmt,
268 params: &[String],
269 _param_sets: &[ClosedRangeOrRange],
270 parameter_index_assignment: &Vec<usize>,
271 param_value_strings_of_each_param: &Vec<Vec<String>>,
272 ) -> Result<(), RuntimeError> {
273 for (parameter_position, parameter_name) in params.iter().enumerate() {
274 let assigned_integer_string = param_value_strings_of_each_param[parameter_position]
275 [parameter_index_assignment[parameter_position]]
276 .clone();
277 self.store_free_param_or_identifier_name(parameter_name, ParamObjType::Forall)?;
278
279 let parameter_in_z_atomic_fact = AtomicFact::InFact(InFact::new(
280 obj_for_bound_param_in_scope(parameter_name.to_string(), ParamObjType::Forall),
281 StandardSet::Z.into(),
282 stmt.line_file.clone(),
283 ));
284 self.store_atomic_fact_without_well_defined_verified_and_infer(
285 parameter_in_z_atomic_fact,
286 )?;
287
288 let parameter_equal_to_assigned_obj_atomic_fact =
289 AtomicFact::EqualFact(EqualFact::new(
290 obj_for_bound_param_in_scope(parameter_name.to_string(), ParamObjType::Forall),
291 Number::new(assigned_integer_string).into(),
292 stmt.line_file.clone(),
293 ));
294 self.store_atomic_fact_without_well_defined_verified_and_infer(
295 parameter_equal_to_assigned_obj_atomic_fact,
296 )?;
297 }
298
299 let verify_state = VerifyState::new(0, false);
300 for dom_fact in stmt.forall_fact.dom_facts.iter() {
301 let verify_dom_result = self.verify_fact(dom_fact, &verify_state)?;
302 if verify_dom_result.is_true() {
303 self.verify_well_defined_and_store_and_infer_with_default_verify_state(
304 dom_fact.clone(),
305 )?;
306 } else if verify_dom_result.is_unknown() {
307 if let Some(negated_domain) = Self::negated_domain_fact_for_by_for_skip(dom_fact) {
308 let verify_negation_result =
309 self.verify_fact(&negated_domain, &verify_state)?;
310 if verify_negation_result.is_true() {
311 return Ok(());
312 }
313 }
314 return Err(short_exec_error(
315 stmt.clone().into(),
316 format!(
317 "by for: domain fact `{}` is not decided (could not verify it or its negation)",
318 dom_fact
319 ),
320 None,
321 vec![],
322 ));
323 }
324 }
325
326 for proof_stmt in stmt.proof.iter() {
327 self.exec_stmt(proof_stmt)?;
328 }
329 for fact_to_prove in stmt.forall_fact.then_facts.iter() {
330 let verified_result =
331 self.verify_exist_or_and_chain_atomic_fact(fact_to_prove, &verify_state)?;
332 if verified_result.is_unknown() {
333 return Err(short_exec_error(
334 stmt.clone().into(),
335 format!("by for: failed to prove `{}`", fact_to_prove),
336 None,
337 vec![],
338 ));
339 }
340 }
341 Ok(())
342 }
343}