{- |

Module : $Header$

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 = iriToStringShortUnsecure . setAngles False

xmlLibDefn :: LogicGraph -> GlobalAnnos -> LIB_DEFN -> Element

xmlLibDefn lg ga (Lib_defn n il rg an) =

add_attrs (mkNameAttr (show $ setAngles False $ getLibId n) : rgAttrs rg)

$ unode "Lib" $ annos "Global" ga an ++ libItems lg ga il

libItems :: LogicGraph -> GlobalAnnos -> [Annoted LIB_ITEM] -> [Element]

libItems lg ga is = case is of

[] -> []

i : rs -> annoted libItem lg ga i : libItems (case item i of

Logic_decl aa _ -> setLogicName aa lg

_ -> lg) ga rs

unsupported :: PrettyLG a => LogicGraph -> GlobalAnnos -> a -> Element

unsupported lg ga =

unode "Unsupported" . show . useGlobalAnnos ga . prettyLG lg

libItem :: LogicGraph -> GlobalAnnos -> LIB_ITEM -> Element

libItem lg ga li = case li of

Spec_defn n g as rg ->

add_attrs (mkNameAttr (iriToStr n) : rgAttrs rg)

$ unode "SpecDefn" $ genericity lg ga g ++ [annoted spec lg ga as]

View_defn n g (View_type from to _) mapping rg ->

add_attrs (mkNameAttr (iriToStr n) : rgAttrs rg)

$ unode "ViewDefn" $ genericity lg ga g

++ [ unode "Source" $ annoted spec lg ga from

, unode "Target" $ annoted spec lg ga to ]

++ concatMap (gmapping ga) mapping

Download_items n mapping rg ->

add_attrs (mkNameAttr (show $ getLibId n) : rgAttrs rg)

$ unode "Import" $ downloadItems mapping

Logic_decl n rg ->

add_attrs (mkNameAttr (showDoc n "") : rgAttrs rg)

$ unode "Logic" ()

_ -> unsupported lg ga li

downloadItems :: DownloadItems -> [Element]

downloadItems d = case d of

ItemMaps l -> map itemNameOrMap l

UniqueItem i -> [add_attr (mkAttr "as" $ iriToStr i)

$ unode "Item" ()]

spec :: LogicGraph -> GlobalAnnos -> SPEC -> Element

spec lg ga s = case s of

Basic_spec bs rg -> withRg rg $ gBasicSpec lg ga bs

EmptySpec rg -> withRg rg $ unode "Empty" ()

Translation as (Renaming m _) ->

unode "Translation" $ annoted spec lg ga as : concatMap (gmapping ga) m

Reduction as m ->

unode "Restriction" $ annoted spec lg ga as : restriction ga m

Union asl rg -> withRg rg $ unode "Union"

$ map (unode "Spec" . annoted spec lg ga) asl

Extension asl rg -> withRg rg $ unode "Extension"

$ map (unode "Spec" . annoted spec lg ga) asl

Free_spec as rg -> withRg rg $ unode "Free" $ annoted spec lg ga as

Cofree_spec as rg -> withRg rg $ unode "Cofree" $ annoted spec lg ga as

Minimize_spec as rg -> withRg rg $ unode "Minimize" $ annoted spec lg ga as

Local_spec as ins rg -> withRg rg $ unode "Local"

[ unode "Spec" $ annoted spec lg ga as

, unode "Within" $ annoted spec lg ga ins]

Closed_spec as rg -> withRg rg $ unode "Closed" $ annoted spec lg ga as

Group as rg -> withRg rg $ unode "Group" $ annoted spec lg ga as

Spec_inst n fa _ rg ->

add_attrs (mkNameAttr (iriToStr n) : rgAttrs rg)

$ unode "Actuals" $ map (annoted fitArg lg ga) fa

Qualified_spec ln as rg -> withRg rg $ unode "Qualified"

[prettyElem "Logic" ga ln, annoted spec (setLogicName ln lg) ga as]

Data l1 _ s1 s2 rg ->

add_attrs (mkAttr "data-logic" (show l1) : rgAttrs rg)

$ unode "Data" [ annoted spec (setCurLogic (show l1) lg) ga s1

, annoted spec lg ga s2]

_ -> unsupported lg ga s

fitArg :: LogicGraph -> GlobalAnnos -> FIT_ARG -> Element

fitArg lg ga fa = case fa of

Fit_spec as m rg -> withRg rg $ unode "Spec"

$ annoted spec lg ga as : concatMap (gmapping ga) m

Fit_view n fargs rg ->

add_attrs (mkNameAttr (iriToStr n) : rgAttrs rg)

$ unode "Spec" $ unode "Actuals" $ map (annoted fitArg lg ga) fargs

itemNameOrMap :: ItemNameMap -> Element

itemNameOrMap (ItemNameMap name m) =

add_attrs (mkNameAttr (iriToStr name) : case m of

Nothing -> []

Just as -> [mkAttr "as" $ iriToStr as])

$ unode "Item" ()

gmapping :: GlobalAnnos -> G_mapping -> [Element]

gmapping ga gm = case gm of

G_symb_map l -> subnodes "Mapping" $ gSymbMapItemList ga l

G_logic_translation lc -> [ add_attrs (logicCode lc)

$ unode "Logictranslation" () ]

ghiding :: GlobalAnnos -> G_hiding -> Element

ghiding ga gm = case gm of

G_symb_list l -> unode "Hiding" $ gSymbItemList ga l

G_logic_projection lc -> add_attrs (logicCode lc)

$ unode "Logicprojection" ()

gBasicSpec :: LogicGraph -> GlobalAnnos -> G_basic_spec -> Element

gBasicSpec lg ga (G_basic_spec lid bs) = itemToXml lg ga $ toItem lid bs

genericity :: LogicGraph -> GlobalAnnos -> GENERICITY -> [Element]

genericity lg ga (Genericity (Params pl) (Imported il) rg) =

if null pl then [] else

unode "Parameters" (spec lg ga $ Union pl rg)

: if null il then [] else

[ unode "Imports" $ spec lg ga $ Union il rg ]

restriction :: GlobalAnnos -> RESTRICTION -> [Element]

restriction ga restr = case restr of

Hidden m _ -> map (ghiding ga) m

Revealed m _ -> gSymbMapItemList ga m

gSymbItemList :: GlobalAnnos -> G_symb_items_list -> [Element]

gSymbItemList ga (G_symb_items_list _ l) = map (prettyElem "SymbItems" ga) l

gSymbMapItemList :: GlobalAnnos -> G_symb_map_items_list -> [Element]

gSymbMapItemList ga (G_symb_map_items_list _ l) =

map (prettyElem "SymbMapItems" ga) l

logicCode :: Logic_code -> [Attr]

logicCode (Logic_code enc src trg _) =

(case enc of

Nothing -> []

Just t -> [mkAttr "encoding" t])

++ (case src of

Nothing -> []

Just l -> [mkAttr "source" $ show $ pretty l])

++ case trg of

Nothing -> []

Just l -> [mkAttr "target" $ show $ pretty l]

isEmptyItem :: Annoted Item -> Bool

isEmptyItem ai =

let i = item ai

IT _ attrs mdoc = itemType i

in null (rgAttrs $ range i) && null attrs && isNothing mdoc

&& null (l_annos ai) && null (r_annos ai)

&& all isEmptyItem (items i)

itemToXml :: LogicGraph -> GlobalAnnos -> Item -> Element

itemToXml lg ga i =

let IT name attrs mdoc = itemType i

in add_attrs (map (uncurry mkAttr) attrs ++ rgAttrs (range i))

$ unode name $ (case mdoc of

Nothing -> []

Just d -> [mkText $ show $ useGlobalAnnos ga d])

++ map (Elem . annoted itemToXml lg ga)

(filter (not . isEmptyItem) $ items i)

-- range attribute without file name

rgAttrs :: Range -> [Attr]

rgAttrs = rangeAttrsF $ show . prettyRange . map (\ p -> p { sourceName = "" })

annos :: String -> GlobalAnnos -> [Annotation] -> [Element]

annos str ga = subnodes str

. map (annotationF rgAttrs ga)

annoted :: (LogicGraph -> GlobalAnnos -> a -> Element) -> LogicGraph

-> GlobalAnnos -> Annoted a -> Element

annoted f lg ga a = let

e = f lg ga $ item a

l = annos "Left" ga $ l_annos a

r = annos "Right" ga $ r_annos a

in e { elContent = map Elem l ++ elContent e ++ map Elem r }

withRg :: Range -> Element -> Element

withRg r e = if isJust (getAttrVal "range" e) then e else

add_attrs (rgAttrs r) e