litex/obj/
atom_obj.rs

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

litex/obj/
atom_obj.rs
