nar/syntax/abs/
decl.rs

1use voile_util::{
2    level::Level,
3    loc::{Ident, Loc, ToLoc},
4    uid::GI,
5};
6
7use crate::syntax::abs::{Abs, AbsCopat, AbsTele};
8
9#[derive(Debug, PartialEq, Eq, Clone)]
10pub struct AbsConsInfo {
11    pub source: Loc,
12    pub name: Ident,
13    pub tele: AbsTele,
14    /// Corresponding datatype's index.
15    pub data_ix: GI,
16}
17
18#[derive(Debug, PartialEq, Eq, Clone)]
19pub struct AbsDefnInfo {
20    pub source: Loc,
21    pub name: Ident,
22    pub ty: Abs,
23}
24
25#[derive(Debug, PartialEq, Eq, Clone)]
26pub struct AbsProjInfo {
27    pub source: Loc,
28    pub name: Ident,
29    pub ty: Abs,
30    /// Corresponding coinductive record's index.
31    pub codata_ix: GI,
32}
33
34#[derive(Debug, PartialEq, Eq, Clone)]
35pub struct AbsCodataInfo {
36    pub source: Loc,
37    pub self_ref: Option<Ident>,
38    pub name: Ident,
39    pub fields: Vec<GI>,
40    pub level: Level,
41    pub tele: AbsTele,
42}
43
44#[derive(Debug, PartialEq, Eq, Clone)]
45pub struct AbsDataInfo {
46    pub source: Loc,
47    pub name: Ident,
48    pub level: Level,
49    pub tele: AbsTele,
50    pub conses: Vec<GI>,
51}
52
53/// Declaration.
54/// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/Agda-Syntax-Abstract.html#t:Declaration).
55#[derive(Debug, PartialEq, Eq, Clone)]
56pub enum AbsDecl {
57    /// Datatypes.
58    Data(AbsDataInfo),
59    /// Datatype constructors.
60    Cons(AbsConsInfo),
61    /// Coinductive record projections.
62    Proj(AbsProjInfo),
63    /// Function signature definition.
64    Defn(AbsDefnInfo),
65    /// Pattern matching clause.
66    Clause(AbsClause),
67    /// Coinductive records.
68    Codata(AbsCodataInfo),
69}
70
71impl AbsDecl {
72    pub fn decl_name(&self) -> &Ident {
73        use AbsDecl::*;
74        match self {
75            Defn(info) => &info.name,
76            Clause(info) => &info.name,
77            Data(info) => &info.name,
78            Cons(info) => &info.name,
79            Proj(info) => &info.name,
80            Codata(info) => &info.name,
81        }
82    }
83}
84
85impl ToLoc for AbsDecl {
86    fn loc(&self) -> Loc {
87        use AbsDecl::*;
88        match self {
89            Defn(i) => i.loc(),
90            Data(i) => i.loc(),
91            Cons(i) => i.loc(),
92            Clause(i) => i.loc(),
93            Codata(i) => i.loc(),
94            Proj(i) => i.loc(),
95        }
96    }
97}
98
99/// Clause information in abstract syntax.
100/// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.Syntax.Abstract.html#Clause%27).
101#[derive(Debug, PartialEq, Eq, Clone)]
102pub struct AbsClause {
103    pub source: Loc,
104    /// Name of the function we're adding clause to.
105    pub name: Ident,
106    /// Lhs.
107    pub patterns: Vec<AbsCopat>,
108    /// Index of the type signature definition.
109    pub definition: GI,
110    /// Rhs.
111    pub body: Abs,
112}
nar/syntax/abs/decl.rs

nar/syntax/abs/
decl.rs
