{-# 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 }