{- |
Module      :  ./SoftFOL/Conversions.hs
Description :  Functions to convert to internal SP* data structures.
Copyright   :  (c) Rene Wagner, Klaus Luettich, Uni Bremen 2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  provisional
Portability :  unknown

Functions to convert to internal SP* data structures.
-}

module SoftFOL.Conversions where

import Control.Exception
import Data.Time
import Data.Maybe
import Data.List

import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Common.Lib.Rel as Rel

import Common.AS_Annotation
import Common.Id
import Common.Utils (number)

import SoftFOL.Sign

{- |
  Converts a Sign to an initial (no axioms or goals) SPLogicalPart.
-}
signToSPLogicalPart :: Sign -> SPLogicalPart
signToSPLogicalPart :: Sign -> SPLogicalPart
signToSPLogicalPart s :: Sign
s =
    Bool -> SPLogicalPart -> SPLogicalPart
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Sign -> Bool
checkArities Sign
s)
               (SPLogicalPart
emptySPLogicalPart {symbolList :: Maybe SPSymbolList
symbolList = Maybe SPSymbolList
sList,
                                    declarationList :: Maybe [SPDeclaration]
declarationList = [SPDeclaration] -> Maybe [SPDeclaration]
forall a. a -> Maybe a
Just [SPDeclaration]
decList,
                                    formulaLists :: [SPFormulaList]
formulaLists = if [SPDeclaration] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SPDeclaration]
decList
                                                   then []
                                                   else [SPFormulaList
predArgRestrictions]
                                   }
               )
  where
    sList :: Maybe SPSymbolList
sList = if Rel SPIdentifier -> Bool
forall a. Rel a -> Bool
Rel.nullKeys (Sign -> Rel SPIdentifier
sortRel Sign
s) Bool -> Bool -> Bool
&& Map SPIdentifier (Set ([SPIdentifier], SPIdentifier)) -> Bool
forall k a. Map k a -> Bool
Map.null (Sign -> Map SPIdentifier (Set ([SPIdentifier], SPIdentifier))
funcMap Sign
s) Bool -> Bool -> Bool
&&
               Map SPIdentifier (Set [SPIdentifier]) -> Bool
forall k a. Map k a -> Bool
Map.null (Sign -> Map SPIdentifier (Set [SPIdentifier])
predMap Sign
s) Bool -> Bool -> Bool
&& Map SPIdentifier (Maybe Generated) -> Bool
forall k a. Map k a -> Bool
Map.null (Sign -> Map SPIdentifier (Maybe Generated)
sortMap Sign
s)
              then Maybe SPSymbolList
forall a. Maybe a
Nothing
              else SPSymbolList -> Maybe SPSymbolList
forall a. a -> Maybe a
Just SPSymbolList
emptySymbolList
                       { functions :: [SPSignSym]
functions =
                             ((SPIdentifier, Set ([SPIdentifier], SPIdentifier)) -> SPSignSym)
-> [(SPIdentifier, Set ([SPIdentifier], SPIdentifier))]
-> [SPSignSym]
forall a b. (a -> b) -> [a] -> [b]
map (\ (f :: SPIdentifier
f, ts :: Set ([SPIdentifier], SPIdentifier)
ts) ->
                                      SPSignSym :: SPIdentifier -> Int -> SPSignSym
SPSignSym {sym :: SPIdentifier
sym = SPIdentifier
f,
                                                 arity :: Int
arity = [SPIdentifier] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (([SPIdentifier], SPIdentifier) -> [SPIdentifier]
forall a b. (a, b) -> a
fst ([([SPIdentifier], SPIdentifier)] -> ([SPIdentifier], SPIdentifier)
forall a. [a] -> a
head
                                                            (Set ([SPIdentifier], SPIdentifier)
-> [([SPIdentifier], SPIdentifier)]
forall a. Set a -> [a]
Set.toList Set ([SPIdentifier], SPIdentifier)
ts)))})
                                     (Map SPIdentifier (Set ([SPIdentifier], SPIdentifier))
-> [(SPIdentifier, Set ([SPIdentifier], SPIdentifier))]
forall k a. Map k a -> [(k, a)]
Map.toList (Sign -> Map SPIdentifier (Set ([SPIdentifier], SPIdentifier))
funcMap Sign
s)),
                         predicates :: [SPSignSym]
predicates =
                             ((SPIdentifier, Set [SPIdentifier]) -> SPSignSym)
-> [(SPIdentifier, Set [SPIdentifier])] -> [SPSignSym]
forall a b. (a -> b) -> [a] -> [b]
map (\ (p :: SPIdentifier
p, ts :: Set [SPIdentifier]
ts) ->
                                      SPSignSym :: SPIdentifier -> Int -> SPSignSym
SPSignSym {sym :: SPIdentifier
sym = SPIdentifier
p,
                                                 arity :: Int
arity = [SPIdentifier] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([[SPIdentifier]] -> [SPIdentifier]
forall a. [a] -> a
head
                                                          (Set [SPIdentifier] -> [[SPIdentifier]]
forall a. Set a -> [a]
Set.toList Set [SPIdentifier]
ts))})
                                     (Map SPIdentifier (Set [SPIdentifier])
-> [(SPIdentifier, Set [SPIdentifier])]
forall k a. Map k a -> [(k, a)]
Map.toList (Sign -> Map SPIdentifier (Set [SPIdentifier])
predMap Sign
s)),
                         sorts :: [SPSignSym]
sorts = (SPIdentifier -> SPSignSym) -> [SPIdentifier] -> [SPSignSym]
forall a b. (a -> b) -> [a] -> [b]
map SPIdentifier -> SPSignSym
SPSimpleSignSym ([SPIdentifier] -> [SPSignSym]) -> [SPIdentifier] -> [SPSignSym]
forall a b. (a -> b) -> a -> b
$ Map SPIdentifier (Maybe Generated) -> [SPIdentifier]
forall k a. Map k a -> [k]
Map.keys (Map SPIdentifier (Maybe Generated) -> [SPIdentifier])
-> Map SPIdentifier (Maybe Generated) -> [SPIdentifier]
forall a b. (a -> b) -> a -> b
$ Sign -> Map SPIdentifier (Maybe Generated)
sortMap Sign
s }

    decList :: [SPDeclaration]
