{-# 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)