67f0eb92a02309cd70d9c9691a94d96d70cd0b85Christian Maeder{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$

c8a9d35be2207e0d4fbd26a2411e1ba17e3e4c96Christian MaederDescription : xml output of Hets development graphs

67f0eb92a02309cd70d9c9691a94d96d70cd0b85Christian MaederCopyright : (c) Ewaryst Schulz, Uni Bremen 2009

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt

67f0eb92a02309cd70d9c9691a94d96d70cd0b85Christian MaederMaintainer : Ewaryst.Schulz@dfki.de

1d581e55c7ec020a445684310394c3a5fc056e96Christian MaederStability : provisional

67f0eb92a02309cd70d9c9691a94d96d70cd0b85Christian MaederPortability : non-portable(Grothendieck)

c8a9d35be2207e0d4fbd26a2411e1ba17e3e4c96Christian Maeder

67f0eb92a02309cd70d9c9691a94d96d70cd0b85Christian MaederXml of Hets DGs

c8a9d35be2207e0d4fbd26a2411e1ba17e3e4c96Christian Maeder-}

ffb20d566649ab4ce80c225a791c44d8b8487492Hendrik Iben

ffb20d566649ab4ce80c225a791c44d8b8487492Hendrik Ibenmodule Static.ToXml

c8a9d35be2207e0d4fbd26a2411e1ba17e3e4c96Christian Maeder ( dGraph

ffb20d566649ab4ce80c225a791c44d8b8487492Hendrik Iben , lnode

f4f87c3db7dcb604833cb7813475dcb1313013b3Christian Maeder , dgSymbols

f4f87c3db7dcb604833cb7813475dcb1313013b3Christian Maeder , showSymbols

773a3d8e40d41417d7c7c92c65c9ff1e49f66ce2Christian Maeder , showSymbolsTh

67f0eb92a02309cd70d9c9691a94d96d70cd0b85Christian Maeder ) where

ffb20d566649ab4ce80c225a791c44d8b8487492Hendrik Iben

ffb20d566649ab4ce80c225a791c44d8b8487492Hendrik Ibenimport Driver.Options

367103718689f8d3aa1a8648eba9e50af51c3a94Florian Mossakowski

adaf5a640e615848c19de372218377a418f954ceFlorian Mossakowskiimport Static.DgUtils

67f0eb92a02309cd70d9c9691a94d96d70cd0b85Christian Maederimport Static.DevGraph

67f0eb92a02309cd70d9c9691a94d96d70cd0b85Christian Maederimport Static.GTheory

86d9bb76813208a0855c899a21e5ffca3ad1aa38Christian Maederimport Static.ComputeTheory (getImportNames)

67f0eb92a02309cd70d9c9691a94d96d70cd0b85Christian Maederimport Static.PrintDevGraph

c8a9d35be2207e0d4fbd26a2411e1ba17e3e4c96Christian Maeder

adaf5a640e615848c19de372218377a418f954ceFlorian Mossakowskiimport Logic.Prover

f4f87c3db7dcb604833cb7813475dcb1313013b3Christian Maederimport Logic.Logic

f4f87c3db7dcb604833cb7813475dcb1313013b3Christian Maederimport Logic.Comorphism

67f0eb92a02309cd70d9c9691a94d96d70cd0b85Christian Maederimport Logic.Grothendieck

367103718689f8d3aa1a8648eba9e50af51c3a94Florian Mossakowski

f4f87c3db7dcb604833cb7813475dcb1313013b3Christian Maederimport Common.AS_Annotation

367103718689f8d3aa1a8648eba9e50af51c3a94Florian Mossakowskiimport Common.ConvertGlobalAnnos

367103718689f8d3aa1a8648eba9e50af51c3a94Florian Mossakowskiimport Common.Consistency

67f0eb92a02309cd70d9c9691a94d96d70cd0b85Christian Maederimport Common.DocUtils

67f0eb92a02309cd70d9c9691a94d96d70cd0b85Christian Maederimport Common.ExtSign

67f0eb92a02309cd70d9c9691a94d96d70cd0b85Christian Maederimport Common.GlobalAnnotations

5c09a5b695699a46a95795259a7bcbba60aea3bdHendrik Ibenimport Common.Id