decList = if Sign -> Bool
singleSorted Sign
s Bool -> Bool -> Bool
&& [Maybe Generated] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Map SPIdentifier (Maybe Generated) -> [Maybe Generated]
forall k a. Map k a -> [a]
Map.elems (Map SPIdentifier (Maybe Generated) -> [Maybe Generated])
-> Map SPIdentifier (Maybe Generated) -> [Maybe Generated]
forall a b. (a -> b) -> a -> b
$ Sign -> Map SPIdentifier (Maybe Generated)
sortMap Sign
s) then []
                else [SPDeclaration]
subsortDecl [SPDeclaration] -> [SPDeclaration] -> [SPDeclaration]
forall a. [a] -> [a] -> [a]
++ [SPDeclaration]
termDecl [SPDeclaration] -> [SPDeclaration] -> [SPDeclaration]
forall a. [a] -> [a] -> [a]
++ [SPDeclaration]
predDecl [SPDeclaration] -> [SPDeclaration] -> [SPDeclaration]
forall a. [a] -> [a] -> [a]
++ [SPDeclaration]
genDecl

    subsortDecl :: [SPDeclaration]
subsortDecl = ((SPIdentifier, SPIdentifier) -> SPDeclaration)
-> [(SPIdentifier, SPIdentifier)] -> [SPDeclaration]
forall a b. (a -> b) -> [a] -> [b]
map (\ (a :: SPIdentifier
a, b :: SPIdentifier
b) -> SPSubsortDecl :: SPIdentifier -> SPIdentifier -> SPDeclaration
SPSubsortDecl {sortSymA :: SPIdentifier
sortSymA = SPIdentifier
a, sortSymB :: SPIdentifier
sortSymB = SPIdentifier
b})
                      (Rel SPIdentifier -> [(SPIdentifier, SPIdentifier)]
forall a. Rel a -> [(a, a)]
Rel.toList (Rel SPIdentifier -> Rel SPIdentifier
forall a. Ord a => Rel a -> Rel a
Rel.transReduce (Sign -> Rel SPIdentifier
sortRel Sign
s)))

    termDecl :: [SPDeclaration]
termDecl = ((SPIdentifier, Set ([SPIdentifier], SPIdentifier))
 -> [SPDeclaration])
-> [(SPIdentifier, Set ([SPIdentifier], SPIdentifier))]
-> [SPDeclaration]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SPIdentifier, Set ([SPIdentifier], SPIdentifier))
-> [SPDeclaration]
termDecls (Map SPIdentifier (Set ([SPIdentifier], SPIdentifier))
-> [(SPIdentifier, Set ([SPIdentifier], SPIdentifier))]
forall k a. Map k a -> [(k, a)]
Map.toList (Sign -> Map SPIdentifier (Set ([SPIdentifier], SPIdentifier))
funcMap Sign
s))

    termDecls :: (SPIdentifier, Set ([SPIdentifier], SPIdentifier))
-> [SPDeclaration]
termDecls (fsym :: SPIdentifier
fsym, tset :: Set ([SPIdentifier], SPIdentifier)
tset) = (([SPIdentifier], SPIdentifier) -> SPDeclaration)
-> [([SPIdentifier], SPIdentifier)] -> [SPDeclaration]
forall a b. (a -> b) -> [a] -> [b]
map (SPIdentifier -> ([SPIdentifier], SPIdentifier) -> SPDeclaration
toFDecl SPIdentifier
fsym) (Set ([SPIdentifier], SPIdentifier)
-> [([SPIdentifier], SPIdentifier)]
forall a. Set a -> [a]
Set.toList Set ([SPIdentifier], SPIdentifier)
tset)
    toFDecl :: SPIdentifier -> ([SPIdentifier], SPIdentifier) -> SPDeclaration
toFDecl fsym :: SPIdentifier
fsym (args :: [SPIdentifier]
args, ret :: SPIdentifier
ret) =
        if [SPIdentifier] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SPIdentifier]
