158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian MaederDescription : devGraph rule that calls consistency checker for specific logics
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian MaederCopyright : (c) C. Maeder DFKI GmbH 2010
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian MaederMaintainer : Christian.Maeder@dfki.de
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian MaederStability : provisional
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian MaederPortability : non-portable(Logic)
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian MaederdevGraph rule that calls consistency checker for specific logics
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder ( consistencyCheck
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder , ConsistencyStatus (..)
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht , cStatusToColor
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht , cStatusToPrefix
6a26171b5bc5b6ec3e1b02ae30dcfb6f03d7ffefSimon Ulbricht , basicProofToConStatus
7c99a6c982aaf61547de8054296c8055c8d1a13aSimon Ulbricht , getConsistencyOf
7c99a6c982aaf61547de8054296c8055c8d1a13aSimon Ulbrichtimport Static.DgUtils (ConsStatus (..))
7c99a6c982aaf61547de8054296c8055c8d1a13aSimon Ulbrichtimport Common.Consistency (Conservativity (..))
a81a6e924a0a027f48823b0a09cf51ad807c2e5bChristian Maederimport Common.Utils (timeoutSecs)
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maederimport Data.Time.LocalTime (timeToTimeOfDay)
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maederimport Data.Time.Clock (secondsToDiffTime)
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maederimport Data.Ord (comparing)
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maederdata SType = CSUnchecked
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder | CSInconsistent
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder | CSConsistent
2e272fd9da4f84258524b3cad10492b7bc54ef49Christian Maeder deriving (Eq, Ord, Show)
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maederdata ConsistencyStatus = ConsistencyStatus { sType :: SType
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder , sMessage :: String }
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maederinstance Show ConsistencyStatus where
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder show cs = case sType cs of
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder CSUnchecked -> "Unchecked"
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder _ -> sMessage cs
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maederinstance Eq ConsistencyStatus where
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder (==) cs1 cs2 = compare cs1 cs2 == EQ
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maederinstance Ord ConsistencyStatus where
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder compare = comparing sType
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon UlbrichtcStatusToColor :: ConsistencyStatus -> String
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon UlbrichtcStatusToColor s = case sType s of
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht CSUnchecked -> "black"
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht CSConsistent -> "green"
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht CSInconsistent -> "red"
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht CSTimeout -> "blue"
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht CSError -> "darkred"
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon UlbrichtcStatusToPrefix :: ConsistencyStatus -> String
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon UlbrichtcStatusToPrefix s = case sType s of
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht CSUnchecked -> "[ ] "
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht CSConsistent -> "[+] "
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht CSInconsistent -> "[-] "
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht CSTimeout -> "[t] "
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht CSError -> "[f] "
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon UlbrichtcInvert :: ConsistencyStatus -> ConsistencyStatus
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon UlbrichtcInvert cs = case sType cs of
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht CSConsistent -> ConsistencyStatus CSInconsistent (sMessage cs)
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht CSInconsistent -> ConsistencyStatus CSConsistent (sMessage cs)
6a26171b5bc5b6ec3e1b02ae30dcfb6f03d7ffefSimon Ulbricht{- converts a GTheory.BasicProof to ConsistencyStatus.
6a26171b5bc5b6ec3e1b02ae30dcfb6f03d7ffefSimon UlbrichtThe conversion is not exact, but sufficient since this function is only
6a26171b5bc5b6ec3e1b02ae30dcfb6f03d7ffefSimon Ulbrichtimplemented in GtkDisprove for proper display of goalstatus.
6a26171b5bc5b6ec3e1b02ae30dcfb6f03d7ffefSimon UlbrichtbasicProofToConStatus :: BasicProof -> ConsistencyStatus
6a26171b5bc5b6ec3e1b02ae30dcfb6f03d7ffefSimon UlbrichtbasicProofToConStatus bp = ConsistencyStatus (basicProofToSType bp) ""
6a26171b5bc5b6ec3e1b02ae30dcfb6f03d7ffefSimon UlbrichtbasicProofToSType :: BasicProof -> SType
6a26171b5bc5b6ec3e1b02ae30dcfb6f03d7ffefSimon UlbrichtbasicProofToSType bp = case bp of
6a26171b5bc5b6ec3e1b02ae30dcfb6f03d7ffefSimon Ulbricht BasicProof _ st -> case goalStatus st of
3ac14720aa7f1e0715311bd1598e7d78c37dd3c6Simon Ulbricht Disproved -> CSInconsistent
3ac14720aa7f1e0715311bd1598e7d78c37dd3c6Simon Ulbricht _ -> CSUnchecked
3ac14720aa7f1e0715311bd1598e7d78c37dd3c6Simon Ulbricht _ -> CSUnchecked
7c99a6c982aaf61547de8054296c8055c8d1a13aSimon Ulbricht-- roughly transform the nodes consStatus into ConsistencyStatus
7c99a6c982aaf61547de8054296c8055c8d1a13aSimon UlbrichtgetConsistencyOf :: DGNodeLab -> ConsistencyStatus
7c99a6c982aaf61547de8054296c8055c8d1a13aSimon UlbrichtgetConsistencyOf n = case getNodeConsStatus n of
7c99a6c982aaf61547de8054296c8055c8d1a13aSimon Ulbricht ConsStatus _ pc thmls ->
7c99a6c982aaf61547de8054296c8055c8d1a13aSimon Ulbricht let t = showDoc thmls "" in case pc of
7c99a6c982aaf61547de8054296c8055c8d1a13aSimon Ulbricht Inconsistent -> ConsistencyStatus CSInconsistent t
7c99a6c982aaf61547de8054296c8055c8d1a13aSimon Ulbricht Cons -> ConsistencyStatus CSConsistent t
7c99a6c982aaf61547de8054296c8055c8d1a13aSimon Ulbricht _ -> ConsistencyStatus CSUnchecked t
a81a6e924a0a027f48823b0a09cf51ad807c2e5bChristian Maeder{- TODO instead of LibEnv.. get FreeDefs as Input. create wrapper that calcs
a81a6e924a0a027f48823b0a09cf51ad807c2e5bChristian MaederFreeDefs from LibEnv, DGraph and LibName (so that the call remains the same).
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian MaederconsistencyCheck :: Bool -> G_cons_checker -> AnyComorphism -> LibName -> LibEnv
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder -> DGraph -> LNode DGNodeLab -> Int -> IO ConsistencyStatus
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian MaederconsistencyCheck includeTheorems (G_cons_checker lid4 cc) (Comorphism cid) ln
0976720c7cc7b105c5ca1532635a8d364c6b1df6Simon Ulbricht le dg (n', lbl) t'' = do
0976720c7cc7b105c5ca1532635a8d364c6b1df6Simon Ulbricht let lidS = sourceLogic cid
0976720c7cc7b105c5ca1532635a8d364c6b1df6Simon Ulbricht lidT = targetLogic cid
11c3a215d5cf043181e83929f1ce214df65cb587Christian Maeder thName = libToFileName ln ++ "_" ++ getDGNodeName lbl
0976720c7cc7b105c5ca1532635a8d364c6b1df6Simon Ulbricht t' = timeToTimeOfDay $ secondsToDiffTime $ toInteger t''
0976720c7cc7b105c5ca1532635a8d364c6b1df6Simon Ulbricht ts = TacticScript $ if ccNeedsTimer cc then "" else show t''
0976720c7cc7b105c5ca1532635a8d364c6b1df6Simon Ulbricht mTimeout = "No results within: " ++ show t'
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian Maeder (G_theory lid1 _ (ExtSign sign _) _ axs _) <- getGlobalTheory lbl
0976720c7cc7b105c5ca1532635a8d364c6b1df6Simon Ulbricht let namedSens = toNamedList axs
0976720c7cc7b105c5ca1532635a8d364c6b1df6Simon Ulbricht sens = if includeTheorems then
0976720c7cc7b105c5ca1532635a8d364c6b1df6Simon Ulbricht map (\ s -> s { isAxiom = True }) namedSens
0976720c7cc7b105c5ca1532635a8d364c6b1df6Simon Ulbricht else namedSens
0976720c7cc7b105c5ca1532635a8d364c6b1df6Simon Ulbricht bTh'@(sig1, _) <- coerceBasicTheory lid1 lidS "" (sign, sens)
0976720c7cc7b105c5ca1532635a8d364c6b1df6Simon Ulbricht (sig2, sens2) <- wrapMapTheory cid bTh'
0976720c7cc7b105c5ca1532635a8d364c6b1df6Simon Ulbricht incl <- subsig_inclusion lidT (empty_signature lidT) sig2
0976720c7cc7b105c5ca1532635a8d364c6b1df6Simon Ulbricht return (sig1, TheoryMorphism
0976720c7cc7b105c5ca1532635a8d364c6b1df6Simon Ulbricht { tSource = emptyTheory lidT
0976720c7cc7b105c5ca1532635a8d364c6b1df6Simon Ulbricht , tTarget = Theory sig2 $ toThSens sens2
0976720c7cc7b105c5ca1532635a8d364c6b1df6Simon Ulbricht , tMorphism = incl }) of
0976720c7cc7b105c5ca1532635a8d364c6b1df6Simon Ulbricht Result ds Nothing ->
0976720c7cc7b105c5ca1532635a8d364c6b1df6Simon Ulbricht return $ ConsistencyStatus CSError $ unlines $ map diagString ds
0976720c7cc7b105c5ca1532635a8d364c6b1df6Simon Ulbricht Result _ (Just (sig1, mor)) -> do
0976720c7cc7b105c5ca1532635a8d364c6b1df6Simon Ulbricht cc' <- coerceConsChecker lid4 lidT "" cc
dba73947b1f8befd8ffb81fbed7deb6e582f3f62Christian Maeder let gfreeDMs = getCFreeDefMorphs le ln dg n'
dba73947b1f8befd8ffb81fbed7deb6e582f3f62Christian Maeder freeDMs <- mapM (\ (GFreeDefMorphism fdlid fd) ->
dba73947b1f8befd8ffb81fbed7deb6e582f3f62Christian Maeder coerceFreeDefMorphism fdlid lidT "" fd) gfreeDMs
a81a6e924a0a027f48823b0a09cf51ad807c2e5bChristian Maeder ret <- (if ccNeedsTimer cc then timeoutSecs t''
a81a6e924a0a027f48823b0a09cf51ad807c2e5bChristian Maeder else ((return . Just) =<<))
dba73947b1f8befd8ffb81fbed7deb6e582f3f62Christian Maeder (ccAutomatic cc' thName ts mor freeDMs)
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder return $ case ret of
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder Just ccStatus -> case ccResult ccStatus of
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder Just b -> if b then let
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder Result ds ms = extractModel cid sig1 $ ccProofTree ccStatus
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder msgLines = map diagString ds ++ lines (show $ ccProofTree ccStatus)
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder in case ms of
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder Nothing -> ConsistencyStatus CSConsistent $ unlines
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder ("consistent, but could not reconstruct a model" : msgLines)
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder Just (sig3, sens3) -> let
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder thTxt = showDoc
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian Maeder (G_theory lidS Nothing (mkExtSign sig3) startSigId
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian Maeder (toThSens sens3) startThId) ""
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder in ConsistencyStatus CSConsistent $
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder case filterDiags 2 ds of
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder _ -> unlines $ lines thTxt ++ "%[" : msgLines ++ ["]%"]
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder else ConsistencyStatus CSInconsistent $ show (ccProofTree ccStatus)
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder Nothing -> if ccUsedTime ccStatus >= t' then
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder ConsistencyStatus CSTimeout mTimeout
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder else ConsistencyStatus CSError $ show (ccProofTree ccStatus)
158e6d8b5f7ebabef2d020ff045ede18fab15ff9Christian Maeder Nothing -> ConsistencyStatus CSTimeout mTimeout