{- |
Module      :  ./Proofs/ConsistencyCheck.hs
Description :  devGraph rule that calls consistency checker for specific logics
Copyright   :  (c) C. Maeder DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable(Logic)

devGraph rule that calls consistency checker for specific logics
-}

module Proofs.ConsistencyCheck
  ( consistencyCheck
  , SType (..)
  , ConsistencyStatus (..)
  , cStatusToColor
  , cStatusToPrefix
  , cInvert
  , basicProofToConStatus
  , getConsistencyOf
  ) where

import Static.GTheory
import Static.DevGraph
import Static.DgUtils (ConsStatus (..))
import Static.PrintDevGraph ()
import Static.ComputeTheory

import Proofs.AbstractState
import Proofs.FreeDefLinks

import Common.DocUtils (showDoc)
import Common.ExtSign
import Common.LibName
import Common.Result
import Common.AS_Annotation
import Common.Consistency (Conservativity (..))
import Common.Utils (timeoutSecs)

import Logic.Logic
import Logic.Prover
import Logic.Grothendieck
import Logic.Comorphism
import Logic.Coerce

import Data.Graph.Inductive.Graph
import Data.Time.LocalTime (timeToTimeOfDay)
import Data.Time.Clock (secondsToDiffTime)
import Data.Ord (comparing)

data SType = CSUnchecked
           | CSTimeout
           | CSError
           | CSInconsistent
           | CSConsistent
           deriving (SType -> SType -> Bool
(SType -> SType -> Bool) -> (SType -> SType -> Bool) -> Eq SType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SType -> SType -> Bool
$c/= :: SType -> SType -> Bool
== :: SType -> SType -> Bool
$c== :: SType -> SType -> Bool
Eq, Eq SType
Eq SType =>
(SType -> SType -> Ordering)
-> (SType -> SType -> Bool)
-> (SType -> SType -> Bool)
-> (SType -> SType -> Bool)
-> (SType -> SType -> Bool)
-> (SType -> SType -> SType)
-> (SType -> SType -> SType)
-> Ord SType
SType -> SType -> Bool
SType -> SType -> Ordering
SType -> SType -> SType
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 :: SType -> SType -> SType
$cmin :: SType -> SType -> SType
max :: SType -> SType -> SType
$cmax :: SType -> SType -> SType
>= :: SType -> SType -> Bool
$c>= :: SType -> SType -> Bool
> :: SType -> SType -> Bool
$c> :: SType -> SType -> Bool
<= :: SType -> SType -> Bool
$c<= :: SType -> SType -> Bool
< :: SType -> SType -> Bool
$c< :: SType -> SType -> Bool
compare :: SType -> SType -> Ordering
$ccompare :: SType -> SType -> Ordering
$cp1Ord :: Eq SType
Ord, Int -> SType -> ShowS
[SType] -> ShowS
SType -> String
(Int -> SType -> ShowS)
-> (SType -> String) -> ([SType] -> ShowS) -> Show SType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SType] -> ShowS
$cshowList :: [SType] -> ShowS
show :: SType -> String
$cshow :: SType -> String
showsPrec :: Int -> SType -> ShowS
$cshowsPrec :: Int -> SType -> ShowS
Show)

data ConsistencyStatus = ConsistencyStatus { ConsistencyStatus -> SType
sType :: SType
                                           , ConsistencyStatus -> String
sMessage :: String }

instance Show ConsistencyStatus where
  show :: ConsistencyStatus -> String
show cs :: ConsistencyStatus
cs = case ConsistencyStatus -> SType
sType ConsistencyStatus
cs of
    CSUnchecked -> "Unchecked"
    _ -> ConsistencyStatus -> String
sMessage ConsistencyStatus
cs

instance Eq ConsistencyStatus where
  == :: ConsistencyStatus -> ConsistencyStatus -> Bool
(==) cs1 :: ConsistencyStatus
cs1 cs2 :: ConsistencyStatus
cs2 = ConsistencyStatus -> ConsistencyStatus -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ConsistencyStatus
cs1 ConsistencyStatus
cs2 Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ

instance Ord ConsistencyStatus where
  compare :: ConsistencyStatus -> ConsistencyStatus -> Ordering
compare = (ConsistencyStatus -> SType)
-> ConsistencyStatus -> ConsistencyStatus -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing ConsistencyStatus -> SType
sType

