GtkDisprove.hs revision 1651c7f5055453e18a8c34f96c333e2aa702a34e
212032b342cab2f8798b146813d800ce522f9a66ndModule : $Header$
fd9abdda70912b99b24e3bf1a38f26fde908a74cndDescription : Gtk Module to enable disproving Theorems
fd9abdda70912b99b24e3bf1a38f26fde908a74cndCopyright : (c) Simon Ulbricht, Uni Bremen 2010
fd9abdda70912b99b24e3bf1a38f26fde908a74cndLicense : GPLv2 or higher, see LICENSE.txt
212032b342cab2f8798b146813d800ce522f9a66ndMaintainer : tekknix@informatik.uni-bremen.de
212032b342cab2f8798b146813d800ce522f9a66ndStability : provisional
212032b342cab2f8798b146813d800ce522f9a66ndPortability : portable
212032b342cab2f8798b146813d800ce522f9a66ndThis module provides a disproving module that checks consistency of inverted
d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowenmodule GUI.GtkDisprove (showDisproveGUI) where
3f08db06526d6901aa08c110b5bc7dde6bc39905ndimport GUI.GtkUtils as GtkUtils
212032b342cab2f8798b146813d800ce522f9a66ndimport qualified GUI.Glade.NodeChecker as ConsistencyChecker
f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjungimport Interfaces.GenericATPState (guiDefaultTimeLimit)
1844bb5f7939bd31f51dffaf8d8cf1c00657a681rbowenimport Comorphisms.LogicGraph (logicGraph)
212032b342cab2f8798b146813d800ce522f9a66ndimport qualified Common.OrderedMap as OMap
212032b342cab2f8798b146813d800ce522f9a66ndimport Common.LibName (LibName)
b12f74e1aaac71d21e4b9a376b31d7307a8d87d8ndimport Control.Concurrent (forkIO, killThread)
212032b342cab2f8798b146813d800ce522f9a66ndimport qualified Data.Map as Map
e4ca72aa494fed7b6948012734b9c9c098fbba07ndshowDisproveGUI :: GInfo -> LibEnv -> DGraph -> LNode DGNodeLab -> IO ()
e4ca72aa494fed7b6948012734b9c9c098fbba07ndshowDisproveGUI gi le dg (i,lbl) = case globalTheory lbl of
91f378b5a10f2d83820902ed10ba7967a3920c18nilgun Nothing -> error "GtkDisprove.showDisproveGUI"
9335f6d807d76d60e54af4ededdebebddb3e3d13noodl Just gt@(G_theory lid1 (ExtSign sign symb) _ sens _) -> let
e4ca72aa494fed7b6948012734b9c9c098fbba07nd fgoal g = let th = negate_th gt g
e4ca72aa494fed7b6948012734b9c9c098fbba07nd n' = (i, lbl { dgn_theory = th })
e4ca72aa494fed7b6948012734b9c9c098fbba07nd in FNode { name = g, node = n', sublogic = sublogicOfTh th,
e4ca72aa494fed7b6948012734b9c9c098fbba07nd cStatus = ConsistencyStatus CSUnchecked "" }
e4ca72aa494fed7b6948012734b9c9c098fbba07nd fgoals = map fgoal $ OMap.keys $ OMap.filter (not . isAxiom) sens
99ca75ffd7b9d0e6573ba8858c6e59d4a6d2fa15nd showDisproveWindow gi le dg gt fgoals
99ca75ffd7b9d0e6573ba8858c6e59d4a6d2fa15ndnegate_th :: G_theory -> String -> G_theory
e4ca72aa494fed7b6948012734b9c9c098fbba07ndnegate_th g_th goal = case g_th of
e4ca72aa494fed7b6948012734b9c9c098fbba07nd G_theory lid1 (ExtSign sign symb) i1 sens i2 ->
e4ca72aa494fed7b6948012734b9c9c098fbba07nd let axs = OMap.filter isAxiom sens
e4ca72aa494fed7b6948012734b9c9c098fbba07nd negSen = case OMap.lookup goal sens of
e4ca72aa494fed7b6948012734b9c9c098fbba07nd Nothing -> error "GtkDisprove.disproveThmSingle(1)"
e4ca72aa494fed7b6948012734b9c9c098fbba07nd Just sen ->
a29610af88e278144045bfa1bc63b4a1a4b5ff14trawick case negation lid1 $ sentence sen of
e4ca72aa494fed7b6948012734b9c9c098fbba07nd Nothing -> error "GtkDisprove.disproveThmSingle(2)"
e4ca72aa494fed7b6948012734b9c9c098fbba07nd Just sen' -> sen { sentence = sen', isAxiom = True }
91f378b5a10f2d83820902ed10ba7967a3920c18nilgun sens' = OMap.insert goal negSen axs
9335f6d807d76d60e54af4ededdebebddb3e3d13noodl in G_theory lid1 (ExtSign sign symb) i1 sens' i2
99ca75ffd7b9d0e6573ba8858c6e59d4a6d2fa15nd-- | Displays a GUI to set TimeoutLimit and select the ConsistencyChecker
e4ca72aa494fed7b6948012734b9c9c098fbba07nd-- and holds the functionality to call the ConsistencyChecker for the
99ca75ffd7b9d0e6573ba8858c6e59d4a6d2fa15nd-- (previously negated) selected Theorems.
e4ca72aa494fed7b6948012734b9c9c098fbba07ndshowDisproveWindow :: GInfo -> LibEnv -> DGraph -> G_theory -> [FNode] -> IO ()
e4ca72aa494fed7b6948012734b9c9c098fbba07ndshowDisproveWindow gi le dg g_th fgoals = postGUIAsync $ do
e4ca72aa494fed7b6948012734b9c9c098fbba07nd xml <- getGladeXML ConsistencyChecker.get
e4ca72aa494fed7b6948012734b9c9c098fbba07nd -- get objects
e4ca72aa494fed7b6948012734b9c9c098fbba07nd window <- xmlGetWidget xml castToWindow "NodeChecker"
91f378b5a10f2d83820902ed10ba7967a3920c18nilgun btnClose <- xmlGetWidget xml castToButton "btnClose"
91f378b5a10f2d83820902ed10ba7967a3920c18nilgun btnResults <- xmlGetWidget xml castToButton "btnResults"
15b1ec87bc44ffcbe4630fc8a266439bcaedd4e8mrumph -- get nodes view and buttons
99ca75ffd7b9d0e6573ba8858c6e59d4a6d2fa15nd trvNodes <- xmlGetWidget xml castToTreeView "trvNodes"
e4ca72aa494fed7b6948012734b9c9c098fbba07nd btnNodesAll <- xmlGetWidget xml castToButton "btnNodesAll"
99ca75ffd7b9d0e6573ba8858c6e59d4a6d2fa15nd btnNodesNone <- xmlGetWidget xml castToButton "btnNodesNone"
91f378b5a10f2d83820902ed10ba7967a3920c18nilgun btnNodesInvert <- xmlGetWidget xml castToButton "btnNodesInvert"
99ca75ffd7b9d0e6573ba8858c6e59d4a6d2fa15nd btnNodesUnchecked <- xmlGetWidget xml castToButton "btnNodesUnchecked"
e4ca72aa494fed7b6948012734b9c9c098fbba07nd btnNodesTimeout <- xmlGetWidget xml castToButton "btnNodesTimeout"
e4ca72aa494fed7b6948012734b9c9c098fbba07nd cbInclThms <- xmlGetWidget xml castToCheckButton "cbInclThms"
91f378b5a10f2d83820902ed10ba7967a3920c18nilgun -- get checker view and buttons
99ca75ffd7b9d0e6573ba8858c6e59d4a6d2fa15nd cbComorphism <- xmlGetWidget xml castToComboBox "cbComorphism"
e4ca72aa494fed7b6948012734b9c9c098fbba07nd lblSublogic <- xmlGetWidget xml castToLabel "lblSublogic"
8e88ea9de3027912dc4c69ebb44f32257c4bb0c4rbowen sbTimeout <- xmlGetWidget xml castToSpinButton "sbTimeout"
8e88ea9de3027912dc4c69ebb44f32257c4bb0c4rbowen btnCheck <- xmlGetWidget xml castToButton "btnCheck"
8e88ea9de3027912dc4c69ebb44f32257c4bb0c4rbowen btnStop <- xmlGetWidget xml castToButton "btnStop"
212032b342cab2f8798b146813d800ce522f9a66nd trvFinder <- xmlGetWidget xml castToTreeView "trvFinder"
212032b342cab2f8798b146813d800ce522f9a66nd windowSetTitle window "Consistency Checker"
a2a160100f0a51cb7fd738c1462a0b251215870erbowen spinButtonSetValue sbTimeout $ fromIntegral guiDefaultTimeLimit
a2a160100f0a51cb7fd738c1462a0b251215870erbowen let widgets = [ toWidget sbTimeout
a2a160100f0a51cb7fd738c1462a0b251215870erbowen , toWidget cbComorphism
a2a160100f0a51cb7fd738c1462a0b251215870erbowen , toWidget lblSublogic ]
838d5ac1582d50020a146d747b64d64548fa8c92rbowen checkWidgets = widgets ++ [ toWidget btnClose
838d5ac1582d50020a146d747b64d64548fa8c92rbowen , toWidget btnNodesAll
8e88ea9de3027912dc4c69ebb44f32257c4bb0c4rbowen , toWidget btnNodesNone
8e88ea9de3027912dc4c69ebb44f32257c4bb0c4rbowen , toWidget btnNodesInvert
8e88ea9de3027912dc4c69ebb44f32257c4bb0c4rbowen , toWidget btnNodesUnchecked
8e88ea9de3027912dc4c69ebb44f32257c4bb0c4rbowen , toWidget btnNodesTimeout
8e88ea9de3027912dc4c69ebb44f32257c4bb0c4rbowen , toWidget btnResults ]
212032b342cab2f8798b146813d800ce522f9a66nd switch b = do
212032b342cab2f8798b146813d800ce522f9a66nd widgetSetSensitive btnStop $ not b
212032b342cab2f8798b146813d800ce522f9a66nd widgetSetSensitive btnCheck b
838d5ac1582d50020a146d747b64d64548fa8c92rbowen widgetSetSensitive btnStop False
212032b342cab2f8798b146813d800ce522f9a66nd widgetSetSensitive btnCheck False
a2a160100f0a51cb7fd738c1462a0b251215870erbowen threadId <- newEmptyMVar
838d5ac1582d50020a146d747b64d64548fa8c92rbowen wait <- newEmptyMVar
838d5ac1582d50020a146d747b64d64548fa8c92rbowen mView <- newEmptyMVar
212032b342cab2f8798b146813d800ce522f9a66nd -- setup data
212032b342cab2f8798b146813d800ce522f9a66nd listNodes <- setListData trvNodes show $ sort fgoals
212032b342cab2f8798b146813d800ce522f9a66nd listFinder <- setListData trvFinder fName []
838d5ac1582d50020a146d747b64d64548fa8c92rbowen -- setup comorphism combobox
212032b342cab2f8798b146813d800ce522f9a66nd comboBoxSetModelText cbComorphism
212032b342cab2f8798b146813d800ce522f9a66nd shC <- after cbComorphism changed
212032b342cab2f8798b146813d800ce522f9a66nd $ setSelectedComorphism trvFinder listFinder cbComorphism
419d55842022e9e257941bfe226549661fb2c6c7humbedooh -- setup view selection actions
a2a160100f0a51cb7fd738c1462a0b251215870erbowen let update = do
838d5ac1582d50020a146d747b64d64548fa8c92rbowen mf <- getSelectedSingle trvFinder listFinder
838d5ac1582d50020a146d747b64d64548fa8c92rbowen updateComorphism trvFinder listFinder cbComorphism shC
838d5ac1582d50020a146d747b64d64548fa8c92rbowen widgetSetSensitive btnCheck $ isJust mf
a2a160100f0a51cb7fd738c1462a0b251215870erbowen setListSelectorSingle trvFinder update
a2a160100f0a51cb7fd738c1462a0b251215870erbowen let upd = updateNodes trvNodes listNodes
a2a160100f0a51cb7fd738c1462a0b251215870erbowen (\ b s -> do
a2a160100f0a51cb7fd738c1462a0b251215870erbowen labelSetLabel lblSublogic $ show s
99ca75ffd7b9d0e6573ba8858c6e59d4a6d2fa15nd updateFinder trvFinder listFinder b s)
91f378b5a10f2d83820902ed10ba7967a3920c18nilgun labelSetLabel lblSublogic "No sublogic"
91f378b5a10f2d83820902ed10ba7967a3920c18nilgun listStoreClear listFinder
91f378b5a10f2d83820902ed10ba7967a3920c18nilgun activate widgets False
91f378b5a10f2d83820902ed10ba7967a3920c18nilgun widgetSetSensitive btnCheck False)
99ca75ffd7b9d0e6573ba8858c6e59d4a6d2fa15nd (activate widgets True >> widgetSetSensitive btnCheck True)
212032b342cab2f8798b146813d800ce522f9a66nd shN <- setListSelectorMultiple trvNodes btnNodesAll btnNodesNone
212032b342cab2f8798b146813d800ce522f9a66nd btnNodesInvert upd
a2a160100f0a51cb7fd738c1462a0b251215870erbowen -- bindings
a2a160100f0a51cb7fd738c1462a0b251215870erbowen let selectWithAux f u = do
8e88ea9de3027912dc4c69ebb44f32257c4bb0c4rbowen signalBlock shN
8e88ea9de3027912dc4c69ebb44f32257c4bb0c4rbowen sel <- treeViewGetSelection trvNodes
8e88ea9de3027912dc4c69ebb44f32257c4bb0c4rbowen treeSelectionSelectAll sel
8e88ea9de3027912dc4c69ebb44f32257c4bb0c4rbowen rs <- treeSelectionGetSelectedRows sel
8e88ea9de3027912dc4c69ebb44f32257c4bb0c4rbowen mapM_ ( \ p@(row : []) -> do
8e88ea9de3027912dc4c69ebb44f32257c4bb0c4rbowen fn <- listStoreGetValue listNodes row
838d5ac1582d50020a146d747b64d64548fa8c92rbowen (if f fn then treeSelectionSelectPath else treeSelectionUnselectPath)
15b1ec87bc44ffcbe4630fc8a266439bcaedd4e8mrumph signalUnblock shN
212032b342cab2f8798b146813d800ce522f9a66nd selectWith f = selectWithAux $ f . cStatus
9bcfc3697a91b5215893a7d0206865b13fc72148nd onClicked btnNodesUnchecked
9bcfc3697a91b5215893a7d0206865b13fc72148nd $ selectWith (== ConsistencyStatus CSUnchecked "") upd
8e88ea9de3027912dc4c69ebb44f32257c4bb0c4rbowen onClicked btnNodesTimeout $ selectWith (== ConsistencyStatus CSTimeout "") upd
91f378b5a10f2d83820902ed10ba7967a3920c18nilgun onClicked btnResults $ showModelView mView "Models" listNodes []
8e88ea9de3027912dc4c69ebb44f32257c4bb0c4rbowen onClicked btnClose $ widgetDestroy window
212032b342cab2f8798b146813d800ce522f9a66nd onClicked btnStop $ takeMVar threadId >>= killThread >>= putMVar wait
212032b342cab2f8798b146813d800ce522f9a66nd onClicked btnCheck $ do
212032b342cab2f8798b146813d800ce522f9a66nd activate checkWidgets False
a2a160100f0a51cb7fd738c1462a0b251215870erbowen timeout <- spinButtonGetValueAsInt sbTimeout
9bcfc3697a91b5215893a7d0206865b13fc72148nd inclThms <- toggleButtonGetActive cbInclThms
a2a160100f0a51cb7fd738c1462a0b251215870erbowen (updat, pexit) <- progressBar "Checking consistency" "please wait..."
212032b342cab2f8798b146813d800ce522f9a66nd nodes' <- getSelectedMultiple trvNodes listNodes
212032b342cab2f8798b146813d800ce522f9a66nd mf <- getSelectedSingle trvFinder listFinder
212032b342cab2f8798b146813d800ce522f9a66nd f <- case mf of
212032b342cab2f8798b146813d800ce522f9a66nd Nothing -> error "Consistency checker: internal error"
212032b342cab2f8798b146813d800ce522f9a66nd Just (_, f) -> return f
212032b342cab2f8798b146813d800ce522f9a66nd switch False
212032b342cab2f8798b146813d800ce522f9a66nd tid <- forkIO $ do
a2a160100f0a51cb7fd738c1462a0b251215870erbowen --check inclThms ln le dg f timeout listNodes updat nodes'
9bcfc3697a91b5215893a7d0206865b13fc72148nd putMVar wait ()
a2a160100f0a51cb7fd738c1462a0b251215870erbowen putMVar threadId tid
8e88ea9de3027912dc4c69ebb44f32257c4bb0c4rbowen forkIO_ $ do
8e88ea9de3027912dc4c69ebb44f32257c4bb0c4rbowen takeMVar wait
a2a160100f0a51cb7fd738c1462a0b251215870erbowen postGUIAsync $ do
838d5ac1582d50020a146d747b64d64548fa8c92rbowen switch True
838d5ac1582d50020a146d747b64d64548fa8c92rbowen tryTakeMVar threadId
838d5ac1582d50020a146d747b64d64548fa8c92rbowen showModelView mView "Results of consistency check" listNodes []
838d5ac1582d50020a146d747b64d64548fa8c92rbowen signalBlock shN
838d5ac1582d50020a146d747b64d64548fa8c92rbowen sortNodes trvNodes listNodes
8c3bb4bd8e33f6712e32fe1b938733292551e293slive signalUnblock shN
838d5ac1582d50020a146d747b64d64548fa8c92rbowen activate checkWidgets True
212032b342cab2f8798b146813d800ce522f9a66nd{- onDestroy window $ do
4aa603e6448b99f9371397d439795c91a93637eand nodes' <- listStoreToList listNodes
15292da5451dea4ad10c12d35d9addc88be302c5humbedooh let changes = foldl (\ cs (FNode { node = (i, l), cStatus = s }) ->
15292da5451dea4ad10c12d35d9addc88be302c5humbedooh if (\ st -> st /= CSConsistent && st /= CSInconsistent)
15292da5451dea4ad10c12d35d9addc88be302c5humbedooh $ sType s then cs
4aa603e6448b99f9371397d439795c91a93637eand let n = (i, if sType s == CSInconsistent then
419d55842022e9e257941bfe226549661fb2c6c7humbedooh markNodeInconsistent "" l
212032b342cab2f8798b146813d800ce522f9a66nd else markNodeConsistent "" l)
9335f6d807d76d60e54af4ededdebebddb3e3d13noodl in SetNodeLab l n : cs
838d5ac1582d50020a146d747b64d64548fa8c92rbowen ) [] nodes'
8c3bb4bd8e33f6712e32fe1b938733292551e293slive dg' = changesDGH dg changes
212032b342cab2f8798b146813d800ce522f9a66nd putMVar res $ Map.insert ln (groupHistory dg (DGRule "Consistency") dg') le
c27a94ad0c1ec49cc72ccdf9796b31ab56415604nd selectWith (== ConsistencyStatus CSUnchecked "") upd
8e88ea9de3027912dc4c69ebb44f32257c4bb0c4rbowen widgetShow window
6dea816e0f19e6dc7674282f4a8aaa486d11eed3sfdisproveThmSingle :: FNode
212032b342cab2f8798b146813d800ce522f9a66nd -> Int -- ^ timeout limit
9335f6d807d76d60e54af4ededdebebddb3e3d13noodl -> ProofState lid sentence
212032b342cab2f8798b146813d800ce522f9a66nd -> IO (ProofState lid sentence)
212032b342cab2f8798b146813d800ce522f9a66nddisproveThmSingle fgoal fdr t'' state = undefined {-
212032b342cab2f8798b146813d800ce522f9a66nd let info s = infoDialog ("Disprove " ++ selGoal) s in
212032b342cab2f8798b146813d800ce522f9a66nd case globalTheory lbl of
212032b342cab2f8798b146813d800ce522f9a66nd Nothing -> info "Disprove failed: No global Theory"
212032b342cab2f8798b146813d800ce522f9a66nd Just (G_theory lid1 (ExtSign sign symb) i1 sens i2) ->
212032b342cab2f8798b146813d800ce522f9a66nd case OMap.lookup selGoal sens of
838d5ac1582d50020a146d747b64d64548fa8c92rbowen Nothing -> error "GtkDisprove.disproveThmSingle(1)"
838d5ac1582d50020a146d747b64d64548fa8c92rbowen Just sen -> case negation lid1 $ sentence sen of
838d5ac1582d50020a146d747b64d64548fa8c92rbowen Nothing -> info "Disprove failed: negation is not defined"
838d5ac1582d50020a146d747b64d64548fa8c92rbowen Just s' -> do
838d5ac1582d50020a146d747b64d64548fa8c92rbowen let negSen = sen { sentence = s', isAxiom = True }
838d5ac1582d50020a146d747b64d64548fa8c92rbowen axs = OMap.filter isAxiom sens
838d5ac1582d50020a146d747b64d64548fa8c92rbowen sens' = OMap.insert selGoal negSen axs
838d5ac1582d50020a146d747b64d64548fa8c92rbowen g_th = G_theory lid1 (ExtSign sign symb) i1 sens' i2
8c3bb4bd8e33f6712e32fe1b938733292551e293slive subL = sublogicOfTh g_th
8e88ea9de3027912dc4c69ebb44f32257c4bb0c4rbowen lcc = getConsCheckers $ findComorphismPaths logicGraph subL
8e88ea9de3027912dc4c69ebb44f32257c4bb0c4rbowen case find (\ (p, _) -> getPName p == selPr) lcc of
8e88ea9de3027912dc4c69ebb44f32257c4bb0c4rbowen info $ "failed to find Consistency Checker for the selected prover\n\n"
b12f74e1aaac71d21e4b9a376b31d7307a8d87d8nd ++ "possible ConsCheckers are:\n" ++ intercalate "\n"
8e88ea9de3027912dc4c69ebb44f32257c4bb0c4rbowen (nubOrd $ map (getPName . fst) lcc)
212032b342cab2f8798b146813d800ce522f9a66nd Just (G_cons_checker lid4 cc, Comorphism cid) -> do
838d5ac1582d50020a146d747b64d64548fa8c92rbowen let lidS = sourceLogic cid
9bcfc3697a91b5215893a7d0206865b13fc72148nd lidT = targetLogic cid
838d5ac1582d50020a146d747b64d64548fa8c92rbowen bTh' <- coerceBasicTheory lid1 lidS "" (sign, toNamedList sens')
838d5ac1582d50020a146d747b64d64548fa8c92rbowen (sig2, sens2) <- wrapMapTheory cid bTh'
212032b342cab2f8798b146813d800ce522f9a66nd incl <- subsig_inclusion lidT (empty_signature lidT) sig2
1c28b8f24d373dfe800f9d99b9eea20fd05c1376rjung return TheoryMorphism
8c3bb4bd8e33f6712e32fe1b938733292551e293slive { tSource = emptyTheory lidT
212032b342cab2f8798b146813d800ce522f9a66nd , tTarget = Theory sig2 $ toThSens sens2
838d5ac1582d50020a146d747b64d64548fa8c92rbowen , tMorphism = incl }
8c3bb4bd8e33f6712e32fe1b938733292551e293slive case maybeResult res of
8c3bb4bd8e33f6712e32fe1b938733292551e293slive info "Disprove failed: TheoryMorphism could not be constructed"
8c3bb4bd8e33f6712e32fe1b938733292551e293slive Just mor -> do
838d5ac1582d50020a146d747b64d64548fa8c92rbowen let thName = getDGNodeName lbl
9335f6d807d76d60e54af4ededdebebddb3e3d13noodl ts = TacticScript $ if ccNeedsTimer cc then "" else show t''
212032b342cab2f8798b146813d800ce522f9a66nd cc' <- coerceConsChecker lid4 lidT "" cc
212032b342cab2f8798b146813d800ce522f9a66nd ccS <- (if ccNeedsTimer cc' then timeoutSecs t'' else ((return . Just) =<<))
212032b342cab2f8798b146813d800ce522f9a66nd (ccAutomatic cc' thName ts mor [])
212032b342cab2f8798b146813d800ce522f9a66nd case ccS of
838d5ac1582d50020a146d747b64d64548fa8c92rbowen Just ccStatus -> do
838d5ac1582d50020a146d747b64d64548fa8c92rbowen info $ "the ConsistencyChecker " ++ ccName cc' ++ " has returned "
838d5ac1582d50020a146d747b64d64548fa8c92rbowen ++ "the following " ++ case ccResult ccStatus of
212032b342cab2f8798b146813d800ce522f9a66nd Nothing -> ""
a2a160100f0a51cb7fd738c1462a0b251215870erbowen Just b -> if b then "consistent" else "inconsistent"
a2a160100f0a51cb7fd738c1462a0b251215870erbowen ++ " results:\n" ++ show (ccProofTree ccStatus)
a2a160100f0a51cb7fd738c1462a0b251215870erbowen Nothing -> do
a2a160100f0a51cb7fd738c1462a0b251215870erbowen info $ "the ConsistencyChecker has not returned any results\n"
a2a160100f0a51cb7fd738c1462a0b251215870erbowen ++ "ConsistencyChecker used: " ++ ccName cc'