diff options
| author | Malte Voos <git@mal.tc> | 2024-02-19 12:57:26 +0100 |
|---|---|---|
| committer | Malte Voos <git@mal.tc> | 2024-02-19 16:54:45 +0100 |
| commit | 407a2a4a0a440c41adc19fbe8b67283b7b7c65ab (patch) | |
| tree | c55ed80f1a90741e547c0b3fa102f5f709aa1836 /lib/Parser.mly | |
| parent | 169ff6c0d196246e28c4413b43895ad5a377a2e5 (diff) | |
| download | toytt-407a2a4a0a440c41adc19fbe8b67283b7b7c65ab.tar.gz toytt-407a2a4a0a440c41adc19fbe8b67283b7b7c65ab.zip | |
core syntax, semantic domain, evaluation
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 } |