{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Static/XGraph.hs
Description :  xml input for Hets development graphs
Copyright   :  (c) Simon Ulbricht, DFKI GmbH 2011
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  tekknix@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (DevGraph)

convert an Xml-Graph into an XGraph-Structure.
-}

module Static.XGraph where

import Static.DgUtils

import Common.AnalyseAnnos (getGlobalAnnos)
import Common.Consistency (Conservativity (..))
import Common.GlobalAnnotations (GlobalAnnos, emptyGlobalAnnos)
import Common.LibName
import Common.Result (Result (..))
import Common.Utils (readMaybe)
import Common.XUpdate (getAttrVal, readAttrVal)

import Control.Monad
import qualified Control.Monad.Fail as Fail

import Data.Data
import Data.List
import Data.Maybe (fromMaybe)

import qualified Data.Set as Set
import qualified Data.Map as Map

import Text.XML.Light

{- -------------
Data Types -}

-- represent element information in the order they can be processed later
data XGraph = XGraph { XGraph -> LibName
libName :: LibName
                     , XGraph -> GlobalAnnos
globAnnos :: GlobalAnnos
                     , XGraph -> EdgeId
nextLinkId :: EdgeId
                     , XGraph -> [XLink]
thmLinks :: [XLink]
                     , XGraph -> [XNode]
startNodes :: [XNode]
                     , XGraph -> XTree
xg_body :: XTree }
  deriving (Typeable, Typeable XGraph
Constr
DataType
Typeable XGraph =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> XGraph -> c XGraph)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c XGraph)
-> (XGraph -> Constr)
-> (XGraph -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c XGraph))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c XGraph))
-> ((forall b. Data b => b -> b) -> XGraph -> XGraph)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> XGraph -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> XGraph -> r)
-> (forall u. (forall d. Data d => d -> u) -> XGraph -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> XGraph -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> XGraph -> m XGraph)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> XGraph -> m XGraph)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> XGraph -> m XGraph)
-> Data XGraph
XGraph -> Constr
XGraph -> DataType
(forall b. Data b => b -> b) -> XGraph -> XGraph
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> XGraph -> c XGraph
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c XGraph
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> XGraph -> u
forall u. (forall d. Data d => d -> u) -> XGraph -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> XGraph -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> XGraph -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> XGraph -> m XGraph
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> XGraph -> m XGraph
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c XGraph
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> XGraph -> c XGraph
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c XGraph)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c XGraph)
$cXGraph :: Constr
$tXGraph :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> XGraph -> m XGraph
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> XGraph -> m XGraph
gmapMp :: (forall d. Data d => d -> m d) -> XGraph -> m XGraph
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> XGraph -> m XGraph
gmapM :: (forall d. Data d => d -> m d) -> XGraph -> m XGraph
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> XGraph -> m XGraph
gmapQi :: Int -> (forall d. Data d => d -> u) -> XGraph -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> XGraph -> u
gmapQ :: (forall d. Data d => d -> u) -> XGraph -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> XGraph -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> XGraph -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> XGraph -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> XGraph -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> XGraph -> r
gmapT :: (forall b. Data b => b -> b) -> XGraph -> XGraph
$cgmapT :: (forall b. Data b => b -> b) -> XGraph -> XGraph
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c XGraph)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c XGraph)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c XGraph)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c XGraph)
dataTypeOf :: XGraph -> DataType
$cdataTypeOf :: XGraph -> DataType
toConstr :: XGraph -> Constr
$ctoConstr :: XGraph -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c XGraph
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c XGraph
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> XGraph -> c XGraph
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> XGraph -> c XGraph
$cp1Data :: Typeable XGraph
Data)

{- outer list must be executed in order; inner lists represent all def-links
-node bundles that can be processed in one step -}
type XTree = [[([XLink], XNode)]]

type EdgeMap = Map.Map String (Map.Map String [XLink])

data XNode = XNode { XNode -> NodeName
nodeName :: NodeName
                   , XNode -> String
logicName :: String
                   , XNode -> (Bool, String)
symbs :: (Bool, String) -- ^ hidden?
                   , XNode -> String
specs :: String -- ^ Sentences
                   , XNode -> Conservativity
nd_cons :: Conservativity }
           | XRef { nodeName :: NodeName
                  , XNode -> String
refNode :: String
                  , XNode -> String
refLib :: String
                  , specs :: String }
  deriving (Typeable, Typeable XNode
Constr
DataType
Typeable XNode =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> XNode -> c XNode)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c XNode)
-> (XNode -> Constr)
-> (XNode -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c XNode))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c XNode))
-> ((forall b. Data b => b -> b) -> XNode -> XNode)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> XNode -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> XNode -> r)
-> (forall u. (forall d. Data d => d -> u) -> XNode -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> XNode -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> XNode -> m XNode)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> XNode -> m XNode)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> XNode -> m XNode)
-> Data XNode
XNode -> Constr
XNode -> DataType
(forall b. Data b => b -> b) -> XNode -> XNode
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> XNode -> c XNode
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c XNode
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> XNode -> u
forall u. (forall d. Data d => d -> u) -> XNode -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> XNode -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> XNode -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> XNode -> m XNode
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> XNode -> m XNode
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c XNode
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> XNode -> c XNode
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c XNode)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c XNode)
$cXRef :: Constr
$cXNode :: Constr
$tXNode :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> XNode -> m XNode
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> XNode -> m XNode
gmapMp :: (forall d. Data d => d -> m d) -> XNode -> m XNode
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> XNode -> m XNode
gmapM :: (forall d. Data d => d -> m d) -> XNode -> m XNode
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> XNode -> m XNode
gmapQi :: Int -> (forall d. Data d => d -> u) -> XNode -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> XNode -> u
gmapQ :: (forall d. Data d => d -> u) -> XNode -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> XNode -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> XNode -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> XNode -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> XNode -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> XNode -> r
gmapT :: (forall b. Data b => b -> b) -> XNode -> XNode
$cgmapT :: (forall b. Data b => b -> b) -> XNode -> XNode
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c XNode)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c XNode)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c XNode)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c XNode)
dataTypeOf :: XNode -> DataType
$cdataTypeOf :: XNode -> DataType
toConstr :: XNode -> Constr
$ctoConstr :: XNode -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c XNode
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c XNode
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> XNode -> c XNode
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> XNode -> c XNode
$cp1Data :: Typeable XNode
Data)

