GtkDisprove.hs revision d815d2b83e945875100ceca322ebd50d96714206
0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon UlbrichtModule : $Header$
0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon UlbrichtDescription : Gtk Module to enable disproving Theorems
0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon UlbrichtCopyright : (c) Simon Ulbricht, Uni Bremen 2010
0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon UlbrichtLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon UlbrichtMaintainer : tekknix@informatik.uni-bremen.de
0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon UlbrichtStability : provisional
0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon UlbrichtPortability : portable
0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon UlbrichtThis module provides a disproving module that checks consistency of inverted
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbrichtimport Data.Time.LocalTime (timeToTimeOfDay)
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbrichtimport Data.Time.Clock (secondsToDiffTime)
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbrichtimport Data.Ord (comparing)
2643008447e30b6025f742eb6a661f38be756b1eSimon Ulbricht -- TODO write error messages with content!
2643008447e30b6025f742eb6a661f38be756b1eSimon Ulbricht -- TODO use return value of consistencyCheck and mark node
2643008447e30b6025f742eb6a661f38be756b1eSimon Ulbricht -- TODO implement in GtkProverGui
d815d2b83e945875100ceca322ebd50d96714206Simon UlbrichtdisproveNode ::
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht AnyComorphism -> String -> LNode DGNodeLab
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht -> ProofState lid sentence -> Int -> IO (ProofState lid sentence)
d815d2b83e945875100ceca322ebd50d96714206Simon UlbrichtdisproveNode ac@(Comorphism cid) selGoal (i, lbl) state t'' = undefined {- do
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht case (fst . head) $ getConsCheckers [ac] of
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht (G_cons_checker lid4 cc) ->
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht lidS = sourceLogic cid
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht lidT = targetLogic cid
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht thName = getDGNodeName lbl
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht t = t'' * 1000000
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht t' = timeToTimeOfDay $ secondsToDiffTime $ toInteger t''
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht ts = TacticScript $ if ccNeedsTimer cc then "" else show t''
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht mTimeout = "No results within: " ++ show t'
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht (G_theory lid1 (ExtSign sign _) _ axs _) <- getGlobalTheory lbl
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht let sens = toNamedList axs
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht bTh'@(sig1, _) <- coerceBasicTheory lid1 lidS "" (sign, sens)
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht (sig2, sens2) <- wrapMapTheory cid bTh'
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht incl <- subsig_inclusion lidT (empty_signature lidT) sig2
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht return (sig1, TheoryMorphism
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht { tSource = emptyTheory lidT
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht , tTarget = Theory sig2 $ toThSens sens2
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht , tMorphism = incl }) of
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht Result ds Nothing -> return state -- node is not changed
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht Result _ (Just (sig1, mor)) -> do
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht cc' <- coerceConsChecker lid4 lidT "" cc
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht ccS <- (if ccNeedsTimer cc then timeout t else ((return . Just) =<<))
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht (ccAutomatic cc' thName ts mor [])
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht return $ case ccS of
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht Just ccStatus ->
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht case ccResult ccStatus of
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht Just b -> if b
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht then let ps'' = openProofStatus selGoal
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht (getPName cc) (ccProofTree ccStatus)
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht ps' = ps'' { goalStatus = Disproved }
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht in markProved ac lidT [ps'] state
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht Nothing -> state
d815d2b83e945875100ceca322ebd50d96714206Simon Ulbricht Nothing -> state