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