data XLink = XLink { XLink -> String
source :: String
                   , XLink -> String
target :: String
                   , XLink -> EdgeId
edgeId :: EdgeId
                   , XLink -> DGEdgeType
lType :: DGEdgeType
                   , XLink -> DGRule
rule :: DGRule
                   , XLink -> Conservativity
cons :: Conservativity
                   , XLink -> ProofBasis
prBasis :: ProofBasis
                   , XLink -> String
mr_name :: String
                   , XLink -> Maybe String
mr_source :: Maybe String
                   , XLink -> String
mapping :: String }
  deriving (Typeable, Typeable XLink
Constr
DataType
Typeable XLink =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> XLink -> c XLink)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c XLink)
-> (XLink -> Constr)
-> (XLink -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c XLink))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c XLink))
-> ((forall b. Data b => b -> b) -> XLink -> XLink)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> XLink -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> XLink -> r)
-> (forall u. (forall d. Data d => d -> u) -> XLink -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> XLink -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> XLink -> m XLink)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> XLink -> m XLink)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> XLink -> m XLink)
-> Data XLink
XLink -> Constr
XLink -> DataType
(forall b. Data b => b -> b) -> XLink -> XLink
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> XLink -> c XLink
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c XLink
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> XLink -> u
forall u. (forall d. Data d => d -> u) -> XLink -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> XLink -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> XLink -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> XLink -> m XLink
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> XLink -> m XLink
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c XLink
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> XLink -> c XLink
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c XLink)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c XLink)
$cXLink :: Constr
$tXLink :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> XLink -> m XLink
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> XLink -> m XLink
gmapMp :: (forall d. Data d => d -> m d) -> XLink -> m XLink
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> XLink -> m XLink
gmapM :: (forall d. Data d => d -> m d) -> XLink -> m XLink
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> XLink -> m XLink
gmapQi :: Int -> (forall d. Data d => d -> u) -> XLink -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> XLink -> u
gmapQ :: (forall d. Data d => d -> u) -> XLink -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> XLink -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> XLink -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> XLink -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> XLink -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> XLink -> r
gmapT :: (forall b. Data b => b -> b) -> XLink -> XLink
$cgmapT :: (forall b. Data b => b -> b) -> XLink -> XLink
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c XLink)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c XLink)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c XLink)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c XLink)
dataTypeOf :: XLink -> DataType
$cdataTypeOf :: XLink -> DataType
toConstr :: XLink -> Constr
$ctoConstr :: XLink -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c XLink
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c XLink
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> XLink -> c XLink
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> XLink -> c XLink
$cp1Data :: Typeable XLink
Data)

instance Show XNode where
  show :: XNode -> String
show xn :: XNode
xn = NodeName -> String
showName (XNode -> NodeName
nodeName XNode
xn)

instance Show XLink where
  show :: XLink -> String
show xl :: XLink
xl = EdgeId -> String
showEdgeId (XLink -> EdgeId
edgeId XLink
xl) String -> ShowS
forall a. [a] -> [a] -> [a]
++ ": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ XLink -> String
source XLink
xl String -> ShowS
forall a. [a] -> [a] -> [a]
++ " -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ XLink -> String
target XLink
xl

instance Ord XLink where
  compare :: XLink -> XLink -> Ordering
compare xl1 :: XLink
xl1 xl2 :: XLink
xl2 = (EdgeId, String, String) -> (EdgeId, String, String) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (XLink -> EdgeId
edgeId XLink
xl1, XLink -> String
source XLink
xl1, XLink -> String
target XLink
xl1)
    (XLink -> EdgeId
edgeId XLink
xl2, XLink -> String
source XLink
xl2, XLink -> String
target XLink
xl2)

instance Eq XLink where
  a :: XLink
a == :: XLink -> XLink -> Bool
== b :: XLink
b = XLink -> XLink -> Ordering
forall a. Ord a => a -> a -> Ordering
compare XLink
a XLink
b Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ

