293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor{- |

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorModule : $Header$

fd9abdda70912b99b24e3bf1a38f26fde908a74cndDescription : xml output of Hets development graphs

fd9abdda70912b99b24e3bf1a38f26fde908a74cndCopyright : (c) Ewaryst Schulz, Uni Bremen 2009

fd9abdda70912b99b24e3bf1a38f26fde908a74cndLicense : GPLv2 or higher, see LICENSE.txt

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorMaintainer : Ewaryst.Schulz@dfki.de

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorStability : provisional

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorPortability : non-portable(Grothendieck)

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor

96ad5d81ee4a2cc66a4ae19893efc8aa6d06fae7jailletcXml of Hets DGs

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor-}

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowenmodule Static.ToXml

2e545ce2450a9953665f701bb05350f0d3f26275nd ( dGraph

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen , lnode

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen , dgSymbols

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor , showSymbols

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor , showSymbolsTh

af33a4994ae2ff15bc67d19ff1a7feb906745bf8rbowen ) where

3f08db06526d6901aa08c110b5bc7dde6bc39905nd

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport Driver.Options

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport Static.DgUtils

3f08db06526d6901aa08c110b5bc7dde6bc39905ndimport Static.DevGraph

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport Static.GTheory

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport Static.ComputeTheory (getImportNames)

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport Static.PrintDevGraph

f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjung

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport Logic.Prover

35ac4e1a6ec5aa3cfa1a34d8f20fe8a841cc46b7rbowenimport Logic.Logic

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport Logic.Comorphism

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport Logic.Grothendieck

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport Common.AS_Annotation

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport Common.ConvertGlobalAnnos

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport Common.Consistency

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport Common.DocUtils

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport Common.ExtSign

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport Common.GlobalAnnotations

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport Common.Id

35ac4e1a6ec5aa3cfa1a34d8f20fe8a841cc46b7rbowenimport Common.IRI

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport Common.LibName

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport qualified Common.OrderedMap as OMap

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport Common.Result

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport Common.ToXml

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor

