From 8d40541003736d5319ec981278338e8c8c66daf6 Mon Sep 17 00:00:00 2001
From: Malte Voos <git@mal.tc>
Date: Sun, 23 Jun 2024 01:36:48 +0200
Subject: keep track of bound names everywhere to be able to output names
 instead of de bruijn indices

---
 lib/Parser.mly | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

(limited to 'lib/Parser.mly')

diff --git a/lib/Parser.mly b/lib/Parser.mly
index fc82d1a..8588b56 100644
--- a/lib/Parser.mly
+++ b/lib/Parser.mly
@@ -5,7 +5,7 @@ open Ast
 %token <string> IDENT
 %token LPR RPR
 %token LBR RBR
-%token ARROW ASTERISK BACKSLASH COLON DOUBLE_COLON COMMA DOT FATARROW
+%token ARROW ASTERISK BACKSLASH COLON DOUBLE_COLON COMMA DOT FATARROW UNDERSCORE
 %token BOOL TRUE FALSE BOOL_ELIM AT
 %token FST SND
 %token TYPE
@@ -28,7 +28,13 @@ raw_ident: id = separated_nonempty_list(DOT, IDENT) { id }
 %inline
 ident: id = locate(raw_ident) { id }
 
-arg: LPR; name = ident; COLON; tp = expr; RPR
+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:
@@ -41,7 +47,7 @@ raw_expr:
 
   | a = arg; ARROW; b = expr
 	{ Pi (a, b) }
-  | BACKSLASH; a = ident; ARROW; b = expr
+  | BACKSLASH; a = local_name; ARROW; b = expr
 	{ Lam (a, b) }
   | a = expr; b = expr %prec APP
 	{ App (a, b) }
@@ -64,7 +70,7 @@ raw_expr:
 	{ True }
   | FALSE
 	{ False }
-  | BOOL_ELIM; scrut = expr; AT; motive_var = ident; ARROW; motive_body = expr;
+  | 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 } }
 
-- 
cgit 1.4.1