{-# OPTIONS -w -O0 #-}
{-# LANGUAGE CPP, StandaloneDeriving, DeriveDataTypeable, DeriveGeneric #-}
module ATC.XGraph () where
import ATC.DgUtils
import ATC.Grothendieck
import ATerm.Lib
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 Data.Data
import Data.List
import Data.Maybe (fromMaybe)
import Static.DgUtils
import Static.XGraph
import Text.XML.Light
import qualified Control.Monad.Fail as Fail
import qualified Data.Map as Map
import qualified Data.Set as Set
instance ShATermLG Static.XGraph.XGraph where
toShATermLG :: ATermTable -> XGraph -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: XGraph
xv = case XGraph
xv of
XGraph a :: LibName
a b :: GlobalAnnos
b c :: EdgeId
c d :: [XLink]
d e :: [XNode]
e f :: XTree
f -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> LibName -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 LibName
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> GlobalAnnos -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 GlobalAnnos
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> EdgeId -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 EdgeId
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> [XLink] -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att3 [XLink]
d
(att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> [XNode] -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att4 [XNode]
e
(att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> XTree -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att5 XTree
f
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "XGraph" [Int
a', Int
b', Int
c', Int
d', Int
e',
Int
f'] []) ATermTable
att6
fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, XGraph)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "XGraph" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e, f :: Int
f] _ ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, LibName)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: LibName
a') ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, GlobalAnnos)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: GlobalAnnos
b') ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, EdgeId)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: EdgeId
c') ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, [XLink])
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: [XLink]
d') ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, [XNode])
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
e ATermTable
att4 of
{ (att5 :: ATermTable
att5, e' :: [XNode]
e') ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, XTree)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
f ATermTable
att5 of
{ (att6 :: ATermTable
att6, f' :: XTree
f') ->
(ATermTable
att6, LibName
-> GlobalAnnos -> EdgeId -> [XLink] -> [XNode] -> XTree -> XGraph
XGraph LibName
a' GlobalAnnos
b' EdgeId
c' [XLink]
d' [XNode]
e' XTree
f') }}}}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, XGraph)
forall a. String -> ShATerm -> a
fromShATermError "Static.XGraph.XGraph" ShATerm
u
instance ShATermLG Static.XGraph.XNode where
toShATermLG :: ATermTable -> XNode -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: XNode
xv = case XNode
xv of
XNode a :: NodeName
a b :: String
b c :: (Bool, String)
c d :: String
d e :: Conservativity
e -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NodeName -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 NodeName
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 String
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> (Bool, String) -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 (Bool, String)
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att3 String
d
(att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> Conservativity -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att4 Conservativity
e
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "XNode" [Int
a', Int
b', Int
c', Int
d', Int
e'] []) ATermTable
att5
XRef a :: NodeName
a b :: String
b c :: String
c d :: String
d -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NodeName -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 NodeName
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 String
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 String
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att3 String
d
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "XRef" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, XNode)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "XNode" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e] _ ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, NodeName)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: NodeName
a') ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: String
b') ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, (Bool, String))
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: (Bool, String)
c') ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: String
d') ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, Conservativity)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
e ATermTable
att4 of
{ (att5 :: ATermTable
att5, e' :: Conservativity
e') ->
(ATermTable
att5, NodeName
-> String -> (Bool, String) -> String -> Conservativity -> XNode
XNode NodeName
a' String
b' (Bool, String)
c' String
d' Conservativity
e') }}}}}
ShAAppl "XRef" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, NodeName)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: NodeName
a') ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: String
b') ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: String
c') ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: String
d') ->
(ATermTable
att4, NodeName -> String -> String -> String -> XNode
XRef NodeName
a' String
b' String
c' String
d') }}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, XNode)
forall a. String -> ShATerm -> a
fromShATermError "Static.XGraph.XNode" ShATerm
u
instance ShATermLG Static.XGraph.XLink where
toShATermLG :: ATermTable -> XLink -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: XLink
xv = case XLink
xv of
XLink a :: String
a b :: String
b c :: EdgeId
c d :: DGEdgeType
d e :: DGRule
e f :: Conservativity
f g :: ProofBasis
g h :: String
h i :: Maybe String
i j :: String
j -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 String
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 String
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> EdgeId -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 EdgeId
c
(att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> DGEdgeType -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att3 DGEdgeType
d
(att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> DGRule -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att4 DGRule
e
(att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> Conservativity -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att5 Conservativity
f
(att7 :: ATermTable
att7, g' :: Int
g') <- ATermTable -> ProofBasis -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att6 ProofBasis
g
(att8 :: ATermTable
att8, h' :: Int
h') <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att7 String
h
(att9 :: ATermTable
att9, i' :: Int
i') <- ATermTable -> Maybe String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att8 Maybe String
i
(att10 :: ATermTable
att10, j' :: Int
j') <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att9 String
j
(ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "XLink" [Int
a', Int
b', Int
c', Int
d', Int
e', Int
f', Int
g', Int
h',
Int
i', Int
j'] []) ATermTable
att10
fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, XLink)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "XLink" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e, f :: Int
f, g :: Int
g, h :: Int
h, i :: Int
i, j :: Int
j] _ ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: String
a') ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: String
b') ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, EdgeId)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: EdgeId
c') ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, DGEdgeType)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
d ATermTable
att3 of
{ (att4 :: ATermTable
att4, d' :: DGEdgeType
d') ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, DGRule)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
e ATermTable
att4 of
{ (att5 :: ATermTable
att5, e' :: DGRule
e') ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, Conservativity)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
f ATermTable
att5 of
{ (att6 :: ATermTable
att6, f' :: Conservativity
f') ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, ProofBasis)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
g ATermTable
att6 of
{ (att7 :: ATermTable
att7, g' :: ProofBasis
g') ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
h ATermTable
att7 of
{ (att8 :: ATermTable
att8, h' :: String
h') ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, Maybe String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i ATermTable
att8 of
{ (att9 :: ATermTable
att9, i' :: Maybe String
i') ->
case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
j ATermTable
att9 of
{ (att10 :: ATermTable
att10, j' :: String
j') ->
(ATermTable
att10, String
-> String
-> EdgeId
-> DGEdgeType
-> DGRule
-> Conservativity
-> ProofBasis
-> String
-> Maybe String
-> String
-> XLink
XLink String
a' String
b' EdgeId
c' DGEdgeType
d' DGRule
e' Conservativity
f' ProofBasis
g' String
h' Maybe String
i' String
j') }}}}}}}}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, XLink)
forall a. String -> ShATerm -> a
fromShATermError "Static.XGraph.XLink" ShATerm
u