1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{- |

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuModule : $Header$

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerDescription : Logic for manipulating the graph in the Central GUI

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuCopyright : (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006

431571057e88a650a974adec93ea4bb5173b6213Felix Gabriel ManceLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuMaintainer : till@tzi.de

431571057e88a650a974adec93ea4bb5173b6213Felix Gabriel ManceStability : provisional

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuPortability : non-portable (imports Logic)

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-}

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiumodule GUI.GraphLogic

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu ( undo

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , redo

19e01e1a7e319063434bd86c8ecbc5f241ef9993Felix Gabriel Mance , reload

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , performProofAction

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski , openProofStatus

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , saveProofStatus

a604cbad8e2202147b5c6bb9f2e06ae61162d654Felix Gabriel Mance , nodeErr

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , proofMenu

be2439588008221e691321fdf4f75432cfb72878Felix Gabriel Mance , openTranslateGraph

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , showReferencedLibrary

fc05327b875b5723b6c17849b83477f29ec12c90Felix Gabriel Mance , showSpec

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , getSignatureOfNode

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , getTheoryOfNode

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , getLocalAxOfNode

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , translateTheoryOfNode

0dd6e7830de0887c9a12356447975a826b3b3db2Christian Maeder , displaySubsortGraph

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , displayConceptGraph

e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder , lookupTheoryOfNode

424860079d47bf490fa98d5d7498096a0447c569mcodescu , getSublogicOfNode

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , showOriginOfNode

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , showProofStatusOfNode

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder , proveAtNode

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder , showJustSubtree

32bbac77828be0233953f8fe476edb0a9585408dChristian Maeder , showIDOfEdge

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , getNumberOfNode

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , showMorphismOfEdge

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , showOriginOfEdge

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , checkconservativityOfEdge

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , showProofStatusOfThm

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , convertNodes

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , convertEdges

27fdf879983dd28e211b41f3be6c0e930b7c816bFelix Gabriel Mance , hideNodes

431571057e88a650a974adec93ea4bb5173b6213Felix Gabriel Mance , getLibDeps

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder , hideShowNames

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , showNodes

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , translateGraph

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , showLibGraph

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu )

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu where

b84c87f199dc287d235d7dad6ea344f6912ef531Christian Maeder

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Logic.Logic(conservativityCheck)

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Logic.Coerce(coerceSign, coerceMorphism)

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Logic.Grothendieck

be00381168b3f10192afabbba136fb06d3a9f358Christian Maederimport Logic.Comorphism

be00381168b3f10192afabbba136fb06d3a9f358Christian Maederimport Logic.Prover

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu

27fdf879983dd28e211b41f3be6c0e930b7c816bFelix Gabriel Manceimport Comorphisms.LogicGraph(logicGraph)

7852de3551fc797566ee71165bafe05b6d81728cnotanartist

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Syntax.AS_Library(LIB_NAME, getModTime, getLIB_ID)

27fdf879983dd28e211b41f3be6c0e930b7c816bFelix Gabriel Mance

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Static.DevGraph

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Static.DGToSpec(dgToSpec, computeTheory)

27fdf879983dd28e211b41f3be6c0e930b7c816bFelix Gabriel Manceimport Static.AnalysisLibrary(anaLibExt, anaLib)

d0f58d27c2536eba454d8f77de8617bc6a2c99cdFelix Gabriel Manceimport Static.DGTranslation(libEnv_translation)

d0f58d27c2536eba454d8f77de8617bc6a2c99cdFelix Gabriel Mance

d0f58d27c2536eba454d8f77de8617bc6a2c99cdFelix Gabriel Manceimport Proofs.EdgeUtils

d0f58d27c2536eba454d8f77de8617bc6a2c99cdFelix Gabriel Manceimport Proofs.InferBasic(basicInferenceNode)

431571057e88a650a974adec93ea4bb5173b6213Felix Gabriel Manceimport Proofs.StatusUtils(lookupHistory, removeContraryChanges)

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu

27fdf879983dd28e211b41f3be6c0e930b7c816bFelix Gabriel Manceimport GUI.Utils(listBox, createTextSaveDisplay)

424860079d47bf490fa98d5d7498096a0447c569mcodescuimport GUI.Taxonomy (displayConceptGraph,displaySubsortGraph)

60f30f0eeeacdfc1e0dfe39664373ddf5a0675adFelix Gabriel Manceimport GUI.DGTranslation(getDGLogic)

60f30f0eeeacdfc1e0dfe39664373ddf5a0675adFelix Gabriel Manceimport GUI.GraphTypes

0dd6e7830de0887c9a12356447975a826b3b3db2Christian Maederimport GUI.AbstractGraphView as AGV

424860079d47bf490fa98d5d7498096a0447c569mcodescuimport qualified GUI.HTkUtils (displayTheory,

424860079d47bf490fa98d5d7498096a0447c569mcodescu displayTheoryWithWarning,

424860079d47bf490fa98d5d7498096a0447c569mcodescu createInfoDisplayWithTwoButtons)

60f30f0eeeacdfc1e0dfe39664373ddf5a0675adFelix Gabriel Mance

d6d81ead61a5f9fb7d047e623f7898e730c258camcodescuimport GraphDisp(deleteArc, deleteNode)

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport TextDisplay(createTextDisplay)

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport InfoBus(encapsulateWaitTermAct)

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport DialogWin (useHTk)

60f30f0eeeacdfc1e0dfe39664373ddf5a0675adFelix Gabriel Manceimport Messages(errorMess)

7852de3551fc797566ee71165bafe05b6d81728cnotanartistimport qualified HTk

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu

60f30f0eeeacdfc1e0dfe39664373ddf5a0675adFelix Gabriel Manceimport Common.Id(nullRange)

9475501a6acf48434052d9e6f4a05ed6681eaaabFrancisc Nicolae Bungiuimport Common.DocUtils(showDoc, pretty)

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Common.Doc(vcat)

7852de3551fc797566ee71165bafe05b6d81728cnotanartistimport Common.ResultT(liftR, runResultT)

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowskiimport Common.AS_Annotation(isAxiom)

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowskiimport Common.Result as Res

424860079d47bf490fa98d5d7498096a0447c569mcodescuimport qualified Common.OrderedMap as OMap

0dd6e7830de0887c9a12356447975a826b3b3db2Christian Maederimport qualified Common.InjMap as InjMap

0dd6e7830de0887c9a12356447975a826b3b3db2Christian Maederimport qualified Common.Lib.Rel as Rel

424860079d47bf490fa98d5d7498096a0447c569mcodescuimport qualified Common.Lib.Graph as Tree

0dd6e7830de0887c9a12356447975a826b3b3db2Christian Maeder

0dd6e7830de0887c9a12356447975a826b3b3db2Christian Maederimport Driver.Options

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Driver.WriteFn(writeShATermFile)

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Driver.ReadFn(libNameToFile, readVerbose)

d0f58d27c2536eba454d8f77de8617bc6a2c99cdFelix Gabriel Mance

60f30f0eeeacdfc1e0dfe39664373ddf5a0675adFelix Gabriel Manceimport System.Directory(getModificationTime)

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Data.IORef

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Data.Maybe(fromJust)

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Data.List(nub,deleteBy,find)

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Data.Graph.Inductive.Graph as Graph(Node, LEdge, LNode, lab', labNode')

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport qualified Data.IntMap as IntMap

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport qualified Data.Map as Map

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu--import Control.Monad()

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Control.Monad.Trans(lift)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Control.Concurrent.MVar(tryPutMVar, readMVar, tryTakeMVar)

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | Undo one step of the History

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederundo :: GInfo -> LibEnv -> IO ()

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuundo (GInfo {libEnvIORef = ioRefProofStatus,

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu conversionMapsIORef = convRef,

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu graphId = gid,

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu gi_LIB_NAME = ln,

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder gi_GraphInfo = actGraphInfo

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu }) initEnv = do

31e9d2a02e15b7dbc157e0d3fb3b84f6c8666482Christian Maeder oldEnv <- readIORef ioRefProofStatus

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu let

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu gctx = lookupGlobalContext ln oldEnv

656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder initgctx = lookupGlobalContext ln initEnv

d3cb3401882f6956de016f8eecbec1cd3b868acbFelix Gabriel Mance phist = proofHistory gctx

d3cb3401882f6956de016f8eecbec1cd3b868acbFelix Gabriel Mance rhist = redoHistory gctx

d3cb3401882f6956de016f8eecbec1cd3b868acbFelix Gabriel Mance if phist == [emptyHistory] then return ()

d3cb3401882f6956de016f8eecbec1cd3b868acbFelix Gabriel Mance else do

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu let

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu lastchange = head phist

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu phist' = tail phist

7852de3551fc797566ee71165bafe05b6d81728cnotanartist rhist' = lastchange:rhist

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu gctx' = (applyProofHistory phist' initgctx ) {redoHistory = rhist'}

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu newEnv = Map.insert ln gctx' initEnv

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu dgraph = devGraph gctx'

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu writeIORef ioRefProofStatus newEnv

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu remakeGraph convRef gid actGraphInfo dgraph ln

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu

0dd6e7830de0887c9a12356447975a826b3b3db2Christian Maeder-- | redo one step of the redoHistory

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuredo :: GInfo -> LibEnv -> IO ()

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuredo (GInfo {libEnvIORef = ioRefProofStatus,

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu conversionMapsIORef = convRef,

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu graphId = gid,

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu gi_LIB_NAME = ln,

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu gi_GraphInfo = actGraphInfo

06acd8a23b2f06e7b2373d53f738cf56c7f03223Francisc Nicolae Bungiu }) initEnv = do

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu oldEnv <- readIORef ioRefProofStatus

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu let

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu gctx = lookupGlobalContext ln oldEnv

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu initgctx = lookupGlobalContext ln initEnv

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu phist = proofHistory gctx

7852de3551fc797566ee71165bafe05b6d81728cnotanartist rhist = redoHistory gctx

32bbac77828be0233953f8fe476edb0a9585408dChristian Maeder if rhist == [emptyHistory] then return ()

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski else do

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski let

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski nextchange = head rhist

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski rhist' = tail rhist

32bbac77828be0233953f8fe476edb0a9585408dChristian Maeder phist' = nextchange:phist

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski gctx' = (applyProofHistory phist' initgctx) {redoHistory = rhist'}

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu newEnv = Map.insert ln gctx' initEnv

cf0439f74f1d55a9840d38a88f9b0f4fc00d5547Christian Maeder dgraph = devGraph gctx'

cf0439f74f1d55a9840d38a88f9b0f4fc00d5547Christian Maeder writeIORef ioRefProofStatus newEnv

cf0439f74f1d55a9840d38a88f9b0f4fc00d5547Christian Maeder remakeGraph convRef gid actGraphInfo dgraph ln

cf0439f74f1d55a9840d38a88f9b0f4fc00d5547Christian Maeder

b84c87f199dc287d235d7dad6ea344f6912ef531Christian Maeder-- | reloads the Library of the DevGraph

7852de3551fc797566ee71165bafe05b6d81728cnotanartistreload :: GInfo -> IO()

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowskireload (GInfo {libEnvIORef = ioRefProofStatus,

cf0439f74f1d55a9840d38a88f9b0f4fc00d5547Christian Maeder conversionMapsIORef = convRef,

cf0439f74f1d55a9840d38a88f9b0f4fc00d5547Christian Maeder graphId = gid,

cf0439f74f1d55a9840d38a88f9b0f4fc00d5547Christian Maeder gi_LIB_NAME = ln,

cf0439f74f1d55a9840d38a88f9b0f4fc00d5547Christian Maeder gi_GraphInfo = actGraphInfo,

cf0439f74f1d55a9840d38a88f9b0f4fc00d5547Christian Maeder gi_hetcatsOpts = opts

cf0439f74f1d55a9840d38a88f9b0f4fc00d5547Christian Maeder }) = do

cf0439f74f1d55a9840d38a88f9b0f4fc00d5547Christian Maeder oldle <- readIORef ioRefProofStatus

cf0439f74f1d55a9840d38a88f9b0f4fc00d5547Christian Maeder let

cf0439f74f1d55a9840d38a88f9b0f4fc00d5547Christian Maeder libdeps = Rel.toList $ Rel.intransKernel $ Rel.transClosure $ Rel.fromList

cf0439f74f1d55a9840d38a88f9b0f4fc00d5547Christian Maeder $ getLibDeps oldle

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu ioruplibs <- newIORef ([] :: [LIB_NAME])

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu writeIORef ioruplibs []

7852de3551fc797566ee71165bafe05b6d81728cnotanartist reloadLibs ioRefProofStatus opts libdeps ioruplibs ln

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu le <- readIORef ioRefProofStatus

7852de3551fc797566ee71165bafe05b6d81728cnotanartist let

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski dgraph = devGraph $ lookupGlobalContext ln le

624f8c31bd8d6746b93f4b5966aa6fc7680fefc5Felix Gabriel Mance writeIORef ioRefProofStatus le

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski remakeGraph convRef gid actGraphInfo dgraph ln

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- | Creates a list of all LIB_NAME pairs, which have a dependency

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiugetLibDeps :: LibEnv -> [(LIB_NAME, LIB_NAME)]

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiugetLibDeps le =

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu concat $ map (\ ln -> getDep ln le) $ Map.keys le

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- | Creates a list of LIB_NAME pairs for the fist argument

b84c87f199dc287d235d7dad6ea344f6912ef531Christian MaedergetDep :: LIB_NAME -> LibEnv -> [(LIB_NAME, LIB_NAME)]

624f8c31bd8d6746b93f4b5966aa6fc7680fefc5Felix Gabriel MancegetDep ln le =

7852de3551fc797566ee71165bafe05b6d81728cnotanartist map (\ x -> (ln, x)) $ map (\ (_,x,_) -> dgn_libname x) $ IntMap.elems $

624f8c31bd8d6746b93f4b5966aa6fc7680fefc5Felix Gabriel Mance IntMap.filter (\ (_,x,_) -> isDGRef x) $ Tree.convertToMap $

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder dgBody $ devGraph $ lookupGlobalContext ln le

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- | Reloads a library

ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiureloadLib :: IORef LibEnv -> HetcatsOpts -> IORef [LIB_NAME] -> LIB_NAME

d0f58d27c2536eba454d8f77de8617bc6a2c99cdFelix Gabriel Mance -> IO ()

431571057e88a650a974adec93ea4bb5173b6213Felix Gabriel MancereloadLib iorle opts ioruplibs ln = do

431571057e88a650a974adec93ea4bb5173b6213Felix Gabriel Mance mfile <- existsAnSource opts {intype = GuessIn}

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescu $ rmSuffix $ libNameToFile opts ln

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescu case mfile of

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescu Nothing -> do

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescu return ()

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescu Just file -> do

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescu le <- readIORef iorle

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescu let

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescu le' = Map.delete ln le

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescu mres <- anaLibExt opts file le'

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescu case mres of

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescu Just (_, newle) -> do

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescu uplibs <- readIORef ioruplibs

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescu writeIORef ioruplibs $ ln:uplibs

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescu writeIORef iorle newle

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescu return ()

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescu Nothing -> do

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescu fail $ "Could not read original development graph from '"++ file

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescu ++ "'"

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescu return ()

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescu

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescu-- | Reloads libraries if nessesary

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescureloadLibs :: IORef LibEnv -> HetcatsOpts -> [(LIB_NAME, LIB_NAME)]

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescu -> IORef [LIB_NAME] -> LIB_NAME -> IO Bool

b90f0b7fd6ccfbdd7e5adb65b1f6c02c7758ff5cmcodescureloadLibs iorle opts deps ioruplibs ln = do

uplibs <- readIORef ioruplibs

case elem ln uplibs of

True -> return True

False -> do

let

deps' = map (snd) $ filter (\ (ln',_) -> ln == ln') deps

