{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}

{- |

Module : $Header$

Description : Handling of extended parameter relations

Copyright : (c) Ewaryst Schulz, DFKI Bremen 2010

License : GPLv2 or higher, see LICENSE.txt

Maintainer : ewaryst.schulz@dfki.de

Stability : experimental

Portability : non-portable

This module defines an ordering on extended parameters and

provides analysis tools. -}

module CSL.EPRelation where

import Control.Monad.Trans

import Control.Monad.Reader

import qualified Data.Map as Map

import qualified Data.Set as Set

import Data.Char

import Data.List

import Data.Maybe

import Data.Tree

import Data.Traversable (fmapDefault)

import System.IO

import CSL.BoolBasic

import qualified CSL.SMTComparison as CMP

import CSL.TreePO

import CSL.AS_BASIC_CSL

import CSL.ExtendedParameter

import Common.Id (tokStr)

import Common.Doc

import Common.DocUtils

{- ----------------------------------------------------------------------

Datatypes for efficient Extended Parameter comparison

---------------------------------------------------------------------- -}

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

particularly for comparison -}

type EPExps = Map.Map String EPExp

evalEPs :: (String -> Int) -> EPExps -> Bool

evalEPs f = Map.foldWithKey g True where

g k v b = evalEP (f k) v && b

prettyEPs :: EPExps -> Doc

prettyEPs eps

| Map.null eps = text "*"

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

showEPs :: EPExps -> String

showEPs = show . prettyEPs

{- | A star expression is the unconstrained expression corresponding to the

whole space of extended parameter values -}

isStarEP :: EPExps -> Bool

isStarEP = Map.null

-- | 'isStarEP' lifted for Range expressions.

isStarRange :: EPRange -> Bool

isStarRange (Atom e) = isStarEP e

isStarRange _ = False

-- | The star range.

starRange :: EPRange

starRange = Atom Map.empty

-- | Conversion function into the more efficient representation.

toEPExps :: [EXTPARAM] -> EPExps

toEPExps = Map.fromList . mapMaybe toEPExp

{- | Sets representing the Parameters for which there is a propagation break

(filtered) and for which there is a constraint (constrained) -}

filteredConstrainedParams :: [EXTPARAM] -> (Set.Set String, Set.Set String)

filteredConstrainedParams = foldl f (Set.empty, Set.empty)

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

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

{- | This type represents the domain of the extended parameters. It can have

0 entries = no restriction

1 entry = opened rectangle, at least one parameter is one sided restricted

2 entries = probably closed rectangle, at least one parameter is restricted

from both sides

The domain is the intersection of both entries (if there are two)

The domain is important for building partitions, because the partitions are

defined only on the domain, not on the unrestricted space.

-}

type EPDomain = [EPExps]

data EPRange = Union [EPRange] | Intersection [EPRange]

| Complement EPRange | Atom EPExps | Empty

-- | In some cases 'EPRange' can be translated back to 'EPExps'

tryDowncast :: EPRange -> Maybe EPExps

tryDowncast (Complement (Atom x)) =

if Map.size x == 1 then Just $ Map.map complementEP x else Nothing

tryDowncast (Atom x) = Just x

tryDowncast _ = Nothing

evalRange :: (String -> Int) -> EPRange -> Bool

evalRange f re =

case re of

Complement r -> not $ evalRange f r

Union l -> any (evalRange f) l

Intersection l -> all (evalRange f) l

Empty -> False

Atom eps -> evalEPs f eps

{- | A diagnostic output for 'EPRange' which highlights problems in the

internal representation -}

diagnoseEPRange :: EPRange -> Doc

diagnoseEPRange re =

let asIfx s l = parens $ fsep $ punctuate (text s) $ map diagnoseEPRange l

diag s re' = text "DIAG" <>

