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_atomic_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 }
414 }
415
416 pub fn store_exist_fact_by_ref(
417 &mut self,
418 exist_fact: &ExistFactEnum,
419 ) -> Result<(), RuntimeError> {
420 self.store_exist_fact(exist_fact.clone())
421 }
422
423 pub fn store_exist_or_and_chain_atomic_fact(
424 &mut self,
425 fact: ExistOrAndChainAtomicFact,
426 ) -> Result<(), RuntimeError> {
427 match fact {
428 ExistOrAndChainAtomicFact::AtomicFact(atomic_fact) => {
429 self.store_atomic_fact(atomic_fact)
430 }
431 ExistOrAndChainAtomicFact::AndFact(and_fact) => self.store_and_fact(and_fact),
432 ExistOrAndChainAtomicFact::ChainFact(chain_fact) => self.store_chain_fact(chain_fact),
433 ExistOrAndChainAtomicFact::OrFact(or_fact) => self.store_or_fact(or_fact),
434 ExistOrAndChainAtomicFact::ExistFact(exist_fact) => self.store_exist_fact(exist_fact),
435 }
436 }
437
438 pub fn store_and_chain_atomic_fact(
439 &mut self,
440 and_chain_atomic_fact: AndChainAtomicFact,
441 ) -> Result<(), RuntimeError> {
442 match and_chain_atomic_fact {
443 AndChainAtomicFact::AtomicFact(atomic_fact) => self.store_atomic_fact(atomic_fact),
444 AndChainAtomicFact::AndFact(and_fact) => self.store_and_fact(and_fact),
445 AndChainAtomicFact::ChainFact(chain_fact) => self.store_chain_fact(chain_fact),
446 }
447 }
448
449 pub fn store_or_and_chain_atomic_fact(
450 &mut self,
451 fact: OrAndChainAtomicFact,
452 ) -> Result<(), RuntimeError> {
453 match fact {
454 OrAndChainAtomicFact::AtomicFact(atomic_fact) => self.store_atomic_fact(atomic_fact),
455 OrAndChainAtomicFact::AndFact(and_fact) => self.store_and_fact(and_fact),
456 OrAndChainAtomicFact::ChainFact(chain_fact) => self.store_chain_fact(chain_fact),
457 OrAndChainAtomicFact::OrFact(or_fact) => self.store_or_fact(or_fact),
458 }
459 }
460
461 fn store_chain_fact(&mut self, chain_fact: ChainFact) -> Result<(), RuntimeError> {
462 let atomic_facts = chain_fact
463 .facts_with_order_transitive_closure()
464 .map_err(RuntimeError::wrap_new_atomic_fact_as_store_conflict)?;
465 for atomic_fact in atomic_facts {
466 self.store_atomic_fact(atomic_fact)?;
467 }
468 Ok(())
469 }
470
471 pub fn store_chain_fact_by_ref(&mut self, chain_fact: &ChainFact) -> Result<(), RuntimeError> {
472 self.store_chain_fact(chain_fact.clone())
473 }
474
475 pub fn store_equality(&mut self, equality: &EqualFact) -> Result<(), RuntimeError> {
476 let left_as_string: ObjString = equality.left.to_string();
477 let right_as_string: ObjString = equality.right.to_string();
478 if left_as_string == right_as_string {
479 return Ok(());
480 }
481
482 let left_rc = self
483 .known_equality
484 .get(&left_as_string)
485 .map(|(_, rc)| Rc::clone(rc));
486 let right_rc = self
487 .known_equality
488 .get(&right_as_string)
489 .map(|(_, rc)| Rc::clone(rc));
490
491 let equal_atomic_fact = AtomicFact::EqualFact(equality.clone());
492
493 match (left_rc, right_rc) {
494 (Some(ref left_class_rc), Some(ref right_class_rc)) => {
495 if Rc::ptr_eq(left_class_rc, right_class_rc) {
496 return Ok(());
497 }
498 let merged_vec: Vec<Obj> = {
499 let left_vec: &Vec<Obj> = left_class_rc.as_ref();
500 let right_vec: &Vec<Obj> = right_class_rc.as_ref();
501 let mut merged = Vec::with_capacity(left_vec.len() + right_vec.len());
502 for obj in left_vec.iter().chain(right_vec.iter()) {
503 merged.push(obj.clone());
504 }
505 merged.sort_by(|a_obj, b_obj| a_obj.to_string().cmp(&b_obj.to_string()));
506 merged.dedup_by(|a_obj, b_obj| a_obj.to_string() == b_obj.to_string());
507 merged
508 };
509 let new_equiv_rc = Rc::new(merged_vec);
510
511 let keys_in_either_class: Vec<ObjString> = self
512 .known_equality
513 .iter()
514 .filter(|(_, (_, class_rc))| {
515 Rc::ptr_eq(class_rc, left_class_rc) || Rc::ptr_eq(class_rc, right_class_rc)
516 })
517 .map(|(k, _)| k.clone())
518 .collect();
519
520 for key_in_class in keys_in_either_class {
521 let removed_entry = match self.known_equality.remove(&key_in_class) {
522 Some(entry) => entry,
523 None => continue,
524 };
525 let (mut direct_equality_proof_map, _) = removed_entry;
526 if key_in_class == left_as_string {
527 direct_equality_proof_map
528 .insert(right_as_string.clone(), equal_atomic_fact.clone());
529 }
530 if key_in_class == right_as_string {
531 direct_equality_proof_map
532 .insert(left_as_string.clone(), equal_atomic_fact.clone());
533 }
534 self.known_equality.insert(
535 key_in_class,
536 (direct_equality_proof_map, Rc::clone(&new_equiv_rc)),
537 );
538 }
539 }
540 (Some(existing_class_rc), None) => {
541 let mut new_vec = (*existing_class_rc).clone();
542 new_vec.push(equality.right.clone());
543 let new_equiv_rc = Rc::new(new_vec);
544
545 let keys_in_existing_class: Vec<ObjString> = self
546 .known_equality
547 .iter()
548 .filter(|(_, (_, class_rc))| Rc::ptr_eq(class_rc, &existing_class_rc))
549 .map(|(k, _)| k.clone())
550 .collect();
551
552 for key_in_class in keys_in_existing_class {
553 let removed_entry = match self.known_equality.remove(&key_in_class) {
554 Some(entry) => entry,
555 None => continue,
556 };
557 let (mut direct_equality_proof_map, _) = removed_entry;
558 if key_in_class == left_as_string {
559 direct_equality_proof_map
560 .insert(right_as_string.clone(), equal_atomic_fact.clone());
561 }
562 self.known_equality.insert(
563 key_in_class,
564 (direct_equality_proof_map, Rc::clone(&new_equiv_rc)),
565 );
566 }
567
568 let mut proof_for_new_right: HashMap<ObjString, AtomicFact> = HashMap::new();
569 proof_for_new_right.insert(left_as_string.clone(), equal_atomic_fact.clone());
570 self.known_equality
571 .insert(right_as_string, (proof_for_new_right, new_equiv_rc));
572 }
573 (None, Some(existing_class_rc)) => {
574 let mut new_vec = (*existing_class_rc).clone();
575 new_vec.push(equality.left.clone());
576 let new_equiv_rc = Rc::new(new_vec);
577
578 let keys_in_existing_class: Vec<ObjString> = self
579 .known_equality
580 .iter()
581 .filter(|(_, (_, class_rc))| Rc::ptr_eq(class_rc, &existing_class_rc))
582 .map(|(k, _)| k.clone())
583 .collect();
584
585 for key_in_class in keys_in_existing_class {
586 let removed_entry = match self.known_equality.remove(&key_in_class) {
587 Some(entry) => entry,
588 None => continue,
589 };
590 let (mut direct_equality_proof_map, _) = removed_entry;
591 if key_in_class == right_as_string {
592 direct_equality_proof_map
593 .insert(left_as_string.clone(), equal_atomic_fact.clone());
594 }
595 self.known_equality.insert(
596 key_in_class,
597 (direct_equality_proof_map, Rc::clone(&new_equiv_rc)),
598 );
599 }
600
601 let mut proof_for_new_left: HashMap<ObjString, AtomicFact> = HashMap::new();
602 proof_for_new_left.insert(right_as_string.clone(), equal_atomic_fact.clone());
603 self.known_equality
604 .insert(left_as_string, (proof_for_new_left, new_equiv_rc));
605 }
606 (None, None) => {
607 let equiv_members = vec![equality.left.clone(), equality.right.clone()];
608 let new_equiv_rc = Rc::new(equiv_members);
609
610 let mut left_direct_proof_map: HashMap<ObjString, AtomicFact> = HashMap::new();
611 left_direct_proof_map.insert(right_as_string.clone(), equal_atomic_fact.clone());
612
613 let mut right_direct_proof_map: HashMap<ObjString, AtomicFact> = HashMap::new();
614 right_direct_proof_map.insert(left_as_string.clone(), equal_atomic_fact);
615
616 self.known_equality.insert(
617 left_as_string.clone(),
618 (left_direct_proof_map, Rc::clone(&new_equiv_rc)),
619 );
620 self.known_equality
621 .insert(right_as_string, (right_direct_proof_map, new_equiv_rc));
622 }
623 }
624
625 if let Some(derived) =
626 super::equality_linear_derive::maybe_derived_linear_equal_fact(equality)
627 {
628 if derived.left.to_string() != derived.right.to_string() {
629 self.store_equality(&derived)?;
630 }
631 }
632 Ok(())
633 }
634}
635
636impl Environment {
637 pub fn new_empty_env() -> Self {
638 Environment::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 HashMap::new(),
657 HashMap::new(),
658 HashMap::new(),
659 HashMap::new(),
660 HashMap::new(),
661 )
662 }
663}
664
665impl Environment {
666 pub fn store_fact_to_cache_known_fact(
667 &mut self,
668 fact_key: FactString,
669 fact_line_file: LineFile,
670 ) -> Result<(), RuntimeError> {
671 self.cache_known_fact.insert(fact_key, fact_line_file);
672 Ok(())
673 }
674}
675
676pub struct KnownForallFactParamsAndDom {
677 pub params_def: ParamDefWithType,
678 pub dom: Vec<Fact>,
679 pub line_file: LineFile,
680}
681
682impl KnownForallFactParamsAndDom {
683 pub fn new(params: ParamDefWithType, dom: Vec<Fact>, line_file: LineFile) -> Self {
684 KnownForallFactParamsAndDom {
685 params_def: params,
686 dom,
687 line_file,
688 }
689 }
690}