{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Logic/Prover.hs
Description :  General datastructures for theorem prover interfaces
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)

General datastructures for theorem prover interfaces
-}

module Logic.Prover where

import Common.AS_Annotation as AS_Anno
import Common.Doc
import Common.DocUtils
import Common.Result
import Common.ProofUtils
import Common.ProverTools
import qualified Common.OrderedMap as OMap

import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.List
import Data.Maybe (isJust)
import Data.Time (TimeOfDay, midnight)
import Data.Typeable

import Control.Monad
import qualified Control.Concurrent as Concurrent

-- * pack sentences with their proofs

{- | 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'. -}
type SenStatus a tStatus = SenAttr a (ThmStatus tStatus)

thmStatus :: SenStatus a tStatus -> [tStatus]
thmStatus :: SenStatus a tStatus -> [tStatus]
thmStatus = ThmStatus tStatus -> [tStatus]
forall a. ThmStatus a -> [a]
getThmStatus (ThmStatus tStatus -> [tStatus])
-> (SenStatus a tStatus -> ThmStatus tStatus)
-> SenStatus a tStatus
-> [tStatus]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SenStatus a tStatus -> ThmStatus tStatus
forall s a. SenAttr s a -> a
senAttr

-- | the wrapped list of proof scripts or (AnyComorphism, BasicProof) pairs
data ThmStatus a = ThmStatus { ThmStatus a -> [a]
getThmStatus :: [a] }
  deriving (Int -> ThmStatus a -> ShowS
[ThmStatus a] -> ShowS
ThmStatus a -> String
(Int -> ThmStatus a -> ShowS)
-> (ThmStatus a -> String)
-> ([ThmStatus a] -> ShowS)
-> Show (ThmStatus a)
forall a. Show a => Int -> ThmStatus a -> ShowS
forall a. Show a => [ThmStatus a] -> ShowS
forall a. Show a => ThmStatus a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ThmStatus a] -> ShowS
$cshowList :: forall a. Show a => [ThmStatus a] -> ShowS
show :: ThmStatus a -> String
$cshow :: forall a. Show a => ThmStatus a -> String
showsPrec :: Int -> ThmStatus a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> ThmStatus a -> ShowS
Show, ThmStatus a -> ThmStatus a -> Bool
(ThmStatus a -> ThmStatus a -> Bool)
-> (ThmStatus a -> ThmStatus a -> Bool) -> Eq (ThmStatus a)
forall a. Eq a => ThmStatus a -> ThmStatus a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ThmStatus a -> ThmStatus a -> Bool
$c/= :: forall a. Eq a => ThmStatus a -> ThmStatus a -> Bool
== :: ThmStatus a -> ThmStatus a -> Bool
$c== :: forall a. Eq a => ThmStatus a -> ThmStatus a -> Bool
Eq, Eq (ThmStatus a)
Eq (ThmStatus a) =>
(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)
-> (ThmStatus a -> ThmStatus a -> ThmStatus a)
-> (ThmStatus a -> ThmStatus a -> ThmStatus a)
-> Ord (ThmStatus a)
ThmStatus a -> ThmStatus a -> Bool
ThmStatus a -> ThmStatus a -> Ordering
ThmStatus a -> ThmStatus a -> ThmStatus a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (ThmStatus a)
forall a. Ord a => ThmStatus a -> ThmStatus a -> Bool
forall a. Ord a => ThmStatus a -> ThmStatus a -> Ordering
forall a. Ord a => ThmStatus a -> ThmStatus a -> ThmStatus a
min :: ThmStatus a -> ThmStatus a -> ThmStatus a
$cmin :: forall a. Ord a => ThmStatus a -> ThmStatus a -> ThmStatus a
max :: ThmStatus a -> ThmStatus a -> ThmStatus a
$cmax :: forall a. Ord a => ThmStatus a -> ThmStatus a -> ThmStatus a
>= :: ThmStatus a -> ThmStatus a -> Bool
$c>= :: forall a. Ord a => ThmStatus a -> ThmStatus a -> Bool
> :: ThmStatus a -> ThmStatus a -> Bool
$c> :: forall a. Ord a => ThmStatus a -> ThmStatus a -> Bool
<= :: ThmStatus a -> ThmStatus a -> Bool
$c<= :: forall a. Ord a => ThmStatus a -> ThmStatus a -> Bool
< :: ThmStatus a -> ThmStatus a -> Bool
$c< :: forall a. Ord a => ThmStatus a -> ThmStatus a -> Bool
compare :: ThmStatus a -> ThmStatus a -> Ordering
$ccompare :: forall a. Ord a => ThmStatus a -> ThmStatus a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (ThmStatus a)
Ord, Typeable)

emptySenStatus :: SenStatus a b
emptySenStatus :: SenStatus a b
emptySenStatus = ThmStatus b -> a -> SenStatus a b
forall a s. a -> s -> SenAttr s a
makeNamed ([b] -> ThmStatus b
forall a. [a] -> ThmStatus a
ThmStatus []) (a -> SenStatus a b) -> a -> SenStatus a b
forall a b. (a -> b) -> a -> b
$ String -> a
forall a. HasCallStack => String -> a
error "emptySenStatus"

instance Pretty a => Pretty (OMap.ElemWOrd a) where
    pretty :: ElemWOrd a -> Doc
pretty = (a -> Doc) -> ElemWOrd a -> Doc
forall a. (a -> Doc) -> ElemWOrd a -> Doc
printOMapElemWOrd a -> Doc
forall a. Pretty a => a -> Doc
pretty

printOMapElemWOrd :: (a -> Doc) -> OMap.ElemWOrd a -> Doc
printOMapElemWOrd :: (a -> Doc) -> ElemWOrd a -> Doc
printOMapElemWOrd = ((a -> Doc) -> (ElemWOrd a -> a) -> ElemWOrd a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ElemWOrd a -> a
forall a. ElemWOrd a -> a
OMap.ele)

-- | the map from labels to the theorem plus status (and position)
type ThSens a b = OMap.OMap String (SenStatus a b)

noSens :: ThSens a b
noSens :: ThSens a b
noSens = ThSens a b
forall k a. Map k a
Map.empty

mapThSensValueM :: Monad m => (a -> m b) -> ThSens a c -> m (ThSens b c)
mapThSensValueM :: (a -> m b) -> ThSens a c -> m (ThSens b c)
mapThSensValueM f :: a -> m b
f = (ThSens b c
 -> (String, ElemWOrd (SenStatus a c)) -> m (ThSens b c))
-> ThSens b c
-> [(String, ElemWOrd (SenStatus a c))]
-> m (ThSens b c)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ m :: ThSens b c
m (k :: String
k, v :: ElemWOrd (SenStatus a c)
v) -> do
  let oe :: SenStatus a c
oe = ElemWOrd (SenStatus a c) -> SenStatus a c
forall a. ElemWOrd a -> a
OMap.ele ElemWOrd (SenStatus a c)
v
  b
ns <- a -> m b
f (a -> m b) -> a -> m b
forall a b. (a -> b) -> a -> b
$ SenStatus a c -> a
forall s a. SenAttr s a -> s
sentence SenStatus a c
oe
  let ne :: SenAttr b (ThmStatus c)
ne = SenStatus a c
oe { sentence :: b
sentence = b
ns }
  ThSens b c -> m (ThSens b c)
