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

litex/stmt/
parameter_def.rs
