Prover.hs revision f094a7999dfa79cad2eb34ce15f1939c0d6b9e39
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederModule : $Header$
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederDescription : General datastructures for theorem prover interfaces
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederCopyright : (c) Till Mossakowski, Klaus Luettich, Uni Bremen 2002-2005
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederMaintainer : till@informatik.uni-bremen.de
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederStability : provisional
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederPortability : non-portable (deriving Typeable)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederGeneral datastructures for theorem prover interfaces
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport qualified Common.OrderedMap as OMap
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport qualified Data.Map as Map
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport Data.Time (TimeOfDay,midnight)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport qualified Control.Concurrent as Concurrent
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- * pack sentences with their proofs
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{- | instead of the sentence name (that will be the key into the order map)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederthe theorem status will be stored as attribute. The theorem status will be a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder(wrapped) list of pairs (AnyComorphism, BasicProof) in G_theory, but a wrapped
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederlist of (Proof_status proof_tree) in a logic specific 'Theory'. -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedertype SenStatus a tStatus = SenAttr a (ThmStatus tStatus)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederthmStatus :: SenStatus a tStatus -> [tStatus]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederthmStatus = getThmStatus . senAttr
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | the wrapped list of proof scripts or (AnyComorphism, BasicProof) pairs
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederdata ThmStatus a = ThmStatus { getThmStatus :: [a] } deriving Show
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederinstance Eq (ThmStatus a) where
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder _ == _ = True
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- Ord must be consistent with Eq
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederinstance Ord (ThmStatus a) where
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder compare _ _ = EQ
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederinstance (Show b, Pretty a) => Pretty (SenAttr a b) where
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder pretty = printSenStatus pretty
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederprintSenStatus :: (a -> Doc) -> SenAttr a b -> Doc
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederprintSenStatus fA = fA . sentence
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederemptySenStatus :: SenStatus a b
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederemptySenStatus = makeNamed (ThmStatus []) $ error "emptySenStatus"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederinstance Pretty a => Pretty (OMap.ElemWOrd a) where
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder pretty = printOMapElemWOrd pretty
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederprintOMapElemWOrd :: (a -> Doc) -> OMap.ElemWOrd a -> Doc
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederprintOMapElemWOrd fA = fA . OMap.ele
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | the map from lables to the theorem plus status (and position)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedertype ThSens a b = OMap.OMap String (SenStatus a b)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedernoSens :: ThSens a b
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermapThSensValueM :: Monad m => (a -> m b) -> ThSens a c -> m (ThSens b c)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermapThSensValueM f = foldM (\ m (k, v) -> do
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ns <- f $ sentence oe
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder let ne = oe { sentence = ns }
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder return $ Map.insert k v { OMap.ele = ne } m) Map.empty . Map.toList
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermapThSensStatus :: (b -> c) -> ThSens a b -> ThSens a c
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermapThSensStatus f = OMap.map (mapStatus f)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | join and disambiguate
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- * separate Axioms from Theorems
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- * don't merge sentences with same key but different contents?
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederjoinSens :: (Ord a,Eq b) => ThSens a b -> ThSens a b -> ThSens a b
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederjoinSens s1 s2 = let
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder l1 = sortBy cmpSnd $ Map.toList s1
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder updN n (_, e) = (n, e)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder l2 = map (\ (x,e) -> (x,e {OMap.order = m + OMap.order e })) $
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder sortBy cmpSnd $ Map.toList s2
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder in Map.fromList $ mergeSens l1 $
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder genericDisambigSens fst updN (OMap.keysSet s1) l2
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder where mergeSens [] l2 = l2
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder mergeSens l1 [] = l1
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder mergeSens l1@((k1, e1) : r1) l2@((k2, e2) : r2) =
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder case cmpSenEle e1 e2 of
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder LT -> (k1, e1) : mergeSens r1 l2
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder { senAttr = ThmStatus $
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder union (thmStatus $ OMap.ele e1)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (thmStatus $ OMap.ele e2)}})
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder : mergeSens r1 r2
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder GT -> (k2, e2) : mergeSens l1 r2
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedercmpSnd :: (Ord a1) => (String, OMap.ElemWOrd (SenStatus a1 b))
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> (String, OMap.ElemWOrd (SenStatus a1 b)) -> Ordering
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedercmpSnd (_, a) (_, b) = cmpSenEle a b
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedercmpSenEle :: (Ord a1) => OMap.ElemWOrd (SenStatus a1 b)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> OMap.ElemWOrd (SenStatus a1 b) -> Ordering
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedercmpSenEle x y = case (OMap.ele x,OMap.ele y) of
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (d1, d2) -> compare
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder (sentence d1, isAxiom d1, isDef d1) (sentence d2, isAxiom d2, isDef d2)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederdiffSens :: (Ord a,Eq b) => ThSens a b -> ThSens a b -> ThSens a b
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederdiffSens s1 s2 = let
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder l1 = sortBy cmpSnd $ Map.toList s1
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder l2 = sortBy cmpSnd $ Map.toList s2
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder in Map.fromList $ diffS l1 l2
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder where diffS [] _ = []
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder diffS l1 [] = l1
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder diffS l1@((k1, e1) : r1) l2@((_, e2) : r2) =
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder case cmpSenEle e1 e2 of
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder LT -> (k1, e1) : diffS r1 l2
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder EQ -> diffS r1 r2
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder GT -> diffS l1 r2
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermapValue :: (a -> b) -> SenStatus a c -> SenStatus b c
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermapValue f d = d { sentence = f $ sentence d }
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermapStatus :: (b -> c) -> SenStatus a b -> SenStatus a c
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermapStatus f d = d { senAttr = ThmStatus $ map f $ thmStatus d }
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | sets the field isAxiom according to the boolean value;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- if isAxiom is False for a sentence and set to True,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- the field wasTheorem is set to True
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermarkAsAxiom :: Ord a => Bool -> ThSens a b -> ThSens a b
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermarkAsAxiom b = OMap.map $ \ d -> d
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder { isAxiom = b
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , wasTheorem = b && (not (isAxiom d) || wasTheorem d) }
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermarkAsGoal :: Ord a => ThSens a b -> ThSens a b
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermarkAsGoal = markAsAxiom False
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedertoNamedList :: ThSens a b -> [AS_Anno.Named a]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedertoNamedList = map (uncurry toNamed) . OMap.toList
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedertoNamed :: String -> SenStatus a b -> AS_Anno.Named a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedertoNamed k s = s { AS_Anno.senAttr = k }
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | putting Sentences from a list into a map
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedertoThSens :: Ord a => [AS_Anno.Named a] -> ThSens a b
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ( \ v -> (AS_Anno.senAttr v, v { senAttr = ThmStatus [] }))
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder . nameAndDisambiguate
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | theories with a signature and sentences with proof states
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederdata Theory sign sen proof_tree =
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Theory sign (ThSens sen (Proof_status proof_tree))
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermapTheoryStatus :: (a->b) -> Theory sign sentence a
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> Theory sign sentence b
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermapTheoryStatus f (Theory sig thSens) =
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Theory sig (mapThSensStatus (mapProofStatus f) thSens)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | theory morphisms between two theories
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederdata TheoryMorphism sign sen mor proof_tree = TheoryMorphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder { t_source :: Theory sign sen proof_tree
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , t_target :: Theory sign sen proof_tree
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , t_morphism :: mor }
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- e.g. the file name, or the script itself, or a configuration string
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederdata Tactic_script = Tactic_script String deriving (Eq, Ord, Show)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | enumeration type representing the status of a goal
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederdata GoalStatus = Open | Disproved
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder | Proved (Maybe Bool) -- ^ Just True means consistent; Nothing don't know
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder deriving (Eq, Ord)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- needed for automated theorem provers like SPASS;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- provers like Isabelle set it to Nothing
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederinstance Show GoalStatus where
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder show gs = case gs of
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Open -> "Open"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Disproved -> "Disproved"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Proved mc -> "Proved" ++ maybe ""
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ( \ c -> "(" ++ (if c then "" else "in") ++ "consistent)") mc
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | data type representing the proof status for a goal or
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederdata Proof_status proof_tree = Proof_status
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder { goalName :: String
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , goalStatus :: GoalStatus
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , usedAxioms :: [String] -- ^ used axioms
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , proverName :: String -- ^ name of prover
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , proofTree :: proof_tree
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , usedTime :: TimeOfDay
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , tacticScript :: Tactic_script }
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder | Consistent Tactic_script
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder deriving (Show, Eq, Ord)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{- | constructs an open proof status with basic information filled in;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder make sure to set proofTree to a useful value before you access it. -}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederopenProof_status :: Ord pt => String -- ^ name of the goal
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> String -- ^ name of the prover
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> pt -> Proof_status pt
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederopenProof_status goalname provername proof_tree = Proof_status
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder { goalName = goalname
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , goalStatus = Open
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , usedAxioms = []
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , proverName = provername
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , proofTree = proof_tree
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , usedTime = midnight
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , tacticScript = Tactic_script "" }
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermapProofStatus :: (a->b) -> Proof_status a -> Proof_status b
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermapProofStatus f st = st {proofTree = f $ proofTree st}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederisProvedStat :: Proof_status proof_tree -> Bool
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederisProvedStat pst = case pst of
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Consistent _ -> False
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder _ -> isProvedGStat . goalStatus $ pst
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederisProvedGStat :: GoalStatus -> Bool
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederisProvedGStat gs = case gs of
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Proved _ -> True
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedergoalUsedInProof :: Monad m => Proof_status proof_tree -> m Bool
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedergoalUsedInProof pst = case goalStatus pst of
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Proved m -> maybe (fail "don't know if goal was used") return m
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder _ -> fail "not a proof"
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | different kinds of prover interfaces
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederdata ProverKind = ProveGUI | ProveCMDLautomatic | ProveCMDLinteractive
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | determine if a prover kind is implemented
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederhasProverKind :: ProverKind -> ProverTemplate x m y z -> Bool
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederhasProverKind pk pt = case pk of
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ProveGUI -> isJust $ proveGUI pt
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ProveCMDLautomatic ->
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder isJust (proveCMDLautomatic pt) && isJust (proveCMDLautomaticBatch pt)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ProveCMDLinteractive -> isJust $ proveCMDLinteractive pt
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederdata FreeDefMorphism morphism = FreeDefMorphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder { freeDefMorphism :: morphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , pathFromFreeDef :: morphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , isCofree :: Bool }
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder deriving (Eq, Show)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | prover or consistency checker
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederdata ProverTemplate theory morphism sublogics proof_tree = Prover
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder { prover_name :: String,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder prover_sublogic :: sublogics,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder proveGUI :: Maybe (String -> theory -> [FreeDefMorphism morphism]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> IO ([Proof_status proof_tree])),
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- input: imported theories, theory name, theory (incl. goals)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- output: proof status for goals and lemmas
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder proveCMDLautomatic :: Maybe (String -> Tactic_script
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> theory -> [FreeDefMorphism morphism]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ->IO (Result ([Proof_status proof_tree]))),
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- blocks until a result is determined
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- input: theory name, Tactic_script,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- theory (incl. goals, but only the first one is tried)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- output: proof status for goals and lemmas
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder proveCMDLinteractive :: Maybe (String -> Tactic_script
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> theory -> [FreeDefMorphism morphism] -> IO (Result ([Proof_status proof_tree]))),
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- input, output: see above
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder proveCMDLautomaticBatch ::
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Maybe (Bool -- 1.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> Bool -- 2.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> Concurrent.MVar (Result [Proof_status proof_tree]) -- 3.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> String -- 4.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> Tactic_script -- 5.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> theory -- 6.
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> [FreeDefMorphism morphism]
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> IO (Concurrent.ThreadId,Concurrent.MVar ())) -- output
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- input: 1. True means include proven theorems in subsequent
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- proof attempts;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- 2. True means save problem file for each goal;
4c4a3329080becd4b81d56396586b740487924cbChristian Maeder -- 3. MVar reference to a Result [] or empty MVar,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- used to store the result of each attempt in the batch run;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- 4. theory name;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- 5. default Tactic_script;
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- 6. theory (incl. goals and
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- Open SenStatus for individual tactic_scripts)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- output: fst --> identifier of the batch thread for killing it,
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -- after each proof attempt the result is stored in the
4c4a3329080becd4b81d56396586b740487924cbChristian Maeder -- snd --> MVar to wait for the end of the thread
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder } deriving Typeable
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedertype Prover sign sentence morphism sublogics proof_tree =
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ProverTemplate (Theory sign sentence proof_tree) morphism sublogics proof_tree
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermkProverTemplate :: String -> sublogics
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> (String -> theory -> [FreeDefMorphism morphism] -> IO ([Proof_status proof_tree]))
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder -> ProverTemplate theory morphism sublogics proof_tree
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaedermkProverTemplate str sl fct = Prover
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder { prover_name = str
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , prover_sublogic = sl
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , proveGUI = Just fct
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , proveCMDLautomatic = Nothing
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , proveCMDLinteractive = Nothing
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder , proveCMDLautomaticBatch = Nothing }
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedertype ConsChecker sign sentence sublogics morphism proof_tree =
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder ProverTemplate (TheoryMorphism sign sentence morphism proof_tree)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder morphism sublogics proof_tree