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    pub fn param_defs_and_boxed_args_to_param_to_arg_map(
116        &self,
117        args: &[Box<Obj>],
118    ) -> HashMap<String, Obj> {
119        let param_names = self.collect_param_names();
120        if param_names.len() != args.len() {
121            unreachable!();
122        }
123
124        let mut result: HashMap<String, Obj> = HashMap::new();
125        let mut index = 0;
126        while index < param_names.len() {
127            let param_name = &param_names[index];
128            let arg = &args[index];
129            result.insert(param_name.clone(), (**arg).clone());
130            index += 1;
131        }
132        result
133    }
134}
135
136impl fmt::Display for ParamDefWithType {
137    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
138        write!(f, "{}", vec_to_string_join_by_comma(&self.groups))
139    }
140}
141
142impl From<Vec<ParamGroupWithParamType>> for ParamDefWithType {
143    fn from(groups: Vec<ParamGroupWithParamType>) -> Self {
144        ParamDefWithType::new(groups)
145    }
146}
147
148#[derive(Clone)]
149pub struct ParamGroupWithSet {
150    pub params: Vec<String>,
151    pub param_type: Box<Obj>,
152}
153
154#[derive(Clone)]
155pub struct ParamGroupWithParamType {
156    pub params: Vec<String>,
157    pub param_type: ParamType,
158}
159
160#[derive(Clone)]
161pub struct Set {}
162
163#[derive(Clone)]
164pub struct NonemptySet {}
165
166#[derive(Clone)]
167pub struct FiniteSet {}
168
169impl Set {
170    pub fn new() -> Self {
171        Set {}
172    }
173}
174
175impl NonemptySet {
176    pub fn new() -> Self {
177        NonemptySet {}
178    }
179}
180
181impl FiniteSet {
182    pub fn new() -> Self {
183        FiniteSet {}
184    }
185}
186
187impl fmt::Display for ParamType {
188    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
189        match self {
190            ParamType::Set(set) => write!(f, "{}", set.to_string()),
191            ParamType::NonemptySet(nonempty_set) => write!(f, "{}", nonempty_set.to_string()),
192            ParamType::FiniteSet(finite_set) => write!(f, "{}", finite_set.to_string()),
193            ParamType::Obj(obj) => write!(f, "{}", obj),
194        }
195    }
196}
197
198impl fmt::Display for Set {
199    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
200        write!(f, "{}", SET)
201    }
202}
203
204impl fmt::Display for NonemptySet {
205    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
206        write!(f, "{}", NONEMPTY_SET)
207    }
208}
209
210impl fmt::Display for FiniteSet {
211    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
212        write!(f, "{}", FINITE_SET)
213    }
214}
215
216impl fmt::Display for ParamGroupWithSet {
217    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
218        write!(
219            f,
220            "{} {}",
221            comma_separated_stored_fn_params_as_user_source(&self.params),
222            self.param_type
223        )
224    }
225}
226
227impl fmt::Display for ParamGroupWithParamType {
228    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
229        write!(
230            f,
231            "{} {}",
232            vec_to_string_join_by_comma(&self.params),
233            self.param_type
234        )
235    }
236}
237
238impl ParamGroupWithParamType {
239    pub fn new(params: Vec<String>, param_type: ParamType) -> Self {
240        ParamGroupWithParamType { params, param_type }
241    }
242
243    pub fn param_names(&self) -> &Vec<String> {
244        &self.params
245    }
246}
247
248impl ParamGroupWithSet {
249    pub fn new(params: Vec<String>, set: Obj) -> Self {
250        ParamGroupWithSet {
251            params,
252            param_type: Box::new(set),
253        }
254    }
255
256    pub fn set_obj(&self) -> &Obj {
257        self.param_type.as_ref()
258    }
259
260    /// Membership facts for parameters; element tagging must match [`define_params_with_set_in_scope`]'s `binding_scope` (e.g. `FnSet` ~5 for `fn` and `'` anonymous heads).
261    pub fn facts_for_binding_scope(&self, binding_scope: ParamObjType) -> Vec<Fact> {
262        let mut facts = Vec::with_capacity(self.params.len());
263        for name in self.params.iter() {
264            let fact = InFact::new(
265                obj_for_bound_param_in_scope(name.clone(), binding_scope),
266                self.set_obj().clone(),
267                default_line_file(),
268            )
269            .into();
270            facts.push(fact);
271        }
272        facts
273    }
274
275    pub fn facts(&self) -> Vec<Fact> {
276        self.facts_for_binding_scope(ParamObjType::FnSet)
277    }
278
279    // 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.
280    // 与 [`ParamGroupWithParamType`] 不同：此处每个参数必须属于**事先确定**的集合（不能用 `set` / `nonempty_set` / `finite_set` 等语法糖），且该集合不能依赖更早的参数。例如 `x R, y f(x)` 不允许。
281    pub fn facts_for_args_satisfy_param_def_with_set_vec(
282        runtime: &Runtime,
283        param_defs: &Vec<ParamGroupWithSet>,
284        args: &Vec<Obj>,
285        param_obj_type: ParamObjType,
286    ) -> Result<Vec<AtomicFact>, RuntimeError> {
287        let instantiated_param_sets =
288            runtime.inst_param_def_with_set_one_by_one(param_defs, args, param_obj_type)?;
289        let flat_param_sets =
290            Self::flat_instantiated_param_sets_for_args(param_defs, &instantiated_param_sets);
291        let mut facts = Vec::with_capacity(args.len());
292        for (arg, param_set) in args.iter().zip(flat_param_sets.iter()) {
293            facts.push(InFact::new(arg.clone(), param_set.clone(), default_line_file()).into());
294        }
295        Ok(facts)
296    }
297
298    fn flat_instantiated_param_sets_for_args(
299        param_defs: &Vec<ParamGroupWithSet>,
300        instantiated_param_sets: &Vec<Obj>,
301    ) -> Vec<Obj> {
302        let mut result = Vec::with_capacity(Self::number_of_params(param_defs));
303        for (param_def, param_set) in param_defs.iter().zip(instantiated_param_sets.iter()) {
304            for _ in param_def.params.iter() {
305                result.push(param_set.clone());
306            }
307        }
308        result
309    }
310
311    pub fn param_names(&self) -> &Vec<String> {
312        &self.params
313    }
314
315    pub fn collect_param_names(param_defs: &Vec<ParamGroupWithSet>) -> Vec<String> {
316        let mut names: Vec<String> = Vec::with_capacity(Self::number_of_params(param_defs));
317        for def in param_defs.iter() {
318            for name in def.param_names().iter() {
319                names.push(name.clone());
320            }
321        }
322        names
323    }
324
325    pub fn number_of_params(param_defs: &Vec<ParamGroupWithSet>) -> usize {
326        let mut total_param_count: usize = 0;
327        for p in param_defs.iter() {
328            total_param_count += p.params.len();
329        }
330        return total_param_count;
331    }
332
333    pub fn param_defs_and_args_to_param_to_arg_map(
334        param_defs: &Vec<ParamGroupWithSet>,
335        args: &Vec<Obj>,
336    ) -> HashMap<String, Obj> {
337        let param_names = Self::collect_param_names(param_defs);
338        if param_names.len() != args.len() {
339            unreachable!();
340        }
341
342        let mut result: HashMap<String, Obj> = HashMap::new();
343        let mut index = 0;
344        while index < param_names.len() {
345            let param_name = &param_names[index];
346            let arg = &args[index];
347            result.insert(param_name.clone(), arg.clone());
348            index += 1;
349        }
350        result
351    }
352}
litex/stmt/parameter_def.rs

litex/stmt/
parameter_def.rs
