1 files changed, 66 insertions, 0 deletions
diff --git a/lib/Parser.mly b/lib/Parser.mly
new file mode 100644
index 0000000..db2a9e2
--- /dev/null
+++ b/lib/Parser.mly
@@ -0,0 +1,66 @@
+%{
+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 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 }
+
+%inline
+expr: e = locate(raw_expr) { e }
+
+parse: e = expr; EOF { e }