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

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

Automatic derivation of instances via DrIFT-rule ShATermConvertible, Json
  for the type(s):
'TPTP.AS.BASIC_SPEC'
'TPTP.AS.TPTP'
'TPTP.AS.TPTP_input'
'TPTP.AS.Comment'
'TPTP.AS.DefinedComment'
'TPTP.AS.SystemComment'
'TPTP.AS.Annotated_formula'
'TPTP.AS.TPI_annotated'
'TPTP.AS.THF_annotated'
'TPTP.AS.TFX_annotated'
'TPTP.AS.TFF_annotated'
'TPTP.AS.TCF_annotated'
'TPTP.AS.FOF_annotated'
'TPTP.AS.CNF_annotated'
'TPTP.AS.Annotations'
'TPTP.AS.Formula_role'
'TPTP.AS.THF_formula'
'TPTP.AS.THF_logic_formula'
'TPTP.AS.THF_binary_formula'
'TPTP.AS.THF_binary_pair'
'TPTP.AS.THF_binary_tuple'
'TPTP.AS.THF_unitary_formula'
'TPTP.AS.THF_quantified_formula'
'TPTP.AS.THF_quantification'
'TPTP.AS.THF_variable'
'TPTP.AS.THF_typed_variable'
'TPTP.AS.THF_unary_formula'
'TPTP.AS.THF_atom'
'TPTP.AS.THF_function'
'TPTP.AS.THF_conn_term'
'TPTP.AS.THF_conditional'
'TPTP.AS.THF_let'
'TPTP.AS.THF_let_defns'
'TPTP.AS.THF_let_defn'
'TPTP.AS.THF_let_quantified_defn'
'TPTP.AS.THF_let_plain_defn'
'TPTP.AS.THF_let_defn_LHS'
'TPTP.AS.THF_type_formula'
'TPTP.AS.THF_typeable_formula'
'TPTP.AS.THF_subtype'
'TPTP.AS.THF_top_level_type'
'TPTP.AS.THF_unitary_type'
'TPTP.AS.THF_binary_type'
'TPTP.AS.THF_sequent'
'TPTP.AS.THF_tuple'
'TPTP.AS.TFX_formula'
'TPTP.AS.TFX_logic_formula'
'TPTP.AS.TFF_formula'
'TPTP.AS.TFF_logic_formula'
'TPTP.AS.TFF_binary_formula'
'TPTP.AS.TFF_binary_nonassoc'
'TPTP.AS.TFF_binary_assoc'
'TPTP.AS.TFF_unitary_formula'
'TPTP.AS.TFF_quantified_formula'
'TPTP.AS.TFF_variable'
'TPTP.AS.TFF_typed_variable'
'TPTP.AS.TFF_unary_formula'
'TPTP.AS.TFF_conditional'
'TPTP.AS.TFF_let'
'TPTP.AS.TFF_let_term_defns'
'TPTP.AS.TFF_let_term_defn'
'TPTP.AS.TFF_let_term_binding'
'TPTP.AS.TFF_let_formula_defns'
'TPTP.AS.TFF_let_formula_defn'
'TPTP.AS.TFF_let_formula_binding'
'TPTP.AS.TFF_sequent'
'TPTP.AS.TFF_formula_tuple'
'TPTP.AS.TFF_typed_atom'
'TPTP.AS.TFF_subtype'
'TPTP.AS.TFF_top_level_type'
'TPTP.AS.TF1_quantified_type'
'TPTP.AS.TFF_monotype'
'TPTP.AS.TFF_unitary_type'
'TPTP.AS.TFF_atomic_type'
'TPTP.AS.TFF_mapping_type'
'TPTP.AS.TFF_xprod_type'
'TPTP.AS.TCF_formula'
'TPTP.AS.TCF_logic_formula'
'TPTP.AS.TCF_quantified_formula'
'TPTP.AS.FOF_formula'
'TPTP.AS.FOF_logic_formula'
'TPTP.AS.FOF_binary_formula'
'TPTP.AS.FOF_binary_nonassoc'
'TPTP.AS.FOF_binary_assoc'
'TPTP.AS.FOF_unitary_formula'
'TPTP.AS.FOF_quantified_formula'
'TPTP.AS.FOF_unary_formula'
'TPTP.AS.FOF_infix_unary'
'TPTP.AS.FOF_atomic_formula'
'TPTP.AS.FOF_plain_atomic_formula'
'TPTP.AS.FOF_defined_atomic_formula'
'TPTP.AS.FOF_defined_plain_formula'
'TPTP.AS.FOF_defined_infix_formula'
'TPTP.AS.FOF_system_atomic_formula'
'TPTP.AS.FOF_plain_term'
'TPTP.AS.FOF_defined_term'
'TPTP.AS.FOF_defined_atomic_term'
'TPTP.AS.FOF_defined_plain_term'
'TPTP.AS.FOF_system_term'
'TPTP.AS.FOF_term'
'TPTP.AS.FOF_function_term'
'TPTP.AS.TFF_conditional_term'
'TPTP.AS.TFF_let_term'
'TPTP.AS.FOF_sequent'
'TPTP.AS.FOF_formula_tuple'
'TPTP.AS.CNF_formula'
'TPTP.AS.Disjunction'
'TPTP.AS.Literal'
'TPTP.AS.THF_quantifier'
'TPTP.AS.TH1_quantifier'
'TPTP.AS.TH0_quantifier'
'TPTP.AS.THF_pair_connective'
'TPTP.AS.THF_unary_connective'
'TPTP.AS.TH1_unary_connective'
'TPTP.AS.FOF_quantifier'
'TPTP.AS.Binary_connective'
'TPTP.AS.Assoc_connective'
'TPTP.AS.Unary_connective'
'TPTP.AS.Defined_type'
'TPTP.AS.Atom'
'TPTP.AS.Untyped_atom'
'TPTP.AS.Defined_proposition'
'TPTP.AS.Defined_predicate'
'TPTP.AS.Defined_infix_pred'
'TPTP.AS.Defined_functor'
'TPTP.AS.Defined_term'
'TPTP.AS.Source'
'TPTP.AS.DAG_source'
'TPTP.AS.Inference_record'
'TPTP.AS.Parent_info'
'TPTP.AS.Internal_source'
'TPTP.AS.Intro_type'
'TPTP.AS.External_source'
'TPTP.AS.File_source'
'TPTP.AS.Theory'
'TPTP.AS.Theory_name'
'TPTP.AS.Creator_source'
'TPTP.AS.Useful_info'
'TPTP.AS.Info_item'
'TPTP.AS.Formula_item'
'TPTP.AS.Inference_item'
'TPTP.AS.Inference_status'
'TPTP.AS.Status_value'
'TPTP.AS.Inference_info'
'TPTP.AS.New_symbol_record'
'TPTP.AS.Principal_symbol'
'TPTP.AS.Include'
'TPTP.AS.General_term'
'TPTP.AS.General_data'
'TPTP.AS.General_function'
'TPTP.AS.Formula_data'
'TPTP.AS.Name'
'TPTP.AS.Number'
'TPTP.Sign.Symbol'
'TPTP.Sign.SymbolType'
'TPTP.Sign.THFTypeable'
'TPTP.Sign.FunctorType'
'TPTP.Sign.PredicateType'
'TPTP.Sign.Type_functorType'
'TPTP.Sign.Sign'
'TPTP.Sublogic.Sublogic'
-}

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

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

