{- |
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 :: (BASIC_SPEC, Sign, GlobalAnnos)
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence])
basicAnalysis (basicSpec :: BASIC_SPEC
basicSpec, signOfIncludes :: Sign
signOfIncludes, _) =
  let ns :: [Named Sentence]
ns = BASIC_SPEC -> [Named Sentence]
toNamedSen BASIC_SPEC
basicSpec
      specSign :: Sign
specSign = [Named Sentence] -> Sign
signOfSentences [Named Sentence]
ns
      nonImportedSyms :: Set Symbol
nonImportedSyms = Sign -> Set Symbol
symbolsOfSign Sign
specSign
      completeSignWithTypeConstants :: Sign
completeSignWithTypeConstants = Sign
specSign Sign -> Sign -> Sign
`signatureUnion` Sign
signOfIncludes
      completeSign :: Sign
completeSign = Sign -> Sign
postProcessSign Sign
completeSignWithTypeConstants
  in  (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence])
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return (BASIC_SPEC
basicSpec, Sign -> Set Symbol -> ExtSign Sign Symbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign Sign
completeSign Set Symbol
nonImportedSyms, [Named Sentence]
ns)

toNamedSen :: BASIC_SPEC -> [Named Sentence]
toNamedSen :: BASIC_SPEC -> [Named Sentence]
toNamedSen (Basic_spec annotedItems :: [Annoted TPTP]
annotedItems) =
  (Annoted TPTP -> [Named Sentence])
-> [Annoted TPTP] -> [Named Sentence]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (TPTP -> [Named Sentence]
toNamedSenTPTP (TPTP -> [Named Sentence])
-> (Annoted TPTP -> TPTP) -> Annoted TPTP -> [Named Sentence]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted TPTP -> TPTP
forall a. Annoted a -> a
item)  [Annoted TPTP]
annotedItems
  where
    toNamedSenTPTP :: TPTP -> [Named Sentence]
    toNamedSenTPTP :: TPTP -> [Named Sentence]
toNamedSenTPTP (TPTP inputs :: [TPTP_input]
inputs) = (TPTP_input -> [Named Sentence])
-> [TPTP_input] -> [Named Sentence]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TPTP_input -> [Named Sentence]
toNamedSenI [TPTP_input]
inputs

    toNamedSenI :: TPTP_input -> [Named Sentence]
    toNamedSenI :: TPTP_input -> [Named Sentence]
toNamedSenI i :: TPTP_input
i = case TPTP_input
i of
      Annotated_formula af :: Sentence
af ->
        [(String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed (Sentence -> String
nameS Sentence
af) Sentence
af) { isAxiom :: Bool
isAxiom = Sentence -> Bool
formulaIsAxiom Sentence
af
                                   , isDef :: Bool
isDef = Sentence -> Bool
formulaIsDef Sentence
af
                                   , wasTheorem :: Bool
wasTheorem = Sentence -> Bool
formulaWasTheorem Sentence
af
                                   }]
      _ -> []

    formulaIsAxiom :: Annotated_formula -> Bool
    formulaIsAxiom :: Sentence -> Bool
formulaIsAxiom af :: Sentence
af = case Sentence -> Formula_role
formulaRole Sentence
af of
      Conjecture -> Bool
False
      Negated_conjecture -> Bool
False
      _ -> Bool
True

    formulaIsDef :: Annotated_formula -> Bool
    formulaIsDef :: Sentence -> Bool
formulaIsDef af :: Sentence
af = case Sentence -> Formula_role
formulaRole Sentence
af of
      Definition -> Bool
True
      _ -> Bool
False

    formulaWasTheorem :: Annotated_formula -> Bool
    formulaWasTheorem :: Sentence -> Bool
formulaWasTheorem af :: Sentence
af = case Sentence -> Formula_role
formulaRole Sentence
af of
      Theorem -> Bool
True
      Lemma -> Bool
True
      _ -> Bool
False

signatureUnionR :: Sign -> Sign -> Result Sign
signatureUnionR :: Sign -> Sign -> Result Sign
signatureUnionR s1 :: Sign
s1 s2 :: Sign
s2 = [Diagnosis] -> Maybe Sign -> Result Sign
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Debug "All fine sigUnion" Range
nullRange]
                  (Maybe Sign -> Result Sign) -> Maybe Sign -> Result Sign
