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

litex/obj/
free_param_obj.rs
