| Copyright | (c) Till Mossakowski and Uni Bremen 2002-2005 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Christian.Maeder@dfki.de |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
CASL.Quantification
Description
Free variables; getting rid of superfluous quantifications
- symbolsRecord :: (f -> Set Symbol) -> Record f (Set Symbol) (Set Symbol)
- flatVAR_DECLs :: [VAR_DECL] -> [(VAR, SORT)]
- freeVarsRecord :: (f -> VarSet) -> Record f VarSet VarSet
- freeTermVars :: TermExtension f => Sign f e -> TERM f -> VarSet
- freeVars :: TermExtension f => Sign f e -> FORMULA f -> VarSet
- varSetToDecls :: VarSet -> [VAR_DECL]
- quantFreeVars :: TermExtension f => Sign f e -> FORMULA f -> Range -> FORMULA f
- effQuantify :: TermExtension f => Sign f e -> QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
- stripRecord :: TermExtension f => Sign f e -> (f -> f) -> Record f (FORMULA f) (TERM f)
- stripQuant :: TermExtension f => Sign f e -> FORMULA f -> FORMULA f
- stripAllQuant :: FORMULA f -> FORMULA f
- getQuantVars :: FORMULA f -> VarSet
- getTopVars :: [Named (FORMULA f)] -> VarSet
- diffVars :: Map VAR SORT -> VarSet -> Map VAR SORT
- warnUnusedVars :: String -> Sign f e -> VarSet -> [Diagnosis]
- warnUnused :: Sign f e -> [Named (FORMULA f)] -> [Diagnosis]
Documentation
flatVAR_DECLs :: [VAR_DECL] -> [(VAR, SORT)]
freeVarsRecord :: (f -> VarSet) -> Record f VarSet VarSet
freeTermVars :: TermExtension f => Sign f e -> TERM f -> VarSet
freeVars :: TermExtension f => Sign f e -> FORMULA f -> VarSet
varSetToDecls :: VarSet -> [VAR_DECL]
quantFreeVars :: TermExtension f => Sign f e -> FORMULA f -> Range -> FORMULA f
effQuantify :: TermExtension f => Sign f e -> QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
quantify only over free variables (and only once)
stripRecord :: TermExtension f => Sign f e -> (f -> f) -> Record f (FORMULA f) (TERM f)
stripQuant :: TermExtension f => Sign f e -> FORMULA f -> FORMULA f
strip superfluous (or nested) quantifications
stripAllQuant :: FORMULA f -> FORMULA f
strip all universal quantifications
getQuantVars :: FORMULA f -> VarSet
get top-level variables
getTopVars :: [Named (FORMULA f)] -> VarSet
get top-level variables for all sentences
warnUnusedVars :: String -> Sign f e -> VarSet -> [Diagnosis]
warnUnused :: Sign f e -> [Named (FORMULA f)] -> [Diagnosis]