{-# OPTIONS -w -O0 #-}
{-# LANGUAGE CPP, StandaloneDeriving, DeriveDataTypeable, DeriveGeneric #-}
module TPTP.ATC_TPTP () where
import ATC.AS_Annotation
import ATerm.Lib
import Common.AS_Annotation (item)
import Common.DefaultMorphism
import Common.IRI
import Common.Id
import Common.Id as Id
import Common.Json.Instances
import Data.Aeson(ToJSON, FromJSON)
import Data.Data
import GHC.Generics(Generic)
import Syntax.AS_Structured ()
import TPTP.AS
import TPTP.Morphism
import TPTP.Sign
import TPTP.Sublogic
import qualified Common.AS_Annotation as AS_Anno
import qualified Data.Map as Map
import qualified Data.Set as Set
instance ShATermConvertible TPTP.AS.BASIC_SPEC where
toShATermAux :: ATermTable -> BASIC_SPEC -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: BASIC_SPEC
xv = case BASIC_SPEC
xv of
Basic_spec a :: [Annoted TPTP]
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [Annoted TPTP] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [Annoted TPTP]
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 "Basic_spec" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, BASIC_SPEC)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Basic_spec" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, [Annoted TPTP])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [Annoted TPTP]
a') ->
(ATermTable
att1, [Annoted TPTP] -> BASIC_SPEC
Basic_spec [Annoted TPTP]
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, BASIC_SPEC)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.BASIC_SPEC" ShATerm
u
instance ShATermConvertible TPTP.AS.TPTP where
toShATermAux :: ATermTable -> TPTP -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TPTP
xv = case TPTP
xv of
TPTP a :: [TPTP_input]
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [TPTP_input] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [TPTP_input]
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" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, TPTP)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "TPTP" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, [TPTP_input])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [TPTP_input]
a') ->
(ATermTable
att1, [TPTP_input] -> TPTP
TPTP [TPTP_input]
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TPTP)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.TPTP" ShATerm
u
instance ShATermConvertible TPTP.AS.TPTP_input where
toShATermAux :: ATermTable -> TPTP_input -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TPTP_input
xv = case TPTP_input
xv of
Annotated_formula a :: Annotated_formula
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Annotated_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Annotated_formula
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 "Annotated_formula" [Int
a'] []) ATermTable
att1
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
fromShATermAux :: Int -> ATermTable -> (ATermTable, TPTP_input)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Annotated_formula" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Annotated_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Annotated_formula
a') ->
(ATermTable
att1, Annotated_formula -> TPTP_input
Annotated_formula Annotated_formula
a') }
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_input
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_input
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_input
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_input
TPTP_system_comment SystemComment
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TPTP_input)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.TPTP_input" ShATerm
u
instance ShATermConvertible TPTP.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 "TPTP.AS.Comment" ShATerm
u
instance ShATermConvertible TPTP.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 "TPTP.AS.DefinedComment" ShATerm
u
instance ShATermConvertible TPTP.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 "TPTP.AS.SystemComment" ShATerm
u
instance ShATermConvertible TPTP.AS.Annotated_formula where
toShATermAux :: ATermTable -> Annotated_formula -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Annotated_formula
xv = case Annotated_formula
xv of
AF_THF_Annotated a :: THF_annotated
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_annotated -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_annotated
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 "AF_THF_Annotated" [Int
a'] []) ATermTable
att1
AF_TFX_Annotated a :: TFX_annotated
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TFX_annotated -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TFX_annotated
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 "AF_TFX_Annotated" [Int
a'] []) ATermTable
att1
AF_TFF_Annotated a :: TFF_annotated
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TFF_annotated -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TFF_annotated
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 "AF_TFF_Annotated" [Int
a'] []) ATermTable
att1
AF_TCF_Annotated a :: TCF_annotated
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TCF_annotated -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TCF_annotated
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 "AF_TCF_Annotated" [Int
a'] []) ATermTable
att1
AF_FOF_Annotated a :: FOF_annotated
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> FOF_annotated -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 FOF_annotated
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 "AF_FOF_Annotated" [Int
a'] []) ATermTable
att1
AF_CNF_Annotated a :: CNF_annotated
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> CNF_annotated -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 CNF_annotated
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 "AF_CNF_Annotated" [Int
a'] []) ATermTable
att1
AF_TPI_Annotated a :: TPI_annotated
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TPI_annotated -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TPI_annotated
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 "AF_TPI_Annotated" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, Annotated_formula)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "AF_THF_Annotated" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_annotated)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_annotated
a') ->
(ATermTable
att1, THF_annotated -> Annotated_formula
AF_THF_Annotated THF_annotated
a') }
ShAAppl "AF_TFX_Annotated" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, TFX_annotated)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TFX_annotated
a') ->
(ATermTable
att1, TFX_annotated -> Annotated_formula
AF_TFX_Annotated TFX_annotated
a') }
ShAAppl "AF_TFF_Annotated" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, TFF_annotated)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TFF_annotated
a') ->
(ATermTable
att1, TFF_annotated -> Annotated_formula
AF_TFF_Annotated TFF_annotated
a') }
ShAAppl "AF_TCF_Annotated" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, TCF_annotated)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TCF_annotated
a') ->
(ATermTable
att1, TCF_annotated -> Annotated_formula
AF_TCF_Annotated TCF_annotated
a') }
ShAAppl "AF_FOF_Annotated" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, FOF_annotated)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: FOF_annotated
a') ->
(ATermTable
att1, FOF_annotated -> Annotated_formula
AF_FOF_Annotated FOF_annotated
a') }
ShAAppl "AF_CNF_Annotated" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, CNF_annotated)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: CNF_annotated
a') ->
(ATermTable
att1, CNF_annotated -> Annotated_formula
AF_CNF_Annotated CNF_annotated
a') }
ShAAppl "AF_TPI_Annotated" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, TPI_annotated)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TPI_annotated
a') ->
(ATermTable
att1, TPI_annotated -> Annotated_formula
AF_TPI_Annotated TPI_annotated
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Annotated_formula)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.Annotated_formula" ShATerm
u
instance ShATermConvertible TPTP.AS.TPI_annotated where
toShATermAux :: ATermTable -> TPI_annotated -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TPI_annotated
xv = case TPI_annotated
xv of
TPI_annotated a :: Name
a b :: Formula_role
b c :: FOF_formula
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 -> Formula_role -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Formula_role
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> FOF_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 FOF_formula
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 "TPI_annotated" [Int
a', Int
b', Int
c',
Int
d'] []) ATermTable
att4
fromShATermAux :: Int -> ATermTable -> (ATermTable, TPI_annotated)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "TPI_annotated" [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, Formula_role)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Formula_role
b') ->
case Int -> ATermTable -> (ATermTable, FOF_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: FOF_formula
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 -> Formula_role -> FOF_formula -> Annotations -> TPI_annotated
TPI_annotated Name
a' Formula_role
b' FOF_formula
c' Annotations
d') }}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TPI_annotated)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.TPI_annotated" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_annotated where
toShATermAux :: ATermTable -> THF_annotated -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_annotated
xv = case THF_annotated
xv of
THF_annotated a :: Name
a b :: Formula_role
b c :: THF_formula
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 -> Formula_role -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Formula_role
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> THF_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 THF_formula
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 "THF_annotated" [Int
a', Int
b', Int
c',
Int
d'] []) ATermTable
att4
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_annotated)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THF_annotated" [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, Formula_role)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Formula_role
b') ->
case Int -> ATermTable -> (ATermTable, THF_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: THF_formula
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 -> Formula_role -> THF_formula -> Annotations -> THF_annotated
THF_annotated Name
a' Formula_role
b' THF_formula
c' Annotations
d') }}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_annotated)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_annotated" ShATerm
u
instance ShATermConvertible TPTP.AS.TFX_annotated where
toShATermAux :: ATermTable -> TFX_annotated -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TFX_annotated
xv = case TFX_annotated
xv of
TFX_annotated a :: Name
a b :: Formula_role
b c :: TFX_formula
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 -> Formula_role -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Formula_role
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> TFX_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 TFX_formula
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 "TFX_annotated" [Int
a', Int
b', Int
c',
Int
d'] []) ATermTable
att4
fromShATermAux :: Int -> ATermTable -> (ATermTable, TFX_annotated)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "TFX_annotated" [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, Formula_role)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Formula_role
b') ->
case Int -> ATermTable -> (ATermTable, TFX_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: TFX_formula
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 -> Formula_role -> TFX_formula -> Annotations -> TFX_annotated
TFX_annotated Name
a' Formula_role
b' TFX_formula
c' Annotations
d') }}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TFX_annotated)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.TFX_annotated" ShATerm
u
instance ShATermConvertible TPTP.AS.TFF_annotated where
toShATermAux :: ATermTable -> TFF_annotated -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TFF_annotated
xv = case TFF_annotated
xv of
TFF_annotated a :: Name
a b :: Formula_role
b c :: TFF_formula
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 -> Formula_role -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Formula_role
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> TFF_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 TFF_formula
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 "TFF_annotated" [Int
a', Int
b', Int
c',
Int
d'] []) ATermTable
att4
fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_annotated)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "TFF_annotated" [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, Formula_role)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Formula_role
b') ->
case Int -> ATermTable -> (ATermTable, TFF_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: TFF_formula
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 -> Formula_role -> TFF_formula -> Annotations -> TFF_annotated
TFF_annotated Name
a' Formula_role
b' TFF_formula
c' Annotations
d') }}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TFF_annotated)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.TFF_annotated" ShATerm
u
instance ShATermConvertible TPTP.AS.TCF_annotated where
toShATermAux :: ATermTable -> TCF_annotated -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TCF_annotated
xv = case TCF_annotated
xv of
TCF_annotated a :: Name
a b :: Formula_role
b c :: TCF_formula
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 -> Formula_role -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Formula_role
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> TCF_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 TCF_formula
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 "TCF_annotated" [Int
a', Int
b', Int
c',
Int
d'] []) ATermTable
att4
fromShATermAux :: Int -> ATermTable -> (ATermTable, TCF_annotated)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "TCF_annotated" [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, Formula_role)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Formula_role
b') ->
case Int -> ATermTable -> (ATermTable, TCF_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: TCF_formula
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 -> Formula_role -> TCF_formula -> Annotations -> TCF_annotated
TCF_annotated Name
a' Formula_role
b' TCF_formula
c' Annotations
d') }}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TCF_annotated)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.TCF_annotated" ShATerm
u
instance ShATermConvertible TPTP.AS.FOF_annotated where
toShATermAux :: ATermTable -> FOF_annotated -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: FOF_annotated
xv = case FOF_annotated
xv of
FOF_annotated a :: Name
a b :: Formula_role
b c :: FOF_formula
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 -> Formula_role -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Formula_role
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> FOF_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 FOF_formula
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 "FOF_annotated" [Int
a', Int
b', Int
c',
Int
d'] []) ATermTable
att4
fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_annotated)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "FOF_annotated" [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, Formula_role)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Formula_role
b') ->
case Int -> ATermTable -> (ATermTable, FOF_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: FOF_formula
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 -> Formula_role -> FOF_formula -> Annotations -> FOF_annotated
FOF_annotated Name
a' Formula_role
b' FOF_formula
c' Annotations
d') }}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, FOF_annotated)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.FOF_annotated" ShATerm
u
instance ShATermConvertible TPTP.AS.CNF_annotated where
toShATermAux :: ATermTable -> CNF_annotated -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: CNF_annotated
xv = case CNF_annotated
xv of
CNF_annotated a :: Name
a b :: Formula_role
b c :: CNF_formula
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 -> Formula_role -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 Formula_role
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> CNF_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 CNF_formula
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 "CNF_annotated" [Int
a', Int
b', Int
c',
Int
d'] []) ATermTable
att4
fromShATermAux :: Int -> ATermTable -> (ATermTable, CNF_annotated)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "CNF_annotated" [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, Formula_role)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: Formula_role
b') ->
case Int -> ATermTable -> (ATermTable, CNF_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: CNF_formula
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 -> Formula_role -> CNF_formula -> Annotations -> CNF_annotated
CNF_annotated Name
a' Formula_role
b' CNF_formula
c' Annotations
d') }}}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, CNF_annotated)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.CNF_annotated" ShATerm
u
instance ShATermConvertible TPTP.AS.Annotations where
toShATermAux :: ATermTable -> Annotations -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Annotations
xv = case Annotations
xv of
Annotations a :: Maybe (Source, Optional_info)
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Maybe (Source, Optional_info) -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Maybe (Source, Optional_info)
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 "Annotations" [Int
a'] []) ATermTable
att1
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] _ ->
case Int -> ATermTable -> (ATermTable, Maybe (Source, Optional_info))
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Maybe (Source, Optional_info)
a') ->
(ATermTable
att1, Maybe (Source, Optional_info) -> Annotations
Annotations Maybe (Source, Optional_info)
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Annotations)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.Annotations" ShATerm
u
instance ShATermConvertible TPTP.AS.Formula_role where
toShATermAux :: ATermTable -> Formula_role -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: Formula_role
xv = case Formula_role
xv of
Axiom -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Axiom" [] []) ATermTable
att0
Hypothesis -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Hypothesis" [] []) ATermTable
att0
Definition -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Definition" [] []) ATermTable
att0
Assumption -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Assumption" [] []) ATermTable
att0
Lemma -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Lemma" [] []) ATermTable
att0
Theorem -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Theorem" [] []) ATermTable
att0
Corollary -> (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "Corollary" [] []) 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
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
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
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
Other_formula_role 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 "Other_formula_role" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, Formula_role)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "Axiom" [] _ -> (ATermTable
att0, Formula_role
Axiom)
ShAAppl "Hypothesis" [] _ -> (ATermTable
att0, Formula_role
Hypothesis)
ShAAppl "Definition" [] _ -> (ATermTable
att0, Formula_role
Definition)
ShAAppl "Assumption" [] _ -> (ATermTable
att0, Formula_role
Assumption)
ShAAppl "Lemma" [] _ -> (ATermTable
att0, Formula_role
Lemma)
ShAAppl "Theorem" [] _ -> (ATermTable
att0, Formula_role
Theorem)
ShAAppl "Corollary" [] _ -> (ATermTable
att0, Formula_role
Corollary)
ShAAppl "Conjecture" [] _ -> (ATermTable
att0, Formula_role
Conjecture)
ShAAppl "Negated_conjecture" [] _ -> (ATermTable
att0, Formula_role
Negated_conjecture)
ShAAppl "Plain" [] _ -> (ATermTable
att0, Formula_role
Plain)
ShAAppl "Type" [] _ -> (ATermTable
att0, Formula_role
Type)
ShAAppl "Fi_domain" [] _ -> (ATermTable
att0, Formula_role
Fi_domain)
ShAAppl "Fi_functors" [] _ -> (ATermTable
att0, Formula_role
Fi_functors)
ShAAppl "Fi_predicates" [] _ -> (ATermTable
att0, Formula_role
Fi_predicates)
ShAAppl "Unknown" [] _ -> (ATermTable
att0, Formula_role
Unknown)
ShAAppl "Other_formula_role" [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 -> Formula_role
Other_formula_role Token
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, Formula_role)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.Formula_role" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_formula where
toShATermAux :: ATermTable -> THF_formula -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_formula
xv = case THF_formula
xv of
THFF_logic a :: THF_logic_formula
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_logic_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_logic_formula
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 "THFF_logic" [Int
a'] []) ATermTable
att1
THFF_sequent a :: THF_sequent
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_sequent -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_sequent
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 "THFF_sequent" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_formula)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THFF_logic" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_logic_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_logic_formula
a') ->
(ATermTable
att1, THF_logic_formula -> THF_formula
THFF_logic THF_logic_formula
a') }
ShAAppl "THFF_sequent" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_sequent)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_sequent
a') ->
(ATermTable
att1, THF_sequent -> THF_formula
THFF_sequent THF_sequent
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_formula)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_formula" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_logic_formula where
toShATermAux :: ATermTable -> THF_logic_formula -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_logic_formula
xv = case THF_logic_formula
xv of
THFLF_binary a :: THF_binary_formula
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_binary_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_binary_formula
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 "THFLF_binary" [Int
a'] []) ATermTable
att1
THFLF_unitary a :: THF_unitary_formula
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_unitary_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_unitary_formula
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 "THFLF_unitary" [Int
a'] []) ATermTable
att1
THFLF_type a :: THF_type_formula
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_type_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_type_formula
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 "THFLF_type" [Int
a'] []) ATermTable
att1
THFLF_subtype a :: THF_subtype
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_subtype -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_subtype
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 "THFLF_subtype" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_logic_formula)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THFLF_binary" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_binary_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_binary_formula
a') ->
(ATermTable
att1, THF_binary_formula -> THF_logic_formula
THFLF_binary THF_binary_formula
a') }
ShAAppl "THFLF_unitary" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_unitary_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_unitary_formula
a') ->
(ATermTable
att1, THF_unitary_formula -> THF_logic_formula
THFLF_unitary THF_unitary_formula
a') }
ShAAppl "THFLF_type" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_type_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_type_formula
a') ->
(ATermTable
att1, THF_type_formula -> THF_logic_formula
THFLF_type THF_type_formula
a') }
ShAAppl "THFLF_subtype" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_subtype)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_subtype
a') ->
(ATermTable
att1, THF_subtype -> THF_logic_formula
THFLF_subtype THF_subtype
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_logic_formula)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_logic_formula" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_binary_formula where
toShATermAux :: ATermTable -> THF_binary_formula -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_binary_formula
xv = case THF_binary_formula
xv of
THFBF_pair a :: THF_binary_pair
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_binary_pair -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_binary_pair
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 "THFBF_pair" [Int
a'] []) ATermTable
att1
THFBF_tuple a :: THF_binary_tuple
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_binary_tuple -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_binary_tuple
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 "THFBF_tuple" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_binary_formula)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THFBF_pair" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_binary_pair)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_binary_pair
a') ->
(ATermTable
att1, THF_binary_pair -> THF_binary_formula
THFBF_pair THF_binary_pair
a') }
ShAAppl "THFBF_tuple" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_binary_tuple)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_binary_tuple
a') ->
(ATermTable
att1, THF_binary_tuple -> THF_binary_formula
THFBF_tuple THF_binary_tuple
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_binary_formula)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_binary_formula" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_binary_pair where
toShATermAux :: ATermTable -> THF_binary_pair -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_binary_pair
xv = case THF_binary_pair
xv of
THF_binary_pair a :: THF_pair_connective
a b :: THF_unitary_formula
b c :: THF_unitary_formula
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_pair_connective -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_pair_connective
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> THF_unitary_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 THF_unitary_formula
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> THF_unitary_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 THF_unitary_formula
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 "THF_binary_pair" [Int
a', Int
b', Int
c'] []) ATermTable
att3
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_binary_pair)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THF_binary_pair" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, THF_pair_connective)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_pair_connective
a') ->
case Int -> ATermTable -> (ATermTable, THF_unitary_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: THF_unitary_formula
b') ->
case Int -> ATermTable -> (ATermTable, THF_unitary_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: THF_unitary_formula
c') ->
(ATermTable
att3, THF_pair_connective
-> THF_unitary_formula -> THF_unitary_formula -> THF_binary_pair
THF_binary_pair THF_pair_connective
a' THF_unitary_formula
b' THF_unitary_formula
c') }}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_binary_pair)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_binary_pair" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_binary_tuple where
toShATermAux :: ATermTable -> THF_binary_tuple -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_binary_tuple
xv = case THF_binary_tuple
xv of
THFBT_or a :: THF_or_formula
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_or_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_or_formula
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 "THFBT_or" [Int
a'] []) ATermTable
att1
THFBT_and a :: THF_or_formula
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_or_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_or_formula
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 "THFBT_and" [Int
a'] []) ATermTable
att1
THFBT_apply a :: THF_or_formula
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_or_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_or_formula
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 "THFBT_apply" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_binary_tuple)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THFBT_or" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_or_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_or_formula
a') ->
(ATermTable
att1, THF_or_formula -> THF_binary_tuple
THFBT_or THF_or_formula
a') }
ShAAppl "THFBT_and" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_or_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_or_formula
a') ->
(ATermTable
att1, THF_or_formula -> THF_binary_tuple
THFBT_and THF_or_formula
a') }
ShAAppl "THFBT_apply" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_or_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_or_formula
a') ->
(ATermTable
att1, THF_or_formula -> THF_binary_tuple
THFBT_apply THF_or_formula
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_binary_tuple)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_binary_tuple" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_unitary_formula where
toShATermAux :: ATermTable -> THF_unitary_formula -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_unitary_formula
xv = case THF_unitary_formula
xv of
THFUF_quantified a :: THF_quantified_formula
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_quantified_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_quantified_formula
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 "THFUF_quantified" [Int
a'] []) ATermTable
att1
THFUF_unary a :: THF_unary_formula
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_unary_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_unary_formula
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 "THFUF_unary" [Int
a'] []) ATermTable
att1
THFUF_atom a :: THF_atom
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_atom -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_atom
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 "THFUF_atom" [Int
a'] []) ATermTable
att1
THFUF_conditional a :: THF_conditional
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_conditional -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_conditional
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 "THFUF_conditional" [Int
a'] []) ATermTable
att1
THFUF_let a :: THF_let
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_let -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_let
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 "THFUF_let" [Int
a'] []) ATermTable
att1
THFUF_tuple a :: THF_tuple
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_tuple -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_tuple
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 "THFUF_tuple" [Int
a'] []) ATermTable
att1
THFUF_logic a :: THF_logic_formula
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_logic_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_logic_formula
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 "THFUF_logic" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_unitary_formula)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THFUF_quantified" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_quantified_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_quantified_formula
a') ->
(ATermTable
att1, THF_quantified_formula -> THF_unitary_formula
THFUF_quantified THF_quantified_formula
a') }
ShAAppl "THFUF_unary" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_unary_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_unary_formula
a') ->
(ATermTable
att1, THF_unary_formula -> THF_unitary_formula
THFUF_unary THF_unary_formula
a') }
ShAAppl "THFUF_atom" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_atom)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_atom
a') ->
(ATermTable
att1, THF_atom -> THF_unitary_formula
THFUF_atom THF_atom
a') }
ShAAppl "THFUF_conditional" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_conditional)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_conditional
a') ->
(ATermTable
att1, THF_conditional -> THF_unitary_formula
THFUF_conditional THF_conditional
a') }
ShAAppl "THFUF_let" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_let)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_let
a') ->
(ATermTable
att1, THF_let -> THF_unitary_formula
THFUF_let THF_let
a') }
ShAAppl "THFUF_tuple" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_tuple)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_tuple
a') ->
(ATermTable
att1, THF_tuple -> THF_unitary_formula
THFUF_tuple THF_tuple
a') }
ShAAppl "THFUF_logic" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_logic_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_logic_formula
a') ->
(ATermTable
att1, THF_logic_formula -> THF_unitary_formula
THFUF_logic THF_logic_formula
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_unitary_formula)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_unitary_formula" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_quantified_formula where
toShATermAux :: ATermTable -> THF_quantified_formula -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_quantified_formula
xv = case THF_quantified_formula
xv of
THF_quantified_formula a :: THF_quantification
a b :: THF_unitary_formula
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_quantification -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_quantification
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> THF_unitary_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 THF_unitary_formula
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 "THF_quantified_formula" [Int
a',
Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_quantified_formula)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THF_quantified_formula" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, THF_quantification)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_quantification
a') ->
case Int -> ATermTable -> (ATermTable, THF_unitary_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: THF_unitary_formula
b') ->
(ATermTable
att2, THF_quantification -> THF_unitary_formula -> THF_quantified_formula
THF_quantified_formula THF_quantification
a' THF_unitary_formula
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_quantified_formula)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_quantified_formula" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_quantification where
toShATermAux :: ATermTable -> THF_quantification -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_quantification
xv = case THF_quantification
xv of
THF_quantification a :: THF_quantifier
a b :: THF_variable_list
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_quantifier -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_quantifier
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> THF_variable_list -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 THF_variable_list
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 "THF_quantification" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_quantification)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THF_quantification" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, THF_quantifier)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_quantifier
a') ->
case Int -> ATermTable -> (ATermTable, THF_variable_list)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: THF_variable_list
b') ->
(ATermTable
att2, THF_quantifier -> THF_variable_list -> THF_quantification
THF_quantification THF_quantifier
a' THF_variable_list
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_quantification)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_quantification" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_variable where
toShATermAux :: ATermTable -> THF_variable -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_variable
xv = case THF_variable
xv of
THFV_typed a :: THF_typed_variable
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_typed_variable -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_typed_variable
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 "THFV_typed" [Int
a'] []) ATermTable
att1
THFV_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 "THFV_variable" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_variable)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THFV_typed" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_typed_variable)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_typed_variable
a') ->
(ATermTable
att1, THF_typed_variable -> THF_variable
THFV_typed THF_typed_variable
a') }
ShAAppl "THFV_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 -> THF_variable
THFV_variable Token
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_variable)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_variable" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_typed_variable where
toShATermAux :: ATermTable -> THF_typed_variable -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_typed_variable
xv = case THF_typed_variable
xv of
THF_typed_variable a :: Token
a b :: THF_top_level_type
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 -> THF_top_level_type -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 THF_top_level_type
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 "THF_typed_variable" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_typed_variable)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "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, THF_top_level_type)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: THF_top_level_type
b') ->
(ATermTable
att2, Token -> THF_top_level_type -> THF_typed_variable
THF_typed_variable Token
a' THF_top_level_type
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_typed_variable)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_typed_variable" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_unary_formula where
toShATermAux :: ATermTable -> THF_unary_formula -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_unary_formula
xv = case THF_unary_formula
xv of
THF_unary_formula a :: THF_unary_connective
a b :: THF_logic_formula
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_unary_connective -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_unary_connective
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> THF_logic_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 THF_logic_formula
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 "THF_unary_formula" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_unary_formula)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THF_unary_formula" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, THF_unary_connective)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_unary_connective
a') ->
case Int -> ATermTable -> (ATermTable, THF_logic_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: THF_logic_formula
b') ->
(ATermTable
att2, THF_unary_connective -> THF_logic_formula -> THF_unary_formula
THF_unary_formula THF_unary_connective
a' THF_logic_formula
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_unary_formula)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_unary_formula" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_atom where
toShATermAux :: ATermTable -> THF_atom -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_atom
xv = case THF_atom
xv of
THF_atom_function a :: THF_function
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_function -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_function
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 "THF_atom_function" [Int
a'] []) ATermTable
att1
THF_atom_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 "THF_atom_variable" [Int
a'] []) ATermTable
att1
THF_atom_defined a :: Defined_term
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Defined_term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Defined_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 "THF_atom_defined" [Int
a'] []) ATermTable
att1
THF_atom_conn a :: THF_conn_term
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_conn_term -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_conn_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 "THF_atom_conn" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_atom)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THF_atom_function" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_function)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_function
a') ->
(ATermTable
att1, THF_function -> THF_atom
THF_atom_function THF_function
a') }
ShAAppl "THF_atom_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 -> THF_atom
THF_atom_variable Token
a') }
ShAAppl "THF_atom_defined" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Defined_term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Defined_term
a') ->
(ATermTable
att1, Defined_term -> THF_atom
THF_atom_defined Defined_term
a') }
ShAAppl "THF_atom_conn" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_conn_term)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_conn_term
a') ->
(ATermTable
att1, THF_conn_term -> THF_atom
THF_atom_conn THF_conn_term
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_atom)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_atom" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_function where
toShATermAux :: ATermTable -> THF_function -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_function
xv = case THF_function
xv of
THFF_atom a :: Atom
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Atom -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Atom
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 "THFF_atom" [Int
a'] []) ATermTable
att1
THFF_functor a :: Token
a b :: [THF_logic_formula]
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 -> [THF_logic_formula] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [THF_logic_formula]
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 "THFF_functor" [Int
a', Int
b'] []) ATermTable
att2
THFF_defined a :: Defined_functor
a b :: [THF_logic_formula]
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Defined_functor -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Defined_functor
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> [THF_logic_formula] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [THF_logic_formula]
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 "THFF_defined" [Int
a', Int
b'] []) ATermTable
att2
THFF_system a :: Token
a b :: [THF_logic_formula]
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 -> [THF_logic_formula] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 [THF_logic_formula]
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 "THFF_system" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_function)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THFF_atom" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Atom)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Atom
a') ->
(ATermTable
att1, Atom -> THF_function
THFF_atom Atom
a') }
ShAAppl "THFF_functor" [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, [THF_logic_formula])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [THF_logic_formula]
b') ->
(ATermTable
att2, Token -> [THF_logic_formula] -> THF_function
THFF_functor Token
a' [THF_logic_formula]
b') }}
ShAAppl "THFF_defined" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, Defined_functor)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Defined_functor
a') ->
case Int -> ATermTable -> (ATermTable, [THF_logic_formula])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [THF_logic_formula]
b') ->
(ATermTable
att2, Defined_functor -> [THF_logic_formula] -> THF_function
THFF_defined Defined_functor
a' [THF_logic_formula]
b') }}
ShAAppl "THFF_system" [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, [THF_logic_formula])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: [THF_logic_formula]
b') ->
(ATermTable
att2, Token -> [THF_logic_formula] -> THF_function
THFF_system Token
a' [THF_logic_formula]
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_function)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_function" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_conn_term where
toShATermAux :: ATermTable -> THF_conn_term -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_conn_term
xv = case THF_conn_term
xv of
THFC_pair a :: THF_pair_connective
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_pair_connective -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_pair_connective
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 "THFC_pair" [Int
a'] []) ATermTable
att1
THFC_assoc a :: Assoc_connective
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> Assoc_connective -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 Assoc_connective
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 "THFC_assoc" [Int
a'] []) ATermTable
att1
THFC_unary a :: THF_unary_connective
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_unary_connective -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_unary_connective
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 "THFC_unary" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_conn_term)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THFC_pair" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_pair_connective)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_pair_connective
a') ->
(ATermTable
att1, THF_pair_connective -> THF_conn_term
THFC_pair THF_pair_connective
a') }
ShAAppl "THFC_assoc" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, Assoc_connective)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: Assoc_connective
a') ->
(ATermTable
att1, Assoc_connective -> THF_conn_term
THFC_assoc Assoc_connective
a') }
ShAAppl "THFC_unary" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_unary_connective)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_unary_connective
a') ->
(ATermTable
att1, THF_unary_connective -> THF_conn_term
THFC_unary THF_unary_connective
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_conn_term)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_conn_term" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_conditional where
toShATermAux :: ATermTable -> THF_conditional -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_conditional
xv = case THF_conditional
xv of
THF_conditional a :: THF_logic_formula
a b :: THF_logic_formula
b c :: THF_logic_formula
c -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_logic_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_logic_formula
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> THF_logic_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 THF_logic_formula
b
(att3 :: ATermTable
att3, c' :: Int
c') <- ATermTable -> THF_logic_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att2 THF_logic_formula
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 "THF_conditional" [Int
a', Int
b', Int
c'] []) ATermTable
att3
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_conditional)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THF_conditional" [a :: Int
a, b :: Int
b, c :: Int
c] _ ->
case Int -> ATermTable -> (ATermTable, THF_logic_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_logic_formula
a') ->
case Int -> ATermTable -> (ATermTable, THF_logic_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: THF_logic_formula
b') ->
case Int -> ATermTable -> (ATermTable, THF_logic_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
c ATermTable
att2 of
{ (att3 :: ATermTable
att3, c' :: THF_logic_formula
c') ->
(ATermTable
att3, THF_logic_formula
-> THF_logic_formula -> THF_logic_formula -> THF_conditional
THF_conditional THF_logic_formula
a' THF_logic_formula
b' THF_logic_formula
c') }}}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_conditional)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_conditional" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_let where
toShATermAux :: ATermTable -> THF_let -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_let
xv = case THF_let
xv of
THF_let a :: THF_let_defns
a b :: THF_formula
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_let_defns -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_let_defns
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> THF_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 THF_formula
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 "THF_let" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_let)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THF_let" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, THF_let_defns)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_let_defns
a') ->
case Int -> ATermTable -> (ATermTable, THF_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: THF_formula
b') ->
(ATermTable
att2, THF_let_defns -> THF_formula -> THF_let
THF_let THF_let_defns
a' THF_formula
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_let)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_let" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_let_defns where
toShATermAux :: ATermTable -> THF_let_defns -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_let_defns
xv = case THF_let_defns
xv of
THFLD_single a :: THF_let_defn
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_let_defn -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_let_defn
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 "THFLD_single" [Int
a'] []) ATermTable
att1
THFLD_many a :: THF_let_defn_list
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_let_defn_list -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_let_defn_list
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 "THFLD_many" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_let_defns)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THFLD_single" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_let_defn)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_let_defn
a') ->
(ATermTable
att1, THF_let_defn -> THF_let_defns
THFLD_single THF_let_defn
a') }
ShAAppl "THFLD_many" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_let_defn_list)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_let_defn_list
a') ->
(ATermTable
att1, THF_let_defn_list -> THF_let_defns
THFLD_many THF_let_defn_list
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_let_defns)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_let_defns" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_let_defn where
toShATermAux :: ATermTable -> THF_let_defn -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_let_defn
xv = case THF_let_defn
xv of
THFLD_quantified a :: THF_let_quantified_defn
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_let_quantified_defn -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_let_quantified_defn
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 "THFLD_quantified" [Int
a'] []) ATermTable
att1
THFLD_plain a :: THF_let_plain_defn
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_let_plain_defn -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_let_plain_defn
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 "THFLD_plain" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_let_defn)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THFLD_quantified" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_let_quantified_defn)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_let_quantified_defn
a') ->
(ATermTable
att1, THF_let_quantified_defn -> THF_let_defn
THFLD_quantified THF_let_quantified_defn
a') }
ShAAppl "THFLD_plain" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_let_plain_defn)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_let_plain_defn
a') ->
(ATermTable
att1, THF_let_plain_defn -> THF_let_defn
THFLD_plain THF_let_plain_defn
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_let_defn)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_let_defn" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_let_quantified_defn where
toShATermAux :: ATermTable -> THF_let_quantified_defn -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_let_quantified_defn
xv = case THF_let_quantified_defn
xv of
THF_let_quantified_defn a :: THF_quantification
a b :: THF_let_plain_defn
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_quantification -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_quantification
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> THF_let_plain_defn -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 THF_let_plain_defn
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 "THF_let_quantified_defn" [Int
a',
Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_let_quantified_defn)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THF_let_quantified_defn" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, THF_quantification)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_quantification
a') ->
case Int -> ATermTable -> (ATermTable, THF_let_plain_defn)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: THF_let_plain_defn
b') ->
(ATermTable
att2, THF_quantification -> THF_let_plain_defn -> THF_let_quantified_defn
THF_let_quantified_defn THF_quantification
a' THF_let_plain_defn
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_let_quantified_defn)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_let_quantified_defn" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_let_plain_defn where
toShATermAux :: ATermTable -> THF_let_plain_defn -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_let_plain_defn
xv = case THF_let_plain_defn
xv of
THF_let_plain_defn a :: THF_let_defn_LHS
a b :: THF_formula
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_let_defn_LHS -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_let_defn_LHS
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> THF_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 THF_formula
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 "THF_let_plain_defn" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_let_plain_defn)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THF_let_plain_defn" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, THF_let_defn_LHS)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_let_defn_LHS
a') ->
case Int -> ATermTable -> (ATermTable, THF_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: THF_formula
b') ->
(ATermTable
att2, THF_let_defn_LHS -> THF_formula -> THF_let_plain_defn
THF_let_plain_defn THF_let_defn_LHS
a' THF_formula
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_let_plain_defn)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_let_plain_defn" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_let_defn_LHS where
toShATermAux :: ATermTable -> THF_let_defn_LHS -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_let_defn_LHS
xv = case THF_let_defn_LHS
xv of
THFLDL_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 "THFLDL_constant" [Int
a'] []) ATermTable
att1
THFLDL_functor a :: Token
a b :: FOF_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 -> FOF_arguments -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 FOF_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 "THFLDL_functor" [Int
a', Int
b'] []) ATermTable
att2
THFLDL_tuple a :: THF_tuple
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_tuple -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_tuple
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 "THFLDL_tuple" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_let_defn_LHS)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THFLDL_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 -> THF_let_defn_LHS
THFLDL_constant Token
a') }
ShAAppl "THFLDL_functor" [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, FOF_arguments)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: FOF_arguments
b') ->
(ATermTable
att2, Token -> FOF_arguments -> THF_let_defn_LHS
THFLDL_functor Token
a' FOF_arguments
b') }}
ShAAppl "THFLDL_tuple" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_tuple)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_tuple
a') ->
(ATermTable
att1, THF_tuple -> THF_let_defn_LHS
THFLDL_tuple THF_tuple
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_let_defn_LHS)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_let_defn_LHS" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_type_formula where
toShATermAux :: ATermTable -> THF_type_formula -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_type_formula
xv = case THF_type_formula
xv of
THFTF_typeable a :: THF_typeable_formula
a b :: THF_top_level_type
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_typeable_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_typeable_formula
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> THF_top_level_type -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 THF_top_level_type
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 "THFTF_typeable" [Int
a', Int
b'] []) ATermTable
att2
THFTF_constant a :: Token
a b :: THF_top_level_type
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 -> THF_top_level_type -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 THF_top_level_type
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 "THFTF_constant" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_type_formula)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THFTF_typeable" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, THF_typeable_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_typeable_formula
a') ->
case Int -> ATermTable -> (ATermTable, THF_top_level_type)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: THF_top_level_type
b') ->
(ATermTable
att2, THF_typeable_formula -> THF_top_level_type -> THF_type_formula
THFTF_typeable THF_typeable_formula
a' THF_top_level_type
b') }}
ShAAppl "THFTF_constant" [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, THF_top_level_type)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: THF_top_level_type
b') ->
(ATermTable
att2, Token -> THF_top_level_type -> THF_type_formula
THFTF_constant Token
a' THF_top_level_type
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_type_formula)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_type_formula" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_typeable_formula where
toShATermAux :: ATermTable -> THF_typeable_formula -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_typeable_formula
xv = case THF_typeable_formula
xv of
THFTF_atom a :: THF_atom
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_atom -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_atom
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 "THFTF_atom" [Int
a'] []) ATermTable
att1
THFTF_logic a :: THF_logic_formula
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_logic_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_logic_formula
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 "THFTF_logic" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_typeable_formula)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THFTF_atom" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_atom)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_atom
a') ->
(ATermTable
att1, THF_atom -> THF_typeable_formula
THFTF_atom THF_atom
a') }
ShAAppl "THFTF_logic" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_logic_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_logic_formula
a') ->
(ATermTable
att1, THF_logic_formula -> THF_typeable_formula
THFTF_logic THF_logic_formula
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_typeable_formula)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_typeable_formula" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_subtype where
toShATermAux :: ATermTable -> THF_subtype -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_subtype
xv = case THF_subtype
xv of
THF_subtype a :: THF_atom
a b :: THF_atom
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_atom -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_atom
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> THF_atom -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 THF_atom
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 "THF_subtype" [Int
a', Int
b'] []) ATermTable
att2
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_subtype)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THF_subtype" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, THF_atom)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_atom
a') ->
case Int -> ATermTable -> (ATermTable, THF_atom)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: THF_atom
b') ->
(ATermTable
att2, THF_atom -> THF_atom -> THF_subtype
THF_subtype THF_atom
a' THF_atom
b') }}
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_subtype)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_subtype" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_top_level_type where
toShATermAux :: ATermTable -> THF_top_level_type -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_top_level_type
xv = case THF_top_level_type
xv of
THFTLT_unitary a :: THF_unitary_type
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_unitary_type -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_unitary_type
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 "THFTLT_unitary" [Int
a'] []) ATermTable
att1
THFTLT_mapping a :: THF_mapping_type
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_mapping_type -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_mapping_type
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 "THFTLT_mapping" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_top_level_type)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THFTLT_unitary" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_unitary_type)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_unitary_type
a') ->
(ATermTable
att1, THF_unitary_type -> THF_top_level_type
THFTLT_unitary THF_unitary_type
a') }
ShAAppl "THFTLT_mapping" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_mapping_type)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_mapping_type
a') ->
(ATermTable
att1, THF_mapping_type -> THF_top_level_type
THFTLT_mapping THF_mapping_type
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_top_level_type)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_top_level_type" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_unitary_type where
toShATermAux :: ATermTable -> THF_unitary_type -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_unitary_type
xv = case THF_unitary_type
xv of
THFUT_unitary a :: THF_unitary_formula
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_unitary_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_unitary_formula
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 "THFUT_unitary" [Int
a'] []) ATermTable
att1
THFUT_binary a :: THF_binary_type
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_binary_type -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_binary_type
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 "THFUT_binary" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_unitary_type)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THFUT_unitary" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_unitary_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_unitary_formula
a') ->
(ATermTable
att1, THF_unitary_formula -> THF_unitary_type
THFUT_unitary THF_unitary_formula
a') }
ShAAppl "THFUT_binary" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_binary_type)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_binary_type
a') ->
(ATermTable
att1, THF_binary_type -> THF_unitary_type
THFUT_binary THF_binary_type
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_unitary_type)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_unitary_type" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_binary_type where
toShATermAux :: ATermTable -> THF_binary_type -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_binary_type
xv = case THF_binary_type
xv of
THFBT_mapping a :: THF_mapping_type
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_mapping_type -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_mapping_type
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 "THFBT_mapping" [Int
a'] []) ATermTable
att1
THFBT_xprod a :: THF_mapping_type
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_mapping_type -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_mapping_type
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 "THFBT_xprod" [Int
a'] []) ATermTable
att1
THFBT_union a :: THF_mapping_type
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_mapping_type -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_mapping_type
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 "THFBT_union" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_binary_type)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THFBT_mapping" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_mapping_type)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_mapping_type
a') ->
(ATermTable
att1, THF_mapping_type -> THF_binary_type
THFBT_mapping THF_mapping_type
a') }
ShAAppl "THFBT_xprod" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_mapping_type)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_mapping_type
a') ->
(ATermTable
att1, THF_mapping_type -> THF_binary_type
THFBT_xprod THF_mapping_type
a') }
ShAAppl "THFBT_union" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_mapping_type)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_mapping_type
a') ->
(ATermTable
att1, THF_mapping_type -> THF_binary_type
THFBT_union THF_mapping_type
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_binary_type)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_binary_type" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_sequent where
toShATermAux :: ATermTable -> THF_sequent -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_sequent
xv = case THF_sequent
xv of
THFS_plain a :: THF_tuple
a b :: THF_tuple
b -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_tuple -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_tuple
a
(att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> THF_tuple -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 THF_tuple
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 "THFS_plain" [Int
a', Int
b'] []) ATermTable
att2
THFS_parens a :: THF_sequent
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_sequent -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_sequent
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 "THFS_parens" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_sequent)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THFS_plain" [a :: Int
a, b :: Int
b] _ ->
case Int -> ATermTable -> (ATermTable, THF_tuple)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_tuple
a') ->
case Int -> ATermTable -> (ATermTable, THF_tuple)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of
{ (att2 :: ATermTable
att2, b' :: THF_tuple
b') ->
(ATermTable
att2, THF_tuple -> THF_tuple -> THF_sequent
THFS_plain THF_tuple
a' THF_tuple
b') }}
ShAAppl "THFS_parens" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_sequent)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_sequent
a') ->
(ATermTable
att1, THF_sequent -> THF_sequent
THFS_parens THF_sequent
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_sequent)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_sequent" ShATerm
u
instance ShATermConvertible TPTP.AS.THF_tuple where
toShATermAux :: ATermTable -> THF_tuple -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: THF_tuple
xv = case THF_tuple
xv of
THF_tuple a :: [THF_logic_formula]
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> [THF_logic_formula] -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 [THF_logic_formula]
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 "THF_tuple" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_tuple)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "THF_tuple" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, [THF_logic_formula])
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: [THF_logic_formula]
a') ->
(ATermTable
att1, [THF_logic_formula] -> THF_tuple
THF_tuple [THF_logic_formula]
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, THF_tuple)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.THF_tuple" ShATerm
u
instance ShATermConvertible TPTP.AS.TFX_formula where
toShATermAux :: ATermTable -> TFX_formula -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TFX_formula
xv = case TFX_formula
xv of
TFXF_logic a :: TFX_logic_formula
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TFX_logic_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TFX_logic_formula
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 "TFXF_logic" [Int
a'] []) ATermTable
att1
TFXF_sequent a :: THF_sequent
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_sequent -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_sequent
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 "TFXF_sequent" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, TFX_formula)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "TFXF_logic" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, TFX_logic_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TFX_logic_formula
a') ->
(ATermTable
att1, TFX_logic_formula -> TFX_formula
TFXF_logic TFX_logic_formula
a') }
ShAAppl "TFXF_sequent" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_sequent)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_sequent
a') ->
(ATermTable
att1, THF_sequent -> TFX_formula
TFXF_sequent THF_sequent
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TFX_formula)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.TFX_formula" ShATerm
u
instance ShATermConvertible TPTP.AS.TFX_logic_formula where
toShATermAux :: ATermTable -> TFX_logic_formula -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TFX_logic_formula
xv = case TFX_logic_formula
xv of
TFXLF_binary a :: THF_binary_formula
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_binary_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_binary_formula
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 "TFXLF_binary" [Int
a'] []) ATermTable
att1
TFXLF_unitary a :: THF_unitary_formula
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> THF_unitary_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 THF_unitary_formula
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 "TFXLF_unitary" [Int
a'] []) ATermTable
att1
TFXLF_typed a :: TFF_typed_atom
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TFF_typed_atom -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TFF_typed_atom
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 "TFXLF_typed" [Int
a'] []) ATermTable
att1
TFXLF_subtype a :: TFF_subtype
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TFF_subtype -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TFF_subtype
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 "TFXLF_subtype" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, TFX_logic_formula)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "TFXLF_binary" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_binary_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_binary_formula
a') ->
(ATermTable
att1, THF_binary_formula -> TFX_logic_formula
TFXLF_binary THF_binary_formula
a') }
ShAAppl "TFXLF_unitary" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, THF_unitary_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: THF_unitary_formula
a') ->
(ATermTable
att1, THF_unitary_formula -> TFX_logic_formula
TFXLF_unitary THF_unitary_formula
a') }
ShAAppl "TFXLF_typed" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, TFF_typed_atom)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TFF_typed_atom
a') ->
(ATermTable
att1, TFF_typed_atom -> TFX_logic_formula
TFXLF_typed TFF_typed_atom
a') }
ShAAppl "TFXLF_subtype" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, TFF_subtype)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TFF_subtype
a') ->
(ATermTable
att1, TFF_subtype -> TFX_logic_formula
TFXLF_subtype TFF_subtype
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TFX_logic_formula)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.TFX_logic_formula" ShATerm
u
instance ShATermConvertible TPTP.AS.TFF_formula where
toShATermAux :: ATermTable -> TFF_formula -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TFF_formula
xv = case TFF_formula
xv of
TFFF_logic a :: TFF_logic_formula
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TFF_logic_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TFF_logic_formula
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 "TFFF_logic" [Int
a'] []) ATermTable
att1
TFFF_atom a :: TFF_typed_atom
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TFF_typed_atom -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TFF_typed_atom
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 "TFFF_atom" [Int
a'] []) ATermTable
att1
TFFF_sequent a :: TFF_sequent
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TFF_sequent -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TFF_sequent
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 "TFFF_sequent" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_formula)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "TFFF_logic" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, TFF_logic_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TFF_logic_formula
a') ->
(ATermTable
att1, TFF_logic_formula -> TFF_formula
TFFF_logic TFF_logic_formula
a') }
ShAAppl "TFFF_atom" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, TFF_typed_atom)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TFF_typed_atom
a') ->
(ATermTable
att1, TFF_typed_atom -> TFF_formula
TFFF_atom TFF_typed_atom
a') }
ShAAppl "TFFF_sequent" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, TFF_sequent)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TFF_sequent
a') ->
(ATermTable
att1, TFF_sequent -> TFF_formula
TFFF_sequent TFF_sequent
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TFF_formula)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.TFF_formula" ShATerm
u
instance ShATermConvertible TPTP.AS.TFF_logic_formula where
toShATermAux :: ATermTable -> TFF_logic_formula -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TFF_logic_formula
xv = case TFF_logic_formula
xv of
TFFLF_binary a :: TFF_binary_formula
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TFF_binary_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TFF_binary_formula
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 "TFFLF_binary" [Int
a'] []) ATermTable
att1
TFFLF_unitary a :: TFF_unitary_formula
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TFF_unitary_formula -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TFF_unitary_formula
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 "TFFLF_unitary" [Int
a'] []) ATermTable
att1
TFFLF_subtype a :: TFF_subtype
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TFF_subtype -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TFF_subtype
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 "TFFLF_subtype" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_logic_formula)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "TFFLF_binary" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, TFF_binary_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TFF_binary_formula
a') ->
(ATermTable
att1, TFF_binary_formula -> TFF_logic_formula
TFFLF_binary TFF_binary_formula
a') }
ShAAppl "TFFLF_unitary" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, TFF_unitary_formula)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TFF_unitary_formula
a') ->
(ATermTable
att1, TFF_unitary_formula -> TFF_logic_formula
TFFLF_unitary TFF_unitary_formula
a') }
ShAAppl "TFFLF_subtype" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, TFF_subtype)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TFF_subtype
a') ->
(ATermTable
att1, TFF_subtype -> TFF_logic_formula
TFFLF_subtype TFF_subtype
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TFF_logic_formula)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.TFF_logic_formula" ShATerm
u
instance ShATermConvertible TPTP.AS.TFF_binary_formula where
toShATermAux :: ATermTable -> TFF_binary_formula -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TFF_binary_formula
xv = case TFF_binary_formula
xv of
TFFBF_nonassoc a :: TFF_binary_nonassoc
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TFF_binary_nonassoc -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TFF_binary_nonassoc
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 "TFFBF_nonassoc" [Int
a'] []) ATermTable
att1
TFFBF_assoc a :: TFF_binary_assoc
a -> do
(att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> TFF_binary_assoc -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 TFF_binary_assoc
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 "TFFBF_assoc" [Int
a'] []) ATermTable
att1
fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_binary_formula)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
ShAAppl "TFFBF_nonassoc" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, TFF_binary_nonassoc)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TFF_binary_nonassoc
a') ->
(ATermTable
att1, TFF_binary_nonassoc -> TFF_binary_formula
TFFBF_nonassoc TFF_binary_nonassoc
a') }
ShAAppl "TFFBF_assoc" [a :: Int
a] _ ->
case Int -> ATermTable -> (ATermTable, TFF_binary_assoc)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of
{ (att1 :: ATermTable
att1, a' :: TFF_binary_assoc
a') ->
(ATermTable
att1, TFF_binary_assoc -> TFF_binary_formula
TFFBF_assoc TFF_binary_assoc
a') }
u :: ShATerm
u -> String -> ShATerm -> (ATermTable, TFF_binary_formula)
forall a. String -> ShATerm -> a
fromShATermError "TPTP.AS.TFF_binary_formula" ShATerm
u
instance ShATermConvertible TPTP.AS.TFF_binary_nonassoc where
toShATermAux :: ATermTable -> TFF_binary_nonassoc -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 xv :: TFF_binary_nonassoc