args
        then SPTerm -> SPDeclaration
SPSimpleTermDecl (SPTerm -> SPDeclaration) -> SPTerm -> SPDeclaration
forall a b. (a -> b) -> a -> b
$ SPSymbol -> [SPTerm] -> SPTerm
compTerm (SPIdentifier -> SPSymbol
spSym SPIdentifier
ret) [SPSymbol -> SPTerm
simpTerm (SPSymbol -> SPTerm) -> SPSymbol -> SPTerm
forall a b. (a -> b) -> a -> b
$ SPIdentifier -> SPSymbol
spSym SPIdentifier
fsym]
        else let
            xTerm :: Int -> SPTerm
            xTerm :: Int -> SPTerm
xTerm i :: Int
i = SPSymbol -> SPTerm
simpTerm (SPSymbol -> SPTerm) -> SPSymbol -> SPTerm
forall a b. (a -> b) -> a -> b
$ String -> SPSymbol
mkSPCustomSymbol (String -> SPSymbol) -> String -> SPSymbol
forall a b. (a -> b) -> a -> b
$ 'X' Char -> String -> String
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
i
            in SPTermDecl :: [SPTerm] -> SPTerm -> SPDeclaration
SPTermDecl
               { termDeclTermList :: [SPTerm]
termDeclTermList =
                 ((SPIdentifier, Int) -> SPTerm)
-> [(SPIdentifier, Int)] -> [SPTerm]
forall a b. (a -> b) -> [a] -> [b]
map (\ (t :: SPIdentifier
t, i :: Int
i) -> SPSymbol -> [SPTerm] -> SPTerm
compTerm (SPIdentifier -> SPSymbol
spSym SPIdentifier
t) [Int -> SPTerm
xTerm Int
i]) ([(SPIdentifier, Int)] -> [SPTerm])
-> [(SPIdentifier, Int)] -> [SPTerm]
forall a b. (a -> b) -> a -> b
$ [SPIdentifier] -> [(SPIdentifier, Int)]
forall a. [a] -> [(a, Int)]
number [SPIdentifier]
args
               , termDeclTerm :: SPTerm
termDeclTerm = SPSymbol -> [SPTerm] -> SPTerm
compTerm (SPIdentifier -> SPSymbol
spSym SPIdentifier
ret) [SPSymbol -> [SPTerm] -> SPTerm
compTerm (SPIdentifier -> SPSymbol
spSym SPIdentifier
fsym)
                   ([SPTerm] -> SPTerm) -> [SPTerm] -> SPTerm
forall a b. (a -> b) -> a -> b
$ ((SPIdentifier, Int) -> SPTerm)
-> [(SPIdentifier, Int)] -> [SPTerm]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> SPTerm
xTerm (Int -> SPTerm)
-> ((SPIdentifier, Int) -> Int) -> (SPIdentifier, Int) -> SPTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SPIdentifier, Int) -> Int
forall a b. (a, b) -> b
snd) ([(SPIdentifier, Int)] -> [SPTerm])
-> [(SPIdentifier, Int)] -> [SPTerm]
forall a b. (a -> b) -> a -> b
$ [SPIdentifier] -> [(SPIdentifier, Int)]
forall a. [a] -> [(a, Int)]
number [SPIdentifier]
args] }
    predArgRestrictions :: SPFormulaList
predArgRestrictions =
          SPFormulaList :: SPOriginType -> [SPFormula] -> SPFormulaList
SPFormulaList { originType :: SPOriginType
originType = SPOriginType
SPOriginAxioms
                        , formulae :: [SPFormula]
formulae = (SPIdentifier -> Set [SPIdentifier] -> [SPFormula] -> [SPFormula])
-> [SPFormula]
-> Map SPIdentifier (Set [SPIdentifier])
-> [SPFormula]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey SPIdentifier -> Set [SPIdentifier] -> [SPFormula] -> [SPFormula]
toArgRestriction []
                                     (Map SPIdentifier (Set [SPIdentifier]) -> [SPFormula])
-> Map SPIdentifier (Set [SPIdentifier]) -> [SPFormula]
forall a b. (a -> b) -> a -> b
$ Sign -> Map SPIdentifier (Set [SPIdentifier])
predMap Sign
s
                        }
    toArgRestriction :: SPIdentifier -> Set [SPIdentifier] -> [SPFormula] -> [SPFormula]
toArgRestriction psym :: SPIdentifier
psym tset :: Set [SPIdentifier]
tset acc :: [SPFormula]
acc
        | Set [SPIdentifier] -> Bool
forall a. Set a -> Bool
Set.null Set [SPIdentifier]
tset = String -> [SPFormula]
forall a. (?callStack::CallStack) => String -> a
error
           "SoftFOL.Conversions.toArgRestriction: empty set"
        | Set [SPIdentifier] -> Int
forall a. Set a -> Int
Set.size Set [SPIdentifier]
tset Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 = [SPFormula]
acc [SPFormula] -> [SPFormula] -> [SPFormula]
forall a. [a] -> [a] -> [a]
++
            [SPFormula]
