ConsistencyCheck.hs revision a81a6e924a0a027f48823b0a09cf51ad807c2e5b
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbModule : $Header$
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbDescription : devGraph rule that calls consistency checker for specific logics
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbCopyright : (c) C. Maeder DFKI GmbH 2010
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbLicense : GPLv2 or higher, see LICENSE.txt
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbMaintainer : Christian.Maeder@dfki.de
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbStability : provisional
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbPortability : non-portable(Logic)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbdevGraph rule that calls consistency checker for specific logics
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb ( consistencyCheck
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb , SType (..)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb , ConsistencyStatus (..)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport Common.DocUtils (showDoc)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport Common.Utils (timeoutSecs)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport Data.Time.LocalTime (timeToTimeOfDay)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport Data.Time.Clock (secondsToDiffTime)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport Data.Ord (comparing)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbdata SType = CSUnchecked
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb | CSTimeout
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb | CSInconsistent
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb | CSConsistent
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb deriving (Eq, Ord)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbdata ConsistencyStatus = ConsistencyStatus { sType :: SType
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb , sMessage :: String }
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbinstance Show ConsistencyStatus where
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb show cs = case sType cs of
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb CSUnchecked -> "Unchecked"
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb _ -> sMessage cs
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbinstance Eq ConsistencyStatus where
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (==) cs1 cs2 = compare cs1 cs2 == EQ
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbinstance Ord ConsistencyStatus where
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb compare = comparing sType
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb{- TODO instead of LibEnv.. get FreeDefs as Input. create wrapper that calcs
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbFreeDefs from LibEnv, DGraph and LibName (so that the call remains the same).
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbconsistencyCheck :: Bool -> G_cons_checker -> AnyComorphism -> LibName -> LibEnv
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -> DGraph -> LNode DGNodeLab -> Int -> IO ConsistencyStatus
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbconsistencyCheck includeTheorems (G_cons_checker lid4 cc) (Comorphism cid) ln
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb le dg (n', lbl) t'' = do
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb let lidS = sourceLogic cid
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb lidT = targetLogic cid
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb thName = shows (getLibId ln) "_" ++ getDGNodeName lbl
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb t' = timeToTimeOfDay $ secondsToDiffTime $ toInteger t''
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb ts = TacticScript $ if ccNeedsTimer cc then "" else show t''
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb mTimeout = "No results within: " ++ show t'
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (G_theory lid1 (ExtSign sign _) _ axs _) <- getGlobalTheory lbl
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb let namedSens = toNamedList axs
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb sens = if includeTheorems then
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb map (\ s -> s { isAxiom = True }) namedSens
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb else namedSens
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb bTh'@(sig1, _) <- coerceBasicTheory lid1 lidS "" (sign, sens)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (sig2, sens2) <- wrapMapTheory cid bTh'
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb incl <- subsig_inclusion lidT (empty_signature lidT) sig2
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb return (sig1, TheoryMorphism
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb { tSource = emptyTheory lidT
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb , tTarget = Theory sig2 $ toThSens sens2
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb , tMorphism = incl }) of
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb Result ds Nothing ->
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb return $ ConsistencyStatus CSError $ unlines $ map diagString ds
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb Result _ (Just (sig1, mor)) -> do
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb cc' <- coerceConsChecker lid4 lidT "" cc
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb ret <- (if ccNeedsTimer cc then timeoutSecs t''
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb else ((return . Just) =<<))
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (ccAutomatic cc' thName ts mor $ getCFreeDefMorphs lidT le ln dg n')
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb return $ case ret of
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb Just ccStatus -> case ccResult ccStatus of
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb Just b -> if b then let
b45c1c292ff1fa635004ae81fa691f8cb3cdda85rbb Result ds ms = extractModel cid sig1 $ ccProofTree ccStatus
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb msgLines = map diagString ds ++ lines (show $ ccProofTree ccStatus)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb in case ms of
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb Nothing -> ConsistencyStatus CSConsistent $ unlines
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb ("consistent, but could not reconstruct a model" : msgLines)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb Just (sig3, sens3) -> let
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb thTxt = showDoc
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (G_theory lidS (mkExtSign sig3) startSigId (toThSens sens3)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb startThId) ""
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb in ConsistencyStatus CSConsistent $
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb case filterDiags 2 ds of
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb [] -> thTxt
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb _ -> unlines $ lines thTxt ++ "%[" : msgLines ++ ["]%"]
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb else ConsistencyStatus CSInconsistent $ show (ccProofTree ccStatus)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb Nothing -> if ccUsedTime ccStatus >= t' then
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb ConsistencyStatus CSTimeout mTimeout
c3e342e5b0b9fea6617ee16d2da02c3ef2108126dougm else ConsistencyStatus CSError $ show (ccProofTree ccStatus)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb Nothing -> ConsistencyStatus CSTimeout mTimeout