{-! for TPTP.AS.BASIC_SPEC derive : ShATermConvertible !-}
{-! for TPTP.AS.TPTP derive : ShATermConvertible !-}
{-! for TPTP.AS.TPTP_input derive : ShATermConvertible !-}
{-! for TPTP.AS.Comment derive : ShATermConvertible !-}
{-! for TPTP.AS.DefinedComment derive : ShATermConvertible !-}
{-! for TPTP.AS.SystemComment derive : ShATermConvertible !-}
{-! for TPTP.AS.Annotated_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.TPI_annotated derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_annotated derive : ShATermConvertible !-}
{-! for TPTP.AS.TFX_annotated derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_annotated derive : ShATermConvertible !-}
{-! for TPTP.AS.TCF_annotated derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_annotated derive : ShATermConvertible !-}
{-! for TPTP.AS.CNF_annotated derive : ShATermConvertible !-}
{-! for TPTP.AS.Annotations derive : ShATermConvertible !-}
{-! for TPTP.AS.Formula_role derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_logic_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_binary_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_binary_pair derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_binary_tuple derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_unitary_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_quantified_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_quantification derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_variable derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_typed_variable derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_unary_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_atom derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_function derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_conn_term derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_conditional derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_let derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_let_defns derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_let_defn derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_let_quantified_defn derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_let_plain_defn derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_let_defn_LHS derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_type_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_typeable_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_subtype derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_top_level_type derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_unitary_type derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_binary_type derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_sequent derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_tuple derive : ShATermConvertible !-}
{-! for TPTP.AS.TFX_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.TFX_logic_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_logic_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_binary_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_binary_nonassoc derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_binary_assoc derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_unitary_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_quantified_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_variable derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_typed_variable derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_unary_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_conditional derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_let derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_let_term_defns derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_let_term_defn derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_let_term_binding derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_let_formula_defns derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_let_formula_defn derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_let_formula_binding derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_sequent derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_formula_tuple derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_typed_atom derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_subtype derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_top_level_type derive : ShATermConvertible !-}
{-! for TPTP.AS.TF1_quantified_type derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_monotype derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_unitary_type derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_atomic_type derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_mapping_type derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_xprod_type derive : ShATermConvertible !-}
{-! for TPTP.AS.TCF_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.TCF_logic_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.TCF_quantified_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_logic_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_binary_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_binary_nonassoc derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_binary_assoc derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_unitary_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_quantified_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_unary_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_infix_unary derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_atomic_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_plain_atomic_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_defined_atomic_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_defined_plain_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_defined_infix_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_system_atomic_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_plain_term derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_defined_term derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_defined_atomic_term derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_defined_plain_term derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_system_term derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_term derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_function_term derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_conditional_term derive : ShATermConvertible !-}
{-! for TPTP.AS.TFF_let_term derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_sequent derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_formula_tuple derive : ShATermConvertible !-}
{-! for TPTP.AS.CNF_formula derive : ShATermConvertible !-}
{-! for TPTP.AS.Disjunction derive : ShATermConvertible !-}
{-! for TPTP.AS.Literal derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_quantifier derive : ShATermConvertible !-}
{-! for TPTP.AS.TH1_quantifier derive : ShATermConvertible !-}
{-! for TPTP.AS.TH0_quantifier derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_pair_connective derive : ShATermConvertible !-}
{-! for TPTP.AS.THF_unary_connective derive : ShATermConvertible !-}
{-! for TPTP.AS.TH1_unary_connective derive : ShATermConvertible !-}
{-! for TPTP.AS.FOF_quantifier derive : ShATermConvertible !-}
{-! for TPTP.AS.Binary_connective derive : ShATermConvertible !-}
{-! for TPTP.AS.Assoc_connective derive : ShATermConvertible !-}
{-! for TPTP.AS.Unary_connective derive : ShATermConvertible !-}
{-! for TPTP.AS.Defined_type derive : ShATermConvertible !-}
{-! for TPTP.AS.Atom derive : ShATermConvertible !-}
{-! for TPTP.AS.Untyped_atom derive : ShATermConvertible !-}
{-! for TPTP.AS.Defined_proposition derive : ShATermConvertible !-}
{-! for TPTP.AS.Defined_predicate derive : ShATermConvertible !-}
{-! for TPTP.AS.Defined_infix_pred derive : ShATermConvertible !-}
{-! for TPTP.AS.Defined_functor derive : ShATermConvertible !-}
{-! for TPTP.AS.Defined_term derive : ShATermConvertible !-}
{-! for TPTP.AS.Source derive : ShATermConvertible !-}
{-! for TPTP.AS.DAG_source derive : ShATermConvertible !-}
{-! for TPTP.AS.Inference_record derive : ShATermConvertible !-}
{-! for TPTP.AS.Parent_info derive : ShATermConvertible !-}
{-! for TPTP.AS.Internal_source derive : ShATermConvertible !-}
{-! for TPTP.AS.Intro_type derive : ShATermConvertible !-}
{-! for TPTP.AS.External_source derive : ShATermConvertible !-}
{-! for TPTP.AS.File_source derive : ShATermConvertible !-}
{-! for TPTP.AS.Theory derive : ShATermConvertible !-}
{-! for TPTP.AS.Theory_name derive : ShATermConvertible !-}
{-! for TPTP.AS.Creator_source derive : ShATermConvertible !-}
{-! for TPTP.AS.Useful_info derive : ShATermConvertible !-}
{-! for TPTP.AS.Info_item derive : ShATermConvertible !-}
{-! for TPTP.AS.Formula_item derive : ShATermConvertible !-}
{-! for TPTP.AS.Inference_item derive : ShATermConvertible !-}
{-! for TPTP.AS.Inference_status derive : ShATermConvertible !-}
{-! for TPTP.AS.Status_value derive : ShATermConvertible !-}
{-! for TPTP.AS.Inference_info derive : ShATermConvertible !-}
{-! for TPTP.AS.New_symbol_record derive : ShATermConvertible !-}
{-! for TPTP.AS.Principal_symbol derive : ShATermConvertible !-}
{-! for TPTP.AS.Include derive : ShATermConvertible !-}
{-! for TPTP.AS.General_term derive : ShATermConvertible !-}
{-! for TPTP.AS.General_data derive : ShATermConvertible !-}
{-! for TPTP.AS.General_function derive : ShATermConvertible !-}
{-! for TPTP.AS.Formula_data derive : ShATermConvertible !-}
{-! for TPTP.AS.Name derive : ShATermConvertible !-}
{-! for TPTP.AS.Number derive : ShATermConvertible !-}
{-! for TPTP.Sign.Symbol derive : ShATermConvertible !-}
{-! for TPTP.Sign.SymbolType derive : ShATermConvertible !-}
{-! for TPTP.Sign.THFTypeable derive : ShATermConvertible !-}
{-! for TPTP.Sign.FunctorType derive : ShATermConvertible !-}
{-! for TPTP.Sign.PredicateType derive : ShATermConvertible !-}
{-! for TPTP.Sign.Type_functorType derive : ShATermConvertible !-}
{-! for TPTP.Sign.Sign derive : ShATermConvertible !-}
{-! for TPTP.Sublogic.Sublogic derive : ShATermConvertible !-}