-> (SPTerm -> [SPFormula]) -> Maybe SPTerm -> [SPFormula]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe []
                  ((SPFormula -> [SPFormula] -> [SPFormula]
forall a. a -> [a] -> [a]
: []) (SPFormula -> [SPFormula])
-> (SPTerm -> SPFormula) -> SPTerm -> [SPFormula]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> SPTerm -> SPFormula
forall a s. a -> s -> SenAttr s a
makeNamed ("arg_restriction_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SPIdentifier -> String
tokStr SPIdentifier
psym))
                  ([SPDeclaration] -> Maybe SPDeclaration
forall a. [a] -> Maybe a
listToMaybe (SPIdentifier -> [SPIdentifier] -> [SPDeclaration]
toPDecl SPIdentifier
psym ([SPIdentifier] -> [SPDeclaration])
-> [SPIdentifier] -> [SPDeclaration]
forall a b. (a -> b) -> a -> b
$ [[SPIdentifier]] -> [SPIdentifier]
forall a. [a] -> a
head ([[SPIdentifier]] -> [SPIdentifier])
-> [[SPIdentifier]] -> [SPIdentifier]
forall a b. (a -> b) -> a -> b
$ Set [SPIdentifier] -> [[SPIdentifier]]
forall a. Set a -> [a]
Set.toList Set [SPIdentifier]
tset)
                    Maybe SPDeclaration
-> (SPDeclaration -> Maybe SPTerm) -> Maybe SPTerm
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SPDeclaration -> Maybe SPTerm
predDecl2Term)
        | Bool
otherwise = [SPFormula]
acc [SPFormula] -> [SPFormula] -> [SPFormula]
forall a. [a] -> [a] -> [a]
++
             let argLists :: [[SPIdentifier]]
argLists = Set [SPIdentifier] -> [[SPIdentifier]]
forall a. Set a -> [a]
Set.toList Set [SPIdentifier]
tset
             in [String -> SPTerm -> SPFormula
forall a s. a -> s -> SenAttr s a
makeNamed ("arg_restriction_o_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SPIdentifier -> String
tokStr SPIdentifier
psym) (SPTerm -> SPFormula) -> SPTerm -> SPFormula
forall a b. (a -> b) -> a -> b
$
                 SPIdentifier -> [[SPIdentifier]] -> SPTerm
makeTerm SPIdentifier
psym ([[SPIdentifier]] -> SPTerm) -> [[SPIdentifier]] -> SPTerm
forall a b. (a -> b) -> a -> b
$
                 ([[SPIdentifier]] -> [SPIdentifier] -> [[SPIdentifier]])
-> [[SPIdentifier]] -> [[SPIdentifier]] -> [[SPIdentifier]]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (([SPIdentifier] -> SPIdentifier -> [SPIdentifier])
-> [[SPIdentifier]] -> [SPIdentifier] -> [[SPIdentifier]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ((SPIdentifier -> [SPIdentifier] -> [SPIdentifier])
-> [SPIdentifier] -> SPIdentifier -> [SPIdentifier]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (:)))
                      ((SPIdentifier -> [SPIdentifier])
-> [SPIdentifier] -> [[SPIdentifier]]
forall a b. (a -> b) -> [a] -> [b]
map ([SPIdentifier] -> SPIdentifier -> [SPIdentifier]
forall a b. a -> b -> a
const []) ([SPIdentifier] -> [[SPIdentifier]])
-> [SPIdentifier] -> [[SPIdentifier]]
forall a b. (a -> b) -> a -> b
$ [[SPIdentifier]] -> [SPIdentifier]
forall a. [a] -> a
head [[SPIdentifier]]
argLists) [[SPIdentifier]]
argLists]

    makeTerm :: SPIdentifier -> [[SPIdentifier]] -> SPTerm
makeTerm psym :: SPIdentifier
psym tss :: [[SPIdentifier]]
tss =
        let varList :: [SPIdentifier]
varList = (SPIdentifier -> [SPIdentifier] -> SPIdentifier)
-> [SPIdentifier] -> [[SPIdentifier]] -> [SPIdentifier]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SPIdentifier -> [SPIdentifier] -> SPIdentifier
forall a b. a -> b -> a
const (SPIdentifier -> [SPIdentifier] -> [SPIdentifier]
genVarList SPIdentifier
psym ([SPIdentifier] -> [SPIdentifier])
-> [SPIdentifier] -> [SPIdentifier]
forall a b. (a -> b) -> a -> b
$ [SPIdentifier] -> [SPIdentifier]
forall a. Eq a => [a] -> [a]
nub ([SPIdentifier] -> [SPIdentifier])
-> [SPIdentifier] -> [SPIdentifier]
forall a b. (a -> b) -> a -> b
$ [[SPIdentifier]] -> [SPIdentifier]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[SPIdentifier]]
tss) [[SPIdentifier]]
tss
            varListTerms :: [SPTerm]
varListTerms = [SPIdentifier] -> [SPTerm]
spTerms [SPIdentifier]
varList
        in if [SPIdentifier] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SPIdentifier]
varList
           then String -> SPTerm
