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
 | DeclareFun FunDecl
 | DefineFunsRec [FunDef] [Expr]
 | MonoAssert Assertion Expr
 | ParAssert Assertion [Symbol] Expr
  deriving (Eq,Ord,Show,Read)

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

data FunDef =
   ParFunDef [Symbol] InnerFunDef
 | MonoFunDef InnerFunDef
  deriving (Eq,Ord,Show,Read)

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

data FunDecl =
   ParFunDecl [Symbol] InnerFunDecl
 | MonoFunDecl InnerFunDecl
  deriving (Eq,Ord,Show,Read)

data InnerFunDecl =
   InnerFunDecl Symbol [Type] 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 Binding 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
 | 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)