{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  $Header$
Description :  A collection of data-structures, functions and instances for
                the THF modules.
Copyright   :  (c) A. Tsogias, DFKI Bremen 2011
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Alexis.Tsogias@dfki.de
Stability   :  provisional
Portability :  portable

Data structures and functions used in Logic_THF and HasCASL2THF.
Note: Some of the implenentations depend on the THF0 Syntax.
-}

module THF.Cons where

import THF.As

import Common.Id

import Data.Data

-- Some empty instances

{- -----------------------------------------------------------------------------
BasicSpecTHF
----------------------------------------------------------------------------- -}

data BasicSpecTHF =
    BasicSpecTHF [TPTP_THF]
    deriving (Show, Eq, Ord, Typeable, Data)

instance GetRange BasicSpecTHF

{- -----------------------------------------------------------------------------
SymbolTHF
----------------------------------------------------------------------------- -}

data SymbolTHF = Symbol
    { symId :: Constant
    , symName :: Name
    , symType :: SymbolType
    } deriving (Show, Eq, Ord, Typeable, Data)

instance GetRange SymbolTHF

data SymbolType =
    ST_Const Type
  | ST_Type Kind
    deriving (Show, Eq, Ord, Typeable, Data)

data Type =
    TType
  | OType
  | IType
  | MapType Type Type
  | ProdType [Type]
  | CType Constant
  | SType Token
  | VType Token
  | ParType Type
    deriving (Show, Eq, Ord, Typeable, Data)

data Kind = Kind
 deriving (Show, Eq, Ord, Typeable, Data)
