hets/SoftFOL/Conversions.hs

	Conversions.hs revision bfe34c9d0a279f8f86eae778b761f32e4788d42d
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder{- |
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederModule      :  $Header$
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederDescription :  Functions to convert to internal SP* data structures.
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederCopyright   :  (c) Rene Wagner, Klaus L�ttich, Uni Bremen 2005
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederLicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederMaintainer  :  luecke@informatik.uni-bremen.de
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederStability   :  provisional
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederPortability :  unknown
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederFunctions to convert to internal SP* data structures.
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder-}
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maedermodule SoftFOL.Conversions where
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder
8191ab400cc9ebb5a3f6c6f18104a208aae187e8Christian Maederimport Control.Exception
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport System.Time
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport Data.Maybe
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport Data.List
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport qualified Data.Map as Map
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport qualified Data.Set as Set
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport qualified Common.Lib.Rel as Rel
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport Common.AS_Annotation
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport Common.Id
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport SoftFOL.Sign
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder{- |
8191ab400cc9ebb5a3f6c6f18104a208aae187e8Christian Maeder  Converts a Sign to an initial (no axioms or goals) SPLogicalPart.
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder-}
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaedersignToSPLogicalPart :: Sign -> SPLogicalPart
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaedersignToSPLogicalPart s =
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder    assert (checkArities s)
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder               (emptySPLogicalPart {symbolList = sList,
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                                    declarationList = Just decList,
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                                    formulaLists = if null decList
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                                                   then []
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                                                   else [predArgRestrictions]
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                                   }
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder               )
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder  where
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder    sList = if Rel.null (sortRel s) && Map.null (funcMap s) &&
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder               Map.null (predMap s) && Map.null (sortMap s)
8191ab400cc9ebb5a3f6c6f18104a208aae187e8Christian Maeder              then Nothing
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder              else Just emptySymbolList
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                       { functions =
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                             map (\(f, ts) ->
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                                      SPSignSym {sym = f,
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                                                 arity = length (fst (head
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                                                            (Set.toList ts)))})
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                                     (Map.toList (funcMap s)),
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                         predicates =
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                             map (\(p, ts) ->
186de7a36bdf5910e0616c3a0447603e98217dc7Christian Maeder                                      SPSignSym {sym = p,
186de7a36bdf5910e0616c3a0447603e98217dc7Christian Maeder                                                 arity = length (head
186de7a36bdf5910e0616c3a0447603e98217dc7Christian Maeder                                                          (Set.toList ts))})
186de7a36bdf5910e0616c3a0447603e98217dc7Christian Maeder                                     (Map.toList (predMap s)),
186de7a36bdf5910e0616c3a0447603e98217dc7Christian Maeder                         sorts = map SPSimpleSignSym $ Map.keys $ sortMap s }
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder    decList = if (singleSorted s &&
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                  (null . Map.elems . sortMap) s ) then []
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                else subsortDecl ++ termDecl ++ predDecl ++ genDecl
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder    subsortDecl = map (\(a, b) -> SPSubsortDecl {sortSymA = a, sortSymB = b})
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                      (Rel.toList (Rel.transReduce (sortRel s)))
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder    termDecl = concatMap termDecls (Map.toList (funcMap s))
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder    termDecls (fsym, tset) = map (toFDecl fsym) (Set.toList tset)
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder    toFDecl fsym (args, ret) =
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder        if null args
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder        then SPSimpleTermDecl
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                 (SPComplexTerm {symbol = SPCustomSymbol ret,
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                                 arguments = [SPSimpleTerm
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                                              (SPCustomSymbol fsym)]})
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder        else SPTermDecl {
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder               termDeclTermList =
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                 map (\(t, i) -> SPComplexTerm {symbol = SPCustomSymbol t,
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                                                arguments = [SPSimpleTerm
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                                      (mkSPCustomSymbol ('X' : (show i)))]})
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                     (zip args [(1::Int)..]),
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder               termDeclTerm = SPComplexTerm {symbol = SPCustomSymbol ret,
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                                             arguments =
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                   [SPComplexTerm {symbol = SPCustomSymbol fsym,
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                                   arguments = map
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                           (SPSimpleTerm . mkSPCustomSymbol
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                            . ('X':) . show . snd)
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                           (zip args [(1::Int)..])}]}}
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder    predArgRestrictions =
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder          SPFormulaList { originType = SPOriginAxioms
8191ab400cc9ebb5a3f6c6f18104a208aae187e8Christian Maeder                        , formulae = Map.foldWithKey toArgRestriction []
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                                     $ predMap s
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder                        }
    toArgRestriction psym tset acc
        | Set.null tset = error "SoftFOL.Conversions.toArgRestriction: empty set"
        | Set.size tset == 1 = acc ++
            maybe []
                  ((:[]) . makeNamed ("arg_restriction_" ++ tokStr psym))
                  ((listToMaybe $ toPDecl psym $ head
                                    $ Set.toList tset)
                    >>= predDecl2Term)
        | otherwise = acc ++
            (let argLists = Set.toList tset
             in [makeNamed ("arg_restriction_o_" ++ tokStr psym) $
                 makeTerm psym $
                 foldl (zipWith (flip (:)))
                      (replicate (length $ head argLists) []) argLists])

    makeTerm psym tss =
        let varList = take (length tss) $
                      genVarList psym (nub $ concat tss)
            varListTerms = spTerms varList
        in if null varList
           then error "SoftFOL.Conversions.makeTerm: no propositional constants"
           else (SPQuantTerm{
                   quantSym=SPForall,
                   variableList=varListTerms,
                   qFormula=SPComplexTerm{
                               symbol=SPImplies,
                               arguments=[SPComplexTerm{
                                            symbol=SPCustomSymbol psym,
                                            arguments=varListTerms},
                                          foldl1 mkConj $
                                          zipWith (\ v ->
                                                       foldl1 mkDisj .
                                                       map (typedVarTerm v))
                                          varList tss]
                                                       }
                                            })

    predDecl = concatMap predDecls (Map.toList (predMap s))

    predDecls (p, tset) = -- assert (Set.size tset == 1)
                          concatMap (toPDecl p) (Set.toList tset)
    toPDecl p t
        | null t    = []
        | otherwise = [SPPredDecl {predSym = p, sortSyms = t}]

    genDecl = map (\(ssym, Just gen) ->
                       SPGenDecl {sortSym = ssym,
                                  freelyGenerated = freely gen,
                                  funcList = byFunctions gen})
                  (filter (isJust . snd) (Map.toList (sortMap s)))

