c82fca6d3f5608b946f18d37e8710b1d71e3478dnd{- |

c82fca6d3f5608b946f18d37e8710b1d71e3478dndModule : $Header$

fd9abdda70912b99b24e3bf1a38f26fde908a74cndDescription : Gtk Module to enable disproving Theorems

fd9abdda70912b99b24e3bf1a38f26fde908a74cndCopyright : (c) Simon Ulbricht, Uni Bremen 2010

fd9abdda70912b99b24e3bf1a38f26fde908a74cndLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

c82fca6d3f5608b946f18d37e8710b1d71e3478dnd

c82fca6d3f5608b946f18d37e8710b1d71e3478dndMaintainer : tekknix@informatik.uni-bremen.de

c82fca6d3f5608b946f18d37e8710b1d71e3478dndStability : provisional

c82fca6d3f5608b946f18d37e8710b1d71e3478dndPortability : portable

96ad5d81ee4a2cc66a4ae19893efc8aa6d06fae7jailletc

c82fca6d3f5608b946f18d37e8710b1d71e3478dndThis module provides a disproving module that checks consistency of inverted

c82fca6d3f5608b946f18d37e8710b1d71e3478dndtheorems.

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen-}

2e545ce2450a9953665f701bb05350f0d3f26275nd

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowenmodule GUI.GtkDisprove where

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen

c82fca6d3f5608b946f18d37e8710b1d71e3478dndimport Static.GTheory

c82fca6d3f5608b946f18d37e8710b1d71e3478dndimport Static.DevGraph

af33a4994ae2ff15bc67d19ff1a7feb906745bf8rbowenimport Static.ComputeTheory

3f08db06526d6901aa08c110b5bc7dde6bc39905nd

c82fca6d3f5608b946f18d37e8710b1d71e3478dndimport Proofs.AbstractState

c82fca6d3f5608b946f18d37e8710b1d71e3478dnd

c82fca6d3f5608b946f18d37e8710b1d71e3478dndimport Common.ExtSign

fc056b4d564cebe1d186a536e9d21fb661a2f5c5humbedoohimport Common.Result

3b3b7fc78d1f5bfc2769903375050048ff41ff26ndimport Common.AS_Annotation

d474d8ef01ec5c2a09341cd148851ed383c3287crbowenimport Common.OrderedMap as OMap

d474d8ef01ec5c2a09341cd148851ed383c3287crbowen

3b3b7fc78d1f5bfc2769903375050048ff41ff26ndimport Logic.Logic

3b3b7fc78d1f5bfc2769903375050048ff41ff26ndimport Logic.Prover

4eb0f4031876c60c0ba2035666579dac07304b9drbowenimport Logic.Comorphism

4eb0f4031876c60c0ba2035666579dac07304b9drbowenimport Logic.Coerce

4eb0f4031876c60c0ba2035666579dac07304b9drbowen

4eb0f4031876c60c0ba2035666579dac07304b9drbowenimport Data.Graph.Inductive.Graph

c82fca6d3f5608b946f18d37e8710b1d71e3478dnd

c82fca6d3f5608b946f18d37e8710b1d71e3478dndimport System.Timeout

4eb0f4031876c60c0ba2035666579dac07304b9drbowen

c82fca6d3f5608b946f18d37e8710b1d71e3478dnd -- TODO use return value of consistencyCheck and mark node

fc056b4d564cebe1d186a536e9d21fb661a2f5c5humbedooh -- TODO implement in GtkProverGui

c40959d803d2d8328b2ead89dd975ac88ba946f6humbedooh

c82fca6d3f5608b946f18d37e8710b1d71e3478dnddisproveNode :: Logic lid sublogics

c82fca6d3f5608b946f18d37e8710b1d71e3478dnd basic_spec sentence symb_items symb_map_items

c82fca6d3f5608b946f18d37e8710b1d71e3478dnd sign morphism symbol raw_symbol proof_tree =>

c82fca6d3f5608b946f18d37e8710b1d71e3478dnd AnyComorphism -> String -> LNode DGNodeLab

fc056b4d564cebe1d186a536e9d21fb661a2f5c5humbedooh -> ProofState lid sentence -> Int -> IO (ProofState lid sentence)

c82fca6d3f5608b946f18d37e8710b1d71e3478dnddisproveNode ac@(Comorphism cid) selGoal (_, lbl) state t'' = do

fc056b4d564cebe1d186a536e9d21fb661a2f5c5humbedooh case (fst . head) $ getConsCheckers [ac] of

fc056b4d564cebe1d186a536e9d21fb661a2f5c5humbedooh (G_cons_checker lid4 cc) ->

fc056b4d564cebe1d186a536e9d21fb661a2f5c5humbedooh let

