Skip to main content

litex/fact/
matchable_fact_with_atomic_fact_inside.rs

1use crate::prelude::*;
2use std::fmt;
3
4#[derive(Clone)]
5pub struct AndFact {
6    pub facts: Vec<AtomicFact>,
7    pub line_file: LineFile,
8}
9
10impl AndFact {
11    pub fn new(facts: Vec<AtomicFact>, line_file: LineFile) -> Self {
12        AndFact { facts, line_file }
13    }
14    pub fn line_file(&self) -> LineFile {
15        self.line_file.clone()
16    }
17}
18
19#[derive(Clone)]
20pub struct ChainFact {
21    pub objs: Vec<Obj>,
22    pub prop_names: Vec<IdentifierOrIdentifierWithMod>,
23    pub line_file: LineFile,
24}
25
26impl ChainFact {
27    pub fn new(
28        objs: Vec<Obj>,
29        prop_names: Vec<IdentifierOrIdentifierWithMod>,
30        line_file: LineFile,
31    ) -> Self {
32        ChainFact {
33            objs,
34            prop_names,
35            line_file,
36        }
37    }
38    pub fn line_file(&self) -> LineFile {
39        self.line_file.clone()
40    }
41
42    pub fn facts(&self) -> Result<Vec<AtomicFact>, RuntimeError> {
43        if self.objs.len() != self.prop_names.len() + 1 {
44            return Err(
45                NewAtomicFactRuntimeError(RuntimeErrorStruct::new(
46                    None,
47                    format!(
48                        "the number of objects ({}) is not equal to the number of property names ({}) + 1",
49                        self.objs.len(),
50                        self.prop_names.len(),
51                    ),
52                    default_line_file(),
53                    None,
54                    vec![],
55                ))
56                .into(),
57            );
58        }
59
60        let mut facts = Vec::with_capacity(self.prop_names.len());
61        for (i, _) in self.prop_names.iter().enumerate() {
62            let prop_name = self.prop_names[i].clone();
63            let left_obj = self.objs[i].clone();
64            let right_obj = self.objs[i + 1].clone();
65            let atomic_fact = AtomicFact::to_atomic_fact(
66                prop_name,
67                true,
68                vec![left_obj, right_obj],
69                self.line_file.clone(),
70            );
71            facts.push(atomic_fact?);
72        }
73        Ok(facts)
74    }
75}
76
77#[derive(Clone)]
78pub enum ChainAtomicFact {
79    AtomicFact(AtomicFact),
80    ChainFact(ChainFact),
81}
82
83impl fmt::Display for ChainAtomicFact {
84    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
85        match self {
86            ChainAtomicFact::AtomicFact(a) => write!(f, "{}", a),
87            ChainAtomicFact::ChainFact(c) => write!(f, "{}", c),
88        }
89    }
90}
91
92#[derive(Clone)]
93pub enum AndChainAtomicFact {
94    AtomicFact(AtomicFact),
95    AndFact(AndFact),
96    ChainFact(ChainFact),
97}
98
99impl AndChainAtomicFact {
100    pub fn line_file(&self) -> LineFile {
101        match self {
102            AndChainAtomicFact::AtomicFact(a) => a.line_file(),
103            AndChainAtomicFact::AndFact(a) => a.line_file(),
104            AndChainAtomicFact::ChainFact(c) => c.line_file(),
105        }
106    }
107
108    pub fn with_new_line_file(self, line_file: LineFile) -> Self {
109        match self {
110            AndChainAtomicFact::AtomicFact(a) => {
111                AndChainAtomicFact::AtomicFact(a.with_new_line_file(line_file))
112            }
113            AndChainAtomicFact::AndFact(af) => AndChainAtomicFact::AndFact(AndFact::new(
114                af.facts
115                    .into_iter()
116                    .map(|x| x.with_new_line_file(line_file.clone()))
117                    .collect(),
118                line_file,
119            )),
120            AndChainAtomicFact::ChainFact(cf) => {
121                AndChainAtomicFact::ChainFact(ChainFact::new(cf.objs, cf.prop_names, line_file))
122            }
123        }
124    }
125
126    pub fn replace_bound_identifier(self, from: &str, to: &str) -> Self {
127        if from == to {
128            return self;
129        }
130        match self {
131            AndChainAtomicFact::AtomicFact(a) => {
132                AndChainAtomicFact::AtomicFact(a.replace_bound_identifier(from, to))
133            }
134            AndChainAtomicFact::AndFact(af) => AndChainAtomicFact::AndFact(AndFact::new(
135                af.facts
136                    .into_iter()
137                    .map(|x| x.replace_bound_identifier(from, to))
138                    .collect(),
139                af.line_file,
140            )),
141            AndChainAtomicFact::ChainFact(cf) => AndChainAtomicFact::ChainFact(ChainFact::new(
142                cf.objs
143                    .into_iter()
144                    .map(|o| Obj::replace_bound_identifier(o, from, to))
145                    .collect(),
146                cf.prop_names,
147                cf.line_file,
148            )),
149        }
150    }
151}
152
153impl From<AtomicFact> for AndChainAtomicFact {
154    fn from(atomic_fact: AtomicFact) -> Self {
155        AndChainAtomicFact::AtomicFact(atomic_fact)
156    }
157}
158
159impl From<GreaterEqualFact> for AndChainAtomicFact {
160    fn from(f: GreaterEqualFact) -> Self {
161        AtomicFact::from(f).into()
162    }
163}
164
165impl fmt::Display for AndFact {
166    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
167        write!(
168            f,
169            "{}",
170            vec_to_string_with_sep(&self.facts, format!(" {} ", AND))
171        )
172    }
173}
174
175impl AndFact {
176    pub fn key(&self) -> String {
177        vec_to_string_with_sep(
178            &self.facts.iter().map(|a| a.key()).collect::<Vec<_>>(),
179            format!(" {} ", AND),
180        )
181    }
182
183    pub fn get_args_from_fact(&self) -> Vec<Obj> {
184        let mut result: Vec<Obj> = Vec::new();
185        for atomic_fact in self.facts.iter() {
186            let args_from_atomic_fact = atomic_fact.get_args_from_fact();
187            for arg in args_from_atomic_fact {
188                result.push(arg);
189            }
190        }
191        result
192    }
193}
194
195impl fmt::Display for ChainFact {
196    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
197        let mut s = self.objs[0].to_string();
198        for (i, obj) in self.objs[1..].iter().enumerate() {
199            if is_comparison_str(&self.prop_names[i].to_string()) {
200                s.push_str(&format!(" {} {}", self.prop_names[i], obj));
201            } else {
202                s.push_str(&format!(" {}{} {}", FACT_PREFIX, self.prop_names[i], obj));
203            }
204        }
205        write!(f, "{}", s)
206    }
207}
208
209impl ChainFact {
210    pub fn key(&self) -> String {
211        vec_to_string_with_sep(
212            &self
213                .prop_names
214                .iter()
215                .map(|p| p.to_string())
216                .collect::<Vec<_>>(),
217            format!(" {} ", AND),
218        )
219    }
220
221    pub fn get_args_from_fact(&self) -> Vec<Obj> {
222        let mut result: Vec<Obj> = Vec::new();
223        for obj in self.objs.iter() {
224            result.push(obj.clone());
225        }
226        result
227    }
228}
229
230impl fmt::Display for AndChainAtomicFact {
231    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
232        match self {
233            AndChainAtomicFact::AtomicFact(a) => write!(f, "{}", a),
234            AndChainAtomicFact::AndFact(a) => write!(f, "{}", a),
235            AndChainAtomicFact::ChainFact(c) => write!(f, "{}", c),
236        }
237    }
238}
239
240impl AndChainAtomicFact {
241    pub fn key(&self) -> String {
242        match self {
243            AndChainAtomicFact::AtomicFact(a) => a.key(),
244            AndChainAtomicFact::AndFact(a) => a.key(),
245            AndChainAtomicFact::ChainFact(c) => c.key(),
246        }
247    }
248}
249
250impl From<AndChainAtomicFact> for ExistOrAndChainAtomicFact {
251    fn from(f: AndChainAtomicFact) -> Self {
252        match f {
253            AndChainAtomicFact::AtomicFact(a) => ExistOrAndChainAtomicFact::AtomicFact(a),
254            AndChainAtomicFact::AndFact(a) => ExistOrAndChainAtomicFact::AndFact(a),
255            AndChainAtomicFact::ChainFact(c) => ExistOrAndChainAtomicFact::ChainFact(c),
256        }
257    }
258}
259
260impl AndChainAtomicFact {
261    pub fn get_args_from_fact(&self) -> Vec<Obj> {
262        match self {
263            AndChainAtomicFact::AtomicFact(atomic_fact) => atomic_fact.get_args_from_fact(),
264            AndChainAtomicFact::AndFact(and_fact) => and_fact.get_args_from_fact(),
265            AndChainAtomicFact::ChainFact(chain_fact) => chain_fact.get_args_from_fact(),
266        }
267    }
268}