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    /// Anonymous function literal used as applied head, e.g. `'(x R) R {x}(a)`.
15    AnonymousFnLiteral(Box<AnonymousFn>),
16    FiniteSeqListObj(FiniteSeqListObj),
17    Induc(ByInducFreeParamObj),
18    DefAlgo(DefAlgoFreeParamObj),
19    InstantiatedTemplateObj(InstantiatedTemplateObj),
20}
21
22impl fmt::Display for FnObjHead {
23    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
24        match self {
25            FnObjHead::Identifier(x) => write!(f, "{}", x),
26            FnObjHead::IdentifierWithMod(x) => write!(f, "{}", x),
27            FnObjHead::Forall(p) => write!(f, "{}", p),
28            FnObjHead::DefHeader(p) => write!(f, "{}", p),
29            FnObjHead::Exist(p) => write!(f, "{}", p),
30            FnObjHead::SetBuilder(p) => write!(f, "{}", p),
31            FnObjHead::FnSet(p) => write!(f, "{}", p),
32            FnObjHead::AnonymousFnLiteral(a) => write!(f, "{}", a),
33            FnObjHead::FiniteSeqListObj(v) => write!(f, "{}", v),
34            FnObjHead::Induc(p) => write!(f, "{}", p),
35            FnObjHead::DefAlgo(p) => write!(f, "{}", p),
36            FnObjHead::InstantiatedTemplateObj(t) => write!(f, "{}", t),
37        }
38    }
39}
40
41impl FnObjHead {
42    /// If `obj` is a plain name shape, returns the corresponding function head; otherwise `None`.
43    pub fn given_an_atom_return_a_fn_obj_head(obj: Obj) -> Option<FnObjHead> {
44        match obj {
45            Obj::Atom(a) => match a {
46                AtomObj::Identifier(x) => Some(FnObjHead::Identifier(x)),
47                AtomObj::IdentifierWithMod(x) => Some(FnObjHead::IdentifierWithMod(x)),
48                AtomObj::Forall(p) => Some(FnObjHead::Forall(p)),
49                AtomObj::Def(p) => Some(FnObjHead::DefHeader(p)),
50                AtomObj::Exist(p) => Some(FnObjHead::Exist(p)),
51                AtomObj::SetBuilder(p) => Some(FnObjHead::SetBuilder(p)),
52                AtomObj::FnSet(p) => Some(FnObjHead::FnSet(p)),
53                AtomObj::Induc(p) => Some(FnObjHead::Induc(p)),
54                AtomObj::DefAlgo(p) => Some(FnObjHead::DefAlgo(p)),
55                AtomObj::DefStructField(_) => None,
56            },
57            _ => None,
58        }
59    }
60}
61
62impl From<ForallFreeParamObj> for FnObjHead {
63    fn from(p: ForallFreeParamObj) -> Self {
64        FnObjHead::Forall(p)
65    }
66}
67
68impl From<DefHeaderFreeParamObj> for FnObjHead {
69    fn from(p: DefHeaderFreeParamObj) -> Self {
70        FnObjHead::DefHeader(p)
71    }
72}
73
74impl From<ExistFreeParamObj> for FnObjHead {
75    fn from(p: ExistFreeParamObj) -> Self {
76        FnObjHead::Exist(p)
77    }
78}
79
80impl From<SetBuilderFreeParamObj> for FnObjHead {
81    fn from(p: SetBuilderFreeParamObj) -> Self {
82        FnObjHead::SetBuilder(p)
83    }
84}
85
86impl From<FnSetFreeParamObj> for FnObjHead {
87    fn from(p: FnSetFreeParamObj) -> Self {
88        FnObjHead::FnSet(p)
89    }
90}
91
92impl From<ByInducFreeParamObj> for FnObjHead {
93    fn from(p: ByInducFreeParamObj) -> Self {
94        FnObjHead::Induc(p)
95    }
96}
97
98impl From<DefAlgoFreeParamObj> for FnObjHead {
99    fn from(p: DefAlgoFreeParamObj) -> Self {
100        FnObjHead::DefAlgo(p)
101    }
102}
103
104impl From<FnObjHead> for Obj {
105    fn from(h: FnObjHead) -> Self {
106        match h {
107            FnObjHead::Identifier(x) => x.into(),
108            FnObjHead::IdentifierWithMod(x) => x.into(),
109            FnObjHead::Forall(p) => p.into(),
110            FnObjHead::DefHeader(p) => p.into(),
111            FnObjHead::Exist(p) => p.into(),
112            FnObjHead::SetBuilder(p) => p.into(),
113            FnObjHead::FnSet(p) => p.into(),
114            FnObjHead::AnonymousFnLiteral(a) => (*a).clone().into(),
115            FnObjHead::FiniteSeqListObj(v) => v.into(),
116            FnObjHead::Induc(p) => p.into(),
117            FnObjHead::DefAlgo(p) => p.into(),
118            FnObjHead::InstantiatedTemplateObj(t) => t.into(),
119        }
120    }
121}
litex/obj/fn_obj_head.rs

litex/obj/
fn_obj_head.rs
