diff options
Diffstat (limited to 'lib/Parser.mly')
| -rw-r--r-- | lib/Parser.mly | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/lib/Parser.mly b/lib/Parser.mly index 5c587b2..d0395ac 100644 --- a/lib/Parser.mly +++ b/lib/Parser.mly @@ -12,7 +12,7 @@ open Ast %token EOF %right ARROW ASTERISK -%left IDENT LPR APP BACKSLASH FST SND BOOL TRUE FALSE BOOL_ELIM +%left IDENT LPR APP BACKSLASH FST SND TYPE BOOL TRUE FALSE BOOL_ELIM %start <Ast.expr> parse @@ -35,15 +35,6 @@ raw_expr: { 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) } @@ -64,6 +55,16 @@ raw_expr: | TYPE { Type } + | 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 } } + %inline expr: e = locate(raw_expr) { e } |