{-# OPTIONS -w -O0 #-}
{-# LANGUAGE CPP, StandaloneDeriving, DeriveDataTypeable, DeriveGeneric #-}
{- |
Module      :  ATC/DgUtils.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.DgUtils.XPathPart'
'Static.DgUtils.NodeName'
'Static.DgUtils.DGNodeType'
'Static.DgUtils.NodeMod'
'Static.DgUtils.EdgeId'
'Static.DgUtils.ProofBasis'
'Static.DgUtils.DGRule'
'Static.DgUtils.ThmLinkStatus'
'Static.DgUtils.Scope'
'Static.DgUtils.LinkKind'
'Static.DgUtils.FreeOrCofree'
'Static.DgUtils.ConsStatus'
'Static.DgUtils.DGEdgeType'
'Static.DgUtils.DGEdgeTypeModInc'
'Static.DgUtils.ThmTypes'
'Static.DgUtils.RTPointer'
'Static.DgUtils.RTLeaves'
-}

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

module ATC.DgUtils () where

import ATC.Consistency
import ATC.Grothendieck
import ATC.LibName
import ATerm.Lib
import Common.Consistency
import Common.IRI
import Common.Id
import Common.LibName
import Common.Utils
import Data.Data
import Data.List
import Data.Maybe
import Static.DgUtils
import qualified Common.Lib.Rel as Rel
import qualified Control.Monad.Fail as Fail
import qualified Data.Map as Map
import qualified Data.Set as Set

{-! for Static.DgUtils.XPathPart derive : ShATermLG !-}
{-! for Static.DgUtils.NodeName derive : ShATermLG !-}
{-! for Static.DgUtils.DGNodeType derive : ShATermLG !-}
{-! for Static.DgUtils.NodeMod derive : ShATermLG !-}
{-! for Static.DgUtils.EdgeId derive : ShATermLG !-}
{-! for Static.DgUtils.ProofBasis derive : ShATermLG !-}
{-! for Static.DgUtils.DGRule derive : ShATermLG !-}
{-! for Static.DgUtils.ThmLinkStatus derive : ShATermLG !-}
{-! for Static.DgUtils.Scope derive : ShATermLG !-}
{-! for Static.DgUtils.LinkKind derive : ShATermLG !-}
{-! for Static.DgUtils.FreeOrCofree derive : ShATermLG !-}
{-! for Static.DgUtils.ConsStatus derive : ShATermLG !-}
{-! for Static.DgUtils.DGEdgeType derive : ShATermLG !-}
{-! for Static.DgUtils.DGEdgeTypeModInc derive : ShATermLG !-}
{-! for Static.DgUtils.ThmTypes derive : ShATermLG !-}
{-! for Static.DgUtils.RTPointer derive : ShATermLG !-}
{-! for Static.DgUtils.RTLeaves derive : ShATermLG !-}

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

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

instance ShATermLG Static.DgUtils.NodeName where
  toShATermLG :: ATermTable -> NodeName -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: NodeName
xv = case NodeName
xv of
    NodeName a :: IRI
a b :: String
b c :: Int
c d :: [XPathPart]
d e :: Range
e -> 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 -> 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 -> Int -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 Int
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> [XPathPart] -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att3 [XPathPart]
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> Range -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att4 Range
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 "NodeName" [Int
a', Int
b', Int
c', Int
d', Int
e'] []) ATermTable
att5
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, NodeName)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "NodeName" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e] _ ->
      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, 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, Int)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Int
c') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, [XPathPart])
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: [XPathPart]
d') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Range)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: Range
e') ->
      (ATermTable
att5, IRI -> String -> Int -> [XPathPart] -> Range -> NodeName
NodeName IRI
a' String
b' Int
c' [XPathPart]
d' Range
e') }}}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, NodeName)
forall a. String -> ShATerm -> a
fromShATermError "Static.DgUtils.NodeName" ShATerm
u

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

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

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

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

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

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

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

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

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

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

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

instance ShATermLG Static.DgUtils.DGEdgeTypeModInc where
  toShATermLG :: ATermTable -> DGEdgeTypeModInc -> IO (ATermTable, Int)
toShATermLG att0 :: ATermTable
att0 xv :: DGEdgeTypeModInc
xv = case DGEdgeTypeModInc
xv of
    GlobalDef -> (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 "GlobalDef" [] []) ATermTable
att0
    HetDef -> (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 "HetDef" [] []) ATermTable
att0
    HidingDef -> (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 "HidingDef" [] []) ATermTable
att0
    LocalDef -> (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 "LocalDef" [] []) ATermTable
att0
    FreeOrCofreeDef 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 "FreeOrCofreeDef" [Int
a'] []) ATermTable
att1
    ThmType a :: ThmTypes
a b :: Bool
b c :: Bool
c d :: Bool
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> ThmTypes -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att0 ThmTypes
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att1 Bool
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG' ATermTable
att2 Bool
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
      (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 "ThmType" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
  fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, DGEdgeTypeModInc)
fromShATermLG lg :: LogicGraph
lg ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "GlobalDef" [] _ -> (ATermTable
att0, DGEdgeTypeModInc
GlobalDef)
    ShAAppl "HetDef" [] _ -> (ATermTable
att0, DGEdgeTypeModInc
HetDef)
    ShAAppl "HidingDef" [] _ -> (ATermTable
att0, DGEdgeTypeModInc
HidingDef)
    ShAAppl "LocalDef" [] _ -> (ATermTable
att0, DGEdgeTypeModInc
LocalDef)
    ShAAppl "FreeOrCofreeDef" [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 -> DGEdgeTypeModInc
FreeOrCofreeDef FreeOrCofree
a') }
    ShAAppl "ThmType" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, ThmTypes)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: ThmTypes
a') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Bool
b') ->
      case LogicGraph -> Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermLG t =>
LogicGraph -> Int -> ATermTable -> (ATermTable, t)
fromShATermLG' LogicGraph
lg Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Bool
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') ->
      (ATermTable
att4, ThmTypes -> Bool -> Bool -> Bool -> DGEdgeTypeModInc
ThmType ThmTypes
a' Bool
b' Bool
c' Bool
d') }}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, DGEdgeTypeModInc)
forall a. String -> ShATerm -> a
fromShATermError "Static.DgUtils.DGEdgeTypeModInc" ShATerm
u

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

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

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