7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder{- |

7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederModule : $Header$

2dc26996d32244796c48c71fe44413c8ebf8bbc9Christian MaederDescription : General datastructures for theorem prover interfaces

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaederCopyright : (c) Till Mossakowski, Klaus Luettich, Uni Bremen 2002-2005

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederMaintainer : till@informatik.uni-bremen.de

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : provisional

7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederPortability : non-portable (deriving Typeable)

a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder

08faa81d4dd8409cd923b334064f64f802ecc33dChristian MaederGeneral datastructures for theorem prover interfaces

2dc26996d32244796c48c71fe44413c8ebf8bbc9Christian Maeder-}

08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maeder

08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maedermodule Logic.Prover where

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maederimport Common.AS_Annotation as AS_Anno

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.Doc

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport Common.DocUtils

23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maederimport Common.Result

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.ProofUtils

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport qualified Common.OrderedMap as OMap

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederimport qualified Data.Map as Map

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport Data.List

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Data.Maybe (isJust)

23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maederimport Data.Time (TimeOfDay, midnight)

2dc26996d32244796c48c71fe44413c8ebf8bbc9Christian Maederimport Data.Typeable

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maederimport Control.Monad

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maederimport qualified Control.Concurrent as Concurrent

a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- * pack sentences with their proofs

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder{- | instead of the sentence name (that will be the key into the order map)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederthe theorem status will be stored as attribute. The theorem status will be a

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder(wrapped) list of pairs (AnyComorphism, BasicProof) in G_theory, but a wrapped

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederlist of (ProofStatus proof_tree) in a logic specific 'Theory'. -}

a0e24c863b78669b05797ff8ce635995a9bede44Christian Maedertype SenStatus a tStatus = SenAttr a (ThmStatus tStatus)

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder

81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederthmStatus :: SenStatus a tStatus -> [tStatus]

81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederthmStatus = getThmStatus . senAttr

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder-- | the wrapped list of proof scripts or (AnyComorphism, BasicProof) pairs

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederdata ThmStatus a = ThmStatus { getThmStatus :: [a] } deriving (Show, Eq, Ord)

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederinstance (Show b, Pretty a) => Pretty (SenAttr a b) where

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder pretty = printSenStatus pretty

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaederprintSenStatus :: (a -> Doc) -> SenAttr a b -> Doc

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaederprintSenStatus = (. sentence)

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaederemptySenStatus :: SenStatus a b

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaederemptySenStatus = makeNamed (ThmStatus []) $ error "emptySenStatus"

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maederinstance Pretty a => Pretty (OMap.ElemWOrd a) where

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder pretty = printOMapElemWOrd pretty

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaederprintOMapElemWOrd :: (a -> Doc) -> OMap.ElemWOrd a -> Doc

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaederprintOMapElemWOrd = (. OMap.ele)

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder-- | the map from lables to the theorem plus status (and position)

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maedertype ThSens a b = OMap.OMap String (SenStatus a b)

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian MaedernoSens :: ThSens a b

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian MaedernoSens = OMap.empty

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaedermapThSensValueM :: Monad m => (a -> m b) -> ThSens a c -> m (ThSens b c)

7feac39f792f587cffdc8b63b0e7c5a7d2de292eChristian MaedermapThSensValueM f = foldM (\ m (k, v) -> do

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder let oe = OMap.ele v

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder ns <- f $ sentence oe

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder let ne = oe { sentence = ns }

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder return $ Map.insert k v { OMap.ele = ne } m) Map.empty . Map.toList

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaedermapThSensStatus :: (b -> c) -> ThSens a b -> ThSens a c

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaedermapThSensStatus = OMap.map . mapStatus

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder-- | join and disambiguate

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder--

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder-- * separate Axioms from Theorems

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder--

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- * don't merge sentences with same key but different contents?

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaederjoinSensAux :: (Ord a, Eq b) => ThSens a b -> ThSens a b

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder -> (ThSens a b, [(String, String)])

81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederjoinSensAux s1 s2 = let

a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder l1 = Map.toList s1

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder updN n (_, e) = (n, e)

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder m = OMap.size s1

a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder l2 = map (\ (x, e) -> (x, e {OMap.order = m + OMap.order e }))

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder $ Map.toList s2

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder sl2 = genericDisambigSens m fst updN (OMap.keysSet s1) l2

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder in (Map.fromList $ l1 ++ sl2,

a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder zipWith (\ (n1, _) (n2, _) -> (n1, n2)) l2 sl2)

a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder

a0e24c863b78669b05797ff8ce635995a9bede44Christian MaederjoinSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b -> ThSens a b