cStatusToColor :: ConsistencyStatus -> String
cStatusToColor :: ConsistencyStatus -> String
cStatusToColor s :: ConsistencyStatus
s = case ConsistencyStatus -> SType
sType ConsistencyStatus
s of
  CSUnchecked -> "black"
  CSConsistent -> "green"
  CSInconsistent -> "red"
  CSTimeout -> "blue"
  CSError -> "darkred"

cStatusToPrefix :: ConsistencyStatus -> String
cStatusToPrefix :: ConsistencyStatus -> String
cStatusToPrefix s :: ConsistencyStatus
s = case ConsistencyStatus -> SType
sType ConsistencyStatus
s of
  CSUnchecked -> "[ ] "
  CSConsistent -> "[+] "
  CSInconsistent -> "[-] "
  CSTimeout -> "[t] "
  CSError -> "[f] "

cInvert :: ConsistencyStatus -> ConsistencyStatus
cInvert :: ConsistencyStatus -> ConsistencyStatus
cInvert cs :: ConsistencyStatus
cs = case ConsistencyStatus -> SType
sType ConsistencyStatus
cs of
  CSConsistent -> SType -> String -> ConsistencyStatus
ConsistencyStatus SType
CSInconsistent (ConsistencyStatus -> String
sMessage ConsistencyStatus
cs)
  CSInconsistent -> SType -> String -> ConsistencyStatus
ConsistencyStatus SType
CSConsistent (ConsistencyStatus -> String
sMessage ConsistencyStatus
cs)
  _ -> ConsistencyStatus
cs

{- converts a GTheory.BasicProof to ConsistencyStatus.
The conversion is not exact, but sufficient since this function is only
implemented in GtkDisprove for proper display of goalstatus.
-}
basicProofToConStatus :: BasicProof -> ConsistencyStatus
basicProofToConStatus :: BasicProof -> ConsistencyStatus
basicProofToConStatus bp :: BasicProof
bp = SType -> String -> ConsistencyStatus
ConsistencyStatus (BasicProof -> SType
basicProofToSType BasicProof
bp) ""

basicProofToSType :: BasicProof -> SType
basicProofToSType :: BasicProof -> SType
basicProofToSType bp :: BasicProof
bp = case BasicProof
bp of
  BasicProof _ st :: ProofStatus proof_tree
st -> case ProofStatus proof_tree -> GoalStatus
forall proof_tree. ProofStatus proof_tree -> GoalStatus
goalStatus ProofStatus proof_tree
st of
    Disproved -> SType
CSInconsistent
    _ -> SType
CSUnchecked
  _ -> SType
CSUnchecked

-- roughly transform the nodes consStatus into ConsistencyStatus
getConsistencyOf :: DGNodeLab -> ConsistencyStatus
getConsistencyOf :: DGNodeLab -> ConsistencyStatus
getConsistencyOf n :: DGNodeLab
n = case DGNodeLab -> ConsStatus
getNodeConsStatus DGNodeLab
n of
  ConsStatus _ pc :: Conservativity
pc thmls :: ThmLinkStatus
thmls ->
    let t :: String
t = ThmLinkStatus -> ShowS
forall a. Pretty a => a -> ShowS
showDoc ThmLinkStatus
thmls "" in case Conservativity
pc of
          Inconsistent -> SType -> String -> ConsistencyStatus
ConsistencyStatus SType
CSInconsistent String
t
          Cons -> SType -> String -> ConsistencyStatus
ConsistencyStatus SType
CSConsistent String
t
          _ -> SType -> String -> ConsistencyStatus
ConsistencyStatus SType
CSUnchecked String
t

{- TODO instead of LibEnv.. get FreeDefs as Input. create wrapper that calcs
FreeDefs from LibEnv, DGraph and LibName (so that the call remains the same).
 -}

consistencyCheck :: Bool -> G_cons_checker -> AnyComorphism -> LibName -> LibEnv
                 -> DGraph -> LNode DGNodeLab -> Int -> IO ConsistencyStatus
consistencyCheck :: Bool
-> G_cons_checker
-> AnyComorphism
-> LibName
-> LibEnv
-> DGraph
-> LNode DGNodeLab
-> Int
-> IO ConsistencyStatus
consistencyCheck includeTheorems :: Bool
includeTheorems (G_cons_checker lid4 :: lid
lid4 cc :: ConsChecker sign sentence sublogics morphism proof_tree
cc) (Comorphism cid :: cid
cid) ln :: LibName
ln
  le :: LibEnv
le dg :: DGraph
dg (n' :: Int
n', lbl :: DGNodeLab
lbl) t'' :: Int
t'' = do
  let lidS :: lid1
