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    ) -> Self {
19        ForallFact {
20            params_def_with_type,
21            dom_facts,
22            then_facts,
23            line_file,
24        }
25    }
26
27    pub fn expand_then_facts_with_order_chain_closure(&mut self) -> Result<(), RuntimeError> {
28        let mut new_then: Vec<ExistOrAndChainAtomicFact> =
29            Vec::with_capacity(self.then_facts.len().saturating_mul(2));
30        for tf in std::mem::take(&mut self.then_facts) {
31            match tf {
32                ExistOrAndChainAtomicFact::ChainFact(c) => {
33                    let atomics = c.facts_with_order_transitive_closure()?;
34                    new_then.push(ExistOrAndChainAtomicFact::ChainFact(c));
35                    for af in atomics {
36                        new_then.push(ExistOrAndChainAtomicFact::AtomicFact(af));
37                    }
38                }
39                other => new_then.push(other),
40            }
41        }
42        self.then_facts = new_then;
43        Ok(())
44    }
45}
46
47impl fmt::Display for ForallFact {
48    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
49        match self.dom_facts.len() {
50            0 => write!(
51                f,
52                "{} {}{}\n{}",
53                FORALL,
54                self.params_def_with_type.to_string(),
55                COLON,
56                vec_to_string_add_four_spaces_at_beginning_of_each_line(&self.then_facts, 1)
57            ),
58            _ => write!(
59                f,
60                "{} {}{}\n{}\n{}{}\n{}",
61                FORALL,
62                self.params_def_with_type.to_string(),
63                COLON,
64                vec_to_string_add_four_spaces_at_beginning_of_each_line(&self.dom_facts, 1),
65                to_string_and_add_four_spaces_at_beginning_of_each_line(&RIGHT_ARROW, 1),
66                COLON,
67                vec_to_string_add_four_spaces_at_beginning_of_each_line(&self.then_facts, 2)
68            ),
69        }
70    }
71}
litex/fact/forall_fact.rs

litex/fact/
forall_fact.rs
