hets/CSL/GeneralExtendedParameter.hs

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

-}