67f0eb92a02309cd70d9c9691a94d96d70cd0b85Christian Maederimport Common.IRI

67f0eb92a02309cd70d9c9691a94d96d70cd0b85Christian Maederimport Common.LibName

ffb20d566649ab4ce80c225a791c44d8b8487492Hendrik Ibenimport qualified Common.OrderedMap as OMap

adaf5a640e615848c19de372218377a418f954ceFlorian Mossakowskiimport Common.Result

adaf5a640e615848c19de372218377a418f954ceFlorian Mossakowskiimport Common.ToXml

67f0eb92a02309cd70d9c9691a94d96d70cd0b85Christian Maeder

67f0eb92a02309cd70d9c9691a94d96d70cd0b85Christian Maederimport Text.XML.Light

ffb20d566649ab4ce80c225a791c44d8b8487492Hendrik Iben

adaf5a640e615848c19de372218377a418f954ceFlorian Mossakowskiimport Data.Graph.Inductive.Graph as Graph

773a3d8e40d41417d7c7c92c65c9ff1e49f66ce2Christian Maederimport Data.Maybe

67f0eb92a02309cd70d9c9691a94d96d70cd0b85Christian Maederimport qualified Data.Map as Map

67f0eb92a02309cd70d9c9691a94d96d70cd0b85Christian Maederimport qualified Data.Set as Set (toList)

adaf5a640e615848c19de372218377a418f954ceFlorian Mossakowskiimport Data.Char (toLower)

adaf5a640e615848c19de372218377a418f954ceFlorian Mossakowski

86d9bb76813208a0855c899a21e5ffca3ad1aa38Christian Maeder{- |

adaf5a640e615848c19de372218377a418f954ceFlorian MossakowskiExport the development graph as xml. If the flag full is True then

86d9bb76813208a0855c899a21e5ffca3ad1aa38Christian Maedersymbols for all nodes are shown as declarations, otherwise (the

f4f87c3db7dcb604833cb7813475dcb1313013b3Christian Maederdefault) only declaration for basic spec nodes are shown that are

367103718689f8d3aa1a8648eba9e50af51c3a94Florian Mossakowskisufficient to reconstruct the development from the xml output. -}

367103718689f8d3aa1a8648eba9e50af51c3a94Florian MossakowskidGraph :: HetcatsOpts -> LibEnv -> LibName -> DGraph -> Element

773a3d8e40d41417d7c7c92c65c9ff1e49f66ce2Christian MaederdGraph full lenv ln dg =

adaf5a640e615848c19de372218377a418f954ceFlorian Mossakowski let body = dgBody dg

ffb20d566649ab4ce80c225a791c44d8b8487492Hendrik Iben ga = globalAnnos dg

ffb20d566649ab4ce80c225a791c44d8b8487492Hendrik Iben lnodes = labNodes body

ffb20d566649ab4ce80c225a791c44d8b8487492Hendrik Iben ledges = labEdges body

67f0eb92a02309cd70d9c9691a94d96d70cd0b85Christian Maeder in add_attrs [ mkAttr "filename" $ getFilePath ln

67f0eb92a02309cd70d9c9691a94d96d70cd0b85Christian Maeder , mkAttr "mime-type" . fromMaybe "unknown" $ mimeType ln

d34c6711bc746459074986c06f7c28b083b4be2fChristian Maeder , mkAttr "libname" . show $ setAngles False $ getLibId ln

5c09a5b695699a46a95795259a7bcbba60aea3bdHendrik Iben , mkAttr "dgnodes" . show $ length lnodes

c8a9d35be2207e0d4fbd26a2411e1ba17e3e4c96Christian Maeder , mkAttr "dgedges" . show $ length ledges

ffb20d566649ab4ce80c225a791c44d8b8487492Hendrik Iben , mkAttr "nextlinkid" . showEdgeId $ getNewEdgeId dg ]

6dcb974e3ccdbc9bcd013a5a923f87069a65e09fFlorian Mossakowski . unode "DGraph" $

c8a9d35be2207e0d4fbd26a2411e1ba17e3e4c96Christian Maeder subnodes "Global" (annotations ga . convertGlobalAnnos

$ removeHetCASLprefixes ga)

++ map (lnode full ga lenv) lnodes

++ map (ledge full ga dg) ledges

