-- This Happy file was machine-generated by the BNF converter
{
{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns #-}
module Tip.Parser.ParTIP where
import Tip.Parser.AbsTIP
import Tip.Parser.LexTIP
import Tip.Parser.ErrM

}

%name pStart Start
%name pListDecl ListDecl
%name pDecl Decl
%name pAssertion Assertion
%name pPar Par
%name pConstDecl ConstDecl
%name pFunDecl FunDecl
%name pFunDef FunDef
%name pFunDec FunDec
%name pInnerFunDec InnerFunDec
%name pDatatype Datatype
%name pConstructor Constructor
%name pBinding Binding
%name pLetDecl LetDecl
%name pType Type
%name pExpr Expr
%name pBinder Binder
%name pCase Case
%name pPattern Pattern
%name pHead Head
%name pListLetDecl ListLetDecl
%name pListCase ListCase
%name pListExpr ListExpr
%name pListDatatype ListDatatype
%name pListConstructor ListConstructor
%name pListBinding ListBinding
%name pListSymbol ListSymbol
%name pListType ListType
%name pListFunDecl ListFunDecl
%name pListFunDef ListFunDef
%name pListFunDec ListFunDec

-- no lexer declaration
%monad { Err } { thenM } { returnM }
%tokentype { Token }

%token
  '(' { PT _ (TS _ 1) }
  ')' { PT _ (TS _ 2) }
  '*' { PT _ (TS _ 3) }
  '+' { PT _ (TS _ 4) }
  '-' { PT _ (TS _ 5) }
  '<' { PT _ (TS _ 6) }
  '<=' { PT _ (TS _ 7) }
  '=' { PT _ (TS _ 8) }
  '=>' { PT _ (TS _ 9) }
  '>' { PT _ (TS _ 10) }
  '>=' { PT _ (TS _ 11) }
  '@' { PT _ (TS _ 12) }
  'Bool' { PT _ (TS _ 13) }
  'Int' { PT _ (TS _ 14) }
  'and' { PT _ (TS _ 15) }
  'as' { PT _ (TS _ 16) }
  'assert' { PT _ (TS _ 17) }
  'assert-not' { PT _ (TS _ 18) }
  'case' { PT _ (TS _ 19) }
  'check-sat' { PT _ (TS _ 20) }
  'declare-const' { PT _ (TS _ 21) }
  'declare-datatypes' { PT _ (TS _ 22) }
  'declare-fun' { PT _ (TS _ 23) }
  'declare-sort' { PT _ (TS _ 24) }
  'default' { PT _ (TS _ 25) }
  'define-fun' { PT _ (TS _ 26) }
  'define-fun-rec' { PT _ (TS _ 27) }
  'define-funs-rec' { PT _ (TS _ 28) }
  'distinct' { PT _ (TS _ 29) }
  'div' { PT _ (TS _ 30) }
  'exists' { PT _ (TS _ 31) }
  'false' { PT _ (TS _ 32) }
  'forall' { PT _ (TS _ 33) }
  'ite' { PT _ (TS _ 34) }
  'lambda' { PT _ (TS _ 35) }
  'let' { PT _ (TS _ 36) }
  'match' { PT _ (TS _ 37) }
  'mod' { PT _ (TS _ 38) }
  'not' { PT _ (TS _ 39) }
  'or' { PT _ (TS _ 40) }
  'par' { PT _ (TS _ 41) }
  'true' { PT _ (TS _ 42) }

L_integ  { PT _ (TI $$) }
L_Symbol { PT _ (T_Symbol _) }


%%

Integer :: { Integer } : L_integ  { (read ( $1)) :: Integer }
Symbol    :: { Symbol} : L_Symbol { Symbol (mkPosToken $1)}

Start :: { Start }
Start : ListDecl { Start $1 } 


ListDecl :: { [Decl] }
ListDecl : '(' 'check-sat' ')' { [] } 
  | '(' Decl ')' ListDecl { (:) $2 $4 }


Decl :: { Decl }
Decl : 'declare-datatypes' '(' ListSymbol ')' '(' ListDatatype ')' { DeclareDatatypes (reverse $3) (reverse $6) } 
  | 'declare-sort' Symbol Integer { DeclareSort $2 $3 }
  | 'declare-const' ConstDecl { DeclareConst $2 }
  | 'declare-const' '(' Par '(' ConstDecl ')' ')' { DeclareConstPar $3 $5 }
  | 'declare-fun' FunDecl { DeclareFun $2 }
  | 'declare-fun' '(' Par '(' FunDecl ')' ')' { DeclareFunPar $3 $5 }
  | 'define-fun' FunDef { DefineFun $2 }
  | 'define-fun' '(' Par '(' FunDef ')' ')' { DefineFunPar $3 $5 }
  | 'define-fun-rec' FunDef { DefineFunRec $2 }
  | 'define-fun-rec' '(' Par '(' FunDef ')' ')' { DefineFunRecPar $3 $5 }
  | 'define-funs-rec' '(' ListFunDec ')' '(' ListExpr ')' { DefineFunsRec (reverse $3) (reverse $6) }
  | Assertion Expr { Assert $1 $2 }
  | Assertion '(' Par Expr ')' { AssertPar $1 $3 $4 }


Assertion :: { Assertion }
Assertion : 'assert' { AssertIt } 
  | 'assert-not' { AssertNot }


Par :: { Par }
Par : 'par' '(' ListSymbol ')' { Par (reverse $3) } 


ConstDecl :: { ConstDecl }
ConstDecl : Symbol Type { ConstDecl $1 $2 } 


FunDecl :: { FunDecl }
FunDecl : Symbol '(' ListType ')' Type { FunDecl $1 (reverse $3) $5 } 


FunDef :: { FunDef }
FunDef : Symbol '(' ListBinding ')' Type Expr { FunDef $1 (reverse $3) $5 $6 } 


FunDec :: { FunDec }
FunDec : '(' Par InnerFunDec ')' { ParFunDec $2 $3 } 
  | InnerFunDec { MonoFunDec $1 }


InnerFunDec :: { InnerFunDec }
InnerFunDec : '(' Symbol '(' ListBinding ')' Type ')' { InnerFunDec $2 (reverse $4) $6 } 


Datatype :: { Datatype }
Datatype : '(' Symbol ListConstructor ')' { Datatype $2 (reverse $3) } 


Constructor :: { Constructor }
Constructor : '(' Symbol ListBinding ')' { Constructor $2 (reverse $3) } 


Binding :: { Binding }
Binding : '(' Symbol Type ')' { Binding $2 $3 } 


LetDecl :: { LetDecl }
LetDecl : '(' Symbol Expr ')' { LetDecl $2 $3 } 


Type :: { Type }
Type : Symbol { TyVar $1 } 
  | '(' Symbol ListType ')' { TyApp $2 (reverse $3) }
  | '(' '=>' ListType ')' { ArrowTy (reverse $3) }
  | 'Int' { IntTy }
  | 'Bool' { BoolTy }


Expr :: { Expr }
Expr : Symbol { Var $1 } 
  | '(' 'as' Expr Type ')' { As $3 $4 }
  | '(' Head ListExpr ')' { App $2 (reverse $3) }
  | '(' 'match' Expr ListCase ')' { Match $3 (reverse $4) }
  | '(' 'let' '(' ListLetDecl ')' Expr ')' { Let (reverse $4) $6 }
  | '(' Binder '(' ListBinding ')' Expr ')' { Binder $2 (reverse $4) $6 }
  | Integer { LitInt $1 }
  | '-' Integer { LitNegInt $2 }
  | 'true' { LitTrue }
  | 'false' { LitFalse }


Binder :: { Binder }
Binder : 'lambda' { Lambda } 
  | 'forall' { Forall }
  | 'exists' { Exists }


Case :: { Case }
Case : '(' 'case' Pattern Expr ')' { Case $3 $4 } 


Pattern :: { Pattern }
Pattern : 'default' { Default } 
  | '(' Symbol ListSymbol ')' { ConPat $2 (reverse $3) }
  | Symbol { SimplePat $1 }


Head :: { Head }
Head : Symbol { Const $1 } 
  | '@' { At }
  | 'ite' { IfThenElse }
  | 'and' { And }
  | 'or' { Or }
  | 'not' { Not }
  | '=>' { Implies }
  | '=' { Equal }
  | 'distinct' { Distinct }
  | '+' { IntAdd }
  | '-' { IntSub }
  | '*' { IntMul }
  | 'div' { IntDiv }
  | 'mod' { IntMod }
  | '>' { IntGt }
  | '>=' { IntGe }
  | '<' { IntLt }
  | '<=' { IntLe }


ListLetDecl :: { [LetDecl] }
ListLetDecl : {- empty -} { [] } 
  | ListLetDecl LetDecl { flip (:) $1 $2 }


ListCase :: { [Case] }
ListCase : {- empty -} { [] } 
  | ListCase Case { flip (:) $1 $2 }


ListExpr :: { [Expr] }
ListExpr : {- empty -} { [] } 
  | ListExpr Expr { flip (:) $1 $2 }


ListDatatype :: { [Datatype] }
ListDatatype : {- empty -} { [] } 
  | ListDatatype Datatype { flip (:) $1 $2 }


ListConstructor :: { [Constructor] }
ListConstructor : {- empty -} { [] } 
  | ListConstructor Constructor { flip (:) $1 $2 }


ListBinding :: { [Binding] }
ListBinding : {- empty -} { [] } 
  | ListBinding Binding { flip (:) $1 $2 }


ListSymbol :: { [Symbol] }
ListSymbol : {- empty -} { [] } 
  | ListSymbol Symbol { flip (:) $1 $2 }


ListType :: { [Type] }
ListType : {- empty -} { [] } 
  | ListType Type { flip (:) $1 $2 }


ListFunDecl :: { [FunDecl] }
ListFunDecl : {- empty -} { [] } 
  | ListFunDecl FunDecl { flip (:) $1 $2 }


ListFunDef :: { [FunDef] }
ListFunDef : {- empty -} { [] } 
  | ListFunDef FunDef { flip (:) $1 $2 }


ListFunDec :: { [FunDec] }
ListFunDec : {- empty -} { [] } 
  | ListFunDec FunDec { flip (:) $1 $2 }



{

returnM :: a -> Err a
returnM = return

thenM :: Err a -> (a -> Err b) -> Err b
thenM = (>>=)

happyError :: [Token] -> Err a
happyError ts =
  Bad $ "syntax error at " ++ tokenPos ts ++ 
  case ts of
    [] -> []
    [Err _] -> " due to lexer error"
    _ -> " before " ++ unwords (map (id . prToken) (take 4 ts))

myLexer = tokens
}