added names for internal nodes

git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@3981 cec4b9c1-7d33-0410-9eda-942365e851bb
spechub · Mar 20, 2005 · db71439 · db71439
1 parent 6388978
commit db71439
Show file tree

Hide file tree

Showing 8 changed files with 159 additions and 128 deletions.
diff --git a/Common/Id.hs b/Common/Id.hs
@@ -8,7 +8,7 @@ Stability   :  provisional
 Portability :  portable
 
 
-This modul supplies positions, simple and mixfix identifiers. 
+This module supplies positions, simple and mixfix identifiers. 
 A simple identifier is a lexical token given by a string and a start position.
 
 -  A 'place' is a special token within mixfix identifiers.
@@ -76,6 +76,9 @@ type SIMPLE_ID = Token
 mkSimpleId :: String -> Token
 mkSimpleId s = Token s nullPos
 
+extSimpleId :: String -> SIMPLE_ID -> SIMPLE_ID
+extSimpleId s sid = sid {tokStr = tokStr sid ++ s}
+
 -- | show the plain string
 showTok :: Token -> ShowS
 showTok = showString . tokStr

diff --git a/GUI/ConvertDevToAbstractGraph.hs b/GUI/ConvertDevToAbstractGraph.hs
@@ -108,6 +108,7 @@ type GInfo = (IORef ProofStatus,
               Descr,
               LIB_NAME,
               GraphInfo,
+              IORef Bool, -- show internal names?
               HetcatsOpts)
 
 initializeConverter :: IO (IORef GraphMem)
@@ -163,6 +164,7 @@ initializeGraph ioRefGraphMem ln dGraph convMaps globContext hetsOpts = do
   graphMem <- readIORef ioRefGraphMem
   event <- newIORef 0
   convRef <- newIORef convMaps
+  showInternalNames <- newIORef True
   ioRefProofStatus <- newIORef (globContext, libname2dg convMaps,
 		                [([]::[DGRule], []::[DGChange])],
 				dGraph)
@@ -171,7 +173,7 @@ initializeGraph ioRefGraphMem ln dGraph convMaps globContext hetsOpts = do
   let gid = nextGraphId graphMem -- newIORef (nextGraphId convMaps)
       actGraphInfo = graphInfo graphMem
 --  graphId <- newIORef 0
-  let gInfo = (ioRefProofStatus, event, convRef, gid, ln, actGraphInfo, hetsOpts)
+  let gInfo = (ioRefProofStatus, event, convRef, gid, ln, actGraphInfo, showInternalNames, hetsOpts)
   Result descr _ <- 
     makegraph ("Development graph for "++show ln) 
          -- action on "open"