lidS = cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid1
sourceLogic cid
cid
      lidT :: lid2
lidT = cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid
      thName :: String
thName = LibName -> String
libToFileName LibName
ln String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ DGNodeLab -> String
getDGNodeName DGNodeLab
lbl
      t' :: TimeOfDay
t' = DiffTime -> TimeOfDay
timeToTimeOfDay (DiffTime -> TimeOfDay) -> DiffTime -> TimeOfDay
forall a b. (a -> b) -> a -> b
$ Integer -> DiffTime
secondsToDiffTime (Integer -> DiffTime) -> Integer -> DiffTime
forall a b. (a -> b) -> a -> b
$ Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
t''
      ts :: TacticScript
ts = String -> TacticScript
TacticScript (String -> TacticScript) -> String -> TacticScript
forall a b. (a -> b) -> a -> b
$ if ConsChecker sign sentence sublogics morphism proof_tree -> Bool
forall sign sentence sublogics morphism proof_tree.
ConsChecker sign sentence sublogics morphism proof_tree -> Bool
ccNeedsTimer ConsChecker sign sentence sublogics morphism proof_tree
cc then "" else Int -> String
forall a. Show a => a -> String
show Int
t''
      mTimeout :: String
mTimeout = "No results within: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TimeOfDay -> String
forall a. Show a => a -> String
show TimeOfDay
t'
  case do
        (G_theory lid1 :: lid
lid1 _ (ExtSign sign :: sign
sign _) _ axs :: ThSens sentence (AnyComorphism, BasicProof)
axs _) <- DGNodeLab -> Result G_theory
getGlobalTheory DGNodeLab
lbl
        let namedSens :: [Named sentence]
namedSens = ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
axs
            sens :: [Named sentence]
sens = if Bool
includeTheorems then
              (Named sentence -> Named sentence)
-> [Named sentence] -> [Named sentence]
forall a b. (a -> b) -> [a] -> [b]
map (\ s :: Named sentence
s -> Named sentence
s { isAxiom :: Bool
isAxiom = Bool
True }) [Named sentence]
namedSens
              else [Named sentence]
namedSens
        bTh' :: (sign1, [Named sentence1])
bTh'@(sig1 :: sign1
sig1, _) <- lid
-> lid1
-> String
-> (sign, [Named sentence])
-> Result (sign1, [Named sentence1])
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid1 lid1
lidS "" (sign
sign, [Named sentence]
sens)
        (sig2 :: sign2
sig2, sens2 :: [Named sentence2]
sens2) <- cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory cid
cid (sign1, [Named sentence1])
bTh'
        morphism2
incl <- lid2 -> sign2 -> sign2 -> Result morphism2
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Result morphism
subsig_inclusion lid2
lidT (lid2 -> sign2
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign
empty_signature lid2
lidT) sign2
sig2
        (sign1, TheoryMorphism sign2 sentence2 morphism2 proof_tree2)
-> Result
     (sign1, TheoryMorphism sign2 sentence2 morphism2 proof_tree2)
forall (m :: * -> *) a. Monad m => a -> m a
return (sign1
sig1, TheoryMorphism :: forall sign sen mor proof_tree.
Theory sign sen proof_tree
-> Theory sign sen proof_tree
-> mor
-> TheoryMorphism sign sen mor proof_tree
TheoryMorphism
          { tSource :: Theory sign2 sentence2 proof_tree2
tSource = lid2 -> Theory sign2 sentence2 proof_tree2
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol proof_tree.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> Theory sign sentence proof_tree
emptyTheory lid2
lidT
          , tTarget :: Theory sign2 sentence2 proof_tree2
tTarget = sign2
-> ThSens sentence2 (ProofStatus proof_tree2)
-> Theory sign2 sentence2 proof_tree2
forall sign sen proof_tree.
sign
-> ThSens sen (ProofStatus proof_tree)
-> Theory sign sen proof_tree
Theory sign2
sig2 (ThSens sentence2 (ProofStatus proof_tree2)
 -> Theory sign2 sentence2 proof_tree2)
-> ThSens sentence2 (ProofStatus proof_tree2)
-> Theory sign2 sentence2 proof_tree2
forall a b. (a -> b) -> a -> b
$ [Named sentence2] -> ThSens sentence2 (ProofStatus proof_tree2)
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [Named sentence2]
sens2
          , tMorphism :: morphism2
tMorphism = morphism2
incl }) of
    Result ds :: [Diagnosis]
ds Nothing ->
      ConsistencyStatus -> IO ConsistencyStatus
