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

ATC.Prover

Contents

Description

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

Orphan instances

ShATermConvertible ProverKind Source # 

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 # 

Methods

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

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

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

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

ShATermConvertible Reason Source # 

Methods

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

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

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

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

ShATermConvertible TacticScript Source # 

Methods

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

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

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

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

ShATermConvertible proof_tree => ShATermConvertible (CCStatus proof_tree) Source # 

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 # 

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 # 

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

(ShATermConvertible sentence, ShATermConvertible morphism) => ShATermConvertible (FreeDefMorphism sentence morphism) Source # 

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

(ShATermConvertible sign, ShATermConvertible sen, ShATermConvertible proof_tree) => ShATermConvertible (Theory sign sen proof_tree) Source # 

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

(ShATermConvertible sign, ShATermConvertible sen, ShATermConvertible mor, ShATermConvertible proof_tree) => ShATermConvertible (TheoryMorphism sign sen mor proof_tree) Source # 

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