Hets - the Heterogeneous Tool Set

Copyright(c) Till Mossakowski and Uni Bremen 2002-2005
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

CASL.Quantification

Description

Free variables; getting rid of superfluous quantifications

Synopsis

Documentation

symbolsRecord :: (f -> Set Symbol) -> Record f (Set Symbol) (Set Symbol) 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

getTopVars :: [Named (FORMULA f)] -> VarSet Source #

get top-level variables for all sentences

diffVars :: Map VAR SORT -> VarSet -> Map VAR SORT Source #

warnUnusedVars :: String -> Sign f e -> VarSet -> [Diagnosis] Source #