a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowen{- |

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowenModule : $Header$

fd9abdda70912b99b24e3bf1a38f26fde908a74cndDescription : Utilities for CASL and its comorphisms

fd9abdda70912b99b24e3bf1a38f26fde908a74cndCopyright : (c) Klaus Luettich and Uni Bremen 2002-2004

fd9abdda70912b99b24e3bf1a38f26fde908a74cndLicense : GPLv2 or higher, see LICENSE.txt

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowen

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowenMaintainer : Christian.Maeder@dfki.de

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowenStability : provisional

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowenPortability : portable

96ad5d81ee4a2cc66a4ae19893efc8aa6d06fae7jailletc

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowenUtilities for CASL and its comorphisms

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowen

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen-}

2e545ce2450a9953665f701bb05350f0d3f26275nd

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowenmodule CASL.Utils where

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowenimport Data.Maybe

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowenimport Data.List

af33a4994ae2ff15bc67d19ff1a7feb906745bf8rbowen

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowenimport qualified Data.Set as Set

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowenimport qualified Data.Map as Map

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowen

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowenimport Common.Id

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowen

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowenimport CASL.AS_Basic_CASL

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowenimport CASL.Sign (mkVarTerm)

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowenimport CASL.Fold

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowen

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowen{- |

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowenreplacePropPredication replaces a propositional predication of a

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowengiven symbol with an also given formula. Optionally a given variable

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowenis replaced in the predication of another predicate symbol with a

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowengiven term, the variable must occur in the first argument position

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowenof the predication. -}

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowen

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowenreplacePropPredication :: Maybe (PRED_NAME, VAR, TERM ())

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowen {- ^ Just (pSymb,x,t) replace x

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowen with t in Predication of pSymb -}

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowen -> PRED_NAME -- ^ propositional symbol to replace

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowen -> FORMULA () -- ^ Formula to insert

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowen -> FORMULA () -- ^ Formula with placeholder

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowen -> FORMULA ()

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowenreplacePropPredication mTerm pSymb frmIns =

205f749042ed530040a4f0080dbcb47ceae8a374rjung foldFormula (mapRecord $ const ())

af33a4994ae2ff15bc67d19ff1a7feb906745bf8rbowen { foldPredication = \ orig _ ts _ ->

0d0ba3a410038e179b695446bb149cce6264e0abnd let Predication qpn _ ps = orig

7fec19672a491661b2fe4b29f685bc7f4efa64d4nd (pSymbT, var, term) = fromJust mTerm

7fec19672a491661b2fe4b29f685bc7f4efa64d4nd in case qpn of

7fec19672a491661b2fe4b29f685bc7f4efa64d4nd Qual_pred_name symb (Pred_type s _) _

a9d50067373f032c3c9678ad55de69bb3f9fcb70rbowen | symb == pSymb && null ts && null s -> frmIns

| isJust mTerm && symb == pSymbT -> case ts of

Sorted_term (Qual_var v1 _ _) _ _ : args

| v1 == var -> Predication qpn (term : args) ps

_ -> Predication qpn ts ps

_ -> Predication qpn ts ps

, foldConditional = \ t _ _ _ _ -> t }

type FreshVARMap f = Map.Map VAR (TERM f)

{- | buildVMap constructs a mapping between a list of old variables and

corresponding fresh variables based on two lists of VAR_DECL -}

buildVMap :: [VAR_DECL] -> [VAR_DECL] -> FreshVARMap f

buildVMap vDecls fVDecls =

Map.fromList (concat (zipWith toTups vDecls fVDecls))

where toTups (Var_decl vars1 sor1 _) (Var_decl vars2 sor2 _) =

if sor1 == sor2 then zipWith (toTup sor1) vars1 vars2

else error "CASL.Utils.buildVMap"

toTup s v1 v2 = (v1, mkVarTerm v2 s)

{- | specialised lookup in FreshVARMap that ensures that the VAR with

the correct type (SORT) is replaced -}

lookupVMap :: VAR -> SORT -> FreshVARMap f -> Maybe (TERM f)

lookupVMap v s =

maybe Nothing