forall (m :: * -> *) a. Monad m => a -> m a
return (ThSens b c -> m (ThSens b c)) -> ThSens b c -> m (ThSens b c)
forall a b. (a -> b) -> a -> b
$ String
-> ElemWOrd (SenAttr b (ThmStatus c)) -> ThSens b c -> ThSens b c
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
k ElemWOrd (SenStatus a c)
v { ele :: SenAttr b (ThmStatus c)
OMap.ele = SenAttr b (ThmStatus c)
ne } ThSens b c
m) ThSens b c
forall k a. Map k a
Map.empty ([(String, ElemWOrd (SenStatus a c))] -> m (ThSens b c))
-> (ThSens a c -> [(String, ElemWOrd (SenStatus a c))])
-> ThSens a c
-> m (ThSens b c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThSens a c -> [(String, ElemWOrd (SenStatus a c))]
forall k a. Map k a -> [(k, a)]
Map.toList

{- | join and disambiguate

   * separate Axioms from Theorems

   * don't merge sentences with same key but different contents?
-}
joinSensAux :: (Ord a, Eq b) => ThSens a b -> ThSens a b
            -> (ThSens a b, [(String, String)])
joinSensAux :: ThSens a b -> ThSens a b -> (ThSens a b, [(String, String)])
joinSensAux s1 :: ThSens a b
s1 s2 :: ThSens a b
s2 = let
    l1 :: [(String, ElemWOrd (SenStatus a b))]
l1 = ThSens a b -> [(String, ElemWOrd (SenStatus a b))]
forall k a. Map k a -> [(k, a)]
Map.toList ThSens a b
s1
    updN :: a -> (a, b) -> (a, b)
updN n :: a
n (_, e :: b
e) = (a
n, b
e)
    m :: Int
m = if [(String, ElemWOrd (SenStatus a b))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, ElemWOrd (SenStatus a b))]
l1 then 0 else [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ ((String, ElemWOrd (SenStatus a b)) -> Int)
-> [(String, ElemWOrd (SenStatus a b))] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (ElemWOrd (SenStatus a b) -> Int
forall a. ElemWOrd a -> Int
OMap.order (ElemWOrd (SenStatus a b) -> Int)
-> ((String, ElemWOrd (SenStatus a b)) -> ElemWOrd (SenStatus a b))
-> (String, ElemWOrd (SenStatus a b))
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, ElemWOrd (SenStatus a b)) -> ElemWOrd (SenStatus a b)
forall a b. (a, b) -> b
snd) [(String, ElemWOrd (SenStatus a b))]
l1
    l2 :: [(String, ElemWOrd (SenStatus a b))]
l2 = ((String, ElemWOrd (SenStatus a b))
 -> (String, ElemWOrd (SenStatus a b)))
-> [(String, ElemWOrd (SenStatus a b))]
-> [(String, ElemWOrd (SenStatus a b))]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: String
x, e :: ElemWOrd (SenStatus a b)
e) -> (String
x, ElemWOrd (SenStatus a b)
e {order :: Int
OMap.order = Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ ElemWOrd (SenStatus a b) -> Int
forall a. ElemWOrd a -> Int
OMap.order ElemWOrd (SenStatus a b)
e }))
         ([(String, ElemWOrd (SenStatus a b))]
 -> [(String, ElemWOrd (SenStatus a b))])
-> [(String, ElemWOrd (SenStatus a b))]
-> [(String, ElemWOrd (SenStatus a b))]
forall a b. (a -> b) -> a -> b
$ ThSens a b -> [(String, ElemWOrd (SenStatus a b))]
forall k a. Map k a -> [(k, a)]
Map.toList ThSens a b
s2
    sl2 :: [(String, ElemWOrd (SenStatus a b))]
sl2 = Int
-> ((String, ElemWOrd (SenStatus a b)) -> String)
-> (String
    -> (String, ElemWOrd (SenStatus a b))
    -> (String, ElemWOrd (SenStatus a b)))
-> Set String
-> [(String, ElemWOrd (SenStatus a b))]
-> [(String, ElemWOrd (SenStatus a b))]
forall a.
Int
-> (a -> String) -> (String -> a -> a) -> Set String -> [a] -> [a]
genericDisambigSens Int
m (String, ElemWOrd (SenStatus a b)) -> String
forall a b. (a, b) -> a
fst String
-> (String, ElemWOrd (SenStatus a b))
-> (String, ElemWOrd (SenStatus a b))
forall a a b. a -> (a, b) -> (a, b)
updN (ThSens a b -> Set String
forall k a. Map k a -> Set k
Map.keysSet ThSens a b
s1) [(String, ElemWOrd (SenStatus a b))]
l2
    in ([(String, ElemWOrd (SenStatus a b))] -> ThSens a b
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(String, ElemWOrd (SenStatus a b))] -> ThSens a b)
-> [(String, ElemWOrd (SenStatus a b))] -> ThSens a b
forall a b. (a -> b) -> a -> b
$ [(String, ElemWOrd (SenStatus a b))]
l1 [(String, ElemWOrd (SenStatus a b))]
-> [(String, ElemWOrd (SenStatus a b))]
-> [(String, ElemWOrd (SenStatus a b))]
forall a. [a] -> [a] -> [a]
++ [(String, ElemWOrd (SenStatus a b))]
sl2,
         ((String, ElemWOrd (SenStatus a b))
 -> (String, ElemWOrd (SenStatus a b)) -> (String, String))
-> [(String, ElemWOrd (SenStatus a b))]
-> [(String, ElemWOrd (SenStatus a b))]
-> [(String, String)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ (n1 :: String
n1, _) (n2 :: String
n2, _) -> (String
n1, String
n2)) [(String, ElemWOrd (SenStatus a b))]
l2 [(String, ElemWOrd (SenStatus a b))]
sl2)

joinSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b -> ThSens a b
joinSens :: ThSens a b -> ThSens a b -> ThSens a b
joinSens s1 :: ThSens a b
s1 = (ThSens a b, [(String, String)]) -> ThSens a b
forall a b. (a, b) -> a
fst ((ThSens a b, [(String, String)]) -> ThSens a b)
-> (ThSens a b -> (ThSens a b, [(String, String)]))
-> ThSens a b
-> ThSens a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThSens a b -> ThSens a b -> (ThSens a b, [(String, String)])
forall a b.
(Ord a, Eq b) =>
ThSens a b -> ThSens a b -> (ThSens a b, [(String, String)])
joinSensAux ThSens a b
s1

intersectSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b -> ThSens a b
intersectSens :: ThSens a b -> ThSens a b -> ThSens a b
intersectSens s1 :: ThSens a b
s1 s2 :: ThSens a b
s2 = let
  sens1 :: [a]
