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

use voile_util::{
    level::Level,
    loc::{Ident, Loc, ToLoc},
    meta::MI,
    uid::{GI, UID},
    vec1::Vec1,
};

use crate::syntax::{common, pat::*};

/// The abstract syntax.
#[derive(Debug, PartialEq, Eq, Clone)]
pub enum Abs {
    Def(Ident, GI),
    Var(Ident, UID),
    Meta(Ident, MI),
    App(Box<Self>, Box<Vec1<Self>>),
    Pi(Loc, Bind<Box<Self>>, Box<Self>),
    Type(Ident, Level),
    Cons(Ident, GI),
    Proj(Ident, GI),
}

/// Application's internal view.
/// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.Syntax.Abstract.Views.html#AppView).
#[derive(Debug, PartialEq, Eq, Clone)]
pub struct AppView {
    pub fun: Abs,
    pub args: Vec<Abs>,
}

impl AppView {
    pub fn new(fun: Abs, args: Vec<Abs>) -> Self {
        Self { fun, args }
    }

    pub fn into_abs(mut self) -> Abs {
        if self.args.is_empty() {
            self.fun
        } else {
            let head = self.args.remove(0);
            Abs::app(self.fun, Vec1::new(head, self.args))
        }
    }
}

impl Abs {
    /// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.Syntax.Abstract.Views.html#appView).
    pub fn into_app_view(self) -> AppView {
        match self {
            Abs::App(f, arg) => {
                let mut view = f.into_app_view();
                arg.append_self_into(&mut view.args);
                view
            }
            e => AppView::new(e, vec![]),
        }
    }

    pub fn simple_app(f: Self, arg: Self) -> Self {
        Self::app(f, From::from(arg))
    }

    pub fn app(f: Self, args: Vec1<Self>) -> Self {
        Abs::App(Box::new(f), Box::new(args))
    }

    pub fn universe(id: Ident) -> Self {
        Abs::universe_at(id, Default::default())
    }

    pub fn meta(id: Ident, mi: MI) -> Self {
        Abs::Meta(id, mi)
    }

    pub fn universe_at(id: Ident, level: Level) -> Self {
        Abs::Type(id, level)
    }
}

impl ToLoc for Abs {
    fn loc(&self) -> Loc {
        use Abs::*;
        match self {
            Proj(ident, ..)
            | Cons(ident, ..)
            | Type(ident, ..)
            | Def(ident, ..)
            | Var(ident, ..)
            | Meta(ident, ..) => ident.loc,
            Pi(loc, ..) => *loc,
            App(f, a) => f.loc() + a.last().loc(),
        }
    }
}

/// Name binding.
pub type Bind<T = Abs> = common::Bind<T>;

/// Telescopes in the abstract syntax.
pub type AbsTele = Vec<Bind>;

/// Patterns in the abstract syntax.
pub type AbsCopat = Copat<UID, Abs>;
pub type AbsPat = Pat<UID, Abs>;