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