sens1 = (SenAttr a (ThmStatus b) -> a) -> [SenAttr a (ThmStatus b)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map SenAttr a (ThmStatus b) -> a
forall s a. SenAttr s a -> s
sentence ([SenAttr a (ThmStatus b)] -> [a])
-> [SenAttr a (ThmStatus b)] -> [a]
forall a b. (a -> b) -> a -> b
$ ThSens a b -> [SenAttr a (ThmStatus b)]
forall k a. Ord k => OMap k a -> [a]
OMap.elems ThSens a b
s1
  sens2 :: [a]
sens2 = (SenAttr a (ThmStatus b) -> a) -> [SenAttr a (ThmStatus b)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map SenAttr a (ThmStatus b) -> a
forall s a. SenAttr s a -> s
sentence ([SenAttr a (ThmStatus b)] -> [a])
-> [SenAttr a (ThmStatus b)] -> [a]
forall a b. (a -> b) -> a -> b
$ ThSens a b -> [SenAttr a (ThmStatus b)]
forall k a. Ord k => OMap k a -> [a]
OMap.elems ThSens a b
s2
  sensI :: Set a
sensI = Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection ([a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList [a]
sens1) ([a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList [a]
sens2)
 in [Named a] -> ThSens a b
forall a b. Ord a => [Named a] -> ThSens a b
toThSens ([Named a] -> ThSens a b) -> [Named a] -> ThSens a b
forall a b. (a -> b) -> a -> b
$ (a -> Named a) -> [a] -> [Named a]
forall a b. (a -> b) -> [a] -> [b]
map (String -> a -> Named a
forall a s. a -> s -> SenAttr s a
AS_Anno.makeNamed "") ([a] -> [Named a]) -> [a] -> [Named a]
forall a b. (a -> b) -> a -> b
$ Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
sensI

reduceSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b
reduceSens :: ThSens a b -> ThSens a b
reduceSens =
    [(String, ElemWOrd (SenAttr a (ThmStatus b)))] -> ThSens a b
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
  ([(String, ElemWOrd (SenAttr a (ThmStatus b)))] -> ThSens a b)
-> (ThSens a b -> [(String, ElemWOrd (SenAttr a (ThmStatus b)))])
-> ThSens a b
-> ThSens a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(String, ElemWOrd (SenAttr a (ThmStatus b)))]
 -> (String, ElemWOrd (SenAttr a (ThmStatus b))))
-> [[(String, ElemWOrd (SenAttr a (ThmStatus b)))]]
-> [(String, ElemWOrd (SenAttr a (ThmStatus b)))]
forall a b. (a -> b) -> [a] -> [b]
map [(String, ElemWOrd (SenAttr a (ThmStatus b)))]
-> (String, ElemWOrd (SenAttr a (ThmStatus b)))
forall a. [a] -> a
head
  ([[(String, ElemWOrd (SenAttr a (ThmStatus b)))]]
 -> [(String, ElemWOrd (SenAttr a (ThmStatus b)))])
-> (ThSens a b -> [[(String, ElemWOrd (SenAttr a (ThmStatus b)))]])
-> ThSens a b
-> [(String, ElemWOrd (SenAttr a (ThmStatus b)))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, ElemWOrd (SenAttr a (ThmStatus b)))
 -> (String, ElemWOrd (SenAttr a (ThmStatus b))) -> Bool)
-> [(String, ElemWOrd (SenAttr a (ThmStatus b)))]
-> [[(String, ElemWOrd (SenAttr a (ThmStatus b)))]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (\ (_, a :: ElemWOrd (SenAttr a (ThmStatus b))
a) (_, b :: ElemWOrd (SenAttr a (ThmStatus b))
b) -> SenAttr a (ThmStatus b) -> a
forall s a. SenAttr s a -> s
sentence (ElemWOrd (SenAttr a (ThmStatus b)) -> SenAttr a (ThmStatus b)
forall a. ElemWOrd a -> a
OMap.ele ElemWOrd (SenAttr a (ThmStatus b))
a) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== SenAttr a (ThmStatus b) -> a
forall s a. SenAttr s a -> s
sentence (ElemWOrd (SenAttr a (ThmStatus b)) -> SenAttr a (ThmStatus b)
forall a. ElemWOrd a -> a
OMap.ele ElemWOrd (SenAttr a (ThmStatus b))
b))
  ([(String, ElemWOrd (SenAttr a (ThmStatus b)))]
 -> [[(String, ElemWOrd (SenAttr a (ThmStatus b)))]])
-> (ThSens a b -> [(String, ElemWOrd (SenAttr a (ThmStatus b)))])
-> ThSens a b
-> [[(String, ElemWOrd (SenAttr a (ThmStatus b)))]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, ElemWOrd (SenAttr a (ThmStatus b)))
 -> (String, ElemWOrd (SenAttr a (ThmStatus b))) -> Ordering)
-> [(String, ElemWOrd (SenAttr a (ThmStatus b)))]
-> [(String, ElemWOrd (SenAttr a (ThmStatus b)))]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (String, ElemWOrd (SenAttr a (ThmStatus b)))
-> (String, ElemWOrd (SenAttr a (ThmStatus b))) -> Ordering
forall a1 b.
Ord a1 =>
(String, ElemWOrd (SenStatus a1 b))
-> (String, ElemWOrd (SenStatus a1 b)) -> Ordering
cmpSnd
  ([(String, ElemWOrd (SenAttr a (ThmStatus b)))]
 -> [(String, ElemWOrd (SenAttr a (ThmStatus b)))])
-> (ThSens a b -> [(String, ElemWOrd (SenAttr a (ThmStatus b)))])
-> ThSens a b
-> [(String, ElemWOrd (SenAttr a (ThmStatus b)))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThSens a b -> [(String, ElemWOrd (SenAttr a (ThmStatus b)))]
forall k a. Map k a -> [(k, a)]
Map.toList

cmpSnd :: (Ord a1) => (String, OMap.ElemWOrd (SenStatus a1 b))
       -> (String, OMap.ElemWOrd (SenStatus a1 b)) -> Ordering
cmpSnd :: (String, ElemWOrd (SenStatus a1 b))
-> (String, ElemWOrd (SenStatus a1 b)) -> Ordering
cmpSnd (_, a :: ElemWOrd (SenStatus a1 b)
a) (_, b :: ElemWOrd (SenStatus a1 b)
b) = ElemWOrd (SenStatus a1 b) -> ElemWOrd (SenStatus a1 b) -> Ordering
forall a1 b.
Ord a1 =>
ElemWOrd (SenStatus a1 b) -> ElemWOrd (SenStatus a1 b) -> Ordering
cmpSenEle ElemWOrd (SenStatus a1 b)
a ElemWOrd (SenStatus a1 b)
b

cmpSenEle :: (Ord a1) => OMap.ElemWOrd (SenStatus a1 b)
          -> OMap.ElemWOrd (SenStatus a1 b) -> Ordering
cmpSenEle :: ElemWOrd (SenStatus a1 b) -> ElemWOrd (SenStatus a1 b) -> Ordering
cmpSenEle x :: ElemWOrd (SenStatus a1 b)
x y :: ElemWOrd (SenStatus a1 b)
y = case (ElemWOrd (SenStatus a1 b) -> SenStatus a1 b
forall a. ElemWOrd a -> a
OMap.ele ElemWOrd (SenStatus a1 b)
x, ElemWOrd (SenStatus a1 b) -> SenStatus a1 b
forall a. ElemWOrd a -> a
OMap.ele ElemWOrd (SenStatus a1 b)
y) of
    (d1 :: SenStatus a1 b
d1, d2 :: SenStatus a1 b
d2) -> (a1, Bool, Bool) -> (a1, Bool, Bool) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare
      (SenStatus a1 b -> a1
forall s a. SenAttr s a -> s
sentence SenStatus a1 b
d1, SenStatus a1 b -> Bool
forall s a. SenAttr s a -> Bool
isAxiom SenStatus a1 b
d2, SenStatus a1 b -> Bool
forall s a. SenAttr s a -> Bool
isDef SenStatus a1 b
d2) (SenStatus a1 b -> a1
forall s a. SenAttr s a -> s
sentence SenStatus a1 b
d2, SenStatus a1 b -> Bool
forall s a. SenAttr s a -> Bool
isAxiom SenStatus a1 b
d1, SenStatus a1 b -> Bool
forall s a. SenAttr s a -> Bool
isDef SenStatus a1 b
d1)

mapValue :: (a -> b) -> SenStatus a c -> SenStatus b c
mapValue :: (a -> b) -> SenStatus a c -> SenStatus b c
mapValue f :: a -> b
f d :: SenStatus a c
d = SenStatus a c
d { sentence :: b
sentence = a -> b
f (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ SenStatus a c -> a
forall s a. SenAttr s a -> s
sentence SenStatus a c
d }

{- | 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.
-}
markAsAxiom :: Ord a => Bool -> ThSens a b -> ThSens a b
markAsAxiom :: Bool -> ThSens a b -> ThSens a b
markAsAxiom b :: Bool
b = (SenAttr a (ThmStatus b) -> SenAttr a (ThmStatus b))
-> ThSens a b -> ThSens a b
forall k a b. Ord k => (a -> b) -> OMap k a -> OMap k b
OMap.map ((SenAttr a (ThmStatus b) -> SenAttr a (ThmStatus b))
 -> ThSens a b -> ThSens a b)
-> (SenAttr a (ThmStatus b) -> SenAttr a (ThmStatus b))
-> ThSens a b
-> ThSens a b
forall a b. (a -> b) -> a -> b
$ \ d :: SenAttr a (ThmStatus b)
d -> SenAttr a (ThmStatus b)
d
   { isAxiom :: Bool
isAxiom = Bool
b
   , wasTheorem :: Bool
wasTheorem = Bool
b Bool -> Bool -> Bool
&& (Bool -> Bool
not (SenAttr a (ThmStatus b) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom SenAttr a (ThmStatus b)
d) Bool -> Bool -> Bool
|| SenAttr a (ThmStatus b) -> Bool
forall s a. SenAttr s a -> Bool
wasTheorem SenAttr a (ThmStatus b)
d) }

markAsGoal :: Ord a => ThSens a b -> ThSens a b
markAsGoal :: ThSens a b -> ThSens a b
markAsGoal = Bool -> ThSens a b -> ThSens a b
forall a b. Ord a => Bool -> ThSens a b -> ThSens a b
markAsAxiom Bool
False

toNamedList :: ThSens a b -> [AS_Anno.Named a]
toNamedList :: ThSens a b -> [Named a]
toNamedList = ((String, SenStatus a b) -> Named a)
-> [(String, SenStatus a b)] -> [Named a]
forall a b. (a -> b) -> [a] -> [b]
map ((String -> SenStatus a b -> Named a)
-> (String, SenStatus a b) -> Named a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry String -> SenStatus a b -> Named a
forall a b. String -> SenStatus a b -> Named a
toNamed) ([(String, SenStatus a b)] -> [Named a])
-> (ThSens a b -> [(String, SenStatus a b)])
-> ThSens a b
-> [Named a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThSens a b -> [(String, SenStatus a b)]
forall k a. Ord k => OMap k a -> [(k, a)]
OMap.toList

toNamed :: String -> SenStatus a b -> AS_Anno.Named a
toNamed :: String -> SenStatus a b -> Named a
toNamed k :: String
k s :: SenStatus a b
s = SenStatus a b
s { senAttr :: String
AS_Anno.senAttr = String
k }

-- | putting Sentences from a list into a map
toThSens :: Ord a => [AS_Anno.Named a] -> ThSens a b
toThSens :: [Named a] -> ThSens a b
toThSens = [(String, SenAttr a (ThmStatus b))] -> ThSens a b
forall k a. Ord k => [(k, a)] -> OMap k a
OMap.fromList ([(String, SenAttr a (ThmStatus b))] -> ThSens a b)
-> ([Named a] -> [(String, SenAttr a (ThmStatus b))])
-> [Named a]
-> ThSens a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named a -> (String, SenAttr a (ThmStatus b)))
-> [Named a] -> [(String, SenAttr a (ThmStatus b))]
forall a b. (a -> b) -> [a] -> [b]
map
    ( \ v :: Named a
v -> (Named a -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named a
v, Named a
v { senAttr :: ThmStatus b
senAttr = [b] -> ThmStatus b
forall a. [a] -> ThmStatus a
ThmStatus [] }))
    ([Named a] -> [(String, SenAttr a (ThmStatus b))])
-> ([Named a] -> [Named a])
-> [Named a]
-> [(String, SenAttr a (ThmStatus b))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Named a] -> [Named a]
forall a. [Named a] -> [Named a]
nameAndDisambiguate

-- | theories with a signature and sentences with proof states
data Theory sign sen proof_tree =
     Theory sign (ThSens sen (ProofStatus proof_tree))
  deriving Typeable

-- e.g. the file name, or the script itself, or a configuration string
data TacticScript = TacticScript String deriving (TacticScript -> TacticScript -> Bool
(TacticScript -> TacticScript -> Bool)
-> (TacticScript -> TacticScript -> Bool) -> Eq TacticScript
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TacticScript -> TacticScript -> Bool
$c/= :: TacticScript -> TacticScript -> Bool
== :: TacticScript -> TacticScript -> Bool
$c== :: TacticScript -> TacticScript -> Bool
Eq, Eq TacticScript
Eq TacticScript =>
(TacticScript -> TacticScript -> Ordering)
-> (TacticScript -> TacticScript -> Bool)
-> (TacticScript -> TacticScript -> Bool)
-> (TacticScript -> TacticScript -> Bool)
-> (TacticScript -> TacticScript -> Bool)
-> (TacticScript -> TacticScript -> TacticScript)
-> (TacticScript -> TacticScript -> TacticScript)
-> Ord TacticScript
TacticScript -> TacticScript -> Bool
TacticScript -> TacticScript -> Ordering
TacticScript -> TacticScript -> TacticScript
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TacticScript -> TacticScript -> TacticScript
$cmin :: TacticScript -> TacticScript -> TacticScript
max :: TacticScript -> TacticScript -> TacticScript
$cmax :: TacticScript -> TacticScript -> TacticScript
>= :: TacticScript -> TacticScript -> Bool
$c>= :: TacticScript -> TacticScript -> Bool
> :: TacticScript -> TacticScript -> Bool
$c> :: TacticScript -> TacticScript -> Bool
<= :: TacticScript -> TacticScript -> Bool
$c<= :: TacticScript -> TacticScript -> Bool
< :: TacticScript -> TacticScript -> Bool
$c< :: TacticScript -> TacticScript -> Bool
compare :: TacticScript -> TacticScript -> Ordering
$ccompare :: TacticScript -> TacticScript -> Ordering
$cp1Ord :: Eq TacticScript
Ord, Int -> TacticScript -> ShowS
[TacticScript] -> ShowS
TacticScript -> String
(Int -> TacticScript -> ShowS)
-> (TacticScript -> String)
-> ([TacticScript] -> ShowS)
-> Show TacticScript
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TacticScript] -> ShowS
$cshowList :: [TacticScript] -> ShowS
show :: TacticScript -> String
$cshow :: TacticScript -> String
showsPrec :: Int -> TacticScript -> ShowS
$cshowsPrec :: Int -> TacticScript -> ShowS
Show, Typeable)

-- | failure reason
data Reason = Reason [String] deriving Typeable

instance Ord Reason where
  compare :: Reason -> Reason -> Ordering
compare _ _ = Ordering
EQ

instance Eq Reason where
  a :: Reason
a == :: Reason -> Reason -> Bool
== b :: Reason
b = Reason -> Reason -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Reason
a Reason
b Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ

-- | enumeration type representing the status of a goal
data GoalStatus =
    Open Reason -- ^ failure reason
  | Disproved
  | Proved Bool -- ^ True means consistent; False inconsistent
    deriving (GoalStatus -> GoalStatus -> Bool
(GoalStatus -> GoalStatus -> Bool)
-> (GoalStatus -> GoalStatus -> Bool) -> Eq GoalStatus
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GoalStatus -> GoalStatus -> Bool
$c/= :: GoalStatus -> GoalStatus -> Bool
== :: GoalStatus -> GoalStatus -> Bool
$c== :: GoalStatus -> GoalStatus -> Bool
Eq, Eq GoalStatus
Eq GoalStatus =>
(GoalStatus -> GoalStatus -> Ordering)
-> (GoalStatus -> GoalStatus -> Bool)
-> (GoalStatus -> GoalStatus -> Bool)
-> (GoalStatus -> GoalStatus -> Bool)
-> (GoalStatus -> GoalStatus -> Bool)
-> (GoalStatus -> GoalStatus -> GoalStatus)
-> (GoalStatus -> GoalStatus -> GoalStatus)
-> Ord GoalStatus
GoalStatus -> GoalStatus -> Bool
GoalStatus -> GoalStatus -> Ordering
GoalStatus -> GoalStatus -> GoalStatus
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: GoalStatus -> GoalStatus -> GoalStatus
$cmin :: GoalStatus -> GoalStatus -> GoalStatus
max :: GoalStatus -> GoalStatus -> GoalStatus
$cmax :: GoalStatus -> GoalStatus -> GoalStatus
>= :: GoalStatus -> GoalStatus -> Bool
$c>= :: GoalStatus -> GoalStatus -> Bool
> :: GoalStatus -> GoalStatus -> Bool
$c> :: GoalStatus -> GoalStatus -> Bool
<= :: GoalStatus -> GoalStatus -> Bool
$c<= :: GoalStatus -> GoalStatus -> Bool
< :: GoalStatus -> GoalStatus -> Bool
$c< :: GoalStatus -> GoalStatus -> Bool
compare :: GoalStatus -> GoalStatus -> Ordering
$ccompare :: GoalStatus -> GoalStatus -> Ordering
$cp1Ord :: Eq GoalStatus
Ord, Typeable)

instance Show GoalStatus where
    show :: GoalStatus -> String
show gs :: GoalStatus
gs = case GoalStatus
gs of
        Open (Reason l :: [String]
l) -> [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ "Open" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
l
        Disproved -> "Disproved"
        Proved c :: Bool
c -> "Proved" String -> ShowS
forall a. [a] -> [a] -> [a]
++ if Bool
c then "" else "(inconsistent)"

isOpenGoal :: GoalStatus -> Bool
isOpenGoal :: GoalStatus -> Bool
isOpenGoal gs :: GoalStatus
gs = case GoalStatus
gs of
  Open _ -> Bool
True
  _ -> Bool
False

openGoalStatus :: GoalStatus
openGoalStatus :: GoalStatus
openGoalStatus = Reason -> GoalStatus
Open (Reason -> GoalStatus) -> Reason -> GoalStatus
forall a b. (a -> b) -> a -> b
$ [String] -> Reason
Reason []

-- | data type representing the proof status for a goal
data ProofStatus proof_tree = ProofStatus
    { ProofStatus proof_tree -> String
goalName :: String
    , ProofStatus proof_tree -> GoalStatus
goalStatus :: GoalStatus
    , ProofStatus proof_tree -> [String]
usedAxioms :: [String] -- ^ used axioms
    , ProofStatus proof_tree -> String
usedProver :: String -- ^ name of prover
    , ProofStatus proof_tree -> proof_tree
proofTree :: proof_tree
    , ProofStatus proof_tree -> TimeOfDay
usedTime :: TimeOfDay
    , ProofStatus proof_tree -> TacticScript
tacticScript :: TacticScript
    , ProofStatus proof_tree -> [String]
proofLines :: [String] }
    deriving (Int -> ProofStatus proof_tree -> ShowS
[ProofStatus proof_tree] -> ShowS
ProofStatus proof_tree -> String
(Int -> ProofStatus proof_tree -> ShowS)
-> (ProofStatus proof_tree -> String)
-> ([ProofStatus proof_tree] -> ShowS)
-> Show (ProofStatus proof_tree)
forall proof_tree.
Show proof_tree =>
Int -> ProofStatus proof_tree -> ShowS
forall proof_tree.
Show proof_tree =>
[ProofStatus proof_tree] -> ShowS
forall proof_tree.
Show proof_tree =>
ProofStatus proof_tree -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProofStatus proof_tree] -> ShowS
$cshowList :: forall proof_tree.
Show proof_tree =>
[ProofStatus proof_tree] -> ShowS
show :: ProofStatus proof_tree -> String
$cshow :: forall proof_tree.
Show proof_tree =>
ProofStatus proof_tree -> String
showsPrec :: Int -> ProofStatus proof_tree -> ShowS
$cshowsPrec :: forall proof_tree.
Show proof_tree =>
Int -> ProofStatus proof_tree -> ShowS
Show, ProofStatus proof_tree -> ProofStatus proof_tree -> Bool
(ProofStatus proof_tree -> ProofStatus proof_tree -> Bool)
-> (ProofStatus proof_tree -> ProofStatus proof_tree -> Bool)
-> Eq (ProofStatus proof_tree)
forall proof_tree.
Eq proof_tree =>
ProofStatus proof_tree -> ProofStatus proof_tree -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool
$c/= :: forall proof_tree.
Eq proof_tree =>
ProofStatus proof_tree -> ProofStatus proof_tree -> Bool
== :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool
$c== :: forall proof_tree.
Eq proof_tree =>
ProofStatus proof_tree -> ProofStatus proof_tree -> Bool
Eq, Eq (ProofStatus proof_tree)
Eq (ProofStatus proof_tree) =>
(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)
-> (ProofStatus proof_tree
    -> ProofStatus proof_tree -> ProofStatus proof_tree)
-> (ProofStatus proof_tree
    -> ProofStatus proof_tree -> ProofStatus proof_tree)
-> Ord (ProofStatus proof_tree)
ProofStatus proof_tree -> ProofStatus proof_tree -> Bool
ProofStatus proof_tree -> ProofStatus proof_tree -> Ordering
ProofStatus proof_tree
-> ProofStatus proof_tree -> ProofStatus proof_tree
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall proof_tree. Ord proof_tree => Eq (ProofStatus proof_tree)
forall proof_tree.
Ord proof_tree =>
ProofStatus proof_tree -> ProofStatus proof_tree -> Bool
forall proof_tree.
Ord proof_tree =>
ProofStatus proof_tree -> ProofStatus proof_tree -> Ordering
forall proof_tree.
Ord proof_tree =>
ProofStatus proof_tree
-> ProofStatus proof_tree -> ProofStatus proof_tree
min :: ProofStatus proof_tree
-> ProofStatus proof_tree -> ProofStatus proof_tree
$cmin :: forall proof_tree.
Ord proof_tree =>
ProofStatus proof_tree
-> ProofStatus proof_tree -> ProofStatus proof_tree
max :: ProofStatus proof_tree
-> ProofStatus proof_tree -> ProofStatus proof_tree
$cmax :: forall proof_tree.
Ord proof_tree =>
ProofStatus proof_tree
-> ProofStatus proof_tree -> ProofStatus proof_tree
>= :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool
$c>= :: forall proof_tree.
Ord proof_tree =>
ProofStatus proof_tree -> ProofStatus proof_tree -> Bool
> :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool
$c> :: forall proof_tree.
Ord proof_tree =>
ProofStatus proof_tree -> ProofStatus proof_tree -> Bool
<= :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool
$c<= :: forall proof_tree.
Ord proof_tree =>
ProofStatus proof_tree -> ProofStatus proof_tree -> Bool
< :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool
$c< :: forall proof_tree.
Ord proof_tree =>
ProofStatus proof_tree -> ProofStatus proof_tree -> Bool
compare :: ProofStatus proof_tree -> ProofStatus proof_tree -> Ordering
$ccompare :: forall proof_tree.
Ord proof_tree =>
ProofStatus proof_tree -> ProofStatus proof_tree -> Ordering
$cp1Ord :: forall proof_tree. Ord proof_tree => Eq (ProofStatus proof_tree)
Ord, Typeable)

{- | 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 :: String -> String -> pt -> ProofStatus pt
openProofStatus goalname :: String
goalname provername :: String
provername proof_tree :: pt
proof_tree = ProofStatus :: forall proof_tree.
String
-> GoalStatus
-> [String]
-> String
-> proof_tree
-> TimeOfDay
-> TacticScript
-> [String]
-> ProofStatus proof_tree
ProofStatus
   { goalName :: String
goalName = String
goalname
   , goalStatus :: GoalStatus
goalStatus = GoalStatus
openGoalStatus
   , usedAxioms :: [String]
usedAxioms = []
   , usedProver :: String
usedProver = String
provername
   , proofTree :: pt
proofTree = pt
proof_tree
   , usedTime :: TimeOfDay
usedTime = TimeOfDay
midnight
   , tacticScript :: TacticScript
tacticScript = String -> TacticScript
TacticScript ""
   , proofLines :: [String]
proofLines = [] }

isProvedStat :: ProofStatus proof_tree -> Bool
isProvedStat :: ProofStatus proof_tree -> Bool
isProvedStat = GoalStatus -> Bool
isProvedGStat (GoalStatus -> Bool)
-> (ProofStatus proof_tree -> GoalStatus)
-> ProofStatus proof_tree
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofStatus proof_tree -> GoalStatus
forall proof_tree. ProofStatus proof_tree -> GoalStatus
goalStatus

isProvedGStat :: GoalStatus -> Bool
isProvedGStat :: GoalStatus -> Bool
isProvedGStat gs :: GoalStatus
gs = case GoalStatus
gs of
    Proved _ -> Bool
True
    _ -> Bool
False

-- | different kinds of prover interfaces
data ProverKind = ProveGUI | ProveCMDLautomatic deriving Typeable

-- | determine if a prover kind is implemented
hasProverKind :: ProverKind -> ProverTemplate x s m y z -> Bool
hasProverKind :: ProverKind -> ProverTemplate x s m y z -> Bool
hasProverKind pk :: ProverKind
pk pt :: ProverTemplate x s m y z
pt = case ProverKind
pk of
    ProveGUI -> Maybe
  (String
   -> x
   -> [FreeDefMorphism s m]
   -> IO ([ProofStatus z], [(Named s, ProofStatus z)]))
-> Bool
forall a. Maybe a -> Bool
isJust (Maybe
   (String
    -> x
    -> [FreeDefMorphism s m]
    -> IO ([ProofStatus z], [(Named s, ProofStatus z)]))
 -> Bool)
-> Maybe
     (String
      -> x
      -> [FreeDefMorphism s m]
      -> IO ([ProofStatus z], [(Named s, ProofStatus z)]))
-> Bool
forall a b. (a -> b) -> a -> b
$ ProverTemplate x s m y z
-> Maybe
     (String
      -> x
      -> [FreeDefMorphism s m]
      -> IO ([ProofStatus z], [(Named s, ProofStatus z)]))
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> Maybe
     (String
      -> theory
      -> [FreeDefMorphism sentence morphism]
      -> IO
           ([ProofStatus proof_tree],
            [(Named sentence, ProofStatus proof_tree)]))
proveGUI ProverTemplate x s m y z
pt
    ProveCMDLautomatic -> Maybe
  (Bool
   -> Bool
   -> MVar (Result [ProofStatus z])
   -> String
   -> TacticScript
   -> x
   -> [FreeDefMorphism s m]
   -> IO (ThreadId, MVar ()))
-> Bool
forall a. Maybe a -> Bool
isJust (Maybe
   (Bool
    -> Bool
    -> MVar (Result [ProofStatus z])
    -> String
    -> TacticScript
    -> x
    -> [FreeDefMorphism s m]
    -> IO (ThreadId, MVar ()))
 -> Bool)
-> Maybe
     (Bool
      -> Bool
      -> MVar (Result [ProofStatus z])
      -> String
      -> TacticScript
      -> x
      -> [FreeDefMorphism s m]
      -> IO (ThreadId, MVar ()))
-> Bool
forall a b. (a -> b) -> a -> b
$ ProverTemplate x s m y z
-> Maybe
     (Bool
      -> Bool
      -> MVar (Result [ProofStatus z])
      -> String
      -> TacticScript
      -> x
      -> [FreeDefMorphism s m]
      -> IO (ThreadId, MVar ()))
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> Maybe
     (Bool
      -> Bool
      -> MVar (Result [ProofStatus proof_tree])
      -> String
      -> TacticScript
      -> theory
      -> [FreeDefMorphism sentence morphism]
      -> IO (ThreadId, MVar ()))
proveCMDLautomaticBatch ProverTemplate x s m y z
pt

data FreeDefMorphism sentence morphism = FreeDefMorphism
  { FreeDefMorphism sentence morphism -> morphism
freeDefMorphism :: morphism
  , FreeDefMorphism sentence morphism -> morphism
pathFromFreeDef :: morphism
  , FreeDefMorphism sentence morphism -> [Named sentence]
freeTheory :: [AS_Anno.Named sentence]
  , FreeDefMorphism sentence morphism -> Bool
isCofree :: Bool }
  deriving (Int -> FreeDefMorphism sentence morphism -> ShowS
[FreeDefMorphism sentence morphism] -> ShowS
FreeDefMorphism sentence morphism -> String
(Int -> FreeDefMorphism sentence morphism -> ShowS)
-> (FreeDefMorphism sentence morphism -> String)
-> ([FreeDefMorphism sentence morphism] -> ShowS)
-> Show (FreeDefMorphism sentence morphism)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall sentence morphism.
(Show morphism, Show sentence) =>
Int -> FreeDefMorphism sentence morphism -> ShowS
forall sentence morphism.
(Show morphism, Show sentence) =>
[FreeDefMorphism sentence morphism] -> ShowS
forall sentence morphism.
(Show morphism, Show sentence) =>
FreeDefMorphism sentence morphism -> String
showList :: [FreeDefMorphism sentence morphism] -> ShowS
$cshowList :: forall sentence morphism.
(Show morphism, Show sentence) =>
[FreeDefMorphism sentence morphism] -> ShowS
show :: FreeDefMorphism sentence morphism -> String
$cshow :: forall sentence morphism.
(Show morphism, Show sentence) =>
FreeDefMorphism sentence morphism -> String
showsPrec :: Int -> FreeDefMorphism sentence morphism -> ShowS
$cshowsPrec :: forall sentence morphism.
(Show morphism, Show sentence) =>
Int -> FreeDefMorphism sentence morphism -> ShowS
Show, FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism -> Bool
(FreeDefMorphism sentence morphism
 -> FreeDefMorphism sentence morphism -> Bool)
-> (FreeDefMorphism sentence morphism
    -> FreeDefMorphism sentence morphism -> Bool)
-> Eq (FreeDefMorphism sentence morphism)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall sentence morphism.
(Eq morphism, Eq sentence) =>
FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism -> Bool
/= :: FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism -> Bool
$c/= :: forall sentence morphism.
(Eq morphism, Eq sentence) =>
FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism -> Bool
== :: FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism -> Bool
$c== :: forall sentence morphism.
(Eq morphism, Eq sentence) =>
FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism -> Bool
Eq, Eq (FreeDefMorphism sentence morphism)
Eq (FreeDefMorphism sentence morphism) =>
(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)
-> (FreeDefMorphism sentence morphism
    -> FreeDefMorphism sentence morphism
    -> FreeDefMorphism sentence morphism)
-> (FreeDefMorphism sentence morphism
    -> FreeDefMorphism sentence morphism
    -> FreeDefMorphism sentence morphism)
-> Ord (FreeDefMorphism sentence morphism)
FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism -> Bool
FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism -> Ordering
FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall sentence morphism.
(Ord morphism, Ord sentence) =>
Eq (FreeDefMorphism sentence morphism)
forall sentence morphism.
(Ord morphism, Ord sentence) =>
FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism -> Bool
forall sentence morphism.
(Ord morphism, Ord sentence) =>
FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism -> Ordering
forall sentence morphism.
(Ord morphism, Ord sentence) =>
FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism
min :: FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism
$cmin :: forall sentence morphism.
(Ord morphism, Ord sentence) =>
FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism
max :: FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism
$cmax :: forall sentence morphism.
(Ord morphism, Ord sentence) =>
FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism
>= :: FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism -> Bool
$c>= :: forall sentence morphism.
(Ord morphism, Ord sentence) =>
FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism -> Bool
> :: FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism -> Bool
$c> :: forall sentence morphism.
(Ord morphism, Ord sentence) =>
FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism -> Bool
<= :: FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism -> Bool
$c<= :: forall sentence morphism.
(Ord morphism, Ord sentence) =>
FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism -> Bool
< :: FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism -> Bool
$c< :: forall sentence morphism.
(Ord morphism, Ord sentence) =>
FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism -> Bool
compare :: FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism -> Ordering
$ccompare :: forall sentence morphism.
(Ord morphism, Ord sentence) =>
FreeDefMorphism sentence morphism
-> FreeDefMorphism sentence morphism -> Ordering
$cp1Ord :: forall sentence morphism.
(Ord morphism, Ord sentence) =>
Eq (FreeDefMorphism sentence morphism)
Ord, Typeable)

-- | prover or consistency checker
data ProverTemplate theory sentence morphism sublogics proof_tree = Prover
    { ProverTemplate theory sentence morphism sublogics proof_tree
-> String
proverName :: String,
      ProverTemplate theory sentence morphism sublogics proof_tree
-> IO (Maybe String)
proverUsable :: IO (Maybe String),
      -- are required binaries or jars installed, Nothing if yes
      ProverTemplate theory sentence morphism sublogics proof_tree
-> sublogics
proverSublogic :: sublogics,
      ProverTemplate theory sentence morphism sublogics proof_tree
-> Maybe
     (String
      -> theory
      -> [FreeDefMorphism sentence morphism]
      -> IO
           ([ProofStatus proof_tree],
            [(Named sentence, ProofStatus proof_tree)]))
proveGUI :: Maybe (String -> theory -> [FreeDefMorphism sentence morphism]
                         -> IO ( [ProofStatus proof_tree]
                               , [(Named sentence, ProofStatus proof_tree)])),
      {- input: imported theories, theory name, theory (incl. goals)
         output:
         fst --> proof status for goals and lemmas
         snd --> new lemmas (with proofs) -}
      ProverTemplate theory sentence morphism sublogics proof_tree
-> Maybe
     (Bool
      -> Bool
      -> MVar (Result [ProofStatus proof_tree])
      -> String
      -> TacticScript
      -> theory
      -> [FreeDefMorphism sentence morphism]
      -> IO (ThreadId, MVar ()))
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)
         7. ingoing free def morphisms
         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 :: String
-> sublogics
-> (String
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO [ProofStatus proof_tree])
-> ProverTemplate theory sentence morphism sublogics proof_tree
mkProverTemplate str :: String
str sl :: sublogics
sl fct :: String
-> theory
-> [FreeDefMorphism sentence morphism]
-> IO [ProofStatus proof_tree]
fct = Prover :: forall theory sentence morphism sublogics proof_tree.
String
-> IO (Maybe String)
-> sublogics
-> Maybe
     (String
      -> theory
      -> [FreeDefMorphism sentence morphism]
      -> IO
           ([ProofStatus proof_tree],
            [(Named sentence, ProofStatus proof_tree)]))
-> Maybe
     (Bool
      -> Bool
      -> MVar (Result [ProofStatus proof_tree])
      -> String
      -> TacticScript
      -> theory
      -> [FreeDefMorphism sentence morphism]
      -> IO (ThreadId, MVar ()))
-> ProverTemplate theory sentence morphism sublogics proof_tree
Prover
    { proverName :: String
proverName = String
str
    , proverUsable :: IO (Maybe String)
proverUsable = Maybe String -> IO (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe String
forall a. Maybe a
Nothing
    , proverSublogic :: sublogics
proverSublogic = sublogics
sl
    , proveGUI :: Maybe
  (String
   -> theory
   -> [FreeDefMorphism sentence morphism]
   -> IO
        ([ProofStatus proof_tree],
         [(Named sentence, ProofStatus proof_tree)]))
proveGUI = (String
 -> theory
 -> [FreeDefMorphism sentence morphism]
 -> IO
      ([ProofStatus proof_tree],
       [(Named sentence, ProofStatus proof_tree)]))
-> Maybe
     (String
      -> theory
      -> [FreeDefMorphism sentence morphism]
      -> IO
           ([ProofStatus proof_tree],
            [(Named sentence, ProofStatus proof_tree)]))
forall a. a -> Maybe a
Just ((String
  -> theory
  -> [FreeDefMorphism sentence morphism]
  -> IO
       ([ProofStatus proof_tree],
        [(Named sentence, ProofStatus proof_tree)]))
 -> Maybe
      (String
       -> theory
       -> [FreeDefMorphism sentence morphism]
       -> IO
            ([ProofStatus proof_tree],
             [(Named sentence, ProofStatus proof_tree)])))
-> (String
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO
         ([ProofStatus proof_tree],
          [(Named sentence, ProofStatus proof_tree)]))
-> Maybe
     (String
      -> theory
      -> [FreeDefMorphism sentence morphism]
      -> IO
           ([ProofStatus proof_tree],
            [(Named sentence, ProofStatus proof_tree)]))
forall a b. (a -> b) -> a -> b
$ \ s :: String
s t :: theory
t fs :: [FreeDefMorphism sentence morphism]
fs -> do
                [ProofStatus proof_tree]
ps <- String
-> theory
-> [FreeDefMorphism sentence morphism]
-> IO [ProofStatus proof_tree]
fct String
s theory
t [FreeDefMorphism sentence morphism]
fs
                ([ProofStatus proof_tree],
 [(Named sentence, ProofStatus proof_tree)])
-> IO
     ([ProofStatus proof_tree],
      [(Named sentence, ProofStatus proof_tree)])
forall (m :: * -> *) a. Monad m => a -> m a
return ([ProofStatus proof_tree]
ps, [])
    , proveCMDLautomaticBatch :: Maybe
  (Bool
   -> Bool
   -> MVar (Result [ProofStatus proof_tree])
   -> String
   -> TacticScript
   -> theory
   -> [FreeDefMorphism sentence morphism]
   -> IO (ThreadId, MVar ()))
proveCMDLautomaticBatch = Maybe
  (Bool
   -> Bool
   -> MVar (Result [ProofStatus proof_tree])
   -> String
   -> TacticScript
   -> theory
   -> [FreeDefMorphism sentence morphism]
   -> IO (ThreadId, MVar ()))
forall a. Maybe a
Nothing }

mkUsableProver :: String -> 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
mkUsableProver bin :: String
bin str :: String
str sl :: sublogics
sl fct :: String
-> theory
-> [FreeDefMorphism sentence morphism]
-> IO [ProofStatus proof_tree]
fct =
  (String
-> sublogics
-> (String
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO [ProofStatus proof_tree])
-> ProverTemplate theory sentence morphism sublogics proof_tree
forall sublogics theory sentence morphism proof_tree.
String
-> sublogics
-> (String
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO [ProofStatus proof_tree])
-> ProverTemplate theory sentence morphism sublogics proof_tree
mkProverTemplate String
str sublogics
sl String
-> theory
-> [FreeDefMorphism sentence morphism]
-> IO [ProofStatus proof_tree]
fct) { proverUsable :: IO (Maybe String)
proverUsable = String -> IO (Maybe String)
checkBinary String
bin }

mkAutomaticProver :: String -> String -> sublogics
  -> (String -> theory -> [FreeDefMorphism sentence morphism]
      -> IO [ProofStatus proof_tree])
  -> (Bool -> Bool -> Concurrent.MVar (Result [ProofStatus proof_tree])
      -> String -> TacticScript -> theory -> [FreeDefMorphism sentence morphism]
      -> IO (Concurrent.ThreadId, Concurrent.MVar ()))
  -> 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
mkAutomaticProver bin :: String
bin str :: String
str sl :: sublogics
sl fct :: String
-> theory
-> [FreeDefMorphism sentence morphism]
-> IO [ProofStatus proof_tree]
fct bFct :: Bool
-> Bool
-> MVar (Result [ProofStatus proof_tree])
-> String
-> TacticScript
-> theory
-> [FreeDefMorphism sentence morphism]
-> IO (ThreadId, MVar ())
bFct =
  (String
-> String
-> sublogics
-> (String
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO [ProofStatus proof_tree])
-> ProverTemplate theory sentence morphism sublogics proof_tree
forall sublogics theory sentence morphism proof_tree.
String
-> String
-> sublogics
-> (String
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO [ProofStatus proof_tree])
-> ProverTemplate theory sentence morphism sublogics proof_tree
mkUsableProver String
bin String
str sublogics
sl String
-> theory
-> [FreeDefMorphism sentence morphism]
-> IO [ProofStatus proof_tree]
fct)
  { proveCMDLautomaticBatch :: Maybe
  (Bool
   -> Bool
   -> MVar (Result [ProofStatus proof_tree])
   -> String
   -> TacticScript
   -> theory
   -> [FreeDefMorphism sentence morphism]
   -> IO (ThreadId, MVar ()))
proveCMDLautomaticBatch = (Bool
 -> Bool
 -> MVar (Result [ProofStatus proof_tree])
 -> String
 -> TacticScript
 -> theory
 -> [FreeDefMorphism sentence morphism]
 -> IO (ThreadId, MVar ()))
-> Maybe
     (Bool
      -> Bool
      -> MVar (Result [ProofStatus proof_tree])
      -> String
      -> TacticScript
      -> theory
      -> [FreeDefMorphism sentence morphism]
      -> IO (ThreadId, MVar ()))
forall a. a -> Maybe a
Just Bool
-> Bool
-> MVar (Result [ProofStatus proof_tree])
-> String
-> TacticScript
-> theory
-> [FreeDefMorphism sentence morphism]
-> IO (ThreadId, MVar ())
bFct }

-- | theory morphisms between two theories
data TheoryMorphism sign sen mor proof_tree = TheoryMorphism
    { TheoryMorphism sign sen mor proof_tree
-> Theory sign sen proof_tree
tSource :: Theory sign sen proof_tree
    , TheoryMorphism sign sen mor proof_tree
-> Theory sign sen proof_tree
tTarget :: Theory sign sen proof_tree
    , TheoryMorphism sign sen mor proof_tree -> mor
tMorphism :: mor }
    deriving Typeable

data CCStatus proof_tree = CCStatus
  { CCStatus proof_tree -> proof_tree
ccProofTree :: proof_tree
  , CCStatus proof_tree -> TimeOfDay
ccUsedTime :: TimeOfDay
  , CCStatus proof_tree -> Maybe Bool
ccResult :: Maybe Bool }
  deriving Typeable

data ConsChecker sign sentence sublogics morphism proof_tree = ConsChecker
  { ConsChecker sign sentence sublogics morphism proof_tree -> String
ccName :: String
  , ConsChecker sign sentence sublogics morphism proof_tree
-> IO (Maybe String)
ccUsable :: IO (Maybe String)
  , ConsChecker sign sentence sublogics morphism proof_tree
-> sublogics
ccSublogic :: sublogics
  , ConsChecker sign sentence sublogics morphism proof_tree -> Bool
ccBatch :: Bool -- True for batch checkers
  , ConsChecker sign sentence sublogics morphism proof_tree -> Bool
ccNeedsTimer :: Bool -- True for checkers that ignore time limits
  , ConsChecker sign sentence sublogics morphism proof_tree
-> String
-> TacticScript
-> TheoryMorphism sign sentence morphism proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO (CCStatus proof_tree)
ccAutomatic :: String -- 1.
                 -> TacticScript  -- 2.
                 -> TheoryMorphism sign sentence morphism proof_tree  -- 3.
                 -> [FreeDefMorphism sentence morphism]  -- 4.
                 -> IO (CCStatus proof_tree) -- output
  } deriving Typeable
{- input: 1. theory name
      2. default TacticScript
      3. theory morphism
      5. ingoing free definition morphisms
      output: consistency result status -}

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 :: 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 :: String
n sl :: sublogics
sl f :: String
-> TacticScript
-> TheoryMorphism sign sentence morphism proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO (CCStatus proof_tree)
f = ConsChecker :: forall sign sentence sublogics morphism proof_tree.
String
-> IO (Maybe String)
-> sublogics
-> Bool
-> Bool
-> (String
    -> TacticScript
    -> TheoryMorphism sign sentence morphism proof_tree
    -> [FreeDefMorphism sentence morphism]
    -> IO (CCStatus proof_tree))
-> ConsChecker sign sentence sublogics morphism proof_tree
ConsChecker
  { ccName :: String
ccName = String
n
  , ccUsable :: IO (Maybe String)
ccUsable = Maybe String -> IO (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe String
forall a. Maybe a
Nothing
  , ccSublogic :: sublogics
ccSublogic = sublogics
sl
  , ccBatch :: Bool
ccBatch = Bool
True
  , ccNeedsTimer :: Bool
ccNeedsTimer = Bool
True
  , ccAutomatic :: String
-> TacticScript
-> TheoryMorphism sign sentence morphism proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO (CCStatus proof_tree)
ccAutomatic = String
-> TacticScript
-> TheoryMorphism sign sentence morphism proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO (CCStatus proof_tree)
f }

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
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
mkUsableConsChecker bin :: String
bin n :: String
n sl :: sublogics
sl f :: String
-> TacticScript
-> TheoryMorphism sign sentence morphism proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO (CCStatus proof_tree)
f =
  (String
-> sublogics
-> (String
    -> TacticScript
    -> TheoryMorphism sign sentence morphism proof_tree
    -> [FreeDefMorphism sentence morphism]
    -> IO (CCStatus proof_tree))
-> ConsChecker sign sentence sublogics morphism proof_tree
forall sublogics sign sentence morphism proof_tree.
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 String
n sublogics
sl String
-> TacticScript
-> TheoryMorphism sign sentence morphism proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO (CCStatus proof_tree)
f) { ccUsable :: IO (Maybe String)
ccUsable = String -> IO (Maybe String)
checkBinary String
bin }