{- |
Module      :  ./Syntax/ToXml.hs
Description :  xml output of Hets specification libaries
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 printing of Hets specification libaries
-}

module Syntax.ToXml (xmlLibDefn) where

import Syntax.AS_Structured
import Syntax.Print_AS_Structured
import Syntax.AS_Library
import Syntax.Print_AS_Library ()

import Common.AS_Annotation
import Common.Id
import Common.IRI
import Common.Item
import Common.LibName
import Common.Result
import Common.DocUtils
import Common.GlobalAnnotations
import Common.ToXml
import Common.XUpdate

import Logic.Logic
import Logic.Grothendieck

import Text.XML.Light

import Data.Maybe

iriToStr :: IRI -> String
iriToStr :: IRI -> String
iriToStr = IRI -> String
iriToStringShortUnsecure (IRI -> String) -> (IRI -> IRI) -> IRI -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> IRI -> IRI
setAngles Bool
False

xmlLibDefn :: LogicGraph -> GlobalAnnos -> LIB_DEFN -> Element
xmlLibDefn :: LogicGraph -> GlobalAnnos -> LIB_DEFN -> Element
xmlLibDefn lg :: LogicGraph
lg ga :: GlobalAnnos
ga (Lib_defn n :: LibName
n il :: [Annoted LIB_ITEM]
il rg :: Range
rg an :: [Annotation]
an) =
  [Attr] -> Element -> Element
