0N/A{-|

2362N/A

0N/AModule : $Header$

0N/ACopyright : (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2004

0N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

0N/A

2362N/AMaintainer : jfgerken@tzi.de

0N/AStability : provisional

2362N/APortability : non-portable(Logic)

0N/A

0N/Adata types for proofs in development graphs.

0N/A

0N/A-}

0N/A

0N/Amodule Proofs.Proofs where

0N/A

0N/Aimport Static.DevGraph

0N/Aimport Data.Graph.Inductive.Graph

0N/Aimport qualified Common.Lib.Map as Map

0N/Aimport Syntax.AS_Library

2362N/A

2362N/A{-

2362N/A proof status = (DG0,[(R1,DG1),...,(Rn,DGn)])

0N/A DG0 is the development graph resulting from the static analysis

0N/A Ri is a list of rules that transforms DGi-1 to DGi

0N/A With the list of intermediate proof states, one can easily implement

0N/A an undo operation

0N/A-}

0N/A

0N/A{-type ProofStatus = (GlobalContext,LibEnv,[([DGRule],[DGChange])],DGraph)

0N/Aumstellen auf:-}

0N/A

0N/Atype ProofHistory = [([DGRule],[DGChange])]

0N/Atype ProofStatus = (LIB_NAME,LibEnv,Map.Map LIB_NAME ProofHistory)

0N/A

0N/Adata DGChange = InsertNode (LNode DGNodeLab)

0N/A | DeleteNode (LNode DGNodeLab)

0N/A | InsertEdge (LEdge DGLinkLab)

0N/A | DeleteEdge (LEdge DGLinkLab)

0N/A deriving (Eq,Show)