QualifyNames.hs revision b8d9955b50a96db03997a4946b07826be018b17c
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederModule : $Header$
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederDescription : qualify all names in the nodes of development graphs
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederCopyright : (c) Igor Stassiy, C.Maeder DFKI Bremen 2008
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederMaintainer : Christian.Maeder@dfki.de
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederStability : provisional
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederPortability : non-portable(Logic)
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maederqualify and disambiguate all names in the nodes of a development graph for
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederOMDoc output or for writing out multiple theories for Isabelle or VSE. Note
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maederhowever that signature will be always be complete, i.e. imported entities
99b26e2ab8ba89bc9a050c1524137eb6269e2753Christian Maederwill be repeated.
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maedermodule Proofs.QualifyNames (qualifyLibEnv) where
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport qualified Data.Map as Map
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maederimport qualified Data.Set as Set
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian MaederqualifyLibEnv :: LibEnv -> Result LibEnv
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederqualifyLibEnv libEnv = fmap fst
d97700a22b2585ece83b05f3fff945fdfd0c44b4Christian Maeder $ foldM (\ (le, m) ln -> do
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder dg0 <- updateRefNodes (le, m) $ lookupDGraph ln le
1d65a799298f6b1253d774c22f61029e6eb99cadcmaeder (dg, trm) <- qualifyDGraph ln dg0
1d65a799298f6b1253d774c22f61029e6eb99cadcmaeder return ( Map.insert ln (computeDGraphTheories le dg) le
de8eee2014437ec4020be15cd363257f87e79943Christian Maeder (libEnv, Map.empty) $ getTopsortedLibs libEnv
fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maedertype RenameMap = Map.Map Int (GMorphism, GMorphism)
f674d7a58db3f991300a708f3799d80c369781f8Eugen KuksaqualifyDGraph :: LibName -> DGraph -> Result (DGraph, RenameMap)
fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian MaederqualifyDGraph ln dg =
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder addErrorDiag "qualification failed for" (getLibId ln)
473f5af6e4803fbeecc814065952396f2501039bChristian Maeder let es = map (\ (_, _, lb) -> dgl_id lb) $ labEdgesDG dg
473f5af6e4803fbeecc814065952396f2501039bChristian Maeder unless (Set.size (Set.fromList es) == length es) $
473f5af6e4803fbeecc814065952396f2501039bChristian Maeder fail $ "inkonsistent graph for library " ++ showDoc ln ""
473f5af6e4803fbeecc814065952396f2501039bChristian Maeder (dg1, trm) <- foldM (qualifyLabNode ln) (dg, Map.empty) $ topsortedNodes dg
473f5af6e4803fbeecc814065952396f2501039bChristian Maeder return (groupHistory dg (DGRule "Qualified-Names") dg1, trm)
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht{- consider that loops are part of innDG and outDG that should not be handled
275698320a734a6fd647ea6a461d6ce38862da1dChristian MaederproperEdge :: LEdge a -> Bool
844c7d2ec3917393e139e53503757098d568713eSimon UlbrichtproperEdge (x, y, _) = x /= y
734a5ebd38032798f0ab908e2d52862c71b2c127Simon UlbrichtproperInEdges :: DGraph -> Node -> [LEdge DGLinkLab]
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian MaederproperInEdges dg n =
c8afa08a8bda589ef6670068dff0108464be4da7Christian Maeder let pes = filter properEdge $ innDG dg n
c99b0eb6632087d502dd4269599c5aa68a148eebSimon Ulbricht (gs, rs) = partition (liftE isGlobalDef) pes
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder in gs ++ rs
df67ddf64192bfcae6ece65255ad796a17cbe532Christian MaederconstructUnion :: Logic lid sublogics
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder basic_spec sentence symb_items symb_map_items
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder sign morphism symbol raw_symbol proof_tree =>
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder lid -> morphism -> [morphism] -> morphism
526e7f36639cb58e3c99a54bea082499a6b04a25Christian MaederconstructUnion lid hd l = case l of
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder sd : tl -> case maybeResult $ morphism_union lid hd sd of
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder Just m -> case maybeResult $ inverse m of
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder Just _ -> constructUnion lid m tl
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder Nothing -> constructUnion lid sd tl
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder Nothing -> constructUnion lid sd tl
275698320a734a6fd647ea6a461d6ce38862da1dChristian MaederupdateRefNodes :: (LibEnv, Map.Map LibName RenameMap) -> DGraph
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder -> Result DGraph
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian MaederupdateRefNodes (le, trm) dgraph =
f56cdf11927c31495bae642a9eb383212c90ba61Christian Maeder foldM (\ dg (n, lb) ->
7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder if isDGRef lb then do
2e2559f894aaa661b199e4fa00609f522bc5482aSimon Ulbricht let refLn = dgn_libname lb
df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder refNode = dgn_node lb
be1ce1c2b2819ef32743136c13101f1927375311Christian Maeder gp = Map.findWithDefault (error "updateRefNodes2") refNode
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder $ Map.findWithDefault (error "updateRefNodes1") refLn trm
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa refGr = lookupDGraph refLn le
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder gth = dgn_theory $ labDG refGr refNode
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder newlb = lb { dgn_theory = createGThWith gth startSigId startThId }
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder (ds, is) <- createChanges dg n (properInEdges dg n) gp
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder return $ changesDGH dg $ ds ++ SetNodeLab lb (n, newlb) : is
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder else return dg) dgraph $ labNodesDG dgraph
275698320a734a6fd647ea6a461d6ce38862da1dChristian MaedercreateChanges :: DGraph -> Node -> [LEdge DGLinkLab] -> (GMorphism, GMorphism)
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder -> Result ([DGChange], [DGChange])
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian MaedercreateChanges dg n inss (gm1, grm) = do
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder let allOuts = outDG dg n
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder nAllouts <- mapM (composeWithMorphism False gm1 grm) allOuts
e98c3d3efab62d97ebdeed52f4109d961f6432aaChristian Maeder let (nouts, nloops) = partition properEdge nAllouts
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder nAllinss <- mapM (composeWithMorphism True gm1 grm) $ nloops ++ inss
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder return (map DeleteEdge $ allOuts ++ inss, map InsertEdge $ nAllinss ++ nouts)
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian MaederqualifyLabNode :: LibName -> (DGraph, RenameMap) -> LNode DGNodeLab
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder -> Result (DGraph, RenameMap)
26acf851cacd7a31bdc9b25a42af9949942fa7c6Christian MaederqualifyLabNode ln (dg, mormap) (n, lb) =
26acf851cacd7a31bdc9b25a42af9949942fa7c6Christian Maeder if isDGRef lb then return (dg, mormap) else case dgn_theory lb of
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder G_theory lid (ExtSign sig _) _ sens _ -> do
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder let inss = properInEdges dg n
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder hins <- foldM (\ l (GMorphism cid _ _ mor _) ->
5fb6343a5a2b4bbc67bc83479c84a92d23d30edfChristian Maeder if isIdComorphism (Comorphism cid) && language_name lid ==
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder language_name (targetLogic cid) then do
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder hmor <- coerceMorphism (targetLogic cid) lid
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder "qualifyLabNode" mor
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder return $ hmor : l
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder else return l) [] $ map (\ (_, _, ld) -> dgl_morphism ld) inss
11c3a215d5cf043181e83929f1ce214df65cb587Christian Maeder let revHins = mapMaybe (maybeResult . inverse) hins
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder m = case revHins of
5fb6343a5a2b4bbc67bc83479c84a92d23d30edfChristian Maeder [] -> ide sig
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder hd : tl -> constructUnion lid hd tl
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder (m1, osens) <- qualify lid (mkSimpleId $ getDGNodeName lb)
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder (getLibId ln) m sig
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder rm <- inverse m1
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder nThSens <- mapThSensValueM (map_sen lid m1) $ joinSens sens
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder $ toThSens osens
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder let nlb = lb { dgn_theory = G_theory lid
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder (makeExtSign lid (cod m1)) startSigId
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder nThSens startThId }
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder gm1 <- return $ gEmbed $ G_morphism lid m1 startMorId
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder grm <- return $ gEmbed $ G_morphism lid rm startMorId
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder let gp = (gm1, grm)
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder (ds, is) <- createChanges dg n inss gp
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder return ( changesDGH dg $ ds ++ SetNodeLab lb (n, nlb) : is
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder-- consider that hiding definition links have a reverse morphism
8723ec450f2e7a024230467c0c28a3f154905483cmaeder-- and hiding theorems are also special
8723ec450f2e7a024230467c0c28a3f154905483cmaedercomposeWithMorphism :: Bool -> GMorphism -> GMorphism -> LEdge DGLinkLab
8723ec450f2e7a024230467c0c28a3f154905483cmaeder -> Result (LEdge DGLinkLab)
8723ec450f2e7a024230467c0c28a3f154905483cmaedercomposeWithMorphism dir mor rmor (s, t, lb) = do
8723ec450f2e7a024230467c0c28a3f154905483cmaeder let lmor = dgl_morphism lb
8723ec450f2e7a024230467c0c28a3f154905483cmaeder inmor = comp lmor mor
8723ec450f2e7a024230467c0c28a3f154905483cmaeder outmor = comp rmor lmor
8723ec450f2e7a024230467c0c28a3f154905483cmaeder nlb <- addErrorDiag
8723ec450f2e7a024230467c0c28a3f154905483cmaeder ((if dir then "in" else "out") ++ "-edge " ++ show (s, t, dgl_id lb)) ()
8723ec450f2e7a024230467c0c28a3f154905483cmaeder $ case dgl_type lb of
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder HidingDefLink -> do
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder nmor <- if dir then outmor else inmor
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder return lb { dgl_morphism = nmor }
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder HidingFreeOrCofreeThm Nothing hmor st -> if dir then do
9d50556254571c0811e94b4d948463754812a5aaChristian Maeder nmor <- inmor
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder return lb { dgl_morphism = nmor }
1f0483f71bad0707f10293d0b4db4649aa93fb35Christian Maeder nhmor <- comp hmor mor
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder return lb { dgl_type = HidingFreeOrCofreeThm Nothing nhmor st }
c5b8b64377e24bcbf5cc108ca433cfbbd6235ba1Christian Maeder nmor <- if dir then inmor else outmor
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder return lb { dgl_morphism = nmor }
9d50556254571c0811e94b4d948463754812a5aaChristian Maeder return (s, t, nlb)