From 06d52c8ba30b1bd6e1174ebffbd6cc5ba668ecc2 Mon Sep 17 00:00:00 2001
From: Malte Voos <git@mal.tc>
Date: Fri, 16 Feb 2024 00:43:04 +0100
Subject: basic lexer and parser

---
 lib/Parser.mly | 66 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 66 insertions(+)
 create mode 100644 lib/Parser.mly

(limited to 'lib/Parser.mly')

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 }
-- 
cgit 1.4.1