%{ 
  open Gui
  open User
%}
%token <string> VAR
%token <string> LVAR
%token COLON
%token COMMA
%token LPAREN
%token RPAREN
%token LBRACKET
%token RBRACKET
%token FUN
%token ARROW
%token ANY
%token EOI
%token DARROW
%token LFUN

/*優先順位と連結性をここに書く(下に行くほど強くなる)*/
%right ARROW

/*開始記号の定義*/
%type <User.Judge.fix_t> start
%type <User.Var.fix_t> vars
%type <User.Term.fix_t> terms
%type <User.TVar.fix_t> tvars
%type <User.Type.fix_t> types
%type <User.Env.fix_t> envs
%start start vars terms tvars types envs

%%

start:
| judge EOI                          {$1}

vars:
| var EOI                            {$1}

terms:
| term EOI                           {$1}

tvars:
| tvar EOI                           {$1}

types:
| typ EOI                            {$1}

envs:
| env EOI                            {$1}

judge:
| term                               {judge empty $1 (Type.make_meta "T")}
| term COLON typ                     {judge empty $1 $3}
| env DARROW term                    {judge $1 $3 (Type.make_meta "T")}
| env DARROW term COLON typ          {judge $1 $3 $5}

term:
| simple_term                        {$1}
| app                                {$1}
| LFUN tvar ARROW term               {term_tabs $2 $4}
| FUN LPAREN var COLON typ RPAREN ARROW term          {term_abs $3 $5 $8}
| FUN var ARROW term                 {term_abs $2 (Type.make_meta "T") $4}

simple_term:
| LVAR                               {Term.make_meta $1}
| VAR                                {term_var (var $1)}
| LPAREN term RPAREN                 {$2}

app:
| simple_term simple_term            {term_app $1 $2}
| app simple_term                    {term_app $1 $2}
| simple_term LBRACKET typ RBRACKET  {term_tapp $1 $3}
| app LBRACKET typ RBRACKET          {term_tapp $1 $3}

var:
| VAR                                {var $1}
| LVAR                               {Var.make_meta $1}

typ:
| LVAR                               {Type.make_meta $1}
| VAR                                {tvar (tv $1)}
| typ ARROW typ                      {tfun $1 $3}
| ANY tvar ARROW typ                 {ut $2 $4}
| LPAREN typ RPAREN                  {$2}

tvar:
| VAR                                {tv $1}
| LVAR                               {TVar.make_meta $1}

env:
| env_c                              {cons $1 empty}
| env_c COMMA env                    {cons $1 $3}
| LPAREN env RPAREN                  {$2}

env_c:
| tvar                               {env_t $1}
| var COLON typ                      {env_e $1 $3}