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

litex/stmt/
parameter_def.rs
