{-# OPTIONS -w -O0 #-}
{-# LANGUAGE CPP, StandaloneDeriving, DeriveDataTypeable, DeriveGeneric #-}
{- |
Module      :  ATC/DevGraph.der.hs
Description :  generated ShATermLG instances
Copyright   :  (c) DFKI GmbH 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable(derive Typeable instances)

Automatic derivation of instances via DrIFT-rule ShATermLG
  for the type(s):
'Static.DevGraph.NodeSig'
'Static.DevGraph.MaybeNode'
'Static.DevGraph.Renamed'
'Static.DevGraph.MaybeRestricted'
'Static.DevGraph.DGOrigin'
'Static.DevGraph.DGNodeInfo'
'Static.DevGraph.DGNodeLab'
'Static.DevGraph.Fitted'
'Static.DevGraph.DGLinkOrigin'
'Static.DevGraph.DGLinkType'
'Static.DevGraph.DGLinkLab'
'Static.DevGraph.GenSig'
'Static.DevGraph.ExtGenSig'
'Static.DevGraph.ExtViewSig'
'Static.DevGraph.UnitSig'
'Static.DevGraph.ImpUnitSigOrSig'
'Static.DevGraph.RefSig'
'Static.DevGraph.BranchSig'
'Static.DevGraph.GlobalEntry'
'Static.DevGraph.AlignSig'
'Static.DevGraph.DGChange'
'Static.DevGraph.HistElem'
'Static.DevGraph.RTNodeType'
'Static.DevGraph.RTNodeLab'
'Static.DevGraph.RTLinkType'
'Static.DevGraph.RTLinkLab'
'Static.DevGraph.DiagNodeLab'
'Static.DevGraph.DiagLinkLab'
'Static.DevGraph.Diag'
'Static.DevGraph.DGraph'
-}

{-
Generated by 'genRules' (automatic rule generation for DrIFT). Don't touch!!
  dependency files:
Static/DevGraph.hs
-}

module ATC.DevGraph () where

import ATC.AS_Library
import ATC.Grothendieck
import ATC.XGraph
import ATerm.Lib
import Common.AS_Annotation
import Common.Consistency
import Common.GlobalAnnotations
import Common.IRI
import Common.Id
import Common.LibName
import Common.Result
import Control.Concurrent.MVar
import Data.Graph.Inductive.Basic
import Data.Graph.Inductive.Graph as Graph
import Data.Graph.Inductive.Query.DFS
import Data.List
import Data.Maybe
import Data.Ord
import Data.Typeable
import Logic.Comorphism
import Logic.ExtSign
import Logic.Grothendieck
import Logic.Logic
import Logic.Prover
import Static.DevGraph
import Static.DgUtils
import Static.GTheory
import Syntax.AS_Library
import Syntax.AS_Structured
import qualified Common.Lib.Graph as Tree
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel
import qualified Common.Lib.SizedList as SizedList
import qualified Common.OrderedMap as OMap
import qualified Control.Monad.Fail as Fail
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Static.XGraph as XGraph

{-! for Static.DevGraph.NodeSig derive : ShATermLG !-}
{-! for Static.DevGraph.MaybeNode derive : ShATermLG !-}
{-! for Static.DevGraph.Renamed derive : ShATermLG !-}
{-! for Static.DevGraph.MaybeRestricted derive : ShATermLG !-}
{-! for Static.DevGraph.DGOrigin derive : ShATermLG !-}
{-! for Static.DevGraph.DGNodeInfo derive : ShATermLG !-}
{-! for Static.DevGraph.DGNodeLab derive : ShATermLG !-}
{-! for Static.DevGraph.Fitted derive : ShATermLG !-}
{-! for Static.DevGraph.DGLinkOrigin derive : ShATermLG !-}
{-! for Static.DevGraph.DGLinkType derive : ShATermLG !-}
{-! for Static.DevGraph.DGLinkLab derive : ShATermLG !-}
{-! for Static.DevGraph.GenSig derive : ShATermLG !-}
{-! for Static.DevGraph.ExtGenSig derive : ShATermLG !-}
{-! for Static.DevGraph.ExtViewSig derive : ShATermLG !-}
{-! for Static.DevGraph.UnitSig derive : ShATermLG !-}
{-! for Static.DevGraph.ImpUnitSigOrSig derive : ShATermLG !-}
{-! for Static.DevGraph.RefSig derive : ShATermLG !-}
{-! for Static.DevGraph.BranchSig derive : ShATermLG !-}
{-! for Static.DevGraph.GlobalEntry derive : ShATermLG !-}
{-! for Static.DevGraph.AlignSig derive : ShATermLG !-}
{-! for Static.DevGraph.DGChange derive : ShATermLG !-}
{-! for Static.DevGraph.HistElem derive : ShATermLG !-}
{-! for Static.DevGraph.RTNodeType derive : ShATermLG !-}
{-! for Static.DevGraph.RTNodeLab derive : ShATermLG !-}
{-! for Static.DevGraph.RTLinkType derive : ShATermLG !-}
{-! for Static.DevGraph.RTLinkLab derive : ShATermLG !-}
{-! for Static.DevGraph.DiagNodeLab derive : ShATermLG !-}
{-! for Static.DevGraph.DiagLinkLab derive : ShATermLG !-}
{-! for Static.DevGraph.Diag derive : ShATermLG !-}
{-! for Static.DevGraph.DGraph derive : ShATermLG !-}

-- Generated by DrIFT, look but don't touch!

instance ShATermLG Static.DevGraph.DGraph where
  toShATermLG :: ATermTable -> DGraph -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: DGraph
xv = case DGraph
xv of
    DGraph a :: GlobalAnnos
a b :: Maybe LIB_DEFN
b c :: GlobalEnv
c d :: Gr DGNodeLab DGLinkLab
d e :: Maybe NodeSig
e f :: Gr RTNodeLab RTLinkLab
f g :: Map String [Int]
g h :: MapSet String Int
h i :: Map String Diag
i j :: EdgeId
j k :: Map (LibName, Int) Int
k l :: Map SigId G_sign
l m :: Map ThId G_theory
m n :: Map MorId G_morphism
n o :: ProofHistory
o p :: ProofHistory
p -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> GlobalAnnos -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 GlobalAnnos
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Maybe LIB_DEFN -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 Maybe LIB_DEFN
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> GlobalEnv -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 GlobalEnv
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Gr DGNodeLab DGLinkLab -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att3 Gr DGNodeLab DGLinkLab
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> Maybe NodeSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att4 Maybe NodeSig
e
      (att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> Gr RTNodeLab RTLinkLab -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att5 Gr RTNodeLab RTLinkLab
f
      (att7 :: ATermTable
att7, g' :: Int
g') <- ATermTable -> Map String [Int] -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att6 Map String [Int]
g
      (att8 :: ATermTable
att8, h' :: Int
h') <- ATermTable -> MapSet String Int -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att7 MapSet String Int
h
      (att9 :: ATermTable
att9, i' :: Int
i') <- ATermTable -> Map String Diag -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att8 Map String Diag
i
      (att10 :: ATermTable
att10, j' :: Int
j') <- ATermTable -> EdgeId -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att9 EdgeId
j
      (att11 :: ATermTable
att11, k' :: Int
k') <- ATermTable -> Map (LibName, Int) Int -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att10 Map (LibName, Int) Int
k
      (att12 :: ATermTable
att12, l' :: Int
l') <- ATermTable -> Map SigId G_sign -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att11 Map SigId G_sign
l
      (att13 :: ATermTable
att13, m' :: Int
m') <- ATermTable -> Map ThId G_theory -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att12 Map ThId G_theory
m
      (att14 :: ATermTable
att14, n' :: Int
n') <- ATermTable -> Map MorId G_morphism -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att13 Map MorId G_morphism
n
      (att15 :: ATermTable
att15, o' :: Int
o') <- ATermTable -> ProofHistory -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att14 ProofHistory
o
      (att16 :: ATermTable
att16, p' :: Int
p') <- ATermTable -> ProofHistory -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att15 ProofHistory
p
      (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 "DGraph" [Int
a', Int
b', Int
c', Int
d', Int
e', Int
f', Int
g',
                                           Int
h', Int
i', Int
j', Int
k', Int
l', Int
m', Int
n', Int
o', Int
p'] []) ATermTable
att16
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DGraph)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "DGraph" [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, k :: Int
k, l :: Int
l, m :: Int
m, n :: Int
n, o :: Int
o,
                      p :: Int
p] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, GlobalAnnos)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: GlobalAnnos
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Maybe LIB_DEFN)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Maybe LIB_DEFN
b') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, GlobalEnv)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: GlobalEnv
c') ->
      case LogicGraph
-> Int -> ATermTable -> (ATermTable, Gr DGNodeLab DGLinkLab)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Gr DGNodeLab DGLinkLab
d') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Maybe NodeSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: Maybe NodeSig
e') ->
      case LogicGraph
-> Int -> ATermTable -> (ATermTable, Gr RTNodeLab RTLinkLab)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
f ATermTable
att5 of
      { (att6 :: ATermTable
att6, f' :: Gr RTNodeLab RTLinkLab
f') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Map String [Int])
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
g ATermTable
att6 of
      { (att7 :: ATermTable
att7, g' :: Map String [Int]
g') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, MapSet String Int)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
h ATermTable
att7 of
      { (att8 :: ATermTable
att8, h' :: MapSet String Int
h') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Map String Diag)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i ATermTable
att8 of
      { (att9 :: ATermTable
att9, i' :: Map String Diag
i') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, EdgeId)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
j ATermTable
att9 of
      { (att10 :: ATermTable
att10, j' :: EdgeId
j') ->
      case LogicGraph
-> Int -> ATermTable -> (ATermTable, Map (LibName, Int) Int)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
k ATermTable
att10 of
      { (att11 :: ATermTable
att11, k' :: Map (LibName, Int) Int
k') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Map SigId G_sign)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
l ATermTable
att11 of
      { (att12 :: ATermTable
att12, l' :: Map SigId G_sign
l') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Map ThId G_theory)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
m ATermTable
att12 of
      { (att13 :: ATermTable
att13, m' :: Map ThId G_theory
m') ->
      case LogicGraph
-> Int -> ATermTable -> (ATermTable, Map MorId G_morphism)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
n ATermTable
att13 of
      { (att14 :: ATermTable
att14, n' :: Map MorId G_morphism
n') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, ProofHistory)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
o ATermTable
att14 of
      { (att15 :: ATermTable
att15, o' :: ProofHistory
o') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, ProofHistory)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
p ATermTable
att15 of
      { (att16 :: ATermTable
att16, p' :: ProofHistory
p') ->
      (ATermTable
att16, GlobalAnnos
-> Maybe LIB_DEFN
-> GlobalEnv
-> Gr DGNodeLab DGLinkLab
-> Maybe NodeSig
-> Gr RTNodeLab RTLinkLab
-> Map String [Int]
-> MapSet String Int
-> Map String Diag
-> EdgeId
-> Map (LibName, Int) Int
-> Map SigId G_sign
-> Map ThId G_theory
-> Map MorId G_morphism
-> ProofHistory
-> ProofHistory
-> DGraph
DGraph GlobalAnnos
a' Maybe LIB_DEFN
b' GlobalEnv
c' Gr DGNodeLab DGLinkLab
d' Maybe NodeSig
e' Gr RTNodeLab RTLinkLab
f' Map String [Int]
g' MapSet String Int
h' Map String Diag
i' EdgeId
j' Map (LibName, Int) Int
k' Map SigId G_sign
l' Map ThId G_theory
m' Map MorId G_morphism
n' ProofHistory
o'
              ProofHistory
p') }}}}}}}}}}}}}}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, DGraph)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.DGraph" ShATerm
u

instance ShATermLG Static.DevGraph.Diag where
  toShATermLG :: ATermTable -> Diag -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: Diag
xv = case Diag
xv of
    Diagram a :: Gr DiagNodeLab DiagLinkLab
a b :: Int
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Gr DiagNodeLab DiagLinkLab -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 Gr DiagNodeLab DiagLinkLab
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Int -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 Int
b
      (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 "Diagram" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, Diag)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Diagram" [a :: Int
a, b :: Int
b] _ ->
      case LogicGraph
-> Int -> ATermTable -> (ATermTable, Gr DiagNodeLab DiagLinkLab)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Gr DiagNodeLab DiagLinkLab
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Int)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Int
b') ->
      (ATermTable
att2, Gr DiagNodeLab DiagLinkLab -> Int -> Diag
Diagram Gr DiagNodeLab DiagLinkLab
a' Int
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Diag)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.Diag" ShATerm
u

instance ShATermLG Static.DevGraph.DiagLinkLab where
  toShATermLG :: ATermTable -> DiagLinkLab -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: DiagLinkLab
xv = case DiagLinkLab
xv of
    DiagLink a :: GMorphism
a b :: Int
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> GMorphism -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 GMorphism
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Int -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 Int
b
      (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 "DiagLink" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DiagLinkLab)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "DiagLink" [a :: Int
a, b :: Int
b] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, GMorphism)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: GMorphism
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Int)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Int
b') ->
      (ATermTable
att2, GMorphism -> Int -> DiagLinkLab
DiagLink GMorphism
a' Int
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, DiagLinkLab)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.DiagLinkLab" ShATerm
u

instance ShATermLG Static.DevGraph.DiagNodeLab where
  toShATermLG :: ATermTable -> DiagNodeLab -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: DiagNodeLab
xv = case DiagNodeLab
xv of
    DiagNode a :: NodeSig
a b :: String
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NodeSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 NodeSig
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
      (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 "DiagNode" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DiagNodeLab)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "DiagNode" [a :: Int
a, b :: Int
b] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, NodeSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: NodeSig
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') ->
      (ATermTable
att2, NodeSig -> String -> DiagNodeLab
DiagNode NodeSig
a' String
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, DiagNodeLab)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.DiagNodeLab" ShATerm
u

instance ShATermLG Static.DevGraph.RTLinkLab where
  toShATermLG :: ATermTable -> RTLinkLab -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: RTLinkLab
xv = case RTLinkLab
xv of
    RTLink a :: RTLinkType
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> RTLinkType -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 RTLinkType
a
      (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 "RTLink" [Int
a'] []) ATermTable
att1
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, RTLinkLab)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "RTLink" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, RTLinkType)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: RTLinkType
a') ->
      (ATermTable
att1, RTLinkType -> RTLinkLab
RTLink RTLinkType
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, RTLinkLab)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.RTLinkLab" ShATerm
u

instance ShATermLG Static.DevGraph.RTLinkType where
  toShATermLG :: ATermTable -> RTLinkType -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: RTLinkType
xv = case RTLinkType
xv of
    RTRefine -> (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 "RTRefine" [] []) ATermTable
att0
    RTComp -> (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 "RTComp" [] []) ATermTable
att0
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, RTLinkType)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "RTRefine" [] _ -> (ATermTable
att0, RTLinkType
RTRefine)
    ShAAppl "RTComp" [] _ -> (ATermTable
att0, RTLinkType
RTComp)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, RTLinkType)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.RTLinkType" ShATerm
u

instance ShATermLG Static.DevGraph.RTNodeLab where
  toShATermLG :: ATermTable -> RTNodeLab -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: RTNodeLab
xv = case RTNodeLab
xv of
    RTNodeLab a :: RTNodeType
a b :: String
b c :: String
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> RTNodeType -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 RTNodeType
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
      (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 "RTNodeLab" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, RTNodeLab)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "RTNodeLab" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, RTNodeType)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: RTNodeType
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') ->
      (ATermTable
att3, RTNodeType -> String -> String -> RTNodeLab
RTNodeLab RTNodeType
a' String
b' String
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, RTNodeLab)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.RTNodeLab" ShATerm
u

instance ShATermLG Static.DevGraph.RTNodeType where
  toShATermLG :: ATermTable -> RTNodeType -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: RTNodeType
xv = case RTNodeType
xv of
    RTPlain a :: UnitSig
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> UnitSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 UnitSig
a
      (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 "RTPlain" [Int
a'] []) ATermTable
att1
    RTRef a :: Int
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Int -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 Int
a
      (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 "RTRef" [Int
a'] []) ATermTable
att1
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, RTNodeType)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "RTPlain" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, UnitSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: UnitSig
a') ->
      (ATermTable
att1, UnitSig -> RTNodeType
RTPlain UnitSig
a') }
    ShAAppl "RTRef" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Int)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Int
a') ->
      (ATermTable
att1, Int -> RTNodeType
RTRef Int
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, RTNodeType)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.RTNodeType" ShATerm
u

instance ShATermLG Static.DevGraph.HistElem where
  toShATermLG :: ATermTable -> HistElem -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: HistElem
xv = case HistElem
xv of
    HistElem a :: DGChange
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> DGChange -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 DGChange
a
      (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 "HistElem" [Int
a'] []) ATermTable
att1
    HistGroup a :: DGRule
a b :: ProofHistory
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> DGRule -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 DGRule
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> ProofHistory -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 ProofHistory
b
      (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 "HistGroup" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, HistElem)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "HistElem" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, DGChange)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: DGChange
a') ->
      (ATermTable
att1, DGChange -> HistElem
HistElem DGChange
a') }
    ShAAppl "HistGroup" [a :: Int
a, b :: Int
b] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, DGRule)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: DGRule
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, ProofHistory)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: ProofHistory
b') ->
      (ATermTable
att2, DGRule -> ProofHistory -> HistElem
HistGroup DGRule
a' ProofHistory
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, HistElem)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.HistElem" ShATerm
u

instance ShATermLG Static.DevGraph.DGChange where
  toShATermLG :: ATermTable -> DGChange -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: DGChange
xv = case DGChange
xv of
    InsertNode a :: LNode DGNodeLab
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> LNode DGNodeLab -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 LNode DGNodeLab
a
      (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 "InsertNode" [Int
a'] []) ATermTable
att1
    DeleteNode a :: LNode DGNodeLab
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> LNode DGNodeLab -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 LNode DGNodeLab
a
      (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 "DeleteNode" [Int
a'] []) ATermTable
att1
    InsertEdge a :: LEdge DGLinkLab
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> LEdge DGLinkLab -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 LEdge DGLinkLab
a
      (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 "InsertEdge" [Int
a'] []) ATermTable
att1
    DeleteEdge a :: LEdge DGLinkLab
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> LEdge DGLinkLab -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 LEdge DGLinkLab
a
      (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 "DeleteEdge" [Int
a'] []) ATermTable
att1
    SetNodeLab a :: DGNodeLab
a b :: LNode DGNodeLab
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> DGNodeLab -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 DGNodeLab
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> LNode DGNodeLab -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 LNode DGNodeLab
b
      (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 "SetNodeLab" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DGChange)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "InsertNode" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, LNode DGNodeLab)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: LNode DGNodeLab
a') ->
      (ATermTable
att1, LNode DGNodeLab -> DGChange
InsertNode LNode DGNodeLab
a') }
    ShAAppl "DeleteNode" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, LNode DGNodeLab)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: LNode DGNodeLab
a') ->
      (ATermTable
att1, LNode DGNodeLab -> DGChange
DeleteNode LNode DGNodeLab
a') }
    ShAAppl "InsertEdge" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, LEdge DGLinkLab)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: LEdge DGLinkLab
a') ->
      (ATermTable
att1, LEdge DGLinkLab -> DGChange
InsertEdge LEdge DGLinkLab
a') }
    ShAAppl "DeleteEdge" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, LEdge DGLinkLab)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: LEdge DGLinkLab
a') ->
      (ATermTable
att1, LEdge DGLinkLab -> DGChange
DeleteEdge LEdge DGLinkLab
a') }
    ShAAppl "SetNodeLab" [a :: Int
a, b :: Int
b] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, DGNodeLab)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: DGNodeLab
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, LNode DGNodeLab)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: LNode DGNodeLab
b') ->
      (ATermTable
att2, DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
a' LNode DGNodeLab
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, DGChange)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.DGChange" ShATerm
u

instance ShATermLG Static.DevGraph.AlignSig where
  toShATermLG :: ATermTable -> AlignSig -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: AlignSig
xv = case AlignSig
xv of
    AlignMor a :: NodeSig
a b :: GMorphism
b c :: NodeSig
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NodeSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 NodeSig
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> GMorphism -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 GMorphism
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> NodeSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 NodeSig
c
      (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 "AlignMor" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    AlignSpan a :: NodeSig
a b :: GMorphism
b c :: NodeSig
c d :: GMorphism
d e :: NodeSig
e -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NodeSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 NodeSig
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> GMorphism -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 GMorphism
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> NodeSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 NodeSig
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> GMorphism -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att3 GMorphism
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> NodeSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att4 NodeSig
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 "AlignSpan" [Int
a', Int
b', Int
c', Int
d',
                                              Int
e'] []) ATermTable
att5
    WAlign a :: NodeSig
a b :: GMorphism
b c :: GMorphism
c d :: NodeSig
d e :: GMorphism
e f :: GMorphism
f g :: NodeSig
g h :: NodeSig
h i :: NodeSig
i -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NodeSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 NodeSig
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> GMorphism -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 GMorphism
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> GMorphism -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 GMorphism
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> NodeSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att3 NodeSig
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> GMorphism -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att4 GMorphism
e
      (att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> GMorphism -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att5 GMorphism
f
      (att7 :: ATermTable
att7, g' :: Int
g') <- ATermTable -> NodeSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att6 NodeSig
g
      (att8 :: ATermTable
att8, h' :: Int
h') <- ATermTable -> NodeSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att7 NodeSig
h
      (att9 :: ATermTable
att9, i' :: Int
i') <- ATermTable -> NodeSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att8 NodeSig
i
      (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 "WAlign" [Int
a', Int
b', Int
c', Int
d', Int
e', Int
f', Int
g',
                                           Int
h', Int
i'] []) ATermTable
att9
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, AlignSig)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "AlignMor" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, NodeSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: NodeSig
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, GMorphism)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: GMorphism
b') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, NodeSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: NodeSig
c') ->
      (ATermTable
att3, NodeSig -> GMorphism -> NodeSig -> AlignSig
AlignMor NodeSig
a' GMorphism
b' NodeSig
c') }}}
    ShAAppl "AlignSpan" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, NodeSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: NodeSig
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, GMorphism)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: GMorphism
b') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, NodeSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: NodeSig
c') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, GMorphism)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: GMorphism
d') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, NodeSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: NodeSig
e') ->
      (ATermTable
att5, NodeSig -> GMorphism -> NodeSig -> GMorphism -> NodeSig -> AlignSig
AlignSpan NodeSig
a' GMorphism
b' NodeSig
c' GMorphism
d' NodeSig
e') }}}}}
    ShAAppl "WAlign" [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] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, NodeSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: NodeSig
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, GMorphism)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: GMorphism
b') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, GMorphism)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: GMorphism
c') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, NodeSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: NodeSig
d') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, GMorphism)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: GMorphism
e') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, GMorphism)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
f ATermTable
att5 of
      { (att6 :: ATermTable
att6, f' :: GMorphism
f') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, NodeSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
g ATermTable
att6 of
      { (att7 :: ATermTable
att7, g' :: NodeSig
g') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, NodeSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
h ATermTable
att7 of
      { (att8 :: ATermTable
att8, h' :: NodeSig
h') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, NodeSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i ATermTable
att8 of
      { (att9 :: ATermTable
att9, i' :: NodeSig
i') ->
      (ATermTable
att9, NodeSig
-> GMorphism
-> GMorphism
-> NodeSig
-> GMorphism
-> GMorphism
-> NodeSig
-> NodeSig
-> NodeSig
-> AlignSig
WAlign NodeSig
a' GMorphism
b' GMorphism
c' NodeSig
d' GMorphism
e' GMorphism
f' NodeSig
g' NodeSig
h' NodeSig
i') }}}}}}}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, AlignSig)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.AlignSig" ShATerm
u

instance ShATermLG Static.DevGraph.GlobalEntry where
  toShATermLG :: ATermTable -> GlobalEntry -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: GlobalEntry
xv = case GlobalEntry
xv of
    SpecEntry a :: ExtGenSig
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> ExtGenSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 ExtGenSig
a
      (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 "SpecEntry" [Int
a'] []) ATermTable
att1
    ViewOrStructEntry a :: Bool
a b :: ExtViewSig
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 Bool
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> ExtViewSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 ExtViewSig
b
      (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 "ViewOrStructEntry" [Int
a', Int
b'] []) ATermTable
att2
    ArchOrRefEntry a :: Bool
a b :: RefSig
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 Bool
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> RefSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 RefSig
b
      (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 "ArchOrRefEntry" [Int
a', Int
b'] []) ATermTable
att2
    AlignEntry a :: AlignSig
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> AlignSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 AlignSig
a
      (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 "AlignEntry" [Int
a'] []) ATermTable
att1
    UnitEntry a :: UnitSig
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> UnitSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 UnitSig
a
      (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 "UnitEntry" [Int
a'] []) ATermTable
att1
    NetworkEntry a :: GDiagram
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> GDiagram -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 GDiagram
a
      (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 "NetworkEntry" [Int
a'] []) ATermTable
att1
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, GlobalEntry)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SpecEntry" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, ExtGenSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: ExtGenSig
a') ->
      (ATermTable
att1, ExtGenSig -> GlobalEntry
SpecEntry ExtGenSig
a') }
    ShAAppl "ViewOrStructEntry" [a :: Int
a, b :: Int
b] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Bool
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, ExtViewSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: ExtViewSig
b') ->
      (ATermTable
att2, Bool -> ExtViewSig -> GlobalEntry
ViewOrStructEntry Bool
a' ExtViewSig
b') }}
    ShAAppl "ArchOrRefEntry" [a :: Int
a, b :: Int
b] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Bool
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, RefSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: RefSig
b') ->
      (ATermTable
att2, Bool -> RefSig -> GlobalEntry
ArchOrRefEntry Bool
a' RefSig
b') }}
    ShAAppl "AlignEntry" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, AlignSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: AlignSig
a') ->
      (ATermTable
att1, AlignSig -> GlobalEntry
AlignEntry AlignSig
a') }
    ShAAppl "UnitEntry" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, UnitSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: UnitSig
a') ->
      (ATermTable
att1, UnitSig -> GlobalEntry
UnitEntry UnitSig
a') }
    ShAAppl "NetworkEntry" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, GDiagram)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: GDiagram
a') ->
      (ATermTable
att1, GDiagram -> GlobalEntry
NetworkEntry GDiagram
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, GlobalEntry)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.GlobalEntry" ShATerm
u

instance ShATermLG Static.DevGraph.BranchSig where
  toShATermLG :: ATermTable -> BranchSig -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: BranchSig
xv = case BranchSig
xv of
    UnitSigAsBranchSig a :: UnitSig
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> UnitSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 UnitSig
a
      (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 "UnitSigAsBranchSig" [Int
a'] []) ATermTable
att1
    BranchStaticContext a :: BStContext
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> BStContext -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 BStContext
a
      (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 "BranchStaticContext" [Int
a'] []) ATermTable
att1
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, BranchSig)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "UnitSigAsBranchSig" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, UnitSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: UnitSig
a') ->
      (ATermTable
att1, UnitSig -> BranchSig
UnitSigAsBranchSig UnitSig
a') }
    ShAAppl "BranchStaticContext" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, BStContext)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: BStContext
a') ->
      (ATermTable
att1, BStContext -> BranchSig
BranchStaticContext BStContext
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, BranchSig)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.BranchSig" ShATerm
u

instance ShATermLG Static.DevGraph.RefSig where
  toShATermLG :: ATermTable -> RefSig -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: RefSig
xv = case RefSig
xv of
    BranchRefSig a :: RTPointer
a b :: (UnitSig, Maybe BranchSig)
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> RTPointer -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 RTPointer
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> (UnitSig, Maybe BranchSig) -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 (UnitSig, Maybe BranchSig)
b
      (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 "BranchRefSig" [Int
a', Int
b'] []) ATermTable
att2
    ComponentRefSig a :: RTPointer
a b :: BStContext
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> RTPointer -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 RTPointer
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> BStContext -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 BStContext
b
      (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 "ComponentRefSig" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, RefSig)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "BranchRefSig" [a :: Int
a, b :: Int
b] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, RTPointer)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: RTPointer
a') ->
      case LogicGraph
-> Int -> ATermTable -> (ATermTable, (UnitSig, Maybe BranchSig))
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: (UnitSig, Maybe BranchSig)
b') ->
      (ATermTable
att2, RTPointer -> (UnitSig, Maybe BranchSig) -> RefSig
BranchRefSig RTPointer
a' (UnitSig, Maybe BranchSig)
b') }}
    ShAAppl "ComponentRefSig" [a :: Int
a, b :: Int
b] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, RTPointer)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: RTPointer
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, BStContext)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: BStContext
b') ->
      (ATermTable
att2, RTPointer -> BStContext -> RefSig
ComponentRefSig RTPointer
a' BStContext
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, RefSig)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.RefSig" ShATerm
u

instance ShATermLG Static.DevGraph.ImpUnitSigOrSig where
  toShATermLG :: ATermTable -> ImpUnitSigOrSig -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: ImpUnitSigOrSig
xv = case ImpUnitSigOrSig
xv of
    ImpUnitSig a :: MaybeNode
a b :: UnitSig
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> MaybeNode -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 MaybeNode
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> UnitSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 UnitSig
b
      (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 "ImpUnitSig" [Int
a', Int
b'] []) ATermTable
att2
    Sig a :: NodeSig
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NodeSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 NodeSig
a
      (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 "Sig" [Int
a'] []) ATermTable
att1
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, ImpUnitSigOrSig)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "ImpUnitSig" [a :: Int
a, b :: Int
b] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, MaybeNode)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: MaybeNode
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, UnitSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: UnitSig
b') ->
      (ATermTable
att2, MaybeNode -> UnitSig -> ImpUnitSigOrSig
ImpUnitSig MaybeNode
a' UnitSig
b') }}
    ShAAppl "Sig" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, NodeSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: NodeSig
a') ->
      (ATermTable
att1, NodeSig -> ImpUnitSigOrSig
Sig NodeSig
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, ImpUnitSigOrSig)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.ImpUnitSigOrSig" ShATerm
u

instance ShATermLG Static.DevGraph.UnitSig where
  toShATermLG :: ATermTable -> UnitSig -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: UnitSig
xv = case UnitSig
xv of
    UnitSig a :: [NodeSig]
a b :: NodeSig
b c :: Maybe NodeSig
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [NodeSig] -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 [NodeSig]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> NodeSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 NodeSig
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Maybe NodeSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 Maybe NodeSig
c
      (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 "UnitSig" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, UnitSig)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "UnitSig" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, [NodeSig])
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [NodeSig]
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, NodeSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: NodeSig
b') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Maybe NodeSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Maybe NodeSig
c') ->
      (ATermTable
att3, [NodeSig] -> NodeSig -> Maybe NodeSig -> UnitSig
UnitSig [NodeSig]
a' NodeSig
b' Maybe NodeSig
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, UnitSig)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.UnitSig" ShATerm
u

instance ShATermLG Static.DevGraph.ExtViewSig where
  toShATermLG :: ATermTable -> ExtViewSig -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: ExtViewSig
xv = case ExtViewSig
xv of
    ExtViewSig a :: NodeSig
a b :: GMorphism
b c :: ExtGenSig
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NodeSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 NodeSig
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> GMorphism -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 GMorphism
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> ExtGenSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 ExtGenSig
c
      (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 "ExtViewSig" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, ExtViewSig)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "ExtViewSig" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, NodeSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: NodeSig
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, GMorphism)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: GMorphism
b') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, ExtGenSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: ExtGenSig
c') ->
      (ATermTable
att3, NodeSig -> GMorphism -> ExtGenSig -> ExtViewSig
ExtViewSig NodeSig
a' GMorphism
b' ExtGenSig
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, ExtViewSig)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.ExtViewSig" ShATerm
u

instance ShATermLG Static.DevGraph.ExtGenSig where
  toShATermLG :: ATermTable -> ExtGenSig -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: ExtGenSig
xv = case ExtGenSig
xv of
    ExtGenSig a :: GenSig
a b :: NodeSig
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> GenSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 GenSig
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> NodeSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 NodeSig
b
      (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 "ExtGenSig" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, ExtGenSig)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "ExtGenSig" [a :: Int
a, b :: Int
b] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, GenSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: GenSig
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, NodeSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: NodeSig
b') ->
      (ATermTable
att2, GenSig -> NodeSig -> ExtGenSig
ExtGenSig GenSig
a' NodeSig
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, ExtGenSig)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.ExtGenSig" ShATerm
u

instance ShATermLG Static.DevGraph.GenSig where
  toShATermLG :: ATermTable -> GenSig -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: GenSig
xv = case GenSig
xv of
    GenSig a :: MaybeNode
a b :: [NodeSig]
b c :: MaybeNode
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> MaybeNode -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 MaybeNode
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [NodeSig] -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 [NodeSig]
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> MaybeNode -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 MaybeNode
c
      (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 "GenSig" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, GenSig)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "GenSig" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, MaybeNode)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: MaybeNode
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, [NodeSig])
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [NodeSig]
b') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, MaybeNode)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: MaybeNode
c') ->
      (ATermTable
att3, MaybeNode -> [NodeSig] -> MaybeNode -> GenSig
GenSig MaybeNode
a' [NodeSig]
b' MaybeNode
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, GenSig)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.GenSig" ShATerm
u

instance ShATermLG Static.DevGraph.DGLinkLab where
  toShATermLG :: ATermTable -> DGLinkLab -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: DGLinkLab
xv = case DGLinkLab
xv of
    DGLink a :: GMorphism
a b :: DGLinkType
b c :: DGLinkOrigin
c d :: Bool
d e :: EdgeId
e f :: String
f -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> GMorphism -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 GMorphism
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> DGLinkType -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 DGLinkType
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> DGLinkOrigin -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 DGLinkOrigin
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att3 Bool
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> EdgeId -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att4 EdgeId
e
      (att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> String -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att5 String
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 "DGLink" [Int
a', Int
b', Int
c', Int
d', Int
e',
                                           Int
f'] []) ATermTable
att6
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DGLinkLab)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "DGLink" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e, f :: Int
f] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, GMorphism)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: GMorphism
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, DGLinkType)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: DGLinkType
b') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, DGLinkOrigin)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: DGLinkOrigin
c') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Bool
d') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, EdgeId)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: EdgeId
e') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
f ATermTable
att5 of
      { (att6 :: ATermTable
att6, f' :: String
f') ->
      (ATermTable
att6, GMorphism
-> DGLinkType
-> DGLinkOrigin
-> Bool
-> EdgeId
-> String
-> DGLinkLab
DGLink GMorphism
a' DGLinkType
b' DGLinkOrigin
c' Bool
d' EdgeId
e' String
f') }}}}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, DGLinkLab)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.DGLinkLab" ShATerm
u

instance ShATermLG Static.DevGraph.DGLinkType where
  toShATermLG :: ATermTable -> DGLinkType -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: DGLinkType
xv = case DGLinkType
xv of
    ScopedLink a :: Scope
a b :: LinkKind
b c :: ConsStatus
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Scope -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 Scope
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> LinkKind -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 LinkKind
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> ConsStatus -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 ConsStatus
c
      (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 "ScopedLink" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    HidingDefLink -> (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 "HidingDefLink" [] []) ATermTable
att0
    FreeOrCofreeDefLink a :: FreeOrCofree
a b :: MaybeNode
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> FreeOrCofree -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 FreeOrCofree
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> MaybeNode -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 MaybeNode
b
      (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 "FreeOrCofreeDefLink" [Int
a', Int
b'] []) ATermTable
att2
    HidingFreeOrCofreeThm a :: Maybe FreeOrCofree
a b :: Int
b c :: GMorphism
c d :: ThmLinkStatus
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Maybe FreeOrCofree -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 Maybe FreeOrCofree
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Int -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 Int
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> GMorphism -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 GMorphism
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> ThmLinkStatus -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att3 ThmLinkStatus
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 "HidingFreeOrCofreeThm" [Int
a', Int
b', Int
c',
                                                          Int
d'] []) ATermTable
att4
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DGLinkType)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "ScopedLink" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Scope)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Scope
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, LinkKind)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: LinkKind
b') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, ConsStatus)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: ConsStatus
c') ->
      (ATermTable
att3, Scope -> LinkKind -> ConsStatus -> DGLinkType
ScopedLink Scope
a' LinkKind
b' ConsStatus
c') }}}
    ShAAppl "HidingDefLink" [] _ -> (ATermTable
att0, DGLinkType
HidingDefLink)
    ShAAppl "FreeOrCofreeDefLink" [a :: Int
a, b :: Int
b] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, FreeOrCofree)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: FreeOrCofree
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, MaybeNode)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: MaybeNode
b') ->
      (ATermTable
att2, FreeOrCofree -> MaybeNode -> DGLinkType
FreeOrCofreeDefLink FreeOrCofree
a' MaybeNode
b') }}
    ShAAppl "HidingFreeOrCofreeThm" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Maybe FreeOrCofree)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Maybe FreeOrCofree
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Int)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Int
b') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, GMorphism)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: GMorphism
c') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, ThmLinkStatus)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: ThmLinkStatus
d') ->
      (ATermTable
att4, Maybe FreeOrCofree
-> Int -> GMorphism -> ThmLinkStatus -> DGLinkType
HidingFreeOrCofreeThm Maybe FreeOrCofree
a' Int
b' GMorphism
c' ThmLinkStatus
d') }}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, DGLinkType)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.DGLinkType" ShATerm
u

instance ShATermLG Static.DevGraph.DGLinkOrigin where
  toShATermLG :: ATermTable -> DGLinkOrigin -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: DGLinkOrigin
xv = case DGLinkOrigin
xv of
    SeeTarget -> (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 "SeeTarget" [] []) ATermTable
att0
    SeeSource -> (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 "SeeSource" [] []) ATermTable
att0
    TEST -> (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 "TEST" [] []) ATermTable
att0
    DGLinkVerif -> (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 "DGLinkVerif" [] []) ATermTable
att0
    DGImpliesLink -> (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 "DGImpliesLink" [] []) ATermTable
att0
    DGLinkExtension -> (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 "DGLinkExtension" [] []) ATermTable
att0
    DGLinkTranslation ->
      (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 "DGLinkTranslation" [] []) ATermTable
att0
    DGLinkClosedLenv ->
      (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 "DGLinkClosedLenv" [] []) ATermTable
att0
    DGLinkImports -> (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 "DGLinkImports" [] []) ATermTable
att0
    DGLinkIntersect -> (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 "DGLinkIntersect" [] []) ATermTable
att0
    DGLinkMorph a :: IRI
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> IRI -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 IRI
a
      (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 "DGLinkMorph" [Int
a'] []) ATermTable
att1
    DGLinkInst a :: IRI
a b :: Fitted
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> IRI -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 IRI
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Fitted -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 Fitted
b
      (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 "DGLinkInst" [Int
a', Int
b'] []) ATermTable
att2
    DGLinkInstArg a :: IRI
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> IRI -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 IRI
a
      (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 "DGLinkInstArg" [Int
a'] []) ATermTable
att1
    DGLinkView a :: IRI
a b :: Fitted
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> IRI -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 IRI
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Fitted -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 Fitted
b
      (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 "DGLinkView" [Int
a', Int
b'] []) ATermTable
att2
    DGLinkAlign a :: IRI
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> IRI -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 IRI
a
      (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 "DGLinkAlign" [Int
a'] []) ATermTable
att1
    DGLinkFitView a :: IRI
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> IRI -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 IRI
a
      (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 "DGLinkFitView" [Int
a'] []) ATermTable
att1
    DGLinkFitViewImp a :: IRI
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> IRI -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 IRI
a
      (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 "DGLinkFitViewImp" [Int
a'] []) ATermTable
att1
    DGLinkProof -> (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 "DGLinkProof" [] []) ATermTable
att0
    DGLinkFlatteningUnion ->
      (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 "DGLinkFlatteningUnion" [] []) ATermTable
att0
    DGLinkFlatteningRename ->
      (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 "DGLinkFlatteningRename" [] []) ATermTable
att0
    DGLinkRefinement a :: IRI
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> IRI -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 IRI
a
      (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 "DGLinkRefinement" [Int
a'] []) ATermTable
att1
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DGLinkOrigin)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SeeTarget" [] _ -> (ATermTable
att0, DGLinkOrigin
SeeTarget)
    ShAAppl "SeeSource" [] _ -> (ATermTable
att0, DGLinkOrigin
SeeSource)
    ShAAppl "TEST" [] _ -> (ATermTable
att0, DGLinkOrigin
TEST)
    ShAAppl "DGLinkVerif" [] _ -> (ATermTable
att0, DGLinkOrigin
DGLinkVerif)
    ShAAppl "DGImpliesLink" [] _ -> (ATermTable
att0, DGLinkOrigin
DGImpliesLink)
    ShAAppl "DGLinkExtension" [] _ -> (ATermTable
att0, DGLinkOrigin
DGLinkExtension)
    ShAAppl "DGLinkTranslation" [] _ -> (ATermTable
att0, DGLinkOrigin
DGLinkTranslation)
    ShAAppl "DGLinkClosedLenv" [] _ -> (ATermTable
att0, DGLinkOrigin
DGLinkClosedLenv)
    ShAAppl "DGLinkImports" [] _ -> (ATermTable
att0, DGLinkOrigin
DGLinkImports)
    ShAAppl "DGLinkIntersect" [] _ -> (ATermTable
att0, DGLinkOrigin
DGLinkIntersect)
    ShAAppl "DGLinkMorph" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, IRI)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: IRI
a') ->
      (ATermTable
att1, IRI -> DGLinkOrigin
DGLinkMorph IRI
a') }
    ShAAppl "DGLinkInst" [a :: Int
a, b :: Int
b] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, IRI)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: IRI
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Fitted)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Fitted
b') ->
      (ATermTable
att2, IRI -> Fitted -> DGLinkOrigin
DGLinkInst IRI
a' Fitted
b') }}
    ShAAppl "DGLinkInstArg" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, IRI)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: IRI
a') ->
      (ATermTable
att1, IRI -> DGLinkOrigin
DGLinkInstArg IRI
a') }
    ShAAppl "DGLinkView" [a :: Int
a, b :: Int
b] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, IRI)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: IRI
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Fitted)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Fitted
b') ->
      (ATermTable
att2, IRI -> Fitted -> DGLinkOrigin
DGLinkView IRI
a' Fitted
b') }}
    ShAAppl "DGLinkAlign" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, IRI)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: IRI
a') ->
      (ATermTable
att1, IRI -> DGLinkOrigin
DGLinkAlign IRI
a') }
    ShAAppl "DGLinkFitView" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, IRI)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: IRI
a') ->
      (ATermTable
att1, IRI -> DGLinkOrigin
DGLinkFitView IRI
a') }
    ShAAppl "DGLinkFitViewImp" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, IRI)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: IRI
a') ->
      (ATermTable
att1, IRI -> DGLinkOrigin
DGLinkFitViewImp IRI
a') }
    ShAAppl "DGLinkProof" [] _ -> (ATermTable
att0, DGLinkOrigin
DGLinkProof)
    ShAAppl "DGLinkFlatteningUnion" [] _ -> (ATermTable
att0, DGLinkOrigin
DGLinkFlatteningUnion)
    ShAAppl "DGLinkFlatteningRename" [] _ -> (ATermTable
att0, DGLinkOrigin
DGLinkFlatteningRename)
    ShAAppl "DGLinkRefinement" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, IRI)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: IRI
a') ->
      (ATermTable
att1, IRI -> DGLinkOrigin
DGLinkRefinement IRI
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, DGLinkOrigin)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.DGLinkOrigin" ShATerm
u

instance ShATermLG Static.DevGraph.Fitted where
  toShATermLG :: ATermTable -> Fitted -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: Fitted
xv = case Fitted
xv of
    Fitted a :: [G_mapping]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [G_mapping] -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 [G_mapping]
a
      (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 "Fitted" [Int
a'] []) ATermTable
att1
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, Fitted)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Fitted" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, [G_mapping])
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [G_mapping]
a') ->
      (ATermTable
att1, [G_mapping] -> Fitted
Fitted [G_mapping]
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Fitted)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.Fitted" ShATerm
u

instance ShATermLG Static.DevGraph.DGNodeLab where
  toShATermLG :: ATermTable -> DGNodeLab -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: DGNodeLab
xv = case DGNodeLab
xv of
    DGNodeLab a :: NodeName
a b :: G_theory
b c :: Maybe G_theory
c d :: Bool
d e :: Bool
e f :: Maybe Int
f g :: Maybe GMorphism
g h :: Maybe Int
h i :: Maybe GMorphism
i j :: DGNodeInfo
j k :: NodeMod
k l :: Maybe XNode
l m :: Maybe (MVar ())
m -> 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 -> G_theory -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 G_theory
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Maybe G_theory -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 Maybe G_theory
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att3 Bool
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att4 Bool
e
      (att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> Maybe Int -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att5 Maybe Int
f
      (att7 :: ATermTable
att7, g' :: Int
g') <- ATermTable -> Maybe GMorphism -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att6 Maybe GMorphism
g
      (att8 :: ATermTable
att8, h' :: Int
h') <- ATermTable -> Maybe Int -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att7 Maybe Int
h
      (att9 :: ATermTable
att9, i' :: Int
i') <- ATermTable -> Maybe GMorphism -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att8 Maybe GMorphism
i
      (att10 :: ATermTable
att10, j' :: Int
j') <- ATermTable -> DGNodeInfo -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att9 DGNodeInfo
j
      (att11 :: ATermTable
att11, k' :: Int
k') <- ATermTable -> NodeMod -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att10 NodeMod
k
      (att12 :: ATermTable
att12, l' :: Int
l') <- ATermTable -> Maybe XNode -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att11 Maybe XNode
l
      (att13 :: ATermTable
att13, m' :: Int
m') <- ATermTable -> Maybe (MVar ()) -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att12 Maybe (MVar ())
m
      (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 "DGNodeLab" [Int
a', Int
b', Int
c', Int
d', Int
e', Int
f', Int
g',
                                              Int
h', Int
i', Int
j', Int
k', Int
l', Int
m'] []) ATermTable
att13
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DGNodeLab)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "DGNodeLab" [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, k :: Int
k, l :: Int
l, m :: Int
m] _ ->
      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, G_theory)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: G_theory
b') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Maybe G_theory)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Maybe G_theory
c') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Bool
d') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: Bool
e') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Maybe Int)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
f ATermTable
att5 of
      { (att6 :: ATermTable
att6, f' :: Maybe Int
f') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Maybe GMorphism)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
g ATermTable
att6 of
      { (att7 :: ATermTable
att7, g' :: Maybe GMorphism
g') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Maybe Int)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
h ATermTable
att7 of
      { (att8 :: ATermTable
att8, h' :: Maybe Int
h') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Maybe GMorphism)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
i ATermTable
att8 of
      { (att9 :: ATermTable
att9, i' :: Maybe GMorphism
i') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, DGNodeInfo)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
j ATermTable
att9 of
      { (att10 :: ATermTable
att10, j' :: DGNodeInfo
j') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, NodeMod)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
k ATermTable
att10 of
      { (att11 :: ATermTable
att11, k' :: NodeMod
k') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Maybe XNode)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
l ATermTable
att11 of
      { (att12 :: ATermTable
att12, l' :: Maybe XNode
l') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Maybe (MVar ()))
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
m ATermTable
att12 of
      { (att13 :: ATermTable
att13, m' :: Maybe (MVar ())
m') ->
      (ATermTable
att13, NodeName
-> G_theory
-> Maybe G_theory
-> Bool
-> Bool
-> Maybe Int
-> Maybe GMorphism
-> Maybe Int
-> Maybe GMorphism
-> DGNodeInfo
-> NodeMod
-> Maybe XNode
-> Maybe (MVar ())
-> DGNodeLab
DGNodeLab NodeName
a' G_theory
b' Maybe G_theory
c' Bool
d' Bool
e' Maybe Int
f' Maybe GMorphism
g' Maybe Int
h' Maybe GMorphism
i' DGNodeInfo
j' NodeMod
k' Maybe XNode
l'
              Maybe (MVar ())
m') }}}}}}}}}}}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, DGNodeLab)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.DGNodeLab" ShATerm
u

instance ShATermLG Static.DevGraph.DGNodeInfo where
  toShATermLG :: ATermTable -> DGNodeInfo -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: DGNodeInfo
xv = case DGNodeInfo
xv of
    DGNode a :: DGOrigin
a b :: ConsStatus
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> DGOrigin -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 DGOrigin
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> ConsStatus -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 ConsStatus
b
      (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 "DGNode" [Int
a', Int
b'] []) ATermTable
att2
    DGRef a :: LibName
a b :: Int
b -> 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 -> Int -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 Int
b
      (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 "DGRef" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DGNodeInfo)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "DGNode" [a :: Int
a, b :: Int
b] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, DGOrigin)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: DGOrigin
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, ConsStatus)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: ConsStatus
b') ->
      (ATermTable
att2, DGOrigin -> ConsStatus -> DGNodeInfo
DGNode DGOrigin
a' ConsStatus
b') }}
    ShAAppl "DGRef" [a :: Int
a, b :: Int
b] _ ->
      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, Int)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Int
b') ->
      (ATermTable
att2, LibName -> Int -> DGNodeInfo
DGRef LibName
a' Int
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, DGNodeInfo)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.DGNodeInfo" ShATerm
u

instance ShATermLG Static.DevGraph.DGOrigin where
  toShATermLG :: ATermTable -> DGOrigin -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: DGOrigin
xv = case DGOrigin
xv of
    DGEmpty -> (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 "DGEmpty" [] []) ATermTable
att0
    DGBasic -> (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 "DGBasic" [] []) ATermTable
att0
    DGBasicSpec a :: Maybe G_basic_spec
a b :: G_sign
b c :: Set G_symbol
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Maybe G_basic_spec -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 Maybe G_basic_spec
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> G_sign -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 G_sign
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Set G_symbol -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 Set G_symbol
c
      (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 "DGBasicSpec" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    DGExtension -> (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 "DGExtension" [] []) ATermTable
att0
    DGLogicCoercion -> (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 "DGLogicCoercion" [] []) ATermTable
att0
    DGTranslation a :: Renamed
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Renamed -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 Renamed
a
      (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 "DGTranslation" [Int
a'] []) ATermTable
att1
    DGUnion -> (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 "DGUnion" [] []) ATermTable
att0
    DGIntersect -> (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 "DGIntersect" [] []) ATermTable
att0
    DGExtract -> (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 "DGExtract" [] []) ATermTable
att0
    DGRestriction a :: MaybeRestricted
a b :: Set G_symbol
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> MaybeRestricted -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 MaybeRestricted
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Set G_symbol -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 Set G_symbol
b
      (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 "DGRestriction" [Int
a', Int
b'] []) ATermTable
att2
    DGRevealTranslation ->
      (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 "DGRevealTranslation" [] []) ATermTable
att0
    DGFreeOrCofree a :: FreeOrCofree
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> FreeOrCofree -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 FreeOrCofree
a
      (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 "DGFreeOrCofree" [Int
a'] []) ATermTable
att1
    DGLocal -> (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 "DGLocal" [] []) ATermTable
att0
    DGClosed -> (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 "DGClosed" [] []) ATermTable
att0
    DGLogicQual -> (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 "DGLogicQual" [] []) ATermTable
att0
    DGData -> (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 "DGData" [] []) ATermTable
att0
    DGFormalParams -> (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 "DGFormalParams" [] []) ATermTable
att0
    DGVerificationGeneric ->
      (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 "DGVerificationGeneric" [] []) ATermTable
att0
    DGImports -> (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 "DGImports" [] []) ATermTable
att0
    DGInst a :: IRI
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> IRI -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 IRI
a
      (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 "DGInst" [Int
a'] []) ATermTable
att1
    DGFitSpec -> (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 "DGFitSpec" [] []) ATermTable
att0
    DGFitView a :: IRI
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> IRI -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 IRI
a
      (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 "DGFitView" [Int
a'] []) ATermTable
att1
    DGProof -> (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 "DGProof" [] []) ATermTable
att0
    DGNormalForm a :: Int
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Int -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 Int
a
      (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 "DGNormalForm" [Int
a'] []) ATermTable
att1
    DGintegratedSCC -> (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 "DGintegratedSCC" [] []) ATermTable
att0
    DGFlattening -> (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 "DGFlattening" [] []) ATermTable
att0
    DGAlignment -> (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 "DGAlignment" [] []) ATermTable
att0
    DGTest -> (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 "DGTest" [] []) ATermTable
att0
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DGOrigin)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "DGEmpty" [] _ -> (ATermTable
att0, DGOrigin
DGEmpty)
    ShAAppl "DGBasic" [] _ -> (ATermTable
att0, DGOrigin
DGBasic)
    ShAAppl "DGBasicSpec" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Maybe G_basic_spec)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Maybe G_basic_spec
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, G_sign)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: G_sign
b') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Set G_symbol)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Set G_symbol
c') ->
      (ATermTable
att3, Maybe G_basic_spec -> G_sign -> Set G_symbol -> DGOrigin
DGBasicSpec Maybe G_basic_spec
a' G_sign
b' Set G_symbol
c') }}}
    ShAAppl "DGExtension" [] _ -> (ATermTable
att0, DGOrigin
DGExtension)
    ShAAppl "DGLogicCoercion" [] _ -> (ATermTable
att0, DGOrigin
DGLogicCoercion)
    ShAAppl "DGTranslation" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Renamed)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Renamed
a') ->
      (ATermTable
att1, Renamed -> DGOrigin
DGTranslation Renamed
a') }
    ShAAppl "DGUnion" [] _ -> (ATermTable
att0, DGOrigin
DGUnion)
    ShAAppl "DGIntersect" [] _ -> (ATermTable
att0, DGOrigin
DGIntersect)
    ShAAppl "DGExtract" [] _ -> (ATermTable
att0, DGOrigin
DGExtract)
    ShAAppl "DGRestriction" [a :: Int
a, b :: Int
b] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, MaybeRestricted)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: MaybeRestricted
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Set G_symbol)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Set G_symbol
b') ->
      (ATermTable
att2, MaybeRestricted -> Set G_symbol -> DGOrigin
DGRestriction MaybeRestricted
a' Set G_symbol
b') }}
    ShAAppl "DGRevealTranslation" [] _ -> (ATermTable
att0, DGOrigin
DGRevealTranslation)
    ShAAppl "DGFreeOrCofree" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, FreeOrCofree)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: FreeOrCofree
a') ->
      (ATermTable
att1, FreeOrCofree -> DGOrigin
DGFreeOrCofree FreeOrCofree
a') }
    ShAAppl "DGLocal" [] _ -> (ATermTable
att0, DGOrigin
DGLocal)
    ShAAppl "DGClosed" [] _ -> (ATermTable
att0, DGOrigin
DGClosed)
    ShAAppl "DGLogicQual" [] _ -> (ATermTable
att0, DGOrigin
DGLogicQual)
    ShAAppl "DGData" [] _ -> (ATermTable
att0, DGOrigin
DGData)
    ShAAppl "DGFormalParams" [] _ -> (ATermTable
att0, DGOrigin
DGFormalParams)
    ShAAppl "DGVerificationGeneric" [] _ -> (ATermTable
att0, DGOrigin
DGVerificationGeneric)
    ShAAppl "DGImports" [] _ -> (ATermTable
att0, DGOrigin
DGImports)
    ShAAppl "DGInst" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, IRI)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: IRI
a') ->
      (ATermTable
att1, IRI -> DGOrigin
DGInst IRI
a') }
    ShAAppl "DGFitSpec" [] _ -> (ATermTable
att0, DGOrigin
DGFitSpec)
    ShAAppl "DGFitView" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, IRI)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: IRI
a') ->
      (ATermTable
att1, IRI -> DGOrigin
DGFitView IRI
a') }
    ShAAppl "DGProof" [] _ -> (ATermTable
att0, DGOrigin
DGProof)
    ShAAppl "DGNormalForm" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Int)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Int
a') ->
      (ATermTable
att1, Int -> DGOrigin
DGNormalForm Int
a') }
    ShAAppl "DGintegratedSCC" [] _ -> (ATermTable
att0, DGOrigin
DGintegratedSCC)
    ShAAppl "DGFlattening" [] _ -> (ATermTable
att0, DGOrigin
DGFlattening)
    ShAAppl "DGAlignment" [] _ -> (ATermTable
att0, DGOrigin
DGAlignment)
    ShAAppl "DGTest" [] _ -> (ATermTable
att0, DGOrigin
DGTest)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, DGOrigin)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.DGOrigin" ShATerm
u

instance ShATermLG Static.DevGraph.MaybeRestricted where
  toShATermLG :: ATermTable -> MaybeRestricted -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: MaybeRestricted
xv = case MaybeRestricted
xv of
    NoRestriction -> (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 "NoRestriction" [] []) ATermTable
att0
    Restricted a :: RESTRICTION
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> RESTRICTION -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 RESTRICTION
a
      (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 "Restricted" [Int
a'] []) ATermTable
att1
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, MaybeRestricted)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "NoRestriction" [] _ -> (ATermTable
att0, MaybeRestricted
NoRestriction)
    ShAAppl "Restricted" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, RESTRICTION)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: RESTRICTION
a') ->
      (ATermTable
att1, RESTRICTION -> MaybeRestricted
Restricted RESTRICTION
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, MaybeRestricted)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.MaybeRestricted" ShATerm
u

instance ShATermLG Static.DevGraph.Renamed where
  toShATermLG :: ATermTable -> Renamed -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: Renamed
xv = case Renamed
xv of
    Renamed a :: RENAMING
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> RENAMING -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 RENAMING
a
      (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 "Renamed" [Int
a'] []) ATermTable
att1
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, Renamed)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Renamed" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, RENAMING)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: RENAMING
a') ->
      (ATermTable
att1, RENAMING -> Renamed
Renamed RENAMING
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Renamed)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.Renamed" ShATerm
u

instance ShATermLG Static.DevGraph.MaybeNode where
  toShATermLG :: ATermTable -> MaybeNode -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: MaybeNode
xv = case MaybeNode
xv of
    JustNode a :: NodeSig
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NodeSig -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 NodeSig
a
      (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 "JustNode" [Int
a'] []) ATermTable
att1
    EmptyNode a :: AnyLogic
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> AnyLogic -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 AnyLogic
a
      (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 "EmptyNode" [Int
a'] []) ATermTable
att1
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, MaybeNode)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "JustNode" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, NodeSig)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: NodeSig
a') ->
      (ATermTable
att1, NodeSig -> MaybeNode
JustNode NodeSig
a') }
    ShAAppl "EmptyNode" [a :: Int
a] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, AnyLogic)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: AnyLogic
a') ->
      (ATermTable
att1, AnyLogic -> MaybeNode
EmptyNode AnyLogic
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, MaybeNode)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.MaybeNode" ShATerm
u

instance ShATermLG Static.DevGraph.NodeSig where
  toShATermLG :: ATermTable -> NodeSig -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: NodeSig
xv = case NodeSig
xv of
    NodeSig a :: Int
a b :: G_sign
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Int -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 Int
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> G_sign -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 G_sign
b
      (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 "NodeSig" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, NodeSig)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "NodeSig" [a :: Int
a, b :: Int
b] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Int)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Int
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, G_sign)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: G_sign
b') ->
      (ATermTable
att2, Int -> G_sign -> NodeSig
NodeSig Int
a' G_sign
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, NodeSig)
forall a. String -> ShATerm -> a
fromShATermError "Static.DevGraph.NodeSig" ShATerm
u