Hets - the Heterogeneous Tool Set

Copyright(c) DFKI GmbH 2012
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilitynon-portable(derive Typeable instances)
Safe HaskellNone

TPTP.ATC_TPTP

Contents

Description

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

Orphan instances

ShATermConvertible Number Source # 

Methods

toShATermAux :: ATermTable -> Number -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Number] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Number)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Number])

ShATermConvertible Name Source # 

Methods

toShATermAux :: ATermTable -> Name -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Name] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Name)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Name])

ShATermConvertible Formula_data Source # 

Methods

toShATermAux :: ATermTable -> Formula_data -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Formula_data] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Formula_data)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Formula_data])

ShATermConvertible General_function Source # 

Methods

toShATermAux :: ATermTable -> General_function -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [General_function] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, General_function)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [General_function])

ShATermConvertible General_data Source # 

Methods

toShATermAux :: ATermTable -> General_data -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [General_data] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, General_data)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [General_data])

ShATermConvertible General_term Source # 

Methods

toShATermAux :: ATermTable -> General_term -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [General_term] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, General_term)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [General_term])

ShATermConvertible Include Source # 

Methods

toShATermAux :: ATermTable -> Include -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Include] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Include)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Include])

ShATermConvertible Principal_symbol Source # 

Methods

toShATermAux :: ATermTable -> Principal_symbol -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Principal_symbol] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Principal_symbol)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Principal_symbol])

ShATermConvertible New_symbol_record Source # 

Methods

toShATermAux :: ATermTable -> New_symbol_record -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [New_symbol_record] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, New_symbol_record)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [New_symbol_record])

ShATermConvertible Inference_info Source # 

Methods

toShATermAux :: ATermTable -> Inference_info -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Inference_info] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Inference_info)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Inference_info])

ShATermConvertible Status_value Source # 

Methods

toShATermAux :: ATermTable -> Status_value -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Status_value] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Status_value)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Status_value])

ShATermConvertible Inference_status Source # 

Methods

toShATermAux :: ATermTable -> Inference_status -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Inference_status] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Inference_status)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Inference_status])

ShATermConvertible Inference_item Source # 

Methods

toShATermAux :: ATermTable -> Inference_item -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Inference_item] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Inference_item)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Inference_item])

ShATermConvertible Formula_item Source # 

Methods

toShATermAux :: ATermTable -> Formula_item -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Formula_item] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Formula_item)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Formula_item])

ShATermConvertible Info_item Source # 

Methods

toShATermAux :: ATermTable -> Info_item -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Info_item] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Info_item)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Info_item])

ShATermConvertible Useful_info Source # 

Methods

toShATermAux :: ATermTable -> Useful_info -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Useful_info] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Useful_info)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Useful_info])

ShATermConvertible Creator_source Source # 

Methods

toShATermAux :: ATermTable -> Creator_source -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Creator_source] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Creator_source)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Creator_source])

ShATermConvertible Theory_name Source # 

Methods

toShATermAux :: ATermTable -> Theory_name -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Theory_name] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Theory_name)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Theory_name])

ShATermConvertible Theory Source # 

Methods

toShATermAux :: ATermTable -> Theory -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Theory] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Theory)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Theory])

ShATermConvertible File_source Source # 

Methods

toShATermAux :: ATermTable -> File_source -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [File_source] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, File_source)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [File_source])

ShATermConvertible External_source Source # 

Methods

toShATermAux :: ATermTable -> External_source -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [External_source] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, External_source)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [External_source])

ShATermConvertible Intro_type Source # 

Methods

toShATermAux :: ATermTable -> Intro_type -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Intro_type] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Intro_type)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Intro_type])

ShATermConvertible Internal_source Source # 

Methods

toShATermAux :: ATermTable -> Internal_source -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Internal_source] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Internal_source)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Internal_source])

ShATermConvertible Parent_info Source # 

Methods

toShATermAux :: ATermTable -> Parent_info -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Parent_info] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Parent_info)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Parent_info])

ShATermConvertible Inference_record Source # 

Methods

