diff options
author | Malte Voos <git@mal.tc> | 2024-02-16 00:43:04 +0100 |
---|---|---|
committer | Malte Voos <git@mal.tc> | 2024-02-16 00:43:04 +0100 |
commit | 06d52c8ba30b1bd6e1174ebffbd6cc5ba668ecc2 (patch) | |
tree | c558e81d84fd12ef66e99c558e5b7dd1322e5c03 /lib/Parser.mly | |
parent | 2bc6cae2458ba5f9573985791536618a00cbed8a (diff) | |
download | toytt-06d52c8ba30b1bd6e1174ebffbd6cc5ba668ecc2.tar.gz toytt-06d52c8ba30b1bd6e1174ebffbd6cc5ba668ecc2.zip |
basic lexer and parser
Diffstat (limited to 'lib/Parser.mly')
-rw-r--r-- | lib/Parser.mly | 66 |
1 files changed, 66 insertions, 0 deletions
diff --git a/lib/Parser.mly b/lib/Parser.mly new file mode 100644 index 0000000..db2a9e2 --- /dev/null +++ b/lib/Parser.mly @@ -0,0 +1,66 @@ +%{ +open Ast +%} + +%token <string> IDENT +%token LPR RPR +%token LBR RBR +%token ARROW ASTERISK BACKSLASH COLON COMMA DOT FATARROW +%token BOOL TRUE FALSE BOOL_ELIM AT +%token FST SND +%token EOF + +%right ARROW ASTERISK +%left IDENT LPR APP BACKSLASH FST SND BOOL TRUE FALSE BOOL_ELIM + +%start <Ast.expr> parse + +%% + +%inline +locate(X): e = X { Asai.Range.locate_lex $loc e } + +%inline +ident: id = locate(IDENT) { id } + +raw_arg: LPR; name = ident; COLON; ty = expr; RPR + { { name; ty } } + +%inline +arg: a = locate(raw_arg) { a } + +raw_expr: + | name = IDENT + { 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) } + | BACKSLASH; a = ident; ARROW; b = expr + { Lam (a, b) } + | a = expr; b = expr %prec APP + { App (a, b) } + + | a = arg; ASTERISK; b = expr + { Sg (a, b) } + | LPR; a = expr; COMMA; b = expr; RPR + { Pair (a, b) } + | FST; p = expr + { Fst p } + | SND; p = expr + { Snd p } + +%inline +expr: e = locate(raw_expr) { e } + +parse: e = expr; EOF { e } |