aboutsummaryrefslogtreecommitdiff
path: root/lib/Parser.mly
diff options
context:
space:
mode:
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 }