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(StructAsParamType),
12}
13
14#[derive(Clone)]
15pub struct StructAsParamType {
16    pub name: NameOrNameWithMod,
17    pub args: Vec<Box<Obj>>,
18}
19
20#[derive(Clone)]
21pub enum NameOrNameWithMod {
22    Name(String),
23    NameWithMod(String, String),
24}
25
26impl StructAsParamType {
27    pub fn new(name: NameOrNameWithMod, args: Vec<Obj>) -> Self {
28        let args = args.into_iter().map(Box::new).collect();
29        StructAsParamType { name, args }
30    }
31
32    pub fn new_with_boxed_args(name: NameOrNameWithMod, args: Vec<Box<Obj>>) -> Self {
33        StructAsParamType { name, args }
34    }
35
36    pub fn struct_name(&self) -> String {
37        self.name.to_string()
38    }
39}
40
41impl NameOrNameWithMod {
42    pub fn new_name(name: String) -> Self {
43        NameOrNameWithMod::Name(name)
44    }
45
46    pub fn new_name_with_mod(mod_name: String, name: String) -> Self {
47        NameOrNameWithMod::NameWithMod(mod_name, name)
48    }
49}
50
51impl fmt::Display for StructAsParamType {
52    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
53        if self.args.is_empty() {
54            write!(f, "{} {}", STRUCT, self.name)
55        } else {
56            write!(
57                f,
58                "{} {}{}{}{}",
59                STRUCT,
60                self.name,
61                LEFT_BRACE,
62                vec_to_string_join_by_comma(&self.args),
63                RIGHT_BRACE
64            )
65        }
66    }
67}
68
69impl fmt::Display for NameOrNameWithMod {
70    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
71        match self {
72            NameOrNameWithMod::Name(name) => write!(f, "{}", name),
73            NameOrNameWithMod::NameWithMod(mod_name, name) => {
74                write!(f, "{}{}{}", mod_name, MOD_SIGN, name)
75            }
76        }
77    }
78}
79
80/// Full parameter list with types, e.g. `a, b T, c E` as a sequence of [`ParamGroupWithParamType`].
81#[derive(Clone)]
82pub struct ParamDefWithType {
83    pub groups: Vec<ParamGroupWithParamType>,
84}
85
86impl ParamDefWithType {
87    pub fn new(groups: Vec<ParamGroupWithParamType>) -> Self {
88        ParamDefWithType { groups }
89    }
90
91    pub fn len(&self) -> usize {
92        self.groups.len()
93    }
94
95    pub fn is_empty(&self) -> bool {
96        self.groups.is_empty()
97    }
98
99    pub fn iter(&self) -> std::slice::Iter<'_, ParamGroupWithParamType> {
100        self.groups.iter()
101    }
102
103    pub fn as_slice(&self) -> &[ParamGroupWithParamType] {
104        self.groups.as_slice()
105    }
106
107    pub fn number_of_params(&self) -> usize {
108        let mut total_param_count: usize = 0;
109        for p in self.groups.iter() {
110            total_param_count += p.params.len();
111        }
112        total_param_count
113    }
114
115    pub fn collect_param_names(&self) -> Vec<String> {
116        let mut names: Vec<String> = Vec::with_capacity(self.number_of_params());
117        for def in self.groups.iter() {
118            for name in def.param_names().iter() {
119                names.push(name.clone());
120            }
121        }
122        names
123    }
124
125    pub fn collect_param_names_with_types(&self) -> Vec<(String, ParamType)> {
126        let mut out: Vec<(String, ParamType)> = Vec::with_capacity(self.number_of_params());
127        for def in self.groups.iter() {
128            for name in def.param_names().iter() {
129                out.push((name.clone(), def.param_type.clone()));
130            }
131        }
132        out
133    }
134
135    pub fn flat_instantiated_types_for_args(
136        &self,
137        instantiated_types: &[ParamType],
138    ) -> Vec<ParamType> {
139        let mut result = Vec::with_capacity(self.number_of_params());
140        for (param_def, param_type) in self.groups.iter().zip(instantiated_types.iter()) {
141            for _ in param_def.params.iter() {
142                result.push(param_type.clone());
143            }
144        }
145        result
146    }
147
148    pub fn param_def_params_to_arg_map(
149        &self,
150        arg_map: &HashMap<String, Obj>,
151    ) -> Option<HashMap<String, Obj>> {
152        let param_names = self.collect_param_names();
153        let mut result = HashMap::new();
154        for param_name in param_names.iter() {
155            let objs_option = arg_map.get(param_name);
156            let objs = match objs_option {
157                Some(v) => v,
158                None => return None,
159            };
160            result.insert(param_name.clone(), objs.clone());
161        }
162        Some(result)
163    }
164
165    pub fn param_defs_and_args_to_param_to_arg_map(&self, args: &[Obj]) -> HashMap<String, Obj> {
166        let param_names = self.collect_param_names();
167        if param_names.len() != args.len() {
168            unreachable!();
169        }
170
171        let mut result: HashMap<String, Obj> = HashMap::new();
172        let mut index = 0;
173        while index < param_names.len() {
174            let param_name = &param_names[index];
175            let arg = &args[index];
176            result.insert(param_name.clone(), arg.clone());
177            index += 1;
178        }
179        result
180    }
181
182    pub fn param_defs_and_boxed_args_to_param_to_arg_map(
183        &self,
184        args: &[Box<Obj>],
185    ) -> HashMap<String, Obj> {
186        let param_names = self.collect_param_names();
187        if param_names.len() != args.len() {
188            unreachable!();
189        }
190
191        let mut result: HashMap<String, Obj> = HashMap::new();
192        let mut index = 0;
193        while index < param_names.len() {
194            let param_name = &param_names[index];
195            let arg = &args[index];
196            result.insert(param_name.clone(), (**arg).clone());
197            index += 1;
198        }
199        result
200    }
201}
202
203impl fmt::Display for ParamDefWithType {
204    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
205        write!(f, "{}", vec_to_string_join_by_comma(&self.groups))
206    }
207}
208
209impl From<Vec<ParamGroupWithParamType>> for ParamDefWithType {
210    fn from(groups: Vec<ParamGroupWithParamType>) -> Self {
211        ParamDefWithType::new(groups)
212    }
213}
214
215#[derive(Clone)]
216pub struct ParamGroupWithSet {
217    pub params: Vec<String>,
218    pub param_type: ParamGroupWithSetTypeEnum,
219}
220
221#[derive(Clone)]
222pub enum ParamGroupWithSetTypeEnum {
223    Set(Obj),
224    Struct(StructAsParamType),
225}
226
227#[derive(Clone)]
228pub struct ParamGroupWithParamType {
229    pub params: Vec<String>,
230    pub param_type: ParamType,
231}
232
233#[derive(Clone)]
234pub struct Set {}
235
236#[derive(Clone)]
237pub struct NonemptySet {}
238
239#[derive(Clone)]
240pub struct FiniteSet {}
241
242impl Set {
243    pub fn new() -> Self {
244        Set {}
245    }
246}
247
248impl NonemptySet {
249    pub fn new() -> Self {
250        NonemptySet {}
251    }
252}
253
254impl FiniteSet {
255    pub fn new() -> Self {
256        FiniteSet {}
257    }
258}
259
260impl fmt::Display for ParamType {
261    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
262        match self {
263            ParamType::Set(set) => write!(f, "{}", set.to_string()),
264            ParamType::NonemptySet(nonempty_set) => write!(f, "{}", nonempty_set.to_string()),
265            ParamType::FiniteSet(finite_set) => write!(f, "{}", finite_set.to_string()),
266            ParamType::Obj(obj) => write!(f, "{}", obj),
267            ParamType::Struct(struct_ty) => write!(f, "{}", struct_ty),
268        }
269    }
270}
271
272impl fmt::Display for Set {
273    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
274        write!(f, "{}", SET)
275    }
276}
277
278impl fmt::Display for NonemptySet {
279    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
280        write!(f, "{}", NONEMPTY_SET)
281    }
282}
283
284impl fmt::Display for FiniteSet {
285    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
286        write!(f, "{}", FINITE_SET)
287    }
288}
289
290impl fmt::Display for ParamGroupWithSet {
291    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
292        let param_type = match &self.param_type {
293            ParamGroupWithSetTypeEnum::Set(set) => set.to_string(),
294            ParamGroupWithSetTypeEnum::Struct(struct_ty) => struct_ty.to_string(),
295        };
296        write!(
297            f,
298            "{} {}",
299            comma_separated_stored_fn_params_as_user_source(&self.params),
300            param_type
301        )
302    }
303}
304
305impl fmt::Display for ParamGroupWithParamType {
306    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
307        write!(
308            f,
309            "{} {}",
310            vec_to_string_join_by_comma(&self.params),
311            self.param_type
312        )
313    }
314}
315
316impl ParamGroupWithParamType {
317    pub fn new(params: Vec<String>, param_type: ParamType) -> Self {
318        ParamGroupWithParamType { params, param_type }
319    }
320
321    pub fn param_names(&self) -> &Vec<String> {
322        &self.params
323    }
324}
325
326impl ParamGroupWithSet {
327    pub fn new(params: Vec<String>, set: Obj) -> Self {
328        ParamGroupWithSet {
329            params,
330            param_type: ParamGroupWithSetTypeEnum::Set(set),
331        }
332    }
333
334    pub fn new_struct(params: Vec<String>, struct_ty: StructAsParamType) -> Self {
335        ParamGroupWithSet {
336            params,
337            param_type: ParamGroupWithSetTypeEnum::Struct(struct_ty),
338        }
339    }
340
341    pub fn set_obj(&self) -> Option<&Obj> {
342        match &self.param_type {
343            ParamGroupWithSetTypeEnum::Set(set) => Some(set),
344            ParamGroupWithSetTypeEnum::Struct(_) => None,
345        }
346    }
347
348    pub fn struct_ty(&self) -> Option<&StructAsParamType> {
349        match &self.param_type {
350            ParamGroupWithSetTypeEnum::Set(_) => None,
351            ParamGroupWithSetTypeEnum::Struct(struct_ty) => Some(struct_ty),
352        }
353    }
354
355    /// 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).
356    pub fn facts_for_binding_scope(&self, binding_scope: ParamObjType) -> Vec<Fact> {
357        let Some(set) = self.set_obj() else {
358            return vec![];
359        };
360        let mut facts = Vec::with_capacity(self.params.len());
361        for name in self.params.iter() {
362            let fact = InFact::new(
363                obj_for_bound_param_in_scope(name.clone(), binding_scope),
364                set.clone(),
365                default_line_file(),
366            )
367            .into();
368            facts.push(fact);
369        }
370        facts
371    }
372
373    pub fn facts(&self) -> Vec<Fact> {
374        self.facts_for_binding_scope(ParamObjType::FnSet)
375    }
376
377    // 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.
378    // 与 [`ParamGroupWithParamType`] 不同：此处每个参数必须属于**事先确定**的集合（不能用 `set` / `nonempty_set` / `finite_set` 等语法糖），且该集合不能依赖更早的参数。例如 `x R, y f(x)` 不允许。
379    pub fn facts_for_args_satisfy_param_def_with_set_vec(
380        runtime: &Runtime,
381        param_defs: &Vec<ParamGroupWithSet>,
382        args: &Vec<Obj>,
383        param_obj_type: ParamObjType,
384    ) -> Result<Vec<AtomicFact>, RuntimeError> {
385        for param_def in param_defs.iter() {
386            if param_def.struct_ty().is_some() {
387                return Err(RuntimeError::from(VerifyRuntimeError(
388                    RuntimeErrorStruct::new_with_just_msg(
389                        "struct fn parameter must be checked as a struct parameter, not as `$in`"
390                            .to_string(),
391                    ),
392                )));
393            }
394        }
395        let instantiated_param_sets =
396            runtime.inst_param_def_with_set_one_by_one(param_defs, args, param_obj_type)?;
397        let flat_param_sets =
398            Self::flat_instantiated_param_sets_for_args(param_defs, &instantiated_param_sets);
399        let mut facts = Vec::with_capacity(args.len());
400        for (arg, param_set) in args.iter().zip(flat_param_sets.iter()) {
401            facts.push(InFact::new(arg.clone(), param_set.clone(), default_line_file()).into());
402        }
403        Ok(facts)
404    }
405
406    fn flat_instantiated_param_sets_for_args(
407        param_defs: &Vec<ParamGroupWithSet>,
408        instantiated_param_sets: &Vec<Obj>,
409    ) -> Vec<Obj> {
410        let mut result = Vec::with_capacity(Self::number_of_params(param_defs));
411        for (param_def, param_set) in param_defs.iter().zip(instantiated_param_sets.iter()) {
412            for _ in param_def.params.iter() {
413                result.push(param_set.clone());
414            }
415        }
416        result
417    }
418
419    pub fn param_names(&self) -> &Vec<String> {
420        &self.params
421    }
422
423    pub fn collect_param_names(param_defs: &Vec<ParamGroupWithSet>) -> Vec<String> {
424        let mut names: Vec<String> = Vec::with_capacity(Self::number_of_params(param_defs));
425        for def in param_defs.iter() {
426            for name in def.param_names().iter() {
427                names.push(name.clone());
428            }
429        }
430        names
431    }
432
433    pub fn number_of_params(param_defs: &Vec<ParamGroupWithSet>) -> usize {
434        let mut total_param_count: usize = 0;
435        for p in param_defs.iter() {
436            total_param_count += p.params.len();
437        }
438        return total_param_count;
439    }
440
441    pub fn param_defs_and_args_to_param_to_arg_map(
442        param_defs: &Vec<ParamGroupWithSet>,
443        args: &Vec<Obj>,
444    ) -> HashMap<String, Obj> {
445        let param_names = Self::collect_param_names(param_defs);
446        if param_names.len() != args.len() {
447            unreachable!();
448        }
449
450        let mut result: HashMap<String, Obj> = HashMap::new();
451        let mut index = 0;
452        while index < param_names.len() {
453            let param_name = &param_names[index];
454            let arg = &args[index];
455            result.insert(param_name.clone(), arg.clone());
456            index += 1;
457        }
458        result
459    }
460}
litex/stmt/parameter_def.rs

litex/stmt/
parameter_def.rs
