Hets - the Heterogeneous Tool Set
Copyright(c) Jonathan von Schroeder DFKI GmbH 2010
LicenseGPLv2 or higher, see LICENSE.txt
Maintainerjonathan.von_schroeder@dfki.de
Stabilityexperimental
Portabilityportable
Safe HaskellSafe

HolLight.Term

Description

Definition of terms for HolLight logic

Ref.

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

Documentation

data HolType Source #

Constructors

TyVar String 
TyApp String [HolType] 

Instances

Instances details
Eq HolType Source # 
Instance details

Defined in HolLight.Term

Methods

(==) :: HolType -> HolType -> Bool

(/=) :: HolType -> HolType -> Bool

Data HolType Source # 
Instance details

Defined in HolLight.Term

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HolType -> c HolType

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HolType

toConstr :: HolType -> Constr

dataTypeOf :: HolType -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HolType)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HolType)

gmapT :: (forall b. Data b => b -> b) -> HolType -> HolType

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HolType -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HolType -> r

gmapQ :: (forall d. Data d => d -> u) -> HolType -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> HolType -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> HolType -> m HolType

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HolType -> m HolType

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HolType -> m HolType

Ord HolType Source # 
Instance details

Defined in HolLight.Term

Methods

compare :: HolType -> HolType -> Ordering

(<) :: HolType -> HolType -> Bool

(<=) :: HolType -> HolType -> Bool

(>) :: HolType -> HolType -> Bool

(>=) :: HolType -> HolType -> Bool

max :: HolType -> HolType -> HolType

min :: HolType -> HolType -> HolType

Read HolType Source # 
Instance details

Defined in HolLight.Term

Methods

readsPrec :: Int -> ReadS HolType

readList :: ReadS [HolType]

readPrec :: ReadPrec HolType

readListPrec :: ReadPrec [HolType]

Show HolType Source # 
Instance details

Defined in HolLight.Term

Methods

showsPrec :: Int -> HolType -> ShowS

show :: HolType -> String

showList :: [HolType] -> ShowS

Generic HolType 
Instance details

Defined in HolLight.ATC_HolLight

Associated Types

type Rep HolType :: Type -> Type

Methods

from :: HolType -> Rep HolType x

to :: Rep HolType x -> HolType

FromJSON HolType 
Instance details

Defined in HolLight.ATC_HolLight

Methods

parseJSON :: Value -> Parser HolType

parseJSONList :: Value -> Parser [HolType]

ToJSON HolType 
Instance details

Defined in HolLight.ATC_HolLight

Methods

toJSON :: HolType -> Value

toEncoding :: HolType -> Encoding

toJSONList :: [HolType] -> Value

toEncodingList :: [HolType] -> Encoding

ShATermConvertible HolType 
Instance details

Defined in HolLight.ATC_HolLight

Methods

toShATermAux :: ATermTable -> HolType -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [HolType] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, HolType)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [HolType])

type Rep HolType 
Instance details

Defined in HolLight.ATC_HolLight

type Rep HolType = D1 ('MetaData "HolType" "HolLight.Term" "main" 'False) (C1 ('MetaCons "TyVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "TyApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [HolType])))

data HolProof Source #

Constructors

NoProof 

Instances

Instances details
Eq HolProof Source # 
Instance details

Defined in HolLight.Term

Methods

(==) :: HolProof -> HolProof -> Bool

(/=) :: HolProof -> HolProof -> Bool

Data HolProof Source # 
Instance details

Defined in HolLight.Term

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HolProof -> c HolProof

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HolProof

toConstr :: HolProof -> Constr

dataTypeOf :: HolProof -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HolProof)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HolProof)

gmapT :: (forall b. Data b => b -> b) -> HolProof -> HolProof

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HolProof -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HolProof -> r

gmapQ :: (forall d. Data d => d -> u) -> HolProof -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> HolProof -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> HolProof -> m HolProof

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HolProof -> m HolProof

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HolProof -> m HolProof

Ord HolProof Source # 
Instance details

Defined in HolLight.Term

Methods

compare :: HolProof -> HolProof -> Ordering

(<) :: HolProof -> HolProof -> Bool

(<=) :: HolProof -> HolProof -> Bool

(>) :: HolProof -> HolProof -> Bool

(>=) :: HolProof -> HolProof -> Bool

max :: HolProof -> HolProof -> HolProof

min :: HolProof -> HolProof -> HolProof

Show HolProof Source # 
Instance details

Defined in HolLight.Term

Methods

showsPrec :: Int -> HolProof -> ShowS

show :: HolProof -> String

showList :: [HolProof] -> ShowS

Generic HolProof 
Instance details

Defined in HolLight.ATC_HolLight

Associated Types

type Rep HolProof :: Type -> Type

Methods

