Copyright	(c) Till Mossakowski Klaus Luettich Uni Bremen 2002-2005
License	GPLv2 or higher, see LICENSE.txt
Maintainer	till@informatik.uni-bremen.de
Stability	provisional
Portability	non-portable (deriving Typeable)
Safe Haskell	None

Logic.Prover

Contents

pack sentences with their proofs
Orphan instances

Description

General datastructures for theorem prover interfaces

Synopsis

type SenStatus a tStatus = SenAttr a (ThmStatus tStatus)
thmStatus :: SenStatus a tStatus -> [tStatus]
data ThmStatus a = ThmStatus {
- getThmStatus :: [a]
}
emptySenStatus :: SenStatus a b
printOMapElemWOrd :: (a -> Doc) -> ElemWOrd a -> Doc
type ThSens a b = OMap String (SenStatus a b)
noSens :: ThSens a b
mapThSensValueM :: Monad m => (a -> m b) -> ThSens a c -> m (ThSens b c)
joinSensAux :: (Ord a, Eq b) => ThSens a b -> ThSens a b -> (ThSens a b, [(String, String)])
joinSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b -> ThSens a b
intersectSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b -> ThSens a b
reduceSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b
cmpSnd :: Ord a1 => (String, ElemWOrd (SenStatus a1 b)) -> (String, ElemWOrd (SenStatus a1 b)) -> Ordering
cmpSenEle :: Ord a1 => ElemWOrd (SenStatus a1 b) -> ElemWOrd (SenStatus a1 b) -> Ordering
mapValue :: (a -> b) -> SenStatus a c -> SenStatus b c
markAsAxiom :: Ord a => Bool -> ThSens a b -> ThSens a b
markAsGoal :: Ord a => ThSens a b -> ThSens a b
toNamedList :: ThSens a b -> [Named a]
toNamed :: String -> SenStatus a b -> Named a
toThSens :: Ord a => [Named a] -> ThSens a b
data Theory sign sen proof_tree = Theory sign (ThSens sen (ProofStatus proof_tree))
data TacticScript = TacticScript String
data Reason = Reason [String]
data GoalStatus
- = Open Reason
- | Disproved
- | Proved Bool
isOpenGoal :: GoalStatus -> Bool
openGoalStatus :: GoalStatus
data ProofStatus proof_tree = ProofStatus {
- goalName :: String
- goalStatus :: GoalStatus
- usedAxioms :: [String]
- usedProver :: String
- proofTree :: proof_tree
- usedTime :: TimeOfDay
- tacticScript :: TacticScript
- proofLines :: [String]
}
openProofStatus :: Ord pt => String -> String -> pt -> ProofStatus pt
isProvedStat :: ProofStatus proof_tree -> Bool
isProvedGStat :: GoalStatus -> Bool
data ProverKind
- = ProveGUI
- | ProveCMDLautomatic
hasProverKind :: ProverKind -> ProverTemplate x s m y z -> Bool
data FreeDefMorphism sentence morphism = FreeDefMorphism {
- freeDefMorphism :: morphism
- pathFromFreeDef :: morphism
- freeTheory :: [Named sentence]
- isCofree :: Bool
}
data ProverTemplate theory sentence morphism sublogics proof_tree = Prover {
- proverName :: String
- proverUsable :: IO (Maybe String)
- proverSublogic :: sublogics
- proveGUI :: Maybe (String -> theory -> [FreeDefMorphism sentence morphism] -> IO ([ProofStatus proof_tree], [(Named sentence, ProofStatus proof_tree)]))
- proveCMDLautomaticBatch :: Maybe (Bool -> Bool -> MVar (Result [ProofStatus proof_tree]) -> String -> TacticScript -> theory -> [FreeDefMorphism sentence morphism] -> IO (ThreadId, MVar ()))
}
type Prover sign sentence morphism sublogics proof_tree = ProverTemplate (Theory sign sentence proof_tree) sentence morphism sublogics proof_tree
mkProverTemplate :: String -> sublogics -> (String -> theory -> [FreeDefMorphism sentence morphism] -> IO [ProofStatus proof_tree]) -> ProverTemplate theory sentence morphism sublogics proof_tree
mkUsableProver :: String -> String -> sublogics -> (String -> theory -> [FreeDefMorphism sentence morphism] -> IO [ProofStatus proof_tree]) -> ProverTemplate theory sentence morphism sublogics proof_tree
mkAutomaticProver :: String -> String -> sublogics -> (String -> theory -> [FreeDefMorphism sentence morphism] -> IO [ProofStatus proof_tree]) -> (Bool -> Bool -> MVar (Result [ProofStatus proof_tree]) -> String -> TacticScript -> theory -> [FreeDefMorphism sentence morphism] -> IO (ThreadId, MVar ())) -> ProverTemplate theory sentence morphism sublogics proof_tree
data TheoryMorphism sign sen mor proof_tree = TheoryMorphism {
- tSource :: Theory sign sen proof_tree
- tTarget :: Theory sign sen proof_tree
- tMorphism :: mor
}
data CCStatus proof_tree = CCStatus {
- ccProofTree :: proof_tree
- ccUsedTime :: TimeOfDay
- ccResult :: Maybe Bool
}
data ConsChecker sign sentence sublogics morphism proof_tree = ConsChecker {
- ccName :: String
- ccUsable :: IO (Maybe String)
- ccSublogic :: sublogics
- ccBatch :: Bool
- ccNeedsTimer :: Bool
- ccAutomatic :: String -> TacticScript -> TheoryMorphism sign sentence morphism proof_tree -> [FreeDefMorphism sentence morphism] -> IO (CCStatus proof_tree)
}
mkConsChecker :: String -> sublogics -> (String -> TacticScript -> TheoryMorphism sign sentence morphism proof_tree -> [FreeDefMorphism sentence morphism] -> IO (CCStatus proof_tree)) -> ConsChecker sign sentence sublogics morphism proof_tree
mkUsableConsChecker :: String -> String -> sublogics -> (String -> TacticScript -> TheoryMorphism sign sentence morphism proof_tree -> [FreeDefMorphism sentence morphism] -> IO (CCStatus proof_tree)) -> ConsChecker sign sentence sublogics morphism proof_tree

