1use crate::prelude::*;
2
3impl Runtime {
4 fn verify_obj_well_defined_from_cache_if_known(&self, obj: &Obj) -> Option<()> {
5 let key = obj.to_string();
6 if self.cache_well_defined_obj_contains(&key) {
7 Some(())
8 } else {
9 None
10 }
11 }
12
13 pub fn verify_obj_well_defined_and_store_cache(
14 &mut self,
15 obj: &Obj,
16 verify_state: &VerifyState,
17 ) -> Result<(), RuntimeError> {
18 if self
19 .verify_obj_well_defined_from_cache_if_known(obj)
20 .is_some()
21 {
22 return Ok(());
23 }
24
25 match obj {
26 Obj::Atom(AtomObj::Identifier(identifier)) => {
27 self.verify_identifier_well_defined(identifier)
28 }
29 Obj::Atom(AtomObj::IdentifierWithMod(x)) => {
30 self.verify_identifier_with_mod_well_defined(x)
31 }
32 Obj::FnObj(fn_obj) => self.verify_fn_obj_well_defined(fn_obj, verify_state),
33 Obj::Number(_) => Ok(()),
34 Obj::Add(add) => self.verify_add_well_defined(add, verify_state),
35 Obj::Sub(sub) => self.verify_sub_well_defined(sub, verify_state),
36 Obj::Mul(mul) => self.verify_mul_well_defined(mul, verify_state),
37 Obj::Div(div) => self.verify_div_well_defined(div, verify_state),
38 Obj::Mod(m) => self.verify_mod_well_defined(m, verify_state),
39 Obj::Pow(pow) => self.verify_pow_well_defined(pow, verify_state),
40 Obj::Abs(abs) => self.verify_abs_well_defined(abs, verify_state),
41 Obj::Log(log) => self.verify_log_well_defined(log, verify_state),
42 Obj::Max(max) => self.verify_max_well_defined(max, verify_state),
43 Obj::Min(min) => self.verify_min_well_defined(min, verify_state),
44 Obj::Union(x) => self.verify_union_well_defined(x, verify_state),
45 Obj::Intersect(x) => self.verify_intersect_well_defined(x, verify_state),
46 Obj::SetMinus(x) => self.verify_set_minus_well_defined(x, verify_state),
47 Obj::SetDiff(x) => self.verify_set_diff_well_defined(x, verify_state),
48 Obj::Cup(x) => self.verify_cup_well_defined(x, verify_state),
49 Obj::Cap(x) => self.verify_cap_well_defined(x, verify_state),
50 Obj::ListSet(x) => self.verify_list_set_well_defined(x, verify_state),
51 Obj::SetBuilder(x) => {
52 self.run_in_local_env(|rt| rt.verify_set_builder_well_defined(x, verify_state))
53 }
54 Obj::FnSet(x) => {
55 self.run_in_local_env(|rt| rt.verify_fn_set_well_defined(x, verify_state))
56 }
57 Obj::AnonymousFn(x) => self.verify_anonymous_fn_well_defined(x, verify_state),
58 Obj::StandardSet(StandardSet::NPos) => self.verify_n_pos_obj_well_defined(),
59 Obj::StandardSet(StandardSet::N) => self.verify_n_obj_well_defined(),
60 Obj::StandardSet(StandardSet::Q) => self.verify_q_obj_well_defined(),
61 Obj::StandardSet(StandardSet::Z) => self.verify_z_obj_well_defined(),
62 Obj::StandardSet(StandardSet::R) => self.verify_r_obj_well_defined(),
63 Obj::Cart(x) => self.verify_cart_well_defined(x, verify_state),
64 Obj::CartDim(x) => self.verify_cart_dim_well_defined(x, verify_state),
65 Obj::Proj(x) => self.verify_proj_well_defined(x, verify_state),
66 Obj::TupleDim(x) => self.verify_dim_well_defined(x, verify_state),
67 Obj::Tuple(x) => self.verify_tuple_well_defined(x, verify_state),
68 Obj::Count(x) => self.verify_count_well_defined(x, verify_state),
69 Obj::Sum(x) => self.verify_sum_obj_well_defined(x, verify_state),
70 Obj::Product(x) => self.verify_product_obj_well_defined(x, verify_state),
71 Obj::Range(x) => self.verify_range_well_defined(x, verify_state),
72 Obj::ClosedRange(x) => self.verify_closed_range_well_defined(x, verify_state),
73 Obj::FiniteSeqSet(x) => self.verify_finite_seq_set_well_defined(x, verify_state),
74 Obj::SeqSet(x) => self.verify_seq_set_well_defined(x, verify_state),
75 Obj::FiniteSeqListObj(x) => {
76 self.verify_finite_seq_list_obj_well_defined(x, verify_state)
77 }
78 Obj::MatrixSet(x) => self.verify_matrix_set_well_defined(x, verify_state),
79 Obj::MatrixListObj(x) => self.verify_matrix_list_obj_well_defined(x, verify_state),
80 Obj::MatrixAdd(x) => self.verify_matrix_add_well_defined(x, verify_state),
81 Obj::MatrixSub(x) => self.verify_matrix_sub_well_defined(x, verify_state),
82 Obj::MatrixMul(x) => self.verify_matrix_mul_well_defined(x, verify_state),
83 Obj::MatrixScalarMul(x) => self.verify_matrix_scalar_mul_well_defined(x, verify_state),
84 Obj::MatrixPow(x) => self.verify_matrix_pow_well_defined(x, verify_state),
85 Obj::PowerSet(x) => self.verify_power_set_well_defined(x, verify_state),
86 Obj::Choose(x) => self.verify_choose_well_defined(x, verify_state),
87 Obj::ObjAtIndex(x) => self.verify_obj_at_index_well_defined(x, verify_state),
88 Obj::StandardSet(StandardSet::QPos) => self.verify_q_pos_well_defined(),
89 Obj::StandardSet(StandardSet::RPos) => self.verify_r_pos_well_defined(),
90 Obj::StandardSet(StandardSet::QNeg) => self.verify_q_neg_well_defined(),
91 Obj::StandardSet(StandardSet::ZNeg) => self.verify_z_neg_well_defined(),
92 Obj::StandardSet(StandardSet::RNeg) => self.verify_r_neg_well_defined(),
93 Obj::StandardSet(StandardSet::QNz) => self.verify_q_nz_well_defined(),
94 Obj::StandardSet(StandardSet::ZNz) => self.verify_z_nz_well_defined(),
95 Obj::StandardSet(StandardSet::RNz) => self.verify_r_nz_well_defined(),
96 Obj::FamilyObj(family) => {
97 self.verify_param_type_family_well_defined(family, verify_state)
98 }
99 Obj::Atom(AtomObj::Forall(_)) => Ok(()),
100 Obj::Atom(AtomObj::Def(_)) => Ok(()),
101 Obj::Atom(AtomObj::Exist(_)) => Ok(()),
102 Obj::Atom(AtomObj::SetBuilder(_)) => Ok(()),
103 Obj::Atom(AtomObj::FnSet(_)) => Ok(()),
104 Obj::Atom(AtomObj::Induc(_)) => Ok(()),
105 Obj::Atom(AtomObj::DefAlgo(_)) => Ok(()),
106 }?;
107
108 self.store_well_defined_obj_cache(obj);
109
110 Ok(())
111 }
112
113 fn verify_identifier_well_defined(&self, identifier: &Identifier) -> Result<(), RuntimeError> {
114 if self.is_name_used_for_identifier_and_field_access(&identifier.name) {
115 Ok(())
116 } else {
117 Err(RuntimeError::from(WellDefinedRuntimeError(
118 RuntimeErrorStruct::new_with_just_msg(format!(
119 "identifier `{}` not defined",
120 identifier.to_string()
121 )),
122 )))
123 }
124 }
125
126 fn verify_identifier_with_mod_well_defined(
127 &self,
128 x: &IdentifierWithMod,
129 ) -> Result<(), RuntimeError> {
130 let _ = x;
131 unreachable!()
132 }
133
134 fn verify_fn_obj_well_defined(
135 &mut self,
136 fn_obj: &FnObj,
137 verify_state: &VerifyState,
138 ) -> Result<(), RuntimeError> {
139 let mut space = match fn_obj.head.as_ref() {
140 FnObjHead::AnonymousFnLiteral(a) => {
141 self.verify_anonymous_fn_well_defined(a.as_ref(), verify_state)
142 .map_err(|well_defined_error| {
143 RuntimeError::from(WellDefinedRuntimeError(RuntimeErrorStruct::new_with_msg_and_cause(format!(
144 "object {} is not well-defined: anonymous function head is not well-defined",
145 fn_obj.to_string()
146 ), well_defined_error)))
147 })?;
148 FnSetSpace::Anon((**a).clone())
149 }
150 _ => {
151 let function_name_obj: Obj = (*fn_obj.head).clone().into();
152 let body = self
153 .get_object_in_fn_set_or_restrict(&function_name_obj)
154 .ok_or_else(|| {
155 RuntimeError::from(WellDefinedRuntimeError(
156 RuntimeErrorStruct::new_with_just_msg(todo_error_message(format!(
157 "`{}` is not a defined function",
158 fn_obj.head.to_string()
159 ))),
160 ))
161 })?
162 .clone();
163 FnSetSpace::Set(FnSet::from_body(body)?)
164 }
165 };
166
167 for (i, args) in fn_obj.body.iter().enumerate() {
168 self.verify_fn_obj_well_defined_against_fn_like_space(
169 args,
170 space.params(),
171 space.dom(),
172 space.binding(),
173 verify_state,
174 )
175 .map_err(|well_defined_error| {
176 RuntimeError::from(WellDefinedRuntimeError(RuntimeErrorStruct::new_with_msg_and_cause(format!(
177 "object {} is not well-defined, failed to verify arguments satisfy function domain.",
178 fn_obj.to_string()
179 ), well_defined_error)))
180 })?;
181
182 let set_where_the_next_fn_obj_is_in = space.ret_set_obj();
183
184 let fn_obj_prefix_body: Vec<Vec<Box<Obj>>> =
185 fn_obj.body[..=i].iter().cloned().collect();
186 let fn_obj_prefix_as_obj: Obj =
187 FnObj::new(*fn_obj.head.clone(), fn_obj_prefix_body).into();
188 let intermediate_in_fact = InFact::new(
189 fn_obj_prefix_as_obj,
190 set_where_the_next_fn_obj_is_in,
191 default_line_file(),
192 );
193 let intermediate_atomic_fact = AtomicFact::InFact(intermediate_in_fact);
194 let intermediate_line_file = intermediate_atomic_fact.line_file();
195 let intermediate_fact_string = intermediate_atomic_fact.to_string();
196 self.top_level_env()
197 .store_atomic_fact(intermediate_atomic_fact)
198 .map_err(|store_fact_error| {
199 RuntimeError::from(WellDefinedRuntimeError(
200 RuntimeErrorStruct::new_with_msg_and_cause(
201 format!(
202 "failed to store intermediate fn-obj membership fact while verifying `{}`",
203 fn_obj.to_string()
204 ),
205 store_fact_error,
206 ),
207 ))
208 })?;
209 self.top_level_env()
210 .store_fact_to_cache_known_fact(intermediate_fact_string, intermediate_line_file)
211 .map_err(|store_fact_error| {
212 RuntimeError::from(WellDefinedRuntimeError(
213 RuntimeErrorStruct::new_with_msg_and_cause(
214 format!(
215 "failed to store intermediate fn-obj membership fact while verifying `{}`",
216 fn_obj.to_string()
217 ),
218 store_fact_error,
219 ),
220 ))
221 })?;
222
223 if i == fn_obj.body.len() - 1 {
224 break;
225 }
226
227 space = FnSetSpace::from_ret_obj(space.ret_set_obj())?;
228 }
229
230 Ok(())
231 }
232
233 fn verify_fn_obj_well_defined_against_fn_like_space(
234 &mut self,
235 args: &Vec<Box<Obj>>,
236 params_def_with_set: &Vec<ParamGroupWithSet>,
237 dom_facts: &Vec<OrAndChainAtomicFact>,
238 param_binding: ParamObjType,
239 verify_state: &VerifyState,
240 ) -> Result<(), RuntimeError> {
241 let param_count = ParamGroupWithSet::number_of_params(params_def_with_set);
242 if args.len() != param_count {
243 return Err(RuntimeError::from(WellDefinedRuntimeError(
244 RuntimeErrorStruct::new_with_just_msg(format!(
245 "number of args ({}) does not match fn set with dom param count ({})",
246 args.len(),
247 param_count
248 )),
249 )));
250 }
251
252 for arg in args.iter() {
253 self.verify_obj_well_defined_and_store_cache(arg, verify_state)?;
254 }
255
256 let mut args_as_obj: Vec<Obj> = Vec::with_capacity(args.len());
257 for arg in args.iter() {
258 args_as_obj.push((**arg).clone());
259 }
260
261 let args_satisfy_fn_set_params_set_facts =
262 ParamGroupWithSet::facts_for_args_satisfy_param_def_with_set_vec(
263 self,
264 params_def_with_set,
265 &args_as_obj,
266 param_binding,
267 )
268 .map_err(|stmt_error| {
269 RuntimeError::from(WellDefinedRuntimeError(
270 RuntimeErrorStruct::new_with_msg_and_cause(
271 format!("failed to build facts for args satisfy fn set parameter sets"),
272 stmt_error,
273 ),
274 ))
275 })?;
276
277 for fact in args_satisfy_fn_set_params_set_facts.iter() {
278 let verify_result =
279 self.verify_atomic_fact(fact, verify_state)
280 .map_err(|verify_error| {
281 RuntimeError::from(WellDefinedRuntimeError(
282 RuntimeErrorStruct::new_with_msg_and_cause(
283 format!(
284 "failed to verify arg satisfy fn set parameter set: {}",
285 fact
286 ),
287 verify_error,
288 ),
289 ))
290 })?;
291 if verify_result.is_unknown() {
292 return Err(RuntimeError::from(WellDefinedRuntimeError(
293 RuntimeErrorStruct::new_with_just_msg(format!(
294 "arg does not satisfy fn set parameter set, the fact is unknown: {}",
295 fact
296 )),
297 )));
298 }
299 }
300
301 let param_to_arg_map = ParamGroupWithSet::param_defs_and_args_to_param_to_arg_map(
302 params_def_with_set,
303 &args_as_obj,
304 );
305 for dom_fact in dom_facts.iter() {
306 let instantiated_dom_fact = self
307 .inst_or_and_chain_atomic_fact(dom_fact, ¶m_to_arg_map, param_binding, None)
308 .map_err(|e| {
309 RuntimeError::from(WellDefinedRuntimeError(
310 RuntimeErrorStruct::new_with_msg_and_cause(
311 format!("failed to instantiate function domain fact: {}", e),
312 e,
313 ),
314 ))
315 })?;
316 let verify_result = self
317 .verify_or_and_chain_atomic_fact(&instantiated_dom_fact, verify_state)
318 .map_err(|verify_error| {
319 RuntimeError::from(WellDefinedRuntimeError(
320 RuntimeErrorStruct::new_with_msg_and_cause(
321 format!(
322 "failed to verify function domain fact:\n{}",
323 instantiated_dom_fact
324 ),
325 verify_error,
326 ),
327 ))
328 })?;
329 if verify_result.is_unknown() {
330 return Err(RuntimeError::from(WellDefinedRuntimeError(
331 RuntimeErrorStruct::new_with_just_msg(format!(
332 "failed to verify function domain fact:\n{}",
333 instantiated_dom_fact
334 )),
335 )));
336 }
337 }
338
339 Ok(())
340 }
341
342 fn require_obj_in_r(
343 &mut self,
344 obj: &Obj,
345 verify_state: &VerifyState,
346 ) -> Result<(), RuntimeError> {
347 if let Obj::Abs(a) = obj {
348 return self.require_obj_in_r(&a.arg, verify_state);
349 }
350 if let Obj::Max(m) = obj {
351 self.require_obj_in_r(&m.left, verify_state)?;
352 return self.require_obj_in_r(&m.right, verify_state);
353 }
354 if let Obj::Min(m) = obj {
355 self.require_obj_in_r(&m.left, verify_state)?;
356 return self.require_obj_in_r(&m.right, verify_state);
357 }
358 if let Obj::Log(l) = obj {
359 self.require_obj_in_r(&l.base, verify_state)?;
360 return self.require_obj_in_r(&l.arg, verify_state);
361 }
362 let r_obj = StandardSet::R.into();
363 let element = obj.clone();
364 let in_fact = InFact::new(element, r_obj, default_line_file());
365 let atomic_fact = AtomicFact::InFact(in_fact);
366 let result = self.verify_atomic_fact(&atomic_fact, verify_state)?;
367 if result.is_unknown() {
368 return Err(RuntimeError::from(WellDefinedRuntimeError(
369 RuntimeErrorStruct::new_with_just_msg(format!(
370 "obj {} is not in r",
371 obj.to_string()
372 )),
373 )));
374 }
375 Ok(())
376 }
377
378 fn require_obj_in_z(
379 &mut self,
380 obj: &Obj,
381 verify_state: &VerifyState,
382 ) -> Result<(), RuntimeError> {
383 let z_obj = StandardSet::Z.into();
384 let element = obj.clone();
385 let in_fact = InFact::new(element, z_obj, default_line_file());
386 let atomic_fact = AtomicFact::InFact(in_fact);
387 let result = self.verify_atomic_fact(&atomic_fact, verify_state)?;
388 if result.is_unknown() {
389 return Err(RuntimeError::from(WellDefinedRuntimeError(
390 RuntimeErrorStruct::new_with_just_msg(format!(
391 "obj {} is not in z",
392 obj.to_string()
393 )),
394 )));
395 }
396 Ok(())
397 }
398
399 fn require_less_equal_verified(
401 &mut self,
402 left: &Obj,
403 right: &Obj,
404 verify_state: &VerifyState,
405 err_detail: String,
406 ) -> Result<(), RuntimeError> {
407 let f: AtomicFact =
408 LessEqualFact::new(left.clone(), right.clone(), default_line_file()).into();
409 let r = self.verify_atomic_fact(&f, verify_state)?;
410 if r.is_unknown() {
411 return Err(RuntimeError::from(WellDefinedRuntimeError(
412 RuntimeErrorStruct::new_with_just_msg(err_detail),
413 )));
414 }
415 Ok(())
416 }
417
418 fn range_endpoints_are_numeric_for_interval_order_check(&self, start: &Obj, end: &Obj) -> bool {
421 self.resolve_obj_to_number(start).is_some() && self.resolve_obj_to_number(end).is_some()
422 }
423
424 fn verify_add_well_defined(
425 &mut self,
426 add: &Add,
427 verify_state: &VerifyState,
428 ) -> Result<(), RuntimeError> {
429 self.verify_obj_well_defined_and_store_cache(&add.left, verify_state)?;
430 self.verify_obj_well_defined_and_store_cache(&add.right, verify_state)?;
431 self.require_obj_in_r(&add.left, verify_state)?;
432 self.require_obj_in_r(&add.right, verify_state)?;
433 Ok(())
434 }
435
436 fn verify_sub_well_defined(
437 &mut self,
438 sub: &Sub,
439 verify_state: &VerifyState,
440 ) -> Result<(), RuntimeError> {
441 self.verify_obj_well_defined_and_store_cache(&sub.left, verify_state)?;
442 self.verify_obj_well_defined_and_store_cache(&sub.right, verify_state)?;
443 self.require_obj_in_r(&sub.left, verify_state)?;
444 self.require_obj_in_r(&sub.right, verify_state)?;
445 Ok(())
446 }
447
448 fn verify_mul_well_defined(
449 &mut self,
450 mul: &Mul,
451 verify_state: &VerifyState,
452 ) -> Result<(), RuntimeError> {
453 self.verify_obj_well_defined_and_store_cache(&mul.left, verify_state)?;
454 self.verify_obj_well_defined_and_store_cache(&mul.right, verify_state)?;
455 self.require_obj_in_r(&mul.left, verify_state)?;
456 self.require_obj_in_r(&mul.right, verify_state)?;
457 Ok(())
458 }
459
460 fn verify_div_well_defined(
461 &mut self,
462 div: &Div,
463 verify_state: &VerifyState,
464 ) -> Result<(), RuntimeError> {
465 self.verify_obj_well_defined_and_store_cache(&div.left, verify_state)?;
466 self.verify_obj_well_defined_and_store_cache(&div.right, verify_state)?;
467
468 let zero: Obj = Number::new("0".to_string()).into();
469 let not_equal_fact = NotEqualFact::new((*div.right).clone(), zero, default_line_file());
470 let atomic_fact = AtomicFact::NotEqualFact(not_equal_fact);
471 let result = self.verify_atomic_fact(&atomic_fact, verify_state)?;
472 if result.is_unknown() {
473 return Err(RuntimeError::from(WellDefinedRuntimeError(
474 RuntimeErrorStruct::new_with_just_msg(format!(
475 "divisor `{}` must be non-zero",
476 div.right.to_string()
477 )),
478 )));
479 }
480
481 self.require_obj_in_r(&div.left, verify_state)?;
482 self.require_obj_in_r(&div.right, verify_state)?;
483 Ok(())
484 }
485
486 fn verify_mod_well_defined(
487 &mut self,
488 m: &Mod,
489 verify_state: &VerifyState,
490 ) -> Result<(), RuntimeError> {
491 self.verify_obj_well_defined_and_store_cache(&m.left, verify_state)?;
492 self.verify_obj_well_defined_and_store_cache(&m.right, verify_state)?;
493 self.require_obj_in_z(&m.left, verify_state)?;
494 self.require_obj_in_z(&m.right, verify_state)?;
495 let zero: Obj = Number::new("0".to_string()).into();
496 let not_equal_fact = NotEqualFact::new((*m.right).clone(), zero, default_line_file());
497 let atomic_fact = AtomicFact::NotEqualFact(not_equal_fact);
498 let result = self.verify_atomic_fact(&atomic_fact, verify_state)?;
499 if result.is_unknown() {
500 return Err(RuntimeError::from(WellDefinedRuntimeError(
501 RuntimeErrorStruct::new_with_just_msg(format!(
502 "modulus `{}` must be non-zero",
503 m.right.to_string()
504 )),
505 )));
506 }
507 Ok(())
508 }
509
510 fn verify_abs_well_defined(
511 &mut self,
512 abs: &Abs,
513 verify_state: &VerifyState,
514 ) -> Result<(), RuntimeError> {
515 self.verify_obj_well_defined_and_store_cache(&abs.arg, verify_state)?;
516 self.require_obj_in_r(&abs.arg, verify_state)?;
517 Ok(())
518 }
519
520 fn verify_log_well_defined(
521 &mut self,
522 log: &Log,
523 verify_state: &VerifyState,
524 ) -> Result<(), RuntimeError> {
525 self.verify_obj_well_defined_and_store_cache(&log.base, verify_state)?;
526 self.verify_obj_well_defined_and_store_cache(&log.arg, verify_state)?;
527 self.require_obj_in_r(&log.base, verify_state)?;
528 self.require_obj_in_r(&log.arg, verify_state)?;
529 let zero: Obj = Number::new("0".to_string()).into();
530 let one: Obj = Number::new("1".to_string()).into();
531 let lf = default_line_file();
532 let checks: [(&str, AtomicFact); 3] = [
533 (
534 "log: base must be > 0",
535 GreaterFact::new((*log.base).clone(), zero.clone(), lf.clone()).into(),
536 ),
537 (
538 "log: argument must be > 0",
539 GreaterFact::new((*log.arg).clone(), zero.clone(), lf.clone()).into(),
540 ),
541 (
542 "log: base must be != 1",
543 NotEqualFact::new((*log.base).clone(), one, lf.clone()).into(),
544 ),
545 ];
546 for (msg, atomic) in checks {
547 let result = self.verify_atomic_fact(&atomic, verify_state)?;
548 if result.is_unknown() {
549 return Err(RuntimeError::from(WellDefinedRuntimeError(
550 RuntimeErrorStruct::new_with_msg_and_line_file(msg.to_string(), lf.clone()),
551 )));
552 }
553 }
554 Ok(())
555 }
556
557 fn verify_max_well_defined(
558 &mut self,
559 max: &Max,
560 verify_state: &VerifyState,
561 ) -> Result<(), RuntimeError> {
562 self.verify_obj_well_defined_and_store_cache(&max.left, verify_state)?;
563 self.verify_obj_well_defined_and_store_cache(&max.right, verify_state)?;
564 self.require_obj_in_r(&max.left, verify_state)?;
565 self.require_obj_in_r(&max.right, verify_state)?;
566 Ok(())
567 }
568
569 fn verify_min_well_defined(
570 &mut self,
571 min: &Min,
572 verify_state: &VerifyState,
573 ) -> Result<(), RuntimeError> {
574 self.verify_obj_well_defined_and_store_cache(&min.left, verify_state)?;
575 self.verify_obj_well_defined_and_store_cache(&min.right, verify_state)?;
576 self.require_obj_in_r(&min.left, verify_state)?;
577 self.require_obj_in_r(&min.right, verify_state)?;
578 Ok(())
579 }
580
581 fn verify_pow_well_defined(
587 &mut self,
588 pow: &Pow,
589 verify_state: &VerifyState,
590 ) -> Result<(), RuntimeError> {
591 self.verify_obj_well_defined_and_store_cache(&pow.base, verify_state)?;
592 self.verify_obj_well_defined_and_store_cache(&pow.exponent, verify_state)?;
593
594 let zero_obj: Obj = Number::new("0".to_string()).into();
595
596 let positive_base_and_real_exponent = AndChainAtomicFact::AndFact(AndFact::new(
597 vec![
598 GreaterFact::new((*pow.base).clone(), zero_obj.clone(), default_line_file()).into(),
599 InFact::new(
600 (*pow.exponent).clone(),
601 StandardSet::R.into(),
602 default_line_file(),
603 )
604 .into(),
605 ],
606 default_line_file(),
607 ));
608
609 let result =
610 self.verify_and_chain_atomic_fact(&positive_base_and_real_exponent, verify_state)?;
611
612 if result.is_true() {
613 return Ok(());
614 }
615
616 let zero_base_and_positive_real_exponent = AndChainAtomicFact::AndFact(AndFact::new(
617 vec![
618 EqualFact::new((*pow.base).clone(), zero_obj.clone(), default_line_file()).into(),
619 InFact::new(
620 (*pow.exponent).clone(),
621 StandardSet::R.into(),
622 default_line_file(),
623 )
624 .into(),
625 GreaterFact::new(
626 (*pow.exponent).clone(),
627 zero_obj.clone(),
628 default_line_file(),
629 )
630 .into(),
631 ],
632 default_line_file(),
633 ));
634
635 let result =
636 self.verify_and_chain_atomic_fact(&zero_base_and_positive_real_exponent, verify_state)?;
637 if result.is_true() {
638 return Ok(());
639 }
640
641 let nonzero_base_integer_exponent = AndChainAtomicFact::AndFact(AndFact::new(
642 vec![
643 InFact::new(
644 (*pow.exponent).clone(),
645 StandardSet::Z.into(),
646 default_line_file(),
647 )
648 .into(),
649 NotEqualFact::new((*pow.base).clone(), zero_obj.clone(), default_line_file())
650 .into(),
651 ],
652 default_line_file(),
653 ));
654
655 let exponent_in_n_pos = AndChainAtomicFact::AtomicFact(
656 InFact::new(
657 (*pow.exponent).clone(),
658 StandardSet::NPos.into(),
659 default_line_file(),
660 )
661 .into(),
662 );
663
664 let pow_domain_or_fact = OrFact::new(
665 vec![
666 positive_base_and_real_exponent,
667 zero_base_and_positive_real_exponent,
668 nonzero_base_integer_exponent,
669 exponent_in_n_pos,
670 ],
671 default_line_file(),
672 );
673
674 let result = self.verify_or_fact(&pow_domain_or_fact, verify_state)?;
675 if result.is_true() {
676 return Ok(());
677 }
678
679 let pow_display = Obj::Pow(pow.clone()).to_string();
680 return Err(RuntimeError::from(WellDefinedRuntimeError(
681 RuntimeErrorStruct::new_with_just_msg(format!(
682 "base and exponent do not satisfy the pow domain: {}",
683 pow_display
684 )),
685 )));
686 }
687
688 fn verify_union_well_defined(
689 &mut self,
690 x: &Union,
691 verify_state: &VerifyState,
692 ) -> Result<(), RuntimeError> {
693 self.verify_obj_well_defined_and_store_cache(&x.left, verify_state)?;
694 self.verify_obj_well_defined_and_store_cache(&x.right, verify_state)?;
695 Ok(())
696 }
697
698 fn verify_intersect_well_defined(
699 &mut self,
700 x: &Intersect,
701 verify_state: &VerifyState,
702 ) -> Result<(), RuntimeError> {
703 self.verify_obj_well_defined_and_store_cache(&x.left, verify_state)?;
704 self.verify_obj_well_defined_and_store_cache(&x.right, verify_state)?;
705 Ok(())
706 }
707
708 fn verify_set_minus_well_defined(
709 &mut self,
710 x: &SetMinus,
711 verify_state: &VerifyState,
712 ) -> Result<(), RuntimeError> {
713 self.verify_obj_well_defined_and_store_cache(&x.left, verify_state)?;
714 self.verify_obj_well_defined_and_store_cache(&x.right, verify_state)?;
715 Ok(())
716 }
717
718 fn verify_set_diff_well_defined(
719 &mut self,
720 x: &SetDiff,
721 verify_state: &VerifyState,
722 ) -> Result<(), RuntimeError> {
723 self.verify_obj_well_defined_and_store_cache(&x.left, verify_state)?;
724 self.verify_obj_well_defined_and_store_cache(&x.right, verify_state)?;
725 Ok(())
726 }
727
728 fn verify_cup_well_defined(
729 &mut self,
730 x: &Cup,
731 verify_state: &VerifyState,
732 ) -> Result<(), RuntimeError> {
733 self.verify_obj_well_defined_and_store_cache(&x.left, verify_state)?;
734 Ok(())
735 }
736
737 fn verify_cap_well_defined(
738 &mut self,
739 x: &Cap,
740 verify_state: &VerifyState,
741 ) -> Result<(), RuntimeError> {
742 self.verify_obj_well_defined_and_store_cache(&x.left, verify_state)?;
743 Ok(())
744 }
745
746 fn verify_list_set_well_defined(
747 &mut self,
748 x: &ListSet,
749 verify_state: &VerifyState,
750 ) -> Result<(), RuntimeError> {
751 for obj in &x.list {
752 self.verify_obj_well_defined_and_store_cache(obj, verify_state)?;
753 }
754
755 let next_verify_state = verify_state.make_state_with_req_ok_set_to_true();
756 let len = x.list.len();
757 let mut i = 0;
758 while i < len {
759 let left_obj = match x.list.get(i) {
760 Some(left_obj) => (**left_obj).clone(),
761 None => break,
762 };
763 let mut j = i + 1;
764 while j < len {
765 let right_obj = match x.list.get(j) {
766 Some(right_obj) => (**right_obj).clone(),
767 None => break,
768 };
769 let not_equal_atomic_fact =
770 NotEqualFact::new(left_obj.clone(), right_obj, default_line_file()).into();
771 let verify_result = self
772 .verify_atomic_fact(¬_equal_atomic_fact, &next_verify_state)
773 .map_err(|previous_error| {
774 RuntimeError::from(WellDefinedRuntimeError(
775 RuntimeErrorStruct::new_with_msg_and_cause(
776 format!(
777 "failed to verify list set elements are pairwise not equal: {}",
778 not_equal_atomic_fact
779 ),
780 previous_error,
781 ),
782 ))
783 })?;
784 if verify_result.is_unknown() {
785 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)))));
786 }
787 j += 1;
788 }
789 i += 1;
790 }
791
792 Ok(())
793 }
794
795 fn verify_set_builder_well_defined(
796 &mut self,
797 x: &SetBuilder,
798 verify_state: &VerifyState,
799 ) -> Result<(), RuntimeError> {
800 self.run_in_local_env(|rt| {
805 if let Err(well_defined_error) = rt
806 .verify_obj_well_defined_and_store_cache(&x.param_set, &VerifyState::new(0, false))
807 {
808 return Err(RuntimeError::from(WellDefinedRuntimeError(
809 RuntimeErrorStruct::new_with_msg_and_cause(
810 format!(
811 "failed to verify well-defined of set builder {}",
812 x.to_string()
813 ),
814 well_defined_error,
815 ),
816 )));
817 }
818 if let Err(e) =
819 rt.store_free_param_or_identifier_name(&x.param, ParamObjType::SetBuilder)
820 {
821 return Err(RuntimeError::from(WellDefinedRuntimeError(
822 RuntimeErrorStruct::new_with_msg_and_cause(
823 format!(
824 "failed to verify well-defined of set builder {}",
825 x.to_string()
826 ),
827 e,
828 ),
829 )));
830 }
831 let param_in_set: Fact = InFact::new(
832 obj_for_bound_param_in_scope(x.param.clone(), ParamObjType::SetBuilder),
833 (*x.param_set).clone(),
834 default_line_file(),
835 )
836 .into();
837 if let Err(e) =
838 rt.verify_well_defined_and_store_and_infer_with_default_verify_state(param_in_set)
839 {
840 return Err(RuntimeError::from(WellDefinedRuntimeError(
841 RuntimeErrorStruct::new_with_msg_and_cause(
842 format!(
843 "failed to verify well-defined of set builder {}",
844 x.to_string()
845 ),
846 e,
847 ),
848 )));
849 }
850
851 for fact in x.facts.iter() {
852 if let Err(e) = rt.verify_or_and_chain_atomic_fact_well_defined_and_store_and_infer(
853 fact,
854 verify_state,
855 ) {
856 return Err(RuntimeError::from(WellDefinedRuntimeError(
857 RuntimeErrorStruct::new_with_msg_and_cause(
858 format!(
859 "failed to verify well-defined of set builder {}",
860 x.to_string()
861 ),
862 e,
863 ),
864 )));
865 }
866 }
867
868 Ok(())
869 })
870 }
871
872 fn verify_fn_set_well_defined(
873 &mut self,
874 x: &FnSet,
875 verify_state: &VerifyState,
876 ) -> Result<(), RuntimeError> {
877 for param_def_with_set in x.body.params_def_with_set.iter() {
878 if let Err(e) = self.define_params_with_set(param_def_with_set) {
879 return Err(RuntimeError::from(WellDefinedRuntimeError(
880 RuntimeErrorStruct::new_with_msg_and_cause(
881 format!(
882 "failed to verify well-defined of fn set with dom {}",
883 x.to_string()
884 ),
885 e,
886 ),
887 )));
888 }
889 }
890
891 for fact in x.body.dom_facts.iter() {
892 if let Err(e) = self.verify_or_and_chain_atomic_fact_well_defined_and_store_and_infer(
893 fact,
894 verify_state,
895 ) {
896 return Err(RuntimeError::from(WellDefinedRuntimeError(
897 RuntimeErrorStruct::new_with_msg_and_cause(
898 format!(
899 "failed to verify well-defined of fn set with dom {}",
900 x.to_string()
901 ),
902 e,
903 ),
904 )));
905 }
906 }
907
908 if let Err(e) = self.verify_obj_well_defined_and_store_cache(&x.body.ret_set, verify_state)
909 {
910 return Err(RuntimeError::from(WellDefinedRuntimeError(
911 RuntimeErrorStruct::new_with_msg_and_cause(
912 format!(
913 "failed to verify well-defined of fn set with dom {}",
914 x.to_string()
915 ),
916 e,
917 ),
918 )));
919 }
920
921 Ok(())
922 }
923
924 fn verify_anonymous_fn_well_defined(
925 &mut self,
926 x: &AnonymousFn,
927 verify_state: &VerifyState,
928 ) -> Result<(), RuntimeError> {
929 self.run_in_local_env(|rt| {
930 for param_def_with_set in x.body.params_def_with_set.iter() {
931 if let Err(e) =
932 rt.define_params_with_set_in_scope(param_def_with_set, ParamObjType::FnSet)
933 {
934 return Err(RuntimeError::from(WellDefinedRuntimeError(
935 RuntimeErrorStruct::new_with_msg_and_cause(
936 format!(
937 "failed to verify well-defined of anonymous fn {}",
938 x.to_string()
939 ),
940 e,
941 ),
942 )));
943 }
944 }
945
946 for fact in x.body.dom_facts.iter() {
947 if let Err(e) = rt.verify_or_and_chain_atomic_fact_well_defined_and_store_and_infer(
948 fact,
949 verify_state,
950 ) {
951 return Err(RuntimeError::from(WellDefinedRuntimeError(
952 RuntimeErrorStruct::new_with_msg_and_cause(
953 format!(
954 "failed to verify well-defined of anonymous fn {}",
955 x.to_string()
956 ),
957 e,
958 ),
959 )));
960 }
961 }
962
963 if let Err(e) =
964 rt.verify_obj_well_defined_and_store_cache(&x.body.ret_set, verify_state)
965 {
966 return Err(RuntimeError::from(WellDefinedRuntimeError(
967 RuntimeErrorStruct::new_with_msg_and_cause(
968 format!(
969 "failed to verify well-defined of anonymous fn {}",
970 x.to_string()
971 ),
972 e,
973 ),
974 )));
975 }
976
977 if let Err(e) = rt.verify_obj_well_defined_and_store_cache(&x.equal_to, verify_state) {
978 return Err(RuntimeError::from(WellDefinedRuntimeError(
979 RuntimeErrorStruct::new_with_msg_and_cause(
980 format!(
981 "failed to verify well-defined of anonymous fn {}",
982 x.to_string()
983 ),
984 e,
985 ),
986 )));
987 }
988
989 Ok(())
990 })
991 }
992
993 fn verify_n_pos_obj_well_defined(&mut self) -> Result<(), RuntimeError> {
994 Ok(())
995 }
996
997 fn verify_n_obj_well_defined(&mut self) -> Result<(), RuntimeError> {
998 Ok(())
999 }
1000
1001 fn verify_q_obj_well_defined(&self) -> Result<(), RuntimeError> {
1002 Ok(())
1003 }
1004
1005 fn verify_z_obj_well_defined(&self) -> Result<(), RuntimeError> {
1006 Ok(())
1007 }
1008
1009 fn verify_r_obj_well_defined(&self) -> Result<(), RuntimeError> {
1010 Ok(())
1011 }
1012
1013 fn verify_cart_well_defined(
1014 &mut self,
1015 x: &Cart,
1016 verify_state: &VerifyState,
1017 ) -> Result<(), RuntimeError> {
1018 for obj in &x.args {
1019 self.verify_obj_well_defined_and_store_cache(obj, verify_state)?;
1020 }
1021 Ok(())
1022 }
1023
1024 fn verify_cart_dim_well_defined(
1025 &mut self,
1026 x: &CartDim,
1027 verify_state: &VerifyState,
1028 ) -> Result<(), RuntimeError> {
1029 self.verify_obj_well_defined_and_store_cache(&x.set, verify_state)?;
1030
1031 let is_cart_fact = IsCartFact::new((*x.set).clone(), default_line_file()).into();
1032 let result = self.verify_atomic_fact(&is_cart_fact, verify_state)?;
1033 if result.is_unknown() {
1034 return Err(RuntimeError::from(WellDefinedRuntimeError(
1035 RuntimeErrorStruct::new_with_just_msg(format!(
1036 "set {} is not a cart",
1037 x.set.to_string()
1038 )),
1039 )));
1040 }
1041
1042 Ok(())
1043 }
1044
1045 fn verify_proj_well_defined(
1046 &mut self,
1047 x: &Proj,
1048 verify_state: &VerifyState,
1049 ) -> Result<(), RuntimeError> {
1050 self.verify_obj_well_defined_and_store_cache(&x.set, verify_state)?;
1051 self.verify_obj_well_defined_and_store_cache(&x.dim, verify_state)?;
1052
1053 let projection_dimension_number = self.resolve_obj_to_number(&x.dim).ok_or_else(|| {
1054 RuntimeError::from(WellDefinedRuntimeError(
1055 RuntimeErrorStruct::new_with_just_msg(format!(
1056 "projection dimension {} is not a number",
1057 x.dim
1058 )),
1059 ))
1060 })?;
1061 let projection_dimension_obj: Obj =
1062 Number::new(projection_dimension_number.normalized_value).into();
1063
1064 let projection_dimension_is_positive_integer_fact = InFact::new(
1065 projection_dimension_obj.clone(),
1066 StandardSet::NPos.into(),
1067 default_line_file(),
1068 )
1069 .into();
1070 let projection_dimension_is_positive_integer_result =
1071 self.verify_atomic_fact(&projection_dimension_is_positive_integer_fact, verify_state)?;
1072 if projection_dimension_is_positive_integer_result.is_unknown() {
1073 return Err(RuntimeError::from(WellDefinedRuntimeError(
1074 RuntimeErrorStruct::new_with_just_msg(format!(
1075 "projection dimension {} is not a positive integer",
1076 projection_dimension_obj
1077 )),
1078 )));
1079 }
1080
1081 let left_set_is_cart_fact = IsCartFact::new((*x.set).clone(), default_line_file()).into();
1082 let left_set_is_cart_result =
1083 self.verify_atomic_fact(&left_set_is_cart_fact, verify_state)?;
1084 if left_set_is_cart_result.is_unknown() {
1085 return Err(RuntimeError::from(WellDefinedRuntimeError(
1086 RuntimeErrorStruct::new_with_just_msg(format!(
1087 "projection left side {} is not a cart",
1088 x.set
1089 )),
1090 )));
1091 }
1092
1093 let left_set_cart_dim_obj: Obj = CartDim::new((*x.set).clone()).into();
1094
1095 let proj_index_not_larger_than_cart_dim = LessEqualFact::new(
1096 projection_dimension_obj.clone(),
1097 left_set_cart_dim_obj.clone(),
1098 default_line_file(),
1099 )
1100 .into();
1101 let left_set_cart_dim_less_equal_projection_dimension_result =
1102 self.verify_atomic_fact(&proj_index_not_larger_than_cart_dim, verify_state)?;
1103 if left_set_cart_dim_less_equal_projection_dimension_result.is_unknown() {
1104 return Err(RuntimeError::from(WellDefinedRuntimeError(
1105 RuntimeErrorStruct::new_with_just_msg(format!(
1106 "{} <= {} is unknown",
1107 projection_dimension_obj, left_set_cart_dim_obj
1108 )),
1109 )));
1110 }
1111
1112 Ok(())
1113 }
1114
1115 fn verify_dim_well_defined(
1116 &mut self,
1117 x: &TupleDim,
1118 verify_state: &VerifyState,
1119 ) -> Result<(), RuntimeError> {
1120 self.verify_obj_well_defined_and_store_cache(&x.arg, verify_state)?;
1121
1122 let is_tuple_fact = IsTupleFact::new((*x.arg).clone(), default_line_file()).into();
1123 let result = self.verify_atomic_fact(&is_tuple_fact, verify_state)?;
1124 if result.is_unknown() {
1125 return Err(RuntimeError::from(WellDefinedRuntimeError(
1126 RuntimeErrorStruct::new_with_just_msg(format!(
1127 "`{}` is unknown, `dim` object requires its argument to be a tuple",
1128 is_tuple_fact
1129 )),
1130 )));
1131 }
1132
1133 Ok(())
1134 }
1135
1136 fn verify_tuple_well_defined(
1137 &mut self,
1138 x: &Tuple,
1139 verify_state: &VerifyState,
1140 ) -> Result<(), RuntimeError> {
1141 for obj in &x.args {
1142 self.verify_obj_well_defined_and_store_cache(obj, verify_state)?;
1143 }
1144 Ok(())
1145 }
1146
1147 fn verify_count_well_defined(
1148 &mut self,
1149 x: &Count,
1150 verify_state: &VerifyState,
1151 ) -> Result<(), RuntimeError> {
1152 let is_finite_set_fact = IsFiniteSetFact::new((*x.set).clone(), default_line_file()).into();
1154 let result = self.verify_atomic_fact(&is_finite_set_fact, verify_state)?;
1155 if result.is_unknown() {
1156 return Err(RuntimeError::from(WellDefinedRuntimeError(
1157 RuntimeErrorStruct::new_with_just_msg(format!(
1158 "set {} is not a finite set",
1159 x.set.to_string()
1160 )),
1161 )));
1162 }
1163 Ok(())
1164 }
1165
1166 fn verify_sum_obj_well_defined(
1167 &mut self,
1168 x: &Sum,
1169 verify_state: &VerifyState,
1170 ) -> Result<(), RuntimeError> {
1171 self.verify_obj_well_defined_and_store_cache(&x.start, verify_state)?;
1172 self.verify_obj_well_defined_and_store_cache(&x.end, verify_state)?;
1173 self.require_obj_in_z(&x.start, verify_state)?;
1174 self.require_obj_in_z(&x.end, verify_state)?;
1175 if self.range_endpoints_are_numeric_for_interval_order_check(&x.start, &x.end) {
1176 self.require_less_equal_verified(
1177 &x.start,
1178 &x.end,
1179 verify_state,
1180 "sum: cannot verify start <= end for the summation range".to_string(),
1181 )?;
1182 }
1183 self.verify_obj_well_defined_and_store_cache(&x.func, verify_state)?;
1184 self.verify_iterated_op_summand_under_integer_index_interval(
1185 &x.func,
1186 x.start.as_ref(),
1187 x.end.as_ref(),
1188 verify_state,
1189 "sum",
1190 )
1191 }
1192
1193 fn verify_product_obj_well_defined(
1194 &mut self,
1195 x: &Product,
1196 verify_state: &VerifyState,
1197 ) -> Result<(), RuntimeError> {
1198 self.verify_obj_well_defined_and_store_cache(&x.start, verify_state)?;
1199 self.verify_obj_well_defined_and_store_cache(&x.end, verify_state)?;
1200 self.require_obj_in_z(&x.start, verify_state)?;
1201 self.require_obj_in_z(&x.end, verify_state)?;
1202 if self.range_endpoints_are_numeric_for_interval_order_check(&x.start, &x.end) {
1203 self.require_less_equal_verified(
1204 &x.start,
1205 &x.end,
1206 verify_state,
1207 "product: cannot verify start <= end for the product range".to_string(),
1208 )?;
1209 }
1210 self.verify_obj_well_defined_and_store_cache(&x.func, verify_state)?;
1211 self.verify_iterated_op_summand_under_integer_index_interval(
1212 &x.func,
1213 x.start.as_ref(),
1214 x.end.as_ref(),
1215 verify_state,
1216 "product",
1217 )
1218 }
1219
1220 fn unary_param_set_from_params_def(
1222 params_def: &[ParamGroupWithSet],
1223 pname: &str,
1224 ) -> Option<Obj> {
1225 for g in params_def {
1226 if g.params.iter().any(|n| n == pname) {
1227 return Some(g.set.clone());
1228 }
1229 }
1230 None
1231 }
1232
1233 fn verify_closed_range_each_integer_satisfies_unary_param_set(
1236 &mut self,
1237 start: &Obj,
1238 end: &Obj,
1239 param_set: &Obj,
1240 verify_state: &VerifyState,
1241 op: &str,
1242 ) -> Result<(), RuntimeError> {
1243 let Some(a_num) = self.resolve_obj_to_number(start) else {
1244 return Ok(());
1245 };
1246 let Some(b_num) = self.resolve_obj_to_number(end) else {
1247 return Ok(());
1248 };
1249 let as_ = a_num.normalized_value.trim();
1250 let bs = b_num.normalized_value.trim();
1251 if !is_number_string_literally_integer_without_dot(as_.to_string())
1252 || !is_number_string_literally_integer_without_dot(bs.to_string())
1253 {
1254 return Ok(());
1255 }
1256 let Some(ai) = as_.parse::<i128>().ok() else {
1257 return Ok(());
1258 };
1259 let Some(bi) = bs.parse::<i128>().ok() else {
1260 return Ok(());
1261 };
1262 if ai > bi {
1263 return Ok(());
1264 }
1265 for k in ai..=bi {
1266 let k_obj: Obj = Number::new(k.to_string()).into();
1267 let in_fact = InFact::new(k_obj, param_set.clone(), default_line_file());
1268 let atomic_fact = AtomicFact::InFact(in_fact);
1269 let result = self.verify_atomic_fact(&atomic_fact, verify_state)?;
1270 if result.is_unknown() {
1271 return Err(RuntimeError::from(WellDefinedRuntimeError(
1272 RuntimeErrorStruct::new_with_just_msg(format!(
1273 "{op}: each integer in the closed range from {} to {} must belong to the index parameter's type; not satisfied at index {}",
1274 start, end, k
1275 )),
1276 )));
1277 }
1278 }
1279 Ok(())
1280 }
1281
1282 fn verify_iterated_op_summand_with_stored_fn_set_body(
1283 &mut self,
1284 fs_body: FnSetBody,
1285 start: &Obj,
1286 end: &Obj,
1287 verify_state: &VerifyState,
1288 op: &str,
1289 ) -> Result<(), RuntimeError> {
1290 if ParamGroupWithSet::number_of_params(&fs_body.params_def_with_set) != 1 {
1291 return Err(RuntimeError::from(WellDefinedRuntimeError(
1292 RuntimeErrorStruct::new_with_just_msg(format!(
1293 "{op}: the function in the function set must be unary (one index)"
1294 )),
1295 )));
1296 }
1297 let param_names = ParamGroupWithSet::collect_param_names(&fs_body.params_def_with_set);
1298 let pname = param_names[0].clone();
1299 let Some(param_set_for_index) =
1300 Self::unary_param_set_from_params_def(&fs_body.params_def_with_set, &pname)
1301 else {
1302 return Err(RuntimeError::from(WellDefinedRuntimeError(
1303 RuntimeErrorStruct::new_with_just_msg(format!(
1304 "{op}: could not find index parameter in params_def_with_set"
1305 )),
1306 )));
1307 };
1308 self.verify_closed_range_each_integer_satisfies_unary_param_set(
1309 start,
1310 end,
1311 ¶m_set_for_index,
1312 verify_state,
1313 op,
1314 )?;
1315 let start_c = start.clone();
1316 let end_c = end.clone();
1317 self.run_in_local_env(|rt| {
1318 for g in fs_body.params_def_with_set.iter() {
1319 rt.define_params_with_set_in_scope(g, ParamObjType::FnSet)
1320 .map_err(|e| {
1321 RuntimeError::from(WellDefinedRuntimeError(
1322 RuntimeErrorStruct::new_with_msg_and_cause(
1323 format!(
1324 "{op}: could not bind index parameter in local well-defined check"
1325 ),
1326 e,
1327 ),
1328 ))
1329 })?;
1330 }
1331 let k: Obj = Identifier::new(pname).into();
1332 let le_lo = OrAndChainAtomicFact::AtomicFact(
1333 LessEqualFact::new(start_c.clone(), k.clone(), default_line_file()).into(),
1334 );
1335 let le_hi = OrAndChainAtomicFact::AtomicFact(
1336 LessEqualFact::new(k, end_c.clone(), default_line_file()).into(),
1337 );
1338 rt.store_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(le_lo)
1339 .map_err(|e| {
1340 RuntimeError::from(WellDefinedRuntimeError(
1341 RuntimeErrorStruct::new_with_msg_and_cause(
1342 format!("{op}: could not add lower bound in local check"),
1343 e,
1344 ),
1345 ))
1346 })?;
1347 rt.store_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(le_hi)
1348 .map_err(|e| {
1349 RuntimeError::from(WellDefinedRuntimeError(
1350 RuntimeErrorStruct::new_with_msg_and_cause(
1351 format!("{op}: could not add upper bound in local check"),
1352 e,
1353 ),
1354 ))
1355 })?;
1356 for df in fs_body.dom_facts.iter() {
1357 rt.verify_or_and_chain_atomic_fact_well_defined_and_store_and_infer(
1358 df,
1359 verify_state,
1360 )
1361 .map_err(|e| {
1362 RuntimeError::from(WellDefinedRuntimeError(
1363 RuntimeErrorStruct::new_with_msg_and_cause(
1364 format!("{op}: function set dom in local check failed"),
1365 e,
1366 ),
1367 ))
1368 })?;
1369 }
1370 rt.verify_obj_well_defined_and_store_cache(&fs_body.ret_set, verify_state)
1371 .map_err(|e| {
1372 RuntimeError::from(WellDefinedRuntimeError(
1373 RuntimeErrorStruct::new_with_msg_and_cause(
1374 format!("{op}: return set not well-defined on the integer range"),
1375 e,
1376 ),
1377 ))
1378 })
1379 })
1380 }
1381
1382 fn verify_iterated_op_summand_under_integer_index_interval(
1383 &mut self,
1384 func: &Obj,
1385 start: &Obj,
1386 end: &Obj,
1387 verify_state: &VerifyState,
1388 op: &str,
1389 ) -> Result<(), RuntimeError> {
1390 if let Some(af) = Self::summand_as_unary_anonymous_fn(func) {
1391 return self.verify_unary_iterated_anonymous_in_interval(
1392 af,
1393 start,
1394 end,
1395 verify_state,
1396 op,
1397 );
1398 }
1399 if let Obj::FnObj(fo) = func {
1400 if !fo.body.is_empty() {
1401 return Err(RuntimeError::from(WellDefinedRuntimeError(
1402 RuntimeErrorStruct::new_with_just_msg(format!(
1403 "{op}: expected a bare function as summand, not a function application"
1404 )),
1405 )));
1406 }
1407 let function_name_obj: Obj = (*fo.head).clone().into();
1408 let Some(fs_body) = self
1409 .get_object_in_fn_set_or_restrict(&function_name_obj)
1410 .cloned()
1411 else {
1412 return Err(RuntimeError::from(WellDefinedRuntimeError(
1413 RuntimeErrorStruct::new_with_just_msg(format!(
1414 "{op}: summand must be a unary anonymous function, or a name with a stored function set; got {}",
1415 func
1416 )),
1417 )));
1418 };
1419 return self.verify_iterated_op_summand_with_stored_fn_set_body(
1420 fs_body,
1421 start,
1422 end,
1423 verify_state,
1424 op,
1425 );
1426 }
1427 if let Some(fs_body) = self.get_cloned_object_in_fn_set_or_restrict(func) {
1428 return self.verify_iterated_op_summand_with_stored_fn_set_body(
1429 fs_body,
1430 start,
1431 end,
1432 verify_state,
1433 op,
1434 );
1435 }
1436 Err(RuntimeError::from(WellDefinedRuntimeError(
1437 RuntimeErrorStruct::new_with_just_msg(format!(
1438 "{op}: summand must be a unary anonymous function, or a defined unary function in a function set; got {}",
1439 func
1440 )),
1441 )))
1442 }
1443
1444 fn summand_as_unary_anonymous_fn(obj: &Obj) -> Option<&AnonymousFn> {
1445 match obj {
1446 Obj::AnonymousFn(af) => Some(af),
1447 Obj::FnObj(fo) => {
1448 if !fo.body.is_empty() {
1449 return None;
1450 }
1451 match fo.head.as_ref() {
1452 FnObjHead::AnonymousFnLiteral(a) => Some(a.as_ref()),
1453 _ => None,
1454 }
1455 }
1456 _ => None,
1457 }
1458 }
1459
1460 fn verify_unary_iterated_anonymous_in_interval(
1461 &mut self,
1462 af: &AnonymousFn,
1463 start: &Obj,
1464 end: &Obj,
1465 verify_state: &VerifyState,
1466 op: &str,
1467 ) -> Result<(), RuntimeError> {
1468 if ParamGroupWithSet::number_of_params(&af.body.params_def_with_set) != 1 {
1469 return Err(RuntimeError::from(WellDefinedRuntimeError(
1470 RuntimeErrorStruct::new_with_just_msg(format!(
1471 "{op}: summation/product index function must be unary (one parameter)"
1472 )),
1473 )));
1474 }
1475 let param_names = ParamGroupWithSet::collect_param_names(&af.body.params_def_with_set);
1476 let pname = param_names[0].clone();
1477 let Some(param_set_for_index) =
1478 Self::unary_param_set_from_params_def(&af.body.params_def_with_set, &pname)
1479 else {
1480 return Err(RuntimeError::from(WellDefinedRuntimeError(
1481 RuntimeErrorStruct::new_with_just_msg(format!(
1482 "{op}: could not find index parameter in params_def_with_set"
1483 )),
1484 )));
1485 };
1486 self.verify_closed_range_each_integer_satisfies_unary_param_set(
1487 start,
1488 end,
1489 ¶m_set_for_index,
1490 verify_state,
1491 op,
1492 )?;
1493 self.run_in_local_env(|rt| {
1494 for g in af.body.params_def_with_set.iter() {
1495 rt.define_params_with_set_in_scope(g, ParamObjType::FnSet)
1496 .map_err(|e| {
1497 RuntimeError::from(WellDefinedRuntimeError(RuntimeErrorStruct::new_with_msg_and_cause(format!("{op}: could not bind index parameter in local well-defined check"), e)))
1498 })?;
1499 }
1500 let k: Obj = Identifier::new(pname).into();
1501 let le_lo = OrAndChainAtomicFact::AtomicFact(
1502 LessEqualFact::new(start.clone(), k.clone(), default_line_file()).into(),
1503 );
1504 let le_hi = OrAndChainAtomicFact::AtomicFact(
1505 LessEqualFact::new(k, end.clone(), default_line_file()).into(),
1506 );
1507 rt.store_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(le_lo)
1508 .map_err(|e| {
1509 RuntimeError::from(WellDefinedRuntimeError(RuntimeErrorStruct::new_with_msg_and_cause(format!("{op}: could not add lower bound in local check"), e)))
1510 })?;
1511 rt.store_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(le_hi)
1512 .map_err(|e| {
1513 RuntimeError::from(WellDefinedRuntimeError(RuntimeErrorStruct::new_with_msg_and_cause(format!("{op}: could not add upper bound in local check"), e)))
1514 })?;
1515 for df in af.body.dom_facts.iter() {
1516 rt.verify_or_and_chain_atomic_fact_well_defined_and_store_and_infer(
1517 df,
1518 verify_state,
1519 )
1520 .map_err(|e| {
1521 RuntimeError::from(WellDefinedRuntimeError(RuntimeErrorStruct::new_with_msg_and_cause(format!("{op}: local dom of anonymous summand in integer range check failed"), e)))
1522 })?;
1523 }
1524 rt.verify_obj_well_defined_and_store_cache(&af.body.ret_set, verify_state)
1525 .map_err(|e| {
1526 RuntimeError::from(WellDefinedRuntimeError(RuntimeErrorStruct::new_with_msg_and_cause(format!("{op}: return set not well-defined on the integer range"), e)))
1527 })?;
1528 rt.verify_obj_well_defined_and_store_cache(&af.equal_to, verify_state)
1529 .map_err(|e| {
1530 RuntimeError::from(WellDefinedRuntimeError(RuntimeErrorStruct::new_with_msg_and_cause(format!("{op}: expression body not well-defined on the integer range"), e)))
1531 })
1532 })
1533 }
1534
1535 fn verify_range_well_defined(
1536 &mut self,
1537 x: &Range,
1538 verify_state: &VerifyState,
1539 ) -> Result<(), RuntimeError> {
1540 self.verify_obj_well_defined_and_store_cache(&x.start, verify_state)?;
1541 self.verify_obj_well_defined_and_store_cache(&x.end, verify_state)?;
1542 self.require_obj_in_z(&x.start, verify_state)?;
1543 self.require_obj_in_z(&x.end, verify_state)?;
1544 if self.range_endpoints_are_numeric_for_interval_order_check(&x.start, &x.end) {
1545 self.require_less_equal_verified(
1546 &x.start,
1547 &x.end,
1548 verify_state,
1549 format!(
1550 "range: cannot verify {} <= {} (numeric half-open interval needs lower <= upper)",
1551 x.start, x.end
1552 ),
1553 )?;
1554 }
1555 Ok(())
1556 }
1557
1558 fn verify_closed_range_well_defined(
1559 &mut self,
1560 x: &ClosedRange,
1561 verify_state: &VerifyState,
1562 ) -> Result<(), RuntimeError> {
1563 self.verify_obj_well_defined_and_store_cache(&x.start, verify_state)?;
1564 self.verify_obj_well_defined_and_store_cache(&x.end, verify_state)?;
1565 self.require_obj_in_z(&x.start, verify_state)?;
1566 self.require_obj_in_z(&x.end, verify_state)?;
1567 if self.range_endpoints_are_numeric_for_interval_order_check(&x.start, &x.end) {
1568 self.require_less_equal_verified(
1569 &x.start,
1570 &x.end,
1571 verify_state,
1572 format!(
1573 "closed_range: cannot verify {} <= {} (numeric closed interval needs lower <= upper)",
1574 x.start, x.end
1575 ),
1576 )?;
1577 }
1578 Ok(())
1579 }
1580
1581 fn verify_finite_seq_set_well_defined(
1582 &mut self,
1583 x: &FiniteSeqSet,
1584 verify_state: &VerifyState,
1585 ) -> Result<(), RuntimeError> {
1586 self.verify_obj_well_defined_and_store_cache(&x.set, verify_state)?;
1587 self.verify_obj_well_defined_and_store_cache(&x.n, verify_state)?;
1588 let is_set_fact = IsSetFact::new((*x.set).clone(), default_line_file()).into();
1589 let set_ok = self.verify_atomic_fact(&is_set_fact, verify_state)?;
1590 if set_ok.is_unknown() {
1591 return Err(RuntimeError::from(WellDefinedRuntimeError(
1592 RuntimeErrorStruct::new_with_just_msg(format!(
1593 "finite_seq_set: first argument {} is not a set",
1594 x.set
1595 )),
1596 )));
1597 }
1598 let n_in_n_pos = InFact::new(
1599 (*x.n).clone(),
1600 StandardSet::NPos.into(),
1601 default_line_file(),
1602 )
1603 .into();
1604 let n_ok = self.verify_atomic_fact(&n_in_n_pos, verify_state)?;
1605 if n_ok.is_unknown() {
1606 return Err(RuntimeError::from(WellDefinedRuntimeError(
1607 RuntimeErrorStruct::new_with_just_msg(format!(
1608 "finite_seq_set: length argument {} is not verified in N_pos",
1609 x.n
1610 )),
1611 )));
1612 }
1613 Ok(())
1614 }
1615
1616 fn verify_seq_set_well_defined(
1617 &mut self,
1618 x: &SeqSet,
1619 verify_state: &VerifyState,
1620 ) -> Result<(), RuntimeError> {
1621 self.verify_obj_well_defined_and_store_cache(&x.set, verify_state)?;
1622 let is_set_fact = IsSetFact::new((*x.set).clone(), default_line_file()).into();
1623 let set_ok = self.verify_atomic_fact(&is_set_fact, verify_state)?;
1624 if set_ok.is_unknown() {
1625 return Err(RuntimeError::from(WellDefinedRuntimeError(
1626 RuntimeErrorStruct::new_with_just_msg(format!(
1627 "seq: argument {} is not a set",
1628 x.set
1629 )),
1630 )));
1631 }
1632 Ok(())
1633 }
1634
1635 fn verify_finite_seq_list_obj_well_defined(
1636 &mut self,
1637 x: &FiniteSeqListObj,
1638 verify_state: &VerifyState,
1639 ) -> Result<(), RuntimeError> {
1640 for o in x.objs.iter() {
1641 self.verify_obj_well_defined_and_store_cache(o, verify_state)?;
1642 }
1643 Ok(())
1644 }
1645
1646 fn verify_matrix_set_well_defined(
1647 &mut self,
1648 x: &MatrixSet,
1649 verify_state: &VerifyState,
1650 ) -> Result<(), RuntimeError> {
1651 self.verify_obj_well_defined_and_store_cache(&x.set, verify_state)?;
1652 self.verify_obj_well_defined_and_store_cache(&x.row_len, verify_state)?;
1653 self.verify_obj_well_defined_and_store_cache(&x.col_len, verify_state)?;
1654 let is_set_fact = IsSetFact::new((*x.set).clone(), default_line_file()).into();
1655 let set_ok = self.verify_atomic_fact(&is_set_fact, verify_state)?;
1656 if set_ok.is_unknown() {
1657 return Err(RuntimeError::from(WellDefinedRuntimeError(
1658 RuntimeErrorStruct::new_with_just_msg(format!(
1659 "matrix: first argument {} is not a set",
1660 x.set
1661 )),
1662 )));
1663 }
1664 for (label, len_obj) in [("row_len", &x.row_len), ("col_len", &x.col_len)] {
1665 let in_n_pos = InFact::new(
1666 (**len_obj).clone(),
1667 StandardSet::NPos.into(),
1668 default_line_file(),
1669 )
1670 .into();
1671 let ok = self.verify_atomic_fact(&in_n_pos, verify_state)?;
1672 if ok.is_unknown() {
1673 return Err(RuntimeError::from(WellDefinedRuntimeError(
1674 RuntimeErrorStruct::new_with_just_msg(format!(
1675 "matrix: {} argument {} is not verified in N_pos",
1676 label, len_obj
1677 )),
1678 )));
1679 }
1680 }
1681 Ok(())
1682 }
1683
1684 fn verify_matrix_list_obj_well_defined(
1685 &mut self,
1686 x: &MatrixListObj,
1687 verify_state: &VerifyState,
1688 ) -> Result<(), RuntimeError> {
1689 if !x.rows.is_empty() {
1690 let col_len = x.rows[0].len();
1691 for row in x.rows.iter() {
1692 if row.len() != col_len {
1693 return Err(RuntimeError::from(WellDefinedRuntimeError(
1694 RuntimeErrorStruct::new_with_just_msg(format!(
1695 "matrix literal: row length {} differs from first row length {}",
1696 row.len(),
1697 col_len
1698 )),
1699 )));
1700 }
1701 }
1702 }
1703 for row in x.rows.iter() {
1704 for o in row.iter() {
1705 self.verify_obj_well_defined_and_store_cache(o, verify_state)?;
1706 }
1707 }
1708 Ok(())
1709 }
1710
1711 fn verify_matrix_add_well_defined(
1712 &mut self,
1713 ma: &MatrixAdd,
1714 verify_state: &VerifyState,
1715 ) -> Result<(), RuntimeError> {
1716 self.verify_obj_well_defined_and_store_cache(&ma.left, verify_state)?;
1717 self.verify_obj_well_defined_and_store_cache(&ma.right, verify_state)?;
1718 let shape_left = Self::matrix_value_shape(self, &ma.left)?;
1719 let shape_right = Self::matrix_value_shape(self, &ma.right)?;
1720 if shape_left != shape_right {
1721 return Err(RuntimeError::from(WellDefinedRuntimeError(
1722 RuntimeErrorStruct::new_with_just_msg(format!(
1723 "matrix ++: shape {:?} and {:?} do not match",
1724 shape_left, shape_right
1725 )),
1726 )));
1727 }
1728 Ok(())
1729 }
1730
1731 fn verify_matrix_sub_well_defined(
1732 &mut self,
1733 ms: &MatrixSub,
1734 verify_state: &VerifyState,
1735 ) -> Result<(), RuntimeError> {
1736 self.verify_obj_well_defined_and_store_cache(&ms.left, verify_state)?;
1737 self.verify_obj_well_defined_and_store_cache(&ms.right, verify_state)?;
1738 let shape_left = Self::matrix_value_shape(self, &ms.left)?;
1739 let shape_right = Self::matrix_value_shape(self, &ms.right)?;
1740 if shape_left != shape_right {
1741 return Err(RuntimeError::from(WellDefinedRuntimeError(
1742 RuntimeErrorStruct::new_with_just_msg(format!(
1743 "matrix --: shape {:?} and {:?} do not match",
1744 shape_left, shape_right
1745 )),
1746 )));
1747 }
1748 Ok(())
1749 }
1750
1751 fn verify_matrix_mul_well_defined(
1752 &mut self,
1753 mm: &MatrixMul,
1754 verify_state: &VerifyState,
1755 ) -> Result<(), RuntimeError> {
1756 self.verify_obj_well_defined_and_store_cache(&mm.left, verify_state)?;
1757 self.verify_obj_well_defined_and_store_cache(&mm.right, verify_state)?;
1758 let shape_left = Self::matrix_value_shape(self, &mm.left)?;
1759 let shape_right = Self::matrix_value_shape(self, &mm.right)?;
1760 if shape_left.1 != shape_right.0 {
1761 return Err(RuntimeError::from(WellDefinedRuntimeError(
1762 RuntimeErrorStruct::new_with_just_msg(format!(
1763 "matrix **: left columns {} != right rows {}",
1764 shape_left.1, shape_right.0
1765 )),
1766 )));
1767 }
1768 Ok(())
1769 }
1770
1771 fn verify_matrix_scalar_mul_well_defined(
1772 &mut self,
1773 m: &MatrixScalarMul,
1774 verify_state: &VerifyState,
1775 ) -> Result<(), RuntimeError> {
1776 self.verify_obj_well_defined_and_store_cache(&m.scalar, verify_state)?;
1777 self.verify_obj_well_defined_and_store_cache(&m.matrix, verify_state)?;
1778 let _ = Self::matrix_value_shape(self, &m.matrix)?;
1779 Ok(())
1780 }
1781
1782 fn verify_matrix_pow_well_defined(
1783 &mut self,
1784 m: &MatrixPow,
1785 verify_state: &VerifyState,
1786 ) -> Result<(), RuntimeError> {
1787 self.verify_obj_well_defined_and_store_cache(&m.base, verify_state)?;
1788 self.verify_obj_well_defined_and_store_cache(&m.exponent, verify_state)?;
1789 let shape_base = Self::matrix_value_shape(self, &m.base)?;
1790 if shape_base.0 != shape_base.1 {
1791 return Err(RuntimeError::from(WellDefinedRuntimeError(
1792 RuntimeErrorStruct::new_with_just_msg(format!(
1793 "matrix ^^: base must be square, got {}x{}",
1794 shape_base.0, shape_base.1
1795 )),
1796 )));
1797 }
1798 let exp_in_n_pos = InFact::new(
1799 (*m.exponent).clone(),
1800 StandardSet::NPos.into(),
1801 default_line_file(),
1802 )
1803 .into();
1804 let ok = self.verify_atomic_fact(&exp_in_n_pos, verify_state)?;
1805 if ok.is_unknown() {
1806 return Err(RuntimeError::from(WellDefinedRuntimeError(
1807 RuntimeErrorStruct::new_with_just_msg(format!(
1808 "matrix ^^: exponent {} is not verified in N_pos",
1809 m.exponent
1810 )),
1811 )));
1812 }
1813 Ok(())
1814 }
1815
1816 fn matrix_value_shape(rt: &Runtime, obj: &Obj) -> Result<(usize, usize), RuntimeError> {
1818 match obj {
1819 Obj::MatrixListObj(m) => Self::rectangular_shape_of_matrix_list_obj(m),
1820 Obj::Atom(AtomObj::Identifier(id)) => {
1821 Self::matrix_list_shape_for_name_known_as_matrix_list(rt, &id.name)
1822 }
1823 Obj::MatrixAdd(inner) => Self::matrix_value_shape(rt, &inner.left),
1824 Obj::MatrixSub(inner) => Self::matrix_value_shape(rt, &inner.left),
1825 Obj::MatrixMul(inner) => {
1826 let sl = Self::matrix_value_shape(rt, &inner.left)?;
1827 let sr = Self::matrix_value_shape(rt, &inner.right)?;
1828 if sl.1 != sr.0 {
1829 return Err(RuntimeError::from(WellDefinedRuntimeError(
1830 RuntimeErrorStruct::new_with_just_msg(format!(
1831 "matrix **: left columns {} != right rows {}",
1832 sl.1, sr.0
1833 )),
1834 )));
1835 }
1836 Ok((sl.0, sr.1))
1837 }
1838 Obj::MatrixScalarMul(inner) => Self::matrix_value_shape(rt, &inner.matrix),
1839 Obj::MatrixPow(inner) => {
1840 let s = Self::matrix_value_shape(rt, &inner.base)?;
1841 if s.0 != s.1 {
1842 return Err(RuntimeError::from(WellDefinedRuntimeError(
1843 RuntimeErrorStruct::new_with_just_msg(format!(
1844 "matrix ^^: base must be square, got {}x{}",
1845 s.0, s.1
1846 )),
1847 )));
1848 }
1849 Ok(s)
1850 }
1851 _ => Self::matrix_list_shape_for_name_known_as_matrix_list(rt, &obj.to_string()),
1852 }
1853 }
1854
1855 fn matrix_list_shape_for_name_known_as_matrix_list(
1858 rt: &Runtime,
1859 key: &str,
1860 ) -> Result<(usize, usize), RuntimeError> {
1861 let Some(known) = rt.get_obj_equal_to_matrix_list(key) else {
1862 return Err(RuntimeError::from(WellDefinedRuntimeError(
1863 RuntimeErrorStruct::new_with_just_msg(format!(
1864 "`{}` is not known as a matrix list value",
1865 key
1866 )),
1867 )));
1868 };
1869 let shape = Self::rectangular_shape_of_matrix_list_obj(&known)?;
1870 if let Some(ms) = rt.get_matrix_set_for_obj_equal_to_matrix_list(key) {
1871 Self::ensure_matrix_list_matches_matrix_set(rt, &known, &ms)?;
1872 }
1873 Ok(shape)
1874 }
1875
1876 fn ensure_matrix_list_matches_matrix_set(
1877 rt: &Runtime,
1878 m: &MatrixListObj,
1879 ms: &MatrixSet,
1880 ) -> Result<(), RuntimeError> {
1881 let (rows, cols) = Self::rectangular_shape_of_matrix_list_obj(m)?;
1882 let row_expect = rt
1883 .resolve_obj_to_number(ms.row_len.as_ref())
1884 .ok_or_else(|| {
1885 RuntimeError::from(WellDefinedRuntimeError(
1886 RuntimeErrorStruct::new_with_just_msg(format!(
1887 "matrix: cannot resolve row_len {} of matrix type for list shape check",
1888 ms.row_len
1889 )),
1890 ))
1891 })?;
1892 let col_expect = rt
1893 .resolve_obj_to_number(ms.col_len.as_ref())
1894 .ok_or_else(|| {
1895 RuntimeError::from(WellDefinedRuntimeError(
1896 RuntimeErrorStruct::new_with_just_msg(format!(
1897 "matrix: cannot resolve col_len {} of matrix type for list shape check",
1898 ms.col_len
1899 )),
1900 ))
1901 })?;
1902 let r = row_expect.normalized_value.parse::<usize>().map_err(|_| {
1903 RuntimeError::from(WellDefinedRuntimeError(
1904 RuntimeErrorStruct::new_with_just_msg(format!(
1905 "matrix: row_len `{}` is not a valid size",
1906 row_expect.normalized_value
1907 )),
1908 ))
1909 })?;
1910 let c = col_expect.normalized_value.parse::<usize>().map_err(|_| {
1911 RuntimeError::from(WellDefinedRuntimeError(
1912 RuntimeErrorStruct::new_with_just_msg(format!(
1913 "matrix: col_len `{}` is not a valid size",
1914 col_expect.normalized_value
1915 )),
1916 ))
1917 })?;
1918 if r != rows || c != cols {
1919 return Err(RuntimeError::from(WellDefinedRuntimeError(
1920 RuntimeErrorStruct::new_with_just_msg(format!(
1921 "matrix list has shape {}x{} but matrix type expects {}x{}",
1922 rows, cols, r, c
1923 )),
1924 )));
1925 }
1926 Ok(())
1927 }
1928
1929 fn rectangular_shape_of_matrix_list_obj(
1930 m: &MatrixListObj,
1931 ) -> Result<(usize, usize), RuntimeError> {
1932 let rows = m.rows.len();
1933 let cols = if rows == 0 { 0 } else { m.rows[0].len() };
1934 for row in m.rows.iter() {
1935 if row.len() != cols {
1936 return Err(RuntimeError::from(WellDefinedRuntimeError(
1937 RuntimeErrorStruct::new_with_just_msg(
1938 "matrix list is not rectangular (row lengths differ)".to_string(),
1939 ),
1940 )));
1941 }
1942 }
1943 Ok((rows, cols))
1944 }
1945
1946 fn verify_power_set_well_defined(
1947 &mut self,
1948 x: &PowerSet,
1949 verify_state: &VerifyState,
1950 ) -> Result<(), RuntimeError> {
1951 self.verify_obj_well_defined_and_store_cache(&x.set, verify_state)?;
1952 Ok(())
1953 }
1954
1955 fn verify_choose_well_defined(
1956 &mut self,
1957 _x: &Choose,
1958 _verify_state: &VerifyState,
1959 ) -> Result<(), RuntimeError> {
1960 let choose_from = *_x.set.clone();
1961
1962 let choose_from_is_nonempty_set_fact = AtomicFact::IsNonemptySetFact(
1963 IsNonemptySetFact::new(choose_from.clone(), default_line_file()),
1964 );
1965 let choose_from_is_nonempty_set_result =
1966 self.verify_atomic_fact(&choose_from_is_nonempty_set_fact, _verify_state)?;
1967 if choose_from_is_nonempty_set_result.is_unknown() {
1968 return Err(RuntimeError::from(WellDefinedRuntimeError(
1969 RuntimeErrorStruct::new_with_just_msg(format!(
1970 "set {} is not a nonempty set",
1971 choose_from.to_string()
1972 )),
1973 )));
1974 }
1975
1976 let random_param = self.generate_random_unused_name();
1977
1978 let nonempty_set_fact = IsNonemptySetFact::new(
1979 obj_for_bound_param_in_scope(random_param.clone(), ParamObjType::Forall),
1980 default_line_file(),
1981 );
1982
1983 let forall_x_in_choose_from_x_is_nonempty = ForallFact::new(
1984 ParamDefWithType::new(vec![ParamGroupWithParamType::new(
1985 vec![random_param.clone().to_string()],
1986 ParamType::Obj(choose_from),
1987 )]),
1988 vec![],
1989 vec![nonempty_set_fact.into()],
1990 default_line_file(),
1991 )?
1992 .into();
1993
1994 self.verify_fact(&forall_x_in_choose_from_x_is_nonempty, _verify_state)?;
1995
1996 Ok(())
1997 }
1998
1999 fn verify_obj_at_index_well_defined(
2000 &mut self,
2001 x: &ObjAtIndex,
2002 verify_state: &VerifyState,
2003 ) -> Result<(), RuntimeError> {
2004 self.verify_obj_well_defined_and_store_cache(&x.obj, verify_state)?;
2005 self.verify_obj_well_defined_and_store_cache(&x.index, verify_state)?;
2006
2007 let index_calculated_number = self.resolve_obj_to_number(&x.index).ok_or_else(|| {
2008 RuntimeError::from(WellDefinedRuntimeError(
2009 RuntimeErrorStruct::new_with_just_msg(format!(
2010 "index {} is not a number",
2011 x.index.to_string()
2012 )),
2013 ))
2014 })?;
2015 let index_calculated_obj: Obj =
2016 Number::new(index_calculated_number.normalized_value).into();
2017
2018 let index_is_positive_integer_in_z_pos_fact = InFact::new(
2019 index_calculated_obj.clone(),
2020 StandardSet::NPos.into(),
2021 default_line_file(),
2022 )
2023 .into();
2024 let index_is_positive_integer_result =
2025 self.verify_atomic_fact(&index_is_positive_integer_in_z_pos_fact, verify_state)?;
2026 if index_is_positive_integer_result.is_unknown() {
2027 return Err(RuntimeError::from(WellDefinedRuntimeError(
2028 RuntimeErrorStruct::new_with_just_msg(format!(
2029 "index {} is not a positive integer",
2030 index_calculated_obj
2031 )),
2032 )));
2033 }
2034
2035 let target_obj_is_tuple_fact =
2036 IsTupleFact::new((*x.obj).clone(), default_line_file()).into();
2037 let target_obj_is_tuple_result =
2038 self.verify_atomic_fact(&target_obj_is_tuple_fact, verify_state)?;
2039 if target_obj_is_tuple_result.is_unknown() {
2040 return Err(RuntimeError::from(WellDefinedRuntimeError(
2041 RuntimeErrorStruct::new_with_just_msg(format!(
2042 "index target {} is not a tuple",
2043 x.obj
2044 )),
2045 )));
2046 }
2047
2048 let target_tuple_dim_obj: Obj = TupleDim::new((*x.obj).clone()).into();
2049 let index_not_larger_than_tuple_dim_fact = LessEqualFact::new(
2050 index_calculated_obj.clone(),
2051 target_tuple_dim_obj.clone(),
2052 default_line_file(),
2053 )
2054 .into();
2055 let index_not_larger_than_tuple_dim_result =
2056 self.verify_atomic_fact(&index_not_larger_than_tuple_dim_fact, verify_state)?;
2057 if index_not_larger_than_tuple_dim_result.is_unknown() {
2058 return Err(RuntimeError::from(WellDefinedRuntimeError(
2059 RuntimeErrorStruct::new_with_just_msg(format!(
2060 "{} <= {} is unknown",
2061 index_calculated_obj, target_tuple_dim_obj
2062 )),
2063 )));
2064 }
2065
2066 Ok(())
2067 }
2068
2069 fn verify_q_pos_well_defined(&self) -> Result<(), RuntimeError> {
2070 Ok(())
2071 }
2072
2073 fn verify_r_pos_well_defined(&self) -> Result<(), RuntimeError> {
2074 Ok(())
2075 }
2076
2077 fn verify_q_neg_well_defined(&self) -> Result<(), RuntimeError> {
2078 Ok(())
2079 }
2080
2081 fn verify_z_neg_well_defined(&self) -> Result<(), RuntimeError> {
2082 Ok(())
2083 }
2084
2085 fn verify_r_neg_well_defined(&self) -> Result<(), RuntimeError> {
2086 Ok(())
2087 }
2088
2089 fn verify_q_nz_well_defined(&self) -> Result<(), RuntimeError> {
2090 Ok(())
2091 }
2092
2093 fn verify_z_nz_well_defined(&self) -> Result<(), RuntimeError> {
2094 Ok(())
2095 }
2096
2097 fn verify_r_nz_well_defined(&self) -> Result<(), RuntimeError> {
2098 Ok(())
2099 }
2100}
2101
2102impl Runtime {
2103 pub fn verify_param_type_well_defined(
2104 &mut self,
2105 param_type: &ParamType,
2106 verify_state: &VerifyState,
2107 ) -> Result<(), RuntimeError> {
2108 match param_type {
2109 ParamType::Set(_) => Ok(()),
2110 ParamType::NonemptySet(_) => Ok(()),
2111 ParamType::FiniteSet(_) => Ok(()),
2112 ParamType::Obj(obj) => match obj {
2113 Obj::FamilyObj(family) => {
2114 self.verify_param_type_family_well_defined(family, verify_state)
2115 }
2116 _ => self.verify_obj_well_defined_and_store_cache(obj, verify_state),
2117 },
2118 }
2119 }
2120
2121 fn verify_param_type_family_well_defined(
2122 &mut self,
2123 family_param_type: &FamilyObj,
2124 verify_state: &VerifyState,
2125 ) -> Result<(), RuntimeError> {
2126 let family_name = family_param_type.name.to_string();
2127 let def = match self.get_cloned_family_definition_by_name(&family_name) {
2128 Some(d) => d,
2129 None => {
2130 return Err(RuntimeError::from(WellDefinedRuntimeError(
2131 RuntimeErrorStruct::new_with_just_msg(format!(
2132 "family `{}` is not defined",
2133 family_name
2134 )),
2135 )));
2136 }
2137 };
2138
2139 let expected_count = def.params_def_with_type.number_of_params();
2140 if family_param_type.params.len() != expected_count {
2141 return Err(RuntimeError::from(WellDefinedRuntimeError(
2142 RuntimeErrorStruct::new_with_just_msg(format!(
2143 "family `{}` expects {} parameter(s), got {}",
2144 family_name,
2145 expected_count,
2146 family_param_type.params.len()
2147 )),
2148 )));
2149 }
2150
2151 for arg in family_param_type.params.iter() {
2152 self.verify_obj_well_defined_and_store_cache(arg, verify_state)?;
2153 }
2154
2155 let args_param_types = self
2156 .verify_args_satisfy_param_def_flat_types(
2157 &def.params_def_with_type,
2158 &family_param_type.params,
2159 verify_state,
2160 ParamObjType::DefHeader,
2161 )
2162 .map_err(|runtime_error| {
2163 RuntimeError::from(WellDefinedRuntimeError(
2164 RuntimeErrorStruct::new_with_msg_and_cause(
2165 format!(
2166 "failed to verify family `{}` arguments satisfy parameter types",
2167 family_name
2168 ),
2169 runtime_error,
2170 ),
2171 ))
2172 })?;
2173 if args_param_types.is_unknown() {
2174 return Err(RuntimeError::from(WellDefinedRuntimeError(
2175 RuntimeErrorStruct::new_with_just_msg(format!(
2176 "failed to verify family `{}` arguments satisfy parameter types",
2177 family_name
2178 )),
2179 )));
2180 }
2181
2182 let param_to_arg_map = def
2183 .params_def_with_type
2184 .param_defs_and_args_to_param_to_arg_map(family_param_type.params.as_slice());
2185
2186 for dom_fact in def.dom_facts.iter() {
2187 let instantiated_dom_fact = self
2188 .inst_or_and_chain_atomic_fact(
2189 dom_fact,
2190 ¶m_to_arg_map,
2191 ParamObjType::DefHeader,
2192 None,
2193 )
2194 .map_err(|e| {
2195 RuntimeError::from(WellDefinedRuntimeError(
2196 RuntimeErrorStruct::new_with_msg_and_cause(
2197 format!(
2198 "failed to instantiate family `{}` domain fact: {}",
2199 family_name, e
2200 ),
2201 e,
2202 ),
2203 ))
2204 })?;
2205 let verify_result = self
2206 .verify_or_and_chain_atomic_fact(&instantiated_dom_fact, verify_state)
2207 .map_err(|verify_error| {
2208 RuntimeError::from(WellDefinedRuntimeError(
2209 RuntimeErrorStruct::new_with_msg_and_cause(
2210 format!(
2211 "failed to verify family `{}` domain fact:\n{}",
2212 family_name, instantiated_dom_fact
2213 ),
2214 verify_error,
2215 ),
2216 ))
2217 })?;
2218 if verify_result.is_unknown() {
2219 return Err(RuntimeError::from(WellDefinedRuntimeError(
2220 RuntimeErrorStruct::new_with_just_msg(format!(
2221 "failed to verify family `{}` domain fact:\n{}",
2222 family_name, instantiated_dom_fact
2223 )),
2224 )));
2225 }
2226 }
2227
2228 let instantiated_equal_to = self
2229 .inst_obj(&def.equal_to, ¶m_to_arg_map, ParamObjType::DefHeader)
2230 .map_err(|e| {
2231 RuntimeError::from(WellDefinedRuntimeError(
2232 RuntimeErrorStruct::new_with_msg_and_cause(
2233 format!(
2234 "failed to instantiate family `{}` member set: {}",
2235 family_name, e
2236 ),
2237 e,
2238 ),
2239 ))
2240 })?;
2241 self.verify_obj_well_defined_and_store_cache(&instantiated_equal_to, verify_state)?;
2242
2243 Ok(())
2244 }
2245}