(\ t -> case t of

Qual_var _ s' _ | s == s' -> Just t

_ -> Nothing)

. Map.lookup v

-- | specialized delete that deletes all shadowed variables

deleteVMap :: [VAR_DECL] -> FreshVARMap f -> FreshVARMap f

deleteVMap vDecls m = foldr Map.delete m

$ concatMap (\ (Var_decl vs _ _) -> vs) vDecls

replaceVarsRec :: FreshVARMap f -> (f -> f) -> Record f (FORMULA f) (TERM f)

replaceVarsRec m mf = (mapRecord mf)

{ foldQual_var = \ qv v s _ ->

fromMaybe qv $ lookupVMap v s m

, foldQuantification = \ orig _ _ _ _ ->

let Quantification q vs f ps = orig

nm = deleteVMap vs m

in Quantification q vs (replaceVarsF nm mf f) ps

}

{- | replaceVars replaces all Qual_var occurences that are supposed

to be replaced according to the FreshVARMap -}

replaceVarsF :: FreshVARMap f

-> (f -> f)

-- ^ this function replaces Qual_var in ExtFORMULA

-> FORMULA f -> FORMULA f

replaceVarsF m = foldFormula . replaceVarsRec m

codeOutUniqueRecord :: (f -> f) -> (f -> f) -> Record f (FORMULA f) (TERM f)

codeOutUniqueRecord rf mf = (mapRecord mf)