{- ------------
Functions -}

insertXLink :: XLink -> EdgeMap -> EdgeMap
insertXLink :: XLink -> EdgeMap -> EdgeMap
insertXLink l :: XLink
l = (Map String [XLink] -> Map String [XLink] -> Map String [XLink])
-> String -> Map String [XLink] -> EdgeMap -> EdgeMap
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (([XLink] -> [XLink] -> [XLink])
-> Map String [XLink] -> Map String [XLink] -> Map String [XLink]
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith [XLink] -> [XLink] -> [XLink]
forall a. [a] -> [a] -> [a]
(++)) (XLink -> String
target XLink
l)
  (Map String [XLink] -> EdgeMap -> EdgeMap)
-> Map String [XLink] -> EdgeMap -> EdgeMap
forall a b. (a -> b) -> a -> b
$ String -> [XLink] -> Map String [XLink]
forall k a. k -> a -> Map k a
Map.singleton (XLink -> String
source XLink
l) [XLink
l]

mkEdgeMap :: [XLink] -> EdgeMap
mkEdgeMap :: [XLink] -> EdgeMap
mkEdgeMap = (EdgeMap -> XLink -> EdgeMap) -> EdgeMap -> [XLink] -> EdgeMap
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((XLink -> EdgeMap -> EdgeMap) -> EdgeMap -> XLink -> EdgeMap
forall a b c. (a -> b -> c) -> b -> a -> c
flip XLink -> EdgeMap -> EdgeMap
insertXLink) EdgeMap
forall k a. Map k a
Map.empty

xGraph :: Element -> Result XGraph
xGraph :: Element -> Result XGraph
xGraph xml :: Element
xml = do
  [XNode]
allNodes <- Element -> Result [XNode]
forall (m :: * -> *). MonadFail m => Element -> m [XNode]
extractXNodes Element
xml
  [XLink]
allLinks <- Element -> Result [XLink]
forall (m :: * -> *). MonadFail m => Element -> m [XLink]
extractXLinks Element
xml
  Set EdgeId
_ <- (Set EdgeId -> XLink -> Result (Set EdgeId))
-> Set EdgeId -> [XLink] -> Result (Set EdgeId)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ s :: Set EdgeId
s l :: XLink
l -> let e :: EdgeId
e = XLink -> EdgeId
edgeId XLink
l in
    if EdgeId -> Set EdgeId -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member EdgeId
e Set EdgeId
s then String -> Result (Set EdgeId)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result (Set EdgeId)) -> String -> Result (Set EdgeId)
forall a b. (a -> b) -> a -> b
$ "duplicate edge id: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ EdgeId -> String
forall a. Show a => a -> String
show EdgeId
e
    else Set EdgeId -> Result (Set EdgeId)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set EdgeId -> Result (Set EdgeId))
-> Set EdgeId -> Result (Set EdgeId)
forall a b. (a -> b) -> a -> b
$ EdgeId -> Set EdgeId -> Set EdgeId
forall a. Ord a => a -> Set a -> Set a
Set.insert EdgeId
e Set EdgeId
s) Set EdgeId
forall a. Set a
Set.empty [XLink]
allLinks
  Map String XNode
nodeMap <- (Map String XNode -> XNode -> Result (Map String XNode))
-> Map String XNode -> [XNode] -> Result (Map String XNode)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ m :: Map String XNode
m n :: XNode
n -> let s :: String
s = NodeName -> String
showName (NodeName -> String) -> NodeName -> String
forall a b. (a -> b) -> a -> b
$ XNode -> NodeName
nodeName XNode
n in
    if String -> Map String XNode -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member String
s Map String XNode
m then String -> Result (Map String XNode)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result (Map String XNode))
-> String -> Result (Map String XNode)
forall a b. (a -> b) -> a -> b
$ "duplicate node name: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
       else Map String XNode -> Result (Map String XNode)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map String XNode -> Result (Map String XNode))
-> Map String XNode -> Result (Map String XNode)
forall a b. (a -> b) -> a -> b
$ String -> XNode -> Map String XNode -> Map String XNode
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
s XNode
n Map String XNode
m) Map String XNode
forall k a. Map k a
Map.empty [XNode]
allNodes
  let (thmLk :: [XLink]
thmLk, defLk :: [XLink]
defLk) = (XLink -> Bool) -> [XLink] -> ([XLink], [XLink])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\ l :: XLink
l -> case DGEdgeType -> DGEdgeTypeModInc
edgeTypeModInc (DGEdgeType -> DGEdgeTypeModInc) -> DGEdgeType -> DGEdgeTypeModInc
forall a b. (a -> b) -> a -> b
$ XLink -> DGEdgeType
lType XLink
l of
                         ThmType {} -> Bool
True
                         _ -> Bool
False) [XLink]
allLinks
      edgeMap :: EdgeMap