gmorph :: HetcatsOpts -> GlobalAnnos -> GMorphism -> Element

gmorph opts ga gm@(GMorphism cid (ExtSign ssig _) _ tmor _) =

case map_sign cid ssig of

Result _ mr -> case mr of

Nothing -> error $ "Static.ToXml.gmorph: " ++ showGlobalDoc ga gm ""

Just (tsig, tsens) -> let

tid = targetLogic cid

sl = Map.toList . Map.filterWithKey (/=) $ symmap_of tid tmor

in add_attr (mkNameAttr $ language_name cid)

$ unode "GMorphism" $

(if fullTheories opts then [] else subnodes "ComorphismAxioms"

$ map (showSen (targetLogic cid) ga Nothing tsig) tsens)

++ map (\ (s, t) -> unode "map" [showSym tid s, showSym tid t]) sl

prettyRangeElem :: (GetRange a, Pretty a) => String -> GlobalAnnos -> a

-> Element

prettyRangeElem s ga a =

add_attrs (rangeAttrs $ getRangeSpan a) $ prettyElem s ga a

prettySymbol :: (GetRange a, Pretty a) => GlobalAnnos -> a -> Element

prettySymbol = prettyRangeElem "Symbol"

lnode :: HetcatsOpts -> GlobalAnnos -> LibEnv -> LNode DGNodeLab -> Element

lnode full ga lenv (_, lbl) =

let nm = dgn_name lbl

(spn, xp) = case reverse $ xpath nm of

ElemName s : t -> (s, showXPath t)

l -> ("?", showXPath l)

in add_attrs (mkNameAttr (showName nm)

: rangeAttrs (srcRange nm)

++ mkAttr "reference" (map toLower $ show $ isDGRef lbl)

: case signOf $ dgn_theory lbl of

G_sign slid _ _ -> mkAttr "logic" (show slid)

: if not (isDGRef lbl) && dgn_origin lbl < DGProof then

[mkAttr "refname" spn, mkAttr "relxpath" xp ]

else [])

$ unode "DGNode"

$ case nodeInfo lbl of

DGRef li rf ->

[ add_attrs

[ mkAttr "library" $ show $ setAngles False $ getLibId li

, mkAttr "location" $ getFilePath li

, mkAttr "node" $ getNameOfNode rf $ lookupDGraph li lenv ]

$ unode "Reference" () ]

DGNode orig cs -> consStatus cs ++ case orig of

DGBasicSpec _ (G_sign lid (ExtSign dsig _) _) _ ->

subnodes "Declarations"

$ map (showSym lid)

$ mostSymsOf lid dsig

DGRestriction _ hidSyms -> subnodes "Hidden"

$ map (prettySymbol ga)

$ Set.toList hidSyms

_ -> []

++ case dgn_theory lbl of

G_theory lid _ (ExtSign sig _) _ thsens _ -> let

(axs, thms) = OMap.partition isAxiom thsens in

(if fullSign full

then subnodes "Symbols" (map (showSym lid) $ symlist_of lid sig)

else [])

++ subnodes "Axioms"

(map (showSen lid ga Nothing sig) $ toNamedList axs)

++ subnodes "Theorems"

(map (\ (s, t) -> showSen lid ga

(Just $ isProvenSenStatus t) sig $ toNamed s t)

$ OMap.toList thms)

++ if fullTheories full then case globalTheory lbl of

Just (G_theory glid _ _ _ allSens _) -> case

coerceThSens glid lid "xml-lnode" allSens of

Just gsens -> subnodes "ImpAxioms"

$ map (showSen lid ga Nothing sig) $ toNamedList

$ OMap.filter ((`notElem` map sentence

(OMap.elems thsens)) . sentence) gsens

_ -> []

_ -> []

else []

-- | a status may be open, proven or outdated

mkStatusAttr :: String -> Attr

mkStatusAttr = mkAttr "status"

mkProvenAttr :: Bool -> Attr

mkProvenAttr b = mkStatusAttr $ if b then "proven" else "open"

consStatus :: ConsStatus -> [Element]

consStatus cs = case getConsOfStatus cs of

None -> []

cStat -> [unode "ConsStatus" $ show cStat]

ledge :: HetcatsOpts -> GlobalAnnos -> DGraph -> LEdge DGLinkLab -> Element