toShATermAux :: ATermTable -> Inference_record -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Inference_record] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Inference_record)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Inference_record])

ShATermConvertible DAG_source Source # 

Methods

toShATermAux :: ATermTable -> DAG_source -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [DAG_source] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, DAG_source)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [DAG_source])

ShATermConvertible Source Source # 

Methods

toShATermAux :: ATermTable -> Source -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Source] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Source)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Source])

ShATermConvertible Defined_term Source # 

Methods

toShATermAux :: ATermTable -> Defined_term -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Defined_term] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Defined_term)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Defined_term])

ShATermConvertible Defined_functor Source # 

Methods

toShATermAux :: ATermTable -> Defined_functor -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Defined_functor] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Defined_functor)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Defined_functor])

ShATermConvertible Defined_infix_pred Source # 

Methods

toShATermAux :: ATermTable -> Defined_infix_pred -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Defined_infix_pred] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Defined_infix_pred)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Defined_infix_pred])

ShATermConvertible Defined_predicate Source # 

Methods

toShATermAux :: ATermTable -> Defined_predicate -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Defined_predicate] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Defined_predicate)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Defined_predicate])

ShATermConvertible Defined_proposition Source # 

Methods

toShATermAux :: ATermTable -> Defined_proposition -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Defined_proposition] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Defined_proposition)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Defined_proposition])

ShATermConvertible Untyped_atom Source # 

Methods

toShATermAux :: ATermTable -> Untyped_atom -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Untyped_atom] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Untyped_atom)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Untyped_atom])

ShATermConvertible Atom Source # 

Methods

toShATermAux :: ATermTable -> Atom -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Atom] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Atom)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Atom])

ShATermConvertible Defined_type Source # 

Methods

toShATermAux :: ATermTable -> Defined_type -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Defined_type] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Defined_type)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Defined_type])

ShATermConvertible Unary_connective Source # 

Methods

toShATermAux :: ATermTable -> Unary_connective -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Unary_connective] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Unary_connective)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Unary_connective])

ShATermConvertible Assoc_connective Source # 

Methods

toShATermAux :: ATermTable -> Assoc_connective -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Assoc_connective] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Assoc_connective)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Assoc_connective])

ShATermConvertible Binary_connective Source # 

Methods

toShATermAux :: ATermTable -> Binary_connective -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Binary_connective] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Binary_connective)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Binary_connective])

ShATermConvertible FOF_quantifier Source # 

Methods

toShATermAux :: ATermTable -> FOF_quantifier -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_quantifier] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_quantifier)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_quantifier])

ShATermConvertible TH1_unary_connective Source # 

Methods

toShATermAux :: ATermTable -> TH1_unary_connective -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TH1_unary_connective] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TH1_unary_connective)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TH1_unary_connective])

ShATermConvertible THF_unary_connective Source # 

Methods

toShATermAux :: ATermTable -> THF_unary_connective -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_unary_connective] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_unary_connective)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_unary_connective])

ShATermConvertible THF_pair_connective Source # 

Methods

toShATermAux :: ATermTable -> THF_pair_connective -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_pair_connective] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_pair_connective)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_pair_connective])

ShATermConvertible TH0_quantifier Source # 

Methods

toShATermAux :: ATermTable -> TH0_quantifier -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TH0_quantifier] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TH0_quantifier)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TH0_quantifier])

ShATermConvertible TH1_quantifier Source # 

Methods

toShATermAux :: ATermTable -> TH1_quantifier -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TH1_quantifier] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TH1_quantifier)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TH1_quantifier])

ShATermConvertible THF_quantifier Source # 

Methods

toShATermAux :: ATermTable -> THF_quantifier -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_quantifier] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_quantifier)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_quantifier])

ShATermConvertible Literal Source # 

Methods

toShATermAux :: ATermTable -> Literal -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Literal] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Literal)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Literal])

ShATermConvertible Disjunction Source # 

Methods

toShATermAux :: ATermTable -> Disjunction -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Disjunction] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Disjunction)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Disjunction])

ShATermConvertible CNF_formula Source # 

Methods

