{- |

Module : ./TPTP/StaticAnalysis.hs

Description : Static Analysis for TPTP.

Copyright : (c) Eugen Kuksa University of Magdeburg 2017

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Eugen Kuksa <kuksa@iks.cs.ovgu.de>

Stability : provisional

Portability : portable

Static Analysis for TPTP.

-}

module TPTP.StaticAnalysis ( basicAnalysis

, signatureUnionR

, signOfSentence

) where

import TPTP.AS

import TPTP.Sign

import TPTP.Morphism

import Common.AS_Annotation hiding (Name)

import Common.ExtSign

import Common.GlobalAnnotations

import Common.Id

import Common.Result

import qualified Data.Map as Map

import qualified Data.Set as Set

basicAnalysis :: (BASIC_SPEC, Sign, GlobalAnnos)

-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence])

basicAnalysis (basicSpec, signOfIncludes, _) =

let ns = toNamedSen basicSpec

specSign = signOfSentences ns

nonImportedSyms = symbolsOfSign specSign

completeSignWithTypeConstants = specSign `signatureUnion` signOfIncludes

completeSign = postProcessSign completeSignWithTypeConstants

in return (basicSpec, ExtSign completeSign nonImportedSyms, ns)

toNamedSen :: BASIC_SPEC -> [Named Sentence]

toNamedSen (Basic_spec annotedItems) =

concatMap (toNamedSenTPTP . item) annotedItems

where

toNamedSenTPTP :: TPTP -> [Named Sentence]

toNamedSenTPTP (TPTP inputs) = concatMap toNamedSenI inputs

toNamedSenI :: TPTP_input -> [Named Sentence]

toNamedSenI i = case i of

Annotated_formula af ->

[(makeNamed (nameS af) af) { isAxiom = formulaIsAxiom af

, isDef = formulaIsDef af

, wasTheorem = formulaWasTheorem af

}]

_ -> []

formulaIsAxiom :: Annotated_formula -> Bool

formulaIsAxiom af = case formulaRole af of

Conjecture -> False

Negated_conjecture -> False

_ -> True

formulaIsDef :: Annotated_formula -> Bool

formulaIsDef af = case formulaRole af of

Definition -> True

_ -> False

formulaWasTheorem :: Annotated_formula -> Bool

formulaWasTheorem af = case formulaRole af of

Theorem -> True

Lemma -> True

_ -> False

signatureUnionR :: Sign -> Sign -> Result Sign

signatureUnionR s1 s2 = Result [Diag Debug "All fine sigUnion" nullRange]

$ Just $ postProcessSign $ signatureUnion s1 s2

signatureUnion :: Sign -> Sign -> Sign

signatureUnion s1 s2 =

Sign { constantSet = constantSet s1 `Set.union` constantSet s2

, numberSet = numberSet s1 `Set.union` numberSet s2

, propositionSet = propositionSet s1 `Set.union` propositionSet s2

, thfPredicateMap = thfPredicateMap s1 `Map.union` thfPredicateMap s2

, tffPredicateMap = tffPredicateMap s1 `Map.union` tffPredicateMap s2

, fofPredicateMap = unionFOFPredicate (fofPredicateMap s1) (fofPredicateMap s2)

, fofFunctorMap = unionFOFFunctor (fofFunctorMap s1) (fofFunctorMap s2)

, thfTypeConstantMap = thfTypeConstantMap s1 `Map.union` thfTypeConstantMap s2

, tffTypeConstantMap = tffTypeConstantMap s1 `Map.union` tffTypeConstantMap s2

, thfTypeFunctorMap = thfTypeFunctorMap s1 `Map.union` thfTypeFunctorMap s2

, tffTypeFunctorMap = tffTypeFunctorMap s1 `Map.union` tffTypeFunctorMap s2

, thfSubtypeMap = thfSubtypeMap s1 `Map.union` thfSubtypeMap s2

, tffSubtypeMap = tffSubtypeMap s1 `Map.union` tffSubtypeMap s2

, thfTypeDeclarationMap = thfTypeDeclarationMap s1 `Map.union` thfTypeDeclarationMap s2

, tffTypeDeclarationMap = tffTypeDeclarationMap s1 `Map.union` tffTypeDeclarationMap s2

}

where

unionFOFPredicate :: FOFPredicateMap -> FOFPredicateMap -> FOFPredicateMap

unionFOFPredicate = Map.unionWith Set.union

unionFOFFunctor :: FOFFunctorMap -> FOFFunctorMap -> FOFFunctorMap

unionFOFFunctor = Map.unionWith Set.union

signatureUnions :: [Sign] -> Sign

signatureUnions signs = foldr signatureUnion emptySign signs

signOfSentences :: [Named Sentence] -> Sign

signOfSentences nss =

postProcessSign $

foldr (\ sign result -> signatureUnion sign result) emptySign $

map (signOfSentenceNaive . sentence) nss

postProcessSign :: Sign -> Sign

postProcessSign = partitionTypeDeclarations . removeTypeDeclarationsFromConstantSet

where

partitionTypeDeclarations :: Sign -> Sign

partitionTypeDeclarations sign =

let (thfPredicates, thfRemainder) =

Map.partition isTHFBooleanType $ thfTypeDeclarationMap sign

