| 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 |
| Safe Haskell | None |
SoftFOL.Conversions
Description
Functions to convert to internal SP* data structures.
Synopsis
- signToSPLogicalPart :: Sign -> SPLogicalPart
- insertSentence :: SPLogicalPart -> Named Sentence -> SPLogicalPart
- genSoftFOLProblem :: String -> SPLogicalPart -> Maybe (Named SPTerm) -> IO SPProblem
- genVarList :: SPIdentifier -> [SPIdentifier] -> [SPIdentifier]
- predDecl2Term :: SPDeclaration -> Maybe SPTerm
- checkArities :: Sign -> Bool
- checkPredArities :: PredMap -> Bool
- checkFuncArities :: FuncMap -> Bool
Documentation
signToSPLogicalPart :: Sign -> SPLogicalPart Source #
Converts a Sign to an initial (no axioms or goals) SPLogicalPart.
insertSentence :: SPLogicalPart -> Named Sentence -> SPLogicalPart Source #
Inserts a Named Sentence (axiom or goal) into an SPLogicalPart.
genSoftFOLProblem :: String -> SPLogicalPart -> Maybe (Named SPTerm) -> IO SPProblem Source #
Generate a SoftFOL problem with time stamp while maybe adding a goal.
genVarList :: SPIdentifier -> [SPIdentifier] -> [SPIdentifier] Source #
generates a variable for each for each symbol in the input list without symbol overlap
predDecl2Term :: SPDeclaration -> Maybe SPTerm Source #
checkArities :: Sign -> Bool Source #
checkArities
checks if the signature has only overloaded symbols with the same arity
checkPredArities :: PredMap -> Bool Source #
checkFuncArities :: FuncMap -> Bool Source #