litex/fact/
forall_fact.rs

1use crate::prelude::*;
2use std::fmt;
3
4#[derive(Clone)]
5pub struct ForallFact {
6    pub params_def_with_type: Vec<ParamGroupWithParamType>,
7    pub dom_facts: Vec<ExistOrAndChainAtomicFact>,
8    pub then_facts: Vec<ExistOrAndChainAtomicFact>,
9    pub line_file: LineFile,
10}
11
12impl ForallFact {
13    pub fn new(
14        params_def_with_type: Vec<ParamGroupWithParamType>,
15        dom_facts: Vec<ExistOrAndChainAtomicFact>,
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
28impl fmt::Display for ForallFact {
29    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
30        match self.dom_facts.len() {
31            0 => write!(
32                f,
33                "{} {}{}\n{}",
34                FORALL,
35                vec_to_string_join_by_comma(&self.params_def_with_type),
36                COLON,
37                vec_to_string_add_four_spaces_at_beginning_of_each_line(&self.then_facts, 1)
38            ),
39            _ => write!(
40                f,
41                "{} {}{}\n{}\n{}{}\n{}",
42                FORALL,
43                vec_to_string_join_by_comma(&self.params_def_with_type),
44                COLON,
45                vec_to_string_add_four_spaces_at_beginning_of_each_line(&self.dom_facts, 1),
46                to_string_and_add_four_spaces_at_beginning_of_each_line(&RIGHT_ARROW, 1),
47                COLON,
48                vec_to_string_add_four_spaces_at_beginning_of_each_line(&self.then_facts, 2)
49            ),
50        }
51    }
52}
litex/fact/forall_fact.rs

litex/fact/
forall_fact.rs