edgeMap = [XLink] -> EdgeMap
mkEdgeMap [XLink]
defLk
      (initN :: Map String XNode
initN, restN :: Map String XNode
restN) = (String -> XNode -> Bool)
-> Map String XNode -> (Map String XNode, Map String XNode)
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey
         (\ n :: String
n _ -> String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember String
n (Set String -> Bool) -> Set String -> Bool
forall a b. (a -> b) -> a -> b
$ EdgeMap -> Set String
forall k a. Map k a -> Set k
Map.keysSet EdgeMap
edgeMap)
         Map String XNode
nodeMap
      tgts :: Set String
tgts = Map String XNode -> Set String
forall k a. Map k a -> Set k
Map.keysSet Map String XNode
nodeMap
      missingTgts :: Set String
missingTgts = Set String -> Set String -> Set String
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (EdgeMap -> Set String
forall k a. Map k a -> Set k
Map.keysSet EdgeMap
edgeMap) Set String
tgts
      srcs :: Set String
srcs = [Set String] -> Set String
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set String] -> Set String) -> [Set String] -> Set String
forall a b. (a -> b) -> a -> b
$ (Map String [XLink] -> Set String)
-> [Map String [XLink]] -> [Set String]
forall a b. (a -> b) -> [a] -> [b]
map Map String [XLink] -> Set String
forall k a. Map k a -> Set k
Map.keysSet ([Map String [XLink]] -> [Set String])
-> [Map String [XLink]] -> [Set String]
forall a b. (a -> b) -> a -> b
$ EdgeMap -> [Map String [XLink]]
forall k a. Map k a -> [a]
Map.elems EdgeMap
edgeMap
      missingSrcs :: Set String
missingSrcs = Set String -> Set String -> Set String
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set String
srcs Set String
tgts
  Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set String -> Bool
forall a. Set a -> Bool
Set.null Set String
missingTgts)
    (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result ()) -> String -> Result ()
forall a b. (a -> b) -> a -> b
$ "missing nodes for edge targets " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set String -> String
forall a. Show a => a -> String
show Set String
missingTgts
  Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set String -> Bool
forall a. Set a -> Bool
Set.null Set String
missingSrcs)
    (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result ()) -> String -> Result ()
forall a b. (a -> b) -> a -> b
$ "missing nodes for edge sources " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set String -> String
forall a. Show a => a -> String
show Set String
missingSrcs
  String
nm <- String -> Element -> Result String
forall (m :: * -> *). MonadFail m => String -> Element -> m String
getAttrVal "libname" Element
xml
  String
fl <- String -> Element -> Result String
forall (m :: * -> *). MonadFail m => String -> Element -> m String
getAttrVal "filename" Element
xml
  let ln :: LibName
ln = String -> LibName -> LibName
setFilePath String
fl (LibName -> LibName) -> LibName -> LibName
forall a b. (a -> b) -> a -> b
$ String -> LibName
emptyLibName String
nm
  GlobalAnnos
ga <- Element -> Result GlobalAnnos
extractGlobalAnnos Element
xml
  EdgeId
i' <- (String -> EdgeId) -> Result String -> Result EdgeId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> EdgeId
readEdgeId (Result String -> Result EdgeId) -> Result String -> Result EdgeId
forall a b. (a -> b) -> a -> b
$ String -> Element -> Result String
forall (m :: * -> *). MonadFail m => String -> Element -> m String
getAttrVal "nextlinkid" Element
xml
  XTree
xg <- Set String -> EdgeMap -> Map String XNode -> XTree -> Result XTree
forall (m :: * -> *).
MonadFail m =>
Set String -> EdgeMap -> Map String XNode -> XTree -> m XTree
builtXGraph (Map String XNode -> Set String
forall k a. Map k a -> Set k
Map.keysSet Map String XNode
initN) EdgeMap
edgeMap Map String XNode
restN []
  XGraph -> Result XGraph
forall (m :: * -> *) a. Monad m => a -> m a
return (XGraph -> Result XGraph) -> XGraph -> Result XGraph
forall a b. (a -> b) -> a -> b
$ LibName
-> GlobalAnnos -> EdgeId -> [XLink] -> [XNode] -> XTree -> XGraph
XGraph LibName
ln GlobalAnnos
ga EdgeId
i' [XLink]
thmLk (Map String XNode -> [XNode]
forall k a. Map k a -> [a]
Map.elems Map String XNode
initN) XTree
xg

builtXGraph :: Fail.MonadFail m => Set.Set String -> EdgeMap -> Map.Map String XNode
            -> XTree -> m XTree
builtXGraph :: Set String -> EdgeMap -> Map String XNode -> XTree -> m XTree
builtXGraph ns :: Set String
ns xls :: EdgeMap
xls xns :: Map String XNode
xns xg :: XTree
xg = if EdgeMap -> Bool
forall k a. Map k a -> Bool
Map.null EdgeMap
xls Bool -> Bool -> Bool
&& Map String XNode -> Bool
forall k a. Map k a -> Bool
Map.null Map String XNode
xns then XTree -> m XTree
forall (m :: * -> *) a. Monad m => a -> m a
return XTree
xg
  else do
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (EdgeMap -> Bool
forall k a. Map k a -> Bool
Map.null EdgeMap
xls) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "unprocessed nodes: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set String -> String
forall a. Show a => a -> String
show (Map String XNode -> Set String
forall k a. Map k a -> Set k
Map.keysSet Map String XNode
xns)
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Map String XNode -> Bool
forall k a. Map k a -> Bool
Map.null Map String XNode
xns) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "unprocessed links: "
       String -> ShowS
