{- |
Module : ./CSL/GeneralExtendedParameter.hs
Description : Handling of extended parameters
Copyright : (c) Ewaryst Schulz, DFKI Bremen 2010
License : GPLv2 or higher, see LICENSE.txt
Maintainer : ewaryst.schulz@dfki.de
Stability : experimental
Portability : portable
This module defines an ordering on extended parameters and other analysis tools.
Extended parameters may be based on one of the following
relations:
> =, <=, >=, !=, <, >, -|
We work more generally (compared to CSL.ExtendedParameter) with a
sequence of intervals which generalizes sets representable by
the given relations and with the advantage that this
representation is closed under union, intersection and
complement. Such sequences are represented by an ordered
sequence of intervals.
A sequence of intervals [a_i, b_i] is normalized when for all i
b_i + 1 < a_{i+1}
This implies that this sequence is
1. nonoverlapping (I_i and I_j are disjoint for i/=j)
2. noncontinuing (The union of I_i and I_{i+1} is not an interval)
3. ordered (i<j => !x,y. x in I_i and y in I_j => x < y)
-}
module CSL.GeneralExtendedParameter where
import Data.List (intercalate)
import CSL.BoolBasic
import CSL.TreePO
import CSL.AS_BASIC_CSL
import Common.Id (tokStr)
{- ----------------------------------------------------------------------
Datatypes for efficient Extended Parameter comparison
---------------------------------------------------------------------- -}
data ExtNumber = LeftInf | RightInf | Regular APInt deriving (Show, Eq)
instance Ord ExtNumber where
compare a b | a == b = EQ
| otherwise =
case (a, b) of
(LeftInf, _) -> LT
(RightInf, _) -> GT
(Regular i, Regular j) -> compare i j
_ -> swapCompare $ compare b a
type BaseInterval = (ExtNumber, ExtNumber)
leftOpen :: APInt -> BaseInterval
leftOpen i = (LeftInf, Regular i)
rightOpen :: APInt -> BaseInterval
rightOpen i = (Regular i, RightInf)
between :: APInt -> APInt -> BaseInterval
between i j = (Regular i, Regular j)
-- All methods in the following presuppose normalized expressions
-- | Normalized generalized representation of an extended parameter constraint
type EPExp = [BaseInterval]
showBaseInterval :: String -> BaseInterval -> String
showBaseInterval _ (LeftInf, RightInf) = error "showBaseInterval: unconstrained expression"
showBaseInterval s (LeftInf, Regular i) = concat [s, " <= ", show i]
showBaseInterval s (Regular i, RightInf) = concat [s, " >= ", show i]
showBaseInterval s (Regular i, Regular j)
| i == j = concat [s, " = ", show j]
| otherwise = concat [show i, " <= ", s, " <= ", show j]
showBaseInterval _ ep = error $ "malformed expression: " ++ show ep
showEP :: (String, EPExp) -> String
showEP (s, ep) = intercalate " \\/ " $ map (showBaseInterval s) ep
toBoolRep :: String -> EPExp -> BoolRep
toBoolRep = error "TODO"
-- | Conversion function into the more efficient representation.
toEPExp :: EXTPARAM -> Maybe (String, EPExp)
toEPExp (EP t r i) =
let l = case r of
"<=" -> [leftOpen i]
"<" -> [leftOpen $ i - 1]
">=" -> [rightOpen i]
">" -> [rightOpen $ i + 1]
"=" -> [between i i]
"!=" -> [leftOpen $ i - 1, rightOpen $ i + 1]
"-|" -> []
_ -> error $ "toEPExp: unsupported relation: " ++ r
in if null l then Nothing else Just (tokStr t, l)
{- ----------------------------------------------------------------------
Extended Parameter comparison (subset-comparison)
---------------------------------------------------------------------- -}
leftOf :: BaseInterval -> BaseInterval -> Bool
leftOf (_, b) (_, d) = b <= d
compareBI :: BaseInterval -> BaseInterval -> SetOrdering
compareBI i1@(a, b) i2@(c, d)
| i1 == i2 = Comparable EQ
| b < c || a > d = Incomparable Disjoint
| a <= c = if b < d then Incomparable Overlap else Comparable GT
| b <= d = Comparable LT
| otherwise = Incomparable Overlap
compareBIEP :: BaseInterval -> EPExp -> SetOrdering
compareBIEP _ [] = Comparable GT
compareBIEP i1 [i2] = compareBI i1 i2
compareBIEP i1 (i2 : l) =
case compareBI i1 i2 of
Incomparable Disjoint ->
if leftOf i1 i2 then Incomparable Disjoint else compareBIEP i1 l
Incomparable Overlap -> Incomparable Overlap
Comparable EQ -> Comparable LT -- l has here at least length one!
Comparable LT -> Comparable LT
Comparable GT -> case compareBIEP i1 l of
-- EQ and LT is here an impossible outcome
Comparable GT -> Comparable GT
_ -> Incomparable Overlap
-- TODO: implement this comparison procedure
-- | Compares two 'EPExp': They are uncompareable if they overlap or are disjoint.
compareEP :: EPExp -> EPExp -> SetOrdering
compareEP [] [] = Comparable EQ
compareEP _ [] = Comparable GT
compareEP [] _ = Comparable LT
compareEP _ _ = error "GeneralExtendedParameter: TODO"
{-
compareEP ep1@(i1:l1) ep2@(i2:l2) =
case compareBI i1 i2 of
Comparable EQ -> case compareEP l1 l2 of
Incomparable
i1 == i2 -> wenn compareEP l1 l2 disjoint dann overlap sonst ergebnis
i1 > i2 -> wenn compareEP
-}