{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances, ScopedTypeVariables #-}
{- |
Module      :  ./Comorphisms/SuleCFOL2TPTP.hs
Description :  Coding of a CASL subset into TPTP
Copyright   :  (c) Eugen Kuksa and Till Mossakowksi
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  kuksa@iks.cs.ovgu.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

The translating comorphism from a CASL subset to TPTP.
-}

module Comorphisms.SuleCFOL2TPTP
  ( suleCFOL2TPTP
  ) where

import Logic.Logic as Logic
import Logic.Comorphism

import Common.AS_Annotation hiding (sentence)
import qualified Common.AS_Annotation as AS_Annotation (sentence)
import Common.Id
import Common.Result
import Common.ProofTree
import qualified Common.Lib.Rel as Rel
import qualified Common.Lib.MapSet as MapSet
import qualified Control.Monad.Fail as Fail

import qualified Data.Map as Map
import qualified Data.Set as Set

import Data.List as List hiding (sort)
import Data.Char
import Numeric (showHex)

import CASL.Logic_CASL
import CASL.AS_Basic_CASL as CAS
import CASL.Sublogic as SL
import CASL.Sign as CSign hiding (sentences)
import CASL.Morphism
import CASL.Overload
import CASL.Utils
import CASL.ToDoc

import TPTP.AS as TAS hiding (name)
import TPTP.Morphism as TMorphism
import TPTP.Sign as TSign
import TPTP.Logic_TPTP
import TPTP.Sublogic

data TPTP_FOF = TPTP_FOF

instance Show TPTP_FOF where
  show :: TPTP_FOF -> String
show TPTP_FOF = "TPTP_FOF"

-- | The identity of the comorphisms
data GenSuleCFOL2TPTP = GenSuleCFOL2TPTP deriving Int -> GenSuleCFOL2TPTP -> ShowS
[GenSuleCFOL2TPTP] -> ShowS
GenSuleCFOL2TPTP -> String
(Int -> GenSuleCFOL2TPTP -> ShowS)
-> (GenSuleCFOL2TPTP -> String)
-> ([GenSuleCFOL2TPTP] -> ShowS)
-> Show GenSuleCFOL2TPTP
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GenSuleCFOL2TPTP] -> ShowS
$cshowList :: [GenSuleCFOL2TPTP] -> ShowS
show :: GenSuleCFOL2TPTP -> String
$cshow :: GenSuleCFOL2TPTP -> String
showsPrec :: Int -> GenSuleCFOL2TPTP -> ShowS
$cshowsPrec :: Int -> GenSuleCFOL2TPTP -> ShowS
Show

suleCFOL2TPTP :: GenSuleCFOL2TPTP
suleCFOL2TPTP :: GenSuleCFOL2TPTP
suleCFOL2TPTP = GenSuleCFOL2TPTP
GenSuleCFOL2TPTP

-- | TPTP theories
type TPTPTheory = (TSign.Sign, [Named Sentence])

instance Language GenSuleCFOL2TPTP where
  language_name :: GenSuleCFOL2TPTP -> String
language_name GenSuleCFOL2TPTP = "CASL2TPTP_FOF"

instance Comorphism GenSuleCFOL2TPTP
               CASL CASL_Sublogics
               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CASLSign
               CASLMor
               CSign.Symbol RawSymbol ProofTree
               TPTP.Logic_TPTP.TPTP Sublogic TAS.BASIC_SPEC Sentence () ()
               TSign.Sign TMorphism.Morphism TSign.Symbol () ProofTree where
    sourceLogic :: GenSuleCFOL2TPTP -> CASL
sourceLogic GenSuleCFOL2TPTP = CASL
CASL
    sourceSublogic :: GenSuleCFOL2TPTP -> CASL_Sublogics
sourceSublogic GenSuleCFOL2TPTP = CASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.cFol
                       { sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures
LocFilSub
                      , cons_features :: SortGenerationFeatures
cons_features = SortGenerationFeatures
emptyMapConsFeature
                       , has_empty_sorts :: Bool
has_empty_sorts = Bool
True }
    sourceSublogicLossy :: GenSuleCFOL2TPTP -> CASL_Sublogics
sourceSublogicLossy GenSuleCFOL2TPTP = CASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.fol
                      { sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures
LocFilSub
                      , has_empty_sorts :: Bool
has_empty_sorts = Bool
True }
    targetLogic :: GenSuleCFOL2TPTP -> TPTP
targetLogic GenSuleCFOL2TPTP = TPTP
TPTP.Logic_TPTP.TPTP
    mapSublogic :: GenSuleCFOL2TPTP -> CASL_Sublogics -> Maybe Sublogic
mapSublogic _ _ = Sublogic -> Maybe Sublogic
forall a. a -> Maybe a
Just Sublogic
FOF
    map_theory :: GenSuleCFOL2TPTP
-> (CASLSign, [Named CASLFORMULA])
-> Result (Sign, [Named Sentence])
map_theory GenSuleCFOL2TPTP = (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Sentence])
forall f e.
(FormExtension f, Eq f) =>
(Sign f e, [Named (FORMULA f)]) -> Result (Sign, [Named Sentence])
transTheory
    has_model_expansion :: GenSuleCFOL2TPTP -> Bool
has_model_expansion GenSuleCFOL2TPTP = Bool
True

transTheory :: (FormExtension f, Eq f)
            => (CSign.Sign f e, [Named (FORMULA f)])
            -> Result TPTPTheory
transTheory :: (Sign f e, [Named (FORMULA f)]) -> Result (Sign, [Named Sentence])
transTheory (sign :: Sign f e
sign, sens :: [Named (FORMULA f)]
sens) = do
  let signWithRenamings :: (Sign f e, Map (OP_NAME, OpType) OP_NAME,
 Map (OP_NAME, PredType) OP_NAME)
signWithRenamings@(preparedSign :: Sign f e
preparedSign, _, _) = Sign f e
-> (Sign f e, Map (OP_NAME, OpType) OP_NAME,
    Map (OP_NAME, PredType) OP_NAME)
forall f e.
(FormExtension f, Eq f) =>
Sign f e -> SignWithRenamings f e
prepareSign Sign f e
sign
  let preparedSens :: [Named (FORMULA f)]
preparedSens = (Named (FORMULA f) -> Named (FORMULA f))
-> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map Named (FORMULA f) -> Named (FORMULA f)
forall f.
(FormExtension f, Eq f) =>
Named (FORMULA f) -> Named (FORMULA f)
prepareNamedFormula [Named (FORMULA f)]
sens
  (tptpSign :: Sign
tptpSign, signSentences :: [Named Sentence]
signSentences) <- Sign f e -> Result (Sign, [Named Sentence])
forall f e.
(FormExtension f, Eq f) =>
Sign f e -> Result (Sign, [Named Sentence])
translateSign Sign f e
preparedSign
  [Named Sentence]
translatedSentences <- (Named (FORMULA f) -> Result (Named Sentence))
-> [Named (FORMULA f)] -> Result [Named Sentence]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Sign f e, Map (OP_NAME, OpType) OP_NAME,
 Map (OP_NAME, PredType) OP_NAME)
-> Named (FORMULA f) -> Result (Named Sentence)
forall f e.
(FormExtension f, Eq f) =>
SignWithRenamings f e
-> Named (FORMULA f) -> Result (Named Sentence)
translateNamedFormula (Sign f e, Map (OP_NAME, OpType) OP_NAME,
 Map (OP_NAME, PredType) OP_NAME)
signWithRenamings) [Named (FORMULA f)]
preparedSens
  (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
tptpSign, [Named Sentence]
signSentences [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence]
translatedSentences)

prepareNamedFormula :: (FormExtension f, Eq f)
                    => Named (FORMULA f) -> Named (FORMULA f)
prepareNamedFormula :: Named (FORMULA f) -> Named (FORMULA f)
prepareNamedFormula formula :: Named (FORMULA f)
formula =
  let expandedFormula :: FORMULA f
expandedFormula =
        (f -> f) -> FORMULA f -> FORMULA f
