| 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
Synopsis
- 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
freeTermVars :: TermExtension f => Sign f e -> TERM f -> VarSet Source #
varSetToDecls :: VarSet -> [VAR_DECL] Source #
quantFreeVars :: TermExtension f => Sign f e -> FORMULA f -> Range -> FORMULA f Source #
effQuantify :: TermExtension f => Sign f e -> QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f Source #
quantify only over free variables (and only once)
stripRecord :: TermExtension f => Sign f e -> (f -> f) -> Record f (FORMULA f) (TERM f) Source #
stripQuant :: TermExtension f => Sign f e -> FORMULA f -> FORMULA f Source #
strip superfluous (or nested) quantifications
stripAllQuant :: FORMULA f -> FORMULA f Source #
strip all universal quantifications
getQuantVars :: FORMULA f -> VarSet Source #
get top-level variables