30471a4650391f57975f60bbb6e4a90be7b284bfhumbedoohimport Text.XML.Light

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport Data.Graph.Inductive.Graph as Graph

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport Data.Maybe

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport qualified Data.Map as Map

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport qualified Data.Set as Set (toList)

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorimport Data.Char (toLower)

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor{- |

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorExport the development graph as xml. If the flag full is True then

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorsymbols for all nodes are shown as declarations, otherwise (the

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzordefault) only declaration for basic spec nodes are shown that are

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorsufficient to reconstruct the development from the xml output. -}

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzordGraph :: HetcatsOpts -> LibEnv -> LibName -> DGraph -> Element

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzordGraph full lenv ln dg =

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor let body = dgBody dg

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor ga = globalAnnos dg

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor lnodes = labNodes body

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor ledges = labEdges body

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor in add_attrs [ mkAttr "filename" $ getFilePath ln

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor , mkAttr "libname" . show $ setAnkles False $ getLibId ln

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor , mkAttr "dgnodes" . show $ length lnodes

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor , mkAttr "dgedges" . show $ length ledges

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor , mkAttr "nextlinkid" . showEdgeId $ getNewEdgeId dg ]

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor . unode "DGraph" $

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor subnodes "Global" (annotations ga . convertGlobalAnnos

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor $ removeHetCASLprefixes ga)

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor ++ map (lnode full ga lenv) lnodes

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor ++ map (ledge full ga dg) ledges

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorgmorph :: HetcatsOpts -> GlobalAnnos -> GMorphism -> Element

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor case map_sign cid ssig of

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor Result _ mr -> case mr of

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor Just (tsig, tsens) -> let

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor tid = targetLogic cid

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor in add_attr (mkNameAttr $ language_name cid)

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor $ unode "GMorphism" $

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

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

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor -> Element

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorprettyRangeElem s ga a =

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorprettySymbol = prettyRangeElem "Symbol"

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorlnode :: HetcatsOpts -> GlobalAnnos -> LibEnv -> LNode DGNodeLab -> Element

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorlnode full ga lenv (_, lbl) =

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor let nm = dgn_name lbl

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

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor l -> ("?", showXPath l)

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor in add_attrs (mkNameAttr (showName nm)

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor : mkAttr "reference" (map toLower $ show $ isDGRef lbl)

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor : case signOf $ dgn_theory lbl of

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

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

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor else [])

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor $ unode "DGNode"

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor $ case nodeInfo lbl of

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor DGRef li rf ->

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor [ add_attrs

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor [ mkAttr "library" $ show $ setAnkles False $ getLibId li

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor , mkAttr "location" $ getFilePath li

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor $ unode "Reference" () ]

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

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor subnodes "Declarations"

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor $ map (showSym lid)

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor $ mostSymsOf lid dsig

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor DGRestriction _ hidSyms -> subnodes "Hidden"

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor $ map (prettySymbol ga)

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor $ Set.toList hidSyms

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor _ -> []

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor ++ case dgn_theory lbl of

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

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor (if fullSign full

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor else [])

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor ++ subnodes "Axioms"

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor ++ subnodes "Theorems"

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

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor $ OMap.toList thms)

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor ++ if fullTheories full then case globalTheory lbl of

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor coerceThSens glid lid "xml-lnode" allSens of

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor Just gsens -> subnodes "ImpAxioms"

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor $ map (showSen lid ga Nothing sig) $ toNamedList

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor $ OMap.filter ((`notElem` map sentence

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor (OMap.elems thsens)) . sentence) gsens

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor _ -> []

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor _ -> []

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor else []

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzormkStatusAttr :: String -> Attr

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzormkStatusAttr = mkAttr "status"

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzormkProvenAttr :: Bool -> Attr

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzormkProvenAttr b = mkStatusAttr $ if b then "proven" else "open"

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorconsStatus :: ConsStatus -> [Element]

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorconsStatus cs = case getConsOfStatus cs of

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor None -> []

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorledge :: HetcatsOpts -> GlobalAnnos -> DGraph -> LEdge DGLinkLab -> Element

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorledge opts ga dg (f, t, lbl) = let

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor typ = dgl_type lbl

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor mor = gmorph opts ga $ dgl_morphism lbl

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor lnkSt = case thmLinkStatus typ of

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor Nothing -> []

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor Just tls -> case tls of

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor LeftOpen -> []

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor add_attr (mkAttr "linkref" $ showEdgeId e)

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor in add_attrs

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor ([ mkAttr "source" $ getNameOfNode f dg

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor , mkAttr "target" $ getNameOfNode t dg

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor , mkAttr "linkid" $ showEdgeId $ dgl_id lbl

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor ] ++ case dgl_origin lbl of

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor DGLinkView i _ ->

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor [mkNameAttr . iriToStringShortUnsecure $ setAnkles False i]

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor _ -> [])

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor $ unode "DGLink"

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor $ unode "Type" (getDGLinkType lbl) : lnkSt

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor ++ consStatus (getLinkConsStatus typ)

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor ++ [case typ of

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor HidingFreeOrCofreeThm _ n _ _ -> mkMor n

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor _ -> mor]

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzordgrule :: DGRule -> [Element]

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzordgrule r =

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor unode "Rule" (dgRuleHeader r)

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor : case r of

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor DGRuleLocalInference m ->

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor $ unode "MovedTheorems" ()) m

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor Composition es -> map (\ e ->

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor add_attr (mkAttr "linkref" $ showEdgeId e)

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor $ unode "Composition" ()) es

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor DGRuleWithEdge _ e ->

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor [ add_attr (mkAttr "linkref" $ showEdgeId e)

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor $ unode "RuleTarget" () ]

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor _ -> []

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzordgSymbols :: DGraph -> Element

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzordgSymbols dg = let ga = globalAnnos dg in unode "Ontologies"

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor showSymbols ins ga lbl) $ labNodesDG dg

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorshowSymbols :: [String] -> GlobalAnnos -> DGNodeLab -> Element

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorshowSymbols ins ga lbl = showSymbolsTh ins (getDGNodeName lbl) ga

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor $ dgn_theory lbl

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorshowSymbolsTh :: [String] -> String -> GlobalAnnos -> G_theory -> Element

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorshowSymbolsTh ins name ga th = case th of

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor [ mkAttr "logic" $ language_name lid

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor , mkNameAttr name ]

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor . unode "Ontology"

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

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor ++ map (unode "Import") ins

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorshowSen :: ( GetRange sentence, Pretty sentence

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor , Sentences lid sentence sign morphism symbol) =>

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorshowSen lid ga mt sig ns = let s = sentence ns in add_attrs

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor (case mt of

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor Nothing -> []

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor Just b -> [mkProvenAttr b]

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

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

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor (show . useGlobalAnnos ga . print_named lid

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor . makeNamed "" $ simplify_sen lid sig s)

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor : map (showSym lid) (symsOfSen lid s)

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorshowSym :: (Sentences lid sentence sign morphism symbol) =>

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor lid -> symbol -> Element

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzorshowSym lid s = add_attrs

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor [ mkAttr "kind" $ symKind lid s

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor , mkNameAttr . show $ sym_name lid s ]

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor $ prettySymbol emptyGlobalAnnos s

293aa6caecb1db771e9baa2f79c92f1c381caee4gryzor