From 407a2a4a0a440c41adc19fbe8b67283b7b7c65ab Mon Sep 17 00:00:00 2001 From: Malte Voos Date: Mon, 19 Feb 2024 12:57:26 +0100 Subject: core syntax, semantic domain, evaluation --- lib/Parser.mly | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) (limited to 'lib/Parser.mly') 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 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 } -- cgit 1.4.1