forall f. Eq f => (f -> f) -> FORMULA f -> FORMULA f
codeOutConditionalF f -> f
forall a. a -> a
id (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ -- Expand conditionals
        (f -> f) -> (f -> f) -> FORMULA f -> FORMULA f
forall f. (f -> f) -> (f -> f) -> FORMULA f -> FORMULA f
codeOutUniqueExtF f -> f
forall a. a -> a
id f -> f
forall a. a -> a
id (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ -- Expand "exists!" quantification
        Named (FORMULA f) -> FORMULA f
forall s a. SenAttr s a -> s
AS_Annotation.sentence Named (FORMULA f)
formula
  in  Named (FORMULA f)
formula { sentence :: FORMULA f
AS_Annotation.sentence = FORMULA f
expandedFormula }

translateNamedFormula :: (FormExtension f, Eq f)
                      => SignWithRenamings f e
                      -> Named (FORMULA f) -> Result (Named TSign.Sentence)
translateNamedFormula :: SignWithRenamings f e
-> Named (FORMULA f) -> Result (Named Sentence)
translateNamedFormula signWithRenamings :: SignWithRenamings f e
signWithRenamings x :: Named (FORMULA f)
x = do
  let nameS :: String
nameS = "ax_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
toAlphaNum ((Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Named (FORMULA f) -> String
forall s a. SenAttr s a -> a
senAttr Named (FORMULA f)
x)
  Sentence
translated <-
    SignWithRenamings f e
-> String -> Bool -> FORMULA f -> Result Sentence
forall e f.
(FormExtension f, Eq f) =>
SignWithRenamings f e
-> String -> Bool -> FORMULA f -> Result Sentence
translateFormula SignWithRenamings f e
signWithRenamings String
nameS (Named (FORMULA f) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom Named (FORMULA f)
x) (FORMULA f -> Result Sentence) -> FORMULA f -> Result Sentence
forall a b. (a -> b) -> a -> b
$
      Named (FORMULA f) -> FORMULA f
forall s a. SenAttr s a -> s
AS_Annotation.sentence Named (FORMULA f)
x
  Named Sentence -> Result (Named Sentence)
forall (m :: * -> *) a. Monad m => a -> m a
return (Named Sentence -> Result (Named Sentence))
-> Named Sentence -> Result (Named Sentence)
forall a b. (a -> b) -> a -> b
$ Named (FORMULA f)
x { sentence :: Sentence
AS_Annotation.sentence = Sentence
translated
             }

translateFormula :: forall e f . (FormExtension f, Eq f)
                 => SignWithRenamings f e -> String -> Bool -> FORMULA f
                 -> Result TSign.Sentence
translateFormula :: SignWithRenamings f e
-> String -> Bool -> FORMULA f -> Result Sentence
translateFormula signWithRenamings :: SignWithRenamings f e
signWithRenamings nameS :: String
nameS isAxiom' :: Bool
isAxiom' formula :: FORMULA f
formula = do
  let name :: Name
name = Token -> Name
NameString (Token -> Name) -> Token -> Name
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId String
nameS
  FOF_unitary_formula
fofFormula <- FORMULA f -> Result FOF_unitary_formula
(FormExtension f, Eq f) => FORMULA f -> Result FOF_unitary_formula
toUnitaryFormula FORMULA f
formula
  Sentence -> Result Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> Result Sentence) -> Sentence -> Result Sentence
forall a b. (a -> b) -> a -> b
$ if Bool
isAxiom'
           then Name -> FOF_unitary_formula -> Sentence
fofUnitaryFormulaToAxiom Name
name FOF_unitary_formula
fofFormula
           else Name -> FOF_unitary_formula -> Sentence
fofUnitaryFormulaToConjecture Name
name FOF_unitary_formula
fofFormula
  where
    toUnitaryFormula :: (FormExtension f, Eq f)
                         => FORMULA f
                         -> Result FOF_unitary_formula
    toUnitaryFormula :: FORMULA f -> Result FOF_unitary_formula
toUnitaryFormula x :: FORMULA f
x = case FORMULA f
x of
      Quantification q :: QUANTIFIER
q vars :: [VAR_DECL]
vars f :: FORMULA f
f _ -> do
        let fofVars :: [(Token, OP_NAME)]
fofVars = [VAR_DECL] -> [(Token, OP_NAME)]
translateVarDecls [VAR_DECL]
vars
        let variableList :: [Token]
variableList = ((Token, OP_NAME) -> Token) -> [(Token, OP_NAME)] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map (Token, OP_NAME) -> Token
forall a b. (a, b) -> a
fst [(Token, OP_NAME)]
fofVars
        let variableDeclaration :: FOF_unitary_formula
variableDeclaration =
              FOF_and_formula -> FOF_unitary_formula
unitaryFormulaAnd (FOF_and_formula -> FOF_unitary_formula)
-> FOF_and_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ ((Token, OP_NAME) -> FOF_unitary_formula)
-> [(Token, OP_NAME)] -> FOF_and_formula
forall a b. (a -> b) -> [a] -> [b]
map ((Token -> OP_NAME -> FOF_unitary_formula)
-> (Token, OP_NAME) -> FOF_unitary_formula
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Token -> OP_NAME -> FOF_unitary_formula
sortOfX) [(Token, OP_NAME)]
fofVars
        FOF_unitary_formula
fofF <- FORMULA f -> Result FOF_unitary_formula
(FormExtension f, Eq f) => FORMULA f -> Result FOF_unitary_formula
toUnitaryFormula FORMULA f
f
        case QUANTIFIER
q of
          Universal ->
            let implication :: FOF_unitary_formula
implication =
                  FOF_logic_formula -> FOF_unitary_formula
FOFUF_logic (FOF_logic_formula -> FOF_unitary_formula)
-> FOF_logic_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_binary_formula -> FOF_logic_formula
FOFLF_binary (FOF_binary_formula -> FOF_logic_formula)
-> FOF_binary_formula -> FOF_logic_formula
forall a b. (a -> b) -> a -> b
$ FOF_binary_nonassoc -> FOF_binary_formula
FOFBF_nonassoc (FOF_binary_nonassoc -> FOF_binary_formula)
-> FOF_binary_nonassoc -> FOF_binary_formula
forall a b. (a -> b) -> a -> b
$
                  Binary_connective
-> FOF_unitary_formula
-> FOF_unitary_formula
-> FOF_binary_nonassoc
FOF_binary_nonassoc Binary_connective
TAS.Implication FOF_unitary_formula
variableDeclaration FOF_unitary_formula
fofF
            in  FOF_unitary_formula -> Result FOF_unitary_formula
forall (m :: * -> *) a. Monad m => a -> m a
return (FOF_unitary_formula -> Result FOF_unitary_formula)
-> FOF_unitary_formula -> Result FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_quantified_formula -> FOF_unitary_formula
FOFUF_quantified (FOF_quantified_formula -> FOF_unitary_formula)
-> FOF_quantified_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$
                         FOF_quantifier
-> [Token] -> FOF_unitary_formula -> FOF_quantified_formula
FOF_quantified_formula FOF_quantifier
ForAll [Token]
variableList FOF_unitary_formula
implication
          Existential ->
            let conjunction :: FOF_unitary_formula
conjunction = FOF_and_formula -> FOF_unitary_formula
unitaryFormulaAnd [FOF_unitary_formula
variableDeclaration, FOF_unitary_formula
fofF]
            in  FOF_unitary_formula -> Result FOF_unitary_formula
forall (m :: * -> *) a. Monad m => a -> m a
return (FOF_unitary_formula -> Result FOF_unitary_formula)
-> FOF_unitary_formula -> Result FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_quantified_formula -> FOF_unitary_formula
FOFUF_quantified (FOF_quantified_formula -> FOF_unitary_formula)
-> FOF_quantified_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$
                         FOF_quantifier
-> [Token] -> FOF_unitary_formula -> FOF_quantified_formula
FOF_quantified_formula FOF_quantifier
Exists [Token]
variableList FOF_unitary_formula
conjunction
          -- Has been resolved/removed by prepareNamedFormula:
          Unique_existential ->
            String -> Result FOF_unitary_formula
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "SuleCFOL2TPTP: Unique_existential occurred where it cannot occur. This is a bug in Hets."
      Junction Con fs :: [FORMULA f]
fs _ -> do
        FOF_and_formula
fofs <- (FORMULA f -> Result FOF_unitary_formula)
-> [FORMULA f] -> Result FOF_and_formula
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM FORMULA f -> Result FOF_unitary_formula
(FormExtension f, Eq f) => FORMULA f -> Result FOF_unitary_formula
toUnitaryFormula [FORMULA f]
fs
        FOF_unitary_formula -> Result FOF_unitary_formula
forall (m :: * -> *) a. Monad m => a -> m a
return (FOF_unitary_formula -> Result FOF_unitary_formula)
-> FOF_unitary_formula -> Result FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_and_formula -> FOF_unitary_formula
unitaryFormulaAnd FOF_and_formula
fofs
      Junction Dis fs :: [FORMULA f]
fs _ -> do
        FOF_and_formula
fofs <- (FORMULA f -> Result FOF_unitary_formula)
-> [FORMULA f] -> Result FOF_and_formula
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM FORMULA f -> Result FOF_unitary_formula
(FormExtension f, Eq f) => FORMULA f -> Result FOF_unitary_formula
toUnitaryFormula [FORMULA f]
fs
        FOF_unitary_formula -> Result FOF_unitary_formula
forall (m :: * -> *) a. Monad m => a -> m a
return (FOF_unitary_formula -> Result FOF_unitary_formula)
-> FOF_unitary_formula -> Result FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_and_formula -> FOF_unitary_formula
unitaryFormulaOr FOF_and_formula
fofs
      Relation f1 :: FORMULA f
f1 CAS.Implication f2 :: FORMULA f
f2 _ -> do
        FOF_unitary_formula
fof1 <- FORMULA f -> Result FOF_unitary_formula
(FormExtension f, Eq f) => FORMULA f -> Result FOF_unitary_formula
toUnitaryFormula FORMULA f
f1
        FOF_unitary_formula
fof2 <- FORMULA f -> Result FOF_unitary_formula
(FormExtension f, Eq f) => FORMULA f -> Result FOF_unitary_formula
toUnitaryFormula FORMULA f
f2
        FOF_unitary_formula -> Result FOF_unitary_formula
forall (m :: * -> *) a. Monad m => a -> m a
return (FOF_unitary_formula -> Result FOF_unitary_formula)
-> FOF_unitary_formula -> Result FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_logic_formula -> FOF_unitary_formula
FOFUF_logic (FOF_logic_formula -> FOF_unitary_formula)
-> FOF_logic_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_binary_formula -> FOF_logic_formula
FOFLF_binary (FOF_binary_formula -> FOF_logic_formula)
-> FOF_binary_formula -> FOF_logic_formula
forall a b. (a -> b) -> a -> b
$ FOF_binary_nonassoc -> FOF_binary_formula
FOFBF_nonassoc (FOF_binary_nonassoc -> FOF_binary_formula)
-> FOF_binary_nonassoc -> FOF_binary_formula
forall a b. (a -> b) -> a -> b
$
                 Binary_connective
-> FOF_unitary_formula
-> FOF_unitary_formula
-> FOF_binary_nonassoc
FOF_binary_nonassoc Binary_connective
TAS.Implication FOF_unitary_formula
fof1 FOF_unitary_formula
fof2
      -- For some reason, "f2 if f1" is saved as "Relation f1 RevImpl f2 _"
      Relation f1 :: FORMULA f
f1 RevImpl f2 :: FORMULA f
f2 _ -> do
        FOF_unitary_formula
fof1 <- FORMULA f -> Result FOF_unitary_formula
(FormExtension f, Eq f) => FORMULA f -> Result FOF_unitary_formula
toUnitaryFormula FORMULA f
f1
        FOF_unitary_formula
fof2 <- FORMULA f -> Result FOF_unitary_formula
(FormExtension f, Eq f) => FORMULA f -> Result FOF_unitary_formula
toUnitaryFormula FORMULA f
f2
        -- Flip the formulae:
        FOF_unitary_formula -> Result FOF_unitary_formula
forall (m :: * -> *) a. Monad m => a -> m a
return (FOF_unitary_formula -> Result FOF_unitary_formula)
-> FOF_unitary_formula -> Result FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_logic_formula -> FOF_unitary_formula
FOFUF_logic (FOF_logic_formula -> FOF_unitary_formula)
-> FOF_logic_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_binary_formula -> FOF_logic_formula
FOFLF_binary (FOF_binary_formula -> FOF_logic_formula)
-> FOF_binary_formula -> FOF_logic_formula
forall a b. (a -> b) -> a -> b
$ FOF_binary_nonassoc -> FOF_binary_formula
FOFBF_nonassoc (FOF_binary_nonassoc -> FOF_binary_formula)
-> FOF_binary_nonassoc -> FOF_binary_formula
forall a b. (a -> b) -> a -> b
$
                 Binary_connective
-> FOF_unitary_formula
-> FOF_unitary_formula
-> FOF_binary_nonassoc
FOF_binary_nonassoc Binary_connective
ReverseImplication FOF_unitary_formula
fof2 FOF_unitary_formula
fof1
      Relation f1 :: FORMULA f
f1 CAS.Equivalence f2 :: FORMULA f
f2 _ -> do
        FOF_unitary_formula
fof1 <- FORMULA f -> Result FOF_unitary_formula
(FormExtension f, Eq f) => FORMULA f -> Result FOF_unitary_formula
toUnitaryFormula FORMULA f
f1
        FOF_unitary_formula
fof2 <- FORMULA f -> Result FOF_unitary_formula
(FormExtension f, Eq f) => FORMULA f -> Result FOF_unitary_formula
toUnitaryFormula FORMULA f
f2
        FOF_unitary_formula -> Result FOF_unitary_formula
forall (m :: * -> *) a. Monad m => a -> m a
return (FOF_unitary_formula -> Result FOF_unitary_formula)
-> FOF_unitary_formula -> Result FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_logic_formula -> FOF_unitary_formula
FOFUF_logic (FOF_logic_formula -> FOF_unitary_formula)
-> FOF_logic_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_binary_formula -> FOF_logic_formula
FOFLF_binary (FOF_binary_formula -> FOF_logic_formula)
-> FOF_binary_formula -> FOF_logic_formula
forall a b. (a -> b) -> a -> b
$ FOF_binary_nonassoc -> FOF_binary_formula
FOFBF_nonassoc (FOF_binary_nonassoc -> FOF_binary_formula)
-> FOF_binary_nonassoc -> FOF_binary_formula
forall a b. (a -> b) -> a -> b
$
                 Binary_connective
-> FOF_unitary_formula
-> FOF_unitary_formula
-> FOF_binary_nonassoc
FOF_binary_nonassoc Binary_connective
TAS.Equivalence FOF_unitary_formula
fof1 FOF_unitary_formula
fof2
      Negation f :: FORMULA f
f _ -> do
        FOF_unitary_formula
fofF <- FORMULA f -> Result FOF_unitary_formula
(FormExtension f, Eq f) => FORMULA f -> Result FOF_unitary_formula
toUnitaryFormula FORMULA f
f
        FOF_unitary_formula -> Result FOF_unitary_formula
forall (m :: * -> *) a. Monad m => a -> m a
return (FOF_unitary_formula -> Result FOF_unitary_formula)
-> FOF_unitary_formula -> Result FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_unary_formula -> FOF_unitary_formula
FOFUF_unary (FOF_unary_formula -> FOF_unitary_formula)
-> FOF_unary_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ Unary_connective -> FOF_unitary_formula -> FOF_unary_formula
FOFUF_connective Unary_connective
NOT FOF_unitary_formula
fofF
      Atom True _ ->
        FOF_unitary_formula -> Result FOF_unitary_formula
forall (m :: * -> *) a. Monad m => a -> m a
return (FOF_unitary_formula -> Result FOF_unitary_formula)
-> FOF_unitary_formula -> Result FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_atomic_formula -> FOF_unitary_formula
FOFUF_atomic (FOF_atomic_formula -> FOF_unitary_formula)
-> FOF_atomic_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_defined_atomic_formula -> FOF_atomic_formula
FOFAT_defined (FOF_defined_atomic_formula -> FOF_atomic_formula)
-> FOF_defined_atomic_formula -> FOF_atomic_formula
forall a b. (a -> b) -> a -> b
$ FOF_defined_plain_formula -> FOF_defined_atomic_formula
FOFDAF_plain (FOF_defined_plain_formula -> FOF_defined_atomic_formula)
-> FOF_defined_plain_formula -> FOF_defined_atomic_formula
forall a b. (a -> b) -> a -> b
$
                 Defined_proposition -> FOF_defined_plain_formula
FOFDPF_proposition (Defined_proposition -> FOF_defined_plain_formula)
-> Defined_proposition -> FOF_defined_plain_formula
forall a b. (a -> b) -> a -> b
$ Defined_proposition
TPTP_true
      Atom False _ ->
        FOF_unitary_formula -> Result FOF_unitary_formula
forall (m :: * -> *) a. Monad m => a -> m a
return (FOF_unitary_formula -> Result FOF_unitary_formula)
-> FOF_unitary_formula -> Result FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_atomic_formula -> FOF_unitary_formula
FOFUF_atomic (FOF_atomic_formula -> FOF_unitary_formula)
-> FOF_atomic_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_defined_atomic_formula -> FOF_atomic_formula
FOFAT_defined (FOF_defined_atomic_formula -> FOF_atomic_formula)
-> FOF_defined_atomic_formula -> FOF_atomic_formula
forall a b. (a -> b) -> a -> b
$ FOF_defined_plain_formula -> FOF_defined_atomic_formula
FOFDAF_plain (FOF_defined_plain_formula -> FOF_defined_atomic_formula)
-> FOF_defined_plain_formula -> FOF_defined_atomic_formula
forall a b. (a -> b) -> a -> b
$
                 Defined_proposition -> FOF_defined_plain_formula
FOFDPF_proposition (Defined_proposition -> FOF_defined_plain_formula)
-> Defined_proposition -> FOF_defined_plain_formula
forall a b. (a -> b) -> a -> b
$ Defined_proposition
TPTP_false
      Predication predSymb :: PRED_SYMB
predSymb terms :: [TERM f]
terms _ -> do
        OP_NAME
predName <- case PRED_SYMB
predSymb of
              Pred_name _ ->
                String -> Result OP_NAME
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "SuleCFOL2TPTP: An unqualified predicate has been detected. This is a bug in Hets."
              Qual_pred_name predName :: OP_NAME
predName (Pred_type args :: [OP_NAME]
args _) _ ->
                OP_NAME -> Result OP_NAME
forall (m :: * -> *) a. Monad m => a -> m a
return (OP_NAME -> Result OP_NAME) -> OP_NAME -> Result OP_NAME
forall a b. (a -> b) -> a -> b
$ SignWithRenamings f e -> OP_NAME -> PredType -> OP_NAME
forall f e.
(FormExtension f, Eq f) =>
SignWithRenamings f e -> OP_NAME -> PredType -> OP_NAME
lookupPredName SignWithRenamings f e
signWithRenamings OP_NAME
predName (PredType -> OP_NAME) -> PredType -> OP_NAME
forall a b. (a -> b) -> a -> b
$
                  PredType :: [OP_NAME] -> PredType
PredType { predArgs :: [OP_NAME]
predArgs = [OP_NAME]
args }
        let predicate :: Token
predicate = OP_NAME -> Token
predicateOfPred OP_NAME
predName
        [FOF_term]
args <- (TERM f -> Result FOF_term) -> [TERM f] -> Result [FOF_term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SignWithRenamings f e -> TERM f -> Result FOF_term
forall f e.
(FormExtension f, Eq f) =>
SignWithRenamings f e -> TERM f -> Result FOF_term
translateTerm SignWithRenamings f e
signWithRenamings) [TERM f]
terms
        case [FOF_term]
args of
          [] -> FOF_unitary_formula -> Result FOF_unitary_formula
forall (m :: * -> *) a. Monad m => a -> m a
return (FOF_unitary_formula -> Result FOF_unitary_formula)
-> FOF_unitary_formula -> Result FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_atomic_formula -> FOF_unitary_formula
FOFUF_atomic (FOF_atomic_formula -> FOF_unitary_formula)
-> FOF_atomic_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_plain_atomic_formula -> FOF_atomic_formula
FOFAT_plain (FOF_plain_atomic_formula -> FOF_atomic_formula)
-> FOF_plain_atomic_formula -> FOF_atomic_formula
forall a b. (a -> b) -> a -> b
$ Token -> FOF_plain_atomic_formula
FOFPAF_proposition Token
predicate
          _ -> FOF_unitary_formula -> Result FOF_unitary_formula
forall (m :: * -> *) a. Monad m => a -> m a
return (FOF_unitary_formula -> Result FOF_unitary_formula)
-> FOF_unitary_formula -> Result FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_atomic_formula -> FOF_unitary_formula
FOFUF_atomic (FOF_atomic_formula -> FOF_unitary_formula)
-> FOF_atomic_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_plain_atomic_formula -> FOF_atomic_formula
FOFAT_plain (FOF_plain_atomic_formula -> FOF_atomic_formula)
-> FOF_plain_atomic_formula -> FOF_atomic_formula
forall a b. (a -> b) -> a -> b
$ Token -> [FOF_term] -> FOF_plain_atomic_formula
FOFPAF_predicate Token
predicate [FOF_term]
args
      -- There is no Equation t1 Existl t2 in SuleCFOL
      Equation t1 :: TERM f
t1 Strong t2 :: TERM f
t2 _ -> do
        FOF_term
fofTerm1 <- SignWithRenamings f e -> TERM f -> Result FOF_term
forall f e.
(FormExtension f, Eq f) =>
SignWithRenamings f e -> TERM f -> Result FOF_term
translateTerm SignWithRenamings f e
signWithRenamings TERM f
t1
        FOF_term
fofTerm2 <- SignWithRenamings f e -> TERM f -> Result FOF_term
forall f e.
(FormExtension f, Eq f) =>
SignWithRenamings f e -> TERM f -> Result FOF_term
translateTerm SignWithRenamings f e
signWithRenamings TERM f
t2
        FOF_unitary_formula -> Result FOF_unitary_formula
forall (m :: * -> *) a. Monad m => a -> m a
return (FOF_unitary_formula -> Result FOF_unitary_formula)
-> FOF_unitary_formula -> Result FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_atomic_formula -> FOF_unitary_formula
FOFUF_atomic (FOF_atomic_formula -> FOF_unitary_formula)
-> FOF_atomic_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_defined_atomic_formula -> FOF_atomic_formula
FOFAT_defined (FOF_defined_atomic_formula -> FOF_atomic_formula)
-> FOF_defined_atomic_formula -> FOF_atomic_formula
forall a b. (a -> b) -> a -> b
$ FOF_defined_infix_formula -> FOF_defined_atomic_formula
FOFDAF_infix (FOF_defined_infix_formula -> FOF_defined_atomic_formula)
-> FOF_defined_infix_formula -> FOF_defined_atomic_formula
forall a b. (a -> b) -> a -> b
$
                 Defined_infix_pred
-> FOF_term -> FOF_term -> FOF_defined_infix_formula
FOF_defined_infix_formula
                 Defined_infix_pred
Defined_infix_equality FOF_term
fofTerm1 FOF_term
fofTerm2
      Membership term :: TERM f
term sort :: OP_NAME
sort _ -> do
        FOF_term
fofTerm <- SignWithRenamings f e -> TERM f -> Result FOF_term
forall f e.
(FormExtension f, Eq f) =>
SignWithRenamings f e -> TERM f -> Result FOF_term
translateTerm SignWithRenamings f e
signWithRenamings TERM f
term
        FOF_unitary_formula -> Result FOF_unitary_formula
forall (m :: * -> *) a. Monad m => a -> m a
return (FOF_unitary_formula -> Result FOF_unitary_formula)
-> FOF_unitary_formula -> Result FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_atomic_formula -> FOF_unitary_formula
FOFUF_atomic (FOF_atomic_formula -> FOF_unitary_formula)
-> FOF_atomic_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_plain_atomic_formula -> FOF_atomic_formula
FOFAT_plain (FOF_plain_atomic_formula -> FOF_atomic_formula)
-> FOF_plain_atomic_formula -> FOF_atomic_formula
forall a b. (a -> b) -> a -> b
$
                 Token -> [FOF_term] -> FOF_plain_atomic_formula
FOFPAF_predicate (OP_NAME -> Token
predicateOfSort OP_NAME
sort) [FOF_term
fofTerm]
      -- Sort_gen_ax cannot be translated. Fail:
      -- See https://github.com/spechub/Hets/issues/1706
      Sort_gen_ax _ _ ->
        FOF_unitary_formula -> String -> Result FOF_unitary_formula
forall a. a -> String -> Result a
justWarn (FOF_atomic_formula -> FOF_unitary_formula
FOFUF_atomic (FOF_atomic_formula -> FOF_unitary_formula)
-> FOF_atomic_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_defined_atomic_formula -> FOF_atomic_formula
FOFAT_defined (FOF_defined_atomic_formula -> FOF_atomic_formula)
-> FOF_defined_atomic_formula -> FOF_atomic_formula
forall a b. (a -> b) -> a -> b
$ FOF_defined_plain_formula -> FOF_defined_atomic_formula
FOFDAF_plain (FOF_defined_plain_formula -> FOF_defined_atomic_formula)
-> FOF_defined_plain_formula -> FOF_defined_atomic_formula
forall a b. (a -> b) -> a -> b
$
                  Defined_proposition -> FOF_defined_plain_formula
FOFDPF_proposition (Defined_proposition -> FOF_defined_plain_formula)
-> Defined_proposition -> FOF_defined_plain_formula
forall a b. (a -> b) -> a -> b
$ Defined_proposition
TPTP_true)
                 "SuleCFOL2TPTP: Sort generation axioms are not yet supported."
      -- There is no Definedness in SuleCFOL
      -- There is no Mixfix_formula - it only occurs during parsing
      -- There is no Unparsed_formula
      -- There is no QuantOp in SuleCFOL
      -- There is no QuantPred in SuleCFOL
      -- There is no ExtFORMULA in SuleCFOL
      _ -> String -> Result FOF_unitary_formula
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "SuleCFOL2TPTP: A formula that should not occur has occurred."

    translateVarDecls :: [VAR_DECL] -> [(TAS.Variable, SORT)]
    translateVarDecls :: [VAR_DECL] -> [(Token, OP_NAME)]
translateVarDecls = (VAR_DECL -> [(Token, OP_NAME)])
-> [VAR_DECL] -> [(Token, OP_NAME)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap VAR_DECL -> [(Token, OP_NAME)]
translateVarDecl

    translateVarDecl :: VAR_DECL -> [(TAS.Variable, SORT)]
    translateVarDecl :: VAR_DECL -> [(Token, OP_NAME)]
translateVarDecl x :: VAR_DECL
x = case VAR_DECL
x of
      Var_decl vars :: [Token]
vars sort :: OP_NAME
sort _ -> [Token] -> [OP_NAME] -> [(Token, OP_NAME)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Token -> Token) -> [Token] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map Token -> Token
variableOfVar [Token]
vars) ([OP_NAME] -> [(Token, OP_NAME)])
-> [OP_NAME] -> [(Token, OP_NAME)]
forall a b. (a -> b) -> a -> b
$ OP_NAME -> [OP_NAME]
forall a. a -> [a]
repeat OP_NAME
sort

unitaryFormulaAnd :: FOF_and_formula -> FOF_unitary_formula
unitaryFormulaAnd :: FOF_and_formula -> FOF_unitary_formula
unitaryFormulaAnd = FOF_logic_formula -> FOF_unitary_formula
FOFUF_logic (FOF_logic_formula -> FOF_unitary_formula)
-> (FOF_and_formula -> FOF_logic_formula)
-> FOF_and_formula
-> FOF_unitary_formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FOF_binary_formula -> FOF_logic_formula
FOFLF_binary (FOF_binary_formula -> FOF_logic_formula)
-> (FOF_and_formula -> FOF_binary_formula)
-> FOF_and_formula
-> FOF_logic_formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FOF_binary_assoc -> FOF_binary_formula
FOFBF_assoc (FOF_binary_assoc -> FOF_binary_formula)
-> (FOF_and_formula -> FOF_binary_assoc)
-> FOF_and_formula
-> FOF_binary_formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FOF_and_formula -> FOF_binary_assoc
FOFBA_and

unitaryFormulaOr :: FOF_or_formula -> FOF_unitary_formula
unitaryFormulaOr :: FOF_and_formula -> FOF_unitary_formula
unitaryFormulaOr = FOF_logic_formula -> FOF_unitary_formula
FOFUF_logic (FOF_logic_formula -> FOF_unitary_formula)
-> (FOF_and_formula -> FOF_logic_formula)
-> FOF_and_formula
-> FOF_unitary_formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FOF_binary_formula -> FOF_logic_formula
FOFLF_binary (FOF_binary_formula -> FOF_logic_formula)
-> (FOF_and_formula -> FOF_binary_formula)
-> FOF_and_formula
-> FOF_logic_formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FOF_binary_assoc -> FOF_binary_formula
FOFBF_assoc (FOF_binary_assoc -> FOF_binary_formula)
-> (FOF_and_formula -> FOF_binary_assoc)
-> FOF_and_formula
-> FOF_binary_formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FOF_and_formula -> FOF_binary_assoc
FOFBA_or


translateTerm :: (FormExtension f, Eq f)
              => SignWithRenamings f e
              -> TERM f
              -> Result TAS.FOF_term
translateTerm :: SignWithRenamings f e -> TERM f -> Result FOF_term
translateTerm signWithRenamings :: SignWithRenamings f e
signWithRenamings x :: TERM f
x = case TERM f
x of
  Qual_var var :: Token
var _ _ -> FOF_term -> Result FOF_term
forall (m :: * -> *) a. Monad m => a -> m a
return (FOF_term -> Result FOF_term) -> FOF_term -> Result FOF_term
forall a b. (a -> b) -> a -> b
$ Token -> FOF_term
FOFT_variable (Token -> FOF_term) -> Token -> FOF_term
forall a b. (a -> b) -> a -> b
$ Token -> Token
variableOfVar Token
var
  Application opSymb :: OP_SYMB
opSymb terms :: [TERM f]
terms _ -> do
    OP_NAME
opName <- case OP_SYMB
opSymb of
          Op_name _ ->
            String -> Result OP_NAME
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "SuleCFOL2TPTP: An unqualified operation has been detected. This is a bug in Hets."
          Qual_op_name opName :: OP_NAME
opName (Op_type kind :: OpKind
kind args :: [OP_NAME]
args res :: OP_NAME
res _) _ ->
            OP_NAME -> Result OP_NAME
forall (m :: * -> *) a. Monad m => a -> m a
return (OP_NAME -> Result OP_NAME) -> OP_NAME -> Result OP_NAME
forall a b. (a -> b) -> a -> b
$ SignWithRenamings f e -> OP_NAME -> OpType -> OP_NAME
forall f e.
(FormExtension f, Eq f) =>
SignWithRenamings f e -> OP_NAME -> OpType -> OP_NAME
lookupOpName SignWithRenamings f e
signWithRenamings OP_NAME
opName (OpType -> OP_NAME) -> OpType -> OP_NAME
forall a b. (a -> b) -> a -> b
$
              OpType :: OpKind -> [OP_NAME] -> OP_NAME -> OpType
OpType { opKind :: OpKind
opKind = OpKind
kind, opArgs :: [OP_NAME]
opArgs = [OP_NAME]
args, opRes :: OP_NAME
opRes = OP_NAME
res }
    let function :: Token
function = OP_NAME -> Token
functionOfOp OP_NAME
opName
    [FOF_term]
args <- (TERM f -> Result FOF_term) -> [TERM f] -> Result [FOF_term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SignWithRenamings f e -> TERM f -> Result FOF_term
forall f e.
(FormExtension f, Eq f) =>
SignWithRenamings f e -> TERM f -> Result FOF_term
translateTerm SignWithRenamings f e
signWithRenamings) [TERM f]
terms
    case [FOF_term]
args of
      [] -> FOF_term -> Result FOF_term
forall (m :: * -> *) a. Monad m => a -> m a
return (FOF_term -> Result FOF_term) -> FOF_term -> Result FOF_term
forall a b. (a -> b) -> a -> b
$ FOF_function_term -> FOF_term
FOFT_function (FOF_function_term -> FOF_term) -> FOF_function_term -> FOF_term
forall a b. (a -> b) -> a -> b
$ FOF_plain_term -> FOF_function_term
FOFFT_plain (FOF_plain_term -> FOF_function_term)
-> FOF_plain_term -> FOF_function_term
forall a b. (a -> b) -> a -> b
$ Token -> FOF_plain_term
FOFPT_constant (Token -> FOF_plain_term) -> Token -> FOF_plain_term
forall a b. (a -> b) -> a -> b
$ Token
function
      _ -> FOF_term -> Result FOF_term
forall (m :: * -> *) a. Monad m => a -> m a
return (FOF_term -> Result FOF_term) -> FOF_term -> Result FOF_term
forall a b. (a -> b) -> a -> b
$ FOF_function_term -> FOF_term
FOFT_function (FOF_function_term -> FOF_term) -> FOF_function_term -> FOF_term
forall a b. (a -> b) -> a -> b
$ FOF_plain_term -> FOF_function_term
FOFFT_plain (FOF_plain_term -> FOF_function_term)
-> FOF_plain_term -> FOF_function_term
forall a b. (a -> b) -> a -> b
$ Token -> [FOF_term] -> FOF_plain_term
FOFPT_functor Token
function [FOF_term]
args
  -- The sort can be ignored:
  Sorted_term term :: TERM f
term _ _ -> SignWithRenamings f e -> TERM f -> Result FOF_term
forall f e.
(FormExtension f, Eq f) =>
SignWithRenamings f e -> TERM f -> Result FOF_term
translateTerm SignWithRenamings f e
signWithRenamings TERM f
term
  -- Conditional has been resolved/removed in prepareNamedFormula
  -- There is no Cast in SuleCFOL
  -- Everything else cannot occur
  _ -> String -> Result FOF_term
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "SuleCFOL2TPTP: A term that should not occur has occurred."


fofUnitaryFormulaToAxiom :: TAS.Name -> FOF_unitary_formula -> TSign.Sentence
fofUnitaryFormulaToAxiom :: Name -> FOF_unitary_formula -> Sentence
fofUnitaryFormulaToAxiom name :: Name
name f :: FOF_unitary_formula
f =
  let formula :: FOF_formula
formula = FOF_logic_formula -> FOF_formula
FOFF_logic (FOF_logic_formula -> FOF_formula)
-> FOF_logic_formula -> FOF_formula
forall a b. (a -> b) -> a -> b
$ FOF_unitary_formula -> FOF_logic_formula
FOFLF_unitary FOF_unitary_formula
f
  in  FOF_annotated -> Sentence
AF_FOF_Annotated (FOF_annotated -> Sentence) -> FOF_annotated -> Sentence
forall a b. (a -> b) -> a -> b
$ Name -> Formula_role -> FOF_formula -> Annotations -> FOF_annotated
FOF_annotated Name
name Formula_role
Axiom FOF_formula
formula (Maybe (Source, Optional_info) -> Annotations
Annotations Maybe (Source, Optional_info)
forall a. Maybe a
Nothing)

fofUnitaryFormulaToConjecture :: TAS.Name -> FOF_unitary_formula
                              -> TSign.Sentence
fofUnitaryFormulaToConjecture :: Name -> FOF_unitary_formula -> Sentence
fofUnitaryFormulaToConjecture name :: Name
name f :: FOF_unitary_formula
f =
  let formula :: FOF_formula
formula = FOF_logic_formula -> FOF_formula
FOFF_logic (FOF_logic_formula -> FOF_formula)
-> FOF_logic_formula -> FOF_formula
forall a b. (a -> b) -> a -> b
$ FOF_unitary_formula -> FOF_logic_formula
FOFLF_unitary FOF_unitary_formula
f
  in  FOF_annotated -> Sentence
AF_FOF_Annotated (FOF_annotated -> Sentence) -> FOF_annotated -> Sentence
forall a b. (a -> b) -> a -> b
$
        Name -> Formula_role -> FOF_formula -> Annotations -> FOF_annotated
FOF_annotated Name
name Formula_role
Conjecture FOF_formula
formula (Maybe (Source, Optional_info) -> Annotations
Annotations Maybe (Source, Optional_info)
forall a. Maybe a
Nothing)

lookupOpName :: (FormExtension f, Eq f)
             => SignWithRenamings f e -> OP_NAME -> OpType -> OP_NAME
lookupOpName :: SignWithRenamings f e -> OP_NAME -> OpType -> OP_NAME
lookupOpName (_, renamedOps :: Map (OP_NAME, OpType) OP_NAME
renamedOps, _) opName :: OP_NAME
opName opType :: OpType
opType =
  OP_NAME
-> (OP_NAME, OpType) -> Map (OP_NAME, OpType) OP_NAME -> OP_NAME
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault OP_NAME
opName (OP_NAME
opName, OpType
opType) Map (OP_NAME, OpType) OP_NAME
renamedOps

lookupPredName :: (FormExtension f, Eq f)
             => SignWithRenamings f e -> PRED_NAME -> PredType -> PRED_NAME
lookupPredName :: SignWithRenamings f e -> OP_NAME -> PredType -> OP_NAME
lookupPredName (_, _, renamedPreds :: Map (OP_NAME, PredType) OP_NAME
renamedPreds) predName :: OP_NAME
predName predType :: PredType
predType =
  OP_NAME
-> (OP_NAME, PredType)
-> Map (OP_NAME, PredType) OP_NAME
-> OP_NAME
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault OP_NAME
predName (OP_NAME
predName, PredType
predType) Map (OP_NAME, PredType) OP_NAME
renamedPreds

-- Ops and Preds in the overloading relation must be renamed.
-- This type contains the Sign with renaming applied and the information what
-- each original op+type or pred+type was renamed to.
type SignWithRenamings f e = (CSign.Sign f e,
                              Map.Map (OP_NAME, OpType) OP_NAME,
                              Map.Map (PRED_NAME, PredType) PRED_NAME)

-- finds ops and preds that have the same name but operate on different connected components. Renames these ops and preds.
prepareSign :: (FormExtension f, Eq f)
            => CSign.Sign f e -> SignWithRenamings f e
prepareSign :: Sign f e -> SignWithRenamings f e
prepareSign sign :: Sign f e
sign =
  let connectedComponents :: [Set OP_NAME]
connectedComponents = Sign f e -> [Set OP_NAME]
forall f e. (FormExtension f, Eq f) => Sign f e -> [Set OP_NAME]
gatherConnectedComponents Sign f e
sign
      connectedComponentMap :: Map OP_NAME Int
connectedComponentMap = [Set OP_NAME] -> Map OP_NAME Int
connectedComponentsToMap [Set OP_NAME]
connectedComponents
      renamedOps :: Map (OP_NAME, OpType) OP_NAME
renamedOps =
        (OP_NAME
 -> Set OpType
 -> Map (OP_NAME, OpType) OP_NAME
 -> Map (OP_NAME, OpType) OP_NAME)
-> Map (OP_NAME, OpType) OP_NAME
-> Map OP_NAME (Set OpType)
-> Map (OP_NAME, OpType) OP_NAME
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (Map OP_NAME Int
-> OP_NAME
-> Set OpType
-> Map (OP_NAME, OpType) OP_NAME
-> Map (OP_NAME, OpType) OP_NAME
addOpIfConflicting Map OP_NAME Int
connectedComponentMap) Map (OP_NAME, OpType) OP_NAME
forall k a. Map k a
Map.empty (Map OP_NAME (Set OpType) -> Map (OP_NAME, OpType) OP_NAME)
-> Map OP_NAME (Set OpType) -> Map (OP_NAME, OpType) OP_NAME
forall a b. (a -> b) -> a -> b
$
          MapSet OP_NAME OpType -> Map OP_NAME (Set OpType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap (MapSet OP_NAME OpType -> Map OP_NAME (Set OpType))
-> MapSet OP_NAME OpType -> Map OP_NAME (Set OpType)
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet OP_NAME OpType
forall f e. Sign f e -> MapSet OP_NAME OpType
opMap Sign f e
sign
      renamedPreds :: Map (OP_NAME, PredType) OP_NAME
renamedPreds =
        (OP_NAME
 -> Set PredType
 -> Map (OP_NAME, PredType) OP_NAME
 -> Map (OP_NAME, PredType) OP_NAME)
-> Map (OP_NAME, PredType) OP_NAME
-> Map OP_NAME (Set PredType)
-> Map (OP_NAME, PredType) OP_NAME
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (Map OP_NAME Int
-> OP_NAME
-> Set PredType
-> Map (OP_NAME, PredType) OP_NAME
-> Map (OP_NAME, PredType) OP_NAME
addPredIfConflicting Map OP_NAME Int
connectedComponentMap) Map (OP_NAME, PredType) OP_NAME
forall k a. Map k a
Map.empty (Map OP_NAME (Set PredType) -> Map (OP_NAME, PredType) OP_NAME)
-> Map OP_NAME (Set PredType) -> Map (OP_NAME, PredType) OP_NAME
forall a b. (a -> b) -> a -> b
$
          MapSet OP_NAME PredType -> Map OP_NAME (Set PredType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap (MapSet OP_NAME PredType -> Map OP_NAME (Set PredType))
-> MapSet OP_NAME PredType -> Map OP_NAME (Set PredType)
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet OP_NAME PredType
forall f e. Sign f e -> MapSet OP_NAME PredType
predMap Sign f e
sign
      renamedOpMap :: MapSet OP_NAME OpType
renamedOpMap =
        (OP_NAME
 -> OpType -> MapSet OP_NAME OpType -> MapSet OP_NAME OpType)
-> MapSet OP_NAME OpType
-> MapSet OP_NAME OpType
-> MapSet OP_NAME OpType
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey (Map (OP_NAME, OpType) OP_NAME
-> OP_NAME
-> OpType
-> MapSet OP_NAME OpType
-> MapSet OP_NAME OpType
modifyOpMap Map (OP_NAME, OpType) OP_NAME
renamedOps) (Sign f e -> MapSet OP_NAME OpType
forall f e. Sign f e -> MapSet OP_NAME OpType
opMap Sign f e
sign) (MapSet OP_NAME OpType -> MapSet OP_NAME OpType)
-> MapSet OP_NAME OpType -> MapSet OP_NAME OpType
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet OP_NAME OpType
forall f e. Sign f e -> MapSet OP_NAME OpType
opMap Sign f e
sign
      renamedPredMap :: MapSet OP_NAME PredType
renamedPredMap =
        (OP_NAME
 -> PredType -> MapSet OP_NAME PredType -> MapSet OP_NAME PredType)
-> MapSet OP_NAME PredType
-> MapSet OP_NAME PredType
-> MapSet OP_NAME PredType
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey (Map (OP_NAME, PredType) OP_NAME
-> OP_NAME
-> PredType
-> MapSet OP_NAME PredType
-> MapSet OP_NAME PredType
modifyPredMap Map (OP_NAME, PredType) OP_NAME
renamedPreds) (Sign f e -> MapSet OP_NAME PredType
forall f e. Sign f e -> MapSet OP_NAME PredType
predMap Sign f e
sign) (MapSet OP_NAME PredType -> MapSet OP_NAME PredType)
-> MapSet OP_NAME PredType -> MapSet OP_NAME PredType
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet OP_NAME PredType
forall f e. Sign f e -> MapSet OP_NAME PredType
predMap Sign f e
sign
  in  (Sign f e
sign { opMap :: MapSet OP_NAME OpType
opMap = MapSet OP_NAME OpType
renamedOpMap, predMap :: MapSet OP_NAME PredType
predMap = MapSet OP_NAME PredType
renamedPredMap},
       Map (OP_NAME, OpType) OP_NAME
renamedOps,
       Map (OP_NAME, PredType) OP_NAME
renamedPreds)
  where
    gatherConnectedComponents :: (FormExtension f, Eq f)
                              => CSign.Sign f e -> [Set.Set SORT]
    gatherConnectedComponents :: Sign f e -> [Set OP_NAME]
gatherConnectedComponents sign' :: Sign f e
sign' =
      let topSortsL :: [OP_NAME]
topSortsL = Set OP_NAME -> [OP_NAME]
forall a. Set a -> [a]
Set.toList (Set OP_NAME -> [OP_NAME]) -> Set OP_NAME -> [OP_NAME]
forall a b. (a -> b) -> a -> b
$ Rel OP_NAME -> Set OP_NAME
forall a. Ord a => Rel a -> Set a
Rel.mostRight (Rel OP_NAME -> Set OP_NAME) -> Rel OP_NAME -> Set OP_NAME
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel OP_NAME
forall f e. Sign f e -> Rel OP_NAME
sortRel Sign f e
sign'
          revReflTransClosureSortRel :: Rel OP_NAME
revReflTransClosureSortRel =
            Rel OP_NAME -> Rel OP_NAME
forall a. Ord a => Rel a -> Rel a
Rel.transpose (Rel OP_NAME -> Rel OP_NAME) -> Rel OP_NAME -> Rel OP_NAME
forall a b. (a -> b) -> a -> b
$ Rel OP_NAME -> Rel OP_NAME
forall a. Ord a => Rel a -> Rel a
Rel.reflexive (Rel OP_NAME -> Rel OP_NAME) -> Rel OP_NAME -> Rel OP_NAME
forall a b. (a -> b) -> a -> b
$ Rel OP_NAME -> Rel OP_NAME
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (Rel OP_NAME -> Rel OP_NAME) -> Rel OP_NAME -> Rel OP_NAME
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel OP_NAME
forall f e. Sign f e -> Rel OP_NAME
sortRel Sign f e
sign'
      in  (OP_NAME -> Set OP_NAME) -> [OP_NAME] -> [Set OP_NAME]
forall a b. (a -> b) -> [a] -> [b]
map (\ topSort :: OP_NAME
topSort -> OP_NAME -> Set OP_NAME -> Set OP_NAME
forall a. Ord a => a -> Set a -> Set a
Set.insert OP_NAME
topSort (Set OP_NAME -> Set OP_NAME) -> Set OP_NAME -> Set OP_NAME
forall a b. (a -> b) -> a -> b
$
            Rel OP_NAME -> OP_NAME -> Set OP_NAME
forall a. Ord a => Rel a -> a -> Set a
Rel.succs Rel OP_NAME
revReflTransClosureSortRel OP_NAME
topSort) [OP_NAME]
topSortsL

    -- Maps a SORT to the index of the connected Component
    connectedComponentsToMap :: [Set.Set SORT] -> Map.Map SORT Int
    connectedComponentsToMap :: [Set OP_NAME] -> Map OP_NAME Int
connectedComponentsToMap connectedComponents :: [Set OP_NAME]
connectedComponents =
      let indexedCCs :: [(Set OP_NAME, Int)]
indexedCCs = [Set OP_NAME] -> [Int] -> [(Set OP_NAME, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Set OP_NAME]
connectedComponents [1..]
      in  ((Set OP_NAME, Int) -> Map OP_NAME Int -> Map OP_NAME Int)
-> Map OP_NAME Int -> [(Set OP_NAME, Int)] -> Map OP_NAME Int
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (cc :: Set OP_NAME
cc, i :: Int
i) ccMap :: Map OP_NAME Int
ccMap ->
                  (OP_NAME -> Map OP_NAME Int -> Map OP_NAME Int)
-> Map OP_NAME Int -> Set OP_NAME -> Map OP_NAME Int
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.foldr (\ sort :: OP_NAME
sort ccMap' :: Map OP_NAME Int
ccMap' ->
                              OP_NAME -> Int -> Map OP_NAME Int -> Map OP_NAME Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert OP_NAME
sort Int
i Map OP_NAME Int
ccMap'
                            ) Map OP_NAME Int
ccMap Set OP_NAME
cc
                ) Map OP_NAME Int
forall k a. Map k a
Map.empty [(Set OP_NAME, Int)]
indexedCCs

    addOpIfConflicting :: Map.Map SORT Int -> OP_NAME -> Set.Set OpType
                       -> Map.Map (OP_NAME, OpType) OP_NAME
                       -> Map.Map (OP_NAME, OpType) OP_NAME
    addOpIfConflicting :: Map OP_NAME Int
-> OP_NAME
-> Set OpType
-> Map (OP_NAME, OpType) OP_NAME
-> Map (OP_NAME, OpType) OP_NAME
addOpIfConflicting connectedComponentMap :: Map OP_NAME Int
connectedComponentMap opName :: OP_NAME
opName opTypes :: Set OpType
opTypes conflicts :: Map (OP_NAME, OpType) OP_NAME
conflicts =
      let opTypesL :: [OpType]
opTypesL = Set OpType -> [OpType]
forall a. Set a -> [a]
Set.toList Set OpType
opTypes
          opTypeCombinations :: [(OpType, OpType)]
opTypeCombinations = [(OpType
x,OpType
y) | OpType
x <- [OpType]
opTypesL, OpType
y <- [OpType]
opTypesL, OpType
x OpType -> OpType -> Bool
forall a. Ord a => a -> a -> Bool
< OpType
y]
      in  ((OpType, OpType)
 -> Map (OP_NAME, OpType) OP_NAME -> Map (OP_NAME, OpType) OP_NAME)
-> Map (OP_NAME, OpType) OP_NAME
-> [(OpType, OpType)]
-> Map (OP_NAME, OpType) OP_NAME
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (OpType, OpType)
-> Map (OP_NAME, OpType) OP_NAME -> Map (OP_NAME, OpType) OP_NAME
addIfConflicting Map (OP_NAME, OpType) OP_NAME
conflicts [(OpType, OpType)]
opTypeCombinations
      where
        addIfConflicting :: (OpType, OpType)
                         -> Map.Map (OP_NAME, OpType) OP_NAME
                         -> Map.Map (OP_NAME, OpType) OP_NAME
        addIfConflicting :: (OpType, OpType)
-> Map (OP_NAME, OpType) OP_NAME -> Map (OP_NAME, OpType) OP_NAME
addIfConflicting (t1 :: OpType
t1, t2 :: OpType
t2) conflicts' :: Map (OP_NAME, OpType) OP_NAME
conflicts' =
          if OpType -> OpType -> Bool
isConflicting OpType
t1 OpType
t2
          then (OP_NAME, OpType)
-> OP_NAME
-> Map (OP_NAME, OpType) OP_NAME
-> Map (OP_NAME, OpType) OP_NAME
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (OP_NAME
opName, OpType
t1) (OpType -> OP_NAME
renameCurrentOp OpType
t1) (Map (OP_NAME, OpType) OP_NAME -> Map (OP_NAME, OpType) OP_NAME)
-> Map (OP_NAME, OpType) OP_NAME -> Map (OP_NAME, OpType) OP_NAME
forall a b. (a -> b) -> a -> b
$
                 (OP_NAME, OpType)
-> OP_NAME
-> Map (OP_NAME, OpType) OP_NAME
-> Map (OP_NAME, OpType) OP_NAME
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (OP_NAME
opName, OpType
t2) (OpType -> OP_NAME
renameCurrentOp OpType
t2) Map (OP_NAME, OpType) OP_NAME
conflicts'
          else if OpType -> OpType -> Bool
hasAllArgsInSameCC OpType
t1 OpType
t2
               then let greaterOpType :: OpType
greaterOpType = if OpType -> OpType -> Bool
leqOpType OpType
t1 OpType
t2 then OpType
t2 else OpType
t1 in
                    (OP_NAME, OpType)
-> OP_NAME
-> Map (OP_NAME, OpType) OP_NAME
-> Map (OP_NAME, OpType) OP_NAME
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (OP_NAME
opName, OpType
t1) (OpType -> OP_NAME
renameCurrentOp OpType
greaterOpType) (Map (OP_NAME, OpType) OP_NAME -> Map (OP_NAME, OpType) OP_NAME)
-> Map (OP_NAME, OpType) OP_NAME -> Map (OP_NAME, OpType) OP_NAME
forall a b. (a -> b) -> a -> b
$
                      (OP_NAME, OpType)
-> OP_NAME
-> Map (OP_NAME, OpType) OP_NAME
-> Map (OP_NAME, OpType) OP_NAME
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (OP_NAME
opName, OpType
t2) (OpType -> OP_NAME
renameCurrentOp OpType
greaterOpType) Map (OP_NAME, OpType) OP_NAME
conflicts'
               else Map (OP_NAME, OpType) OP_NAME
conflicts'

        leqOpType :: OpType -> OpType -> Bool
        leqOpType :: OpType -> OpType -> Bool
leqOpType t1 :: OpType
t1 t2 :: OpType
t2 = ((OP_NAME, OP_NAME) -> Bool) -> [(OP_NAME, OP_NAME)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((OP_NAME -> OP_NAME -> Bool) -> (OP_NAME, OP_NAME) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((OP_NAME -> OP_NAME -> Bool) -> (OP_NAME, OP_NAME) -> Bool)
-> (OP_NAME -> OP_NAME -> Bool) -> (OP_NAME, OP_NAME) -> Bool
forall a b. (a -> b) -> a -> b
$ Sign f e -> OP_NAME -> OP_NAME -> Bool
forall f e. Sign f e -> OP_NAME -> OP_NAME -> Bool
leqSort Sign f e
sign) ([(OP_NAME, OP_NAME)] -> Bool) -> [(OP_NAME, OP_NAME)] -> Bool
forall a b. (a -> b) -> a -> b
$
          [OP_NAME] -> [OP_NAME] -> [(OP_NAME, OP_NAME)]
forall a b. [a] -> [b] -> [(a, b)]
zip (OpType -> [OP_NAME]
opArgs OpType
t1 [OP_NAME] -> [OP_NAME] -> [OP_NAME]
forall a. [a] -> [a] -> [a]
++ [OpType -> OP_NAME
opRes OpType
t1]) (OpType -> [OP_NAME]
opArgs OpType
t2 [OP_NAME] -> [OP_NAME] -> [OP_NAME]
forall a. [a] -> [a] -> [a]
++ [OpType -> OP_NAME
opRes OpType
t2])

        isConflicting :: OpType -> OpType -> Bool
        isConflicting :: OpType -> OpType -> Bool
isConflicting t1 :: OpType
t1 t2 :: OpType
t2 =
          OpType -> OpType -> Bool
hasAllArgsInSameCC OpType
t1 OpType
t2 Bool -> Bool -> Bool
&& Bool -> Bool
not (Sign f e -> OpType -> OpType -> Bool
forall f e. Sign f e -> OpType -> OpType -> Bool
leqF Sign f e
sign OpType
t1 OpType
t2 Bool -> Bool -> Bool
|| Sign f e -> OpType -> OpType -> Bool
forall f e. Sign f e -> OpType -> OpType -> Bool
leqF Sign f e
sign OpType
t2 OpType
t1)

        hasAllArgsInSameCC :: OpType -> OpType -> Bool
        hasAllArgsInSameCC :: OpType -> OpType -> Bool
hasAllArgsInSameCC t1 :: OpType
t1 t2 :: OpType
t2 =
          let sameNumberOfArgs :: Bool
sameNumberOfArgs = [OP_NAME] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (OpType -> [OP_NAME]
opArgs OpType
t1) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [OP_NAME] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (OpType -> [OP_NAME]
opArgs OpType
t2)
              allArgsInSameCC :: Bool
allArgsInSameCC =
                ((OP_NAME, OP_NAME) -> Bool) -> [(OP_NAME, OP_NAME)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Map OP_NAME Int -> (OP_NAME, OP_NAME) -> Bool
isInSameCC Map OP_NAME Int
connectedComponentMap) ([(OP_NAME, OP_NAME)] -> Bool) -> [(OP_NAME, OP_NAME)] -> Bool
forall a b. (a -> b) -> a -> b
$
                  [OP_NAME] -> [OP_NAME] -> [(OP_NAME, OP_NAME)]
forall a b. [a] -> [b] -> [(a, b)]
zip (OpType -> [OP_NAME]
opArgs OpType
t1) (OpType -> [OP_NAME]
opArgs OpType
t2)
          in Bool
sameNumberOfArgs Bool -> Bool -> Bool
&& Bool
allArgsInSameCC

        renameCurrentOp :: OpType -> OP_NAME
        renameCurrentOp :: OpType -> OP_NAME
renameCurrentOp opType :: OpType
opType =
          let argsS :: String
argsS =
                String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "_" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (OP_NAME -> String) -> [OP_NAME] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (ShowS
toAlphaNum ShowS -> (OP_NAME -> String) -> OP_NAME -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OP_NAME -> String
forall a. Show a => a -> String
show) ([OP_NAME] -> [String]) -> [OP_NAME] -> [String]
forall a b. (a -> b) -> a -> b
$ OpType -> [OP_NAME]
opArgs OpType
opType
              resultS :: String
resultS = ShowS
toAlphaNum ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ OP_NAME -> String
forall a. Show a => a -> String
show (OP_NAME -> String) -> OP_NAME -> String
forall a b. (a -> b) -> a -> b
$ OpType -> OP_NAME
opRes OpType
opType
              newOpNameS :: String
newOpNameS =
                ShowS
toAlphaNum (OP_NAME -> String
forall a. Show a => a -> String
show OP_NAME
opName) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
argsS String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
resultS
          in  OP_NAME
opName { getTokens :: [Token]
getTokens = [String -> Token
mkSimpleId String
newOpNameS] }

    addPredIfConflicting :: Map.Map SORT Int -> PRED_NAME -> Set.Set PredType
                         -> Map.Map (PRED_NAME, PredType) PRED_NAME
                         -> Map.Map (PRED_NAME, PredType) PRED_NAME
    addPredIfConflicting :: Map OP_NAME Int
-> OP_NAME
-> Set PredType
-> Map (OP_NAME, PredType) OP_NAME
-> Map (OP_NAME, PredType) OP_NAME
addPredIfConflicting connectedComponentMap :: Map OP_NAME Int
connectedComponentMap predName :: OP_NAME
predName predTypes :: Set PredType
predTypes conflicts :: Map (OP_NAME, PredType) OP_NAME
conflicts =
      let predTypesL :: [PredType]
predTypesL = Set PredType -> [PredType]
forall a. Set a -> [a]
Set.toList Set PredType
predTypes
          predTypeCombinations :: [(PredType, PredType)]
predTypeCombinations =
            [(PredType
x,PredType
y) | PredType
x <- [PredType]
predTypesL, PredType
y <- [PredType]
predTypesL, PredType
x PredType -> PredType -> Bool
forall a. Ord a => a -> a -> Bool
< PredType
y]
      in  ((PredType, PredType)
 -> Map (OP_NAME, PredType) OP_NAME
 -> Map (OP_NAME, PredType) OP_NAME)
-> Map (OP_NAME, PredType) OP_NAME
-> [(PredType, PredType)]
-> Map (OP_NAME, PredType) OP_NAME
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (PredType, PredType)
-> Map (OP_NAME, PredType) OP_NAME
-> Map (OP_NAME, PredType) OP_NAME
addIfConflicting Map (OP_NAME, PredType) OP_NAME
conflicts [(PredType, PredType)]
predTypeCombinations
      where
        addIfConflicting :: (PredType, PredType)
                         -> Map.Map (PRED_NAME, PredType) PRED_NAME
                         -> Map.Map (PRED_NAME, PredType) PRED_NAME
        addIfConflicting :: (PredType, PredType)
-> Map (OP_NAME, PredType) OP_NAME
-> Map (OP_NAME, PredType) OP_NAME
addIfConflicting (t1 :: PredType
t1, t2 :: PredType
t2) conflicts' :: Map (OP_NAME, PredType) OP_NAME
conflicts' =
          if PredType -> PredType -> Bool
isConflicting PredType
t1 PredType
t2
          then (OP_NAME, PredType)
-> OP_NAME
-> Map (OP_NAME, PredType) OP_NAME
-> Map (OP_NAME, PredType) OP_NAME
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (OP_NAME
predName, PredType
t1) (PredType -> OP_NAME
renameCurrentPred PredType
t1) (Map (OP_NAME, PredType) OP_NAME
 -> Map (OP_NAME, PredType) OP_NAME)
-> Map (OP_NAME, PredType) OP_NAME
-> Map (OP_NAME, PredType) OP_NAME
forall a b. (a -> b) -> a -> b
$
                 (OP_NAME, PredType)
-> OP_NAME
-> Map (OP_NAME, PredType) OP_NAME
-> Map (OP_NAME, PredType) OP_NAME
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (OP_NAME
predName, PredType
t2) (PredType -> OP_NAME
renameCurrentPred PredType
t2) Map (OP_NAME, PredType) OP_NAME
conflicts'
          else if PredType -> PredType -> Bool
hasAllArgsInSameCC PredType
t1 PredType
t2
               then let greaterPredType :: PredType
greaterPredType = if PredType -> PredType -> Bool
leqPredType PredType
t1 PredType
t2 then PredType
t2 else PredType
t1 in
                    (OP_NAME, PredType)
-> OP_NAME
-> Map (OP_NAME, PredType) OP_NAME
-> Map (OP_NAME, PredType) OP_NAME
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (OP_NAME
predName, PredType
t1) (PredType -> OP_NAME
renameCurrentPred PredType
greaterPredType) (Map (OP_NAME, PredType) OP_NAME
 -> Map (OP_NAME, PredType) OP_NAME)
-> Map (OP_NAME, PredType) OP_NAME
-> Map (OP_NAME, PredType) OP_NAME
forall a b. (a -> b) -> a -> b
$
                      (OP_NAME, PredType)
-> OP_NAME
-> Map (OP_NAME, PredType) OP_NAME
-> Map (OP_NAME, PredType) OP_NAME
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (OP_NAME
predName, PredType
t2) (PredType -> OP_NAME
renameCurrentPred PredType
greaterPredType) Map (OP_NAME, PredType) OP_NAME
conflicts'
               else Map (OP_NAME, PredType) OP_NAME
conflicts'

        isConflicting :: PredType -> PredType -> Bool
        isConflicting :: PredType -> PredType -> Bool
isConflicting t1 :: PredType
t1 t2 :: PredType
t2 =
          PredType -> PredType -> Bool
hasAllArgsInSameCC PredType
t1 PredType
t2 Bool -> Bool -> Bool
&& Bool -> Bool
not (Sign f e -> PredType -> PredType -> Bool
forall f e. Sign f e -> PredType -> PredType -> Bool
leqP Sign f e
sign PredType
t1 PredType
t2 Bool -> Bool -> Bool
|| Sign f e -> PredType -> PredType -> Bool
forall f e. Sign f e -> PredType -> PredType -> Bool
leqP Sign f e
sign PredType
t2 PredType
t1)

        leqPredType :: PredType -> PredType -> Bool
        leqPredType :: PredType -> PredType -> Bool
leqPredType t1 :: PredType
t1 t2 :: PredType
t2 = ((OP_NAME, OP_NAME) -> Bool) -> [(OP_NAME, OP_NAME)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((OP_NAME -> OP_NAME -> Bool) -> (OP_NAME, OP_NAME) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((OP_NAME -> OP_NAME -> Bool) -> (OP_NAME, OP_NAME) -> Bool)
-> (OP_NAME -> OP_NAME -> Bool) -> (OP_NAME, OP_NAME) -> Bool
forall a b. (a -> b) -> a -> b
$ Sign f e -> OP_NAME -> OP_NAME -> Bool
forall f e. Sign f e -> OP_NAME -> OP_NAME -> Bool
leqSort Sign f e
sign) ([(OP_NAME, OP_NAME)] -> Bool) -> [(OP_NAME, OP_NAME)] -> Bool
forall a b. (a -> b) -> a -> b
$
          [OP_NAME] -> [OP_NAME] -> [(OP_NAME, OP_NAME)]
forall a b. [a] -> [b] -> [(a, b)]
zip (PredType -> [OP_NAME]
predArgs PredType
t1) (PredType -> [OP_NAME]
predArgs PredType
t2)

        hasAllArgsInSameCC :: PredType -> PredType -> Bool
        hasAllArgsInSameCC :: PredType -> PredType -> Bool
hasAllArgsInSameCC t1 :: PredType
t1 t2 :: PredType
t2 =
          let sameNumberOfArgs :: Bool
sameNumberOfArgs = [OP_NAME] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (PredType -> [OP_NAME]
predArgs PredType
t1) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [OP_NAME] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (PredType -> [OP_NAME]
predArgs PredType
t2)
              allArgsInSameCC :: Bool
allArgsInSameCC =
                ((OP_NAME, OP_NAME) -> Bool) -> [(OP_NAME, OP_NAME)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Map OP_NAME Int -> (OP_NAME, OP_NAME) -> Bool
isInSameCC Map OP_NAME Int
connectedComponentMap) ([(OP_NAME, OP_NAME)] -> Bool) -> [(OP_NAME, OP_NAME)] -> Bool
forall a b. (a -> b) -> a -> b
$
                  [OP_NAME] -> [OP_NAME] -> [(OP_NAME, OP_NAME)]
forall a b. [a] -> [b] -> [(a, b)]
zip (PredType -> [OP_NAME]
predArgs PredType
t1) (PredType -> [OP_NAME]
predArgs PredType
t2)
          in Bool
sameNumberOfArgs Bool -> Bool -> Bool
&& Bool
allArgsInSameCC

        renameCurrentPred :: PredType -> PRED_NAME
        renameCurrentPred :: PredType -> OP_NAME
renameCurrentPred predType :: PredType
predType =
          let argsS :: String
argsS =
                String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "_" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (OP_NAME -> String) -> [OP_NAME] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (ShowS
toAlphaNum ShowS -> (OP_NAME -> String) -> OP_NAME -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OP_NAME -> String
forall a. Show a => a -> String
show) ([OP_NAME] -> [String]) -> [OP_NAME] -> [String]
forall a b. (a -> b) -> a -> b
$ PredType -> [OP_NAME]
predArgs PredType
predType
              newPredNameS :: String
newPredNameS = ShowS
toAlphaNum (OP_NAME -> String
forall a. Show a => a -> String
show OP_NAME
predName) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
argsS
          in  OP_NAME
predName { getTokens :: [Token]
getTokens = [String -> Token
mkSimpleId String
newPredNameS] }

    isInSameCC :: Map.Map SORT Int -> (SORT, SORT) -> Bool
    isInSameCC :: Map OP_NAME Int -> (OP_NAME, OP_NAME) -> Bool
isInSameCC connectedComponentMap :: Map OP_NAME Int
connectedComponentMap (s1 :: OP_NAME
s1, s2 :: OP_NAME
s2) =
      let cc1 :: Maybe Int
cc1 = OP_NAME -> Map OP_NAME Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup OP_NAME
s1 Map OP_NAME Int
connectedComponentMap
          cc2 :: Maybe Int
cc2 = OP_NAME -> Map OP_NAME Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup OP_NAME
s2 Map OP_NAME Int
connectedComponentMap
      in  Maybe Int
cc1 Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Int
cc2 Bool -> Bool -> Bool
&& Maybe Int
cc1 Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe Int
forall a. Maybe a
Nothing -- Nothing can not occur

    modifyOpMap :: Map.Map (OP_NAME, OpType) OP_NAME
                -> OP_NAME -> OpType -> OpMap -> OpMap
    modifyOpMap :: Map (OP_NAME, OpType) OP_NAME
-> OP_NAME
-> OpType
-> MapSet OP_NAME OpType
-> MapSet OP_NAME OpType
modifyOpMap renamedOps :: Map (OP_NAME, OpType) OP_NAME
renamedOps opName :: OP_NAME
opName opType :: OpType
opType opMap' :: MapSet OP_NAME OpType
opMap' =
      case (OP_NAME, OpType) -> Map (OP_NAME, OpType) OP_NAME -> Maybe OP_NAME
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (OP_NAME
opName, OpType
opType) Map (OP_NAME, OpType) OP_NAME
renamedOps of
        Nothing -> MapSet OP_NAME OpType
opMap'
        Just newOpName :: OP_NAME
newOpName -> OP_NAME -> OpType -> MapSet OP_NAME OpType -> MapSet OP_NAME OpType
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert OP_NAME
newOpName OpType
opType (MapSet OP_NAME OpType -> MapSet OP_NAME OpType)
-> MapSet OP_NAME OpType -> MapSet OP_NAME OpType
forall a b. (a -> b) -> a -> b
$
                            OP_NAME -> OpType -> MapSet OP_NAME OpType -> MapSet OP_NAME OpType
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.delete OP_NAME
opName OpType
opType MapSet OP_NAME OpType
opMap'

    modifyPredMap :: Map.Map (PRED_NAME, PredType) PRED_NAME
                  -> PRED_NAME -> PredType -> PredMap -> PredMap
    modifyPredMap :: Map (OP_NAME, PredType) OP_NAME
-> OP_NAME
-> PredType
-> MapSet OP_NAME PredType
-> MapSet OP_NAME PredType
modifyPredMap renamedPreds :: Map (OP_NAME, PredType) OP_NAME
renamedPreds predName :: OP_NAME
predName predType :: PredType
predType predMap' :: MapSet OP_NAME PredType
predMap' =
      case (OP_NAME, PredType)
-> Map (OP_NAME, PredType) OP_NAME -> Maybe OP_NAME
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (OP_NAME
predName, PredType
predType) Map (OP_NAME, PredType) OP_NAME
renamedPreds of
        Nothing -> MapSet OP_NAME PredType
predMap'
        Just newPredName :: OP_NAME
newPredName -> OP_NAME
-> PredType -> MapSet OP_NAME PredType -> MapSet OP_NAME PredType
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert OP_NAME
newPredName PredType
predType (MapSet OP_NAME PredType -> MapSet OP_NAME PredType)
-> MapSet OP_NAME PredType -> MapSet OP_NAME PredType
forall a b. (a -> b) -> a -> b
$
                              OP_NAME
-> PredType -> MapSet OP_NAME PredType -> MapSet OP_NAME PredType
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.delete OP_NAME
predName PredType
predType MapSet OP_NAME PredType
predMap'


translateSign :: (FormExtension f, Eq f)
              => CSign.Sign f e -> Result (TSign.Sign, [Named TSign.Sentence])
translateSign :: Sign f e -> Result (Sign, [Named Sentence])
translateSign caslSign :: Sign f e
caslSign =
  (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
tptpSign, [Named Sentence]
sentencesOfSorts [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence]
sentencesOfOps)
  where
    tptpSign :: TSign.Sign
    tptpSign :: Sign
tptpSign =
      let predicatesOfSorts :: Map Token (Set Int)
predicatesOfSorts =
            (OP_NAME -> Map Token (Set Int) -> Map Token (Set Int))
-> Map Token (Set Int) -> Set OP_NAME -> Map Token (Set Int)
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.foldr (\ sort :: OP_NAME
sort predicates' :: Map Token (Set Int)
predicates' ->
                        (Set Int -> Set Int -> Set Int)
-> Token -> Set Int -> Map Token (Set Int) -> Map Token (Set Int)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith
                          Set Int -> Set Int -> Set Int
forall a. Ord a => Set a -> Set a -> Set a
Set.union
                          (OP_NAME -> Token
predicateOfSort OP_NAME
sort)
                          (Int -> Set Int
forall a. a -> Set a
Set.singleton 1)
                          Map Token (Set Int)
predicates'
                      ) Map Token (Set Int)
forall k a. Map k a
Map.empty (Set OP_NAME -> Map Token (Set Int))
-> Set OP_NAME -> Map Token (Set Int)
forall a b. (a -> b) -> a -> b
$ Rel OP_NAME -> Set OP_NAME
forall a. Ord a => Rel a -> Set a
Rel.nodes (Rel OP_NAME -> Set OP_NAME) -> Rel OP_NAME -> Set OP_NAME
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel OP_NAME
forall f e. Sign f e -> Rel OP_NAME
sortRel Sign f e
caslSign
          constants :: Set Token
constants =
            (OP_NAME -> OpType -> Set Token -> Set Token)
-> Set Token -> MapSet OP_NAME OpType -> Set Token
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey (\ opName :: OP_NAME
opName opType :: OpType
opType constants' :: Set Token
constants' ->
                                 if [OP_NAME] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([OP_NAME] -> Bool) -> [OP_NAME] -> Bool
forall a b. (a -> b) -> a -> b
$ OpType -> [OP_NAME]
opArgs OpType
opType
                                 then Token -> Set Token -> Set Token
forall a. Ord a => a -> Set a -> Set a
Set.insert
                                        (OP_NAME -> Token
functionOfOp OP_NAME
opName)
                                        Set Token
constants'
                                 else Set Token
constants'
                               ) Set Token
forall a. Set a
Set.empty (MapSet OP_NAME OpType -> Set Token)
-> MapSet OP_NAME OpType -> Set Token
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet OP_NAME OpType
forall f e. Sign f e -> MapSet OP_NAME OpType
opMap Sign f e
caslSign
          -- numbers cannot be generated due to prefix "function_"
          propositions :: Set Token
propositions =
            (OP_NAME -> PredType -> Set Token -> Set Token)
-> Set Token -> MapSet OP_NAME PredType -> Set Token
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey (\ predName :: OP_NAME
predName predType :: PredType
predType propositions' :: Set Token
propositions' ->
                                 if [OP_NAME] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([OP_NAME] -> Bool) -> [OP_NAME] -> Bool
forall a b. (a -> b) -> a -> b
$ PredType -> [OP_NAME]
predArgs PredType
predType
                                 then Token -> Set Token -> Set Token
forall a. Ord a => a -> Set a -> Set a
Set.insert
                                        (OP_NAME -> Token
predicateOfPred OP_NAME
predName)
                                        Set Token
propositions'
                                 else Set Token
propositions'
                               ) Set Token
forall a. Set a
Set.empty (MapSet OP_NAME PredType -> Set Token)
-> MapSet OP_NAME PredType -> Set Token
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet OP_NAME PredType
forall f e. Sign f e -> MapSet OP_NAME PredType
predMap Sign f e
caslSign
          predicatesWithoutSorts :: Map Token (Set Int)
predicatesWithoutSorts =
            (OP_NAME -> PredType -> Map Token (Set Int) -> Map Token (Set Int))
-> Map Token (Set Int)
-> MapSet OP_NAME PredType
-> Map Token (Set Int)
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey (\ predName :: OP_NAME
predName predType :: PredType
predType predicates' :: Map Token (Set Int)
predicates' ->
                                 if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [OP_NAME] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([OP_NAME] -> Bool) -> [OP_NAME] -> Bool
forall a b. (a -> b) -> a -> b
$ PredType -> [OP_NAME]
predArgs PredType
predType
                                 then (Set Int -> Set Int -> Set Int)
-> Token -> Set Int -> Map Token (Set Int) -> Map Token (Set Int)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith
                                       Set Int -> Set Int -> Set Int
forall a. Ord a => Set a -> Set a -> Set a
Set.union
                                       (OP_NAME -> Token
predicateOfPred OP_NAME
predName)
                                       (Int -> Set Int
forall a. a -> Set a
Set.singleton (Int -> Set Int) -> Int -> Set Int
forall a b. (a -> b) -> a -> b
$ [OP_NAME] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([OP_NAME] -> Int) -> [OP_NAME] -> Int
forall a b. (a -> b) -> a -> b
$
                                         PredType -> [OP_NAME]
predArgs PredType
predType)
                                       Map Token (Set Int)
predicates'
                                 else Map Token (Set Int)
predicates'
                               ) Map Token (Set Int)
forall k a. Map k a
Map.empty (MapSet OP_NAME PredType -> Map Token (Set Int))
-> MapSet OP_NAME PredType -> Map Token (Set Int)
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet OP_NAME PredType
forall f e. Sign f e -> MapSet OP_NAME PredType
predMap Sign f e
caslSign
          predicates :: Map Token (Set Int)
predicates =
            (Set Int -> Set Int -> Set Int)
-> Map Token (Set Int)
-> Map Token (Set Int)
-> Map Token (Set Int)
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 Map Token (Set Int)
predicatesOfSorts Map Token (Set Int)
predicatesWithoutSorts
          functors :: Map Token (Set Int)
functors =
            (OP_NAME -> OpType -> Map Token (Set Int) -> Map Token (Set Int))
-> Map Token (Set Int)
-> MapSet OP_NAME OpType
-> Map Token (Set Int)
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey (\ opName :: OP_NAME
opName opType :: OpType
opType functors' :: Map Token (Set Int)
functors' ->
                                 if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [OP_NAME] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([OP_NAME] -> Bool) -> [OP_NAME] -> Bool
forall a b. (a -> b) -> a -> b
$ OpType -> [OP_NAME]
opArgs OpType
opType
                                 then (Set Int -> Set Int -> Set Int)
-> Token -> Set Int -> Map Token (Set Int) -> Map Token (Set Int)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith
                                        Set Int -> Set Int -> Set Int
forall a. Ord a => Set a -> Set a -> Set a
Set.union
                                        (OP_NAME -> Token
functionOfOp OP_NAME
opName)
                                        (Int -> Set Int
forall a. a -> Set a
Set.singleton (Int -> Set Int) -> Int -> Set Int
forall a b. (a -> b) -> a -> b
$ [OP_NAME] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([OP_NAME] -> Int) -> [OP_NAME] -> Int
forall a b. (a -> b) -> a -> b
$ OpType -> [OP_NAME]
opArgs OpType
opType)
                                        Map Token (Set Int)
functors'
                                 else Map Token (Set Int)
functors'
                               ) Map Token (Set Int)
forall k a. Map k a
Map.empty (MapSet OP_NAME OpType -> Map Token (Set Int))
-> MapSet OP_NAME OpType -> Map Token (Set Int)
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet OP_NAME OpType
forall f e. Sign f e -> MapSet OP_NAME OpType
opMap Sign f e
caslSign
      in  Sign
TSign.emptySign { constantSet :: Set Token
constantSet = Set Token
constants
                          , propositionSet :: Set Token
propositionSet = Set Token
propositions
                          , fofPredicateMap :: Map Token (Set Int)
fofPredicateMap = Map Token (Set Int)
predicates
                          , fofFunctorMap :: Map Token (Set Int)
fofFunctorMap = Map Token (Set Int)
functors
                          }

    sentencesOfSorts :: [Named TSign.Sentence]
    sentencesOfSorts :: [Named Sentence]
sentencesOfSorts =
      let sortMap :: Map OP_NAME (Set OP_NAME)
sortMap = Rel OP_NAME -> Map OP_NAME (Set OP_NAME)
forall a. Rel a -> Map a (Set a)
Rel.toMap (Rel OP_NAME -> Map OP_NAME (Set OP_NAME))
-> Rel OP_NAME -> Map OP_NAME (Set OP_NAME)
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel OP_NAME
forall f e. Sign f e -> Rel OP_NAME
sortRel Sign f e
caslSign
          emptySorts :: Set OP_NAME
emptySorts = Sign f e -> Set OP_NAME
forall f e. Sign f e -> Set OP_NAME
emptySortSet Sign f e
caslSign
          topSorts :: Set OP_NAME
topSorts = Rel OP_NAME -> Set OP_NAME
forall a. Ord a => Rel a -> Set a
Rel.mostRight (Rel OP_NAME -> Set OP_NAME) -> Rel OP_NAME -> Set OP_NAME
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel OP_NAME
forall f e. Sign f e -> Rel OP_NAME
sortRel Sign f e
caslSign
          subsortSentences :: [Named Sentence]
subsortSentences =
            (OP_NAME -> Set OP_NAME -> [Named Sentence] -> [Named Sentence])
-> [Named Sentence]
-> Map OP_NAME (Set OP_NAME)
-> [Named Sentence]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (Set OP_NAME
-> OP_NAME -> Set OP_NAME -> [Named Sentence] -> [Named Sentence]
createSubsortSentences Set OP_NAME
emptySorts) [] Map OP_NAME (Set OP_NAME)
sortMap
          topSortSentences :: [Named Sentence]
topSortSentences =
            (OP_NAME -> [Named Sentence] -> [Named Sentence])
-> [Named Sentence] -> Set OP_NAME -> [Named Sentence]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.foldr (Set OP_NAME -> OP_NAME -> [Named Sentence] -> [Named Sentence]
createTopSortSentences Set OP_NAME
topSorts) [] Set OP_NAME
topSorts
      in  [Named Sentence]
subsortSentences [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence]
topSortSentences

    createSubsortSentences :: Set.Set SORT -> SORT -> Set.Set SORT
                           -> [Named TSign.Sentence] -> [Named TSign.Sentence]
    createSubsortSentences :: Set OP_NAME
-> OP_NAME -> Set OP_NAME -> [Named Sentence] -> [Named Sentence]
createSubsortSentences emptySorts :: Set OP_NAME
emptySorts sort :: OP_NAME
sort supersorts :: Set OP_NAME
supersorts sentences :: [Named Sentence]
sentences =
      let subsortSentences :: [Named Sentence]
subsortSentences = (OP_NAME -> [Named Sentence] -> [Named Sentence])
-> [Named Sentence] -> Set OP_NAME -> [Named Sentence]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.foldr
            (\ supersort :: OP_NAME
supersort sens :: [Named Sentence]
sens -> OP_NAME -> OP_NAME -> Named Sentence
createSubsortSentence OP_NAME
supersort OP_NAME
sort Named Sentence -> [Named Sentence] -> [Named Sentence]
forall a. a -> [a] -> [a]
: [Named Sentence]
sens)
            [] Set OP_NAME
supersorts
          nonEmptySortsSentence :: [Named Sentence]
nonEmptySortsSentence =
            if OP_NAME -> Set OP_NAME -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member OP_NAME
sort Set OP_NAME
emptySorts
            then []
            else [OP_NAME -> Named Sentence
createNonEmptySortSentence OP_NAME
sort]
      in  [Named Sentence]
subsortSentences [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence]
nonEmptySortsSentence [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence]
sentences

    -- creates:
    -- fof(sort_SUBSORT_subsort_of_SORT, axiom, ! [X]: (SUBSORT(X) => SORT(X))).
    createSubsortSentence :: SORT -> SORT -> Named TSign.Sentence
    createSubsortSentence :: OP_NAME -> OP_NAME -> Named Sentence
createSubsortSentence sort :: OP_NAME
sort subsort :: OP_NAME
subsort =
      let varX :: Token
varX = Token -> Token
variableOfVar (Token -> Token) -> Token -> Token
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId "X"
          nameString :: String
nameString =
            "sign_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
toAlphaNum (OP_NAME -> String
forall a. Show a => a -> String
show OP_NAME
subsort) String -> ShowS
forall a. [a] -> [a] -> [a]
++
            "_subsort_of_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
toAlphaNum (OP_NAME -> String
forall a. Show a => a -> String
show OP_NAME
sort)
          name :: Name
name = Token -> Name
NameString (Token -> Name) -> Token -> Name
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId String
nameString
          formula :: FOF_unitary_formula
formula = FOF_quantified_formula -> FOF_unitary_formula
FOFUF_quantified (FOF_quantified_formula -> FOF_unitary_formula)
-> FOF_quantified_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$
            FOF_quantifier
-> [Token] -> FOF_unitary_formula -> FOF_quantified_formula
FOF_quantified_formula FOF_quantifier
ForAll [Token
varX] (FOF_unitary_formula -> FOF_quantified_formula)
-> FOF_unitary_formula -> FOF_quantified_formula
forall a b. (a -> b) -> a -> b
$
            FOF_logic_formula -> FOF_unitary_formula
FOFUF_logic (FOF_logic_formula -> FOF_unitary_formula)
-> FOF_logic_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_binary_formula -> FOF_logic_formula
FOFLF_binary (FOF_binary_formula -> FOF_logic_formula)
-> FOF_binary_formula -> FOF_logic_formula
forall a b. (a -> b) -> a -> b
$ FOF_binary_nonassoc -> FOF_binary_formula
FOFBF_nonassoc (FOF_binary_nonassoc -> FOF_binary_formula)
-> FOF_binary_nonassoc -> FOF_binary_formula
forall a b. (a -> b) -> a -> b
$
            Binary_connective
-> FOF_unitary_formula
-> FOF_unitary_formula
-> FOF_binary_nonassoc
FOF_binary_nonassoc
              Binary_connective
TAS.Implication (Token -> OP_NAME -> FOF_unitary_formula
sortOfX Token
varX OP_NAME
subsort) (Token -> OP_NAME -> FOF_unitary_formula
sortOfX Token
varX OP_NAME
sort)
          sentence :: Sentence
sentence = Name -> FOF_unitary_formula -> Sentence
fofUnitaryFormulaToAxiom Name
name FOF_unitary_formula
formula
      in  String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed String
nameString Sentence
sentence

    -- creates:
    -- fof(sign_non_empty_sort_SORTNAME, axiom, ? [X]: (SORT(X))).
    createNonEmptySortSentence :: SORT -> Named TSign.Sentence
    createNonEmptySortSentence :: OP_NAME -> Named Sentence
createNonEmptySortSentence sort :: OP_NAME
sort =
      let varX :: Token
varX = Token -> Token
variableOfVar (Token -> Token) -> Token -> Token
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId "X"
          nameString :: String
nameString = "sign_non_empty_sort_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
toAlphaNum (OP_NAME -> String
forall a. Show a => a -> String
show OP_NAME
sort)
          name :: Name
name = Token -> Name
NameString (Token -> Name) -> Token -> Name
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId String
nameString
          formula :: FOF_unitary_formula
formula = FOF_quantified_formula -> FOF_unitary_formula
FOFUF_quantified (FOF_quantified_formula -> FOF_unitary_formula)
-> FOF_quantified_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$
            FOF_quantifier
-> [Token] -> FOF_unitary_formula -> FOF_quantified_formula
FOF_quantified_formula FOF_quantifier
Exists [Token
varX] (FOF_unitary_formula -> FOF_quantified_formula)
-> FOF_unitary_formula -> FOF_quantified_formula
forall a b. (a -> b) -> a -> b
$
            FOF_logic_formula -> FOF_unitary_formula
FOFUF_logic (FOF_logic_formula -> FOF_unitary_formula)
-> FOF_logic_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_unitary_formula -> FOF_logic_formula
FOFLF_unitary (FOF_unitary_formula -> FOF_logic_formula)
-> FOF_unitary_formula -> FOF_logic_formula
forall a b. (a -> b) -> a -> b
$ Token -> OP_NAME -> FOF_unitary_formula
sortOfX Token
varX OP_NAME
sort
          sentence :: Sentence
sentence = Name -> FOF_unitary_formula -> Sentence
fofUnitaryFormulaToAxiom Name
name FOF_unitary_formula
formula
      in  String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed String
nameString Sentence
sentence

    createTopSortSentences :: Set.Set SORT -> SORT
                           -> [Named TSign.Sentence] -> [Named TSign.Sentence]
    createTopSortSentences :: Set OP_NAME -> OP_NAME -> [Named Sentence] -> [Named Sentence]
createTopSortSentences topSorts :: Set OP_NAME
topSorts sort :: OP_NAME
sort sentences :: [Named Sentence]
sentences =
      let otherTopSorts :: Set OP_NAME
otherTopSorts = OP_NAME -> Set OP_NAME -> Set OP_NAME
forall a. Ord a => a -> Set a -> Set a
Set.delete OP_NAME
sort Set OP_NAME
topSorts
      in  if Set OP_NAME -> Bool
forall a. Set a -> Bool
Set.null Set OP_NAME
otherTopSorts
          then []
          else Set OP_NAME -> OP_NAME -> Named Sentence
createTopSortSentence Set OP_NAME
otherTopSorts OP_NAME
sort Named Sentence -> [Named Sentence] -> [Named Sentence]
forall a. a -> [a] -> [a]
: [Named Sentence]
sentences
      where
        -- creates:
        -- fof(sign_topsort_SORT, axiom,
        --   ! [X]: (SORT(X) => ~ OTHER_SORT1(X) & ... & ~ OTHER_SORTn(X)).
        createTopSortSentence :: Set.Set SORT -> SORT -> Named TSign.Sentence
        createTopSortSentence :: Set OP_NAME -> OP_NAME -> Named Sentence
createTopSortSentence otherTopSorts :: Set OP_NAME
otherTopSorts sort' :: OP_NAME
sort' =
          let varX :: Token
varX = Token -> Token
variableOfVar (Token -> Token) -> Token -> Token
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId "X"
              nameString :: String
nameString = "sign_topsort_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
toAlphaNum (OP_NAME -> String
forall a. Show a => a -> String
show OP_NAME
sort')
              name :: Name
name = Token -> Name
NameString (Token -> Name) -> Token -> Name
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId String
nameString

              formula :: FOF_unitary_formula
formula = FOF_quantified_formula -> FOF_unitary_formula
FOFUF_quantified (FOF_quantified_formula -> FOF_unitary_formula)
-> FOF_quantified_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$
                FOF_quantifier
-> [Token] -> FOF_unitary_formula -> FOF_quantified_formula
FOF_quantified_formula FOF_quantifier
ForAll [Token
varX] (FOF_unitary_formula -> FOF_quantified_formula)
-> FOF_unitary_formula -> FOF_quantified_formula
forall a b. (a -> b) -> a -> b
$
                FOF_logic_formula -> FOF_unitary_formula
FOFUF_logic (FOF_logic_formula -> FOF_unitary_formula)
-> FOF_logic_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_binary_formula -> FOF_logic_formula
FOFLF_binary (FOF_binary_formula -> FOF_logic_formula)
-> FOF_binary_formula -> FOF_logic_formula
forall a b. (a -> b) -> a -> b
$ FOF_binary_nonassoc -> FOF_binary_formula
FOFBF_nonassoc (FOF_binary_nonassoc -> FOF_binary_formula)
-> FOF_binary_nonassoc -> FOF_binary_formula
forall a b. (a -> b) -> a -> b
$
                Binary_connective
-> FOF_unitary_formula
-> FOF_unitary_formula
-> FOF_binary_nonassoc
FOF_binary_nonassoc
                  Binary_connective
TAS.Implication
                  (Token -> OP_NAME -> FOF_unitary_formula
sortOfX Token
varX OP_NAME
sort') (FOF_unitary_formula -> FOF_binary_nonassoc)
-> FOF_unitary_formula -> FOF_binary_nonassoc
forall a b. (a -> b) -> a -> b
$
                  FOF_and_formula -> FOF_unitary_formula
unitaryFormulaAnd (FOF_and_formula -> FOF_unitary_formula)
-> FOF_and_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$
                  Set FOF_unitary_formula -> FOF_and_formula
forall a. Set a -> [a]
Set.toList (Set FOF_unitary_formula -> FOF_and_formula)
-> Set FOF_unitary_formula -> FOF_and_formula
forall a b. (a -> b) -> a -> b
$
                  (OP_NAME -> FOF_unitary_formula)
-> Set OP_NAME -> Set FOF_unitary_formula
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (FOF_unitary_formula -> FOF_unitary_formula
negateUnitaryFormula (FOF_unitary_formula -> FOF_unitary_formula)
-> (OP_NAME -> FOF_unitary_formula)
-> OP_NAME
-> FOF_unitary_formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> OP_NAME -> FOF_unitary_formula
sortOfX Token
varX) Set OP_NAME
otherTopSorts

              sentence :: Sentence
sentence = Name -> FOF_unitary_formula -> Sentence
fofUnitaryFormulaToAxiom Name
name FOF_unitary_formula
formula
          in  String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed String
nameString Sentence
sentence

    negateUnitaryFormula :: FOF_unitary_formula -> FOF_unitary_formula
    negateUnitaryFormula :: FOF_unitary_formula -> FOF_unitary_formula
negateUnitaryFormula f :: FOF_unitary_formula
f = FOF_unary_formula -> FOF_unitary_formula
FOFUF_unary (FOF_unary_formula -> FOF_unitary_formula)
-> FOF_unary_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ Unary_connective -> FOF_unitary_formula -> FOF_unary_formula
FOFUF_connective Unary_connective
NOT FOF_unitary_formula
f

    sentencesOfOps :: [Named TSign.Sentence]
    sentencesOfOps :: [Named Sentence]
sentencesOfOps =
      (OP_NAME -> Set OpType -> [Named Sentence] -> [Named Sentence])
-> [Named Sentence] -> Map OP_NAME (Set OpType) -> [Named Sentence]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey OP_NAME -> Set OpType -> [Named Sentence] -> [Named Sentence]
createSentencesOfOp [] (Map OP_NAME (Set OpType) -> [Named Sentence])
-> Map OP_NAME (Set OpType) -> [Named Sentence]
forall a b. (a -> b) -> a -> b
$ MapSet OP_NAME OpType -> Map OP_NAME (Set OpType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap (MapSet OP_NAME OpType -> Map OP_NAME (Set OpType))
-> MapSet OP_NAME OpType -> Map OP_NAME (Set OpType)
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet OP_NAME OpType
forall f e. Sign f e -> MapSet OP_NAME OpType
opMap Sign f e
caslSign
      where
        createSentencesOfOp :: OP_NAME -> Set.Set OpType
                            -> [Named TSign.Sentence] -> [Named TSign.Sentence]
        createSentencesOfOp :: OP_NAME -> Set OpType -> [Named Sentence] -> [Named Sentence]
createSentencesOfOp opName :: OP_NAME
opName opTypes :: Set OpType
opTypes sentences :: [Named Sentence]
sentences =
          -- Assign a new sentence name to each type of the op by adding a suffix
          let useNameSuffix :: Bool
useNameSuffix = Set OpType -> Int
forall a. Set a -> Int
Set.size Set OpType
opTypes Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1
              (sentencesOfThisOp :: [Named Sentence]
sentencesOfThisOp, _) = (OpType -> ([Named Sentence], Int) -> ([Named Sentence], Int))
-> ([Named Sentence], Int) -> Set OpType -> ([Named Sentence], Int)
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.foldr
                (\ opType :: OpType
opType (sens :: [Named Sentence]
sens, i :: Int
i) ->
                  (String -> OP_NAME -> OpType -> Named Sentence
createSentenceOfOp
                    (if Bool
useNameSuffix then "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
i :: Int) else "")
                    OP_NAME
opName OpType
opType Named Sentence -> [Named Sentence] -> [Named Sentence]
forall a. a -> [a] -> [a]
: [Named Sentence]
sens, Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1))
                ([], 1) Set OpType
opTypes
          in  [Named Sentence]
sentencesOfThisOp [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence]
sentences

        -- creates either:
        -- fof(sign_op_OPNAME, axiom, S(op)).
        -- or:
        -- fof(sign_op_OPNAME, axiom,
        --      ! [X1, ..., Xn]: S1(X1) & ... & Sn(Xn) => S(op(X1, ..., Xn))).
        createSentenceOfOp :: String -> OP_NAME -> OpType
                           -> Named TSign.Sentence
        createSentenceOfOp :: String -> OP_NAME -> OpType -> Named Sentence
createSentenceOfOp nameSuffix :: String
nameSuffix opName :: OP_NAME
opName opType :: OpType
opType =
          let nameString :: String
nameString =
                "sign_op" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nameSuffix String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
toAlphaNum (OP_NAME -> String
forall a. Show a => a -> String
show OP_NAME
opName)
              name :: Name
name = Token -> Name
NameString (Token -> Name) -> Token -> Name
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId String
nameString

              predicateResult :: Token
predicateResult = OP_NAME -> Token
predicateOfSort (OP_NAME -> Token) -> OP_NAME -> Token
forall a b. (a -> b) -> a -> b
$ OpType -> OP_NAME
opRes OpType
opType
              predicates :: [Token]
predicates = (OP_NAME -> Token) -> [OP_NAME] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map OP_NAME -> Token
predicateOfSort ([OP_NAME] -> [Token]) -> [OP_NAME] -> [Token]
forall a b. (a -> b) -> a -> b
$ OpType -> [OP_NAME]
opArgs OpType
opType
              variables :: [Token]
variables =
                (Int -> Token) -> [Int] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map (\ i :: Int
i -> Token -> Token
variableOfVar (Token -> Token) -> Token -> Token
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId (String -> Token) -> String -> Token
forall a b. (a -> b) -> a -> b
$ "X" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)
                  [1 .. [OP_NAME] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (OpType -> [OP_NAME]
opArgs OpType
opType)]
              function :: Token
function = OP_NAME -> Token
functionOfOp OP_NAME
opName

              functionAntecedent :: FOF_unitary_formula
functionAntecedent = FOF_and_formula -> FOF_unitary_formula
unitaryFormulaAnd (FOF_and_formula -> FOF_unitary_formula)
-> FOF_and_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$
                ((Token, Token) -> FOF_unitary_formula)
-> [(Token, Token)] -> FOF_and_formula
forall a b. (a -> b) -> [a] -> [b]
map (\ (v :: Token
v, p :: Token
p) ->
                      FOF_atomic_formula -> FOF_unitary_formula
FOFUF_atomic (FOF_atomic_formula -> FOF_unitary_formula)
-> FOF_atomic_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_plain_atomic_formula -> FOF_atomic_formula
FOFAT_plain (FOF_plain_atomic_formula -> FOF_atomic_formula)
-> FOF_plain_atomic_formula -> FOF_atomic_formula
forall a b. (a -> b) -> a -> b
$ Token -> [FOF_term] -> FOF_plain_atomic_formula
FOFPAF_predicate Token
p
                      [FOF_function_term -> FOF_term
FOFT_function (FOF_function_term -> FOF_term) -> FOF_function_term -> FOF_term
forall a b. (a -> b) -> a -> b
$ FOF_plain_term -> FOF_function_term
FOFFT_plain (FOF_plain_term -> FOF_function_term)
-> FOF_plain_term -> FOF_function_term
forall a b. (a -> b) -> a -> b
$ Token -> FOF_plain_term
FOFPT_constant (Token -> FOF_plain_term) -> Token -> FOF_plain_term
forall a b. (a -> b) -> a -> b
$ Token
v]) ([(Token, Token)] -> FOF_and_formula)
-> [(Token, Token)] -> FOF_and_formula
forall a b. (a -> b) -> a -> b
$
                  [Token] -> [Token] -> [(Token, Token)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Token]
variables [Token]
predicates
              functionConsequent :: FOF_unitary_formula
functionConsequent = FOF_atomic_formula -> FOF_unitary_formula
FOFUF_atomic (FOF_atomic_formula -> FOF_unitary_formula)
-> FOF_atomic_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_plain_atomic_formula -> FOF_atomic_formula
FOFAT_plain (FOF_plain_atomic_formula -> FOF_atomic_formula)
-> FOF_plain_atomic_formula -> FOF_atomic_formula
forall a b. (a -> b) -> a -> b
$
                Token -> [FOF_term] -> FOF_plain_atomic_formula
FOFPAF_predicate Token
predicateResult
                [FOF_function_term -> FOF_term
FOFT_function (FOF_function_term -> FOF_term) -> FOF_function_term -> FOF_term
forall a b. (a -> b) -> a -> b
$ FOF_plain_term -> FOF_function_term
FOFFT_plain (FOF_plain_term -> FOF_function_term)
-> FOF_plain_term -> FOF_function_term
forall a b. (a -> b) -> a -> b
$ Token -> [FOF_term] -> FOF_plain_term
FOFPT_functor Token
function ([FOF_term] -> FOF_plain_term) -> [FOF_term] -> FOF_plain_term
forall a b. (a -> b) -> a -> b
$
                  (Token -> FOF_term) -> [Token] -> [FOF_term]
forall a b. (a -> b) -> [a] -> [b]
map Token -> FOF_term
FOFT_variable [Token]
variables]

              unitaryFormulaConstant :: FOF_unitary_formula
unitaryFormulaConstant = FOF_atomic_formula -> FOF_unitary_formula
FOFUF_atomic (FOF_atomic_formula -> FOF_unitary_formula)
-> FOF_atomic_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_plain_atomic_formula -> FOF_atomic_formula
FOFAT_plain (FOF_plain_atomic_formula -> FOF_atomic_formula)
-> FOF_plain_atomic_formula -> FOF_atomic_formula
forall a b. (a -> b) -> a -> b
$
                Token -> [FOF_term] -> FOF_plain_atomic_formula
FOFPAF_predicate Token
predicateResult
                [FOF_function_term -> FOF_term
FOFT_function (FOF_function_term -> FOF_term) -> FOF_function_term -> FOF_term
forall a b. (a -> b) -> a -> b
$ FOF_plain_term -> FOF_function_term
FOFFT_plain (FOF_plain_term -> FOF_function_term)
-> FOF_plain_term -> FOF_function_term
forall a b. (a -> b) -> a -> b
$ Token -> FOF_plain_term
FOFPT_constant (Token -> FOF_plain_term) -> Token -> FOF_plain_term
forall a b. (a -> b) -> a -> b
$ Token
function]

              unitaryFormulaFunction :: FOF_unitary_formula
unitaryFormulaFunction = FOF_quantified_formula -> FOF_unitary_formula
FOFUF_quantified (FOF_quantified_formula -> FOF_unitary_formula)
-> FOF_quantified_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$
                FOF_quantifier
-> [Token] -> FOF_unitary_formula -> FOF_quantified_formula
FOF_quantified_formula FOF_quantifier
ForAll [Token]
variables (FOF_unitary_formula -> FOF_quantified_formula)
-> FOF_unitary_formula -> FOF_quantified_formula
forall a b. (a -> b) -> a -> b
$
                FOF_logic_formula -> FOF_unitary_formula
FOFUF_logic (FOF_logic_formula -> FOF_unitary_formula)
-> FOF_logic_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_binary_formula -> FOF_logic_formula
FOFLF_binary (FOF_binary_formula -> FOF_logic_formula)
-> FOF_binary_formula -> FOF_logic_formula
forall a b. (a -> b) -> a -> b
$ FOF_binary_nonassoc -> FOF_binary_formula
FOFBF_nonassoc (FOF_binary_nonassoc -> FOF_binary_formula)
-> FOF_binary_nonassoc -> FOF_binary_formula
forall a b. (a -> b) -> a -> b
$
                Binary_connective
-> FOF_unitary_formula
-> FOF_unitary_formula
-> FOF_binary_nonassoc
FOF_binary_nonassoc
                  Binary_connective
TAS.Implication FOF_unitary_formula
functionAntecedent FOF_unitary_formula
functionConsequent

              formula :: FOF_unitary_formula
formula =
                if [Token] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Token]
variables
                then FOF_unitary_formula
unitaryFormulaConstant
                else FOF_unitary_formula
unitaryFormulaFunction
              sentenceTptp :: Sentence
sentenceTptp = Name -> FOF_unitary_formula -> Sentence
fofUnitaryFormulaToAxiom Name
name FOF_unitary_formula
formula
          in  String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed String
nameString Sentence
sentenceTptp

sortOfX :: TAS.Variable -> SORT -> FOF_unitary_formula
sortOfX :: Token -> OP_NAME -> FOF_unitary_formula
sortOfX var :: Token
var s :: OP_NAME
s = FOF_atomic_formula -> FOF_unitary_formula
FOFUF_atomic (FOF_atomic_formula -> FOF_unitary_formula)
-> FOF_atomic_formula -> FOF_unitary_formula
forall a b. (a -> b) -> a -> b
$ FOF_plain_atomic_formula -> FOF_atomic_formula
FOFAT_plain (FOF_plain_atomic_formula -> FOF_atomic_formula)
-> FOF_plain_atomic_formula -> FOF_atomic_formula
forall a b. (a -> b) -> a -> b
$
  Token -> [FOF_term] -> FOF_plain_atomic_formula
FOFPAF_predicate (OP_NAME -> Token
predicateOfSort OP_NAME
s) [Token -> FOF_term
FOFT_variable Token
var]

functionOfOp :: OP_NAME -> TAS.TPTP_functor
functionOfOp :: OP_NAME -> Token
functionOfOp opName :: OP_NAME
opName =
  let functionName :: String
functionName = "op_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
toAlphaNum (OP_NAME -> String
forall a. Show a => a -> String
show OP_NAME
opName)
  in  String -> Token
mkSimpleId String
functionName

predicateOfPred :: PRED_NAME -> TAS.Predicate
predicateOfPred :: OP_NAME -> Token
predicateOfPred predName :: OP_NAME
predName =
  let predicateName :: String
predicateName = "pred_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
toAlphaNum (OP_NAME -> String
forall a. Show a => a -> String
show OP_NAME
predName)
  in  String -> Token
mkSimpleId String
predicateName

predicateOfSort :: SORT -> TAS.Predicate
predicateOfSort :: OP_NAME -> Token
predicateOfSort s :: OP_NAME
s =
  let predicateName :: String
predicateName = "sort_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
toAlphaNum (OP_NAME -> String
forall a. Show a => a -> String
show OP_NAME
s)
  in  String -> Token
mkSimpleId String
predicateName

variableOfVar :: VAR -> TAS.Variable
variableOfVar :: Token -> Token
variableOfVar var :: Token
var =
  let varName :: String
varName = "VAR_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
toAlphaNum (Token -> String
forall a. Show a => a -> String
show Token
var)
  in  String -> Token
mkSimpleId String
varName

toAlphaNum :: String -> String
toAlphaNum :: ShowS
toAlphaNum = (Char -> String) -> ShowS
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
toAlphaNumC
  where
    toAlphaNumC :: Char -> String
    toAlphaNumC :: Char -> String
toAlphaNumC c :: Char
c = case Char
c of
      '+' -> "PLUS"
      '-' -> "MINUS"
      '/' -> "SLASH"
      '\\' -> "BACKSLASH"
      '%' -> "PERCENT"
      '<' -> "OPEN"
      '>' -> "CLOSE"
      '~' -> "TILDE"
      '=' -> "EQ"
      '*' -> "STAR"
      '\'' -> "PRIME"
      '\"' -> "QUOTE"
      ' ' -> "_"
      '_' -> "_"
      _ -> if Char -> Bool
isAlphaNum Char
c then [Char
c] else 'U' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> ShowS
forall a. (Integral a, Show a) => a -> ShowS
showHex (Char -> Int
ord Char
c) ""