from :: HolProof -> Rep HolProof x

to :: Rep HolProof x -> HolProof

FromJSON HolProof 
Instance details

Defined in HolLight.ATC_HolLight

Methods

parseJSON :: Value -> Parser HolProof

parseJSONList :: Value -> Parser [HolProof]

ToJSON HolProof 
Instance details

Defined in HolLight.ATC_HolLight

Methods

toJSON :: HolProof -> Value

toEncoding :: HolProof -> Encoding

toJSONList :: [HolProof] -> Value

toEncodingList :: [HolProof] -> Encoding

ShATermConvertible HolProof 
Instance details

Defined in HolLight.ATC_HolLight

Methods

toShATermAux :: ATermTable -> HolProof -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [HolProof] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, HolProof)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [HolProof])

type Rep HolProof 
Instance details

Defined in HolLight.ATC_HolLight

type Rep HolProof = D1 ('MetaData "HolProof" "HolLight.Term" "main" 'False) (C1 ('MetaCons "NoProof" 'PrefixI 'False) (U1 :: Type -> Type))

data HolParseType Source #

Constructors

Normal 
PrefixT 
InfixL Int 
InfixR Int 
Binder 

Instances

Instances details
Eq HolParseType Source # 
Instance details

Defined in HolLight.Term

Methods

(==) :: HolParseType -> HolParseType -> Bool

(/=) :: HolParseType -> HolParseType -> Bool

Data HolParseType Source # 
Instance details

Defined in HolLight.Term

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HolParseType -> c HolParseType

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HolParseType

toConstr :: HolParseType -> Constr

dataTypeOf :: HolParseType -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HolParseType)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HolParseType)

gmapT :: (forall b. Data b => b -> b) -> HolParseType -> HolParseType

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HolParseType -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HolParseType -> r

gmapQ :: (forall d. Data d => d -> u) -> HolParseType -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> HolParseType -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> HolParseType -> m HolParseType

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HolParseType -> m HolParseType

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HolParseType -> m HolParseType

Ord HolParseType Source # 
Instance details

Defined in HolLight.Term

Read HolParseType Source # 
Instance details

Defined in HolLight.Term

Methods

readsPrec :: Int -> ReadS HolParseType

readList :: ReadS [HolParseType]

readPrec :: ReadPrec HolParseType

readListPrec :: ReadPrec [HolParseType]

Show HolParseType Source # 
Instance details

Defined in HolLight.Term

Methods

showsPrec :: Int -> HolParseType -> ShowS

show :: HolParseType -> String

showList :: [HolParseType] -> ShowS

Generic HolParseType 
Instance details

Defined in HolLight.ATC_HolLight

Associated Types

type Rep HolParseType :: Type -> Type

FromJSON HolParseType 
Instance details

Defined in HolLight.ATC_HolLight

Methods

parseJSON :: Value -> Parser HolParseType

parseJSONList :: Value -> Parser [HolParseType]

ToJSON HolParseType 
Instance details

Defined in HolLight.ATC_HolLight

Methods

toJSON :: HolParseType -> Value

toEncoding :: HolParseType -> Encoding

toJSONList :: [HolParseType] -> Value

toEncodingList :: [HolParseType] -> Encoding

ShATermConvertible HolParseType 
Instance details

Defined in HolLight.ATC_HolLight

Methods

toShATermAux :: ATermTable -> HolParseType -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [HolParseType] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, HolParseType)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [HolParseType])

type Rep HolParseType 
Instance details

Defined in HolLight.ATC_HolLight

