{- |
Module      :  ./Static/ToXml.hs
Description :  xml output of Hets development graphs
Copyright   :  (c) Ewaryst Schulz, Uni Bremen 2009
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  Ewaryst.Schulz@dfki.de
Stability   :  provisional
Portability :  non-portable(Grothendieck)

Xml of Hets DGs
-}

module Static.ToXml
  ( dGraph
  , lnode
  , dgSymbols
  , showSymbols
  , showSymbolsTh
  ) where

import Driver.Options

import Static.DgUtils
import Static.DevGraph
import Static.GTheory
import Static.ComputeTheory (getImportNames)
import Static.PrintDevGraph

import Logic.Prover
import Logic.Logic
import Logic.Comorphism
import Logic.Grothendieck

import Common.AS_Annotation
import Common.ConvertGlobalAnnos
import Common.Consistency
import Common.DocUtils
import Common.ExtSign
import Common.GlobalAnnotations
import Common.Id
import Common.IRI
import Common.LibName
import qualified Common.OrderedMap as OMap
import Common.Result
import Common.ToXml

import Text.XML.Light

import Data.Graph.Inductive.Graph as Graph
import Data.Maybe
import qualified Data.Map as Map
import qualified Data.Set as Set (toList)
import Data.Char (toLower)

{- |
Export the development graph as xml. If the flag full is True then
symbols for all nodes are shown as declarations, otherwise (the
default) only declaration for basic spec nodes are shown that are
sufficient to reconstruct the development from the xml output. -}
dGraph :: HetcatsOpts -> LibEnv -> LibName -> DGraph -> Element
dGraph :: HetcatsOpts -> LibEnv -> LibName -> DGraph -> Element
dGraph opts :: HetcatsOpts
opts lenv :: LibEnv
lenv ln :: LibName
ln dg :: DGraph
dg =
  let body :: Gr DGNodeLab DGLinkLab
body = DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg
      ga :: GlobalAnnos
ga = DGraph -> GlobalAnnos
globalAnnos DGraph
dg
      lnodes :: [LNode DGNodeLab]
lnodes = Gr DGNodeLab DGLinkLab -> [LNode DGNodeLab]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr DGNodeLab DGLinkLab
body
      ledges :: [LEdge DGLinkLab]
ledges = Gr DGNodeLab DGLinkLab -> [LEdge DGLinkLab]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges Gr DGNodeLab DGLinkLab
body
  in [Attr] -> Element -> Element
add_attrs [ String -> String -> Attr
mkAttr "filename" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ LibName -> String
getFilePath LibName
ln
               , String -> String -> Attr
mkAttr "mime-type" (String -> Attr)
-> (Maybe String -> String) -> Maybe String -> Attr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe "unknown" (Maybe String -> Attr) -> Maybe String -> Attr
forall a b. (a -> b) -> a -> b
$ LibName -> Maybe String
mimeType LibName
ln
               , String -> String -> Attr
mkAttr "libname" (String -> Attr) -> (IRI -> String) -> IRI -> Attr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> String
forall a. Show a => a -> String
show (IRI -> Attr) -> IRI -> Attr
forall a b. (a -> b) -> a -> b
$ Bool -> IRI -> IRI
setAngles Bool
False (IRI -> IRI) -> IRI -> IRI
forall a b. (a -> b) -> a -> b
$ LibName -> IRI
getLibId LibName
ln
               , String -> String -> Attr
mkAttr "dgnodes" (String -> Attr) -> (Int -> String) -> Int -> Attr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show (Int -> Attr) -> Int -> Attr
forall a b. (a -> b) -> a -> b
$ [LNode DGNodeLab] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [LNode DGNodeLab]
lnodes
               , String -> String -> Attr
mkAttr "dgedges" (String -> Attr) -> (Int -> String) -> Int -> Attr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show (Int -> Attr) -> Int -> Attr
forall a b. (a -> b) -> a -> b
$ [LEdge DGLinkLab] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [LEdge DGLinkLab]
ledges
               , String -> String -> Attr
mkAttr "nextlinkid" (String -> Attr) -> (EdgeId -> String) -> EdgeId -> Attr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EdgeId -> String
showEdgeId (EdgeId -> Attr) -> EdgeId -> Attr
forall a b. (a -> b) -> a -> b
$ DGraph -> EdgeId
getNewEdgeId DGraph
dg ]
     (Element -> Element)
-> ([Element] -> Element) -> [Element] -> Element
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "DGraph" ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$
         String -> [Element] -> [Element]
