Copyright	(c) DFKI GmbH 2012
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	non-portable(derive Typeable instances)
Safe Haskell	None

ATC.Prover

Contents

Orphan instances

Description

Automatic derivation of instances via DrIFT-rule ShATermConvertible, Json for the type(s): ThmStatus Theory TacticScript GoalStatus ProofStatus ProverKind FreeDefMorphism TheoryMorphism CCStatus

Orphan instances

Generic ProverKind Source #
Instance details Associated Types type Rep ProverKind :: Type -> Type Methods from :: ProverKind -> Rep ProverKind x to :: Rep ProverKind x -> ProverKind
Generic GoalStatus Source #
Instance details Associated Types type Rep GoalStatus :: Type -> Type Methods from :: GoalStatus -> Rep GoalStatus x to :: Rep GoalStatus x -> GoalStatus
Generic TacticScript Source #
Instance details Associated Types type Rep TacticScript :: Type -> Type Methods from :: TacticScript -> Rep TacticScript x to :: Rep TacticScript x -> TacticScript
FromJSON ProverKind Source #
Instance details Methods parseJSON :: Value -> Parser ProverKind parseJSONList :: Value -> Parser [ProverKind]
FromJSON GoalStatus Source #
Instance details Methods parseJSON :: Value -> Parser GoalStatus parseJSONList :: Value -> Parser [GoalStatus]
FromJSON TacticScript Source #
Instance details Methods parseJSON :: Value -> Parser TacticScript parseJSONList :: Value -> Parser [TacticScript]
ToJSON ProverKind Source #
Instance details Methods toJSON :: ProverKind -> Value toEncoding :: ProverKind -> Encoding toJSONList :: [ProverKind] -> Value toEncodingList :: [ProverKind] -> Encoding
ToJSON GoalStatus Source #
Instance details Methods toJSON :: GoalStatus -> Value toEncoding :: GoalStatus -> Encoding toJSONList :: [GoalStatus] -> Value toEncodingList :: [GoalStatus] -> Encoding
ToJSON TacticScript Source #
Instance details Methods toJSON :: TacticScript -> Value toEncoding :: TacticScript -> Encoding toJSONList :: [TacticScript] -> Value toEncodingList :: [TacticScript] -> Encoding
ShATermConvertible ProverKind Source #
Instance details Methods toShATermAux :: ATermTable -> ProverKind -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [ProverKind] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, ProverKind) fromShATermList' :: Int -> ATermTable -> (ATermTable, [ProverKind])
ShATermConvertible GoalStatus Source #
Instance details Methods toShATermAux :: ATermTable -> GoalStatus -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [GoalStatus] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, GoalStatus) fromShATermList' :: Int -> ATermTable -> (ATermTable, [GoalStatus])
ShATermConvertible TacticScript Source #
Instance details Methods toShATermAux :: ATermTable -> TacticScript -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [TacticScript] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, TacticScript) fromShATermList' :: Int -> ATermTable -> (ATermTable, [TacticScript])
Generic (CCStatus proof_tree) Source #
Instance details Associated Types type Rep (CCStatus proof_tree) :: Type -> Type Methods from :: CCStatus proof_tree -> Rep (CCStatus proof_tree) x to :: Rep (CCStatus proof_tree) x -> CCStatus proof_tree
Generic (ProofStatus proof_tree) Source #
Instance details Associated Types type Rep (ProofStatus proof_tree) :: Type -> Type Methods from :: ProofStatus proof_tree -> Rep (ProofStatus proof_tree) x to :: Rep (ProofStatus proof_tree) x -> ProofStatus proof_tree
Generic (ThmStatus a) Source #
Instance details Associated Types type Rep (ThmStatus a) :: Type -> Type Methods from :: ThmStatus a -> Rep (ThmStatus a) x to :: Rep (ThmStatus a) x -> ThmStatus a
FromJSON proof_tree => FromJSON (CCStatus proof_tree) Source #
Instance details Methods parseJSON :: Value -> Parser (CCStatus proof_tree) parseJSONList :: Value -> Parser [CCStatus proof_tree]
FromJSON proof_tree => FromJSON (ProofStatus proof_tree) Source #
Instance details Methods parseJSON :: Value -> Parser (ProofStatus proof_tree) parseJSONList :: Value -> Parser [ProofStatus proof_tree]
FromJSON a => FromJSON (ThmStatus a) Source #
Instance details Methods parseJSON :: Value -> Parser (ThmStatus a) parseJSONList :: Value -> Parser [ThmStatus a]
ToJSON proof_tree => ToJSON (CCStatus proof_tree) Source #
Instance details Methods toJSON :: CCStatus proof_tree -> Value toEncoding :: CCStatus proof_tree -> Encoding toJSONList :: [CCStatus proof_tree] -> Value toEncodingList :: [CCStatus proof_tree] -> Encoding
ToJSON proof_tree => ToJSON (ProofStatus proof_tree) Source #
Instance details Methods toJSON :: ProofStatus proof_tree -> Value toEncoding :: ProofStatus proof_tree -> Encoding toJSONList :: [ProofStatus proof_tree] -> Value toEncodingList :: [ProofStatus proof_tree] -> Encoding
ToJSON a => ToJSON (ThmStatus a) Source #
Instance details Methods toJSON :: ThmStatus a -> Value toEncoding :: ThmStatus a -> Encoding toJSONList :: [ThmStatus a] -> Value toEncodingList :: [ThmStatus a] -> Encoding
ShATermConvertible proof_tree => ShATermConvertible (CCStatus proof_tree) Source #
Instance details Methods toShATermAux :: ATermTable -> CCStatus proof_tree -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [CCStatus proof_tree] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, CCStatus proof_tree) fromShATermList' :: Int -> ATermTable -> (ATermTable, [CCStatus proof_tree])
ShATermConvertible proof_tree => ShATermConvertible (ProofStatus proof_tree) Source #
Instance details Methods toShATermAux :: ATermTable -> ProofStatus proof_tree -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [ProofStatus proof_tree] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, ProofStatus proof_tree) fromShATermList' :: Int -> ATermTable -> (ATermTable, [ProofStatus proof_tree])
ShATermConvertible a => ShATermConvertible (ThmStatus a) Source #
Instance details Methods toShATermAux :: ATermTable -> ThmStatus a -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [ThmStatus a] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, ThmStatus a) fromShATermList' :: Int -> ATermTable -> (ATermTable, [ThmStatus a])
Generic (FreeDefMorphism sentence morphism) Source #
Instance details Associated Types type Rep (FreeDefMorphism sentence morphism) :: Type -> Type Methods from :: FreeDefMorphism sentence morphism -> Rep (FreeDefMorphism sentence morphism) x to :: Rep (FreeDefMorphism sentence morphism) x -> FreeDefMorphism sentence morphism
(FromJSON sentence, FromJSON morphism) => FromJSON (FreeDefMorphism sentence morphism) Source #
Instance details Methods parseJSON :: Value -> Parser (FreeDefMorphism sentence morphism) parseJSONList :: Value -> Parser [FreeDefMorphism sentence morphism]
(ToJSON sentence, ToJSON morphism) => ToJSON (FreeDefMorphism sentence morphism) Source #
Instance details Methods toJSON :: FreeDefMorphism sentence morphism -> Value toEncoding :: FreeDefMorphism sentence morphism -> Encoding toJSONList :: [FreeDefMorphism sentence morphism] -> Value toEncodingList :: [FreeDefMorphism sentence morphism] -> Encoding
(ShATermConvertible sentence, ShATermConvertible morphism) => ShATermConvertible (FreeDefMorphism sentence morphism) Source #
Instance details Methods toShATermAux :: ATermTable -> FreeDefMorphism sentence morphism -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [FreeDefMorphism sentence morphism] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, FreeDefMorphism sentence morphism) fromShATermList' :: Int -> ATermTable -> (ATermTable, [FreeDefMorphism sentence morphism])
Generic (Theory sign sen proof_tree) Source #
Instance details Associated Types type Rep (Theory sign sen proof_tree) :: Type -> Type Methods from :: Theory sign sen proof_tree -> Rep (Theory sign sen proof_tree) x to :: Rep (Theory sign sen proof_tree) x -> Theory sign sen proof_tree
(FromJSON sign, FromJSON sen, FromJSON proof_tree) => FromJSON (Theory sign sen proof_tree) Source #
Instance details Methods parseJSON :: Value -> Parser (Theory sign sen proof_tree) parseJSONList :: Value -> Parser [Theory sign sen proof_tree]
(ToJSON sign, ToJSON sen, ToJSON proof_tree) => ToJSON (Theory sign sen proof_tree) Source #
Instance details Methods toJSON :: Theory sign sen proof_tree -> Value toEncoding :: Theory sign sen proof_tree -> Encoding toJSONList :: [Theory sign sen proof_tree] -> Value toEncodingList :: [Theory sign sen proof_tree] -> Encoding
(ShATermConvertible sign, ShATermConvertible sen, ShATermConvertible proof_tree) => ShATermConvertible (Theory sign sen proof_tree) Source #
Instance details Methods toShATermAux :: ATermTable -> Theory sign sen proof_tree -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Theory sign sen proof_tree] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Theory sign sen proof_tree) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Theory sign sen proof_tree])
Generic (TheoryMorphism sign sen mor proof_tree) Source #
Instance details Associated Types type Rep (TheoryMorphism sign sen mor proof_tree) :: Type -> Type Methods from :: TheoryMorphism sign sen mor proof_tree -> Rep (TheoryMorphism sign sen mor proof_tree) x to :: Rep (TheoryMorphism sign sen mor proof_tree) x -> TheoryMorphism sign sen mor proof_tree
(FromJSON sign, FromJSON sen, FromJSON mor, FromJSON proof_tree) => FromJSON (TheoryMorphism sign sen mor proof_tree) Source #
Instance details Methods parseJSON :: Value -> Parser (TheoryMorphism sign sen mor proof_tree) parseJSONList :: Value -> Parser [TheoryMorphism sign sen mor proof_tree]
(ToJSON sign, ToJSON sen, ToJSON mor, ToJSON proof_tree) => ToJSON (TheoryMorphism sign sen mor proof_tree) Source #
Instance details Methods toJSON :: TheoryMorphism sign sen mor proof_tree -> Value toEncoding :: TheoryMorphism sign sen mor proof_tree -> Encoding toJSONList :: [TheoryMorphism sign sen mor proof_tree] -> Value toEncodingList :: [TheoryMorphism sign sen mor proof_tree] -> Encoding
(ShATermConvertible sign, ShATermConvertible sen, ShATermConvertible mor, ShATermConvertible proof_tree) => ShATermConvertible (TheoryMorphism sign sen mor proof_tree) Source #
Instance details Methods toShATermAux :: ATermTable -> TheoryMorphism sign sen mor proof_tree -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [TheoryMorphism sign sen mor proof_tree] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, TheoryMorphism sign sen mor proof_tree) fromShATermList' :: Int -> ATermTable -> (ATermTable, [TheoryMorphism sign sen mor proof_tree])