toShATermAux :: ATermTable -> CNF_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [CNF_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, CNF_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [CNF_formula])

ShATermConvertible FOF_formula_tuple Source # 

Methods

toShATermAux :: ATermTable -> FOF_formula_tuple -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_formula_tuple] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_formula_tuple)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_formula_tuple])

ShATermConvertible FOF_sequent Source # 

Methods

toShATermAux :: ATermTable -> FOF_sequent -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_sequent] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_sequent)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_sequent])

ShATermConvertible TFF_let_term Source # 

Methods

toShATermAux :: ATermTable -> TFF_let_term -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_let_term] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_let_term)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_let_term])

ShATermConvertible TFF_conditional_term Source # 

Methods

toShATermAux :: ATermTable -> TFF_conditional_term -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_conditional_term] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_conditional_term)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_conditional_term])

ShATermConvertible FOF_function_term Source # 

Methods

toShATermAux :: ATermTable -> FOF_function_term -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_function_term] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_function_term)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_function_term])

ShATermConvertible FOF_term Source # 

Methods

toShATermAux :: ATermTable -> FOF_term -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_term] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_term)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_term])

ShATermConvertible FOF_system_term Source # 

Methods

toShATermAux :: ATermTable -> FOF_system_term -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_system_term] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_system_term)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_system_term])

ShATermConvertible FOF_defined_plain_term Source # 

Methods

toShATermAux :: ATermTable -> FOF_defined_plain_term -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_defined_plain_term] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_defined_plain_term)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_defined_plain_term])

ShATermConvertible FOF_defined_atomic_term Source # 

Methods

toShATermAux :: ATermTable -> FOF_defined_atomic_term -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_defined_atomic_term] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_defined_atomic_term)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_defined_atomic_term])

ShATermConvertible FOF_defined_term Source # 

Methods

toShATermAux :: ATermTable -> FOF_defined_term -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_defined_term] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_defined_term)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_defined_term])

ShATermConvertible FOF_plain_term Source # 

Methods

toShATermAux :: ATermTable -> FOF_plain_term -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_plain_term] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_plain_term)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_plain_term])

ShATermConvertible FOF_system_atomic_formula Source # 

Methods

toShATermAux :: ATermTable -> FOF_system_atomic_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_system_atomic_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_system_atomic_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_system_atomic_formula])

ShATermConvertible FOF_defined_infix_formula Source # 

Methods

toShATermAux :: ATermTable -> FOF_defined_infix_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_defined_infix_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_defined_infix_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_defined_infix_formula])

ShATermConvertible FOF_defined_plain_formula Source # 

Methods

toShATermAux :: ATermTable -> FOF_defined_plain_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_defined_plain_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_defined_plain_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_defined_plain_formula])

ShATermConvertible FOF_defined_atomic_formula Source # 

Methods

toShATermAux :: ATermTable -> FOF_defined_atomic_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_defined_atomic_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_defined_atomic_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_defined_atomic_formula])

ShATermConvertible FOF_plain_atomic_formula Source # 

Methods

toShATermAux :: ATermTable -> FOF_plain_atomic_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_plain_atomic_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_plain_atomic_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_plain_atomic_formula])

ShATermConvertible FOF_atomic_formula Source # 

Methods

toShATermAux :: ATermTable -> FOF_atomic_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_atomic_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_atomic_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_atomic_formula])

ShATermConvertible FOF_infix_unary Source # 

Methods

toShATermAux :: ATermTable -> FOF_infix_unary -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_infix_unary] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_infix_unary)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_infix_unary])

ShATermConvertible FOF_unary_formula Source # 

Methods

toShATermAux :: ATermTable -> FOF_unary_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_unary_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_unary_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_unary_formula])

ShATermConvertible FOF_quantified_formula Source # 

Methods

toShATermAux :: ATermTable -> FOF_quantified_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_quantified_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_quantified_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_quantified_formula])

ShATermConvertible FOF_unitary_formula Source # 

Methods

toShATermAux :: ATermTable -> FOF_unitary_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_unitary_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_unitary_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_unitary_formula])

ShATermConvertible FOF_binary_assoc Source # 

