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}
20
21impl fmt::Display for FnObjHead {
22    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
23        match self {
24            FnObjHead::Identifier(x) => write!(f, "{}", x),
25            FnObjHead::IdentifierWithMod(x) => write!(f, "{}", x),
26            FnObjHead::Forall(p) => write!(f, "{}", p),
27            FnObjHead::DefHeader(p) => write!(f, "{}", p),
28            FnObjHead::Exist(p) => write!(f, "{}", p),
29            FnObjHead::SetBuilder(p) => write!(f, "{}", p),
30            FnObjHead::FnSet(p) => write!(f, "{}", p),
31            FnObjHead::AnonymousFnLiteral(a) => write!(f, "{}", a),
32            FnObjHead::FiniteSeqListObj(v) => write!(f, "{}", v),
33            FnObjHead::Induc(p) => write!(f, "{}", p),
34            FnObjHead::DefAlgo(p) => write!(f, "{}", p),
35        }
36    }
37}
38
39impl FnObjHead {
40    /// If `obj` is a plain name shape, returns the corresponding function head; otherwise `None`.
41    pub fn given_an_atom_return_a_fn_obj_head(obj: Obj) -> Option<FnObjHead> {
42        match obj {
43            Obj::Atom(a) => match a {
44                AtomObj::Identifier(x) => Some(FnObjHead::Identifier(x)),
45                AtomObj::IdentifierWithMod(x) => Some(FnObjHead::IdentifierWithMod(x)),
46                AtomObj::Forall(p) => Some(FnObjHead::Forall(p)),
47                AtomObj::Def(p) => Some(FnObjHead::DefHeader(p)),
48                AtomObj::Exist(p) => Some(FnObjHead::Exist(p)),
49                AtomObj::SetBuilder(p) => Some(FnObjHead::SetBuilder(p)),
50                AtomObj::FnSet(p) => Some(FnObjHead::FnSet(p)),
51                AtomObj::Induc(p) => Some(FnObjHead::Induc(p)),
52                AtomObj::DefAlgo(p) => Some(FnObjHead::DefAlgo(p)),
53                AtomObj::DefStructField(_) => None,
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<ByInducFreeParamObj> for FnObjHead {
91    fn from(p: ByInducFreeParamObj) -> Self {
92        FnObjHead::Induc(p)
93    }
94}
95
96impl From<DefAlgoFreeParamObj> for FnObjHead {
97    fn from(p: DefAlgoFreeParamObj) -> Self {
98        FnObjHead::DefAlgo(p)
99    }
100}
101
102impl From<FnObjHead> for Obj {
103    fn from(h: FnObjHead) -> Self {
104        match h {
105            FnObjHead::Identifier(x) => x.into(),
106            FnObjHead::IdentifierWithMod(x) => x.into(),
107            FnObjHead::Forall(p) => p.into(),
108            FnObjHead::DefHeader(p) => p.into(),
109            FnObjHead::Exist(p) => p.into(),
110            FnObjHead::SetBuilder(p) => p.into(),
111            FnObjHead::FnSet(p) => p.into(),
112            FnObjHead::AnonymousFnLiteral(a) => (*a).clone().into(),
113            FnObjHead::FiniteSeqListObj(v) => v.into(),
114            FnObjHead::Induc(p) => p.into(),
115            FnObjHead::DefAlgo(p) => p.into(),
116        }
117    }
118}
litex/obj/fn_obj_head.rs

litex/obj/
fn_obj_head.rs