forall a. [a] -> [a] -> [a]
++ [EdgeId] -> String
forall a. Show a => a -> String
show ((XLink -> EdgeId) -> [XLink] -> [EdgeId]
forall a b. (a -> b) -> [a] -> [b]
map XLink -> EdgeId
edgeId ([XLink] -> [EdgeId]) -> [XLink] -> [EdgeId]
forall a b. (a -> b) -> a -> b
$ [[XLink]] -> [XLink]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[XLink]] -> [XLink]) -> [[XLink]] -> [XLink]
forall a b. (a -> b) -> a -> b
$ (Map String [XLink] -> [[XLink]])
-> [Map String [XLink]] -> [[XLink]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Map String [XLink] -> [[XLink]]
forall k a. Map k a -> [a]
Map.elems ([Map String [XLink]] -> [[XLink]])
-> [Map String [XLink]] -> [[XLink]]
forall a b. (a -> b) -> a -> b
$ EdgeMap -> [Map String [XLink]]
forall k a. Map k a -> [a]
Map.elems EdgeMap
xls)
  let (sls :: EdgeMap
sls, rls :: EdgeMap
rls) = (Map String [XLink] -> Bool) -> EdgeMap -> (EdgeMap, EdgeMap)
forall a k. (a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partition ((Set String -> Set String -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set String
ns) (Set String -> Bool)
-> (Map String [XLink] -> Set String) -> Map String [XLink] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map String [XLink] -> Set String
forall k a. Map k a -> Set k
Map.keysSet) EdgeMap
xls
      bs :: Map String (Map String [XLink], XNode)
bs = (Map String [XLink] -> XNode -> (Map String [XLink], XNode))
-> EdgeMap
-> Map String XNode
-> Map String (Map String [XLink], XNode)
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith (,) EdgeMap
sls Map String XNode
xns
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Map String (Map String [XLink], XNode) -> Bool
forall k a. Map k a -> Bool
Map.null Map String (Map String [XLink], XNode)
bs) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "cannot continue with source nodes:\n "
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set String -> String
forall a. Show a => a -> String
show (Set String -> Set String -> Set String
forall a. Ord a => Set a -> Set a -> Set a
Set.difference ([Set String] -> Set String
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set String] -> Set String) -> [Set String] -> Set String
forall a b. (a -> b) -> a -> b
$ (Map String [XLink] -> Set String)
-> [Map String [XLink]] -> [Set String]
forall a b. (a -> b) -> [a] -> [b]
map Map String [XLink] -> Set String
forall k a. Map k a -> Set k
Map.keysSet ([Map String [XLink]] -> [Set String])
-> [Map String [XLink]] -> [Set String]
forall a b. (a -> b) -> a -> b
$ EdgeMap -> [Map String [XLink]]
forall k a. Map k a -> [a]
Map.elems EdgeMap
rls) Set String
ns)
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nfor given nodes: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set String -> String
forall a. Show a => a -> String
show Set String
ns
  Set String -> EdgeMap -> Map String XNode -> XTree -> m XTree
forall (m :: * -> *).
MonadFail m =>
Set String -> EdgeMap -> Map String XNode -> XTree -> m XTree
builtXGraph (Set String -> Set String -> Set String
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set String
ns (Set String -> Set String) -> Set String -> Set String
forall a b. (a -> b) -> a -> b
$ Map String (Map String [XLink], XNode) -> Set String
forall k a. Map k a -> Set k
Map.keysSet Map String (Map String [XLink], XNode)
bs) EdgeMap
rls
    (Map String XNode
-> Map String (Map String [XLink], XNode) -> Map String XNode
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.difference Map String XNode
xns Map String (Map String [XLink], XNode)
bs) (XTree -> m XTree) -> XTree -> m XTree
forall a b. (a -> b) -> a -> b
$
       ((Map String [XLink], XNode) -> ([XLink], XNode))
-> [(Map String [XLink], XNode)] -> [([XLink], XNode)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (m :: Map String [XLink]
m, x :: XNode
x) -> ([[XLink]] -> [XLink]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[XLink]] -> [XLink]) -> [[XLink]] -> [XLink]
forall a b. (a -> b) -> a -> b
$ Map String [XLink] -> [[XLink]]
forall k a. Map k a -> [a]
Map.elems Map String [XLink]
m, XNode
x)) (Map String (Map String [XLink], XNode)
-> [(Map String [XLink], XNode)]
forall k a. Map k a -> [a]
Map.elems Map String (Map String [XLink], XNode)
bs) [([XLink], XNode)] -> XTree -> XTree
forall a. a -> [a] -> [a]
: XTree
xg

extractXNodes :: Fail.MonadFail m => Element -> m [XNode]
extractXNodes :: Element -> m [XNode]
extractXNodes = (Element -> m XNode) -> [Element] -> m [XNode]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Element -> m XNode
forall (m :: * -> *). MonadFail m => Element -> m XNode
mkXNode ([Element] -> m [XNode])
-> (Element -> [Element]) -> Element -> m [XNode]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Element -> [Element]
findChildren (String -> QName
unqual "DGNode")

