b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantzmodule GUI.GtkDisprove where

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantzimport Common.LibName

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantzimport Common.AS_Annotation

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantzimport qualified Common.OrderedMap as OMap

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantzimport Data.Graph.Inductive.Graph (LNode)

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantzimport Logic.Comorphism

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantzimport Logic.Logic

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantzimport Proofs.AbstractState

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantzimport Proofs.ConsistencyCheck

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantzimport Static.DevGraph

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantzimport Static.GTheory

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz -- TODO write error messages with content!

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

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz -- TODO implement in GtkProverGui

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantzdisproveNode :: G_cons_checker -> AnyComorphism -> String -> LNode DGNodeLab

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz -> Int -> IO ConsistencyStatus

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantzdisproveNode cc ac selGoal (i, l) timeout =

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz case globalTheory l of

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

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz Just (G_theory lid a b sens c) ->

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz let axioms = OMap.filter isAxiom sens

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz negSen = case OMap.lookup selGoal sens of

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

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz Just sen ->

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz case negation lid $ sentence sen of

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz Nothing -> error "GtkDisprove.disproveNode(3)"

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

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz sens' = OMap.insert selGoal negSen axioms

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz in consistencyCheckAux False cc ac (i, l {globalTheory =

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz Just (G_theory lid a b sens' c) }) timeout

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz

b4a287513d176e4355dd56ea47b27228e0e5d75fjerenkrantz