about summary refs log tree commit diff
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 }