%{
open Vcform

let parse_error = Vcformparsing.parse_error
%}

%token <string> IDENT
%token <string> QIDENT
%token <int> NATLIT
%token ARRAYREAD ARRAYWRITE NEWARRAY ARRAYSIZE
%token FIELDWRITE FIELDREAD
%token AND OR NOT IMPL IFF NULL EMPTYSET
%token METAIMPL
%token NCOLON COLON COLONCOLON SEMICOLON DOT CUP CAP
%token COMMA EQ NEQ 
%token LT GT LTEQ GTEQ 
%token PLUS MINUS TIMES DIVIDE DEREF
%token LPAREN RPAREN LBRACKET RBRACKET LBRACE RBRACE
%token ALBRACKET ARBRACKET
%token TRUE FALSE SET BOOL FORALL EXISTS LAMBDA
%token EOL EOF
%token APPLY
%token BOOL INT VOID UNIVERSE LIST ARRAY SET REF ARROW

%left SEMICOLON
%left COLONCOLON
%nonassoc IFF
%right IMPL
%right METAIMPL
%right OR
%right AND
%right NOT DOT
%nonassoc EQ COLON NCOLON
%nonassoc LT GT LTEQ GTEQ NEQ
%right CUP CAP
%right PLUS MINUS
%nonassoc FORALL EXISTS LAMBDA
%right TIMES DIVIDE
%left APPLY
%left DEREF
%left LIST ARRAY SET
%right ARROW

%start main             /* the entry point */
%type <Vcform.form> main
%%
main:
    form EOF          { $1 }
|   form SEMICOLON    { $1 }
;

factor:
| ARRAYREAD {Const ArrayRead}
| ARRAYWRITE {Const ArrayWrite}
| NEWARRAY {Const NewArray}
| ARRAYSIZE {Const ArraySize}
| FIELDREAD {Const FieldRead}
| FIELDWRITE {Const FieldWrite}
| LPAREN form RPAREN
    {$2}
| LPAREN form COMMA form_comma_list RPAREN
    {mk_tuple ($2 :: $4)}
| QIDENT
    {mk_var $1}
| IDENT
    {mk_var $1}
| IDENT LBRACKET form_no_binder RBRACKET
    %prec DEREF
    {App ((Const ArrayRead), [Var $1;$3])}
| NULL
    {Const NullConst}
| TRUE
    {Const (BoolConst true)}
| FALSE
    {Const (BoolConst false)}
| NATLIT
    {Const (IntConst $1)}
| EMPTYSET
    {Const EmptysetConst}
| LBRACE IDENT DOT form RBRACE
    %prec DOT
    {Binder (Comprehension, [($2, TypeUniverse)], $4)}
| LBRACE form_comma_list RBRACE
    {mk_finite_set $2}
| ALBRACKET form_semicol_list ARBRACKET
    %prec SEMICOLON
    {mk_metaand $2}
  ;

form_no_binder:
| factor {$1}
| NOT form_no_binder
    {App (Const Not, [$2])}
| form_no_binder AND form_no_binder
    {App (Const And, [$1;$3])}
| form_no_binder OR form_no_binder
    {App (Const Or, [$1;$3])}
| form_no_binder IMPL form_no_binder
    {App (Const Impl, [$1;$3])}
| form_no_binder METAIMPL form_no_binder
    {App (Const MetaImpl, [$1;$3])}
| form_no_binder IFF form_no_binder
    {App (Const Iff, [$1;$3])}
| form_no_binder EQ form_no_binder
    {App (Const Eq, [$1;$3])}
| form_no_binder NEQ form_no_binder
    {App (Const Not, [App ((Const Eq), [$1;$3])])}
| form_no_binder LT form_no_binder
    {App (Const Lt, [$1;$3])}
| form_no_binder LTEQ form_no_binder
    {App (Const LtEq, [$1;$3])}
| form_no_binder GT form_no_binder
    {App (Const Gt, [$1;$3])}
| form_no_binder GTEQ form_no_binder
    {App (Const GtEq, [$1;$3])}
| form_no_binder COLON form_no_binder
    {mk_elem($1,$3)}
| form_no_binder NCOLON form_no_binder
    {mk_notelem($1,$3)}
| form_no_binder CUP form_no_binder
    {App (Const Cup, [$1;$3])}
| form_no_binder CAP form_no_binder
    {App (Const Cap, [$1;$3])}
| form_no_binder PLUS form_no_binder
    {App (Const Plus, [$1;$3])}
| form_no_binder MINUS form_no_binder
    {App (Const Minus, [$1;$3])}
| form_no_binder TIMES form_no_binder
    {App (Const Mult, [$1;$3])}
| form_no_binder DIVIDE form_no_binder
    {App (Const Div, [$1;$3])}
| form_no_binder COLONCOLON type_form
    {mk_typedform($1,$3)}
| factor factor_list
    %prec APPLY
    {App($1,$2)}
  ;

form:
| form_no_binder
    {$1}
| FORALL tid_list DOT form 
    %prec DOT
    {Binder (Forall,$2,$4)}
| EXISTS tid_list DOT form 
    %prec DOT
    {Binder (Exists,$2,$4)}
| LAMBDA tid_list DOT form
    %prec DOT
    {Binder (Lambda,$2,$4)}
    ;

tid_list:
| tid {[$1]}
| tid_list tid
    {$1 @ [$2]}
  ;

tid:
| IDENT 
  {($1, TypeUniverse)}
| LPAREN IDENT COLONCOLON type_form RPAREN
  {($2, $4)}

factor_list:
| factor
    {[$1]}
| factor_list factor 
    %prec APPLY
    {$1 @ [$2]}
    ;

form_semicol_list:
| form_no_binder
    {[$1]}
| form_semicol_list SEMICOLON form_no_binder
    {$1 @ [$3]}
    ;

form_comma_list:
| form_no_binder
    {[$1]}
| form_comma_list COMMA form_no_binder
    {$1 @ [$3]}
    ;

type_form: 
| LPAREN type_form RPAREN {$2}
| type_form ARROW type_form {TypeFun ([$1], $3)}
| type_form LIST {TypeList $1}
| type_form SET {TypeSet $1}
| type_form ARRAY {TypeArray $1}
| IDENT REF {TypeObjRef $1}
| BOOL {TypeBool}
| INT {TypeInt}
| VOID {TypeVoid}
| UNIVERSE {TypeUniverse}
| IDENT {mk_typevar $1}