litex/fact/
forall_fact.rs

1use crate::prelude::*;
2use std::fmt;
3
4#[derive(Clone)]
5pub struct ForallFact {
6    pub params_def_with_type: ParamDefWithType,
7    pub dom_facts: Vec<Fact>,
8    pub then_facts: Vec<ExistOrAndChainAtomicFact>,
9    pub line_file: LineFile,
10}
11
12impl ForallFact {
13    pub fn new(
14        params_def_with_type: ParamDefWithType,
15        dom_facts: Vec<Fact>,
16        then_facts: Vec<ExistOrAndChainAtomicFact>,
17        line_file: LineFile,
18    ) -> Result<Self, RuntimeError> {
19        let forall_fact = ForallFact {
20            params_def_with_type,
21            dom_facts,
22            then_facts,
23            line_file,
24        };
25        check_forall_fact_has_no_duplicate_forall_free_parameter(&forall_fact)?;
26        Ok(forall_fact)
27    }
28
29    pub fn expand_then_facts_with_order_chain_closure(&mut self) -> Result<(), RuntimeError> {
30        let mut new_then: Vec<ExistOrAndChainAtomicFact> =
31            Vec::with_capacity(self.then_facts.len().saturating_mul(2));
32        for tf in std::mem::take(&mut self.then_facts) {
33            match tf {
34                ExistOrAndChainAtomicFact::ChainFact(c) => {
35                    let atomics = c.facts_with_order_transitive_closure()?;
36                    new_then.push(ExistOrAndChainAtomicFact::ChainFact(c));
37                    for af in atomics {
38                        new_then.push(ExistOrAndChainAtomicFact::AtomicFact(af));
39                    }
40                }
41                other => new_then.push(other),
42            }
43        }
44        self.then_facts = new_then;
45        Ok(())
46    }
47}
48
49impl fmt::Display for ForallFact {
50    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
51        match self.dom_facts.len() {
52            0 => write!(
53                f,
54                "{} {}{}\n{}",
55                FORALL,
56                self.params_def_with_type.to_string(),
57                COLON,
58                vec_to_string_add_four_spaces_at_beginning_of_each_line(&self.then_facts, 1)
59            ),
60            _ => write!(
61                f,
62                "{} {}{}\n{}\n{}{}\n{}",
63                FORALL,
64                self.params_def_with_type.to_string(),
65                COLON,
66                vec_to_string_add_four_spaces_at_beginning_of_each_line(&self.dom_facts, 1),
67                to_string_and_add_four_spaces_at_beginning_of_each_line(&RIGHT_ARROW, 1),
68                COLON,
69                vec_to_string_add_four_spaces_at_beginning_of_each_line(&self.then_facts, 2)
70            ),
71        }
72    }
73}
litex/fact/forall_fact.rs

litex/fact/
forall_fact.rs
