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 |

Utilities for CASL and its comorphisms

## Synopsis

- 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 Source #

specialized delete that deletes all shadowed variables

replaceVars replaces all Qual_var occurences that are supposed to be replaced according to the Subst

buildVMap :: [VAR_DECL] -> [VAR_DECL] -> Subst f Source #

buildVMap constructs a mapping between a list of old variables and corresponding fresh variables based on two lists of VAR_DECL

:: (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)

codeOutConditionalF :: Eq f => (f -> f) -> FORMULA f -> FORMULA f Source #

`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) Source #

Subsitute predications with strong equation if it is equivalent to.