forall a. (?callStack::CallStack) => String -> a
error
             "SoftFOL.Conversions.makeTerm: no propositional constants"
           else SPQuantTerm :: SPQuantSym -> [SPTerm] -> SPTerm -> SPTerm
SPQuantTerm {
                   quantSym :: SPQuantSym
quantSym = SPQuantSym
SPForall,
                   variableList :: [SPTerm]
variableList = [SPTerm]
varListTerms,
                   qFormula :: SPTerm
qFormula = SPSymbol -> [SPTerm] -> SPTerm
compTerm SPSymbol
SPImplies
                     [ SPSymbol -> [SPTerm] -> SPTerm
compTerm (SPIdentifier -> SPSymbol
spSym SPIdentifier
psym) [SPTerm]
varListTerms
                     , (SPTerm -> SPTerm -> SPTerm) -> [SPTerm] -> SPTerm
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 SPTerm -> SPTerm -> SPTerm
mkConj ([SPTerm] -> SPTerm) -> [SPTerm] -> SPTerm
forall a b. (a -> b) -> a -> b
$ (SPIdentifier -> [SPIdentifier] -> SPTerm)
-> [SPIdentifier] -> [[SPIdentifier]] -> [SPTerm]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
                       (\ v :: SPIdentifier
v -> (SPTerm -> SPTerm -> SPTerm) -> [SPTerm] -> SPTerm
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 SPTerm -> SPTerm -> SPTerm
mkDisj ([SPTerm] -> SPTerm)
-> ([SPIdentifier] -> [SPTerm]) -> [SPIdentifier] -> SPTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SPIdentifier -> SPTerm) -> [SPIdentifier] -> [SPTerm]
forall a b. (a -> b) -> [a] -> [b]
map (SPIdentifier -> SPIdentifier -> SPTerm
typedVarTerm SPIdentifier
v))
                       [SPIdentifier]
varList [[SPIdentifier]]
tss ]}

    predDecl :: [SPDeclaration]
predDecl = ((SPIdentifier, Set [SPIdentifier]) -> [SPDeclaration])
-> [(SPIdentifier, Set [SPIdentifier])] -> [SPDeclaration]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SPIdentifier, Set [SPIdentifier]) -> [SPDeclaration]
predDecls ([(SPIdentifier, Set [SPIdentifier])] -> [SPDeclaration])
-> [(SPIdentifier, Set [SPIdentifier])] -> [SPDeclaration]
forall a b. (a -> b) -> a -> b
$ Map SPIdentifier (Set [SPIdentifier])
-> [(SPIdentifier, Set [SPIdentifier])]
forall k a. Map k a -> [(k, a)]
Map.toList (Map SPIdentifier (Set [SPIdentifier])
 -> [(SPIdentifier, Set [SPIdentifier])])
-> Map SPIdentifier (Set [SPIdentifier])
-> [(SPIdentifier, Set [SPIdentifier])]
forall a b. (a -> b) -> a -> b
$ Sign -> Map SPIdentifier (Set [SPIdentifier])
predMap Sign
s

    predDecls :: (SPIdentifier, Set [SPIdentifier]) -> [SPDeclaration]
predDecls (p :: SPIdentifier
p, tset :: Set [SPIdentifier]
tset) = -- assert (Set.size tset == 1)
                          ([SPIdentifier] -> [SPDeclaration])
-> [[SPIdentifier]] -> [SPDeclaration]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SPIdentifier -> [SPIdentifier] -> [SPDeclaration]
toPDecl SPIdentifier
p) (Set [SPIdentifier] -> [[SPIdentifier]]
forall a. Set a -> [a]
Set.toList Set [SPIdentifier]
tset)
    toPDecl :: SPIdentifier -> [SPIdentifier] -> [SPDeclaration]
toPDecl p :: SPIdentifier
p t :: [SPIdentifier]
t
        | [SPIdentifier] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SPIdentifier]
t = []
        | Bool
otherwise = [SPPredDecl :: SPIdentifier -> [SPIdentifier] -> SPDeclaration
SPPredDecl {predSym :: SPIdentifier
predSym = SPIdentifier
p, sortSyms :: [SPIdentifier]
sortSyms = [SPIdentifier]
t}]

    genDecl :: [SPDeclaration]
genDecl = (SPIdentifier
 -> Maybe Generated -> [SPDeclaration] -> [SPDeclaration])
-> [SPDeclaration]
-> Map SPIdentifier (Maybe Generated)
-> [SPDeclaration]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ ssym :: SPIdentifier
ssym ->
                       ([SPDeclaration] -> [SPDeclaration])
-> (Generated -> [SPDeclaration] -> [SPDeclaration])
-> Maybe Generated
-> [SPDeclaration]
-> [SPDeclaration]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [SPDeclaration] -> [SPDeclaration]
forall a. a -> a
id (\ gen :: Generated
gen ->
                             (SPGenDecl :: SPIdentifier -> Bool -> [SPIdentifier] -> SPDeclaration
SPGenDecl {sortSym :: SPIdentifier
sortSym = SPIdentifier
ssym,
                                  freelyGenerated :: Bool
freelyGenerated = Generated -> Bool
freely Generated
gen,
                                  funcList :: [SPIdentifier]
funcList = Generated -> [SPIdentifier]
byFunctions Generated
gen} SPDeclaration -> [SPDeclaration] -> [SPDeclaration]
forall a. a -> [a] -> [a]
:)))
              [] (Map SPIdentifier (Maybe Generated) -> [SPDeclaration])
