content: {- |
  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 = 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
  