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

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

use crate::syntax::abs::*;

impl AbsConsInfo {
    pub fn new(source: Loc, name: Ident, tele: AbsTele, data_index: GI) -> Self {
        Self {
            source,
            name,
            tele,
            data_ix: data_index,
        }
    }
}

impl AbsProjInfo {
    pub fn new(source: Loc, name: Ident, proj_ty: Abs, codata_index: GI) -> Self {
        Self {
            source,
            name,
            ty: proj_ty,
            codata_ix: codata_index,
        }
    }
}

impl AbsDataInfo {
    pub fn new(source: Loc, name: Ident, level: Level, tele: AbsTele, conses: Vec<GI>) -> Self {
        AbsDataInfo {
            source,
            name,
            level,
            tele,
            conses,
        }
    }
}

impl AbsClause {
    pub fn new(
        source: Loc,
        name: Ident,
        patterns: Vec<AbsCopat>,
        definition: GI,
        body: Abs,
    ) -> Self {
        Self {
            source,
            name,
            patterns,
            definition,
            body,
        }
    }
}

impl AbsDefnInfo {
    pub fn new(source: Loc, name: Ident, ty: Abs) -> Self {
        Self { source, name, ty }
    }
}

impl AbsCodataInfo {
    pub fn new(
        source: Loc,
        name: Ident,
        me: Option<Ident>,
        level: Level,
        tele: AbsTele,
        fields: Vec<GI>,
    ) -> Self {
        Self {
            source,
            name,
            self_ref: me,
            level,
            tele,
            fields,
        }
    }
}

macro_rules! simple_to_loc {
    ($name:ident) => {
        impl ToLoc for $name {
            fn loc(&self) -> Loc {
                self.source
            }
        }
    };
}

simple_to_loc!(AbsClause);
simple_to_loc!(AbsConsInfo);
simple_to_loc!(AbsDataInfo);
simple_to_loc!(AbsProjInfo);
simple_to_loc!(AbsDefnInfo);
simple_to_loc!(AbsCodataInfo);