@@ -201,7 +203,13 @@ initializeGraph ioRefGraphMem ln dGraph convMaps globContext hetsOpts = do
          -- the global menu
              [GlobalMenu (Menu Nothing
                [Menu (Just "Unnamed nodes")
-                 [Button "Hide" 
+                 [Button "Hide/show names" 
+                          (do b <- readIORef showInternalNames
+                              writeIORef showInternalNames (not b)
+                              putStrLn ("showInternalNames ="++show b)
+                              redisplay gid actGraphInfo
+                              return ()    ),
+                  Button "Hide nodes" 
                           (do --gid <- readIORef graphId
                               Result descr _ <- hideSetOfNodeTypes gid
 			                            ["internal",
@@ -211,7 +219,7 @@ initializeGraph ioRefGraphMem ln dGraph convMaps globContext hetsOpts = do
                               redisplay gid actGraphInfo
                               return ()    ),
 
-                  Button "Show" 
+                  Button "Show nodes" 
                           (do --gid <- readIORef graphId
 			      descr <- readIORef event
                               showIt gid descr actGraphInfo
@@ -375,7 +383,7 @@ openProofStatus filename ioRefProofStatus convRef hetsOpts =
 proofMenu :: GInfo
              -> (ProofStatus -> IO (Res.Result ProofStatus))
              -> IO ()
-proofMenu (ioRefProofStatus, event, convRef, gid, ln, actGraphInfo, _) proofFun 
+proofMenu (ioRefProofStatus, event, convRef, gid, ln, actGraphInfo, _, _) proofFun 
   = do
   proofStatus <- readIORef ioRefProofStatus
   Res.Result diags res <- proofFun proofStatus
@@ -433,9 +441,12 @@ createLocalMenuNodeTypeSpec color convRef dGraph ioRefSubtreeEvents
                      :: DaVinciNodeTypeParms (String,Int,Int)
 
 -- local menu for the nodetypes internal and locallyEmpty_internal
-createLocalMenuNodeTypeInternal color convRef dGraph gInfo =
+createLocalMenuNodeTypeInternal color convRef dGraph 
+                                gInfo@(_,_,_,_,_,_,showInternalNames,_) =
                  Ellipse $$$ Color color
-		 $$$ ValueTitle (\ (s,_,_) -> return "")
+		 $$$ ValueTitle (\ (s,_,_) -> do
+                       b <- readIORef showInternalNames
+                       if b then return s else return "")
                  $$$ LocalMenu (Menu (Just "node menu")
                     [--createLocalMenuButtonShowSpec convRef dGraph,
 		     createLocalMenuButtonShowNumberOfNode,
@@ -452,7 +463,7 @@ createLocalMenuNodeTypeInternal color convRef dGraph gInfo =
 
 -- local menu for the nodetypes dg_ref and locallyEmpty_dg_ref
 createLocalMenuNodeTypeDgRef color convRef actGraphInfo 
-			     ioRefGraphMem graphMem (_,_,_,_,_,_,hetsOpts) = 
+			     ioRefGraphMem graphMem (_,_,_,_,_,_,_,hetsOpts) = 
                  Box $$$ Color color
 		 $$$ ValueTitle (\ (s,_,_) -> return s)
 		 $$$ LocalMenu (Button "Show referenced library"
@@ -504,7 +515,7 @@ createLocalMenuButtonTranslateTheory gInfo =
 -}
 --createLocalMenuTaxonomy :: IORef ProofStatus -> Descr -> AGraphToDGraphNode -> 
 --                     DGraph -> IO ()
-createLocalMenuTaxonomy (proofStatus,_,_,_,_,_,_) convRef dGraph =
+createLocalMenuTaxonomy (proofStatus,_,_,_,_,_,_,_) convRef dGraph =
       (Menu (Just "Taxonomy graphs")
        [createMenuButton "Subsort graph" 
 	       (passTh displaySubsortGraph) convRef dGraph,
@@ -521,7 +532,7 @@ createLocalMenuTaxonomy (proofStatus,_,_,_,_,_,_) convRef dGraph =
 
 
 
-createLocalMenuButtonShowSublogic (proofStatus,_,_,_,_,_,_) = 
+createLocalMenuButtonShowSublogic (proofStatus,_,_,_,_,_,_,_) = 
   createMenuButton "Show sublogic" (getSublogicOfNode proofStatus)
 createLocalMenuButtonShowNodeOrigin  = 
   createMenuButton "Show origin" showOriginOfNode 
@@ -600,7 +611,8 @@ createLocalMenuButtonShowNumberOfNode =
 createLocalEdgeMenu gInfo = 
     LocalMenu (Menu (Just "edge menu")
 	       [createLocalMenuButtonShowMorphismOfEdge gInfo,
-		createLocalMenuButtonShowOriginOfEdge gInfo]
+		createLocalMenuButtonShowOriginOfEdge gInfo,
+                createLocalMenuButtonCheckconsistencyOfEdge gInfo]
 	      )
 
 createLocalEdgeMenuThmEdge gInfo =
@@ -684,9 +696,7 @@ getSignatureOfNode descr ab2dgNode dgraph =
       do let dgnode = lab' (context node dgraph)
 	 case dgnode of
            (DGNode name (G_sign _ sig) _ _ _ _) ->
-              let title = case name of
-                   Nothing -> "Signature"
-                   Just n -> "Signature of "++showPretty n ""
+              let title = "Signature of "++showName name
                in createTextDisplay title (showPretty sig "") [size(80,50)]
               --putStrLn ((showPretty sig) "\n")
            (DGRef _ _ _) -> error 
@@ -715,7 +725,7 @@ lookupTheoryOfNode proofStatusRef descr ab2dgNode dgraph = do
 used by the node menu defined in initializeGraph-}
 getTheoryOfNode :: GInfo -> Descr -> AGraphToDGraphNode -> 
                      DGraph -> IO()
-getTheoryOfNode  (proofStatusRef,_,_,_,_,_,hetsOpts) descr ab2dgNode dgraph = do
+getTheoryOfNode  (proofStatusRef,_,_,_,_,_,_,hetsOpts) descr ab2dgNode dgraph = do
  r <- lookupTheoryOfNode proofStatusRef descr ab2dgNode dgraph
  case r of
   Res.Result diags res -> do
@@ -736,9 +746,7 @@ displayTheory ext node dgraph gth =
     let dgnode = lab' (context node dgraph)
         str = printTheory (simplifyTh gth) in case dgnode of
            (DGNode name (G_sign _ _) _ _ _ _) ->
-              let thname = case name of
-                   Nothing -> "InternalNode"++show node
-                   Just n -> showPretty n ""
+              let thname = showName name
                   title = ext ++ " of " ++ thname
                in createTextSaveDisplay title (thname++".het") str [size(100,50)]
               --putStrLn ((showPretty sig) "\n")
@@ -751,7 +759,7 @@ displayTheory ext node dgraph gth =
 used by the node menu defined in initializeGraph-}
 translateTheoryOfNode :: GInfo -> Descr -> AGraphToDGraphNode -> 
                      DGraph -> IO()
-translateTheoryOfNode gInfo@(proofStatusRef,_,_,_,_,_,opts) descr ab2dgNode dgraph = do
+translateTheoryOfNode gInfo@(proofStatusRef,_,_,_,_,_,_,opts) descr ab2dgNode dgraph = do
  (_,libEnv,_,_) <- readIORef proofStatusRef
  case (do
    (_libname, node) <- 
@@ -796,13 +804,11 @@ getSublogicOfNode proofStatusRef descr ab2dgNode dgraph = do
       let dgnode = lab' (context node dgraph)
           name = case dgnode of
                        (DGNode name _ _ _ _ _) -> name
-                       _ -> Nothing
+                       _ -> emptyName
        in case computeTheory libEnv dgraph node of
         Res.Result _ (Just th) ->
                 let logstr = show $ sublogicOfTh th
-                    title = case name of
-                     Nothing -> "Sublogic"
-                     Just n -> "Sublogic of "++showPretty n ""
+                    title =  "Sublogic of "++showName name
                  in createTextDisplay title logstr [size(30,10)]
         Res.Result diags _ -> 
           error ("Could not compute theory for sublogic computation: "++
@@ -820,9 +826,7 @@ showOriginOfNode descr ab2dgNode dgraph =
       do let dgnode = lab' (context node dgraph)
 	 case dgnode of
            (DGNode name _ _ _ _ orig) ->    
-              let title = case name of
-                     Nothing -> "Origin of node"
-                     Just n -> "Origin of node "++showPretty n ""
+              let title =  "Origin of node "++showName name
                in createTextDisplay title 
                     (showPretty orig "") [size(30,10)]
     Nothing -> error ("node with descriptor "
@@ -832,7 +836,7 @@ showOriginOfNode descr ab2dgNode dgraph =
 
 {- start local theorem proving or consistency checking at a node -}
 --proveAtNode :: Bool -> Descr -> AGraphToDGraphNode -> DGraph -> IO()
-proveAtNode checkCons gInfo@(_,_,convRef,_,_,_,_) descr ab2dgNode dgraph = 
+proveAtNode checkCons gInfo@(_,_,convRef,_,_,_,_,_) descr ab2dgNode dgraph = 
   case Map.lookup descr ab2dgNode of
     Just libNode -> 
       do convMaps <- readIORef convRef
@@ -879,7 +883,7 @@ showProofStatusOfThm descr Nothing =
 
 {- check consistency of the edge -}
 checkconsistencyOfEdge :: Descr -> GInfo -> Maybe (LEdge DGLinkLab) -> IO()
-checkconsistencyOfEdge _ (ref,_,_,_,_,_,opts) (Just (source,target,linklab)) = do 
+checkconsistencyOfEdge _ (ref,_,_,_,_,_,_,opts) (Just (source,target,linklab)) = do 
   (_,libEnv,_,dgraph) <- readIORef ref
   let dgtar = lab' (context target dgraph)
   case dgtar of
@@ -957,23 +961,17 @@ convertNodesAux convMaps descr graphInfo ((node,dgnode):lNodes) libname =
                                        descr graphInfo lNodes libname)
      return newConvMaps
 
--- gets the name of a development graph node as a string
-
-getDGNodeName :: DGNodeLab -> String
-getDGNodeName dgnode =
-  case get_dgn_name dgnode of
-    Just simpleId -> tokStr simpleId
-    Nothing -> ""
+
 
 -- gets the type of a development graph edge as a string
 getDGNodeType :: DGNodeLab -> IO String
 getDGNodeType dgnode =
   do let nodetype = getDGNodeTypeAux dgnode
      case (isDGRef dgnode) of
        True -> return (nodetype++"dg_ref")
-       False -> case get_dgn_name dgnode of
-                  Just _ -> return (nodetype++"spec")
-                  Nothing -> return (nodetype++"internal")
+       False -> if isInternalNode dgnode 
+                   then return (nodetype++"internal")
+                   else return (nodetype++"spec")
 
 getDGNodeTypeAux :: DGNodeLab -> String
 getDGNodeTypeAux dgnode = if (locallyEmpty dgnode) then "locallyEmpty_"

diff --git a/Proofs/Proofs.hs b/Proofs/Proofs.hs
@@ -670,21 +670,13 @@ prettyPrintPath dgraph path =
 {- returns the name of the source node of the given edge-}
 prettyPrintSourceNode :: DGraph -> LEdge DGLinkLab -> String
 prettyPrintSourceNode dgraph (src,_,_) =
-  case get_dgn_name lab of
-    Just simpleId -> tokStr simpleId
-    Nothing -> ""
-  where
-    lab = lab' (context src dgraph)
+   getDGNodeName $ lab' (context src dgraph)
 
 
 {- returns the name of the target node of the given edge-}
 prettyPrintTargetNode :: DGraph -> LEdge DGLinkLab -> String
 prettyPrintTargetNode dgraph (_,tgt,_) =
-  case get_dgn_name lab of
-    Just simpleId -> tokStr simpleId
-    Nothing -> ""
-  where
-    lab = lab' (context tgt dgraph)
+   getDGNodeName $ lab' (context tgt dgraph)
 
 
 {- creates a unproven global thm edge for the given path, i.e. with the same source and target nodes and the same morphism as the path -}
@@ -1377,7 +1369,7 @@ basicInferenceNode checkCons lg (ln,node)
           DGNode _ _ _ _ _ _-> dgn_name nlab
           DGRef _ _ _ -> dgn_renamed nlab
         thName = showPretty (getLIB_ID ln) "_"
-                 ++ maybe (show node) (flip showPretty "") nodeName
+                 ++ {-maybe (show node)-} showName nodeName
     -- compute the list of proof goals
     let inEdges = inn dGraph node
         localEdges = filter isUnprovenLocalThm inEdges

diff --git a/Static/AnalysisArchitecture.hs b/Static/AnalysisArchitecture.hs
@@ -479,15 +479,15 @@ ana_UNIT_SPEC lgraph defl gctx@(_, genv, _) curl just_struct
         ana_UNIT_SPEC lgraph defl gctx curl just_struct impsig (Spec_name spn)
 -- a trivial unit type
 ana_UNIT_SPEC lgraph _ gctx _ just_struct impsig (Unit_type [] resultSpec poss) =
-    do (resultSpec', resultSig, dg') <- ana_SPEC lgraph gctx impsig Nothing 
-                                                 just_struct (item resultSpec)
+    do (resultSpec', resultSig, dg') <- ana_SPEC lgraph gctx impsig Static.DevGraph.emptyName  
+                                                 just_struct  (item resultSpec)
        return (Unit_sig resultSig, dg', Unit_type [] (replaceAnnoted resultSpec' resultSpec) poss)
 -- a non-trivial unit type
 ana_UNIT_SPEC lgraph defl gctx@(gannos, genv, _) _ opts impSig (Unit_type argSpecs resultSpec poss) =
     do (argSigs, dg1, argSpecs') <- ana_argSpecs lgraph defl gctx opts argSpecs
        (sigUnion, dg2) <- nodeSigUnion lgraph dg1 (impSig : argSigs) DGFormalParams
        (resultSpec', resultSig, dg3) <- ana_SPEC lgraph (gannos, genv, dg2) sigUnion
-                                                 Nothing opts (item resultSpec)
+                                                 Static.DevGraph.emptyName opts (item resultSpec)
        return (Par_unit_sig (argSigs, resultSig), dg3, 
                Unit_type argSpecs' (replaceAnnoted resultSpec' resultSpec) poss) 
 -- SPEC-NAME (an alias)
@@ -531,7 +531,7 @@ ana_argSpecs :: LogicGraph -> AnyLogic -> GlobalContext -> HetcatsOpts -> [Annot
 ana_argSpecs _ _ (_, _, dg) _ [] =
     do return ([], dg, [])
 ana_argSpecs lgraph defl gctx@(gannos, genv, _) opts (argSpec : argSpecs) =
-    do (argSpec', argSig, dg') <- ana_SPEC lgraph gctx (EmptyNode defl) Nothing
+    do (argSpec', argSig, dg') <- ana_SPEC lgraph gctx (EmptyNode defl) Static.DevGraph.emptyName
                                            opts (item argSpec)
        (argSigs, dg'', argSpecs') <- ana_argSpecs lgraph defl (gannos, genv, dg') opts argSpecs
        return (argSig : argSigs, dg'', (replaceAnnoted argSpec' argSpec) : argSpecs')

diff --git a/Static/AnalysisLibrary.hs b/Static/AnalysisLibrary.hs
@@ -270,10 +270,10 @@ ana_LIB_ITEM lgraph _defl opts libenv gctx@(gannos, genv, _) l
      else
      resToIORes $ message () analyseMessage
   (gen',(imp,params,parsig,allparams),dg') <- 
-     resToIORes (ana_GENERICITY lgraph gctx l opts gen)
+     resToIORes (ana_GENERICITY lgraph gctx l opts (extName "P" (makeName spn)) gen)
   (sp',body,dg'') <- 
      resToIORes (ana_SPEC lgraph (gannos,genv,dg') 
-                          allparams (Just spn) opts (item asp))
+                          allparams (makeName spn) opts (item asp))
   let libItem' = Spec_defn spn gen' (replaceAnnoted sp' asp) pos
   if Map.member spn genv 
    then resToIORes (plain_error (libItem',gctx,l,libenv)
@@ -430,9 +430,9 @@ ana_VIEW_DEFN lgraph _defl libenv gctx@(gannos, genv, _) l opts
               vn gen vt gsis pos = do
   let adj = adjustPos (headPos pos)
   (gen',(imp,params,parsig,allparams),dg') <- 
-       ana_GENERICITY lgraph gctx l opts gen
+       ana_GENERICITY lgraph gctx l opts (extName "VG" (makeName vn)) gen
   (vt',(src,tar),dg'') <- 
-       ana_VIEW_TYPE lgraph (gannos,genv,dg') l allparams opts vt
+       ana_VIEW_TYPE lgraph (gannos,genv,dg') l allparams opts (makeName vn) vt
   let gsigmaS = getSig src
       gsigmaT = getSig tar
   G_sign lidS sigmaS <- return gsigmaS
@@ -501,7 +501,7 @@ refNodesig :: LIB_NAME -> (DGraph, [NodeSig]) -> (Maybe SIMPLE_ID, NodeSig)
            -> (DGraph, [NodeSig])
 refNodesig ln (dg,refdNodes) (name,NodeSig(n,sigma)) =
   let node_contents = DGRef {
-        dgn_renamed = name,
+        dgn_renamed = makeMaybeName name,
         dgn_libname = ln,
         dgn_node = n }
       [node] = newNodes 0 dg