GtkDisprove.hs revision 560958e077f513ce6a1633d4514f1950c6840993
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasModule : $Header$
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasDescription : Gtk Module to enable disproving Theorems
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis TsogiasCopyright : (c) Simon Ulbricht, Uni Bremen 2010
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasMaintainer : tekknix@informatik.uni-bremen.de
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasStability : provisional
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasPortability : portable
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis TsogiasThis module provides a disproving module that checks consistency of inverted
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasimport Data.Time.LocalTime (timeToTimeOfDay)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasimport Data.Time.Clock (secondsToDiffTime)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasimport Data.Ord (comparing)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias -- TODO use return value of consistencyCheck and mark node
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias -- TODO implement in GtkProverGui
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasdisproveNode ::
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias AnyComorphism -> String -> LNode DGNodeLab
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias -> ProofState lid sentence -> Int -> IO (ProofState lid sentence)
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis TsogiasdisproveNode ac@(Comorphism cid) selGoal (i, lbl) state t'' = undefined {- do
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias case (fst . head) $ getConsCheckers [ac] of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias (G_cons_checker lid4 cc) ->
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias lidS = sourceLogic cid
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias lidT = targetLogic cid
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias thName = getDGNodeName lbl
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias t = t'' * 1000000
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias t' = timeToTimeOfDay $ secondsToDiffTime $ toInteger t''
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias ts = TacticScript $ if ccNeedsTimer cc then "" else show t''
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias mTimeout = "No results within: " ++ show t'
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias (G_theory lid1 (ExtSign sign _) _ axs _) <- getGlobalTheory lbl
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias let axs' = OMap.filter isAxiom axs
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias negSen = case OMap.lookup selGoal sens of
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias Nothing -> error "GtkDisprove.disproveNode(1)"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias case negation lid $ sentence sen of
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias Nothing -> error "GtkDisprove.disproveNode(2)"
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias Just sen' -> sen { sentence = sen' }
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias sens = toNamedList $ OMap.insert selGoal negSen axs'
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias bTh'@(sig1, _) <- coerceBasicTheory lid1 lidS "" (sign, sens)
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias (sig2, sens2) <- wrapMapTheory cid bTh'
4cea468e955597a7069faba3f43f27e913f2b651Alexis Tsogias incl <- subsig_inclusion lidT (empty_signature lidT) sig2
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias return (sig1, TheoryMorphism
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias { tSource = emptyTheory lidT
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias , tTarget = Theory sig2 $ toThSens sens2
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias , tMorphism = incl }) of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias Result ds Nothing -> return state -- node is not changed
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias Result _ (Just (sig1, mor)) -> do
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias cc' <- coerceConsChecker lid4 lidT "" cc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias ccS <- (if ccNeedsTimer cc then timeout t else ((return . Just) =<<))
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias (ccAutomatic cc' thName ts mor [])
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias return $ case ccS of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias Just ccStatus ->
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias case ccResult ccStatus of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias Just b -> if b
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias then let ps'' = openProofStatus selGoal
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias (getPName cc) (ccProofTree ccStatus)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias ps' = ps'' { goalStatus = Disproved }
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias in markProved ac lidT [ps'] state
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias Nothing -> state
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias Nothing -> state