{- |

Module : ./Logic/LGToXml.hs

Description : export logic graph information as XML

Copyright : (c) Christian Maeder DFKI GmbH 2013

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : non-portable (via imports)

export logic graph information as XML

-}

module Logic.LGToXml where

import Logic.Comorphism

import Logic.Grothendieck

import Logic.Logic

import Logic.Prover

import Control.Monad

import qualified Data.Map as Map

import Data.Char

import Data.Maybe

import Common.Consistency

import Common.ToXml

import Text.XML.Light

usableProvers :: LogicGraph -> IO Element

usableProvers lg = do

ps <- mapM proversOfLogic . Map.elems $ logics lg

return $ unode "provers" $ concat ps

proversOfLogic :: AnyLogic -> IO [Element]

proversOfLogic (Logic lid) = do

bps <- filterM (fmap isNothing . proverUsable) $ provers lid

return $ map (\ p ->

add_attrs [ mkNameAttr $ proverName p

, mkAttr "logic" $ language_name lid]

$ unode "prover" ()) bps

lGToXml :: LogicGraph -> IO Element

lGToXml lg = do

let cs = Map.elems $ comorphisms lg

groupC = Map.toList . Map.fromListWith (++)

ssubs = groupC

$ map (\ (Comorphism cid) -> (G_sublogics (sourceLogic cid)

$ sourceSublogic cid, [language_name cid])) cs

tsubs = groupC

$ map (\ (Comorphism cid) -> (G_sublogics (targetLogic cid)

$ targetSublogic cid, [language_name cid])) cs

nameC = map (\ n -> add_attr (mkNameAttr n) $ unode "comorphism" ())

ls <- mapM logicToXml . Map.elems $ logics lg

return $ unode "LogicGraph"

$ ls

++ map (\ (a, ns) -> add_attr (mkNameAttr $ show a)

$ unode "sourceSublogic" $ nameC ns) ssubs

++ map (\ (a, ns) -> add_attr (mkNameAttr $ show a)

$ unode "targetSublogic" $ nameC ns) tsubs

++ map comorphismToXml cs

logicToXml :: AnyLogic -> IO Element

logicToXml (Logic lid) = do

let ps = provers lid

cs1 = cons_checkers lid

cs2 = conservativityCheck lid

ua b = mkAttr "usable" . map toLower $ show $ isNothing b

bps <- mapM proverUsable ps

bcs1 <- mapM ccUsable cs1

bcs2 <- mapM checkerUsable cs2

return $ add_attrs

[ mkNameAttr $ language_name lid

, mkAttr "Stability" . show $ stability lid

, mkAttr "has_basic_parser" . show . not . Map.null $ parsersAndPrinters lid

, mkAttr "has_basic_analysis" . show . isJust $ basic_analysis lid

, mkAttr "has_symbol_list_parser" . show . isJust $ parse_symb_items lid

, mkAttr "has_symbol_map_parser" . show . isJust $ parse_symb_map_items lid

, mkAttr "is_a_process_logic" . show . isJust $ data_logic lid

] . unode "logic"

$ unode "Description" (mkText $ description lid)

: map (\ a -> add_attr (mkNameAttr a) $ unode "Serialization" ())

(filter (not . null) . Map.keys $ parsersAndPrinters lid)

++ zipWith (\ a b -> add_attrs [mkNameAttr $ proverName a, ua b]

$ unode "Prover" ()) ps bps

++ zipWith (\ a b -> add_attrs [mkNameAttr $ ccName a, ua b]

$ unode "ConsistencyChecker" ()) cs1 bcs1

++ zipWith (\ a b -> add_attrs [mkNameAttr $ checkerId a, ua b]

$ unode "ConservativityChecker" ()) cs2 bcs2

++ [unode "Sublogics" . unlines . map sublogicName $ all_sublogics lid]

comorphismToXml :: AnyComorphism -> Element

comorphismToXml (Comorphism cid) = add_attrs

[ mkNameAttr $ language_name cid

, mkAttr "source" $ language_name (sourceLogic cid)

, mkAttr "target" $ language_name (targetLogic cid)

, mkAttr "sourceSublogic" . sublogicName $ sourceSublogic cid

, mkAttr "targetSublogic" . sublogicName $ targetSublogic cid

, mkAttr "is_inclusion" . show $ isInclusionComorphism cid

, mkAttr "has_model_expansion" . show $ has_model_expansion cid

, mkAttr "is_weakly_amalgamable" . show $ is_weakly_amalgamable cid

] $ unode "comorphism" ()