litex/obj/
atom_obj.rs

1use super::free_param_obj::DefStructFieldFreeParamObj;
2use crate::prelude::*;
3use std::fmt;
4
5/// 仅「名字/绑定子」的 [`Obj`] 载荷：标识符、带 `::` 的名字、与解析期自由参标记。
6#[derive(Clone)]
7pub enum AtomObj {
8    Identifier(Identifier),
9    IdentifierWithMod(IdentifierWithMod),
10    Forall(ForallFreeParamObj),
11    Def(DefHeaderFreeParamObj),
12    Exist(ExistFreeParamObj),
13    SetBuilder(SetBuilderFreeParamObj),
14    FnSet(FnSetFreeParamObj),
15    Induc(ByInducFreeParamObj),
16    DefAlgo(DefAlgoFreeParamObj),
17    DefStructField(DefStructFieldFreeParamObj),
18}
19
20impl fmt::Display for AtomObj {
21    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
22        match self {
23            AtomObj::Identifier(x) => write!(f, "{}", x),
24            AtomObj::IdentifierWithMod(x) => write!(f, "{}", x),
25            AtomObj::Forall(x) => write!(f, "{}", x),
26            AtomObj::Def(x) => write!(f, "{}", x),
27            AtomObj::Exist(x) => write!(f, "{}", x),
28            AtomObj::SetBuilder(x) => write!(f, "{}", x),
29            AtomObj::FnSet(x) => write!(f, "{}", x),
30            AtomObj::Induc(x) => write!(f, "{}", x),
31            AtomObj::DefAlgo(x) => write!(f, "{}", x),
32            AtomObj::DefStructField(x) => write!(f, "{}", x),
33        }
34    }
35}
36
37impl AtomObj {
38    pub fn replace_bound_identifier(self, from: &str, to: &str) -> Self {
39        if from == to {
40            return self;
41        }
42        match self {
43            AtomObj::Identifier(i) => {
44                if i.name == from {
45                    AtomObj::Identifier(Identifier::new(to.to_string()))
46                } else {
47                    AtomObj::Identifier(i)
48                }
49            }
50            AtomObj::IdentifierWithMod(m) => {
51                let name = if m.name == from {
52                    to.to_string()
53                } else {
54                    m.name
55                };
56                AtomObj::IdentifierWithMod(IdentifierWithMod::new(m.mod_name, name))
57            }
58            AtomObj::Forall(p) => {
59                let name = if p.name == from {
60                    to.to_string()
61                } else {
62                    p.name
63                };
64                AtomObj::Forall(ForallFreeParamObj::new(name))
65            }
66            AtomObj::Def(p) => {
67                let name = if p.name == from {
68                    to.to_string()
69                } else {
70                    p.name
71                };
72                AtomObj::Def(DefHeaderFreeParamObj::new(name))
73            }
74            AtomObj::Exist(p) => {
75                let name = if p.name == from {
76                    to.to_string()
77                } else {
78                    p.name
79                };
80                AtomObj::Exist(ExistFreeParamObj::new(name))
81            }
82            AtomObj::SetBuilder(p) => {
83                let name = if p.name == from {
84                    to.to_string()
85                } else {
86                    p.name
87                };
88                AtomObj::SetBuilder(SetBuilderFreeParamObj::new(name))
89            }
90            AtomObj::FnSet(p) => {
91                let name = if p.name == from {
92                    to.to_string()
93                } else {
94                    p.name
95                };
96                AtomObj::FnSet(FnSetFreeParamObj::new(name))
97            }
98            AtomObj::Induc(p) => {
99                let name = if p.name == from {
100                    to.to_string()
101                } else {
102                    p.name
103                };
104                AtomObj::Induc(ByInducFreeParamObj::new(name))
105            }
106            AtomObj::DefAlgo(p) => {
107                let name = if p.name == from {
108                    to.to_string()
109                } else {
110                    p.name
111                };
112                AtomObj::DefAlgo(DefAlgoFreeParamObj::new(name))
113            }
114            AtomObj::DefStructField(p) => {
115                let name = if p.name == from {
116                    to.to_string()
117                } else {
118                    p.name
119                };
120                AtomObj::DefStructField(DefStructFieldFreeParamObj::new(name))
121            }
122        }
123    }
124}
125
126impl From<AtomObj> for Obj {
127    fn from(a: AtomObj) -> Self {
128        Obj::Atom(a)
129    }
130}
litex/obj/atom_obj.rs

litex/obj/
atom_obj.rs
