{-# 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 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 = "TPTP_FOF"
-- | The identity of the comorphisms
data GenSuleCFOL2TPTP = GenSuleCFOL2TPTP deriving Show
suleCFOL2TPTP :: GenSuleCFOL2TPTP
suleCFOL2TPTP = GenSuleCFOL2TPTP
-- | TPTP theories
type TPTPTheory = (TSign.Sign, [Named Sentence])
instance Language GenSuleCFOL2TPTP where
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 () ()
sourceLogic GenSuleCFOL2TPTP = CASL
sourceSublogic GenSuleCFOL2TPTP = SL.cFol
{ sub_features = LocFilSub
, cons_features = NoSortGen
, has_empty_sorts = True }
targetLogic GenSuleCFOL2TPTP = TPTP.Logic_TPTP.TPTP
mapSublogic _ _ = Just FOF
map_theory GenSuleCFOL2TPTP = transTheory
has_model_expansion GenSuleCFOL2TPTP = True
transTheory :: (FormExtension f, Eq f)
=> (CSign.Sign f e, [Named (FORMULA f)])
-> Result TPTPTheory
transTheory (sign, sens) = do
let signWithRenamings@(preparedSign, _, _) = prepareSign sign
let preparedSens = map prepareNamedFormula sens
(tptpSign, signSentences) <- translateSign preparedSign
translatedSentences <- mapM (translateNamedFormula signWithRenamings) preparedSens
return (tptpSign, signSentences ++ translatedSentences)
prepareNamedFormula :: (FormExtension f, Eq f)
=> Named (FORMULA f) -> Named (FORMULA f)
prepareNamedFormula formula =
let expandedFormula =
codeOutConditionalF id $ -- Expand conditionals
codeOutUniqueExtF id id $ -- Expand "exists!" quantification
AS_Annotation.sentence formula
in formula { AS_Annotation.sentence = expandedFormula }
translateNamedFormula :: (FormExtension f, Eq f)
=> SignWithRenamings f e
-> Named (FORMULA f) -> Result (Named TSign.Sentence)
translateNamedFormula signWithRenamings x = do
let nameS = toAlphaNum (map toLower $ senAttr x)
translated <-
translateFormula signWithRenamings nameS (isAxiom x) $
return $ x { senAttr = nameS
, AS_Annotation.sentence = translated
}
translateFormula :: forall e f . (FormExtension f, Eq f)
=> SignWithRenamings f e -> String -> Bool -> FORMULA f
-> Result TSign.Sentence
translateFormula signWithRenamings nameS isAxiom' formula = do
let name = NameString $ mkSimpleId nameS
fofFormula <- toUnitaryFormula formula
return $ if isAxiom'
then fofUnitaryFormulaToAxiom name fofFormula
else fofUnitaryFormulaToConjecture name fofFormula
where
toUnitaryFormula :: (FormExtension f, Eq f)
=> FORMULA f
-> Result FOF_unitary_formula
toUnitaryFormula x = case x of
Quantification q vars f _ -> do
let fofVars = translateVarDecls vars
let variableList = map fst fofVars
let variableDeclaration =
unitaryFormulaAnd $ map (uncurry sortOfX) fofVars
fofF <- toUnitaryFormula f
case q of
Universal ->
let implication =
FOFUF_logic $ FOFLF_binary $ FOFBF_nonassoc $
FOF_binary_nonassoc TAS.Implication variableDeclaration fofF
in return $ FOFUF_quantified $
FOF_quantified_formula ForAll variableList implication
Existential ->
let conjunction = unitaryFormulaAnd [variableDeclaration, fofF]
in return $ FOFUF_quantified $
FOF_quantified_formula Exists variableList conjunction
-- Has been resolved/removed by prepareNamedFormula:
Unique_existential ->
fail "SuleCFOL2TPTP: Unique_existential occurred where it cannot occur. This is a bug in Hets."
Junction Con fs _ -> do
fofs <- mapM toUnitaryFormula fs
return $ unitaryFormulaAnd fofs
Junction Dis fs _ -> do
fofs <- mapM toUnitaryFormula fs
return $ unitaryFormulaOr fofs
Relation f1 CAS.Implication f2 _ -> do
fof1 <- toUnitaryFormula f1
fof2 <- toUnitaryFormula f2
return $ FOFUF_logic $ FOFLF_binary $ FOFBF_nonassoc $
FOF_binary_nonassoc TAS.Implication fof1 fof2
-- For some reason, "f2 if f1" is saved as "Relation f1 RevImpl f2 _"
Relation f1 RevImpl f2 _ -> do
fof1 <- toUnitaryFormula f1
fof2 <- toUnitaryFormula f2
-- Flip the formulae:
return $ FOFUF_logic $ FOFLF_binary $ FOFBF_nonassoc $
FOF_binary_nonassoc ReverseImplication fof2 fof1
Relation f1 CAS.Equivalence f2 _ -> do
fof1 <- toUnitaryFormula f1
fof2 <- toUnitaryFormula f2
return $ FOFUF_logic $ FOFLF_binary $ FOFBF_nonassoc $
FOF_binary_nonassoc TAS.Equivalence fof1 fof2
Negation f _ -> do
fofF <- toUnitaryFormula f
return $ FOFUF_unary $ FOFUF_connective NOT fofF
Atom True _ ->
return $ FOFUF_atomic $ FOFAT_defined $ FOFDAF_plain $
FOFDPF_proposition $ TPTP_true
Atom False _ ->
return $ FOFUF_atomic $ FOFAT_defined $ FOFDAF_plain $
FOFDPF_proposition $ TPTP_false
Predication predSymb terms _ -> do
predName <- case predSymb of
Pred_name _ ->
fail "SuleCFOL2TPTP: An unqualified predicate has been detected. This is a bug in Hets."
Qual_pred_name predName (Pred_type args _) _ ->
return $ lookupPredName signWithRenamings predName $
PredType { predArgs = args }
let predicate = predicateOfPred predName
args <- mapM (translateTerm signWithRenamings) terms
case args of
[] -> return $ FOFUF_atomic $ FOFAT_plain $ FOFPAF_proposition predicate
_ -> return $ FOFUF_atomic $ FOFAT_plain $ FOFPAF_predicate predicate args
-- There is no Equation t1 Existl t2 in SuleCFOL
Equation t1 Strong t2 _ -> do
fofTerm1 <- translateTerm signWithRenamings t1
fofTerm2 <- translateTerm signWithRenamings t2
return $ FOFUF_atomic $ FOFAT_defined $ FOFDAF_infix $
FOF_defined_infix_formula
Defined_infix_equality fofTerm1 fofTerm2
Membership term sort _ -> do
fofTerm <- translateTerm signWithRenamings term
return $ FOFUF_atomic $ FOFAT_plain $
FOFPAF_predicate (predicateOfSort sort) [fofTerm]
-- Sort_gen_ax cannot be translated. Fail:
Sort_gen_ax _ _ -> fail "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
_ -> fail "SuleCFOL2TPTP: A formula that should not occur has occurred."
translateVarDecls :: [VAR_DECL] -> [(TAS.Variable, SORT)]
translateVarDecls = concatMap translateVarDecl
translateVarDecl :: VAR_DECL -> [(TAS.Variable, SORT)]
translateVarDecl x = case x of
Var_decl vars sort _ -> zip (map variableOfVar vars) $ repeat sort
unitaryFormulaAnd :: FOF_and_formula -> FOF_unitary_formula
unitaryFormulaAnd = FOFUF_logic . FOFLF_binary . FOFBF_assoc . FOFBA_and
unitaryFormulaOr :: FOF_or_formula -> FOF_unitary_formula
unitaryFormulaOr = FOFUF_logic . FOFLF_binary . FOFBF_assoc . FOFBA_or
translateTerm :: (FormExtension f, Eq f)
=> SignWithRenamings f e
-> TERM f
-> Result TAS.FOF_term
translateTerm signWithRenamings x = case x of
Qual_var var _ _ -> return $ FOFT_variable $ variableOfVar var
Application opSymb terms _ -> do
opName <- case opSymb of
Op_name _ ->
fail "SuleCFOL2TPTP: An unqualified operation has been detected. This is a bug in Hets."
Qual_op_name opName (Op_type kind args res _) _ ->
return $ lookupOpName signWithRenamings opName $
OpType { opKind = kind, opArgs = args, opRes = res }
let function = functionOfOp opName
args <- mapM (translateTerm signWithRenamings) terms
case args of
[] -> return $ FOFT_function $ FOFFT_plain $ FOFPT_constant $ function
_ -> return $ FOFT_function $ FOFFT_plain $ FOFPT_functor function args
-- The sort can be ignored:
Sorted_term term _ _ -> translateTerm signWithRenamings term
-- Conditional has been resolved/removed in prepareNamedFormula
-- There is no Cast in SuleCFOL
-- Everything else cannot occur
_ -> fail "SuleCFOL2TPTP: A term that should not occur has occurred."
fofUnitaryFormulaToAxiom :: TAS.Name -> FOF_unitary_formula -> TSign.Sentence
fofUnitaryFormulaToAxiom name f =
let formula = FOFF_logic $ FOFLF_unitary f
in AF_FOF_Annotated $ FOF_annotated name Axiom formula (Annotations Nothing)
fofUnitaryFormulaToConjecture :: TAS.Name -> FOF_unitary_formula
fofUnitaryFormulaToConjecture name f =
let formula = FOFF_logic $ FOFLF_unitary f
in AF_FOF_Annotated $
FOF_annotated name Conjecture formula (Annotations Nothing)
lookupOpName :: (FormExtension f, Eq f)
=> SignWithRenamings f e -> OP_NAME -> OpType -> OP_NAME
lookupOpName (_, renamedOps, _) opName opType =
Map.findWithDefault opName (opName, opType) renamedOps
lookupPredName :: (FormExtension f, Eq f)
=> SignWithRenamings f e -> PRED_NAME -> PredType -> PRED_NAME
lookupPredName (_, _, renamedPreds) predName predType =
Map.findWithDefault predName (predName, predType) 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 =
let connectedComponents = gatherConnectedComponents sign
connectedComponentMap = connectedComponentsToMap connectedComponents
renamedOps =
Map.foldrWithKey (addOpIfConflicting connectedComponentMap) Map.empty $
MapSet.toMap $ opMap sign
renamedPreds =
Map.foldrWithKey (addPredIfConflicting connectedComponentMap) Map.empty $
MapSet.toMap $ predMap sign
renamedOpMap =
MapSet.foldWithKey (modifyOpMap renamedOps) (opMap sign) $ opMap sign
renamedPredMap =
MapSet.foldWithKey (modifyPredMap renamedPreds) (predMap sign) $ predMap sign
in (sign { opMap = renamedOpMap, predMap = renamedPredMap},
renamedOps,
renamedPreds)
where
gatherConnectedComponents :: (FormExtension f, Eq f)
=> CSign.Sign f e -> [Set.Set SORT]
gatherConnectedComponents sign' =
let topSortsL = Set.toList $ Rel.mostRight $ sortRel sign'
revReflTransClosureSortRel =
in map (\ topSort -> Set.insert topSort $
Rel.succs revReflTransClosureSortRel topSort) topSortsL
-- Maps a SORT to the index of the connected Component
connectedComponentsToMap connectedComponents =
let indexedCCs = zip connectedComponents [1..]
in foldr (\ (cc, i) ccMap ->
Set.foldr (\ sort ccMap' ->
Map.insert sort i ccMap'
) ccMap cc
) Map.empty indexedCCs
-> Map.Map (OP_NAME, OpType) OP_NAME
-> Map.Map (OP_NAME, OpType) OP_NAME
addOpIfConflicting connectedComponentMap opName opTypes conflicts =
let opTypesL = Set.toList opTypes
opTypeCombinations = [(x,y) | x <- opTypesL, y <- opTypesL, x < y]
in foldr addIfConflicting conflicts opTypeCombinations
where
addIfConflicting :: (OpType, OpType)
-> Map.Map (OP_NAME, OpType) OP_NAME
-> Map.Map (OP_NAME, OpType) OP_NAME
addIfConflicting (t1, t2) conflicts' =
if isConflicting t1 t2
then Map.insert (opName, t1) (renameCurrentOp t1) $
Map.insert (opName, t2) (renameCurrentOp t2) conflicts'
else if hasAllArgsInSameCC t1 t2
then let greaterOpType = if leqOpType t1 t2 then t2 else t1 in
Map.insert (opName, t1) (renameCurrentOp greaterOpType) $
Map.insert (opName, t2) (renameCurrentOp greaterOpType) conflicts'
else conflicts'
leqOpType :: OpType -> OpType -> Bool
leqOpType t1 t2 = all (uncurry $ leqSort sign) $
zip (opArgs t1 ++ [opRes t1]) (opArgs t2 ++ [opRes t2])
isConflicting :: OpType -> OpType -> Bool
isConflicting t1 t2 =
hasAllArgsInSameCC t1 t2 && not (leqF sign t1 t2 || leqF sign t2 t1)
hasAllArgsInSameCC :: OpType -> OpType -> Bool
hasAllArgsInSameCC t1 t2 =
let sameNumberOfArgs = length (opArgs t1) == length (opArgs t2)
allArgsInSameCC =
all (isInSameCC connectedComponentMap) $
zip (opArgs t1) (opArgs t2)
in sameNumberOfArgs && allArgsInSameCC
renameCurrentOp :: OpType -> OP_NAME
renameCurrentOp opType =
let argsS =
intercalate "_" $ map (toAlphaNum . show) $ opArgs opType
resultS = toAlphaNum $ show $ opRes opType
newOpNameS =
toAlphaNum (show opName) ++ "_" ++ argsS ++ "_" ++ resultS
in opName { getTokens = [mkSimpleId newOpNameS] }
-> Map.Map (PRED_NAME, PredType) PRED_NAME
-> Map.Map (PRED_NAME, PredType) PRED_NAME
addPredIfConflicting connectedComponentMap predName predTypes conflicts =
let predTypesL = Set.toList predTypes
predTypeCombinations =
[(x,y) | x <- predTypesL, y <- predTypesL, x < y]
in foldr addIfConflicting conflicts predTypeCombinations
where
addIfConflicting :: (PredType, PredType)
-> Map.Map (PRED_NAME, PredType) PRED_NAME
-> Map.Map (PRED_NAME, PredType) PRED_NAME
addIfConflicting (t1, t2) conflicts' =
if isConflicting t1 t2
then Map.insert (predName, t1) (renameCurrentPred t1) $
Map.insert (predName, t2) (renameCurrentPred t2) conflicts'
else if hasAllArgsInSameCC t1 t2
then let greaterPredType = if leqPredType t1 t2 then t2 else t1 in
Map.insert (predName, t1) (renameCurrentPred greaterPredType) $
Map.insert (predName, t2) (renameCurrentPred greaterPredType) conflicts'
else conflicts'
isConflicting :: PredType -> PredType -> Bool
isConflicting t1 t2 =
hasAllArgsInSameCC t1 t2 && not (leqP sign t1 t2 || leqP sign t2 t1)
leqPredType :: PredType -> PredType -> Bool
leqPredType t1 t2 = all (uncurry $ leqSort sign) $
zip (predArgs t1) (predArgs t2)
hasAllArgsInSameCC :: PredType -> PredType -> Bool
hasAllArgsInSameCC t1 t2 =
let sameNumberOfArgs = length (predArgs t1) == length (predArgs t2)
allArgsInSameCC =
all (isInSameCC connectedComponentMap) $
zip (predArgs t1) (predArgs t2)
in sameNumberOfArgs && allArgsInSameCC
renameCurrentPred :: PredType -> PRED_NAME
renameCurrentPred predType =
let argsS =
intercalate "_" $ map (toAlphaNum . show) $ predArgs predType
newPredNameS = toAlphaNum (show predName) ++ "_" ++ argsS
in predName { getTokens = [mkSimpleId newPredNameS] }
isInSameCC :: Map.Map SORT Int -> (SORT, SORT) -> Bool
isInSameCC connectedComponentMap (s1, s2) =
let cc1 = Map.lookup s1 connectedComponentMap
cc2 = Map.lookup s2 connectedComponentMap
in cc1 == cc2 && cc1 /= Nothing -- Nothing can not occur
modifyOpMap :: Map.Map (OP_NAME, OpType) OP_NAME
-> OP_NAME -> OpType -> OpMap -> OpMap
modifyOpMap renamedOps opName opType opMap' =
case Map.lookup (opName, opType) renamedOps of
Nothing -> opMap'
Just newOpName -> MapSet.insert newOpName opType $
MapSet.delete opName opType opMap'
modifyPredMap :: Map.Map (PRED_NAME, PredType) PRED_NAME
-> PRED_NAME -> PredType -> PredMap -> PredMap
modifyPredMap renamedPreds predName predType predMap' =
case Map.lookup (predName, predType) renamedPreds of
Nothing -> predMap'
Just newPredName -> MapSet.insert newPredName predType $
MapSet.delete predName predType predMap'
translateSign :: (FormExtension f, Eq f)
translateSign caslSign =
return (tptpSign, sentencesOfSorts ++ sentencesOfOps)
where
tptpSign :: TSign.Sign
tptpSign =
let predicatesOfSorts =
Set.foldr (\ sort predicates' ->
(predicateOfSort sort)
(Set.singleton 1)
predicates'
constants =
MapSet.foldWithKey (\ opName opType constants' ->
if null $ opArgs opType
then Set.insert
(functionOfOp opName)
constants'
else constants'
) Set.empty $ opMap caslSign
-- numbers cannot be generated due to prefix "function_"
propositions =
MapSet.foldWithKey (\ predName predType propositions' ->
if null $ predArgs predType
then Set.insert
(predicateOfPred predName)
propositions'
else propositions'
) Set.empty $ predMap caslSign
predicatesWithoutSorts =
MapSet.foldWithKey (\ predName predType predicates' ->
if not $ null $ predArgs predType
then Map.insertWith
(predicateOfPred predName)
(Set.singleton $ length $
predArgs predType)
predicates'
else predicates'
) Map.empty $ predMap caslSign
predicates =
Map.unionWith Set.union predicatesOfSorts predicatesWithoutSorts
functors =
MapSet.foldWithKey (\ opName opType functors' ->
if not $ null $ opArgs opType
then Map.insertWith
(functionOfOp opName)
(Set.singleton $ length $ opArgs opType)
functors'
else functors'
) Map.empty $ opMap caslSign
in TSign.emptySign { constantSet = constants
, propositionSet = propositions
, fofPredicateMap = predicates
, fofFunctorMap = functors
}
sentencesOfSorts :: [Named TSign.Sentence]
sentencesOfSorts =
let sortMap = Rel.toMap $ sortRel caslSign
emptySorts = emptySortSet caslSign
topSorts = Rel.mostRight $ sortRel caslSign
subsortSentences =
Map.foldrWithKey (createSubsortSentences emptySorts) [] sortMap
topSortSentences =
Set.foldr (createTopSortSentences topSorts) [] topSorts
in subsortSentences ++ topSortSentences
-> [Named TSign.Sentence] -> [Named TSign.Sentence]
createSubsortSentences emptySorts sort supersorts sentences =
let subsortSentences = Set.foldr
(\ supersort sens -> createSubsortSentence supersort sort : sens)
[] supersorts
nonEmptySortsSentence =
if Set.member sort emptySorts
then []
else [createNonEmptySortSentence sort]
in subsortSentences ++ nonEmptySortsSentence ++ sentences
-- creates:
-- fof(sort_SUBSORT_subsort_of_SORT, axiom, ! [X]: (SUBSORT(X) => SORT(X))).
createSubsortSentence :: SORT -> SORT -> Named TSign.Sentence
createSubsortSentence sort subsort =
let varX = variableOfVar $ mkSimpleId "X"
nameString =
"sign_" ++ toAlphaNum (show subsort) ++
"_subsort_of_" ++ toAlphaNum (show sort)
name = NameString $ mkSimpleId nameString
formula = FOFUF_quantified $
FOF_quantified_formula ForAll [varX] $
FOFUF_logic $ FOFLF_binary $ FOFBF_nonassoc $
FOF_binary_nonassoc
TAS.Implication (sortOfX varX subsort) (sortOfX varX sort)
sentence = fofUnitaryFormulaToAxiom name formula
in makeNamed nameString sentence
-- creates:
-- fof(sign_non_empty_sort_SORTNAME, axiom, ? [X]: (SORT(X))).
createNonEmptySortSentence :: SORT -> Named TSign.Sentence
createNonEmptySortSentence sort =
let varX = variableOfVar $ mkSimpleId "X"
nameString = "sign_non_empty_sort_" ++ toAlphaNum (show sort)
name = NameString $ mkSimpleId nameString
formula = FOFUF_quantified $
FOF_quantified_formula Exists [varX] $
FOFUF_logic $ FOFLF_unitary $ sortOfX varX sort
sentence = fofUnitaryFormulaToAxiom name formula
in makeNamed nameString sentence
createTopSortSentences :: Set.Set SORT -> SORT
-> [Named TSign.Sentence] -> [Named TSign.Sentence]
createTopSortSentences topSorts sort sentences =
let otherTopSorts = Set.delete sort topSorts
in if Set.null otherTopSorts
then []
else createTopSortSentence otherTopSorts sort : 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 otherTopSorts sort' =
let varX = variableOfVar $ mkSimpleId "X"
nameString = "sign_topsort_" ++ toAlphaNum (show sort')
name = NameString $ mkSimpleId nameString
formula = FOFUF_quantified $
FOF_quantified_formula ForAll [varX] $
FOFUF_logic $ FOFLF_binary $ FOFBF_nonassoc $
FOF_binary_nonassoc
(sortOfX varX sort') $
unitaryFormulaAnd $
Set.map (negateUnitaryFormula . sortOfX varX) otherTopSorts
sentence = fofUnitaryFormulaToAxiom name formula
in makeNamed nameString sentence
negateUnitaryFormula :: FOF_unitary_formula -> FOF_unitary_formula
negateUnitaryFormula f = FOFUF_unary $ FOFUF_connective NOT f
sentencesOfOps :: [Named TSign.Sentence]
sentencesOfOps =
Map.foldrWithKey createSentencesOfOp [] $ MapSet.toMap $ opMap caslSign
where
createSentencesOfOp :: OP_NAME -> Set.Set OpType
-> [Named TSign.Sentence] -> [Named TSign.Sentence]
createSentencesOfOp opName opTypes sentences =
-- Assign a new sentence name to each type of the op by adding a suffix
let useNameSuffix = Set.size opTypes > 1
(sentencesOfThisOp, _) = Set.foldr
(\ opType (sens, i) ->
(createSentenceOfOp
(if useNameSuffix then "_" ++ show (i :: Int) else "")
opName opType : sens, i + 1))
([], 1) opTypes
in sentencesOfThisOp ++ 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 nameSuffix opName opType =
let nameString =
"sign_op" ++ nameSuffix ++ "_" ++ toAlphaNum (show opName)
name = NameString $ mkSimpleId nameString
predicateResult = predicateOfSort $ opRes opType
predicates = map predicateOfSort $ opArgs opType
variables =
map (\ i -> variableOfVar $ mkSimpleId $ "X" ++ show i)
[1 .. length (opArgs opType)]
function = functionOfOp opName
functionAntecedent = unitaryFormulaAnd $
map (\ (v, p) ->
FOFUF_atomic $ FOFAT_plain $ FOFPAF_predicate p
[FOFT_function $ FOFFT_plain $ FOFPT_constant $ v]) $
zip variables predicates
functionConsequent = FOFUF_atomic $ FOFAT_plain $
FOFPAF_predicate predicateResult
[FOFT_function $ FOFFT_plain $ FOFPT_functor function $
map FOFT_variable variables]
unitaryFormulaConstant = FOFUF_atomic $ FOFAT_plain $
FOFPAF_predicate predicateResult
[FOFT_function $ FOFFT_plain $ FOFPT_constant $ function]
unitaryFormulaFunction = FOFUF_quantified $
FOF_quantified_formula ForAll variables $
FOFUF_logic $ FOFLF_binary $ FOFBF_nonassoc $
FOF_binary_nonassoc
TAS.Implication functionAntecedent functionConsequent
formula =
if null variables
then unitaryFormulaConstant
else unitaryFormulaFunction
sentenceTptp = fofUnitaryFormulaToAxiom name formula
in makeNamed nameString sentenceTptp
sortOfX :: TAS.Variable -> SORT -> FOF_unitary_formula
sortOfX var s = FOFUF_atomic $ FOFAT_plain $
FOFPAF_predicate (predicateOfSort s) [FOFT_variable var]
functionOfOp :: OP_NAME -> TAS.TPTP_functor
functionOfOp opName =
let functionName = "op_" ++ toAlphaNum (show opName)
in mkSimpleId functionName
predicateOfPred :: PRED_NAME -> TAS.Predicate
predicateOfPred predName =
let predicateName = "pred_" ++ toAlphaNum (show predName)
in mkSimpleId predicateName
predicateOfSort :: SORT -> TAS.Predicate
predicateOfSort s =
let predicateName = "sort_" ++ toAlphaNum (show s)
in mkSimpleId predicateName
variableOfVar :: VAR -> TAS.Variable
variableOfVar var =
let varName = "VAR_" ++ toAlphaNum (show var)
in mkSimpleId varName
toAlphaNum :: String -> String
toAlphaNum = concatMap toAlphaNumC
where
toAlphaNumC :: Char -> String
toAlphaNumC c = case c of
'+' -> "PLUS"
'-' -> "MINUS"
'/' -> "SLASH"
'\\' -> "BACKSLASH"
'%' -> "PERCENT"
'<' -> "OPEN"
'>' -> "CLOSE"
'~' -> "TILDE"
'=' -> "EQ"
'*' -> "STAR"
'\'' -> "PRIME"
'\"' -> "QUOTE"
' ' -> "_"
'_' -> "_"
_ -> if isAlphaNum c then [c] else 'U' : showHex (ord c) ""