    {-# 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 ( Sym t -> Sym t -> Bool
    (Sym t -> Sym t -> Bool) -> (Sym t -> Sym t -> Bool) -> Eq (Sym t)
    forall t. Eq t => Sym t -> Sym t -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall t. Eq t => Sym t -> Sym t -> Bool
    == :: Sym t -> Sym t -> Bool
    $c/= :: forall t. Eq t => Sym t -> Sym t -> Bool
    /= :: Sym t -> Sym t -> Bool
    Eq, Eq (Sym t)
    Eq (Sym t) =>
    (Sym t -> Sym t -> Ordering)
    -> (Sym t -> Sym t -> Bool)
    -> (Sym t -> Sym t -> Bool)
    -> (Sym t -> Sym t -> Bool)
    -> (Sym t -> Sym t -> Bool)
    -> (Sym t -> Sym t -> Sym t)
    -> (Sym t -> Sym t -> Sym t)
    -> Ord (Sym t)
    Sym t -> Sym t -> Bool
    Sym t -> Sym t -> Ordering
    Sym t -> Sym t -> Sym t
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    forall t. Ord t => Eq (Sym t)
    forall t. Ord t => Sym t -> Sym t -> Bool
    forall t. Ord t => Sym t -> Sym t -> Ordering
    forall t. Ord t => Sym t -> Sym t -> Sym t
    $ccompare :: forall t. Ord t => Sym t -> Sym t -> Ordering
    compare :: Sym t -> Sym t -> Ordering
    $c< :: forall t. Ord t => Sym t -> Sym t -> Bool
    < :: Sym t -> Sym t -> Bool
    $c<= :: forall t. Ord t => Sym t -> Sym t -> Bool
    <= :: Sym t -> Sym t -> Bool
    $c> :: forall t. Ord t => Sym t -> Sym t -> Bool
    > :: Sym t -> Sym t -> Bool
    $c>= :: forall t. Ord t => Sym t -> Sym t -> Bool
    >= :: Sym t -> Sym t -> Bool
    $cmax :: forall t. Ord t => Sym t -> Sym t -> Sym t
    max :: Sym t -> Sym t -> Sym t
    $cmin :: forall t. Ord t => Sym t -> Sym t -> Sym t
    min :: Sym t -> Sym t -> Sym t
    Ord, Int -> Sym t -> ShowS
    [Sym t] -> ShowS
    Sym t -> [Char]
    (Int -> Sym t -> ShowS)
    -> (Sym t -> [Char]) -> ([Sym t] -> ShowS) -> Show (Sym t)
    forall t. Show t => Int -> Sym t -> ShowS
    forall t. Show t => [Sym t] -> ShowS
    forall t. Show t => Sym t -> [Char]
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall t. Show t => Int -> Sym t -> ShowS
    showsPrec :: Int -> Sym t -> ShowS
    $cshow :: forall t. Show t => Sym t -> [Char]
    show :: Sym t -> [Char]
    $cshowList :: forall t. Show t => [Sym t] -> ShowS
    showList :: [Sym t] -> ShowS
    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 { forall t. NumSym t -> Maybe Int
    symbolNum :: Maybe NumT
                           , forall t. NumSym t -> Sym t
    symbol    :: Sym t
                           } deriving ( NumSym t -> NumSym t -> Bool
    (NumSym t -> NumSym t -> Bool)
    -> (NumSym t -> NumSym t -> Bool) -> Eq (NumSym t)
    forall t. Eq t => NumSym t -> NumSym t -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall t. Eq t => NumSym t -> NumSym t -> Bool
    == :: NumSym t -> NumSym t -> Bool
    $c/= :: forall t. Eq t => NumSym t -> NumSym t -> Bool
    /= :: NumSym t -> NumSym t -> Bool
    Eq, Int -> NumSym t -> ShowS
    [NumSym t] -> ShowS
    NumSym t -> [Char]
    (Int -> NumSym t -> ShowS)
    -> (NumSym t -> [Char]) -> ([NumSym t] -> ShowS) -> Show (NumSym t)
    forall t. Show t => Int -> NumSym t -> ShowS
    forall t. Show t => [NumSym t] -> ShowS
    forall t. Show t => NumSym t -> [Char]
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall t. Show t => Int -> NumSym t -> ShowS
    showsPrec :: Int -> NumSym t -> ShowS
    $cshow :: forall t. Show t => NumSym t -> [Char]
    show :: NumSym t -> [Char]
    $cshowList :: forall t. Show t => [NumSym t] -> ShowS
    showList :: [NumSym t] -> ShowS
    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 Int -> RegExp t -> ShowS
    [RegExp t] -> ShowS
    RegExp t -> [Char]
    (Int -> RegExp t -> ShowS)
    -> (RegExp t -> [Char]) -> ([RegExp t] -> ShowS) -> Show (RegExp t)
    forall t. Show t => Int -> RegExp t -> ShowS
    forall t. Show t => [RegExp t] -> ShowS
    forall t. Show t => RegExp t -> [Char]
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall t. Show t => Int -> RegExp t -> ShowS
    showsPrec :: Int -> RegExp t -> ShowS
    $cshow :: forall t. Show t => RegExp t -> [Char]
    show :: RegExp t -> [Char]
    $cshowList :: forall t. Show t => [RegExp t] -> ShowS
    showList :: [RegExp t] -> ShowS
    Show

    -- | Parsers for single characters.
    lquote, rquote, lparen, rparen,
      star, plus, qmark, point, minus,
      nondigit :: CharParser () Char
    lquote :: CharParser () Char
    lquote = Char -> CharParser () Char
    forall s (m :: * -> *) u.
    Stream s m Char =>
    Char -> ParsecT s u m Char
    char Char
    '<'
    rquote :: CharParser () Char
    rquote = Char -> CharParser () Char
    forall s (m :: * -> *) u.
    Stream s m Char =>
    Char -> ParsecT s u m Char
    char Char
    '>'
    lparen :: CharParser () Char
    lparen = Char -> CharParser () Char
    forall s (m :: * -> *) u.
    Stream s m Char =>
    Char -> ParsecT s u m Char
    char Char
    '('
    rparen :: CharParser () Char
    rparen = Char -> CharParser () Char
    forall s (m :: * -> *) u.
    Stream s m Char =>
    Char -> ParsecT s u m Char
    char Char
    ')'
    star :: CharParser () Char
    star   = Char -> CharParser () Char
    forall s (m :: * -> *) u.
    Stream s m Char =>
    Char -> ParsecT s u m Char
    char Char
    '*'
    plus :: CharParser () Char
    plus   = Char -> CharParser () Char
    forall s (m :: * -> *) u.
    Stream s m Char =>
    Char -> ParsecT s u m Char
    char Char
    '+'
    qmark :: CharParser () Char
    qmark  = Char -> CharParser () Char
    forall s (m :: * -> *) u.
    Stream s m Char =>
    Char -> ParsecT s u m Char
    char Char
    '?'
    point :: CharParser () Char
    point  = Char -> CharParser () Char
    forall s (m :: * -> *) u.
    Stream s m Char =>
    Char -> ParsecT s u m Char
    char Char
    '.'
    minus :: CharParser () Char
    minus  = Char -> CharParser () Char
    forall s (m :: * -> *) u.
    Stream s m Char =>
    Char -> ParsecT s u m Char
    char Char
    '-'

    nondigit :: CharParser () Char
    nondigit = Char -> CharParser () Char
    forall s (m :: * -> *) u.
    Stream s m Char =>
    Char -> ParsecT s u m Char
    char Char
    '_' CharParser () Char -> CharParser () Char -> CharParser () Char
    forall s u (m :: * -> *) a.
    ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
    <|> CharParser () Char
    forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m 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 :: forall tok a b.
    GenParser tok () a -> GenParser tok () b -> GenParser tok () a
    followedBy GenParser tok () a
    p GenParser tok () b
    p' = GenParser tok () a
    p GenParser tok () a
    -> (a -> GenParser tok () a) -> GenParser tok () a
    forall a b.
    ParsecT [tok] () Identity a
    -> (a -> ParsecT [tok] () Identity b)
    -> ParsecT [tok] () Identity b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \ a
    r -> GenParser tok () b
    p' GenParser tok () b -> GenParser tok () a -> GenParser tok () a
    forall a b.
    ParsecT [tok] () Identity a
    -> ParsecT [tok] () Identity b -> ParsecT [tok] () Identity b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> a -> GenParser tok () a
    forall a. a -> ParsecT [tok] () Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    r

    -- | Parsing a string p' with prefix p, returning both in order.
    cPrefix, optCPrefix :: GenParser tok () Char
                        -> GenParser tok () String
                        -> GenParser tok () String
    cPrefix :: forall tok.
    GenParser tok () Char
    -> GenParser tok () [Char] -> GenParser tok () [Char]
    cPrefix GenParser tok () Char
    p GenParser tok () [Char]
    p' = GenParser tok () Char
    p  GenParser tok () Char
    -> (Char -> GenParser tok () [Char]) -> GenParser tok () [Char]
    forall a b.
    ParsecT [tok] () Identity a
    -> (a -> ParsecT [tok] () Identity b)
    -> ParsecT [tok] () Identity b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \ Char
    c -> ShowS -> GenParser tok () [Char] -> GenParser tok () [Char]
    forall a b.
    (a -> b)
    -> ParsecT [tok] () Identity a -> ParsecT [tok] () Identity b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ( Char
    c Char -> ShowS
    forall a. a -> [a] -> [a]
    : ) GenParser tok () [Char]
    p'

    -- | Parsing a string @p'@ with the character @p@ as an optional prefix, return
    -- the result with the optional prefix.
    optCPrefix :: forall tok.
    GenParser tok () Char
    -> GenParser tok () [Char] -> GenParser tok () [Char]
    optCPrefix GenParser tok () Char
    p GenParser tok () [Char]
    p' = GenParser tok () Char -> ParsecT [tok] () Identity (Maybe Char)
    forall s (m :: * -> *) t u a.
    Stream s m t =>
    ParsecT s u m a -> ParsecT s u m (Maybe a)
    optionMaybe GenParser tok () Char
    p
                      ParsecT [tok] () Identity (Maybe Char)
    -> (Maybe Char -> GenParser tok () [Char])
    -> GenParser tok () [Char]
    forall a b.
    ParsecT [tok] () Identity a
    -> (a -> ParsecT [tok] () Identity b)
    -> ParsecT [tok] () Identity b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \ Maybe Char
    r -> case Maybe Char
    r of
                                   Maybe Char
    Nothing -> GenParser tok () [Char]
    p'
                                   Just Char
    c  -> ShowS -> GenParser tok () [Char] -> GenParser tok () [Char]
    forall a b.
    (a -> b)
    -> ParsecT [tok] () Identity a -> ParsecT [tok] () Identity b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ( Char
    c Char -> ShowS
    forall a. a -> [a] -> [a]
    : ) GenParser tok () [Char]
    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 :: [Char] -> GenParser Char () [Char]
    ci = (Char -> CharParser () Char) -> [Char] -> GenParser Char () [Char]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM ( \ Char
    c -> ( Char -> CharParser () Char
    forall s (m :: * -> *) u.
    Stream s m Char =>
    Char -> ParsecT s u m Char
    char (Char -> CharParser () Char)
    -> (Char -> Char) -> Char -> CharParser () Char
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Char -> Char
    toLower ) Char
    c CharParser () Char -> CharParser () Char -> CharParser () Char
    forall s u (m :: * -> *) a.
    ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
    <|> ( Char -> CharParser () Char
    forall s (m :: * -> *) u.
    Stream s m Char =>
    Char -> ParsecT s u m Char
    char (Char -> CharParser () Char)
    -> (Char -> Char) -> Char -> CharParser () Char
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Char -> Char
    toUpper ) Char
    c )

    -- | Parser for regular expressions
    regexp  :: ( SymbolParser t ) => GenParser Char () ( RegExp t )
    regexp :: forall t. SymbolParser t => GenParser Char () (RegExp t)
    regexp  = ParsecT [Char] () Identity (RegExp t)
    -> ParsecT [Char] () Identity (RegExp t -> RegExp t -> RegExp t)
    -> ParsecT [Char] () Identity (RegExp t)
    forall s (m :: * -> *) t u a.
    Stream s m t =>
    ParsecT s u m a -> ParsecT s u m (a -> a -> a) -> ParsecT s u m a
    chainr1 ParsecT [Char] () Identity (RegExp t)
    forall t. SymbolParser t => GenParser Char () (RegExp t)
    term ParsecT [Char] () Identity (RegExp t -> RegExp t -> RegExp t)
    forall t. GenParser Char () (RegExp t -> RegExp t -> RegExp t)
    opOr

    term    :: ( SymbolParser t ) => GenParser Char () ( RegExp t )
    term :: forall t. SymbolParser t => GenParser Char () (RegExp t)
    term    = ParsecT [Char] () Identity (RegExp t)
    -> ParsecT [Char] () Identity (RegExp t -> RegExp t -> RegExp t)
    -> RegExp t
    -> ParsecT [Char] () Identity (RegExp t)
    forall s (m :: * -> *) t u a.
    Stream s m t =>
    ParsecT s u m a
    -> ParsecT s u m (a -> a -> a) -> a -> ParsecT s u m a
    chainr ParsecT [Char] () Identity (RegExp t)
    forall t. SymbolParser t => GenParser Char () (RegExp t)
    factor ParsecT [Char] () Identity (RegExp t -> RegExp t -> RegExp t)
    forall t. GenParser Char () (RegExp t -> RegExp t -> RegExp t)
    opConcat RegExp t
    forall t. RegExp t
    REpsilon

    factor  :: ( SymbolParser t ) => GenParser Char () ( RegExp t )
    factor :: forall t. SymbolParser t => GenParser Char () (RegExp t)
    factor  = GenParser Char () (RegExp t) -> GenParser Char () (RegExp t)
    forall t.
    GenParser Char () (RegExp t) -> GenParser Char () (RegExp t)
    opSuffix GenParser Char () (RegExp t)
    forall t. SymbolParser t => GenParser Char () (RegExp t)
    factor'

    factor' :: ( SymbolParser t ) => GenParser Char () ( RegExp t )
    factor' :: forall t. SymbolParser t => GenParser Char () (RegExp t)
    factor' = CharParser () Char
    -> CharParser () Char
    -> ParsecT [Char] () Identity (RegExp t)
    -> ParsecT [Char] () Identity (RegExp t)
    forall s (m :: * -> *) t u open close a.
    Stream s m t =>
    ParsecT s u m open
    -> ParsecT s u m close -> ParsecT s u m a -> ParsecT s u m a
    between CharParser () Char
    lparen CharParser () Char
    rparen ParsecT [Char] () Identity (RegExp t)
    forall t. SymbolParser t => GenParser Char () (RegExp t)
    regexp
              ParsecT [Char] () Identity (RegExp t)
    -> ParsecT [Char] () Identity (RegExp t)
    -> ParsecT [Char] () Identity (RegExp t)
    forall s u (m :: * -> *) a.
    ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
    <|> ParsecT [Char] () Identity (RegExp t)
    forall t. SymbolParser t => GenParser Char () (RegExp t)
    anySym
              ParsecT [Char] () Identity (RegExp t)
    -> ParsecT [Char] () Identity (RegExp t)
    -> ParsecT [Char] () Identity (RegExp t)
    forall s u (m :: * -> *) a.
    ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
    <|> ParsecT [Char] () Identity (RegExp t)
    forall t. SymbolParser t => GenParser Char () (RegExp t)
    parseSym

    -- | Parses the "." - point character used to match any symbol.
    anySym  :: ( SymbolParser t ) => GenParser Char () ( RegExp t )
    anySym :: forall t. SymbolParser t => GenParser Char () (RegExp t)
    anySym  = CharParser () Char
    point CharParser () Char
    -> ParsecT [Char] () Identity (RegExp t)
    -> ParsecT [Char] () Identity (RegExp t)
    forall a b.
    ParsecT [Char] () Identity a
    -> ParsecT [Char] () Identity b -> ParsecT [Char] () Identity b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> ( RegExp t -> ParsecT [Char] () Identity (RegExp t)
    forall a. a -> ParsecT [Char] () Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (RegExp t -> ParsecT [Char] () Identity (RegExp t))
    -> (NumSym t -> RegExp t)
    -> NumSym t
    -> ParsecT [Char] () Identity (RegExp t)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NumSym t -> RegExp t
    forall t. NumSym t -> RegExp t
    RSymbol ) ( Maybe Int -> Sym t -> NumSym t
    forall t. Maybe Int -> Sym t -> NumSym t
    NumSym Maybe Int
    forall a. Maybe a
    Nothing Sym t
    forall t. Sym t
    Any )

    class SymbolParser t where
        parseSym :: GenParser Char () ( RegExp t )

    instance SymbolParser Bool where
        parseSym :: GenParser Char () (RegExp Bool)
    parseSym = do { truth <- ( [Char] -> GenParser Char () [Char]
    ci [Char]
    "t" GenParser Char () [Char]
    -> ParsecT [Char] () Identity () -> ParsecT [Char] () Identity ()
    forall a b.
    ParsecT [Char] () Identity a
    -> ParsecT [Char] () Identity b -> ParsecT [Char] () Identity b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> GenParser Char () [Char] -> ParsecT [Char] () Identity ()
    forall s (m :: * -> *) t u a.
    Stream s m t =>
    ParsecT s u m a -> ParsecT s u m ()
    optional ( [Char] -> GenParser Char () [Char]
    ci [Char]
    "rue" )
                                   ParsecT [Char] () Identity ()
    -> ParsecT [Char] () Identity Bool
    -> ParsecT [Char] () Identity Bool
    forall a b.
    ParsecT [Char] () Identity a
    -> ParsecT [Char] () Identity b -> ParsecT [Char] () Identity b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Bool -> ParsecT [Char] () Identity Bool
    forall a. a -> ParsecT [Char] () Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True )
                                  ParsecT [Char] () Identity Bool
    -> ParsecT [Char] () Identity Bool
    -> ParsecT [Char] () Identity Bool
    forall s u (m :: * -> *) a.
    ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
    <|> ( [Char] -> GenParser Char () [Char]
    ci [Char]
    "f" GenParser Char () [Char]
    -> ParsecT [Char] () Identity () -> ParsecT [Char] () Identity ()
    forall a b.
    ParsecT [Char] () Identity a
    -> ParsecT [Char] () Identity b -> ParsecT [Char] () Identity b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> GenParser Char () [Char] -> ParsecT [Char] () Identity ()
    forall s (m :: * -> *) t u a.
    Stream s m t =>
    ParsecT s u m a -> ParsecT s u m ()
    optional ( [Char] -> GenParser Char () [Char]
    ci [Char]
    "alse" )
                                        ParsecT [Char] () Identity ()
    -> ParsecT [Char] () Identity Bool
    -> ParsecT [Char] () Identity Bool
    forall a b.
    ParsecT [Char] () Identity a
    -> ParsecT [Char] () Identity b -> ParsecT [Char] () Identity b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Bool -> ParsecT [Char] () Identity Bool
    forall a. a -> ParsecT [Char] () Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False )
                                  ParsecT [Char] () Identity Bool
    -> ParsecT [Char] () Identity Bool
    -> ParsecT [Char] () Identity Bool
    forall s u (m :: * -> *) a.
    ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
    <|> ( [Char] -> GenParser Char () [Char]
    forall s (m :: * -> *) u.
    Stream s m Char =>
    [Char] -> ParsecT s u m [Char]
    string [Char]
    "1" GenParser Char () [Char]
    -> ParsecT [Char] () Identity Bool
    -> ParsecT [Char] () Identity Bool
    forall a b.
    ParsecT [Char] () Identity a
    -> ParsecT [Char] () Identity b -> ParsecT [Char] () Identity b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Bool -> ParsecT [Char] () Identity Bool
    forall a. a -> ParsecT [Char] () Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True )
                                  ParsecT [Char] () Identity Bool
    -> ParsecT [Char] () Identity Bool
    -> ParsecT [Char] () Identity Bool
    forall s u (m :: * -> *) a.
    ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
    <|> ( [Char] -> GenParser Char () [Char]
    forall s (m :: * -> *) u.
    Stream s m Char =>
    [Char] -> ParsecT s u m [Char]
    string [Char]
    "0" GenParser Char () [Char]
    -> ParsecT [Char] () Identity Bool
    -> ParsecT [Char] () Identity Bool
    forall a b.
    ParsecT [Char] () Identity a
    -> ParsecT [Char] () Identity b -> ParsecT [Char] () Identity b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Bool -> ParsecT [Char] () Identity Bool
    forall a. a -> ParsecT [Char] () Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False )
                      ; return $ RSymbol ( NumSym Nothing $ Sym truth )
                      }

    parseWordSym :: ( Integral t )
                    => GenParser Char () ( RegExp t )
    parseWordSym :: forall t. Integral t => GenParser Char () (RegExp t)
    parseWordSym = do { num <- CharParser () Char
    -> CharParser () Char
    -> GenParser Char () [Char]
    -> GenParser Char () [Char]
    forall s (m :: * -> *) t u open close a.
    Stream s m t =>
    ParsecT s u m open
    -> ParsecT s u m close -> ParsecT s u m a -> ParsecT s u m a
    between CharParser () Char
    lquote CharParser () Char
    rquote (GenParser Char () [Char] -> GenParser Char () [Char])
    -> GenParser Char () [Char] -> GenParser Char () [Char]
    forall a b. (a -> b) -> a -> b
    $ CharParser () Char -> GenParser Char () [Char]
    forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
    many1 CharParser () Char
    forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
    digit
                      ; return . RSymbol . NumSym Nothing . Sym
                        $ fromIntegral ( read num :: Integer )
                      }

    parseIntSym :: ( Integral t )
                    => GenParser Char () ( RegExp t )
    parseIntSym :: forall t. Integral t => GenParser Char () (RegExp t)
    parseIntSym = do { num <- CharParser () Char
    -> CharParser () Char
    -> GenParser Char () [Char]
    -> GenParser Char () [Char]
    forall s (m :: * -> *) t u open close a.
    Stream s m t =>
    ParsecT s u m open
    -> ParsecT s u m close -> ParsecT s u m a -> ParsecT s u m a
    between CharParser () Char
    lquote CharParser () Char
    rquote (GenParser Char () [Char] -> GenParser Char () [Char])
    -> GenParser Char () [Char] -> GenParser Char () [Char]
    forall a b. (a -> b) -> a -> b
    $
                              CharParser () Char
    -> GenParser Char () [Char] -> GenParser Char () [Char]
    forall tok.
    GenParser tok () Char
    -> GenParser tok () [Char] -> GenParser tok () [Char]
    optCPrefix CharParser () Char
    minus ( CharParser () Char -> GenParser Char () [Char]
    forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
    many1 CharParser () Char
    forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
    digit )
                     ; return . RSymbol . NumSym Nothing . Sym
                       $ fromIntegral ( read num :: Integer )
                     }

    type StreamName = String
    newtype P = P { P -> [Char]
    getName :: StreamName }
        deriving P -> P -> Bool
    (P -> P -> Bool) -> (P -> P -> Bool) -> Eq P
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: P -> P -> Bool
    == :: P -> P -> Bool
    $c/= :: P -> P -> Bool
    /= :: P -> P -> Bool
    Eq

    parsePSym :: GenParser Char () ( RegExp P )
    parsePSym :: GenParser Char () (RegExp P)
    parsePSym = do { pStream <- CharParser () Char
    -> CharParser () Char
    -> GenParser Char () [Char]
    -> GenParser Char () [Char]
    forall s (m :: * -> *) t u open close a.
    Stream s m t =>
    ParsecT s u m open
    -> ParsecT s u m close -> ParsecT s u m a -> ParsecT s u m a
    between CharParser () Char
    lquote CharParser () Char
    rquote (GenParser Char () [Char] -> GenParser Char () [Char])
    -> GenParser Char () [Char] -> GenParser Char () [Char]
    forall a b. (a -> b) -> a -> b
    $
                                CharParser () Char
    -> GenParser Char () [Char] -> GenParser Char () [Char]
    forall tok.
    GenParser tok () Char
    -> GenParser tok () [Char] -> GenParser tok () [Char]
    cPrefix CharParser () Char
    nondigit ( CharParser () Char -> GenParser Char () [Char]
    forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
    many (CharParser () Char -> GenParser Char () [Char])
    -> CharParser () Char -> GenParser Char () [Char]
    forall a b. (a -> b) -> a -> b
    $ CharParser () Char
    nondigit CharParser () Char -> CharParser () Char -> CharParser () Char
    forall s u (m :: * -> *) a.
    ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
    <|> CharParser () Char
    forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
    digit )
                   ; return . RSymbol . NumSym Nothing . Sym
                     $ P pStream
                   }

    instance SymbolParser Word8 where
        parseSym :: GenParser Char () (RegExp Word8)
    parseSym = GenParser Char () (RegExp Word8)
    forall t. Integral t => GenParser Char () (RegExp t)
    parseWordSym

    instance SymbolParser Word16 where
        parseSym :: GenParser Char () (RegExp Word16)
    parseSym = GenParser Char () (RegExp Word16)
    forall t. Integral t => GenParser Char () (RegExp t)
    parseWordSym

    instance SymbolParser Word32 where
        parseSym :: GenParser Char () (RegExp Word32)
    parseSym = GenParser Char () (RegExp Word32)
    forall t. Integral t => GenParser Char () (RegExp t)
    parseWordSym

    instance SymbolParser Word64 where
        parseSym :: GenParser Char () (RegExp Word64)
    parseSym = GenParser Char () (RegExp Word64)
    forall t. Integral t => GenParser Char () (RegExp t)
    parseWordSym

    instance SymbolParser Int8 where
        parseSym :: GenParser Char () (RegExp Int8)
    parseSym = GenParser Char () (RegExp Int8)
    forall t. Integral t => GenParser Char () (RegExp t)
    parseIntSym

    instance SymbolParser Int16 where
        parseSym :: GenParser Char () (RegExp Int16)
    parseSym = GenParser Char () (RegExp Int16)
    forall t. Integral t => GenParser Char () (RegExp t)
    parseIntSym

    instance SymbolParser Int32 where
        parseSym :: GenParser Char () (RegExp Int32)
    parseSym = GenParser Char () (RegExp Int32)
    forall t. Integral t => GenParser Char () (RegExp t)
    parseIntSym

    instance SymbolParser Int64 where
        parseSym :: GenParser Char () (RegExp Int64)
    parseSym = GenParser Char () (RegExp Int64)
    forall t. Integral t => GenParser Char () (RegExp t)
    parseIntSym

    instance SymbolParser P where
        parseSym :: GenParser Char () (RegExp P)
    parseSym = GenParser Char () (RegExp P)
    parsePSym

    opOr       :: GenParser Char () ( RegExp t -> RegExp t -> RegExp t )
    opOr :: forall t. GenParser Char () (RegExp t -> RegExp t -> RegExp t)
    opOr       = Char -> CharParser () Char
    forall s (m :: * -> *) u.
    Stream s m Char =>
    Char -> ParsecT s u m Char
    char Char
    '|' CharParser () Char
    -> ParsecT [Char] () Identity (RegExp t -> RegExp t -> RegExp t)
    -> ParsecT [Char] () Identity (RegExp t -> RegExp t -> RegExp t)
    forall a b.
    ParsecT [Char] () Identity a
    -> ParsecT [Char] () Identity b -> ParsecT [Char] () Identity b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> (RegExp t -> RegExp t -> RegExp t)
    -> ParsecT [Char] () Identity (RegExp t -> RegExp t -> RegExp t)
    forall a. a -> ParsecT [Char] () Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return RegExp t -> RegExp t -> RegExp t
    forall t. RegExp t -> RegExp t -> RegExp t
    ROr

    opConcat   :: GenParser Char () ( RegExp t -> RegExp t -> RegExp t )
    opConcat :: forall t. GenParser Char () (RegExp t -> RegExp t -> RegExp t)
    opConcat   = (RegExp t -> RegExp t -> RegExp t)
    -> ParsecT [Char] () Identity (RegExp t -> RegExp t -> RegExp t)
    forall a. a -> ParsecT [Char] () Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return RegExp t -> RegExp t -> RegExp t
    forall t. RegExp t -> RegExp t -> RegExp t
    RConcat

    opSuffix   :: GenParser Char () ( RegExp t )
               -> GenParser Char () ( RegExp t )
    opSuffix :: forall t.
    GenParser Char () (RegExp t) -> GenParser Char () (RegExp t)
    opSuffix GenParser Char () (RegExp t)
    r = do
      subexp   <- GenParser Char () (RegExp t)
    r
      suffixes <- many $ choice [ star, plus, qmark ]
      let transform RegExp t
    rexp Char
    suffix =
              case Char
    suffix of
                Char
    '*'   -> RegExp t -> RegExp t
    forall t. RegExp t -> RegExp t
    RStar   RegExp t
    rexp
                Char
    '+'   -> RegExp t -> RegExp t -> RegExp t
    forall t. RegExp t -> RegExp t -> RegExp t
    RConcat RegExp t
    rexp ( RegExp t -> RegExp t
    forall t. RegExp t -> RegExp t
    RStar RegExp t
    rexp )
                Char
    '?'   -> RegExp t -> RegExp t -> RegExp t
    forall t. RegExp t -> RegExp t -> RegExp t
    ROr     RegExp t
    rexp   RegExp t
    forall t. RegExp t
    REpsilon
                Char
    other -> [Char] -> RegExp t
    forall a. [Char] -> a
    C.badUsage ([Char]
    "in Regular Expression library: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++
                                   [Char]
    "unhandled operator: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Char -> [Char]
    forall a. Show a => a -> [Char]
    show Char
    other)
      return $ foldl transform subexp suffixes

    parser :: ( SymbolParser t )
             => GenParser Char () ( RegExp t )
    parser :: forall t. SymbolParser t => GenParser Char () (RegExp t)
    parser = GenParser Char () (RegExp t)
    forall t. SymbolParser t => GenParser Char () (RegExp t)
    regexp GenParser Char () (RegExp t)
    -> ParsecT [Char] () Identity () -> GenParser Char () (RegExp t)
    forall tok a b.
    GenParser tok () a -> GenParser tok () b -> GenParser tok () a
    `followedBy` ParsecT [Char] () Identity ()
    forall s (m :: * -> *) t u.
    (Stream s m t, Show t) =>
    ParsecT s u m ()
    eof

    hasEpsilon                    :: RegExp t -> Bool
    hasEpsilon :: forall t. RegExp t -> Bool
    hasEpsilon   RegExp t
    REpsilon         = Bool
    True
    hasEpsilon ( RSymbol  NumSym t
    _     ) = Bool
    False
    hasEpsilon ( ROr      RegExp t
    r1 RegExp t
    r2 ) = RegExp t -> Bool
    forall t. RegExp t -> Bool
    hasEpsilon RegExp t
    r1 Bool -> Bool -> Bool
    || RegExp t -> Bool
    forall t. RegExp t -> Bool
    hasEpsilon RegExp t
    r2
    hasEpsilon ( RConcat  RegExp t
    r1 RegExp t
    r2 ) = RegExp t -> Bool
    forall t. RegExp t -> Bool
    hasEpsilon RegExp t
    r1 Bool -> Bool -> Bool
    && RegExp t -> Bool
    forall t. RegExp t -> Bool
    hasEpsilon RegExp t
    r2
    hasEpsilon ( RStar    RegExp t
    _     ) = Bool
    True

    first                    :: RegExp t -> [ NumSym t ]
    first :: forall t. RegExp t -> [NumSym t]
    first   RegExp t
    REpsilon         = []
    first ( RSymbol  NumSym t
    s     ) = [ NumSym t
    s ]
    first ( ROr      RegExp t
    r1 RegExp t
    r2 ) = RegExp t -> [NumSym t]
    forall t. RegExp t -> [NumSym t]
    first RegExp t
    r1 [NumSym t] -> [NumSym t] -> [NumSym t]
    forall a. [a] -> [a] -> [a]
    ++ RegExp t -> [NumSym t]
    forall t. RegExp t -> [NumSym t]
    first RegExp t
    r2
    first ( RConcat  RegExp t
    r1 RegExp t
    r2 ) = RegExp t -> [NumSym t]
    forall t. RegExp t -> [NumSym t]
    first RegExp t
    r1 [NumSym t] -> [NumSym t] -> [NumSym t]
    forall a. [a] -> [a] -> [a]
    ++ if RegExp t -> Bool
    forall t. RegExp t -> Bool
    hasEpsilon RegExp t
    r1 then
                                               RegExp t -> [NumSym t]
    forall t. RegExp t -> [NumSym t]
    first RegExp t
    r2 else []
    first ( RStar    RegExp t
    r     ) = RegExp t -> [NumSym t]
    forall t. RegExp t -> [NumSym t]
    first RegExp t
    r

    reverse'                   :: RegExp t -> RegExp t
    reverse' :: forall t. RegExp t -> RegExp t
    reverse' ( ROr     RegExp t
    r1 RegExp t
    r2 ) = RegExp t -> RegExp t -> RegExp t
    forall t. RegExp t -> RegExp t -> RegExp t
    ROr     ( RegExp t -> RegExp t
    forall t. RegExp t -> RegExp t
    reverse' RegExp t
    r1 ) ( RegExp t -> RegExp t
    forall t. RegExp t -> RegExp t
    reverse' RegExp t
    r2 )
    reverse' ( RConcat RegExp t
    r1 RegExp t
    r2 ) = RegExp t -> RegExp t -> RegExp t
    forall t. RegExp t -> RegExp t -> RegExp t
    RConcat ( RegExp t -> RegExp t
    forall t. RegExp t -> RegExp t
    reverse' RegExp t
    r2 ) ( RegExp t -> RegExp t
    forall t. RegExp t -> RegExp t
    reverse' RegExp t
    r1 )
    reverse' ( RStar   RegExp t
    r     ) = RegExp t -> RegExp t
    forall t. RegExp t -> RegExp t
    RStar   ( RegExp t -> RegExp t
    forall t. RegExp t -> RegExp t
    reverse' RegExp t
    r  )
    reverse'   RegExp t
    e               = RegExp t
    e

    last' :: RegExp t -> [ NumSym t ]
    last' :: forall t. RegExp t -> [NumSym t]
    last' = RegExp t -> [NumSym t]
    forall t. RegExp t -> [NumSym t]
    first (RegExp t -> [NumSym t])
    -> (RegExp t -> RegExp t) -> RegExp t -> [NumSym t]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RegExp t -> RegExp t
    forall t. RegExp t -> RegExp t
    reverse'

    follow                        :: ( Eq t ) =>
                                     RegExp t -> NumSym t -> [ NumSym t ]
    follow :: forall t. Eq t => RegExp t -> NumSym t -> [NumSym t]
    follow   RegExp t
    REpsilon         NumSym t
    _   = []
    follow ( RSymbol  NumSym t
    _     ) NumSym t
    _   = []
    follow ( ROr      RegExp t
    r1 RegExp t
    r2 ) NumSym t
    sNr = RegExp t -> NumSym t -> [NumSym t]
    forall t. Eq t => RegExp t -> NumSym t -> [NumSym t]
    follow RegExp t
    r1 NumSym t
    sNr [NumSym t] -> [NumSym t] -> [NumSym t]
    forall a. [a] -> [a] -> [a]
    ++ RegExp t -> NumSym t -> [NumSym t]
    forall t. Eq t => RegExp t -> NumSym t -> [NumSym t]
    follow RegExp t
    r2 NumSym t
    sNr
    follow ( RConcat  RegExp t
    r1 RegExp t
    r2 ) NumSym t
    sNr = RegExp t -> NumSym t -> [NumSym t]
    forall t. Eq t => RegExp t -> NumSym t -> [NumSym t]
    follow RegExp t
    r1 NumSym t
    sNr [NumSym t] -> [NumSym t] -> [NumSym t]
    forall a. [a] -> [a] -> [a]
    ++ RegExp t -> NumSym t -> [NumSym t]
    forall t. Eq t => RegExp t -> NumSym t -> [NumSym t]
    follow RegExp t
    r2 NumSym t
    sNr
                                    [NumSym t] -> [NumSym t] -> [NumSym t]
    forall a. [a] -> [a] -> [a]
    ++ if NumSym t
    sNr NumSym t -> [NumSym t] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` RegExp t -> [NumSym t]
    forall t. RegExp t -> [NumSym t]
    last' RegExp t
    r1 then
                                           RegExp t -> [NumSym t]
    forall t. RegExp t -> [NumSym t]
    first RegExp t
    r2 else []
    follow ( RStar    RegExp t
    r     ) NumSym t
    sNr = RegExp t -> NumSym t -> [NumSym t]
    forall t. Eq t => RegExp t -> NumSym t -> [NumSym t]
    follow RegExp t
    r NumSym t
    sNr
                                    [NumSym t] -> [NumSym t] -> [NumSym t]
    forall a. Eq a => [a] -> [a] -> [a]
    `union` if NumSym t
    sNr NumSym t -> [NumSym t] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` RegExp t -> [NumSym t]
    forall t. RegExp t -> [NumSym t]
    last' RegExp t
    r then
                                                RegExp t -> [NumSym t]
    forall t. RegExp t -> [NumSym t]
    first RegExp t
    r else []

    preceding :: ( Eq t ) => RegExp t -> NumSym t -> [ NumSym t ]
    preceding :: forall t. Eq t => RegExp t -> NumSym t -> [NumSym t]
    preceding = RegExp t -> NumSym t -> [NumSym t]
    forall t. Eq t => RegExp t -> NumSym t -> [NumSym t]
    follow (RegExp t -> NumSym t -> [NumSym t])
    -> (RegExp t -> RegExp t) -> RegExp t -> NumSym t -> [NumSym t]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RegExp t -> RegExp t
    forall t. RegExp t -> RegExp t
    reverse'

    hasFinitePath                   :: RegExp t -> Bool
    hasFinitePath :: forall t. RegExp t -> Bool
    hasFinitePath ( ROr     RegExp t
    r1 RegExp t
    r2 ) = RegExp t -> Bool
    forall t. RegExp t -> Bool
    hasFinitePath RegExp t
    r1 Bool -> Bool -> Bool
    || RegExp t -> Bool
    forall t. RegExp t -> Bool
    hasFinitePath RegExp t
    r2
    hasFinitePath ( RConcat RegExp t
    _  RegExp t
    r2 ) = RegExp t -> Bool
    forall t. RegExp t -> Bool
    hasFinitePath RegExp t
    r2
    hasFinitePath ( RStar   RegExp t
    _     ) = Bool
    False
    hasFinitePath   RegExp t
    _               = Bool
    True

    getSymbols                   :: RegExp t -> [ NumSym t ]
    getSymbols :: forall t. RegExp t -> [NumSym t]
    getSymbols ( RSymbol NumSym t
    s     ) = [ NumSym t
    s ]
    getSymbols ( ROr     RegExp t
    r1 RegExp t
    r2 ) = RegExp t -> [NumSym t]
    forall t. RegExp t -> [NumSym t]
    getSymbols RegExp t
    r1 [NumSym t] -> [NumSym t] -> [NumSym t]
    forall a. [a] -> [a] -> [a]
    ++ RegExp t -> [NumSym t]
    forall t. RegExp t -> [NumSym t]
    getSymbols RegExp t
    r2
    getSymbols ( RConcat RegExp t
    r1 RegExp t
    r2 ) = RegExp t -> [NumSym t]
    forall t. RegExp t -> [NumSym t]
    getSymbols RegExp t
    r1 [NumSym t] -> [NumSym t] -> [NumSym t]
    forall a. [a] -> [a] -> [a]
    ++ RegExp t -> [NumSym t]
    forall t. RegExp t -> [NumSym t]
    getSymbols RegExp t
    r2
    getSymbols ( RStar   RegExp t
    r     ) = RegExp t -> [NumSym t]
    forall t. RegExp t -> [NumSym t]
    getSymbols RegExp t
    r
    getSymbols   RegExp t
    _               = []

    -- assign each symbol in the regular expression a
    -- unique number, counting up from 0
    enumSyms   :: RegExp t -> RegExp t
    enumSyms :: forall t. RegExp t -> RegExp t
    enumSyms RegExp t
    rexp = State Int (RegExp t) -> Int -> RegExp t
    forall s a. State s a -> s -> a
    evalState ( RegExp t -> State Int (RegExp t)
    forall {m :: * -> *} {t}.
    MonadState Int m =>
    RegExp t -> m (RegExp t)
    enumSyms' RegExp t
    rexp ) Int
    0
        where
          enumSyms' :: RegExp t -> m (RegExp t)
    enumSyms' ( RSymbol NumSym t
    s     ) = do
            num <- m Int
    forall s (m :: * -> *). MonadState s m => m s
    get
            modify ( + 1 )
            return $ RSymbol s { symbolNum = Just num }
          enumSyms' ( ROr     RegExp t
    r1 RegExp t
    r2 ) = do
            r1' <- RegExp t -> m (RegExp t)
    enumSyms' RegExp t
    r1
            r2' <- enumSyms' r2
            return $ ROr r1' r2'
          enumSyms' ( RConcat RegExp t
    r1 RegExp t
    r2 ) = do
            r1' <- RegExp t -> m (RegExp t)
    enumSyms' RegExp t
    r1
            r2' <- enumSyms' r2
            return $ RConcat r1' r2'
          enumSyms' ( RStar   RegExp t
    r     ) = do
            r'  <- RegExp t -> m (RegExp t)
    enumSyms' RegExp t
    r
            return $ RStar   r'
          enumSyms'   RegExp t
    other           =
            RegExp t -> m (RegExp t)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return RegExp t
    other

    regexp2CopilotNFA :: ( C.Typed t, Eq t )
                         => C.Stream t -> RegExp t -> C.Stream Bool -> C.Stream Bool
    regexp2CopilotNFA :: forall t.
    (Typed t, Eq t) =>
    Stream t -> RegExp t -> Stream Bool -> Stream Bool
    regexp2CopilotNFA Stream t
    inStream RegExp t
    rexp Stream Bool
    reset =
        let symbols :: [NumSym t]
    symbols                    = RegExp t -> [NumSym t]
    forall t. RegExp t -> [NumSym t]
    getSymbols RegExp t
    rexp
            first' :: [NumSym t]
    first'                     = RegExp t -> [NumSym t]
    forall t. RegExp t -> [NumSym t]
    first RegExp t
    rexp
            start :: Stream Bool
    start                      = [ Bool
    True ] [Bool] -> Stream Bool -> Stream Bool
    forall a. Typed a => [a] -> Stream a -> Stream a
    C.++ Stream Bool
    C.false

            preceding' :: NumSym t -> [Stream Bool]
    preceding'   NumSym t
    numSym        = let ps :: [NumSym t]
    ps    = RegExp t -> NumSym t -> [NumSym t]
    forall t. Eq t => RegExp t -> NumSym t -> [NumSym t]
    preceding RegExp t
    rexp NumSym t
    numSym
                                             s :: [Stream Bool]
    s     = if NumSym t
    numSym NumSym t -> [NumSym t] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [NumSym t]
    first' then
                                                       [ Stream Bool
    start ] else []
                                         in [Stream Bool]
    s [Stream Bool] -> [Stream Bool] -> [Stream Bool]
    forall a. [a] -> [a] -> [a]
    ++ [ [Stream Bool]
    streams [Stream Bool] -> Int -> Stream Bool
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    i
                                                 | Int
    i <- (NumSym t -> Int) -> [NumSym t] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map ( Maybe Int -> Int
    forall a. HasCallStack => Maybe a -> a
    fromJust (Maybe Int -> Int) -> (NumSym t -> Maybe Int) -> NumSym t -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NumSym t -> Maybe Int
    forall t. NumSym t -> Maybe Int
    symbolNum ) [NumSym t]
    ps ]

            matchesInput :: NumSym t -> Stream Bool
    matchesInput NumSym t
    numSym        = case NumSym t -> Sym t
    forall t. NumSym t -> Sym t
    symbol NumSym t
    numSym of
                                           Sym t
    Any   -> Stream Bool
    C.true
                                           Sym t
    t -> Stream t
    inStream Stream t -> Stream t -> Stream Bool
    forall a. (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
    C.== t -> Stream t
    forall a. Typed a => a -> Stream a
    C.constant t
    t

            transitions :: NumSym t -> t (Stream Bool) -> Stream Bool
    transitions  NumSym t
    numSym t (Stream Bool)
    ps     = NumSym t -> Stream Bool
    matchesInput NumSym t
    numSym
                                         Stream Bool -> Stream Bool -> Stream Bool
    C.&& ( (Stream Bool -> Stream Bool -> Stream Bool)
    -> Stream Bool -> t (Stream Bool) -> Stream Bool
    forall b a. (b -> a -> b) -> b -> t a -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl ( C.|| ) Stream Bool
    C.false t (Stream Bool)
    ps )

            stream :: NumSym t -> Stream Bool
    stream       NumSym t
    numSym        = let ps :: [Stream Bool]
    ps    = NumSym t -> [Stream Bool]
    preceding' NumSym t
    numSym
                                             init_ :: Stream Bool
    init_ = Bool -> Stream Bool
    forall a. Typed a => a -> Stream a
    C.constant (Bool -> Stream Bool) -> Bool -> Stream Bool
    forall a b. (a -> b) -> a -> b
    $ NumSym t
    numSym NumSym t -> [NumSym t] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [NumSym t]
    first'
                                         in Stream Bool -> Stream Bool -> Stream Bool -> Stream Bool
    forall a.
    Typed a =>
    Stream Bool -> Stream a -> Stream a -> Stream a
    C.mux Stream Bool
    reset
                                            ( [ Bool
    False ] [Bool] -> Stream Bool -> Stream Bool
    forall a. Typed a => [a] -> Stream a -> Stream a
    C.++ NumSym t -> Stream Bool
    matchesInput NumSym t
    numSym Stream Bool -> Stream Bool -> Stream Bool
    C.&& Stream Bool
    init_ )
                                            ( [ Bool
    False ] [Bool] -> Stream Bool -> Stream Bool
    forall a. Typed a => [a] -> Stream a -> Stream a
    C.++ NumSym t -> [Stream Bool] -> Stream Bool
    forall {t :: * -> *}.
    Foldable t =>
    NumSym t -> t (Stream Bool) -> Stream Bool
    transitions  NumSym t
    numSym [Stream Bool]
    ps )

            streams :: [Stream Bool]
    streams                    = (NumSym t -> Stream Bool) -> [NumSym t] -> [Stream Bool]
    forall a b. (a -> b) -> [a] -> [b]
    map NumSym t -> Stream Bool
    stream [NumSym t]
    symbols

            outStream :: Stream Bool
    outStream                  = (Stream Bool -> Stream Bool -> Stream Bool)
    -> Stream Bool -> [Stream Bool] -> Stream Bool
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl ( C.|| ) Stream Bool
    start [Stream Bool]
    streams

        in Stream Bool
    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 :: forall t.
    (Typed t, SymbolParser t, Eq t) =>
    Stream t -> [Char] -> Stream Bool -> Stream Bool
    copilotRegexp Stream t
    inStream [Char]
    rexp Stream Bool
    reset =
      case Parsec [Char] () (RegExp t)
    -> [Char] -> [Char] -> Either ParseError (RegExp t)
    forall s t a.
    Stream s Identity t =>
    Parsec s () a -> [Char] -> s -> Either ParseError a
    parse Parsec [Char] () (RegExp t)
    forall t. SymbolParser t => GenParser Char () (RegExp t)
    parser [Char]
    rexp [Char]
    rexp of
        Left  ParseError
    err -> [Char] -> Stream Bool
    forall a. [Char] -> a
    C.badUsage ([Char]
    "parsing regular exp: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ParseError -> [Char]
    forall a. Show a => a -> [Char]
    show ParseError
    err)
        Right RegExp t
    rexp' -> let nrexp :: RegExp t
    nrexp = RegExp t -> RegExp t
    forall t. RegExp t -> RegExp t
    enumSyms RegExp t
    rexp' in
            if RegExp t -> Bool
    forall t. RegExp t -> Bool
    hasFinitePath RegExp t
    nrexp then
                [Char] -> Stream Bool
    forall a. [Char] -> a
    C.badUsage ([Char] -> Stream Bool) -> [Char] -> Stream Bool
    forall a b. (a -> b) -> a -> b
    $
                [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [ [Char]
    "The regular expression contains a finite path "
                       , [Char]
    "which is something that will fail to match "
                       , [Char]
    "since we do not have a distinct end-of-input "
                       , [Char]
    "symbol on infinite streams." ]
            else if RegExp t -> Bool
    forall t. RegExp t -> Bool
    hasEpsilon RegExp t
    nrexp then
                     [Char] -> Stream Bool
    forall a. [Char] -> a
    C.badUsage ([Char] -> Stream Bool) -> [Char] -> Stream Bool
    forall a b. (a -> b) -> a -> b
    $
                     [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [ [Char]
    "The regular expression matches a language "
                            , [Char]
    "that contains epsilon. This cannot be handled "
                            , [Char]
    "on infinite streams, since we do not have "
                            , [Char]
    "a distinct end-of-input symbol." ]
                 else Stream t -> RegExp t -> Stream Bool -> Stream Bool
    forall t.
    (Typed t, Eq t) =>
    Stream t -> RegExp t -> Stream Bool -> Stream Bool
    regexp2CopilotNFA Stream t
    inStream RegExp t
    nrexp Stream Bool
    reset

    regexp2CopilotNFAB :: RegExp P -> [ ( StreamName, C.Stream Bool ) ]
                          -> C.Stream Bool -> C.Stream Bool
    regexp2CopilotNFAB :: RegExp P -> [([Char], Stream Bool)] -> Stream Bool -> Stream Bool
    regexp2CopilotNFAB RegExp P
    rexp [([Char], Stream Bool)]
    propositions Stream Bool
    reset =
        let symbols :: [NumSym P]
    symbols                    = RegExp P -> [NumSym P]
    forall t. RegExp t -> [NumSym t]
    getSymbols RegExp P
    rexp
            first' :: [NumSym P]
    first'                     = RegExp P -> [NumSym P]
    forall t. RegExp t -> [NumSym t]
    first RegExp P
    rexp
            start :: Stream Bool
    start                      = [ Bool
    True ] [Bool] -> Stream Bool -> Stream Bool
    forall a. Typed a => [a] -> Stream a -> Stream a
    C.++ Stream Bool
    C.false

            preceding' :: NumSym P -> [Stream Bool]
    preceding'   NumSym P
    numSym        = let ps :: [NumSym P]
    ps    = RegExp P -> NumSym P -> [NumSym P]
    forall t. Eq t => RegExp t -> NumSym t -> [NumSym t]
    preceding RegExp P
    rexp NumSym P
    numSym
                                             s :: [Stream Bool]
    s     = if NumSym P
    numSym NumSym P -> [NumSym P] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [NumSym P]
    first' then
                                                       [ Stream Bool
    start ] else []
                                         in [Stream Bool]
    s [Stream Bool] -> [Stream Bool] -> [Stream Bool]
    forall a. [a] -> [a] -> [a]
    ++ [ [Stream Bool]
    streams [Stream Bool] -> Int -> Stream Bool
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    i
                                                 | Int
    i <- (NumSym P -> Int) -> [NumSym P] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map ( Maybe Int -> Int
    forall a. HasCallStack => Maybe a -> a
    fromJust (Maybe Int -> Int) -> (NumSym P -> Maybe Int) -> NumSym P -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NumSym P -> Maybe Int
    forall t. NumSym t -> Maybe Int
    symbolNum ) [NumSym P]
    ps ]

            lookup' :: [Char] -> [([Char], a)] -> a
    lookup' [Char]
    a [([Char], a)]
    l = case [Char] -> [([Char], a)] -> Maybe a
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup [Char]
    a [([Char], a)]
    l of
                            Maybe a
    Nothing -> [Char] -> a
    forall a. [Char] -> a
    C.badUsage ([Char]
    "boolean stream "
                                                 [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    a
                                                 [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " is not defined")
                            Just a
    s  -> a
    s

            matchesInput :: NumSym P -> Stream Bool
    matchesInput NumSym P
    numSym        = case NumSym P -> Sym P
    forall t. NumSym t -> Sym t
    symbol NumSym P
    numSym of
                                           Sym P
    Any   -> Stream Bool
    C.true
                                           Sym P
    t -> [Char] -> [([Char], Stream Bool)] -> Stream Bool
    forall {a}. [Char] -> [([Char], a)] -> a
    lookup' ( P -> [Char]
    getName P
    t ) [([Char], Stream Bool)]
    propositions

            transitions :: NumSym P -> t (Stream Bool) -> Stream Bool
    transitions  NumSym P
    numSym t (Stream Bool)
    ps     = NumSym P -> Stream Bool
    matchesInput NumSym P
    numSym
                                         Stream Bool -> Stream Bool -> Stream Bool
    C.&& ( (Stream Bool -> Stream Bool -> Stream Bool)
    -> Stream Bool -> t (Stream Bool) -> Stream Bool
    forall b a. (b -> a -> b) -> b -> t a -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl ( C.|| ) Stream Bool
    C.false t (Stream Bool)
    ps )

            stream :: NumSym P -> Stream Bool
    stream       NumSym P
    numSym        = let ps :: [Stream Bool]
    ps    = NumSym P -> [Stream Bool]
    preceding' NumSym P
    numSym
                                             init_ :: Stream Bool
    init_ = Bool -> Stream Bool
    forall a. Typed a => a -> Stream a
    C.constant (Bool -> Stream Bool) -> Bool -> Stream Bool
    forall a b. (a -> b) -> a -> b
    $ NumSym P
    numSym NumSym P -> [NumSym P] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [NumSym P]
    first'
                                         in Stream Bool -> Stream Bool -> Stream Bool -> Stream Bool
    forall a.
    Typed a =>
    Stream Bool -> Stream a -> Stream a -> Stream a
    C.mux Stream Bool
    reset
                                            ( [ Bool
    False ] [Bool] -> Stream Bool -> Stream Bool
    forall a. Typed a => [a] -> Stream a -> Stream a
    C.++ NumSym P -> Stream Bool
    matchesInput NumSym P
    numSym Stream Bool -> Stream Bool -> Stream Bool
    C.&& Stream Bool
    init_ )
                                            ( [ Bool
    False ] [Bool] -> Stream Bool -> Stream Bool
    forall a. Typed a => [a] -> Stream a -> Stream a
    C.++ NumSym P -> [Stream Bool] -> Stream Bool
    forall {t :: * -> *}.
    Foldable t =>
    NumSym P -> t (Stream Bool) -> Stream Bool
    transitions  NumSym P
    numSym [Stream Bool]
    ps )

            streams :: [Stream Bool]
    streams                    = (NumSym P -> Stream Bool) -> [NumSym P] -> [Stream Bool]
    forall a b. (a -> b) -> [a] -> [b]
    map NumSym P -> Stream Bool
    stream [NumSym P]
    symbols

            outStream :: Stream Bool
    outStream                  = (Stream Bool -> Stream Bool -> Stream Bool)
    -> Stream Bool -> [Stream Bool] -> Stream Bool
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl ( C.|| ) Stream Bool
    start [Stream Bool]
    streams

        in Stream Bool
    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 :: [Char] -> [([Char], Stream Bool)] -> Stream Bool -> Stream Bool
    copilotRegexpB [Char]
    rexp [([Char], Stream Bool)]
    propositions Stream Bool
    reset =
      case GenParser Char () (RegExp P)
    -> [Char] -> [Char] -> Either ParseError (RegExp P)
    forall s t a.
    Stream s Identity t =>
    Parsec s () a -> [Char] -> s -> Either ParseError a
    parse GenParser Char () (RegExp P)
    forall t. SymbolParser t => GenParser Char () (RegExp t)
    parser [Char]
    rexp [Char]
    rexp of
        Left  ParseError
    err -> [Char] -> Stream Bool
    forall a. [Char] -> a
    C.badUsage ([Char]
    "parsing regular exp: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ParseError -> [Char]
    forall a. Show a => a -> [Char]
    show ParseError
    err)
        Right RegExp P
    rexp' -> let nrexp :: RegExp P
    nrexp = RegExp P -> RegExp P
    forall t. RegExp t -> RegExp t
    enumSyms RegExp P
    rexp' in
            if RegExp P -> Bool
    forall t. RegExp t -> Bool
    hasFinitePath RegExp P
    nrexp then
                [Char] -> Stream Bool
    forall a. [Char] -> a
    C.badUsage ([Char] -> Stream Bool) -> [Char] -> Stream Bool
    forall a b. (a -> b) -> a -> b
    $
                [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [ [Char]
    "The regular expression contains a finite path "
                       , [Char]
    "which is something that will fail to match "
                       , [Char]
    "since we do not have a distinct end-of-input "
                       , [Char]
    "symbol on infinite streams." ]
            else if RegExp P -> Bool
    forall t. RegExp t -> Bool
    hasEpsilon RegExp P
    nrexp then
                     [Char] -> Stream Bool
    forall a. [Char] -> a
    C.badUsage ([Char] -> Stream Bool) -> [Char] -> Stream Bool
    forall a b. (a -> b) -> a -> b
    $
                     [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [ [Char]
    "The regular expression matches a language "
                            , [Char]
    "that contains epsilon. This cannot be handled "
                            , [Char]
    "on infinite streams, since we do not have "
                            , [Char]
    "a distinct end-of-input symbol." ]
                 else RegExp P -> [([Char], Stream Bool)] -> Stream Bool -> Stream Bool
    regexp2CopilotNFAB RegExp P
    nrexp [([Char], Stream Bool)]
    propositions Stream Bool
    reset