{
module Parser where
import Lex
}

%name getProg Prog
%name getType Type
%name getAx AxList

%tokentype { Token }

%token

nz         { TokenZero }
num        { TokenNum $$ }
var        { TokenVar $$ }
lam        { TokenLam }
':'        { TokenCol }
';'        { TokenSemicol }
'.'        { TokenDot }
'{'        { TokenCBOpen }
'}'        { TokenCBClose }
'('        { TokenPAROpen }
')'        { TokenPARClose }
','        { TokenCom }
prime      { TokenPrime }
'+'        { TokenPlus }
fix        { TokenFix }
proj       { TokenProj }
inj        { TokenInj }
case       { TokenCase }
if         { TokenIf }
'='        { TokenEqual }
'<'        { TokenLess }
else       { TokenElse }
inx        { TokenInx }
casx       { TokenCasx }
of         { TokenOf }

'#'        { TokenNat }
arr        { TokenArrow }
'&'        { TokenAnd }
'|'        { TokenOr }
'!'        { TokenUnivQ }
'?'        { TokenExistQ }

%right arr
%right '|'
%right '&'
%nonassoc '<'
%nonassoc '='
%left APP
%left '+'
%nonassoc prime


%%

Prog    : num                             { numToTerm $1 }
        | Prog prime                      { Succ $1 }
        | Prog '+' Prog                   { Plus $1 $3 }
        | var                             { Var $1 }
        | lam var ':' Type '.' Prog       { Abs $2 $4 $6 }
        | Prog Prog  %prec APP            { App $1 $2 }
        | '(' Prog ')'                    { $2 }
        | fix var ':' Type '.' Prog       { Fix $2 $4 $6 }
        | '{' PList '}'                   { PSum $2 }
        | proj num Prog                   { Proj $2 $3 }
        | inj num Prog                    { Inj $2 $3 }
        | case Prog arr '(' PList ')'     { Case $2 $5 }
        | inx Prog arr Prog               { Inx $2 $4 }
        | casx Prog arr Prog              { Casx $2 $4 }
      | case Prog of nz arr Prog '|' var prime arr Prog { Casz $2 $6 $8 $11 }

PList   : {- empty -}                     { [] }
        | PList1                          { $1 }
PList1  : Prog                            { [$1] }
        | Prog ',' PList                  { $1:$3 }

Type    : '#'                             { Nat }
	| var				  { TypeVar $1 }
        | var '(' PList ')'               { Pred $1 $3 }
        | Type arr Type			  { TArrow $1 $3 }
        | T_and                           { T_And $1 }
        | T_or                            { T_Or $1 }
        | '!' var '.' Type                { TUniv $2 $4 }
        | '?' var '.' Type                { TExist $2 $4 }
        | Prog '=' Prog                   { T_Equal  $1 $3 }
        | Prog '<' Prog                   { T_Less   $1 $3 }
	| '(' Type ')'			  { $2 }

T_and   : Type '&' T_and                  { $1:$3 }
        | Type '&' Type                   { [$1,$3] }
T_or    : Type '|' T_or                   { $1:$3 }
        | Type '|' Type                   { [$1,$3] }

Ax1     : var ':' Type ';'                { Axiom $1 $3 }
AxList  : {- empty -}                     { [] }
        | Ax1 AxList                      { $1:$2 }

{

happyError :: [Token] -> a
happyError _ = error "Happy Parse Error!"

  
data Prog = Zero
          | Succ Prog
          | Var String
          | Abs String Type Prog
          | App Prog Prog
          | Fix String Type Prog
          | If String Int Prog Prog
          | PSum [Prog]
          | Proj Int Prog
          | Inj Int Prog
          | Case Prog [Prog]
          | Inx Prog Prog
          | Casx Prog Prog
          | Casz Prog Prog String Prog
          | Plus Prog Prog
          | Axiom String Type
      deriving Show

data Type = Nat
	  | TypeVar String
          | Pred String [Prog]
          | TArrow Type Type
          | T_And [Type]
          | T_Or  [Type]
          | TUniv String Type
          | TExist String Type
          | T_Equal Prog Prog
          | T_Less Prog Prog
      deriving Show


numToTerm :: Int -> Prog
numToTerm n = if n==0 then Zero else (Succ (numToTerm (n-1)))

}