{-# OPTIONS -w -O0 #-}
{-# LANGUAGE CPP, StandaloneDeriving, DeriveDataTypeable, DeriveGeneric #-}
{- |
Module      :  THF/ATC_THF.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):
'THF.As.TPTP_THF'
'THF.As.Comment'
'THF.As.DefinedComment'
'THF.As.SystemComment'
'THF.As.Include'
'THF.As.Annotations'
'THF.As.FormulaRole'
'THF.As.THFFormula'
'THF.As.THFLogicFormula'
'THF.As.THFBinaryFormula'
'THF.As.THFBinaryTuple'
'THF.As.THFUnitaryFormula'
'THF.As.THFQuantifiedFormula'
'THF.As.THFVariable'
'THF.As.THFTypedConst'
'THF.As.THFTypeFormula'
'THF.As.THFTypeableFormula'
'THF.As.THFSubType'
'THF.As.THFTopLevelType'
'THF.As.THFUnitaryType'
'THF.As.THFBinaryType'
'THF.As.THFAtom'
'THF.As.THFSequent'
'THF.As.THFConnTerm'
'THF.As.THFQuantifier'
'THF.As.Quantifier'
'THF.As.THFPairConnective'
'THF.As.THFUnaryConnective'
'THF.As.AssocConnective'
'THF.As.DefinedType'
'THF.As.DefinedPlainFormula'
'THF.As.DefinedProp'
'THF.As.DefinedPred'
'THF.As.Term'
'THF.As.FunctionTerm'
'THF.As.PlainTerm'
'THF.As.DefinedTerm'
'THF.As.DefinedAtom'
'THF.As.DefinedPlainTerm'
'THF.As.DefinedFunctor'
'THF.As.SystemTerm'
'THF.As.PrincipalSymbol'
'THF.As.Source'
'THF.As.DagSource'
'THF.As.ParentInfo'
'THF.As.IntroType'
'THF.As.ExternalSource'
'THF.As.FileSource'
'THF.As.TheoryName'
'THF.As.InfoItem'
'THF.As.FormulaItem'
'THF.As.InferenceItem'
'THF.As.InferenceStatus'
'THF.As.StatusValue'
'THF.As.GeneralTerm'
'THF.As.GeneralData'
'THF.As.GeneralFunction'
'THF.As.FormulaData'
'THF.As.Name'
'THF.As.AtomicWord'
'THF.As.Number'
'THF.Cons.BasicSpecTHF'
'THF.Cons.SymbolTHF'
'THF.Cons.SymbolType'
'THF.Cons.Type'
'THF.Cons.Kind'
'THF.Sign.SignTHF'
'THF.Sign.TypeInfo'
'THF.Sign.ConstInfo'
'THF.Sublogic.THFCoreSl'
'THF.Sublogic.THFSl'
-}

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

module THF.ATC_THF () where

import ATC.GlobalAnnotations
import ATC.Id
import ATerm.Lib
import Common.DefaultMorphism
import Common.Id
import Common.Id hiding (typeId)
import Common.Json.Instances
import Common.Result
import Data.Aeson(ToJSON, FromJSON)
import Data.Data
import GHC.Generics(Generic)
import Logic.Logic
import THF.As
import THF.Cons
import THF.Sign
import THF.Sublogic
import qualified Data.Map as Map

{-! for THF.As.TPTP_THF derive : ShATermConvertible !-}
{-! for THF.As.Comment derive : ShATermConvertible !-}
{-! for THF.As.DefinedComment derive : ShATermConvertible !-}
{-! for THF.As.SystemComment derive : ShATermConvertible !-}
{-! for THF.As.Include derive : ShATermConvertible !-}
{-! for THF.As.Annotations derive : ShATermConvertible !-}
{-! for THF.As.FormulaRole derive : ShATermConvertible !-}
{-! for THF.As.THFFormula derive : ShATermConvertible !-}
{-! for THF.As.THFLogicFormula derive : ShATermConvertible !-}
{-! for THF.As.THFBinaryFormula derive : ShATermConvertible !-}
{-! for THF.As.THFBinaryTuple derive : ShATermConvertible !-}
{-! for THF.As.THFUnitaryFormula derive : ShATermConvertible !-}
{-! for THF.As.THFQuantifiedFormula derive : ShATermConvertible !-}
{-! for THF.As.THFVariable derive : ShATermConvertible !-}
{-! for THF.As.THFTypedConst derive : ShATermConvertible !-}
{-! for THF.As.THFTypeFormula derive : ShATermConvertible !-}
{-! for THF.As.THFTypeableFormula derive : ShATermConvertible !-}
{-! for THF.As.THFSubType derive : ShATermConvertible !-}
{-! for THF.As.THFTopLevelType derive : ShATermConvertible !-}
{-! for THF.As.THFUnitaryType derive : ShATermConvertible !-}
{-! for THF.As.THFBinaryType derive : ShATermConvertible !-}
{-! for THF.As.THFAtom derive : ShATermConvertible !-}
{-! for THF.As.THFSequent derive : ShATermConvertible !-}
{-! for THF.As.THFConnTerm derive : ShATermConvertible !-}
{-! for THF.As.THFQuantifier derive : ShATermConvertible !-}
{-! for THF.As.Quantifier derive : ShATermConvertible !-}
{-! for THF.As.THFPairConnective derive : ShATermConvertible !-}
{-! for THF.As.THFUnaryConnective derive : ShATermConvertible !-}
{-! for THF.As.AssocConnective derive : ShATermConvertible !-}
{-! for THF.As.DefinedType derive : ShATermConvertible !-}
{-! for THF.As.DefinedPlainFormula derive : ShATermConvertible !-}
{-! for THF.As.DefinedProp derive : ShATermConvertible !-}
{-! for THF.As.DefinedPred derive : ShATermConvertible !-}
{-! for THF.As.Term derive : ShATermConvertible !-}
{-! for THF.As.FunctionTerm derive : ShATermConvertible !-}
{-! for THF.As.PlainTerm derive : ShATermConvertible !-}
{-! for THF.As.DefinedTerm derive : ShATermConvertible !-}
{-! for THF.As.DefinedAtom derive : ShATermConvertible !-}
{-! for THF.As.DefinedPlainTerm derive : ShATermConvertible !-}
{-! for THF.As.DefinedFunctor derive : ShATermConvertible !-}
{-! for THF.As.SystemTerm derive : ShATermConvertible !-}
{-! for THF.As.PrincipalSymbol derive : ShATermConvertible !-}
{-! for THF.As.Source derive : ShATermConvertible !-}
{-! for THF.As.DagSource derive : ShATermConvertible !-}
{-! for THF.As.ParentInfo derive : ShATermConvertible !-}
{-! for THF.As.IntroType derive : ShATermConvertible !-}
{-! for THF.As.ExternalSource derive : ShATermConvertible !-}
{-! for THF.As.FileSource derive : ShATermConvertible !-}
{-! for THF.As.TheoryName derive : ShATermConvertible !-}
{-! for THF.As.InfoItem derive : ShATermConvertible !-}
{-! for THF.As.FormulaItem derive : ShATermConvertible !-}
{-! for THF.As.InferenceItem derive : ShATermConvertible !-}
{-! for THF.As.InferenceStatus derive : ShATermConvertible !-}
{-! for THF.As.StatusValue derive : ShATermConvertible !-}
{-! for THF.As.GeneralTerm derive : ShATermConvertible !-}
{-! for THF.As.GeneralData derive : ShATermConvertible !-}
{-! for THF.As.GeneralFunction derive : ShATermConvertible !-}
{-! for THF.As.FormulaData derive : ShATermConvertible !-}
{-! for THF.As.Name derive : ShATermConvertible !-}
{-! for THF.As.AtomicWord derive : ShATermConvertible !-}
{-! for THF.As.Number derive : ShATermConvertible !-}
{-! for THF.Cons.BasicSpecTHF derive : ShATermConvertible !-}
{-! for THF.Cons.SymbolTHF derive : ShATermConvertible !-}
{-! for THF.Cons.SymbolType derive : ShATermConvertible !-}
{-! for THF.Cons.Type derive : ShATermConvertible !-}
{-! for THF.Cons.Kind derive : ShATermConvertible !-}
{-! for THF.Sign.SignTHF derive : ShATermConvertible !-}
{-! for THF.Sign.TypeInfo derive : ShATermConvertible !-}
{-! for THF.Sign.ConstInfo derive : ShATermConvertible !-}
{-! for THF.Sublogic.THFCoreSl derive : ShATermConvertible !-}
{-! for THF.Sublogic.THFSl derive : ShATermConvertible !-}

{-! for THF.As.TPTP_THF derive : Json !-}
{-! for THF.As.Comment derive : Json !-}
{-! for THF.As.DefinedComment derive : Json !-}
{-! for THF.As.SystemComment derive : Json !-}
{-! for THF.As.Include derive : Json !-}
{-! for THF.As.Annotations derive : Json !-}
{-! for THF.As.FormulaRole derive : Json !-}
{-! for THF.As.THFFormula derive : Json !-}
{-! for THF.As.THFLogicFormula derive : Json !-}
{-! for THF.As.THFBinaryFormula derive : Json !-}
{-! for THF.As.THFBinaryTuple derive : Json !-}
{-! for THF.As.THFUnitaryFormula derive : Json !-}
{-! for THF.As.THFQuantifiedFormula derive : Json !-}
{-! for THF.As.THFVariable derive : Json !-}
{-! for THF.As.THFTypedConst derive : Json !-}
{-! for THF.As.THFTypeFormula derive : Json !-}
{-! for THF.As.THFTypeableFormula derive : Json !-}
{-! for THF.As.THFSubType derive : Json !-}
{-! for THF.As.THFTopLevelType derive : Json !-}
{-! for THF.As.THFUnitaryType derive : Json !-}
{-! for THF.As.THFBinaryType derive : Json !-}
{-! for THF.As.THFAtom derive : Json !-}
{-! for THF.As.THFSequent derive : Json !-}
{-! for THF.As.THFConnTerm derive : Json !-}
{-! for THF.As.THFQuantifier derive : Json !-}
{-! for THF.As.Quantifier derive : Json !-}
{-! for THF.As.THFPairConnective derive : Json !-}
{-! for THF.As.THFUnaryConnective derive : Json !-}
{-! for THF.As.AssocConnective derive : Json !-}
{-! for THF.As.DefinedType derive : Json !-}
{-! for THF.As.DefinedPlainFormula derive : Json !-}
{-! for THF.As.DefinedProp derive : Json !-}
{-! for THF.As.DefinedPred derive : Json !-}
{-! for THF.As.Term derive : Json !-}
{-! for THF.As.FunctionTerm derive : Json !-}
{-! for THF.As.PlainTerm derive : Json !-}
{-! for THF.As.DefinedTerm derive : Json !-}
{-! for THF.As.DefinedAtom derive : Json !-}
{-! for THF.As.DefinedPlainTerm derive : Json !-}
{-! for THF.As.DefinedFunctor derive : Json !-}
{-! for THF.As.SystemTerm derive : Json !-}
{-! for THF.As.PrincipalSymbol derive : Json !-}
{-! for THF.As.Source derive : Json !-}
{-! for THF.As.DagSource derive : Json !-}
{-! for THF.As.ParentInfo derive : Json !-}
{-! for THF.As.IntroType derive : Json !-}
{-! for THF.As.ExternalSource derive : Json !-}
{-! for THF.As.FileSource derive : Json !-}
{-! for THF.As.TheoryName derive : Json !-}
{-! for THF.As.InfoItem derive : Json !-}
{-! for THF.As.FormulaItem derive : Json !-}
{-! for THF.As.InferenceItem derive : Json !-}
{-! for THF.As.InferenceStatus derive : Json !-}
{-! for THF.As.StatusValue derive : Json !-}
{-! for THF.As.GeneralTerm derive : Json !-}
{-! for THF.As.GeneralData derive : Json !-}
{-! for THF.As.GeneralFunction derive : Json !-}
{-! for THF.As.FormulaData derive : Json !-}
{-! for THF.As.Name derive : Json !-}
{-! for THF.As.AtomicWord derive : Json !-}
{-! for THF.As.Number derive : Json !-}
{-! for THF.Cons.BasicSpecTHF derive : Json !-}
{-! for THF.Cons.SymbolTHF derive : Json !-}
{-! for THF.Cons.SymbolType derive : Json !-}
{-! for THF.Cons.Type derive : Json !-}
{-! for THF.Cons.Kind derive : Json !-}
{-! for THF.Sign.SignTHF derive : Json !-}
{-! for THF.Sign.TypeInfo derive : Json !-}
{-! for THF.Sign.ConstInfo derive : Json !-}
{-! for THF.Sublogic.THFCoreSl derive : Json !-}
{-! for THF.Sublogic.THFSl derive : Json !-}

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

instance ShATermConvertible THF.As.TPTP_THF where
  toShATermAux :: ATermTable -> TPTP_THF -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TPTP_THF
xv = case TPTP_THF
xv of
    TPTP_THF_Annotated_Formula a :: Name
a b :: FormulaRole
b c :: THFFormula
c d :: Annotations
d -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Name -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Name
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> FormulaRole -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 FormulaRole
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> THFFormula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 THFFormula
c
      (att4 :: ATermTable
att4, d' :: Int
d') <- ATermTable -> Annotations -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att3 Annotations
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 "TPTP_THF_Annotated_Formula" [Int
a', Int
b',
                                                               Int
c', Int
d'] []) ATermTable
att4
    TPTP_Include a :: Include
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Include -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Include
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 "TPTP_Include" [Int
a'] []) ATermTable
att1
    TPTP_Comment a :: Comment
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Comment -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Comment
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 "TPTP_Comment" [Int
a'] []) ATermTable
att1
    TPTP_Defined_Comment a :: DefinedComment
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> DefinedComment -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 DefinedComment
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 "TPTP_Defined_Comment" [Int
a'] []) ATermTable
att1
    TPTP_System_Comment a :: SystemComment
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SystemComment -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SystemComment
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 "TPTP_System_Comment" [Int
a'] []) ATermTable
att1
    TPTP_Header a :: [Comment]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Comment] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Comment]
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 "TPTP_Header" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, TPTP_THF)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "TPTP_THF_Annotated_Formula" [a :: Int
a, b :: Int
b, c :: Int
c, d :: Int
d] _ ->
      case Int -> ATermTable -> (ATermTable, Name)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Name
a') ->
      case Int -> ATermTable -> (ATermTable, FormulaRole)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: FormulaRole
b') ->
      case Int -> ATermTable -> (ATermTable, THFFormula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: THFFormula
c') ->
      case Int -> ATermTable -> (ATermTable, Annotations)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
d ATermTable
att3 of
      { (att4 :: ATermTable
att4, d' :: Annotations
d') ->
      (ATermTable
att4, Name -> FormulaRole -> THFFormula -> Annotations -> TPTP_THF
TPTP_THF_Annotated_Formula Name
a' FormulaRole
b' THFFormula
c' Annotations
d') }}}}
    ShAAppl "TPTP_Include" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Include)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Include
a') ->
      (ATermTable
att1, Include -> TPTP_THF
TPTP_Include Include
a') }
    ShAAppl "TPTP_Comment" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Comment)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Comment
a') ->
      (ATermTable
att1, Comment -> TPTP_THF
TPTP_Comment Comment
a') }
    ShAAppl "TPTP_Defined_Comment" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, DefinedComment)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: DefinedComment
a') ->
      (ATermTable
att1, DefinedComment -> TPTP_THF
TPTP_Defined_Comment DefinedComment
a') }
    ShAAppl "TPTP_System_Comment" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, SystemComment)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SystemComment
a') ->
      (ATermTable
att1, SystemComment -> TPTP_THF
TPTP_System_Comment SystemComment
a') }
    ShAAppl "TPTP_Header" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, [Comment])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [Comment]
a') ->
      (ATermTable
att1, [Comment] -> TPTP_THF
TPTP_Header [Comment]
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TPTP_THF)
forall a. String -> ShATerm -> a
fromShATermError "THF.As.TPTP_THF" ShATerm
u

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

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

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

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

instance ShATermConvertible THF.As.Annotations where
  toShATermAux :: ATermTable -> Annotations -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Annotations
xv = case Annotations
xv of
    Annotations a :: Source
a b :: OptionalInfo
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 -> OptionalInfo -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 OptionalInfo
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 "Annotations" [Int
a', Int
b'] []) ATermTable
att2
    Null -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Null" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, Annotations)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Annotations" [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, OptionalInfo)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: OptionalInfo
b') ->
      (ATermTable
att2, Source -> OptionalInfo -> Annotations
Annotations Source
a' OptionalInfo
b') }}
    ShAAppl "Null" [] _ -> (ATermTable
att0, Annotations
Null)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Annotations)
forall a. String -> ShATerm -> a
fromShATermError "THF.As.Annotations" ShATerm
u

instance ShATermConvertible THF.As.FormulaRole where
  toShATermAux :: ATermTable -> FormulaRole -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: FormulaRole
xv = case FormulaRole
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, FormulaRole)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Axiom" [] _ -> (ATermTable
att0, FormulaRole
Axiom)
    ShAAppl "Hypothesis" [] _ -> (ATermTable
att0, FormulaRole
Hypothesis)
    ShAAppl "Definition" [] _ -> (ATermTable
att0, FormulaRole
Definition)
    ShAAppl "Assumption" [] _ -> (ATermTable
att0, FormulaRole
Assumption)
    ShAAppl "Lemma" [] _ -> (ATermTable
att0, FormulaRole
Lemma)
    ShAAppl "Theorem" [] _ -> (ATermTable
att0, FormulaRole
Theorem)
    ShAAppl "Conjecture" [] _ -> (ATermTable
att0, FormulaRole
Conjecture)
    ShAAppl "Negated_Conjecture" [] _ -> (ATermTable
att0, FormulaRole
Negated_Conjecture)
    ShAAppl "Plain" [] _ -> (ATermTable
att0, FormulaRole
Plain)
    ShAAppl "Fi_Domain" [] _ -> (ATermTable
att0, FormulaRole
Fi_Domain)
    ShAAppl "Fi_Functors" [] _ -> (ATermTable
att0, FormulaRole
Fi_Functors)
    ShAAppl "Fi_Predicates" [] _ -> (ATermTable
att0, FormulaRole
Fi_Predicates)
    ShAAppl "Type" [] _ -> (ATermTable
att0, FormulaRole
Type)
    ShAAppl "Unknown" [] _ -> (ATermTable
att0, FormulaRole
Unknown)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, FormulaRole)
forall a. String -> ShATerm -> a
fromShATermError "THF.As.FormulaRole" ShATerm
u

instance ShATermConvertible THF.As.THFFormula where
  toShATermAux :: ATermTable -> THFFormula -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THFFormula
xv = case THFFormula
xv of
    TF_THF_Logic_Formula a :: THFLogicFormula
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFLogicFormula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFLogicFormula
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 "TF_THF_Logic_Formula" [Int
a'] []) ATermTable
att1
    TF_THF_Sequent a :: THFSequent
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFSequent -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFSequent
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 "TF_THF_Sequent" [Int
a'] []) ATermTable
att1
    T0F_THF_Typed_Const a :: THFTypedConst
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFTypedConst -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFTypedConst
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 "T0F_THF_Typed_Const" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, THFFormula)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "TF_THF_Logic_Formula" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, THFLogicFormula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFLogicFormula
a') ->
      (ATermTable
att1, THFLogicFormula -> THFFormula
TF_THF_Logic_Formula THFLogicFormula
a') }
    ShAAppl "TF_THF_Sequent" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, THFSequent)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFSequent
a') ->
      (ATermTable
att1, THFSequent -> THFFormula
TF_THF_Sequent THFSequent
a') }
    ShAAppl "T0F_THF_Typed_Const" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, THFTypedConst)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFTypedConst
a') ->
      (ATermTable
att1, THFTypedConst -> THFFormula
T0F_THF_Typed_Const THFTypedConst
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THFFormula)
forall a. String -> ShATerm -> a
fromShATermError "THF.As.THFFormula" ShATerm
u

instance ShATermConvertible THF.As.THFLogicFormula where
  toShATermAux :: ATermTable -> THFLogicFormula -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THFLogicFormula
xv = case THFLogicFormula
xv of
    TLF_THF_Binary_Formula a :: THFBinaryFormula
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFBinaryFormula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFBinaryFormula
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 "TLF_THF_Binary_Formula" [Int
a'] []) ATermTable
att1
    TLF_THF_Unitary_Formula a :: THFUnitaryFormula
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFUnitaryFormula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFUnitaryFormula
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 "TLF_THF_Unitary_Formula" [Int
a'] []) ATermTable
att1
    TLF_THF_Type_Formula a :: THFTypeFormula
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFTypeFormula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFTypeFormula
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 "TLF_THF_Type_Formula" [Int
a'] []) ATermTable
att1
    TLF_THF_Sub_Type a :: THFSubType
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFSubType -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFSubType
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 "TLF_THF_Sub_Type" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, THFLogicFormula)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "TLF_THF_Binary_Formula" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, THFBinaryFormula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFBinaryFormula
a') ->
      (ATermTable
att1, THFBinaryFormula -> THFLogicFormula
TLF_THF_Binary_Formula THFBinaryFormula
a') }
    ShAAppl "TLF_THF_Unitary_Formula" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, THFUnitaryFormula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFUnitaryFormula
a') ->
      (ATermTable
att1, THFUnitaryFormula -> THFLogicFormula
TLF_THF_Unitary_Formula THFUnitaryFormula
a') }
    ShAAppl "TLF_THF_Type_Formula" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, THFTypeFormula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFTypeFormula
a') ->
      (ATermTable
att1, THFTypeFormula -> THFLogicFormula
TLF_THF_Type_Formula THFTypeFormula
a') }
    ShAAppl "TLF_THF_Sub_Type" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, THFSubType)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFSubType
a') ->
      (ATermTable
att1, THFSubType -> THFLogicFormula
TLF_THF_Sub_Type THFSubType
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THFLogicFormula)
forall a. String -> ShATerm -> a
fromShATermError "THF.As.THFLogicFormula" ShATerm
u

instance ShATermConvertible THF.As.THFBinaryFormula where
  toShATermAux :: ATermTable -> THFBinaryFormula -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THFBinaryFormula
xv = case THFBinaryFormula
xv of
    TBF_THF_Binary_Pair a :: THFUnitaryFormula
a b :: THFPairConnective
b c :: THFUnitaryFormula
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFUnitaryFormula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFUnitaryFormula
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> THFPairConnective -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 THFPairConnective
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> THFUnitaryFormula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 THFUnitaryFormula
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 "TBF_THF_Binary_Pair" [Int
a', Int
b',
                                                        Int
c'] []) ATermTable
att3
    TBF_THF_Binary_Tuple a :: THFBinaryTuple
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFBinaryTuple -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFBinaryTuple
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 "TBF_THF_Binary_Tuple" [Int
a'] []) ATermTable
att1
    TBF_THF_Binary_Type a :: THFBinaryType
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFBinaryType -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFBinaryType
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 "TBF_THF_Binary_Type" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, THFBinaryFormula)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "TBF_THF_Binary_Pair" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, THFUnitaryFormula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFUnitaryFormula
a') ->
      case Int -> ATermTable -> (ATermTable, THFPairConnective)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: THFPairConnective
b') ->
      case Int -> ATermTable -> (ATermTable, THFUnitaryFormula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: THFUnitaryFormula
c') ->
      (ATermTable
att3, THFUnitaryFormula
-> THFPairConnective -> THFUnitaryFormula -> THFBinaryFormula
TBF_THF_Binary_Pair THFUnitaryFormula
a' THFPairConnective
b' THFUnitaryFormula
c') }}}
    ShAAppl "TBF_THF_Binary_Tuple" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, THFBinaryTuple)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFBinaryTuple
a') ->
      (ATermTable
att1, THFBinaryTuple -> THFBinaryFormula
TBF_THF_Binary_Tuple THFBinaryTuple
a') }
    ShAAppl "TBF_THF_Binary_Type" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, THFBinaryType)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFBinaryType
a') ->
      (ATermTable
att1, THFBinaryType -> THFBinaryFormula
TBF_THF_Binary_Type THFBinaryType
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THFBinaryFormula)
forall a. String -> ShATerm -> a
fromShATermError "THF.As.THFBinaryFormula" ShATerm
u

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

instance ShATermConvertible THF.As.THFUnitaryFormula where
  toShATermAux :: ATermTable -> THFUnitaryFormula -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THFUnitaryFormula
xv = case THFUnitaryFormula
xv of
    TUF_THF_Quantified_Formula a :: THFQuantifiedFormula
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFQuantifiedFormula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFQuantifiedFormula
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 "TUF_THF_Quantified_Formula" [Int
a'] []) ATermTable
att1
    TUF_THF_Unary_Formula a :: THFUnaryConnective
a b :: THFLogicFormula
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFUnaryConnective -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFUnaryConnective
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> THFLogicFormula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 THFLogicFormula
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 "TUF_THF_Unary_Formula" [Int
a',
                                                          Int
b'] []) ATermTable
att2
    TUF_THF_Atom a :: THFAtom
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFAtom -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFAtom
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 "TUF_THF_Atom" [Int
a'] []) ATermTable
att1
    TUF_THF_Tuple a :: [THFLogicFormula]
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [THFLogicFormula] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [THFLogicFormula]
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 "TUF_THF_Tuple" [Int
a'] []) ATermTable
att1
    TUF_THF_Conditional a :: THFLogicFormula
a b :: THFLogicFormula
b c :: THFLogicFormula
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFLogicFormula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFLogicFormula
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> THFLogicFormula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 THFLogicFormula
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> THFLogicFormula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 THFLogicFormula
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 "TUF_THF_Conditional" [Int
a', Int
b',
                                                        Int
c'] []) ATermTable
att3
    TUF_THF_Logic_Formula_Par a :: THFLogicFormula
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFLogicFormula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFLogicFormula
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 "TUF_THF_Logic_Formula_Par" [Int
a'] []) ATermTable
att1
    T0UF_THF_Abstraction a :: THFVariableList
a b :: THFUnitaryFormula
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFVariableList -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFVariableList
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> THFUnitaryFormula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 THFUnitaryFormula
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 "T0UF_THF_Abstraction" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, THFUnitaryFormula)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "TUF_THF_Quantified_Formula" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, THFQuantifiedFormula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFQuantifiedFormula
a') ->
      (ATermTable
att1, THFQuantifiedFormula -> THFUnitaryFormula
TUF_THF_Quantified_Formula THFQuantifiedFormula
a') }
    ShAAppl "TUF_THF_Unary_Formula" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, THFUnaryConnective)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFUnaryConnective
a') ->
      case Int -> ATermTable -> (ATermTable, THFLogicFormula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: THFLogicFormula
b') ->
      (ATermTable
att2, THFUnaryConnective -> THFLogicFormula -> THFUnitaryFormula
TUF_THF_Unary_Formula THFUnaryConnective
a' THFLogicFormula
b') }}
    ShAAppl "TUF_THF_Atom" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, THFAtom)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFAtom
a') ->
      (ATermTable
att1, THFAtom -> THFUnitaryFormula
TUF_THF_Atom THFAtom
a') }
    ShAAppl "TUF_THF_Tuple" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, [THFLogicFormula])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: [THFLogicFormula]
a') ->
      (ATermTable
att1, [THFLogicFormula] -> THFUnitaryFormula
TUF_THF_Tuple [THFLogicFormula]
a') }
    ShAAppl "TUF_THF_Conditional" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, THFLogicFormula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFLogicFormula
a') ->
      case Int -> ATermTable -> (ATermTable, THFLogicFormula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: THFLogicFormula
b') ->
      case Int -> ATermTable -> (ATermTable, THFLogicFormula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: THFLogicFormula
c') ->
      (ATermTable
att3, THFLogicFormula
-> THFLogicFormula -> THFLogicFormula -> THFUnitaryFormula
TUF_THF_Conditional THFLogicFormula
a' THFLogicFormula
b' THFLogicFormula
c') }}}
    ShAAppl "TUF_THF_Logic_Formula_Par" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, THFLogicFormula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFLogicFormula
a') ->
      (ATermTable
att1, THFLogicFormula -> THFUnitaryFormula
TUF_THF_Logic_Formula_Par THFLogicFormula
a') }
    ShAAppl "T0UF_THF_Abstraction" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, THFVariableList)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFVariableList
a') ->
      case Int -> ATermTable -> (ATermTable, THFUnitaryFormula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: THFUnitaryFormula
b') ->
      (ATermTable
att2, THFVariableList -> THFUnitaryFormula -> THFUnitaryFormula
T0UF_THF_Abstraction THFVariableList
a' THFUnitaryFormula
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THFUnitaryFormula)
forall a. String -> ShATerm -> a
fromShATermError "THF.As.THFUnitaryFormula" ShATerm
u

instance ShATermConvertible THF.As.THFQuantifiedFormula where
  toShATermAux :: ATermTable -> THFQuantifiedFormula -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THFQuantifiedFormula
xv = case THFQuantifiedFormula
xv of
    TQF_THF_Quantified_Formula a :: THFQuantifier
a b :: THFVariableList
b c :: THFUnitaryFormula
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFQuantifier -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFQuantifier
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> THFVariableList -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 THFVariableList
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> THFUnitaryFormula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 THFUnitaryFormula
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 "TQF_THF_Quantified_Formula" [Int
a', Int
b',
                                                               Int
c'] []) ATermTable
att3
    T0QF_THF_Quantified_Var a :: Quantifier
a b :: THFVariableList
b c :: THFUnitaryFormula
c -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Quantifier -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Quantifier
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> THFVariableList -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 THFVariableList
b
      (att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> THFUnitaryFormula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 THFUnitaryFormula
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 "T0QF_THF_Quantified_Var" [Int
a', Int
b',
                                                            Int
c'] []) ATermTable
att3
    T0QF_THF_Quantified_Novar a :: THFQuantifier
a b :: THFUnitaryFormula
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFQuantifier -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFQuantifier
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> THFUnitaryFormula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 THFUnitaryFormula
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 "T0QF_THF_Quantified_Novar" [Int
a',
                                                              Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, THFQuantifiedFormula)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "TQF_THF_Quantified_Formula" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, THFQuantifier)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFQuantifier
a') ->
      case Int -> ATermTable -> (ATermTable, THFVariableList)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: THFVariableList
b') ->
      case Int -> ATermTable -> (ATermTable, THFUnitaryFormula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: THFUnitaryFormula
c') ->
      (ATermTable
att3, THFQuantifier
-> THFVariableList -> THFUnitaryFormula -> THFQuantifiedFormula
TQF_THF_Quantified_Formula THFQuantifier
a' THFVariableList
b' THFUnitaryFormula
c') }}}
    ShAAppl "T0QF_THF_Quantified_Var" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
      case Int -> ATermTable -> (ATermTable, Quantifier)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Quantifier
a') ->
      case Int -> ATermTable -> (ATermTable, THFVariableList)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: THFVariableList
b') ->
      case Int -> ATermTable -> (ATermTable, THFUnitaryFormula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
      { (att3 :: ATermTable
att3, c' :: THFUnitaryFormula
c') ->
      (ATermTable
att3, Quantifier
-> THFVariableList -> THFUnitaryFormula -> THFQuantifiedFormula
T0QF_THF_Quantified_Var Quantifier
a' THFVariableList
b' THFUnitaryFormula
c') }}}
    ShAAppl "T0QF_THF_Quantified_Novar" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, THFQuantifier)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFQuantifier
a') ->
      case Int -> ATermTable -> (ATermTable, THFUnitaryFormula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
      { (att2 :: ATermTable
att2, b' :: THFUnitaryFormula
b') ->
      (ATermTable
att2, THFQuantifier -> THFUnitaryFormula -> THFQuantifiedFormula
T0QF_THF_Quantified_Novar THFQuantifier
a' THFUnitaryFormula
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THFQuantifiedFormula)
forall a. String -> ShATerm -> a
fromShATermError "THF.As.THFQuantifiedFormula" ShATerm
u

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

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

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

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

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

instance ShATermConvertible THF.As.THFTopLevelType where
  toShATermAux :: ATermTable -> THFTopLevelType -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THFTopLevelType
xv = case THFTopLevelType
xv of
    TTLT_THF_Logic_Formula a :: THFLogicFormula
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFLogicFormula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFLogicFormula
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 "TTLT_THF_Logic_Formula" [Int
a'] []) ATermTable
att1
    T0TLT_Constant a :: Constant
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Constant -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Constant
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 "T0TLT_Constant" [Int
a'] []) ATermTable
att1
    T0TLT_Variable a :: Token
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Token -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Token
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 "T0TLT_Variable" [Int
a'] []) ATermTable
att1
    T0TLT_Defined_Type a :: DefinedType
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> DefinedType -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 DefinedType
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 "T0TLT_Defined_Type" [Int
a'] []) ATermTable
att1
    T0TLT_System_Type a :: Token
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Token -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Token
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 "T0TLT_System_Type" [Int
a'] []) ATermTable
att1
    T0TLT_THF_Binary_Type a :: THFBinaryType
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFBinaryType -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFBinaryType
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 "T0TLT_THF_Binary_Type" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, THFTopLevelType)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "TTLT_THF_Logic_Formula" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, THFLogicFormula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFLogicFormula
a') ->
      (ATermTable
att1, THFLogicFormula -> THFTopLevelType
TTLT_THF_Logic_Formula THFLogicFormula
a') }
    ShAAppl "T0TLT_Constant" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Constant)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Constant
a') ->
      (ATermTable
att1, Constant -> THFTopLevelType
T0TLT_Constant Constant
a') }
    ShAAppl "T0TLT_Variable" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Token)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Token
a') ->
      (ATermTable
att1, Token -> THFTopLevelType
T0TLT_Variable Token
a') }
    ShAAppl "T0TLT_Defined_Type" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, DefinedType)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: DefinedType
a') ->
      (ATermTable
att1, DefinedType -> THFTopLevelType
T0TLT_Defined_Type DefinedType
a') }
    ShAAppl "T0TLT_System_Type" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Token)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Token
a') ->
      (ATermTable
att1, Token -> THFTopLevelType
T0TLT_System_Type Token
a') }
    ShAAppl "T0TLT_THF_Binary_Type" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, THFBinaryType)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFBinaryType
a') ->
      (ATermTable
att1, THFBinaryType -> THFTopLevelType
T0TLT_THF_Binary_Type THFBinaryType
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THFTopLevelType)
forall a. String -> ShATerm -> a
fromShATermError "THF.As.THFTopLevelType" ShATerm
u

instance ShATermConvertible THF.As.THFUnitaryType where
  toShATermAux :: ATermTable -> THFUnitaryType -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THFUnitaryType
xv = case THFUnitaryType
xv of
    TUT_THF_Unitary_Formula a :: THFUnitaryFormula
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFUnitaryFormula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFUnitaryFormula
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 "TUT_THF_Unitary_Formula" [Int
a'] []) ATermTable
att1
    T0UT_Constant a :: Constant
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Constant -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Constant
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 "T0UT_Constant" [Int
a'] []) ATermTable
att1
    T0UT_Variable a :: Token
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Token -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Token
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 "T0UT_Variable" [Int
a'] []) ATermTable
att1
    T0UT_Defined_Type a :: DefinedType
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> DefinedType -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 DefinedType
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 "T0UT_Defined_Type" [Int
a'] []) ATermTable
att1
    T0UT_System_Type a :: Token
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Token -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Token
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 "T0UT_System_Type" [Int
a'] []) ATermTable
att1
    T0UT_THF_Binary_Type_Par a :: THFBinaryType
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFBinaryType -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFBinaryType
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 "T0UT_THF_Binary_Type_Par" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, THFUnitaryType)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "TUT_THF_Unitary_Formula" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, THFUnitaryFormula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFUnitaryFormula
a') ->
      (ATermTable
att1, THFUnitaryFormula -> THFUnitaryType
TUT_THF_Unitary_Formula THFUnitaryFormula
a') }
    ShAAppl "T0UT_Constant" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Constant)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Constant
a') ->
      (ATermTable
att1, Constant -> THFUnitaryType
T0UT_Constant Constant
a') }
    ShAAppl "T0UT_Variable" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Token)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Token
a') ->
      (ATermTable
att1, Token -> THFUnitaryType
T0UT_Variable Token
a') }
    ShAAppl "T0UT_Defined_Type" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, DefinedType)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: DefinedType
a') ->
      (ATermTable
att1, DefinedType -> THFUnitaryType
T0UT_Defined_Type DefinedType
a') }
    ShAAppl "T0UT_System_Type" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Token)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Token
a') ->
      (ATermTable
att1, Token -> THFUnitaryType
T0UT_System_Type Token
a') }
    ShAAppl "T0UT_THF_Binary_Type_Par" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, THFBinaryType)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFBinaryType
a') ->
      (ATermTable
att1, THFBinaryType -> THFUnitaryType
T0UT_THF_Binary_Type_Par THFBinaryType
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THFUnitaryType)
forall a. String -> ShATerm -> a
fromShATermError "THF.As.THFUnitaryType" ShATerm
u

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

instance ShATermConvertible THF.As.THFAtom where
  toShATermAux :: ATermTable -> THFAtom -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THFAtom
xv = case THFAtom
xv of
    TA_Term a :: Term
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Term
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 "TA_Term" [Int
a'] []) ATermTable
att1
    TA_THF_Conn_Term a :: THFConnTerm
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFConnTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFConnTerm
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 "TA_THF_Conn_Term" [Int
a'] []) ATermTable
att1
    TA_Defined_Type a :: DefinedType
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> DefinedType -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 DefinedType
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 "TA_Defined_Type" [Int
a'] []) ATermTable
att1
    TA_Defined_Plain_Formula a :: DefinedPlainFormula
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> DefinedPlainFormula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 DefinedPlainFormula
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 "TA_Defined_Plain_Formula" [Int
a'] []) ATermTable
att1
    TA_System_Type a :: Token
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Token -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Token
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 "TA_System_Type" [Int
a'] []) ATermTable
att1
    TA_System_Atomic_Formula a :: SystemTerm
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SystemTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SystemTerm
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 "TA_System_Atomic_Formula" [Int
a'] []) ATermTable
att1
    T0A_Constant a :: Constant
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Constant -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Constant
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 "T0A_Constant" [Int
a'] []) ATermTable
att1
    T0A_Defined_Constant a :: Token
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Token -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Token
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 "T0A_Defined_Constant" [Int
a'] []) ATermTable
att1
    T0A_System_Constant a :: Token
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Token -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Token
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 "T0A_System_Constant" [Int
a'] []) ATermTable
att1
    T0A_Variable a :: Token
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Token -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Token
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 "T0A_Variable" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, THFAtom)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "TA_Term" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Term
a') ->
      (ATermTable
att1, Term -> THFAtom
TA_Term Term
a') }
    ShAAppl "TA_THF_Conn_Term" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, THFConnTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFConnTerm
a') ->
      (ATermTable
att1, THFConnTerm -> THFAtom
TA_THF_Conn_Term THFConnTerm
a') }
    ShAAppl "TA_Defined_Type" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, DefinedType)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: DefinedType
a') ->
      (ATermTable
att1, DefinedType -> THFAtom
TA_Defined_Type DefinedType
a') }
    ShAAppl "TA_Defined_Plain_Formula" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, DefinedPlainFormula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: DefinedPlainFormula
a') ->
      (ATermTable
att1, DefinedPlainFormula -> THFAtom
TA_Defined_Plain_Formula DefinedPlainFormula
a') }
    ShAAppl "TA_System_Type" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Token)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Token
a') ->
      (ATermTable
att1, Token -> THFAtom
TA_System_Type Token
a') }
    ShAAppl "TA_System_Atomic_Formula" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, SystemTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SystemTerm
a') ->
      (ATermTable
att1, SystemTerm -> THFAtom
TA_System_Atomic_Formula SystemTerm
a') }
    ShAAppl "T0A_Constant" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Constant)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Constant
a') ->
      (ATermTable
att1, Constant -> THFAtom
T0A_Constant Constant
a') }
    ShAAppl "T0A_Defined_Constant" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Token)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Token
a') ->
      (ATermTable
att1, Token -> THFAtom
T0A_Defined_Constant Token
a') }
    ShAAppl "T0A_System_Constant" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Token)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Token
a') ->
      (ATermTable
att1, Token -> THFAtom
T0A_System_Constant Token
a') }
    ShAAppl "T0A_Variable" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, Token)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: Token
a') ->
      (ATermTable
att1, Token -> THFAtom
T0A_Variable Token
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THFAtom)
forall a. String -> ShATerm -> a
fromShATermError "THF.As.THFAtom" ShATerm
u

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

instance ShATermConvertible THF.As.THFConnTerm where
  toShATermAux :: ATermTable -> THFConnTerm -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THFConnTerm
xv = case THFConnTerm
xv of
    TCT_THF_Pair_Connective a :: THFPairConnective
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFPairConnective -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFPairConnective
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 "TCT_THF_Pair_Connective" [Int
a'] []) ATermTable
att1
    TCT_Assoc_Connective a :: AssocConnective
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> AssocConnective -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 AssocConnective
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 "TCT_Assoc_Connective" [Int
a'] []) ATermTable
att1
    TCT_THF_Unary_Connective a :: THFUnaryConnective
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFUnaryConnective -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFUnaryConnective
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 "TCT_THF_Unary_Connective" [Int
a'] []) ATermTable
att1
    T0CT_THF_Quantifier a :: THFQuantifier
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THFQuantifier -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THFQuantifier
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 "T0CT_THF_Quantifier" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, THFConnTerm)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "TCT_THF_Pair_Connective" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, THFPairConnective)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFPairConnective
a') ->
      (ATermTable
att1, THFPairConnective -> THFConnTerm
TCT_THF_Pair_Connective THFPairConnective
a') }
    ShAAppl "TCT_Assoc_Connective" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, AssocConnective)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: AssocConnective
a') ->
      (ATermTable
att1, AssocConnective -> THFConnTerm
TCT_Assoc_Connective AssocConnective
a') }
    ShAAppl "TCT_THF_Unary_Connective" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, THFUnaryConnective)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFUnaryConnective
a') ->
      (ATermTable
att1, THFUnaryConnective -> THFConnTerm
TCT_THF_Unary_Connective THFUnaryConnective
a') }
    ShAAppl "T0CT_THF_Quantifier" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, THFQuantifier)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: THFQuantifier
a') ->
      (ATermTable
att1, THFQuantifier -> THFConnTerm
T0CT_THF_Quantifier THFQuantifier
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THFConnTerm)
forall a. String -> ShATerm -> a
fromShATermError "THF.As.THFConnTerm" ShATerm
u

instance ShATermConvertible THF.As.THFQuantifier where
  toShATermAux :: ATermTable -> THFQuantifier -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THFQuantifier
xv = case THFQuantifier
xv of
    TQ_ForAll -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "TQ_ForAll" [] []) ATermTable
att0
    TQ_Exists -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "TQ_Exists" [] []) ATermTable
att0
    TQ_Lambda_Binder ->
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "TQ_Lambda_Binder" [] []) ATermTable
att0
    TQ_Dependent_Product ->
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "TQ_Dependent_Product" [] []) ATermTable
att0
    TQ_Dependent_Sum ->
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "TQ_Dependent_Sum" [] []) ATermTable
att0
    TQ_Indefinite_Description ->
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "TQ_Indefinite_Description" [] []) ATermTable
att0
    TQ_Definite_Description ->
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "TQ_Definite_Description" [] []) ATermTable
att0
    T0Q_PiForAll -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "T0Q_PiForAll" [] []) ATermTable
att0
    T0Q_SigmaExists -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "T0Q_SigmaExists" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, THFQuantifier)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "TQ_ForAll" [] _ -> (ATermTable
att0, THFQuantifier
TQ_ForAll)
    ShAAppl "TQ_Exists" [] _ -> (ATermTable
att0, THFQuantifier
TQ_Exists)
    ShAAppl "TQ_Lambda_Binder" [] _ -> (ATermTable
att0, THFQuantifier
TQ_Lambda_Binder)
    ShAAppl "TQ_Dependent_Product" [] _ -> (ATermTable
att0, THFQuantifier
TQ_Dependent_Product)
    ShAAppl "TQ_Dependent_Sum" [] _ -> (ATermTable
att0, THFQuantifier
TQ_Dependent_Sum)
    ShAAppl "TQ_Indefinite_Description" [] _ -> (ATermTable
att0, THFQuantifier
TQ_Indefinite_Description)
    ShAAppl "TQ_Definite_Description" [] _ -> (ATermTable
att0, THFQuantifier
TQ_Definite_Description)
    ShAAppl "T0Q_PiForAll" [] _ -> (ATermTable
att0, THFQuantifier
T0Q_PiForAll)
    ShAAppl "T0Q_SigmaExists" [] _ -> (ATermTable
att0, THFQuantifier
T0Q_SigmaExists)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THFQuantifier)
forall a. String -> ShATerm -> a
fromShATermError "THF.As.THFQuantifier" ShATerm
u

instance ShATermConvertible THF.As.Quantifier where
  toShATermAux :: ATermTable -> Quantifier -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Quantifier
xv = case Quantifier
xv of
    T0Q_ForAll -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "T0Q_ForAll" [] []) ATermTable
att0
    T0Q_Exists -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "T0Q_Exists" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, Quantifier)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "T0Q_ForAll" [] _ -> (ATermTable
att0, Quantifier
T0Q_ForAll)
    ShAAppl "T0Q_Exists" [] _ -> (ATermTable
att0, Quantifier
T0Q_Exists)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Quantifier)
forall a. String -> ShATerm -> a
fromShATermError "THF.As.Quantifier" ShATerm
u

instance ShATermConvertible THF.As.THFPairConnective where
  toShATermAux :: ATermTable -> THFPairConnective -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THFPairConnective
xv = case THFPairConnective
xv of
    Infix_Equality -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Infix_Equality" [] []) ATermTable
att0
    Infix_Inequality ->
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Infix_Inequality" [] []) ATermTable
att0
    Equivalent -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Equivalent" [] []) ATermTable
att0
    Implication -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Implication" [] []) ATermTable
att0
    IF -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "IF" [] []) ATermTable
att0
    XOR -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "XOR" [] []) ATermTable
att0
    NOR -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "NOR" [] []) ATermTable
att0
    NAND -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "NAND" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, THFPairConnective)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Infix_Equality" [] _ -> (ATermTable
att0, THFPairConnective
Infix_Equality)
    ShAAppl "Infix_Inequality" [] _ -> (ATermTable
att0, THFPairConnective
Infix_Inequality)
    ShAAppl "Equivalent" [] _ -> (ATermTable
att0, THFPairConnective
Equivalent)
    ShAAppl "Implication" [] _ -> (ATermTable
att0, THFPairConnective
Implication)
    ShAAppl "IF" [] _ -> (ATermTable
att0, THFPairConnective
IF)
    ShAAppl "XOR" [] _ -> (ATermTable
att0, THFPairConnective
XOR)
    ShAAppl "NOR" [] _ -> (ATermTable
att0, THFPairConnective
NOR)
    ShAAppl "NAND" [] _ -> (ATermTable
att0, THFPairConnective
NAND)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THFPairConnective)
forall a. String -> ShATerm -> a
fromShATermError "THF.As.THFPairConnective" ShATerm
u

instance ShATermConvertible THF.As.THFUnaryConnective where
  toShATermAux :: ATermTable -> THFUnaryConnective -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THFUnaryConnective
xv = case THFUnaryConnective
xv of
    Negation -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Negation" [] []) ATermTable
att0
    PiForAll -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "PiForAll" [] []) ATermTable
att0
    SigmaExists -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "SigmaExists" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, THFUnaryConnective)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Negation" [] _ -> (ATermTable
att0, THFUnaryConnective
Negation)
    ShAAppl "PiForAll" [] _ -> (ATermTable
att0, THFUnaryConnective
PiForAll)
    ShAAppl "SigmaExists" [] _ -> (ATermTable
att0, THFUnaryConnective
SigmaExists)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THFUnaryConnective)
forall a. String -> ShATerm -> a
fromShATermError "THF.As.THFUnaryConnective" ShATerm
u

instance ShATermConvertible THF.As.AssocConnective where
  toShATermAux :: ATermTable -> AssocConnective -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: AssocConnective
xv = case AssocConnective
xv of
    OR -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "OR" [] []) ATermTable
att0
    AND -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "AND" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, AssocConnective)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "OR" [] _ -> (ATermTable
att0, AssocConnective
OR)
    ShAAppl "AND" [] _ -> (ATermTable
att0, AssocConnective
AND)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, AssocConnective)
forall a. String -> ShATerm -> a
fromShATermError "THF.As.AssocConnective" ShATerm
u

instance ShATermConvertible THF.As.DefinedType where
  toShATermAux :: ATermTable -> DefinedType -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: DefinedType
xv = case DefinedType
xv of
    DT_oType -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "DT_oType" [] []) ATermTable
att0
    DT_o -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "DT_o" [] []) ATermTable
att0
    DT_iType -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "DT_iType" [] []) ATermTable
att0
    DT_i -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "DT_i" [] []) ATermTable
att0
    DT_tType -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "DT_tType" [] []) ATermTable
att0
    DT_real -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "DT_real" [] []) ATermTable
att0
    DT_rat -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "DT_rat" [] []) ATermTable
att0
    DT_int -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "DT_int" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, DefinedType)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "DT_oType" [] _ -> (ATermTable
att0, DefinedType
DT_oType)
    ShAAppl "DT_o" [] _ -> (ATermTable
att0, DefinedType
DT_o)
    ShAAppl "DT_iType" [] _ -> (ATermTable
att0, DefinedType
DT_iType)
    ShAAppl "DT_i" [] _ -> (ATermTable
att0, DefinedType
DT_i)
    ShAAppl "DT_tType" [] _ -> (ATermTable
att0, DefinedType
DT_tType)
    ShAAppl "DT_real" [] _ -> (ATermTable
att0, DefinedType
DT_real)
    ShAAppl "DT_rat" [] _ -> (ATermTable
att0, DefinedType
DT_rat)
    ShAAppl "DT_int" [] _ -> (ATermTable
att0, DefinedType
DT_int)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, DefinedType)
forall a. String -> ShATerm -> a
fromShATermError "THF.As.DefinedType" ShATerm
u

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

instance ShATermConvertible THF.As.DefinedProp where
  toShATermAux :: ATermTable -> DefinedProp -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: DefinedProp
xv = case DefinedProp
xv of
    DP_True -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "DP_True" [] []) ATermTable
att0
    DP_False -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "DP_False" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, DefinedProp)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "DP_True" [] _ -> (ATermTable
att0, DefinedProp
DP_True)
    ShAAppl "DP_False" [] _ -> (ATermTable
att0, DefinedProp
DP_False)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, DefinedProp)
forall a. String -> ShATerm -> a
fromShATermError "THF.As.DefinedProp" ShATerm
u

instance ShATermConvertible THF.As.DefinedPred where
  toShATermAux :: ATermTable -> DefinedPred -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: DefinedPred
xv = case DefinedPred
xv of
    Disrinct -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Disrinct" [] []) ATermTable
att0
    Less -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Less" [] []) ATermTable
att0
    Lesseq -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Lesseq" [] []) ATermTable
att0
    Greater -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Greater" [] []) ATermTable
att0
    Greatereq -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Greatereq" [] []) ATermTable
att0
    Is_int -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Is_int" [] []) ATermTable
att0
    Is_rat -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Is_rat" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, DefinedPred)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "Disrinct" [] _ -> (ATermTable
att0, DefinedPred
Disrinct)
    ShAAppl "Less" [] _ -> (ATermTable
att0, DefinedPred
Less)
    ShAAppl "Lesseq" [] _ -> (ATermTable
att0, DefinedPred
Lesseq)
    ShAAppl "Greater" [] _ -> (ATermTable
att0, DefinedPred
Greater)
    ShAAppl "Greatereq" [] _ -> (ATermTable
att0, DefinedPred
Greatereq)
    ShAAppl "Is_int" [] _ -> (ATermTable
att0, DefinedPred
Is_int)
    ShAAppl "Is_rat" [] _ -> (ATermTable
att0, DefinedPred
Is_rat)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, DefinedPred)
forall a. String -> ShATerm -> a
fromShATermError "THF.As.DefinedPred" ShATerm
u

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

instance ShATermConvertible THF.As.FunctionTerm where
  toShATermAux :: ATermTable -> FunctionTerm -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: FunctionTerm
xv = case FunctionTerm
xv of
    FT_Plain_Term a :: PlainTerm
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> PlainTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 PlainTerm
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 "FT_Plain_Term" [Int
a'] []) ATermTable
att1
    FT_Defined_Term a :: DefinedTerm
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> DefinedTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 DefinedTerm
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 "FT_Defined_Term" [Int
a'] []) ATermTable
att1
    FT_System_Term a :: SystemTerm
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> SystemTerm -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 SystemTerm
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 "FT_System_Term" [Int
a'] []) ATermTable
att1
  fromShATermAux :: Int -> ATermTable -> (ATermTable, FunctionTerm)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "FT_Plain_Term" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, PlainTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: PlainTerm
a') ->
      (ATermTable
att1, PlainTerm -> FunctionTerm
FT_Plain_Term PlainTerm
a') }
    ShAAppl "FT_Defined_Term" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, DefinedTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: DefinedTerm
a') ->
      (ATermTable
att1, DefinedTerm -> FunctionTerm
FT_Defined_Term DefinedTerm
a') }
    ShAAppl "FT_System_Term" [a :: Int
a] _ ->
      case Int -> ATermTable -> (ATermTable, SystemTerm)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
      { (att1 :: ATermTable
att1, a' :: SystemTerm
a') ->
      (ATermTable
att1, SystemTerm -> FunctionTerm
FT_System_Term SystemTerm
a') }
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, FunctionTerm)
forall a. String -> ShATerm -> a
fromShATermError "THF.As.FunctionTerm" ShATerm
u

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

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

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

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

instance ShATermConvertible THF.As.DefinedFunctor where
  toShATermAux :: ATermTable -> DefinedFunctor -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: DefinedFunctor
xv = case DefinedFunctor
xv of
    UMinus -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "UMinus" [] []) ATermTable
att0
    Sum -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Sum" [] []) ATermTable
att0
    Difference -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Difference" [] []) ATermTable
att0
    Product -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Product" [] []) ATermTable
att0
    Quotient -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Quotient" [] []) ATermTable
att0
    Quotient_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 "Quotient_e" [] []) ATermTable
att0
    Quotient_t -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Quotient_t" [] []) ATermTable
att0
    Quotient_f -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Quotient_f" [] []) ATermTable
att0
    Remainder_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 "Remainder_e" [] []) ATermTable
att0
    Remainder_t -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Remainder_t" [] []) ATermTable
att0
    Remainder_f -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Remainder_f" [] []) ATermTable
att0
    Floor -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Floor" [] []) ATermTable
att0
    Ceiling -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Ceiling" [] []) ATermTable
att0
    Truncate -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Truncate" [] []) ATermTable
att0
    Round -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Round" [] []) ATermTable
att0
    To_int -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "To_int" [] []) ATermTable
att0
    To_rat -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "To_rat" [] []) ATermTable
att0
    To_real -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "To_real" [] []) ATermTable
att0
  fromShATermAux :: Int -> ATermTable -> (ATermTable, DefinedFunctor)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "UMinus" [] _ -> (ATermTable
att0, DefinedFunctor
UMinus)
    ShAAppl "Sum" [] _ -> (ATermTable
att0, DefinedFunctor
Sum)
    ShAAppl "Difference" [] _ -> (ATermTable
att0, DefinedFunctor
Difference)
    ShAAppl "Product" [] _ -> (ATermTable
att0, DefinedFunctor
Product)
    ShAAppl "Quotient" [] _ -> (ATermTable
att0, DefinedFunctor
Quotient)
    ShAAppl "Quotient_e" [] _ -> (ATermTable
att0, DefinedFunctor
Quotient_e)
    ShAAppl "Quotient_t" [] _ -> (ATermTable
att0, DefinedFunctor
Quotient_t)
    ShAAppl "Quotient_f" [] _ -> (ATermTable
att0, DefinedFunctor
Quotient_f)
    ShAAppl "Remainder_e" [] _ -> (ATermTable
att0, DefinedFunctor
Remainder_e)
    ShAAppl "Remainder_t" [] _ -> (ATermTable
att0, DefinedFunctor
Remainder_t)
    ShAAppl "Remainder_f" [] _ -> (ATermTable
att0, DefinedFunctor
Remainder_f)
    ShAAppl "Floor" [] _ -> (ATermTable
att0, DefinedFunctor
Floor)
    ShAAppl "Ceiling" [] _ -> (ATermTable
att0, DefinedFunctor
Ceiling)
    ShAAppl "Truncate" [] _ -> (ATermTable
att0, DefinedFunctor
Truncate)
    ShAAppl "Round" [] _ -> (ATermTable
att0, DefinedFunctor
Round)
    ShAAppl "To_int" [] _ -> (ATermTable
att0, DefinedFunctor
To_int)
    ShAAppl "To_rat" [] _ -> (ATermTable
att0, DefinedFunctor
To_rat)
    ShAAppl "To_real" [] _ -> (ATermTable
att0, DefinedFunctor
To_real)
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, DefinedFunctor)
forall a. String -> ShATerm -> a
fromShATermError "THF.As.DefinedFunctor" ShATerm
u

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

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

instance ShATermConvertible THF.As.Source where
  toShATermAux :: ATermTable -> Source -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Source
xv = case Source
xv of
    S_Dag_Source a :: DagSource
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> DagSource -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 DagSource
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 "S_Dag_Source" [Int
a'] []) ATermTable
att1
    S_Internal_Source a :: IntroType
a b :: OptionalInfo
b -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> IntroType -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 IntroType
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> OptionalInfo -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 OptionalInfo
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 "S_Internal_Source" [Int
a', Int
b'] []) ATermTable
att2
    S_External_Source a :: ExternalSource
a -> do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> ExternalSource -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 ExternalSource
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