forall (m :: * -> *) a. Monad m => a -> m a
return (ConsistencyStatus -> IO ConsistencyStatus)
-> ConsistencyStatus -> IO ConsistencyStatus
forall a b. (a -> b) -> a -> b
$ SType -> String -> ConsistencyStatus
ConsistencyStatus SType
CSError (String -> ConsistencyStatus) -> String -> ConsistencyStatus
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Diagnosis -> String) -> [Diagnosis] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Diagnosis -> String
diagString [Diagnosis]
ds
    Result _ (Just (sig1 :: sign1
sig1, mor :: TheoryMorphism sign2 sentence2 morphism2 proof_tree2
mor)) -> do
      ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2
cc' <- lid
-> lid2
-> String
-> ConsChecker sign sentence sublogics morphism proof_tree
-> IO
     (ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2)
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> ConsChecker sign1 sentence1 sublogics1 morphism1 proof_tree1
-> m (ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2)
coerceConsChecker lid
lid4 lid2
lidT "" ConsChecker sign sentence sublogics morphism proof_tree
cc
      let gfreeDMs :: [GFreeDefMorphism]
gfreeDMs = LibEnv -> LibName -> DGraph -> Int -> [GFreeDefMorphism]
getCFreeDefMorphs LibEnv
le LibName
ln DGraph
dg Int
n'
      [FreeDefMorphism sentence2 morphism2]
freeDMs <- (GFreeDefMorphism -> IO (FreeDefMorphism sentence2 morphism2))
-> [GFreeDefMorphism] -> IO [FreeDefMorphism sentence2 morphism2]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (GFreeDefMorphism fdlid :: lid
fdlid fd :: FreeDefMorphism sentence morphism
fd) ->
                       lid
-> lid2
-> String
-> FreeDefMorphism sentence morphism
-> IO (FreeDefMorphism sentence2 morphism2)
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> FreeDefMorphism sentence1 morphism1
-> m (FreeDefMorphism sentence2 morphism2)
coerceFreeDefMorphism lid
fdlid lid2
lidT "" FreeDefMorphism sentence morphism
fd) [GFreeDefMorphism]
gfreeDMs
      Maybe (CCStatus proof_tree2)
ret <- (if ConsChecker sign sentence sublogics morphism proof_tree -> Bool
forall sign sentence sublogics morphism proof_tree.
ConsChecker sign sentence sublogics morphism proof_tree -> Bool
ccNeedsTimer ConsChecker sign sentence sublogics morphism proof_tree
cc then Int
-> IO (CCStatus proof_tree2) -> IO (Maybe (CCStatus proof_tree2))
forall a. Int -> IO a -> IO (Maybe a)
timeoutSecs Int
t''
              else ((Maybe (CCStatus proof_tree2) -> IO (Maybe (CCStatus proof_tree2))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (CCStatus proof_tree2) -> IO (Maybe (CCStatus proof_tree2)))
-> (CCStatus proof_tree2 -> Maybe (CCStatus proof_tree2))
-> CCStatus proof_tree2
-> IO (Maybe (CCStatus proof_tree2))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CCStatus proof_tree2 -> Maybe (CCStatus proof_tree2)
forall a. a -> Maybe a
Just) (CCStatus proof_tree2 -> IO (Maybe (CCStatus proof_tree2)))
-> IO (CCStatus proof_tree2) -> IO (Maybe (CCStatus proof_tree2))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<))
        (ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2
-> String
-> TacticScript
-> TheoryMorphism sign2 sentence2 morphism2 proof_tree2
-> [FreeDefMorphism sentence2 morphism2]
-> IO (CCStatus proof_tree2)
forall sign sentence sublogics morphism proof_tree.
ConsChecker sign sentence sublogics morphism proof_tree
-> String
-> TacticScript
-> TheoryMorphism sign sentence morphism proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO (CCStatus proof_tree)
ccAutomatic ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2
cc' String
thName TacticScript
ts TheoryMorphism sign2 sentence2 morphism2 proof_tree2
mor [FreeDefMorphism sentence2 morphism2]
freeDMs)
      ConsistencyStatus -> IO ConsistencyStatus
forall (m :: * -> *) a. Monad m => a -> m a
return (ConsistencyStatus -> IO ConsistencyStatus)
-> ConsistencyStatus -> IO ConsistencyStatus
forall a b. (a -> b) -> a -> b
$ case Maybe (CCStatus proof_tree2)
ret of
        Just ccStatus :: CCStatus proof_tree2