81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederjoinSens s1 = fst . joinSensAux s1

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder

81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederreduceSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian MaederreduceSens =

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder Map.fromList

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder . map head

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder . groupBy (\ (_, a) (_, b) -> let e = OMap.ele b in

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder sentence (OMap.ele a) == sentence e && isAxiom e)

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder . sortBy cmpSnd

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder . Map.toList

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian MaedercmpSnd :: (Ord a1) => (String, OMap.ElemWOrd (SenStatus a1 b))

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder -> (String, OMap.ElemWOrd (SenStatus a1 b)) -> Ordering

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian MaedercmpSnd (_, a) (_, b) = cmpSenEle a b

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder

32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian MaedercmpSenEle :: (Ord a1) => OMap.ElemWOrd (SenStatus a1 b)

32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder -> OMap.ElemWOrd (SenStatus a1 b) -> Ordering

32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian MaedercmpSenEle x y = case (OMap.ele x, OMap.ele y) of

32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder (d1, d2) -> compare

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder (sentence d1, isAxiom d2, isDef d2) (sentence d2, isAxiom d1, isDef d1)

a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder

a0e24c863b78669b05797ff8ce635995a9bede44Christian MaedermapValue :: (a -> b) -> SenStatus a c -> SenStatus b c

a0e24c863b78669b05797ff8ce635995a9bede44Christian MaedermapValue f d = d { sentence = f $ sentence d }

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedermapStatus :: (b -> c) -> SenStatus a b -> SenStatus a c

a0e24c863b78669b05797ff8ce635995a9bede44Christian MaedermapStatus f d = d { senAttr = ThmStatus $ map f $ thmStatus d }

32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder

32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder-- | sets the field isAxiom according to the boolean value;

32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder-- if isAxiom is False for a sentence and set to True,

32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder-- the field wasTheorem is set to True

32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian MaedermarkAsAxiom :: Ord a => Bool -> ThSens a b -> ThSens a b

a0e24c863b78669b05797ff8ce635995a9bede44Christian MaedermarkAsAxiom b = OMap.map $ \ d -> d

32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder { isAxiom = b

a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder , wasTheorem = b && (not (isAxiom d) || wasTheorem d) }

32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedermarkAsGoal :: Ord a => ThSens a b -> ThSens a b

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedermarkAsGoal = markAsAxiom False

a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedertoNamedList :: ThSens a b -> [AS_Anno.Named a]

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian MaedertoNamedList = map (uncurry toNamed) . OMap.toList

32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedertoNamed :: String -> SenStatus a b -> AS_Anno.Named a

afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedertoNamed k s = s { AS_Anno.senAttr = k }

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder-- | putting Sentences from a list into a map

a0e24c863b78669b05797ff8ce635995a9bede44Christian MaedertoThSens :: Ord a => [AS_Anno.Named a] -> ThSens a b

afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedertoThSens = OMap.fromList . map

a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder ( \ v -> (AS_Anno.senAttr v, v { senAttr = ThmStatus [] }))

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder . nameAndDisambiguate

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- | theories with a signature and sentences with proof states

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederdata Theory sign sen proof_tree =

a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder Theory sign (ThSens sen (ProofStatus proof_tree))

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedermapTheoryStatus :: (a -> b) -> Theory sign sentence a

a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder -> Theory sign sentence b

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaedermapTheoryStatus f (Theory sig thSens) =

a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder Theory sig (mapThSensStatus (mapProofStatus f) thSens)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- e.g. the file name, or the script itself, or a configuration string

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederdata TacticScript = TacticScript String deriving (Eq, Ord, Show)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder-- | failure reason

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederdata Reason = Reason [String]

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederinstance Ord Reason where

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder compare _ _ = EQ

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederinstance Eq Reason where

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder a == b = compare a b == EQ

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder-- | enumeration type representing the status of a goal

a0e24c863b78669b05797ff8ce635995a9bede44Christian Maederdata GoalStatus =

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder Open Reason -- ^ failure reason

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder | Disproved

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder | Proved Bool -- ^ Just True means consistent; False inconsistent

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder deriving (Eq, Ord)

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder -- needed for automated theorem provers like SPASS;

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder -- provers like Isabelle set it to Nothing

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederinstance Show GoalStatus where

show gs = case gs of

Open (Reason l) -> unlines $ "Open" : l

Disproved -> "Disproved"

Proved c -> "Proved" ++ if c then "" else "(inconsistent)"

isOpenGoal :: GoalStatus -> Bool

isOpenGoal gs = case gs of

Open _ -> True

_ -> False

openGoalStatus :: GoalStatus

openGoalStatus = Open $ Reason []

