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

litex/obj/
free_param_obj.rs
