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