1 files changed, 80 insertions, 0 deletions
diff --git a/src/parser/Grammar.mly b/src/parser/Grammar.mly
new file mode 100644
index 0000000..bb98029
--- /dev/null
+++ b/src/parser/Grammar.mly
@@ -0,0 +1,80 @@
+%{
+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) }
+  | 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) }
+  | 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 }