{-# OPTIONS -w -O0 #-}
{-# LANGUAGE CPP, StandaloneDeriving, DeriveDataTypeable, DeriveGeneric #-}
{- |
Module      :  SoftFOL/ATC_SoftFOL.der.hs
Description :  generated ShATermConvertible, Json 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 ShATermConvertible, Json
  for the type(s):
'SoftFOL.Sign.Sign'
'SoftFOL.Sign.Generated'
'SoftFOL.Sign.SFSymbol'
'SoftFOL.Sign.SFSymbType'
'SoftFOL.Sign.SPProblem'
'SoftFOL.Sign.SPLogicalPart'
'SoftFOL.Sign.SPSymbolList'
'SoftFOL.Sign.SPSignSym'
'SoftFOL.Sign.SPSortSym'
'SoftFOL.Sign.SPDeclaration'
'SoftFOL.Sign.SPFormulaList'
'SoftFOL.Sign.SPClauseList'
'SoftFOL.Sign.SPOriginType'
'SoftFOL.Sign.SPClauseType'
'SoftFOL.Sign.NSPClause'
'SoftFOL.Sign.NSPClauseBody'
'SoftFOL.Sign.TermWsList'
'SoftFOL.Sign.SPTerm'
'SoftFOL.Sign.FileName'
'SoftFOL.Sign.FormKind'
'SoftFOL.Sign.Role'
'SoftFOL.Sign.Name'
'SoftFOL.Sign.Annos'
'SoftFOL.Sign.Source'
'SoftFOL.Sign.AWord'
'SoftFOL.Sign.GenTerm'
'SoftFOL.Sign.GenData'
'SoftFOL.Sign.FormData'
'SoftFOL.Sign.Info'
'SoftFOL.Sign.TPTP'
'SoftFOL.Sign.SPLiteral'
'SoftFOL.Sign.SPQuantSym'
'SoftFOL.Sign.SPSymbol'
'SoftFOL.Sign.SPProofList'
'SoftFOL.Sign.SPProofStep'
'SoftFOL.Sign.SPReference'
'SoftFOL.Sign.SPResult'
'SoftFOL.Sign.SPRuleAppl'
'SoftFOL.Sign.SPUserRuleAppl'
'SoftFOL.Sign.SPParent'
'SoftFOL.Sign.SPKey'
'SoftFOL.Sign.SPValue'
'SoftFOL.Sign.SPDescription'
'SoftFOL.Sign.SPLogState'
'SoftFOL.Sign.SPSetting'
'SoftFOL.Sign.SPSettingBody'
'SoftFOL.Sign.SPHypothesis'
'SoftFOL.Sign.SPSettingLabel'
'SoftFOL.Sign.SPCRBIND'
-}

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

module SoftFOL.ATC_SoftFOL () where

import ATC.AS_Annotation
import ATerm.Lib
import Common.AS_Annotation hiding (Name)
import Common.DefaultMorphism
import Common.Id
import Common.Json.Instances
import Data.Aeson(ToJSON, FromJSON)
import Data.Char
import Data.Data
import Data.Maybe (isNothing)
import GHC.Generics(Generic)
import SoftFOL.Sign
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 SoftFOL.Sign.Sign derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.Generated derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SFSymbol derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SFSymbType derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPProblem derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPLogicalPart derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPSymbolList derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPSignSym derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPSortSym derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPDeclaration derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPFormulaList derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPClauseList derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPOriginType derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPClauseType derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.NSPClause derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.NSPClauseBody derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.TermWsList derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPTerm derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.FileName derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.FormKind derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.Role derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.Name derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.Annos derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.Source derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.AWord derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.GenTerm derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.GenData derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.FormData derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.Info derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.TPTP derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPLiteral derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPQuantSym derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPSymbol derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPProofList derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPProofStep derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPReference derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPResult derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPRuleAppl derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPUserRuleAppl derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPParent derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPKey derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPValue derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPDescription derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPLogState derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPSetting derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPSettingBody derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPHypothesis derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPSettingLabel derive : ShATermConvertible !-}
{-! for SoftFOL.Sign.SPCRBIND derive : ShATermConvertible !-}

{-! for SoftFOL.Sign.Sign derive : Json !-}
{-! for SoftFOL.Sign.Generated derive : Json !-}
{-! for SoftFOL.Sign.SFSymbol derive : Json !-}
{-! for SoftFOL.Sign.SFSymbType derive : Json !-}
{-! for SoftFOL.Sign.SPProblem derive : Json !-}
{-! for SoftFOL.Sign.SPLogicalPart derive : Json !-}
{-! for SoftFOL.Sign.SPSymbolList derive : Json !-}
{-! for SoftFOL.Sign.SPSignSym derive : Json !-}
{-! for SoftFOL.Sign.SPSortSym derive : Json !-}
{-! for SoftFOL.Sign.SPDeclaration derive : Json !-}
{-! for SoftFOL.Sign.SPFormulaList derive : Json !-}
{-! for SoftFOL.Sign.SPClauseList derive : Json !-}
{-! for SoftFOL.Sign.SPOriginType derive : Json !-}
{-! for SoftFOL.Sign.SPClauseType derive : Json !-}
{-! for SoftFOL.Sign.NSPClause derive : Json !-}
{-! for SoftFOL.Sign.NSPClauseBody derive : Json !-}
{-! for SoftFOL.Sign.TermWsList derive : Json !-}
{-! for SoftFOL.Sign.SPTerm derive : Json !-}
{-! for SoftFOL.Sign.FileName derive : Json !-}
{-! for SoftFOL.Sign.FormKind derive : Json !-}
{-! for SoftFOL.Sign.Role derive : Json !-}
{-! for SoftFOL.Sign.Name derive : Json !-}
{-! for SoftFOL.Sign.Annos derive : Json !-}
{-! for SoftFOL.Sign.Source derive : Json !-}
{-! for SoftFOL.Sign.AWord derive : Json !-}
{-! for SoftFOL.Sign.GenTerm derive : Json !-}
{-! for SoftFOL.Sign.GenData derive : Json !-}
{-! for SoftFOL.Sign.FormData derive : Json !-}
{-! for SoftFOL.Sign.Info derive : Json !-}
{-! for SoftFOL.Sign.TPTP derive : Json !-}
{-! for SoftFOL.Sign.SPLiteral derive : Json !-}
{-! for SoftFOL.Sign.SPQuantSym derive : Json !-}
{-! for SoftFOL.Sign.SPSymbol derive : Json !-}
{-! for SoftFOL.Sign.SPProofList derive : Json !-}
{-! for SoftFOL.Sign.SPProofStep derive : Json !-}
{-! for SoftFOL.Sign.SPReference derive : Json !-}
{-! for SoftFOL.Sign.SPResult derive : Json !-}
{-! for SoftFOL.Sign.SPRuleAppl derive : Json !-}
{-! for SoftFOL.Sign.SPUserRuleAppl derive : Json !-}
{-! for SoftFOL.Sign.SPParent derive : Json !-}
{-! for SoftFOL.Sign.SPKey derive : Json !-}
{-! for SoftFOL.Sign.SPValue derive : Json !-}
{-! for SoftFOL.Sign.SPDescription derive : Json !-}
{-! for SoftFOL.Sign.SPLogState derive : Json !-}
{-! for SoftFOL.Sign.SPSetting derive : Json !-}
{-! for SoftFOL.Sign.SPSettingBody derive : Json !-}
{-! for SoftFOL.Sign.SPHypothesis derive : Json !-}
{-! for SoftFOL.Sign.SPSettingLabel derive : Json !-}
{-! for SoftFOL.Sign.SPCRBIND derive : Json !-}

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

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPCRBIND
instance Data.Aeson.ToJSON SoftFOL.Sign.SPCRBIND where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPCRBIND where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPSettingLabel
instance Data.Aeson.ToJSON SoftFOL.Sign.SPSettingLabel where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPSettingLabel where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPHypothesis
instance Data.Aeson.ToJSON SoftFOL.Sign.SPHypothesis where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPHypothesis where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPSettingBody
instance Data.Aeson.ToJSON SoftFOL.Sign.SPSettingBody where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPSettingBody where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPSetting
instance Data.Aeson.ToJSON SoftFOL.Sign.SPSetting where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPSetting where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPLogState
instance Data.Aeson.ToJSON SoftFOL.Sign.SPLogState where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPLogState where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPDescription
instance Data.Aeson.ToJSON SoftFOL.Sign.SPDescription where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPDescription where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPValue
instance Data.Aeson.ToJSON SoftFOL.Sign.SPValue where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPValue where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPKey
instance Data.Aeson.ToJSON SoftFOL.Sign.SPKey where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPKey where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPParent
instance Data.Aeson.ToJSON SoftFOL.Sign.SPParent where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPParent where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPUserRuleAppl
instance Data.Aeson.ToJSON SoftFOL.Sign.SPUserRuleAppl where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPUserRuleAppl where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPRuleAppl
instance Data.Aeson.ToJSON SoftFOL.Sign.SPRuleAppl where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPRuleAppl where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPResult
instance Data.Aeson.ToJSON SoftFOL.Sign.SPResult where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPResult where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPReference
instance Data.Aeson.ToJSON SoftFOL.Sign.SPReference where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPReference where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPProofStep
instance Data.Aeson.ToJSON SoftFOL.Sign.SPProofStep where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPProofStep where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPProofList
instance Data.Aeson.ToJSON SoftFOL.Sign.SPProofList where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPProofList where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPSymbol
instance Data.Aeson.ToJSON SoftFOL.Sign.SPSymbol where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPSymbol where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPQuantSym
instance Data.Aeson.ToJSON SoftFOL.Sign.SPQuantSym where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPQuantSym where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPLiteral
instance Data.Aeson.ToJSON SoftFOL.Sign.SPLiteral where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPLiteral where

deriving instance GHC.Generics.Generic SoftFOL.Sign.TPTP
instance Data.Aeson.ToJSON SoftFOL.Sign.TPTP where
instance Data.Aeson.FromJSON SoftFOL.Sign.TPTP where

deriving instance GHC.Generics.Generic SoftFOL.Sign.Info
instance Data.Aeson.ToJSON SoftFOL.Sign.Info where
instance Data.Aeson.FromJSON SoftFOL.Sign.Info where

deriving instance GHC.Generics.Generic SoftFOL.Sign.FormData
instance Data.Aeson.ToJSON SoftFOL.Sign.FormData where
instance Data.Aeson.FromJSON SoftFOL.Sign.FormData where

deriving instance GHC.Generics.Generic SoftFOL.Sign.GenData
instance Data.Aeson.ToJSON SoftFOL.Sign.GenData where
instance Data.Aeson.FromJSON SoftFOL.Sign.GenData where

deriving instance GHC.Generics.Generic SoftFOL.Sign.GenTerm
instance Data.Aeson.ToJSON SoftFOL.Sign.GenTerm where
instance Data.Aeson.FromJSON SoftFOL.Sign.GenTerm where

deriving instance GHC.Generics.Generic SoftFOL.Sign.AWord
instance Data.Aeson.ToJSON SoftFOL.Sign.AWord where
instance Data.Aeson.FromJSON SoftFOL.Sign.AWord where

deriving instance GHC.Generics.Generic SoftFOL.Sign.Source
instance Data.Aeson.ToJSON SoftFOL.Sign.Source where
instance Data.Aeson.FromJSON SoftFOL.Sign.Source where

deriving instance GHC.Generics.Generic SoftFOL.Sign.Annos
instance Data.Aeson.ToJSON SoftFOL.Sign.Annos where
instance Data.Aeson.FromJSON SoftFOL.Sign.Annos where

deriving instance GHC.Generics.Generic SoftFOL.Sign.Name
instance Data.Aeson.ToJSON SoftFOL.Sign.Name where
instance Data.Aeson.FromJSON SoftFOL.Sign.Name where

deriving instance GHC.Generics.Generic SoftFOL.Sign.Role
instance Data.Aeson.ToJSON SoftFOL.Sign.Role where
instance Data.Aeson.FromJSON SoftFOL.Sign.Role where

deriving instance GHC.Generics.Generic SoftFOL.Sign.FormKind
instance Data.Aeson.ToJSON SoftFOL.Sign.FormKind where
instance Data.Aeson.FromJSON SoftFOL.Sign.FormKind where

deriving instance GHC.Generics.Generic SoftFOL.Sign.FileName
instance Data.Aeson.ToJSON SoftFOL.Sign.FileName where
instance Data.Aeson.FromJSON SoftFOL.Sign.FileName where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPTerm
instance Data.Aeson.ToJSON SoftFOL.Sign.SPTerm where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPTerm where

deriving instance GHC.Generics.Generic SoftFOL.Sign.TermWsList
instance Data.Aeson.ToJSON SoftFOL.Sign.TermWsList where
instance Data.Aeson.FromJSON SoftFOL.Sign.TermWsList where

deriving instance GHC.Generics.Generic SoftFOL.Sign.NSPClauseBody
instance Data.Aeson.ToJSON SoftFOL.Sign.NSPClauseBody where
instance Data.Aeson.FromJSON SoftFOL.Sign.NSPClauseBody where

deriving instance GHC.Generics.Generic SoftFOL.Sign.NSPClause
instance Data.Aeson.ToJSON SoftFOL.Sign.NSPClause where
instance Data.Aeson.FromJSON SoftFOL.Sign.NSPClause where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPClauseType
instance Data.Aeson.ToJSON SoftFOL.Sign.SPClauseType where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPClauseType where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPOriginType
instance Data.Aeson.ToJSON SoftFOL.Sign.SPOriginType where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPOriginType where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPClauseList
instance Data.Aeson.ToJSON SoftFOL.Sign.SPClauseList where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPClauseList where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPFormulaList
instance Data.Aeson.ToJSON SoftFOL.Sign.SPFormulaList where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPFormulaList where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPDeclaration
instance Data.Aeson.ToJSON SoftFOL.Sign.SPDeclaration where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPDeclaration where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPSortSym
instance Data.Aeson.ToJSON SoftFOL.Sign.SPSortSym where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPSortSym where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPSignSym
instance Data.Aeson.ToJSON SoftFOL.Sign.SPSignSym where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPSignSym where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPSymbolList
instance Data.Aeson.ToJSON SoftFOL.Sign.SPSymbolList where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPSymbolList where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPLogicalPart
instance Data.Aeson.ToJSON SoftFOL.Sign.SPLogicalPart where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPLogicalPart where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SPProblem
instance Data.Aeson.ToJSON SoftFOL.Sign.SPProblem where
instance Data.Aeson.FromJSON SoftFOL.Sign.SPProblem where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SFSymbType
instance Data.Aeson.ToJSON SoftFOL.Sign.SFSymbType where
instance Data.Aeson.FromJSON SoftFOL.Sign.SFSymbType where

deriving instance GHC.Generics.Generic SoftFOL.Sign.SFSymbol
instance Data.Aeson.ToJSON SoftFOL.Sign.SFSymbol where
instance Data.Aeson.FromJSON SoftFOL.Sign.SFSymbol where

deriving instance GHC.Generics.Generic SoftFOL.Sign.Generated
instance Data.Aeson.ToJSON SoftFOL.Sign.Generated where
instance Data.Aeson.FromJSON SoftFOL.Sign.Generated where

deriving instance GHC.Generics.Generic SoftFOL.Sign.Sign
instance Data.Aeson.ToJSON SoftFOL.Sign.Sign where
instance Data.Aeson.FromJSON SoftFOL.Sign.Sign where

instance ShATermConvertible SoftFOL.Sign.SPCRBIND where
  toShATermAux :: ATermTable -> SPCRBIND -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPCRBIND
xv = case SPCRBIND
xv of
    SPCRBIND a :: String
a b :: String
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 String
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' 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 "SPCRBIND" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPCRBIND)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SPCRBIND" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: String
a') ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: String
b') ->
      (ATermTable
att2, String -> String -> SPCRBIND
SPCRBIND String
a' String
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPCRBIND)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPCRBIND" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPSettingLabel where
  toShATermAux :: ATermTable -> SPSettingLabel -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPSettingLabel
xv = case SPSettingLabel
xv of
    KIV -> (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 "KIV" [] []) ATermTable
att0
    LEM -> (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 "LEM" [] []) ATermTable
att0
    OTTER -> (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 "OTTER" [] []) ATermTable
att0
    PROTEIN -> (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 "PROTEIN" [] []) ATermTable
att0
    SATURATE -> (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 "SATURATE" [] []) ATermTable
att0
    ThreeTAP -> (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 "ThreeTAP" [] []) ATermTable
att0
    SETHEO -> (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 "SETHEO" [] []) ATermTable
att0
    SPASS -> (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 "SPASS" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPSettingLabel)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "KIV" [] _ -> (ATermTable
att0, SPSettingLabel
KIV)
    ShAAppl "LEM" [] _ -> (ATermTable
att0, SPSettingLabel
LEM)
    ShAAppl "OTTER" [] _ -> (ATermTable
att0, SPSettingLabel
OTTER)
    ShAAppl "PROTEIN" [] _ -> (ATermTable
att0, SPSettingLabel
PROTEIN)
    ShAAppl "SATURATE" [] _ -> (ATermTable
att0, SPSettingLabel
SATURATE)
    ShAAppl "ThreeTAP" [] _ -> (ATermTable
att0, SPSettingLabel
ThreeTAP)
    ShAAppl "SETHEO" [] _ -> (ATermTable
att0, SPSettingLabel
SETHEO)
    ShAAppl "SPASS" [] _ -> (ATermTable
att0, SPSettingLabel
SPASS)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPSettingLabel)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPSettingLabel" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPHypothesis where
  toShATermAux :: ATermTable -> SPHypothesis -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPHypothesis
xv = case SPHypothesis
xv of
    SPHypothesis a :: [SPIdentifier]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [SPIdentifier] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [SPIdentifier]
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 "SPHypothesis" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPHypothesis)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SPHypothesis" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, [SPIdentifier])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [SPIdentifier]
a') ->
      (ATermTable
att1, [SPIdentifier] -> SPHypothesis
SPHypothesis [SPIdentifier]
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPHypothesis)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPHypothesis" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPSettingBody where
  toShATermAux :: ATermTable -> SPSettingBody -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPSettingBody
xv = case SPSettingBody
xv of
    SPClauseRelation a :: [SPCRBIND]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [SPCRBIND] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [SPCRBIND]
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 "SPClauseRelation" [Int
a'] []) ATermTable
att1
    SPFlag a :: String
a b :: [String]
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 String
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [String] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' 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 "SPFlag" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPSettingBody)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SPClauseRelation" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, [SPCRBIND])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [SPCRBIND]
a') ->
      (ATermTable
att1, [SPCRBIND] -> SPSettingBody
SPClauseRelation [SPCRBIND]
a') }
    ShAAppl "SPFlag" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: String
a') ->
      case Int -> ATermTable -> (ATermTable, [String])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [String]
b') ->
      (ATermTable
att2, String -> [String] -> SPSettingBody
SPFlag String
a' [String]
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPSettingBody)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPSettingBody" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPSetting where
  toShATermAux :: ATermTable -> SPSetting -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPSetting
xv = case SPSetting
xv of
    SPGeneralSettings a :: [SPHypothesis]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [SPHypothesis] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [SPHypothesis]
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 "SPGeneralSettings" [Int
a'] []) ATermTable
att1
    SPSettings a :: SPSettingLabel
a b :: [SPSettingBody]
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPSettingLabel -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPSettingLabel
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [SPSettingBody] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [SPSettingBody]
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 "SPSettings" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPSetting)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SPGeneralSettings" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, [SPHypothesis])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [SPHypothesis]
a') ->
      (ATermTable
att1, [SPHypothesis] -> SPSetting
SPGeneralSettings [SPHypothesis]
a') }
    ShAAppl "SPSettings" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, SPSettingLabel)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPSettingLabel
a') ->
      case Int -> ATermTable -> (ATermTable, [SPSettingBody])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [SPSettingBody]
b') ->
      (ATermTable
att2, SPSettingLabel -> [SPSettingBody] -> SPSetting
SPSettings SPSettingLabel
a' [SPSettingBody]
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPSetting)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPSetting" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPLogState where
  toShATermAux :: ATermTable -> SPLogState -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPLogState
xv = case SPLogState
xv of
    SPStateSatisfiable ->
      (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 "SPStateSatisfiable" [] []) ATermTable
att0
    SPStateUnsatisfiable ->
      (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 "SPStateUnsatisfiable" [] []) ATermTable
att0
    SPStateUnknown -> (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 "SPStateUnknown" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPLogState)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SPStateSatisfiable" [] _ -> (ATermTable
att0, SPLogState
SPStateSatisfiable)
    ShAAppl "SPStateUnsatisfiable" [] _ -> (ATermTable
att0, SPLogState
SPStateUnsatisfiable)
    ShAAppl "SPStateUnknown" [] _ -> (ATermTable
att0, SPLogState
SPStateUnknown)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPLogState)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPLogState" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPDescription where
  toShATermAux :: ATermTable -> SPDescription -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPDescription
xv = case SPDescription
xv of
    SPDescription a :: String
a b :: String
b c :: Maybe String
c d :: Maybe String
d e :: SPLogState
e f :: String
f g :: Maybe String
g -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 String
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 String
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Maybe String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Maybe String
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Maybe String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Maybe String
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> SPLogState -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 SPLogState
e
      (att6 :: ATermTable
att6, f' :: Int
f') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att5 String
f
      (att7 :: ATermTable
att7, g' :: Int
g') <- ATermTable -> Maybe String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att6 Maybe String
g
      (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 "SPDescription" [Int
a', Int
b', Int
c', Int
d', Int
e', Int
f',
                                                  Int
g'] []) ATermTable
att7
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPDescription)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SPDescription" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e, f :: Int
f, g :: Int
g] _ ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: String
a') ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: String
b') ->
      case Int -> ATermTable -> (ATermTable, Maybe String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Maybe String
c') ->
      case Int -> ATermTable -> (ATermTable, Maybe String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Maybe String
d') ->
      case Int -> ATermTable -> (ATermTable, SPLogState)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: SPLogState
e') ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
f ATermTable
att5 of
      { (att6 :: ATermTable
att6, f' :: String
f') ->
      case Int -> ATermTable -> (ATermTable, Maybe String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
g ATermTable
att6 of
      { (att7 :: ATermTable
att7, g' :: Maybe String
g') ->
      (ATermTable
att7, String
-> String
-> Maybe String
-> Maybe String
-> SPLogState
-> String
-> Maybe String
-> SPDescription
SPDescription String
a' String
b' Maybe String
c' Maybe String
d' SPLogState
e' String
f' Maybe String
g') }}}}}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPDescription)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPDescription" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPValue where
  toShATermAux :: ATermTable -> SPValue -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPValue
xv = case SPValue
xv of
    PValTerm a :: SPTerm
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPTerm
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 "PValTerm" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPValue)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "PValTerm" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, SPTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPTerm
a') ->
      (ATermTable
att1, SPTerm -> SPValue
PValTerm SPTerm
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPValue)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPValue" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPKey where
  toShATermAux :: ATermTable -> SPKey -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPKey
xv = case SPKey
xv of
    PKeyTerm a :: SPTerm
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPTerm
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 "PKeyTerm" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPKey)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "PKeyTerm" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, SPTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPTerm
a') ->
      (ATermTable
att1, SPTerm -> SPKey
PKeyTerm SPTerm
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPKey)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPKey" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPParent where
  toShATermAux :: ATermTable -> SPParent -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPParent
xv = case SPParent
xv of
    PParTerm a :: SPTerm
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPTerm
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 "PParTerm" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPParent)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "PParTerm" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, SPTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPTerm
a') ->
      (ATermTable
att1, SPTerm -> SPParent
PParTerm SPTerm
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPParent)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPParent" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPUserRuleAppl where
  toShATermAux :: ATermTable -> SPUserRuleAppl -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPUserRuleAppl
xv = case SPUserRuleAppl
xv of
    GeR -> (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 "GeR" [] []) ATermTable
att0
    SpL -> (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 "SpL" [] []) ATermTable
att0
    SpR -> (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 "SpR" [] []) ATermTable
att0
    EqF -> (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 "EqF" [] []) ATermTable
att0
    Rew -> (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 "Rew" [] []) ATermTable
att0
    Obv -> (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 "Obv" [] []) ATermTable
att0
    EmS -> (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 "EmS" [] []) ATermTable
att0
    SoR -> (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 "SoR" [] []) ATermTable
att0
    EqR -> (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 "EqR" [] []) ATermTable
att0
    Mpm -> (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 "Mpm" [] []) ATermTable
att0
    SPm -> (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 "SPm" [] []) ATermTable
att0
    OPm -> (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 "OPm" [] []) ATermTable
att0
    SHy -> (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 "SHy" [] []) ATermTable
att0
    OHy -> (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 "OHy" [] []) ATermTable
att0
    URR -> (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 "URR" [] []) ATermTable
att0
    Fac -> (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 "Fac" [] []) ATermTable
att0
    Spt -> (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 "Spt" [] []) ATermTable
att0
    Inp -> (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 "Inp" [] []) ATermTable
att0
    Con -> (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 "Con" [] []) ATermTable
att0
    RRE -> (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 "RRE" [] []) ATermTable
att0
    SSi -> (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 "SSi" [] []) ATermTable
att0
    ClR -> (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 "ClR" [] []) ATermTable
att0
    UnC -> (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 "UnC" [] []) ATermTable
att0
    Ter -> (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 "Ter" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPUserRuleAppl)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "GeR" [] _ -> (ATermTable
att0, SPUserRuleAppl
GeR)
    ShAAppl "SpL" [] _ -> (ATermTable
att0, SPUserRuleAppl
SpL)
    ShAAppl "SpR" [] _ -> (ATermTable
att0, SPUserRuleAppl
SpR)
    ShAAppl "EqF" [] _ -> (ATermTable
att0, SPUserRuleAppl
EqF)
    ShAAppl "Rew" [] _ -> (ATermTable
att0, SPUserRuleAppl
Rew)
    ShAAppl "Obv" [] _ -> (ATermTable
att0, SPUserRuleAppl
Obv)
    ShAAppl "EmS" [] _ -> (ATermTable
att0, SPUserRuleAppl
EmS)
    ShAAppl "SoR" [] _ -> (ATermTable
att0, SPUserRuleAppl
SoR)
    ShAAppl "EqR" [] _ -> (ATermTable
att0, SPUserRuleAppl
EqR)
    ShAAppl "Mpm" [] _ -> (ATermTable
att0, SPUserRuleAppl
Mpm)
    ShAAppl "SPm" [] _ -> (ATermTable
att0, SPUserRuleAppl
SPm)
    ShAAppl "OPm" [] _ -> (ATermTable
att0, SPUserRuleAppl
OPm)
    ShAAppl "SHy" [] _ -> (ATermTable
att0, SPUserRuleAppl
SHy)
    ShAAppl "OHy" [] _ -> (ATermTable
att0, SPUserRuleAppl
OHy)
    ShAAppl "URR" [] _ -> (ATermTable
att0, SPUserRuleAppl
URR)
    ShAAppl "Fac" [] _ -> (ATermTable
att0, SPUserRuleAppl
Fac)
    ShAAppl "Spt" [] _ -> (ATermTable
att0, SPUserRuleAppl
Spt)
    ShAAppl "Inp" [] _ -> (ATermTable
att0, SPUserRuleAppl
Inp)
    ShAAppl "Con" [] _ -> (ATermTable
att0, SPUserRuleAppl
Con)
    ShAAppl "RRE" [] _ -> (ATermTable
att0, SPUserRuleAppl
RRE)
    ShAAppl "SSi" [] _ -> (ATermTable
att0, SPUserRuleAppl
SSi)
    ShAAppl "ClR" [] _ -> (ATermTable
att0, SPUserRuleAppl
ClR)
    ShAAppl "UnC" [] _ -> (ATermTable
att0, SPUserRuleAppl
UnC)
    ShAAppl "Ter" [] _ -> (ATermTable
att0, SPUserRuleAppl
Ter)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPUserRuleAppl)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPUserRuleAppl" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPRuleAppl where
  toShATermAux :: ATermTable -> SPRuleAppl -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPRuleAppl
xv = case SPRuleAppl
xv of
    PRuleTerm a :: SPTerm
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPTerm
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 "PRuleTerm" [Int
a'] []) ATermTable
att1
    PRuleUser a :: SPUserRuleAppl
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPUserRuleAppl -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPUserRuleAppl
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 "PRuleUser" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPRuleAppl)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "PRuleTerm" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, SPTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPTerm
a') ->
      (ATermTable
att1, SPTerm -> SPRuleAppl
PRuleTerm SPTerm
a') }
    ShAAppl "PRuleUser" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, SPUserRuleAppl)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPUserRuleAppl
a') ->
      (ATermTable
att1, SPUserRuleAppl -> SPRuleAppl
PRuleUser SPUserRuleAppl
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPRuleAppl)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPRuleAppl" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPResult where
  toShATermAux :: ATermTable -> SPResult -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPResult
xv = case SPResult
xv of
    PResTerm a :: SPTerm
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPTerm
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 "PResTerm" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPResult)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "PResTerm" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, SPTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPTerm
a') ->
      (ATermTable
att1, SPTerm -> SPResult
PResTerm SPTerm
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPResult)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPResult" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPReference where
  toShATermAux :: ATermTable -> SPReference -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPReference
xv = case SPReference
xv of
    PRefTerm a :: SPTerm
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPTerm
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 "PRefTerm" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPReference)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "PRefTerm" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, SPTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPTerm
a') ->
      (ATermTable
att1, SPTerm -> SPReference
PRefTerm SPTerm
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPReference)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPReference" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPProofStep where
  toShATermAux :: ATermTable -> SPProofStep -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPProofStep
xv = case SPProofStep
xv of
    SPProofStep a :: SPReference
a b :: SPResult
b c :: SPRuleAppl
c d :: [SPParent]
d e :: SPAssocList
e -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPReference -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPReference
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> SPResult -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 SPResult
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> SPRuleAppl -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 SPRuleAppl
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> [SPParent] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 [SPParent]
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> SPAssocList -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 SPAssocList
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 "SPProofStep" [Int
a', Int
b', Int
c', Int
d',
                                                Int
e'] []) ATermTable
att5
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPProofStep)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SPProofStep" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e] _ ->
      case Int -> ATermTable -> (ATermTable, SPReference)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPReference
a') ->
      case Int -> ATermTable -> (ATermTable, SPResult)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: SPResult
b') ->
      case Int -> ATermTable -> (ATermTable, SPRuleAppl)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: SPRuleAppl
c') ->
      case Int -> ATermTable -> (ATermTable, [SPParent])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: [SPParent]
d') ->
      case Int -> ATermTable -> (ATermTable, SPAssocList)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: SPAssocList
e') ->
      (ATermTable
att5, SPReference
-> SPResult
-> SPRuleAppl
-> [SPParent]
-> SPAssocList
-> SPProofStep
SPProofStep SPReference
a' SPResult
b' SPRuleAppl
c' [SPParent]
d' SPAssocList
e') }}}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPProofStep)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPProofStep" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPProofList where
  toShATermAux :: ATermTable -> SPProofList -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPProofList
xv = case SPProofList
xv of
    SPProofList a :: Maybe SPIdentifier
a b :: SPAssocList
b c :: [SPProofStep]
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Maybe SPIdentifier -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Maybe SPIdentifier
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> SPAssocList -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 SPAssocList
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [SPProofStep] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [SPProofStep]
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 "SPProofList" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPProofList)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SPProofList" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, Maybe SPIdentifier)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Maybe SPIdentifier
a') ->
      case Int -> ATermTable -> (ATermTable, SPAssocList)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: SPAssocList
b') ->
      case Int -> ATermTable -> (ATermTable, [SPProofStep])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: [SPProofStep]
c') ->
      (ATermTable
att3, Maybe SPIdentifier -> SPAssocList -> [SPProofStep] -> SPProofList
SPProofList Maybe SPIdentifier
a' SPAssocList
b' [SPProofStep]
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPProofList)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPProofList" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPSymbol where
  toShATermAux :: ATermTable -> SPSymbol -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPSymbol
xv = case SPSymbol
xv of
    SPEqual -> (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 "SPEqual" [] []) ATermTable
att0
    SPTrue -> (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 "SPTrue" [] []) ATermTable
att0
    SPFalse -> (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 "SPFalse" [] []) ATermTable
att0
    SPOr -> (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 "SPOr" [] []) ATermTable
att0
    SPAnd -> (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 "SPAnd" [] []) ATermTable
att0
    SPNot -> (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 "SPNot" [] []) ATermTable
att0
    SPImplies -> (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 "SPImplies" [] []) ATermTable
att0
    SPImplied -> (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 "SPImplied" [] []) ATermTable
att0
    SPEquiv -> (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 "SPEquiv" [] []) ATermTable
att0
    SPID -> (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 "SPID" [] []) ATermTable
att0
    SPDiv -> (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 "SPDiv" [] []) ATermTable
att0
    SPComp -> (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 "SPComp" [] []) ATermTable
att0
    SPSum -> (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 "SPSum" [] []) ATermTable
att0
    SPConv -> (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 "SPConv" [] []) ATermTable
att0
    SPCustomSymbol a :: SPIdentifier
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPIdentifier -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPIdentifier
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 "SPCustomSymbol" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPSymbol)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SPEqual" [] _ -> (ATermTable
att0, SPSymbol
SPEqual)
    ShAAppl "SPTrue" [] _ -> (ATermTable
att0, SPSymbol
SPTrue)
    ShAAppl "SPFalse" [] _ -> (ATermTable
att0, SPSymbol
SPFalse)
    ShAAppl "SPOr" [] _ -> (ATermTable
att0, SPSymbol
SPOr)
    ShAAppl "SPAnd" [] _ -> (ATermTable
att0, SPSymbol
SPAnd)
    ShAAppl "SPNot" [] _ -> (ATermTable
att0, SPSymbol
SPNot)
    ShAAppl "SPImplies" [] _ -> (ATermTable
att0, SPSymbol
SPImplies)
    ShAAppl "SPImplied" [] _ -> (ATermTable
att0, SPSymbol
SPImplied)
    ShAAppl "SPEquiv" [] _ -> (ATermTable
att0, SPSymbol
SPEquiv)
    ShAAppl "SPID" [] _ -> (ATermTable
att0, SPSymbol
SPID)
    ShAAppl "SPDiv" [] _ -> (ATermTable
att0, SPSymbol
SPDiv)
    ShAAppl "SPComp" [] _ -> (ATermTable
att0, SPSymbol
SPComp)
    ShAAppl "SPSum" [] _ -> (ATermTable
att0, SPSymbol
SPSum)
    ShAAppl "SPConv" [] _ -> (ATermTable
att0, SPSymbol
SPConv)
    ShAAppl "SPCustomSymbol" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, SPIdentifier)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPIdentifier
a') ->
      (ATermTable
att1, SPIdentifier -> SPSymbol
SPCustomSymbol SPIdentifier
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPSymbol)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPSymbol" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPQuantSym where
  toShATermAux :: ATermTable -> SPQuantSym -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPQuantSym
xv = case SPQuantSym
xv of
    SPForall -> (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 "SPForall" [] []) ATermTable
att0
    SPExists -> (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 "SPExists" [] []) ATermTable
att0
    SPCustomQuantSym a :: SPIdentifier
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPIdentifier -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPIdentifier
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 "SPCustomQuantSym" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPQuantSym)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SPForall" [] _ -> (ATermTable
att0, SPQuantSym
SPForall)
    ShAAppl "SPExists" [] _ -> (ATermTable
att0, SPQuantSym
SPExists)
    ShAAppl "SPCustomQuantSym" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, SPIdentifier)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPIdentifier
