ToXml.hs revision bea536c79193020edac8fc6ebdd51b11f885b5af
93fa7e4374de6e37328e752991a698bf03032c75Christian MaederModule : $Header$
93fa7e4374de6e37328e752991a698bf03032c75Christian MaederDescription : xml output of Hets development graphs
93fa7e4374de6e37328e752991a698bf03032c75Christian MaederCopyright : (c) Ewaryst Schulz, Uni Bremen 2009
93fa7e4374de6e37328e752991a698bf03032c75Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
93fa7e4374de6e37328e752991a698bf03032c75Christian MaederMaintainer : Ewaryst.Schulz@dfki.de
93fa7e4374de6e37328e752991a698bf03032c75Christian MaederStability : provisional
93fa7e4374de6e37328e752991a698bf03032c75Christian MaederPortability : non-portable(Grothendieck)
d697755cce49a436e1170e8e158c19f79b0389b8Christian MaederXml of Hets DGs
d697755cce49a436e1170e8e158c19f79b0389b8Christian Maedermodule Static.ToXml (dGraph, lnode, dgSymbols, showSymbols, showSymbolsTh)
fd40e201b7277427113c89724d8a2389c18e9cbdChristian Maederimport Static.ComputeTheory (getImportNames)
b26211de8c1e50efbabbb95497e7508c4d852634Christian Maederimport qualified Common.OrderedMap as OMap
b26211de8c1e50efbabbb95497e7508c4d852634Christian Maederimport qualified Data.Map as Map
b26211de8c1e50efbabbb95497e7508c4d852634Christian Maederimport qualified Data.Set as Set (toList)
b26211de8c1e50efbabbb95497e7508c4d852634Christian MaederdGraph :: LibEnv -> LibName -> DGraph -> Element
c8bf82bdb27dfa58f7f05045c639c14276be3333Christian MaederdGraph lenv ln dg =
b26211de8c1e50efbabbb95497e7508c4d852634Christian Maeder let body = dgBody dg
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder ga = globalAnnos dg
e4eed2389ec1b1bfa03c662c71e8165e93df43c4Christian Maeder lnodes = labNodes body
e4eed2389ec1b1bfa03c662c71e8165e93df43c4Christian Maeder in add_attrs [ mkAttr "filename" $ getFilePath ln
70ca840c8a6cf3591d5f9aa9a3de6fae42d696e8Christian Maeder , mkAttr "libname" $ show $ getLibId ln
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder , mkAttr "nextlinkid" $ showEdgeId $ getNewEdgeId dg ]
e4eed2389ec1b1bfa03c662c71e8165e93df43c4Christian Maeder $ unode "DGraph" $
e4eed2389ec1b1bfa03c662c71e8165e93df43c4Christian Maeder subnodes "Global" (annotations ga $ convertGlobalAnnos
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder $ removeHetCASLprefixes ga)
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder ++ map (lnode ga lenv) lnodes
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder ++ map (ledge ga dg) (labEdges body)
93fa7e4374de6e37328e752991a698bf03032c75Christian Maedergmorph :: GlobalAnnos -> GMorphism -> Element
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maedergmorph ga gm@(GMorphism cid (ExtSign ssig _) _ tmor _) =
e4eed2389ec1b1bfa03c662c71e8165e93df43c4Christian Maeder case map_sign cid ssig of
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder Result _ mr -> case mr of
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder Nothing -> error $ "Static.ToXml.gmorph: " ++ showGlobalDoc ga gm ""
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder Just (tsig, tsens) -> let
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder tid = targetLogic cid
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder sl = Map.toList . Map.filterWithKey (/=) $ symmap_of tid tmor
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder psym = prettyElem "Symbol" ga
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder in add_attr (mkNameAttr $ language_name cid)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder $ unode "GMorphism" $
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder subnodes "Axioms"
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder (map (showSen (targetLogic cid) ga Nothing tsig) tsens)
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder ++ map (\ (s, t) -> unode "map" [psym s, psym t]) sl
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaederprettyRangeElem :: (GetRange a, Pretty a) => String -> GlobalAnnos -> a
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian MaederprettyRangeElem s ga a =
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder add_attrs (rangeAttrs $ getRangeSpan a) $ prettyElem s ga a
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian MaederprettySymbol :: (GetRange a, Pretty a) => GlobalAnnos -> a -> Element
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaederprettySymbol = prettyRangeElem "Symbol"
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maederlnode :: GlobalAnnos -> LibEnv -> LNode DGNodeLab -> Element
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maederlnode ga lenv (_, lbl) =
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder let nm = dgn_name lbl
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (spn, xp) = case reverse $ xpath nm of
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder ElemName s : t -> (s, showXPath t)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder l -> ("?", showXPath l)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder in add_attrs (mkNameAttr (showName nm)
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder : if not (isDGRef lbl) then case signOf $ dgn_theory lbl of
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder G_sign slid _ _ -> mkAttr "logic" (show slid)
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder : if dgn_origin lbl < DGProof then
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder [mkAttr "refname" spn, mkAttr "relxpath" xp ]
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder else [] else [])
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder $ unode "DGNode"
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder $ case nodeInfo lbl of
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder DGRef li rf ->
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder [ add_attrs [ mkAttr "library" $ show $ getLibId li
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder , mkAttr "node" $ getNameOfNode rf
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder $ lookupDGraph li lenv ]
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder $ unode "Reference" () ]
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder DGNode orig cs -> consStatus cs ++ case orig of
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder DGBasicSpec _ (G_sign lid (ExtSign dsig _) _) _ ->
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder subnodes "Declarations"
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder $ map (showSym lid)
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder $ mostSymsOf lid dsig
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder DGRestriction _ hidSyms -> subnodes "Hidden"
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder $ map (prettySymbol ga)
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder ++ case dgn_theory lbl of
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder G_theory lid (ExtSign sig _) _ thsens _ -> let
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder (axs, thms) = OMap.partition isAxiom thsens
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder in subnodes "Axioms"
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (map (showSen lid ga Nothing sig) $ toNamedList axs)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder ++ subnodes "Theorems"
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder (map (\ (s, t) -> showSen lid ga
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder (Just $ isProvenSenStatus t) sig $ toNamed s t)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder-- | a status may be open, proven or outdated
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedermkStatusAttr :: String -> Attr
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedermkStatusAttr = mkAttr "status"
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian MaedermkProvenAttr :: Bool -> Attr
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedermkProvenAttr b = mkStatusAttr $ if b then "proven" else "open"
6fb319833285f714693d58e9620d67ab21ddebe4Christian MaederconsStatus :: ConsStatus -> [Element]
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaederconsStatus cs = case getConsOfStatus cs of
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder cStat -> [unode "ConsStatus" $ show cStat]
6fb319833285f714693d58e9620d67ab21ddebe4Christian Maederledge :: GlobalAnnos -> DGraph -> LEdge DGLinkLab -> Element
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maederledge ga dg (f, t, lbl) = let
6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder typ = dgl_type lbl
6eed7cde6b75d63ec6b8f7e31caac6919558a676Christian Maeder mor = gmorph ga $ dgl_morphism lbl
6eed7cde6b75d63ec6b8f7e31caac6919558a676Christian Maeder mkMor n = add_attr (mkAttr "morphismsource" $ getNameOfNode n dg) mor
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder lnkSt = case thmLinkStatus typ of
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder Nothing -> []
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder Just tls -> case tls of
6eed7cde6b75d63ec6b8f7e31caac6919558a676Christian Maeder LeftOpen -> []
6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder Proven r ls -> dgrule r ++ map (\ e ->
6eed7cde6b75d63ec6b8f7e31caac6919558a676Christian Maeder add_attr (mkAttr "linkref" $ showEdgeId e)
6eed7cde6b75d63ec6b8f7e31caac6919558a676Christian Maeder $ unode "ProofBasis" ()) (Set.toList $ proofBasis ls)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder ([ mkAttr "source" $ getNameOfNode f dg
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder , mkAttr "target" $ getNameOfNode t dg
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder , mkAttr "linkid" $ showEdgeId $ dgl_id lbl
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder ] ++ case dgl_origin lbl of
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder DGLinkView i _ -> [mkNameAttr $ iriToStringShortUnsecure i]
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder $ unode "DGLink"
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder $ unode "Type" (getDGLinkType lbl) : lnkSt
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder ++ consStatus (getLinkConsStatus typ)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder ++ [case typ of
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder HidingFreeOrCofreeThm _ n _ _ -> mkMor n
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder FreeOrCofreeDefLink _ (JustNode ns) -> mkMor $ getNode ns
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maederdgrule :: DGRule -> [Element]
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder unode "Rule" (dgRuleHeader r)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder DGRuleLocalInference m ->
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder map (\ (s, t) -> add_attrs [mkNameAttr s, mkAttr "renamedTo" t]
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder $ unode "MovedTheorems" ()) m
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder Composition es -> map (\ e ->
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder add_attr (mkAttr "linkref" $ showEdgeId e)
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder $ unode "Composition" ()) es
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder DGRuleWithEdge _ e ->
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder [ add_attr (mkAttr "linkref" $ showEdgeId e)
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder $ unode "RuleTarget" () ]
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder-- | collects all symbols from dg and displays them as xml
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian MaederdgSymbols :: DGraph -> Element
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian MaederdgSymbols dg = let ga = globalAnnos dg in unode "Ontologies"
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder $ map (\ (i, lbl) -> let ins = getImportNames dg i in
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder showSymbols ins ga lbl) $ labNodesDG dg
70ca840c8a6cf3591d5f9aa9a3de6fae42d696e8Christian MaedershowSymbols :: [String] -> GlobalAnnos -> DGNodeLab -> Element
6fb319833285f714693d58e9620d67ab21ddebe4Christian MaedershowSymbols ins ga lbl = showSymbolsTh ins (getDGNodeName lbl) ga
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder $ dgn_theory lbl
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedershowSymbolsTh :: [String] -> String -> GlobalAnnos -> G_theory -> Element
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedershowSymbolsTh ins name ga th = case th of
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder G_theory lid (ExtSign sig _) _ sens _ -> add_attrs
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder [ mkAttr "logic" $ language_name lid
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder , mkNameAttr name ]
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder . unode "Ontology"
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder $ [ unode "Symbols" . map (showSym lid) $ symlist_of lid sig
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder , unode "Axioms" . map (showSen lid ga Nothing sig) $ toNamedList sens ]
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder ++ map (unode "Import") ins
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedershowSen :: ( GetRange sentence, Pretty sentence
70ca840c8a6cf3591d5f9aa9a3de6fae42d696e8Christian Maeder , Sentences lid sentence sign morphism symbol) =>
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder lid -> GlobalAnnos -> Maybe Bool -> sign -> Named sentence -> Element
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian MaedershowSen lid ga mt sig ns = let s = sentence ns in add_attrs
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder Nothing -> []
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder Just b -> [mkProvenAttr b]
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder ++ mkNameAttr (senAttr ns) : rangeAttrs (getRangeSpan s))
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder . unode (if isJust mt then "Theorem" else "Axiom") $ unode "Text"
e69bfc714e534d71322f504dde433941142e1c05Christian Maeder (show $ useGlobalAnnos ga (print_named lid
6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder $ mapNamed (simplify_sen lid sig) ns))
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder : map (showSym lid) (symsOfSen lid s)
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian MaedershowSym :: (Sentences lid sentence sign morphism symbol) =>
6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder lid -> symbol -> Element
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedershowSym lid s = add_attrs
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder [ mkAttr "kind" $ symKind lid s
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder , mkNameAttr . show $ sym_name lid s ]
e69bfc714e534d71322f504dde433941142e1c05Christian Maeder $ prettySymbol emptyGlobalAnnos s