content: {- |
  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
  
  -}
  