parens (text s <> comma <+> diagnoseEPRange re')

in case re of

Union [] -> diag "EmptyUnion" Empty

Union [x] -> diag "SingletonUnion" x

Union l -> asIfx [' ', chr 8746] l

Intersection [] -> diag "EmptyIntersection" Empty

Intersection [x] -> diag "SingletonIntersection" x

Intersection [x, Complement r] -> asIfx [' ', chr 8726] [x, r]

Intersection l -> asIfx [' ', chr 8745] l

Complement r -> text [chr 8705] <> diagnoseEPRange r

Empty -> text [chr 8709]

Atom eps -> prettyEPs eps

{-

to see what you get here use:

writeFile "/tmp/t.txt" $ map chr [8746, 10, 8726, 10, 8745, 10, 8705, 10, 8709]

you will see: union, difference, intersection, complement, emptyset

-}

-- | Pretty output for 'EPRange'

prettyEPRange :: EPRange -> Doc

prettyEPRange re =

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

g s l = parens $ hsep $ text s : map prettyEPRange l

in case re of

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

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

Complement r -> g "C" [r]

Union l -> g "Union" l

Intersection l -> g "Intersection" l

Empty -> text "Empty"

Atom eps -> prettyEPs eps

mkUnion :: [EPRange] -> EPRange

mkUnion [] = error "mkUnion: empty list"

mkUnion [x] = x

mkUnion l = Union l

mkIntersection :: [EPRange] -> EPRange

mkIntersection [] = error "mkIntersection: empty list"

mkIntersection [x] = x

mkIntersection l = Intersection l

showEPRange :: EPRange -> String

showEPRange = show . prettyEPRange

instance Show EPRange where

show = showEPRange

instance Pretty EPRange where

pretty = prettyEPRange

{- | Behaves as a map on the list of leafs of the range expression

(from left to right) -}

mapRangeLeafs :: (EPExps -> b) -> EPRange -> [b]

mapRangeLeafs f re =

case re of

Union l -> g l

Intersection l -> g l

Complement r -> mapRangeLeafs f r

Atom eps -> [f eps]

Empty -> []

where g = concatMap (mapRangeLeafs f)

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

mapRange :: (EPExps -> EPExps) -> EPRange -> EPRange

mapRange f re =

case re of

Union l -> Union $ g l

Intersection l -> Intersection $ g l

Complement r -> Complement $ mapRange f r

Atom eps -> Atom $ f eps

_ -> re

where g = map (mapRange f)

class RangeUtils a where

rangeNames :: a -> Set.Set String

instance RangeUtils EPExps where

rangeNames = Map.keysSet

instance RangeUtils EPRange where

rangeNames = Set.unions . mapRangeLeafs rangeNames

namesInList :: RangeUtils a => [a] -> Set.Set String

namesInList = Set.unions . map rangeNames

{- |

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

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

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

these extended parameters

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

with the second one.

-}

projectEPs :: EPExps -> EPExps -> Maybe EPExps

projectEPs e1 e2

| isStarEP e1 = Just e2

| otherwise =

-- take first element from e1 delete it from e1 and proceed with it

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

e2' = Map.delete k e2

in case Map.lookup k e2 of

Nothing -> projectEPs e1' e2

Just v2 ->

case compareEP v v2 of

Incomparable Disjoint -> Nothing

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

else error $ "projectEPs: e1 > e2 "

++ show (e1, e2)

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

{- |

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

parameters), we instantiate it partially with the given

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

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

atomic subexpressions in A which talk about x

(1) by the subexpression

where the constraint for x is removed if the given instantiation

satisfies this subexpression (e.g., x<10) or

(2) by 'Empty' if this

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

-}

projectRange :: EPExps -> EPRange -> EPRange

projectRange e re = simplifyRange $ f re

where f rexp =

case rexp of

Union l -> Union $ map f l

Intersection l -> Intersection $ map f l

Complement r -> Complement $ f r

Atom eps -> case projectEPs e eps of

Nothing -> Empty

Just eps' -> Atom eps'

Empty -> Empty

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

Union [,*,] -> * (top element)

Intersection [,*,] -> Intersection [,] (neutral element)

Complement * -> Empty (bottom element)

For Empty its the Union-Intersection-dual behaviour

-}

simplifyRange :: EPRange -> EPRange

simplifyRange re =

case tryDowncast re of

Just eps -> Atom eps

_ ->

case re of

Union l -> f [] l

Intersection l -> g [] l

Complement r ->

case simplifyRange r of

Empty -> starRange

r' | isStarRange r' -> Empty

| otherwise -> Complement r'

_ -> re

where -- returns either a simplified list or a new expression

f acc [] = if null acc then Empty else mkUnion acc

f acc (r : l) =

case simplifyRange r of

Empty -> f acc l

r' | isStarRange r' -> r'

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

g acc [] = if null acc then starRange else mkIntersection acc

