{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  $Header$
Description :  Tern for HolLight logic
Copyright   :  (c) Jonathan von Schroeder, DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  jonathan.von_schroeder@dfki.de
Stability   :  experimental
Portability :  portable

Definition of terms for HolLight logic

  Ref.

  <http://www.cl.cam.ac.uk/~jrh13/hol-light/>

-}

module HolLight.Term where

import Data.Data

data HolType = TyVar String | TyApp String [HolType]
  deriving (Eq, Ord, Show, Read, Typeable, Data)

data HolProof = NoProof deriving (Eq, Ord, Show, Typeable, Data)

data HolParseType = Normal | PrefixT
 | InfixL Int | InfixR Int | Binder
 deriving (Eq, Ord, Show, Read, Typeable, Data)

data HolTermInfo = HolTermInfo (HolParseType, Maybe (String, HolParseType))
  deriving (Eq, Ord, Show, Read, Typeable, Data)

data Term = Var String HolType HolTermInfo
     | Const String HolType HolTermInfo
     | Comb Term Term
     | Abs Term Term deriving (Eq, Ord, Show, Read, Typeable, Data)
