Hets - the Heterogeneous Tool Set

Copyright (c) Klaus Luettich and Uni Bremen 2002-2004 GPLv2 or higher, see LICENSE.txt Christian.Maeder@dfki.de provisional portable Safe-Inferred

CASL.Utils

Description

Utilities for CASL and its comorphisms

Synopsis

# Documentation

type Subst f = Map VAR (TERM f)

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)

replaceVarsF

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)

codeOutUniqueExtF

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)

codeOutCondPredication

Arguments

 :: Eq f => FORMULA f -> Either (FORMULA f) (FORMULA f) Left means check again for Conditional, Right means no Conditional left

mkEquationAtom

Arguments

 :: Eq f => (TERM f -> TERM f -> Range -> FORMULA f) equational constructor -> TERM f -> TERM f -> Range -> Either (FORMULA f) (FORMULA f) Left means check again for Conditional, Right means no Conditional left

mkSingleTermF

Arguments

 :: Eq f => (TERM f -> Range -> FORMULA f) single term atom constructor -> TERM f -> Range -> Either (FORMULA f) (FORMULA f) Left means check again for Conditional, Right means no Conditional left

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)`'

substConditionalRecord

Arguments

 :: Eq f => TERM f Conditional to search for -> TERM f newly inserted term -> Record f (FORMULA f) (TERM f)

substConditionalF

Arguments

 :: Eq f => TERM f Conditional to search for -> TERM f newly inserted term -> FORMULA f -> FORMULA f

eqSubstRecord

Arguments

 :: Set PRED_SYMB equivalent predicates -> (f -> f) -> Record f (FORMULA f) (TERM f)

Subsitute predications with strong equation if it is equivalent to.

substEqPreds :: Set PRED_SYMB -> (f -> f) -> FORMULA f -> FORMULA f