g acc (r : l) =

case simplifyRange r of

Empty -> Empty

r' | isStarRange r' -> g acc l

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

{- ----------------------------------------------------------------------

Models for 'EPRange' expressions

---------------------------------------------------------------------- -}

data Model a = Model [(Int, Int)] (Map.Map [Int] a)

boolModelChar :: Bool -> Char

boolModelChar b = if b then '*' else ' '

modelToString :: (a -> Char) -> Model a -> String

modelToString f (Model l vm) =

case l of

[(a, b)] -> map (f . h . (: [])) [a .. b] ++ "\n"

[(a, b), (c, d)] ->

let g y = map (f . (vm Map.!)) [[x, y] | x <- [a .. b]]

in unlines $ map g [c .. d]

[] -> ""

_ -> concat ["Cannot output a ", show $ length l, "-dim model"]

where err x = error $ concat [ "modelToString: elem not in map "

, show x, "\n", show $ Map.keys vm ]

h x = Map.findWithDefault (err x) x vm

modelOf :: Map.Map String (Int, Int) -> EPRange -> Model Bool

modelOf rm re = let

f l s = l !! Map.findIndex s rm

g (a, b) l = [x : y | y <- l, x <- [a .. b]]

inpl = Map.fold g [[]] rm

h x = (x, evalRange (f x) re)

in Model (Map.elems rm) $ Map.fromList $ map h inpl

{- ----------------------------------------------------------------------

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 -> SetOrdering

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'

{-

we need to take into account the global constraints on the range of the

extended parameters, e.g., I in [1,5] or I>=0...

This complicates the simple comparison and we postpone it for the moment.

-- | We try to decide the relation between the given ranges without using

-- an external decision procedure.

trySimpleFullCmp :: EPRange -> EPRange -> Maybe (SetOrdering, Bool, Bool)

trySimpleFullCmp r1 r2

| isStarRange r1 && r1 == r2 = Just (Comparable EQ, False, False)

| r1 == Empty && r1 == r2 = Just (Comparable EQ, True, True)

| otherwise =

case map tryDowncast [r1, r2] of

[Just eps1, Just eps2] -> Just (compareEPs eps1 eps2, False, False)

_ -> Nothing

{- | Same as 'trySimpleFullCmp' but without deciding

if the ranges are empty or not -}

trySimpleCmp :: EPRange -> EPRange -> Maybe (SetOrdering, Bool, Bool)

trySimpleCmp r1 r2

| isStarRange r1 = Just (Comparable GT, False, r2 == Empty)

| isStarRange r2 = Just (Comparable LT, r1 == Empty, False)

-}

{- ----------------------------------------------------------------------

SMT based comparison - utility functions

---------------------------------------------------------------------- -}

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

Variable names are composed from the string "x" together with an integer. -}

boolExps :: CMP.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 :: CMP.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

{- ----------------------------------------------------------------------

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'. We need to check if the new node subsumes

a nonempty subset of the given forrest. -}

insertEPNodeToForest :: EPTree a {- ^ Node to insert, assumed to have an

empty subforest (the subforest is ignored) -}

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

-> EPForest a -- ^ Resulting forest

insertEPNodeToForest n [] = [n]

insertEPNodeToForest n ft@(t : rft) =

if null ssf then

case insertEPNode n t of

Just t' -> t' : rft

Nothing -> t : insertEPNodeToForest n rft

else n {subForest = ssf} : nssf

where (ssf, nssf) = getSubsumedForest (eplabel $ rootLabel n) ft

{- | Splits the given forest to a by the 'EPExps' subsumed part and a not

subsumed part. Errors are reported in situations which would lead to invalid

forests when used in the 'insertEPNodeToForest'-method. -}

getSubsumedForest :: EPExps -- ^ Expression to be checked against the forest

-> EPForest a -- ^ Forest to be checked for being subsumed

-> (EPForest a, EPForest a) -- ^ Subsumed forest and the rest

getSubsumedForest eps = partition p where

ep2 = eplabel . rootLabel

p t = case compareEPs eps (ep2 t) of

Comparable EQ ->

error $ concat [ "getSubsumedForest: equality "

, "overlap ", show $ prettyEPs eps, " = "

, show $ prettyEPs (ep2 t) ]

Incomparable Overlap ->

