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

litex/obj/
free_param_obj.rs
