litex/obj/
free_param_obj.rs

1use crate::prelude::*;
2use std::fmt;
3
4#[derive(Clone, Copy, Debug, PartialEq, Eq)]
5pub enum ParamObjType {
6    Identifier,
7    Forall,
8    DefHeader,
9    Exist,
10    SetBuilder,
11    FnSet,
12    /// Summation index in `sum(i, lo, hi, body)` — bound only in `body`.
13    Sum,
14    Induc,
15    DefAlgo,
16    /// Product index in `product(i, lo, hi, body)` — bound only in `body`.
17    Product,
18}
19
20impl ParamObjType {
21    pub fn free_param_display_tag(self) -> u8 {
22        match self {
23            ParamObjType::Identifier => 0,
24            ParamObjType::Forall => 1,
25            ParamObjType::DefHeader => 2,
26            ParamObjType::Exist => 3,
27            ParamObjType::SetBuilder => 4,
28            ParamObjType::FnSet => 5,
29            ParamObjType::Sum => 6,
30            ParamObjType::Induc => 7,
31            ParamObjType::DefAlgo => 8,
32            ParamObjType::Product => 9,
33        }
34    }
35}
36
37pub type ToInstWhatKindOfParam = ParamObjType;
38const FREE_PARAM_DISPLAY_TAG_PREFIX: char = '~';
39
40fn write_parsing_free_param_tagged_spine(
41    f: &mut fmt::Formatter<'_>,
42    kind: ParamObjType,
43    spine: &str,
44) -> fmt::Result {
45    write!(
46        f,
47        "{}{}{}",
48        FREE_PARAM_DISPLAY_TAG_PREFIX,
49        kind.free_param_display_tag(),
50        spine
51    )
52}
53
54pub fn strip_parsing_free_param_tags_for_user_display(text: &str) -> String {
55    let mut out = String::with_capacity(text.len());
56    let mut it = text.chars().peekable();
57    while let Some(c) = it.next() {
58        if c == FREE_PARAM_DISPLAY_TAG_PREFIX {
59            while it.peek().map(|x| x.is_ascii_digit()).unwrap_or(false) {
60                it.next();
61            }
62        } else {
63            out.push(c);
64        }
65    }
66    out
67}
68
69/// Removes `~` plus following ASCII digits everywhere (e.g. `~2aaa` → `aaa`). Used on full
70/// display JSON so every field is normalized; keeps `~` when not followed by digits (e.g. `~/`).
71pub fn strip_free_param_numeric_tags_in_display(text: &str) -> String {
72    let mut out = String::with_capacity(text.len());
73    let mut it = text.chars().peekable();
74    while let Some(c) = it.next() {
75        if c == FREE_PARAM_DISPLAY_TAG_PREFIX {
76            if it.peek().map(|x| x.is_ascii_digit()).unwrap_or(false) {
77                while it.peek().map(|x| x.is_ascii_digit()).unwrap_or(false) {
78                    it.next();
79                }
80            } else {
81                out.push(c);
82            }
83        } else {
84            out.push(c);
85        }
86    }
87    out
88}
89
90#[derive(Clone, Debug, PartialEq, Eq)]
91pub struct ForallFreeParamObj {
92    pub name: String,
93}
94
95#[derive(Clone, Debug, PartialEq, Eq)]
96pub struct DefHeaderFreeParamObj {
97    pub name: String,
98}
99
100#[derive(Clone, Debug, PartialEq, Eq)]
101pub struct ExistFreeParamObj {
102    pub name: String,
103}
104
105#[derive(Clone, Debug, PartialEq, Eq)]
106pub struct SetBuilderFreeParamObj {
107    pub name: String,
108}
109
110#[derive(Clone, Debug, PartialEq, Eq)]
111pub struct FnSetFreeParamObj {
112    pub name: String,
113}
114
115#[derive(Clone, Debug, PartialEq, Eq)]
116pub struct SumFreeParamObj {
117    pub name: String,
118}
119
120#[derive(Clone, Debug, PartialEq, Eq)]
121pub struct ProductFreeParamObj {
122    pub name: String,
123}
124
125#[derive(Clone, Debug, PartialEq, Eq)]
126pub struct ByInducFreeParamObj {
127    pub name: String,
128}
129
130#[derive(Clone, Debug, PartialEq, Eq)]
131pub struct DefAlgoFreeParamObj {
132    pub name: String,
133}
134
135impl ForallFreeParamObj {
136    pub fn new(name: String) -> Self {
137        ForallFreeParamObj { name }
138    }
139}
140
141impl DefHeaderFreeParamObj {
142    pub fn new(name: String) -> Self {
143        DefHeaderFreeParamObj { name }
144    }
145}
146
147impl ExistFreeParamObj {
148    pub fn new(name: String) -> Self {
149        ExistFreeParamObj { name }
150    }
151}
152
153impl SetBuilderFreeParamObj {
154    pub fn new(name: String) -> Self {
155        SetBuilderFreeParamObj { name }
156    }
157}
158
159impl FnSetFreeParamObj {
160    pub fn new(name: String) -> Self {
161        FnSetFreeParamObj { name }
162    }
163}
164
165impl SumFreeParamObj {
166    pub fn new(name: String) -> Self {
167        SumFreeParamObj { name }
168    }
169}
170
171impl ProductFreeParamObj {
172    pub fn new(name: String) -> Self {
173        ProductFreeParamObj { name }
174    }
175}
176
177impl ByInducFreeParamObj {
178    pub fn new(name: String) -> Self {
179        ByInducFreeParamObj { name }
180    }
181}
182
183impl DefAlgoFreeParamObj {
184    pub fn new(name: String) -> Self {
185        DefAlgoFreeParamObj { name }
186    }
187}
188
189impl fmt::Display for ForallFreeParamObj {
190    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
191        write_parsing_free_param_tagged_spine(f, ParamObjType::Forall, &self.name)
192    }
193}
194
195impl fmt::Display for DefHeaderFreeParamObj {
196    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
197        write_parsing_free_param_tagged_spine(f, ParamObjType::DefHeader, &self.name)
198    }
199}
200
201impl fmt::Display for ExistFreeParamObj {
202    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
203        write_parsing_free_param_tagged_spine(f, ParamObjType::Exist, &self.name)
204    }
205}
206
207impl fmt::Display for SetBuilderFreeParamObj {
208    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
209        write_parsing_free_param_tagged_spine(f, ParamObjType::SetBuilder, &self.name)
210    }
211}
212
213impl fmt::Display for FnSetFreeParamObj {
214    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
215        write_parsing_free_param_tagged_spine(f, ParamObjType::FnSet, &self.name)
216    }
217}
218
219impl fmt::Display for SumFreeParamObj {
220    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
221        write_parsing_free_param_tagged_spine(f, ParamObjType::Sum, &self.name)
222    }
223}
224
225impl fmt::Display for ProductFreeParamObj {
226    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
227        write_parsing_free_param_tagged_spine(f, ParamObjType::Product, &self.name)
228    }
229}
230
231impl fmt::Display for ByInducFreeParamObj {
232    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
233        write_parsing_free_param_tagged_spine(f, ParamObjType::Induc, &self.name)
234    }
235}
236
237impl fmt::Display for DefAlgoFreeParamObj {
238    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
239        write_parsing_free_param_tagged_spine(f, ParamObjType::DefAlgo, &self.name)
240    }
241}
242
243impl From<ForallFreeParamObj> for Obj {
244    fn from(v: ForallFreeParamObj) -> Self {
245        Obj::Atom(AtomObj::Forall(v))
246    }
247}
248
249impl From<DefHeaderFreeParamObj> for Obj {
250    fn from(v: DefHeaderFreeParamObj) -> Self {
251        Obj::Atom(AtomObj::Def(v))
252    }
253}
254
255impl From<ExistFreeParamObj> for Obj {
256    fn from(v: ExistFreeParamObj) -> Self {
257        Obj::Atom(AtomObj::Exist(v))
258    }
259}
260
261impl From<SetBuilderFreeParamObj> for Obj {
262    fn from(v: SetBuilderFreeParamObj) -> Self {
263        Obj::Atom(AtomObj::SetBuilder(v))
264    }
265}
266
267impl From<FnSetFreeParamObj> for Obj {
268    fn from(v: FnSetFreeParamObj) -> Self {
269        Obj::Atom(AtomObj::FnSet(v))
270    }
271}
272
273impl From<SumFreeParamObj> for Obj {
274    fn from(v: SumFreeParamObj) -> Self {
275        Obj::Atom(AtomObj::Sum(v))
276    }
277}
278
279impl From<ProductFreeParamObj> for Obj {
280    fn from(v: ProductFreeParamObj) -> Self {
281        Obj::Atom(AtomObj::Product(v))
282    }
283}
284
285impl From<ByInducFreeParamObj> for Obj {
286    fn from(v: ByInducFreeParamObj) -> Self {
287        Obj::Atom(AtomObj::Induc(v))
288    }
289}
290
291impl From<DefAlgoFreeParamObj> for Obj {
292    fn from(v: DefAlgoFreeParamObj) -> Self {
293        Obj::Atom(AtomObj::DefAlgo(v))
294    }
295}
296
297/// Bound-parameter [`Obj`] for runtime-synthesized facts (`by` stmts, coverage, etc.), matching parse-time `~kind` tagging and [`Runtime::inst_obj`] substitution rules.
298pub fn obj_for_bound_param_in_scope(name: String, scope: ParamObjType) -> Obj {
299    match scope {
300        ParamObjType::Forall => ForallFreeParamObj::new(name).into(),
301        ParamObjType::Exist => ExistFreeParamObj::new(name).into(),
302        ParamObjType::DefHeader => DefHeaderFreeParamObj::new(name).into(),
303        ParamObjType::SetBuilder => SetBuilderFreeParamObj::new(name).into(),
304        ParamObjType::FnSet => FnSetFreeParamObj::new(name).into(),
305        ParamObjType::Sum => SumFreeParamObj::new(name).into(),
306        ParamObjType::Induc => ByInducFreeParamObj::new(name).into(),
307        ParamObjType::DefAlgo => DefAlgoFreeParamObj::new(name).into(),
308        ParamObjType::Product => ProductFreeParamObj::new(name).into(),
309        ParamObjType::Identifier => {
310            unreachable!(
311                "obj_for_bound_param_in_scope: {:?} is not a bare-name binding scope",
312                scope
313            );
314        }
315    }
316}
317
318/// Element [`Obj`] for stored typing / membership facts so keys match parsed bound names (`~tag` spine).
319pub fn param_binding_element_obj_for_store(name: String, binding_kind: ParamObjType) -> Obj {
320    match binding_kind {
321        ParamObjType::Identifier => Identifier::new(name).into(),
322        ParamObjType::Forall
323        | ParamObjType::Exist
324        | ParamObjType::DefHeader
325        | ParamObjType::SetBuilder
326        | ParamObjType::FnSet
327        | ParamObjType::Sum
328        | ParamObjType::Induc
329        | ParamObjType::DefAlgo
330        | ParamObjType::Product => obj_for_bound_param_in_scope(name, binding_kind),
331    }
332}
333
334#[cfg(test)]
335mod strip_numeric_tags_tests {
336    use super::strip_free_param_numeric_tags_in_display;
337
338    #[test]
339    fn tilde_digits_removed_suffix_kept() {
340        assert_eq!(strip_free_param_numeric_tags_in_display("~2aaa"), "aaa");
341        assert_eq!(
342            strip_free_param_numeric_tags_in_display(r#""x": "~2foo""#),
343            r#""x": "foo""#
344        );
345    }
346
347    #[test]
348    fn tilde_not_followed_by_digit_kept() {
349        assert_eq!(
350            strip_free_param_numeric_tags_in_display("~/tmp.lit"),
351            "~/tmp.lit"
352        );
353        assert_eq!(strip_free_param_numeric_tags_in_display("~"), "~");
354    }
355}
litex/obj/free_param_obj.rs

litex/obj/
free_param_obj.rs
