nar 0.0.8

Narc, a dependently-typed programming language with dependent pattern matching
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112

use voile_util::{level::Level, loc::*, uid::GI};

use crate::{
    check::pats::CoreCopat,
    syntax::core::{Tele, Term},
};

#[derive(Debug, PartialEq, Eq, Clone)]
pub struct CodataInfo {
    pub loc: Loc,
    pub self_ref: Option<Ident>,
    pub name: Ident,
    pub params: Tele,
    /// References to its projections (fields).
    pub fields: Vec<GI>,
    pub level: Level,
}

#[derive(Debug, PartialEq, Eq, Clone)]
pub struct FuncInfo {
    pub loc: Loc,
    pub name: Ident,
    pub signature: Term,
    pub clauses: Vec<Clause>,
}

#[derive(Debug, PartialEq, Eq, Clone)]
pub struct ConsInfo {
    pub loc: Loc,
    pub name: Ident,
    pub params: Tele,
    pub data: GI,
    /// If this is a record constructor,
    /// we fill the fields' names here.
    pub fields: Option<Vec<String>>,
}

#[derive(Debug, PartialEq, Eq, Clone)]
pub struct DataInfo {
    pub loc: Loc,
    pub name: Ident,
    pub params: Tele,
    /// References to its constructors.
    pub conses: Vec<GI>,
    pub level: Level,
}

/// Declaration.
/// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.TypeChecking.Monad.Base.html#Function).
#[derive(Debug, PartialEq, Eq, Clone)]
pub enum Decl {
    /// Datatypes.
    Data(DataInfo),
    /// Coinductive records.
    Codata(CodataInfo),
    Cons(ConsInfo),
    Proj {
        loc: Loc,
        name: Ident,
        codata: GI,
        ty: Term,
    },
    /// Function definitions.
    Func(FuncInfo),
    /// Placeholder for a clause, should never be accessed.
    ClausePlaceholder,
}

impl Decl {
    pub fn def_name(&self) -> &Ident {
        match self {
            Decl::Proj { name, .. } => name,
            Decl::Data(i) => &i.name,
            Decl::Cons(i) => &i.name,
            Decl::Codata(i) => &i.name,
            Decl::Func(i) => &i.name,
            Decl::ClausePlaceholder => unreachable!(),
        }
    }
}

impl ToLoc for Decl {
    fn loc(&self) -> Loc {
        match self {
            Decl::Proj { loc, .. } => *loc,
            Decl::Data(i) => i.loc(),
            Decl::Cons(i) => i.loc(),
            Decl::Codata(i) => i.loc(),
            Decl::Func(i) => i.loc(),
            Decl::ClausePlaceholder => unreachable!(),
        }
    }
}

/// Function clauses.
/// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.Syntax.Internal.html#Clause).
#[derive(Debug, PartialEq, Eq, Clone)]
pub struct Clause {
    /// $\Delta$. The types of the pattern variables in dependency order.
    pub pat_tele: Tele,
    /// $\Delta \vdash ps$. The de Bruijn indices refer to $\Delta$.
    pub patterns: Vec<CoreCopat>,
    /// `Some(v)` if $\Delta \vdash v$, while `None` if the patterns are absurd.
    pub body: Option<Term>,
    // TODO: case-trees.
}

impl Clause {
    pub fn is_absurd(&self) -> bool {
        self.body.is_none()
    }
}