4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{-# LANGUAGE TypeSynonymInstances #-}

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner{- |

5ba323da9f037264b4a356085e844889aedeac23Christian MaederModule : $Header$

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaederDescription : Handling of extended parameter relations

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuCopyright : (c) Ewaryst Schulz, DFKI Bremen 2010

23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian MaederLicense : GPLv2 or higher, see LICENSE.txt

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederMaintainer : ewaryst.schulz@dfki.de

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederStability : experimental

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederPortability : non-portable

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder

23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian MaederThis module defines an ordering on extended parameters and provides analysis tools.

23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder -}

23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maedermodule CSL.EPRelation where

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport qualified Data.Map as Map

af621d0066770895fd79562728e93099c8c52060Christian Maederimport qualified Data.Set as Set

7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maederimport Data.Maybe

167b6ed8639bce096380defb7311ded501ebb5daChristian Maederimport Data.Tree

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Data.List

79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian Maederimport Data.Traversable (fmapDefault)

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maederimport System.Process

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maederimport System.IO.Unsafe

c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maeder

c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maederimport CSL.EPBasic

c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maederimport CSL.TreePO

c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maederimport CSL.AS_BASIC_CSL

c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maederimport CSL.ExtendedParameter as EP

c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maeder (toBoolRep, showEP, toEPExp, EPExp, compareEP)

c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maederimport Common.Id (tokStr)

c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maeder

c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maederimport Common.Doc

c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maeder

c0ef189e724dfd960074248c97fb01dfa5842a5cChristian Maeder-- ----------------------------------------------------------------------

f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder-- * Datatypes for efficient Extended Parameter comparison

024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder-- ----------------------------------------------------------------------

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- | A more efficient representation of a list of extended parameters,

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- particularly for comparison

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maedertype EPExps = Map.Map String EPExp

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederprettyEPs :: EPExps -> Doc

afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederprettyEPs eps

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder | Map.null eps = text "*"

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder | otherwise = brackets $ sepByCommas $ map (text . showEP) $ Map.toList eps

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedershowEPs :: EPExps -> String

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedershowEPs = show . prettyEPs

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- | A star expression is the unconstrained expression corresponding to the

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- whole space of extended parameter values

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederisStarEP :: EPExps -> Bool

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederisStarEP = Map.null

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- | 'isStarEP' lifted for Range expressions.

afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederisStarRange :: EPRange -> Bool

afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederisStarRange (Atom e) = isStarEP e

afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederisStarRange _ = False

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | The star range.

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederstarRange :: EPRange

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederstarRange = Atom Map.empty

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder-- | Conversion function into the more efficient representation.

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedertoEPExps :: [EXTPARAM] -> EPExps

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedertoEPExps = Map.fromList . mapMaybe toEPExp

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- | Sets representing the Parameters for which there is a propagation break

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder-- (filtered) and for which there is a constraint (constrained)

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederfilteredConstrainedParams :: [EXTPARAM] -> (Set.Set String, Set.Set String)

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederfilteredConstrainedParams = foldl f (Set.empty, Set.empty)

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder where f (fs, cs) (EP t "-|" _) = (Set.insert (tokStr t) fs, cs)

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder f (fs, cs) (EP t _ _) = (fs, Set.insert (tokStr t) cs)

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederdata EPRange = Union [EPRange] | Intersection [EPRange]

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder | Complement EPRange | Atom EPExps | Empty

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederprettyEPRange :: EPRange -> Doc

792df0347edab377785d98c63e2be8e2ce0a8bdeChristian MaederprettyEPRange re =

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder let f s a b = parens $ hsep [prettyEPRange a, text s, prettyEPRange b]

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder g s l = parens $ hsep $ text s : map prettyEPRange l

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder in case re of

d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder Union [r1, r2] -> f "Un" r1 r2

d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder Intersection [r1, r2] -> f "In" r1 r2

986e0e9cf8c2358f455460b3fc75ce7c5dcf0973Christian Maeder Complement r -> g "C" [r]

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder Union l -> g "Union" l

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder Intersection l -> g "Intersection" l

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder Empty -> text "Empty"

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder Atom eps -> prettyEPs eps

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder

167b6ed8639bce096380defb7311ded501ebb5daChristian MaedershowEPRange :: EPRange -> String

167b6ed8639bce096380defb7311ded501ebb5daChristian MaedershowEPRange = show . prettyEPRange

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder

167b6ed8639bce096380defb7311ded501ebb5daChristian Maederinstance Show EPRange where

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder show = showEPRange

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder-- | Behaves as a map on the list of leafs of the range expression

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder-- (from left to right)

167b6ed8639bce096380defb7311ded501ebb5daChristian MaedermapRangeLeafs :: (EPExps -> b) -> EPRange -> [b]

167b6ed8639bce096380defb7311ded501ebb5daChristian MaedermapRangeLeafs f re =

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder case re of

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder Union l -> g l

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder Intersection l -> g l

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder Complement r -> mapRangeLeafs f r

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder Atom eps -> [f eps]

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder Empty -> []

6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder where g = concatMap (mapRangeLeafs f)

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder-- | Maps an EP expression transformer over the given range expression

59c301c268f79cfde0a4c30a2c572a368db98da5Christian MaedermapRange :: (EPExps -> EPExps) -> EPRange -> EPRange

59c301c268f79cfde0a4c30a2c572a368db98da5Christian MaedermapRange f re =

5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maeder case re of

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder Union l -> Union $ g l

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder Intersection l -> Intersection $ g l

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder Complement r -> Complement $ mapRange f r

0a320bc4cdbf38f480b75ac15a54db1c4885b497Christian Maeder Atom eps -> Atom $ f eps

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder _ -> re

31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder where g = map (mapRange f)

31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder

31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maederclass RangeUtils a where

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder rangeNames :: a -> Set.Set String

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder

167b6ed8639bce096380defb7311ded501ebb5daChristian Maederinstance RangeUtils EPExps where

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder rangeNames = Map.keysSet

167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder

167b6ed8639bce096380defb7311ded501ebb5daChristian Maederinstance RangeUtils EPRange where

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder rangeNames = Set.unions . mapRangeLeafs rangeNames

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaedernamesInList :: RangeUtils a => [a] -> Set.Set String

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaedernamesInList = Set.unions . map rangeNames

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder-- TODO: check the todos at the end for projection-fix

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder

964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder{- |

997c56f3bc74a703043010978e5013fdb074d659Christian Maeder (1) If the arguments are disjoint -> 'Nothing'

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder (2) If all extended parameter constraints from the first argument are

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder subsumed by the second argument -> second argument with deleted entries for

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder these extended parameters

8485da94b57d8b5135ee685b55c982b037ed4140Christian Maeder (3) Otherwise -> error: the first argument must be subsumed by or disjoint

8485da94b57d8b5135ee685b55c982b037ed4140Christian Maeder with the second one.

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder-}

e76e6a43f51438215737d6fc176c89da05bb86daChristian MaederprojectEPs :: EPExps -> EPExps -> Maybe EPExps

e76e6a43f51438215737d6fc176c89da05bb86daChristian MaederprojectEPs e1 e2

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder | isStarEP e1 = Just e2

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder | otherwise =

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder -- take first element from e1 delete it from e1 and proceed with it

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder let ((k, v), e1') = Map.deleteFindMin e1

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder e2' = Map.delete k e2

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder in case Map.lookup k e2 of

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder Nothing -> projectEPs e1' e2

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder Just v2 ->

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder case compareEP v v2 of

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Incomparable Disjoint -> Nothing

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder Comparable x -> if x /= GT then projectEPs e1' e2'

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder else error $ "projectEPs: e1 > e2 "

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder ++ show (e1,e2)

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder _ -> error $ "projectEPs: overlap " ++ show (e1,e2)

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder{- |

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder Given a range predicate, e.g, A x y z (here with three extended

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder parameters), we instantiate it partially with the given

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder instantiation, e.g., x=1, and obtain A 1 y z. The new predicate

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder does not depend on x anymore and can be built by replacing all

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder atomic subexpressions in A which talk about x (1) by the subexpression

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder where the constraint for x is removed if the given instantiation

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder satisfies this subexpression (e.g., x<10) or (2) by 'Empty' if this

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder constraint is not satisfied (e.g., x>1)

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-}

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaederprojectRange :: EPExps -> EPRange -> EPRange

f6f2955769bfe80dbb4cca3b3ee33c5a8a0f5355Christian MaederprojectRange e re = simplifyRange $ f re

c1031ac42b3f3d7d0fe7d9d6b54423a092d473a0Christian Maeder where f rexp =

fce77b2785912d1abbcc3680088b235f534bdeffChristian Maeder case rexp of

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Union l -> Union $ map f l

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder Intersection l -> Intersection $ map f l

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder Complement r -> Complement $ f r

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Atom eps -> case projectEPs e eps of

ac19566dc64536c38b5d1d3ae510fb8a07784c2fChristian Maeder Nothing -> Empty

039b7a8265baaeab2ded2a3e3826c04f13364d87Christian Maeder Just eps' -> Atom eps'

fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder Empty -> Empty

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder

039b7a8265baaeab2ded2a3e3826c04f13364d87Christian Maeder{- | Removes all star- and empty-entries from inside of the range expression.

ac19566dc64536c38b5d1d3ae510fb8a07784c2fChristian Maeder

3cafc73a998493f9ed3d5e934c0ab80bcfb465c2Christian Maeder Union [,*,] -> * (top element)

7bf6d421b0ea31ae63f1fe04919942b931abda47Christian Maeder Intersection [,*,] -> Intersection [,] (neutral element)

021d7137df04ec1834911d99d90243a092841cedChristian Maeder Complement * -> Empty (bottom element)

021d7137df04ec1834911d99d90243a092841cedChristian Maeder

7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maeder For Empty its the dual behaviour

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder-}

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedersimplifyRange :: EPRange -> EPRange

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaedersimplifyRange re =

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder case re of

7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maeder Union l -> f [] l

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder Intersection l -> g [] l

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder Complement r ->

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder case simplifyRange r of

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Empty -> starRange

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder r' | isStarRange r' -> Empty

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder | otherwise -> Complement r'

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder _ -> re

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder where -- returns either a simplified list or a new expression

908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder f acc [] = if null acc then Empty else Union acc

908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder f acc (r:l) =

908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder case simplifyRange r of

908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder Empty -> f acc l

bb3bdd4a260606a6184b5f5a5774ca6632ca597aChristian Maeder r' | isStarRange r' -> r'

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder | otherwise -> f (acc++[r']) l

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder g acc [] = if null acc then starRange else Intersection acc

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder g acc (r:l) =

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder case simplifyRange r of

7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder Empty -> Empty

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder r' | isStarRange r' -> g acc l

| otherwise -> g (acc++[r']) l

-- ----------------------------------------------------------------------

-- * Extended Parameter comparison

-- ----------------------------------------------------------------------

{- | Compares two 'EPExps': They are pairwise compared over the common

extended parameter names (see also the operator-table in combineCmp).

This function can be optimized in returning directly disjoint

once a disjoint subresult encountered.

-}

compareEPs :: EPExps -> EPExps -> EPCompare

compareEPs eps1 eps2 =

-- choose smaller map for fold, and remember if maps are swapped

let (eps, eps', sw) = if Map.size eps1 > Map.size eps2

then (eps2, eps1, True) else (eps1, eps2, False)

-- foldfunction

f k ep (b, c) = let (cmp', c') =

case Map.lookup k eps' of

-- increment the counter

Just ep' -> (compareEP ep ep', c+1)

-- if key not present in reference map then

-- ep < *

_ -> (Comparable LT, c)

in (combineCmp b cmp', c')

-- we fold over the smaller map, which can be more efficient.

-- We have to count the number of matched parameter names to see if

-- there are still EPs in eps' which indicates to compare with ">" at

-- the end of the fold.

(epc, cnt) = Map.foldWithKey f

(Comparable EQ, 0) -- start the fold with "=",

-- the identity element

eps -- the smaller map

epc' = if Map.size eps' > cnt

then combineCmp (Comparable GT) epc else epc

-- if the maps were swapped then swap the result

in if sw then swapCmp epc' else epc'

-- ----------------------------------------------------------------------

-- * SMT output generation for smt based comparison

-- ----------------------------------------------------------------------

type VarMap = Map.Map String Int

-- | Generates from a list of Extended Parameter names an id-mapping

varMapFromList :: [String] -> VarMap

varMapFromList l = Map.fromList $ zip l $ [1 .. length l]

-- | Generates from a list of Extended Parameter names an id-mapping

varMapFromSet :: Set.Set String -> VarMap

varMapFromSet = varMapFromList . Set.toList

-- | Builds a Boolean representation from the extended parameter expression

boolExps :: VarMap -> EPExps -> BoolRep

boolExps m eps | isStarEP eps = trueBool

| otherwise = And $ map f $ Map.assocs eps where

err = error "boolExps: No matching"

f (k, v) = toBoolRep ("x" ++ show (Map.findWithDefault err k m)) v

boolRange :: VarMap -> EPRange -> BoolRep

boolRange m (Union l) = Or $ map (boolRange m) l

boolRange m (Intersection l) = And $ map (boolRange m) l

boolRange m (Complement a) = Not $ boolRange m a

boolRange m (Atom eps) = boolExps m eps

boolRange _ Empty = falseBool

-- TODO: put this rather into another module and replace EPRange by BoolRep

smtPredDef :: VarMap -> String -> BoolRep -> String

smtPredDef m s b = concat [ "(define ", s, "::(-> "

, concatMap (const "int ") $ smtVars m ""

, "bool) (lambda ("

, concatMap (++ "::int ") $ smtVars m "x", ") "

, smtBoolExp b, "))" ]

smtVarDef :: VarMap -> String

smtVarDef m =

unlines $ map (\ x -> "(define " ++ x ++ " ::int)") $ smtVars m "y"

smtVars :: VarMap -> String -> [String]

smtVars m s = map ((s++) . show) [1 .. Map.size m]

smtGenericStmt :: VarMap -> String -> String -> String -> String

smtGenericStmt m s a b =

let vl = concat $ map (" "++) $ smtVars m "y"

in "(assert+ (not (" ++ s ++ " (" ++ a ++ vl ++ ") (" ++ b ++ vl ++ "))))"

smtEQStmt :: VarMap -> String -> String -> String

smtEQStmt m a b = smtGenericStmt m "=" a b

smtLEStmt :: VarMap -> String -> String -> String

smtLEStmt m a b = smtGenericStmt m "=>" a b

smtDisjStmt :: VarMap -> String -> String -> String

smtDisjStmt m a b =

let vl = concat $ map (" "++) $ smtVars m "y"

in "(assert+ (and (" ++ a ++ vl ++ ") (" ++ b ++ vl ++ ")))"

smtAllScript :: VarMap -> EPRange -> EPRange -> String

smtAllScript m r1 r2 =

unlines [ smtScriptHead m r1 r2

, smtEQStmt m "A" "B", "(check) (retract 1)"

, smtLEStmt m "A" "B", "(check) (retract 2)"

, smtLEStmt m "B" "A", "(check) (retract 3)"

, smtDisjStmt m "A" "B", "(check)" ]

smtAllScripts :: VarMap -> EPRange -> EPRange -> [String]

smtAllScripts m r1 r2 =

let h = smtScriptHead m r1 r2

in [ unlines [h, smtEQStmt m "A" "B", "(check)"]

, unlines [h, smtLEStmt m "A" "B", "(check)"]

, unlines [h, smtLEStmt m "B" "A", "(check)"]

, unlines [h, smtDisjStmt m "A" "B", "(check)"]

]

smtScriptHead :: VarMap -> EPRange -> EPRange -> String

smtScriptHead m r1 r2 = unlines [ "(set-arith-only! true)"

, smtPredDef m "A" $ boolRange m r1

, smtPredDef m "B" $ boolRange m r2

, smtVarDef m ]

smtGenericScript :: VarMap -> (VarMap -> String -> String -> String)

-> EPRange -> EPRange -> String

smtGenericScript m f r1 r2 = smtScriptHead m r1 r2 ++ "\n" ++ f m "A" "B"

smtEQScript :: VarMap -> EPRange -> EPRange -> String

smtEQScript m r1 r2 = smtGenericScript m smtEQStmt r1 r2

smtLEScript :: VarMap -> EPRange -> EPRange -> String

smtLEScript m r1 r2 = smtGenericScript m smtLEStmt r1 r2

smtDisjScript :: VarMap -> EPRange -> EPRange -> String

smtDisjScript m r1 r2 = smtGenericScript m smtDisjStmt r1 r2

data SMTStatus = Sat | Unsat deriving (Show, Eq)

smtCheck :: VarMap -> EPRange -> EPRange -> IO [SMTStatus]

smtCheck m r1 r2 = smtMultiResponse $ smtAllScript m r1 r2

smtCheck' :: VarMap -> EPRange -> EPRange -> IO [SMTStatus]

smtCheck' m r1 r2 = mapM smtResponse $ smtAllScripts m r1 r2

-- | The result states of the smt solver are translated to the

-- adequate compare outcome. The boolean value is true if the corresponding

-- set is empty.

smtStatusCompareTable :: [SMTStatus] -> (EPCompare, Bool, Bool)

smtStatusCompareTable l =

case l of

[Unsat, Unsat, Unsat, x] -> let b = x == Unsat in (Comparable EQ, b, b)

[Sat, Unsat, Sat, x] -> let b = x == Unsat in (Comparable LT, b, b)

[Sat, Sat, Unsat, x] -> let b = x == Unsat in (Comparable GT, b, b)

[Sat, Sat, Sat, Unsat] -> (Incomparable Disjoint, False, False)

[Sat, Sat, Sat, Sat] -> (Incomparable Overlap, False, False)

x -> error $ "smtStatusCompareTable: malformed status " ++ show x

smtCompare :: VarMap -> EPRange -> EPRange -> EPCompare

smtCompare m r1 r2 =

let (c, _, _) = smtStatusCompareTable $ unsafePerformIO $ smtCheck m r1 r2

in c

smtFullCompare :: VarMap -> EPRange -> EPRange -> (EPCompare, Bool, Bool)

smtFullCompare m r1 r2 = smtStatusCompareTable $ unsafePerformIO $ smtCheck m r1 r2

smtCompare' :: VarMap -> EPRange -> EPRange -> EPCompare

smtCompare' m r1 r2 =

let (c, _, _) = smtStatusCompareTable $ unsafePerformIO $ smtCheck' m r1 r2

in c

smtResponseToStatus :: String -> SMTStatus

smtResponseToStatus s

| s == "sat" = Sat

| s == "unsat" = Unsat

| s == "" = Sat

| isInfixOf "Error" s = error $ "yices-error: " ++ s

| otherwise = error $ "unknown yices error"

smtMultiResponse :: String -> IO [SMTStatus]

smtMultiResponse inp = do

s <- readProcess "yices" [] inp

return $ map smtResponseToStatus $ lines s

smtResponse :: String -> IO SMTStatus

smtResponse inp = do

s <- readProcess "yices" [] inp

-- putStrLn "------ yices output ------"

-- putStrLn s

return $ smtResponseToStatus $

case lines s of

[] -> ""

x:_ -> x

-- ----------------------------------------------------------------------

-- * Trees to store Extended Parameter indexed values

-- ----------------------------------------------------------------------

{- | We use trees with special labels of this type.

In two assignments of the same constant we don't allow the

extended parameter part to overlap. Hence we can store the

definiens of assignments in a tree indexed by the extended

parameters. The labels of the tree contain the extended parameter

and an arbitrary value and all elements in the subforest have a

label with an extended parameter lower than the extended

parameter at the root node.

-}

data EPNodeLabel a = EPNL { eplabel :: EPExps

, nodelabel :: a }

type EPTree a = Tree (EPNodeLabel a)

type EPForest a = Forest (EPNodeLabel a)

makeEPLeaf :: a -> EPExps -> EPTree a

makeEPLeaf x eps = Node { rootLabel = EPNL { eplabel = eps, nodelabel = x }

, subForest = [] }

-- | Inserts a node to an 'EPForest'.

insertEPNodeToForest :: EPTree a -- ^ Node to insert

-> EPForest a -- ^ Forest to insert the given node in

-> EPForest a -- ^ Resulting forest

insertEPNodeToForest n [] = [n]

insertEPNodeToForest n (t:ft) = case insertEPNode n t of

Just t' -> t': ft

Nothing -> t : insertEPNodeToForest n ft

-- | Inserts a node to an 'EPTree' and if the nodes are disjoint

-- 'Nothing' is returned. Both insert methods return an error if an

-- overlapping occurs.

insertEPNode :: EPTree a -- ^ Node to insert

-> EPTree a -- ^ Tree to insert the given node in

-> Maybe (EPTree a) -- ^ Resulting tree

insertEPNode n t =

case compareEPs ep1 ep2 of

Comparable EQ -> error $ concat [ "insertEPNode: equality overlap "

, show ep1, " = ", show ep2 ]

Incomparable Overlap -> error $ concat [ "insertEPNode: overlap "

, show ep1, " = ", show ep2 ]

Incomparable Disjoint -> Nothing

Comparable GT -> aInB t n

Comparable LT -> aInB n t

where

aInB a b = Just b { subForest = insertEPNodeToForest a (subForest b) }

ep1 = eplabel $ rootLabel n

ep2 = eplabel $ rootLabel t

-- | Returns a graphical representation of the forest.

showEPForest :: (a -> String) -> EPForest a -> String

showEPForest pr =

let f lbl = showEPs (eplabel lbl)

++ case pr $ nodelabel lbl of

[] -> []

x -> ": " ++ x

in drawForest . (map $ fmapDefault f)

-- | This function is not a simple map, but inserts the nodes correctly

-- to the tree.

forestFromEPsGen :: (a -> EPTree b) -> [a] -> EPForest b

forestFromEPsGen f l = foldr (insertEPNodeToForest . f) [] l

-- | This function is not a simple map, but inserts the nodes correctly

-- to the tree.

forestFromEPs :: (a -> (b, EPExps)) -> [a] -> EPForest b

forestFromEPs f = forestFromEPsGen $ uncurry makeEPLeaf . f

-- ----------------------------------------------------------------------

-- * Partitions based on 'EPRange'

-- ----------------------------------------------------------------------

data Partition a = AllPartition a | Partition [(EPRange, a)]

instance Functor Partition where

fmap f (AllPartition x) = AllPartition $ f x

fmap f (Partition l) = Partition $ map g l

where g (er, x) = (er, f x)

refinePartition :: Partition a -> Partition b -> Partition (a,b)

refinePartition pa pb = error ""

restrictPartition :: EPRange -> Partition a -> Partition a

restrictPartition er pb = error ""