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    Struct(StructObj),
12}
13
14#[derive(Clone)]
15pub enum StructFieldType {
16    Obj(Obj),
17    Set(Set),
18    FiniteSet(FiniteSet),
19    NonemptySet(NonemptySet),
20}
21
22impl StructFieldType {
23    pub fn to_param_type(&self) -> ParamType {
24        match self {
25            StructFieldType::Obj(o) => ParamType::Obj(o.clone()),
26            StructFieldType::Set(s) => ParamType::Set(s.clone()),
27            StructFieldType::FiniteSet(f) => ParamType::FiniteSet(f.clone()),
28            StructFieldType::NonemptySet(n) => ParamType::NonemptySet(n.clone()),
29        }
30    }
31}
32
33impl fmt::Display for StructFieldType {
34    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
35        write!(f, "{}", self.to_param_type())
36    }
37}
38
39#[derive(Clone)]
40pub struct ParamGroupWithSet {
41    pub params: Vec<String>,
42    pub set: Obj,
43}
44
45#[derive(Clone)]
46pub struct ParamGroupWithParamType {
47    pub params: Vec<String>,
48    pub param_type: ParamType,
49}
50
51#[derive(Clone)]
52pub struct ParamGroupWithStructFieldType {
53    pub params: Vec<String>,
54    pub struct_field_type: StructFieldType,
55}
56
57impl fmt::Display for ParamGroupWithStructFieldType {
58    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
59        write!(
60            f,
61            "{} {}",
62            vec_to_string_join_by_comma(&self.params),
63            self.struct_field_type
64        )
65    }
66}
67
68impl ParamGroupWithStructFieldType {
69    pub fn new(params: Vec<String>, struct_field_type: StructFieldType) -> Self {
70        ParamGroupWithStructFieldType {
71            params,
72            struct_field_type,
73        }
74    }
75
76    pub fn number_of_params(defs: &Vec<ParamGroupWithStructFieldType>) -> usize {
77        let mut total_param_count: usize = 0;
78        for p in defs.iter() {
79            total_param_count += p.params.len();
80        }
81        total_param_count
82    }
83
84    pub fn to_param_group_with_param_type(&self) -> ParamGroupWithParamType {
85        ParamGroupWithParamType::new(self.params.clone(), self.struct_field_type.to_param_type())
86    }
87
88    pub fn to_param_groups_with_param_type(
89        defs: &[ParamGroupWithStructFieldType],
90    ) -> Vec<ParamGroupWithParamType> {
91        defs.iter()
92            .map(|d| d.to_param_group_with_param_type())
93            .collect()
94    }
95
96    pub fn param_names(&self) -> &Vec<String> {
97        &self.params
98    }
99
100    pub fn collect_param_names(param_defs: &Vec<ParamGroupWithStructFieldType>) -> Vec<String> {
101        let mut names: Vec<String> = Vec::with_capacity(Self::number_of_params(param_defs));
102        for def in param_defs.iter() {
103            for name in def.param_names().iter() {
104                names.push(name.clone());
105            }
106        }
107        names
108    }
109
110    pub fn param_defs_and_args_to_param_to_arg_map(
111        param_defs: &Vec<ParamGroupWithStructFieldType>,
112        args: &Vec<Obj>,
113    ) -> HashMap<String, Obj> {
114        let param_names = Self::collect_param_names(param_defs);
115        if param_names.len() != args.len() {
116            unreachable!();
117        }
118
119        let mut result: HashMap<String, Obj> = HashMap::new();
120        let mut index = 0;
121        while index < param_names.len() {
122            let param_name = &param_names[index];
123            let arg = &args[index];
124            result.insert(param_name.clone(), arg.clone());
125            index += 1;
126        }
127        result
128    }
129}
130
131#[derive(Clone)]
132pub struct Set {}
133
134#[derive(Clone)]
135pub struct NonemptySet {}
136
137#[derive(Clone)]
138pub struct FiniteSet {}
139
140impl Set {
141    pub fn new() -> Self {
142        Set {}
143    }
144}
145
146impl NonemptySet {
147    pub fn new() -> Self {
148        NonemptySet {}
149    }
150}
151
152impl FiniteSet {
153    pub fn new() -> Self {
154        FiniteSet {}
155    }
156}
157
158impl fmt::Display for ParamType {
159    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
160        match self {
161            ParamType::Set(set) => write!(f, "{}", set.to_string()),
162            ParamType::NonemptySet(nonempty_set) => write!(f, "{}", nonempty_set.to_string()),
163            ParamType::FiniteSet(finite_set) => write!(f, "{}", finite_set.to_string()),
164            ParamType::Obj(obj) => write!(f, "{}", obj),
165            ParamType::Struct(struct_ty) => write!(f, "{}", struct_ty),
166        }
167    }
168}
169
170impl fmt::Display for Set {
171    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
172        write!(f, "{}", SET)
173    }
174}
175
176impl fmt::Display for NonemptySet {
177    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
178        write!(f, "{}", NONEMPTY_SET)
179    }
180}
181
182impl fmt::Display for FiniteSet {
183    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
184        write!(f, "{}", FINITE_SET)
185    }
186}
187
188impl fmt::Display for ParamGroupWithSet {
189    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
190        write!(
191            f,
192            "{} {}",
193            comma_separated_stored_fn_params_as_user_source(&self.params),
194            self.set
195        )
196    }
197}
198
199impl fmt::Display for ParamGroupWithParamType {
200    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
201        write!(
202            f,
203            "{} {}",
204            vec_to_string_join_by_comma(&self.params),
205            self.param_type
206        )
207    }
208}
209
210impl ParamType {
211    pub fn get_all_param_names(param_def: &Vec<ParamGroupWithParamType>) -> Vec<String> {
212        let mut names = vec![];
213        for param_def in param_def.iter() {
214            for name in param_def.params.iter() {
215                names.push(name.clone());
216            }
217        }
218        names
219    }
220}
221
222impl ParamGroupWithParamType {
223    pub fn new(params: Vec<String>, param_type: ParamType) -> Self {
224        ParamGroupWithParamType { params, param_type }
225    }
226
227    pub fn number_of_params(defs: &Vec<ParamGroupWithParamType>) -> usize {
228        let mut total_param_count: usize = 0;
229        for p in defs.iter() {
230            total_param_count += p.params.len();
231        }
232        return total_param_count;
233    }
234
235    pub fn flat_instantiated_types_for_args(
236        param_defs: &Vec<ParamGroupWithParamType>,
237        instantiated_types: &Vec<ParamType>,
238    ) -> Vec<ParamType> {
239        let mut result = Vec::with_capacity(Self::number_of_params(param_defs));
240        for (param_def, param_type) in param_defs.iter().zip(instantiated_types.iter()) {
241            for _ in param_def.params.iter() {
242                result.push(param_type.clone());
243            }
244        }
245        result
246    }
247
248    pub fn param_names(&self) -> &Vec<String> {
249        &self.params
250    }
251
252    pub fn collect_param_names(param_defs: &Vec<ParamGroupWithParamType>) -> Vec<String> {
253        let mut names: Vec<String> = Vec::with_capacity(Self::number_of_params(param_defs));
254        for def in param_defs.iter() {
255            for name in def.param_names().iter() {
256                names.push(name.clone());
257            }
258        }
259        names
260    }
261
262    pub fn param_def_params_to_arg_map(
263        param_defs: &Vec<ParamGroupWithParamType>,
264        arg_map: &HashMap<String, Obj>,
265    ) -> Option<HashMap<String, Obj>> {
266        let param_names = Self::collect_param_names(param_defs);
267        let mut result = HashMap::new();
268        for param_name in param_names.iter() {
269            let objs_option = arg_map.get(param_name);
270            let objs = match objs_option {
271                Some(v) => v,
272                None => return None,
273            };
274            result.insert(param_name.clone(), objs.clone());
275        }
276        Some(result)
277    }
278
279    pub fn param_defs_and_args_to_param_to_arg_map(
280        param_defs: &Vec<ParamGroupWithParamType>,
281        args: &Vec<Obj>,
282    ) -> HashMap<String, Obj> {
283        let param_names = Self::collect_param_names(param_defs);
284        if param_names.len() != args.len() {
285            unreachable!();
286        }
287
288        let mut result: HashMap<String, Obj> = HashMap::new();
289        let mut index = 0;
290        while index < param_names.len() {
291            let param_name = &param_names[index];
292            let arg = &args[index];
293            result.insert(param_name.clone(), arg.clone());
294            index += 1;
295        }
296        result
297    }
298}
299
300impl ParamGroupWithSet {
301    pub fn new(params: Vec<String>, set: Obj) -> Self {
302        ParamGroupWithSet { params, set }
303    }
304
305    pub fn facts(&self) -> Vec<Fact> {
306        let mut facts = Vec::with_capacity(self.params.len());
307        for name in self.params.iter() {
308            let fact = Fact::AtomicFact(AtomicFact::InFact(InFact::new(
309                Obj::Identifier(Identifier::new(name.clone())),
310                self.set.clone(),
311                default_line_file(),
312            )));
313            facts.push(fact);
314        }
315        facts
316    }
317
318    // 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.
319    // 与 [`ParamGroupWithParamType`] 不同：此处每个参数必须属于**事先确定**的集合（不能用 `set` / `nonempty_set` / `finite_set` 等语法糖），且该集合不能依赖更早的参数。例如 `x R, y f(x)` 不允许。
320    pub fn facts_for_args_satisfy_param_def_with_set_vec(
321        runtime: &Runtime,
322        param_defs: &Vec<ParamGroupWithSet>,
323        args: &Vec<Obj>,
324    ) -> Result<Vec<AtomicFact>, RuntimeError> {
325        let instantiated_param_sets =
326            runtime.inst_param_def_with_set_one_by_one(param_defs, args)?;
327        let flat_param_sets =
328            Self::flat_instantiated_param_sets_for_args(param_defs, &instantiated_param_sets);
329        let mut facts = Vec::with_capacity(args.len());
330        for (arg, param_set) in args.iter().zip(flat_param_sets.iter()) {
331            facts.push(AtomicFact::InFact(InFact::new(
332                arg.clone(),
333                param_set.clone(),
334                default_line_file(),
335            )));
336        }
337        Ok(facts)
338    }
339
340    fn flat_instantiated_param_sets_for_args(
341        param_defs: &Vec<ParamGroupWithSet>,
342        instantiated_param_sets: &Vec<Obj>,
343    ) -> Vec<Obj> {
344        let mut result = Vec::with_capacity(Self::number_of_params(param_defs));
345        for (param_def, param_set) in param_defs.iter().zip(instantiated_param_sets.iter()) {
346            for _ in param_def.params.iter() {
347                result.push(param_set.clone());
348            }
349        }
350        result
351    }
352
353    pub fn param_names(&self) -> &Vec<String> {
354        &self.params
355    }
356
357    pub fn collect_param_names(param_defs: &Vec<ParamGroupWithSet>) -> Vec<String> {
358        let mut names: Vec<String> = Vec::with_capacity(Self::number_of_params(param_defs));
359        for def in param_defs.iter() {
360            for name in def.param_names().iter() {
361                names.push(name.clone());
362            }
363        }
364        names
365    }
366
367    pub fn number_of_params(param_defs: &Vec<ParamGroupWithSet>) -> usize {
368        let mut total_param_count: usize = 0;
369        for p in param_defs.iter() {
370            total_param_count += p.params.len();
371        }
372        return total_param_count;
373    }
374
375    pub fn param_defs_and_args_to_param_to_arg_map(
376        param_defs: &Vec<ParamGroupWithSet>,
377        args: &Vec<Obj>,
378    ) -> HashMap<String, Obj> {
379        let param_names = Self::collect_param_names(param_defs);
380        if param_names.len() != args.len() {
381            unreachable!();
382        }
383
384        let mut result: HashMap<String, Obj> = HashMap::new();
385        let mut index = 0;
386        while index < param_names.len() {
387            let param_name = &param_names[index];
388            let arg = &args[index];
389            result.insert(param_name.clone(), arg.clone());
390            index += 1;
391        }
392        result
393    }
394}
litex/stmt/parameter_def.rs

litex/stmt/
parameter_def.rs