a') ->
      (ATermTable
att1, SPIdentifier -> SPQuantSym
SPCustomQuantSym SPIdentifier
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPQuantSym)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPQuantSym" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPLiteral where
  toShATermAux :: ATermTable -> SPLiteral -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPLiteral
xv = case SPLiteral
xv of
    SPLiteral a :: Bool
a b :: SPSymbol
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Bool
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> SPSymbol -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 SPSymbol
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 "SPLiteral" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPLiteral)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SPLiteral" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Bool
a') ->
      case Int -> ATermTable -> (ATermTable, SPSymbol)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: SPSymbol
b') ->
      (ATermTable
att2, Bool -> SPSymbol -> SPLiteral
SPLiteral Bool
a' SPSymbol
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPLiteral)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPLiteral" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.TPTP where
  toShATermAux :: ATermTable -> TPTP -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TPTP
xv = case TPTP
xv of
    FormAnno a :: FormKind
a b :: Name
b c :: Role
c d :: SPTerm
d e :: Maybe Annos
e -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> FormKind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 FormKind
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Name -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Name
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> Role -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 Role
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> SPTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 SPTerm
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> Maybe Annos -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 Maybe Annos
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 "FormAnno" [Int
a', Int
b', Int
c', Int
d', Int
e'] []) ATermTable
att5
    Include a :: FileName
a b :: [Name]
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> FileName -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 FileName
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [Name] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [Name]
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 "Include" [Int
a', Int
b'] []) ATermTable
att2
    CommentLine a :: String
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' 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 "CommentLine" [Int
a'] []) ATermTable
att1
    EmptyLine -> (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 "EmptyLine" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, TPTP)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "FormAnno" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e] _ ->
      case Int -> ATermTable -> (ATermTable, FormKind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: FormKind
a') ->
      case Int -> ATermTable -> (ATermTable, Name)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Name
b') ->
      case Int -> ATermTable -> (ATermTable, Role)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: Role
c') ->
      case Int -> ATermTable -> (ATermTable, SPTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: SPTerm
d') ->
      case Int -> ATermTable -> (ATermTable, Maybe Annos)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: Maybe Annos
e') ->
      (ATermTable
att5, FormKind -> Name -> Role -> SPTerm -> Maybe Annos -> TPTP
FormAnno FormKind
a' Name
b' Role
c' SPTerm
d' Maybe Annos
e') }}}}}
    ShAAppl "Include" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, FileName)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: FileName
a') ->
      case Int -> ATermTable -> (ATermTable, [Name])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [Name]
b') ->
      (ATermTable
att2, FileName -> [Name] -> TPTP
Include FileName
a' [Name]
b') }}
    ShAAppl "CommentLine" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: String
a') ->
      (ATermTable
att1, String -> TPTP
CommentLine String
a') }
    ShAAppl "EmptyLine" [] _ -> (ATermTable
att0, TPTP
EmptyLine)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TPTP)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.TPTP" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.Info where
  toShATermAux :: ATermTable -> Info -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Info
xv = case Info
xv of
    Info a :: [GenTerm]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [GenTerm] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [GenTerm]
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 "Info" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, Info)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Info" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, [GenTerm])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [GenTerm]
a') ->
      (ATermTable
att1, [GenTerm] -> Info
Info [GenTerm]
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Info)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.Info" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.FormData where
  toShATermAux :: ATermTable -> FormData -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: FormData
xv = case FormData
xv of
    FormData a :: FormKind
a b :: SPTerm
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> FormKind -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 FormKind
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> SPTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 SPTerm
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 "FormData" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, FormData)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "FormData" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, FormKind)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: FormKind
a') ->
      case Int -> ATermTable -> (ATermTable, SPTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: SPTerm
b') ->
      (ATermTable
att2, FormKind -> SPTerm -> FormData
FormData FormKind
a' SPTerm
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, FormData)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.FormData" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.GenData where
  toShATermAux :: ATermTable -> GenData -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: GenData
xv = case GenData
xv of
    GenData a :: AWord
a b :: [GenTerm]
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> AWord -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 AWord
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [GenTerm] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [GenTerm]
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 "GenData" [Int
a', Int
b'] []) ATermTable
att2
    OtherGenData a :: String
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' 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 "OtherGenData" [Int
a'] []) ATermTable
att1
    GenFormData a :: FormData
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> FormData -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 FormData
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 "GenFormData" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, GenData)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "GenData" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, AWord)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: AWord
a') ->
      case Int -> ATermTable -> (ATermTable, [GenTerm])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [GenTerm]
b') ->
      (ATermTable
att2, AWord -> [GenTerm] -> GenData
GenData AWord
a' [GenTerm]
b') }}
    ShAAppl "OtherGenData" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: String
a') ->
      (ATermTable
att1, String -> GenData
OtherGenData String
a') }
    ShAAppl "GenFormData" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, FormData)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: FormData
a') ->
      (ATermTable
att1, FormData -> GenData
GenFormData FormData
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, GenData)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.GenData" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.GenTerm where
  toShATermAux :: ATermTable -> GenTerm -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: GenTerm
xv = case GenTerm
xv of
    GenTerm a :: GenData
a b :: Maybe GenTerm
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> GenData -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 GenData
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Maybe GenTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Maybe GenTerm
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 "GenTerm" [Int
a', Int
b'] []) ATermTable
att2
    GenTermList a :: [GenTerm]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [GenTerm] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [GenTerm]
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 "GenTermList" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, GenTerm)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "GenTerm" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, GenData)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: GenData
a') ->
      case Int -> ATermTable -> (ATermTable, Maybe GenTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Maybe GenTerm
b') ->
      (ATermTable
att2, GenData -> Maybe GenTerm -> GenTerm
GenTerm GenData
a' Maybe GenTerm
b') }}
    ShAAppl "GenTermList" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, [GenTerm])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [GenTerm]
a') ->
      (ATermTable
att1, [GenTerm] -> GenTerm
GenTermList [GenTerm]
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, GenTerm)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.GenTerm" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.AWord where
  toShATermAux :: ATermTable -> AWord -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: AWord
xv = case AWord
xv of
    AWord a :: String
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' 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 "AWord" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, AWord)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "AWord" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: String
a') ->
      (ATermTable
att1, String -> AWord
AWord String
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, AWord)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.AWord" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.Source where
  toShATermAux :: ATermTable -> Source -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Source
xv = case Source
xv of
    Source a :: GenTerm
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> GenTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 GenTerm
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 "Source" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, Source)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Source" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, GenTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: GenTerm
a') ->
      (ATermTable
att1, GenTerm -> Source
Source GenTerm
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Source)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.Source" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.Annos where
  toShATermAux :: ATermTable -> Annos -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Annos
xv = case Annos
xv of
    Annos a :: Source
a b :: Maybe Info
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Source -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Source
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Maybe Info -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Maybe Info
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 "Annos" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, Annos)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Annos" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, Source)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Source
a') ->
      case Int -> ATermTable -> (ATermTable, Maybe Info)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Maybe Info