{- |
  Inserts a Named Sentence (axiom or goal) into an SPLogicalPart.
-}
insertSentence :: SPLogicalPart -> Named Sentence -> SPLogicalPart
insertSentence lp nSen = lp {formulaLists = fLists'}
  where
    insertFormula oType x [] =
      [SPFormulaList {originType= oType, formulae= [x]}]
    insertFormula oType x (l:ls) =
      if originType l == oType
        then l{formulae= x:(formulae l)}:ls
        else l:(insertFormula oType x ls)
    fLists' = if isAxiom nSen
                then insertFormula SPOriginAxioms nSen fLists
                else insertFormula SPOriginConjectures nSen fLists
    fLists = formulaLists lp

{- |
  Generate a SoftFOL problem with time stamp while maybe adding a goal.
-}
genSoftFOLProblem :: String -> SPLogicalPart
                -> Maybe (Named SPTerm) -> IO SPProblem
genSoftFOLProblem thName lp m_nGoal =
    do d <- getClockTime
       return $ problem $ show d
    where
    problem sd = SPProblem
        {identifier = mkSimpleId "hets_exported",
         description = SPDescription
                       {name = thName++
                               (maybe ""
                                      (\ nGoal -> '_':senAttr nGoal)
                                      m_nGoal),
                        author = "hets",
                        SoftFOL.Sign.version = Nothing,
                        logic = Nothing,
                        status = SPStateUnknown,
                        desc = "",
                        date = Just sd},
         logicalPart = maybe lp (insertSentence lp) m_nGoal,
         settings = []}

{-|
  generates a variable for each for each symbol in the input list
  without symbol overlap
-}
genVarList :: SPIdentifier -> [SPIdentifier] -> [SPIdentifier]
genVarList chSym symList =
    let reservSym = chSym:symList
        varSource = filter (\x -> not $ elem x reservSym) $
                           map (mkSimpleId . showChar 'Y' . show) [(0::Int)..]
    in take (length symList) varSource

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

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

checkPredArities :: PredMap -> Bool
checkPredArities = Map.fold checkSet True
    where checkSet s bv = bv && not (Set.null s) &&
                  all (\ x -> length x == length hd) tl
                      where hd : tl = Set.toList s

checkFuncArities :: FuncMap -> Bool
checkFuncArities = checkPredArities . mapToPredMap
    where mapToPredMap = Map.map (Set.map fst)