extractXLinks :: Fail.MonadFail m => Element -> m [XLink]
extractXLinks :: Element -> m [XLink]
extractXLinks = (Element -> m XLink) -> [Element] -> m [XLink]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Element -> m XLink
forall (m :: * -> *). MonadFail m => Element -> m XLink
mkXLink ([Element] -> m [XLink])
-> (Element -> [Element]) -> Element -> m [XLink]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Element -> [Element]
findChildren (String -> QName
unqual "DGLink")

mkXNode :: Fail.MonadFail m => Element -> m XNode
mkXNode :: Element -> m XNode
mkXNode el :: Element
el = let spcs :: String
spcs = [String] -> String
unlines ([String] -> String)
-> ([Element] -> [String]) -> [Element] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Element -> String) -> [Element] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Element -> String
strContent
                   ([Element] -> [String])
-> ([Element] -> [Element]) -> [Element] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Element -> [Element]) -> [Element] -> [Element]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (QName -> Element -> [Element]
findChildren (QName -> Element -> [Element]) -> QName -> Element -> [Element]
forall a b. (a -> b) -> a -> b
$ String -> QName
unqual "Text")
                   ([Element] -> String) -> [Element] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> Element -> [Element]
deepSearch ["Axiom", "Theorem"] Element
el
                 get :: ([String] -> c) -> String -> Element -> c
get f :: [String] -> c
f s :: String
s = [String] -> c
f ([String] -> c) -> (Element -> [String]) -> Element -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Element -> String) -> [Element] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Element -> String
strContent ([Element] -> [String])
-> (Element -> [Element]) -> Element -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> Element -> [Element]
deepSearch [String
s]
                 get' :: String -> Element -> String
get' = ([String] -> String) -> String -> Element -> String
forall c. ([String] -> c) -> String -> Element -> c
get [String] -> String
unlines in do
  NodeName
nm <- Element -> m NodeName
forall (m :: * -> *). MonadFail m => Element -> m NodeName
extractNodeName Element
el
  case QName -> Element -> Maybe Element
findChild (String -> QName
unqual "Reference") Element
el of
    Just rf :: Element
rf -> do
      String
rfNm <- String -> Element -> m String
forall (m :: * -> *). MonadFail m => String -> Element -> m String
getAttrVal "node" Element
rf
      String
rfLib <- String -> Element -> m String
forall (m :: * -> *). MonadFail m => String -> Element -> m String
getAttrVal "library" Element
rf
      XNode -> m XNode
forall (m :: * -> *) a. Monad m => a -> m a
return (XNode -> m XNode) -> XNode -> m XNode
forall a b. (a -> b) -> a -> b
$ NodeName -> String -> String -> String -> XNode
XRef NodeName
nm String
rfNm String
rfLib String
spcs
    Nothing -> let
      hdSyms :: (Bool, String)
hdSyms = case QName -> Element -> Maybe Element
findChild (String -> QName
unqual "Hidden") Element
el of
            Nothing -> case QName -> Element -> Maybe Element
findChild (String -> QName
unqual "Declarations") Element
el of
              -- Case #1: No declared or hidden symbols
              Nothing -> (Bool
False, "")
              -- Case #2: Node has declared symbols (DGBasicSpec)
              Just ch :: Element
ch -> (Bool
False, String -> Element -> String
get' "Symbol" Element
ch)
            -- Case #3: Node has hidden symbols (DGRestricted)
            Just ch :: Element
ch -> (Bool
True, ([String] -> String) -> String -> Element -> String
forall c. ([String] -> c) -> String -> Element -> c
get (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", ") "Symbol" Element
ch)
      in do
        String
lgN <- String -> Element -> m String
forall (m :: * -> *). MonadFail m => String -> Element -> m String
getAttrVal "logic" Element
el
        String
xp0 <- String -> Element -> m String
forall (m :: * -> *). MonadFail m => String -> Element -> m String
getAttrVal "relxpath" Element
el
        String
nm0 <- String -> Element -> m String
forall (m :: * -> *). MonadFail m => String -> Element -> m String
getAttrVal "refname" Element
el
        [XPathPart]
xp1 <- String -> m [XPathPart]
forall (m :: * -> *). MonadFail m => String -> m [XPathPart]
readXPath (String
nm0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
xp0)
        XNode -> m XNode
forall (m :: * -> *) a. Monad m => a -> m a
return (XNode -> m XNode) -> XNode -> m XNode
forall a b. (a -> b) -> a -> b
$ NodeName
-> String -> (Bool, String) -> String -> Conservativity -> XNode
XNode NodeName
nm { xpath :: [XPathPart]
xpath = [XPathPart] -> [XPathPart]
forall a. [a] -> [a]
reverse [XPathPart]
xp1 } String
lgN (Bool, String)
hdSyms String
spcs (Conservativity -> XNode) -> Conservativity -> XNode
forall a b. (a -> b) -> a -> b
$ Element -> Conservativity
readCons Element
el

