hets/SoftFOL/Conversions.hs

	Conversions.hs revision 56207d3d8820aef00cba6d90139265a9bc7f9c3d
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder{- |
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederModule      :  $Header$
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederDescription :  Functions to convert to internal SP* data structures.
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederCopyright   :  (c) Rene Wagner, Klaus L�ttich, Uni Bremen 2005
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederLicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederMaintainer  :  luecke@informatik.uni-bremen.de
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederStability   :  provisional
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederPortability :  unknown
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederFunctions to convert to internal SP* data structures.
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder-}
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maedermodule SoftFOL.Conversions where
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport Control.Exception
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport System.Time
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport Data.Maybe
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport Data.List
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport qualified Data.Map as Map
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport qualified Data.Set as Set
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport qualified Common.Lib.Rel as Rel
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport Common.AS_Annotation
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport Common.Id
b99a317dc5c91e28bd294248a0491c374783169aChristian Maederimport SoftFOL.Sign
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder{- |
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder  Converts a Sign to an initial (no axioms or goals) SPLogicalPart.
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder-}
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedersignToSPLogicalPart :: Sign -> SPLogicalPart
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedersignToSPLogicalPart s =
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder    assert (checkArities s)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder               (emptySPLogicalPart {symbolList = sList,
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                                    declarationList = Just decList,
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                                    formulaLists = if null decList
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                                                   then []
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                                                   else [predArgRestrictions]
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder                                   }
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder               )
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder  where
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder    sList = if Rel.null (sortRel s) && Map.null (funcMap s) &&
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder               Map.null (predMap s) && Map.null (sortMap s)
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder              then Nothing
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder              else Just emptySymbolList
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder                       { functions =
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder                             map (\(f, ts) ->
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder                                      SPSignSym {sym = f,
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder                                                 arity = length (fst (head
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder                                                            (Set.toList ts)))})
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder                                     (Map.toList (funcMap s)),
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder                         predicates =
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder                             map (\(p, ts) ->
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder                                      SPSignSym {sym = p,
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder                                                 arity = length (head
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder                                                          (Set.toList ts))})
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder                                     (Map.toList (predMap s)),
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder                         sorts = map SPSimpleSignSym $ Map.keys $ sortMap s }
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder    decList = if (singleSorted s &&
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder                  (null . Map.elems . sortMap) s ) then []
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                else subsortDecl ++ termDecl ++ predDecl ++ genDecl
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder    subsortDecl = map (\(a, b) -> SPSubsortDecl {sortSymA = a, sortSymB = b})
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                      (Rel.toList (Rel.transReduce (sortRel s)))
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder    termDecl = concatMap termDecls (Map.toList (funcMap s))
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder    termDecls (fsym, tset) = map (toFDecl fsym) (Set.toList tset)
99835f4b06ef057b494b529a7fe7f0c2c3dcab6aChristian Maeder    toFDecl fsym (args, ret) =
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder        if null args
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder        then SPSimpleTermDecl $ compTerm (spSym ret) [simpTerm $ spSym fsym]
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder        else let
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder            xTerm :: Int -> SPTerm
42bccfa650b681c2602b412fec3863872c3d057bChristian Maeder            xTerm i = simpTerm $ mkSPCustomSymbol $ 'X' : show i
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder            in SPTermDecl {
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder               termDeclTermList =
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                 zipWith (\ t i -> compTerm (spSym t) [xTerm i]) args [1..],
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder               termDeclTerm = compTerm (spSym ret)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                   $ zipWith (const xTerm) args [1..] }
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder    predArgRestrictions =
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder          SPFormulaList { originType = SPOriginAxioms
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                        , formulae = Map.foldWithKey toArgRestriction []
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                                     $ predMap s
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                        }
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder    toArgRestriction psym tset acc
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder        | Set.null tset = error
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder           "SoftFOL.Conversions.toArgRestriction: empty set"
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder        | Set.size tset == 1 = acc ++
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder            maybe []
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder                  ((: []) . makeNamed ("arg_restriction_" ++ tokStr psym))
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder                  (listToMaybe (toPDecl psym $ head $ Set.toList tset)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                    >>= predDecl2Term)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder        | otherwise = acc ++
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder             let argLists = Set.toList tset
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder             in [makeNamed ("arg_restriction_o_" ++ tokStr psym) $
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                 makeTerm psym $
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                 foldl (zipWith (flip (:)))
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                      (replicate (length $ head argLists) []) argLists]
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder    makeTerm psym tss =
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder        let varList = take (length tss) $
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder                      genVarList psym (nub $ concat tss)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder            varListTerms = spTerms varList
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder        in if null varList
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder           then error
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder             "SoftFOL.Conversions.makeTerm: no propositional constants"
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder           else SPQuantTerm {
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                   quantSym=SPForall,
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                   variableList=varListTerms,
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                   qFormula= compTerm SPImplies
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                     [ compTerm (spSym psym) varListTerms
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                     , foldl1 mkConj $ zipWith
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder                       (\ v ->  foldl1 mkDisj . map (typedVarTerm v))
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                       varList tss ]}
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder    predDecl = concatMap predDecls $ Map.toList $ predMap s
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder    predDecls (p, tset) = -- assert (Set.size tset == 1)
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder                          concatMap (toPDecl p) (Set.toList tset)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder    toPDecl p t
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder        | null t    = []
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder        | otherwise = [SPPredDecl {predSym = p, sortSyms = t}]
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder    genDecl = map (\ (ssym, Just gen) ->
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                       SPGenDecl {sortSym = ssym,
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                                  freelyGenerated = freely gen,
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                                  funcList = byFunctions gen})
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder              $ filter (isJust . snd) $ Map.toList $ sortMap s
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder{- |
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder  Inserts a Named Sentence (axiom or goal) into an SPLogicalPart.
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder-}
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederinsertSentence :: SPLogicalPart -> Named Sentence -> SPLogicalPart
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederinsertSentence lp nSen = lp {formulaLists = fLists'}
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder  where
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder    insertFormula oType x [] =
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder      [SPFormulaList {originType= oType, formulae= [x]}]
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder    insertFormula oType x (l:ls) =
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder      if originType l == oType
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder        then l{formulae= x:(formulae l)}:ls
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder        else l:(insertFormula oType x ls)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder    fLists' = if isAxiom nSen
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                then insertFormula SPOriginAxioms nSen fLists
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                else insertFormula SPOriginConjectures nSen fLists
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder    fLists = formulaLists lp
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder{- |
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder  Generate a SoftFOL problem with time stamp while maybe adding a goal.
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder-}
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedergenSoftFOLProblem :: String -> SPLogicalPart
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                -> Maybe (Named SPTerm) -> IO SPProblem
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedergenSoftFOLProblem thName lp m_nGoal =
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder    do d <- getClockTime
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder       return $ problem $ show d
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder    where
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder    problem sd = SPProblem
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder        {identifier = "hets_exported",
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder         description = SPDescription
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                       {name = thName++
42bccfa650b681c2602b412fec3863872c3d057bChristian Maeder                               (maybe ""
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder                                      (\ nGoal -> '_':senAttr nGoal)
42bccfa650b681c2602b412fec3863872c3d057bChristian Maeder                                      m_nGoal),
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder                        author = "hets",
99835f4b06ef057b494b529a7fe7f0c2c3dcab6aChristian Maeder                        SoftFOL.Sign.version = Nothing,
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                        logic = Nothing,
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder                        status = SPStateUnknown,
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder                        desc = "",
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                        date = Just sd},
99835f4b06ef057b494b529a7fe7f0c2c3dcab6aChristian Maeder         logicalPart = maybe lp (insertSentence lp) m_nGoal,
99835f4b06ef057b494b529a7fe7f0c2c3dcab6aChristian Maeder         settings = []}
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
99835f4b06ef057b494b529a7fe7f0c2c3dcab6aChristian Maeder{-|
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder  generates a variable for each for each symbol in the input list
99835f4b06ef057b494b529a7fe7f0c2c3dcab6aChristian Maeder  without symbol overlap
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder-}
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedergenVarList :: SPIdentifier -> [SPIdentifier] -> [SPIdentifier]
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedergenVarList chSym symList =
99835f4b06ef057b494b529a7fe7f0c2c3dcab6aChristian Maeder    let reservSym = chSym:symList
42bccfa650b681c2602b412fec3863872c3d057bChristian Maeder        varSource = filter (\x -> not $ elem x reservSym) $
99835f4b06ef057b494b529a7fe7f0c2c3dcab6aChristian Maeder                           map (mkSimpleId . showChar 'Y' . show) [(0::Int)..]
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder    in take (length symList) varSource
99835f4b06ef057b494b529a7fe7f0c2c3dcab6aChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederpredDecl2Term :: SPDeclaration -> Maybe SPTerm
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederpredDecl2Term pd = case pd of
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                     SPPredDecl {} -> mkPredTerm
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                     _ -> Nothing
99835f4b06ef057b494b529a7fe7f0c2c3dcab6aChristian Maeder    where mkPredTerm = let varList = genVarList (predSym pd)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                                                (sortSyms pd)
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder                           varListTerms = spTerms varList
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                       in if null varList
99835f4b06ef057b494b529a7fe7f0c2c3dcab6aChristian Maeder                          then Nothing
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                          else Just (
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                               SPQuantTerm{
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                                 quantSym=SPForall,
99835f4b06ef057b494b529a7fe7f0c2c3dcab6aChristian Maeder                                 variableList=varListTerms,
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder                                 qFormula=SPComplexTerm{
99835f4b06ef057b494b529a7fe7f0c2c3dcab6aChristian Maeder                                   symbol=SPImplies,
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder                                   arguments=[SPComplexTerm{
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder                                                symbol=SPCustomSymbol
99835f4b06ef057b494b529a7fe7f0c2c3dcab6aChristian Maeder                                                           (predSym pd),
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder                                                arguments=varListTerms},
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder                                              foldl1 mkConj $
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder                                                zipWith typedVarTerm
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder                                                        varList $ sortSyms pd]
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder                                                       }
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder                                            })
99835f4b06ef057b494b529a7fe7f0c2c3dcab6aChristian Maeder
99835f4b06ef057b494b529a7fe7f0c2c3dcab6aChristian Maeder{- |
99835f4b06ef057b494b529a7fe7f0c2c3dcab6aChristian Maeder'checkArities'
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederchecks if the signature has only overloaded symbols with the same arity
99835f4b06ef057b494b529a7fe7f0c2c3dcab6aChristian Maeder-}
99835f4b06ef057b494b529a7fe7f0c2c3dcab6aChristian MaedercheckArities :: Sign -> Bool
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedercheckArities s =
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder    checkPredArities (predMap s) && checkFuncArities (funcMap s)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedercheckPredArities :: PredMap -> Bool
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedercheckPredArities = Map.fold checkSet True
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder    where checkSet s bv = bv && not (Set.null s) &&
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                  all (\ x -> length x == length hd) tl
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder                      where hd : tl = Set.toList s
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedercheckFuncArities :: FuncMap -> Bool
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedercheckFuncArities = checkPredArities . mapToPredMap
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder    where mapToPredMap = Map.map (Set.map fst)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder