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

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

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

%%

start:
| judge EOI                          {$1}

vars:
| var EOI                            {$1}

terms:
| term EOI                           {$1}

types:
| typ EOI                            {$1}

envs:
| env EOI                            {$1}

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

term:
| simple_term                        {$1}
| app                                {$1}
| FUN var ARROW term                 {term_abs $2 $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}

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

typ:
| LVAR                               {Type.make_meta $1}
| VAR                                {tvar $1}
| typ ARROW typ                      {tfun $1 $3}
| LPAREN typ RPAREN                  {$2}

env:
| LVAR                               {Env.make_meta $1}
| var COLON typ COMMA env            {cons $1 $3 $5}
| var COLON typ                      {cons $1 $3 empty}
| LPAREN env RPAREN                  {$2}