DevGraph.hs revision be5ff99194b2ba0a1a35093e0ea21d4da332b526
074e084f68dd0b08686612bec695a0cfe249da6dml{-# LANGUAGE RankNTypes #-}
074e084f68dd0b08686612bec695a0cfe249da6dmlModule : $Header$
074e084f68dd0b08686612bec695a0cfe249da6dmlDescription : Central datastructures for development graphs
074e084f68dd0b08686612bec695a0cfe249da6dmlCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006
074e084f68dd0b08686612bec695a0cfe249da6dmlLicense : GPLv2 or higher, see LICENSE.txt
074e084f68dd0b08686612bec695a0cfe249da6dmlMaintainer : till@informatik.uni-bremen.de
074e084f68dd0b08686612bec695a0cfe249da6dmlStability : provisional
074e084f68dd0b08686612bec695a0cfe249da6dmlPortability : non-portable(Logic)
074e084f68dd0b08686612bec695a0cfe249da6dmlCentral datastructures for development graphs
074e084f68dd0b08686612bec695a0cfe249da6dml Follows Sect. IV:4.2 of the CASL Reference Manual.
074e084f68dd0b08686612bec695a0cfe249da6dmlWe also provide functions for constructing and modifying development graphs.
074e084f68dd0b08686612bec695a0cfe249da6dmlHowever note that these changes need to be propagated to the GUI if they
074e084f68dd0b08686612bec695a0cfe249da6dmlalso shall be visible in the displayed development graph.
074e084f68dd0b08686612bec695a0cfe249da6dml References:
074e084f68dd0b08686612bec695a0cfe249da6dml T. Mossakowski, S. Autexier and D. Hutter:
074e084f68dd0b08686612bec695a0cfe249da6dml Extending Development Graphs With Hiding.
074e084f68dd0b08686612bec695a0cfe249da6dml H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,
074e084f68dd0b08686612bec695a0cfe249da6dml Lecture Notes in Computer Science 2029, p. 269-283,
074e084f68dd0b08686612bec695a0cfe249da6dml Springer-Verlag 2001.
074e084f68dd0b08686612bec695a0cfe249da6dml T. Mossakowski, S. Autexier, D. Hutter, P. Hoffman:
074e084f68dd0b08686612bec695a0cfe249da6dml CASL Proof calculus. In: CASL reference manual, part IV.
074e084f68dd0b08686612bec695a0cfe249da6dml Available from http://www.cofi.info
074e084f68dd0b08686612bec695a0cfe249da6dmlimport qualified Static.XGraph as XGraph
074e084f68dd0b08686612bec695a0cfe249da6dmlimport qualified Common.Lib.Rel as Rel
074e084f68dd0b08686612bec695a0cfe249da6dmlimport qualified Common.Lib.Graph as Tree
074e084f68dd0b08686612bec695a0cfe249da6dmlimport qualified Common.Lib.SizedList as SizedList
074e084f68dd0b08686612bec695a0cfe249da6dmlimport qualified Common.OrderedMap as OMap
074e084f68dd0b08686612bec695a0cfe249da6dmlimport qualified Data.Map as Map
074e084f68dd0b08686612bec695a0cfe249da6dmlimport qualified Data.Set as Set
074e084f68dd0b08686612bec695a0cfe249da6dml-- * types for structured specification analysis
074e084f68dd0b08686612bec695a0cfe249da6dml-- ** basic types
074e084f68dd0b08686612bec695a0cfe249da6dml-- | Node with signature in a DG
074e084f68dd0b08686612bec695a0cfe249da6dmldata NodeSig = NodeSig { getNode :: Node, getSig :: G_sign }
074e084f68dd0b08686612bec695a0cfe249da6dml deriving (Eq, Show)
074e084f68dd0b08686612bec695a0cfe249da6dml{- | NodeSig or possibly the empty sig in a logic
074e084f68dd0b08686612bec695a0cfe249da6dml (but since we want to avoid lots of vsacuous nodes with empty sig,
074e084f68dd0b08686612bec695a0cfe249da6dml we do not assign a real node in the DG here) -}
074e084f68dd0b08686612bec695a0cfe249da6dmldata MaybeNode = JustNode NodeSig | EmptyNode AnyLogic deriving (Show, Eq)
074e084f68dd0b08686612bec695a0cfe249da6dml-- | a wrapper for renamings with a trivial Ord instance
074e084f68dd0b08686612bec695a0cfe249da6dmlnewtype Renamed = Renamed RENAMING deriving Show
074e084f68dd0b08686612bec695a0cfe249da6dmlinstance Ord Renamed where
074e084f68dd0b08686612bec695a0cfe249da6dml compare _ _ = EQ
074e084f68dd0b08686612bec695a0cfe249da6dmlinstance Eq Renamed where
074e084f68dd0b08686612bec695a0cfe249da6dml _ == _ = True
074e084f68dd0b08686612bec695a0cfe249da6dml-- | a wrapper for restrictions with a trivial Ord instance
074e084f68dd0b08686612bec695a0cfe249da6dmldata MaybeRestricted = NoRestriction | Restricted RESTRICTION deriving Show
074e084f68dd0b08686612bec695a0cfe249da6dmlinstance Ord MaybeRestricted where
074e084f68dd0b08686612bec695a0cfe249da6dml compare _ _ = EQ
074e084f68dd0b08686612bec695a0cfe249da6dmlinstance Eq MaybeRestricted where
074e084f68dd0b08686612bec695a0cfe249da6dml _ == _ = True
074e084f68dd0b08686612bec695a0cfe249da6dml{- | Data type indicating the origin of nodes and edges in the input language
074e084f68dd0b08686612bec695a0cfe249da6dml This is not used in the DG calculus, only may be used in the future
074e084f68dd0b08686612bec695a0cfe249da6dml for reconstruction of input and management of change. -}
074e084f68dd0b08686612bec695a0cfe249da6dmldata DGOrigin =
074e084f68dd0b08686612bec695a0cfe249da6dml | DGBasicSpec (Maybe G_basic_spec) G_sign (Set.Set G_symbol)
074e084f68dd0b08686612bec695a0cfe249da6dml | DGExtension
074e084f68dd0b08686612bec695a0cfe249da6dml | DGLogicCoercion
074e084f68dd0b08686612bec695a0cfe249da6dml | DGTranslation Renamed
074e084f68dd0b08686612bec695a0cfe249da6dml | DGRestriction (MaybeRestricted) (Set.Set G_symbol)
074e084f68dd0b08686612bec695a0cfe249da6dml | DGRevealTranslation
074e084f68dd0b08686612bec695a0cfe249da6dml | DGFreeOrCofree FreeOrCofree
074e084f68dd0b08686612bec695a0cfe249da6dml | DGClosed
074e084f68dd0b08686612bec695a0cfe249da6dml | DGLogicQual
074e084f68dd0b08686612bec695a0cfe249da6dml | DGFormalParams
074e084f68dd0b08686612bec695a0cfe249da6dml | DGImports
074e084f68dd0b08686612bec695a0cfe249da6dml | DGInst SIMPLE_ID
074e084f68dd0b08686612bec695a0cfe249da6dml | DGFitSpec
074e084f68dd0b08686612bec695a0cfe249da6dml | DGFitView SIMPLE_ID
074e084f68dd0b08686612bec695a0cfe249da6dml | DGNormalForm Node
074e084f68dd0b08686612bec695a0cfe249da6dml | DGintegratedSCC
074e084f68dd0b08686612bec695a0cfe249da6dml | DGFlattening
074e084f68dd0b08686612bec695a0cfe249da6dml deriving (Show, Eq, Ord)
074e084f68dd0b08686612bec695a0cfe249da6dml-- | node content or reference to another library's node
074e084f68dd0b08686612bec695a0cfe249da6dmldata DGNodeInfo = DGNode
074e084f68dd0b08686612bec695a0cfe249da6dml { node_origin :: DGOrigin -- origin in input language
074e084f68dd0b08686612bec695a0cfe249da6dml , node_cons_status :: ConsStatus } -- like a link from the empty signature
074e084f68dd0b08686612bec695a0cfe249da6dml | DGRef -- reference to node in a different DG
074e084f68dd0b08686612bec695a0cfe249da6dml { ref_libname :: LibName -- pointer to DG where ref'd node resides
074e084f68dd0b08686612bec695a0cfe249da6dml , ref_node :: Node -- pointer to ref'd node
074e084f68dd0b08686612bec695a0cfe249da6dml } deriving (Show, Eq)
074e084f68dd0b08686612bec695a0cfe249da6dml{- | node inscriptions in development graphs.
074e084f68dd0b08686612bec695a0cfe249da6dmlNothing entries indicate "not computed yet" -}
074e084f68dd0b08686612bec695a0cfe249da6dmldata DGNodeLab =
074e084f68dd0b08686612bec695a0cfe249da6dml { dgn_name :: NodeName -- name in the input language
074e084f68dd0b08686612bec695a0cfe249da6dml , dgn_theory :: G_theory -- local theory
074e084f68dd0b08686612bec695a0cfe249da6dml , globalTheory :: Maybe G_theory -- global theory
074e084f68dd0b08686612bec695a0cfe249da6dml , labelHasHiding :: Bool -- has this node an ingoing hiding link
074e084f68dd0b08686612bec695a0cfe249da6dml , labelHasFree :: Bool -- has incoming free definition link
074e084f68dd0b08686612bec695a0cfe249da6dml , dgn_nf :: Maybe Node -- normal form, for Theorem-Hide-Shift
074e084f68dd0b08686612bec695a0cfe249da6dml , dgn_sigma :: Maybe GMorphism -- inclusion of signature into nf signature
074e084f68dd0b08686612bec695a0cfe249da6dml , dgn_freenf :: Maybe Node -- normal form for freeness
074e084f68dd0b08686612bec695a0cfe249da6dml , dgn_phi :: Maybe GMorphism -- morphism from signature to nffree signature
074e084f68dd0b08686612bec695a0cfe249da6dml , nodeInfo :: DGNodeInfo
074e084f68dd0b08686612bec695a0cfe249da6dml , nodeMod :: NodeMod
074e084f68dd0b08686612bec695a0cfe249da6dml , xnode :: Maybe XGraph.XNode
074e084f68dd0b08686612bec695a0cfe249da6dml , dgn_lock :: Maybe (MVar ())
074e084f68dd0b08686612bec695a0cfe249da6dml , dgn_symbolpathlist :: G_symbolmap [SLinkPath]
074e084f68dd0b08686612bec695a0cfe249da6dmlinstance Show DGNodeLab where
074e084f68dd0b08686612bec695a0cfe249da6dml show _ = "<a DG node label>"
074e084f68dd0b08686612bec695a0cfe249da6dmlisDGRef :: DGNodeLab -> Bool
074e084f68dd0b08686612bec695a0cfe249da6dmlisDGRef l = case nodeInfo l of
074e084f68dd0b08686612bec695a0cfe249da6dml DGNode {} -> False
074e084f68dd0b08686612bec695a0cfe249da6dml DGRef {} -> True
074e084f68dd0b08686612bec695a0cfe249da6dmlsensWithKind :: (forall a . SenStatus a (AnyComorphism, BasicProof) -> Bool)
074e084f68dd0b08686612bec695a0cfe249da6dml -> G_theory -> [String]
074e084f68dd0b08686612bec695a0cfe249da6dmlsensWithKind f (G_theory _lid _sigma _ sens _) = Map.keys $ OMap.filter f sens
074e084f68dd0b08686612bec695a0cfe249da6dmlhasSenKind :: (forall a . SenStatus a (AnyComorphism, BasicProof) -> Bool)
074e084f68dd0b08686612bec695a0cfe249da6dml -> DGNodeLab -> Bool
074e084f68dd0b08686612bec695a0cfe249da6dmlhasSenKind f = not . null . sensWithKind f . dgn_theory
074e084f68dd0b08686612bec695a0cfe249da6dml-- | test if a given node label has local open goals
da14cebe459d3275048785f25bd869cb09b5307fEric ChenghasOpenGoals :: DGNodeLab -> Bool
da14cebe459d3275048785f25bd869cb09b5307fEric ChenghasOpenGoals = hasSenKind (\ s -> not (isAxiom s) && not (isProvenSenStatus s))
da14cebe459d3275048785f25bd869cb09b5307fEric Cheng-- | check if the node has an internal name
da14cebe459d3275048785f25bd869cb09b5307fEric ChengisInternalNode :: DGNodeLab -> Bool
da14cebe459d3275048785f25bd869cb09b5307fEric ChengisInternalNode DGNodeLab {dgn_name = n} = isInternal n
da14cebe459d3275048785f25bd869cb09b5307fEric ChenggetNodeConsStatus :: DGNodeLab -> ConsStatus
da14cebe459d3275048785f25bd869cb09b5307fEric ChenggetNodeConsStatus lbl = case nodeInfo lbl of
da14cebe459d3275048785f25bd869cb09b5307fEric Cheng DGRef {} -> mkConsStatus None
da14cebe459d3275048785f25bd869cb09b5307fEric Cheng DGNode { node_cons_status = c } -> c
da14cebe459d3275048785f25bd869cb09b5307fEric ChenggetNodeCons :: DGNodeLab -> Conservativity
da14cebe459d3275048785f25bd869cb09b5307fEric ChenggetNodeCons = getConsOfStatus . getNodeConsStatus
da14cebe459d3275048785f25bd869cb09b5307fEric Cheng-- | returns the Conservativity if the given node has one, otherwise none
da14cebe459d3275048785f25bd869cb09b5307fEric ChenggetNodeConservativity :: LNode DGNodeLab -> Conservativity
da14cebe459d3275048785f25bd869cb09b5307fEric ChenggetNodeConservativity = getNodeCons . snd
da14cebe459d3275048785f25bd869cb09b5307fEric Cheng{- | test if a node conservativity is open,
da14cebe459d3275048785f25bd869cb09b5307fEric Chengreturn input for refs or nodes with normal forms -}
da14cebe459d3275048785f25bd869cb09b5307fEric ChenghasOpenNodeConsStatus :: Bool -> DGNodeLab -> Bool
da14cebe459d3275048785f25bd869cb09b5307fEric ChenghasOpenNodeConsStatus b lbl = if isJust $ dgn_nf lbl then b else
da14cebe459d3275048785f25bd869cb09b5307fEric Cheng hasOpenConsStatus b $ getNodeConsStatus lbl
da14cebe459d3275048785f25bd869cb09b5307fEric ChengmarkNodeConsistency :: Conservativity -> String -> DGNodeLab -> DGNodeLab
da14cebe459d3275048785f25bd869cb09b5307fEric ChengmarkNodeConsistency newc str dgnode = dgnode
da14cebe459d3275048785f25bd869cb09b5307fEric Cheng { nodeInfo = case nodeInfo dgnode of
da14cebe459d3275048785f25bd869cb09b5307fEric Cheng ninfo@DGNode { node_cons_status = ConsStatus c pc thm } ->
da14cebe459d3275048785f25bd869cb09b5307fEric Cheng if pc == newc && isProvenThmLinkStatus thm then ninfo else
da14cebe459d3275048785f25bd869cb09b5307fEric Cheng ninfo { node_cons_status = ConsStatus c newc
da14cebe459d3275048785f25bd869cb09b5307fEric Cheng $ Proven (DGRule $ showConsistency newc ++ str)
da14cebe459d3275048785f25bd869cb09b5307fEric Cheng emptyProofBasis }
da14cebe459d3275048785f25bd869cb09b5307fEric Cheng ninfo -> ninfo }
da14cebe459d3275048785f25bd869cb09b5307fEric ChengmarkNodeConsistent :: String -> DGNodeLab -> DGNodeLab
da14cebe459d3275048785f25bd869cb09b5307fEric ChengmarkNodeConsistent = markNodeConsistency Cons
074e084f68dd0b08686612bec695a0cfe249da6dmlmarkNodeInconsistent :: String -> DGNodeLab -> DGNodeLab
074e084f68dd0b08686612bec695a0cfe249da6dmlmarkNodeInconsistent = markNodeConsistency Inconsistent
074e084f68dd0b08686612bec695a0cfe249da6dml-- | creates a DGNodeType from a DGNodeLab
type StUnitCtx = Map.Map SIMPLE_ID ImpUnitSigOrSig
emptyStUnitCtx = Map.empty
type RefSigMap = Map.Map SIMPLE_ID RefSig
type BStContext = Map.Map SIMPLE_ID RefSig
$ Map.toList bst
Map.toList rsm
error $ "getUnitSigFromRef:" ++ show (Map.keys rsm)
type RefStUnitCtx = Map.Map SIMPLE_ID RefSig
emptyRefStUnitCtx = Map.empty
&& namesMatchCtx (Map.keys rsmap) bstc rsmap
case Map.findWithDefault (error "namesMatchCtx")
case Map.findWithDefault (error "USABS") un rsmap of
_ -> Map.size bstc' == 1 &&
let un1 = head $ Map.keys bstc'
rsmap' = Map.mapKeys (\ x -> if x == un then un1 else x)
Map.insert un (BranchRefSig (compPointer n1 n2)
Map.insert un
BranchStaticContext $ modifyCtx (Map.keys rsmap') rsmap' bstc'))
_ -> let f = if Map.size bstc' == 1 then
let un1 = head $ Map.keys bstc'
rsmap' = Map.mapKeys
in Map.singleton un $
else Map.empty
in Map.union f $ modifyCtx unitNames rsmap bstc
modifyCtx (Map.keys rsmap) rsmap bstc)
else fail ("Signatures do not match:" ++ show (Map.keys bstc) ++ " "
++ show (Map.keys rsmap))
Map.union rsmap1 rsmap2
type GlobalEnv = Map.Map SIMPLE_ID GlobalEntry
type ProofHistory = SizedList.SizedList HistElem
n = Tree.getNewNode g
f = Map.insert s n $ specRoots dg'
l = Graph.lab g n
(g', _) = Tree.labelNode (n, newL) g
l = Graph.lab g n
(g', _) = Tree.labelNode (n, newL) g
in dg' {specRoots = Map.insert s n $ specRoots dg}
in (d', NPComp (Map.insert k p' cp)))
l = Map.findWithDefault (error $ "addSubTree:" ++ show k) k g
in (d', NPComp (Map.insert k p' cp)))
copySubTree :: DGraph -> Node -> Maybe Node -> (DGraph, Map.Map Node Node)
n' = Tree.getNewNode rTree
in copySubTreeN dg {refTree = rTree'} [n] $ Map.fromList [(n, n')]
Just y -> copySubTreeN dg [n] $ Map.fromList [(n, y)]
copySubTreeN :: DGraph -> [Node] -> Map.Map Node Node
-> (DGraph, Map.Map Node Node)
pairsN = Map.findWithDefault (error "copy") n pairs
copyNode :: Node -> (DGraph, Map.Map Node Node) -> LNode RTLinkLab
-> (DGraph, Map.Map Node Node)
n' = Tree.getNewNode rTree
(rTree'', _) = Tree.insLEdge True orderRT (s, n', eLab) rTree'
in (dg {refTree = rTree''}, Map.insert n n' nMap)
(g', b) = Tree.insLEdge True orderRT
(g1, b1) = Tree.insLEdge True orderRT
diagGraph :: Tree.Gr DiagNodeLab DiagLinkLab,
, dgBody :: Tree.Gr DGNodeLab DGLinkLab -- ^ actual 'DGraph` tree
, refTree :: Tree.Gr RTNodeLab RTLinkLab -- ^ the refinement tree
, specRoots :: Map.Map String Node -- ^ root nodes for named specs
, nameMap :: Map.Map String Node -- ^ all nodes by name
, archSpecDiags :: Map.Map String Diag
, refNodes :: Map.Map Node (LibName, Node) -- ^ unexpanded 'DGRef's
, allRefNodes :: Map.Map (LibName, Node) Node -- ^ all DGRef's
, sigMap :: Map.Map SigId G_sign -- ^ signature map
, thMap :: Map.Map ThId G_theory -- ^ theory map
, morMap :: Map.Map MorId G_morphism -- ^ morphism map
, globalEnv = Map.empty
, dgBody = Graph.empty
, refTree = Graph.empty
, specRoots = Map.empty
, nameMap = Map.empty
, archSpecDiags = Map.empty
, refNodes = Map.empty
, allRefNodes = Map.empty
, sigMap = Map.empty
, thMap = Map.empty
, morMap = Map.empty
, proofHistory = SizedList.empty
, redoHistory = SizedList.empty }
type LibEnv = Map.Map LibName DGraph
emptyLibEnv = Map.empty
, dgn_symbolpathlist = G_symbolmap lid Map.empty }
setSigMapDG :: Map.Map SigId G_sign -> DGraph -> DGraph
setThMapDG :: Map.Map ThId G_theory -> DGraph -> DGraph
setMorMapDG :: Map.Map MorId G_morphism -> DGraph -> DGraph
lookupSigMapDG i = Map.lookup i . sigMap
lookupThMapDG i = Map.lookup i . thMap
lookupMorMapDG i = Map.lookup i . morMap
sigMapI :: DGraph -> (Map.Map SigId G_sign, SigId)
thMapI :: DGraph -> (Map.Map ThId G_theory, ThId)
morMapI :: DGraph -> (Map.Map MorId G_morphism, MorId)
lookupGlobalEnvDG sid = Map.lookup sid . globalEnv
lookupInRefNodesDG n = Map.lookup n . refNodes
Map.lookup (libn, refn) $ allRefNodes dg
n <- Map.lookup s $ nameMap dg
lookupLocalNodeByNameInEnv le s = f $ Map.elems le where
dg { refNodes = Map.insert n (libn, refn) $ refNodes dg
, allRefNodes = Map.insert (libn, refn) n $ allRefNodes dg }
deleteFromRefNodesDG n dg = dg { refNodes = Map.delete n $ refNodes dg }
getNewNodeDG = Tree.getNewNode . dgBody
let (b, l) = Tree.labelNode p $ dgBody g in (g { dgBody = b }, l)
, nameMap = Map.insert (getDGNodeName l) i $ nameMap dg }
{ dgBody = Tree.delLEdge (comparing dgl_id) e
, dgBody = fst $ Tree.insLEdge True compareLinks e $ dgBody g })
(ng, change) = Tree.insLEdge False compareLinks
g { dgBody = fst $ Tree.insLEdge False compareLinks
lookupDGraph ln = Map.findWithDefault (error $ "lookupDGraph " ++ show ln) ln
getLibDepRel :: LibEnv -> Rel.Rel LibName
getLibDepRel = Rel.transClosure
foldr ((\ x -> if isDGRef x then Set.insert (ln, dgn_libname x) else id)
. snd) s $ labNodesDG dg) Set.empty
{- | Get imported libs in topological order, i.e. lib(s) without imports first.
in ( Map.insert e (b, s, t, proofBasis $ thmProofBasis ty) m
, if b && isLocalEdge ty then Set.insert e es else es))
new = Set.union nxt known
in filter (\ (_, _, l) -> dglPending l /= Set.member (dgl_id l) aPs) ls