-> Map SPIdentifier (Maybe Generated) -> [SPDeclaration]
forall a b. (a -> b) -> a -> b
$ Sign -> Map SPIdentifier (Maybe Generated)
sortMap Sign
s

{- |
  Inserts a Named Sentence (axiom or goal) into an SPLogicalPart.
-}
insertSentence :: SPLogicalPart -> Named Sentence -> SPLogicalPart
insertSentence :: SPLogicalPart -> SPFormula -> SPLogicalPart
insertSentence lp :: SPLogicalPart
lp nSen :: SPFormula
nSen = SPLogicalPart
lp {formulaLists :: [SPFormulaList]
formulaLists = [SPFormulaList]
fLists'}
  where
    insertFormula :: SPOriginType -> SPFormula -> [SPFormulaList] -> [SPFormulaList]
insertFormula oType :: SPOriginType
oType x :: SPFormula
x [] =
      [SPFormulaList :: SPOriginType -> [SPFormula] -> SPFormulaList
SPFormulaList {originType :: SPOriginType
originType = SPOriginType
oType, formulae :: [SPFormula]
formulae = [SPFormula
x]}]
    insertFormula oType :: SPOriginType
oType x :: SPFormula
x (l :: SPFormulaList
l : ls :: [SPFormulaList]
ls) =
      if SPFormulaList -> SPOriginType
originType SPFormulaList
l SPOriginType -> SPOriginType -> Bool
forall a. Eq a => a -> a -> Bool
== SPOriginType
oType
        then SPFormulaList
l {formulae :: [SPFormula]
formulae = case SPFormulaList -> [SPFormula]
formulae SPFormulaList
l of
               [f :: SPFormula
f] | SPOriginType
oType SPOriginType -> SPOriginType -> Bool
forall a. Eq a => a -> a -> Bool
== SPOriginType
SPOriginConjectures ->
                  [(String -> String) -> SPFormula -> SPFormula
forall a b s. (a -> b) -> SenAttr s a -> SenAttr s b
reName (String -> String -> String
forall a b. a -> b -> a
const "ga_conjunction_of_theorem")
                   (SPFormula -> SPFormula) -> SPFormula -> SPFormula
forall a b. (a -> b) -> a -> b
$ (SPTerm -> SPTerm) -> SPFormula -> SPFormula
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed (SPTerm -> SPTerm -> SPTerm
forall a b. a -> b -> a
const (SPTerm -> SPTerm -> SPTerm) -> SPTerm -> SPTerm -> SPTerm
forall a b. (a -> b) -> a -> b
$ SPTerm -> SPTerm -> SPTerm
mkConj (SPFormula -> SPTerm
forall s a. SenAttr s a -> s
sentence SPFormula
f) (SPTerm -> SPTerm) -> SPTerm -> SPTerm
forall a b. (a -> b) -> a -> b
$ SPFormula -> SPTerm
forall s a. SenAttr s a -> s
sentence SPFormula
x) SPFormula
f]
               fs :: [SPFormula]
fs -> SPFormula
x SPFormula -> [SPFormula] -> [SPFormula]
forall a. a -> [a] -> [a]
: [SPFormula]
fs} SPFormulaList -> [SPFormulaList] -> [SPFormulaList]
forall a. a -> [a] -> [a]
: [SPFormulaList]
ls
        else SPFormulaList
l SPFormulaList -> [SPFormulaList] -> [SPFormulaList]
forall a. a -> [a] -> [a]
: SPOriginType -> SPFormula -> [SPFormulaList] -> [SPFormulaList]
insertFormula SPOriginType
oType SPFormula
x [SPFormulaList]
ls
    fLists' :: [SPFormulaList]
fLists' = if SPFormula -> Bool
forall s a. SenAttr s a -> Bool
isAxiom SPFormula
nSen
                then SPOriginType -> SPFormula -> [SPFormulaList] -> [SPFormulaList]
insertFormula SPOriginType
SPOriginAxioms SPFormula
nSen [SPFormulaList]
fLists
                else SPOriginType -> SPFormula -> [SPFormulaList] -> [SPFormulaList]
insertFormula SPOriginType
SPOriginConjectures SPFormula
nSen [SPFormulaList]
fLists
    fLists :: [SPFormulaList]
fLists = SPLogicalPart -> [SPFormulaList]
formulaLists SPLogicalPart
lp

{- |
  Generate a SoftFOL problem with time stamp while maybe adding a goal.
-}
genSoftFOLProblem :: String -> SPLogicalPart
                -> Maybe (Named SPTerm) -> IO SPProblem
genSoftFOLProblem :: String -> SPLogicalPart -> Maybe SPFormula -> IO SPProblem
genSoftFOLProblem thName :: String
thName lp :: SPLogicalPart
lp m_nGoal :: Maybe SPFormula
m_nGoal =
    do UTCTime
d <- IO UTCTime
getCurrentTime
       SPProblem -> IO SPProblem
forall (m :: * -> *) a. Monad m => a -> m a
return (SPProblem -> IO SPProblem) -> SPProblem -> IO SPProblem
forall a b. (a -> b) -> a -> b
$ String -> SPProblem
problem (String -> SPProblem) -> String -> SPProblem
forall a b. (a -> b) -> a -> b
$ UTCTime -> String
forall a. Show a => a -> String
show UTCTime
d
    where
    problem :: String -> SPProblem
problem sd :: String
sd = SPProblem :: String
-> SPDescription -> SPLogicalPart -> [SPSetting] -> SPProblem
SPProblem
        {identifier :: String
identifier = "hets_exported",
         description :: SPDescription
description = SPDescription :: String
-> String
-> Maybe String
-> Maybe String
-> SPLogState
-> String
-> Maybe String
-> SPDescription
SPDescription
                       {name :: String
name = String
thName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> (SPFormula -> String) -> Maybe SPFormula -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "" (('_' Char -> String -> String
forall a. a -> [a] -> [a]
:) (String -> String) -> (SPFormula -> String) -> SPFormula -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPFormula -> String
forall s a. SenAttr s a -> a
senAttr) Maybe SPFormula
m_nGoal,
                        author :: String
author = "hets",
                        version :: Maybe String
SoftFOL.Sign.version = Maybe String
forall a. Maybe a
Nothing,
                        logic :: Maybe String
logic = Maybe String
forall a. Maybe a
Nothing,
                        status :: SPLogState
status = SPLogState
SPStateUnknown,
                        desc :: String
desc = "",
                        date :: Maybe String
date = String -> Maybe String
forall a. a -> Maybe a
Just String
sd},
         logicalPart :: SPLogicalPart
logicalPart = SPLogicalPart
-> (SPFormula -> SPLogicalPart) -> Maybe SPFormula -> SPLogicalPart
forall b a. b -> (a -> b) -> Maybe a -> b
maybe SPLogicalPart
lp (SPLogicalPart -> SPFormula -> SPLogicalPart
insertSentence SPLogicalPart
lp) Maybe SPFormula
m_nGoal,
         settings :: [SPSetting]
settings = []}

{- |
  generates a variable for each for each symbol in the input list
  without symbol overlap
-}
genVarList :: SPIdentifier -> [SPIdentifier] -> [SPIdentifier]
genVarList :: SPIdentifier -> [SPIdentifier] -> [SPIdentifier]
genVarList chSym :: SPIdentifier
chSym symList :: [SPIdentifier]
symList =
    let reservSym :: [SPIdentifier]
reservSym = SPIdentifier
chSym SPIdentifier -> [SPIdentifier] -> [SPIdentifier]
forall a. a -> [a] -> [a]
: [SPIdentifier]
symList
        varSource :: [SPIdentifier]
varSource = (SPIdentifier -> Bool) -> [SPIdentifier] -> [SPIdentifier]
forall a. (a -> Bool) -> [a] -> [a]
filter (SPIdentifier -> [SPIdentifier] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [SPIdentifier]
reservSym)
          ([SPIdentifier] -> [SPIdentifier])
-> [SPIdentifier] -> [SPIdentifier]
forall a b. (a -> b) -> a -> b
$ (Int -> SPIdentifier) -> [Int] -> [SPIdentifier]
forall a b. (a -> b) -> [a] -> [b]
map (String -> SPIdentifier
mkSimpleId (String -> SPIdentifier) -> (Int -> String) -> Int -> SPIdentifier
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> String -> String
showChar 'Y' (String -> String) -> (Int -> String) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show) [(0 :: Int) ..]
    in Int -> [SPIdentifier] -> [SPIdentifier]
forall a. Int -> [a] -> [a]
take ([SPIdentifier] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SPIdentifier]
symList) [SPIdentifier]
varSource