subnodes "Global" (GlobalAnnos -> [Annotation] -> [Element]
annotations GlobalAnnos
ga ([Annotation] -> [Element])
-> (GlobalAnnos -> [Annotation]) -> GlobalAnnos -> [Element]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalAnnos -> [Annotation]
convertGlobalAnnos
                            (GlobalAnnos -> [Element]) -> GlobalAnnos -> [Element]
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> GlobalAnnos
removeDOLprefixes GlobalAnnos
ga)
         [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ (LNode DGNodeLab -> Element) -> [LNode DGNodeLab] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (HetcatsOpts -> GlobalAnnos -> LibEnv -> LNode DGNodeLab -> Element
lnode HetcatsOpts
opts GlobalAnnos
ga LibEnv
lenv) [LNode DGNodeLab]
lnodes
         [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ (LEdge DGLinkLab -> Element) -> [LEdge DGLinkLab] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (HetcatsOpts -> GlobalAnnos -> DGraph -> LEdge DGLinkLab -> Element
ledge HetcatsOpts
opts GlobalAnnos
ga DGraph
dg) [LEdge DGLinkLab]
ledges

gmorph :: HetcatsOpts -> GlobalAnnos -> GMorphism -> Element
gmorph :: HetcatsOpts -> GlobalAnnos -> GMorphism -> Element
gmorph opts :: HetcatsOpts
opts ga :: GlobalAnnos
ga gm :: GMorphism
gm@(GMorphism cid :: cid
cid (ExtSign ssig :: sign1
ssig _) _ tmor :: morphism2
tmor _) =
  case cid -> sign1 -> Result (sign2, [Named sentence2])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> sign1 -> Result (sign2, [Named sentence2])
map_sign cid
cid sign1
ssig of
    Result _ mr :: Maybe (sign2, [Named sentence2])
mr -> case Maybe (sign2, [Named sentence2])
mr of
      Nothing -> String -> Element
forall a. HasCallStack => String -> a
error (String -> Element) -> String -> Element
forall a b. (a -> b) -> a -> b
$ "Static.ToXml.gmorph: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ GlobalAnnos -> GMorphism -> String -> String
forall a. Pretty a => GlobalAnnos -> a -> String -> String
showGlobalDoc GlobalAnnos
ga GMorphism
gm ""
      Just (tsig :: sign2
tsig, tsens :: [Named sentence2]
tsens) -> let
        tid :: lid2
tid = cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid
        sl :: [(symbol2, symbol2)]
sl = Map symbol2 symbol2 -> [(symbol2, symbol2)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map symbol2 symbol2 -> [(symbol2, symbol2)])
-> (Map symbol2 symbol2 -> Map symbol2 symbol2)
-> Map symbol2 symbol2
-> [(symbol2, symbol2)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (symbol2 -> symbol2 -> Bool)
-> Map symbol2 symbol2 -> Map symbol2 symbol2
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey symbol2 -> symbol2 -> Bool
forall a. Eq a => a -> a -> Bool
(/=) (Map symbol2 symbol2 -> [(symbol2, symbol2)])
-> Map symbol2 symbol2 -> [(symbol2, symbol2)]
forall a b. (a -> b) -> a -> b
$ lid2 -> morphism2 -> Map symbol2 symbol2
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> morphism -> EndoMap symbol
symmap_of lid2
tid morphism2
tmor
        in Attr -> Element -> Element
add_attr (String -> Attr
mkNameAttr (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid)
           (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "GMorphism" ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$
             (if HetcatsOpts -> Bool
fullTheories HetcatsOpts
opts then [] else String -> [Element] -> [Element]
subnodes "ComorphismAxioms"
             ([Element] -> [Element]) -> [Element] -> [Element]
forall a b. (a -> b) -> a -> b
$ (Named sentence2 -> Element) -> [Named sentence2] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (HetcatsOpts
-> lid2
-> GlobalAnnos
-> Maybe Bool
-> sign2
-> Named sentence2
-> Element
forall sentence lid sign morphism symbol.
(GetRange sentence, Pretty sentence,
 Sentences lid sentence sign morphism symbol) =>
HetcatsOpts
-> lid
-> GlobalAnnos
-> Maybe Bool
-> sign
-> Named sentence
-> Element
showSen HetcatsOpts
opts (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid) GlobalAnnos
ga Maybe Bool
forall a. Maybe a
Nothing sign2
tsig) [Named sentence2]
tsens)
             [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ ((symbol2, symbol2) -> Element)
-> [(symbol2, symbol2)] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: symbol2
s, t :: symbol2
t) -> String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "map" [lid2 -> symbol2 -> Element
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> Element
showSym lid2
tid symbol2
s, lid2 -> symbol2 -> Element
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> Element
showSym lid2
tid symbol2
t]) [(symbol2, symbol2)]
sl

prettyRangeElem :: (GetRange a, Pretty a) => String -> GlobalAnnos -> a
                -> Element
prettyRangeElem :: String -> GlobalAnnos -> a -> Element
prettyRangeElem s :: String
s ga :: GlobalAnnos
ga a :: a
a =
  [Attr] -> Element -> Element
add_attrs (Range -> [Attr]
rangeAttrs (Range -> [Attr]) -> Range -> [Attr]
forall a b. (a -> b) -> a -> b
$ a -> Range
forall a. GetRange a => a -> Range
getRangeSpan a
a) (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> GlobalAnnos -> a -> Element
forall a. Pretty a => String -> GlobalAnnos -> a -> Element
prettyElem String
s GlobalAnnos
ga a
a

prettySymbol :: (GetRange a, Pretty a) => GlobalAnnos -> a -> Element
prettySymbol :: GlobalAnnos -> a -> Element
prettySymbol = String -> GlobalAnnos -> a -> Element
forall a.
(GetRange a, Pretty a) =>
String -> GlobalAnnos -> a -> Element
prettyRangeElem "Symbol"

lnode :: HetcatsOpts -> GlobalAnnos -> LibEnv -> LNode DGNodeLab -> Element
lnode :: HetcatsOpts -> GlobalAnnos -> LibEnv -> LNode DGNodeLab -> Element
lnode opts :: HetcatsOpts
opts ga :: GlobalAnnos
ga lenv :: LibEnv
lenv (nodeId :: Int
nodeId, lbl :: DGNodeLab
lbl) =
  let nm :: NodeName
nm = DGNodeLab -> NodeName
dgn_name DGNodeLab
lbl
      (spn :: String
spn, xp :: String
xp) = case [XPathPart] -> [XPathPart]
forall a. [a] -> [a]
reverse ([XPathPart] -> [XPathPart]) -> [XPathPart] -> [XPathPart]
forall a b. (a -> b) -> a -> b
$ NodeName -> [XPathPart]
xpath NodeName
nm of
          ElemName s :: String
s : t :: [XPathPart]
t -> (String
s, [XPathPart] -> String
showXPath [XPathPart]
t)
          l :: [XPathPart]
l -> ("?", [XPathPart] -> String
showXPath [XPathPart]
l)
  in [Attr] -> Element -> Element
add_attrs (String -> Attr
mkNameAttr (NodeName -> String
showName NodeName
nm)
    Attr -> [Attr] -> [Attr]
forall a. a -> [a] -> [a]
: Range -> [Attr]
rangeAttrs (NodeName -> Range
srcRange NodeName
nm)
    [Attr] -> [Attr] -> [Attr]
forall a. [a] -> [a] -> [a]
++ [String -> String -> Attr
mkAttr "id" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
nodeId]
    [Attr] -> [Attr] -> [Attr]
forall a. [a] -> [a] -> [a]
++ [String -> String -> Attr
mkAttr "internal" ((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Bool -> String
forall a. Show a => a -> String
show (Bool -> String) -> Bool -> String
forall a b. (a -> b) -> a -> b
$ NodeName -> Bool
isInternal NodeName
nm)]
    [Attr] -> [Attr] -> [Attr]
forall a. [a] -> [a] -> [a]
++ String -> String -> Attr
mkAttr "reference" ((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Bool -> String
forall a. Show a => a -> String
show (Bool -> String) -> Bool -> String
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> Bool
isDGRef DGNodeLab
lbl)
    Attr -> [Attr] -> [Attr]
forall a. a -> [a] -> [a]
: case G_theory -> G_sign
signOf (G_theory -> G_sign) -> G_theory -> G_sign
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> G_theory
dgn_theory DGNodeLab
lbl of
        G_sign slid :: lid
slid _ _ -> String -> String -> Attr
mkAttr "logic" (lid -> String
forall a. Show a => a -> String
show lid
slid)
          Attr -> [Attr] -> [Attr]
forall a. a -> [a] -> [a]
: if Bool -> Bool
not (DGNodeLab -> Bool
isDGRef DGNodeLab
lbl) Bool -> Bool -> Bool
&& DGNodeLab -> DGOrigin
dgn_origin DGNodeLab
lbl DGOrigin -> DGOrigin -> Bool
forall a. Ord a => a -> a -> Bool
< DGOrigin
DGProof then
             [String -> String -> Attr
mkAttr "refname" String
spn, String -> String -> Attr
mkAttr "relxpath" String
xp ]
            else [])
  (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "DGNode"
    ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ case DGNodeLab -> DGNodeInfo
nodeInfo DGNodeLab
lbl of
          DGRef li :: LibName
li rf :: Int
rf ->
            [ [Attr] -> Element -> Element
add_attrs
              [ String -> String -> Attr
mkAttr "library" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ IRI -> String
forall a. Show a => a -> String
show (IRI -> String) -> IRI -> String
forall a b. (a -> b) -> a -> b
$ Bool -> IRI -> IRI
setAngles Bool
False (IRI -> IRI) -> IRI -> IRI
forall a b. (a -> b) -> a -> b
$ LibName -> IRI
getLibId LibName
li
              , String -> String -> Attr
mkAttr "location" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ LibName -> String
getFilePath LibName
li
              , String -> String -> Attr
mkAttr "node" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ Int -> DGraph -> String
getNameOfNode Int
rf (DGraph -> String) -> DGraph -> String
forall a b. (a -> b) -> a -> b
$ LibName -> LibEnv -> DGraph
lookupDGraph LibName
li LibEnv
lenv ]
            (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> () -> Element
forall t. Node t => String -> t -> Element
unode "Reference" () ]
          DGNode orig :: DGOrigin
orig cs :: ConsStatus
cs -> ConsStatus -> [Element]
consStatus ConsStatus
cs [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ case DGOrigin
orig of
                   DGBasicSpec _ (G_sign lid :: lid
lid (ExtSign dsig :: sign
dsig _) _) _ ->
                     String -> [Element] -> [Element]
subnodes "Declarations"
                       ([Element] -> [Element]) -> [Element] -> [Element]
forall a b. (a -> b) -> a -> b
$ (symbol -> Element) -> [symbol] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (lid -> symbol -> Element
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> Element
showSym lid
lid)
                       ([symbol] -> [Element]) -> [symbol] -> [Element]
forall a b. (a -> b) -> a -> b
$ lid -> sign -> [symbol]
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> [symbol]
mostSymsOf lid
lid sign
dsig
                   DGRestriction _ hidSyms :: Set G_symbol
hidSyms -> String -> [Element] -> [Element]
subnodes "Hidden"
                       ([Element] -> [Element]) -> [Element] -> [Element]
forall a b. (a -> b) -> a -> b
$ (G_symbol -> Element) -> [G_symbol] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (GlobalAnnos -> G_symbol -> Element
forall a. (GetRange a, Pretty a) => GlobalAnnos -> a -> Element
prettySymbol GlobalAnnos
ga)
                       ([G_symbol] -> [Element]) -> [G_symbol] -> [Element]
forall a b. (a -> b) -> a -> b
$ Set G_symbol -> [G_symbol]
forall a. Set a -> [a]
Set.toList Set G_symbol
hidSyms
                   _ -> []
      [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ case DGNodeLab -> G_theory
dgn_theory DGNodeLab
lbl of
        G_theory lid :: lid
lid _ (ExtSign sig :: sign
sig _) _ thsens :: ThSens sentence (AnyComorphism, BasicProof)
thsens _ -> let
          (axs :: ThSens sentence (AnyComorphism, BasicProof)
axs, thms :: ThSens sentence (AnyComorphism, BasicProof)
thms) = (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> (ThSens sentence (AnyComorphism, BasicProof),
    ThSens sentence (AnyComorphism, BasicProof))
forall k a.
Ord k =>
(a -> Bool) -> OMap k a -> (OMap k a, OMap k a)
OMap.partition SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom ThSens sentence (AnyComorphism, BasicProof)
thsens in
          (if HetcatsOpts -> Bool
fullSign HetcatsOpts
opts
           then String -> [Element] -> [Element]
subnodes "Symbols" ((symbol -> Element) -> [symbol] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (lid -> symbol -> Element
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> Element
showSym lid
lid) ([symbol] -> [Element]) -> [symbol] -> [Element]
forall a b. (a -> b) -> a -> b
$ lid -> sign -> [symbol]
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> [symbol]
symlist_of lid
lid sign
sig)
           else [])
          [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ String -> [Element] -> [Element]
subnodes "Axioms"
                    ((Named sentence -> Element) -> [Named sentence] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (HetcatsOpts
-> lid
-> GlobalAnnos
-> Maybe Bool
-> sign
-> Named sentence
-> Element
forall sentence lid sign morphism symbol.
(GetRange sentence, Pretty sentence,
 Sentences lid sentence sign morphism symbol) =>
HetcatsOpts
-> lid
-> GlobalAnnos
-> Maybe Bool
-> sign
-> Named sentence
-> Element
showSen HetcatsOpts
opts lid
lid GlobalAnnos
ga Maybe Bool
forall a. Maybe a
Nothing sign
sig) ([Named sentence] -> [Element]) -> [Named sentence] -> [Element]
forall a b. (a -> b) -> a -> b
$ ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
axs)
          [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ String -> [Element] -> [Element]
subnodes "Theorems"
                    (((String, SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
 -> Element)
-> [(String,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
-> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: String
s, t :: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
t) -> HetcatsOpts
-> lid
-> GlobalAnnos
-> Maybe Bool
-> sign
-> Named sentence
-> Element
forall sentence lid sign morphism symbol.
(GetRange sentence, Pretty sentence,
 Sentences lid sentence sign morphism symbol) =>
HetcatsOpts
-> lid
-> GlobalAnnos
-> Maybe Bool
-> sign
-> Named sentence
-> Element
showSen HetcatsOpts
opts lid
lid GlobalAnnos
ga
                         (Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool
isProvenSenStatus SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
t) sign
sig (Named sentence -> Element) -> Named sentence -> Element
forall a b. (a -> b) -> a -> b
$ String
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> Named sentence
forall a b. String -> SenStatus a b -> Named a
toNamed String
s SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
t)
                         ([(String,
   SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
 -> [Element])
-> [(String,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
-> [Element]
forall a b. (a -> b) -> a -> b
$ ThSens sentence (AnyComorphism, BasicProof)
-> [(String,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
forall k a. Ord k => OMap k a -> [(k, a)]
OMap.toList ThSens sentence (AnyComorphism, BasicProof)
thms)
          [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ if HetcatsOpts -> Bool
fullTheories HetcatsOpts
opts then case DGNodeLab -> Maybe G_theory
globalTheory DGNodeLab
lbl of
               Just (G_theory glid :: lid
glid _ _ _ allSens :: ThSens sentence (AnyComorphism, BasicProof)
allSens _) -> case
                   lid
-> lid
-> String
-> ThSens sentence (AnyComorphism, BasicProof)
-> Maybe (ThSens sentence (AnyComorphism, BasicProof))
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *) b.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m, Typeable b) =>
lid1
-> lid2 -> String -> ThSens sentence1 b -> m (ThSens sentence2 b)
coerceThSens lid
glid lid
lid "xml-lnode" ThSens sentence (AnyComorphism, BasicProof)
allSens of
                 Just gsens :: ThSens sentence (AnyComorphism, BasicProof)
gsens -> String -> [Element] -> [Element]
subnodes "ImpAxioms"
                    ([Element] -> [Element]) -> [Element] -> [Element]
forall a b. (a -> b) -> a -> b
$ (Named sentence -> Element) -> [Named sentence] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (HetcatsOpts
-> lid
-> GlobalAnnos
-> Maybe Bool
-> sign
-> Named sentence
-> Element
forall sentence lid sign morphism symbol.
(GetRange sentence, Pretty sentence,
 Sentences lid sentence sign morphism symbol) =>
HetcatsOpts
-> lid
-> GlobalAnnos
-> Maybe Bool
-> sign
-> Named sentence
-> Element
showSen HetcatsOpts
opts lid
lid GlobalAnnos
ga Maybe Bool
forall a. Maybe a
Nothing sign
sig) ([Named sentence] -> [Element]) -> [Named sentence] -> [Element]
forall a b. (a -> b) -> a -> b
$ ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList
                     (ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence])
-> ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. (a -> b) -> a -> b
$ (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => (a -> Bool) -> OMap k a -> OMap k a
OMap.filter ((sentence -> [sentence] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
 -> sentence)
-> [SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))]
-> [sentence]
forall a b. (a -> b) -> [a] -> [b]
map SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> sentence
forall s a. SenAttr s a -> s
sentence
                                    (ThSens sentence (AnyComorphism, BasicProof)
-> [SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))]
forall k a. Ord k => OMap k a -> [a]
OMap.elems ThSens sentence (AnyComorphism, BasicProof)
thsens)) (sentence -> Bool)
-> (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
    -> sentence)
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> sentence
forall s a. SenAttr s a -> s
sentence) ThSens sentence (AnyComorphism, BasicProof)
gsens
                 _ -> []
               _ -> []
             else []

-- | a status may be open, proven or outdated
mkStatusAttr :: String -> Attr
mkStatusAttr :: String -> Attr
mkStatusAttr = String -> String -> Attr
mkAttr "status"

mkProvenAttr :: Bool -> Attr
mkProvenAttr :: Bool -> Attr
mkProvenAttr b :: Bool
b = String -> Attr
mkStatusAttr (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ if Bool
b then "proven" else "open"

consStatus :: ConsStatus -> [Element]
consStatus :: ConsStatus -> [Element]
consStatus cs :: ConsStatus
cs = case ConsStatus -> Conservativity
getConsOfStatus ConsStatus
cs of
  None -> []
  cStat :: Conservativity
cStat -> [String -> String -> Element
forall t. Node t => String -> t -> Element
unode "ConsStatus" (String -> Element) -> String -> Element
forall a b. (a -> b) -> a -> b
$ Conservativity -> String
forall a. Show a => a -> String
show Conservativity
cStat]

ledge :: HetcatsOpts -> GlobalAnnos -> DGraph -> LEdge DGLinkLab -> Element
ledge :: HetcatsOpts -> GlobalAnnos -> DGraph -> LEdge DGLinkLab -> Element
ledge opts :: HetcatsOpts
opts ga :: GlobalAnnos
ga dg :: DGraph
dg (f :: Int
f, t :: Int
t, lbl :: DGLinkLab
lbl) = let
  typ :: DGLinkType
typ = DGLinkLab -> DGLinkType
dgl_type DGLinkLab
lbl
  mor :: Element
mor = HetcatsOpts -> GlobalAnnos -> GMorphism -> Element
gmorph HetcatsOpts
opts GlobalAnnos
ga (GMorphism -> Element) -> GMorphism -> Element
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
lbl
  mkMor :: Int -> Element
mkMor n :: Int
n = Attr -> Element -> Element
add_attr (String -> String -> Attr
mkAttr "morphismsource" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ Int -> DGraph -> String
getNameOfNode Int
n DGraph
dg) Element
mor
  lnkSt :: [Element]
lnkSt = case DGLinkType -> Maybe ThmLinkStatus
thmLinkStatus DGLinkType
typ of
         Nothing -> []
         Just tls :: ThmLinkStatus
tls -> case ThmLinkStatus
tls of
            LeftOpen -> []
            Proven r :: DGRule
r ls :: ProofBasis
ls -> DGRule -> [Element]
dgrule DGRule
r [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ (EdgeId -> Element) -> [EdgeId] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (\ e :: EdgeId
e ->
                Attr -> Element -> Element
add_attr (String -> String -> Attr
mkAttr "linkref" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ EdgeId -> String
showEdgeId EdgeId
e)
                (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> () -> Element
forall t. Node t => String -> t -> Element
unode "ProofBasis" ()) (Set EdgeId -> [EdgeId]
forall a. Set a -> [a]
Set.toList (Set EdgeId -> [EdgeId]) -> Set EdgeId -> [EdgeId]
forall a b. (a -> b) -> a -> b
$ ProofBasis -> Set EdgeId
proofBasis ProofBasis
ls)
  in [Attr] -> Element -> Element
add_attrs
  ([ String -> String -> Attr
mkAttr "source" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ Int -> DGraph -> String
getNameOfNode Int
f DGraph
dg
  , String -> String -> Attr
mkAttr "target" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ Int -> DGraph -> String
getNameOfNode Int
t DGraph
dg
  , String -> String -> Attr
mkAttr "linkid" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ EdgeId -> String
showEdgeId (EdgeId -> String) -> EdgeId -> String
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> EdgeId
dgl_id DGLinkLab
lbl
  , String -> String -> Attr
mkAttr "id_source" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
f
  , String -> String -> Attr
mkAttr "id_target" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
t
  ] [Attr] -> [Attr] -> [Attr]
forall a. [a] -> [a] -> [a]
++ case DGLinkLab -> DGLinkOrigin
dgl_origin DGLinkLab
lbl of
         DGLinkView i :: IRI
i _ ->
           [String -> Attr
mkNameAttr (String -> Attr) -> (IRI -> String) -> IRI -> Attr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> String
iriToStringShortUnsecure (IRI -> Attr) -> IRI -> Attr
forall a b. (a -> b) -> a -> b
$ Bool -> IRI -> IRI
setAngles Bool
False IRI
i]
         _ -> [])
  (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "DGLink"
    ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ String -> String -> Element
forall t. Node t => String -> t -> Element
unode "Type" (DGLinkLab -> String
getDGLinkType DGLinkLab
lbl) Element -> [Element] -> [Element]
forall a. a -> [a] -> [a]
: [Element]
lnkSt
    [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ ConsStatus -> [Element]
consStatus (DGLinkType -> ConsStatus
getLinkConsStatus DGLinkType
typ)
    [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ [case DGLinkType
typ of
         HidingFreeOrCofreeThm _ n :: Int
n _ _ -> Int -> Element
mkMor Int
n
         FreeOrCofreeDefLink _ (JustNode ns :: NodeSig
ns) -> Int -> Element
mkMor (Int -> Element) -> Int -> Element
forall a b. (a -> b) -> a -> b
$ NodeSig -> Int
getNode NodeSig
ns
         _ -> Element
mor]

dgrule :: DGRule -> [Element]
dgrule :: DGRule -> [Element]
dgrule r :: DGRule
r =
  String -> String -> Element
forall t. Node t => String -> t -> Element
unode "Rule" (DGRule -> String
dgRuleHeader DGRule
r)
  Element -> [Element] -> [Element]
forall a. a -> [a] -> [a]
: case DGRule
r of
      DGRuleLocalInference m :: [(String, String)]
m ->
        ((String, String) -> Element) -> [(String, String)] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: String
s, t :: String
t) -> [Attr] -> Element -> Element
add_attrs [String -> Attr
mkNameAttr String
s, String -> String -> Attr
mkAttr "renamedTo" String
t]
             (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> () -> Element
forall t. Node t => String -> t -> Element
unode "MovedTheorems" ()) [(String, String)]
m
      Composition es :: [EdgeId]
es -> (EdgeId -> Element) -> [EdgeId] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (\ e :: EdgeId
e ->
        Attr -> Element -> Element
add_attr (String -> String -> Attr
mkAttr "linkref" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ EdgeId -> String
showEdgeId EdgeId
e)
        (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> () -> Element
forall t. Node t => String -> t -> Element
unode "Composition" ()) [EdgeId]
es
      DGRuleWithEdge _ e :: EdgeId
e ->
        [ Attr -> Element -> Element
add_attr (String -> String -> Attr
mkAttr "linkref" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ EdgeId -> String
showEdgeId EdgeId
e)
        (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> () -> Element
forall t. Node t => String -> t -> Element
unode "RuleTarget" () ]
      _ -> []

-- | collects all symbols from dg and displays them as xml
dgSymbols :: HetcatsOpts -> DGraph -> Element
dgSymbols :: HetcatsOpts -> DGraph -> Element
dgSymbols opts :: HetcatsOpts
opts dg :: DGraph
dg = let ga :: GlobalAnnos
ga = DGraph -> GlobalAnnos
globalAnnos DGraph
dg in String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "Ontologies"
  ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ (LNode DGNodeLab -> Element) -> [LNode DGNodeLab] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (\ (i :: Int
i, lbl :: DGNodeLab
lbl) -> let ins :: [String]
ins = DGraph -> Int -> [String]
getImportNames DGraph
dg Int
i in
    HetcatsOpts -> [String] -> GlobalAnnos -> DGNodeLab -> Element
showSymbols HetcatsOpts
opts [String]
ins GlobalAnnos
ga DGNodeLab
lbl) ([LNode DGNodeLab] -> [Element]) -> [LNode DGNodeLab] -> [Element]
forall a b. (a -> b) -> a -> b
$ DGraph -> [LNode DGNodeLab]
labNodesDG DGraph
dg

showSymbols :: HetcatsOpts -> [String] -> GlobalAnnos -> DGNodeLab -> Element
showSymbols :: HetcatsOpts -> [String] -> GlobalAnnos -> DGNodeLab -> Element
showSymbols opts :: HetcatsOpts
opts ins :: [String]
ins ga :: GlobalAnnos
ga lbl :: DGNodeLab
lbl = HetcatsOpts
-> [String] -> String -> GlobalAnnos -> G_theory -> Element
showSymbolsTh HetcatsOpts
opts [String]
ins (DGNodeLab -> String
getDGNodeName DGNodeLab
lbl) GlobalAnnos
ga
  (G_theory -> Element) -> G_theory -> Element
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> G_theory
dgn_theory DGNodeLab
lbl

showSymbolsTh :: HetcatsOpts -> [String] -> String -> GlobalAnnos -> G_theory -> Element
showSymbolsTh :: HetcatsOpts
-> [String] -> String -> GlobalAnnos -> G_theory -> Element
showSymbolsTh opts :: HetcatsOpts
opts ins :: [String]
ins name :: String
name ga :: GlobalAnnos
ga th :: G_theory
th = case G_theory
th of
  G_theory lid :: lid
lid _ (ExtSign sig :: sign
sig _) _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _ -> [Attr] -> Element -> Element
add_attrs
     [ String -> String -> Attr
mkAttr "logic" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid
     , String -> Attr
mkNameAttr String
name ]
     (Element -> Element)
-> ([Element] -> Element) -> [Element] -> Element
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "Ontology"
     ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ [ String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "Symbols" ([Element] -> Element)
-> ([symbol] -> [Element]) -> [symbol] -> Element
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (symbol -> Element) -> [symbol] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (lid -> symbol -> Element
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> Element
showSym lid
lid) ([symbol] -> Element) -> [symbol] -> Element
forall a b. (a -> b) -> a -> b
$ lid -> sign -> [symbol]
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> [symbol]
symlist_of lid
lid sign
sig
       , String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "Axioms" ([Element] -> Element)
-> ([Named sentence] -> [Element]) -> [Named sentence] -> Element
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named sentence -> Element) -> [Named sentence] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (HetcatsOpts
-> lid
-> GlobalAnnos
-> Maybe Bool
-> sign
-> Named sentence
-> Element
forall sentence lid sign morphism symbol.
(GetRange sentence, Pretty sentence,
 Sentences lid sentence sign morphism symbol) =>
HetcatsOpts
-> lid
-> GlobalAnnos
-> Maybe Bool
-> sign
-> Named sentence
-> Element
showSen HetcatsOpts
opts lid
lid GlobalAnnos
ga Maybe Bool
forall a. Maybe a
Nothing sign
sig) ([Named sentence] -> Element) -> [Named sentence] -> Element
forall a b. (a -> b) -> a -> b
$ ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
sens ]
     [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ (String -> Element) -> [String] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String -> Element
forall t. Node t => String -> t -> Element
unode "Import") [String]
ins

showSen :: ( GetRange sentence, Pretty sentence
           , Sentences lid sentence sign morphism symbol) =>
   HetcatsOpts -> lid -> GlobalAnnos -> Maybe Bool -> sign -> Named sentence -> Element
showSen :: HetcatsOpts
-> lid
-> GlobalAnnos
-> Maybe Bool
-> sign
-> Named sentence
-> Element
showSen opts :: HetcatsOpts
opts lid :: lid
lid ga :: GlobalAnnos
ga mt :: Maybe Bool
mt sig :: sign
sig ns :: Named sentence
ns =
 let s :: sentence
s = Named sentence -> sentence
forall s a. SenAttr s a -> s
sentence Named sentence
ns in [Attr] -> Element -> Element
add_attrs
    (case Maybe Bool
mt of
       Nothing -> []
       Just b :: Bool
b -> [Bool -> Attr
mkProvenAttr Bool
b]
     [Attr] -> [Attr] -> [Attr]
forall a. [a] -> [a] -> [a]
++ String -> Attr
mkNameAttr (Named sentence -> String
forall s a. SenAttr s a -> a
senAttr Named sentence
ns) Attr -> [Attr] -> [Attr]
forall a. a -> [a] -> [a]
: Range -> [Attr]
rangeAttrs (sentence -> Range
forall a. GetRange a => a -> Range
getRangeSpan sentence
s)
     [Attr] -> [Attr] -> [Attr]
forall a. [a] -> [a] -> [a]
++ case Named sentence -> Maybe String
forall s a. SenAttr s a -> Maybe String
priority Named sentence
ns of
         Just impo :: String
impo -> [String -> Attr
mkPriorityAttr String
impo]
         _ -> [])
    (Element -> Element)
-> ([Element] -> Element) -> [Element] -> Element
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode (if Maybe Bool -> Bool
forall a. Maybe a -> Bool
isJust Maybe Bool
mt then "Theorem" else "Axiom") ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ String -> String -> Element
forall t. Node t => String -> t -> Element
unode "Text"
          (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (sentence -> Doc) -> sentence -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalAnnos -> Doc -> Doc
useGlobalAnnos GlobalAnnos
ga (Doc -> Doc) -> (sentence -> Doc) -> sentence -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. lid -> Named sentence -> Doc
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> Named sentence -> Doc
print_named lid
lid
                            (Named sentence -> Doc)
-> (sentence -> Named sentence) -> sentence -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> sentence -> Named sentence
forall a s. a -> s -> SenAttr s a
makeNamed "" (sentence -> String) -> sentence -> String
forall a b. (a -> b) -> a -> b
$ lid -> sign -> sentence -> sentence
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> sentence -> sentence
simplify_sen lid
lid sign
sig sentence
s)
          Element -> [Element] -> [Element]
forall a. a -> [a] -> [a]
: (symbol -> Element) -> [symbol] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (lid -> symbol -> Element
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> Element
showSym lid
lid) (lid -> sign -> sentence -> [symbol]
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> sentence -> [symbol]
symsOfSen lid
lid sign
sig sentence
s)
          [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ case Named sentence -> String
forall s a. SenAttr s a -> String
senMark Named sentence
ns of
               "" -> []
               m :: String
m -> [String -> String -> Element
forall t. Node t => String -> t -> Element
unode "ComorphismOrigin" String
m]
          [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ if HetcatsOpts -> Bool
printAST HetcatsOpts
opts
             then [String -> Element -> Element
forall t. Node t => String -> t -> Element
unode "AST" (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ sentence -> Element
forall a. ToXml a => a -> Element
asXml sentence
s]
             else []

showSym :: (Sentences lid sentence sign morphism symbol) =>
           lid -> symbol -> Element
showSym :: lid -> symbol -> Element
showSym lid :: lid
lid s :: symbol
s = [Attr] -> Element -> Element
add_attrs (([Attr] -> [Attr]
forall a. [a] -> [a]
reverse
            ([Attr] -> [Attr]) -> ([Attr] -> [Attr]) -> [Attr] -> [Attr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Attr] -> [Attr])
-> (String -> [Attr] -> [Attr]) -> Maybe String -> [Attr] -> [Attr]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Attr] -> [Attr]
forall a. a -> a
id ((:) (Attr -> [Attr] -> [Attr])
-> (String -> Attr) -> String -> [Attr] -> [Attr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> Attr
mkAttr "label") (lid -> symbol -> Maybe String
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> Maybe String
sym_label lid
lid symbol
s))
            [ String -> String -> Attr
mkAttr "iri" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ lid -> symbol -> String
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> String
fullSymName lid
lid symbol
s
            , String -> Attr
mkNameAttr (String -> Attr) -> (Id -> String) -> Id -> Attr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> String
forall a. Show a => a -> String
show (Id -> Attr) -> Id -> Attr
forall a b. (a -> b) -> a -> b
$ lid -> symbol -> Id
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> Id
sym_name lid
lid symbol
s
            , String -> String -> Attr
mkAttr "kind" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ lid -> symbol -> String
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> String
symKind lid
lid symbol
s
            ]) (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> symbol -> Element
forall a. (GetRange a, Pretty a) => GlobalAnnos -> a -> Element
prettySymbol GlobalAnnos
emptyGlobalAnnos symbol
s