pack sentences with their proofs

type SenStatus a tStatus = SenAttr a (ThmStatus tStatus) Source #

instead of the sentence name (that will be the key into the order map) the theorem status will be stored as attribute. The theorem status will be a (wrapped) list of pairs (AnyComorphism, BasicProof) in G_theory, but a wrapped list of (ProofStatus proof_tree) in a logic specific Theory.

thmStatus :: SenStatus a tStatus -> [tStatus] Source #

data ThmStatus a Source #

the wrapped list of proof scripts or (AnyComorphism, BasicProof) pairs

Constructors

ThmStatus
Fields getThmStatus :: [a]

Instances

Instances details

Eq a => Eq (ThmStatus a) Source #
Instance details Defined in Logic.Prover Methods (==) :: ThmStatus a -> ThmStatus a -> Bool (/=) :: ThmStatus a -> ThmStatus a -> Bool
Ord a => Ord (ThmStatus a) Source #
Instance details Defined in Logic.Prover Methods compare :: ThmStatus a -> ThmStatus a -> Ordering (<) :: ThmStatus a -> ThmStatus a -> Bool (<=) :: ThmStatus a -> ThmStatus a -> Bool (>) :: ThmStatus a -> ThmStatus a -> Bool (>=) :: ThmStatus a -> ThmStatus a -> Bool max :: ThmStatus a -> ThmStatus a -> ThmStatus a min :: ThmStatus a -> ThmStatus a -> ThmStatus a
Show a => Show (ThmStatus a) Source #
Instance details Defined in Logic.Prover Methods showsPrec :: Int -> ThmStatus a -> ShowS show :: ThmStatus a -> String showList :: [ThmStatus a] -> ShowS
Generic (ThmStatus a)
Instance details Defined in ATC.Prover Associated Types type Rep (ThmStatus a) :: Type -> Type Methods from :: ThmStatus a -> Rep (ThmStatus a) x to :: Rep (ThmStatus a) x -> ThmStatus a
FromJSON a => FromJSON (ThmStatus a)
Instance details Defined in ATC.Prover Methods parseJSON :: Value -> Parser (ThmStatus a) parseJSONList :: Value -> Parser [ThmStatus a]
ToJSON a => ToJSON (ThmStatus a)
Instance details Defined in ATC.Prover Methods toJSON :: ThmStatus a -> Value toEncoding :: ThmStatus a -> Encoding toJSONList :: [ThmStatus a] -> Value toEncodingList :: [ThmStatus a] -> Encoding
ShATermConvertible a => ShATermConvertible (ThmStatus a)
Instance details Defined in ATC.Prover 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])
ShATermLG a => ShATermLG (ThmStatus a) Source #
Instance details Defined in ATC.Grothendieck Methods toShATermLG :: ATermTable -> ThmStatus a -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, ThmStatus a) Source #
type Rep (ThmStatus a)
Instance details Defined in ATC.Prover type Rep (ThmStatus a) = D1 ('MetaData "ThmStatus" "Logic.Prover" "main" 'False) (C1 ('MetaCons "ThmStatus" 'PrefixI 'True) (S1 ('MetaSel ('Just "getThmStatus") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [a])))

emptySenStatus :: SenStatus a b Source #

printOMapElemWOrd :: (a -> Doc) -> ElemWOrd a -> Doc Source #

type ThSens a b = OMap String (SenStatus a b) Source #

the map from labels to the theorem plus status (and position)

noSens :: ThSens a b Source #

mapThSensValueM :: Monad m => (a -> m b) -> ThSens a c -> m (ThSens b c) Source #

joinSensAux :: (Ord a, Eq b) => ThSens a b -> ThSens a b -> (ThSens a b, [(String, String)]) Source #

join and disambiguate

separate Axioms from Theorems
don't merge sentences with same key but different contents?

joinSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b -> ThSens a b Source #

intersectSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b -> ThSens a b Source #

reduceSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b Source #

cmpSnd :: Ord a1 => (String, ElemWOrd (SenStatus a1 b)) -> (String, ElemWOrd (SenStatus a1 b)) -> Ordering Source #

cmpSenEle :: Ord a1 => ElemWOrd (SenStatus a1 b) -> ElemWOrd (SenStatus a1 b) -> Ordering Source #

mapValue :: (a -> b) -> SenStatus a c -> SenStatus b c Source #

markAsAxiom :: Ord a => Bool -> ThSens a b -> ThSens a b Source #

sets the field isAxiom according to the boolean value; if isAxiom is False for a sentence and set to True, the field wasTheorem is set to True.

markAsGoal :: Ord a => ThSens a b -> ThSens a b Source #

toNamedList :: ThSens a b -> [Named a] Source #

toNamed :: String -> SenStatus a b -> Named a Source #

toThSens :: Ord a => [Named a] -> ThSens a b Source #

putting Sentences from a list into a map

data Theory sign sen proof_tree Source #

theories with a signature and sentences with proof states

Constructors

Theory sign (ThSens sen (ProofStatus proof_tree))

Instances

Instances details

Generic (Theory sign sen proof_tree)
Instance details Defined in ATC.Prover 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)
Instance details Defined in ATC.Prover 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)
Instance details Defined in ATC.Prover 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)
Instance details Defined in ATC.Prover 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])
type Rep (Theory sign sen proof_tree)
Instance details Defined in ATC.Prover type Rep (Theory sign sen proof_tree) = D1 ('MetaData "Theory" "Logic.Prover" "main" 'False) (C1 ('MetaCons "Theory" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 sign) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ThSens sen (ProofStatus proof_tree)))))

data TacticScript Source #

Constructors

TacticScript String

Instances

Instances details

Eq TacticScript Source #
Instance details Defined in Logic.Prover Methods (==) :: TacticScript -> TacticScript -> Bool (/=) :: TacticScript -> TacticScript -> Bool
Ord TacticScript Source #
Instance details Defined in Logic.Prover Methods compare :: TacticScript -> TacticScript -> Ordering (<) :: TacticScript -> TacticScript -> Bool (<=) :: TacticScript -> TacticScript -> Bool (>) :: TacticScript -> TacticScript -> Bool (>=) :: TacticScript -> TacticScript -> Bool max :: TacticScript -> TacticScript -> TacticScript min :: TacticScript -> TacticScript -> TacticScript
Show TacticScript Source #
Instance details Defined in Logic.Prover Methods showsPrec :: Int -> TacticScript -> ShowS show :: TacticScript -> String showList :: [TacticScript] -> ShowS
Generic TacticScript
Instance details Defined in ATC.Prover Associated Types type Rep TacticScript :: Type -> Type Methods from :: TacticScript -> Rep TacticScript x to :: Rep TacticScript x -> TacticScript
FromJSON TacticScript
Instance details Defined in ATC.Prover Methods parseJSON :: Value -> Parser TacticScript parseJSONList :: Value -> Parser [TacticScript]
ToJSON TacticScript
Instance details Defined in ATC.Prover Methods toJSON :: TacticScript -> Value toEncoding :: TacticScript -> Encoding toJSONList :: [TacticScript] -> Value toEncodingList :: [TacticScript] -> Encoding
ShATermConvertible TacticScript
Instance details Defined in ATC.Prover Methods toShATermAux :: ATermTable -> TacticScript -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [TacticScript] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, TacticScript) fromShATermList' :: Int -> ATermTable -> (ATermTable, [TacticScript])
type Rep TacticScript
Instance details Defined in ATC.Prover type Rep TacticScript = D1 ('MetaData "TacticScript" "Logic.Prover" "main" 'False) (C1 ('MetaCons "TacticScript" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))

data Reason Source #

failure reason

Constructors

Reason [String]

Instances

Instances details

Eq Reason Source #
Instance details Defined in Logic.Prover Methods (==) :: Reason -> Reason -> Bool (/=) :: Reason -> Reason -> Bool
Ord Reason Source #
Instance details Defined in Logic.Prover Methods compare :: Reason -> Reason -> Ordering (<) :: Reason -> Reason -> Bool (<=) :: Reason -> Reason -> Bool (>) :: Reason -> Reason -> Bool (>=) :: Reason -> Reason -> Bool max :: Reason -> Reason -> Reason min :: Reason -> Reason -> Reason
Generic Reason
Instance details Defined in ATC.Prover Associated Types type Rep Reason :: Type -> Type Methods from :: Reason -> Rep Reason x to :: Rep Reason x -> Reason
FromJSON Reason
Instance details Defined in ATC.Prover Methods parseJSON :: Value -> Parser Reason parseJSONList :: Value -> Parser [Reason]
ToJSON Reason
Instance details Defined in ATC.Prover Methods toJSON :: Reason -> Value toEncoding :: Reason -> Encoding toJSONList :: [Reason] -> Value toEncodingList :: [Reason] -> Encoding
ShATermConvertible Reason
Instance details Defined in ATC.Prover Methods toShATermAux :: ATermTable -> Reason -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Reason] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Reason) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Reason])
type Rep Reason
Instance details Defined in ATC.Prover type Rep Reason = D1 ('MetaData "Reason" "Logic.Prover" "main" 'False) (C1 ('MetaCons "Reason" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])))

data GoalStatus Source #

enumeration type representing the status of a goal

Constructors

Open Reason	failure reason
Disproved
Proved Bool	True means consistent; False inconsistent

Instances

Instances details

Eq GoalStatus Source #
Instance details Defined in Logic.Prover Methods (==) :: GoalStatus -> GoalStatus -> Bool (/=) :: GoalStatus -> GoalStatus -> Bool
Ord GoalStatus Source #
Instance details Defined in Logic.Prover Methods compare :: GoalStatus -> GoalStatus -> Ordering (<) :: GoalStatus -> GoalStatus -> Bool (<=) :: GoalStatus -> GoalStatus -> Bool (>) :: GoalStatus -> GoalStatus -> Bool (>=) :: GoalStatus -> GoalStatus -> Bool max :: GoalStatus -> GoalStatus -> GoalStatus min :: GoalStatus -> GoalStatus -> GoalStatus
Show GoalStatus Source #
Instance details Defined in Logic.Prover Methods showsPrec :: Int -> GoalStatus -> ShowS show :: GoalStatus -> String showList :: [GoalStatus] -> ShowS
Generic GoalStatus
Instance details Defined in ATC.Prover Associated Types type Rep GoalStatus :: Type -> Type Methods from :: GoalStatus -> Rep GoalStatus x to :: Rep GoalStatus x -> GoalStatus
FromJSON GoalStatus
Instance details Defined in ATC.Prover Methods parseJSON :: Value -> Parser GoalStatus parseJSONList :: Value -> Parser [GoalStatus]
ToJSON GoalStatus
Instance details Defined in ATC.Prover Methods toJSON :: GoalStatus -> Value toEncoding :: GoalStatus -> Encoding toJSONList :: [GoalStatus] -> Value toEncodingList :: [GoalStatus] -> Encoding
ShATermConvertible GoalStatus
Instance details Defined in ATC.Prover Methods toShATermAux :: ATermTable -> GoalStatus -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [GoalStatus] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, GoalStatus) fromShATermList' :: Int -> ATermTable -> (ATermTable, [GoalStatus])
type Rep GoalStatus
Instance details Defined in ATC.Prover type Rep GoalStatus = D1 ('MetaData "GoalStatus" "Logic.Prover" "main" 'False) (C1 ('MetaCons "Open" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Reason)) :+: (C1 ('MetaCons "Disproved" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Proved" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))

isOpenGoal :: GoalStatus -> Bool Source #

openGoalStatus :: GoalStatus Source #

data ProofStatus proof_tree Source #

data type representing the proof status for a goal

Constructors

ProofStatus
Fields goalName :: String goalStatus :: GoalStatus usedAxioms :: [String] used axioms usedProver :: String name of prover proofTree :: proof_tree usedTime :: TimeOfDay tacticScript :: TacticScript proofLines :: [String]

Instances

Instances details

Eq proof_tree => Eq (ProofStatus proof_tree) Source #
Instance details Defined in Logic.Prover Methods (==) :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool (/=) :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool
Ord proof_tree => Ord (ProofStatus proof_tree) Source #
Instance details Defined in Logic.Prover Methods compare :: ProofStatus proof_tree -> ProofStatus proof_tree -> Ordering (<) :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool (<=) :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool (>) :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool (>=) :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool max :: ProofStatus proof_tree -> ProofStatus proof_tree -> ProofStatus proof_tree min :: ProofStatus proof_tree -> ProofStatus proof_tree -> ProofStatus proof_tree
Show proof_tree => Show (ProofStatus proof_tree) Source #
Instance details Defined in Logic.Prover Methods showsPrec :: Int -> ProofStatus proof_tree -> ShowS show :: ProofStatus proof_tree -> String showList :: [ProofStatus proof_tree] -> ShowS
Generic (ProofStatus proof_tree)
Instance details Defined in ATC.Prover 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
FromJSON proof_tree => FromJSON (ProofStatus proof_tree)
Instance details Defined in ATC.Prover Methods parseJSON :: Value -> Parser (ProofStatus proof_tree) parseJSONList :: Value -> Parser [ProofStatus proof_tree]
ToJSON proof_tree => ToJSON (ProofStatus proof_tree)
Instance details Defined in ATC.Prover Methods toJSON :: ProofStatus proof_tree -> Value toEncoding :: ProofStatus proof_tree -> Encoding toJSONList :: [ProofStatus proof_tree] -> Value toEncodingList :: [ProofStatus proof_tree] -> Encoding
ShATermConvertible proof_tree => ShATermConvertible (ProofStatus proof_tree)
Instance details Defined in ATC.Prover 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])
type Rep (ProofStatus proof_tree)
Instance details Defined in ATC.Prover type Rep (ProofStatus proof_tree) = D1 ('MetaData "ProofStatus" "Logic.Prover" "main" 'False) (C1 ('MetaCons "ProofStatus" 'PrefixI 'True) (((S1 ('MetaSel ('Just "goalName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :: S1 ('MetaSel ('Just "goalStatus") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GoalStatus)) :: (S1 ('MetaSel ('Just "usedAxioms") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String]) :: S1 ('MetaSel ('Just "usedProver") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) :: ((S1 ('MetaSel ('Just "proofTree") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 proof_tree) :: S1 ('MetaSel ('Just "usedTime") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TimeOfDay)) :: (S1 ('MetaSel ('Just "tacticScript") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TacticScript) :*: S1 ('MetaSel ('Just "proofLines") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])))))

openProofStatus Source #

Arguments

:: Ord pt
=> String	name of the goal
-> String	name of the prover
-> pt
-> ProofStatus pt

constructs an open proof status with basic information filled in; make sure to set proofTree to a useful value before you access it.

isProvedStat :: ProofStatus proof_tree -> Bool Source #

isProvedGStat :: GoalStatus -> Bool Source #

data ProverKind Source #

different kinds of prover interfaces

Constructors

ProveGUI
ProveCMDLautomatic

Instances

Instances details

Generic ProverKind
Instance details Defined in ATC.Prover Associated Types type Rep ProverKind :: Type -> Type Methods from :: ProverKind -> Rep ProverKind x to :: Rep ProverKind x -> ProverKind
FromJSON ProverKind
Instance details Defined in ATC.Prover Methods parseJSON :: Value -> Parser ProverKind parseJSONList :: Value -> Parser [ProverKind]
ToJSON ProverKind
Instance details Defined in ATC.Prover Methods toJSON :: ProverKind -> Value toEncoding :: ProverKind -> Encoding toJSONList :: [ProverKind] -> Value toEncodingList :: [ProverKind] -> Encoding
ShATermConvertible ProverKind
Instance details Defined in ATC.Prover Methods toShATermAux :: ATermTable -> ProverKind -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [ProverKind] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, ProverKind) fromShATermList' :: Int -> ATermTable -> (ATermTable, [ProverKind])
type Rep ProverKind
Instance details Defined in ATC.Prover type Rep ProverKind = D1 ('MetaData "ProverKind" "Logic.Prover" "main" 'False) (C1 ('MetaCons "ProveGUI" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ProveCMDLautomatic" 'PrefixI 'False) (U1 :: Type -> Type))

hasProverKind :: ProverKind -> ProverTemplate x s m y z -> Bool Source #

determine if a prover kind is implemented

data FreeDefMorphism sentence morphism Source #

Constructors

FreeDefMorphism
Fields freeDefMorphism :: morphism pathFromFreeDef :: morphism freeTheory :: [Named sentence] isCofree :: Bool

Instances

Instances details

(Eq morphism, Eq sentence) => Eq (FreeDefMorphism sentence morphism) Source #
Instance details Defined in Logic.Prover Methods (==) :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> Bool (/=) :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> Bool
(Ord morphism, Ord sentence) => Ord (FreeDefMorphism sentence morphism) Source #
Instance details Defined in Logic.Prover Methods compare :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> Ordering (<) :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> Bool (<=) :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> Bool (>) :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> Bool (>=) :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> Bool max :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism min :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism
(Show morphism, Show sentence) => Show (FreeDefMorphism sentence morphism) Source #
Instance details Defined in Logic.Prover Methods showsPrec :: Int -> FreeDefMorphism sentence morphism -> ShowS show :: FreeDefMorphism sentence morphism -> String showList :: [FreeDefMorphism sentence morphism] -> ShowS
Generic (FreeDefMorphism sentence morphism)
Instance details Defined in ATC.Prover 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)
Instance details Defined in ATC.Prover Methods parseJSON :: Value -> Parser (FreeDefMorphism sentence morphism) parseJSONList :: Value -> Parser [FreeDefMorphism sentence morphism]
(ToJSON sentence, ToJSON morphism) => ToJSON (FreeDefMorphism sentence morphism)
Instance details Defined in ATC.Prover 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)
Instance details Defined in ATC.Prover 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])
type Rep (FreeDefMorphism sentence morphism)
Instance details Defined in ATC.Prover type Rep (FreeDefMorphism sentence morphism) = D1 ('MetaData "FreeDefMorphism" "Logic.Prover" "main" 'False) (C1 ('MetaCons "FreeDefMorphism" 'PrefixI 'True) ((S1 ('MetaSel ('Just "freeDefMorphism") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 morphism) :: S1 ('MetaSel ('Just "pathFromFreeDef") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 morphism)) :: (S1 ('MetaSel ('Just "freeTheory") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Named sentence]) :*: S1 ('MetaSel ('Just "isCofree") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))

data ProverTemplate theory sentence morphism sublogics proof_tree Source #

prover or consistency checker

Constructors

Prover

Fields

proverName :: String
proverUsable :: IO (Maybe String)
proverSublogic :: sublogics
proveGUI :: Maybe (String -> theory -> [FreeDefMorphism sentence morphism] -> IO ([ProofStatus proof_tree], [(Named sentence, ProofStatus proof_tree)]))
proveCMDLautomaticBatch :: Maybe (Bool -> Bool -> MVar (Result [ProofStatus proof_tree]) -> String -> TacticScript -> theory -> [FreeDefMorphism sentence morphism] -> IO (ThreadId, MVar ()))

type Prover sign sentence morphism sublogics proof_tree = ProverTemplate (Theory sign sentence proof_tree) sentence morphism sublogics proof_tree Source #

mkProverTemplate :: String -> sublogics -> (String -> theory -> [FreeDefMorphism sentence morphism] -> IO [ProofStatus proof_tree]) -> ProverTemplate theory sentence morphism sublogics proof_tree Source #

mkUsableProver :: String -> String -> sublogics -> (String -> theory -> [FreeDefMorphism sentence morphism] -> IO [ProofStatus proof_tree]) -> ProverTemplate theory sentence morphism sublogics proof_tree Source #

mkAutomaticProver :: String -> String -> sublogics -> (String -> theory -> [FreeDefMorphism sentence morphism] -> IO [ProofStatus proof_tree]) -> (Bool -> Bool -> MVar (Result [ProofStatus proof_tree]) -> String -> TacticScript -> theory -> [FreeDefMorphism sentence morphism] -> IO (ThreadId, MVar ())) -> ProverTemplate theory sentence morphism sublogics proof_tree Source #

data TheoryMorphism sign sen mor proof_tree Source #

theory morphisms between two theories

Constructors

TheoryMorphism
Fields tSource :: Theory sign sen proof_tree tTarget :: Theory sign sen proof_tree tMorphism :: mor

Instances

Instances details

Generic (TheoryMorphism sign sen mor proof_tree)
Instance details Defined in ATC.Prover 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)
Instance details Defined in ATC.Prover 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)
Instance details Defined in ATC.Prover 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)
Instance details Defined in ATC.Prover 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])
type Rep (TheoryMorphism sign sen mor proof_tree)
Instance details Defined in ATC.Prover type Rep (TheoryMorphism sign sen mor proof_tree) = D1 ('MetaData "TheoryMorphism" "Logic.Prover" "main" 'False) (C1 ('MetaCons "TheoryMorphism" 'PrefixI 'True) (S1 ('MetaSel ('Just "tSource") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Theory sign sen proof_tree)) :: (S1 ('MetaSel ('Just "tTarget") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Theory sign sen proof_tree)) :: S1 ('MetaSel ('Just "tMorphism") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 mor))))

data CCStatus proof_tree Source #

Constructors

CCStatus
Fields ccProofTree :: proof_tree ccUsedTime :: TimeOfDay ccResult :: Maybe Bool

Instances

Instances details

Generic (CCStatus proof_tree)
Instance details Defined in ATC.Prover 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
FromJSON proof_tree => FromJSON (CCStatus proof_tree)
Instance details Defined in ATC.Prover Methods parseJSON :: Value -> Parser (CCStatus proof_tree) parseJSONList :: Value -> Parser [CCStatus proof_tree]
ToJSON proof_tree => ToJSON (CCStatus proof_tree)
Instance details Defined in ATC.Prover Methods toJSON :: CCStatus proof_tree -> Value toEncoding :: CCStatus proof_tree -> Encoding toJSONList :: [CCStatus proof_tree] -> Value toEncodingList :: [CCStatus proof_tree] -> Encoding
ShATermConvertible proof_tree => ShATermConvertible (CCStatus proof_tree)
Instance details Defined in ATC.Prover 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])
type Rep (CCStatus proof_tree)
Instance details Defined in ATC.Prover type Rep (CCStatus proof_tree) = D1 ('MetaData "CCStatus" "Logic.Prover" "main" 'False) (C1 ('MetaCons "CCStatus" 'PrefixI 'True) (S1 ('MetaSel ('Just "ccProofTree") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 proof_tree) :: (S1 ('MetaSel ('Just "ccUsedTime") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TimeOfDay) :: S1 ('MetaSel ('Just "ccResult") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool)))))

data ConsChecker sign sentence sublogics morphism proof_tree Source #

Constructors

ConsChecker
Fields ccName :: String ccUsable :: IO (Maybe String) ccSublogic :: sublogics ccBatch :: Bool ccNeedsTimer :: Bool ccAutomatic :: String -> TacticScript -> TheoryMorphism sign sentence morphism proof_tree -> [FreeDefMorphism sentence morphism] -> IO (CCStatus proof_tree)

mkConsChecker :: String -> sublogics -> (String -> TacticScript -> TheoryMorphism sign sentence morphism proof_tree -> [FreeDefMorphism sentence morphism] -> IO (CCStatus proof_tree)) -> ConsChecker sign sentence sublogics morphism proof_tree Source #

mkUsableConsChecker :: String -> String -> sublogics -> (String -> TacticScript -> TheoryMorphism sign sentence morphism proof_tree -> [FreeDefMorphism sentence morphism] -> IO (CCStatus proof_tree)) -> ConsChecker sign sentence sublogics morphism proof_tree Source #

Orphan instances

Pretty a => Pretty (ElemWOrd a) Source #
Instance details Methods pretty :: ElemWOrd a -> Doc Source # pretties :: [ElemWOrd a] -> Doc Source #