Prover.hs revision f1af441c245fbecb3453fa730eed772519f293cc
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder{-# LANGUAGE DeriveDataTypeable #-}
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiDescription : General datastructures for theorem prover interfaces
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiCopyright : (c) Till Mossakowski, Klaus Luettich, Uni Bremen 2002-2005
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : till@informatik.uni-bremen.de
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : non-portable (deriving Typeable)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiGeneral datastructures for theorem prover interfaces
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Common.OrderedMap as OMap
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Data.Map as Map
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Data.Time (TimeOfDay, midnight)
0c2a90cbfb63865ff485c3fbe20a14589a5914beTill Mossakowskiimport qualified Control.Concurrent as Concurrent
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- * pack sentences with their proofs
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski{- | instead of the sentence name (that will be the key into the order map)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskithe theorem status will be stored as attribute. The theorem status will be a
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder(wrapped) list of pairs (AnyComorphism, BasicProof) in G_theory, but a wrapped
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederlist of (ProofStatus proof_tree) in a logic specific 'Theory'. -}
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskitype SenStatus a tStatus = SenAttr a (ThmStatus tStatus)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskithmStatus :: SenStatus a tStatus -> [tStatus]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskithmStatus = getThmStatus . senAttr
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- | the wrapped list of proof scripts or (AnyComorphism, BasicProof) pairs
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskidata ThmStatus a = ThmStatus { getThmStatus :: [a] } deriving (Show, Eq, Ord)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance (Show b, Pretty a) => Pretty (SenAttr a b) where
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski pretty = printSenStatus pretty
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiprintSenStatus :: (a -> Doc) -> SenAttr a b -> Doc
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiprintSenStatus = (. sentence)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiemptySenStatus :: SenStatus a b
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederemptySenStatus = makeNamed (ThmStatus []) $ error "emptySenStatus"
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederinstance Pretty a => Pretty (OMap.ElemWOrd a) where
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder pretty = printOMapElemWOrd pretty
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiprintOMapElemWOrd :: (a -> Doc) -> OMap.ElemWOrd a -> Doc
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiprintOMapElemWOrd = (. OMap.ele)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- | the map from lables to the theorem plus status (and position)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedertype ThSens a b = OMap.OMap String (SenStatus a b)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskinoSens :: ThSens a b
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedermapThSensValueM :: Monad m => (a -> m b) -> ThSens a c -> m (ThSens b c)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedermapThSensValueM f = foldM (\ m (k, v) -> do
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski ns <- f $ sentence oe
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski let ne = oe { sentence = ns }
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return $ Map.insert k v { OMap.ele = ne } m) Map.empty . Map.toList
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder{- | join and disambiguate
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder * separate Axioms from Theorems
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder * don't merge sentences with same key but different contents?
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederjoinSensAux :: (Ord a, Eq b) => ThSens a b -> ThSens a b
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -> (ThSens a b, [(String, String)])
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederjoinSensAux s1 s2 = let
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder updN n (_, e) = (n, e)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder m = if null l1 then 0 else maximum $ map (OMap.order . snd) l1
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder l2 = map (\ (x, e) -> (x, e {OMap.order = m + OMap.order e }))
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder sl2 = genericDisambigSens m fst updN (Map.keysSet s1) l2
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski in (Map.fromList $ l1 ++ sl2,
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski zipWith (\ (n1, _) (n2, _) -> (n1, n2)) l2 sl2)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederjoinSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b -> ThSens a b
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederjoinSens s1 = fst . joinSensAux s1
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederreduceSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski . groupBy (\ (_, a) (_, b) -> sentence (OMap.ele a) == sentence (OMap.ele b))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski . sortBy cmpSnd
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskicmpSnd :: (Ord a1) => (String, OMap.ElemWOrd (SenStatus a1 b))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> (String, OMap.ElemWOrd (SenStatus a1 b)) -> Ordering
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedercmpSnd (_, a) (_, b) = cmpSenEle a b
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedercmpSenEle :: (Ord a1) => OMap.ElemWOrd (SenStatus a1 b)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> OMap.ElemWOrd (SenStatus a1 b) -> Ordering
612749008484b6773aedf4d6bbc85b8d074d15c6Christian MaedercmpSenEle x y = case (OMap.ele x, OMap.ele y) of
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder (d1, d2) -> compare
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (sentence d1, isAxiom d2, isDef d2) (sentence d2, isAxiom d1, isDef d1)
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaedermapValue :: (a -> b) -> SenStatus a c -> SenStatus b c
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaedermapValue f d = d { sentence = f $ sentence d }
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder{- | sets the field isAxiom according to the boolean value;
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder if isAxiom is False for a sentence and set to True,
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder the field wasTheorem is set to True.
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedermarkAsAxiom :: Ord a => Bool -> ThSens a b -> ThSens a b
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskimarkAsAxiom b = OMap.map $ \ d -> d
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski { isAxiom = b
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski , wasTheorem = b && (not (isAxiom d) || wasTheorem d) }
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskimarkAsGoal :: Ord a => ThSens a b -> ThSens a b
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskimarkAsGoal = markAsAxiom False
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskitoNamedList :: ThSens a b -> [AS_Anno.Named a]
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskitoNamedList = map (uncurry toNamed) . OMap.toList
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskitoNamed :: String -> SenStatus a b -> AS_Anno.Named a
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskitoNamed k s = s { AS_Anno.senAttr = k }
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- | putting Sentences from a list into a map
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedertoThSens :: Ord a => [AS_Anno.Named a] -> ThSens a b
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder ( \ v -> (AS_Anno.senAttr v, v { senAttr = ThmStatus [] }))
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder . nameAndDisambiguate
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- | theories with a signature and sentences with proof states
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederdata Theory sign sen proof_tree =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Theory sign (ThSens sen (ProofStatus proof_tree))
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- e.g. the file name, or the script itself, or a configuration string
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederdata TacticScript = TacticScript String deriving (Eq, Ord, Show)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- | failure reason
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederdata Reason = Reason [String]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederinstance Ord Reason where
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder compare _ _ = EQ
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederinstance Eq Reason where
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder a == b = compare a b == EQ
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- | enumeration type representing the status of a goal
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskidata GoalStatus =
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Open Reason -- ^ failure reason
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder | Proved Bool -- ^ True means consistent; False inconsistent
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski deriving (Eq, Ord)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederinstance Show GoalStatus where
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski show gs = case gs of
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Open (Reason l) -> unlines $ "Open" : l
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Disproved -> "Disproved"
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Proved c -> "Proved" ++ if c then "" else "(inconsistent)"
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederisOpenGoal :: GoalStatus -> Bool
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederisOpenGoal gs = case gs of
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Open _ -> True
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederopenGoalStatus :: GoalStatus
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiopenGoalStatus = Open $ Reason []
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- | data type representing the proof status for a goal
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskidata ProofStatus proof_tree = ProofStatus
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder { goalName :: String
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , goalStatus :: GoalStatus
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , usedAxioms :: [String] -- ^ used axioms
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , usedProver :: String -- ^ name of prover
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , proofTree :: proof_tree
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , usedTime :: TimeOfDay
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , tacticScript :: TacticScript }
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski deriving (Show, Eq, Ord)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski{- | constructs an open proof status with basic information filled in;
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski make sure to set proofTree to a useful value before you access it. -}
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiopenProofStatus :: Ord pt => String -- ^ name of the goal
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> String -- ^ name of the prover
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> pt -> ProofStatus pt
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiopenProofStatus goalname provername proof_tree = ProofStatus
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski { goalName = goalname
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , goalStatus = openGoalStatus
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , usedAxioms = []
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , usedProver = provername
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , proofTree = proof_tree
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , usedTime = midnight
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , tacticScript = TacticScript "" }
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiisProvedStat :: ProofStatus proof_tree -> Bool
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederisProvedStat = isProvedGStat . goalStatus
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederisProvedGStat :: GoalStatus -> Bool
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiisProvedGStat gs = case gs of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Proved _ -> True
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- | different kinds of prover interfaces
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskidata ProverKind = ProveGUI | ProveCMDLautomatic
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- | determine if a prover kind is implemented
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskihasProverKind :: ProverKind -> ProverTemplate x s m y z -> Bool
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskihasProverKind pk pt = case pk of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ProveGUI -> isJust $ proveGUI pt
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ProveCMDLautomatic -> isJust $ proveCMDLautomaticBatch pt
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskidata FreeDefMorphism sentence morphism = FreeDefMorphism
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski { freeDefMorphism :: morphism
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , pathFromFreeDef :: morphism
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , freeTheory :: [AS_Anno.Named sentence]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , isCofree :: Bool }
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski deriving (Eq, Show)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- | prover or consistency checker
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskidata ProverTemplate theory sentence morphism sublogics proof_tree = Prover
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski { proverName :: String,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski proverSublogic :: sublogics,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski proveGUI :: Maybe (String -> theory -> [FreeDefMorphism sentence morphism]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> IO ( [ProofStatus proof_tree]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , [(Named sentence, ProofStatus proof_tree)])),
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski {- input: imported theories, theory name, theory (incl. goals)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski fst --> proof status for goals and lemmas
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski snd --> new lemmas (with proofs) -}
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski proveCMDLautomaticBatch ::
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Maybe (Bool -- 1.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> Bool -- 2.
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder -> Concurrent.MVar (Result [ProofStatus proof_tree]) -- 3.
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder -> String -- 4.
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder -> TacticScript -- 5.
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder -> theory -- 6.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> [FreeDefMorphism sentence morphism]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> IO (Concurrent.ThreadId, Concurrent.MVar ())) -- output
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 1. True means include proven theorems in subsequent proof attempts;
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 2. True means save problem file for each goal;
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 3. MVar reference to a Result [] or empty MVar,
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder used to store the result of each attempt in the batch run;
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder 4. theory name;
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 5. default TacticScript;
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (incl. goals and Open SenStatus for individual tactic_scripts)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 7. ingoing free def morphisms
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder fst --> identifier of the batch thread for killing it,
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder after each proof attempt the result is stored in the IOref
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski snd --> MVar to wait for the end of the thread -}
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder } deriving Typeable
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskitype Prover sign sentence morphism sublogics proof_tree =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ProverTemplate (Theory sign sentence proof_tree)
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder sentence morphism sublogics proof_tree
612749008484b6773aedf4d6bbc85b8d074d15c6Christian MaedermkProverTemplate :: String -> sublogics
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> (String -> theory -> [FreeDefMorphism sentence morphism]
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder -> IO [ProofStatus proof_tree])
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> ProverTemplate theory sentence morphism sublogics proof_tree
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimkProverTemplate str sl fct = Prover
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder { proverName = str
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder , proverSublogic = sl
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder , proveGUI = Just $ \ s t fs -> do
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder ps <- fct s t fs
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return (ps, [])
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , proveCMDLautomaticBatch = Nothing }
612749008484b6773aedf4d6bbc85b8d074d15c6Christian MaedermkAutomaticProver :: String -> sublogics
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> (String -> theory -> [FreeDefMorphism sentence morphism]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> IO [ProofStatus proof_tree])
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder -> (Bool -> Bool -> Concurrent.MVar (Result [ProofStatus proof_tree])
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> String -> TacticScript -> theory -> [FreeDefMorphism sentence morphism]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> IO (Concurrent.ThreadId, Concurrent.MVar ()))
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder -> ProverTemplate theory sentence morphism sublogics proof_tree
612749008484b6773aedf4d6bbc85b8d074d15c6Christian MaedermkAutomaticProver str sl fct bFct =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (mkProverTemplate str sl fct)
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder { proveCMDLautomaticBatch = Just bFct }
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- | theory morphisms between two theories
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maederdata TheoryMorphism sign sen mor proof_tree = TheoryMorphism
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder { tSource :: Theory sign sen proof_tree
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder , tTarget :: Theory sign sen proof_tree
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski , tMorphism :: mor }
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskidata CCStatus proof_tree = CCStatus
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski { ccProofTree :: proof_tree
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski , ccUsedTime :: TimeOfDay
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski , ccResult :: Maybe Bool }
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskidata ConsChecker sign sentence sublogics morphism proof_tree = ConsChecker
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski { ccName :: String
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski , ccSublogic :: sublogics
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski , ccBatch :: Bool -- True for batch checkers
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski , ccNeedsTimer :: Bool -- True for checkers that ignore time limits
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski , ccAutomatic :: String -- 1.
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski -> TacticScript -- 2.
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski -> TheoryMorphism sign sentence morphism proof_tree -- 3.
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski -> [FreeDefMorphism sentence morphism] -- 4.
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski -> IO (CCStatus proof_tree) -- output
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski -- input: 1. theory name
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski -- 2. default TacticScript
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- 3. theory morphism
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder -- 5. ingoing free definition morphisms
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- output: consistency result status
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski } deriving Typeable
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedermkConsChecker :: String -> sublogics
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -> (String -> TacticScript -> TheoryMorphism sign sentence morphism proof_tree
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -> [FreeDefMorphism sentence morphism] -> IO (CCStatus proof_tree))
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -> ConsChecker sign sentence sublogics morphism proof_tree
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedermkConsChecker n sl f = ConsChecker
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski , ccSublogic = sl
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski , ccBatch = True
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder , ccNeedsTimer = True
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder , ccAutomatic = f }