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    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::AnonymousFnLiteral(a) => write!(f, "{}", a),
31            FnObjHead::Induc(p) => write!(f, "{}", p),
32            FnObjHead::DefAlgo(p) => write!(f, "{}", p),
33        }
34    }
35}
36
37impl FnObjHead {
38    /// If `obj` is a plain name shape, returns the corresponding function head; otherwise `None`.
39    pub fn given_an_atom_return_a_fn_obj_head(obj: Obj) -> Option<FnObjHead> {
40        match obj {
41            Obj::Atom(a) => match a {
42                AtomObj::Identifier(x) => Some(FnObjHead::Identifier(x)),
43                AtomObj::IdentifierWithMod(x) => Some(FnObjHead::IdentifierWithMod(x)),
44                AtomObj::Forall(p) => Some(FnObjHead::Forall(p)),
45                AtomObj::Def(p) => Some(FnObjHead::DefHeader(p)),
46                AtomObj::Exist(p) => Some(FnObjHead::Exist(p)),
47                AtomObj::SetBuilder(p) => Some(FnObjHead::SetBuilder(p)),
48                AtomObj::FnSet(p) => Some(FnObjHead::FnSet(p)),
49                AtomObj::Induc(p) => Some(FnObjHead::Induc(p)),
50                AtomObj::DefAlgo(p) => Some(FnObjHead::DefAlgo(p)),
51                AtomObj::DefStructField(_) => None,
52            },
53            _ => None,
54        }
55    }
56}
57
58impl From<ForallFreeParamObj> for FnObjHead {
59    fn from(p: ForallFreeParamObj) -> Self {
60        FnObjHead::Forall(p)
61    }
62}
63
64impl From<DefHeaderFreeParamObj> for FnObjHead {
65    fn from(p: DefHeaderFreeParamObj) -> Self {
66        FnObjHead::DefHeader(p)
67    }
68}
69
70impl From<ExistFreeParamObj> for FnObjHead {
71    fn from(p: ExistFreeParamObj) -> Self {
72        FnObjHead::Exist(p)
73    }
74}
75
76impl From<SetBuilderFreeParamObj> for FnObjHead {
77    fn from(p: SetBuilderFreeParamObj) -> Self {
78        FnObjHead::SetBuilder(p)
79    }
80}
81
82impl From<FnSetFreeParamObj> for FnObjHead {
83    fn from(p: FnSetFreeParamObj) -> Self {
84        FnObjHead::FnSet(p)
85    }
86}
87
88impl From<ByInducFreeParamObj> for FnObjHead {
89    fn from(p: ByInducFreeParamObj) -> Self {
90        FnObjHead::Induc(p)
91    }
92}
93
94impl From<DefAlgoFreeParamObj> for FnObjHead {
95    fn from(p: DefAlgoFreeParamObj) -> Self {
96        FnObjHead::DefAlgo(p)
97    }
98}
99
100impl From<FnObjHead> for Obj {
101    fn from(h: FnObjHead) -> Self {
102        match h {
103            FnObjHead::Identifier(x) => x.into(),
104            FnObjHead::IdentifierWithMod(x) => x.into(),
105            FnObjHead::Forall(p) => p.into(),
106            FnObjHead::DefHeader(p) => p.into(),
107            FnObjHead::Exist(p) => p.into(),
108            FnObjHead::SetBuilder(p) => p.into(),
109            FnObjHead::FnSet(p) => p.into(),
110            FnObjHead::AnonymousFnLiteral(a) => (*a).clone().into(),
111            FnObjHead::Induc(p) => p.into(),
112            FnObjHead::DefAlgo(p) => p.into(),
113        }
114    }
115}
litex/obj/fn_obj_head.rs

litex/obj/
fn_obj_head.rs
