module Tip.Parser.AbsTIP where

-- Haskell module generated by the BNF converter




newtype Symbol = Symbol ((Int,Int),String) deriving (Eq,Ord,Show,Read)
data Start =
   Start [Decl]
  deriving (Eq,Ord,Show,Read)

data Decl =
   DeclareDatatypes [Symbol] [Datatype]
 | DeclareSort Symbol Integer
 | DeclareConst ConstDecl
 | DeclareConstPar Par ConstDecl
 | DeclareFun FunDecl
 | DeclareFunPar Par FunDecl
 | DefineFun FunDef
 | DefineFunPar Par FunDef
 | DefineFunRec FunDef
 | DefineFunRecPar Par FunDef
 | DefineFunsRec [FunDec] [Expr]
 | Assert Assertion Expr
 | AssertPar Assertion Par Expr
  deriving (Eq,Ord,Show,Read)

data Assertion =
   AssertIt
 | AssertNot
  deriving (Eq,Ord,Show,Read)

data Par =
   Par [Symbol]
  deriving (Eq,Ord,Show,Read)

data ConstDecl =
   ConstDecl Symbol Type
  deriving (Eq,Ord,Show,Read)

data FunDecl =
   FunDecl Symbol [Type] Type
  deriving (Eq,Ord,Show,Read)

data FunDef =
   FunDef Symbol [Binding] Type Expr
  deriving (Eq,Ord,Show,Read)

data FunDec =
   ParFunDec Par InnerFunDec
 | MonoFunDec InnerFunDec
  deriving (Eq,Ord,Show,Read)

data InnerFunDec =
   InnerFunDec Symbol [Binding] Type
  deriving (Eq,Ord,Show,Read)

data Datatype =
   Datatype Symbol [Constructor]
  deriving (Eq,Ord,Show,Read)

data Constructor =
   Constructor Symbol [Binding]
  deriving (Eq,Ord,Show,Read)

data Binding =
   Binding Symbol Type
  deriving (Eq,Ord,Show,Read)

data LetDecl =
   LetDecl Symbol Expr
  deriving (Eq,Ord,Show,Read)

data Type =
   TyVar Symbol
 | TyApp Symbol [Type]
 | ArrowTy [Type]
 | IntTy
 | BoolTy
  deriving (Eq,Ord,Show,Read)

data Expr =
   Var Symbol
 | As Expr Type
 | App Head [Expr]
 | Match Expr [Case]
 | Let [LetDecl] Expr
 | Binder Binder [Binding] Expr
 | LitInt Integer
 | LitNegInt Integer
 | LitTrue
 | LitFalse
  deriving (Eq,Ord,Show,Read)

data Binder =
   Lambda
 | Forall
 | Exists
  deriving (Eq,Ord,Show,Read)

data Case =
   Case Pattern Expr
  deriving (Eq,Ord,Show,Read)

data Pattern =
   Default
 | ConPat Symbol [Symbol]
 | SimplePat Symbol
  deriving (Eq,Ord,Show,Read)

data Head =
   Const Symbol
 | At
 | IfThenElse
 | And
 | Or
 | Not
 | Implies
 | Equal
 | Distinct
 | IntAdd
 | IntSub
 | IntMul
 | IntDiv
 | IntMod
 | IntGt
 | IntGe
 | IntLt
 | IntLe
  deriving (Eq,Ord,Show,Read)