extractNodeName :: Fail.MonadFail m => Element -> m NodeName
extractNodeName :: Element -> m NodeName
extractNodeName e :: Element
e = (String -> NodeName) -> m String -> m NodeName
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM String -> NodeName
parseNodeName (m String -> m NodeName) -> m String -> m NodeName
forall a b. (a -> b) -> a -> b
$ String -> Element -> m String
forall (m :: * -> *). MonadFail m => String -> Element -> m String
getAttrVal "name" Element
e

mkXLink :: Fail.MonadFail m => Element -> m XLink
mkXLink :: Element -> m XLink
mkXLink el :: Element
el = do
  String
sr <- String -> Element -> m String
forall (m :: * -> *). MonadFail m => String -> Element -> m String
getAttrVal "source" Element
el
  String
tr <- String -> Element -> m String
forall (m :: * -> *). MonadFail m => String -> Element -> m String
getAttrVal "target" Element
el
  EdgeId
ei <- Element -> m EdgeId
forall (m :: * -> *). MonadFail m => Element -> m EdgeId
extractEdgeId Element
el
  DGEdgeType
tp <- case QName -> Element -> Maybe Element
findChild (String -> QName
unqual "Type") Element
el of
          Just tp' :: Element
tp' -> DGEdgeType -> m DGEdgeType
forall (m :: * -> *) a. Monad m => a -> m a
return (DGEdgeType -> m DGEdgeType) -> DGEdgeType -> m DGEdgeType
forall a b. (a -> b) -> a -> b
$ String -> DGEdgeType
revertDGEdgeTypeName (String -> DGEdgeType) -> String -> DGEdgeType
forall a b. (a -> b) -> a -> b
$ Element -> String
strContent Element
tp'
          Nothing -> String -> m DGEdgeType
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "links type description is missing"
  DGRule
rl <- case QName -> Element -> Maybe Element
findChild (String -> QName
unqual "Rule") Element
el of
          Nothing -> DGRule -> m DGRule
forall (m :: * -> *) a. Monad m => a -> m a
return (DGRule -> m DGRule) -> DGRule -> m DGRule
forall a b. (a -> b) -> a -> b
$ String -> DGRule
DGRule "no rule"
          Just r' :: Element
r' -> case QName -> Element -> [Element]
findChildren (String -> QName
unqual "MovedTheorems") Element
el of
            [] -> DGRule -> m DGRule
forall (m :: * -> *) a. Monad m => a -> m a
return (DGRule -> m DGRule) -> DGRule -> m DGRule
forall a b. (a -> b) -> a -> b
$ String -> DGRule
DGRule (String -> DGRule) -> String -> DGRule
forall a b. (a -> b) -> a -> b
$ Element -> String
strContent Element
r'
            mThs :: [Element]
mThs -> ([(String, String)] -> DGRule) -> m [(String, String)] -> m DGRule
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [(String, String)] -> DGRule
DGRuleLocalInference (m [(String, String)] -> m DGRule)
-> m [(String, String)] -> m DGRule
forall a b. (a -> b) -> a -> b
$ (Element -> m (String, String))
-> [Element] -> m [(String, String)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ e :: Element
e -> do
                String
nmOld <- String -> Element -> m String
forall (m :: * -> *). MonadFail m => String -> Element -> m String
getAttrVal "name" Element
e
                String
nmNew <- String -> Element -> m String
forall (m :: * -> *). MonadFail m => String -> Element -> m String
getAttrVal "renamedTo" Element
e
                (String, String) -> m (String, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
nmOld, String
nmNew)) [Element]
mThs
  [String]
prB <- (Element -> m String) -> [Element] -> m [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String -> Element -> m String
forall (m :: * -> *). MonadFail m => String -> Element -> m String
getAttrVal "linkref") ([Element] -> m [String]) -> [Element] -> m [String]
forall a b. (a -> b) -> a -> b
$ QName -> Element -> [Element]
findChildren (String -> QName
unqual "ProofBasis") Element
el
  (mrNm :: String
mrNm, mrSrc :: Maybe String
mrSrc) <- case QName -> Element -> Maybe Element
findChild (String -> QName
unqual "GMorphism") Element
el of
    Nothing -> String -> m (String, Maybe String)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Links morphism description is missing!"
    Just mor :: Element
mor -> do
        String
nm <- String -> Element -> m String
forall (m :: * -> *). MonadFail m => String -> Element -> m String
getAttrVal "name" Element
mor
        (String, Maybe String) -> m (String, Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
nm, QName -> Element -> Maybe String
findAttr (String -> QName
unqual "morphismsource") Element
mor)
  let parseSymbMap :: Element -> String
parseSymbMap = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " ([String] -> String) -> (Element -> [String]) -> Element -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Element -> String) -> [Element] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ( String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate " |-> "
          ([String] -> String) -> (Element -> [String]) -> Element -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Element -> String) -> [Element] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Element -> String
strContent ([Element] -> [String])
-> (Element -> [Element]) -> Element -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Element -> [Element]
elChildren ) ([Element] -> [String])
-> (Element -> [Element]) -> Element -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> Element -> [Element]
deepSearch ["map"]
      prBs :: ProofBasis