type Rep HolParseType = D1 ('MetaData "HolParseType" "HolLight.Term" "main" 'False) ((C1 ('MetaCons "Normal" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrefixT" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "InfixL" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: (C1 ('MetaCons "InfixR" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: C1 ('MetaCons "Binder" 'PrefixI 'False) (U1 :: Type -> Type))))

data HolTermInfo Source #

Constructors

HolTermInfo (HolParseType, Maybe (String, HolParseType)) 

Instances

Instances details
Eq HolTermInfo Source # 
Instance details

Defined in HolLight.Term

Methods

(==) :: HolTermInfo -> HolTermInfo -> Bool

(/=) :: HolTermInfo -> HolTermInfo -> Bool

Data HolTermInfo Source # 
Instance details

Defined in HolLight.Term

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HolTermInfo -> c HolTermInfo

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HolTermInfo

toConstr :: HolTermInfo -> Constr

dataTypeOf :: HolTermInfo -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HolTermInfo)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HolTermInfo)

gmapT :: (forall b. Data b => b -> b) -> HolTermInfo -> HolTermInfo

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HolTermInfo -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HolTermInfo -> r

gmapQ :: (forall d. Data d => d -> u) -> HolTermInfo -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> HolTermInfo -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> HolTermInfo -> m HolTermInfo

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HolTermInfo -> m HolTermInfo

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HolTermInfo -> m HolTermInfo

Ord HolTermInfo Source # 
Instance details

Defined in HolLight.Term

Read HolTermInfo Source # 
Instance details

Defined in HolLight.Term

Methods

readsPrec :: Int -> ReadS HolTermInfo

readList :: ReadS [HolTermInfo]

readPrec :: ReadPrec HolTermInfo

readListPrec :: ReadPrec [HolTermInfo]

Show HolTermInfo Source # 
Instance details

Defined in HolLight.Term

Methods

showsPrec :: Int -> HolTermInfo -> ShowS

show :: HolTermInfo -> String

showList :: [HolTermInfo] -> ShowS

Generic HolTermInfo 
Instance details

Defined in HolLight.ATC_HolLight

Associated Types

type Rep HolTermInfo :: Type -> Type

Methods

from :: HolTermInfo -> Rep HolTermInfo x

to :: Rep HolTermInfo x -> HolTermInfo

FromJSON HolTermInfo 
Instance details

Defined in HolLight.ATC_HolLight

Methods

parseJSON :: Value -> Parser HolTermInfo

parseJSONList :: Value -> Parser [HolTermInfo]

ToJSON HolTermInfo 
Instance details

Defined in HolLight.ATC_HolLight

Methods

toJSON :: HolTermInfo -> Value

toEncoding :: HolTermInfo -> Encoding

toJSONList :: [HolTermInfo] -> Value

toEncodingList :: [HolTermInfo] -> Encoding

ShATermConvertible HolTermInfo 
Instance details

Defined in HolLight.ATC_HolLight

Methods

toShATermAux :: ATermTable -> HolTermInfo -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [HolTermInfo] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, HolTermInfo)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [HolTermInfo])

type Rep HolTermInfo 
Instance details

Defined in HolLight.ATC_HolLight

type Rep HolTermInfo = D1 ('MetaData "HolTermInfo" "HolLight.Term" "main" 'False) (C1 ('MetaCons "HolTermInfo" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HolParseType, Maybe (String, HolParseType)))))

data Term Source #

Instances

Instances details
Eq Term Source # 
Instance details

Defined in HolLight.Term

Methods

(==) :: Term -> Term -> Bool

(/=) :: Term -> Term -> Bool

Data Term Source # 
Instance details

Defined in HolLight.Term

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Term -> c Term

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Term

toConstr :: Term -> Constr

dataTypeOf :: Term -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Term)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term)

gmapT :: (forall b. Data b => b -> b) -> Term -> Term

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r

gmapQ :: (forall d. Data d => d -> u) -> Term -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Term -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Term -> m Term

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term

Ord Term Source # 
Instance details

Defined in HolLight.Term

Methods

compare :: Term -> Term -> Ordering

(<) :: Term -> Term -> Bool

(<=) :: Term -> Term -> Bool

(>) :: Term -> Term -> Bool

(>=) :: Term -> Term -> Bool

max :: Term -> Term -> Term

min :: Term -> Term -> Term

Read Term Source # 
Instance details

Defined in HolLight.Term

Methods

readsPrec :: Int -> ReadS Term

readList :: ReadS [Term]

readPrec :: ReadPrec Term

readListPrec :: ReadPrec [Term]

Show Term Source # 
Instance details

Defined in HolLight.Term

Methods

showsPrec :: Int -> Term -> ShowS

show :: Term -> String

showList :: [Term] -> ShowS

Generic Term 
Instance details

Defined in HolLight.ATC_HolLight

Associated Types

type Rep Term :: Type -> Type

Methods

from :: Term -> Rep Term x

to :: Rep Term x -> Term

FromJSON Term 
Instance details

Defined in HolLight.ATC_HolLight

Methods

parseJSON :: Value -> Parser Term

parseJSONList :: Value -> Parser [Term]

ToJSON Term 
Instance details

Defined in HolLight.ATC_HolLight

Methods

toJSON :: Term -> Value

toEncoding :: Term -> Encoding

toJSONList :: [Term] -> Value

toEncodingList :: [Term] -> Encoding

ShATermConvertible Term 
Instance details

Defined in HolLight.ATC_HolLight

Methods

toShATermAux :: ATermTable -> Term -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Term] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Term)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Term])

type Rep Term 
Instance details

Defined in HolLight.ATC_HolLight

type Rep Term = D1 ('MetaData "Term" "HolLight.Term" "main" 'False) ((C1 ('MetaCons "Var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 HolType) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 HolTermInfo))) :+: C1 ('MetaCons "Const" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 HolType) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 HolTermInfo)))) :+: (C1 ('MetaCons "Comb" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: C1 ('MetaCons "Abs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term))))