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
Safe Haskell	Safe

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 Methods compare :: HolParseType -> HolParseType -> Ordering (<) :: HolParseType -> HolParseType -> Bool (<=) :: HolParseType -> HolParseType -> Bool (>) :: HolParseType -> HolParseType -> Bool (>=) :: HolParseType -> HolParseType -> Bool max :: HolParseType -> HolParseType -> HolParseType min :: HolParseType -> HolParseType -> HolParseType
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 Methods from :: HolParseType -> Rep HolParseType x to :: Rep HolParseType x -> HolParseType
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 Methods compare :: HolTermInfo -> HolTermInfo -> Ordering (<) :: HolTermInfo -> HolTermInfo -> Bool (<=) :: HolTermInfo -> HolTermInfo -> Bool (>) :: HolTermInfo -> HolTermInfo -> Bool (>=) :: HolTermInfo -> HolTermInfo -> Bool max :: HolTermInfo -> HolTermInfo -> HolTermInfo min :: HolTermInfo -> HolTermInfo -> HolTermInfo
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 #

Constructors

Var String HolType HolTermInfo
Const String HolType HolTermInfo
Comb Term Term
Abs Term Term

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