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