aboutsummaryrefslogtreecommitdiff
path: root/lib/Parser.mly
diff options
context:
space:
mode:
authorMalte Voos <git@mal.tc>2024-06-23 23:31:59 +0200
committerMalte Voos <git@mal.tc>2024-06-24 00:16:55 +0200
commit5d227bcd0055d02e1d49a3dcd27e80a756923d5b (patch)
treeda468ad3a8f3caf709b731ca2678c86a5a015990 /lib/Parser.mly
parent8d40541003736d5319ec981278338e8c8c66daf6 (diff)
downloadtoytt-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.mly80
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 }