-- | This library packages the functional peal paper
-- 'Sparse Bitmaps for Pattern Match Coverage' submitted to ICFP 2009
-- by Ki Yung Ahn and Tim Sheard.
-- You can look up the tutorial-like paper and the talk slides,
-- which are availabel at:
--
-- <http://kyagrd.dyndns.org/wiki/SparseBitmapsForPatternMatchCoverage >
--
-- Abstract:
--
--  Pattern matching coverage over Algebraic Data Types(ADTs) has most often been studied in the context of pattern compilation algorithms. However, it is worth considering the pattern matching coverage problem in isolation, since general solutions will be independent of the specifics of any implementation or language.
--
--  We define an intuitive and mathematically well-established bit masking semantics for pattern match coverage. We design and implement a sparse bitmap data structure, which realizes this semantics in a compact and flexible manner. This bitmap data structure supports computing coverage solutions of large programs incrementally from coverage solutions of sub-programs. It can also be used as a common data representation for pattern coverage shared between different tools (e.g., compilers, linting tools, software analysis tools) that need pattern match coverage information.

module Data.SparseBIT where

import List

infixr 7 *.
class Expand t where
  -- | type product
  (*.) :: t -> t -> t
  -- ^ Type product of two types is usually a product type (or pair type).
  -- Conceptually, for example, @Int *. Bool = (Int,Bool)@.
  -- Note, ('*.') have at least one identity 'unit',
  -- and type product against such identities may not result in a prodcut type.
 
  -- | identity on ('*.')
  unit :: t
  -- ^ > unit *. a = a = a *. unit
  --
  -- Note, there can be other identities depending on how you define 'expand'.
  -- Any type 'a' that satisfy @null(expand a)@ is an identity on ('*.').
  -- The 'unit' is the most simple and basic identity among them,
  -- which serves as a degenerate type for nullary data data constants
  -- (e.g., 'True', 'False').

  -- | type expansion rule
  expand :: t -> [t]
  -- ^ The definition of expand summarizes the structure of algebraic data type.
  -- Conceptually, for example,
  --
  -- > expand unit = [] -- the-non expandable degenerate type
  -- > expand Bool = [unit,unit]  -- True, False
  -- > expand (Maybe a) = [unit, a] -- Nothing, Just a

data BIT t = O t           -- ^ all 0 bits (identity on ('.|'))
           | I t           -- ^ all 1 bits (identity on ('.&'))
           | Bs [BIT t] t  -- ^ sequence of bits (possibley nested)
  deriving (Eq,Show)

-- | extract the type information of a given bit
typeof           ::  BIT t -> t
typeof (O t)     =   t
typeof (I t)     =   t
typeof (Bs _ t)  =   t
-- ^ For example,
--
-- > typeof (O Bool) = Bool 
-- > typeof (I Bool) = Int
-- > typeof (Bs [O unit,I unit] Bool) = Bool

-- | turn bits into strings without the type information
showB            ::  BIT t -> String
showB (O _)      =   "0"
showB (I _)      =   "1"
showB (Bs xs _)  =   "[" ++ (concatMap showB xs) ++ "]"
-- ^ For example,
--
-- > showB (Bs [O unit,I unit] Bool) = "[01]"

-- | same as 'showB' but takes off the outermost square bracket
showB'    ::  BIT t -> String
showB' b  =   case showB b of '[':cs -> init cs
                              cs     -> cs
-- ^ For example,
--
-- > showB' (Bs [O unit,I unit] Bool) = "01"

-- | print a newline ended string produced from 'showB'' on the standard output
printB  ::  BIT t -> IO ()
printB  =   putStrLn . showB'


-- | bitwise-and
(.&)                   ::  BIT t -> BIT t -> BIT t
O t       .& _         =   O t
_         .& O t       =   O t
I _       .& y         =   y
x         .& I _       =   x
Bs xs t   .& Bs ys _   =   Bs (xs .&. ys) t

(.&.) ::  [BIT t] -> [BIT t] -> [BIT t]
(.&.) =   zipWith (.&)


-- | bitwise-or
(.|)                   ::  BIT t -> BIT t -> BIT t
O _       .| y         = y
x         .| O _       = x
I t       .| _         = I t
_         .| I t       = I t
Bs xs t   .| Bs ys _   = Bs (xs .|. ys) t

(.|.) ::  [BIT t] -> [BIT t] -> [BIT t]
(.|.) =   zipWith (.|)

-- | bitwise negation
neg            ::  BIT t -> BIT t
neg (I t)      =   O t
neg (O t)      =   I t
neg (Bs bs t)  =   Bs (map neg bs) t

-- | reduce 'BIT's to canonical forms
reduce            ::  BIT t -> BIT t
reduce (Bs xs t)   =
  case map reduce xs of
    O _:bs | all o bs -> O t
    I _:bs | all i bs -> I t
    xs'               -> Bs xs' t
  where  o (O _)  = True
         o _      = False
         i (I _)  = True
         i _      = False
reduce x           = x

-- | tensor product
infixr 7 .**
(.**)                 ::  Expand t => BIT t -> BIT t -> BIT t
x         .** O u     =   O (t*.u) where t  = typeof x
O t       .** y       =   O (t*.u) where u  = typeof y
I t       .** I u     =   I (t*.u)
Bs xs t   .** I u     =   case expand u of
                           [] -> Bs xs t
                           us -> Bs xs t .** Bs (map I us) u
I t       .** Bs ys u =   case expand t of
                           [] -> Bs ys u
                           ts -> Bs (map I ts) t .** Bs ys u
Bs xs t   .** Bs ys u =   Bs (xs .**. ys) (t*.u)
  where
    xs  .**. ys  = [ Bs [x .** y | y<-ys] (typeof x *. u) | x <- xs ]


infix 4 =:=
-- | congruence modulo 'reduce'
(=:=)    ::  Eq t => BIT t -> BIT t -> Bool
x =:= y  =   reduce x == reduce y