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            },
52            _ => None,
53        }
54    }
55}
56
57impl From<ForallFreeParamObj> for FnObjHead {
58    fn from(p: ForallFreeParamObj) -> Self {
59        FnObjHead::Forall(p)
60    }
61}
62
63impl From<DefHeaderFreeParamObj> for FnObjHead {
64    fn from(p: DefHeaderFreeParamObj) -> Self {
65        FnObjHead::DefHeader(p)
66    }
67}
68
69impl From<ExistFreeParamObj> for FnObjHead {
70    fn from(p: ExistFreeParamObj) -> Self {
71        FnObjHead::Exist(p)
72    }
73}
74
75impl From<SetBuilderFreeParamObj> for FnObjHead {
76    fn from(p: SetBuilderFreeParamObj) -> Self {
77        FnObjHead::SetBuilder(p)
78    }
79}
80
81impl From<FnSetFreeParamObj> for FnObjHead {
82    fn from(p: FnSetFreeParamObj) -> Self {
83        FnObjHead::FnSet(p)
84    }
85}
86
87impl From<ByInducFreeParamObj> for FnObjHead {
88    fn from(p: ByInducFreeParamObj) -> Self {
89        FnObjHead::Induc(p)
90    }
91}
92
93impl From<DefAlgoFreeParamObj> for FnObjHead {
94    fn from(p: DefAlgoFreeParamObj) -> Self {
95        FnObjHead::DefAlgo(p)
96    }
97}
98
99impl From<FnObjHead> for Obj {
100    fn from(h: FnObjHead) -> Self {
101        match h {
102            FnObjHead::Identifier(x) => x.into(),
103            FnObjHead::IdentifierWithMod(x) => x.into(),
104            FnObjHead::Forall(p) => p.into(),
105            FnObjHead::DefHeader(p) => p.into(),
106            FnObjHead::Exist(p) => p.into(),
107            FnObjHead::SetBuilder(p) => p.into(),
108            FnObjHead::FnSet(p) => p.into(),
109            FnObjHead::AnonymousFnLiteral(a) => (*a).clone().into(),
110            FnObjHead::Induc(p) => p.into(),
111            FnObjHead::DefAlgo(p) => p.into(),
112        }
113    }
114}
litex/obj/fn_obj_head.rs

litex/obj/
fn_obj_head.rs
