%{
open Lam
open Types
open Proof
open Parser_entry
%}

%token DOT
%token PLUS TIMES
%token TOP BOT EXFALSO TILDE
%token LPAREN RPAREN
%token FUN ARR COLON TARR
%token AND OR
%token <string> VARID
%token <string> TYID

%token GOAL UNDO EXACT ASSUMPTION INTRO INTROS CUT APPLY
%token LEFT RIGHT SPLIT

%token EOL
%right TARR
%right OR
%right AND
%right TILDE

%start main
%type <parser_entry> main
                                                         
%%
main:
  | e=expression EOL { Lam e }
  | t=tactic EOL { Cmd t }

tactic:
  | c=command DOT { c }

command:
  | GOAL t=ty             { Goal t }
  | UNDO                  { Undo }
  | EXACT e=expression    { Tact (Exact_term e) }
  | EXACT s=TYID          { Tact (Exact_proof s) }
  | ASSUMPTION            { Tact (Assumption) }
  | INTROS                { Tact (Intros) }
  | INTRO                 { Tact (Intro) }
  | SPLIT                 { Tact (Split) }
  | RIGHT                 { Tact (Right) }
  | LEFT                  { Tact (Left) }
  | CUT t=ty              { Tact (Cut t) }
  | APPLY s=TYID          { Tact (Apply s) }


ty_annot:
  | id=VARID COLON t=ty     { (id, t) }

ty:
  | id=TYID                 { TVar(id) }
  | BOT                     { Bot }
  | LPAREN t=ty RPAREN      { t }
  | TILDE t=ty              { Arr(t, Bot) }
  | t1=ty AND t2=ty         { And(t1, t2) }
  | t1=ty OR t2=ty          { Or(t1, t2) }
  | t1=ty TARR t2=ty        { Arr(t1, t2) }

expression:
  | FUN LPAREN annot=ty_annot RPAREN ARR e=expression 
                            { Fun (annot, e) }
  | EXFALSO LPAREN e=expression COLON t=ty RPAREN
                            { Exf (e, t) }
  | e=app_expr              { e }

app_expr:
  | e=app_expr a=atomic     { App (e, a) }
  | a=atomic                { a }

atomic:
  | id=VARID                { Var id }
  | LPAREN e=expression RPAREN
                            { e }