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