predDecl2Term :: SPDeclaration -> Maybe SPTerm
predDecl2Term :: SPDeclaration -> Maybe SPTerm
predDecl2Term pd :: SPDeclaration
pd = case SPDeclaration
pd of
                     SPPredDecl {} -> Maybe SPTerm
mkPredTerm
                     _ -> Maybe SPTerm
forall a. Maybe a
Nothing
    where mkPredTerm :: Maybe SPTerm
mkPredTerm = let varList :: [SPIdentifier]
varList = SPIdentifier -> [SPIdentifier] -> [SPIdentifier]
genVarList (SPDeclaration -> SPIdentifier
predSym SPDeclaration
pd)
                                                (SPDeclaration -> [SPIdentifier]
sortSyms SPDeclaration
pd)
                           varListTerms :: [SPTerm]
varListTerms = [SPIdentifier] -> [SPTerm]
spTerms [SPIdentifier]
varList
                       in if [SPIdentifier] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SPIdentifier]
varList
                          then Maybe SPTerm
forall a. Maybe a
Nothing
                          else SPTerm -> Maybe SPTerm
forall a. a -> Maybe a
Just
                               SPQuantTerm :: SPQuantSym -> [SPTerm] -> SPTerm -> SPTerm
SPQuantTerm {
                                 quantSym :: SPQuantSym
quantSym = SPQuantSym
SPForall,
                                 variableList :: [SPTerm]
variableList = [SPTerm]
varListTerms,
                                 qFormula :: SPTerm
qFormula = SPComplexTerm :: SPSymbol -> [SPTerm] -> SPTerm
SPComplexTerm {
                                   symbol :: SPSymbol
symbol = SPSymbol
SPImplies,
                                   arguments :: [SPTerm]
arguments = [SPComplexTerm :: SPSymbol -> [SPTerm] -> SPTerm
SPComplexTerm {
                                                symbol :: SPSymbol
symbol = SPIdentifier -> SPSymbol
SPCustomSymbol
                                                           (SPDeclaration -> SPIdentifier
predSym SPDeclaration
pd),
                                                arguments :: [SPTerm]
arguments = [SPTerm]
varListTerms},
                                              (SPTerm -> SPTerm -> SPTerm) -> [SPTerm] -> SPTerm
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 SPTerm -> SPTerm -> SPTerm
mkConj ([SPTerm] -> SPTerm) -> [SPTerm] -> SPTerm
forall a b. (a -> b) -> a -> b
$
                                                (SPIdentifier -> SPIdentifier -> SPTerm)
-> [SPIdentifier] -> [SPIdentifier] -> [SPTerm]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SPIdentifier -> SPIdentifier -> SPTerm
typedVarTerm
                                                        [SPIdentifier]
varList ([SPIdentifier] -> [SPTerm]) -> [SPIdentifier] -> [SPTerm]
forall a b. (a -> b) -> a -> b
$ SPDeclaration -> [SPIdentifier]
sortSyms SPDeclaration
pd]
                                                       }
                                            }