Methods

toShATermAux :: ATermTable -> FOF_binary_assoc -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_binary_assoc] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_binary_assoc)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_binary_assoc])

ShATermConvertible FOF_binary_nonassoc Source # 

Methods

toShATermAux :: ATermTable -> FOF_binary_nonassoc -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_binary_nonassoc] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_binary_nonassoc)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_binary_nonassoc])

ShATermConvertible FOF_binary_formula Source # 

Methods

toShATermAux :: ATermTable -> FOF_binary_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_binary_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_binary_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_binary_formula])

ShATermConvertible FOF_logic_formula Source # 

Methods

toShATermAux :: ATermTable -> FOF_logic_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_logic_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_logic_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_logic_formula])

ShATermConvertible FOF_formula Source # 

Methods

toShATermAux :: ATermTable -> FOF_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_formula])

ShATermConvertible TCF_quantified_formula Source # 

Methods

toShATermAux :: ATermTable -> TCF_quantified_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TCF_quantified_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TCF_quantified_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TCF_quantified_formula])

ShATermConvertible TCF_logic_formula Source # 

Methods

toShATermAux :: ATermTable -> TCF_logic_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TCF_logic_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TCF_logic_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TCF_logic_formula])

ShATermConvertible TCF_formula Source # 

Methods

toShATermAux :: ATermTable -> TCF_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TCF_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TCF_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TCF_formula])

ShATermConvertible TFF_xprod_type Source # 

Methods

toShATermAux :: ATermTable -> TFF_xprod_type -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_xprod_type] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_xprod_type)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_xprod_type])

ShATermConvertible TFF_mapping_type Source # 

Methods

toShATermAux :: ATermTable -> TFF_mapping_type -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_mapping_type] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_mapping_type)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_mapping_type])

ShATermConvertible TFF_atomic_type Source # 

Methods

toShATermAux :: ATermTable -> TFF_atomic_type -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_atomic_type] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_atomic_type)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_atomic_type])

ShATermConvertible TFF_unitary_type Source # 

Methods

toShATermAux :: ATermTable -> TFF_unitary_type -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_unitary_type] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_unitary_type)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_unitary_type])

ShATermConvertible TFF_monotype Source # 

Methods

toShATermAux :: ATermTable -> TFF_monotype -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_monotype] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_monotype)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_monotype])

ShATermConvertible TF1_quantified_type Source # 

Methods

toShATermAux :: ATermTable -> TF1_quantified_type -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TF1_quantified_type] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TF1_quantified_type)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TF1_quantified_type])

ShATermConvertible TFF_top_level_type Source # 

Methods

toShATermAux :: ATermTable -> TFF_top_level_type -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_top_level_type] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_top_level_type)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_top_level_type])

ShATermConvertible TFF_subtype Source # 

Methods

toShATermAux :: ATermTable -> TFF_subtype -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_subtype] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_subtype)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_subtype])

ShATermConvertible TFF_typed_atom Source # 

Methods

toShATermAux :: ATermTable -> TFF_typed_atom -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_typed_atom] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_typed_atom)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_typed_atom])

ShATermConvertible TFF_formula_tuple Source # 

Methods

toShATermAux :: ATermTable -> TFF_formula_tuple -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_formula_tuple] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_formula_tuple)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_formula_tuple])

ShATermConvertible TFF_sequent Source # 

Methods

toShATermAux :: ATermTable -> TFF_sequent -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_sequent] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_sequent)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_sequent])

ShATermConvertible TFF_let_formula_binding Source # 

Methods

toShATermAux :: ATermTable -> TFF_let_formula_binding -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_let_formula_binding] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_let_formula_binding)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_let_formula_binding])

ShATermConvertible TFF_let_formula_defn Source # 

Methods

toShATermAux :: ATermTable -> TFF_let_formula_defn -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_let_formula_defn] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_let_formula_defn)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_let_formula_defn])

ShATermConvertible TFF_let_formula_defns Source # 

Methods

toShATermAux :: ATermTable -> TFF_let_formula_defns -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_let_formula_defns] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_let_formula_defns)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_let_formula_defns])

