litex/stmt/
parameter_def.rs

1use crate::prelude::*;
2use std::collections::HashMap;
3use std::fmt;
4use std::ops::Deref;
5
6#[derive(Clone)]
7pub enum ParamType {
8    Set(Set),
9    NonemptySet(NonemptySet),
10    FiniteSet(FiniteSet),
11    Obj(Obj),
12}
13
14/// Full parameter list with types, e.g. `a, b T, c E` as a sequence of [`ParamGroupWithParamType`].
15#[derive(Clone)]
16pub struct ParamDefWithType {
17    pub groups: Vec<ParamGroupWithParamType>,
18    /// For each parameter group, the flat indices of earlier parameters cited by that group's type.
19    pub param_type_cited_param_indices: Vec<Vec<usize>>,
20}
21
22impl ParamDefWithType {
23    pub fn new(groups: Vec<ParamGroupWithParamType>) -> Self {
24        let param_type_cited_param_indices = cited_param_indices_for_param_type_groups(&groups);
25        ParamDefWithType {
26            groups,
27            param_type_cited_param_indices,
28        }
29    }
30
31    pub fn len(&self) -> usize {
32        self.groups.len()
33    }
34
35    pub fn is_empty(&self) -> bool {
36        self.groups.is_empty()
37    }
38
39    pub fn iter(&self) -> std::slice::Iter<'_, ParamGroupWithParamType> {
40        self.groups.iter()
41    }
42
43    pub fn as_slice(&self) -> &[ParamGroupWithParamType] {
44        self.groups.as_slice()
45    }
46
47    pub fn number_of_params(&self) -> usize {
48        let mut total_param_count: usize = 0;
49        for p in self.groups.iter() {
50            total_param_count += p.params.len();
51        }
52        total_param_count
53    }
54
55    pub fn collect_param_names(&self) -> Vec<String> {
56        let mut names: Vec<String> = Vec::with_capacity(self.number_of_params());
57        for def in self.groups.iter() {
58            for name in def.param_names().iter() {
59                names.push(name.clone());
60            }
61        }
62        names
63    }
64
65    pub fn collect_param_names_with_types(&self) -> Vec<(String, ParamType)> {
66        let mut out: Vec<(String, ParamType)> = Vec::with_capacity(self.number_of_params());
67        for def in self.groups.iter() {
68            for name in def.param_names().iter() {
69                out.push((name.clone(), def.param_type.clone()));
70            }
71        }
72        out
73    }
74
75    pub fn flat_instantiated_types_for_args(
76        &self,
77        instantiated_types: &[ParamType],
78    ) -> Vec<ParamType> {
79        if instantiated_types.len() == self.number_of_params() {
80            return instantiated_types.to_vec();
81        }
82
83        let mut result = Vec::with_capacity(self.number_of_params());
84        for (param_def, param_type) in self.groups.iter().zip(instantiated_types.iter()) {
85            for _ in param_def.params.iter() {
86                result.push(param_type.clone());
87            }
88        }
89        result
90    }
91
92    pub fn param_def_params_to_arg_map(
93        &self,
94        arg_map: &HashMap<String, Obj>,
95    ) -> Option<HashMap<String, Obj>> {
96        let param_names = self.collect_param_names();
97        let mut result = HashMap::new();
98        for param_name in param_names.iter() {
99            let objs_option = arg_map.get(param_name);
100            let objs = match objs_option {
101                Some(v) => v,
102                None => return None,
103            };
104            result.insert(param_name.clone(), objs.clone());
105        }
106        Some(result)
107    }
108
109    pub fn param_defs_and_args_to_param_to_arg_map(&self, args: &[Obj]) -> HashMap<String, Obj> {
110        let param_names = self.collect_param_names();
111        if param_names.len() != args.len() {
112            unreachable!();
113        }
114
115        let mut result: HashMap<String, Obj> = HashMap::new();
116        let mut index = 0;
117        while index < param_names.len() {
118            let param_name = &param_names[index];
119            let arg = &args[index];
120            result.insert(param_name.clone(), arg.clone());
121            index += 1;
122        }
123        result
124    }
125
126    pub fn param_defs_and_boxed_args_to_param_to_arg_map(
127        &self,
128        args: &[Box<Obj>],
129    ) -> HashMap<String, Obj> {
130        let param_names = self.collect_param_names();
131        if param_names.len() != args.len() {
132            unreachable!();
133        }
134
135        let mut result: HashMap<String, Obj> = HashMap::new();
136        let mut index = 0;
137        while index < param_names.len() {
138            let param_name = &param_names[index];
139            let arg = &args[index];
140            result.insert(param_name.clone(), (**arg).clone());
141            index += 1;
142        }
143        result
144    }
145}
146
147impl fmt::Display for ParamDefWithType {
148    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
149        write!(f, "{}", vec_to_string_join_by_comma(&self.groups))
150    }
151}
152
153impl From<Vec<ParamGroupWithParamType>> for ParamDefWithType {
154    fn from(groups: Vec<ParamGroupWithParamType>) -> Self {
155        ParamDefWithType::new(groups)
156    }
157}
158
159/// Full function parameter list with set-valued parameter domains.
160#[derive(Clone)]
161pub struct ParamDefWithSet {
162    pub groups: Vec<ParamGroupWithSet>,
163    /// For each parameter group, the flat indices of earlier parameters cited by that group's set.
164    ///
165    /// Later parameter sets may depend on earlier arguments, e.g.
166    /// `fn(n N_pos, x closed_range(1, n)) R`; function return sets are intentionally outside this
167    /// dependent parameter list and must not cite these parameters.
168    pub param_set_cited_param_indices: Vec<Vec<usize>>,
169}
170
171impl ParamDefWithSet {
172    pub fn new(groups: Vec<ParamGroupWithSet>) -> Self {
173        let param_set_cited_param_indices = cited_param_indices_for_param_set_groups(&groups);
174        ParamDefWithSet {
175            groups,
176            param_set_cited_param_indices,
177        }
178    }
179
180    pub fn len(&self) -> usize {
181        self.groups.len()
182    }
183
184    pub fn is_empty(&self) -> bool {
185        self.groups.is_empty()
186    }
187
188    pub fn iter(&self) -> std::slice::Iter<'_, ParamGroupWithSet> {
189        self.groups.iter()
190    }
191
192    pub fn as_slice(&self) -> &[ParamGroupWithSet] {
193        self.groups.as_slice()
194    }
195
196    pub fn number_of_params(&self) -> usize {
197        ParamGroupWithSet::number_of_params(&self.groups)
198    }
199
200    pub fn collect_param_names(&self) -> Vec<String> {
201        ParamGroupWithSet::collect_param_names(&self.groups)
202    }
203
204    pub fn param_defs_and_args_to_param_to_arg_map(&self, args: &Vec<Obj>) -> HashMap<String, Obj> {
205        ParamGroupWithSet::param_defs_and_args_to_param_to_arg_map(&self.groups, args)
206    }
207
208    pub fn flat_instantiated_param_sets_for_args(
209        &self,
210        instantiated_param_sets: &Vec<Obj>,
211    ) -> Vec<Obj> {
212        let mut result = Vec::with_capacity(self.number_of_params());
213        for (param_def, param_set) in self.groups.iter().zip(instantiated_param_sets.iter()) {
214            for _ in param_def.params.iter() {
215                result.push(param_set.clone());
216            }
217        }
218        result
219    }
220
221    pub fn cited_param_indices_in_obj_from_params(&self, obj: &Obj) -> Vec<usize> {
222        let mut param_indices: HashMap<String, usize> = HashMap::new();
223        let mut flat_index = 0;
224        for group in self.groups.iter() {
225            for param_name in group.params.iter() {
226                param_indices.insert(param_name.clone(), flat_index);
227                flat_index += 1;
228            }
229        }
230        cited_param_indices_in_obj(obj, &param_indices)
231    }
232
233    pub fn has_dependent_param_set(&self) -> bool {
234        self.param_set_cited_param_indices
235            .iter()
236            .any(|indices| !indices.is_empty())
237    }
238
239    pub fn validate_obj_does_not_cite_params(
240        &self,
241        obj: &Obj,
242        context: &str,
243    ) -> Result<(), RuntimeError> {
244        let cited_indices = self.cited_param_indices_in_obj_from_params(obj);
245        if cited_indices.is_empty() {
246            return Ok(());
247        }
248
249        let names = self.collect_param_names();
250        let cited_names: Vec<String> = cited_indices
251            .iter()
252            .filter_map(|index| names.get(*index).cloned())
253            .collect();
254        Err(RuntimeError::from(WellDefinedRuntimeError(
255            RuntimeErrorStruct::new_with_just_msg(format!(
256                "{} cannot depend on function parameters [{}]",
257                context,
258                cited_names.join(", ")
259            )),
260        )))
261    }
262}
263
264impl Deref for ParamDefWithSet {
265    type Target = Vec<ParamGroupWithSet>;
266
267    fn deref(&self) -> &Self::Target {
268        &self.groups
269    }
270}
271
272impl IntoIterator for ParamDefWithSet {
273    type Item = ParamGroupWithSet;
274    type IntoIter = std::vec::IntoIter<ParamGroupWithSet>;
275
276    fn into_iter(self) -> Self::IntoIter {
277        self.groups.into_iter()
278    }
279}
280
281impl<'a> IntoIterator for &'a ParamDefWithSet {
282    type Item = &'a ParamGroupWithSet;
283    type IntoIter = std::slice::Iter<'a, ParamGroupWithSet>;
284
285    fn into_iter(self) -> Self::IntoIter {
286        self.groups.iter()
287    }
288}
289
290impl From<Vec<ParamGroupWithSet>> for ParamDefWithSet {
291    fn from(groups: Vec<ParamGroupWithSet>) -> Self {
292        ParamDefWithSet::new(groups)
293    }
294}
295
296#[derive(Clone)]
297pub struct ParamGroupWithSet {
298    pub params: Vec<String>,
299    pub param_type: Box<Obj>,
300}
301
302#[derive(Clone)]
303pub struct ParamGroupWithParamType {
304    pub params: Vec<String>,
305    pub param_type: ParamType,
306}
307
308#[derive(Clone)]
309pub struct Set {}
310
311#[derive(Clone)]
312pub struct NonemptySet {}
313
314#[derive(Clone)]
315pub struct FiniteSet {}
316
317impl Set {
318    pub fn new() -> Self {
319        Set {}
320    }
321}
322
323impl NonemptySet {
324    pub fn new() -> Self {
325        NonemptySet {}
326    }
327}
328
329impl FiniteSet {
330    pub fn new() -> Self {
331        FiniteSet {}
332    }
333}
334
335impl fmt::Display for ParamType {
336    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
337        match self {
338            ParamType::Set(set) => write!(f, "{}", set.to_string()),
339            ParamType::NonemptySet(nonempty_set) => write!(f, "{}", nonempty_set.to_string()),
340            ParamType::FiniteSet(finite_set) => write!(f, "{}", finite_set.to_string()),
341            ParamType::Obj(obj) => write!(f, "{}", obj),
342        }
343    }
344}
345
346impl fmt::Display for Set {
347    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
348        write!(f, "{}", SET)
349    }
350}
351
352impl fmt::Display for NonemptySet {
353    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
354        write!(f, "{}", NONEMPTY_SET)
355    }
356}
357
358impl fmt::Display for FiniteSet {
359    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
360        write!(f, "{}", FINITE_SET)
361    }
362}
363
364impl fmt::Display for ParamGroupWithSet {
365    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
366        write!(
367            f,
368            "{} {}",
369            comma_separated_stored_fn_params_as_user_source(&self.params),
370            self.param_type
371        )
372    }
373}
374
375impl fmt::Display for ParamGroupWithParamType {
376    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
377        write!(
378            f,
379            "{} {}",
380            vec_to_string_join_by_comma(&self.params),
381            self.param_type
382        )
383    }
384}
385
386impl ParamGroupWithParamType {
387    pub fn new(params: Vec<String>, param_type: ParamType) -> Self {
388        ParamGroupWithParamType { params, param_type }
389    }
390
391    pub fn param_names(&self) -> &Vec<String> {
392        &self.params
393    }
394}
395
396impl ParamGroupWithSet {
397    pub fn new(params: Vec<String>, set: Obj) -> Self {
398        ParamGroupWithSet {
399            params,
400            param_type: Box::new(set),
401        }
402    }
403
404    pub fn set_obj(&self) -> &Obj {
405        self.param_type.as_ref()
406    }
407
408    /// 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).
409    pub fn facts_for_binding_scope(&self, binding_scope: ParamObjType) -> Vec<Fact> {
410        let mut facts = Vec::with_capacity(self.params.len());
411        for name in self.params.iter() {
412            let fact = InFact::new(
413                obj_for_bound_param_in_scope(name.clone(), binding_scope),
414                self.set_obj().clone(),
415                default_line_file(),
416            )
417            .into();
418            facts.push(fact);
419        }
420        facts
421    }
422
423    pub fn facts(&self) -> Vec<Fact> {
424        self.facts_for_binding_scope(ParamObjType::FnSet)
425    }
426
427    // Example: given fn(x R, y Q(x)), 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(1).
428    pub fn facts_for_args_satisfy_param_def_with_set_vec(
429        runtime: &Runtime,
430        param_defs: &ParamDefWithSet,
431        args: &Vec<Obj>,
432        param_obj_type: ParamObjType,
433    ) -> Result<Vec<AtomicFact>, RuntimeError> {
434        let instantiated_param_sets =
435            runtime.inst_param_def_with_set_one_by_one(param_defs, args, param_obj_type)?;
436        let flat_param_sets =
437            param_defs.flat_instantiated_param_sets_for_args(&instantiated_param_sets);
438        let mut facts = Vec::with_capacity(args.len());
439        for (arg, param_set) in args.iter().zip(flat_param_sets.iter()) {
440            facts.push(InFact::new(arg.clone(), param_set.clone(), default_line_file()).into());
441        }
442        Ok(facts)
443    }
444
445    pub fn param_names(&self) -> &Vec<String> {
446        &self.params
447    }
448
449    pub fn collect_param_names(param_defs: &Vec<ParamGroupWithSet>) -> Vec<String> {
450        let mut names: Vec<String> = Vec::with_capacity(Self::number_of_params(param_defs));
451        for def in param_defs.iter() {
452            for name in def.param_names().iter() {
453                names.push(name.clone());
454            }
455        }
456        names
457    }
458
459    pub fn number_of_params(param_defs: &Vec<ParamGroupWithSet>) -> usize {
460        let mut total_param_count: usize = 0;
461        for p in param_defs.iter() {
462            total_param_count += p.params.len();
463        }
464        return total_param_count;
465    }
466
467    pub fn param_defs_and_args_to_param_to_arg_map(
468        param_defs: &Vec<ParamGroupWithSet>,
469        args: &Vec<Obj>,
470    ) -> HashMap<String, Obj> {
471        let param_names = Self::collect_param_names(param_defs);
472        if param_names.len() != args.len() {
473            unreachable!();
474        }
475
476        let mut result: HashMap<String, Obj> = HashMap::new();
477        let mut index = 0;
478        while index < param_names.len() {
479            let param_name = &param_names[index];
480            let arg = &args[index];
481            result.insert(param_name.clone(), arg.clone());
482            index += 1;
483        }
484        result
485    }
486}
487
488fn cited_param_indices_for_param_type_groups(
489    groups: &[ParamGroupWithParamType],
490) -> Vec<Vec<usize>> {
491    let mut previous_param_indices: HashMap<String, usize> = HashMap::new();
492    let mut result = Vec::with_capacity(groups.len());
493    let mut flat_index: usize = 0;
494    for group in groups.iter() {
495        result.push(cited_param_indices_in_param_type(
496            &group.param_type,
497            &previous_param_indices,
498        ));
499        for param_name in group.params.iter() {
500            previous_param_indices.insert(param_name.clone(), flat_index);
501            flat_index += 1;
502        }
503    }
504    result
505}
506
507fn cited_param_indices_for_param_set_groups(groups: &[ParamGroupWithSet]) -> Vec<Vec<usize>> {
508    let mut previous_param_indices: HashMap<String, usize> = HashMap::new();
509    let mut result = Vec::with_capacity(groups.len());
510    let mut flat_index: usize = 0;
511    for group in groups.iter() {
512        result.push(cited_param_indices_in_obj(
513            group.set_obj(),
514            &previous_param_indices,
515        ));
516        for param_name in group.params.iter() {
517            previous_param_indices.insert(param_name.clone(), flat_index);
518            flat_index += 1;
519        }
520    }
521    result
522}
523
524fn cited_param_indices_in_param_type(
525    param_type: &ParamType,
526    previous_param_indices: &HashMap<String, usize>,
527) -> Vec<usize> {
528    match param_type {
529        ParamType::Set(_) | ParamType::NonemptySet(_) | ParamType::FiniteSet(_) => Vec::new(),
530        ParamType::Obj(obj) => cited_param_indices_in_obj(obj, previous_param_indices),
531    }
532}
533
534fn cited_param_indices_in_obj(
535    obj: &Obj,
536    previous_param_indices: &HashMap<String, usize>,
537) -> Vec<usize> {
538    let mut result = Vec::new();
539    let mut shadowed_names = Vec::new();
540    collect_cited_param_indices_from_obj(
541        obj,
542        previous_param_indices,
543        &mut shadowed_names,
544        &mut result,
545    );
546    result
547}
548
549fn collect_cited_param_indices_from_obj(
550    obj: &Obj,
551    previous_param_indices: &HashMap<String, usize>,
552    shadowed_names: &mut Vec<String>,
553    out: &mut Vec<usize>,
554) {
555    match obj {
556        Obj::Atom(atom) => {
557            collect_cited_param_indices_from_atom(atom, previous_param_indices, shadowed_names, out)
558        }
559        Obj::FnObj(fn_obj) => {
560            collect_cited_param_indices_from_fn_head(
561                &fn_obj.head,
562                previous_param_indices,
563                shadowed_names,
564                out,
565            );
566            for group in fn_obj.body.iter() {
567                for arg in group.iter() {
568                    collect_cited_param_indices_from_obj(
569                        arg,
570                        previous_param_indices,
571                        shadowed_names,
572                        out,
573                    );
574                }
575            }
576        }
577        Obj::Number(_) | Obj::StandardSet(_) => {}
578        Obj::Add(x) => collect_cited_param_indices_from_two_objs(
579            &x.left,
580            &x.right,
581            previous_param_indices,
582            shadowed_names,
583            out,
584        ),
585        Obj::Sub(x) => collect_cited_param_indices_from_two_objs(
586            &x.left,
587            &x.right,
588            previous_param_indices,
589            shadowed_names,
590            out,
591        ),
592        Obj::Mul(x) => collect_cited_param_indices_from_two_objs(
593            &x.left,
594            &x.right,
595            previous_param_indices,
596            shadowed_names,
597            out,
598        ),
599        Obj::Div(x) => collect_cited_param_indices_from_two_objs(
600            &x.left,
601            &x.right,
602            previous_param_indices,
603            shadowed_names,
604            out,
605        ),
606        Obj::Mod(x) => collect_cited_param_indices_from_two_objs(
607            &x.left,
608            &x.right,
609            previous_param_indices,
610            shadowed_names,
611            out,
612        ),
613        Obj::Pow(x) => collect_cited_param_indices_from_two_objs(
614            &x.base,
615            &x.exponent,
616            previous_param_indices,
617            shadowed_names,
618            out,
619        ),
620        Obj::Abs(x) => collect_cited_param_indices_from_obj(
621            &x.arg,
622            previous_param_indices,
623            shadowed_names,
624            out,
625        ),
626        Obj::Sqrt(x) => collect_cited_param_indices_from_obj(
627            &x.arg,
628            previous_param_indices,
629            shadowed_names,
630            out,
631        ),
632        Obj::Log(x) => collect_cited_param_indices_from_two_objs(
633            &x.base,
634            &x.arg,
635            previous_param_indices,
636            shadowed_names,
637            out,
638        ),
639        Obj::Max(x) => collect_cited_param_indices_from_two_objs(
640            &x.left,
641            &x.right,
642            previous_param_indices,
643            shadowed_names,
644            out,
645        ),
646        Obj::Min(x) => collect_cited_param_indices_from_two_objs(
647            &x.left,
648            &x.right,
649            previous_param_indices,
650            shadowed_names,
651            out,
652        ),
653        Obj::Union(x) => collect_cited_param_indices_from_two_objs(
654            &x.left,
655            &x.right,
656            previous_param_indices,
657            shadowed_names,
658            out,
659        ),
660        Obj::Intersect(x) => collect_cited_param_indices_from_two_objs(
661            &x.left,
662            &x.right,
663            previous_param_indices,
664            shadowed_names,
665            out,
666        ),
667        Obj::SetMinus(x) => collect_cited_param_indices_from_two_objs(
668            &x.left,
669            &x.right,
670            previous_param_indices,
671            shadowed_names,
672            out,
673        ),
674        Obj::SetDiff(x) => collect_cited_param_indices_from_two_objs(
675            &x.left,
676            &x.right,
677            previous_param_indices,
678            shadowed_names,
679            out,
680        ),
681        Obj::Cup(x) => collect_cited_param_indices_from_obj(
682            &x.left,
683            previous_param_indices,
684            shadowed_names,
685            out,
686        ),
687        Obj::Cap(x) => collect_cited_param_indices_from_obj(
688            &x.left,
689            previous_param_indices,
690            shadowed_names,
691            out,
692        ),
693        Obj::PowerSet(x) => collect_cited_param_indices_from_obj(
694            &x.set,
695            previous_param_indices,
696            shadowed_names,
697            out,
698        ),
699        Obj::ListSet(x) => {
700            for item in x.list.iter() {
701                collect_cited_param_indices_from_obj(
702                    item,
703                    previous_param_indices,
704                    shadowed_names,
705                    out,
706                );
707            }
708        }
709        Obj::SetBuilder(x) => {
710            collect_cited_param_indices_from_obj(
711                &x.param_set,
712                previous_param_indices,
713                shadowed_names,
714                out,
715            );
716            shadowed_names.push(x.param.clone());
717            for fact in x.facts.iter() {
718                collect_cited_param_indices_from_or_and_chain(
719                    fact,
720                    previous_param_indices,
721                    shadowed_names,
722                    out,
723                );
724            }
725            shadowed_names.pop();
726        }
727        Obj::FnSet(x) => collect_cited_param_indices_from_fn_set_body(
728            &x.body,
729            previous_param_indices,
730            shadowed_names,
731            out,
732        ),
733        Obj::AnonymousFn(x) => {
734            collect_cited_param_indices_from_fn_set_body(
735                &x.body,
736                previous_param_indices,
737                shadowed_names,
738                out,
739            );
740            let added = push_param_names_to_shadow(&x.body.params_def_with_set, shadowed_names);
741            collect_cited_param_indices_from_obj(
742                &x.equal_to,
743                previous_param_indices,
744                shadowed_names,
745                out,
746            );
747            pop_shadowed_names(shadowed_names, added);
748        }
749        Obj::Cart(x) => {
750            for arg in x.args.iter() {
751                collect_cited_param_indices_from_obj(
752                    arg,
753                    previous_param_indices,
754                    shadowed_names,
755                    out,
756                );
757            }
758        }
759        Obj::CartDim(x) => collect_cited_param_indices_from_obj(
760            &x.set,
761            previous_param_indices,
762            shadowed_names,
763            out,
764        ),
765        Obj::Proj(x) => collect_cited_param_indices_from_two_objs(
766            &x.set,
767            &x.dim,
768            previous_param_indices,
769            shadowed_names,
770            out,
771        ),
772        Obj::TupleDim(x) => collect_cited_param_indices_from_obj(
773            &x.arg,
774            previous_param_indices,
775            shadowed_names,
776            out,
777        ),
778        Obj::Tuple(x) => {
779            for arg in x.args.iter() {
780                collect_cited_param_indices_from_obj(
781                    arg,
782                    previous_param_indices,
783                    shadowed_names,
784                    out,
785                );
786            }
787        }
788        Obj::Count(x) => collect_cited_param_indices_from_obj(
789            &x.set,
790            previous_param_indices,
791            shadowed_names,
792            out,
793        ),
794        Obj::Sum(x) => {
795            collect_cited_param_indices_from_obj(
796                &x.start,
797                previous_param_indices,
798                shadowed_names,
799                out,
800            );
801            collect_cited_param_indices_from_obj(
802                &x.end,
803                previous_param_indices,
804                shadowed_names,
805                out,
806            );
807            collect_cited_param_indices_from_obj(
808                &x.func,
809                previous_param_indices,
810                shadowed_names,
811                out,
812            );
813        }
814        Obj::Product(x) => {
815            collect_cited_param_indices_from_obj(
816                &x.start,
817                previous_param_indices,
818                shadowed_names,
819                out,
820            );
821            collect_cited_param_indices_from_obj(
822                &x.end,
823                previous_param_indices,
824                shadowed_names,
825                out,
826            );
827            collect_cited_param_indices_from_obj(
828                &x.func,
829                previous_param_indices,
830                shadowed_names,
831                out,
832            );
833        }
834        Obj::Range(x) => collect_cited_param_indices_from_two_objs(
835            &x.start,
836            &x.end,
837            previous_param_indices,
838            shadowed_names,
839            out,
840        ),
841        Obj::ClosedRange(x) => collect_cited_param_indices_from_two_objs(
842            &x.start,
843            &x.end,
844            previous_param_indices,
845            shadowed_names,
846            out,
847        ),
848        Obj::FiniteSeqSet(x) => collect_cited_param_indices_from_two_objs(
849            &x.set,
850            &x.n,
851            previous_param_indices,
852            shadowed_names,
853            out,
854        ),
855        Obj::SeqSet(x) => collect_cited_param_indices_from_obj(
856            &x.set,
857            previous_param_indices,
858            shadowed_names,
859            out,
860        ),
861        Obj::FiniteSeqListObj(x) => {
862            for arg in x.objs.iter() {
863                collect_cited_param_indices_from_obj(
864                    arg,
865                    previous_param_indices,
866                    shadowed_names,
867                    out,
868                );
869            }
870        }
871        Obj::Choose(x) => collect_cited_param_indices_from_obj(
872            &x.set,
873            previous_param_indices,
874            shadowed_names,
875            out,
876        ),
877        Obj::ObjAtIndex(x) => collect_cited_param_indices_from_two_objs(
878            &x.obj,
879            &x.index,
880            previous_param_indices,
881            shadowed_names,
882            out,
883        ),
884        Obj::MatrixSet(x) => {
885            collect_cited_param_indices_from_obj(
886                &x.set,
887                previous_param_indices,
888                shadowed_names,
889                out,
890            );
891            collect_cited_param_indices_from_obj(
892                &x.row_len,
893                previous_param_indices,
894                shadowed_names,
895                out,
896            );
897            collect_cited_param_indices_from_obj(
898                &x.col_len,
899                previous_param_indices,
900                shadowed_names,
901                out,
902            );
903        }
904        Obj::MatrixListObj(x) => {
905            for row in x.rows.iter() {
906                for item in row.iter() {
907                    collect_cited_param_indices_from_obj(
908                        item,
909                        previous_param_indices,
910                        shadowed_names,
911                        out,
912                    );
913                }
914            }
915        }
916        Obj::MatrixAdd(x) => collect_cited_param_indices_from_two_objs(
917            &x.left,
918            &x.right,
919            previous_param_indices,
920            shadowed_names,
921            out,
922        ),
923        Obj::MatrixSub(x) => collect_cited_param_indices_from_two_objs(
924            &x.left,
925            &x.right,
926            previous_param_indices,
927            shadowed_names,
928            out,
929        ),
930        Obj::MatrixMul(x) => collect_cited_param_indices_from_two_objs(
931            &x.left,
932            &x.right,
933            previous_param_indices,
934            shadowed_names,
935            out,
936        ),
937        Obj::MatrixScalarMul(x) => collect_cited_param_indices_from_two_objs(
938            &x.scalar,
939            &x.matrix,
940            previous_param_indices,
941            shadowed_names,
942            out,
943        ),
944        Obj::MatrixPow(x) => collect_cited_param_indices_from_two_objs(
945            &x.base,
946            &x.exponent,
947            previous_param_indices,
948            shadowed_names,
949            out,
950        ),
951        Obj::StructObj(x) => {
952            for arg in x.params.iter() {
953                collect_cited_param_indices_from_obj(
954                    arg,
955                    previous_param_indices,
956                    shadowed_names,
957                    out,
958                );
959            }
960        }
961        Obj::ObjAsStructInstanceWithFieldAccess(x) => {
962            for arg in x.struct_obj.params.iter() {
963                collect_cited_param_indices_from_obj(
964                    arg,
965                    previous_param_indices,
966                    shadowed_names,
967                    out,
968                );
969            }
970            collect_cited_param_indices_from_obj(
971                &x.obj,
972                previous_param_indices,
973                shadowed_names,
974                out,
975            );
976        }
977        Obj::InstantiatedTemplateObj(x) => {
978            for arg in x.args.iter() {
979                collect_cited_param_indices_from_obj(
980                    arg,
981                    previous_param_indices,
982                    shadowed_names,
983                    out,
984                );
985            }
986        }
987    }
988}
989
990fn collect_cited_param_indices_from_two_objs(
991    left: &Obj,
992    right: &Obj,
993    previous_param_indices: &HashMap<String, usize>,
994    shadowed_names: &mut Vec<String>,
995    out: &mut Vec<usize>,
996) {
997    collect_cited_param_indices_from_obj(left, previous_param_indices, shadowed_names, out);
998    collect_cited_param_indices_from_obj(right, previous_param_indices, shadowed_names, out);
999}
1000
1001fn collect_cited_param_indices_from_atom(
1002    atom: &AtomObj,
1003    previous_param_indices: &HashMap<String, usize>,
1004    shadowed_names: &mut Vec<String>,
1005    out: &mut Vec<usize>,
1006) {
1007    match atom {
1008        AtomObj::Identifier(x) => {
1009            push_cited_param_index(&x.name, previous_param_indices, shadowed_names, out)
1010        }
1011        AtomObj::IdentifierWithMod(_) => {}
1012        AtomObj::Forall(x) => {
1013            push_cited_param_index(&x.name, previous_param_indices, shadowed_names, out)
1014        }
1015        AtomObj::Def(x) => {
1016            push_cited_param_index(&x.name, previous_param_indices, shadowed_names, out)
1017        }
1018        AtomObj::Exist(x) => {
1019            push_cited_param_index(&x.name, previous_param_indices, shadowed_names, out)
1020        }
1021        AtomObj::SetBuilder(x) => {
1022            push_cited_param_index(&x.name, previous_param_indices, shadowed_names, out)
1023        }
1024        AtomObj::FnSet(x) => {
1025            push_cited_param_index(&x.name, previous_param_indices, shadowed_names, out)
1026        }
1027        AtomObj::Induc(x) => {
1028            push_cited_param_index(&x.name, previous_param_indices, shadowed_names, out)
1029        }
1030        AtomObj::DefAlgo(x) => {
1031            push_cited_param_index(&x.name, previous_param_indices, shadowed_names, out)
1032        }
1033        AtomObj::DefStructField(x) => {
1034            push_cited_param_index(&x.name, previous_param_indices, shadowed_names, out)
1035        }
1036    }
1037}
1038
1039fn collect_cited_param_indices_from_fn_head(
1040    head: &FnObjHead,
1041    previous_param_indices: &HashMap<String, usize>,
1042    shadowed_names: &mut Vec<String>,
1043    out: &mut Vec<usize>,
1044) {
1045    match head {
1046        FnObjHead::Identifier(x) => {
1047            push_cited_param_index(&x.name, previous_param_indices, shadowed_names, out)
1048        }
1049        FnObjHead::IdentifierWithMod(_) => {}
1050        FnObjHead::Forall(x) => {
1051            push_cited_param_index(&x.name, previous_param_indices, shadowed_names, out)
1052        }
1053        FnObjHead::DefHeader(x) => {
1054            push_cited_param_index(&x.name, previous_param_indices, shadowed_names, out)
1055        }
1056        FnObjHead::Exist(x) => {
1057            push_cited_param_index(&x.name, previous_param_indices, shadowed_names, out)
1058        }
1059        FnObjHead::SetBuilder(x) => {
1060            push_cited_param_index(&x.name, previous_param_indices, shadowed_names, out)
1061        }
1062        FnObjHead::FnSet(x) => {
1063            push_cited_param_index(&x.name, previous_param_indices, shadowed_names, out)
1064        }
1065        FnObjHead::AnonymousFnLiteral(x) => collect_cited_param_indices_from_anonymous_fn(
1066            x,
1067            previous_param_indices,
1068            shadowed_names,
1069            out,
1070        ),
1071        FnObjHead::FiniteSeqListObj(x) => {
1072            for arg in x.objs.iter() {
1073                collect_cited_param_indices_from_obj(
1074                    arg,
1075                    previous_param_indices,
1076                    shadowed_names,
1077                    out,
1078                );
1079            }
1080        }
1081        FnObjHead::Induc(x) => {
1082            push_cited_param_index(&x.name, previous_param_indices, shadowed_names, out)
1083        }
1084        FnObjHead::DefAlgo(x) => {
1085            push_cited_param_index(&x.name, previous_param_indices, shadowed_names, out)
1086        }
1087        FnObjHead::InstantiatedTemplateObj(x) => {
1088            for arg in x.args.iter() {
1089                collect_cited_param_indices_from_obj(
1090                    arg,
1091                    previous_param_indices,
1092                    shadowed_names,
1093                    out,
1094                );
1095            }
1096        }
1097    }
1098}
1099
1100fn collect_cited_param_indices_from_anonymous_fn(
1101    anonymous_fn: &AnonymousFn,
1102    previous_param_indices: &HashMap<String, usize>,
1103    shadowed_names: &mut Vec<String>,
1104    out: &mut Vec<usize>,
1105) {
1106    collect_cited_param_indices_from_fn_set_body(
1107        &anonymous_fn.body,
1108        previous_param_indices,
1109        shadowed_names,
1110        out,
1111    );
1112    let added = push_param_names_to_shadow(&anonymous_fn.body.params_def_with_set, shadowed_names);
1113    collect_cited_param_indices_from_obj(
1114        &anonymous_fn.equal_to,
1115        previous_param_indices,
1116        shadowed_names,
1117        out,
1118    );
1119    pop_shadowed_names(shadowed_names, added);
1120}
1121
1122fn collect_cited_param_indices_from_fn_set_body(
1123    body: &FnSetBody,
1124    previous_param_indices: &HashMap<String, usize>,
1125    shadowed_names: &mut Vec<String>,
1126    out: &mut Vec<usize>,
1127) {
1128    let original_shadow_len = shadowed_names.len();
1129    for group in body.params_def_with_set.iter() {
1130        collect_cited_param_indices_from_obj(
1131            group.set_obj(),
1132            previous_param_indices,
1133            shadowed_names,
1134            out,
1135        );
1136        for param_name in group.params.iter() {
1137            shadowed_names.push(param_name.clone());
1138        }
1139    }
1140    for fact in body.dom_facts.iter() {
1141        collect_cited_param_indices_from_or_and_chain(
1142            fact,
1143            previous_param_indices,
1144            shadowed_names,
1145            out,
1146        );
1147    }
1148    collect_cited_param_indices_from_obj(
1149        &body.ret_set,
1150        previous_param_indices,
1151        shadowed_names,
1152        out,
1153    );
1154    while shadowed_names.len() > original_shadow_len {
1155        shadowed_names.pop();
1156    }
1157}
1158
1159fn collect_cited_param_indices_from_or_and_chain(
1160    fact: &OrAndChainAtomicFact,
1161    previous_param_indices: &HashMap<String, usize>,
1162    shadowed_names: &mut Vec<String>,
1163    out: &mut Vec<usize>,
1164) {
1165    for arg in fact.get_args_from_fact().iter() {
1166        collect_cited_param_indices_from_obj(arg, previous_param_indices, shadowed_names, out);
1167    }
1168}
1169
1170fn push_param_names_to_shadow(
1171    param_defs: &ParamDefWithSet,
1172    shadowed_names: &mut Vec<String>,
1173) -> usize {
1174    let mut count = 0;
1175    for group in param_defs.iter() {
1176        for param_name in group.params.iter() {
1177            shadowed_names.push(param_name.clone());
1178            count += 1;
1179        }
1180    }
1181    count
1182}
1183
1184fn pop_shadowed_names(shadowed_names: &mut Vec<String>, count: usize) {
1185    for _ in 0..count {
1186        shadowed_names.pop();
1187    }
1188}
1189
1190fn push_cited_param_index(
1191    name: &str,
1192    previous_param_indices: &HashMap<String, usize>,
1193    shadowed_names: &Vec<String>,
1194    out: &mut Vec<usize>,
1195) {
1196    if shadowed_names
1197        .iter()
1198        .any(|shadowed_name| shadowed_name == name)
1199    {
1200        return;
1201    }
1202    if let Some(index) = previous_param_indices.get(name) {
1203        if !out.contains(index) {
1204            out.push(*index);
1205        }
1206    }
1207}
1208
1209#[cfg(test)]
1210mod tests {
1211    use super::*;
1212
1213    #[test]
1214    fn param_def_with_type_records_flat_cited_param_indices() {
1215        let cited_type = Tuple::new(vec![
1216            ForallFreeParamObj::new("a".to_string()).into(),
1217            ForallFreeParamObj::new("b".to_string()).into(),
1218        ])
1219        .into();
1220        let param_def = ParamDefWithType::new(vec![
1221            ParamGroupWithParamType::new(
1222                vec!["a".to_string(), "b".to_string()],
1223                ParamType::Set(Set::new()),
1224            ),
1225            ParamGroupWithParamType::new(vec!["f".to_string()], ParamType::Obj(cited_type)),
1226        ]);
1227
1228        assert_eq!(
1229            param_def.param_type_cited_param_indices[0],
1230            Vec::<usize>::new()
1231        );
1232        assert_eq!(param_def.param_type_cited_param_indices[1], vec![0, 1]);
1233    }
1234
1235    #[test]
1236    fn param_def_with_set_records_flat_cited_param_indices() {
1237        let dependent_set = ClosedRange::new(
1238            Number::new("1".to_string()).into(),
1239            FnSetFreeParamObj::new("n".to_string()).into(),
1240        )
1241        .into();
1242        let param_def = ParamDefWithSet::new(vec![
1243            ParamGroupWithSet::new(vec!["n".to_string()], StandardSet::NPos.into()),
1244            ParamGroupWithSet::new(vec!["x".to_string()], dependent_set),
1245        ]);
1246
1247        assert_eq!(
1248            param_def.param_set_cited_param_indices[0],
1249            Vec::<usize>::new()
1250        );
1251        assert_eq!(param_def.param_set_cited_param_indices[1], vec![0]);
1252    }
1253
1254    #[test]
1255    fn dependent_param_set_instantiates_with_previous_arg() {
1256        let dependent_set = ClosedRange::new(
1257            Number::new("1".to_string()).into(),
1258            FnSetFreeParamObj::new("n".to_string()).into(),
1259        )
1260        .into();
1261        let param_def = ParamDefWithSet::new(vec![
1262            ParamGroupWithSet::new(vec!["n".to_string()], StandardSet::NPos.into()),
1263            ParamGroupWithSet::new(vec!["x".to_string()], dependent_set),
1264        ]);
1265        let args = vec![
1266            Number::new("3".to_string()).into(),
1267            Number::new("2".to_string()).into(),
1268        ];
1269        let runtime = Runtime::new();
1270
1271        let instantiated = runtime
1272            .inst_param_def_with_set_one_by_one(&param_def, &args, ParamObjType::FnSet)
1273            .unwrap();
1274
1275        assert_eq!(instantiated[1].to_string(), "closed_range(1, 3)");
1276    }
1277}
litex/stmt/parameter_def.rs

litex/stmt/
parameter_def.rs
