litex/obj/
fn_obj_head.rs

1use crate::prelude::*;
2use std::fmt;
3
4/// Function-application head: plain identifier pieces or tagged free-parameter binders.
5#[derive(Clone)]
6pub enum FnObjHead {
7    Identifier(Identifier),
8    IdentifierWithMod(IdentifierWithMod),
9    Forall(ForallFreeParamObj),
10    DefHeader(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 FnObjHead {
21    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
22        match self {
23            FnObjHead::Identifier(x) => write!(f, "{}", x),
24            FnObjHead::IdentifierWithMod(x) => write!(f, "{}", x),
25            FnObjHead::Forall(p) => write!(f, "{}", p),
26            FnObjHead::DefHeader(p) => write!(f, "{}", p),
27            FnObjHead::Exist(p) => write!(f, "{}", p),
28            FnObjHead::SetBuilder(p) => write!(f, "{}", p),
29            FnObjHead::FnSet(p) => write!(f, "{}", p),
30            FnObjHead::Sum(p) => write!(f, "{}", p),
31            FnObjHead::Product(p) => write!(f, "{}", p),
32            FnObjHead::Induc(p) => write!(f, "{}", p),
33            FnObjHead::DefAlgo(p) => write!(f, "{}", p),
34        }
35    }
36}
37
38impl FnObjHead {
39    /// If `obj` is a plain name shape, returns the corresponding function head; otherwise `None`.
40    pub fn from_name_obj(obj: Obj) -> Option<FnObjHead> {
41        match obj {
42            Obj::Atom(a) => match a {
43                AtomObj::Identifier(x) => Some(FnObjHead::Identifier(x)),
44                AtomObj::IdentifierWithMod(x) => Some(FnObjHead::IdentifierWithMod(x)),
45                AtomObj::Forall(p) => Some(FnObjHead::Forall(p)),
46                AtomObj::Def(p) => Some(FnObjHead::DefHeader(p)),
47                AtomObj::Exist(p) => Some(FnObjHead::Exist(p)),
48                AtomObj::SetBuilder(p) => Some(FnObjHead::SetBuilder(p)),
49                AtomObj::FnSet(p) => Some(FnObjHead::FnSet(p)),
50                AtomObj::Sum(p) => Some(FnObjHead::Sum(p)),
51                AtomObj::Product(p) => Some(FnObjHead::Product(p)),
52                AtomObj::Induc(p) => Some(FnObjHead::Induc(p)),
53                AtomObj::DefAlgo(p) => Some(FnObjHead::DefAlgo(p)),
54            },
55            _ => None,
56        }
57    }
58}
59
60impl From<ForallFreeParamObj> for FnObjHead {
61    fn from(p: ForallFreeParamObj) -> Self {
62        FnObjHead::Forall(p)
63    }
64}
65
66impl From<DefHeaderFreeParamObj> for FnObjHead {
67    fn from(p: DefHeaderFreeParamObj) -> Self {
68        FnObjHead::DefHeader(p)
69    }
70}
71
72impl From<ExistFreeParamObj> for FnObjHead {
73    fn from(p: ExistFreeParamObj) -> Self {
74        FnObjHead::Exist(p)
75    }
76}
77
78impl From<SetBuilderFreeParamObj> for FnObjHead {
79    fn from(p: SetBuilderFreeParamObj) -> Self {
80        FnObjHead::SetBuilder(p)
81    }
82}
83
84impl From<FnSetFreeParamObj> for FnObjHead {
85    fn from(p: FnSetFreeParamObj) -> Self {
86        FnObjHead::FnSet(p)
87    }
88}
89
90impl From<SumFreeParamObj> for FnObjHead {
91    fn from(p: SumFreeParamObj) -> Self {
92        FnObjHead::Sum(p)
93    }
94}
95
96impl From<ProductFreeParamObj> for FnObjHead {
97    fn from(p: ProductFreeParamObj) -> Self {
98        FnObjHead::Product(p)
99    }
100}
101
102impl From<ByInducFreeParamObj> for FnObjHead {
103    fn from(p: ByInducFreeParamObj) -> Self {
104        FnObjHead::Induc(p)
105    }
106}
107
108impl From<DefAlgoFreeParamObj> for FnObjHead {
109    fn from(p: DefAlgoFreeParamObj) -> Self {
110        FnObjHead::DefAlgo(p)
111    }
112}
113
114impl From<FnObjHead> for Obj {
115    fn from(h: FnObjHead) -> Self {
116        match h {
117            FnObjHead::Identifier(x) => x.into(),
118            FnObjHead::IdentifierWithMod(x) => x.into(),
119            FnObjHead::Forall(p) => p.into(),
120            FnObjHead::DefHeader(p) => p.into(),
121            FnObjHead::Exist(p) => p.into(),
122            FnObjHead::SetBuilder(p) => p.into(),
123            FnObjHead::FnSet(p) => p.into(),
124            FnObjHead::Sum(p) => p.into(),
125            FnObjHead::Product(p) => p.into(),
126            FnObjHead::Induc(p) => p.into(),
127            FnObjHead::DefAlgo(p) => p.into(),
128        }
129    }
130}
litex/obj/fn_obj_head.rs

litex/obj/
fn_obj_head.rs