-- | data type representing the proof status for a goal

data ProofStatus proof_tree = ProofStatus

{ goalName :: String

, goalStatus :: GoalStatus

, usedAxioms :: [String] -- ^ used axioms

, usedProver :: String -- ^ name of prover

, proofTree :: proof_tree

, usedTime :: TimeOfDay

, tacticScript :: TacticScript }

deriving (Show, Eq, Ord)

{- | constructs an open proof status with basic information filled in;

make sure to set proofTree to a useful value before you access it. -}

openProofStatus :: Ord pt => String -- ^ name of the goal

-> String -- ^ name of the prover

-> pt -> ProofStatus pt

openProofStatus goalname provername proof_tree = ProofStatus

{ goalName = goalname

, goalStatus = openGoalStatus

, usedAxioms = []

, usedProver = provername

, proofTree = proof_tree

, usedTime = midnight

, tacticScript = TacticScript "" }

mapProofStatus :: (a -> b) -> ProofStatus a -> ProofStatus b

mapProofStatus f st = st {proofTree = f $ proofTree st}

isProvedStat :: ProofStatus proof_tree -> Bool

isProvedStat = isProvedGStat . goalStatus

isProvedGStat :: GoalStatus -> Bool

isProvedGStat gs = case gs of

Proved _ -> True

_ -> False

-- | different kinds of prover interfaces

data ProverKind = ProveGUI | ProveCMDLautomatic

-- | determine if a prover kind is implemented

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

hasProverKind pk pt = case pk of

ProveGUI -> isJust $ proveGUI pt

ProveCMDLautomatic -> isJust $ proveCMDLautomatic pt

data FreeDefMorphism sentence morphism = FreeDefMorphism

{ freeDefMorphism :: morphism

, pathFromFreeDef :: morphism

, freeTheory :: [AS_Anno.Named sentence]

, isCofree :: Bool }

deriving (Eq, Show)

-- | prover or consistency checker

data ProverTemplate theory sentence morphism sublogics proof_tree = Prover

{ proverName :: String,

proverSublogic :: sublogics,

proveGUI :: Maybe (String -> theory -> [FreeDefMorphism sentence morphism]

-> IO ([ProofStatus proof_tree])),

-- input: imported theories, theory name, theory (incl. goals)

-- output: proof status for goals and lemmas

proveCMDLautomatic :: Maybe (String -> TacticScript

-> theory -> [FreeDefMorphism sentence morphism]

->IO (Result ([ProofStatus proof_tree]))),

-- input: theory name, TacticScript,

-- theory (incl. goals, but only the first one is tried)

-- output: proof status for goals and lemmas

proveCMDLautomaticBatch ::

Maybe (Bool -- 1.

-> Bool -- 2.

-> Concurrent.MVar (Result [ProofStatus proof_tree]) -- 3.

-> String -- 4.

-> TacticScript -- 5.

-> theory -- 6.

-> [FreeDefMorphism sentence morphism]

-> IO (Concurrent.ThreadId, Concurrent.MVar ())) -- output

-- input: 1. True means include proven theorems in subsequent

-- proof attempts;

-- 2. True means save problem file for each goal;

-- 3. MVar reference to a Result [] or empty MVar,

-- used to store the result of each attempt in the batch run;

-- 4. theory name;

-- 5. default TacticScript;

-- 6. theory (incl. goals and

-- Open SenStatus for individual tactic_scripts)

-- output: fst --> identifier of the batch thread for killing it,

-- after each proof attempt the result is stored in the

-- IOref

-- snd --> MVar to wait for the end of the thread

} deriving Typeable

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

mkProverTemplate str sl fct = Prover

{ proverName = str

, proverSublogic = sl

, proveGUI = Just fct

, proveCMDLautomatic = Nothing

, proveCMDLautomaticBatch = Nothing }

-- | theory morphisms between two theories

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

, ccSublogic :: sublogics

, ccBatch :: Bool -- True for batch checkers

, ccNeedsTimer :: Bool -- True for checkers that ignore time limits

, ccAutomatic :: String -- 1.

-> TacticScript -- 2.

-> TheoryMorphism sign sentence morphism proof_tree -- 3.

-> [FreeDefMorphism sentence morphism] -- 4.

-> IO (CCStatus proof_tree) -- output

-- input: 1. theory name

-- 2. default TacticScript

-- 3. theory morphism

-- 5. ingoing free definition morphisms

-- output: consistency result status

} deriving Typeable

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

mkConsChecker n sl f = ConsChecker

{ ccName = n

, ccSublogic = sl

, ccBatch = True

, ccNeedsTimer = True

, ccAutomatic = f }