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