From 04d62df9fdd42c603fad7bb1b5e3fb49bf8550c1 Mon Sep 17 00:00:00 2001
From: Malte Voos <git@mal.tc>
Date: Mon, 17 Jun 2024 17:41:38 +0200
Subject: implement typechecking

---
 lib/Parser.mly | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

(limited to 'lib/Parser.mly')

diff --git a/lib/Parser.mly b/lib/Parser.mly
index 0390b3c..fc82d1a 100644
--- a/lib/Parser.mly
+++ b/lib/Parser.mly
@@ -5,13 +5,15 @@ open Ast
 %token <string> IDENT
 %token LPR RPR
 %token LBR RBR
-%token ARROW ASTERISK BACKSLASH COLON COMMA DOT FATARROW
+%token ARROW ASTERISK BACKSLASH COLON DOUBLE_COLON COMMA DOT FATARROW
 %token BOOL TRUE FALSE BOOL_ELIM AT
 %token FST SND
 %token TYPE
 %token EOF
 
-%right ARROW ASTERISK
+%nonassoc DOUBLE_COLON
+%right ARROW
+%right ASTERISK
 %left IDENT LPR APP BACKSLASH FST SND TYPE BOOL TRUE FALSE BOOL_ELIM
 
 %start <Ast.expr> parse
@@ -19,24 +21,23 @@ open Ast
 %%
 
 %inline
-locate(X): e = X { Asai.Range.locate_lex $loc e }
+locate(X): e = X { Asai.Range.locate_lex ~source:(ParserEff.Eff.read()) $loc e }
 
 raw_ident: id = separated_nonempty_list(DOT, IDENT) { id }
 
 %inline
 ident: id = locate(raw_ident) { id }
 
-raw_arg: LPR; name = ident; COLON; ty = expr; RPR
-	{ { name; ty } }
-
-%inline
-arg: a = locate(raw_arg) { a }
+arg: LPR; name = ident; 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) }
-- 
cgit 1.4.1