diff options
Diffstat (limited to 'lib/Parser.mly')
| -rw-r--r-- | lib/Parser.mly | 14 |
1 files changed, 10 insertions, 4 deletions
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 } } |