Hets - the Heterogeneous Tool Set
Copyright(c) DFKI GmbH 2012
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilitynon-portable(derive Typeable instances)
Safe HaskellNone

HolLight.ATC_HolLight

Description

Automatic derivation of instances via DrIFT-rule ShATermConvertible, Json for the type(s): Sentence Sign HolLightSL HolType HolProof HolParseType HolTermInfo Term

Orphan instances

Generic HolLightSL Source # 
Instance details

Associated Types

type Rep HolLightSL :: Type -> Type

Methods

from :: HolLightSL -> Rep HolLightSL x

to :: Rep HolLightSL x -> HolLightSL

Generic Term Source # 
Instance details

Associated Types

type Rep Term :: Type -> Type

Methods

from :: Term -> Rep Term x

to :: Rep Term x -> Term

Generic HolTermInfo Source # 
Instance details

Associated Types

type Rep HolTermInfo :: Type -> Type

Methods

from :: HolTermInfo -> Rep HolTermInfo x

to :: Rep HolTermInfo x -> HolTermInfo

Generic HolParseType Source # 
Instance details

Associated Types

type Rep HolParseType :: Type -> Type

Generic HolProof Source # 
Instance details

Associated Types

type Rep HolProof :: Type -> Type

Methods

from :: HolProof -> Rep HolProof x

to :: Rep HolProof x -> HolProof

Generic HolType Source # 
Instance details

Associated Types

type Rep HolType :: Type -> Type

Methods

from :: HolType -> Rep HolType x

to :: Rep HolType x -> HolType

Generic Sign Source # 
Instance details

Associated Types

type Rep Sign :: Type -> Type

Methods

from :: Sign -> Rep Sign x

to :: Rep Sign x -> Sign

Generic Sentence Source # 
Instance details

Associated Types

type Rep Sentence :: Type -> Type

Methods

from :: Sentence -> Rep Sentence x

to :: Rep Sentence x -> Sentence

FromJSON HolLightSL Source # 
Instance details

Methods

parseJSON :: Value -> Parser HolLightSL

parseJSONList :: Value -> Parser [HolLightSL]

FromJSON Term Source # 
Instance details

Methods

parseJSON :: Value -> Parser Term

parseJSONList :: Value -> Parser [Term]

FromJSON HolTermInfo Source # 
Instance details

Methods

parseJSON :: Value -> Parser HolTermInfo

parseJSONList :: Value -> Parser [HolTermInfo]

FromJSON HolParseType Source # 
Instance details

Methods

parseJSON :: Value -> Parser HolParseType

parseJSONList :: Value -> Parser [HolParseType]

FromJSON HolProof Source # 
Instance details

Methods

parseJSON :: Value -> Parser HolProof

parseJSONList :: Value -> Parser [HolProof]

FromJSON HolType Source # 
Instance details

Methods

parseJSON :: Value -> Parser HolType

parseJSONList :: Value -> Parser [HolType]

FromJSON Sign Source # 
Instance details

Methods

parseJSON :: Value -> Parser Sign

parseJSONList :: Value -> Parser [Sign]

FromJSON Sentence Source # 
Instance details

Methods

parseJSON :: Value -> Parser Sentence

parseJSONList :: Value -> Parser [Sentence]

ToJSON HolLightSL Source # 
Instance details

Methods

toJSON :: HolLightSL -> Value

toEncoding :: HolLightSL -> Encoding

toJSONList :: [HolLightSL] -> Value

toEncodingList :: [HolLightSL] -> Encoding

ToJSON Term Source # 
Instance details

Methods

toJSON :: Term -> Value

toEncoding :: Term -> Encoding

toJSONList :: [Term] -> Value

toEncodingList :: [Term] -> Encoding

ToJSON HolTermInfo Source # 
Instance details

Methods

toJSON :: HolTermInfo -> Value

toEncoding :: HolTermInfo -> Encoding

toJSONList :: [HolTermInfo] -> Value

toEncodingList :: [HolTermInfo] -> Encoding

ToJSON HolParseType Source # 
Instance details

Methods

toJSON :: HolParseType -> Value

toEncoding :: HolParseType -> Encoding

toJSONList :: [HolParseType] -> Value

toEncodingList :: [HolParseType] -> Encoding

ToJSON HolProof Source # 
Instance details

Methods

toJSON :: HolProof -> Value

toEncoding :: HolProof -> Encoding

toJSONList :: [HolProof] -> Value

toEncodingList :: [HolProof] -> Encoding

ToJSON HolType Source # 
Instance details

Methods

toJSON :: HolType -> Value

toEncoding :: HolType -> Encoding

toJSONList :: [HolType] -> Value

toEncodingList :: [HolType] -> Encoding

ToJSON Sign Source # 
Instance details

Methods

toJSON :: Sign -> Value

toEncoding :: Sign -> Encoding

toJSONList :: [Sign] -> Value

toEncodingList :: [Sign] -> Encoding

ToJSON Sentence Source # 
Instance details

Methods

toJSON :: Sentence -> Value

toEncoding :: Sentence -> Encoding

toJSONList :: [Sentence] -> Value

toEncodingList :: [Sentence] -> Encoding

ShATermConvertible HolLightSL Source # 
Instance details

Methods

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

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

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

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

ShATermConvertible Term Source # 
Instance details

Methods

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

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

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

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

ShATermConvertible HolTermInfo Source # 
Instance details

Methods

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

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

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

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

ShATermConvertible HolParseType Source # 
Instance details

Methods

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

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

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

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

ShATermConvertible HolProof Source # 
Instance details

Methods

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

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

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

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

ShATermConvertible HolType Source # 
Instance details

Methods

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

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

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

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

ShATermConvertible Sign Source # 
Instance details

Methods

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

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

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

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

ShATermConvertible Sentence Source # 
Instance details

Methods

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

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

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

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