blob: 5c587b29fa12a84899d5a52a50394e08d789df6f (
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
|
%{
open Ast
%}
%token <string> IDENT
%token LPR RPR
%token LBR RBR
%token ARROW ASTERISK BACKSLASH COLON COMMA DOT FATARROW
%token BOOL TRUE FALSE BOOL_ELIM AT
%token FST SND
%token TYPE
%token EOF
%right ARROW ASTERISK
%left IDENT LPR APP BACKSLASH FST SND BOOL TRUE FALSE BOOL_ELIM
%start <Ast.expr> parse
%%
%inline
locate(X): e = X { Asai.Range.locate_lex $loc e }
%inline
ident: id = locate(IDENT) { id }
raw_arg: LPR; name = ident; COLON; ty = expr; RPR
{ { name; ty } }
%inline
arg: a = locate(raw_arg) { a }
raw_expr:
| name = IDENT
{ Var name }
| LPR; e = raw_expr; RPR
{ e }
| BOOL
{ Bool }
| TRUE
{ True }
| FALSE
{ False }
| BOOL_ELIM; scrut = expr; AT; motive_var = ident; ARROW; motive_body = expr;
LBR; TRUE; FATARROW; true_case = expr; COMMA; FALSE; FATARROW; false_case = expr; RBR
{ BoolElim { motive_var; motive_body; true_case; false_case; scrut } }
| a = arg; ARROW; b = expr
{ Pi (a, b) }
| BACKSLASH; a = ident; ARROW; b = expr
{ Lam (a, b) }
| a = expr; b = expr %prec APP
{ App (a, b) }
| a = arg; ASTERISK; b = expr
{ Sg (a, b) }
| LPR; a = expr; COMMA; b = expr; RPR
{ Pair (a, b) }
| FST; p = expr
{ Fst p }
| SND; p = expr
{ Snd p }
| TYPE
{ Type }
%inline
expr: e = locate(raw_expr) { e }
parse: e = expr; EOF { e }
|