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