forall a b. (a -> b) -> a -> b
$ Sign -> Maybe Sign
forall a. a -> Maybe a
Just (Sign -> Maybe Sign) -> Sign -> Maybe Sign
forall a b. (a -> b) -> a -> b
$ Sign -> Sign
postProcessSign (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ Sign -> Sign -> Sign
signatureUnion Sign
s1 Sign
s2

signatureUnion :: Sign -> Sign -> Sign
signatureUnion :: Sign -> Sign -> Sign
signatureUnion s1 :: Sign
s1 s2 :: Sign
s2 =
  Sign :: ConstantSet
-> NumberSet
-> ConstantSet
-> THFSubTypeMap
-> TFFSubTypeMap
-> THFPredicateMap
-> TFFPredicateMap
-> FOFPredicateMap
-> FOFPredicateMap
-> THFPredicateMap
-> TFFPredicateMap
-> THFPredicateMap
-> TFFPredicateMap
-> THFPredicateMap
-> TFFPredicateMap
-> Sign
Sign { constantSet :: ConstantSet
constantSet = Sign -> ConstantSet
constantSet Sign
s1 ConstantSet -> ConstantSet -> ConstantSet
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Sign -> ConstantSet
constantSet Sign
s2
       , numberSet :: NumberSet
numberSet = Sign -> NumberSet
numberSet Sign
s1 NumberSet -> NumberSet -> NumberSet
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Sign -> NumberSet
numberSet Sign
s2
       , propositionSet :: ConstantSet
propositionSet = Sign -> ConstantSet
propositionSet Sign
s1 ConstantSet -> ConstantSet -> ConstantSet
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Sign -> ConstantSet
propositionSet Sign
s2
       , thfPredicateMap :: THFPredicateMap
thfPredicateMap = Sign -> THFPredicateMap
thfPredicateMap Sign
s1 THFPredicateMap -> THFPredicateMap -> THFPredicateMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Sign -> THFPredicateMap
thfPredicateMap Sign
s2
       , tffPredicateMap :: TFFPredicateMap
tffPredicateMap = Sign -> TFFPredicateMap
tffPredicateMap Sign
s1 TFFPredicateMap -> TFFPredicateMap -> TFFPredicateMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Sign -> TFFPredicateMap
tffPredicateMap Sign
s2
       , fofPredicateMap :: FOFPredicateMap
fofPredicateMap = FOFPredicateMap -> FOFPredicateMap -> FOFPredicateMap
unionFOFPredicate (Sign -> FOFPredicateMap
fofPredicateMap Sign
s1) (Sign -> FOFPredicateMap
fofPredicateMap Sign
s2)
       , fofFunctorMap :: FOFPredicateMap
fofFunctorMap = FOFPredicateMap -> FOFPredicateMap -> FOFPredicateMap
unionFOFFunctor (Sign -> FOFPredicateMap
fofFunctorMap Sign
s1) (Sign -> FOFPredicateMap
fofFunctorMap Sign
s2)
       , thfTypeConstantMap :: THFPredicateMap
thfTypeConstantMap = Sign -> THFPredicateMap
thfTypeConstantMap Sign
s1 THFPredicateMap -> THFPredicateMap -> THFPredicateMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Sign -> THFPredicateMap
thfTypeConstantMap Sign
s2
       , tffTypeConstantMap :: TFFPredicateMap
tffTypeConstantMap = Sign -> TFFPredicateMap
tffTypeConstantMap Sign
s1 TFFPredicateMap -> TFFPredicateMap -> TFFPredicateMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Sign -> TFFPredicateMap
tffTypeConstantMap Sign
s2
       , thfTypeFunctorMap :: THFPredicateMap
thfTypeFunctorMap = Sign -> THFPredicateMap
thfTypeFunctorMap Sign
s1 THFPredicateMap -> THFPredicateMap -> THFPredicateMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Sign -> THFPredicateMap
thfTypeFunctorMap Sign
s2
       , tffTypeFunctorMap :: TFFPredicateMap
tffTypeFunctorMap = Sign -> TFFPredicateMap
tffTypeFunctorMap Sign
s1 TFFPredicateMap -> TFFPredicateMap -> TFFPredicateMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Sign -> TFFPredicateMap
tffTypeFunctorMap Sign
s2
       , thfSubtypeMap :: THFSubTypeMap
thfSubtypeMap = Sign -> THFSubTypeMap
thfSubtypeMap Sign
s1 THFSubTypeMap -> THFSubTypeMap -> THFSubTypeMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Sign -> THFSubTypeMap
thfSubtypeMap Sign
s2
       , tffSubtypeMap :: TFFSubTypeMap
tffSubtypeMap = Sign -> TFFSubTypeMap
tffSubtypeMap Sign
s1 TFFSubTypeMap -> TFFSubTypeMap -> TFFSubTypeMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Sign -> TFFSubTypeMap
tffSubtypeMap Sign
s2
       , thfTypeDeclarationMap :: THFPredicateMap
thfTypeDeclarationMap = Sign -> THFPredicateMap
thfTypeDeclarationMap Sign
s1 THFPredicateMap -> THFPredicateMap -> THFPredicateMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Sign -> THFPredicateMap
thfTypeDeclarationMap Sign
s2
       , tffTypeDeclarationMap :: TFFPredicateMap
tffTypeDeclarationMap = Sign -> TFFPredicateMap
tffTypeDeclarationMap Sign
s1 TFFPredicateMap -> TFFPredicateMap -> TFFPredicateMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Sign -> TFFPredicateMap
tffTypeDeclarationMap Sign
s2
       }
  where
    unionFOFPredicate :: FOFPredicateMap -> FOFPredicateMap -> FOFPredicateMap
    unionFOFPredicate :: FOFPredicateMap -> FOFPredicateMap -> FOFPredicateMap
unionFOFPredicate = (Set Int -> Set Int -> Set Int)
-> FOFPredicateMap -> FOFPredicateMap -> FOFPredicateMap
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set Int -> Set Int -> Set Int
forall a. Ord a => Set a -> Set a -> Set a
Set.union

    unionFOFFunctor :: FOFFunctorMap -> FOFFunctorMap -> FOFFunctorMap
    unionFOFFunctor :: FOFPredicateMap -> FOFPredicateMap -> FOFPredicateMap
unionFOFFunctor = (Set Int -> Set Int -> Set Int)
-> FOFPredicateMap -> FOFPredicateMap -> FOFPredicateMap
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set Int -> Set Int -> Set Int
forall a. Ord a => Set a -> Set a -> Set a
Set.union

signatureUnions :: [Sign] -> Sign
signatureUnions :: [Sign] -> Sign
signatureUnions signs :: [Sign]
signs = (Sign -> Sign -> Sign) -> Sign -> [Sign] -> Sign
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Sign -> Sign -> Sign
signatureUnion Sign
emptySign [Sign]
signs

signOfSentences :: [Named Sentence] -> Sign
signOfSentences :: [Named Sentence] -> Sign
signOfSentences nss :: [Named Sentence]
nss =
  Sign -> Sign
postProcessSign (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$
    (Sign -> Sign -> Sign) -> Sign -> [Sign] -> Sign
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ sign :: Sign
sign result :: Sign
result -> Sign -> Sign -> Sign
signatureUnion Sign
sign Sign
result) Sign
emptySign ([Sign] -> Sign) -> [Sign] -> Sign
forall a b. (a -> b) -> a -> b
$
      (Named Sentence -> Sign) -> [Named Sentence] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map (Sentence -> Sign
signOfSentenceNaive (Sentence -> Sign)
-> (Named Sentence -> Sentence) -> Named Sentence -> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence) [Named Sentence]
nss

postProcessSign :: Sign -> Sign
postProcessSign :: Sign -> Sign
postProcessSign = Sign -> Sign
partitionTypeDeclarations (Sign -> Sign) -> (Sign -> Sign) -> Sign -> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Sign
removeTypeDeclarationsFromConstantSet
  where
    partitionTypeDeclarations :: Sign -> Sign
    partitionTypeDeclarations :: Sign -> Sign
partitionTypeDeclarations sign :: Sign
sign =
      let (thfPredicates :: THFPredicateMap
thfPredicates, thfRemainder :: THFPredicateMap
thfRemainder) =
            (THF_top_level_type -> Bool)
-> THFPredicateMap -> (THFPredicateMap, THFPredicateMap)
forall a k. (a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partition THF_top_level_type -> Bool
isTHFBooleanType (THFPredicateMap -> (THFPredicateMap, THFPredicateMap))
-> THFPredicateMap -> (THFPredicateMap, THFPredicateMap)
forall a b. (a -> b) -> a -> b
$ Sign -> THFPredicateMap
thfTypeDeclarationMap Sign
sign
          (thfTypes :: THFPredicateMap
thfTypes, thfRemainder' :: THFPredicateMap
thfRemainder') = (THF_top_level_type -> Bool)
-> THFPredicateMap -> (THFPredicateMap, THFPredicateMap)
forall a k. (a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partition THF_top_level_type -> Bool
isTHFType THFPredicateMap
thfRemainder
          (tffPredicates :: TFFPredicateMap
tffPredicates, tffRemainder :: TFFPredicateMap
tffRemainder) =
            (TFF_top_level_type -> Bool)
-> TFFPredicateMap -> (TFFPredicateMap, TFFPredicateMap)
forall a k. (a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partition TFF_top_level_type -> Bool
isTFFBooleanType (TFFPredicateMap -> (TFFPredicateMap, TFFPredicateMap))
-> TFFPredicateMap -> (TFFPredicateMap, TFFPredicateMap)
forall a b. (a -> b) -> a -> b
$ Sign -> TFFPredicateMap
tffTypeDeclarationMap Sign
sign
          (tffTypes :: TFFPredicateMap
tffTypes, tffRemainder' :: TFFPredicateMap
tffRemainder') = (TFF_top_level_type -> Bool)
-> TFFPredicateMap -> (TFFPredicateMap, TFFPredicateMap)
forall a k. (a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partition TFF_top_level_type -> Bool
isTFFType TFFPredicateMap
tffRemainder
      in Sign
sign { thfPredicateMap :: THFPredicateMap
thfPredicateMap = THFPredicateMap
thfPredicates
              , thfTypeConstantMap :: THFPredicateMap
thfTypeConstantMap = THFPredicateMap
thfTypes
              , thfTypeFunctorMap :: THFPredicateMap
thfTypeFunctorMap = THFPredicateMap
thfRemainder'
              , tffPredicateMap :: TFFPredicateMap
tffPredicateMap = TFFPredicateMap
tffPredicates
              , tffTypeConstantMap :: TFFPredicateMap
tffTypeConstantMap = TFFPredicateMap
tffTypes
              , tffTypeFunctorMap :: TFFPredicateMap
tffTypeFunctorMap = TFFPredicateMap
tffRemainder'
              }

    -- Type helpers
    isTHFBooleanType :: THF_top_level_type -> Bool
    isTHFBooleanType :: THF_top_level_type -> Bool
isTHFBooleanType x :: THF_top_level_type
x = case THF_top_level_type
x of
      THFTLT_unitary (THFUT_unitary (THFUF_atom (THF_atom_function (THFF_atom (Atom_constant (DF_atomic_defined_word w :: Atomic_defined_word
w)))))) -> Atomic_defined_word -> String
tokStr Atomic_defined_word
w String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "$o"
      THFTLT_mapping types :: THF_mapping_type
types -> THF_top_level_type -> Bool
isTHFBooleanType (THF_top_level_type -> Bool) -> THF_top_level_type -> Bool
forall a b. (a -> b) -> a -> b
$ THF_unitary_type -> THF_top_level_type
THFTLT_unitary (THF_unitary_type -> THF_top_level_type)
-> THF_unitary_type -> THF_top_level_type
forall a b. (a -> b) -> a -> b
$ THF_mapping_type -> THF_unitary_type
forall a. [a] -> a
last THF_mapping_type
types
      _ -> Bool
False

    isTHFType :: THF_top_level_type -> Bool
    isTHFType :: THF_top_level_type -> Bool
isTHFType x :: THF_top_level_type
x = case THF_top_level_type
x of
      THFTLT_unitary (THFUT_unitary (THFUF_atom (THF_atom_function (THFF_atom (Atom_constant (DF_atomic_defined_word w :: Atomic_defined_word
w)))))) -> Atomic_defined_word -> String
tokStr Atomic_defined_word
w String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "$tType"
      _ -> Bool
False

    isTFFBooleanType :: TFF_top_level_type -> Bool
    isTFFBooleanType :: TFF_top_level_type -> Bool
isTFFBooleanType x :: TFF_top_level_type
x = case TFF_top_level_type
x of
      TFFTLT_mapping (TFF_mapping_type _ (TFFAT_defined O)) -> Bool
True
      _ -> Bool
False

    isTFFType :: TFF_top_level_type -> Bool
    isTFFType :: TFF_top_level_type -> Bool
isTFFType x :: TFF_top_level_type
x = case TFF_top_level_type
x of
      TFFTLT_atomic (TFFAT_defined TType) -> Bool
True
      _ -> Bool
False

    removeTypeDeclarationsFromConstantSet :: Sign -> Sign
    removeTypeDeclarationsFromConstantSet :: Sign -> Sign
removeTypeDeclarationsFromConstantSet sign :: Sign
sign =
      let tffTypeKeys :: Set Untyped_atom
tffTypeKeys = TFFPredicateMap -> Set Untyped_atom
forall k a. Map k a -> Set k
Map.keysSet (TFFPredicateMap -> Set Untyped_atom)
-> TFFPredicateMap -> Set Untyped_atom
forall a b. (a -> b) -> a -> b
$ Sign -> TFFPredicateMap
tffTypeDeclarationMap Sign
sign
          tffTypeNames :: ConstantSet
tffTypeNames = (Untyped_atom -> Atomic_defined_word)
-> Set Untyped_atom -> ConstantSet
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Untyped_atom -> Atomic_defined_word
unpackConstant (Set Untyped_atom -> ConstantSet)
-> Set Untyped_atom -> ConstantSet
forall a b. (a -> b) -> a -> b
$ (Untyped_atom -> Bool) -> Set Untyped_atom -> Set Untyped_atom
forall a. (a -> Bool) -> Set a -> Set a
Set.filter Untyped_atom -> Bool
isConstant (Set Untyped_atom -> Set Untyped_atom)
-> Set Untyped_atom -> Set Untyped_atom
forall a b. (a -> b) -> a -> b
$ Set Untyped_atom
tffTypeKeys
          thfTypeKeys :: Set THFTypeable
thfTypeKeys = THFPredicateMap -> Set THFTypeable
forall k a. Map k a -> Set k
Map.keysSet (THFPredicateMap -> Set THFTypeable)
-> THFPredicateMap -> Set THFTypeable
forall a b. (a -> b) -> a -> b
$ Sign -> THFPredicateMap
thfTypeDeclarationMap Sign
sign
          thfTypeNames :: ConstantSet
thfTypeNames = (THFTypeable -> Atomic_defined_word)
-> Set THFTypeable -> ConstantSet
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map THFTypeable -> Atomic_defined_word
unpackConstantTHF (Set THFTypeable -> ConstantSet) -> Set THFTypeable -> ConstantSet
forall a b. (a -> b) -> a -> b
$ (THFTypeable -> Bool) -> Set THFTypeable -> Set THFTypeable
forall a. (a -> Bool) -> Set a -> Set a
Set.filter THFTypeable -> Bool
isConstantTHF (Set THFTypeable -> Set THFTypeable)
-> Set THFTypeable -> Set THFTypeable
forall a b. (a -> b) -> a -> b
$
                           Set THFTypeable
thfTypeKeys
          typeNames :: ConstantSet
typeNames = ConstantSet
tffTypeNames ConstantSet -> ConstantSet -> ConstantSet
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` ConstantSet
thfTypeNames
      in  Sign
sign { constantSet :: ConstantSet
constantSet = Sign -> ConstantSet
constantSet Sign
sign ConstantSet -> ConstantSet -> ConstantSet
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ ConstantSet
typeNames }

    isConstant :: Untyped_atom -> Bool
    isConstant :: Untyped_atom -> Bool
isConstant ua :: Untyped_atom
ua = case Untyped_atom
ua of
      UA_constant _ -> Bool
True
      _ -> Bool
False

    unpackConstant :: Untyped_atom -> Constant
    unpackConstant :: Untyped_atom -> Atomic_defined_word
unpackConstant ua :: Untyped_atom
ua = case Untyped_atom
ua of
      UA_constant c :: Atomic_defined_word
c -> Atomic_defined_word
c
      _ -> String -> Atomic_defined_word
forall a. HasCallStack => String -> a
error "Error in TPTP.StaticAnalysis.unpackConstant: Non-constant encountered."

    isConstantTHF :: THFTypeable -> Bool
    isConstantTHF :: THFTypeable -> Bool
isConstantTHF x :: THFTypeable
x = case THFTypeable
x of
      THFTypeConstant _ -> Bool
True
      _ -> Bool
False

    unpackConstantTHF :: THFTypeable -> Constant
    unpackConstantTHF :: THFTypeable -> Atomic_defined_word
unpackConstantTHF x :: THFTypeable
x = case THFTypeable
x of
      THFTypeConstant c :: Atomic_defined_word
c -> Atomic_defined_word
c
      _ -> String -> Atomic_defined_word
forall a. HasCallStack => String -> a
error "Error in TPTP.StaticAnalysis.unpackConstant: Non-constant encountered."

signOfSentence :: Sentence -> Sign
signOfSentence :: Sentence -> Sign
signOfSentence sen :: Sentence
sen = [Named Sentence] -> Sign
signOfSentences [String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed "" Sentence
sen]

signOfSentenceNaive :: Sentence -> Sign
signOfSentenceNaive :: Sentence -> Sign
signOfSentenceNaive sen :: Sentence
sen = case Sentence
sen of
  AF_THF_Annotated f :: THF_annotated
f -> THF_annotated -> Sign
signOfTHF_annotated THF_annotated
f
  AF_TFX_Annotated f :: TFX_annotated
f -> TFX_annotated -> Sign
signOfTFX_annotated TFX_annotated
f
  AF_TFF_Annotated f :: TFF_annotated
f -> TFF_annotated -> Sign
signOfTFF_annotated TFF_annotated
f
  AF_TCF_Annotated f :: TCF_annotated
f -> TCF_annotated -> Sign
signOfTCF_annotated TCF_annotated
f
  AF_FOF_Annotated f :: FOF_annotated
f -> FOF_annotated -> Sign
signOfFOF_annotated FOF_annotated
f
  AF_CNF_Annotated f :: CNF_annotated
f -> CNF_annotated -> Sign
signOfCNF_annotated CNF_annotated
f
  AF_TPI_Annotated f :: TPI_annotated
f -> TPI_annotated -> Sign
signOfTPI_annotated TPI_annotated
f

signOfTPI_annotated :: TPI_annotated -> Sign
signOfTPI_annotated :: TPI_annotated -> Sign
signOfTPI_annotated x :: TPI_annotated
x = case TPI_annotated
x of
  TPI_annotated _ _ f :: TPI_formula
f _ -> TPI_formula -> Sign
signOfFOF_formula TPI_formula
f

signOfTHF_annotated :: THF_annotated -> Sign
signOfTHF_annotated :: THF_annotated -> Sign
signOfTHF_annotated x :: THF_annotated
x = case THF_annotated
x of
  THF_annotated _ _ f :: THF_formula
f _ -> THF_formula -> Sign
signOfTHF_formula THF_formula
f

signOfTFX_annotated :: TFX_annotated -> Sign
signOfTFX_annotated :: TFX_annotated -> Sign
signOfTFX_annotated x :: TFX_annotated
x = case TFX_annotated
x of
  TFX_annotated _ _ f :: TFX_formula
f _ -> TFX_formula -> Sign
signOfTFX_formula TFX_formula
f

signOfTFF_annotated :: TFF_annotated -> Sign
signOfTFF_annotated :: TFF_annotated -> Sign
signOfTFF_annotated x :: TFF_annotated
x = case TFF_annotated
x of
  TFF_annotated _ _ f :: TFF_formula
f _ -> TFF_formula -> Sign
signOfTFF_formula TFF_formula
f

signOfTCF_annotated :: TCF_annotated -> Sign
signOfTCF_annotated :: TCF_annotated -> Sign
signOfTCF_annotated x :: TCF_annotated
x = case TCF_annotated
x of
  TCF_annotated _ _ f :: TCF_formula
f _ -> TCF_formula -> Sign
signOfTCF_formula TCF_formula
f

signOfFOF_annotated :: FOF_annotated -> Sign
signOfFOF_annotated :: FOF_annotated -> Sign
signOfFOF_annotated x :: FOF_annotated
x = case FOF_annotated
x of
  FOF_annotated _ _ f :: TPI_formula
f _ -> TPI_formula -> Sign
signOfFOF_formula TPI_formula
f

signOfCNF_annotated :: CNF_annotated -> Sign
signOfCNF_annotated :: CNF_annotated -> Sign
signOfCNF_annotated x :: CNF_annotated
x = case CNF_annotated
x of
  CNF_annotated _ _ f :: CNF_formula
f _ -> CNF_formula -> Sign
signOfCNF_formula CNF_formula
f

-- signOfAnnotations :: Annotations -> Sign
-- signOfAnnotations _ = emptySign

-- signOfFormula_role :: Formula_role -> Sign
-- signOfFormula_role _ = emptySign

signOfTHF_formula :: THF_formula -> Sign
signOfTHF_formula :: THF_formula -> Sign
signOfTHF_formula x :: THF_formula
x = case THF_formula
x of
  THFF_logic f :: THF_logic_formula
f -> THF_logic_formula -> Sign
signOfTHF_logic_formula THF_logic_formula
f
  THFF_sequent s :: THF_sequent
s -> THF_sequent -> Sign
signOfTHF_sequent THF_sequent
s

signOfTHF_logic_formula :: THF_logic_formula -> Sign
signOfTHF_logic_formula :: THF_logic_formula -> Sign
signOfTHF_logic_formula x :: THF_logic_formula
x = case THF_logic_formula
x of
  THFLF_binary f :: THF_binary_formula
f -> THF_binary_formula -> Sign
signOfTHF_binary_formula THF_binary_formula
f
  THFLF_unitary f :: THF_unitary_formula
f -> THF_unitary_formula -> Sign
signOfTHF_unitary_formula THF_unitary_formula
f
  THFLF_type f :: THF_type_formula
f -> THF_type_formula -> Sign
signOfTHF_type_formula THF_type_formula
f
  THFLF_subtype f :: THF_subtype
f -> THF_subtype -> Sign
signOfTHF_subtype THF_subtype
f

signOfTHF_binary_formula :: THF_binary_formula -> Sign
signOfTHF_binary_formula :: THF_binary_formula -> Sign
signOfTHF_binary_formula x :: THF_binary_formula
x = case THF_binary_formula
x of
  THFBF_pair a :: THF_binary_pair
a -> THF_binary_pair -> Sign
signOfTHF_binary_pair THF_binary_pair
a
  THFBF_tuple a :: THF_binary_tuple
a -> THF_binary_tuple -> Sign
signOfTHF_binary_tuple THF_binary_tuple
a

signOfTHF_binary_pair :: THF_binary_pair -> Sign
signOfTHF_binary_pair :: THF_binary_pair -> Sign
signOfTHF_binary_pair x :: THF_binary_pair
x = case THF_binary_pair
x of
  THF_binary_pair _ f1 :: THF_unitary_formula
f1 f2 :: THF_unitary_formula
f2 ->
    [Sign] -> Sign
signatureUnions ([Sign] -> Sign) -> [Sign] -> Sign
forall a b. (a -> b) -> a -> b
$ (THF_unitary_formula -> Sign) -> [THF_unitary_formula] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map THF_unitary_formula -> Sign
signOfTHF_unitary_formula [THF_unitary_formula
f1, THF_unitary_formula
f2]

signOfTHF_binary_tuple :: THF_binary_tuple -> Sign
signOfTHF_binary_tuple :: THF_binary_tuple -> Sign
signOfTHF_binary_tuple x :: THF_binary_tuple
x = case THF_binary_tuple
x of
  THFBT_or fs :: [THF_unitary_formula]
fs -> [THF_unitary_formula] -> Sign
signOfTHF_or_formula [THF_unitary_formula]
fs
  THFBT_and fs :: [THF_unitary_formula]
fs -> [THF_unitary_formula] -> Sign
signOfTHF_and_formula [THF_unitary_formula]
fs
  THFBT_apply fs :: [THF_unitary_formula]
fs -> [THF_unitary_formula] -> Sign
signOfTHF_apply_formula [THF_unitary_formula]
fs

signOfTHF_or_formula :: THF_or_formula -> Sign
signOfTHF_or_formula :: [THF_unitary_formula] -> Sign
signOfTHF_or_formula = [Sign] -> Sign
signatureUnions ([Sign] -> Sign)
-> ([THF_unitary_formula] -> [Sign])
-> [THF_unitary_formula]
-> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (THF_unitary_formula -> Sign) -> [THF_unitary_formula] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map THF_unitary_formula -> Sign
signOfTHF_unitary_formula

signOfTHF_and_formula :: THF_or_formula -> Sign
signOfTHF_and_formula :: [THF_unitary_formula] -> Sign
signOfTHF_and_formula = [Sign] -> Sign
signatureUnions ([Sign] -> Sign)
-> ([THF_unitary_formula] -> [Sign])
-> [THF_unitary_formula]
-> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (THF_unitary_formula -> Sign) -> [THF_unitary_formula] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map THF_unitary_formula -> Sign
signOfTHF_unitary_formula

signOfTHF_apply_formula :: THF_or_formula -> Sign
signOfTHF_apply_formula :: [THF_unitary_formula] -> Sign
signOfTHF_apply_formula = [Sign] -> Sign
signatureUnions ([Sign] -> Sign)
-> ([THF_unitary_formula] -> [Sign])
-> [THF_unitary_formula]
-> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (THF_unitary_formula -> Sign) -> [THF_unitary_formula] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map THF_unitary_formula -> Sign
signOfTHF_unitary_formula

signOfTHF_unitary_formula :: THF_unitary_formula -> Sign
signOfTHF_unitary_formula :: THF_unitary_formula -> Sign
signOfTHF_unitary_formula x :: THF_unitary_formula
x = case THF_unitary_formula
x of
  THFUF_quantified a :: THF_quantified_formula
a -> THF_quantified_formula -> Sign
signOfTHF_quantified_formula THF_quantified_formula
a
  THFUF_unary a :: THF_unary_formula
a -> THF_unary_formula -> Sign
signOfTHF_unary_formula THF_unary_formula
a
  THFUF_atom a :: THF_atom
a -> THF_atom -> Sign
signOfTHF_atom THF_atom
a
  THFUF_conditional a :: THF_conditional
a -> THF_conditional -> Sign
signOfTHF_conditional THF_conditional
a
  THFUF_let a :: THF_let
a -> THF_let -> Sign
signOfTHF_let THF_let
a
  THFUF_tuple a :: THF_tuple
a -> THF_tuple -> Sign
signOfTHF_tuple THF_tuple
a
  THFUF_logic a :: THF_logic_formula
a -> THF_logic_formula -> Sign
signOfTHF_logic_formula THF_logic_formula
a

signOfTHF_quantified_formula :: THF_quantified_formula -> Sign
signOfTHF_quantified_formula :: THF_quantified_formula -> Sign
signOfTHF_quantified_formula x :: THF_quantified_formula
x = case THF_quantified_formula
x of
  THF_quantified_formula q :: THF_quantification
q f :: THF_unitary_formula
f ->
    [Sign] -> Sign
signatureUnions [THF_quantification -> Sign
signOfTHF_quantification THF_quantification
q, THF_unitary_formula -> Sign
signOfTHF_unitary_formula THF_unitary_formula
f]

signOfTHF_quantification :: THF_quantification -> Sign
signOfTHF_quantification :: THF_quantification -> Sign
signOfTHF_quantification x :: THF_quantification
x = case THF_quantification
x of
  THF_quantification q :: THF_quantifier
q vars :: THF_variable_list
vars ->
    [Sign] -> Sign
signatureUnions [THF_quantifier -> Sign
signOfTHF_quantifier THF_quantifier
q, THF_variable_list -> Sign
signOfTHF_variable_list THF_variable_list
vars]

signOfTHF_variable_list :: THF_variable_list -> Sign
signOfTHF_variable_list :: THF_variable_list -> Sign
signOfTHF_variable_list = [Sign] -> Sign
signatureUnions ([Sign] -> Sign)
-> (THF_variable_list -> [Sign]) -> THF_variable_list -> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (THF_variable -> Sign) -> THF_variable_list -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map THF_variable -> Sign
signOfTHF_variable

signOfTHF_variable :: THF_variable -> Sign
signOfTHF_variable :: THF_variable -> Sign
signOfTHF_variable x :: THF_variable
x = case THF_variable
x of
  THFV_typed a :: THF_typed_variable
a -> THF_typed_variable -> Sign
signOfTHF_typed_variable THF_typed_variable
a
  THFV_variable a :: Atomic_defined_word
a -> Atomic_defined_word -> Sign
signOfVariable Atomic_defined_word
a

signOfTHF_typed_variable :: THF_typed_variable -> Sign
signOfTHF_typed_variable :: THF_typed_variable -> Sign
signOfTHF_typed_variable x :: THF_typed_variable
x = case THF_typed_variable
x of
  THF_typed_variable v :: Atomic_defined_word
v tlt :: THF_top_level_type
tlt ->
    [Sign] -> Sign
signatureUnions [Atomic_defined_word -> Sign
signOfVariable Atomic_defined_word
v, THF_top_level_type -> Sign
signOfTHF_top_level_type THF_top_level_type
tlt]

signOfTHF_unary_formula :: THF_unary_formula -> Sign
signOfTHF_unary_formula :: THF_unary_formula -> Sign
signOfTHF_unary_formula x :: THF_unary_formula
x = case THF_unary_formula
x of
  THF_unary_formula c :: THF_unary_connective
c f :: THF_logic_formula
f ->
    [Sign] -> Sign
signatureUnions [THF_unary_connective -> Sign
signOfTHF_unary_connective THF_unary_connective
c, THF_logic_formula -> Sign
signOfTHF_logic_formula THF_logic_formula
f]

signOfTHF_atom :: THF_atom -> Sign
signOfTHF_atom :: THF_atom -> Sign
signOfTHF_atom x :: THF_atom
x = case THF_atom
x of
  THF_atom_function a :: THF_function
a -> THF_function -> Sign
signOfTHF_function THF_function
a
  THF_atom_variable a :: Atomic_defined_word
a -> Atomic_defined_word -> Sign
signOfVariable Atomic_defined_word
a
  THF_atom_defined a :: Defined_term
a -> Defined_term -> Sign
signOfDefined_term Defined_term
a
  THF_atom_conn a :: THF_conn_term
a -> THF_conn_term -> Sign
signOfTHF_conn_term THF_conn_term
a

signOfTHF_function :: THF_function -> Sign
signOfTHF_function :: THF_function -> Sign
signOfTHF_function x :: THF_function
x = case THF_function
x of
  THFF_atom a :: Atom
a -> Atom -> Sign
signOfAtom Atom
a
  THFF_functor f :: Atomic_defined_word
f args :: THF_arguments
args ->
    [Sign] -> Sign
signatureUnions [ Atomic_defined_word -> Int -> Sign
signOfTPTP_functor Atomic_defined_word
f (Int -> Sign) -> Int -> Sign
forall a b. (a -> b) -> a -> b
$ THF_arguments -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length THF_arguments
args
                    , THF_arguments -> Sign
signOfTHF_arguments THF_arguments
args]
  THFF_defined f :: Defined_functor
f args :: THF_arguments
args ->
    [Sign] -> Sign
signatureUnions [Defined_functor -> Sign
signOfDefined_functor Defined_functor
f, THF_arguments -> Sign
signOfTHF_arguments THF_arguments
args]
  THFF_system f :: Atomic_defined_word
f args :: THF_arguments
args ->
    [Sign] -> Sign
signatureUnions [Atomic_defined_word -> Sign
signOfSystem_functor Atomic_defined_word
f, THF_arguments -> Sign
signOfTHF_arguments THF_arguments
args]

signOfTHF_conn_term :: THF_conn_term -> Sign
signOfTHF_conn_term :: THF_conn_term -> Sign
signOfTHF_conn_term x :: THF_conn_term
x = case THF_conn_term
x of
  THFC_pair a :: THF_pair_connective
a -> THF_pair_connective -> Sign
signOfTHF_pair_connective THF_pair_connective
a
  THFC_assoc a :: Assoc_connective
a -> Assoc_connective -> Sign
signOfAssoc_connective Assoc_connective
a
  THFC_unary a :: THF_unary_connective
a -> THF_unary_connective -> Sign
signOfTHF_unary_connective THF_unary_connective
a

signOfTHF_conditional :: THF_conditional -> Sign
signOfTHF_conditional :: THF_conditional -> Sign
signOfTHF_conditional x :: THF_conditional
x = case THF_conditional
x of
  THF_conditional f_if :: THF_logic_formula
f_if f_then :: THF_logic_formula
f_then f_else :: THF_logic_formula
f_else ->
    [Sign] -> Sign
signatureUnions ([Sign] -> Sign) -> [Sign] -> Sign
forall a b. (a -> b) -> a -> b
$ (THF_logic_formula -> Sign) -> THF_arguments -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map THF_logic_formula -> Sign
signOfTHF_logic_formula [THF_logic_formula
f_if, THF_logic_formula
f_then, THF_logic_formula
f_else]

signOfTHF_let :: THF_let -> Sign
signOfTHF_let :: THF_let -> Sign
signOfTHF_let x :: THF_let
x = case THF_let
x of
  THF_let defns :: THF_let_defns
defns f :: THF_formula
f ->
    [Sign] -> Sign
signatureUnions [THF_let_defns -> Sign
signOfTHF_let_defns THF_let_defns
defns, THF_formula -> Sign
signOfTHF_formula THF_formula
f]

signOfTHF_let_defns :: THF_let_defns -> Sign
signOfTHF_let_defns :: THF_let_defns -> Sign
signOfTHF_let_defns x :: THF_let_defns
x = case THF_let_defns
x of
  THFLD_single a :: THF_let_defn
a -> THF_let_defn -> Sign
signOfTHF_let_defn THF_let_defn
a
  THFLD_many a :: THF_let_defn_list
a -> THF_let_defn_list -> Sign
signOfTHF_let_defn_list THF_let_defn_list
a

signOfTHF_let_defn_list :: THF_let_defn_list -> Sign
signOfTHF_let_defn_list :: THF_let_defn_list -> Sign
signOfTHF_let_defn_list = [Sign] -> Sign
signatureUnions ([Sign] -> Sign)
-> (THF_let_defn_list -> [Sign]) -> THF_let_defn_list -> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (THF_let_defn -> Sign) -> THF_let_defn_list -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map THF_let_defn -> Sign
signOfTHF_let_defn

signOfTHF_let_defn :: THF_let_defn -> Sign
signOfTHF_let_defn :: THF_let_defn -> Sign
signOfTHF_let_defn x :: THF_let_defn
x = case THF_let_defn
x of
  THFLD_quantified a :: THF_let_quantified_defn
a -> THF_let_quantified_defn -> Sign
signOfTHF_let_quantified_defn THF_let_quantified_defn
a
  THFLD_plain a :: THF_let_plain_defn
a -> THF_let_plain_defn -> Sign
signOfTHF_let_plain_defn THF_let_plain_defn
a

signOfTHF_let_quantified_defn :: THF_let_quantified_defn -> Sign
signOfTHF_let_quantified_defn :: THF_let_quantified_defn -> Sign
signOfTHF_let_quantified_defn x :: THF_let_quantified_defn
x = case THF_let_quantified_defn
x of
  THF_let_quantified_defn q :: THF_quantification
q lpd :: THF_let_plain_defn
lpd ->
    [Sign] -> Sign
signatureUnions [THF_quantification -> Sign
signOfTHF_quantification THF_quantification
q, THF_let_plain_defn -> Sign
signOfTHF_let_plain_defn THF_let_plain_defn
lpd]

signOfTHF_let_plain_defn :: THF_let_plain_defn -> Sign
signOfTHF_let_plain_defn :: THF_let_plain_defn -> Sign
signOfTHF_let_plain_defn x :: THF_let_plain_defn
x = case THF_let_plain_defn
x of
  THF_let_plain_defn lhs :: THF_let_defn_LHS
lhs f :: THF_formula
f ->
    [Sign] -> Sign
signatureUnions [THF_let_defn_LHS -> Sign
signOfTHF_let_defn_LHS THF_let_defn_LHS
lhs, THF_formula -> Sign
signOfTHF_formula THF_formula
f]

signOfTHF_let_defn_LHS :: THF_let_defn_LHS -> Sign
signOfTHF_let_defn_LHS :: THF_let_defn_LHS -> Sign
signOfTHF_let_defn_LHS x :: THF_let_defn_LHS
x = case THF_let_defn_LHS
x of
  THFLDL_constant a :: Atomic_defined_word
a -> Atomic_defined_word -> Sign
signOfConstant Atomic_defined_word
a
  THFLDL_functor f :: Atomic_defined_word
f args :: FOF_arguments
args ->
    [Sign] -> Sign
signatureUnions [ Atomic_defined_word -> Int -> Sign
signOfTPTP_functor Atomic_defined_word
f (Int -> Sign) -> Int -> Sign
forall a b. (a -> b) -> a -> b
$ FOF_arguments -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length FOF_arguments
args
                    , FOF_arguments -> Sign
signOfFOF_arguments FOF_arguments
args]
  THFLDL_tuple a :: THF_tuple
a -> THF_tuple -> Sign
signOfTHF_tuple THF_tuple
a

signOfTHF_arguments :: THF_arguments -> Sign
signOfTHF_arguments :: THF_arguments -> Sign
signOfTHF_arguments = THF_arguments -> Sign
signOfTHF_formula_list

signOfTHF_type_formula :: THF_type_formula -> Sign
signOfTHF_type_formula :: THF_type_formula -> Sign
signOfTHF_type_formula x :: THF_type_formula
x = case THF_type_formula
x of
  THFTF_typeable f :: THF_typeable_formula
f tlt :: THF_top_level_type
tlt -> [Sign] -> Sign
signatureUnions
    [ Sign
emptySign { thfTypeDeclarationMap :: THFPredicateMap
thfTypeDeclarationMap = THFTypeable -> THF_top_level_type -> THFPredicateMap
forall k a. k -> a -> Map k a
Map.singleton (THF_typeable_formula -> THFTypeable
THFTypeFormula THF_typeable_formula
f) THF_top_level_type
tlt }
    , THF_typeable_formula -> Sign
signOfTHF_typeable_formula THF_typeable_formula
f
    , THF_top_level_type -> Sign
signOfTHF_top_level_type THF_top_level_type
tlt
    ]
  THFTF_constant c :: Atomic_defined_word
c tlt :: THF_top_level_type
tlt -> [Sign] -> Sign
signatureUnions
    [ Sign
emptySign { thfTypeDeclarationMap :: THFPredicateMap
thfTypeDeclarationMap = THFTypeable -> THF_top_level_type -> THFPredicateMap
forall k a. k -> a -> Map k a
Map.singleton (Atomic_defined_word -> THFTypeable
THFTypeConstant Atomic_defined_word
c) THF_top_level_type
tlt }
    , Atomic_defined_word -> Sign
signOfConstant Atomic_defined_word
c
    , THF_top_level_type -> Sign
signOfTHF_top_level_type THF_top_level_type
tlt
    ]

signOfTHF_typeable_formula :: THF_typeable_formula -> Sign
signOfTHF_typeable_formula :: THF_typeable_formula -> Sign
signOfTHF_typeable_formula x :: THF_typeable_formula
x = case THF_typeable_formula
x of
  THFTF_atom a :: THF_atom
a -> THF_atom -> Sign
signOfTHF_atom THF_atom
a
  THFTF_logic a :: THF_logic_formula
a -> THF_logic_formula -> Sign
signOfTHF_logic_formula THF_logic_formula
a

signOfTHF_subtype :: THF_subtype -> Sign
signOfTHF_subtype :: THF_subtype -> Sign
signOfTHF_subtype x :: THF_subtype
x = case THF_subtype
x of
  THF_subtype a1 :: THF_atom
a1 a2 :: THF_atom
a2 -> [Sign] -> Sign
signatureUnions
    [ Sign
emptySign { thfSubtypeMap :: THFSubTypeMap
thfSubtypeMap = THF_atom -> THF_atom -> THFSubTypeMap
forall k a. k -> a -> Map k a
Map.singleton THF_atom
a1 THF_atom
a2 }
    , THF_atom -> Sign
signOfTHF_atom THF_atom
a1, THF_atom -> Sign
signOfTHF_atom THF_atom
a2
    ]

signOfTHF_top_level_type :: THF_top_level_type -> Sign
signOfTHF_top_level_type :: THF_top_level_type -> Sign
signOfTHF_top_level_type x :: THF_top_level_type
x = case THF_top_level_type
x of
  THFTLT_unitary a :: THF_unitary_type
a -> THF_unitary_type -> Sign
signOfTHF_unitary_type THF_unitary_type
a
  THFTLT_mapping a :: THF_mapping_type
a -> THF_mapping_type -> Sign
signOfTHF_mapping_type THF_mapping_type
a

signOfTHF_unitary_type :: THF_unitary_type -> Sign
signOfTHF_unitary_type :: THF_unitary_type -> Sign
signOfTHF_unitary_type x :: THF_unitary_type
x = case THF_unitary_type
x of
  THFUT_unitary a :: THF_unitary_formula
a -> THF_unitary_formula -> Sign
signOfTHF_unitary_formula THF_unitary_formula
a
  THFUT_binary a :: THF_binary_type
a -> THF_binary_type -> Sign
signOfTHF_binary_type THF_binary_type
a

signOfTHF_binary_type :: THF_binary_type -> Sign
signOfTHF_binary_type :: THF_binary_type -> Sign
signOfTHF_binary_type x :: THF_binary_type
x = case THF_binary_type
x of
  THFBT_mapping a :: THF_mapping_type
a -> THF_mapping_type -> Sign
signOfTHF_mapping_type THF_mapping_type
a
  THFBT_xprod a :: THF_mapping_type
a -> THF_mapping_type -> Sign
signOfTHF_xprod_type THF_mapping_type
a
  THFBT_union a :: THF_mapping_type
a -> THF_mapping_type -> Sign
signOfTHF_union_type THF_mapping_type
a

signOfTHF_mapping_type :: THF_mapping_type -> Sign
signOfTHF_mapping_type :: THF_mapping_type -> Sign
signOfTHF_mapping_type = [Sign] -> Sign
signatureUnions ([Sign] -> Sign)
-> (THF_mapping_type -> [Sign]) -> THF_mapping_type -> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (THF_unitary_type -> Sign) -> THF_mapping_type -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map THF_unitary_type -> Sign
signOfTHF_unitary_type

signOfTHF_xprod_type :: THF_xprod_type -> Sign
signOfTHF_xprod_type :: THF_mapping_type -> Sign
signOfTHF_xprod_type = [Sign] -> Sign
signatureUnions ([Sign] -> Sign)
-> (THF_mapping_type -> [Sign]) -> THF_mapping_type -> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (THF_unitary_type -> Sign) -> THF_mapping_type -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map THF_unitary_type -> Sign
signOfTHF_unitary_type

signOfTHF_union_type :: THF_union_type -> Sign
signOfTHF_union_type :: THF_mapping_type -> Sign
signOfTHF_union_type = [Sign] -> Sign
signatureUnions ([Sign] -> Sign)
-> (THF_mapping_type -> [Sign]) -> THF_mapping_type -> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (THF_unitary_type -> Sign) -> THF_mapping_type -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map THF_unitary_type -> Sign
signOfTHF_unitary_type

signOfTHF_sequent :: THF_sequent -> Sign
signOfTHF_sequent :: THF_sequent -> Sign
signOfTHF_sequent x :: THF_sequent
x = case THF_sequent
x of
  THFS_plain t1 :: THF_tuple
t1 t2 :: THF_tuple
t2 -> [Sign] -> Sign
signatureUnions ([Sign] -> Sign) -> [Sign] -> Sign
forall a b. (a -> b) -> a -> b
$ (THF_tuple -> Sign) -> [THF_tuple] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map THF_tuple -> Sign
signOfTHF_tuple [THF_tuple
t1, THF_tuple
t2]
  THFS_parens a :: THF_sequent
a -> THF_sequent -> Sign
signOfTHF_sequent THF_sequent
a

signOfTHF_tuple :: THF_tuple -> Sign
signOfTHF_tuple :: THF_tuple -> Sign
signOfTHF_tuple x :: THF_tuple
x = case THF_tuple
x of
  THF_tuple a :: THF_arguments
a -> THF_arguments -> Sign
signOfTHF_formula_list THF_arguments
a

signOfTHF_formula_list :: THF_formula_list -> Sign
signOfTHF_formula_list :: THF_arguments -> Sign
signOfTHF_formula_list = [Sign] -> Sign
signatureUnions ([Sign] -> Sign)
-> (THF_arguments -> [Sign]) -> THF_arguments -> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (THF_logic_formula -> Sign) -> THF_arguments -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map THF_logic_formula -> Sign
signOfTHF_logic_formula

signOfTFX_formula :: TFX_formula -> Sign
signOfTFX_formula :: TFX_formula -> Sign
signOfTFX_formula x :: TFX_formula
x = case TFX_formula
x of
  TFXF_logic a :: TFX_logic_formula
a -> TFX_logic_formula -> Sign
signOfTFX_logic_formula TFX_logic_formula
a
  TFXF_sequent a :: THF_sequent
a -> THF_sequent -> Sign
signOfTHF_sequent THF_sequent
a

signOfTFX_logic_formula :: TFX_logic_formula -> Sign
signOfTFX_logic_formula :: TFX_logic_formula -> Sign
signOfTFX_logic_formula x :: TFX_logic_formula
x = case TFX_logic_formula
x of
  TFXLF_binary a :: THF_binary_formula
a -> THF_binary_formula -> Sign
signOfTHF_binary_formula THF_binary_formula
a
  TFXLF_unitary a :: THF_unitary_formula
a -> THF_unitary_formula -> Sign
signOfTHF_unitary_formula THF_unitary_formula
a
  TFXLF_typed a :: TFF_typed_atom
a -> TFF_typed_atom -> Sign
signOfTFF_typed_atom TFF_typed_atom
a
  TFXLF_subtype a :: TFF_subtype
a -> TFF_subtype -> Sign
signOfTFF_subtype TFF_subtype
a

signOfTFF_formula :: TFF_formula -> Sign
signOfTFF_formula :: TFF_formula -> Sign
signOfTFF_formula x :: TFF_formula
x = case TFF_formula
x of
  TFFF_logic a :: TFF_logic_formula
a -> TFF_logic_formula -> Sign
signOfTFF_logic_formula TFF_logic_formula
a
  TFFF_atom a :: TFF_typed_atom
a -> TFF_typed_atom -> Sign
signOfTFF_typed_atom TFF_typed_atom
a
  TFFF_sequent a :: TFF_sequent
a -> TFF_sequent -> Sign
signOfTFF_sequent TFF_sequent
a

signOfTFF_logic_formula :: TFF_logic_formula -> Sign
signOfTFF_logic_formula :: TFF_logic_formula -> Sign
signOfTFF_logic_formula x :: TFF_logic_formula
x = case TFF_logic_formula
x of
  TFFLF_binary a :: TFF_binary_formula
a -> TFF_binary_formula -> Sign
signOfTFF_binary_formula TFF_binary_formula
a
  TFFLF_unitary a :: TFF_unitary_formula
a -> TFF_unitary_formula -> Sign
signOfTFF_unitary_formula TFF_unitary_formula
a
  TFFLF_subtype a :: TFF_subtype
a -> TFF_subtype -> Sign
signOfTFF_subtype TFF_subtype
a

signOfTFF_binary_formula :: TFF_binary_formula -> Sign
signOfTFF_binary_formula :: TFF_binary_formula -> Sign
signOfTFF_binary_formula x :: TFF_binary_formula
x = case TFF_binary_formula
x of
  TFFBF_nonassoc a :: TFF_binary_nonassoc
a -> TFF_binary_nonassoc -> Sign
signOfTFF_binary_nonassoc TFF_binary_nonassoc
a
  TFFBF_assoc a :: TFF_binary_assoc
a -> TFF_binary_assoc -> Sign
signOfTFF_binary_assoc TFF_binary_assoc
a

signOfTFF_binary_nonassoc :: TFF_binary_nonassoc -> Sign
signOfTFF_binary_nonassoc :: TFF_binary_nonassoc -> Sign
signOfTFF_binary_nonassoc x :: TFF_binary_nonassoc
x = case TFF_binary_nonassoc
x of
  TFF_binary_nonassoc c :: Binary_connective
c f1 :: TFF_unitary_formula
f1 f2 :: TFF_unitary_formula
f2 ->
    [Sign] -> Sign
signatureUnions ([Sign] -> Sign) -> [Sign] -> Sign
forall a b. (a -> b) -> a -> b
$
      Binary_connective -> Sign
signOfBinary_connective Binary_connective
c Sign -> [Sign] -> [Sign]
forall a. a -> [a] -> [a]
: (TFF_unitary_formula -> Sign) -> [TFF_unitary_formula] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map TFF_unitary_formula -> Sign
signOfTFF_unitary_formula [TFF_unitary_formula
f1, TFF_unitary_formula
f2]

signOfTFF_binary_assoc :: TFF_binary_assoc -> Sign
signOfTFF_binary_assoc :: TFF_binary_assoc -> Sign
signOfTFF_binary_assoc x :: TFF_binary_assoc
x = case TFF_binary_assoc
x of
  TFFBA_or a :: [TFF_unitary_formula]
a -> [TFF_unitary_formula] -> Sign
signOfTFF_or_formula [TFF_unitary_formula]
a
  TFFBA_and a :: [TFF_unitary_formula]
a -> [TFF_unitary_formula] -> Sign
signOfTFF_and_formula [TFF_unitary_formula]
a

signOfTFF_or_formula :: TFF_or_formula -> Sign
signOfTFF_or_formula :: [TFF_unitary_formula] -> Sign
signOfTFF_or_formula = [Sign] -> Sign
signatureUnions ([Sign] -> Sign)
-> ([TFF_unitary_formula] -> [Sign])
-> [TFF_unitary_formula]
-> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TFF_unitary_formula -> Sign) -> [TFF_unitary_formula] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map TFF_unitary_formula -> Sign
signOfTFF_unitary_formula

signOfTFF_and_formula :: TFF_and_formula -> Sign
signOfTFF_and_formula :: [TFF_unitary_formula] -> Sign
signOfTFF_and_formula = [Sign] -> Sign
signatureUnions ([Sign] -> Sign)
-> ([TFF_unitary_formula] -> [Sign])
-> [TFF_unitary_formula]
-> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TFF_unitary_formula -> Sign) -> [TFF_unitary_formula] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map TFF_unitary_formula -> Sign
signOfTFF_unitary_formula

signOfTFF_unitary_formula :: TFF_unitary_formula -> Sign
signOfTFF_unitary_formula :: TFF_unitary_formula -> Sign
signOfTFF_unitary_formula x :: TFF_unitary_formula
x = case TFF_unitary_formula
x of
  TFFUF_quantified a :: TFF_quantified_formula
a -> TFF_quantified_formula -> Sign
signOfTFF_quantified_formula TFF_quantified_formula
a
  TFFUF_unary a :: TFF_unary_formula
a -> TFF_unary_formula -> Sign
signOfTFF_unary_formula TFF_unary_formula
a
  TFFUF_atomic a :: TFF_atomic_formula
a -> TFF_atomic_formula -> Sign
signOfTFF_atomic_formula TFF_atomic_formula
a
  TFFUF_conditional a :: TFF_conditional
a -> TFF_conditional -> Sign
signOfTFF_conditional TFF_conditional
a
  TFFUF_let a :: TFF_let
a -> TFF_let -> Sign
signOfTFF_let TFF_let
a
  TFFUF_logic a :: TFF_logic_formula
a -> TFF_logic_formula -> Sign
signOfTFF_logic_formula TFF_logic_formula
a

signOfTFF_quantified_formula :: TFF_quantified_formula -> Sign
signOfTFF_quantified_formula :: TFF_quantified_formula -> Sign
signOfTFF_quantified_formula x :: TFF_quantified_formula
x = case TFF_quantified_formula
x of
  TFF_quantified_formula q :: FOF_quantifier
q vars :: TFF_variable_list
vars f :: TFF_unitary_formula
f ->
    [Sign] -> Sign
signatureUnions [ FOF_quantifier -> Sign
signOfFOF_quantifier FOF_quantifier
q
                    , TFF_variable_list -> Sign
signOfTFF_variable_list TFF_variable_list
vars
                    , TFF_unitary_formula -> Sign
signOfTFF_unitary_formula TFF_unitary_formula
f
                    ]

signOfTFF_variable_list :: TFF_variable_list -> Sign
signOfTFF_variable_list :: TFF_variable_list -> Sign
signOfTFF_variable_list = [Sign] -> Sign
signatureUnions ([Sign] -> Sign)
-> (TFF_variable_list -> [Sign]) -> TFF_variable_list -> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TFF_variable -> Sign) -> TFF_variable_list -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map TFF_variable -> Sign
signOfTFF_variable

signOfTFF_variable :: TFF_variable -> Sign
signOfTFF_variable :: TFF_variable -> Sign
signOfTFF_variable x :: TFF_variable
x = case TFF_variable
x of
  TFFV_typed a :: TFF_typed_variable
a -> TFF_typed_variable -> Sign
signOfTFF_typed_variable TFF_typed_variable
a
  TFFV_variable a :: Atomic_defined_word
a -> Atomic_defined_word -> Sign
signOfVariable Atomic_defined_word
a

signOfTFF_typed_variable :: TFF_typed_variable -> Sign
signOfTFF_typed_variable :: TFF_typed_variable -> Sign
signOfTFF_typed_variable x :: TFF_typed_variable
x = case TFF_typed_variable
x of
  TFF_typed_variable v :: Atomic_defined_word
v t :: TFF_atomic_type
t ->
    [Sign] -> Sign
signatureUnions [Atomic_defined_word -> Sign
signOfVariable Atomic_defined_word
v, TFF_atomic_type -> Sign
signOfTFF_atomic_type TFF_atomic_type
t]

signOfTFF_unary_formula :: TFF_unary_formula -> Sign
signOfTFF_unary_formula :: TFF_unary_formula -> Sign
signOfTFF_unary_formula x :: TFF_unary_formula
x = case TFF_unary_formula
x of
  TFFUF_connective c :: Unary_connective
c f :: TFF_unitary_formula
f ->
    [Sign] -> Sign
signatureUnions [Unary_connective -> Sign
signOfUnary_connective Unary_connective
c, TFF_unitary_formula -> Sign
signOfTFF_unitary_formula TFF_unitary_formula
f]
  TFFUF_infix a :: FOF_infix_unary
a -> FOF_infix_unary -> Sign
signOfFOF_infix_unary FOF_infix_unary
a

signOfTFF_atomic_formula :: TFF_atomic_formula -> Sign
signOfTFF_atomic_formula :: TFF_atomic_formula -> Sign
signOfTFF_atomic_formula = TFF_atomic_formula -> Sign
signOfFOF_atomic_formula

signOfTFF_conditional :: TFF_conditional -> Sign
signOfTFF_conditional :: TFF_conditional -> Sign
signOfTFF_conditional x :: TFF_conditional
x = case TFF_conditional
x of
  TFF_conditional f_if :: TFF_logic_formula
f_if f_then :: TFF_logic_formula
f_then f_else :: TFF_logic_formula
f_else ->
    [Sign] -> Sign
signatureUnions ([Sign] -> Sign) -> [Sign] -> Sign
forall a b. (a -> b) -> a -> b
$ (TFF_logic_formula -> Sign) -> [TFF_logic_formula] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map TFF_logic_formula -> Sign
signOfTFF_logic_formula [TFF_logic_formula
f_if, TFF_logic_formula
f_then, TFF_logic_formula
f_else]

signOfTFF_let :: TFF_let -> Sign
signOfTFF_let :: TFF_let -> Sign
signOfTFF_let x :: TFF_let
x = case TFF_let
x of
  TFF_let_term_defns defns :: TFF_let_term_defns
defns f :: TFF_formula
f ->
    [Sign] -> Sign
signatureUnions [TFF_let_term_defns -> Sign
signOfTFF_let_term_defns TFF_let_term_defns
defns, TFF_formula -> Sign
signOfTFF_formula TFF_formula
f]
  TFF_let_formula_defns defns :: TFF_let_formula_defns
defns f :: TFF_formula
f ->
    [Sign] -> Sign
signatureUnions [TFF_let_formula_defns -> Sign
signOfTFF_let_formula_defns TFF_let_formula_defns
defns, TFF_formula -> Sign
signOfTFF_formula TFF_formula
f]

signOfTFF_let_term_defns :: TFF_let_term_defns -> Sign
signOfTFF_let_term_defns :: TFF_let_term_defns -> Sign
signOfTFF_let_term_defns x :: TFF_let_term_defns
x = case TFF_let_term_defns
x of
  TFFLTD_single a :: TFF_let_term_defn
a -> TFF_let_term_defn -> Sign
signOfTFF_let_term_defn TFF_let_term_defn
a
  TFFLTD_many a :: TFF_let_term_list
a -> TFF_let_term_list -> Sign
signOfTFF_let_term_list TFF_let_term_list
a

signOfTFF_let_term_list :: TFF_let_term_list -> Sign
signOfTFF_let_term_list :: TFF_let_term_list -> Sign
signOfTFF_let_term_list = [Sign] -> Sign
signatureUnions ([Sign] -> Sign)
-> (TFF_let_term_list -> [Sign]) -> TFF_let_term_list -> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TFF_let_term_defn -> Sign) -> TFF_let_term_list -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map TFF_let_term_defn -> Sign
signOfTFF_let_term_defn

signOfTFF_let_term_defn :: TFF_let_term_defn -> Sign
signOfTFF_let_term_defn :: TFF_let_term_defn -> Sign
signOfTFF_let_term_defn x :: TFF_let_term_defn
x = case TFF_let_term_defn
x of
  TFFLTD_variable vars :: TFF_variable_list
vars defn :: TFF_let_term_defn
defn ->
    [Sign] -> Sign
signatureUnions [ TFF_variable_list -> Sign
signOfTFF_variable_list TFF_variable_list
vars
                    , TFF_let_term_defn -> Sign
signOfTFF_let_term_defn TFF_let_term_defn
defn
                    ]
  TFFLTD_binding a :: TFF_let_term_binding
a -> TFF_let_term_binding -> Sign
signOfTFF_let_term_binding TFF_let_term_binding
a

signOfTFF_let_term_binding :: TFF_let_term_binding -> Sign
signOfTFF_let_term_binding :: TFF_let_term_binding -> Sign
signOfTFF_let_term_binding x :: TFF_let_term_binding
x = case TFF_let_term_binding
x of
  TFFLTB_plain pt :: FOF_plain_term
pt t :: FOF_term
t ->
    [Sign] -> Sign
signatureUnions [FOF_plain_term -> Sign
signOfFOF_plain_term FOF_plain_term
pt, FOF_term -> Sign
signOfFOF_term FOF_term
t]
  TFFLTB_binding a :: TFF_let_term_binding
a -> TFF_let_term_binding -> Sign
signOfTFF_let_term_binding TFF_let_term_binding
a

signOfTFF_let_formula_defns :: TFF_let_formula_defns -> Sign
signOfTFF_let_formula_defns :: TFF_let_formula_defns -> Sign
signOfTFF_let_formula_defns x :: TFF_let_formula_defns
x = case TFF_let_formula_defns
x of
  TFFLFD_single a :: TFF_let_formula_defn
a -> TFF_let_formula_defn -> Sign
signOfTFF_let_formula_defn TFF_let_formula_defn
a
  TFFLFD_many a :: TFF_let_formula_list
a -> TFF_let_formula_list -> Sign
signOfTFF_let_formula_list TFF_let_formula_list
a

signOfTFF_let_formula_list :: TFF_let_formula_list -> Sign
signOfTFF_let_formula_list :: TFF_let_formula_list -> Sign
signOfTFF_let_formula_list = [Sign] -> Sign
signatureUnions ([Sign] -> Sign)
-> (TFF_let_formula_list -> [Sign]) -> TFF_let_formula_list -> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TFF_let_formula_defn -> Sign) -> TFF_let_formula_list -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map TFF_let_formula_defn -> Sign
signOfTFF_let_formula_defn

signOfTFF_let_formula_defn :: TFF_let_formula_defn -> Sign
signOfTFF_let_formula_defn :: TFF_let_formula_defn -> Sign
signOfTFF_let_formula_defn x :: TFF_let_formula_defn
x = case TFF_let_formula_defn
x of
  TFFLFD_variable vars :: TFF_variable_list
vars defn :: TFF_let_formula_defn
defn ->
    [Sign] -> Sign
signatureUnions [ TFF_variable_list -> Sign
signOfTFF_variable_list TFF_variable_list
vars
                    , TFF_let_formula_defn -> Sign
signOfTFF_let_formula_defn TFF_let_formula_defn
defn
                    ]
  TFFLFD_binding a :: TFF_let_formula_binding
a -> TFF_let_formula_binding -> Sign
signOfTFF_let_formula_binding TFF_let_formula_binding
a

signOfTFF_let_formula_binding :: TFF_let_formula_binding -> Sign
signOfTFF_let_formula_binding :: TFF_let_formula_binding -> Sign
signOfTFF_let_formula_binding x :: TFF_let_formula_binding
x = case TFF_let_formula_binding
x of
  TFFLFB_plain paf :: FOF_plain_atomic_formula
paf uf :: TFF_unitary_formula
uf ->
    [Sign] -> Sign
signatureUnions [ FOF_plain_atomic_formula -> Sign
signOfFOF_plain_atomic_formula FOF_plain_atomic_formula
paf
                    , TFF_unitary_formula -> Sign
signOfTFF_unitary_formula TFF_unitary_formula
uf
                    ]
  TFFLFB_binding a :: TFF_let_formula_binding
a -> TFF_let_formula_binding -> Sign
signOfTFF_let_formula_binding TFF_let_formula_binding
a

signOfTFF_sequent :: TFF_sequent -> Sign
signOfTFF_sequent :: TFF_sequent -> Sign
signOfTFF_sequent x :: TFF_sequent
x = case TFF_sequent
x of
  TFFS_plain t1 :: TFF_formula_tuple
t1 t2 :: TFF_formula_tuple
t2 -> [Sign] -> Sign
signatureUnions ([Sign] -> Sign) -> [Sign] -> Sign
forall a b. (a -> b) -> a -> b
$ (TFF_formula_tuple -> Sign) -> [TFF_formula_tuple] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map TFF_formula_tuple -> Sign
signOfTFF_formula_tuple [TFF_formula_tuple
t1, TFF_formula_tuple
t2]
  TFFS_parens a :: TFF_sequent
a -> TFF_sequent -> Sign
signOfTFF_sequent TFF_sequent
a

signOfTFF_formula_tuple :: TFF_formula_tuple -> Sign
signOfTFF_formula_tuple :: TFF_formula_tuple -> Sign
signOfTFF_formula_tuple x :: TFF_formula_tuple
x = case TFF_formula_tuple
x of
  TFF_formula_tuple a :: [TFF_logic_formula]
a -> [TFF_logic_formula] -> Sign
signOfTFF_formula_tuple_list [TFF_logic_formula]
a

signOfTFF_formula_tuple_list :: TFF_formula_tuple_list -> Sign
signOfTFF_formula_tuple_list :: [TFF_logic_formula] -> Sign
signOfTFF_formula_tuple_list = [Sign] -> Sign
signatureUnions ([Sign] -> Sign)
-> ([TFF_logic_formula] -> [Sign]) -> [TFF_logic_formula] -> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TFF_logic_formula -> Sign) -> [TFF_logic_formula] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map TFF_logic_formula -> Sign
signOfTFF_logic_formula

signOfTFF_typed_atom :: TFF_typed_atom -> Sign
signOfTFF_typed_atom :: TFF_typed_atom -> Sign
signOfTFF_typed_atom x :: TFF_typed_atom
x = case TFF_typed_atom
x of
  TFFTA_plain ua :: Untyped_atom
ua tlt :: TFF_top_level_type
tlt -> [Sign] -> Sign
signatureUnions
    [ Sign
emptySign { tffTypeDeclarationMap :: TFFPredicateMap
tffTypeDeclarationMap = Untyped_atom -> TFF_top_level_type -> TFFPredicateMap
forall k a. k -> a -> Map k a
Map.singleton Untyped_atom
ua TFF_top_level_type
tlt }
    , Untyped_atom -> Sign
signOfUntyped_atom Untyped_atom
ua
    , TFF_top_level_type -> Sign
signOfTFF_top_level_type TFF_top_level_type
tlt
    ]
  TFFTA_parens a :: TFF_typed_atom
a -> TFF_typed_atom -> Sign
signOfTFF_typed_atom TFF_typed_atom
a

signOfTFF_subtype :: TFF_subtype -> Sign
signOfTFF_subtype :: TFF_subtype -> Sign
signOfTFF_subtype x :: TFF_subtype
x = case TFF_subtype
x of
  TFF_subtype ua :: Untyped_atom
ua a :: Atom
a -> [Sign] -> Sign
signatureUnions
    [ Sign
emptySign { tffSubtypeMap :: TFFSubTypeMap
tffSubtypeMap = Untyped_atom -> Atom -> TFFSubTypeMap
forall k a. k -> a -> Map k a
Map.singleton Untyped_atom
ua Atom
a }
    , Untyped_atom -> Sign
signOfUntyped_atom Untyped_atom
ua, Atom -> Sign
signOfAtom Atom
a
    ]

signOfTFF_top_level_type :: TFF_top_level_type -> Sign
signOfTFF_top_level_type :: TFF_top_level_type -> Sign
signOfTFF_top_level_type x :: TFF_top_level_type
x = case TFF_top_level_type
x of
  TFFTLT_atomic a :: TFF_atomic_type
a -> TFF_atomic_type -> Sign
signOfTFF_atomic_type TFF_atomic_type
a
  TFFTLT_mapping a :: TFF_mapping_type
a -> TFF_mapping_type -> Sign
signOfTFF_mapping_type TFF_mapping_type
a
  TFFTLT_quantified a :: TF1_quantified_type
a -> TF1_quantified_type -> Sign
signOfTF1_quantified_type TF1_quantified_type
a
  TFFTLT_parens a :: TFF_top_level_type
a -> TFF_top_level_type -> Sign
signOfTFF_top_level_type TFF_top_level_type
a

signOfTF1_quantified_type :: TF1_quantified_type -> Sign
signOfTF1_quantified_type :: TF1_quantified_type -> Sign
signOfTF1_quantified_type x :: TF1_quantified_type
x = case TF1_quantified_type
x of
  TF1_quantified_type vars :: TFF_variable_list
vars t :: TFF_monotype
t ->
    [Sign] -> Sign
signatureUnions [ TFF_variable_list -> Sign
signOfTFF_variable_list TFF_variable_list
vars
                    , TFF_monotype -> Sign
signOfTFF_monotype TFF_monotype
t
                    ]

signOfTFF_monotype :: TFF_monotype -> Sign
signOfTFF_monotype :: TFF_monotype -> Sign
signOfTFF_monotype x :: TFF_monotype
x = case TFF_monotype
x of
  TFFMT_atomic a :: TFF_atomic_type
a -> TFF_atomic_type -> Sign
signOfTFF_atomic_type TFF_atomic_type
a
  TFFMT_mapping a :: TFF_mapping_type
a -> TFF_mapping_type -> Sign
signOfTFF_mapping_type TFF_mapping_type
a

signOfTFF_unitary_type :: TFF_unitary_type -> Sign
signOfTFF_unitary_type :: TFF_unitary_type -> Sign
signOfTFF_unitary_type x :: TFF_unitary_type
x = case TFF_unitary_type
x of
  TFFUT_atomic a :: TFF_atomic_type
a -> TFF_atomic_type -> Sign
signOfTFF_atomic_type TFF_atomic_type
a
  TFFUT_xprod a :: TFF_xprod_type
a -> TFF_xprod_type -> Sign
signOfTFF_xprod_type TFF_xprod_type
a

signOfTFF_atomic_type :: TFF_atomic_type -> Sign
signOfTFF_atomic_type :: TFF_atomic_type -> Sign
signOfTFF_atomic_type x :: TFF_atomic_type
x = case TFF_atomic_type
x of
  TFFAT_constant a :: Atomic_defined_word
a -> Atomic_defined_word -> Sign
signOfType_constant Atomic_defined_word
a
  TFFAT_defined a :: Defined_type
a -> Defined_type -> Sign
signOfDefined_type Defined_type
a
  TFFAT_functor f :: Atomic_defined_word
f args :: TFF_type_arguments
args ->
    [Sign] -> Sign
signatureUnions [Atomic_defined_word -> Sign
signOfType_functor Atomic_defined_word
f, TFF_type_arguments -> Sign
signOfTFF_type_arguments TFF_type_arguments
args]
  TFFAT_variable a :: Atomic_defined_word
a -> Atomic_defined_word -> Sign
signOfVariable Atomic_defined_word
a

signOfTFF_type_arguments :: TFF_type_arguments -> Sign
signOfTFF_type_arguments :: TFF_type_arguments -> Sign
signOfTFF_type_arguments = [Sign] -> Sign
signatureUnions ([Sign] -> Sign)
-> (TFF_type_arguments -> [Sign]) -> TFF_type_arguments -> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TFF_atomic_type -> Sign) -> TFF_type_arguments -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map TFF_atomic_type -> Sign
signOfTFF_atomic_type

signOfTFF_mapping_type :: TFF_mapping_type -> Sign
signOfTFF_mapping_type :: TFF_mapping_type -> Sign
signOfTFF_mapping_type x :: TFF_mapping_type
x = case TFF_mapping_type
x of
  TFF_mapping_type ut :: TFF_unitary_type
ut at :: TFF_atomic_type
at ->
    [Sign] -> Sign
signatureUnions [TFF_unitary_type -> Sign
signOfTFF_unitary_type TFF_unitary_type
ut, TFF_atomic_type -> Sign
signOfTFF_atomic_type TFF_atomic_type
at]

signOfTFF_xprod_type :: TFF_xprod_type -> Sign
signOfTFF_xprod_type :: TFF_xprod_type -> Sign
signOfTFF_xprod_type x :: TFF_xprod_type
x = case TFF_xprod_type
x of
  TFF_xprod_type ut :: TFF_unitary_type
ut ats :: TFF_type_arguments
ats ->
    [Sign] -> Sign
signatureUnions ([Sign] -> Sign) -> [Sign] -> Sign
forall a b. (a -> b) -> a -> b
$ TFF_unitary_type -> Sign
signOfTFF_unitary_type TFF_unitary_type
ut Sign -> [Sign] -> [Sign]
forall a. a -> [a] -> [a]
: (TFF_atomic_type -> Sign) -> TFF_type_arguments -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map TFF_atomic_type -> Sign
signOfTFF_atomic_type TFF_type_arguments
ats


signOfTCF_formula :: TCF_formula -> Sign
signOfTCF_formula :: TCF_formula -> Sign
signOfTCF_formula x :: TCF_formula
x = case TCF_formula
x of
  TCFF_logic a :: TCF_logic_formula
a -> TCF_logic_formula -> Sign
signOfTCF_logic_formula TCF_logic_formula
a
  TCFF_atom a :: TFF_typed_atom
a -> TFF_typed_atom -> Sign
signOfTFF_typed_atom TFF_typed_atom
a

signOfTCF_logic_formula :: TCF_logic_formula -> Sign
signOfTCF_logic_formula :: TCF_logic_formula -> Sign
signOfTCF_logic_formula x :: TCF_logic_formula
x = case TCF_logic_formula
x of
  TCFLF_quantified a :: TCF_quantified_formula
a -> TCF_quantified_formula -> Sign
signOfTCF_quantified_formula TCF_quantified_formula
a
  TCFLF_cnf a :: CNF_formula
a -> CNF_formula -> Sign
signOfCNF_formula CNF_formula
a

signOfTCF_quantified_formula :: TCF_quantified_formula -> Sign
signOfTCF_quantified_formula :: TCF_quantified_formula -> Sign
signOfTCF_quantified_formula x :: TCF_quantified_formula
x = case TCF_quantified_formula
x of
  TCF_quantified vars :: TFF_variable_list
vars f :: CNF_formula
f ->
    [Sign] -> Sign
signatureUnions [ TFF_variable_list -> Sign
signOfTFF_variable_list TFF_variable_list
vars
                    , CNF_formula -> Sign
signOfCNF_formula CNF_formula
f
                    ]

signOfFOF_formula :: FOF_formula -> Sign
signOfFOF_formula :: TPI_formula -> Sign
signOfFOF_formula x :: TPI_formula
x = case TPI_formula
x of
  FOFF_logic a :: FOF_logic_formula
a -> FOF_logic_formula -> Sign
signOfFOF_logic_formula FOF_logic_formula
a
  FOFF_sequent a :: FOF_sequent
a -> FOF_sequent -> Sign
signOfFOF_sequent FOF_sequent
a

signOfFOF_logic_formula :: FOF_logic_formula -> Sign
signOfFOF_logic_formula :: FOF_logic_formula -> Sign
signOfFOF_logic_formula x :: FOF_logic_formula
x = case FOF_logic_formula
x of
  FOFLF_binary a :: FOF_binary_formula
a -> FOF_binary_formula -> Sign
signOfFOF_binary_formula FOF_binary_formula
a
  FOFLF_unitary a :: FOF_unitary_formula
a -> FOF_unitary_formula -> Sign
signOfFOF_unitary_formula FOF_unitary_formula
a

signOfFOF_binary_formula :: FOF_binary_formula -> Sign
signOfFOF_binary_formula :: FOF_binary_formula -> Sign
signOfFOF_binary_formula x :: FOF_binary_formula
x = case FOF_binary_formula
x of
  FOFBF_nonassoc a :: FOF_binary_nonassoc
a -> FOF_binary_nonassoc -> Sign
signOfFOF_binary_nonassoc FOF_binary_nonassoc
a
  FOFBF_assoc a :: FOF_binary_assoc
a -> FOF_binary_assoc -> Sign
signOfFOF_binary_assoc FOF_binary_assoc
a

signOfFOF_binary_nonassoc :: FOF_binary_nonassoc -> Sign
signOfFOF_binary_nonassoc :: FOF_binary_nonassoc -> Sign
signOfFOF_binary_nonassoc x :: FOF_binary_nonassoc
x = case FOF_binary_nonassoc
x of
  FOF_binary_nonassoc c :: Binary_connective
c f1 :: FOF_unitary_formula
f1 f2 :: FOF_unitary_formula
f2 ->
    [Sign] -> Sign
signatureUnions ([Sign] -> Sign) -> [Sign] -> Sign
forall a b. (a -> b) -> a -> b
$
      Binary_connective -> Sign
signOfBinary_connective Binary_connective
c Sign -> [Sign] -> [Sign]
forall a. a -> [a] -> [a]
: (FOF_unitary_formula -> Sign) -> [FOF_unitary_formula] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map FOF_unitary_formula -> Sign
signOfFOF_unitary_formula [FOF_unitary_formula
f1, FOF_unitary_formula
f2]

signOfFOF_binary_assoc :: FOF_binary_assoc -> Sign
signOfFOF_binary_assoc :: FOF_binary_assoc -> Sign
signOfFOF_binary_assoc x :: FOF_binary_assoc
x = case FOF_binary_assoc
x of
  FOFBA_or a :: [FOF_unitary_formula]
a -> [FOF_unitary_formula] -> Sign
signOfFOF_or_formula [FOF_unitary_formula]
a
  FOFBA_and a :: [FOF_unitary_formula]
a -> [FOF_unitary_formula] -> Sign
signOfFOF_and_formula [FOF_unitary_formula]
a

signOfFOF_or_formula :: FOF_or_formula -> Sign
signOfFOF_or_formula :: [FOF_unitary_formula] -> Sign
signOfFOF_or_formula = [Sign] -> Sign
signatureUnions ([Sign] -> Sign)
-> ([FOF_unitary_formula] -> [Sign])
-> [FOF_unitary_formula]
-> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FOF_unitary_formula -> Sign) -> [FOF_unitary_formula] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map FOF_unitary_formula -> Sign
signOfFOF_unitary_formula

signOfFOF_and_formula :: FOF_and_formula -> Sign
signOfFOF_and_formula :: [FOF_unitary_formula] -> Sign
signOfFOF_and_formula = [Sign] -> Sign
signatureUnions ([Sign] -> Sign)
-> ([FOF_unitary_formula] -> [Sign])
-> [FOF_unitary_formula]
-> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FOF_unitary_formula -> Sign) -> [FOF_unitary_formula] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map FOF_unitary_formula -> Sign
signOfFOF_unitary_formula

signOfFOF_unitary_formula :: FOF_unitary_formula -> Sign
signOfFOF_unitary_formula :: FOF_unitary_formula -> Sign
signOfFOF_unitary_formula x :: FOF_unitary_formula
x = case FOF_unitary_formula
x of
  FOFUF_quantified a :: FOF_quantified_formula
a -> FOF_quantified_formula -> Sign
signOfFOF_quantified_formula FOF_quantified_formula
a
  FOFUF_unary a :: FOF_unary_formula
a -> FOF_unary_formula -> Sign
signOfFOF_unary_formula FOF_unary_formula
a
  FOFUF_atomic a :: TFF_atomic_formula
a -> TFF_atomic_formula -> Sign
signOfFOF_atomic_formula TFF_atomic_formula
a
  FOFUF_logic a :: FOF_logic_formula
a -> FOF_logic_formula -> Sign
signOfFOF_logic_formula FOF_logic_formula
a

signOfFOF_quantified_formula :: FOF_quantified_formula -> Sign
signOfFOF_quantified_formula :: FOF_quantified_formula -> Sign
signOfFOF_quantified_formula x :: FOF_quantified_formula
x = case FOF_quantified_formula
x of
  FOF_quantified_formula q :: FOF_quantifier
q vars :: FOF_variable_list
vars f :: FOF_unitary_formula
f ->
    [Sign] -> Sign
signatureUnions [ FOF_quantifier -> Sign
signOfFOF_quantifier FOF_quantifier
q
                    , FOF_variable_list -> Sign
signOfFOF_variable_list FOF_variable_list
vars
                    , FOF_unitary_formula -> Sign
signOfFOF_unitary_formula FOF_unitary_formula
f
                    ]

signOfFOF_variable_list :: FOF_variable_list -> Sign
signOfFOF_variable_list :: FOF_variable_list -> Sign
signOfFOF_variable_list = [Sign] -> Sign
signatureUnions ([Sign] -> Sign)
-> (FOF_variable_list -> [Sign]) -> FOF_variable_list -> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Atomic_defined_word -> Sign) -> FOF_variable_list -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map Atomic_defined_word -> Sign
signOfVariable

signOfFOF_unary_formula :: FOF_unary_formula -> Sign
signOfFOF_unary_formula :: FOF_unary_formula -> Sign
signOfFOF_unary_formula x :: FOF_unary_formula
x = case FOF_unary_formula
x of
  FOFUF_connective c :: Unary_connective
c f :: FOF_unitary_formula
f ->
    [Sign] -> Sign
signatureUnions [Unary_connective -> Sign
signOfUnary_connective Unary_connective
c, FOF_unitary_formula -> Sign
signOfFOF_unitary_formula FOF_unitary_formula
f]
  FOFUF_infix a :: FOF_infix_unary
a -> FOF_infix_unary -> Sign
signOfFOF_infix_unary FOF_infix_unary
a

signOfFOF_infix_unary :: FOF_infix_unary -> Sign
signOfFOF_infix_unary :: FOF_infix_unary -> Sign
signOfFOF_infix_unary x :: FOF_infix_unary
x = case FOF_infix_unary
x of
  FOF_infix_unary t1 :: FOF_term
t1 t2 :: FOF_term
t2 ->
    [Sign] -> Sign
signatureUnions ([Sign] -> Sign) -> [Sign] -> Sign
forall a b. (a -> b) -> a -> b
$ (FOF_term -> Sign) -> FOF_arguments -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map FOF_term -> Sign
signOfFOF_term [FOF_term
t1, FOF_term
t2]

signOfFOF_atomic_formula :: FOF_atomic_formula -> Sign
signOfFOF_atomic_formula :: TFF_atomic_formula -> Sign
signOfFOF_atomic_formula x :: TFF_atomic_formula
x = case TFF_atomic_formula
x of
  FOFAT_plain a :: FOF_plain_atomic_formula
a -> FOF_plain_atomic_formula -> Sign
signOfFOF_plain_atomic_formula FOF_plain_atomic_formula
a
  FOFAT_defined a :: FOF_defined_atomic_formula
a -> FOF_defined_atomic_formula -> Sign
signOfFOF_defined_atomic_formula FOF_defined_atomic_formula
a
  FOFAT_system a :: FOF_system_atomic_formula
a -> FOF_system_atomic_formula -> Sign
signOfFOF_system_atomic_formula FOF_system_atomic_formula
a

signOfFOF_plain_atomic_formula :: FOF_plain_atomic_formula -> Sign
signOfFOF_plain_atomic_formula :: FOF_plain_atomic_formula -> Sign
signOfFOF_plain_atomic_formula x :: FOF_plain_atomic_formula
x = case FOF_plain_atomic_formula
x of
  FOFPAF_proposition a :: Atomic_defined_word
a -> Atomic_defined_word -> Sign
signOfProposition Atomic_defined_word
a
  FOFPAF_predicate p :: Atomic_defined_word
p args :: FOF_arguments
args ->
    [Sign] -> Sign
signatureUnions [Atomic_defined_word -> Int -> Sign
signOfPredicate Atomic_defined_word
p (Int -> Sign) -> Int -> Sign
forall a b. (a -> b) -> a -> b
$ FOF_arguments -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length FOF_arguments
args, FOF_arguments -> Sign
signOfFOF_arguments FOF_arguments
args]

signOfFOF_defined_atomic_formula :: FOF_defined_atomic_formula -> Sign
signOfFOF_defined_atomic_formula :: FOF_defined_atomic_formula -> Sign
signOfFOF_defined_atomic_formula x :: FOF_defined_atomic_formula
x = case FOF_defined_atomic_formula
x of
  FOFDAF_plain a :: FOF_defined_plain_formula
a -> FOF_defined_plain_formula -> Sign
signOfFOF_defined_plain_formula FOF_defined_plain_formula
a
  FOFDAF_infix a :: FOF_defined_infix_formula
a -> FOF_defined_infix_formula -> Sign
signOfFOF_defined_infix_formula FOF_defined_infix_formula
a

signOfFOF_defined_plain_formula :: FOF_defined_plain_formula -> Sign
signOfFOF_defined_plain_formula :: FOF_defined_plain_formula -> Sign
signOfFOF_defined_plain_formula x :: FOF_defined_plain_formula
x = case FOF_defined_plain_formula
x of
  FOFDPF_proposition a :: Defined_proposition
a -> Defined_proposition -> Sign
signOfDefined_proposition Defined_proposition
a
  FOFDPF_predicate p :: Defined_predicate
p args :: FOF_arguments
args ->
    [Sign] -> Sign
signatureUnions [Defined_predicate -> Sign
signOfDefined_predicate Defined_predicate
p, FOF_arguments -> Sign
signOfFOF_arguments FOF_arguments
args]

signOfFOF_defined_infix_formula :: FOF_defined_infix_formula -> Sign
signOfFOF_defined_infix_formula :: FOF_defined_infix_formula -> Sign
signOfFOF_defined_infix_formula x :: FOF_defined_infix_formula
x = case FOF_defined_infix_formula
x of
  FOF_defined_infix_formula dip :: Defined_infix_pred
dip t1 :: FOF_term
t1 t2 :: FOF_term
t2 -> [Sign] -> Sign
signatureUnions
    [FOF_term -> Sign
signOfFOF_term FOF_term
t1, Defined_infix_pred -> Sign
signOfDefined_infix_pred Defined_infix_pred
dip, FOF_term -> Sign
signOfFOF_term FOF_term
t2]

signOfFOF_system_atomic_formula :: FOF_system_atomic_formula -> Sign
signOfFOF_system_atomic_formula :: FOF_system_atomic_formula -> Sign
signOfFOF_system_atomic_formula x :: FOF_system_atomic_formula
x = case FOF_system_atomic_formula
x of
  FOF_system_atomic_formula a :: FOF_system_term
a -> FOF_system_term -> Sign
signOfFOF_system_term FOF_system_term
a

signOfFOF_plain_term :: FOF_plain_term -> Sign
signOfFOF_plain_term :: FOF_plain_term -> Sign
signOfFOF_plain_term x :: FOF_plain_term
x = case FOF_plain_term
x of
  FOFPT_constant a :: Atomic_defined_word
a -> Atomic_defined_word -> Sign
signOfConstant Atomic_defined_word
a
  FOFPT_functor f :: Atomic_defined_word
f args :: FOF_arguments
args ->
    [Sign] -> Sign
signatureUnions [ Atomic_defined_word -> Int -> Sign
signOfTPTP_functor Atomic_defined_word
f (Int -> Sign) -> Int -> Sign
forall a b. (a -> b) -> a -> b
$ FOF_arguments -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length FOF_arguments
args
                    , FOF_arguments -> Sign
signOfFOF_arguments FOF_arguments
args]

signOfFOF_defined_term :: FOF_defined_term -> Sign
signOfFOF_defined_term :: FOF_defined_term -> Sign
signOfFOF_defined_term x :: FOF_defined_term
x = case FOF_defined_term
x of
  FOFDT_term a :: Defined_term
a -> Defined_term -> Sign
signOfDefined_term Defined_term
a
  FOFDT_atomic a :: FOF_defined_atomic_term
a -> FOF_defined_atomic_term -> Sign
signOfFOF_defined_atomic_term FOF_defined_atomic_term
a

signOfFOF_defined_atomic_term :: FOF_defined_atomic_term -> Sign
signOfFOF_defined_atomic_term :: FOF_defined_atomic_term -> Sign
signOfFOF_defined_atomic_term x :: FOF_defined_atomic_term
x = case FOF_defined_atomic_term
x of
  FOFDAT_plain a :: FOF_defined_plain_term
a -> FOF_defined_plain_term -> Sign
signOfFOF_defined_plain_term FOF_defined_plain_term
a
  --  | FOFDAT_indix a -> signOfDefined_infix_term a

signOfFOF_defined_plain_term :: FOF_defined_plain_term -> Sign
signOfFOF_defined_plain_term :: FOF_defined_plain_term -> Sign
signOfFOF_defined_plain_term x :: FOF_defined_plain_term
x = case FOF_defined_plain_term
x of
  FOFDPT_constant a :: Defined_functor
a -> Defined_functor -> Sign
signOfDefined_constant Defined_functor
a
  FOFDPT_functor f :: Defined_functor
f args :: FOF_arguments
args ->
    [Sign] -> Sign
signatureUnions [Defined_functor -> Sign
signOfDefined_functor Defined_functor
f, FOF_arguments -> Sign
signOfFOF_arguments FOF_arguments
args]

signOfFOF_system_term :: FOF_system_term -> Sign
signOfFOF_system_term :: FOF_system_term -> Sign
signOfFOF_system_term x :: FOF_system_term
x = case FOF_system_term
x of
  FOFST_constant a :: Atomic_defined_word
a -> Atomic_defined_word -> Sign
signOfSystem_constant Atomic_defined_word
a
  FOFST_functor f :: Atomic_defined_word
f args :: FOF_arguments
args ->
    [Sign] -> Sign
signatureUnions [Atomic_defined_word -> Sign
signOfSystem_functor Atomic_defined_word
f, FOF_arguments -> Sign
signOfFOF_arguments FOF_arguments
args]

signOfFOF_arguments :: FOF_arguments -> Sign
signOfFOF_arguments :: FOF_arguments -> Sign
signOfFOF_arguments = [Sign] -> Sign
signatureUnions ([Sign] -> Sign)
-> (FOF_arguments -> [Sign]) -> FOF_arguments -> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FOF_term -> Sign) -> FOF_arguments -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map FOF_term -> Sign
signOfFOF_term

signOfFOF_term :: FOF_term -> Sign
signOfFOF_term :: FOF_term -> Sign
signOfFOF_term x :: FOF_term
x = case FOF_term
x of
  FOFT_function a :: FOF_function_term
a -> FOF_function_term -> Sign
signOfFOF_function_term FOF_function_term
a
  FOFT_variable a :: Atomic_defined_word
a -> Atomic_defined_word -> Sign
signOfVariable Atomic_defined_word
a
  FOFT_conditional a :: TFF_conditional_term
a -> TFF_conditional_term -> Sign
signOfTFF_conditional_term TFF_conditional_term
a
  FOFT_let a :: TFF_let_term
a -> TFF_let_term -> Sign
signOfTFF_let_term TFF_let_term
a

signOfFOF_function_term :: FOF_function_term -> Sign
signOfFOF_function_term :: FOF_function_term -> Sign
signOfFOF_function_term x :: FOF_function_term
x = case FOF_function_term
x of
  FOFFT_plain a :: FOF_plain_term
a -> FOF_plain_term -> Sign
signOfFOF_plain_term FOF_plain_term
a
  FOFFT_defined a :: FOF_defined_term
a -> FOF_defined_term -> Sign
signOfFOF_defined_term FOF_defined_term
a
  FOFFT_system a :: FOF_system_term
a -> FOF_system_term -> Sign
signOfFOF_system_term FOF_system_term
a

signOfTFF_conditional_term :: TFF_conditional_term -> Sign
signOfTFF_conditional_term :: TFF_conditional_term -> Sign
signOfTFF_conditional_term x :: TFF_conditional_term
x = case TFF_conditional_term
x of
  TFF_conditional_term f_if :: TFF_logic_formula
f_if t_then :: FOF_term
t_then t_else :: FOF_term
t_else ->
    [Sign] -> Sign
signatureUnions ([Sign] -> Sign) -> [Sign] -> Sign
forall a b. (a -> b) -> a -> b
$
      TFF_logic_formula -> Sign
signOfTFF_logic_formula TFF_logic_formula
f_if Sign -> [Sign] -> [Sign]
forall a. a -> [a] -> [a]
: (FOF_term -> Sign) -> FOF_arguments -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map FOF_term -> Sign
signOfFOF_term [FOF_term
t_then, FOF_term
t_else]

signOfTFF_let_term :: TFF_let_term -> Sign
signOfTFF_let_term :: TFF_let_term -> Sign
signOfTFF_let_term x :: TFF_let_term
x = case TFF_let_term
x of
  TFFLT_formula defns :: TFF_let_formula_defns
defns t :: FOF_term
t ->
    [Sign] -> Sign
signatureUnions [TFF_let_formula_defns -> Sign
signOfTFF_let_formula_defns TFF_let_formula_defns
defns, FOF_term -> Sign
signOfFOF_term FOF_term
t]
  TFFLT_term defns :: TFF_let_term_defns
defns t :: FOF_term
t ->
    [Sign] -> Sign
signatureUnions [TFF_let_term_defns -> Sign
signOfTFF_let_term_defns TFF_let_term_defns
defns, FOF_term -> Sign
signOfFOF_term FOF_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 :: FOF_sequent -> Sign
signOfFOF_sequent x :: FOF_sequent
x = case FOF_sequent
x of
  FOFS_plain t1 :: FOF_formula_tuple
t1 t2 :: FOF_formula_tuple
t2 ->
    [Sign] -> Sign
signatureUnions ([Sign] -> Sign) -> [Sign] -> Sign
forall a b. (a -> b) -> a -> b
$ (FOF_formula_tuple -> Sign) -> [FOF_formula_tuple] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map FOF_formula_tuple -> Sign
signOfFOF_formula_tuple [FOF_formula_tuple
t1, FOF_formula_tuple
t2]
  FOFS_parens a :: FOF_sequent
a -> FOF_sequent -> Sign
signOfFOF_sequent FOF_sequent
a

signOfFOF_formula_tuple :: FOF_formula_tuple -> Sign
signOfFOF_formula_tuple :: FOF_formula_tuple -> Sign
signOfFOF_formula_tuple x :: FOF_formula_tuple
x = case FOF_formula_tuple
x of
  FOF_formula_tuple a :: FOF_formula_tuple_list
a -> FOF_formula_tuple_list -> Sign
signOfFOF_formula_tuple_list FOF_formula_tuple_list
a

signOfFOF_formula_tuple_list :: FOF_formula_tuple_list -> Sign
signOfFOF_formula_tuple_list :: FOF_formula_tuple_list -> Sign
signOfFOF_formula_tuple_list = [Sign] -> Sign
signatureUnions ([Sign] -> Sign)
-> (FOF_formula_tuple_list -> [Sign])
-> FOF_formula_tuple_list
-> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FOF_logic_formula -> Sign) -> FOF_formula_tuple_list -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map FOF_logic_formula -> Sign
signOfFOF_logic_formula


signOfCNF_formula :: CNF_formula -> Sign
signOfCNF_formula :: CNF_formula -> Sign
signOfCNF_formula x :: CNF_formula
x = case CNF_formula
x of
  CNFF_plain a :: Disjunction
a -> Disjunction -> Sign
signOfDisjunction Disjunction
a
  CNFF_parens a :: Disjunction
a -> Disjunction -> Sign
signOfDisjunction Disjunction
a

signOfDisjunction :: Disjunction -> Sign
signOfDisjunction :: Disjunction -> Sign
signOfDisjunction x :: Disjunction
x = case Disjunction
x of
  Disjunction ls :: [Literal]
ls -> [Sign] -> Sign
signatureUnions ([Sign] -> Sign) -> [Sign] -> Sign
forall a b. (a -> b) -> a -> b
$ (Literal -> Sign) -> [Literal] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map Literal -> Sign
signOfLiteral [Literal]
ls

signOfLiteral :: Literal -> Sign
signOfLiteral :: Literal -> Sign
signOfLiteral x :: Literal
x = case Literal
x of
  Lit_atomic a :: TFF_atomic_formula
a -> TFF_atomic_formula -> Sign
signOfFOF_atomic_formula TFF_atomic_formula
a
  Lit_negative a :: TFF_atomic_formula
a -> TFF_atomic_formula -> Sign
signOfFOF_atomic_formula TFF_atomic_formula
a
  Lit_fof_infix a :: FOF_infix_unary
a -> FOF_infix_unary -> Sign
signOfFOF_infix_unary FOF_infix_unary
a

signOfTHF_quantifier :: THF_quantifier -> Sign
signOfTHF_quantifier :: THF_quantifier -> Sign
signOfTHF_quantifier x :: THF_quantifier
x = case THF_quantifier
x of
  THFQ_fof a :: FOF_quantifier
a -> FOF_quantifier -> Sign
signOfFOF_quantifier FOF_quantifier
a
  THFQ_th0 a :: TH0_quantifier
a -> TH0_quantifier -> Sign
signOfTH0_quantifier TH0_quantifier
a
  THFQ_th1 a :: TH1_quantifier
a -> TH1_quantifier -> Sign
signOfTH1_quantifier TH1_quantifier
a


signOfTH1_quantifier :: TH1_quantifier -> Sign
signOfTH1_quantifier :: TH1_quantifier -> Sign
signOfTH1_quantifier x :: TH1_quantifier
x = case TH1_quantifier
x of
  TH1_DependentProduct -> Sign
emptySign
  TH1_DependentSum -> Sign
emptySign

signOfTH0_quantifier :: TH0_quantifier -> Sign
signOfTH0_quantifier :: TH0_quantifier -> Sign
signOfTH0_quantifier x :: TH0_quantifier
x = case TH0_quantifier
x of
  TH0_LambdaBinder -> Sign
emptySign
  TH0_IndefiniteDescription -> Sign
emptySign
  TH0_DefiniteDescription -> Sign
emptySign

signOfTHF_pair_connective :: THF_pair_connective -> Sign
signOfTHF_pair_connective :: THF_pair_connective -> Sign
signOfTHF_pair_connective x :: THF_pair_connective
x = case THF_pair_connective
x of
  THF_infix_equality -> Sign
emptySign
  Infix_inequality -> Sign
emptySign
  THFPC_binary a :: Binary_connective
a -> Binary_connective -> Sign
signOfBinary_connective Binary_connective
a
  THF_assignment -> Sign
emptySign

signOfTHF_unary_connective :: THF_unary_connective -> Sign
signOfTHF_unary_connective :: THF_unary_connective -> Sign
signOfTHF_unary_connective x :: THF_unary_connective
x = case THF_unary_connective
x of
  THFUC_unary a :: Unary_connective
a -> Unary_connective -> Sign
signOfUnary_connective Unary_connective
a
  THFUC_th1 a :: TH1_unary_connective
a -> TH1_unary_connective -> Sign
signOfTH1_unary_connective TH1_unary_connective
a

signOfTH1_unary_connective :: TH1_unary_connective -> Sign
signOfTH1_unary_connective :: TH1_unary_connective -> Sign
signOfTH1_unary_connective x :: TH1_unary_connective
x = case TH1_unary_connective
x of
  TH1_PiForAll -> Sign
emptySign
  TH1_PiSigmaExists -> Sign
emptySign
  TH1_PiIndefiniteDescription -> Sign
emptySign
  TH1_PiDefiniteDescription -> Sign
emptySign
  TH1_PiEquality -> Sign
emptySign

signOfFOF_quantifier :: FOF_quantifier -> Sign
signOfFOF_quantifier :: FOF_quantifier -> Sign
signOfFOF_quantifier x :: FOF_quantifier
x = case FOF_quantifier
x of
  ForAll -> Sign
emptySign
  Exists -> Sign
emptySign

signOfBinary_connective :: Binary_connective -> Sign
signOfBinary_connective :: Binary_connective -> Sign
signOfBinary_connective x :: Binary_connective
x = case Binary_connective
x of
  Equivalence -> Sign
emptySign
  Implication -> Sign
emptySign
  ReverseImplication -> Sign
emptySign
  XOR -> Sign
emptySign
  NOR -> Sign
emptySign
  NAND -> Sign
emptySign

signOfAssoc_connective :: Assoc_connective -> Sign
signOfAssoc_connective :: Assoc_connective -> Sign
signOfAssoc_connective x :: Assoc_connective
x = case Assoc_connective
x of
  OR -> Sign
emptySign
  AND -> Sign
emptySign

signOfUnary_connective :: Unary_connective -> Sign
signOfUnary_connective :: Unary_connective -> Sign
signOfUnary_connective x :: Unary_connective
x = case Unary_connective
x of
  NOT -> Sign
emptySign

signOfType_constant :: Type_constant -> Sign
signOfType_constant :: Atomic_defined_word -> Sign
signOfType_constant _ = Sign
emptySign -- Handled by thfTypeConstantMap and tffTypeConstantMap

signOfType_functor :: Type_functor -> Sign
signOfType_functor :: Atomic_defined_word -> Sign
signOfType_functor _ = Sign
emptySign -- Handled by thfTypeFunctorMap and tffTypeFunctorMap

signOfDefined_type :: Defined_type -> Sign
signOfDefined_type :: Defined_type -> Sign
signOfDefined_type x :: Defined_type
x = case Defined_type
x of
  OType -> Sign
emptySign
  O -> Sign
emptySign
  IType -> Sign
emptySign
  I -> Sign
emptySign
  TType -> Sign
emptySign
  Real -> Sign
emptySign
  Rat -> Sign
emptySign
  Int -> Sign
emptySign

signOfAtom :: Atom -> Sign
signOfAtom :: Atom -> Sign
signOfAtom x :: Atom
x = case Atom
x of
  Atom_untyped a :: Untyped_atom
a -> Untyped_atom -> Sign
signOfUntyped_atom Untyped_atom
a
  Atom_constant a :: Defined_functor
a -> Defined_functor -> Sign
signOfDefined_constant Defined_functor
a

signOfUntyped_atom :: Untyped_atom -> Sign
signOfUntyped_atom :: Untyped_atom -> Sign
signOfUntyped_atom x :: Untyped_atom
x = case Untyped_atom
x of
  UA_constant a :: Atomic_defined_word
a -> Atomic_defined_word -> Sign
signOfConstant Atomic_defined_word
a
  UA_system a :: Atomic_defined_word
a -> Atomic_defined_word -> Sign
signOfSystem_constant Atomic_defined_word
a

signOfProposition :: Proposition -> Sign
signOfProposition :: Atomic_defined_word -> Sign
signOfProposition a :: Atomic_defined_word
a = Sign
emptySign { propositionSet :: ConstantSet
propositionSet = Atomic_defined_word -> ConstantSet
forall a. a -> Set a
Set.singleton Atomic_defined_word
a }

signOfPredicate :: Predicate -> Int -> Sign
signOfPredicate :: Atomic_defined_word -> Int -> Sign
signOfPredicate a :: Atomic_defined_word
a arity :: Int
arity =
  Sign
emptySign { fofPredicateMap :: FOFPredicateMap
fofPredicateMap = Atomic_defined_word -> Set Int -> FOFPredicateMap
forall k a. k -> a -> Map k a
Map.singleton Atomic_defined_word
a (Set Int -> FOFPredicateMap) -> Set Int -> FOFPredicateMap
forall a b. (a -> b) -> a -> b
$ Int -> Set Int
forall a. a -> Set a
Set.singleton Int
arity }

signOfDefined_proposition :: Defined_proposition -> Sign
signOfDefined_proposition :: Defined_proposition -> Sign
signOfDefined_proposition x :: Defined_proposition
x = case Defined_proposition
x of
  TPTP_true -> Sign
emptySign
  TPTP_false -> Sign
emptySign

signOfDefined_predicate :: Defined_predicate -> Sign
signOfDefined_predicate :: Defined_predicate -> Sign
signOfDefined_predicate x :: Defined_predicate
x = case Defined_predicate
x of
  Distinct -> Sign
emptySign
  Less -> Sign
emptySign
  Lesseq -> Sign
emptySign
  Greater -> Sign
emptySign
  Greatereq -> Sign
emptySign
  Is_int -> Sign
emptySign
  Is_rat -> Sign
emptySign
  Box_P -> Sign
emptySign
  Box_i -> Sign
emptySign
  Box_int -> Sign
emptySign
  Box -> Sign
emptySign
  Dia_P -> Sign
emptySign
  Dia_i -> Sign
emptySign
  Dia_int -> Sign
emptySign
  Dia -> Sign
emptySign

signOfDefined_infix_pred :: Defined_infix_pred -> Sign
signOfDefined_infix_pred :: Defined_infix_pred -> Sign
signOfDefined_infix_pred x :: Defined_infix_pred
x = case Defined_infix_pred
x of
  Defined_infix_equality -> Sign
emptySign
  Defined_assignment -> Sign
emptySign

signOfConstant :: Constant -> Sign
signOfConstant :: Atomic_defined_word -> Sign
signOfConstant a :: Atomic_defined_word
a = Sign
emptySign { constantSet :: ConstantSet
constantSet = Atomic_defined_word -> ConstantSet
forall a. a -> Set a
Set.singleton Atomic_defined_word
a }

signOfTPTP_functor :: TPTP_functor -> Int -> Sign
signOfTPTP_functor :: Atomic_defined_word -> Int -> Sign
signOfTPTP_functor a :: Atomic_defined_word
a arity :: Int
arity =
  Sign
emptySign { fofFunctorMap :: FOFPredicateMap
fofFunctorMap = Atomic_defined_word -> Set Int -> FOFPredicateMap
forall k a. k -> a -> Map k a
Map.singleton Atomic_defined_word
a (Set Int -> FOFPredicateMap) -> Set Int -> FOFPredicateMap
forall a b. (a -> b) -> a -> b
$ Int -> Set Int
forall a. a -> Set a
Set.singleton Int
arity }

signOfSystem_constant :: System_constant -> Sign
signOfSystem_constant :: Atomic_defined_word -> Sign
signOfSystem_constant _ = Sign
emptySign

signOfSystem_functor :: System_functor -> Sign
signOfSystem_functor :: Atomic_defined_word -> Sign
signOfSystem_functor _ = Sign
emptySign

signOfDefined_constant :: Defined_constant -> Sign
signOfDefined_constant :: Defined_functor -> Sign
signOfDefined_constant _ = Sign
emptySign

signOfDefined_functor :: Defined_functor -> Sign
signOfDefined_functor :: Defined_functor -> Sign
signOfDefined_functor x :: Defined_functor
x = case Defined_functor
x of
  Uminus -> Sign
emptySign
  Sum -> Sign
emptySign
  Difference -> Sign
emptySign
  Product -> Sign
emptySign
  Quotient -> Sign
emptySign
  Quotient_e -> Sign
emptySign
  Quotient_t -> Sign
emptySign
  Quotient_f -> Sign
emptySign
  Remainder_e -> Sign
emptySign
  Remainder_t -> Sign
emptySign
  Remainder_f -> Sign
emptySign
  Floor -> Sign
emptySign
  Ceiling -> Sign
emptySign
  Truncate -> Sign
emptySign
  Round -> Sign
emptySign
  To_int -> Sign
emptySign
  To_rat -> Sign
emptySign
  To_real -> Sign
emptySign
  DF_atomic_defined_word _ -> Sign
emptySign

signOfDefined_term :: Defined_term -> Sign
signOfDefined_term :: Defined_term -> Sign
signOfDefined_term x :: Defined_term
x = case Defined_term
x of
  DT_number a :: Number
a -> Number -> Sign
signOfNumber Number
a
  DT_object a :: Atomic_defined_word
a -> Atomic_defined_word -> Sign
signOfDistinct_object Atomic_defined_word
a

signOfVariable :: Variable -> Sign
signOfVariable :: Atomic_defined_word -> Sign
signOfVariable _ = Sign
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 :: Number -> Sign
signOfNumber a :: Number
a = Sign
emptySign { numberSet :: NumberSet
numberSet = Number -> NumberSet
forall a. a -> Set a
Set.singleton Number
a }

signOfDistinct_object :: Distinct_object -> Sign
signOfDistinct_object :: Atomic_defined_word -> Sign
signOfDistinct_object _ = Sign
emptySign

-- signOfFile_name :: File_name -> Sign
-- signOfFile_name _ = emptySign

nameS :: Annotated_formula -> String
nameS :: Sentence -> String
nameS f :: Sentence
f = case Sentence -> Name
name Sentence
f of
  NameString s :: Atomic_defined_word
s -> Atomic_defined_word -> String
tokStr Atomic_defined_word
s
  NameInteger i :: Integer
i -> Integer -> String
forall a. Show a => a -> String
show Integer
i