%{
    open Structs;;
    open Tactic;;
%}

/* Description des lexèmes définis dans lexer.mll */
%token LPAREN RPAREN RARROW TILDE LAND LOR COMMA FALSE TRUE
%token EOF

%token <string> VAR_NAME
%token <string> TYPE_NAME

%token DOT INTRO ASSUMPTION APPLY ELIM CUT SPLIT LEFT RIGHT FST SND IG ID CASE
%token FUN MAPS_TO VDOTS EXF

%token AMPERSAND

/* L'ordre de définition définit la priorité */
%right RARROW
%nonassoc TILDE
%left LAND
%left LOR

%start main_type
%type <Structs.ty> main_type

%start main_tactic
%type <Tactic.tactic> main_tactic

%start main_lambda
%type <Structs.lam> main_lambda

%start main_two_lambda
%type <Structs.lam * Structs.lam> main_two_lambda

%%
main_type:
  | ty EOF                                { $1 }

main_tactic:
  | tactic EOF                            { $1 }

main_lambda:
  | lambda EOF                            { $1 }

main_two_lambda:
  | lambda AMPERSAND lambda               { $1, $3 }

/* Types */
ty:
  | LPAREN ty RPAREN                      { $2 }
  | ty RARROW ty                          { TImpl ($1, $3) }
  | TYPE_NAME                             { TSimple $1 }
  | TILDE ty                              { TImpl ($2, TFalse) }
  | ty LAND ty                            { TAnd($1, $3) }
  | ty LOR ty                             { TOr($1, $3) }
  | FALSE                                 { TFalse }
  | TRUE                                  { TTrue }

/* Tactiques */
tactic:
  | INTRO VAR_NAME DOT                    { Intro $2 }
  | ASSUMPTION DOT                        { Assumption }
  | APPLY VAR_NAME DOT                    { Apply $2 }
  | ELIM VAR_NAME DOT                     { Elim $2 }
  | CUT ty DOT                            { Cut $2 }
  | SPLIT DOT                             { Split None }
  | SPLIT VAR_NAME DOT                    { Split (Some $2) }
  | LEFT DOT                              { Left }
  | RIGHT DOT                             { Right }
  
/* Lambda-termes */
lambda_arg: /* Expression pouvant être en argument d'une fonction */
  | VAR_NAME                              { LVar $1 }
  | LPAREN lambda RPAREN                  { $2 }

/* Application d'une fonction */
lambda_app:
  | lambda_app lambda_arg                 { LApp ($1, $2) }
  | lambda_arg                            { $1 }

lambda:
  | lambda_app                            { $1 }
  | FUN VAR_NAME VDOTS ty MAPS_TO lambda  { LFun ($2, $4, $6) }
  | FUN LPAREN VAR_NAME VDOTS ty RPAREN MAPS_TO lambda
                                          { LFun ($3, $5, $8) }
  | EXF LPAREN VAR_NAME VDOTS ty RPAREN   { LExf (LVar $3, $5) }