%{
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 TYPE
%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 }

  | TYPE
	{ Type }

%inline
expr: e = locate(raw_expr) { e }

parse: e = expr; EOF { e }