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'
}
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
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
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]
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
signOfType_functor :: Type_functor -> Sign
signOfType_functor :: Atomic_defined_word -> Sign
signOfType_functor _ = Sign
emptySign
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
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
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