add_attrs (String -> Attr
mkNameAttr (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
n) Attr -> [Attr] -> [Attr]
forall a. a -> [a] -> [a]
: Range -> [Attr]
rgAttrs Range
rg)
     (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "Lib" ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ String -> GlobalAnnos -> [Annotation] -> [Element]
annos "Global" GlobalAnnos
ga [Annotation]
an [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ LogicGraph -> GlobalAnnos -> [Annoted LIB_ITEM] -> [Element]
libItems LogicGraph
lg GlobalAnnos
ga [Annoted LIB_ITEM]
il

libItems :: LogicGraph -> GlobalAnnos -> [Annoted LIB_ITEM] -> [Element]
libItems :: LogicGraph -> GlobalAnnos -> [Annoted LIB_ITEM] -> [Element]
libItems lg :: LogicGraph
lg ga :: GlobalAnnos
ga is :: [Annoted LIB_ITEM]
is = case [Annoted LIB_ITEM]
is of
  [] -> []
  i :: Annoted LIB_ITEM
i : rs :: [Annoted LIB_ITEM]
rs -> (LogicGraph -> GlobalAnnos -> LIB_ITEM -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted LIB_ITEM -> Element
forall a.
(LogicGraph -> GlobalAnnos -> a -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted a -> Element
annoted LogicGraph -> GlobalAnnos -> LIB_ITEM -> Element
libItem LogicGraph
lg GlobalAnnos
ga Annoted LIB_ITEM
i Element -> [Element] -> [Element]
forall a. a -> [a] -> [a]
: LogicGraph -> GlobalAnnos -> [Annoted LIB_ITEM] -> [Element]
libItems (case Annoted LIB_ITEM -> LIB_ITEM
forall a. Annoted a -> a
item Annoted LIB_ITEM
i of
    Logic_decl aa :: LogicDescr
aa _ -> LogicDescr -> LogicGraph -> LogicGraph
setLogicName LogicDescr
aa LogicGraph
lg
    _ -> LogicGraph
lg) GlobalAnnos
ga [Annoted LIB_ITEM]
rs

unsupported :: PrettyLG a => LogicGraph -> GlobalAnnos -> a -> Element
unsupported :: LogicGraph -> GlobalAnnos -> a -> Element
unsupported lg :: LogicGraph
lg ga :: GlobalAnnos
ga =
  String -> String -> Element
forall t. Node t => String -> t -> Element
unode "Unsupported" (String -> Element) -> (a -> String) -> a -> Element
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (a -> Doc) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalAnnos -> Doc -> Doc
useGlobalAnnos GlobalAnnos
ga (Doc -> Doc) -> (a -> Doc) -> a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LogicGraph -> a -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg

libItem :: LogicGraph -> GlobalAnnos -> LIB_ITEM -> Element
libItem :: LogicGraph -> GlobalAnnos -> LIB_ITEM -> Element
libItem lg :: LogicGraph
lg ga :: GlobalAnnos
ga li :: LIB_ITEM
li = case LIB_ITEM
li of
  Spec_defn n :: IRI
n g :: GENERICITY
g as :: Annoted SPEC
as rg :: Range
rg ->
    [Attr] -> Element -> Element
add_attrs (String -> Attr
mkNameAttr (IRI -> String
iriToStr IRI
n) Attr -> [Attr] -> [Attr]
forall a. a -> [a] -> [a]
: Range -> [Attr]
rgAttrs Range
rg)
      (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "SpecDefn" ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ LogicGraph -> GlobalAnnos -> GENERICITY -> [Element]
genericity LogicGraph
lg GlobalAnnos
ga GENERICITY
g [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ [(LogicGraph -> GlobalAnnos -> SPEC -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted SPEC -> Element
forall a.
(LogicGraph -> GlobalAnnos -> a -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted a -> Element
annoted LogicGraph -> GlobalAnnos -> SPEC -> Element
spec LogicGraph
lg GlobalAnnos
ga Annoted SPEC
as]
  View_defn n :: IRI
n g :: GENERICITY
g (View_type from :: Annoted SPEC
from to :: Annoted SPEC
to _) mapping :: [G_mapping]
mapping rg :: Range
rg ->
    [Attr] -> Element -> Element
add_attrs (String -> Attr
mkNameAttr (IRI -> String
iriToStr IRI
n) Attr -> [Attr] -> [Attr]
forall a. a -> [a] -> [a]
: Range -> [Attr]
rgAttrs Range
rg)
      (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "ViewDefn" ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ LogicGraph -> GlobalAnnos -> GENERICITY -> [Element]
genericity LogicGraph
lg GlobalAnnos
ga GENERICITY
g
        [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ [ String -> Element -> Element
forall t. Node t => String -> t -> Element
unode "Source" (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ (LogicGraph -> GlobalAnnos -> SPEC -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted SPEC -> Element
forall a.
(LogicGraph -> GlobalAnnos -> a -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted a -> Element
annoted LogicGraph -> GlobalAnnos -> SPEC -> Element
spec LogicGraph
lg GlobalAnnos
ga Annoted SPEC
from
           , String -> Element -> Element
forall t. Node t => String -> t -> Element
unode "Target" (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ (LogicGraph -> GlobalAnnos -> SPEC -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted SPEC -> Element
forall a.
(LogicGraph -> GlobalAnnos -> a -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted a -> Element
annoted LogicGraph -> GlobalAnnos -> SPEC -> Element
spec LogicGraph
lg GlobalAnnos
ga Annoted SPEC
to ]
        [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ (G_mapping -> [Element]) -> [G_mapping] -> [Element]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (GlobalAnnos -> G_mapping -> [Element]
gmapping GlobalAnnos
ga) [G_mapping]
mapping
  Download_items n :: LibName
n mapping :: DownloadItems
mapping rg :: Range
rg ->
    [Attr] -> Element -> Element
add_attrs (String -> Attr
mkNameAttr (IRI -> String
forall a. Show a => a -> String
show (IRI -> String) -> IRI -> String
forall a b. (a -> b) -> a -> b
$ LibName -> IRI
getLibId LibName
n) Attr -> [Attr] -> [Attr]
forall a. a -> [a] -> [a]
: Range -> [Attr]
rgAttrs Range
rg)
      (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "Import" ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ DownloadItems -> [Element]
downloadItems DownloadItems
mapping
  Logic_decl n :: LogicDescr
n rg :: Range
rg ->
    [Attr] -> Element -> Element
add_attrs (String -> Attr
mkNameAttr (LogicDescr -> ShowS
forall a. Pretty a => a -> ShowS
showDoc LogicDescr
n "") Attr -> [Attr] -> [Attr]
forall a. a -> [a] -> [a]
: Range -> [Attr]
rgAttrs Range
rg)
      (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> () -> Element
forall t. Node t => String -> t -> Element
unode "Logic" ()
  _ -> LogicGraph -> GlobalAnnos -> LIB_ITEM -> Element
forall a. PrettyLG a => LogicGraph -> GlobalAnnos -> a -> Element
unsupported LogicGraph
lg GlobalAnnos
ga LIB_ITEM
li

downloadItems :: DownloadItems -> [Element]
downloadItems :: DownloadItems -> [Element]
downloadItems d :: DownloadItems
d = case DownloadItems
d of
  ItemMaps l :: [ItemNameMap]
l -> (ItemNameMap -> Element) -> [ItemNameMap] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map ItemNameMap -> Element
itemNameOrMap [ItemNameMap]
l
  UniqueItem i :: IRI
i -> [Attr -> Element -> Element
add_attr (String -> String -> Attr
mkAttr "as" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ IRI -> String
iriToStr IRI
i)
    (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> () -> Element
forall t. Node t => String -> t -> Element
unode "Item" ()]

spec :: LogicGraph -> GlobalAnnos -> SPEC -> Element
spec :: LogicGraph -> GlobalAnnos -> SPEC -> Element
spec lg :: LogicGraph
lg ga :: GlobalAnnos
ga s :: SPEC
s = case SPEC
s of
  Basic_spec bs :: G_basic_spec
bs rg :: Range
rg -> Range -> Element -> Element
withRg Range
rg (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ LogicGraph -> GlobalAnnos -> G_basic_spec -> Element
gBasicSpec LogicGraph
lg GlobalAnnos
ga G_basic_spec
bs
  EmptySpec rg :: Range
rg -> Range -> Element -> Element
withRg Range
rg (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> () -> Element
forall t. Node t => String -> t -> Element
unode "Empty" ()
  Translation as :: Annoted SPEC
as (Renaming m :: [G_mapping]
m _) ->
    String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "Translation" ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ (LogicGraph -> GlobalAnnos -> SPEC -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted SPEC -> Element
forall a.
(LogicGraph -> GlobalAnnos -> a -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted a -> Element
annoted LogicGraph -> GlobalAnnos -> SPEC -> Element
spec LogicGraph
lg GlobalAnnos
ga Annoted SPEC
as Element -> [Element] -> [Element]
forall a. a -> [a] -> [a]
: (G_mapping -> [Element]) -> [G_mapping] -> [Element]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (GlobalAnnos -> G_mapping -> [Element]
gmapping GlobalAnnos
ga) [G_mapping]
m
  Reduction as :: Annoted SPEC
as m :: RESTRICTION
m ->
    String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "Restriction" ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ (LogicGraph -> GlobalAnnos -> SPEC -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted SPEC -> Element
forall a.
(LogicGraph -> GlobalAnnos -> a -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted a -> Element
annoted LogicGraph -> GlobalAnnos -> SPEC -> Element
spec LogicGraph
lg GlobalAnnos
ga Annoted SPEC
as Element -> [Element] -> [Element]
forall a. a -> [a] -> [a]
: GlobalAnnos -> RESTRICTION -> [Element]
restriction GlobalAnnos
ga RESTRICTION
m
  Union asl :: [Annoted SPEC]
asl rg :: Range
rg -> Range -> Element -> Element
withRg Range
rg (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "Union"
    ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ (Annoted SPEC -> Element) -> [Annoted SPEC] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Element -> Element
forall t. Node t => String -> t -> Element
unode "Spec" (Element -> Element)
-> (Annoted SPEC -> Element) -> Annoted SPEC -> Element
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LogicGraph -> GlobalAnnos -> SPEC -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted SPEC -> Element
forall a.
(LogicGraph -> GlobalAnnos -> a -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted a -> Element
annoted LogicGraph -> GlobalAnnos -> SPEC -> Element
spec LogicGraph
lg GlobalAnnos
ga) [Annoted SPEC]
asl
  Extension asl :: [Annoted SPEC]
asl rg :: Range
rg -> Range -> Element -> Element
withRg Range
rg (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "Extension"
   ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ (Annoted SPEC -> Element) -> [Annoted SPEC] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Element -> Element
forall t. Node t => String -> t -> Element
unode "Spec" (Element -> Element)
-> (Annoted SPEC -> Element) -> Annoted SPEC -> Element
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LogicGraph -> GlobalAnnos -> SPEC -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted SPEC -> Element
forall a.
(LogicGraph -> GlobalAnnos -> a -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted a -> Element
annoted LogicGraph -> GlobalAnnos -> SPEC -> Element
spec LogicGraph
lg GlobalAnnos
ga) [Annoted SPEC]
asl
  Free_spec as :: Annoted SPEC
as rg :: Range
rg -> Range -> Element -> Element
withRg Range
rg (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> Element -> Element
forall t. Node t => String -> t -> Element
unode "Free" (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ (LogicGraph -> GlobalAnnos -> SPEC -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted SPEC -> Element
forall a.
(LogicGraph -> GlobalAnnos -> a -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted a -> Element
annoted LogicGraph -> GlobalAnnos -> SPEC -> Element
spec LogicGraph
lg GlobalAnnos
ga Annoted SPEC
as
  Cofree_spec as :: Annoted SPEC
as rg :: Range
rg -> Range -> Element -> Element
withRg Range
rg (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> Element -> Element
forall t. Node t => String -> t -> Element
unode "Cofree" (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ (LogicGraph -> GlobalAnnos -> SPEC -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted SPEC -> Element
forall a.
(LogicGraph -> GlobalAnnos -> a -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted a -> Element
annoted LogicGraph -> GlobalAnnos -> SPEC -> Element
spec LogicGraph
lg GlobalAnnos
ga Annoted SPEC
as
  Minimize_spec as :: Annoted SPEC
as rg :: Range
rg -> Range -> Element -> Element
withRg Range
rg (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> Element -> Element
forall t. Node t => String -> t -> Element
unode "Minimize" (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ (LogicGraph -> GlobalAnnos -> SPEC -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted SPEC -> Element
forall a.
(LogicGraph -> GlobalAnnos -> a -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted a -> Element
annoted LogicGraph -> GlobalAnnos -> SPEC -> Element
spec LogicGraph
lg GlobalAnnos
ga Annoted SPEC
as
  Local_spec as :: Annoted SPEC
as ins :: Annoted SPEC
ins rg :: Range
rg -> Range -> Element -> Element
withRg Range
rg (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "Local"
    [ String -> Element -> Element
forall t. Node t => String -> t -> Element
unode "Spec" (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ (LogicGraph -> GlobalAnnos -> SPEC -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted SPEC -> Element
forall a.
(LogicGraph -> GlobalAnnos -> a -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted a -> Element
annoted LogicGraph -> GlobalAnnos -> SPEC -> Element
spec LogicGraph
lg GlobalAnnos
ga Annoted SPEC
as
    , String -> Element -> Element
forall t. Node t => String -> t -> Element
unode "Within" (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ (LogicGraph -> GlobalAnnos -> SPEC -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted SPEC -> Element
forall a.
(LogicGraph -> GlobalAnnos -> a -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted a -> Element
annoted LogicGraph -> GlobalAnnos -> SPEC -> Element
spec LogicGraph
lg GlobalAnnos
ga Annoted SPEC
ins]
  Closed_spec as :: Annoted SPEC
as rg :: Range
rg -> Range -> Element -> Element
withRg Range
rg (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> Element -> Element
forall t. Node t => String -> t -> Element
unode "Closed" (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ (LogicGraph -> GlobalAnnos -> SPEC -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted SPEC -> Element
forall a.
(LogicGraph -> GlobalAnnos -> a -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted a -> Element
annoted LogicGraph -> GlobalAnnos -> SPEC -> Element
spec LogicGraph
lg GlobalAnnos
ga Annoted SPEC
as
  Group as :: Annoted SPEC
as rg :: Range
rg -> Range -> Element -> Element
withRg Range
rg (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> Element -> Element
forall t. Node t => String -> t -> Element
unode "Group" (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ (LogicGraph -> GlobalAnnos -> SPEC -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted SPEC -> Element
forall a.
(LogicGraph -> GlobalAnnos -> a -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted a -> Element
annoted LogicGraph -> GlobalAnnos -> SPEC -> Element
spec LogicGraph
lg GlobalAnnos
ga Annoted SPEC
as
  Spec_inst n :: IRI
n fa :: [Annoted FIT_ARG]
fa _ rg :: Range
rg ->
    [Attr] -> Element -> Element
add_attrs (String -> Attr
mkNameAttr (IRI -> String
iriToStr IRI
n) Attr -> [Attr] -> [Attr]
forall a. a -> [a] -> [a]
: Range -> [Attr]
rgAttrs Range
rg)
    (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "Actuals" ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ (Annoted FIT_ARG -> Element) -> [Annoted FIT_ARG] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map ((LogicGraph -> GlobalAnnos -> FIT_ARG -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted FIT_ARG -> Element
forall a.
(LogicGraph -> GlobalAnnos -> a -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted a -> Element
annoted LogicGraph -> GlobalAnnos -> FIT_ARG -> Element
fitArg LogicGraph
lg GlobalAnnos
ga) [Annoted FIT_ARG]
fa
  Qualified_spec ln :: LogicDescr
ln as :: Annoted SPEC
as rg :: Range
rg -> Range -> Element -> Element
withRg Range
rg (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "Qualified"
    [String -> GlobalAnnos -> LogicDescr -> Element
forall a. Pretty a => String -> GlobalAnnos -> a -> Element
prettyElem "Logic" GlobalAnnos
ga LogicDescr
ln, (LogicGraph -> GlobalAnnos -> SPEC -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted SPEC -> Element
forall a.
(LogicGraph -> GlobalAnnos -> a -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted a -> Element
annoted LogicGraph -> GlobalAnnos -> SPEC -> Element
spec (LogicDescr -> LogicGraph -> LogicGraph
setLogicName LogicDescr
ln LogicGraph
lg) GlobalAnnos
ga Annoted SPEC
as]
  Data l1 :: AnyLogic
l1 _ s1 :: Annoted SPEC
s1 s2 :: Annoted SPEC
s2 rg :: Range
rg ->
    [Attr] -> Element -> Element
add_attrs (String -> String -> Attr
mkAttr "data-logic" (AnyLogic -> String
forall a. Show a => a -> String
show AnyLogic
l1) Attr -> [Attr] -> [Attr]
forall a. a -> [a] -> [a]
: Range -> [Attr]
rgAttrs Range
rg)
      (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "Data" [ (LogicGraph -> GlobalAnnos -> SPEC -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted SPEC -> Element
forall a.
(LogicGraph -> GlobalAnnos -> a -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted a -> Element
annoted LogicGraph -> GlobalAnnos -> SPEC -> Element
spec (String -> LogicGraph -> LogicGraph
setCurLogic (AnyLogic -> String
forall a. Show a => a -> String
show AnyLogic
l1) LogicGraph
lg) GlobalAnnos
ga Annoted SPEC
s1
                     , (LogicGraph -> GlobalAnnos -> SPEC -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted SPEC -> Element
forall a.
(LogicGraph -> GlobalAnnos -> a -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted a -> Element
annoted LogicGraph -> GlobalAnnos -> SPEC -> Element
spec LogicGraph
lg GlobalAnnos
ga Annoted SPEC
s2]
  _ -> LogicGraph -> GlobalAnnos -> SPEC -> Element
forall a. PrettyLG a => LogicGraph -> GlobalAnnos -> a -> Element
unsupported LogicGraph
lg GlobalAnnos
ga SPEC
s

fitArg :: LogicGraph -> GlobalAnnos -> FIT_ARG -> Element
fitArg :: LogicGraph -> GlobalAnnos -> FIT_ARG -> Element
fitArg lg :: LogicGraph
lg ga :: GlobalAnnos
ga fa :: FIT_ARG
fa = case FIT_ARG
fa of
  Fit_spec as :: Annoted SPEC
as m :: [G_mapping]
m rg :: Range
rg -> Range -> Element -> Element
withRg Range
rg (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "Spec"
    ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ (LogicGraph -> GlobalAnnos -> SPEC -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted SPEC -> Element
forall a.
(LogicGraph -> GlobalAnnos -> a -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted a -> Element
annoted LogicGraph -> GlobalAnnos -> SPEC -> Element
spec LogicGraph
lg GlobalAnnos
ga Annoted SPEC
as Element -> [Element] -> [Element]
forall a. a -> [a] -> [a]
: (G_mapping -> [Element]) -> [G_mapping] -> [Element]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (GlobalAnnos -> G_mapping -> [Element]
gmapping GlobalAnnos
ga) [G_mapping]
m
  Fit_view n :: IRI
n fargs :: [Annoted FIT_ARG]
fargs rg :: Range
rg ->
    [Attr] -> Element -> Element
add_attrs (String -> Attr
mkNameAttr (IRI -> String
iriToStr IRI
n) Attr -> [Attr] -> [Attr]
forall a. a -> [a] -> [a]
: Range -> [Attr]
rgAttrs Range
rg)
    (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> Element -> Element
forall t. Node t => String -> t -> Element
unode "Spec" (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "Actuals" ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ (Annoted FIT_ARG -> Element) -> [Annoted FIT_ARG] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map ((LogicGraph -> GlobalAnnos -> FIT_ARG -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted FIT_ARG -> Element
forall a.
(LogicGraph -> GlobalAnnos -> a -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted a -> Element
annoted LogicGraph -> GlobalAnnos -> FIT_ARG -> Element
fitArg LogicGraph
lg GlobalAnnos
ga) [Annoted FIT_ARG]
fargs

itemNameOrMap :: ItemNameMap -> Element
itemNameOrMap :: ItemNameMap -> Element
itemNameOrMap (ItemNameMap name :: IRI
name m :: Maybe IRI
m) =
  [Attr] -> Element -> Element
add_attrs (String -> Attr
mkNameAttr (IRI -> String
iriToStr IRI
name) Attr -> [Attr] -> [Attr]
forall a. a -> [a] -> [a]
: case Maybe IRI
m of
    Nothing -> []
    Just as :: IRI
as -> [String -> String -> Attr
mkAttr "as" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ IRI -> String
iriToStr IRI
as])
  (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> () -> Element
forall t. Node t => String -> t -> Element
unode "Item" ()

gmapping :: GlobalAnnos -> G_mapping -> [Element]
gmapping :: GlobalAnnos -> G_mapping -> [Element]
gmapping ga :: GlobalAnnos
ga gm :: G_mapping
gm = case G_mapping
gm of
  G_symb_map l :: G_symb_map_items_list
l -> String -> [Element] -> [Element]
subnodes "Mapping" ([Element] -> [Element]) -> [Element] -> [Element]
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> G_symb_map_items_list -> [Element]
gSymbMapItemList GlobalAnnos
ga G_symb_map_items_list
l
  G_logic_translation lc :: Logic_code
lc -> [ [Attr] -> Element -> Element
add_attrs (Logic_code -> [Attr]
logicCode Logic_code
lc)
    (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> () -> Element
forall t. Node t => String -> t -> Element
unode "Logictranslation" () ]

ghiding :: GlobalAnnos -> G_hiding -> Element
ghiding :: GlobalAnnos -> G_hiding -> Element
ghiding ga :: GlobalAnnos
ga gm :: G_hiding
gm = case G_hiding
gm of
  G_symb_list l :: G_symb_items_list
l -> String -> [Element] -> Element
forall t. Node t => String -> t -> Element
unode "Hiding" ([Element] -> Element) -> [Element] -> Element
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> G_symb_items_list -> [Element]
gSymbItemList GlobalAnnos
ga G_symb_items_list
l
  G_logic_projection lc :: Logic_code
lc -> [Attr] -> Element -> Element
add_attrs (Logic_code -> [Attr]
logicCode Logic_code
lc)
    (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> () -> Element
forall t. Node t => String -> t -> Element
unode "Logicprojection" ()

gBasicSpec :: LogicGraph -> GlobalAnnos -> G_basic_spec -> Element
gBasicSpec :: LogicGraph -> GlobalAnnos -> G_basic_spec -> Element
gBasicSpec lg :: LogicGraph
lg ga :: GlobalAnnos
ga (G_basic_spec lid :: lid
lid bs :: basic_spec
bs) = LogicGraph -> GlobalAnnos -> Item -> Element
itemToXml LogicGraph
lg GlobalAnnos
ga (Item -> Element) -> Item -> Element
forall a b. (a -> b) -> a -> b
$ lid -> basic_spec -> Item
forall lid basic_spec symbol symb_items symb_map_items.
Syntax lid basic_spec symbol symb_items symb_map_items =>
lid -> basic_spec -> Item
toItem lid
lid basic_spec
bs

genericity :: LogicGraph -> GlobalAnnos -> GENERICITY -> [Element]
genericity :: LogicGraph -> GlobalAnnos -> GENERICITY -> [Element]
genericity lg :: LogicGraph
lg ga :: GlobalAnnos
ga (Genericity (Params pl :: [Annoted SPEC]
pl) (Imported il :: [Annoted SPEC]
il) rg :: Range
rg) =
  if [Annoted SPEC] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted SPEC]
pl then [] else
    String -> Element -> Element
forall t. Node t => String -> t -> Element
unode "Parameters" (LogicGraph -> GlobalAnnos -> SPEC -> Element
spec LogicGraph
lg GlobalAnnos
ga (SPEC -> Element) -> SPEC -> Element
forall a b. (a -> b) -> a -> b
$ [Annoted SPEC] -> Range -> SPEC
Union [Annoted SPEC]
pl Range
rg)
    Element -> [Element] -> [Element]
forall a. a -> [a] -> [a]
: if [Annoted SPEC] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted SPEC]
il then [] else
      [ String -> Element -> Element
forall t. Node t => String -> t -> Element
unode "Imports" (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ LogicGraph -> GlobalAnnos -> SPEC -> Element
spec LogicGraph
lg GlobalAnnos
ga (SPEC -> Element) -> SPEC -> Element
forall a b. (a -> b) -> a -> b
$ [Annoted SPEC] -> Range -> SPEC
Union [Annoted SPEC]
il Range
rg ]

restriction :: GlobalAnnos -> RESTRICTION -> [Element]
restriction :: GlobalAnnos -> RESTRICTION -> [Element]
restriction ga :: GlobalAnnos
ga restr :: RESTRICTION
restr = case RESTRICTION
restr of
  Hidden m :: [G_hiding]
m _ -> (G_hiding -> Element) -> [G_hiding] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (GlobalAnnos -> G_hiding -> Element
ghiding GlobalAnnos
ga) [G_hiding]
m
  Revealed m :: G_symb_map_items_list
m _ -> GlobalAnnos -> G_symb_map_items_list -> [Element]
gSymbMapItemList GlobalAnnos
ga G_symb_map_items_list
m

gSymbItemList :: GlobalAnnos -> G_symb_items_list -> [Element]
gSymbItemList :: GlobalAnnos -> G_symb_items_list -> [Element]
gSymbItemList ga :: GlobalAnnos
ga (G_symb_items_list _ l :: [symb_items]
l) = (symb_items -> Element) -> [symb_items] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (String -> GlobalAnnos -> symb_items -> Element
forall a. Pretty a => String -> GlobalAnnos -> a -> Element
prettyElem "SymbItems" GlobalAnnos
ga) [symb_items]
l

gSymbMapItemList :: GlobalAnnos -> G_symb_map_items_list -> [Element]
gSymbMapItemList :: GlobalAnnos -> G_symb_map_items_list -> [Element]
gSymbMapItemList ga :: GlobalAnnos
ga (G_symb_map_items_list _ l :: [symb_map_items]
l) =
  (symb_map_items -> Element) -> [symb_map_items] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map (String -> GlobalAnnos -> symb_map_items -> Element
forall a. Pretty a => String -> GlobalAnnos -> a -> Element
prettyElem "SymbMapItems" GlobalAnnos
ga) [symb_map_items]
l

logicCode :: Logic_code -> [Attr]
logicCode :: Logic_code -> [Attr]
logicCode (Logic_code enc :: Maybe String
enc src :: Maybe Logic_name
src trg :: Maybe Logic_name
trg _) =
  (case Maybe String
enc of
    Nothing -> []
    Just t :: String
t -> [String -> String -> Attr
mkAttr "encoding" String
t])
  [Attr] -> [Attr] -> [Attr]
forall a. [a] -> [a] -> [a]
++ (case Maybe Logic_name
src of
        Nothing -> []
        Just l :: Logic_name
l -> [String -> String -> Attr
mkAttr "source" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Logic_name -> Doc
forall a. Pretty a => a -> Doc
pretty Logic_name
l])
  [Attr] -> [Attr] -> [Attr]
forall a. [a] -> [a] -> [a]
++ case Maybe Logic_name
trg of
        Nothing -> []
        Just l :: Logic_name
l -> [String -> String -> Attr
mkAttr "target" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Logic_name -> Doc
forall a. Pretty a => a -> Doc
pretty Logic_name
l]

isEmptyItem :: Annoted Item -> Bool
isEmptyItem :: Annoted Item -> Bool
isEmptyItem ai :: Annoted Item
ai =
  let i :: Item
i = Annoted Item -> Item
forall a. Annoted a -> a
item Annoted Item
ai
      IT _ attrs :: [(String, String)]
attrs mdoc :: Maybe Doc
mdoc = Item -> ItemType
itemType Item
i
  in [Attr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Range -> [Attr]
rgAttrs (Range -> [Attr]) -> Range -> [Attr]
forall a b. (a -> b) -> a -> b
$ Item -> Range
range Item
i) Bool -> Bool -> Bool
&& [(String, String)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, String)]
attrs Bool -> Bool -> Bool
&& Maybe Doc -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Doc
mdoc
     Bool -> Bool -> Bool
&& [Annotation] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Annoted Item -> [Annotation]
forall a. Annoted a -> [Annotation]
l_annos Annoted Item
ai) Bool -> Bool -> Bool
&& [Annotation] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Annoted Item -> [Annotation]
forall a. Annoted a -> [Annotation]
r_annos Annoted Item
ai)
     Bool -> Bool -> Bool
&& (Annoted Item -> Bool) -> [Annoted Item] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Annoted Item -> Bool
isEmptyItem (Item -> [Annoted Item]
items Item
i)

itemToXml :: LogicGraph -> GlobalAnnos -> Item -> Element
itemToXml :: LogicGraph -> GlobalAnnos -> Item -> Element
itemToXml lg :: LogicGraph
lg ga :: GlobalAnnos
ga i :: Item
i =
    let IT name :: String
name attrs :: [(String, String)]
attrs mdoc :: Maybe Doc
mdoc = Item -> ItemType
itemType Item
i
    in [Attr] -> Element -> Element
add_attrs (((String, String) -> Attr) -> [(String, String)] -> [Attr]
forall a b. (a -> b) -> [a] -> [b]
map ((String -> String -> Attr) -> (String, String) -> Attr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry String -> String -> Attr
mkAttr) [(String, String)]
attrs [Attr] -> [Attr] -> [Attr]
forall a. [a] -> [a] -> [a]
++ Range -> [Attr]
rgAttrs (Item -> Range
range Item
i))
       (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> [Content] -> Element
forall t. Node t => String -> t -> Element
unode String
name ([Content] -> Element) -> [Content] -> Element
forall a b. (a -> b) -> a -> b
$ (case Maybe Doc
mdoc of
          Nothing -> []
          Just d :: Doc
d -> [String -> Content
mkText (String -> Content) -> String -> Content
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> Doc -> Doc
useGlobalAnnos GlobalAnnos
ga Doc
d])
        [Content] -> [Content] -> [Content]
forall a. [a] -> [a] -> [a]
++ (Annoted Item -> Content) -> [Annoted Item] -> [Content]
forall a b. (a -> b) -> [a] -> [b]
map (Element -> Content
Elem (Element -> Content)
-> (Annoted Item -> Element) -> Annoted Item -> Content
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LogicGraph -> GlobalAnnos -> Item -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted Item -> Element
forall a.
(LogicGraph -> GlobalAnnos -> a -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted a -> Element
annoted LogicGraph -> GlobalAnnos -> Item -> Element
itemToXml LogicGraph
lg GlobalAnnos
ga)
           ((Annoted Item -> Bool) -> [Annoted Item] -> [Annoted Item]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Annoted Item -> Bool) -> Annoted Item -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted Item -> Bool
isEmptyItem) ([Annoted Item] -> [Annoted Item])
-> [Annoted Item] -> [Annoted Item]
forall a b. (a -> b) -> a -> b
$ Item -> [Annoted Item]
items Item
i)

-- range attribute without file name
rgAttrs :: Range -> [Attr]
rgAttrs :: Range -> [Attr]
rgAttrs = ([Pos] -> String) -> Range -> [Attr]
rangeAttrsF (([Pos] -> String) -> Range -> [Attr])
-> ([Pos] -> String) -> Range -> [Attr]
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> ([Pos] -> Doc) -> [Pos] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Pos] -> Doc
prettyRange ([Pos] -> Doc) -> ([Pos] -> [Pos]) -> [Pos] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pos -> Pos) -> [Pos] -> [Pos]
forall a b. (a -> b) -> [a] -> [b]
map (\ p :: Pos
p -> Pos
p { sourceName :: String
sourceName = "" })

annos :: String -> GlobalAnnos -> [Annotation] -> [Element]
annos :: String -> GlobalAnnos -> [Annotation] -> [Element]
annos str :: String
str ga :: GlobalAnnos
ga = String -> [Element] -> [Element]
subnodes String
str
  ([Element] -> [Element])
-> ([Annotation] -> [Element]) -> [Annotation] -> [Element]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Annotation -> Element) -> [Annotation] -> [Element]
forall a b. (a -> b) -> [a] -> [b]
map ((Range -> [Attr]) -> GlobalAnnos -> Annotation -> Element
annotationF Range -> [Attr]
rgAttrs GlobalAnnos
ga)

annoted :: (LogicGraph -> GlobalAnnos -> a -> Element) -> LogicGraph
  -> GlobalAnnos -> Annoted a -> Element
annoted :: (LogicGraph -> GlobalAnnos -> a -> Element)
-> LogicGraph -> GlobalAnnos -> Annoted a -> Element
annoted f :: LogicGraph -> GlobalAnnos -> a -> Element
f lg :: LogicGraph
lg ga :: GlobalAnnos
ga a :: Annoted a
a = let
  e :: Element
e = LogicGraph -> GlobalAnnos -> a -> Element
f LogicGraph
lg GlobalAnnos
ga (a -> Element) -> a -> Element
forall a b. (a -> b) -> a -> b
$ Annoted a -> a
forall a. Annoted a -> a
item Annoted a
a
  l :: [Element]
l = String -> GlobalAnnos -> [Annotation] -> [Element]
annos "Left" GlobalAnnos
ga ([Annotation] -> [Element]) -> [Annotation] -> [Element]
forall a b. (a -> b) -> a -> b
$ Annoted a -> [Annotation]
forall a. Annoted a -> [Annotation]
l_annos Annoted a
a
  r :: [Element]
r = String -> GlobalAnnos -> [Annotation] -> [Element]
annos "Right" GlobalAnnos
ga ([Annotation] -> [Element]) -> [Annotation] -> [Element]
forall a b. (a -> b) -> a -> b
$ Annoted a -> [Annotation]
forall a. Annoted a -> [Annotation]
r_annos Annoted a
a
  in Element
e { elContent :: [Content]
elContent = (Element -> Content) -> [Element] -> [Content]
forall a b. (a -> b) -> [a] -> [b]
map Element -> Content
Elem [Element]
l [Content] -> [Content] -> [Content]
forall a. [a] -> [a] -> [a]
++ Element -> [Content]
elContent Element
e [Content] -> [Content] -> [Content]
forall a. [a] -> [a] -> [a]
++ (Element -> Content) -> [Element] -> [Content]
forall a b. (a -> b) -> [a] -> [b]
map Element -> Content
Elem [Element]
r }

withRg :: Range -> Element -> Element
withRg :: Range -> Element -> Element
withRg r :: Range
r e :: Element
e = if Maybe String -> Bool
forall a. Maybe a -> Bool
isJust (String -> Element -> Maybe String
forall (m :: * -> *). MonadFail m => String -> Element -> m String
getAttrVal "range" Element
e) then Element
e else
   [Attr] -> Element -> Element
add_attrs (Range -> [Attr]
rgAttrs Range
r) Element
e