{- |
'checkArities'
checks if the signature has only overloaded symbols with the same arity
-}
checkArities :: Sign -> Bool
checkArities :: Sign -> Bool
checkArities s :: Sign
s =
    Map SPIdentifier (Set [SPIdentifier]) -> Bool
checkPredArities (Sign -> Map SPIdentifier (Set [SPIdentifier])
predMap Sign
s) Bool -> Bool -> Bool
&& Map SPIdentifier (Set ([SPIdentifier], SPIdentifier)) -> Bool
checkFuncArities (Sign -> Map SPIdentifier (Set ([SPIdentifier], SPIdentifier))
funcMap Sign
s)

checkPredArities :: PredMap -> Bool
checkPredArities :: Map SPIdentifier (Set [SPIdentifier]) -> Bool
checkPredArities = (Set [SPIdentifier] -> Bool -> Bool)
-> Bool -> Map SPIdentifier (Set [SPIdentifier]) -> Bool
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr Set [SPIdentifier] -> Bool -> Bool
forall (t :: * -> *) a. Foldable t => Set (t a) -> Bool -> Bool
checkSet Bool
True
    where checkSet :: Set (t a) -> Bool -> Bool
checkSet s :: Set (t a)
s bv :: Bool
bv = Bool
bv Bool -> Bool -> Bool
&& Bool -> Bool
not (Set (t a) -> Bool
forall a. Set a -> Bool
Set.null Set (t a)
s) Bool -> Bool -> Bool
&&
                  (t a -> Bool) -> [t a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ x :: t a
x -> t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
hd) [t a]
tl
                      where hd :: t a
hd : tl :: [t a]
tl = Set (t a) -> [t a]
forall a. Set a -> [a]
Set.toList Set (t a)
s

checkFuncArities :: FuncMap -> Bool
checkFuncArities :: Map SPIdentifier (Set ([SPIdentifier], SPIdentifier)) -> Bool
checkFuncArities = Map SPIdentifier (Set [SPIdentifier]) -> Bool
checkPredArities (Map SPIdentifier (Set [SPIdentifier]) -> Bool)
-> (Map SPIdentifier (Set ([SPIdentifier], SPIdentifier))
    -> Map SPIdentifier (Set [SPIdentifier]))
-> Map SPIdentifier (Set ([SPIdentifier], SPIdentifier))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map SPIdentifier (Set ([SPIdentifier], SPIdentifier))
-> Map SPIdentifier (Set [SPIdentifier])
forall k b.
Map k (Set ([SPIdentifier], b)) -> Map k (Set [SPIdentifier])
mapToPredMap
    where mapToPredMap :: Map k (Set ([SPIdentifier], b)) -> Map k (Set [SPIdentifier])
mapToPredMap = (Set ([SPIdentifier], b) -> Set [SPIdentifier])
-> Map k (Set ([SPIdentifier], b)) -> Map k (Set [SPIdentifier])
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((([SPIdentifier], b) -> [SPIdentifier])
-> Set ([SPIdentifier], b) -> Set [SPIdentifier]
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ([SPIdentifier], b) -> [SPIdentifier]
forall a b. (a, b) -> a
fst)