%{
open Ast
%}

%token <string> IDENT
%token LPR RPR
%token LBR RBR
%token ARROW ASSIGN ASTERISK BACKSLASH COLON DOUBLE_COLON COMMA DOT FATARROW UNDERSCORE
%token DEF
%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> start_expr
%start <Ast.file> start_file

%%

%inline
locate(X): e = X { Asai.Range.locate_lex ~source:(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) }
  | a = expr; ARROW; b = expr
    { Fun (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) }
  | a = expr; ASTERISK; b = expr
	{ Prod (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 }

item:
  | DEF; name = ident; args = list(arg); COLON; tp = expr; ASSIGN; tm = expr
    { Def { name; args; tp; tm } }

file: items = list(item) { items }

start_expr: e = expr; EOF { e }
start_file: f = file; EOF { f }