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    Induc(ByInducFreeParamObj),
15    DefAlgo(DefAlgoFreeParamObj),
16}
17
18impl fmt::Display for AtomObj {
19    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
20        match self {
21            AtomObj::Identifier(x) => write!(f, "{}", x),
22            AtomObj::IdentifierWithMod(x) => write!(f, "{}", x),
23            AtomObj::Forall(x) => write!(f, "{}", x),
24            AtomObj::Def(x) => write!(f, "{}", x),
25            AtomObj::Exist(x) => write!(f, "{}", x),
26            AtomObj::SetBuilder(x) => write!(f, "{}", x),
27            AtomObj::FnSet(x) => write!(f, "{}", x),
28            AtomObj::Induc(x) => write!(f, "{}", x),
29            AtomObj::DefAlgo(x) => write!(f, "{}", x),
30        }
31    }
32}
33
34impl AtomObj {
35    pub fn replace_bound_identifier(self, from: &str, to: &str) -> Self {
36        if from == to {
37            return self;
38        }
39        match self {
40            AtomObj::Identifier(i) => {
41                if i.name == from {
42                    AtomObj::Identifier(Identifier::new(to.to_string()))
43                } else {
44                    AtomObj::Identifier(i)
45                }
46            }
47            AtomObj::IdentifierWithMod(m) => {
48                let name = if m.name == from {
49                    to.to_string()
50                } else {
51                    m.name
52                };
53                AtomObj::IdentifierWithMod(IdentifierWithMod::new(m.mod_name, name))
54            }
55            AtomObj::Forall(p) => {
56                let name = if p.name == from {
57                    to.to_string()
58                } else {
59                    p.name
60                };
61                AtomObj::Forall(ForallFreeParamObj::new(name))
62            }
63            AtomObj::Def(p) => {
64                let name = if p.name == from {
65                    to.to_string()
66                } else {
67                    p.name
68                };
69                AtomObj::Def(DefHeaderFreeParamObj::new(name))
70            }
71            AtomObj::Exist(p) => {
72                let name = if p.name == from {
73                    to.to_string()
74                } else {
75                    p.name
76                };
77                AtomObj::Exist(ExistFreeParamObj::new(name))
78            }
79            AtomObj::SetBuilder(p) => {
80                let name = if p.name == from {
81                    to.to_string()
82                } else {
83                    p.name
84                };
85                AtomObj::SetBuilder(SetBuilderFreeParamObj::new(name))
86            }
87            AtomObj::FnSet(p) => {
88                let name = if p.name == from {
89                    to.to_string()
90                } else {
91                    p.name
92                };
93                AtomObj::FnSet(FnSetFreeParamObj::new(name))
94            }
95            AtomObj::Induc(p) => {
96                let name = if p.name == from {
97                    to.to_string()
98                } else {
99                    p.name
100                };
101                AtomObj::Induc(ByInducFreeParamObj::new(name))
102            }
103            AtomObj::DefAlgo(p) => {
104                let name = if p.name == from {
105                    to.to_string()
106                } else {
107                    p.name
108                };
109                AtomObj::DefAlgo(DefAlgoFreeParamObj::new(name))
110            }
111        }
112    }
113}
114
115impl From<AtomObj> for Obj {
116    fn from(a: AtomObj) -> Self {
117        Obj::Atom(a)
118    }
119}
litex/obj/atom_obj.rs

litex/obj/
atom_obj.rs
