1use crate::prelude::*;
2use std::collections::HashMap;
3use std::fmt;
4use std::rc::Rc;
5
6pub struct Environment {
7 pub defined_identifiers: HashMap<IdentifierName, ()>,
8 pub defined_def_props: HashMap<PropName, DefPropStmt>,
9 pub defined_abstract_props: HashMap<AbstractPropName, DefAbstractPropStmt>,
10 pub defined_structs: HashMap<StructName, DefStructStmt>,
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<ExistFact>>,
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<(ExistFact, 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_normalized_decimal_number: HashMap<ObjString, Number>,
36
37 pub known_identifier_satisfy_struct: HashMap<FieldAccessName, StructObj>,
38
39 pub known_objs_in_fn_sets: HashMap<ObjString, FnSet>,
40
41 pub cache_well_defined_obj: HashMap<ObjString, ()>,
42 pub cache_known_fact: HashMap<FactString, LineFile>,
43}
44
45impl Environment {
46 pub fn new(
47 objs: HashMap<IdentifierName, ()>,
48 def_props: HashMap<PropName, DefPropStmt>,
49 struct_defs: HashMap<StructName, DefStructStmt>,
50 families: HashMap<FamilyName, DefFamilyStmt>,
51 abstract_props: HashMap<AbstractPropName, DefAbstractPropStmt>,
52 algorithms: HashMap<AlgoName, DefAlgoStmt>,
53 field_access_name: HashMap<FieldAccessName, StructObj>,
54 known_equality: HashMap<ObjString, (HashMap<ObjString, AtomicFact>, Rc<Vec<Obj>>)>,
55 known_fn_in_fn_set: HashMap<ObjString, FnSet>,
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<ExistFact>>,
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<(ExistFact, 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_calculated_value_of_obj: HashMap<ObjString, Number>,
85 cache_known_valid_obj: HashMap<ObjString, ()>,
86 cache_known_fact: HashMap<FactString, LineFile>,
87 ) -> Self {
88 Environment {
89 defined_identifiers: objs,
90 defined_def_props: def_props,
91 defined_structs: struct_defs,
92 defined_families: families,
93 defined_abstract_props: abstract_props,
94 defined_algorithms: algorithms,
95 known_identifier_satisfy_struct: field_access_name,
96 known_equality,
97 known_objs_in_fn_sets: known_fn_in_fn_set,
98 known_atomic_facts_with_0_or_more_than_2_args,
99 known_atomic_facts_with_1_arg: known_atomic_facts_with_1_arg,
100 known_atomic_facts_with_2_args: known_atomic_facts_with_2_args,
101 known_exist_facts,
102 known_atomic_facts_in_forall_facts,
103 known_exist_facts_in_forall_facts,
104 known_or_facts,
105 known_or_facts_in_forall_facts,
106 known_objs_equal_to_tuple: known_tuple_objs,
107 known_objs_equal_to_cart: known_cart_objs,
108 known_objs_equal_to_normalized_decimal_number: known_calculated_value_of_obj,
109 cache_well_defined_obj: cache_known_valid_obj,
110 cache_known_fact,
111 }
112 }
113}
114
115impl fmt::Display for Environment {
116 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
117 write!(f, "Environment {{\n")?;
118 write!(f, " objs: {:?}\n", self.defined_identifiers.len())?;
119 write!(f, " def_props: {:?}\n", self.defined_def_props.len())?;
120 write!(f, " defined_structs: {:?}\n", self.defined_structs.len())?;
121 write!(f, " families: {:?}\n", self.defined_families.len())?;
122 write!(f, " algorithms: {:?}\n", self.defined_algorithms.len())?;
123 write!(f, " known_equality: {:?}\n", self.known_equality.len())?;
124 write!(
125 f,
126 " known_fn_in_fn_set: {:?}\n",
127 self.known_objs_in_fn_sets.len()
128 )?;
129 write!(
130 f,
131 " known_atomic_facts_with_0_or_more_than_two_params: {:?}\n",
132 self.known_atomic_facts_with_0_or_more_than_2_args.len()
133 )?;
134 write!(
135 f,
136 " known_atomic_facts_with_1_arg: {:?}\n",
137 self.known_atomic_facts_with_1_arg.len()
138 )?;
139 write!(
140 f,
141 " known_atomic_facts_with_2_args: {:?}\n",
142 self.known_atomic_facts_with_2_args.len()
143 )?;
144 write!(
145 f,
146 " known_exist_facts_with_more_than_two_params: {:?}\n",
147 self.known_exist_facts.len()
148 )?;
149 write!(
150 f,
151 " known_or_facts_with_more_than_two_params: {:?}\n",
152 self.known_or_facts.len()
153 )?;
154 write!(
155 f,
156 " known_atomic_facts_in_forall_facts: {:?}\n",
157 self.known_atomic_facts_in_forall_facts.len()
158 )?;
159 write!(
160 f,
161 " known_exist_facts_in_forall_facts: {:?}\n",
162 self.known_exist_facts_in_forall_facts.len()
163 )?;
164 write!(
165 f,
166 " known_or_facts_in_forall_facts: {:?}\n",
167 self.known_or_facts_in_forall_facts.len()
168 )?;
169 write!(
170 f,
171 " cache_known_valid_obj: {:?}\n",
172 self.cache_well_defined_obj.len()
173 )?;
174 write!(
175 f,
176 " cache_known_fact: {:?}\n",
177 self.cache_known_fact.len()
178 )?;
179 write!(f, "}}")
180 }
181}
182
183impl Environment {
184 pub fn store_atomic_fact_by_ref(
185 &mut self,
186 atomic_fact: &AtomicFact,
187 ) -> Result<(), RuntimeErrorStruct> {
188 self.store_atomic_fact(atomic_fact.clone())
189 }
190
191 pub(crate) fn store_atomic_fact(
192 &mut self,
193 atomic_fact: AtomicFact,
194 ) -> Result<(), RuntimeErrorStruct> {
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: ExistFact) -> Result<(), RuntimeErrorStruct> {
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<(), RuntimeErrorStruct> {
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_ref: &AtomicFact,
264 forall_params_and_dom: Rc<KnownForallFactParamsAndDom>,
265 ) -> Result<(), RuntimeErrorStruct> {
266 let key: AtomicFactKey = atomic_fact_ref.key();
267 let is_true = atomic_fact_ref.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_ref.clone(), forall_params_and_dom));
273 } else {
274 self.known_atomic_facts_in_forall_facts.insert(
275 (key, is_true),
276 vec![(atomic_fact_ref.clone(), forall_params_and_dom)],
277 );
278 }
279 Ok(())
280 }
281
282 fn store_or_fact_in_forall_fact(
283 &mut self,
284 or_fact: &OrFact,
285 forall_params_and_dom: Rc<KnownForallFactParamsAndDom>,
286 ) -> Result<(), RuntimeErrorStruct> {
287 let key: OrFactKey = or_fact.key();
288 if let Some(vec_ref) = self.known_or_facts_in_forall_facts.get_mut(&key) {
289 vec_ref.push((or_fact.clone(), forall_params_and_dom));
290 } else {
291 self.known_or_facts_in_forall_facts
292 .insert(key, vec![(or_fact.clone(), forall_params_and_dom)]);
293 }
294 Ok(())
295 }
296
297 fn store_a_fact_in_forall_fact(
298 &mut self,
299 fact: &ExistOrAndChainAtomicFact,
300 forall_params_and_dom: Rc<KnownForallFactParamsAndDom>,
301 ) -> Result<(), RuntimeErrorStruct> {
302 match fact {
303 ExistOrAndChainAtomicFact::AtomicFact(spec_fact) => {
304 self.store_atomic_fact_in_forall_fact(&spec_fact, forall_params_and_dom)
305 }
306 ExistOrAndChainAtomicFact::OrFact(or_fact) => {
307 self.store_or_fact_in_forall_fact(&or_fact, forall_params_and_dom)
308 }
309 ExistOrAndChainAtomicFact::AndFact(and_fact) => {
310 self.store_and_fact_in_forall_fact(&and_fact, forall_params_and_dom)
311 }
312 ExistOrAndChainAtomicFact::ChainFact(chain_fact) => {
313 self.store_chain_fact_in_forall_fact(&chain_fact, forall_params_and_dom)
314 }
315 ExistOrAndChainAtomicFact::ExistFact(exist_fact) => {
316 self.store_exist_fact_in_forall_fact(&exist_fact, forall_params_and_dom)
317 }
318 }
319 }
320
321 fn store_chain_fact_in_forall_fact(
322 &mut self,
323 chain_fact: &ChainFact,
324 forall_params_and_dom: Rc<KnownForallFactParamsAndDom>,
325 ) -> Result<(), RuntimeErrorStruct> {
326 for fact in chain_fact
327 .facts()
328 .map_err(|e| {
329 RuntimeErrorStruct::new_with_conflict(
330 e.statement.clone(),
331 e.msg.clone(),
332 e.line_file.clone(),
333 e.conflict_with.clone(),
334 Some(NewAtomicFactRuntimeError(e).into()),
335 vec![],
336 )
337 })?
338 .iter()
339 {
340 self.store_a_fact_in_forall_fact(
341 &ExistOrAndChainAtomicFact::AtomicFact(fact.clone()),
342 forall_params_and_dom.clone(),
343 )?;
344 }
345 Ok(())
346 }
347
348 fn store_exist_fact_in_forall_fact(
349 &mut self,
350 exist_fact: &ExistFact,
351 forall_params_and_dom: Rc<KnownForallFactParamsAndDom>,
352 ) -> Result<(), RuntimeErrorStruct> {
353 let key: ExistFactKey = exist_fact.key();
354 if let Some(vec_ref) = self.known_exist_facts_in_forall_facts.get_mut(&key) {
355 vec_ref.push((exist_fact.clone(), forall_params_and_dom));
356 } else {
357 self.known_exist_facts_in_forall_facts
358 .insert(key, vec![(exist_fact.clone(), forall_params_and_dom)]);
359 }
360 Ok(())
361 }
362
363 fn store_and_fact_in_forall_fact(
364 &mut self,
365 and_fact: &AndFact,
366 forall_params_and_dom: Rc<KnownForallFactParamsAndDom>,
367 ) -> Result<(), RuntimeErrorStruct> {
368 for fact in and_fact.facts.iter() {
369 self.store_a_fact_in_forall_fact(
370 &ExistOrAndChainAtomicFact::AtomicFact(fact.clone()),
371 forall_params_and_dom.clone(),
372 )?;
373 }
374 Ok(())
375 }
376
377 fn store_forall_fact(&mut self, forall_fact: Rc<ForallFact>) -> Result<(), RuntimeErrorStruct> {
378 let forall_params_and_dom = Rc::new(KnownForallFactParamsAndDom::new(
379 forall_fact.params_def_with_type.clone(),
380 forall_fact.dom_facts.clone(),
381 forall_fact.line_file.clone(),
382 ));
383
384 for fact in forall_fact.then_facts.iter() {
385 self.store_a_fact_in_forall_fact(fact, forall_params_and_dom.clone())?;
386 }
387 Ok(())
388 }
389
390 fn store_and_fact(&mut self, and_fact: AndFact) -> Result<(), RuntimeErrorStruct> {
391 for atomic_fact in and_fact.facts {
392 self.store_atomic_fact(atomic_fact)?;
393 }
394 Ok(())
395 }
396
397 fn store_forall_fact_with_iff(
398 &mut self,
399 forall_fact_with_iff: ForallFactWithIff,
400 ) -> Result<(), RuntimeErrorStruct> {
401 let (forall_then_implies_iff, forall_iff_implies_then) =
402 forall_fact_with_iff.to_two_forall_facts();
403 self.store_forall_fact(Rc::new(forall_then_implies_iff))?;
404 self.store_forall_fact(Rc::new(forall_iff_implies_then))?;
405 Ok(())
406 }
407
408 pub fn store_fact(&mut self, fact: Fact) -> Result<(), RuntimeErrorStruct> {
409 match fact {
410 Fact::AtomicFact(atomic_fact) => self.store_atomic_fact(atomic_fact),
411 Fact::ExistFact(exist_fact) => self.store_exist_fact(exist_fact),
412 Fact::OrFact(or_fact) => self.store_or_fact(or_fact),
413 Fact::AndFact(and_fact) => self.store_and_fact(and_fact),
414 Fact::ChainFact(chain_fact) => self.store_chain_fact(chain_fact),
415 Fact::ForallFact(forall_fact) => self.store_forall_fact(Rc::new(forall_fact)),
416 Fact::ForallFactWithIff(forall_fact_with_iff) => {
417 self.store_forall_fact_with_iff(forall_fact_with_iff)
418 }
419 }
420 }
421
422 pub fn store_exist_fact_by_ref(
423 &mut self,
424 exist_fact: &ExistFact,
425 ) -> Result<(), RuntimeErrorStruct> {
426 self.store_exist_fact(exist_fact.clone())
427 }
428
429 pub fn store_exist_or_and_chain_atomic_fact(
430 &mut self,
431 fact: ExistOrAndChainAtomicFact,
432 ) -> Result<(), RuntimeErrorStruct> {
433 match fact {
434 ExistOrAndChainAtomicFact::AtomicFact(atomic_fact) => {
435 self.store_atomic_fact(atomic_fact)
436 }
437 ExistOrAndChainAtomicFact::AndFact(and_fact) => self.store_and_fact(and_fact),
438 ExistOrAndChainAtomicFact::ChainFact(chain_fact) => self.store_chain_fact(chain_fact),
439 ExistOrAndChainAtomicFact::OrFact(or_fact) => self.store_or_fact(or_fact),
440 ExistOrAndChainAtomicFact::ExistFact(exist_fact) => self.store_exist_fact(exist_fact),
441 }
442 }
443
444 pub fn store_and_chain_atomic_fact(
445 &mut self,
446 and_chain_atomic_fact: AndChainAtomicFact,
447 ) -> Result<(), RuntimeErrorStruct> {
448 match and_chain_atomic_fact {
449 AndChainAtomicFact::AtomicFact(atomic_fact) => self.store_atomic_fact(atomic_fact),
450 AndChainAtomicFact::AndFact(and_fact) => self.store_and_fact(and_fact),
451 AndChainAtomicFact::ChainFact(chain_fact) => self.store_chain_fact(chain_fact),
452 }
453 }
454
455 pub fn store_or_and_chain_atomic_fact(
456 &mut self,
457 fact: OrAndChainAtomicFact,
458 ) -> Result<(), RuntimeErrorStruct> {
459 match fact {
460 OrAndChainAtomicFact::AtomicFact(atomic_fact) => self.store_atomic_fact(atomic_fact),
461 OrAndChainAtomicFact::AndFact(and_fact) => self.store_and_fact(and_fact),
462 OrAndChainAtomicFact::ChainFact(chain_fact) => self.store_chain_fact(chain_fact),
463 OrAndChainAtomicFact::OrFact(or_fact) => self.store_or_fact(or_fact),
464 }
465 }
466
467 fn store_chain_fact(&mut self, chain_fact: ChainFact) -> Result<(), RuntimeErrorStruct> {
468 let atomic_facts = chain_fact
469 .facts_with_order_transitive_closure()
470 .map_err(|e| {
471 RuntimeErrorStruct::new_with_conflict(
472 e.statement.clone(),
473 e.msg.clone(),
474 e.line_file.clone(),
475 e.conflict_with.clone(),
476 Some(NewAtomicFactRuntimeError(e).into()),
477 vec![],
478 )
479 })?;
480 for atomic_fact in atomic_facts {
481 self.store_atomic_fact(atomic_fact)?;
482 }
483 Ok(())
484 }
485
486 pub fn store_chain_fact_by_ref(
487 &mut self,
488 chain_fact: &ChainFact,
489 ) -> Result<(), RuntimeErrorStruct> {
490 self.store_chain_fact(chain_fact.clone())
491 }
492
493 pub fn store_equality(&mut self, equality: &EqualFact) -> Result<(), RuntimeErrorStruct> {
494 let left_as_string: ObjString = equality.left.to_string();
495 let right_as_string: ObjString = equality.right.to_string();
496 if left_as_string == right_as_string {
497 return Ok(());
498 }
499
500 let left_rc = self
501 .known_equality
502 .get(&left_as_string)
503 .map(|(_, rc)| Rc::clone(rc));
504 let right_rc = self
505 .known_equality
506 .get(&right_as_string)
507 .map(|(_, rc)| Rc::clone(rc));
508
509 let equal_atomic_fact = AtomicFact::EqualFact(equality.clone());
510
511 match (left_rc, right_rc) {
512 (Some(ref left_class_rc), Some(ref right_class_rc)) => {
513 if Rc::ptr_eq(left_class_rc, right_class_rc) {
514 return Ok(());
515 }
516 let merged_vec: Vec<Obj> = {
517 let left_vec: &Vec<Obj> = left_class_rc.as_ref();
518 let right_vec: &Vec<Obj> = right_class_rc.as_ref();
519 let mut merged = Vec::with_capacity(left_vec.len() + right_vec.len());
520 for obj in left_vec.iter().chain(right_vec.iter()) {
521 merged.push(obj.clone());
522 }
523 merged.sort_by(|a_obj, b_obj| a_obj.to_string().cmp(&b_obj.to_string()));
524 merged.dedup_by(|a_obj, b_obj| a_obj.to_string() == b_obj.to_string());
525 merged
526 };
527 let new_equiv_rc = Rc::new(merged_vec);
528
529 let keys_in_either_class: Vec<ObjString> = self
530 .known_equality
531 .iter()
532 .filter(|(_, (_, class_rc))| {
533 Rc::ptr_eq(class_rc, left_class_rc) || Rc::ptr_eq(class_rc, right_class_rc)
534 })
535 .map(|(k, _)| k.clone())
536 .collect();
537
538 for key_in_class in keys_in_either_class {
539 let removed_entry = match self.known_equality.remove(&key_in_class) {
540 Some(entry) => entry,
541 None => continue,
542 };
543 let (mut direct_equality_proof_map, _) = removed_entry;
544 if key_in_class == left_as_string {
545 direct_equality_proof_map
546 .insert(right_as_string.clone(), equal_atomic_fact.clone());
547 }
548 if key_in_class == right_as_string {
549 direct_equality_proof_map
550 .insert(left_as_string.clone(), equal_atomic_fact.clone());
551 }
552 self.known_equality.insert(
553 key_in_class,
554 (direct_equality_proof_map, Rc::clone(&new_equiv_rc)),
555 );
556 }
557 }
558 (Some(existing_class_rc), None) => {
559 let mut new_vec = (*existing_class_rc).clone();
560 new_vec.push(equality.right.clone());
561 let new_equiv_rc = Rc::new(new_vec);
562
563 let keys_in_existing_class: Vec<ObjString> = self
564 .known_equality
565 .iter()
566 .filter(|(_, (_, class_rc))| Rc::ptr_eq(class_rc, &existing_class_rc))
567 .map(|(k, _)| k.clone())
568 .collect();
569
570 for key_in_class in keys_in_existing_class {
571 let removed_entry = match self.known_equality.remove(&key_in_class) {
572 Some(entry) => entry,
573 None => continue,
574 };
575 let (mut direct_equality_proof_map, _) = removed_entry;
576 if key_in_class == left_as_string {
577 direct_equality_proof_map
578 .insert(right_as_string.clone(), equal_atomic_fact.clone());
579 }
580 self.known_equality.insert(
581 key_in_class,
582 (direct_equality_proof_map, Rc::clone(&new_equiv_rc)),
583 );
584 }
585
586 let mut proof_for_new_right: HashMap<ObjString, AtomicFact> = HashMap::new();
587 proof_for_new_right.insert(left_as_string.clone(), equal_atomic_fact.clone());
588 self.known_equality
589 .insert(right_as_string, (proof_for_new_right, new_equiv_rc));
590 }
591 (None, Some(existing_class_rc)) => {
592 let mut new_vec = (*existing_class_rc).clone();
593 new_vec.push(equality.left.clone());
594 let new_equiv_rc = Rc::new(new_vec);
595
596 let keys_in_existing_class: Vec<ObjString> = self
597 .known_equality
598 .iter()
599 .filter(|(_, (_, class_rc))| Rc::ptr_eq(class_rc, &existing_class_rc))
600 .map(|(k, _)| k.clone())
601 .collect();
602
603 for key_in_class in keys_in_existing_class {
604 let removed_entry = match self.known_equality.remove(&key_in_class) {
605 Some(entry) => entry,
606 None => continue,
607 };
608 let (mut direct_equality_proof_map, _) = removed_entry;
609 if key_in_class == right_as_string {
610 direct_equality_proof_map
611 .insert(left_as_string.clone(), equal_atomic_fact.clone());
612 }
613 self.known_equality.insert(
614 key_in_class,
615 (direct_equality_proof_map, Rc::clone(&new_equiv_rc)),
616 );
617 }
618
619 let mut proof_for_new_left: HashMap<ObjString, AtomicFact> = HashMap::new();
620 proof_for_new_left.insert(right_as_string.clone(), equal_atomic_fact.clone());
621 self.known_equality
622 .insert(left_as_string, (proof_for_new_left, new_equiv_rc));
623 }
624 (None, None) => {
625 let equiv_members = vec![equality.left.clone(), equality.right.clone()];
626 let new_equiv_rc = Rc::new(equiv_members);
627
628 let mut left_direct_proof_map: HashMap<ObjString, AtomicFact> = HashMap::new();
629 left_direct_proof_map.insert(right_as_string.clone(), equal_atomic_fact.clone());
630
631 let mut right_direct_proof_map: HashMap<ObjString, AtomicFact> = HashMap::new();
632 right_direct_proof_map.insert(left_as_string.clone(), equal_atomic_fact);
633
634 self.known_equality.insert(
635 left_as_string.clone(),
636 (left_direct_proof_map, Rc::clone(&new_equiv_rc)),
637 );
638 self.known_equality
639 .insert(right_as_string, (right_direct_proof_map, new_equiv_rc));
640 }
641 }
642 Ok(())
643 }
644}
645
646impl Environment {
647 pub fn new_empty_env() -> Self {
648 Environment::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 HashMap::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 )
672 }
673}
674
675impl Environment {
676 pub fn store_fact_to_cache_known_fact(
677 &mut self,
678 fact_key: FactString,
679 fact_line_file: LineFile,
680 ) -> Result<(), RuntimeErrorStruct> {
681 self.cache_known_fact.insert(fact_key, fact_line_file);
682 Ok(())
683 }
684}
685
686pub struct KnownForallFactParamsAndDom {
687 pub params_def: Vec<ParamGroupWithParamType>,
688 pub dom: Vec<ExistOrAndChainAtomicFact>,
689 pub line_file: LineFile,
690}
691
692impl KnownForallFactParamsAndDom {
693 pub fn new(
694 params: Vec<ParamGroupWithParamType>,
695 dom: Vec<ExistOrAndChainAtomicFact>,
696 line_file: LineFile,
697 ) -> Self {
698 KnownForallFactParamsAndDom {
699 params_def: params,
700 dom,
701 line_file,
702 }
703 }
704}