litex/stmt/
parameter_def.rs

1use crate::prelude::*;
2use std::collections::HashMap;
3use std::fmt;
4
5#[derive(Clone)]
6pub enum ParamType {
7    Set(Set),
8    NonemptySet(NonemptySet),
9    FiniteSet(FiniteSet),
10    Obj(Obj),
11}
12
13/// Full parameter list with types, e.g. `a, b T, c E` as a sequence of [`ParamGroupWithParamType`].
14#[derive(Clone)]
15pub struct ParamDefWithType {
16    pub groups: Vec<ParamGroupWithParamType>,
17}
18
19impl ParamDefWithType {
20    pub fn new(groups: Vec<ParamGroupWithParamType>) -> Self {
21        ParamDefWithType { groups }
22    }
23
24    pub fn len(&self) -> usize {
25        self.groups.len()
26    }
27
28    pub fn is_empty(&self) -> bool {
29        self.groups.is_empty()
30    }
31
32    pub fn iter(&self) -> std::slice::Iter<'_, ParamGroupWithParamType> {
33        self.groups.iter()
34    }
35
36    pub fn as_slice(&self) -> &[ParamGroupWithParamType] {
37        self.groups.as_slice()
38    }
39
40    pub fn number_of_params(&self) -> usize {
41        let mut total_param_count: usize = 0;
42        for p in self.groups.iter() {
43            total_param_count += p.params.len();
44        }
45        total_param_count
46    }
47
48    pub fn collect_param_names(&self) -> Vec<String> {
49        let mut names: Vec<String> = Vec::with_capacity(self.number_of_params());
50        for def in self.groups.iter() {
51            for name in def.param_names().iter() {
52                names.push(name.clone());
53            }
54        }
55        names
56    }
57
58    pub fn collect_param_names_with_types(&self) -> Vec<(String, ParamType)> {
59        let mut out: Vec<(String, ParamType)> = Vec::with_capacity(self.number_of_params());
60        for def in self.groups.iter() {
61            for name in def.param_names().iter() {
62                out.push((name.clone(), def.param_type.clone()));
63            }
64        }
65        out
66    }
67
68    pub fn flat_instantiated_types_for_args(
69        &self,
70        instantiated_types: &[ParamType],
71    ) -> Vec<ParamType> {
72        let mut result = Vec::with_capacity(self.number_of_params());
73        for (param_def, param_type) in self.groups.iter().zip(instantiated_types.iter()) {
74            for _ in param_def.params.iter() {
75                result.push(param_type.clone());
76            }
77        }
78        result
79    }
80
81    pub fn param_def_params_to_arg_map(
82        &self,
83        arg_map: &HashMap<String, Obj>,
84    ) -> Option<HashMap<String, Obj>> {
85        let param_names = self.collect_param_names();
86        let mut result = HashMap::new();
87        for param_name in param_names.iter() {
88            let objs_option = arg_map.get(param_name);
89            let objs = match objs_option {
90                Some(v) => v,
91                None => return None,
92            };
93            result.insert(param_name.clone(), objs.clone());
94        }
95        Some(result)
96    }
97
98    pub fn param_defs_and_args_to_param_to_arg_map(&self, args: &[Obj]) -> HashMap<String, Obj> {
99        let param_names = self.collect_param_names();
100        if param_names.len() != args.len() {
101            unreachable!();
102        }
103
104        let mut result: HashMap<String, Obj> = HashMap::new();
105        let mut index = 0;
106        while index < param_names.len() {
107            let param_name = &param_names[index];
108            let arg = &args[index];
109            result.insert(param_name.clone(), arg.clone());
110            index += 1;
111        }
112        result
113    }
114}
115
116impl fmt::Display for ParamDefWithType {
117    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
118        write!(f, "{}", vec_to_string_join_by_comma(&self.groups))
119    }
120}
121
122impl From<Vec<ParamGroupWithParamType>> for ParamDefWithType {
123    fn from(groups: Vec<ParamGroupWithParamType>) -> Self {
124        ParamDefWithType::new(groups)
125    }
126}
127
128#[derive(Clone)]
129pub struct ParamGroupWithSet {
130    pub params: Vec<String>,
131    pub set: Obj,
132}
133
134#[derive(Clone)]
135pub struct ParamGroupWithParamType {
136    pub params: Vec<String>,
137    pub param_type: ParamType,
138}
139
140#[derive(Clone)]
141pub struct Set {}
142
143#[derive(Clone)]
144pub struct NonemptySet {}
145
146#[derive(Clone)]
147pub struct FiniteSet {}
148
149impl Set {
150    pub fn new() -> Self {
151        Set {}
152    }
153}
154
155impl NonemptySet {
156    pub fn new() -> Self {
157        NonemptySet {}
158    }
159}
160
161impl FiniteSet {
162    pub fn new() -> Self {
163        FiniteSet {}
164    }
165}
166
167impl fmt::Display for ParamType {
168    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
169        match self {
170            ParamType::Set(set) => write!(f, "{}", set.to_string()),
171            ParamType::NonemptySet(nonempty_set) => write!(f, "{}", nonempty_set.to_string()),
172            ParamType::FiniteSet(finite_set) => write!(f, "{}", finite_set.to_string()),
173            ParamType::Obj(obj) => write!(f, "{}", obj),
174        }
175    }
176}
177
178impl fmt::Display for Set {
179    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
180        write!(f, "{}", SET)
181    }
182}
183
184impl fmt::Display for NonemptySet {
185    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
186        write!(f, "{}", NONEMPTY_SET)
187    }
188}
189
190impl fmt::Display for FiniteSet {
191    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
192        write!(f, "{}", FINITE_SET)
193    }
194}
195
196impl fmt::Display for ParamGroupWithSet {
197    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
198        write!(
199            f,
200            "{} {}",
201            comma_separated_stored_fn_params_as_user_source(&self.params),
202            self.set
203        )
204    }
205}
206
207impl fmt::Display for ParamGroupWithParamType {
208    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
209        write!(
210            f,
211            "{} {}",
212            vec_to_string_join_by_comma(&self.params),
213            self.param_type
214        )
215    }
216}
217
218impl ParamGroupWithParamType {
219    pub fn new(params: Vec<String>, param_type: ParamType) -> Self {
220        ParamGroupWithParamType { params, param_type }
221    }
222
223    pub fn param_names(&self) -> &Vec<String> {
224        &self.params
225    }
226}
227
228impl ParamGroupWithSet {
229    pub fn new(params: Vec<String>, set: Obj) -> Self {
230        ParamGroupWithSet { params, set }
231    }
232
233    pub fn facts(&self) -> Vec<Fact> {
234        let mut facts = Vec::with_capacity(self.params.len());
235        for name in self.params.iter() {
236            let fact = InFact::new(
237                obj_for_bound_param_in_scope(name.clone(), ParamObjType::FnSet),
238                self.set.clone(),
239                default_line_file(),
240            )
241            .into();
242            facts.push(fact);
243        }
244        facts
245    }
246
247    // Example: given fn(x R, y Q), we want to verify x = 1, y = 2 can be used as argument to this function. This function returns the facts that 1 $in R, 2 $in Q.
248    // 与 [`ParamGroupWithParamType`] 不同：此处每个参数必须属于**事先确定**的集合（不能用 `set` / `nonempty_set` / `finite_set` 等语法糖），且该集合不能依赖更早的参数。例如 `x R, y f(x)` 不允许。
249    pub fn facts_for_args_satisfy_param_def_with_set_vec(
250        runtime: &Runtime,
251        param_defs: &Vec<ParamGroupWithSet>,
252        args: &Vec<Obj>,
253        param_obj_type: ParamObjType,
254    ) -> Result<Vec<AtomicFact>, RuntimeError> {
255        let instantiated_param_sets =
256            runtime.inst_param_def_with_set_one_by_one(param_defs, args, param_obj_type)?;
257        let flat_param_sets =
258            Self::flat_instantiated_param_sets_for_args(param_defs, &instantiated_param_sets);
259        let mut facts = Vec::with_capacity(args.len());
260        for (arg, param_set) in args.iter().zip(flat_param_sets.iter()) {
261            facts.push(InFact::new(arg.clone(), param_set.clone(), default_line_file()).into());
262        }
263        Ok(facts)
264    }
265
266    fn flat_instantiated_param_sets_for_args(
267        param_defs: &Vec<ParamGroupWithSet>,
268        instantiated_param_sets: &Vec<Obj>,
269    ) -> Vec<Obj> {
270        let mut result = Vec::with_capacity(Self::number_of_params(param_defs));
271        for (param_def, param_set) in param_defs.iter().zip(instantiated_param_sets.iter()) {
272            for _ in param_def.params.iter() {
273                result.push(param_set.clone());
274            }
275        }
276        result
277    }
278
279    pub fn param_names(&self) -> &Vec<String> {
280        &self.params
281    }
282
283    pub fn collect_param_names(param_defs: &Vec<ParamGroupWithSet>) -> Vec<String> {
284        let mut names: Vec<String> = Vec::with_capacity(Self::number_of_params(param_defs));
285        for def in param_defs.iter() {
286            for name in def.param_names().iter() {
287                names.push(name.clone());
288            }
289        }
290        names
291    }
292
293    pub fn number_of_params(param_defs: &Vec<ParamGroupWithSet>) -> usize {
294        let mut total_param_count: usize = 0;
295        for p in param_defs.iter() {
296            total_param_count += p.params.len();
297        }
298        return total_param_count;
299    }
300
301    pub fn param_defs_and_args_to_param_to_arg_map(
302        param_defs: &Vec<ParamGroupWithSet>,
303        args: &Vec<Obj>,
304    ) -> HashMap<String, Obj> {
305        let param_names = Self::collect_param_names(param_defs);
306        if param_names.len() != args.len() {
307            unreachable!();
308        }
309
310        let mut result: HashMap<String, Obj> = HashMap::new();
311        let mut index = 0;
312        while index < param_names.len() {
313            let param_name = &param_names[index];
314            let arg = &args[index];
315            result.insert(param_name.clone(), arg.clone());
316            index += 1;
317        }
318        result
319    }
320}
litex/stmt/parameter_def.rs

litex/stmt/
parameter_def.rs
