ToXml.hs revision 6538c7b76c51c5c4de59b9cb19941cd2f4202ef3
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederModule : $Header$
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederDescription : xml output of Hets development graphs
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederCopyright : (c) Ewaryst Schulz, Uni Bremen 2009
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederMaintainer : Ewaryst.Schulz@dfki.de
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederStability : provisional
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederPortability : non-portable(Grothendieck)
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederXml of Hets DGs
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder , showSymbols
da245da15da78363c896e44ea97a14ab1f83eb50Christian Maeder , showSymbolsTh
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederimport Static.ComputeTheory (getImportNames)
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maederimport qualified Common.OrderedMap as OMap
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederimport qualified Data.Map as Map
712f5e5ca1c3a5cfdd28518154ecf2dd0994cdb5Christian Maederimport qualified Data.Set as Set (toList)
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maederimport Data.Char (toLower)
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian MaederExport the development graph as xml. If the flag full is True then
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maedersymbols for all nodes are shown as declarations, otherwise (the
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maederdefault) only declaration for basic spec nodes are shown that are
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maedersufficient to reconstruct the development from the xml output. -}
86c119e3e74ba4b1b4ca728531282e9100789939Christian MaederdGraph :: HetcatsOpts -> LibEnv -> LibName -> DGraph -> Element
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian MaederdGraph full lenv ln dg =
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder let body = dgBody dg
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder ga = globalAnnos dg
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder lnodes = labNodes body
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder ledges = labEdges body
79a3b1a7bf306fdedbeb39f9908d62405f37f385Christian Maeder in add_attrs [ mkAttr "filename" $ getFilePath ln
79a3b1a7bf306fdedbeb39f9908d62405f37f385Christian Maeder , mkAttr "mime-type" . fromMaybe "unknown" $ mimeType ln
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder , mkAttr "libname" . show $ setAngles False $ getLibId ln
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder , mkAttr "dgnodes" . show $ length lnodes
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder , mkAttr "dgedges" . show $ length ledges
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder , mkAttr "nextlinkid" . showEdgeId $ getNewEdgeId dg ]
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder . unode "DGraph" $
b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder subnodes "Global" (annotations ga . convertGlobalAnnos
b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder $ removeHetCASLprefixes ga)
b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder ++ map (lnode full ga lenv) lnodes
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder ++ map (ledge full ga dg) ledges
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maedergmorph :: HetcatsOpts -> GlobalAnnos -> GMorphism -> Element
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maedergmorph opts ga gm@(GMorphism cid (ExtSign ssig _) _ tmor _) =
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder case map_sign cid ssig of
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder Result _ mr -> case mr of
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder Nothing -> error $ "Static.ToXml.gmorph: " ++ showGlobalDoc ga gm ""
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder Just (tsig, tsens) -> let
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder tid = targetLogic cid
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder sl = Map.toList . Map.filterWithKey (/=) $ symmap_of tid tmor
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder in add_attr (mkNameAttr $ language_name cid)
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder $ unode "GMorphism" $
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder (if fullTheories opts then [] else subnodes "ComorphismAxioms"
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder $ map (showSen (targetLogic cid) ga Nothing tsig) tsens)
712f5e5ca1c3a5cfdd28518154ecf2dd0994cdb5Christian Maeder ++ map (\ (s, t) -> unode "map" [showSym tid s, showSym tid t]) sl
a05bca7a10260c19581dff325389de3f8edefa5eChristian MaederprettyRangeElem :: (GetRange a, Pretty a) => String -> GlobalAnnos -> a
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaederprettyRangeElem s ga a =
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder add_attrs (rangeAttrs $ getRangeSpan a) $ prettyElem s ga a
712f5e5ca1c3a5cfdd28518154ecf2dd0994cdb5Christian MaederprettySymbol :: (GetRange a, Pretty a) => GlobalAnnos -> a -> Element
51281dddda866c0cda9fca22bf6bc4eea7128112Christian MaederprettySymbol = prettyRangeElem "Symbol"
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederlnode :: HetcatsOpts -> GlobalAnnos -> LibEnv -> LNode DGNodeLab -> Element
fe883661c9d1a5a8b42ac4e8673ec133d9dad354Christian Maederlnode full ga lenv (_, lbl) =
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder let nm = dgn_name lbl
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder (spn, xp) = case reverse $ xpath nm of
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder ElemName s : t -> (s, showXPath t)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder l -> ("?", showXPath l)
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder in add_attrs (mkNameAttr (showName nm)
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder : rangeAttrs (srcRange nm)
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder ++ mkAttr "reference" (map toLower $ show $ isDGRef lbl)
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder : case signOf $ dgn_theory lbl of
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder G_sign slid _ _ -> mkAttr "logic" (show slid)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder : if not (isDGRef lbl) && dgn_origin lbl < DGProof then
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder [mkAttr "refname" spn, mkAttr "relxpath" xp ]
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder $ unode "DGNode"
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder $ case nodeInfo lbl of
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder DGRef li rf ->
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder [ mkAttr "library" $ show $ setAngles False $ getLibId li
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder , mkAttr "location" $ getFilePath li
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder , mkAttr "node" $ getNameOfNode rf $ lookupDGraph li lenv ]
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder $ unode "Reference" () ]
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder DGNode orig cs -> consStatus cs ++ case orig of
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder DGBasicSpec _ (G_sign lid (ExtSign dsig _) _) _ ->
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder subnodes "Declarations"
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder $ map (showSym lid)
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder $ mostSymsOf lid dsig
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder DGRestriction _ hidSyms -> subnodes "Hidden"
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder $ map (prettySymbol ga)
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder ++ case dgn_theory lbl of
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder G_theory lid _ (ExtSign sig _) _ thsens _ -> let
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (axs, thms) = OMap.partition isAxiom thsens in
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder (if fullSign full
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder then subnodes "Symbols" (map (showSym lid) $ symlist_of lid sig)
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder ++ subnodes "Axioms"
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder (map (showSen lid ga Nothing sig) $ toNamedList axs)
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder ++ subnodes "Theorems"
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder (map (\ (s, t) -> showSen lid ga
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder (Just $ isProvenSenStatus t) sig $ toNamed s t)
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder ++ if fullTheories full then case globalTheory lbl of
712f5e5ca1c3a5cfdd28518154ecf2dd0994cdb5Christian Maeder Just (G_theory glid _ _ _ allSens _) -> case
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder coerceThSens glid lid "xml-lnode" allSens of
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder Just gsens -> subnodes "ImpAxioms"
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder $ map (showSen lid ga Nothing sig) $ toNamedList
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder $ OMap.filter ((`notElem` map sentence
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder (OMap.elems thsens)) . sentence) gsens
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder-- | a status may be open, proven or outdated
86c119e3e74ba4b1b4ca728531282e9100789939Christian MaedermkStatusAttr :: String -> Attr
86c119e3e74ba4b1b4ca728531282e9100789939Christian MaedermkStatusAttr = mkAttr "status"
86c119e3e74ba4b1b4ca728531282e9100789939Christian MaedermkProvenAttr :: Bool -> Attr
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedermkProvenAttr b = mkStatusAttr $ if b then "proven" else "open"
86c119e3e74ba4b1b4ca728531282e9100789939Christian MaederconsStatus :: ConsStatus -> [Element]
323a93847c763e3755391f953aa79985aed3417eChristian MaederconsStatus cs = case getConsOfStatus cs of
323a93847c763e3755391f953aa79985aed3417eChristian Maeder cStat -> [unode "ConsStatus" $ show cStat]
323a93847c763e3755391f953aa79985aed3417eChristian Maederledge :: HetcatsOpts -> GlobalAnnos -> DGraph -> LEdge DGLinkLab -> Element
323a93847c763e3755391f953aa79985aed3417eChristian Maederledge opts ga dg (f, t, lbl) = let
323a93847c763e3755391f953aa79985aed3417eChristian Maeder typ = dgl_type lbl
712f5e5ca1c3a5cfdd28518154ecf2dd0994cdb5Christian Maeder mor = gmorph opts ga $ dgl_morphism lbl
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder mkMor n = add_attr (mkAttr "morphismsource" $ getNameOfNode n dg) mor
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder lnkSt = case thmLinkStatus typ of
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder Nothing -> []
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder Just tls -> case tls of
712f5e5ca1c3a5cfdd28518154ecf2dd0994cdb5Christian Maeder LeftOpen -> []
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder Proven r ls -> dgrule r ++ map (\ e ->
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder add_attr (mkAttr "linkref" $ showEdgeId e)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder $ unode "ProofBasis" ()) (Set.toList $ proofBasis ls)
9737bb5d563d68e87ce8e38ca533388118d90d2dChristian Maeder ([ mkAttr "source" $ getNameOfNode f dg
9737bb5d563d68e87ce8e38ca533388118d90d2dChristian Maeder , mkAttr "target" $ getNameOfNode t dg
9737bb5d563d68e87ce8e38ca533388118d90d2dChristian Maeder , mkAttr "linkid" $ showEdgeId $ dgl_id lbl
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder ] ++ case dgl_origin lbl of
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder DGLinkView i _ ->
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder [mkNameAttr . iriToStringShortUnsecure $ setAngles False i]
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder $ unode "DGLink"
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder $ unode "Type" (getDGLinkType lbl) : lnkSt
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder ++ consStatus (getLinkConsStatus typ)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder ++ [case typ of
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder HidingFreeOrCofreeThm _ n _ _ -> mkMor n
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder FreeOrCofreeDefLink _ (JustNode ns) -> mkMor $ getNode ns
e05956d1da3c97e4d808926f97c6841c4a561991Christian Maederdgrule :: DGRule -> [Element]
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder unode "Rule" (dgRuleHeader r)
712f5e5ca1c3a5cfdd28518154ecf2dd0994cdb5Christian Maeder DGRuleLocalInference m ->
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder map (\ (s, t) -> add_attrs [mkNameAttr s, mkAttr "renamedTo" t]
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder $ unode "MovedTheorems" ()) m
aa60342b6a000c6798730e1b1ddeec846254c62cChristian Maeder Composition es -> map (\ e ->
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder add_attr (mkAttr "linkref" $ showEdgeId e)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder $ unode "Composition" ()) es
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder DGRuleWithEdge _ e ->
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder [ add_attr (mkAttr "linkref" $ showEdgeId e)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder $ unode "RuleTarget" () ]
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder-- | collects all symbols from dg and displays them as xml
86c119e3e74ba4b1b4ca728531282e9100789939Christian MaederdgSymbols :: DGraph -> Element
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaederdgSymbols dg = let ga = globalAnnos dg in unode "Ontologies"
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder $ map (\ (i, lbl) -> let ins = getImportNames dg i in
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder showSymbols ins ga lbl) $ labNodesDG dg
86c119e3e74ba4b1b4ca728531282e9100789939Christian MaedershowSymbols :: [String] -> GlobalAnnos -> DGNodeLab -> Element
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedershowSymbols ins ga lbl = showSymbolsTh ins (getDGNodeName lbl) ga
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder $ dgn_theory lbl
86c119e3e74ba4b1b4ca728531282e9100789939Christian MaedershowSymbolsTh :: [String] -> String -> GlobalAnnos -> G_theory -> Element
c0467970183fa3dc894edea3caf9ca05d3a09fa8Christian MaedershowSymbolsTh ins name ga th = case th of
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder G_theory lid _ (ExtSign sig _) _ sens _ -> add_attrs
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder [ mkAttr "logic" $ language_name lid
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder , mkNameAttr name ]
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder . unode "Ontology"
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder $ [ unode "Symbols" . map (showSym lid) $ symlist_of lid sig
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder , unode "Axioms" . map (showSen lid ga Nothing sig) $ toNamedList sens ]
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder ++ map (unode "Import") ins
86c119e3e74ba4b1b4ca728531282e9100789939Christian MaedershowSen :: ( GetRange sentence, Pretty sentence
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder , Sentences lid sentence sign morphism symbol) =>
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder lid -> GlobalAnnos -> Maybe Bool -> sign -> Named sentence -> Element
14b47f7dabb39996a31c7286810a5897587aed3aChristian MaedershowSen lid ga mt sig ns =
14b47f7dabb39996a31c7286810a5897587aed3aChristian Maeder let s = sentence ns in add_attrs
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder Nothing -> []
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder Just b -> [mkProvenAttr b]
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder ++ mkNameAttr (senAttr ns) : rangeAttrs (getRangeSpan s)
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder ++ case priority ns of
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder Just impo -> [mkPriorityAttr impo]
5d2f1a7947dde4ff340f8d4908ae0f22c74fdedaChristian Maeder . unode (if isJust mt then "Theorem" else "Axiom") $ unode "Text"
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder (show . useGlobalAnnos ga . print_named lid
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder . makeNamed "" $ simplify_sen lid sig s)
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder : map (showSym lid) (symsOfSen lid s)
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder ++ case senMark ns of
e289294500ad68fa0706b09521af340bbb356a69Christian Maeder m -> [unode "ComorphismOrigin" m]
14b47f7dabb39996a31c7286810a5897587aed3aChristian Maeder ++ [unode "AST" $ asXml s]
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaedershowSym :: (Sentences lid sentence sign morphism symbol) =>
da245da15da78363c896e44ea97a14ab1f83eb50Christian Maeder lid -> symbol -> Element
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaedershowSym lid s = add_attrs ((reverse
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder . maybe id ((:) . mkAttr "label") (sym_label lid s))
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder [ mkAttr "iri" $ fullSymName lid s
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder , mkNameAttr . show $ sym_name lid s
da245da15da78363c896e44ea97a14ab1f83eb50Christian Maeder , mkAttr "kind" $ symKind lid s
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder ]) $ prettySymbol emptyGlobalAnnos s