ledge opts ga dg (f, t, lbl) = let

typ = dgl_type lbl

mor = gmorph opts ga $ dgl_morphism lbl

mkMor n = add_attr (mkAttr "morphismsource" $ getNameOfNode n dg) mor

lnkSt = case thmLinkStatus typ of

Nothing -> []

Just tls -> case tls of

LeftOpen -> []

Proven r ls -> dgrule r ++ map (\ e ->

add_attr (mkAttr "linkref" $ showEdgeId e)

$ unode "ProofBasis" ()) (Set.toList $ proofBasis ls)

in add_attrs

([ mkAttr "source" $ getNameOfNode f dg

, mkAttr "target" $ getNameOfNode t dg

, mkAttr "linkid" $ showEdgeId $ dgl_id lbl

] ++ case dgl_origin lbl of

DGLinkView i _ ->

[mkNameAttr . iriToStringShortUnsecure $ setAngles False i]

_ -> [])

$ unode "DGLink"

$ unode "Type" (getDGLinkType lbl) : lnkSt

++ consStatus (getLinkConsStatus typ)

++ [case typ of

HidingFreeOrCofreeThm _ n _ _ -> mkMor n

FreeOrCofreeDefLink _ (JustNode ns) -> mkMor $ getNode ns

_ -> mor]

dgrule :: DGRule -> [Element]

dgrule r =

unode "Rule" (dgRuleHeader r)

: case r of

DGRuleLocalInference m ->

map (\ (s, t) -> add_attrs [mkNameAttr s, mkAttr "renamedTo" t]

$ unode "MovedTheorems" ()) m

Composition es -> map (\ e ->

add_attr (mkAttr "linkref" $ showEdgeId e)

$ unode "Composition" ()) es

DGRuleWithEdge _ e ->

[ add_attr (mkAttr "linkref" $ showEdgeId e)

$ unode "RuleTarget" () ]

_ -> []

-- | collects all symbols from dg and displays them as xml

dgSymbols :: DGraph -> Element

dgSymbols dg = let ga = globalAnnos dg in unode "Ontologies"

$ map (\ (i, lbl) -> let ins = getImportNames dg i in

showSymbols ins ga lbl) $ labNodesDG dg

showSymbols :: [String] -> GlobalAnnos -> DGNodeLab -> Element

showSymbols ins ga lbl = showSymbolsTh ins (getDGNodeName lbl) ga

$ dgn_theory lbl

showSymbolsTh :: [String] -> String -> GlobalAnnos -> G_theory -> Element

showSymbolsTh ins name ga th = case th of

G_theory lid _ (ExtSign sig _) _ sens _ -> add_attrs

[ mkAttr "logic" $ language_name lid

, mkNameAttr name ]

. unode "Ontology"

$ [ unode "Symbols" . map (showSym lid) $ symlist_of lid sig

, unode "Axioms" . map (showSen lid ga Nothing sig) $ toNamedList sens ]

++ map (unode "Import") ins

showSen :: ( GetRange sentence, Pretty sentence

, Sentences lid sentence sign morphism symbol) =>

lid -> GlobalAnnos -> Maybe Bool -> sign -> Named sentence -> Element

showSen lid ga mt sig ns = let s = sentence ns in add_attrs

(case mt of

Nothing -> []

Just b -> [mkProvenAttr b]

++ mkNameAttr (senAttr ns) : rangeAttrs (getRangeSpan s))

. unode (if isJust mt then "Theorem" else "Axiom") $ unode "Text"

(show . useGlobalAnnos ga . print_named lid

. makeNamed "" $ simplify_sen lid sig s)

: map (showSym lid) (symsOfSen lid s)

++ case senMark ns of

"" -> []

m -> [unode "ComorphismOrigin" m]

++ [unode "AST" $ asXml s]

showSym :: (Sentences lid sentence sign morphism symbol) =>

lid -> symbol -> Element

showSym lid s = add_attrs ((reverse

. maybe id ((:) . mkAttr "label") (sym_label lid s))

[ mkAttr "iri" $ fullSymName lid s

, mkNameAttr . show $ sym_name lid s

, mkAttr "kind" $ symKind lid s

]) $ prettySymbol emptyGlobalAnnos s