diff options
author | Malte Voos <git@mal.tc> | 2024-06-23 23:31:59 +0200 |
---|---|---|
committer | Malte Voos <git@mal.tc> | 2024-06-24 00:16:55 +0200 |
commit | 5d227bcd0055d02e1d49a3dcd27e80a756923d5b (patch) | |
tree | da468ad3a8f3caf709b731ca2678c86a5a015990 /lib/Parser.mly | |
parent | 8d40541003736d5319ec981278338e8c8c66daf6 (diff) | |
download | toytt-5d227bcd0055d02e1d49a3dcd27e80a756923d5b.tar.gz toytt-5d227bcd0055d02e1d49a3dcd27e80a756923d5b.zip |
split code into smaller libraries and make a better repl
Diffstat (limited to 'lib/Parser.mly')
-rw-r--r-- | lib/Parser.mly | 80 |
1 files changed, 0 insertions, 80 deletions
diff --git a/lib/Parser.mly b/lib/Parser.mly deleted file mode 100644 index 8588b56..0000000 --- a/lib/Parser.mly +++ /dev/null @@ -1,80 +0,0 @@ -%{ -open Ast -%} - -%token <string> IDENT -%token LPR RPR -%token LBR RBR -%token ARROW ASTERISK BACKSLASH COLON DOUBLE_COLON COMMA DOT FATARROW UNDERSCORE -%token BOOL TRUE FALSE BOOL_ELIM AT -%token FST SND -%token TYPE -%token EOF - -%nonassoc DOUBLE_COLON -%right ARROW -%right ASTERISK -%left IDENT LPR APP BACKSLASH FST SND TYPE BOOL TRUE FALSE BOOL_ELIM - -%start <Ast.expr> parse - -%% - -%inline -locate(X): e = X { Asai.Range.locate_lex ~source:(ParserEff.Eff.read()) $loc e } - -raw_ident: id = separated_nonempty_list(DOT, IDENT) { id } - -%inline -ident: id = locate(raw_ident) { id } - -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: - | name = raw_ident - { Var name } - | LPR; e = raw_expr; RPR - { e } - | tm = expr; DOUBLE_COLON; tp = expr - { Check (tm, tp) } - - | a = arg; ARROW; b = expr - { Pi (a, b) } - | BACKSLASH; a = local_name; 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 } - - | TYPE - { Type } - - | BOOL - { Bool } - | TRUE - { True } - | FALSE - { False } - | 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 } } - -%inline -expr: e = locate(raw_expr) { e } - -parse: e = expr; EOF { e } |