GtkDisprove.hs revision a81a6e924a0a027f48823b0a09cf51ad807c2e5b
7e79e8fd53348f9fc6e8009a4a2522425ab6f08ffieldingModule : $Header$
7e79e8fd53348f9fc6e8009a4a2522425ab6f08ffieldingDescription : Gtk Module to enable disproving Theorems
7e79e8fd53348f9fc6e8009a4a2522425ab6f08ffieldingCopyright : (c) Simon Ulbricht, Uni Bremen 2010
7e79e8fd53348f9fc6e8009a4a2522425ab6f08ffieldingLicense : GPLv2 or higher, see LICENSE.txt
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fieldingMaintainer : tekknix@informatik.uni-bremen.de
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fieldingStability : provisional
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fieldingPortability : portable
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fieldingThis module provides a disproving module that checks consistency of inverted
7e79e8fd53348f9fc6e8009a4a2522425ab6f08ffieldingimport qualified Common.OrderedMap as OMap
7e79e8fd53348f9fc6e8009a4a2522425ab6f08ffieldingdisproveThmSingle :: String -- ^ selected goal to disprove
7e79e8fd53348f9fc6e8009a4a2522425ab6f08ffielding -> String -- ^ selected prover
7e79e8fd53348f9fc6e8009a4a2522425ab6f08ffielding -> LNode DGNodeLab
7e79e8fd53348f9fc6e8009a4a2522425ab6f08ffielding -> Int -- ^ timeout limit
7e79e8fd53348f9fc6e8009a4a2522425ab6f08ffielding -> IO () -- ^ results are only displayed to the user.
7e79e8fd53348f9fc6e8009a4a2522425ab6f08ffieldingdisproveThmSingle selGoal selPr (_, lbl) t'' =
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding let info s = infoDialog ("Disprove " ++ selGoal) s in
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding case globalTheory lbl of
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding Nothing -> info "Disprove failed: No global Theory"
7e79e8fd53348f9fc6e8009a4a2522425ab6f08ffielding Just (G_theory lid1 (ExtSign sign symb) i1 sens i2) ->
7e79e8fd53348f9fc6e8009a4a2522425ab6f08ffielding case OMap.lookup selGoal sens of
7e79e8fd53348f9fc6e8009a4a2522425ab6f08ffielding Nothing -> error "GtkDisprove.disproveThmSingle(1)"
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding Just sen -> case negation lid1 $ sentence sen of
7e79e8fd53348f9fc6e8009a4a2522425ab6f08ffielding Nothing -> info "Disprove failed: negation is not defined"
7e79e8fd53348f9fc6e8009a4a2522425ab6f08ffielding Just s' -> do
7e79e8fd53348f9fc6e8009a4a2522425ab6f08ffielding let negSen = sen { sentence = s', isAxiom = True }
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding axs = OMap.filter isAxiom sens
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding sens' = OMap.insert selGoal negSen axs
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding g_th = G_theory lid1 (ExtSign sign symb) i1 sens' i2
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding subL = sublogicOfTh g_th
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding lcc = getConsCheckers $ findComorphismPaths logicGraph subL
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding case find (\ (p, _) -> getPName p == selPr) lcc of
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding info $ "failed to find Consistency Checker for the selected prover\n\n"
2d71630471d1c23f0137309e3c3957c633ecbfd6rbb ++ "possible ConsCheckers are:\n" ++ intercalate "\n"
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding (nubOrd $ map (getPName . fst) lcc)
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding Just (G_cons_checker lid4 cc, Comorphism cid) -> do
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding let lidS = sourceLogic cid
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding lidT = targetLogic cid
51af95bb51b5084e883bad250b2afa2838e9ceebfielding bTh' <- coerceBasicTheory lid1 lidS "" (sign, toNamedList sens')
b6055b7832a0e4d0818416252fff5925aaebae4brbb (sig2, sens2) <- wrapMapTheory cid bTh'
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding incl <- subsig_inclusion lidT (empty_signature lidT) sig2
48d7c43629323c8d5ee9f7bd0d194de0a376b391rbb return TheoryMorphism
d4f1d9c1ff112a8ab9bee31f196973761329b236rbb { tSource = emptyTheory lidT
48d7c43629323c8d5ee9f7bd0d194de0a376b391rbb , tTarget = Theory sig2 $ toThSens sens2
48d7c43629323c8d5ee9f7bd0d194de0a376b391rbb , tMorphism = incl }
d4f1d9c1ff112a8ab9bee31f196973761329b236rbb case maybeResult res of
48d7c43629323c8d5ee9f7bd0d194de0a376b391rbb Nothing ->
fdeba8dafd227781a897c772905bb32197e92797trawick info "Disprove failed: TheoryMorphism could not be constructed"
fdeba8dafd227781a897c772905bb32197e92797trawick Just mor -> do
fdeba8dafd227781a897c772905bb32197e92797trawick let thName = getDGNodeName lbl
48d7c43629323c8d5ee9f7bd0d194de0a376b391rbb ts = TacticScript $ if ccNeedsTimer cc then "" else show t''
d4f1d9c1ff112a8ab9bee31f196973761329b236rbb cc' <- coerceConsChecker lid4 lidT "" cc
48d7c43629323c8d5ee9f7bd0d194de0a376b391rbb ccS <- (if ccNeedsTimer cc' then timeoutSecs t'' else ((return . Just) =<<))
d41217398f0e1031adbb6f5bd37f45737c805deftrawick (ccAutomatic cc' thName ts mor [])
d41217398f0e1031adbb6f5bd37f45737c805deftrawick case ccS of
d41217398f0e1031adbb6f5bd37f45737c805deftrawick Just ccStatus -> do
d4f1d9c1ff112a8ab9bee31f196973761329b236rbb info $ "the ConsistencyChecker " ++ ccName cc' ++ " has returned "
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding ++ "the following " ++ case ccResult ccStatus of
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding Nothing -> ""
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding Just b -> if b then "consistent" else "inconsistent"
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding ++ " results:\n" ++ show (ccProofTree ccStatus)
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding Nothing -> do
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding info $ "the ConsistencyChecker has not returned any results\n"
09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding ++ "ConsistencyChecker used: " ++ ccName cc'