(thfTypes, thfRemainder') = Map.partition isTHFType thfRemainder

(tffPredicates, tffRemainder) =

Map.partition isTFFBooleanType $ tffTypeDeclarationMap sign

(tffTypes, tffRemainder') = Map.partition isTFFType tffRemainder

in sign { thfPredicateMap = thfPredicates

, thfTypeConstantMap = thfTypes

, thfTypeFunctorMap = thfRemainder'

, tffPredicateMap = tffPredicates

, tffTypeConstantMap = tffTypes

, tffTypeFunctorMap = tffRemainder'

}

-- Type helpers

isTHFBooleanType :: THF_top_level_type -> Bool

isTHFBooleanType x = case x of

THFTLT_unitary (THFUT_unitary (THFUF_atom (THF_atom_function (THFF_atom (Atom_constant (DF_atomic_defined_word w)))))) -> tokStr w == "$o"

THFTLT_mapping types -> isTHFBooleanType $ THFTLT_unitary $ last types

_ -> False

isTHFType :: THF_top_level_type -> Bool

isTHFType x = case x of

THFTLT_unitary (THFUT_unitary (THFUF_atom (THF_atom_function (THFF_atom (Atom_constant (DF_atomic_defined_word w)))))) -> tokStr w == "$tType"

_ -> False

isTFFBooleanType :: TFF_top_level_type -> Bool

isTFFBooleanType x = case x of

TFFTLT_mapping (TFF_mapping_type _ (TFFAT_defined O)) -> True

_ -> False

isTFFType :: TFF_top_level_type -> Bool

isTFFType x = case x of

TFFTLT_atomic (TFFAT_defined TType) -> True

_ -> False

removeTypeDeclarationsFromConstantSet :: Sign -> Sign

removeTypeDeclarationsFromConstantSet sign =

let tffTypeKeys = Map.keysSet $ tffTypeDeclarationMap sign

tffTypeNames = Set.map unpackConstant $ Set.filter isConstant $ tffTypeKeys

thfTypeKeys = Map.keysSet $ thfTypeDeclarationMap sign

thfTypeNames = Set.map unpackConstantTHF $ Set.filter isConstantTHF $

thfTypeKeys

typeNames = tffTypeNames `Set.union` thfTypeNames

in sign { constantSet = constantSet sign Set.\\ typeNames }

isConstant :: Untyped_atom -> Bool

isConstant ua = case ua of

UA_constant _ -> True

_ -> False

unpackConstant :: Untyped_atom -> Constant

unpackConstant ua = case ua of

UA_constant c -> c

_ -> error "Error in TPTP.StaticAnalysis.unpackConstant: Non-constant encountered."

isConstantTHF :: THFTypeable -> Bool

isConstantTHF x = case x of

THFTypeConstant _ -> True

_ -> False

unpackConstantTHF :: THFTypeable -> Constant

unpackConstantTHF x = case x of

THFTypeConstant c -> c

_ -> error "Error in TPTP.StaticAnalysis.unpackConstant: Non-constant encountered."

signOfSentence :: Sentence -> Sign

signOfSentence sen = signOfSentences [makeNamed "" sen]

signOfSentenceNaive :: Sentence -> Sign

signOfSentenceNaive sen = case sen of

AF_THF_Annotated f -> signOfTHF_annotated f

AF_TFX_Annotated f -> signOfTFX_annotated f

AF_TFF_Annotated f -> signOfTFF_annotated f

AF_TCF_Annotated f -> signOfTCF_annotated f

AF_FOF_Annotated f -> signOfFOF_annotated f

AF_CNF_Annotated f -> signOfCNF_annotated f

AF_TPI_Annotated f -> signOfTPI_annotated f

signOfTPI_annotated :: TPI_annotated -> Sign

signOfTPI_annotated x = case x of

TPI_annotated _ _ f _ -> signOfFOF_formula f

signOfTHF_annotated :: THF_annotated -> Sign

signOfTHF_annotated x = case x of

THF_annotated _ _ f _ -> signOfTHF_formula f

signOfTFX_annotated :: TFX_annotated -> Sign

signOfTFX_annotated x = case x of

TFX_annotated _ _ f _ -> signOfTFX_formula f

signOfTFF_annotated :: TFF_annotated -> Sign

signOfTFF_annotated x = case x of

TFF_annotated _ _ f _ -> signOfTFF_formula f

signOfTCF_annotated :: TCF_annotated -> Sign

signOfTCF_annotated x = case x of

TCF_annotated _ _ f _ -> signOfTCF_formula f

signOfFOF_annotated :: FOF_annotated -> Sign

signOfFOF_annotated x = case x of

FOF_annotated _ _ f _ -> signOfFOF_formula f

signOfCNF_annotated :: CNF_annotated -> Sign

signOfCNF_annotated x = case x of

CNF_annotated _ _ f _ -> signOfCNF_formula f

-- signOfAnnotations :: Annotations -> Sign

-- signOfAnnotations _ = emptySign

-- signOfFormula_role :: Formula_role -> Sign

-- signOfFormula_role _ = emptySign

signOfTHF_formula :: THF_formula -> Sign

signOfTHF_formula x = case x of

THFF_logic f -> signOfTHF_logic_formula f

THFF_sequent s -> signOfTHF_sequent s

signOfTHF_logic_formula :: THF_logic_formula -> Sign

signOfTHF_logic_formula x = case x of

THFLF_binary f -> signOfTHF_binary_formula f

THFLF_unitary f -> signOfTHF_unitary_formula f

THFLF_type f -> signOfTHF_type_formula f

THFLF_subtype f -> signOfTHF_subtype f

signOfTHF_binary_formula :: THF_binary_formula -> Sign

signOfTHF_binary_formula x = case x of

THFBF_pair a -> signOfTHF_binary_pair a

THFBF_tuple a -> signOfTHF_binary_tuple a

signOfTHF_binary_pair :: THF_binary_pair -> Sign

signOfTHF_binary_pair x = case x of

THF_binary_pair _ f1 f2 ->

signatureUnions $ map signOfTHF_unitary_formula [f1, f2]

signOfTHF_binary_tuple :: THF_binary_tuple -> Sign

signOfTHF_binary_tuple x = case x of

THFBT_or fs -> signOfTHF_or_formula fs

THFBT_and fs -> signOfTHF_and_formula fs

THFBT_apply fs -> signOfTHF_apply_formula fs

signOfTHF_or_formula :: THF_or_formula -> Sign

signOfTHF_or_formula = signatureUnions . map signOfTHF_unitary_formula

signOfTHF_and_formula :: THF_or_formula -> Sign

signOfTHF_and_formula = signatureUnions . map signOfTHF_unitary_formula

signOfTHF_apply_formula :: THF_or_formula -> Sign

signOfTHF_apply_formula = signatureUnions . map signOfTHF_unitary_formula

signOfTHF_unitary_formula :: THF_unitary_formula -> Sign

signOfTHF_unitary_formula x = case x of

THFUF_quantified a -> signOfTHF_quantified_formula a

THFUF_unary a -> signOfTHF_unary_formula a

THFUF_atom a -> signOfTHF_atom a

THFUF_conditional a -> signOfTHF_conditional a

THFUF_let a -> signOfTHF_let a

THFUF_tuple a -> signOfTHF_tuple a

THFUF_logic a -> signOfTHF_logic_formula a

signOfTHF_quantified_formula :: THF_quantified_formula -> Sign

signOfTHF_quantified_formula x = case x of

THF_quantified_formula q f ->

signatureUnions [signOfTHF_quantification q, signOfTHF_unitary_formula f]

signOfTHF_quantification :: THF_quantification -> Sign

signOfTHF_quantification x = case x of

THF_quantification q vars ->

signatureUnions [signOfTHF_quantifier q, signOfTHF_variable_list vars]

signOfTHF_variable_list :: THF_variable_list -> Sign

signOfTHF_variable_list = signatureUnions . map signOfTHF_variable

signOfTHF_variable :: THF_variable -> Sign

signOfTHF_variable x = case x of

THFV_typed a -> signOfTHF_typed_variable a

THFV_variable a -> signOfVariable a

signOfTHF_typed_variable :: THF_typed_variable -> Sign

signOfTHF_typed_variable x = case x of

THF_typed_variable v tlt ->

signatureUnions [signOfVariable v, signOfTHF_top_level_type tlt]

signOfTHF_unary_formula :: THF_unary_formula -> Sign

signOfTHF_unary_formula x = case x of

THF_unary_formula c f ->

signatureUnions [signOfTHF_unary_connective c, signOfTHF_logic_formula f]

signOfTHF_atom :: THF_atom -> Sign

signOfTHF_atom x = case x of

THF_atom_function a -> signOfTHF_function a

THF_atom_variable a -> signOfVariable a

THF_atom_defined a -> signOfDefined_term a

THF_atom_conn a -> signOfTHF_conn_term a

signOfTHF_function :: THF_function -> Sign

signOfTHF_function x = case x of

THFF_atom a -> signOfAtom a

THFF_functor f args ->

signatureUnions [ signOfTPTP_functor f $ length args

, signOfTHF_arguments args]

THFF_defined f args ->

signatureUnions [signOfDefined_functor f, signOfTHF_arguments args]

THFF_system f args ->

signatureUnions [signOfSystem_functor f, signOfTHF_arguments args]

signOfTHF_conn_term :: THF_conn_term -> Sign

signOfTHF_conn_term x = case x of

THFC_pair a -> signOfTHF_pair_connective a

THFC_assoc a -> signOfAssoc_connective a

THFC_unary a -> signOfTHF_unary_connective a

signOfTHF_conditional :: THF_conditional -> Sign

signOfTHF_conditional x = case x of

THF_conditional f_if f_then f_else ->

signatureUnions $ map signOfTHF_logic_formula [f_if, f_then, f_else]

signOfTHF_let :: THF_let -> Sign

signOfTHF_let x = case x of

THF_let defns f ->

signatureUnions [signOfTHF_let_defns defns, signOfTHF_formula f]

signOfTHF_let_defns :: THF_let_defns -> Sign

signOfTHF_let_defns x = case x of

THFLD_single a -> signOfTHF_let_defn a

THFLD_many a -> signOfTHF_let_defn_list a

signOfTHF_let_defn_list :: THF_let_defn_list -> Sign

signOfTHF_let_defn_list = signatureUnions . map signOfTHF_let_defn

signOfTHF_let_defn :: THF_let_defn -> Sign

signOfTHF_let_defn x = case x of

THFLD_quantified a -> signOfTHF_let_quantified_defn a

THFLD_plain a -> signOfTHF_let_plain_defn a

signOfTHF_let_quantified_defn :: THF_let_quantified_defn -> Sign

signOfTHF_let_quantified_defn x = case x of

THF_let_quantified_defn q lpd ->

signatureUnions [signOfTHF_quantification q, signOfTHF_let_plain_defn lpd]

signOfTHF_let_plain_defn :: THF_let_plain_defn -> Sign

signOfTHF_let_plain_defn x = case x of

THF_let_plain_defn lhs f ->

signatureUnions [signOfTHF_let_defn_LHS lhs, signOfTHF_formula f]

signOfTHF_let_defn_LHS :: THF_let_defn_LHS -> Sign

signOfTHF_let_defn_LHS x = case x of

THFLDL_constant a -> signOfConstant a

THFLDL_functor f args ->

signatureUnions [ signOfTPTP_functor f $ length args

, signOfFOF_arguments args]

THFLDL_tuple a -> signOfTHF_tuple a

signOfTHF_arguments :: THF_arguments -> Sign

signOfTHF_arguments = signOfTHF_formula_list

signOfTHF_type_formula :: THF_type_formula -> Sign

signOfTHF_type_formula x = case x of

THFTF_typeable f tlt -> signatureUnions

[ emptySign { thfTypeDeclarationMap = Map.singleton (THFTypeFormula f) tlt }

, signOfTHF_typeable_formula f

, signOfTHF_top_level_type tlt

]

THFTF_constant c tlt -> signatureUnions

[ emptySign { thfTypeDeclarationMap = Map.singleton (THFTypeConstant c) tlt }

, signOfConstant c

, signOfTHF_top_level_type tlt

]

signOfTHF_typeable_formula :: THF_typeable_formula -> Sign

signOfTHF_typeable_formula x = case x of

THFTF_atom a -> signOfTHF_atom a

THFTF_logic a -> signOfTHF_logic_formula a

signOfTHF_subtype :: THF_subtype -> Sign

signOfTHF_subtype x = case x of

THF_subtype a1 a2 -> signatureUnions

[ emptySign { thfSubtypeMap = Map.singleton a1 a2 }

, signOfTHF_atom a1, signOfTHF_atom a2

]

signOfTHF_top_level_type :: THF_top_level_type -> Sign

signOfTHF_top_level_type x = case x of

THFTLT_unitary a -> signOfTHF_unitary_type a

THFTLT_mapping a -> signOfTHF_mapping_type a

signOfTHF_unitary_type :: THF_unitary_type -> Sign

signOfTHF_unitary_type x = case x of

THFUT_unitary a -> signOfTHF_unitary_formula a

THFUT_binary a -> signOfTHF_binary_type a

signOfTHF_binary_type :: THF_binary_type -> Sign

signOfTHF_binary_type x = case x of

THFBT_mapping a -> signOfTHF_mapping_type a

THFBT_xprod a -> signOfTHF_xprod_type a

THFBT_union a -> signOfTHF_union_type a

signOfTHF_mapping_type :: THF_mapping_type -> Sign

signOfTHF_mapping_type = signatureUnions . map signOfTHF_unitary_type

signOfTHF_xprod_type :: THF_xprod_type -> Sign

signOfTHF_xprod_type = signatureUnions . map signOfTHF_unitary_type

signOfTHF_union_type :: THF_union_type -> Sign

signOfTHF_union_type = signatureUnions . map signOfTHF_unitary_type

signOfTHF_sequent :: THF_sequent -> Sign

signOfTHF_sequent x = case x of

THFS_plain t1 t2 -> signatureUnions $ map signOfTHF_tuple [t1, t2]

THFS_parens a -> signOfTHF_sequent a

signOfTHF_tuple :: THF_tuple -> Sign

signOfTHF_tuple x = case x of

THF_tuple a -> signOfTHF_formula_list a

signOfTHF_formula_list :: THF_formula_list -> Sign

signOfTHF_formula_list = signatureUnions . map signOfTHF_logic_formula

signOfTFX_formula :: TFX_formula -> Sign

signOfTFX_formula x = case x of

TFXF_logic a -> signOfTFX_logic_formula a

TFXF_sequent a -> signOfTHF_sequent a

signOfTFX_logic_formula :: TFX_logic_formula -> Sign

signOfTFX_logic_formula x = case x of

TFXLF_binary a -> signOfTHF_binary_formula a

TFXLF_unitary a -> signOfTHF_unitary_formula a

TFXLF_typed a -> signOfTFF_typed_atom a

TFXLF_subtype a -> signOfTFF_subtype a

signOfTFF_formula :: TFF_formula -> Sign

signOfTFF_formula x = case x of

TFFF_logic a -> signOfTFF_logic_formula a

TFFF_atom a -> signOfTFF_typed_atom a

TFFF_sequent a -> signOfTFF_sequent a

signOfTFF_logic_formula :: TFF_logic_formula -> Sign

signOfTFF_logic_formula x = case x of

TFFLF_binary a -> signOfTFF_binary_formula a

TFFLF_unitary a -> signOfTFF_unitary_formula a

TFFLF_subtype a -> signOfTFF_subtype a

signOfTFF_binary_formula :: TFF_binary_formula -> Sign

signOfTFF_binary_formula x = case x of

TFFBF_nonassoc a -> signOfTFF_binary_nonassoc a

TFFBF_assoc a -> signOfTFF_binary_assoc a

signOfTFF_binary_nonassoc :: TFF_binary_nonassoc -> Sign

signOfTFF_binary_nonassoc x = case x of

TFF_binary_nonassoc c f1 f2 ->

signatureUnions $

signOfBinary_connective c : map signOfTFF_unitary_formula [f1, f2]

signOfTFF_binary_assoc :: TFF_binary_assoc -> Sign

signOfTFF_binary_assoc x = case x of

TFFBA_or a -> signOfTFF_or_formula a

TFFBA_and a -> signOfTFF_and_formula a

signOfTFF_or_formula :: TFF_or_formula -> Sign

signOfTFF_or_formula = signatureUnions . map signOfTFF_unitary_formula

signOfTFF_and_formula :: TFF_and_formula -> Sign

signOfTFF_and_formula = signatureUnions . map signOfTFF_unitary_formula

signOfTFF_unitary_formula :: TFF_unitary_formula -> Sign

signOfTFF_unitary_formula x = case x of

TFFUF_quantified a -> signOfTFF_quantified_formula a

TFFUF_unary a -> signOfTFF_unary_formula a

TFFUF_atomic a -> signOfTFF_atomic_formula a

TFFUF_conditional a -> signOfTFF_conditional a

TFFUF_let a -> signOfTFF_let a

TFFUF_logic a -> signOfTFF_logic_formula a

signOfTFF_quantified_formula :: TFF_quantified_formula -> Sign

signOfTFF_quantified_formula x = case x of

TFF_quantified_formula q vars f ->

signatureUnions [ signOfFOF_quantifier q

, signOfTFF_variable_list vars

, signOfTFF_unitary_formula f

]

signOfTFF_variable_list :: TFF_variable_list -> Sign

signOfTFF_variable_list = signatureUnions . map signOfTFF_variable

signOfTFF_variable :: TFF_variable -> Sign

signOfTFF_variable x = case x of

TFFV_typed a -> signOfTFF_typed_variable a

TFFV_variable a -> signOfVariable a

signOfTFF_typed_variable :: TFF_typed_variable -> Sign

signOfTFF_typed_variable x = case x of

TFF_typed_variable v t ->

signatureUnions [signOfVariable v, signOfTFF_atomic_type t]

signOfTFF_unary_formula :: TFF_unary_formula -> Sign

signOfTFF_unary_formula x = case x of

TFFUF_connective c f ->

signatureUnions [signOfUnary_connective c, signOfTFF_unitary_formula f]

TFFUF_infix a -> signOfFOF_infix_unary a

signOfTFF_atomic_formula :: TFF_atomic_formula -> Sign

signOfTFF_atomic_formula = signOfFOF_atomic_formula

signOfTFF_conditional :: TFF_conditional -> Sign

signOfTFF_conditional x = case x of

TFF_conditional f_if f_then f_else ->

signatureUnions $ map signOfTFF_logic_formula [f_if, f_then, f_else]

signOfTFF_let :: TFF_let -> Sign

signOfTFF_let x = case x of

TFF_let_term_defns defns f ->

signatureUnions [signOfTFF_let_term_defns defns, signOfTFF_formula f]

TFF_let_formula_defns defns f ->

signatureUnions [signOfTFF_let_formula_defns defns, signOfTFF_formula f]

signOfTFF_let_term_defns :: TFF_let_term_defns -> Sign

signOfTFF_let_term_defns x = case x of

TFFLTD_single a -> signOfTFF_let_term_defn a

TFFLTD_many a -> signOfTFF_let_term_list a

signOfTFF_let_term_list :: TFF_let_term_list -> Sign

signOfTFF_let_term_list = signatureUnions . map signOfTFF_let_term_defn

signOfTFF_let_term_defn :: TFF_let_term_defn -> Sign

signOfTFF_let_term_defn x = case x of

TFFLTD_variable vars defn ->

signatureUnions [ signOfTFF_variable_list vars

, signOfTFF_let_term_defn defn

]

TFFLTD_binding a -> signOfTFF_let_term_binding a

signOfTFF_let_term_binding :: TFF_let_term_binding -> Sign

signOfTFF_let_term_binding x = case x of

TFFLTB_plain pt t ->

signatureUnions [signOfFOF_plain_term pt, signOfFOF_term t]

TFFLTB_binding a -> signOfTFF_let_term_binding a

signOfTFF_let_formula_defns :: TFF_let_formula_defns -> Sign

signOfTFF_let_formula_defns x = case x of

TFFLFD_single a -> signOfTFF_let_formula_defn a

TFFLFD_many a -> signOfTFF_let_formula_list a

signOfTFF_let_formula_list :: TFF_let_formula_list -> Sign

signOfTFF_let_formula_list = signatureUnions . map signOfTFF_let_formula_defn

signOfTFF_let_formula_defn :: TFF_let_formula_defn -> Sign

signOfTFF_let_formula_defn x = case x of

TFFLFD_variable vars defn ->

signatureUnions [ signOfTFF_variable_list vars

, signOfTFF_let_formula_defn defn

]

TFFLFD_binding a -> signOfTFF_let_formula_binding a

signOfTFF_let_formula_binding :: TFF_let_formula_binding -> Sign

signOfTFF_let_formula_binding x = case x of

TFFLFB_plain paf uf ->

signatureUnions [ signOfFOF_plain_atomic_formula paf

, signOfTFF_unitary_formula uf

]

TFFLFB_binding a -> signOfTFF_let_formula_binding a

signOfTFF_sequent :: TFF_sequent -> Sign

signOfTFF_sequent x = case x of

TFFS_plain t1 t2 -> signatureUnions $ map signOfTFF_formula_tuple [t1, t2]

TFFS_parens a -> signOfTFF_sequent a

signOfTFF_formula_tuple :: TFF_formula_tuple -> Sign

signOfTFF_formula_tuple x = case x of

TFF_formula_tuple a -> signOfTFF_formula_tuple_list a

signOfTFF_formula_tuple_list :: TFF_formula_tuple_list -> Sign

signOfTFF_formula_tuple_list = signatureUnions . map signOfTFF_logic_formula

signOfTFF_typed_atom :: TFF_typed_atom -> Sign

signOfTFF_typed_atom x = case x of

TFFTA_plain ua tlt -> signatureUnions

[ emptySign { tffTypeDeclarationMap = Map.singleton ua tlt }

, signOfUntyped_atom ua

, signOfTFF_top_level_type tlt

]

TFFTA_parens a -> signOfTFF_typed_atom a

signOfTFF_subtype :: TFF_subtype -> Sign

signOfTFF_subtype x = case x of

TFF_subtype ua a -> signatureUnions

[ emptySign { tffSubtypeMap = Map.singleton ua a }

, signOfUntyped_atom ua, signOfAtom a

]

signOfTFF_top_level_type :: TFF_top_level_type -> Sign

signOfTFF_top_level_type x = case x of

TFFTLT_atomic a -> signOfTFF_atomic_type a

TFFTLT_mapping a -> signOfTFF_mapping_type a

TFFTLT_quantified a -> signOfTF1_quantified_type a

TFFTLT_parens a -> signOfTFF_top_level_type a

signOfTF1_quantified_type :: TF1_quantified_type -> Sign

signOfTF1_quantified_type x = case x of

TF1_quantified_type vars t ->

signatureUnions [ signOfTFF_variable_list vars

, signOfTFF_monotype t

]

signOfTFF_monotype :: TFF_monotype -> Sign

signOfTFF_monotype x = case x of

TFFMT_atomic a -> signOfTFF_atomic_type a

TFFMT_mapping a -> signOfTFF_mapping_type a

signOfTFF_unitary_type :: TFF_unitary_type -> Sign

signOfTFF_unitary_type x = case x of

TFFUT_atomic a -> signOfTFF_atomic_type a

TFFUT_xprod a -> signOfTFF_xprod_type a

signOfTFF_atomic_type :: TFF_atomic_type -> Sign

signOfTFF_atomic_type x = case x of

TFFAT_constant a -> signOfType_constant a

TFFAT_defined a -> signOfDefined_type a

TFFAT_functor f args ->

signatureUnions [signOfType_functor f, signOfTFF_type_arguments args]

TFFAT_variable a -> signOfVariable a

signOfTFF_type_arguments :: TFF_type_arguments -> Sign

signOfTFF_type_arguments = signatureUnions . map signOfTFF_atomic_type

signOfTFF_mapping_type :: TFF_mapping_type -> Sign

signOfTFF_mapping_type x = case x of

TFF_mapping_type ut at ->

signatureUnions [signOfTFF_unitary_type ut, signOfTFF_atomic_type at]

signOfTFF_xprod_type :: TFF_xprod_type -> Sign

signOfTFF_xprod_type x = case x of

TFF_xprod_type ut ats ->

signatureUnions $ signOfTFF_unitary_type ut : map signOfTFF_atomic_type ats

signOfTCF_formula :: TCF_formula -> Sign

signOfTCF_formula x = case x of

TCFF_logic a -> signOfTCF_logic_formula a

TCFF_atom a -> signOfTFF_typed_atom a

signOfTCF_logic_formula :: TCF_logic_formula -> Sign

signOfTCF_logic_formula x = case x of

TCFLF_quantified a -> signOfTCF_quantified_formula a

TCFLF_cnf a -> signOfCNF_formula a

signOfTCF_quantified_formula :: TCF_quantified_formula -> Sign

signOfTCF_quantified_formula x = case x of

TCF_quantified vars f ->

signatureUnions [ signOfTFF_variable_list vars

, signOfCNF_formula f

]

signOfFOF_formula :: FOF_formula -> Sign

signOfFOF_formula x = case x of

FOFF_logic a -> signOfFOF_logic_formula a

FOFF_sequent a -> signOfFOF_sequent a

signOfFOF_logic_formula :: FOF_logic_formula -> Sign

signOfFOF_logic_formula x = case x of

FOFLF_binary a -> signOfFOF_binary_formula a

FOFLF_unitary a -> signOfFOF_unitary_formula a

signOfFOF_binary_formula :: FOF_binary_formula -> Sign

signOfFOF_binary_formula x = case x of

FOFBF_nonassoc a -> signOfFOF_binary_nonassoc a

FOFBF_assoc a -> signOfFOF_binary_assoc a

signOfFOF_binary_nonassoc :: FOF_binary_nonassoc -> Sign

signOfFOF_binary_nonassoc x = case x of

FOF_binary_nonassoc c f1 f2 ->

signatureUnions $

signOfBinary_connective c : map signOfFOF_unitary_formula [f1, f2]

signOfFOF_binary_assoc :: FOF_binary_assoc -> Sign

signOfFOF_binary_assoc x = case x of

FOFBA_or a -> signOfFOF_or_formula a

FOFBA_and a -> signOfFOF_and_formula a

signOfFOF_or_formula :: FOF_or_formula -> Sign

signOfFOF_or_formula = signatureUnions . map signOfFOF_unitary_formula

signOfFOF_and_formula :: FOF_and_formula -> Sign

signOfFOF_and_formula = signatureUnions . map signOfFOF_unitary_formula

signOfFOF_unitary_formula :: FOF_unitary_formula -> Sign

signOfFOF_unitary_formula x = case x of

FOFUF_quantified a -> signOfFOF_quantified_formula a

FOFUF_unary a -> signOfFOF_unary_formula a

FOFUF_atomic a -> signOfFOF_atomic_formula a

FOFUF_logic a -> signOfFOF_logic_formula a

signOfFOF_quantified_formula :: FOF_quantified_formula -> Sign

signOfFOF_quantified_formula x = case x of

FOF_quantified_formula q vars f ->

signatureUnions [ signOfFOF_quantifier q

, signOfFOF_variable_list vars

, signOfFOF_unitary_formula f

]

signOfFOF_variable_list :: FOF_variable_list -> Sign

signOfFOF_variable_list = signatureUnions . map signOfVariable

signOfFOF_unary_formula :: FOF_unary_formula -> Sign

signOfFOF_unary_formula x = case x of

FOFUF_connective c f ->

signatureUnions [signOfUnary_connective c, signOfFOF_unitary_formula f]

FOFUF_infix a -> signOfFOF_infix_unary a

signOfFOF_infix_unary :: FOF_infix_unary -> Sign

signOfFOF_infix_unary x = case x of

FOF_infix_unary t1 t2 ->

signatureUnions $ map signOfFOF_term [t1, t2]

signOfFOF_atomic_formula :: FOF_atomic_formula -> Sign

signOfFOF_atomic_formula x = case x of

FOFAT_plain a -> signOfFOF_plain_atomic_formula a

FOFAT_defined a -> signOfFOF_defined_atomic_formula a

FOFAT_system a -> signOfFOF_system_atomic_formula a

signOfFOF_plain_atomic_formula :: FOF_plain_atomic_formula -> Sign

signOfFOF_plain_atomic_formula x = case x of

FOFPAF_proposition a -> signOfProposition a

FOFPAF_predicate p args ->

signatureUnions [signOfPredicate p $ length args, signOfFOF_arguments args]

signOfFOF_defined_atomic_formula :: FOF_defined_atomic_formula -> Sign

signOfFOF_defined_atomic_formula x = case x of

FOFDAF_plain a -> signOfFOF_defined_plain_formula a

FOFDAF_infix a -> signOfFOF_defined_infix_formula a

signOfFOF_defined_plain_formula :: FOF_defined_plain_formula -> Sign

signOfFOF_defined_plain_formula x = case x of

FOFDPF_proposition a -> signOfDefined_proposition a

FOFDPF_predicate p args ->

signatureUnions [signOfDefined_predicate p, signOfFOF_arguments args]

signOfFOF_defined_infix_formula :: FOF_defined_infix_formula -> Sign

signOfFOF_defined_infix_formula x = case x of

FOF_defined_infix_formula dip t1 t2 -> signatureUnions

[signOfFOF_term t1, signOfDefined_infix_pred dip, signOfFOF_term t2]

signOfFOF_system_atomic_formula :: FOF_system_atomic_formula -> Sign

signOfFOF_system_atomic_formula x = case x of

FOF_system_atomic_formula a -> signOfFOF_system_term a

signOfFOF_plain_term :: FOF_plain_term -> Sign

signOfFOF_plain_term x = case x of

FOFPT_constant a -> signOfConstant a

FOFPT_functor f args ->

signatureUnions [ signOfTPTP_functor f $ length args

, signOfFOF_arguments args]

signOfFOF_defined_term :: FOF_defined_term -> Sign

signOfFOF_defined_term x = case x of

FOFDT_term a -> signOfDefined_term a

FOFDT_atomic a -> signOfFOF_defined_atomic_term a

signOfFOF_defined_atomic_term :: FOF_defined_atomic_term -> Sign

signOfFOF_defined_atomic_term x = case x of

FOFDAT_plain a -> signOfFOF_defined_plain_term a

-- | FOFDAT_indix a -> signOfDefined_infix_term a

signOfFOF_defined_plain_term :: FOF_defined_plain_term -> Sign

signOfFOF_defined_plain_term x = case x of

FOFDPT_constant a -> signOfDefined_constant a

FOFDPT_functor f args ->

signatureUnions [signOfDefined_functor f, signOfFOF_arguments args]

signOfFOF_system_term :: FOF_system_term -> Sign

signOfFOF_system_term x = case x of

FOFST_constant a -> signOfSystem_constant a

FOFST_functor f args ->

signatureUnions [signOfSystem_functor f, signOfFOF_arguments args]

signOfFOF_arguments :: FOF_arguments -> Sign

signOfFOF_arguments = signatureUnions . map signOfFOF_term

signOfFOF_term :: FOF_term -> Sign

signOfFOF_term x = case x of

FOFT_function a -> signOfFOF_function_term a

FOFT_variable a -> signOfVariable a

FOFT_conditional a -> signOfTFF_conditional_term a

FOFT_let a -> signOfTFF_let_term a

signOfFOF_function_term :: FOF_function_term -> Sign

signOfFOF_function_term x = case x of

FOFFT_plain a -> signOfFOF_plain_term a

FOFFT_defined a -> signOfFOF_defined_term a

FOFFT_system a -> signOfFOF_system_term a

signOfTFF_conditional_term :: TFF_conditional_term -> Sign

signOfTFF_conditional_term x = case x of

TFF_conditional_term f_if t_then t_else ->

signatureUnions $

signOfTFF_logic_formula f_if : map signOfFOF_term [t_then, t_else]

signOfTFF_let_term :: TFF_let_term -> Sign

signOfTFF_let_term x = case x of

TFFLT_formula defns t ->

signatureUnions [signOfTFF_let_formula_defns defns, signOfFOF_term t]

TFFLT_term defns t ->

signatureUnions [signOfTFF_let_term_defns defns, signOfFOF_term t]

{-

%----This section is the FOFX syntax. Not yet in use.

% <fof_let> ::= := [<fof_let_list>] : <fof_unitary_formula>

% <fof_let_list> ::= <fof_defined_var> |

% <fof_defined_var>,<fof_let_list>

% <fof_defined_var> ::= <variable> := <fof_logic_formula> |

% <variable> :- <fof_term> | (<fof_defined_var>)

%

% <fof_conditional> ::= $ite_f(<fof_logic_formula>,<fof_logic_formula>,

% <fof_logic_formula>)

%

% <fof_conditional_term> ::= $ite_t(<fof_logic_formula>,<fof_term>,<fof_term>)

-}

signOfFOF_sequent :: FOF_sequent -> Sign

signOfFOF_sequent x = case x of

FOFS_plain t1 t2 ->

signatureUnions $ map signOfFOF_formula_tuple [t1, t2]

FOFS_parens a -> signOfFOF_sequent a

signOfFOF_formula_tuple :: FOF_formula_tuple -> Sign

signOfFOF_formula_tuple x = case x of

FOF_formula_tuple a -> signOfFOF_formula_tuple_list a

signOfFOF_formula_tuple_list :: FOF_formula_tuple_list -> Sign

signOfFOF_formula_tuple_list = signatureUnions . map signOfFOF_logic_formula

signOfCNF_formula :: CNF_formula -> Sign

signOfCNF_formula x = case x of

CNFF_plain a -> signOfDisjunction a

CNFF_parens a -> signOfDisjunction a

signOfDisjunction :: Disjunction -> Sign

signOfDisjunction x = case x of

Disjunction ls -> signatureUnions $ map signOfLiteral ls

signOfLiteral :: Literal -> Sign

signOfLiteral x = case x of

Lit_atomic a -> signOfFOF_atomic_formula a

Lit_negative a -> signOfFOF_atomic_formula a

Lit_fof_infix a -> signOfFOF_infix_unary a

signOfTHF_quantifier :: THF_quantifier -> Sign

signOfTHF_quantifier x = case x of

THFQ_fof a -> signOfFOF_quantifier a

THFQ_th0 a -> signOfTH0_quantifier a

THFQ_th1 a -> signOfTH1_quantifier a

signOfTH1_quantifier :: TH1_quantifier -> Sign

signOfTH1_quantifier x = case x of

TH1_DependentProduct -> emptySign

TH1_DependentSum -> emptySign

signOfTH0_quantifier :: TH0_quantifier -> Sign

signOfTH0_quantifier x = case x of

TH0_LambdaBinder -> emptySign

TH0_IndefiniteDescription -> emptySign

TH0_DefiniteDescription -> emptySign

signOfTHF_pair_connective :: THF_pair_connective -> Sign

signOfTHF_pair_connective x = case x of

THF_infix_equality -> emptySign

Infix_inequality -> emptySign

THFPC_binary a -> signOfBinary_connective a

THF_assignment -> emptySign

signOfTHF_unary_connective :: THF_unary_connective -> Sign

signOfTHF_unary_connective x = case x of

THFUC_unary a -> signOfUnary_connective a

THFUC_th1 a -> signOfTH1_unary_connective a

signOfTH1_unary_connective :: TH1_unary_connective -> Sign

signOfTH1_unary_connective x = case x of

TH1_PiForAll -> emptySign

TH1_PiSigmaExists -> emptySign

TH1_PiIndefiniteDescription -> emptySign

TH1_PiDefiniteDescription -> emptySign

TH1_PiEquality -> emptySign

signOfFOF_quantifier :: FOF_quantifier -> Sign

signOfFOF_quantifier x = case x of

ForAll -> emptySign

Exists -> emptySign

signOfBinary_connective :: Binary_connective -> Sign

signOfBinary_connective x = case x of

Equivalence -> emptySign

Implication -> emptySign

ReverseImplication -> emptySign

XOR -> emptySign

NOR -> emptySign

NAND -> emptySign

signOfAssoc_connective :: Assoc_connective -> Sign

signOfAssoc_connective x = case x of

OR -> emptySign

AND -> emptySign

signOfUnary_connective :: Unary_connective -> Sign

signOfUnary_connective x = case x of

NOT -> emptySign

signOfType_constant :: Type_constant -> Sign

signOfType_constant _ = emptySign -- Handled by thfTypeConstantMap and tffTypeConstantMap

signOfType_functor :: Type_functor -> Sign

signOfType_functor _ = emptySign -- Handled by thfTypeFunctorMap and tffTypeFunctorMap

signOfDefined_type :: Defined_type -> Sign

signOfDefined_type x = case x of

OType -> emptySign

O -> emptySign

IType -> emptySign

I -> emptySign

TType -> emptySign

Real -> emptySign

Rat -> emptySign

Int -> emptySign

signOfAtom :: Atom -> Sign

signOfAtom x = case x of

Atom_untyped a -> signOfUntyped_atom a

Atom_constant a -> signOfDefined_constant a

signOfUntyped_atom :: Untyped_atom -> Sign

signOfUntyped_atom x = case x of

UA_constant a -> signOfConstant a

UA_system a -> signOfSystem_constant a

signOfProposition :: Proposition -> Sign

signOfProposition a = emptySign { propositionSet = Set.singleton a }

signOfPredicate :: Predicate -> Int -> Sign

signOfPredicate a arity =

emptySign { fofPredicateMap = Map.singleton a $ Set.singleton arity }

signOfDefined_proposition :: Defined_proposition -> Sign

signOfDefined_proposition x = case x of

TPTP_true -> emptySign

TPTP_false -> emptySign

signOfDefined_predicate :: Defined_predicate -> Sign

signOfDefined_predicate x = case x of

Distinct -> emptySign

Less -> emptySign

Lesseq -> emptySign

Greater -> emptySign

Greatereq -> emptySign

Is_int -> emptySign

Is_rat -> emptySign

Box_P -> emptySign

Box_i -> emptySign

Box_int -> emptySign

Box -> emptySign

Dia_P -> emptySign

Dia_i -> emptySign

Dia_int -> emptySign

Dia -> emptySign

signOfDefined_infix_pred :: Defined_infix_pred -> Sign

signOfDefined_infix_pred x = case x of

Defined_infix_equality -> emptySign

Defined_assignment -> emptySign

signOfConstant :: Constant -> Sign

signOfConstant a = emptySign { constantSet = Set.singleton a }

signOfTPTP_functor :: TPTP_functor -> Int -> Sign

signOfTPTP_functor a arity =

emptySign { fofFunctorMap = Map.singleton a $ Set.singleton arity }

signOfSystem_constant :: System_constant -> Sign

signOfSystem_constant _ = emptySign

signOfSystem_functor :: System_functor -> Sign

signOfSystem_functor _ = emptySign

signOfDefined_constant :: Defined_constant -> Sign

signOfDefined_constant _ = emptySign

signOfDefined_functor :: Defined_functor -> Sign

signOfDefined_functor x = case x of

Uminus -> emptySign

Sum -> emptySign

Difference -> emptySign

Product -> emptySign

Quotient -> emptySign

Quotient_e -> emptySign

Quotient_t -> emptySign

Quotient_f -> emptySign

Remainder_e -> emptySign

Remainder_t -> emptySign

Remainder_f -> emptySign

Floor -> emptySign

Ceiling -> emptySign

Truncate -> emptySign

Round -> emptySign

To_int -> emptySign

To_rat -> emptySign

To_real -> emptySign

DF_atomic_defined_word _ -> emptySign

signOfDefined_term :: Defined_term -> Sign

signOfDefined_term x = case x of

DT_number a -> signOfNumber a

DT_object a -> signOfDistinct_object a

signOfVariable :: Variable -> Sign

signOfVariable _ = emptySign

-- The following types are defined in the AS, but never actually used.

-- We only comment them out instead of removing them to be able to adapt to

-- future changes of the TPTP quickly.

-- signOfSource :: Source -> Sign

-- signOfSource x = case x of

-- Source_DAG a -> emptySign

-- Source_internal a -> emptySign

-- Source_external a -> emptySign

-- Unknown_source -> emptySign

-- Source_many a -> emptySign

-- signOfSources :: Sources -> Sign

-- signOfSources _ = emptySign

-- signOfDAG_source :: DAG_source -> Sign

-- signOfDAG_source x = case x of

-- DAGS_name a -> emptySign

-- DAGS_record a -> emptySign

-- signOfInference_record :: Inference_record -> Sign

-- signOfInference_record x = case x of

-- Inference_record ir ui ip -> emptySign

-- signOfInference_rule :: Inference_rule -> Sign

-- signOfInference_rule _ = emptySign

-- signOfInference_parents :: Inference_parents -> Sign

-- signOfInference_parents _ = emptySign

-- signOfParent_list :: Parent_list -> Sign

-- signOfParent_list _ = emptySign

-- signOfParent_info :: Parent_info -> Sign

-- signOfParent_info x = case x of

-- Parent_info s d -> emptySign

-- signOfParent_details :: Parent_details -> Sign

-- signOfParent_details x = case x of

-- Just gl -> emptySign

-- Nothing -> emptySign

-- signOfInternal_source :: Internal_source -> Sign

-- signOfInternal_source x = case x of

-- Internal_source it oi -> emptySign

-- signOfIntro_type :: Intro_type -> Sign

-- signOfIntro_type x = case x of

-- IntroTypeDefinition -> emptySign

-- AxiomOfChoice -> emptySign

-- Tautology -> emptySign

-- IntroTypeAssumption -> emptySign

-- signOfExternal_source :: External_source -> Sign

-- signOfExternal_source x = case x of

-- ExtSrc_file a -> emptySign

-- ExtSrc_theory a -> emptySign

-- ExtSrc_creator a -> emptySign

-- signOfFile_source :: File_source -> emptySign

-- signOfFile_source x = case x of

-- File_source fn fi -> emptySign

-- signOfFile_info :: File_info -> Sign

-- signOfFile_info x = case x of

-- Just n -> emptySign

-- Nothing -> emptySign

-- signOfTheory :: Theory -> Sign

-- signOfTheory x = case x of

-- Theory tn oi -> emptySign

-- signOfTheory_name :: Theory_name -> Sign

-- signOfTheory_name x = case x of

-- TN_equality -> emptySign

-- TN_ac -> emptySign

-- signOfCreator_source :: Creator_source -> Sign

-- signOfCreator_source x = case x of

-- Creator_source cn oi -> emptySign

-- signOfCreator_name :: Creator_name -> Sign

-- signOfCreator_name _ = emptySign

-- signOfOptional_info :: Optional_info -> Sign

-- signOfOptional_info x = case x of

-- Just ui -> emptySign

-- Nothing -> emptySign

-- signOfUseful_info :: Useful_info -> Sign

-- signOfUseful_info x = case x of

-- UI_items a -> emptySign

-- UI_general_list a -> emptySign

-- signOfInfo_items :: Info_items -> Sign

-- signOfInfo_items _ = emptySign

-- signOfInfo_item :: Info_item -> Sign

-- signOfInfo_item x = case x of

-- Info_formula a -> emptySign

-- Info_inference a -> emptySign

-- Info_general a -> emptySign

-- signOfFormula_item :: Formula_item -> Sign

-- signOfFormula_item x = case x of

-- FI_description a -> emptySign

-- FI_iquote a -> emptySign

-- signOfDescription_item :: Description_item -> Sign

-- signOfDescription_item _ = emptySign

-- signOfIquote_item :: Iquote_item -> Sign

-- signOfIquote_item _ = emptySign

-- signOfInference_item :: Inference_item -> Sign

-- signOfInference_item x = case x of

-- Inf_status a -> emptySign

-- Inf_assumption a -> emptySign

-- Inf_symbol a -> emptySign

-- Inf_refutation a -> emptySign

-- signOfInference_status :: Inference_status -> Sign

-- signOfInference_status x = case x of

-- Inf_value sv -> emptySign

-- Inf_info a -> emptySign

-- signOfStatus_value :: Status_value -> Sign

-- signOfStatus_value x = case x of

-- SUC -> emptySign

-- UNP -> emptySign

-- SAP -> emptySign

-- ESA -> emptySign

-- SAT -> emptySign

-- FSA -> emptySign

-- THM -> emptySign

-- EQV -> emptySign

-- TAC -> emptySign

-- WEC -> emptySign

-- ETH -> emptySign

-- TAU -> emptySign

-- WTC -> emptySign

-- WTH -> emptySign

-- CAX -> emptySign

-- SCA -> emptySign

-- TCA -> emptySign

-- WCA -> emptySign

-- CUP -> emptySign

-- CSP -> emptySign

-- ECS -> emptySign

-- CSA -> emptySign

-- CTH -> emptySign

-- CEQ -> emptySign

-- UNC -> emptySign

-- WCC -> emptySign

-- ECT -> emptySign

-- FUN -> emptySign

-- UNS -> emptySign

-- WUC -> emptySign

-- WCT -> emptySign

-- SCC -> emptySign

-- UCA -> emptySign

-- NOC -> emptySign

-- signOfInference_info :: Inference_info -> Sign

-- signOfInference_info x = case x of

-- Inference_info ir aw gl -> emptySign

-- signOfAssumptions_record :: Assumptions_record -> Sign

-- signOfAssumptions_record _ = emptySign

-- signOfRefutation :: Refutation -> emptySign

-- signOfRefutation _ = emptySign

-- signOfNew_symbol_record :: New_symbol_record -> Sign

-- signOfNew_symbol_record x = case x of

-- New_symbol_record aw nsl -> emptySign

-- signOfNew_symbol_list :: New_symbol_list -> Sign

-- signOfNew_symbol_list _ = emptySign

-- signOfPrincipal_symbol :: Principal_symbol -> Sign

-- signOfPrincipal_symbol x = case x of

-- PS_functor a -> emptySign

-- PS_variable a -> emptySign

-- signOfInclude :: Include -> Sign

-- signOfInclude x = case x of

-- Include fn fs -> emptySign

-- signOfFormula_selection :: Formula_selection -> Sign

-- signOfFormula_selection x = case x of

-- Just ns -> emptySign

-- Nothing -> emptySign

-- signOfName_list :: Name_list -> Sign

-- signOfName_list _ = emptySign

-- signOfGeneral_term :: General_term -> Sign

-- signOfGeneral_term x = case x of

-- GT_data a -> emptySign

-- GT_DataTerm gd gt -> emptySign

-- GT_list a -> emptySign

-- signOfGeneral_data :: General_data -> Sign

-- signOfGeneral_data x = case x of

-- GD_atomic_word a -> emptySign

-- GD_general_function a -> emptySign

-- GD_variable a -> emptySign

-- GD_number a -> emptySign

-- GD_distinct_object a -> emptySign

-- GD_formula_data a -> emptySign

-- GD_bind v fd -> emptySign

-- signOfGeneral_function :: General_function -> Sign

-- signOfGeneral_function x = case x of

-- General_function aw gt -> emptySign

-- signOfFormula_data :: Formula_data -> Sign

-- signOfFormula_data x = case x of

-- FD_THF a -> emptySign

-- FD_TFF a -> emptySign

-- FD_FOF a -> emptySign

-- FD_CNF a -> emptySign

-- FD_FOT a -> emptySign

-- signOfGeneral_list :: General_list -> Sign

-- signOfGeneral_list _ = emptySign

-- signOfGeneral_terms :: General_terms -> Sign

-- signOfGeneral_terms _ = emptySign

-- signOfName :: Name -> Sign

-- signOfName x = case x of

-- NameString a -> emptySign

-- NameInteger a -> emptySign

-- signOfAtomic_word :: Atomic_word -> Sign

-- signOfAtomic_word _ = emptySign

-- signOfAtomic_defined_word :: Atomic_defined_word -> Sign

-- signOfAtomic_defined_word _ = emptySign

-- signOfAtomic_system_word :: Atomic_system_word -> Sign

-- signOfAtomic_system_word _ = emptySign

signOfNumber :: Number -> Sign

signOfNumber a = emptySign { numberSet = Set.singleton a }

signOfDistinct_object :: Distinct_object -> Sign

signOfDistinct_object _ = emptySign

-- signOfFile_name :: File_name -> Sign

-- signOfFile_name _ = emptySign

nameS :: Annotated_formula -> String

nameS f = case name f of

NameString s -> tokStr s

NameInteger i -> show i