b') ->
      (ATermTable
att2, Source -> Maybe Info -> Annos
Annos Source
a' Maybe Info
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Annos)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.Annos" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.Name where
  toShATermAux :: ATermTable -> Name -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Name
xv = case Name
xv of
    Name a :: String
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' 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 "Name" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, Name)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Name" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: String
a') ->
      (ATermTable
att1, String -> Name
Name String
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Name)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.Name" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.Role where
  toShATermAux :: ATermTable -> Role -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Role
xv = case Role
xv of
    Axiom -> (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 "Axiom" [] []) ATermTable
att0
    Hypothesis -> (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 "Hypothesis" [] []) ATermTable
att0
    Definition -> (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 "Definition" [] []) ATermTable
att0
    Assumption -> (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 "Assumption" [] []) ATermTable
att0
    Lemma -> (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 "Lemma" [] []) ATermTable
att0
    Theorem -> (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 "Theorem" [] []) ATermTable
att0
    Conjecture -> (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 "Conjecture" [] []) ATermTable
att0
    Negated_conjecture ->
      (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 "Negated_conjecture" [] []) ATermTable
att0
    Plain -> (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 "Plain" [] []) ATermTable
att0
    Fi_domain -> (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 "Fi_domain" [] []) ATermTable
att0
    Fi_functors -> (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 "Fi_functors" [] []) ATermTable