prBs = Set EdgeId -> ProofBasis
ProofBasis (Set EdgeId -> ProofBasis) -> Set EdgeId -> ProofBasis
forall a b. (a -> b) -> a -> b
$ (String -> Set EdgeId -> Set EdgeId)
-> Set EdgeId -> [String] -> Set EdgeId
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (EdgeId -> Set EdgeId -> Set EdgeId
forall a. Ord a => a -> Set a -> Set a
Set.insert (EdgeId -> Set EdgeId -> Set EdgeId)
-> (String -> EdgeId) -> String -> Set EdgeId -> Set EdgeId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> EdgeId
readEdgeId) Set EdgeId
forall a. Set a
Set.empty [String]
prB
      cc :: Conservativity
cc = Element -> Conservativity
readCons Element
el
  XLink -> m XLink
forall (m :: * -> *) a. Monad m => a -> m a
return (XLink -> m XLink) -> XLink -> m XLink
forall a b. (a -> b) -> a -> b
$ String
-> String
-> EdgeId
-> DGEdgeType
-> DGRule
-> Conservativity
-> ProofBasis
-> String
-> Maybe String
-> String
-> XLink
XLink String
sr String
tr EdgeId
ei DGEdgeType
tp DGRule
rl Conservativity
cc ProofBasis
prBs String
mrNm Maybe String
mrSrc (String -> XLink) -> String -> XLink
forall a b. (a -> b) -> a -> b
$ Element -> String
parseSymbMap Element
el

readCons :: Element -> Conservativity
readCons :: Element -> Conservativity
readCons el :: Element
el = case QName -> Element -> Maybe Element
findChild (String -> QName
unqual "ConsStatus") Element
el of
  Nothing -> Conservativity
None
  Just c' :: Element
c' -> Conservativity -> Maybe Conservativity -> Conservativity
forall a. a -> Maybe a -> a
fromMaybe Conservativity
None (Maybe Conservativity -> Conservativity)
-> Maybe Conservativity -> Conservativity
forall a b. (a -> b) -> a -> b
$ String -> Maybe Conservativity
forall a. Read a => String -> Maybe a
readMaybe (String -> Maybe Conservativity) -> String -> Maybe Conservativity
forall a b. (a -> b) -> a -> b
$ Element -> String
strContent Element
c'

extractEdgeId :: Fail.MonadFail m => Element -> m EdgeId
extractEdgeId :: Element -> m EdgeId
extractEdgeId = (Int -> EdgeId) -> m Int -> m EdgeId
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> EdgeId
EdgeId (m Int -> m EdgeId) -> (Element -> m Int) -> Element -> m EdgeId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> Element -> m Int
forall a (m :: * -> *).
(Read a, MonadFail m) =>
String -> String -> Element -> m a
readAttrVal "XGraph.extractEdgeId" "linkid"

readEdgeId :: String -> EdgeId
readEdgeId :: String -> EdgeId
readEdgeId = Int -> EdgeId
EdgeId (Int -> EdgeId) -> (String -> Int) -> String -> EdgeId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe (-1) (Maybe Int -> Int) -> (String -> Maybe Int) -> String -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe Int
forall a. Read a => String -> Maybe a
readMaybe

-- | custom xml-search for not only immediate children
deepSearch :: [String] -> Element -> [Element]
deepSearch :: [String] -> Element -> [Element]
deepSearch tags :: [String]
tags e :: Element
e = Element -> [Element]
filtr Element
e [Element] -> [Element] -> [Element]
forall a. [a] -> [a] -> [a]
++ (Element -> [Element]) -> [Element] -> [Element]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Element -> [Element]
filtr (Element -> [Element]
elChildren Element
e) where
  filtr :: Element -> [Element]
filtr = (QName -> Bool) -> Element -> [Element]
filterChildrenName (QName -> [QName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (String -> QName) -> [String] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map String -> QName
unqual [String]
tags)

-- | extracts the global annotations from the xml-graph
extractGlobalAnnos :: Element -> Result GlobalAnnos
extractGlobalAnnos :: Element -> Result GlobalAnnos
extractGlobalAnnos dgEle :: Element
dgEle = case QName -> Element -> Maybe Element
findChild (String -> QName
unqual "Global") Element
dgEle of
  Nothing -> GlobalAnnos -> Result GlobalAnnos
forall (m :: * -> *) a. Monad m => a -> m a
return GlobalAnnos
emptyGlobalAnnos
  Just gl :: Element
gl -> Element -> Result GlobalAnnos
parseAnnotations Element
gl

parseAnnotations :: Element -> Result GlobalAnnos
parseAnnotations :: Element -> Result GlobalAnnos
parseAnnotations = String -> Result GlobalAnnos
getGlobalAnnos (String -> Result GlobalAnnos)
-> (Element -> String) -> Element -> Result GlobalAnnos
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines ([String] -> String) -> (Element -> [String]) -> Element -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Element -> String) -> [Element] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Element -> String
strContent
    ([Element] -> [String])
-> (Element -> [Element]) -> Element -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Element -> [Element]
findChildren (String -> QName
unqual "Annotation")