| Copyright | (c) Klaus Luettich and Uni Bremen 2002-2004 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Christian.Maeder@dfki.de |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | Safe-Inferred |
CASL.Utils
Description
Utilities for CASL and its comorphisms
- type Subst f = Map VAR (TERM f)
- deleteVMap :: [VAR_DECL] -> Subst f -> Subst f
- replaceVarsRec :: Subst f -> (f -> f) -> Record f (FORMULA f) (TERM f)
- replaceVarsF :: Subst f -> (f -> f) -> FORMULA f -> FORMULA f
- buildVMap :: [VAR_DECL] -> [VAR_DECL] -> Subst f
- codeOutUniqueRecord :: (f -> f) -> (f -> f) -> Record f (FORMULA f) (TERM f)
- codeOutUniqueExtF :: (f -> f) -> (f -> f) -> FORMULA f -> FORMULA f
- codeOutCondRecord :: Eq f => (f -> f) -> Record f (FORMULA f) (TERM f)
- codeOutCondPredication :: Eq f => FORMULA f -> Either (FORMULA f) (FORMULA f)
- constructExpansion :: Eq f => FORMULA f -> TERM f -> FORMULA f
- mkEquationAtom :: Eq f => (TERM f -> TERM f -> Range -> FORMULA f) -> TERM f -> TERM f -> Range -> Either (FORMULA f) (FORMULA f)
- mkSingleTermF :: Eq f => (TERM f -> Range -> FORMULA f) -> TERM f -> Range -> Either (FORMULA f) (FORMULA f)
- codeOutConditionalF :: Eq f => (f -> f) -> FORMULA f -> FORMULA f
- findConditionalRecord :: Record f (Maybe (TERM f)) (Maybe (TERM f))
- findConditionalT :: TERM f -> Maybe (TERM f)
- substConditionalRecord :: Eq f => TERM f -> TERM f -> Record f (FORMULA f) (TERM f)
- substConditionalF :: Eq f => TERM f -> TERM f -> FORMULA f -> FORMULA f
- eqSubstRecord :: Set PRED_SYMB -> (f -> f) -> Record f (FORMULA f) (TERM f)
- substEqPreds :: Set PRED_SYMB -> (f -> f) -> FORMULA f -> FORMULA f
Documentation
deleteVMap :: [VAR_DECL] -> Subst f -> Subst f
specialized delete that deletes all shadowed variables
replaceVarsRec :: Subst f -> (f -> f) -> Record f (FORMULA f) (TERM f)
Arguments
| :: Subst f | |
| -> (f -> f) | this function replaces Qual_var in ExtFORMULA |
| -> FORMULA f | |
| -> FORMULA f |
replaceVars replaces all Qual_var occurences that are supposed to be replaced according to the Subst
buildVMap :: [VAR_DECL] -> [VAR_DECL] -> Subst f
buildVMap constructs a mapping between a list of old variables and corresponding fresh variables based on two lists of VAR_DECL
codeOutUniqueRecord :: (f -> f) -> (f -> f) -> Record f (FORMULA f) (TERM f)
Arguments
| :: (f -> f) | this function replaces Qual_var in ExtFORMULA |
| -> (f -> f) | codes out Unique_existential in ExtFORMULA |
| -> FORMULA f | |
| -> FORMULA f |
codeOutUniqueExtF compiles every unique_existential quantification to simple quantifications. It works recursively through the whole formula and only touches Unique_existential quantifications: exists! x . phi(x) ==> (exists x. phi(x)) (forall x,y . phi(x) phi(y) => x=y)
codeOutCondRecord :: Eq f => (f -> f) -> Record f (FORMULA f) (TERM f)
constructExpansion :: Eq f => FORMULA f -> TERM f -> FORMULA f
codeOutConditionalF :: Eq f => (f -> f) -> FORMULA f -> FORMULA f
codeOutConditionalF implemented via foldFormula
at each atom with a term find first (most left,no recursion into terms within it) Conditional term and report it (findConditionalT)
substitute the original atom with the conjunction of the already encoded atoms and already encoded formula
encoded atoms are the result of the substition (substConditionalF) of the Conditional term with each result term of the Conditional term plus recusion of codingOutConditionalF
encoded formulas are the result of codingOutConditionalF
expansion of conditionals according to CASL-Ref-Manual:
'A[T1 when F else T2]' expands to
'(A[T1] if F) /\ (A[T2] if not F)'
findConditionalT :: TERM f -> Maybe (TERM f)
Subsitute predications with strong equation if it is equivalent to.
substEqPreds :: Set PRED_SYMB -> (f -> f) -> FORMULA f -> FORMULA f