summaryrefslogtreecommitdiff
path: root/src/grammar.lalrpop
blob: 8a4ad83b6806278450356c619273b08b53e13742 (plain)
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
use core;
use core::Expr::*;
use grammar_util::*;
use lexer::{Builtin, Keyword, LexicalError, Tok};

grammar;

extern {
    type Location = usize;
    type Error = LexicalError;

    enum Tok {
        Pi => Tok::Pi,
        Lambda => Tok::Lambda,
        Combine => Tok::Combine,
        "->" => Tok::Arrow,

        Int => Tok::Integer(<isize>),
        Nat => Tok::Natural(<usize>),
        Bool => Tok::Bool(<bool>),
        Label => Tok::Identifier(<String>),
        Let => Tok::Keyword(Keyword::Let),
        In => Tok::Keyword(Keyword::In),
        If => Tok::Keyword(Keyword::If),
        Then => Tok::Keyword(Keyword::Then),
        Else => Tok::Keyword(Keyword::Else),
        Builtin => Tok::Builtin(<Builtin>),

        "(" => Tok::ParenL,
        ")" => Tok::ParenR,
        "&&" => Tok::BoolAnd,
        "||" => Tok::BoolOr,
        "==" => Tok::CompareEQ,
        "!=" => Tok::CompareNE,
        "++" => Tok::Append,
        "*" => Tok::Times,
        "+" => Tok::Plus,
        "." => Tok::Dot,
        ":" => Tok::Ascription,
        "=" => Tok::Equals,
    }
}

pub Expr: BoxExpr = { // exprA
    <ExprB> ":" <Expr> => bx(Annot(<>)),
    ExprB,
};

ExprB: BoxExpr = {
    Lambda "(" <Label> ":" <Expr> ")" "->" <ExprB> => bx(Lam(<>)),
    Pi "(" <Label> ":" <Expr> ")" "->" <ExprB> => bx(Pi(<>)),
    If <Expr> Then <ExprB> Else <ExprC> => bx(BoolIf(<>)),
    <ExprC> "->" <ExprB> => bx(Pi("_".to_owned(), <>)),
    Let <Label> <(":" <Expr>)?> "=" <Expr> In <ExprB> => bx(Let(<>)),
    ExprC,
};

BoolOr: ExprOpFn = { "||" => BoolOr };
NaturalPlus: ExprOpFn = { "+" => NaturalPlus };
TextAppend: ExprOpFn = { "++" => TextAppend };
BoolAnd: ExprOpFn = { "&&" => BoolAnd };
CombineOp: ExprOpFn = { Combine => Combine };
NaturalTimes: ExprOpFn = { "*" => NaturalTimes };
BoolEQ: ExprOpFn = { "==" => BoolEQ };
BoolNE: ExprOpFn = { "!=" => BoolNE };

Tier<NextTier, Op>: BoxExpr = {
    <a:NextTier> <f:Op> <b:Tier<NextTier, Op>> => bx(f(a, b)),
    // <b:Tier<NextTier, Op>> <f:Op> <a:NextTier> => bx(f(a, b)),
    NextTier,
};

ExprC = Tier<ExprC1, BoolOr>;
ExprC1 = Tier<ExprC2, NaturalPlus>;
ExprC2 = Tier<ExprC3, TextAppend>;
ExprC3 = Tier<ExprC4, BoolAnd>;
ExprC4 = Tier<ExprC5, CombineOp>;
ExprC5 = Tier<ExprC6, NaturalTimes>;
ExprC6 = Tier<ExprC7, BoolEQ>;
ExprC7 = Tier<ExprD, BoolNE>;

ExprD: BoxExpr = {
    <v:(ExprE)+> => {
        let mut it = v.into_iter();
        let f = it.next().unwrap();
        it.fold(f, |f, x| bx(App(f, x)))
    }
};

ExprE: BoxExpr = {
    <a:ExprF> <fields:("." <Label>)*> => {
        fields.into_iter().fold(a, |x, f| bx(Field(x, f)))
    },
};

ExprF: BoxExpr = {
    Nat => bx(NaturalLit(<>)),
    Int => bx(IntegerLit(<>)),
    Label => bx(Var(core::Var(<>, 0))), // FIXME support var@n syntax
    Builtin => bx(builtin_expr(<>)),
    Bool => bx(BoolLit(<>)),
    "(" <Expr> ")",
};