1use super::known_fn::KnownFnInfo;
2use crate::prelude::*;
3use std::collections::HashMap;
4use std::fmt;
5use std::rc::Rc;
6
7pub struct Environment {
8 pub defined_identifiers: HashMap<IdentifierName, ParamObjType>,
9 pub defined_def_props: HashMap<PropName, DefPropStmt>,
10 pub defined_abstract_props: HashMap<AbstractPropName, DefAbstractPropStmt>,
11 pub defined_families: HashMap<FamilyName, DefFamilyStmt>,
12 pub defined_algorithms: HashMap<AlgoName, DefAlgoStmt>,
13 pub defined_structs: HashMap<StructName, DefStructStmt>,
14
15 pub known_equality: HashMap<ObjString, (HashMap<ObjString, AtomicFact>, Rc<Vec<Obj>>)>,
16
17 pub known_atomic_facts_with_0_or_more_than_2_args:
18 HashMap<(AtomicFactKey, bool), Vec<AtomicFact>>,
19 pub known_atomic_facts_with_1_arg:
20 HashMap<(AtomicFactKey, bool), HashMap<ObjString, AtomicFact>>,
21 pub known_atomic_facts_with_2_args:
22 HashMap<(AtomicFactKey, bool), HashMap<(ObjString, ObjString), AtomicFact>>,
23
24 pub known_exist_facts: HashMap<ExistFactKey, Vec<ExistFactEnum>>,
25 pub known_or_facts: HashMap<OrFactKey, Vec<OrFact>>,
26
27 pub known_atomic_facts_in_forall_facts:
28 HashMap<(AtomicFactKey, bool), Vec<(AtomicFact, Rc<KnownForallFactParamsAndDom>)>>,
29 pub known_exist_facts_in_forall_facts:
30 HashMap<ExistFactKey, Vec<(ExistFactEnum, Rc<KnownForallFactParamsAndDom>)>>,
31 pub known_or_facts_in_forall_facts:
32 HashMap<OrFactKey, Vec<(OrFact, Rc<KnownForallFactParamsAndDom>)>>,
33
34 pub known_objs_equal_to_tuple: HashMap<ObjString, (Option<Tuple>, Option<Cart>, LineFile)>,
35 pub known_objs_equal_to_cart: HashMap<ObjString, (Cart, LineFile)>,
36 pub known_objs_equal_to_finite_seq_list:
37 HashMap<ObjString, (FiniteSeqListObj, Option<FiniteSeqSet>, LineFile)>,
38 pub known_objs_equal_to_matrix_list:
39 HashMap<ObjString, (MatrixListObj, Option<MatrixSet>, LineFile)>,
40 pub known_objs_equal_to_normalized_decimal_number: HashMap<ObjString, Number>,
41
42 pub known_objs_in_fn_sets: HashMap<ObjString, KnownFnInfo>,
43
44 pub known_transitive_props: HashMap<String, ()>,
45 pub known_commutative_props: HashMap<String, CommutativePropValue>,
46
47 pub cache_well_defined_obj: HashMap<ObjString, ()>,
48 pub cache_known_fact: HashMap<FactString, LineFile>,
49}
50
51impl Environment {
52 pub fn new(
53 objs: HashMap<IdentifierName, ParamObjType>,
54 def_props: HashMap<PropName, DefPropStmt>,
55 families: HashMap<FamilyName, DefFamilyStmt>,
56 abstract_props: HashMap<AbstractPropName, DefAbstractPropStmt>,
57 algorithms: HashMap<AlgoName, DefAlgoStmt>,
58 structs: HashMap<StructName, DefStructStmt>,
59 known_equality: HashMap<ObjString, (HashMap<ObjString, AtomicFact>, Rc<Vec<Obj>>)>,
60 known_fn_in_fn_set: HashMap<ObjString, KnownFnInfo>,
61 known_atomic_facts_with_0_or_more_than_2_args: HashMap<
62 (AtomicFactKey, bool),
63 Vec<AtomicFact>,
64 >,
65 known_atomic_facts_with_1_arg: HashMap<
66 (AtomicFactKey, bool),
67 HashMap<ObjString, AtomicFact>,
68 >,
69 known_atomic_facts_with_2_args: HashMap<
70 (AtomicFactKey, bool),
71 HashMap<(ObjString, ObjString), AtomicFact>,
72 >,
73 known_exist_facts: HashMap<ExistFactKey, Vec<ExistFactEnum>>,
74 known_atomic_facts_in_forall_facts: HashMap<
75 (AtomicFactKey, bool),
76 Vec<(AtomicFact, Rc<KnownForallFactParamsAndDom>)>,
77 >,
78 known_exist_facts_in_forall_facts: HashMap<
79 ExistFactKey,
80 Vec<(ExistFactEnum, Rc<KnownForallFactParamsAndDom>)>,
81 >,
82 known_or_facts: HashMap<OrFactKey, Vec<OrFact>>,
83 known_or_facts_in_forall_facts: HashMap<
84 OrFactKey,
85 Vec<(OrFact, Rc<KnownForallFactParamsAndDom>)>,
86 >,
87 known_tuple_objs: HashMap<ObjString, (Option<Tuple>, Option<Cart>, LineFile)>,
88 known_cart_objs: HashMap<ObjString, (Cart, LineFile)>,
89 known_finite_seq_list_objs: HashMap<
90 ObjString,
91 (FiniteSeqListObj, Option<FiniteSeqSet>, LineFile),
92 >,
93 known_matrix_list_objs: HashMap<ObjString, (MatrixListObj, Option<MatrixSet>, LineFile)>,
94 known_calculated_value_of_obj: HashMap<ObjString, Number>,
95 cache_known_valid_obj: HashMap<ObjString, ()>,
96 cache_known_fact: HashMap<FactString, LineFile>,
97 ) -> Self {
98 Environment {
99 defined_identifiers: objs,
100 defined_def_props: def_props,
101 defined_families: families,
102 defined_abstract_props: abstract_props,
103 defined_algorithms: algorithms,
104 defined_structs: structs,
105 known_equality,
106 known_objs_in_fn_sets: known_fn_in_fn_set,
107 known_atomic_facts_with_0_or_more_than_2_args,
108 known_atomic_facts_with_1_arg: known_atomic_facts_with_1_arg,
109 known_atomic_facts_with_2_args: known_atomic_facts_with_2_args,
110 known_exist_facts,
111 known_atomic_facts_in_forall_facts,
112 known_exist_facts_in_forall_facts,
113 known_or_facts,
114 known_or_facts_in_forall_facts,
115 known_objs_equal_to_tuple: known_tuple_objs,
116 known_objs_equal_to_cart: known_cart_objs,
117 known_objs_equal_to_finite_seq_list: known_finite_seq_list_objs,
118 known_objs_equal_to_matrix_list: known_matrix_list_objs,
119 known_objs_equal_to_normalized_decimal_number: known_calculated_value_of_obj,
120 known_transitive_props: HashMap::new(),
121 known_commutative_props: HashMap::new(),
122 cache_well_defined_obj: cache_known_valid_obj,
123 cache_known_fact,
124 }
125 }
126}
127
128impl fmt::Display for Environment {
129 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
130 write!(f, "Environment {{\n")?;
131 write!(f, " objs: {:?}\n", self.defined_identifiers.len())?;
132 write!(f, " def_props: {:?}\n", self.defined_def_props.len())?;
133 write!(f, " families: {:?}\n", self.defined_families.len())?;
134 write!(f, " algorithms: {:?}\n", self.defined_algorithms.len())?;
135 write!(f, " structs: {:?}\n", self.defined_structs.len())?;
136 write!(f, " known_equality: {:?}\n", self.known_equality.len())?;
137 write!(
138 f,
139 " known_fn_in_fn_set: {:?}\n",
140 self.known_objs_in_fn_sets.len()
141 )?;
142 write!(
143 f,
144 " known_transitive_props: {:?}\n",
145 self.known_transitive_props.len()
146 )?;
147 write!(
148 f,
149 " known_commutative_props: {} predicates, {} permutations\n",
150 self.known_commutative_props.len(),
151 self.known_commutative_props
152 .values()
153 .map(|v| v.len())
154 .sum::<usize>()
155 )?;
156 write!(
157 f,
158 " known_atomic_facts_with_0_or_more_than_two_params: {:?}\n",
159 self.known_atomic_facts_with_0_or_more_than_2_args.len()
160 )?;
161 write!(
162 f,
163 " known_atomic_facts_with_1_arg: {:?}\n",
164 self.known_atomic_facts_with_1_arg.len()
165 )?;
166 write!(
167 f,
168 " known_atomic_facts_with_2_args: {:?}\n",
169 self.known_atomic_facts_with_2_args.len()
170 )?;
171 write!(
172 f,
173 " known_exist_facts_with_more_than_two_params: {:?}\n",
174 self.known_exist_facts.len()
175 )?;
176 write!(
177 f,
178 " known_or_facts_with_more_than_two_params: {:?}\n",
179 self.known_or_facts.len()
180 )?;
181 write!(
182 f,
183 " known_atomic_facts_in_forall_facts: {:?}\n",
184 self.known_atomic_facts_in_forall_facts.len()
185 )?;
186 write!(
187 f,
188 " known_exist_facts_in_forall_facts: {:?}\n",
189 self.known_exist_facts_in_forall_facts.len()
190 )?;
191 write!(
192 f,
193 " known_or_facts_in_forall_facts: {:?}\n",
194 self.known_or_facts_in_forall_facts.len()
195 )?;
196 write!(
197 f,
198 " cache_known_valid_obj: {:?}\n",
199 self.cache_well_defined_obj.len()
200 )?;
201 write!(
202 f,
203 " cache_known_fact: {:?}\n",
204 self.cache_known_fact.len()
205 )?;
206 write!(f, "}}")
207 }
208}
209
210impl Environment {
211 pub fn store_atomic_fact_by_ref(
212 &mut self,
213 atomic_fact: &AtomicFact,
214 ) -> Result<(), RuntimeError> {
215 self.store_atomic_fact(atomic_fact.clone())
216 }
217
218 pub fn store_atomic_fact(&mut self, atomic_fact: AtomicFact) -> Result<(), RuntimeError> {
219 match atomic_fact {
220 AtomicFact::EqualFact(equal_fact) => self.store_equality(&equal_fact),
221 _ => {
222 let key: AtomicFactKey = atomic_fact.key();
223 let is_true = atomic_fact.is_true();
224 if atomic_fact.args().len() == 1 {
225 let arg_key: ObjString = atomic_fact.args()[0].to_string();
226 if let Some(map) = self
227 .known_atomic_facts_with_1_arg
228 .get_mut(&(key.clone(), is_true))
229 {
230 map.insert(arg_key, atomic_fact);
231 } else {
232 self.known_atomic_facts_with_1_arg
233 .insert((key, is_true), HashMap::from([(arg_key, atomic_fact)]));
234 }
235 } else if atomic_fact.args().len() == 2 {
236 let arg_key1: ObjString = atomic_fact.args()[0].to_string();
237 let arg_key2: ObjString = atomic_fact.args()[1].to_string();
238 if let Some(map) = self
239 .known_atomic_facts_with_2_args
240 .get_mut(&(key.clone(), is_true))
241 {
242 map.insert((arg_key1, arg_key2), atomic_fact);
243 } else {
244 self.known_atomic_facts_with_2_args.insert(
245 (key, is_true),
246 HashMap::from([((arg_key1, arg_key2), atomic_fact)]),
247 );
248 }
249 } else {
250 if let Some(vec_ref) = self
251 .known_atomic_facts_with_0_or_more_than_2_args
252 .get_mut(&(key.clone(), is_true))
253 {
254 vec_ref.push(atomic_fact);
255 } else {
256 self.known_atomic_facts_with_0_or_more_than_2_args
257 .insert((key, is_true), vec![atomic_fact]);
258 }
259 }
260 Ok(())
261 }
262 }
263 }
264
265 fn store_exist_fact(&mut self, exist_fact: ExistFactEnum) -> Result<(), RuntimeError> {
266 let key: ExistFactKey = exist_fact.key();
267 if let Some(vec_ref) = self.known_exist_facts.get_mut(&key) {
268 vec_ref.push(exist_fact);
269 } else {
270 self.known_exist_facts.insert(key, vec![exist_fact]);
271 }
272 Ok(())
273 }
274
275 fn store_or_fact(&mut self, or_fact: OrFact) -> Result<(), RuntimeError> {
276 let key: OrFactKey = or_fact.key();
277 if let Some(vec_ref) = self.known_or_facts.get_mut(&key) {
278 vec_ref.push(or_fact);
279 } else {
280 self.known_or_facts.insert(key, vec![or_fact]);
281 }
282 Ok(())
283 }
284
285 fn store_atomic_fact_in_forall_fact(
286 &mut self,
287 atomic_fact: AtomicFact,
288 forall_params_and_dom: Rc<KnownForallFactParamsAndDom>,
289 ) -> Result<(), RuntimeError> {
290 let key: AtomicFactKey = atomic_fact.key();
291 let is_true = atomic_fact.is_true();
292 if let Some(vec_ref) = self
293 .known_atomic_facts_in_forall_facts
294 .get_mut(&(key.clone(), is_true))
295 {
296 vec_ref.push((atomic_fact, forall_params_and_dom));
297 } else {
298 self.known_atomic_facts_in_forall_facts
299 .insert((key, is_true), vec![(atomic_fact, forall_params_and_dom)]);
300 }
301 Ok(())
302 }
303
304 fn store_or_fact_in_forall_fact(
305 &mut self,
306 or_fact: &OrFact,
307 forall_params_and_dom: Rc<KnownForallFactParamsAndDom>,
308 ) -> Result<(), RuntimeError> {
309 let key: OrFactKey = or_fact.key();
310 if let Some(vec_ref) = self.known_or_facts_in_forall_facts.get_mut(&key) {
311 vec_ref.push((or_fact.clone(), forall_params_and_dom));
312 } else {
313 self.known_or_facts_in_forall_facts
314 .insert(key, vec![(or_fact.clone(), forall_params_and_dom)]);
315 }
316 Ok(())
317 }
318
319 fn store_a_fact_in_forall_fact(
320 &mut self,
321 fact: &ExistOrAndChainAtomicFact,
322 forall_params_and_dom: Rc<KnownForallFactParamsAndDom>,
323 ) -> Result<(), RuntimeError> {
324 match fact {
325 ExistOrAndChainAtomicFact::AtomicFact(spec_fact) => {
326 self.store_atomic_fact_in_forall_fact(spec_fact.clone(), forall_params_and_dom)
327 }
328 ExistOrAndChainAtomicFact::OrFact(or_fact) => {
329 self.store_or_fact_in_forall_fact(&or_fact, forall_params_and_dom)
330 }
331 ExistOrAndChainAtomicFact::AndFact(and_fact) => {
332 self.store_and_fact_in_forall_fact(&and_fact, forall_params_and_dom)
333 }
334 ExistOrAndChainAtomicFact::ChainFact(chain_fact) => {
335 self.store_chain_fact_in_forall_fact(&chain_fact, forall_params_and_dom)
336 }
337 ExistOrAndChainAtomicFact::ExistFact(exist_fact) => {
338 self.store_exist_fact_in_forall_fact(&exist_fact, forall_params_and_dom)
339 }
340 }
341 }
342
343 fn store_chain_fact_in_forall_fact(
344 &mut self,
345 chain_fact: &ChainFact,
346 forall_params_and_dom: Rc<KnownForallFactParamsAndDom>,
347 ) -> Result<(), RuntimeError> {
348 for fact in chain_fact
349 .facts()
350 .map_err(RuntimeError::wrap_new_fact_as_store_conflict)?
351 .into_iter()
352 {
353 self.store_atomic_fact_in_forall_fact(fact, forall_params_and_dom.clone())?;
354 }
355 Ok(())
356 }
357
358 fn store_exist_fact_in_forall_fact(
359 &mut self,
360 exist_fact: &ExistFactEnum,
361 forall_params_and_dom: Rc<KnownForallFactParamsAndDom>,
362 ) -> Result<(), RuntimeError> {
363 let pair = || (exist_fact.clone(), forall_params_and_dom.clone());
364 let key: ExistFactKey = exist_fact.key();
365 if let Some(vec_ref) = self.known_exist_facts_in_forall_facts.get_mut(&key) {
366 vec_ref.push(pair());
367 } else {
368 self.known_exist_facts_in_forall_facts
369 .insert(key, vec![pair()]);
370 }
371 let alpha_key = exist_fact.alpha_normalized_key();
372 if alpha_key != exist_fact.key() {
373 if let Some(vec_ref) = self.known_exist_facts_in_forall_facts.get_mut(&alpha_key) {
374 vec_ref.push(pair());
375 } else {
376 self.known_exist_facts_in_forall_facts
377 .insert(alpha_key, vec![pair()]);
378 }
379 }
380 Ok(())
381 }
382
383 fn store_and_fact_in_forall_fact(
384 &mut self,
385 and_fact: &AndFact,
386 forall_params_and_dom: Rc<KnownForallFactParamsAndDom>,
387 ) -> Result<(), RuntimeError> {
388 for fact in and_fact.facts.iter() {
389 self.store_atomic_fact_in_forall_fact(fact.clone(), forall_params_and_dom.clone())?;
390 }
391 Ok(())
392 }
393
394 fn store_forall_fact(&mut self, forall_fact: Rc<ForallFact>) -> Result<(), RuntimeError> {
395 let forall_params_and_dom = Rc::new(KnownForallFactParamsAndDom::new(
396 forall_fact.params_def_with_type.clone(),
397 forall_fact.dom_facts.clone(),
398 forall_fact.line_file.clone(),
399 ));
400
401 for fact in forall_fact.then_facts.iter() {
402 self.store_a_fact_in_forall_fact(fact, forall_params_and_dom.clone())?;
403 }
404 Ok(())
405 }
406
407 fn store_and_fact(&mut self, and_fact: AndFact) -> Result<(), RuntimeError> {
408 for atomic_fact in and_fact.facts {
409 self.store_atomic_fact(atomic_fact)?;
410 }
411 Ok(())
412 }
413
414 fn store_forall_fact_with_iff(
415 &mut self,
416 forall_fact_with_iff: ForallFactWithIff,
417 ) -> Result<(), RuntimeError> {
418 let (forall_then_implies_iff, forall_iff_implies_then) =
419 forall_fact_with_iff.to_two_forall_facts()?;
420 self.store_forall_fact(Rc::new(forall_then_implies_iff))?;
421 self.store_forall_fact(Rc::new(forall_iff_implies_then))?;
422 Ok(())
423 }
424
425 pub fn store_fact(&mut self, fact: Fact) -> Result<(), RuntimeError> {
426 match fact {
427 Fact::AtomicFact(atomic_fact) => self.store_atomic_fact(atomic_fact),
428 Fact::ExistFact(exist_fact) => self.store_exist_fact(exist_fact),
429 Fact::OrFact(or_fact) => self.store_or_fact(or_fact),
430 Fact::AndFact(and_fact) => self.store_and_fact(and_fact),
431 Fact::ChainFact(chain_fact) => self.store_chain_fact(chain_fact),
432 Fact::ForallFact(forall_fact) => self.store_forall_fact(Rc::new(forall_fact)),
433 Fact::ForallFactWithIff(forall_fact_with_iff) => {
434 self.store_forall_fact_with_iff(forall_fact_with_iff)
435 }
436 Fact::NotForall(_) => Ok(()),
437 }
438 }
439
440 pub fn store_exist_fact_by_ref(
441 &mut self,
442 exist_fact: &ExistFactEnum,
443 ) -> Result<(), RuntimeError> {
444 self.store_exist_fact(exist_fact.clone())
445 }
446
447 pub fn store_exist_or_and_chain_atomic_fact(
448 &mut self,
449 fact: ExistOrAndChainAtomicFact,
450 ) -> Result<(), RuntimeError> {
451 match fact {
452 ExistOrAndChainAtomicFact::AtomicFact(atomic_fact) => {
453 self.store_atomic_fact(atomic_fact)
454 }
455 ExistOrAndChainAtomicFact::AndFact(and_fact) => self.store_and_fact(and_fact),
456 ExistOrAndChainAtomicFact::ChainFact(chain_fact) => self.store_chain_fact(chain_fact),
457 ExistOrAndChainAtomicFact::OrFact(or_fact) => self.store_or_fact(or_fact),
458 ExistOrAndChainAtomicFact::ExistFact(exist_fact) => self.store_exist_fact(exist_fact),
459 }
460 }
461
462 pub fn store_and_chain_atomic_fact(
463 &mut self,
464 and_chain_atomic_fact: AndChainAtomicFact,
465 ) -> Result<(), RuntimeError> {
466 match and_chain_atomic_fact {
467 AndChainAtomicFact::AtomicFact(atomic_fact) => self.store_atomic_fact(atomic_fact),
468 AndChainAtomicFact::AndFact(and_fact) => self.store_and_fact(and_fact),
469 AndChainAtomicFact::ChainFact(chain_fact) => self.store_chain_fact(chain_fact),
470 }
471 }
472
473 pub fn store_or_and_chain_atomic_fact(
474 &mut self,
475 fact: OrAndChainAtomicFact,
476 ) -> Result<(), RuntimeError> {
477 match fact {
478 OrAndChainAtomicFact::AtomicFact(atomic_fact) => self.store_atomic_fact(atomic_fact),
479 OrAndChainAtomicFact::AndFact(and_fact) => self.store_and_fact(and_fact),
480 OrAndChainAtomicFact::ChainFact(chain_fact) => self.store_chain_fact(chain_fact),
481 OrAndChainAtomicFact::OrFact(or_fact) => self.store_or_fact(or_fact),
482 }
483 }
484
485 fn store_chain_fact(&mut self, chain_fact: ChainFact) -> Result<(), RuntimeError> {
486 let atomic_facts = chain_fact
487 .facts_with_order_transitive_closure()
488 .map_err(RuntimeError::wrap_new_fact_as_store_conflict)?;
489 for atomic_fact in atomic_facts {
490 self.store_atomic_fact(atomic_fact)?;
491 }
492 Ok(())
493 }
494
495 pub fn store_chain_fact_by_ref(&mut self, chain_fact: &ChainFact) -> Result<(), RuntimeError> {
496 self.store_chain_fact(chain_fact.clone())
497 }
498
499 pub fn store_equality(&mut self, equality: &EqualFact) -> Result<(), RuntimeError> {
500 let left_as_string: ObjString = equality.left.to_string();
501 let right_as_string: ObjString = equality.right.to_string();
502 if left_as_string == right_as_string {
503 return Ok(());
504 }
505
506 let left_rc = self
507 .known_equality
508 .get(&left_as_string)
509 .map(|(_, rc)| Rc::clone(rc));
510 let right_rc = self
511 .known_equality
512 .get(&right_as_string)
513 .map(|(_, rc)| Rc::clone(rc));
514
515 let equal_atomic_fact = AtomicFact::EqualFact(equality.clone());
516
517 match (left_rc, right_rc) {
518 (Some(ref left_class_rc), Some(ref right_class_rc)) => {
519 if Rc::ptr_eq(left_class_rc, right_class_rc) {
520 return Ok(());
521 }
522 let merged_vec: Vec<Obj> = {
523 let left_vec: &Vec<Obj> = left_class_rc.as_ref();
524 let right_vec: &Vec<Obj> = right_class_rc.as_ref();
525 let mut merged = Vec::with_capacity(left_vec.len() + right_vec.len());
526 for obj in left_vec.iter().chain(right_vec.iter()) {
527 merged.push(obj.clone());
528 }
529 merged.sort_by(|a_obj, b_obj| a_obj.to_string().cmp(&b_obj.to_string()));
530 merged.dedup_by(|a_obj, b_obj| a_obj.to_string() == b_obj.to_string());
531 merged
532 };
533 let new_equiv_rc = Rc::new(merged_vec);
534
535 let keys_in_either_class: Vec<ObjString> = self
536 .known_equality
537 .iter()
538 .filter(|(_, (_, class_rc))| {
539 Rc::ptr_eq(class_rc, left_class_rc) || Rc::ptr_eq(class_rc, right_class_rc)
540 })
541 .map(|(k, _)| k.clone())
542 .collect();
543
544 for key_in_class in keys_in_either_class {
545 let removed_entry = match self.known_equality.remove(&key_in_class) {
546 Some(entry) => entry,
547 None => continue,
548 };
549 let (mut direct_equality_proof_map, _) = removed_entry;
550 if key_in_class == left_as_string {
551 direct_equality_proof_map
552 .insert(right_as_string.clone(), equal_atomic_fact.clone());
553 }
554 if key_in_class == right_as_string {
555 direct_equality_proof_map
556 .insert(left_as_string.clone(), equal_atomic_fact.clone());
557 }
558 self.known_equality.insert(
559 key_in_class,
560 (direct_equality_proof_map, Rc::clone(&new_equiv_rc)),
561 );
562 }
563 }
564 (Some(existing_class_rc), None) => {
565 let mut new_vec = (*existing_class_rc).clone();
566 new_vec.push(equality.right.clone());
567 let new_equiv_rc = Rc::new(new_vec);
568
569 let keys_in_existing_class: Vec<ObjString> = self
570 .known_equality
571 .iter()
572 .filter(|(_, (_, class_rc))| Rc::ptr_eq(class_rc, &existing_class_rc))
573 .map(|(k, _)| k.clone())
574 .collect();
575
576 for key_in_class in keys_in_existing_class {
577 let removed_entry = match self.known_equality.remove(&key_in_class) {
578 Some(entry) => entry,
579 None => continue,
580 };
581 let (mut direct_equality_proof_map, _) = removed_entry;
582 if key_in_class == left_as_string {
583 direct_equality_proof_map
584 .insert(right_as_string.clone(), equal_atomic_fact.clone());
585 }
586 self.known_equality.insert(
587 key_in_class,
588 (direct_equality_proof_map, Rc::clone(&new_equiv_rc)),
589 );
590 }
591
592 let mut proof_for_new_right: HashMap<ObjString, AtomicFact> = HashMap::new();
593 proof_for_new_right.insert(left_as_string.clone(), equal_atomic_fact.clone());
594 self.known_equality
595 .insert(right_as_string, (proof_for_new_right, new_equiv_rc));
596 }
597 (None, Some(existing_class_rc)) => {
598 let mut new_vec = (*existing_class_rc).clone();
599 new_vec.push(equality.left.clone());
600 let new_equiv_rc = Rc::new(new_vec);
601
602 let keys_in_existing_class: Vec<ObjString> = self
603 .known_equality
604 .iter()
605 .filter(|(_, (_, class_rc))| Rc::ptr_eq(class_rc, &existing_class_rc))
606 .map(|(k, _)| k.clone())
607 .collect();
608
609 for key_in_class in keys_in_existing_class {
610 let removed_entry = match self.known_equality.remove(&key_in_class) {
611 Some(entry) => entry,
612 None => continue,
613 };
614 let (mut direct_equality_proof_map, _) = removed_entry;
615 if key_in_class == right_as_string {
616 direct_equality_proof_map
617 .insert(left_as_string.clone(), equal_atomic_fact.clone());
618 }
619 self.known_equality.insert(
620 key_in_class,
621 (direct_equality_proof_map, Rc::clone(&new_equiv_rc)),
622 );
623 }
624
625 let mut proof_for_new_left: HashMap<ObjString, AtomicFact> = HashMap::new();
626 proof_for_new_left.insert(right_as_string.clone(), equal_atomic_fact.clone());
627 self.known_equality
628 .insert(left_as_string, (proof_for_new_left, new_equiv_rc));
629 }
630 (None, None) => {
631 let equiv_members = vec![equality.left.clone(), equality.right.clone()];
632 let new_equiv_rc = Rc::new(equiv_members);
633
634 let mut left_direct_proof_map: HashMap<ObjString, AtomicFact> = HashMap::new();
635 left_direct_proof_map.insert(right_as_string.clone(), equal_atomic_fact.clone());
636
637 let mut right_direct_proof_map: HashMap<ObjString, AtomicFact> = HashMap::new();
638 right_direct_proof_map.insert(left_as_string.clone(), equal_atomic_fact);
639
640 self.known_equality.insert(
641 left_as_string.clone(),
642 (left_direct_proof_map, Rc::clone(&new_equiv_rc)),
643 );
644 self.known_equality
645 .insert(right_as_string, (right_direct_proof_map, new_equiv_rc));
646 }
647 }
648
649 if let Some(derived) =
650 super::equality_linear_derive::maybe_derived_linear_equal_fact(equality)
651 {
652 if derived.left.to_string() != derived.right.to_string() {
653 self.store_equality(&derived)?;
654 }
655 }
656 Ok(())
657 }
658}
659
660impl Environment {
661 pub fn new_empty_env() -> Self {
662 Environment::new(
663 HashMap::new(),
664 HashMap::new(),
665 HashMap::new(),
666 HashMap::new(),
667 HashMap::new(),
668 HashMap::new(),
669 HashMap::new(),
670 HashMap::new(),
671 HashMap::new(),
672 HashMap::new(),
673 HashMap::new(),
674 HashMap::new(),
675 HashMap::new(),
676 HashMap::new(),
677 HashMap::new(),
678 HashMap::new(),
679 HashMap::new(),
680 HashMap::new(),
681 HashMap::new(),
682 HashMap::new(),
683 HashMap::new(),
684 HashMap::new(),
685 HashMap::new(),
686 )
687 }
688}
689
690impl Environment {
691 pub fn store_transitive_prop_name(&mut self, prop_name: String) {
692 self.known_transitive_props.insert(prop_name, ());
693 }
694
695 pub fn store_commutative_prop_permutation(
696 &mut self,
697 prop_name: String,
698 gather: Vec<usize>,
699 line_file: LineFile,
700 ) -> Result<(), RuntimeError> {
701 let n = gather.len();
702 if n < 2 {
703 return Err(
704 StoreFactRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(
705 "store_commutative_prop_permutation: arity must be at least 2".to_string(),
706 line_file,
707 ))
708 .into(),
709 );
710 }
711 if !commutative_gather_is_valid_permutation(&gather, n) {
712 return Err(
713 StoreFactRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(
714 "store_commutative_prop_permutation: gather is not a valid permutation"
715 .to_string(),
716 line_file,
717 ))
718 .into(),
719 );
720 }
721 if commutative_gather_is_identity(&gather) {
722 return Err(
723 StoreFactRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(
724 "store_commutative_prop_permutation: identity permutation is not allowed"
725 .to_string(),
726 line_file,
727 ))
728 .into(),
729 );
730 }
731 if let Some(existing) = self.known_commutative_props.get(&prop_name) {
732 if let Some(first) = existing.first() {
733 if first.len() != n {
734 return Err(StoreFactRuntimeError(
735 RuntimeErrorStruct::new_with_msg_and_line_file(
736 format!(
737 "store_commutative_prop_permutation: `{}` already has arity {}, got {}",
738 prop_name,
739 first.len(),
740 n
741 ),
742 line_file,
743 ),
744 )
745 .into());
746 }
747 }
748 }
749 let entry = self
750 .known_commutative_props
751 .entry(prop_name)
752 .or_insert_with(Vec::new);
753 if entry.iter().any(|g| g == &gather) {
754 return Ok(());
755 }
756 entry.push(gather);
757 Ok(())
758 }
759}
760
761impl Environment {
762 pub fn store_fact_to_cache_known_fact(
763 &mut self,
764 fact_key: FactString,
765 fact_line_file: LineFile,
766 ) -> Result<(), RuntimeError> {
767 self.cache_known_fact.insert(fact_key, fact_line_file);
768 Ok(())
769 }
770}
771
772pub struct KnownForallFactParamsAndDom {
773 pub params_def: ParamDefWithType,
774 pub dom: Vec<Fact>,
775 pub line_file: LineFile,
776}
777
778impl KnownForallFactParamsAndDom {
779 pub fn new(params: ParamDefWithType, dom: Vec<Fact>, line_file: LineFile) -> Self {
780 KnownForallFactParamsAndDom {
781 params_def: params,
782 dom,
783 line_file,
784 }
785 }
786}
787
788pub type CommutativePropValue = Vec<Vec<usize>>;
789
790fn commutative_gather_is_identity(gather: &[usize]) -> bool {
791 gather.iter().enumerate().all(|(i, &g)| g == i)
792}
793
794fn commutative_gather_is_valid_permutation(gather: &[usize], n: usize) -> bool {
795 if gather.len() != n {
796 return false;
797 }
798 let mut seen = vec![false; n];
799 for &i in gather {
800 if i >= n {
801 return false;
802 }
803 if seen[i] {
804 return false;
805 }
806 seen[i] = true;
807 }
808 true
809}