ShATermConvertible TFF_let_term_binding Source # 

Methods

toShATermAux :: ATermTable -> TFF_let_term_binding -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_let_term_binding] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_let_term_binding)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_let_term_binding])

ShATermConvertible TFF_let_term_defn Source # 

Methods

toShATermAux :: ATermTable -> TFF_let_term_defn -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_let_term_defn] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_let_term_defn)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_let_term_defn])

ShATermConvertible TFF_let_term_defns Source # 

Methods

toShATermAux :: ATermTable -> TFF_let_term_defns -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_let_term_defns] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_let_term_defns)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_let_term_defns])

ShATermConvertible TFF_let Source # 

Methods

toShATermAux :: ATermTable -> TFF_let -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_let] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_let)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_let])

ShATermConvertible TFF_conditional Source # 

Methods

toShATermAux :: ATermTable -> TFF_conditional -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_conditional] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_conditional)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_conditional])

ShATermConvertible TFF_unary_formula Source # 

Methods

toShATermAux :: ATermTable -> TFF_unary_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_unary_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_unary_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_unary_formula])

ShATermConvertible TFF_typed_variable Source # 

Methods

toShATermAux :: ATermTable -> TFF_typed_variable -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_typed_variable] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_typed_variable)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_typed_variable])

ShATermConvertible TFF_variable Source # 

Methods

toShATermAux :: ATermTable -> TFF_variable -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_variable] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_variable)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_variable])

ShATermConvertible TFF_quantified_formula Source # 

Methods

toShATermAux :: ATermTable -> TFF_quantified_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_quantified_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_quantified_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_quantified_formula])

ShATermConvertible TFF_unitary_formula Source # 

Methods

toShATermAux :: ATermTable -> TFF_unitary_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_unitary_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_unitary_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_unitary_formula])

ShATermConvertible TFF_binary_assoc Source # 

Methods

toShATermAux :: ATermTable -> TFF_binary_assoc -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_binary_assoc] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_binary_assoc)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_binary_assoc])

ShATermConvertible TFF_binary_nonassoc Source # 

Methods

toShATermAux :: ATermTable -> TFF_binary_nonassoc -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_binary_nonassoc] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_binary_nonassoc)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_binary_nonassoc])

ShATermConvertible TFF_binary_formula Source # 

Methods

toShATermAux :: ATermTable -> TFF_binary_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_binary_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_binary_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_binary_formula])

ShATermConvertible TFF_logic_formula Source # 

Methods

toShATermAux :: ATermTable -> TFF_logic_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_logic_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_logic_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_logic_formula])

ShATermConvertible TFF_formula Source # 

Methods

toShATermAux :: ATermTable -> TFF_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_formula])

ShATermConvertible TFX_logic_formula Source # 

Methods

toShATermAux :: ATermTable -> TFX_logic_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFX_logic_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFX_logic_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFX_logic_formula])

ShATermConvertible TFX_formula Source # 

Methods

toShATermAux :: ATermTable -> TFX_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFX_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFX_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFX_formula])

ShATermConvertible THF_tuple Source # 

Methods

toShATermAux :: ATermTable -> THF_tuple -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_tuple] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_tuple)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_tuple])

ShATermConvertible THF_sequent Source # 

Methods

toShATermAux :: ATermTable -> THF_sequent -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_sequent] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_sequent)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_sequent])

ShATermConvertible THF_binary_type Source # 

Methods

toShATermAux :: ATermTable -> THF_binary_type -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_binary_type] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_binary_type)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_binary_type])

ShATermConvertible THF_unitary_type Source # 

Methods

toShATermAux :: ATermTable -> THF_unitary_type -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_unitary_type] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_unitary_type)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_unitary_type])

ShATermConvertible THF_top_level_type Source # 

Methods

toShATermAux :: ATermTable -> THF_top_level_type -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_top_level_type] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_top_level_type)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_top_level_type])

ShATermConvertible THF_subtype Source # 

Methods

toShATermAux :: ATermTable -> THF_subtype -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_subtype] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_subtype)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_subtype])