fc056b4d564cebe1d186a536e9d21fb661a2f5c5humbedooh lidS = sourceLogic cid

fc056b4d564cebe1d186a536e9d21fb661a2f5c5humbedooh lidT = targetLogic cid

fc056b4d564cebe1d186a536e9d21fb661a2f5c5humbedooh thName = getDGNodeName lbl

fc056b4d564cebe1d186a536e9d21fb661a2f5c5humbedooh t = t'' * 1000000

c82fca6d3f5608b946f18d37e8710b1d71e3478dnd ts = TacticScript $ if ccNeedsTimer cc then "" else show t''

c82fca6d3f5608b946f18d37e8710b1d71e3478dnd in case do

c82fca6d3f5608b946f18d37e8710b1d71e3478dnd (G_theory lid1 (ExtSign sign _) _ axs _) <- getGlobalTheory lbl

c40959d803d2d8328b2ead89dd975ac88ba946f6humbedooh let axs' = OMap.filter isAxiom axs

c40959d803d2d8328b2ead89dd975ac88ba946f6humbedooh negSen = case OMap.lookup selGoal axs of

fc056b4d564cebe1d186a536e9d21fb661a2f5c5humbedooh Nothing -> error "GtkDisprove.disproveNode(1)"

fc056b4d564cebe1d186a536e9d21fb661a2f5c5humbedooh Just sen -> sen {-

c40959d803d2d8328b2ead89dd975ac88ba946f6humbedooh case negation lid1 $ sentence sen of

c40959d803d2d8328b2ead89dd975ac88ba946f6humbedooh Nothing -> error "GtkDisprove.disproveNode(2)"

c40959d803d2d8328b2ead89dd975ac88ba946f6humbedooh Just sen' -> sen { sentence = sen' } -}

c82fca6d3f5608b946f18d37e8710b1d71e3478dnd sens = toNamedList $ OMap.insert selGoal negSen axs'

c82fca6d3f5608b946f18d37e8710b1d71e3478dnd bTh'@(sig1, _) <- coerceBasicTheory lid1 lidS "" (sign, sens)

4eb0f4031876c60c0ba2035666579dac07304b9drbowen (sig2, sens2) <- wrapMapTheory cid bTh'

d05d0eb4ae6d2a5e513fc3bf2555ce33da416634nd incl <- subsig_inclusion lidT (empty_signature lidT) sig2

d05d0eb4ae6d2a5e513fc3bf2555ce33da416634nd return (sig1, TheoryMorphism

d05d0eb4ae6d2a5e513fc3bf2555ce33da416634nd { tSource = emptyTheory lidT

fc056b4d564cebe1d186a536e9d21fb661a2f5c5humbedooh , tTarget = Theory sig2 $ toThSens sens2

d05d0eb4ae6d2a5e513fc3bf2555ce33da416634nd , tMorphism = incl }) of

fc056b4d564cebe1d186a536e9d21fb661a2f5c5humbedooh Result _ Nothing -> return state -- node is not changed

fc056b4d564cebe1d186a536e9d21fb661a2f5c5humbedooh Result _ (Just (_, mor)) -> do

d05d0eb4ae6d2a5e513fc3bf2555ce33da416634nd cc' <- coerceConsChecker lid4 lidT "" cc

d05d0eb4ae6d2a5e513fc3bf2555ce33da416634nd putStrLn $ ccName cc'

c82fca6d3f5608b946f18d37e8710b1d71e3478dnd ccS <- (if ccNeedsTimer cc' then timeout t else ((return . Just) =<<))

c82fca6d3f5608b946f18d37e8710b1d71e3478dnd (ccAutomatic cc' thName ts mor [])

3b3b7fc78d1f5bfc2769903375050048ff41ff26nd return $ case ccS of

d474d8ef01ec5c2a09341cd148851ed383c3287crbowen Just ccStatus ->

d474d8ef01ec5c2a09341cd148851ed383c3287crbowen case ccResult ccStatus of

3b3b7fc78d1f5bfc2769903375050048ff41ff26nd Just b -> if b

205f749042ed530040a4f0080dbcb47ceae8a374rjung then let ps' = openProofStatus selGoal

af33a4994ae2ff15bc67d19ff1a7feb906745bf8rbowen (ccName cc') (ccProofTree ccStatus)

0d0ba3a410038e179b695446bb149cce6264e0abnd ps = ps' { goalStatus = Disproved }

7fec19672a491661b2fe4b29f685bc7f4efa64d4nd in markProved ac lidT [ps] state

7fec19672a491661b2fe4b29f685bc7f4efa64d4nd else state

7fec19672a491661b2fe4b29f685bc7f4efa64d4nd Nothing -> state

b636af865d96808dfb18913d607442a150fb53b6jim Nothing -> state