{ foldQuantification = \ _ q vDecl f' ps ->

case q of

Unique_existential -> let

eqForms (Var_decl vars1 sor1 _) (Var_decl vars2 sor2 _) =

if sor1 == sor2 then zipWith (eqFor sor1) vars1 vars2

else error "codeOutUniqueRecord1"

eqFor s v1 v2 = Strong_equation (mkVarTerm v1 s)

(mkVarTerm v2 s)

nullRange

{- freshVars produces new variables based on a list

of defined variables

args: (1) set of already used variable names

(2) list of variables -}

freshVars = mapAccumL freshVar

freshVar accSet (Var_decl vars sor _) =

let accSet' = Set.union (Set.fromList vars) accSet

(accSet'', vars') = mapAccumL nVar accSet' vars

in (accSet'', Var_decl vars' sor nullRange)

genVar t i = mkSimpleId $ tokStr t ++ '_' : show i

nVar aSet v =

let v' = fromJust (find (not . flip Set.member aSet)

[genVar v (i :: Int) | i <- [1 ..]])

in (Set.insert v' aSet, v')

(vSet', vDecl') = freshVars Set.empty vDecl

(_vSet'', vDecl'') = freshVars vSet' vDecl

f'_rep_x = replaceVarsF (buildVMap vDecl vDecl') rf f'

f'_rep_y = replaceVarsF (buildVMap vDecl vDecl'') rf f'

allForm = Quantification Universal (vDecl' ++ vDecl'')

(Implication

(Conjunction [f'_rep_x, f'_rep_y] nullRange)

implForm True ps) nullRange

implForm = let fs = concat (zipWith eqForms vDecl' vDecl'') in

case fs of

[] -> error "codeOutUniqueRecord2"

[hd] -> hd

_ -> Conjunction fs nullRange

in Conjunction

[Quantification Existential vDecl f' ps,

allForm] ps

_ -> Quantification q vDecl f' ps

}

{- | 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) -}

codeOutUniqueExtF :: (f -> f)

-- ^ this function replaces Qual_var in ExtFORMULA

-> (f -> f)

-- ^ codes out Unique_existential in ExtFORMULA

-> FORMULA f -> FORMULA f

codeOutUniqueExtF rf = foldFormula . codeOutUniqueRecord rf

codeOutCondRecord :: (Eq f) => (f -> f)

-> Record f (FORMULA f) (TERM f)

codeOutCondRecord fun =

(mapRecord fun)

{ foldPredication =

\ phi _ _ _ ->

either (codeOutConditionalF fun) id

(codeOutCondPredication phi)

, foldExistl_equation = \ o _ _ _ -> case o of

Existl_equation t1 t2 ps ->

either (codeOutConditionalF fun) id

(mkEquationAtom Existl_equation t1 t2 ps)

_ -> error "codeOutCondRecord.foldExistl_equation"

, foldStrong_equation = \ o _ _ _ -> case o of

Strong_equation t1 t2 ps ->

either (codeOutConditionalF fun) id

(mkEquationAtom Strong_equation t1 t2 ps)

_ -> error "codeOutCondRecord.foldStrong_equation"

, foldMembership = \ o _ _ _ -> case o of

Membership t s ps ->

either (codeOutConditionalF fun) id

(mkSingleTermF (`Membership` s) t ps)

_ -> error "codeOutCondRecord.foldMembership"

, foldDefinedness = \ o _ _ -> case o of

Definedness t ps ->

either (codeOutConditionalF fun) id

(mkSingleTermF Definedness t ps)

_ -> error "codeOutCondRecord.foldDefinedness"

}

codeOutCondPredication :: (Eq f) => FORMULA f

-> Either (FORMULA f) (FORMULA f)

{- ^ Left means check again for Conditional,

Right means no Conditional left -}

codeOutCondPredication phi@(Predication _ ts _) =

maybe (Right phi) (Left . constructExpansion phi)

$ listToMaybe $ mapMaybe findConditionalT ts

codeOutCondPredication _ = error "CASL.Utils: Predication expected"

constructExpansion :: (Eq f) => FORMULA f

-> TERM f

-> FORMULA f

constructExpansion atom c@(Conditional t1 phi t2 ps) =

Conjunction [ Implication phi (substConditionalF c t1 atom) False ps

, Implication (Negation phi ps)

(substConditionalF c t2 atom) False ps] ps

constructExpansion _ _ = error "CASL.Utils: Conditional expected"

mkEquationAtom :: (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 -}

mkEquationAtom cons t1 t2 ps =

maybe (Right phi) (Left . constructExpansion phi)

$ listToMaybe $ mapMaybe findConditionalT [t1, t2]

where phi = cons t1 t2 ps

mkSingleTermF :: (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 -}

mkSingleTermF cons t ps =

maybe (Right phi) (Left . constructExpansion phi)

(findConditionalT t)

where phi = cons t ps

{- |

'codeOutConditionalF' implemented via 'CASL.Fold.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)@\'

-}

codeOutConditionalF :: (Eq f) =>

(f -> f)

-> FORMULA f -> FORMULA f

codeOutConditionalF = foldFormula . codeOutCondRecord

findConditionalRecord :: Record f (Maybe (TERM f)) (Maybe (TERM f))

findConditionalRecord =

(constRecord (error "findConditionalRecord")

(listToMaybe . catMaybes) Nothing)

{ foldConditional = \ cond _ _ _ _ -> Just cond }

findConditionalT :: TERM f -> Maybe (TERM f)

findConditionalT =

foldOnlyTerm (error "findConditionalT") findConditionalRecord

substConditionalRecord :: (Eq f)

=> TERM f -- ^ Conditional to search for

-> TERM f -- ^ newly inserted term

-> Record f (FORMULA f) (TERM f)

substConditionalRecord c t = (mapRecord id)

{ foldConditional = \ c1 _ _ _ _ ->

{- FIXME: correct implementation would use an equality

which checks for correct positions also! -}

if c1 == c then t else c1

}

substConditionalF :: (Eq f)

=> TERM f -- ^ Conditional to search for

-> TERM f -- ^ newly inserted term

-> FORMULA f -> FORMULA f

substConditionalF c = foldFormula . substConditionalRecord c

{- |

Subsitute predications with strong equation if it is equivalent to.

-}

eqSubstRecord :: Set.Set PRED_SYMB -- ^ equivalent predicates

-> (f -> f) -> Record f (FORMULA f) (TERM f)

eqSubstRecord eqPredSet extFun =

(mapRecord extFun) {foldPredication = foldPred}

where foldPred _ psymb tList rng =

if Set.member psymb eqPredSet

then Strong_equation (head tList) (tList !! 1) rng

else Predication psymb tList rng

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

substEqPreds eqPredSet = foldFormula . eqSubstRecord eqPredSet