ShATermConvertible THF_typeable_formula Source # 

Methods

toShATermAux :: ATermTable -> THF_typeable_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_typeable_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_typeable_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_typeable_formula])

ShATermConvertible THF_type_formula Source # 

Methods

toShATermAux :: ATermTable -> THF_type_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_type_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_type_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_type_formula])

ShATermConvertible THF_let_defn_LHS Source # 

Methods

toShATermAux :: ATermTable -> THF_let_defn_LHS -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_let_defn_LHS] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_let_defn_LHS)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_let_defn_LHS])

ShATermConvertible THF_let_plain_defn Source # 

Methods

toShATermAux :: ATermTable -> THF_let_plain_defn -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_let_plain_defn] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_let_plain_defn)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_let_plain_defn])

ShATermConvertible THF_let_quantified_defn Source # 

Methods

toShATermAux :: ATermTable -> THF_let_quantified_defn -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_let_quantified_defn] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_let_quantified_defn)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_let_quantified_defn])

ShATermConvertible THF_let_defn Source # 

Methods

toShATermAux :: ATermTable -> THF_let_defn -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_let_defn] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_let_defn)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_let_defn])

ShATermConvertible THF_let_defns Source # 

Methods

toShATermAux :: ATermTable -> THF_let_defns -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_let_defns] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_let_defns)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_let_defns])

ShATermConvertible THF_let Source # 

Methods

toShATermAux :: ATermTable -> THF_let -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_let] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_let)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_let])

ShATermConvertible THF_conditional Source # 

Methods

toShATermAux :: ATermTable -> THF_conditional -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_conditional] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_conditional)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_conditional])

ShATermConvertible THF_conn_term Source # 

Methods

toShATermAux :: ATermTable -> THF_conn_term -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_conn_term] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_conn_term)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_conn_term])

ShATermConvertible THF_function Source # 

Methods

toShATermAux :: ATermTable -> THF_function -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_function] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_function)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_function])

ShATermConvertible THF_atom Source # 

Methods

toShATermAux :: ATermTable -> THF_atom -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_atom] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_atom)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_atom])

ShATermConvertible THF_unary_formula Source # 

Methods

toShATermAux :: ATermTable -> THF_unary_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_unary_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_unary_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_unary_formula])

ShATermConvertible THF_typed_variable Source # 

Methods

toShATermAux :: ATermTable -> THF_typed_variable -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_typed_variable] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_typed_variable)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_typed_variable])

ShATermConvertible THF_variable Source # 

Methods

toShATermAux :: ATermTable -> THF_variable -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_variable] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_variable)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_variable])

ShATermConvertible THF_quantification Source # 

Methods

toShATermAux :: ATermTable -> THF_quantification -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_quantification] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_quantification)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_quantification])

ShATermConvertible THF_quantified_formula Source # 

Methods

toShATermAux :: ATermTable -> THF_quantified_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_quantified_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_quantified_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_quantified_formula])

ShATermConvertible THF_unitary_formula Source # 

Methods

toShATermAux :: ATermTable -> THF_unitary_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_unitary_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_unitary_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_unitary_formula])

ShATermConvertible THF_binary_tuple Source # 

Methods

toShATermAux :: ATermTable -> THF_binary_tuple -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_binary_tuple] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_binary_tuple)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_binary_tuple])

ShATermConvertible THF_binary_pair Source # 

Methods

toShATermAux :: ATermTable -> THF_binary_pair -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_binary_pair] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_binary_pair)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_binary_pair])

ShATermConvertible THF_binary_formula Source # 

Methods

toShATermAux :: ATermTable -> THF_binary_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_binary_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_binary_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_binary_formula])

ShATermConvertible THF_logic_formula Source # 

Methods

toShATermAux :: ATermTable -> THF_logic_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_logic_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_logic_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_logic_formula])

ShATermConvertible THF_formula Source # 

Methods

toShATermAux :: ATermTable -> THF_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_formula])

ShATermConvertible Formula_role Source # 

Methods