res <- mapM (reloadLibs iorle opts deps ioruplibs) deps'

let

libupdate = foldl (\ u r -> if r then True else u) False res

case libupdate of

True -> do

reloadLib iorle opts ioruplibs ln

return True

False -> do

le <- readIORef iorle

let

newln:_ = filter (ln ==) $ Map.keys le

mfile <- existsAnSource opts $ rmSuffix $ libNameToFile opts ln

case mfile of

Nothing -> do

return False

Just file -> do

newmt <- getModificationTime file

let

libupdate' = (getModTime $ getLIB_ID newln) < newmt

case libupdate' of

False -> return False

True -> do

reloadLib iorle opts ioruplibs ln

return True

-- | Deletes the old edges and nodes of the Graph and makes new ones

remakeGraph :: IORef ConversionMaps -> Descr -> GraphInfo -> DGraph -> LIB_NAME

-> IO ()

remakeGraph convRef gid actginfo dgraph ln = do

(gs,ev_cnt) <- readIORef actginfo

let

Just (_, g) = find (\ (gid', _) -> gid' == gid) gs

gs' = deleteBy (\ (gid1,_) (gid2,_) -> gid1 == gid2) (gid,g) gs

og = theGraph g

-- reads and delets the old nodes and edges

mapM_ (deleteArc og) $ map (\ (_,_,_,x) -> x) $ map snd $ AGV.edges g

mapM_ (deleteNode og) $ map snd $ map snd $ AGV.nodes g

-- stores the graph without nodes and edges in the GraphInfo

let

g' = g {theGraph = og, AGV.nodes = [], AGV.edges = []}

writeIORef actginfo ((gid,g'):gs',ev_cnt)

-- creates new nodes and edges

convMaps <- readIORef convRef

newConvMaps <- convertNodes convMaps gid actginfo dgraph ln

finalConvMaps <- convertEdges newConvMaps gid actginfo dgraph ln

-- writes the ConversionMap and redisplays the graph

writeIORef convRef finalConvMaps

redisplay gid actginfo

return ()

hideShowNames :: GInfo -> IO ()

hideShowNames (GInfo {graphId = gid,

gi_GraphInfo = actGraphInfo,

internalNamesIORef = showInternalNames

}) = do

(intrn::InternalNames) <- readIORef showInternalNames

let showThem = not $ showNames intrn

showItrn s = if showThem then s else ""

mapM_ (\(s,upd) -> upd (\_ -> showItrn s)) $ updater intrn

writeIORef showInternalNames $ intrn {showNames = showThem}

redisplay gid actGraphInfo

return ()

showNodes :: GInfo -> IO ()

showNodes (GInfo {descrIORef = event,

graphId = gid,

gi_GraphInfo = actGraphInfo

}) = do

descr <- readIORef event

showIt gid descr actGraphInfo

redisplay gid actGraphInfo

return ()

translateGraph :: GInfo -> ConvFunc -> LibFunc -> IO ()

translateGraph (GInfo {libEnvIORef = ioRefProofStatus,

gi_LIB_NAME = ln,

gi_hetcatsOpts = opts

}) convGraph showLib = do

le <- readIORef ioRefProofStatus

openTranslateGraph le ln opts (getDGLogic le) convGraph showLib

showLibGraph :: GInfo -> LibFunc -> IO ()

showLibGraph gInfo showLib = do

showLib gInfo

return ()

performProofAction :: GInfo -> IO () -> IO ()

performProofAction gInfo@(GInfo {descrIORef = event,

graphId = gid,

gi_GraphInfo = actGraphInfo

}) proofAction = do

descr <- readIORef event

AGV.Result _ errorMsg <- checkHasHiddenNodes gid descr actGraphInfo

case errorMsg of

Nothing -> do

showNodes gInfo

proofAction

hideNodes gInfo True

Just _ -> proofAction

saveProofStatus :: GInfo -> FilePath -> IO ()

saveProofStatus (GInfo {libEnvIORef = ioRefProofStatus,

gi_LIB_NAME = ln,

gi_hetcatsOpts = opts

}) file = encapsulateWaitTermAct $ do

proofStatus <- readIORef ioRefProofStatus

writeShATermFile file (ln, lookupHistory ln proofStatus)

putIfVerbose opts 2 $ "Wrote " ++ file

-- | implementation of open menu, read in a proof status

openProofStatus :: GInfo -> FilePath -> ConvFunc -> LibFunc

-> IO (Descr, GraphInfo, ConversionMaps)

openProofStatus (GInfo {libEnvIORef = ioRefProofStatus,

conversionMapsIORef = convRef,

gi_LIB_NAME = ln,

gi_hetcatsOpts = opts

}) file convGraph showLib = do

mh <- readVerbose opts ln file

case mh of

Nothing -> fail

$ "Could not read proof status from file '"

++ file ++ "'"

Just h -> do

let libfile = libNameToFile opts ln

m <- anaLib opts { outtypes = [] } libfile

case m of

Nothing -> fail

$ "Could not read original development graph from '"

++ libfile ++ "'"

Just (_, libEnv) -> case Map.lookup ln libEnv of

Nothing -> fail

$ "Could not get original development graph for '"

++ showDoc ln "'"

Just gctx -> do

oldEnv <- readIORef ioRefProofStatus

let proofStatus = Map.insert ln

(applyProofHistory h gctx) oldEnv

writeIORef ioRefProofStatus proofStatus

gInfo <- emptyGInfo

gInfo' <- setGInfo gInfo ln proofStatus opts

(gid, actGraphInfo, convMaps) <-

convGraph gInfo' "Proof Status " showLib

writeIORef convRef convMaps

redisplay gid actGraphInfo

return (gid, actGraphInfo, convMaps)

-- | apply a rule of the development graph calculus

proofMenu :: GInfo

-> (LibEnv -> IO (Res.Result LibEnv))

-> IO ()

proofMenu (GInfo {libEnvIORef = ioRefProofStatus,

descrIORef = event,

conversionMapsIORef = convRef,

graphId = gid,

gi_LIB_NAME = ln,

gi_GraphInfo = actGraphInfo,

gi_hetcatsOpts = hOpts,

proofGUIMVar = guiMVar,

visibleNodesIORef = ioRefVisibleNodes}) proofFun = do

filled <- tryPutMVar guiMVar Nothing

if not filled

then readMVar guiMVar >>=

(maybe (putIfVerbose hOpts 4 "proofMenu: ignored Nothing")

(\ w -> do

putIfVerbose hOpts 4 $

"proofMenu: Ignored Proof command; " ++

"maybe a proof window is still open?"

HTk.putWinOnTop w))

else do

proofStatus <- readIORef ioRefProofStatus

putIfVerbose hOpts 4 "Proof started via \"Proofs\" menu"

Res.Result ds res <- proofFun proofStatus

putIfVerbose hOpts 4 "Analyzing result of proof"

case res of

Nothing -> mapM_ (putStrLn . show) ds

Just newProofStatus -> do

let newGlobContext = lookupGlobalContext ln newProofStatus

history = proofHistory newGlobContext

writeIORef ioRefProofStatus newProofStatus

descr <- readIORef event

convMaps <- readIORef convRef

(newDescr,convMapsAux)

<- applyChanges gid ln actGraphInfo descr ioRefVisibleNodes

convMaps history

writeIORef ioRefProofStatus $

Map.insert ln newGlobContext newProofStatus

writeIORef event newDescr

writeIORef convRef convMapsAux

redisplay gid actGraphInfo

mGUIMVar <- tryTakeMVar guiMVar

maybe (fail $ "should be filled with Nothing after "++

"proof attempt")

(const $ return ())

mGUIMVar

nodeErr :: Descr -> IO ()

nodeErr descr = error $ "node with descriptor " ++ show descr

++ " has no corresponding node in the development graph"

showSpec :: Descr -> DGraphAndAGraphNode -> DGraph -> IO ()

showSpec descr dgAndabstrNodeMap dgraph =

case InjMap.lookupWithB descr dgAndabstrNodeMap of

Nothing -> return ()

Just (_, node) -> do

let sp = dgToSpec dgraph node

putStrLn $ case sp of

Res.Result ds Nothing -> show $ vcat $ map pretty ds

Res.Result _ m -> showDoc m ""

hideNodes :: GInfo -> Bool -> IO ()

hideNodes (GInfo {descrIORef = event,

graphId = gid,

gi_GraphInfo = actGraphInfo

}) showLast = do

AGV.Result descr msg <- hideSetOfNodeTypes gid

["open_cons__internal",

"locallyEmpty__open_cons__internal",

"proven_cons__internal",

"locallyEmpty__proven_cons__internal"]

showLast actGraphInfo

writeIORef event descr

case msg of

Nothing -> do redisplay gid actGraphInfo

return ()

Just err -> putStrLn err

return ()

{- | auxiliary method for debugging. shows the number of the given node

in the abstraction graph -}

getNumberOfNode :: Descr -> IO()

getNumberOfNode descr =

let title = "Number of node"

-- make the node number consistent

in createTextDisplay title (showDoc (descr-1) "") [HTk.size(10,10)]

{- | outputs the signature of a node in a window;

used by the node menu defined in initializeGraph -}

getSignatureOfNode :: Descr -> DGraphAndAGraphNode -> DGraph -> IO()

getSignatureOfNode descr dgAndabstrNodeMap dgraph =

case InjMap.lookupWithB descr dgAndabstrNodeMap of

Just (_, node) ->

let dgnode = lab' (contextDG dgraph node)

title = "Signature of "++showName (dgn_name dgnode)

in createTextDisplay title (showDoc (dgn_sign dgnode) "")

[HTk.size(80,50)]

Nothing -> nodeErr descr

{- |

fetches the theory from a node inside the IO Monad

(added by KL based on code in getTheoryOfNode) -}

lookupTheoryOfNode :: IORef LibEnv -> Descr -> DGraphAndAGraphNode ->

DGraph -> IO (Res.Result (Node,G_theory))

lookupTheoryOfNode proofStatusRef descr dgAndabstrNodeMap _ = do

libEnv <- readIORef proofStatusRef

case (do

(ln, node) <-

maybeToResult nullRange ("Node "++show descr++" not found")

$ InjMap.lookupWithB descr dgAndabstrNodeMap

gth <- computeTheory libEnv ln node

return (node, gth)

) of

r -> do

return r

{- | outputs the local axioms of a node in a window;

used by the node menu defined in initializeGraph-}

getLocalAxOfNode :: GInfo -> Descr -> DGraphAndAGraphNode -> DGraph -> IO ()

getLocalAxOfNode _ descr dgAndabstrNodeMap dgraph = do

case InjMap.lookupWithB descr dgAndabstrNodeMap of

Just (_, node) ->

do let dgnode = lab' (contextDG dgraph node)

case dgnode of

DGNode _ gth _ _ _ _ _ ->

displayTheory "Local Axioms" node dgraph gth

DGRef name _ _ _ _ _ ->

createTextDisplay ("Local Axioms of "++ showName name)

"no local axioms (reference node to other library)"

[HTk.size(30,10)]

Nothing -> nodeErr descr

{- | outputs the theory of a node in a window;

used by the node menu defined in initializeGraph-}

getTheoryOfNode :: GInfo -> Descr -> DGraphAndAGraphNode -> DGraph -> IO ()

getTheoryOfNode gInfo descr dgAndabstrNodeMap dgraph = do

r <- lookupTheoryOfNode (libEnvIORef gInfo) descr dgAndabstrNodeMap dgraph

case r of

Res.Result ds res -> do

showDiags (gi_hetcatsOpts gInfo) ds

case res of

(Just (n, gth)) ->

GUI.HTkUtils.displayTheoryWithWarning

"Theory"

(showName $ dgn_name $ lab' (contextDG dgraph n))

(addHasInHidingWarning dgraph n)

gth

_ -> return ()

displayTheory :: String -> Node -> DGraph -> G_theory -> IO ()

displayTheory ext node dgraph gth =

GUI.HTkUtils.displayTheory ext

(showName $ dgn_name $ lab' (contextDG dgraph node))

gth

{- | translate the theory of a node in a window;

used by the node menu defined in initializeGraph-}

translateTheoryOfNode :: GInfo -> Descr -> DGraphAndAGraphNode -> DGraph

-> IO ()

translateTheoryOfNode gInfo@(GInfo {gi_hetcatsOpts = opts})

descr dgAndabstrNodeMap dgraph = do

libEnv <- readIORef $ libEnvIORef gInfo

case (do

(ln, node) <-

maybeToResult nullRange ("Node "++show descr++" not found")

$ InjMap.lookupWithB descr dgAndabstrNodeMap

th <- computeTheory libEnv ln node

return (node,th) ) of

Res.Result [] (Just (node,th)) -> do

Res.Result ds _ <- runResultT(

do G_theory lid sign _ sens _ <- return th

-- find all comorphism paths starting from lid

let paths = findComorphismPaths logicGraph (sublogicOfTh th)

-- let the user choose one

sel <- lift $ listBox "Choose a logic translation"

(map show paths)

i <- case sel of

Just j -> return j

_ -> liftR $ fail "no logic translation chosen"

Comorphism cid <- return (paths!!i)

-- adjust lid's

let lidS = sourceLogic cid

lidT = targetLogic cid

sign' <- coerceSign lid lidS "" sign

sens' <- coerceThSens lid lidS "" sens

-- translate theory along chosen comorphism

(sign'',sens1) <-

liftR $ wrapMapTheory cid (sign', toNamedList sens')

lift $ GUI.HTkUtils.displayTheoryWithWarning

"Translated Theory"

(showName $ dgn_name $ lab' (contextDG dgraph node))

(addHasInHidingWarning dgraph node)

(G_theory lidT sign'' 0 (toThSens sens1) 0)

)

showDiags opts ds

return ()

Res.Result ds _ -> showDiags opts ds

{- | outputs the sublogic of a node in a window;

used by the node menu defined in initializeGraph -}

getSublogicOfNode :: IORef LibEnv -> Descr -> DGraphAndAGraphNode

-> DGraph -> IO()

getSublogicOfNode proofStatusRef descr dgAndabstrNodeMap dgraph = do

libEnv <- readIORef proofStatusRef

case InjMap.lookupWithB descr dgAndabstrNodeMap of

Just (ln, node) ->

let dgnode = lab' (contextDG dgraph node)

name = case dgnode of

(DGNode nname _ _ _ _ _ _) -> nname

_ -> emptyNodeName

in case computeTheory libEnv ln node of

Res.Result _ (Just th) ->

let logstr = show $ sublogicOfTh th

title = "Sublogic of "++showName name

in createTextDisplay title logstr [HTk.size(30,10)]

Res.Result ds _ ->

error $ "Could not compute theory for sublogic computation: "

++ concatMap show ds

Nothing -> nodeErr descr

-- | prints the origin of the node

showOriginOfNode :: Descr -> DGraphAndAGraphNode -> DGraph -> IO()

showOriginOfNode descr dgAndabstrNodeMap dgraph =

case InjMap.lookupWithB descr dgAndabstrNodeMap of

Just (_, node) ->

do let dgnode = lab' (contextDG dgraph node)

case dgnode of

DGNode name _ _ _ orig _ _ ->

let title = "Origin of node "++showName name

in createTextDisplay title

(showDoc orig "") [HTk.size(30,10)]

DGRef _ _ _ _ _ _ -> error "showOriginOfNode: no DGNode"

Nothing -> nodeErr descr

-- | Show proof status of a node

showProofStatusOfNode :: GInfo -> Descr -> DGraphAndAGraphNode -> DGraph

-> IO ()

showProofStatusOfNode _ descr dgAndabstrNodeMap dgraph =

case InjMap.lookupWithB descr dgAndabstrNodeMap of

Just (_, node) ->

do let dgnode = lab' (contextDG dgraph node)

let stat = showStatusAux dgnode

let title = "Proof status of node "++showName (dgn_name dgnode)

createTextDisplay title stat [HTk.size(105,55)]

Nothing -> nodeErr descr

showStatusAux :: DGNodeLab -> String

showStatusAux dgnode =

case dgn_theory dgnode of

G_theory _ _ _ sens _ ->

let goals = OMap.filter (not . isAxiom) sens

(proven,open) = OMap.partition isProvenSenStatus goals

in "Proven proof goals:\n"

++ showDoc proven ""

++ if not $ hasOpenConsStatus True dgnode

then showDoc (dgn_cons_status dgnode)

"is the conservativity status of this node"

else ""

++ "\nOpen proof goals:\n"

++ showDoc open ""

++ if hasOpenConsStatus False dgnode

then showDoc (dgn_cons_status dgnode)

"should be the conservativity status of this node"

else ""

-- | start local theorem proving or consistency checking at a node

proveAtNode :: Bool -> GInfo -> Descr -> DGraphAndAGraphNode -> DGraph -> IO ()

proveAtNode checkCons

gInfo@(GInfo {gi_LIB_NAME = ln, proofGUIMVar = guiMVar})

descr

dgAndabstrNodeMap

dgraph =

case InjMap.lookupWithB descr dgAndabstrNodeMap of

Just libNode -> if (checkCons

|| not (hasIncomingHidingEdge dgraph $ snd libNode))

then

proofMenu gInfo (basicInferenceNode checkCons

logicGraph libNode ln guiMVar)

else

GUI.HTkUtils.createInfoDisplayWithTwoButtons

"Warning"

"This node has incoming hiding links!!!"

"Prove anyway"

(proofMenu gInfo (basicInferenceNode checkCons

logicGraph libNode ln guiMVar))

Nothing -> nodeErr descr

-- | print the id of the edge

showIDOfEdge :: Descr -> Maybe (LEdge DGLinkLab) -> IO ()

showIDOfEdge _ (Just (_, _, linklab)) =

createTextDisplay "ID of Edge" (show $ dgl_id linklab) [HTk.size(30,10)]

showIDOfEdge descr Nothing =

createTextDisplay "Error"

("edge " ++ show descr ++ " has no corresponding edge"

++ "in the development graph") [HTk.size(30,10)]

-- | print the morphism of the edge

showMorphismOfEdge :: Descr -> Maybe (LEdge DGLinkLab) -> IO ()

showMorphismOfEdge _ (Just (_,_,linklab)) =

createTextDisplay "Signature morphism"

(showDoc (dgl_morphism linklab) "" ++ hidingMorph)

[HTk.size(100,40)]

where

hidingMorph = case dgl_type linklab of

HidingThm morph _ -> "\n ++++++ \n"

++ showDoc morph ""

_ -> ""

showMorphismOfEdge descr Nothing =

createTextDisplay "Error"

("edge " ++ show descr ++ " has no corresponding edge"

++ "in the development graph") [HTk.size(30,10)]

-- | print the origin of the edge

showOriginOfEdge :: Descr -> Maybe (LEdge DGLinkLab) -> IO ()

showOriginOfEdge _ (Just (_,_,linklab)) =

createTextDisplay "Origin of link"

(showDoc (dgl_origin linklab) "") [HTk.size(30,10)]

showOriginOfEdge descr Nothing =

createTextDisplay "Error"

("edge " ++ show descr ++ " has no corresponding edge"

++ "in the development graph") [HTk.size(30,10)]

-- | print the proof base of the edge

showProofStatusOfThm :: Descr -> Maybe (LEdge DGLinkLab) -> IO ()

showProofStatusOfThm _ (Just ledge) =

createTextSaveDisplay "Proof Status" "proofstatus.txt"

(showDoc (getProofStatusOfThm ledge) "\n")

showProofStatusOfThm descr Nothing =

-- why putStrLn here and no createTextDisplay elsewhere with this message

putStrLn ("edge " ++ show descr ++ " has no corresponding edge"

++ "in the development graph")

-- | check conservativity of the edge

checkconservativityOfEdge :: Descr -> GInfo -> Maybe (LEdge DGLinkLab) -> IO()

checkconservativityOfEdge _ gInfo

(Just (source,target,linklab)) = do

libEnv <- readIORef $ libEnvIORef gInfo

let dgraph = lookupDGraph (gi_LIB_NAME gInfo) libEnv

dgtar = lab' (contextDG dgraph target)

case dgtar of

DGNode _ (G_theory lid _ _ sens _) _ _ _ _ _ ->

case dgl_morphism linklab of

GMorphism cid _ _ morphism2 _ -> do

morphism2' <- coerceMorphism (targetLogic cid) lid

"checkconservativityOfEdge" morphism2

let th = case computeTheory libEnv (gi_LIB_NAME gInfo) source of

Res.Result _ (Just th1) -> th1

_ -> error "checkconservativityOfEdge: computeTheory"

G_theory lid1 sign1 _ sens1 _ <- return th

sign2 <- coerceSign lid1 lid "checkconservativityOfEdge.coerceSign" sign1

sens2 <- coerceThSens lid1 lid "" sens1

let Res.Result ds res =

conservativityCheck lid (sign2, toNamedList sens2)

morphism2' $ toNamedList sens

showRes = case res of

Just(Just True) -> "The link is conservative"

Just(Just False) -> "The link is not conservative"

_ -> "Could not determine whether link is conservative"

myDiags = unlines (map show ds)

createTextDisplay "Result of conservativity check"

(showRes ++ "\n" ++ myDiags) [HTk.size(50,50)]

DGRef _ _ _ _ _ _ -> error "checkconservativityOfEdge: no DGNode"

checkconservativityOfEdge descr _ Nothing =

createTextDisplay "Error"

("edge " ++ show descr ++ " has no corresponding edge "

++ "in the development graph") [HTk.size(30,10)]

getProofStatusOfThm :: (LEdge DGLinkLab) -> ThmLinkStatus

getProofStatusOfThm (_,_,label) =

case (dgl_type label) of

(LocalThm proofStatus _ _) -> proofStatus

(GlobalThm proofStatus _ _) -> proofStatus

(HidingThm _ proofStatus) -> proofStatus -- richtig?

_ -> error "the given edge is not a theorem"

{- | converts the nodes of the development graph, if it has any,

and returns the resulting conversion maps

if the graph is empty the conversion maps are returned unchanged-}

convertNodes :: ConversionMaps -> Descr -> GraphInfo -> DGraph

-> LIB_NAME -> IO ConversionMaps

convertNodes convMaps descr grInfo dgraph libname

| isEmptyDG dgraph = return convMaps

| otherwise = convertNodesAux convMaps

descr

grInfo

(labNodesDG dgraph)

libname

{- | auxiliary function for convertNodes if the given list of nodes is

emtpy, it returns the conversion maps unchanged otherwise it adds the

converted first node to the abstract graph and to the affected

conversion maps and afterwards calls itself with the remaining node

list -}

convertNodesAux :: ConversionMaps -> Descr -> GraphInfo ->

[LNode DGNodeLab] -> LIB_NAME -> IO ConversionMaps

convertNodesAux convMaps _ _ [] _ = return convMaps

convertNodesAux convMaps descr grInfo ((node,dgnode) : lNodes) libname =

do let nodetype = getDGNodeType dgnode

AGV.Result newDescr _ <- addnode descr

nodetype

(getDGNodeName dgnode)

grInfo

convertNodesAux convMaps

{ dgAndabstrNode = InjMap.insert (libname, node) newDescr

(dgAndabstrNode convMaps)

} descr grInfo lNodes libname

{- | converts the edges of the development graph

works the same way as convertNods does-}

convertEdges :: ConversionMaps -> Descr -> GraphInfo -> DGraph

-> LIB_NAME -> IO ConversionMaps

convertEdges convMaps descr grInfo dgraph libname

| isEmptyDG dgraph = return convMaps

| otherwise = convertEdgesAux convMaps

descr

grInfo

(labEdgesDG dgraph)

libname

-- | auxiliary function for convertEges

convertEdgesAux :: ConversionMaps -> Descr -> GraphInfo ->

[LEdge DGLinkLab] -> LIB_NAME -> IO ConversionMaps

convertEdgesAux convMaps _ _ [] _ = return convMaps

convertEdgesAux convMaps descr grInfo (ledge@(src,tar,edgelab) : lEdges)

libname =

do let srcnode = InjMap.lookupWithA (libname,src) (dgAndabstrNode convMaps)

tarnode = InjMap.lookupWithA (libname,tar) (dgAndabstrNode convMaps)

case (srcnode, tarnode) of

(Just s, Just t) -> do

AGV.Result newDescr msg <- addlink descr (getDGLinkType edgelab)

"" (Just ledge) s t grInfo

case msg of

Nothing -> return ()

Just err -> fail err

newConvMaps <- convertEdgesAux convMaps

{ dgAndabstrEdge = InjMap.insert (libname,

(src, tar, showDoc edgelab ""))

newDescr (dgAndabstrEdge convMaps)

} descr grInfo lEdges libname

return newConvMaps

_ -> error "Cannot find nodes"

-- | show library referened by a DGRef node (=node drawn as a box)

showReferencedLibrary :: Descr -> GInfo -> ConvFunc -> LibFunc

-> IO (Descr, GraphInfo, ConversionMaps)

showReferencedLibrary

descr gInfo@(GInfo {libEnvIORef = ioRefProofStatus,

conversionMapsIORef = convRef,

gi_GraphInfo = actGraphInfo,

gi_hetcatsOpts = opts}) convGraph

showLib = do

convMaps <- readIORef convRef

libname2dgMap <- readIORef ioRefProofStatus

case InjMap.lookupWithB descr (dgAndabstrNode convMaps) of

Just (libname,node) ->

case Map.lookup libname libname2dgMap of

Just gctx ->

do let dgraph = devGraph gctx

(_,(DGRef _ refLibname _ _ _ _)) =

labNode' (contextDG dgraph node)

case Map.lookup refLibname libname2dgMap of

Just _ -> do

(_,next) <- readIORef actGraphInfo

let gInfo' = gInfo {graphId = next}

gInfo'' <- setGInfo gInfo' refLibname libname2dgMap opts

convGraph gInfo'' "development graph" showLib

Nothing -> error $ "The referenced library ("

++ show refLibname

++ ") is unknown"

Nothing -> error $ "Selected node belongs to unknown library: "

++ show libname

Nothing ->

error $ "there is no node with the descriptor " ++ show descr

-- | prune displayed graph to subtree of selected node

showJustSubtree :: Descr -> Descr -> GInfo

-> IO (Descr, [[Node]], Maybe String)

showJustSubtree descr abstractGraph

(GInfo {libEnvIORef = ioRefProofStatus,

conversionMapsIORef = convRef,

visibleNodesIORef = visibleNodesRef,

gi_GraphInfo = actGraphInfo}) = do

convMaps <- readIORef convRef

libname2dgMap <- readIORef ioRefProofStatus

visibleNodes <- readIORef visibleNodesRef

case InjMap.lookupWithB descr (dgAndabstrNode convMaps) of

Just (libname,parentNode) ->

case Map.lookup libname libname2dgMap of

Just gctx ->

do let dgraph = devGraph gctx

allNodes = getNodeDescriptors (head visibleNodes)

libname convMaps

dgNodesOfSubtree = nub (parentNode:(getNodesOfSubtree dgraph

(head visibleNodes) parentNode))

-- the selected node (parentNode) shall not be hidden either,

-- and we already know its descriptor (descr)

nodesOfSubtree = getNodeDescriptors dgNodesOfSubtree

libname convMaps

nodesToHide = filter (`notElem` nodesOfSubtree) allNodes

AGV.Result eventDescr errorMsg <- hidenodes abstractGraph

nodesToHide actGraphInfo

return (eventDescr, (dgNodesOfSubtree:visibleNodes), errorMsg)

Nothing -> error $

"showJustSubtree: Selected node belongs to unknown library: "

++ show libname

Nothing -> error $ "showJustSubtree: there is no node with the descriptor "

++ show descr

getNodeDescriptors :: [Node] -> LIB_NAME -> ConversionMaps -> [Descr]

getNodeDescriptors [] _ _ = []

getNodeDescriptors (node:nodelist) libname convMaps =

case InjMap.lookupWithA (libname, node) (dgAndabstrNode convMaps) of

Just descr -> descr:(getNodeDescriptors nodelist libname convMaps)

Nothing -> error $ "getNodeDescriptors: There is no descriptor for dgnode "

++ show node

getNodesOfSubtree :: DGraph -> [Node] -> Node -> [Node]

getNodesOfSubtree dgraph visibleNodes node =

concat (map (getNodesOfSubtree dgraph remainingVisibleNodes) predOfNode)

++ predOfNode

where predOfNode = [ n | n <- (preDG dgraph node), elem n visibleNodes]

remainingVisibleNodes =

[ n | n <- visibleNodes, notElem n predOfNode]

-- | apply the changes of first history item (computed by proof rules,

-- see folder Proofs) to the displayed development graph

applyChanges :: Descr -> LIB_NAME -> GraphInfo -> Descr -> IORef [[Node]]

-> ConversionMaps -> [([DGRule],[DGChange])]

-> IO (Descr, ConversionMaps)

applyChanges _ _ _ eventDescr _ convMaps [] = return (eventDescr,convMaps)

applyChanges gid libname grInfo eventDescr ioRefVisibleNodes

convMaps ((_, historyElem) : _) =

applyChangesAux gid libname grInfo ioRefVisibleNodes

(eventDescr, convMaps) $ removeContraryChanges historyElem

-- | auxiliary function for applyChanges

applyChangesAux :: Descr -> LIB_NAME -> GraphInfo -> IORef [[Node]]

-> (Descr, ConversionMaps) -> [DGChange]

-> IO (Descr, ConversionMaps)

applyChangesAux gid libname grInfo ioRefVisibleNodes

(eventDescr, convMaps) changeList =

case changeList of

[] -> return (eventDescr, convMaps)

changes@(_:_) -> do

visibleNodes <- readIORef ioRefVisibleNodes

(newVisibleNodes, newEventDescr, newConvMaps) <-

applyChangesAux2 gid libname grInfo visibleNodes

eventDescr convMaps changes

writeIORef ioRefVisibleNodes newVisibleNodes

return (newEventDescr, newConvMaps)

-- | auxiliary function for applyChanges

applyChangesAux2 :: Descr -> LIB_NAME -> GraphInfo -> [[Node]] -> Descr

-> ConversionMaps -> [DGChange]

-> IO ([[Node]], Descr, ConversionMaps)

applyChangesAux2 _ _ _ visibleNodes eventDescr convMaps [] =

return (visibleNodes, eventDescr+1, convMaps)

applyChangesAux2 gid libname grInfo visibleNodes _ convMaps (change:changes) =

case change of

SetNodeLab _ (node, newLab) -> do

let nodetype = getDGNodeType newLab

nodename = getDGNodeName newLab

dgNode = (libname, node)

case InjMap.lookupWithA dgNode (dgAndabstrNode convMaps) of

Just abstrNode -> do

AGV.Result descr err <-

changeNodeType gid abstrNode nodetype grInfo

case err of

Nothing -> do

let newConvMaps = convMaps

{ dgAndabstrNode = InjMap.updateBWithA dgNode

descr (dgAndabstrNode convMaps) }

applyChangesAux2 gid libname grInfo visibleNodes

(descr+1) newConvMaps changes

Just msg ->

error $ "applyChangesAux2: could not set node "

++ show node ++" with name "

++ show nodename ++ "\n" ++ msg

Nothing -> error $ "applyChangesAux2: could not set node "

++ show node ++ " with name "

++ show nodename ++ ": " ++

"node does not exist in abstraction graph"

InsertNode (node, nodelab) -> do

let nodetype = getDGNodeType nodelab

nodename = getDGNodeName nodelab

AGV.Result descr err <-

addnode gid nodetype nodename grInfo

case err of

Nothing ->

do let dgNode = (libname,node)

newVisibleNodes = map (node :) visibleNodes

newConvMaps = convMaps

{ dgAndabstrNode = InjMap.insert dgNode descr

(dgAndabstrNode convMaps) }

applyChangesAux2 gid libname grInfo newVisibleNodes (descr+1)

newConvMaps changes

Just msg ->

error $ "applyChangesAux2: could not add node " ++ show node

++" with name " ++ show nodename ++ "\n" ++ msg

DeleteNode (node, nodelab) -> do

let nodename = getDGNodeName nodelab

dgnode = (libname,node)

case InjMap.lookupWithA dgnode (dgAndabstrNode convMaps) of

Just abstrNode -> do

AGV.Result descr err <- delnode gid abstrNode grInfo

case err of

Nothing -> do

let newVisibleNodes = map (filter (/= node)) visibleNodes

newConvMaps = convMaps

{ dgAndabstrNode = InjMap.delete dgnode abstrNode

(dgAndabstrNode convMaps) }

applyChangesAux2 gid libname grInfo newVisibleNodes (descr+1)

newConvMaps changes

Just msg -> error $ "applyChangesAux2: could not delete node "

++ show node ++ " with name "

++ show nodename ++ "\n" ++ msg

Nothing -> error $ "applyChangesAux2: could not delete node "

++ show node ++ " with name "

++ show nodename ++": " ++

"node does not exist in abstraction graph"

InsertEdge ledge@(src,tgt,edgelab) ->

do let dgAndabstrNodeMap = dgAndabstrNode convMaps

case (InjMap.lookupWithA (libname, src) dgAndabstrNodeMap,

InjMap.lookupWithA (libname, tgt) dgAndabstrNodeMap) of

(Just abstrSrc, Just abstrTgt) ->

do let dgEdge = (libname, (src,tgt,showDoc edgelab ""))

AGV.Result descr err <-

addlink gid (getDGLinkType edgelab)

"" (Just ledge) abstrSrc abstrTgt grInfo

case err of

Nothing ->

do let newConvMaps = convMaps

{ dgAndabstrEdge = InjMap.insert dgEdge descr

(dgAndabstrEdge convMaps) }

applyChangesAux2 gid libname grInfo visibleNodes

(descr + 1) newConvMaps changes

Just msg ->

error $ "applyChangesAux2: could not add link from "

++ show src ++ " to " ++ show tgt ++ ":\n"

++ show msg

_ -> error $ "applyChangesAux2: could not add link " ++ show src

++ " to " ++ show tgt ++ ": illegal end nodes"

DeleteEdge (src,tgt,edgelab) ->

do let dgEdge = (libname, (src,tgt,showDoc edgelab ""))

dgAndabstrEdgeMap = dgAndabstrEdge convMaps

case (InjMap.lookupWithA dgEdge dgAndabstrEdgeMap) of

Just abstrEdge ->

do AGV.Result descr err <- dellink gid abstrEdge grInfo

case err of

Nothing ->

do let newConvMaps = convMaps

{ dgAndabstrEdge = InjMap.delete dgEdge

abstrEdge (dgAndabstrEdge convMaps) }

applyChangesAux2 gid libname grInfo visibleNodes

(descr + 1) newConvMaps changes

Just msg -> error $

"applyChangesAux2: could not delete edge "

++ shows abstrEdge ":\n" ++ msg

Nothing -> error $ "applyChangesAux2: deleted edge from "

++ shows src " to " ++ shows tgt

" of type " ++ showDoc (dgl_type edgelab)

" and origin " ++ shows (dgl_origin edgelab)

" of development "

++ "graph does not exist in abstraction graph"

-- | display a window of translated graph with maximal sublogic.

openTranslateGraph :: LibEnv -> LIB_NAME -> HetcatsOpts

-> Res.Result G_sublogics -> ConvFunc -> LibFunc -> IO ()

openTranslateGraph libEnv ln opts (Res.Result diagsSl mSublogic) convGraph

showLib =

-- if an error existed by the search of maximal sublogicn

-- (see GUI.DGTranslation.getDGLogic), the process need not to go on.

if hasErrors diagsSl then

errorMess $ unlines $ map show

$ filter (relevantDiagKind . diagKind) diagsSl

else

do case mSublogic of

Just sublogic -> do

let paths = findComorphismPaths logicGraph sublogic

if null paths then

errorMess "This graph has no comorphism to translation."

else do

Res.Result diagsR i <- runResultT ( do

-- the user choose one

sel <- lift $ listBox "Choose a logic translation"

(map show paths)

case sel of

Just j -> return j

_ -> liftR $ fail "no logic translation chosen")

let aComor = paths !! fromJust i

-- graph translation.

case libEnv_translation libEnv aComor of

Res.Result diagsTrans (Just newLibEnv) -> do

showDiags opts (diagsSl ++ diagsR ++ diagsTrans)

if hasErrors (diagsR ++ diagsTrans) then

errorMess $ unlines $ map show

$ filter (relevantDiagKind . diagKind)

$ diagsR ++ diagsTrans

else dg_showGraphAux

(\gI -> do

gInfo <- setGInfo gI ln newLibEnv opts

convGraph gInfo "translation Graph"

showLib)

Res.Result diagsTrans Nothing ->

errorMess $ unlines $ map show

$ filter (relevantDiagKind . diagKind)

$ diagsSl ++ diagsR ++ diagsTrans

Nothing -> errorMess "the maximal sublogic is not found."

where relevantDiagKind Error = True

relevantDiagKind Warning = verbose opts >= 2

relevantDiagKind Hint = verbose opts >= 4

relevantDiagKind Debug = verbose opts >= 5

relevantDiagKind MessageW = False

dg_showGraphAux :: (GInfo -> IO (Descr, GraphInfo, ConversionMaps)) -> IO ()

dg_showGraphAux convFct = do

useHTk -- All messages are displayed in TK dialog windows

-- from this point on

gInfo <- emptyGInfo

(gid, gv, _cmaps) <- convFct gInfo

redisplay gid gv

return ()