{-! for TPTP.AS.BASIC_SPEC derive : Json !-}
{-! for TPTP.AS.TPTP derive : Json !-}
{-! for TPTP.AS.TPTP_input derive : Json !-}
{-! for TPTP.AS.Comment derive : Json !-}
{-! for TPTP.AS.DefinedComment derive : Json !-}
{-! for TPTP.AS.SystemComment derive : Json !-}
{-! for TPTP.AS.Annotated_formula derive : Json !-}
{-! for TPTP.AS.TPI_annotated derive : Json !-}
{-! for TPTP.AS.THF_annotated derive : Json !-}
{-! for TPTP.AS.TFX_annotated derive : Json !-}
{-! for TPTP.AS.TFF_annotated derive : Json !-}
{-! for TPTP.AS.TCF_annotated derive : Json !-}
{-! for TPTP.AS.FOF_annotated derive : Json !-}
{-! for TPTP.AS.CNF_annotated derive : Json !-}
{-! for TPTP.AS.Annotations derive : Json !-}
{-! for TPTP.AS.Formula_role derive : Json !-}
{-! for TPTP.AS.THF_formula derive : Json !-}
{-! for TPTP.AS.THF_logic_formula derive : Json !-}
{-! for TPTP.AS.THF_binary_formula derive : Json !-}
{-! for TPTP.AS.THF_binary_pair derive : Json !-}
{-! for TPTP.AS.THF_binary_tuple derive : Json !-}
{-! for TPTP.AS.THF_unitary_formula derive : Json !-}
{-! for TPTP.AS.THF_quantified_formula derive : Json !-}
{-! for TPTP.AS.THF_quantification derive : Json !-}
{-! for TPTP.AS.THF_variable derive : Json !-}
{-! for TPTP.AS.THF_typed_variable derive : Json !-}
{-! for TPTP.AS.THF_unary_formula derive : Json !-}
{-! for TPTP.AS.THF_atom derive : Json !-}
{-! for TPTP.AS.THF_function derive : Json !-}
{-! for TPTP.AS.THF_conn_term derive : Json !-}
{-! for TPTP.AS.THF_conditional derive : Json !-}
{-! for TPTP.AS.THF_let derive : Json !-}
{-! for TPTP.AS.THF_let_defns derive : Json !-}
{-! for TPTP.AS.THF_let_defn derive : Json !-}
{-! for TPTP.AS.THF_let_quantified_defn derive : Json !-}
{-! for TPTP.AS.THF_let_plain_defn derive : Json !-}
{-! for TPTP.AS.THF_let_defn_LHS derive : Json !-}
{-! for TPTP.AS.THF_type_formula derive : Json !-}
{-! for TPTP.AS.THF_typeable_formula derive : Json !-}
{-! for TPTP.AS.THF_subtype derive : Json !-}
{-! for TPTP.AS.THF_top_level_type derive : Json !-}
{-! for TPTP.AS.THF_unitary_type derive : Json !-}
{-! for TPTP.AS.THF_binary_type derive : Json !-}
{-! for TPTP.AS.THF_sequent derive : Json !-}
{-! for TPTP.AS.THF_tuple derive : Json !-}
{-! for TPTP.AS.TFX_formula derive : Json !-}
{-! for TPTP.AS.TFX_logic_formula derive : Json !-}
{-! for TPTP.AS.TFF_formula derive : Json !-}
{-! for TPTP.AS.TFF_logic_formula derive : Json !-}
{-! for TPTP.AS.TFF_binary_formula derive : Json !-}
{-! for TPTP.AS.TFF_binary_nonassoc derive : Json !-}
{-! for TPTP.AS.TFF_binary_assoc derive : Json !-}
{-! for TPTP.AS.TFF_unitary_formula derive : Json !-}
{-! for TPTP.AS.TFF_quantified_formula derive : Json !-}
{-! for TPTP.AS.TFF_variable derive : Json !-}
{-! for TPTP.AS.TFF_typed_variable derive : Json !-}
{-! for TPTP.AS.TFF_unary_formula derive : Json !-}
{-! for TPTP.AS.TFF_conditional derive : Json !-}
{-! for TPTP.AS.TFF_let derive : Json !-}
{-! for TPTP.AS.TFF_let_term_defns derive : Json !-}
{-! for TPTP.AS.TFF_let_term_defn derive : Json !-}
{-! for TPTP.AS.TFF_let_term_binding derive : Json !-}
{-! for TPTP.AS.TFF_let_formula_defns derive : Json !-}
{-! for TPTP.AS.TFF_let_formula_defn derive : Json !-}
{-! for TPTP.AS.TFF_let_formula_binding derive : Json !-}
{-! for TPTP.AS.TFF_sequent derive : Json !-}
{-! for TPTP.AS.TFF_formula_tuple derive : Json !-}
{-! for TPTP.AS.TFF_typed_atom derive : Json !-}
{-! for TPTP.AS.TFF_subtype derive : Json !-}
{-! for TPTP.AS.TFF_top_level_type derive : Json !-}
{-! for TPTP.AS.TF1_quantified_type derive : Json !-}
{-! for TPTP.AS.TFF_monotype derive : Json !-}
{-! for TPTP.AS.TFF_unitary_type derive : Json !-}
{-! for TPTP.AS.TFF_atomic_type derive : Json !-}
{-! for TPTP.AS.TFF_mapping_type derive : Json !-}
{-! for TPTP.AS.TFF_xprod_type derive : Json !-}
{-! for TPTP.AS.TCF_formula derive : Json !-}
{-! for TPTP.AS.TCF_logic_formula derive : Json !-}
{-! for TPTP.AS.TCF_quantified_formula derive : Json !-}
{-! for TPTP.AS.FOF_formula derive : Json !-}
{-! for TPTP.AS.FOF_logic_formula derive : Json !-}
{-! for TPTP.AS.FOF_binary_formula derive : Json !-}
{-! for TPTP.AS.FOF_binary_nonassoc derive : Json !-}
{-! for TPTP.AS.FOF_binary_assoc derive : Json !-}
{-! for TPTP.AS.FOF_unitary_formula derive : Json !-}
{-! for TPTP.AS.FOF_quantified_formula derive : Json !-}
{-! for TPTP.AS.FOF_unary_formula derive : Json !-}
{-! for TPTP.AS.FOF_infix_unary derive : Json !-}
{-! for TPTP.AS.FOF_atomic_formula derive : Json !-}
{-! for TPTP.AS.FOF_plain_atomic_formula derive : Json !-}
{-! for TPTP.AS.FOF_defined_atomic_formula derive : Json !-}
{-! for TPTP.AS.FOF_defined_plain_formula derive : Json !-}
{-! for TPTP.AS.FOF_defined_infix_formula derive : Json !-}
{-! for TPTP.AS.FOF_system_atomic_formula derive : Json !-}
{-! for TPTP.AS.FOF_plain_term derive : Json !-}
{-! for TPTP.AS.FOF_defined_term derive : Json !-}
{-! for TPTP.AS.FOF_defined_atomic_term derive : Json !-}
{-! for TPTP.AS.FOF_defined_plain_term derive : Json !-}
{-! for TPTP.AS.FOF_system_term derive : Json !-}
{-! for TPTP.AS.FOF_term derive : Json !-}
{-! for TPTP.AS.FOF_function_term derive : Json !-}
{-! for TPTP.AS.TFF_conditional_term derive : Json !-}
{-! for TPTP.AS.TFF_let_term derive : Json !-}
{-! for TPTP.AS.FOF_sequent derive : Json !-}
{-! for TPTP.AS.FOF_formula_tuple derive : Json !-}
{-! for TPTP.AS.CNF_formula derive : Json !-}
{-! for TPTP.AS.Disjunction derive : Json !-}
{-! for TPTP.AS.Literal derive : Json !-}
{-! for TPTP.AS.THF_quantifier derive : Json !-}
{-! for TPTP.AS.TH1_quantifier derive : Json !-}
{-! for TPTP.AS.TH0_quantifier derive : Json !-}
{-! for TPTP.AS.THF_pair_connective derive : Json !-}
{-! for TPTP.AS.THF_unary_connective derive : Json !-}
{-! for TPTP.AS.TH1_unary_connective derive : Json !-}
{-! for TPTP.AS.FOF_quantifier derive : Json !-}
{-! for TPTP.AS.Binary_connective derive : Json !-}
{-! for TPTP.AS.Assoc_connective derive : Json !-}
{-! for TPTP.AS.Unary_connective derive : Json !-}
{-! for TPTP.AS.Defined_type derive : Json !-}
{-! for TPTP.AS.Atom derive : Json !-}
{-! for TPTP.AS.Untyped_atom derive : Json !-}
{-! for TPTP.AS.Defined_proposition derive : Json !-}
{-! for TPTP.AS.Defined_predicate derive : Json !-}
{-! for TPTP.AS.Defined_infix_pred derive : Json !-}
{-! for TPTP.AS.Defined_functor derive : Json !-}
{-! for TPTP.AS.Defined_term derive : Json !-}
{-! for TPTP.AS.Source derive : Json !-}
{-! for TPTP.AS.DAG_source derive : Json !-}
{-! for TPTP.AS.Inference_record derive : Json !-}
{-! for TPTP.AS.Parent_info derive : Json !-}
{-! for TPTP.AS.Internal_source derive : Json !-}
{-! for TPTP.AS.Intro_type derive : Json !-}
{-! for TPTP.AS.External_source derive : Json !-}
{-! for TPTP.AS.File_source derive : Json !-}
{-! for TPTP.AS.Theory derive : Json !-}
{-! for TPTP.AS.Theory_name derive : Json !-}
{-! for TPTP.AS.Creator_source derive : Json !-}
{-! for TPTP.AS.Useful_info derive : Json !-}
{-! for TPTP.AS.Info_item derive : Json !-}
{-! for TPTP.AS.Formula_item derive : Json !-}
{-! for TPTP.AS.Inference_item derive : Json !-}
{-! for TPTP.AS.Inference_status derive : Json !-}
{-! for TPTP.AS.Status_value derive : Json !-}
{-! for TPTP.AS.Inference_info derive : Json !-}
{-! for TPTP.AS.New_symbol_record derive : Json !-}
{-! for TPTP.AS.Principal_symbol derive : Json !-}
{-! for TPTP.AS.Include derive : Json !-}
{-! for TPTP.AS.General_term derive : Json !-}
{-! for TPTP.AS.General_data derive : Json !-}
{-! for TPTP.AS.General_function derive : Json !-}
{-! for TPTP.AS.Formula_data derive : Json !-}
{-! for TPTP.AS.Name derive : Json !-}
{-! for TPTP.AS.Number derive : Json !-}
{-! for TPTP.Sign.Symbol derive : Json !-}
{-! for TPTP.Sign.SymbolType derive : Json !-}
{-! for TPTP.Sign.THFTypeable derive : Json !-}
{-! for TPTP.Sign.FunctorType derive : Json !-}
{-! for TPTP.Sign.PredicateType derive : Json !-}
{-! for TPTP.Sign.Type_functorType derive : Json !-}
{-! for TPTP.Sign.Sign derive : Json !-}
{-! for TPTP.Sublogic.Sublogic derive : Json !-}

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

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