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(Bool), // FIXME
Bool => bx(BoolLit(<>)),
"(" <Expr> ")",
};
|