error $ concat [ "getSubsumedForest: overlap "

, show $ prettyEPs eps, " = "

, show $ prettyEPs (ep2 t) ]

Comparable GT -> True

_ -> False

{- | 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 = foldr (insertEPNodeToForest . f) []

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

instance Pretty a => Pretty (EPNodeLabel a) where

pretty x = parens $ prettyEPs (eplabel x) <> colon <+> pretty (nodelabel x)

instance Pretty a => Show (EPNodeLabel a) where

show = show . pretty

{- ----------------------------------------------------------------------

Partitions based on 'EPRange'

---------------------------------------------------------------------- -}

class MonadIO m => CompareIO m where

rangeFullCmp :: EPRange -> EPRange -> m (SetOrdering, Bool, Bool)

logMessage :: String -> m ()

logMessage _ = return ()

rangeCmp :: CompareIO m => EPRange -> EPRange -> m SetOrdering

rangeCmp x y = liftM fst3 $ rangeFullCmp x y where

fst3 (a, _, _) = a

type SmtComparer = ReaderT CMP.VarEnv IO

execSMTComparer :: CMP.VarEnv -> SmtComparer a -> IO a

execSMTComparer ve smt = runReaderT smt ve

instance CompareIO SmtComparer where

logMessage s = do

ve <- ask

case CMP.loghandle ve of

Just hdl -> liftIO $ hPutStrLn hdl s

_ -> return ()

rangeFullCmp r1 r2 = do

ve <- ask

let vm = CMP.varmap ve

lift $ CMP.smtCompare ve (boolRange vm r1) $ boolRange vm r2

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

instance Show a => Show (Partition a) where

show p = show $ prettyPartition (text . show) p

prettyPartition :: (a -> Doc) -> Partition a -> Doc

prettyPartition f (AllPartition x) = braces $ braces $ f x

prettyPartition f (Partition l) = braces $ sepByCommas $ map (braces . g) l

where g (r, x) = f x <+> text "|" <+> prettyEPRange r

instance Pretty a => Pretty (Partition a) where

pretty (AllPartition x) = text "AllPartition:" <+> pretty x

pretty (Partition l) = text "Partition:" <+>

ppPairlist pretty pretty braces vcat f l

where f a b = parens $ a <+> text "|" <+> b

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)

{- | Two partitions are refined to a result partition which is finer than each

of the input partitions.

The annotations of the new partition are as follows:

a set @x@ in the new partition gets the annotation @(a,b)@ where @x'@ comes

from the first partition and is annotated with @a@ and @x''@ comes

from the second partition and is annotated with @b@ and @x@ is a subset of

both, @x'@ and @x''@.

-}

refinePartition :: (CompareIO m, Pretty a, Pretty b) => Partition a

-> Partition b -> m (Partition (a, b))

refinePartition (AllPartition x) pb = return $ fmap ((,) x) pb

refinePartition pa (AllPartition x) = return $ fmap (flip (,) x) pa

refinePartition (Partition l) (Partition l') =

liftM (Partition . concat) $ mapM (f l') l

where

f [] _ = return []

f ((er', y) : ll) a@(er, x) = do

cmp <- rangeCmp er er'

let er'' = Intersection [er, er']

case cmp of

Comparable GT -> liftM ((er', (x, y)) :) $ f ll a

Incomparable Disjoint -> f ll a

Incomparable Overlap -> liftM ((er'', (x, y)) :) $ f ll a

-- this case combine LT and EQ

_ -> return [(er, (x, y))]

{- | The partition is restricted explicitly to the given range, that is,

each set of the partition is intersected with the set from the range

and the empty sets are filtered out.

-}

restrictPartition :: (CompareIO m, Pretty a) =>

EPRange -> Partition a -> m (Partition a)

restrictPartition er p

| isStarRange er = return p

| otherwise =

case p of

AllPartition x -> return $ Partition [(er, x)]

Partition p' -> liftM Partition $ f p'

where

f [] = return []

f ((er', x) : l) = do

cmp <- rangeCmp er er'

let er'' = Intersection [er, er']

case cmp of

Comparable EQ -> return [(er', x)]

Comparable LT -> return [(er, x)]

Comparable GT -> liftM ((er', x) :) $ f l

Incomparable Disjoint -> f l

Incomparable Overlap -> liftM ((er'', x) :) $ f l