toShATermAux :: ATermTable -> Formula_role -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Formula_role] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Formula_role)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Formula_role])

ShATermConvertible Annotations Source # 

Methods

toShATermAux :: ATermTable -> Annotations -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Annotations] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Annotations)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Annotations])

ShATermConvertible CNF_annotated Source # 

Methods

toShATermAux :: ATermTable -> CNF_annotated -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [CNF_annotated] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, CNF_annotated)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [CNF_annotated])

ShATermConvertible FOF_annotated Source # 

Methods

toShATermAux :: ATermTable -> FOF_annotated -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FOF_annotated] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FOF_annotated)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FOF_annotated])

ShATermConvertible TCF_annotated Source # 

Methods

toShATermAux :: ATermTable -> TCF_annotated -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TCF_annotated] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TCF_annotated)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TCF_annotated])

ShATermConvertible TFF_annotated Source # 

Methods

toShATermAux :: ATermTable -> TFF_annotated -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFF_annotated] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFF_annotated)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFF_annotated])

ShATermConvertible TFX_annotated Source # 

Methods

toShATermAux :: ATermTable -> TFX_annotated -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TFX_annotated] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TFX_annotated)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TFX_annotated])

ShATermConvertible THF_annotated Source # 

Methods

toShATermAux :: ATermTable -> THF_annotated -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THF_annotated] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THF_annotated)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THF_annotated])

ShATermConvertible TPI_annotated Source # 

Methods

toShATermAux :: ATermTable -> TPI_annotated -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TPI_annotated] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TPI_annotated)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TPI_annotated])

ShATermConvertible Annotated_formula Source # 

Methods

toShATermAux :: ATermTable -> Annotated_formula -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Annotated_formula] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Annotated_formula)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Annotated_formula])

ShATermConvertible SystemComment Source # 

Methods

toShATermAux :: ATermTable -> SystemComment -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [SystemComment] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, SystemComment)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [SystemComment])

ShATermConvertible DefinedComment Source # 

Methods

toShATermAux :: ATermTable -> DefinedComment -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [DefinedComment] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, DefinedComment)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [DefinedComment])

ShATermConvertible Comment Source # 

Methods

toShATermAux :: ATermTable -> Comment -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Comment] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Comment)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Comment])

ShATermConvertible TPTP_input Source # 

Methods

toShATermAux :: ATermTable -> TPTP_input -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TPTP_input] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TPTP_input)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TPTP_input])

ShATermConvertible TPTP Source # 

Methods

toShATermAux :: ATermTable -> TPTP -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TPTP] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TPTP)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TPTP])

ShATermConvertible BASIC_SPEC Source # 

Methods

toShATermAux :: ATermTable -> BASIC_SPEC -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [BASIC_SPEC] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, BASIC_SPEC)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [BASIC_SPEC])

ShATermConvertible Sign Source # 

Methods

toShATermAux :: ATermTable -> Sign -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Sign] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Sign)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Sign])

ShATermConvertible Type_functorType Source # 

Methods

toShATermAux :: ATermTable -> Type_functorType -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Type_functorType] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Type_functorType)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Type_functorType])

ShATermConvertible PredicateType Source # 

Methods

toShATermAux :: ATermTable -> PredicateType -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [PredicateType] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, PredicateType)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [PredicateType])

ShATermConvertible FunctorType Source # 

Methods

toShATermAux :: ATermTable -> FunctorType -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FunctorType] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FunctorType)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FunctorType])

ShATermConvertible THFTypeable Source # 

Methods

toShATermAux :: ATermTable -> THFTypeable -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [THFTypeable] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, THFTypeable)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [THFTypeable])

ShATermConvertible SymbolType Source # 

Methods

toShATermAux :: ATermTable -> SymbolType -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [SymbolType] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, SymbolType)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [SymbolType])

ShATermConvertible Symbol Source # 

Methods

toShATermAux :: ATermTable -> Symbol -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Symbol] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Symbol)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Symbol])

ShATermConvertible Sublogic Source # 

Methods

toShATermAux :: ATermTable -> Sublogic -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Sublogic] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Sublogic)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Sublogic])