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