att0
    Fi_predicates -> (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 "Fi_predicates" [] []) ATermTable
att0
    Type -> (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 "Type" [] []) ATermTable
att0
    Unknown -> (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 "Unknown" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, Role)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Axiom" [] _ -> (ATermTable
att0, Role
Axiom)
    ShAAppl "Hypothesis" [] _ -> (ATermTable
att0, Role
Hypothesis)
    ShAAppl "Definition" [] _ -> (ATermTable
att0, Role
Definition)
    ShAAppl "Assumption" [] _ -> (ATermTable
att0, Role
Assumption)
    ShAAppl "Lemma" [] _ -> (ATermTable
att0, Role
Lemma)
    ShAAppl "Theorem" [] _ -> (ATermTable
att0, Role
Theorem)
    ShAAppl "Conjecture" [] _ -> (ATermTable
att0, Role
Conjecture)
    ShAAppl "Negated_conjecture" [] _ -> (ATermTable
att0, Role
Negated_conjecture)
    ShAAppl "Plain" [] _ -> (ATermTable
att0, Role
Plain)
    ShAAppl "Fi_domain" [] _ -> (ATermTable
att0, Role
Fi_domain)
    ShAAppl "Fi_functors" [] _ -> (ATermTable
att0, Role
Fi_functors)
    ShAAppl "Fi_predicates" [] _ -> (ATermTable
att0, Role
Fi_predicates)
    ShAAppl "Type" [] _ -> (ATermTable
att0, Role
Type)
    ShAAppl "Unknown" [] _ -> (ATermTable
att0, Role
Unknown)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Role)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.Role" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.FormKind where
  toShATermAux :: ATermTable -> FormKind -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: FormKind
xv = case FormKind
xv of
    FofKind -> (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 "FofKind" [] []) ATermTable
att0
    CnfKind -> (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 "CnfKind" [] []) ATermTable
att0
    FotKind -> (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 "FotKind" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, FormKind)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "FofKind" [] _ -> (ATermTable
att0, FormKind
FofKind)
    ShAAppl "CnfKind" [] _ -> (ATermTable
att0, FormKind
CnfKind)
    ShAAppl "FotKind" [] _ -> (ATermTable
att0, FormKind
FotKind)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, FormKind)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.FormKind" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.FileName where
  toShATermAux :: ATermTable -> FileName -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: FileName
xv = case FileName
xv of
    FileName a :: String
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' 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 "FileName" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, FileName)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "FileName" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: String
a') ->
      (ATermTable
att1, String -> FileName
FileName String
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, FileName)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.FileName" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPTerm where
  toShATermAux :: ATermTable -> SPTerm -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPTerm
xv = case SPTerm
xv of
    SPQuantTerm a :: SPQuantSym
a b :: [SPTerm]
b c :: SPTerm
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPQuantSym -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPQuantSym
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [SPTerm] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [SPTerm]
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> SPTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 SPTerm
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 "SPQuantTerm" [Int
a', Int
b', Int
c'] []) ATermTable
att3
    SPComplexTerm a :: SPSymbol
a b :: [SPTerm]
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPSymbol -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPSymbol
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [SPTerm] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [SPTerm]
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 "SPComplexTerm" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPTerm)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SPQuantTerm" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, SPQuantSym)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPQuantSym
a') ->
      case Int -> ATermTable -> (ATermTable, [SPTerm])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [SPTerm]
b') ->
      case Int -> ATermTable -> (ATermTable, SPTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: SPTerm
c') ->
      (ATermTable
att3, SPQuantSym -> [SPTerm] -> SPTerm -> SPTerm
SPQuantTerm SPQuantSym
a' [SPTerm]
b' SPTerm
c') }}}
    ShAAppl "SPComplexTerm" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, SPSymbol)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPSymbol
a') ->
      case Int -> ATermTable -> (ATermTable, [SPTerm])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [SPTerm]
b') ->
      (ATermTable
att2, SPSymbol -> [SPTerm] -> SPTerm
SPComplexTerm SPSymbol
a' [SPTerm]
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPTerm)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPTerm" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.TermWsList where
  toShATermAux :: ATermTable -> TermWsList -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TermWsList
xv = case TermWsList
xv of
    TWL a :: [SPTerm]
a b :: Bool
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [SPTerm] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [SPTerm]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' 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 "TWL" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, TermWsList)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "TWL" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [SPTerm])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [SPTerm]
a') ->
      case Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Bool
b') ->
      (ATermTable
att2, [SPTerm] -> Bool -> TermWsList
TWL [SPTerm]
a' Bool
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TermWsList)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.TermWsList" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.NSPClauseBody where
  toShATermAux :: ATermTable -> NSPClauseBody -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: NSPClauseBody
xv = case NSPClauseBody
xv of
    NSPClauseBody a :: SPClauseType
a b :: [SPLiteral]
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPClauseType -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPClauseType
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [SPLiteral] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [SPLiteral]
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 "NSPClauseBody" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, NSPClauseBody)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "NSPClauseBody" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, SPClauseType)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPClauseType
a') ->
      case Int -> ATermTable -> (ATermTable, [SPLiteral])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [SPLiteral]
b') ->
      (ATermTable
att2, SPClauseType -> [SPLiteral] -> NSPClauseBody
NSPClauseBody SPClauseType
a' [SPLiteral]
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, NSPClauseBody)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.NSPClauseBody" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.NSPClause where
  toShATermAux :: ATermTable -> NSPClause -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: NSPClause
xv = case NSPClause
xv of
    QuanClause a :: [SPTerm]
