content: {-# LANGUAGE FlexibleContexts #-}
  -- |
  -- Module: RegExp
  -- Description: Regular expression library
  -- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.
  --
  -- A regular expression library.
  --
  -- For an example, see
  -- <https://github.com/Copilot-Language/examplesForACSL/blob/master/example15/main.hs>
  
  module Copilot.Library.RegExp ( copilotRegexp, copilotRegexpB ) where
  
  import Text.ParserCombinators.Parsec
    ( optional, (<|>), string, char, between, GenParser, many, choice, CharParser
    , optionMaybe, chainr1, chainr, many1, digit, letter, eof, parse
    , SourceName )
  import Data.Int
  import Data.Word
  import Data.List
  import Data.Char
  import Data.Maybe
  
  import Control.Monad.State ( evalState, get, modify )
  
  import qualified Copilot.Language as C
  
  -- | The symbols in a regular expression.
  --
  -- 'Any' is any value of type @t@ (matches any symbol, the "point" character in
  -- a regular expression).
  data Sym t = Any | Sym t
               deriving ( Eq, Ord, Show )
  
  -- | A symbol's value can occur multiple times in a regular expression, e.g.
  -- "t(tfft)*". A running number "symbolNum" is used to make all symbols in a
  -- regular expression unique.
  data NumSym t = NumSym { symbolNum :: Maybe NumT
                         , symbol    :: Sym t
                         } deriving ( Eq, Show )
  type NumT     = Int
  
  -- | The regular expression data type.
  --
  -- For our use, regular expressions describing a language with no words are not
  -- supported since empty languages would not match anything and just yield a
  -- Copilot stream of constant false values.
  data RegExp t = REpsilon
                | RSymbol  ( NumSym t )
                | ROr      ( RegExp t ) ( RegExp t )
                | RConcat  ( RegExp t ) ( RegExp t )
                | RStar    ( RegExp t )
                  deriving Show
  
  -- | Parsers for single characters.
  lquote, rquote, lparen, rparen,
    star, plus, qmark, point, minus,
    nondigit :: CharParser () Char
  lquote = char '<'
  rquote = char '>'
  lparen = char '('
  rparen = char ')'
  star   = char '*'
  plus   = char '+'
  qmark  = char '?'
  point  = char '.'
  minus  = char '-'
  
  nondigit = char '_' <|> letter
  
  -- | A "followedBy" combinator for parsing, parses p, then p' and returns the
  -- result of p.
  followedBy :: GenParser tok () a
             -> GenParser tok () b
             -> GenParser tok () a
  followedBy p p' = p >>= \ r -> p' >> return r
  
  -- | Parsing a string p' with prefix p, returning both in order.
  cPrefix, optCPrefix :: GenParser tok () Char
                      -> GenParser tok () String
                      -> GenParser tok () String
  cPrefix p p' = p  >>= \ c -> fmap ( c : ) p'
  
  -- | Parsing a string @p'@ with the character @p@ as an optional prefix, return
  -- the result with the optional prefix.
  optCPrefix p p' = optionMaybe p
                    >>= \ r -> case r of
                                 Nothing -> p'
                                 Just c  -> fmap ( c : ) p'
  
  -- | "case insensitive". Take one argument of type string, parses for the
  -- string in a case insensitive manner and yields the parsed string (preserving
  -- its case).
  ci :: String -> GenParser Char () String
  ci = mapM ( \ c -> ( char . toLower ) c <|> ( char . toUpper ) c )
  
  -- | Parser for regular expressions
  regexp  :: ( SymbolParser t ) => GenParser Char () ( RegExp t )
  regexp  = chainr1 term opOr
  
  term    :: ( SymbolParser t ) => GenParser Char () ( RegExp t )
  term    = chainr factor opConcat REpsilon
  
  factor  :: ( SymbolParser t ) => GenParser Char () ( RegExp t )
  factor  = opSuffix factor'
  
  factor' :: ( SymbolParser t ) => GenParser Char () ( RegExp t )
  factor' = between lparen rparen regexp
            <|> anySym
            <|> parseSym
  
  -- | Parses the "." - point character used to match any symbol.
  anySym  :: ( SymbolParser t ) => GenParser Char () ( RegExp t )
  anySym  = point >> ( return . RSymbol ) ( NumSym Nothing Any )
  
  class SymbolParser t where
      parseSym :: GenParser Char () ( RegExp t )
  
  instance SymbolParser Bool where
      parseSym = do { truth <- ( ci "t" >> optional ( ci "rue" )
                                 >> return True )
                                <|> ( ci "f" >> optional ( ci "alse" )
                                      >> return False )
                                <|> ( string "1" >> return True )
                                <|> ( string "0" >> return False )
                    ; return $ RSymbol ( NumSym Nothing $ Sym truth )
                    }
  
  parseWordSym :: ( Integral t )
                  => GenParser Char () ( RegExp t )
  parseWordSym = do { num <- between lquote rquote $ many1 digit
                    ; return . RSymbol . NumSym Nothing . Sym
                      $ fromIntegral ( read num :: Integer )
                    }
  
  parseIntSym :: ( Integral t )
                  => GenParser Char () ( RegExp t )
  parseIntSym = do { num <- between lquote rquote $
                            optCPrefix minus ( many1 digit )
                   ; return . RSymbol . NumSym Nothing . Sym
                     $ fromIntegral ( read num :: Integer )
                   }
  
  type StreamName = String
  newtype P = P { getName :: StreamName }
      deriving Eq
  
  parsePSym :: GenParser Char () ( RegExp P )
  parsePSym = do { pStream <- between lquote rquote $
                              cPrefix nondigit ( many $ nondigit <|> digit )
                 ; return . RSymbol . NumSym Nothing . Sym
                   $ P pStream
                 }
  
  instance SymbolParser Word8 where
      parseSym = parseWordSym
  
  instance SymbolParser Word16 where
      parseSym = parseWordSym
  
  instance SymbolParser Word32 where
      parseSym = parseWordSym
  
  instance SymbolParser Word64 where
      parseSym = parseWordSym
  
  instance SymbolParser Int8 where
      parseSym = parseIntSym
  
  instance SymbolParser Int16 where
      parseSym = parseIntSym
  
  instance SymbolParser Int32 where
      parseSym = parseIntSym
  
  instance SymbolParser Int64 where
      parseSym = parseIntSym
  
  instance SymbolParser P where
      parseSym = parsePSym
  
  opOr       :: GenParser Char () ( RegExp t -> RegExp t -> RegExp t )
  opOr       = char '|' >> return ROr
  
  opConcat   :: GenParser Char () ( RegExp t -> RegExp t -> RegExp t )
  opConcat   = return RConcat
  
  opSuffix   :: GenParser Char () ( RegExp t )
             -> GenParser Char () ( RegExp t )
  opSuffix r = do
    subexp   <- r
    suffixes <- many $ choice [ star, plus, qmark ]
    let transform rexp suffix =
            case suffix of
              '*'   -> RStar   rexp
              '+'   -> RConcat rexp ( RStar rexp )
              '?'   -> ROr     rexp   REpsilon
              other -> C.badUsage ("in Regular Expression library: " ++
                                 "unhandled operator: " ++ show other)
    return $ foldl transform subexp suffixes
  
  parser :: ( SymbolParser t )
           => GenParser Char () ( RegExp t )
  parser = regexp `followedBy` eof
  
  hasEpsilon                    :: RegExp t -> Bool
  hasEpsilon   REpsilon         = True
  hasEpsilon ( RSymbol  _     ) = False
  hasEpsilon ( ROr      r1 r2 ) = hasEpsilon r1 || hasEpsilon r2
  hasEpsilon ( RConcat  r1 r2 ) = hasEpsilon r1 && hasEpsilon r2
  hasEpsilon ( RStar    _     ) = True
  
  first                    :: RegExp t -> [ NumSym t ]
  first   REpsilon         = []
  first ( RSymbol  s     ) = [ s ]
  first ( ROr      r1 r2 ) = first r1 ++ first r2
  first ( RConcat  r1 r2 ) = first r1 ++ if hasEpsilon r1 then
                                             first r2 else []
  first ( RStar    r     ) = first r
  
  reverse'                   :: RegExp t -> RegExp t
  reverse' ( ROr     r1 r2 ) = ROr     ( reverse' r1 ) ( reverse' r2 )
  reverse' ( RConcat r1 r2 ) = RConcat ( reverse' r2 ) ( reverse' r1 )
  reverse' ( RStar   r     ) = RStar   ( reverse' r  )
  reverse'   e               = e
  
  last' :: RegExp t -> [ NumSym t ]
  last' = first . reverse'
  
  follow                        :: ( Eq t ) =>
                                   RegExp t -> NumSym t -> [ NumSym t ]
  follow   REpsilon         _   = []
  follow ( RSymbol  _     ) _   = []
  follow ( ROr      r1 r2 ) sNr = follow r1 sNr ++ follow r2 sNr
  follow ( RConcat  r1 r2 ) sNr = follow r1 sNr ++ follow r2 sNr
                                  ++ if sNr `elem` last' r1 then
                                         first r2 else []
  follow ( RStar    r     ) sNr = follow r sNr
                                  `union` if sNr `elem` last' r then
                                              first r else []
  
  preceding :: ( Eq t ) => RegExp t -> NumSym t -> [ NumSym t ]
  preceding = follow . reverse'
  
  hasFinitePath                   :: RegExp t -> Bool
  hasFinitePath ( ROr     r1 r2 ) = hasFinitePath r1 || hasFinitePath r2
  hasFinitePath ( RConcat _  r2 ) = hasFinitePath r2
  hasFinitePath ( RStar   _     ) = False
  hasFinitePath   _               = True
  
  getSymbols                   :: RegExp t -> [ NumSym t ]
  getSymbols ( RSymbol s     ) = [ s ]
  getSymbols ( ROr     r1 r2 ) = getSymbols r1 ++ getSymbols r2
  getSymbols ( RConcat r1 r2 ) = getSymbols r1 ++ getSymbols r2
  getSymbols ( RStar   r     ) = getSymbols r
  getSymbols   _               = []
  
  -- assign each symbol in the regular expression a
  -- unique number, counting up from 0
  enumSyms   :: RegExp t -> RegExp t
  enumSyms rexp = evalState ( enumSyms' rexp ) 0
      where
        enumSyms' ( RSymbol s     ) = do
          num <- get
          modify ( + 1 )
          return $ RSymbol s { symbolNum = Just num }
        enumSyms' ( ROr     r1 r2 ) = do
          r1' <- enumSyms' r1
          r2' <- enumSyms' r2
          return $ ROr r1' r2'
        enumSyms' ( RConcat r1 r2 ) = do
          r1' <- enumSyms' r1
          r2' <- enumSyms' r2
          return $ RConcat r1' r2'
        enumSyms' ( RStar   r     ) = do
          r'  <- enumSyms' r
          return $ RStar   r'
        enumSyms'   other           =
          return other
  
  regexp2CopilotNFA :: ( C.Typed t, Eq t )
                       => C.Stream t -> RegExp t -> C.Stream Bool -> C.Stream Bool
  regexp2CopilotNFA inStream rexp reset =
      let symbols                    = getSymbols rexp
          first'                     = first rexp
          start                      = [ True ] C.++ C.false
  
          preceding'   numSym        = let ps    = preceding rexp numSym
                                           s     = if numSym `elem` first' then
                                                     [ start ] else []
                                       in s ++ [ streams !! i
                                               | i <- map ( fromJust . symbolNum ) ps ]
  
          matchesInput numSym        = case symbol numSym of
                                         Any   -> C.true
                                         Sym t -> inStream C.== C.constant t
  
          transitions  numSym ps     = matchesInput numSym
                                       C.&& ( foldl ( C.|| ) C.false ps )
  
          stream       numSym        = let ps    = preceding' numSym
                                           init_ = C.constant $ numSym `elem` first'
                                       in C.mux reset
                                          ( [ False ] C.++ matchesInput numSym C.&& init_ )
                                          ( [ False ] C.++ transitions  numSym ps )
  
          streams                    = map stream symbols
  
          outStream                  = foldl ( C.|| ) start streams
  
      in outStream
  
  -- | Regular expression matching over an arbitrary stream
  copilotRegexp :: ( C.Typed t, SymbolParser t, Eq t )
                => C.Stream t     -- ^ The stream to monitor.
                -> SourceName     -- ^ The regular expression.
                -> C.Stream Bool  -- ^ A stream indicating when to reset the
                                  --   monitor.
                -> C.Stream Bool
  copilotRegexp inStream rexp reset =
    case parse parser rexp rexp of
      Left  err -> C.badUsage ("parsing regular exp: " ++ show err)
      Right rexp' -> let nrexp = enumSyms rexp' in
          if hasFinitePath nrexp then
              C.badUsage $
              concat [ "The regular expression contains a finite path "
                     , "which is something that will fail to match "
                     , "since we do not have a distinct end-of-input "
                     , "symbol on infinite streams." ]
          else if hasEpsilon nrexp then
                   C.badUsage $
                   concat [ "The regular expression matches a language "
                          , "that contains epsilon. This cannot be handled "
                          , "on infinite streams, since we do not have "
                          , "a distinct end-of-input symbol." ]
               else regexp2CopilotNFA inStream nrexp reset
  
  regexp2CopilotNFAB :: RegExp P -> [ ( StreamName, C.Stream Bool ) ]
                        -> C.Stream Bool -> C.Stream Bool
  regexp2CopilotNFAB rexp propositions reset =
      let symbols                    = getSymbols rexp
          first'                     = first rexp
          start                      = [ True ] C.++ C.false
  
          preceding'   numSym        = let ps    = preceding rexp numSym
                                           s     = if numSym `elem` first' then
                                                     [ start ] else []
                                       in s ++ [ streams !! i
                                               | i <- map ( fromJust . symbolNum ) ps ]
  
          lookup' a l = case lookup a l of
                          Nothing -> C.badUsage ("boolean stream "
                                               ++ a
                                               ++ " is not defined")
                          Just s  -> s
  
          matchesInput numSym        = case symbol numSym of
                                         Any   -> C.true
                                         Sym t -> lookup' ( getName t ) propositions
  
          transitions  numSym ps     = matchesInput numSym
                                       C.&& ( foldl ( C.|| ) C.false ps )
  
          stream       numSym        = let ps    = preceding' numSym
                                           init_ = C.constant $ numSym `elem` first'
                                       in C.mux reset
                                          ( [ False ] C.++ matchesInput numSym C.&& init_ )
                                          ( [ False ] C.++ transitions  numSym ps )
  
          streams                    = map stream symbols
  
          outStream                  = foldl ( C.|| ) start streams
  
      in outStream
  
  -- | Regular expression matching over a collection of boolean streams.
  --
  -- Regular expressions can contain symbols, which are expanded to match
  -- specific streams.
  --
  -- For example, the regular expression:
  --
  -- @
  -- "\<s0\>(\<s1\>)+"
  -- @
  --
  -- would match if you provide a map (association list) that assigns, to the
  -- symbol @"s0"@, a stream that is true at the first sample, and to @"s1"@, a
  -- stream that is true at every sample after the first sample.
  copilotRegexpB :: SourceName                         -- ^ Regular expression
                 -> [ ( StreamName, C.Stream Bool ) ]  -- ^ A table with the
                                                       -- stream associated to
                                                       -- each symbol.
                 -> C.Stream Bool                      -- ^ A stream indicating
                                                       -- when to reset the
                                                       -- monitor.
                 -> C.Stream Bool
  copilotRegexpB rexp propositions reset =
    case parse parser rexp rexp of
      Left  err -> C.badUsage ("parsing regular exp: " ++ show err)
      Right rexp' -> let nrexp = enumSyms rexp' in
          if hasFinitePath nrexp then
              C.badUsage $
              concat [ "The regular expression contains a finite path "
                     , "which is something that will fail to match "
                     , "since we do not have a distinct end-of-input "
                     , "symbol on infinite streams." ]
          else if hasEpsilon nrexp then
                   C.badUsage $
                   concat [ "The regular expression matches a language "
                          , "that contains epsilon. This cannot be handled "
                          , "on infinite streams, since we do not have "
                          , "a distinct end-of-input symbol." ]
               else regexp2CopilotNFAB nrexp propositions reset
  