blob: d8e9ee0eb18c08de8e00ef06a16ed3d3d9dd41e1 (
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
|
%{
open Ast
%}
%token <string> IDENT
%token LPR RPR
%token LBR RBR
%token ARROW ASTERISK BACKSLASH COLON DOUBLE_COLON COMMA DOT FATARROW UNDERSCORE
%token BOOL TRUE FALSE BOOL_ELIM AT
%token FST SND
%token TYPE
%token EOF
%nonassoc DOUBLE_COLON
%right ARROW
%right ASTERISK
%left IDENT LPR APP BACKSLASH FST SND TYPE BOOL TRUE FALSE BOOL_ELIM
%start <Ast.expr> start_expr
%%
%inline
locate(X): e = X { Asai.Range.locate_lex ~source:(Eff.read()) $loc e }
raw_ident: id = separated_nonempty_list(DOT, IDENT) { id }
%inline
ident: id = locate(raw_ident) { id }
raw_local_name:
| name = IDENT { Some name }
| UNDERSCORE { None }
local_name: name = locate(raw_local_name) { name }
arg: LPR; name = local_name; COLON; tp = expr; RPR
{ (name, tp) }
raw_expr:
| name = raw_ident
{ Var name }
| LPR; e = raw_expr; RPR
{ e }
| tm = expr; DOUBLE_COLON; tp = expr
{ Check (tm, tp) }
| a = arg; ARROW; b = expr
{ Pi (a, b) }
| a = expr; ARROW; b = expr
{ Fun (a, b) }
| BACKSLASH; a = local_name; ARROW; b = expr
{ Lam (a, b) }
| a = expr; b = expr %prec APP
{ App (a, b) }
| a = arg; ASTERISK; b = expr
{ Sg (a, b) }
| a = expr; ASTERISK; b = expr
{ Prod (a, b) }
| LPR; a = expr; COMMA; b = expr; RPR
{ Pair (a, b) }
| FST; p = expr
{ Fst p }
| SND; p = expr
{ Snd p }
| TYPE
{ Type }
| BOOL
{ Bool }
| TRUE
{ True }
| FALSE
{ False }
| BOOL_ELIM; scrut = expr; AT; motive_var = local_name; 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 } }
%inline
expr: e = locate(raw_expr) { e }
start_expr: e = expr; EOF { e }
|