a b :: NSPClauseBody
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [SPTerm] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [SPTerm]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> NSPClauseBody -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 NSPClauseBody
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 "QuanClause" [Int
a', Int
b'] []) ATermTable
att2
    SimpleClause a :: NSPClauseBody
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> NSPClauseBody -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 NSPClauseBody
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 "SimpleClause" [Int
a'] []) ATermTable
att1
    BriefClause a :: TermWsList
a b :: TermWsList
b c :: TermWsList
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TermWsList -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TermWsList
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> TermWsList -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 TermWsList
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> TermWsList -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 TermWsList
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 "BriefClause" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  fromShATermAux :: Int -> ATermTable -> (ATermTable, NSPClause)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "QuanClause" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [SPTerm])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [SPTerm]
a') ->
      case Int -> ATermTable -> (ATermTable, NSPClauseBody)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: NSPClauseBody
b') ->
      (ATermTable
att2, [SPTerm] -> NSPClauseBody -> NSPClause
QuanClause [SPTerm]
a' NSPClauseBody
b') }}
    ShAAppl "SimpleClause" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, NSPClauseBody)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: NSPClauseBody
a') ->
      (ATermTable
att1, NSPClauseBody -> NSPClause
SimpleClause NSPClauseBody
a') }
    ShAAppl "BriefClause" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, TermWsList)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: TermWsList
a') ->
      case Int -> ATermTable -> (ATermTable, TermWsList)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: TermWsList
b') ->
      case Int -> ATermTable -> (ATermTable, TermWsList)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: TermWsList
c') ->
      (ATermTable
att3, TermWsList -> TermWsList -> TermWsList -> NSPClause
BriefClause TermWsList
a' TermWsList
b' TermWsList
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, NSPClause)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.NSPClause" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPClauseType where
  toShATermAux :: ATermTable -> SPClauseType -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPClauseType
xv = case SPClauseType
xv of
    SPCNF -> (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 "SPCNF" [] []) ATermTable
att0
    SPDNF -> (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 "SPDNF" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPClauseType)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SPCNF" [] _ -> (ATermTable
att0, SPClauseType
SPCNF)
    ShAAppl "SPDNF" [] _ -> (ATermTable
att0, SPClauseType
SPDNF)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPClauseType)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPClauseType" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPOriginType where
  toShATermAux :: ATermTable -> SPOriginType -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPOriginType
xv = case SPOriginType
xv of
    SPOriginAxioms -> (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 "SPOriginAxioms" [] []) ATermTable
att0
    SPOriginConjectures ->
      (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 "SPOriginConjectures" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPOriginType)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SPOriginAxioms" [] _ -> (ATermTable
att0, SPOriginType
SPOriginAxioms)
    ShAAppl "SPOriginConjectures" [] _ -> (ATermTable
att0, SPOriginType
SPOriginConjectures)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPOriginType)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPOriginType" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPClauseList where
  toShATermAux :: ATermTable -> SPClauseList -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPClauseList
xv = case SPClauseList
xv of
    SPClauseList a :: SPOriginType
a b :: SPClauseType
b c :: [SPClause]
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPOriginType -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPOriginType
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> SPClauseType -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 SPClauseType
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [SPClause] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [SPClause]
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 "SPClauseList" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPClauseList)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SPClauseList" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, SPOriginType)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPOriginType
a') ->
      case Int -> ATermTable -> (ATermTable, SPClauseType)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: SPClauseType
b') ->
      case Int -> ATermTable -> (ATermTable, [SPClause])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: [SPClause]
c') ->
      (ATermTable
att3, SPOriginType -> SPClauseType -> [SPClause] -> SPClauseList
SPClauseList SPOriginType
a' SPClauseType
b' [SPClause]
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPClauseList)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPClauseList" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPFormulaList where
  toShATermAux :: ATermTable -> SPFormulaList -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPFormulaList
xv = case SPFormulaList
xv of
    SPFormulaList a :: SPOriginType
a b :: [SPFormula]
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPOriginType -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPOriginType
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [SPFormula] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [SPFormula]
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 "SPFormulaList" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPFormulaList)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SPFormulaList" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, SPOriginType)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPOriginType
a') ->
      case Int -> ATermTable -> (ATermTable, [SPFormula])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [SPFormula]
b') ->
      (ATermTable
att2, SPOriginType -> [SPFormula] -> SPFormulaList
SPFormulaList SPOriginType
a' [SPFormula]
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPFormulaList)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPFormulaList" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPDeclaration where
  toShATermAux :: ATermTable -> SPDeclaration -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPDeclaration
xv = case SPDeclaration
xv of
    SPSubsortDecl a :: SPIdentifier