ccStatus -> case CCStatus proof_tree2 -> Maybe Bool
forall proof_tree. CCStatus proof_tree -> Maybe Bool
ccResult CCStatus proof_tree2
ccStatus of
          Just b :: Bool
b -> if Bool
b then let
            Result ds :: [Diagnosis]
ds ms :: Maybe (sign1, [Named sentence1])
ms = cid -> sign1 -> proof_tree2 -> Result (sign1, [Named sentence1])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> sign1 -> proof_tree2 -> Result (sign1, [Named sentence1])
extractModel cid
cid sign1
sig1 (proof_tree2 -> Result (sign1, [Named sentence1]))
-> proof_tree2 -> Result (sign1, [Named sentence1])
forall a b. (a -> b) -> a -> b
$ CCStatus proof_tree2 -> proof_tree2
forall proof_tree. CCStatus proof_tree -> proof_tree
ccProofTree CCStatus proof_tree2
ccStatus
            msgLines :: [String]
msgLines = (Diagnosis -> String) -> [Diagnosis] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Diagnosis -> String
diagString [Diagnosis]
ds [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ String -> [String]
lines (proof_tree2 -> String
forall a. Show a => a -> String
show (proof_tree2 -> String) -> proof_tree2 -> String
forall a b. (a -> b) -> a -> b
$ CCStatus proof_tree2 -> proof_tree2
forall proof_tree. CCStatus proof_tree -> proof_tree
ccProofTree CCStatus proof_tree2
ccStatus)
            in case Maybe (sign1, [Named sentence1])
ms of
            Nothing -> SType -> String -> ConsistencyStatus
ConsistencyStatus SType
CSConsistent (String -> ConsistencyStatus) -> String -> ConsistencyStatus
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
              ("consistent, but could not reconstruct a model" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
msgLines)
            Just (sig3 :: sign1
sig3, sens3 :: [Named sentence1]
sens3) -> let
              thTxt :: String
thTxt = G_theory -> ShowS
forall a. Pretty a => a -> ShowS
showDoc
                (lid1
-> Maybe IRI
-> ExtSign sign1 symbol1
-> SigId
-> ThSens sentence1 (AnyComorphism, BasicProof)
-> ThId
-> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid1
lidS Maybe IRI
forall a. Maybe a
Nothing (sign1 -> ExtSign sign1 symbol1
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign sign1
sig3) SigId
startSigId
                 ([Named sentence1] -> ThSens sentence1 (AnyComorphism, BasicProof)
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [Named sentence1]
sens3) ThId
startThId) ""
              in SType -> String -> ConsistencyStatus
ConsistencyStatus SType
CSConsistent (String -> ConsistencyStatus) -> String -> ConsistencyStatus
forall a b. (a -> b) -> a -> b
$
                 case Int -> [Diagnosis] -> [Diagnosis]
filterDiags 2 [Diagnosis]
ds of
                   [] -> String
thTxt
                   _ -> [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String]
lines String
thTxt [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ "%[" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
msgLines [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["]%"]
            else SType -> String -> ConsistencyStatus
ConsistencyStatus SType
CSInconsistent (String -> ConsistencyStatus) -> String -> ConsistencyStatus
forall a b. (a -> b) -> a -> b
$ proof_tree2 -> String
forall a. Show a => a -> String
show (CCStatus proof_tree2 -> proof_tree2
forall proof_tree. CCStatus proof_tree -> proof_tree
ccProofTree CCStatus proof_tree2
ccStatus)
          Nothing -> if CCStatus proof_tree2 -> TimeOfDay
forall proof_tree. CCStatus proof_tree -> TimeOfDay
ccUsedTime CCStatus proof_tree2
ccStatus TimeOfDay -> TimeOfDay -> Bool
forall a. Ord a => a -> a -> Bool
>= TimeOfDay
t' then
            SType -> String -> ConsistencyStatus
ConsistencyStatus SType
CSTimeout String
mTimeout
            else SType -> String -> ConsistencyStatus
ConsistencyStatus SType
CSError (String -> ConsistencyStatus) -> String -> ConsistencyStatus
forall a b. (a -> b) -> a -> b
$ proof_tree2 -> String
forall a. Show a => a -> String
show (CCStatus proof_tree2 -> proof_tree2
forall proof_tree. CCStatus proof_tree -> proof_tree
ccProofTree CCStatus proof_tree2
ccStatus)
        Nothing -> SType -> String -> ConsistencyStatus
ConsistencyStatus SType
CSTimeout String
mTimeout