a b :: SPIdentifier
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPIdentifier -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPIdentifier
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> SPIdentifier -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 SPIdentifier
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 "SPSubsortDecl" [Int
a', Int
b'] []) ATermTable
att2
    SPTermDecl a :: [SPTerm]
a b :: SPTerm
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [SPTerm] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [SPTerm]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> SPTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 SPTerm
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 "SPTermDecl" [Int
a', Int
b'] []) ATermTable
att2
    SPSimpleTermDecl a :: SPTerm
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPTerm
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 "SPSimpleTermDecl" [Int
a'] []) ATermTable
att1
    SPPredDecl a :: SPIdentifier
a b :: [SPIdentifier]
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPIdentifier -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPIdentifier
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [SPIdentifier] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [SPIdentifier]
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 "SPPredDecl" [Int
a', Int
b'] []) ATermTable
att2
    SPGenDecl a :: SPIdentifier
a b :: Bool
b c :: [SPIdentifier]
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPIdentifier -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPIdentifier
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Bool
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [SPIdentifier] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [SPIdentifier]
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 "SPGenDecl" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPDeclaration)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SPSubsortDecl" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, SPIdentifier)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPIdentifier
a') ->
      case Int -> ATermTable -> (ATermTable, SPIdentifier)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: SPIdentifier
b') ->
      (ATermTable
att2, SPIdentifier -> SPIdentifier -> SPDeclaration
SPSubsortDecl SPIdentifier
a' SPIdentifier
b') }}
    ShAAppl "SPTermDecl" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [SPTerm])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [SPTerm]
a') ->
      case Int -> ATermTable -> (ATermTable, SPTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: SPTerm
b') ->
      (ATermTable
att2, [SPTerm] -> SPTerm -> SPDeclaration
SPTermDecl [SPTerm]
a' SPTerm
b') }}
    ShAAppl "SPSimpleTermDecl" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, SPTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPTerm
a') ->
      (ATermTable
att1, SPTerm -> SPDeclaration
SPSimpleTermDecl SPTerm
a') }
    ShAAppl "SPPredDecl" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, SPIdentifier)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPIdentifier
a') ->
      case Int -> ATermTable -> (ATermTable, [SPIdentifier])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [SPIdentifier]
b') ->
      (ATermTable
att2, SPIdentifier -> [SPIdentifier] -> SPDeclaration
SPPredDecl SPIdentifier
a' [SPIdentifier]
b') }}
    ShAAppl "SPGenDecl" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, SPIdentifier)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPIdentifier
a') ->
      case Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Bool
b') ->
      case Int -> ATermTable -> (ATermTable, [SPIdentifier])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: [SPIdentifier]
c') ->
      (ATermTable
att3, SPIdentifier -> Bool -> [SPIdentifier] -> SPDeclaration
SPGenDecl SPIdentifier
a' Bool
b' [SPIdentifier]
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPDeclaration)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPDeclaration" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPSortSym where
  toShATermAux :: ATermTable -> SPSortSym -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPSortSym
xv = case SPSortSym
xv of
    SPSortSym a :: SPIdentifier
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPIdentifier -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPIdentifier
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 "SPSortSym" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPSortSym)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SPSortSym" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, SPIdentifier)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPIdentifier
a') ->
      (ATermTable
att1, SPIdentifier -> SPSortSym
SPSortSym SPIdentifier
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPSortSym)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPSortSym" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPSignSym where
  toShATermAux :: ATermTable -> SPSignSym -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPSignSym
xv = case SPSignSym
xv of
    SPSignSym a :: SPIdentifier
a b :: Int
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPIdentifier -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPIdentifier
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Int -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' 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 "SPSignSym" [Int
a', Int
b'] []) ATermTable
att2
    SPSimpleSignSym a :: SPIdentifier
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPIdentifier -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPIdentifier
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 "SPSimpleSignSym" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPSignSym)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SPSignSym" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, SPIdentifier)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPIdentifier
a') ->
      case Int -> ATermTable -> (ATermTable, Int)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Int
b') ->
      (ATermTable
att2, SPIdentifier -> Int -> SPSignSym
SPSignSym SPIdentifier
a' Int
b') }}
    ShAAppl "SPSimpleSignSym" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, SPIdentifier)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPIdentifier
a') ->
      (ATermTable
att1, SPIdentifier -> SPSignSym
SPSimpleSignSym SPIdentifier
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPSignSym)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPSignSym" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPSymbolList where
  toShATermAux :: ATermTable -> SPSymbolList -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPSymbolList
xv = case SPSymbolList
xv of
    SPSymbolList a :: [SPSignSym]
a b :: [SPSignSym]
b c :: [SPSignSym]
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [SPSignSym] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [SPSignSym]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [SPSignSym] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [SPSignSym]
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [SPSignSym] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [SPSignSym]
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 "SPSymbolList" [Int
a', Int
b', Int
c'] []) ATermTable
att3
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPSymbolList)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SPSymbolList" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, [SPSignSym])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [SPSignSym]
a') ->
      case Int -> ATermTable -> (ATermTable, [SPSignSym])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [SPSignSym]
b') ->
      case Int -> ATermTable -> (ATermTable, [SPSignSym])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: [SPSignSym]
c') ->
      (ATermTable
att3, [SPSignSym] -> [SPSignSym] -> [SPSignSym] -> SPSymbolList
SPSymbolList [SPSignSym]
a' [SPSignSym]
b' [SPSignSym]
c') }}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPSymbolList)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPSymbolList" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPLogicalPart where
  toShATermAux :: ATermTable -> SPLogicalPart -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPLogicalPart
xv = case SPLogicalPart
xv of
    SPLogicalPart a :: Maybe SPSymbolList
a b :: Maybe [SPDeclaration]
b c :: [SPFormulaList]
c d :: [SPClauseList]
d e :: [SPProofList]
e -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Maybe SPSymbolList -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Maybe SPSymbolList
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> Maybe [SPDeclaration] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Maybe [SPDeclaration]
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> [SPFormulaList] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 [SPFormulaList]
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> [SPClauseList] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 [SPClauseList]
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> [SPProofList] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att4 [SPProofList]
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 "SPLogicalPart" [Int
a', Int
b', Int
c', Int
d',
                                                  Int
e'] []) ATermTable
att5
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPLogicalPart)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SPLogicalPart" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e] _ ->
      case Int -> ATermTable -> (ATermTable, Maybe SPSymbolList)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Maybe SPSymbolList
a') ->
      case Int -> ATermTable -> (ATermTable, Maybe [SPDeclaration])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: Maybe [SPDeclaration]
b') ->
      case Int -> ATermTable -> (ATermTable, [SPFormulaList])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: [SPFormulaList]
c') ->
      case Int -> ATermTable -> (ATermTable, [SPClauseList])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: [SPClauseList]
d') ->
      case Int -> ATermTable -> (ATermTable, [SPProofList])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: [SPProofList]
e') ->
      (ATermTable
att5, Maybe SPSymbolList
-> Maybe [SPDeclaration]
-> [SPFormulaList]
-> [SPClauseList]
-> [SPProofList]
-> SPLogicalPart
SPLogicalPart Maybe SPSymbolList
a' Maybe [SPDeclaration]
b' [SPFormulaList]
c' [SPClauseList]
d' [SPProofList]
e') }}}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPLogicalPart)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPLogicalPart" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SPProblem where
  toShATermAux :: ATermTable -> SPProblem -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SPProblem
xv = case SPProblem
xv of
    SPProblem a :: String
a b :: SPDescription
b c :: SPLogicalPart
c d :: [SPSetting]
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> String -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 String
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> SPDescription -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 SPDescription
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> SPLogicalPart -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 SPLogicalPart
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> [SPSetting] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 [SPSetting]
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 "SPProblem" [Int
a', Int
b', Int
c', Int
d'] []) ATermTable
att4
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SPProblem)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SPProblem" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, String)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: String
a') ->
      case Int -> ATermTable -> (ATermTable, SPDescription)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: SPDescription
b') ->
      case Int -> ATermTable -> (ATermTable, SPLogicalPart)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: SPLogicalPart
c') ->
      case Int -> ATermTable -> (ATermTable, [SPSetting])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: [SPSetting]
d') ->
      (ATermTable
att4, String
-> SPDescription -> SPLogicalPart -> [SPSetting] -> SPProblem
SPProblem String
a' SPDescription
b' SPLogicalPart
c' [SPSetting]
d') }}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SPProblem)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SPProblem" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SFSymbType where
  toShATermAux :: ATermTable -> SFSymbType -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SFSymbType
xv = case SFSymbType
xv of
    SFOpType a :: [SPIdentifier]
a b :: SPIdentifier
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [SPIdentifier] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [SPIdentifier]
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> SPIdentifier -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 SPIdentifier
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 "SFOpType" [Int
a', Int
b'] []) ATermTable
att2
    SFPredType a :: [SPIdentifier]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [SPIdentifier] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [SPIdentifier]
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 "SFPredType" [Int
a'] []) ATermTable
att1
    SFSortType -> (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 "SFSortType" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SFSymbType)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SFOpType" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, [SPIdentifier])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [SPIdentifier]
a') ->
      case Int -> ATermTable -> (ATermTable, SPIdentifier)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: SPIdentifier
b') ->
      (ATermTable
att2, [SPIdentifier] -> SPIdentifier -> SFSymbType
SFOpType [SPIdentifier]
a' SPIdentifier
b') }}
    ShAAppl "SFPredType" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, [SPIdentifier])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [SPIdentifier]
a') ->
      (ATermTable
att1, [SPIdentifier] -> SFSymbType
SFPredType [SPIdentifier]
a') }
    ShAAppl "SFSortType" [] _ -> (ATermTable
att0, SFSymbType
SFSortType)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SFSymbType)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SFSymbType" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.SFSymbol where
  toShATermAux :: ATermTable -> SFSymbol -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: SFSymbol
xv = case SFSymbol
xv of
    SFSymbol a :: SPIdentifier
a b :: SFSymbType
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SPIdentifier -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SPIdentifier
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> SFSymbType -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 SFSymbType
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 "SFSymbol" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SFSymbol)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SFSymbol" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, SPIdentifier)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SPIdentifier
a') ->
      case Int -> ATermTable -> (ATermTable, SFSymbType)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: SFSymbType
b') ->
      (ATermTable
att2, SPIdentifier -> SFSymbType -> SFSymbol
SFSymbol SPIdentifier
a' SFSymbType
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SFSymbol)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.SFSymbol" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.Generated where
  toShATermAux :: ATermTable -> Generated -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Generated
xv = case Generated
xv of
    Generated a :: Bool
a b :: [SPIdentifier]
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Bool
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [SPIdentifier] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [SPIdentifier]
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 "Generated" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, Generated)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Generated" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Bool
a') ->
      case Int -> ATermTable -> (ATermTable, [SPIdentifier])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: [SPIdentifier]
b') ->
      (ATermTable
att2, Bool -> [SPIdentifier] -> Generated
Generated Bool
a' [SPIdentifier]
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Generated)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.Generated" ShATerm
u

instance ShATermConvertible SoftFOL.Sign.Sign where
  toShATermAux :: ATermTable -> Sign -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Sign
xv = case Sign
xv of
    Sign a :: Rel SPIdentifier
a b :: SortMap
b c :: FuncMap
c d :: PredMap
d e :: Bool
e -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Rel SPIdentifier -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Rel SPIdentifier
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> SortMap -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 SortMap
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> FuncMap -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 FuncMap
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> PredMap -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 PredMap
d
      (att5 :: ATermTable
att5, e' :: Int
e') <- ATermTable -> Bool -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' 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 "Sign" [Int
a', Int
b', Int
c', Int
d', Int
e'] []) ATermTable
att5
  fromShATermAux :: Int -> ATermTable -> (ATermTable, Sign)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Sign" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d, e :: Int
e] _ ->
      case Int -> ATermTable -> (ATermTable, Rel SPIdentifier)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Rel SPIdentifier
a') ->
      case Int -> ATermTable -> (ATermTable, SortMap)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: SortMap
b') ->
      case Int -> ATermTable -> (ATermTable, FuncMap)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: FuncMap
c') ->
      case Int -> ATermTable -> (ATermTable, PredMap)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: PredMap
d') ->
      case Int -> ATermTable -> (ATermTable, Bool)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
e ATermTable
att4 of
      { (att5 :: ATermTable
att5, e' :: Bool
e') ->
      (ATermTable
att5, Rel SPIdentifier -> SortMap -> FuncMap -> PredMap -> Bool -> Sign
Sign Rel SPIdentifier
a' SortMap
b' FuncMap
c' PredMap
d' Bool
e') }}}}}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Sign)
forall a. String -> ShATerm -> a
fromShATermError "SoftFOL.Sign.Sign" ShATerm
u