{-# LANGUAGE BangPatterns          #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Safe                  #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Kleene.DFA (
    DFA (..),
    -- * Conversions
    fromRE,
    toRE,
    fromERE,
    toERE,
    fromTM,
    fromTMEquiv,
    toKleene,
    toDot,
    toDot',
    ) where

import Algebra.Lattice
       (BoundedJoinSemiLattice (..), BoundedMeetSemiLattice (..), Lattice (..))
import Data.IntMap       (IntMap)
import Data.IntSet       (IntSet)
import Data.List         (intercalate)
import Data.Map          (Map)
import Data.Maybe        (fromMaybe)
import Data.RangeSet.Map (RSet)

import qualified Data.ByteString                    as BS
import qualified Data.Function.Step.Discrete.Closed as SF
import qualified Data.IntMap                        as IntMap
import qualified Data.IntSet                        as IntSet
import qualified Data.Map                           as Map
import qualified Data.MemoTrie                      as MT
import qualified Data.RangeSet.Map                  as RSet

import           Kleene.Classes
import qualified Kleene.ERE             as ERE
import           Kleene.Internal.Pretty
import qualified Kleene.Internal.RE     as RE

-- $setup
-- >>> :set -XOverloadedStrings
-- >>> import Data.Foldable (traverse_)
-- >>> import Data.Semigroup (Semigroup (..))
-- >>> import Algebra.Lattice ((/\))
-- >>> import Kleene.Classes
-- >>> import Kleene.Internal.Pretty (putPretty)
-- >>> import Test.QuickCheck ((===))
-- >>> import qualified Test.QuickCheck as QC
-- >>> import qualified Kleene.RE as RE
-- >>> import qualified Kleene.ERE as ERE
-- >>> import qualified Data.RangeSet.Map as RSet
--
-- >>> newtype Smaller a = Smaller a deriving (Show)
-- >>> let intLog2 = (`div` 10)
-- >>> instance QC.Arbitrary a => QC.Arbitrary (Smaller a) where arbitrary = QC.scale intLog2 QC.arbitrary; shrink (Smaller a) = map Smaller (QC.shrink a)
--
-- >>> let asREChar :: RE.RE Char -> RE.RE Char; asREChar = id

-------------------------------------------------------------------------------
-- DFA
-------------------------------------------------------------------------------

-- | Deterministic finite automaton.
--
-- A deterministic finite automaton (DFA) over an alphabet \(\Sigma\) (type
-- variable @c@) is 4-tuple \(Q\), \(q_0\) , \(F\), \(\delta\), where
--
-- * \(Q\) is a finite set of states (subset of 's'),
-- * \(q_0 \in Q\) is the distinguised start state ('dfaInitial'),
-- * \(F \subset Q\) is a set of final (or  accepting) states ('dfaAcceptable'), and
-- * \(\delta : Q \times \Sigma \to Q\) is a function called the state
-- transition function ('dfaTransition').
--
data DFA c = DFA
    { forall c. DFA c -> IntMap (SF c Int)
dfaTransition   :: !(IntMap (SF.SF c Int))
      -- ^ transition function
    , forall c. DFA c -> Int
dfaInitial      :: !Int
      -- ^ initial state
    , forall c. DFA c -> IntSet
dfaAcceptable   :: !IntSet
      -- ^ accept states
    , forall c. DFA c -> IntSet
dfaBlackholes   :: !IntSet
      -- ^ states we cannot escape
    }
  deriving Int -> DFA c -> ShowS
[DFA c] -> ShowS
DFA c -> String
(Int -> DFA c -> ShowS)
-> (DFA c -> String) -> ([DFA c] -> ShowS) -> Show (DFA c)
forall c. Show c => Int -> DFA c -> ShowS
forall c. Show c => [DFA c] -> ShowS
forall c. Show c => DFA c -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall c. Show c => Int -> DFA c -> ShowS
showsPrec :: Int -> DFA c -> ShowS
$cshow :: forall c. Show c => DFA c -> String
show :: DFA c -> String
$cshowList :: forall c. Show c => [DFA c] -> ShowS
showList :: [DFA c] -> ShowS
Show

-------------------------------------------------------------------------------
-- Construction
-------------------------------------------------------------------------------

-- | Convert 'RE.RE' to 'DFA'.
--
-- >>> putPretty $ fromRE $ RE.star "abc"
-- 0+ -> \x -> if
--     | x <= '`'  -> 3
--     | x <= 'a'  -> 2
--     | otherwise -> 3
-- 1 -> \x -> if
--     | x <= 'b'  -> 3
--     | x <= 'c'  -> 0
--     | otherwise -> 3
-- 2 -> \x -> if
--     | x <= 'a'  -> 3
--     | x <= 'b'  -> 1
--     | otherwise -> 3
-- 3 -> \_ -> 3 -- black hole
--
-- Everything and nothing result in blackholes:
--
-- >>> traverse_ (putPretty . fromRE) [RE.empty, RE.star RE.anyChar]
-- 0 -> \_ -> 0 -- black hole
-- 0+ -> \_ -> 0 -- black hole
--
-- Character ranges are effecient:
--
-- >>> putPretty $ fromRE $ RE.charRange 'a' 'z'
-- 0 -> \x -> if
--     | x <= '`'  -> 2
--     | x <= 'z'  -> 1
--     | otherwise -> 2
-- 1+ -> \_ -> 2
-- 2 -> \_ -> 2 -- black hole
--
-- An example with two blackholes:
--
-- >>> putPretty $ fromRE $ "c" <> RE.star RE.anyChar
-- 0 -> \x -> if
--     | x <= 'b'  -> 2
--     | x <= 'c'  -> 1
--     | otherwise -> 2
-- 1+ -> \_ -> 1 -- black hole
-- 2 -> \_ -> 2 -- black hole
--
fromRE :: forall c. (Ord c, Enum c, Bounded c) => RE.RE c -> DFA c
fromRE :: forall c. (Ord c, Enum c, Bounded c) => RE c -> DFA c
fromRE = RE c -> DFA c
forall k c. (Ord k, Ord c, TransitionMap c k) => k -> DFA c
fromTM

-- | Convert 'ERE.ERE' to 'DFA'.
--
-- We don't always generate a minimal automata:
--
-- >>> putPretty $ fromERE $ "a" /\ "b"
-- 0 -> \_ -> 1
-- 1 -> \_ -> 1 -- black hole
--
-- Compare this to a 'complement' example
--
-- Using 'fromTMEquiv', we can get a minimal automaton, for the cost of higher
-- complexity (slow!).
--
-- >>> putPretty $ fromTMEquiv $ ("a" /\ "b" :: ERE.ERE Char)
-- 0 -> \_ -> 0 -- black hole
--
-- >>> putPretty $ fromERE $ complement $ star "abc"
-- 0 -> \x -> if
--     | x <= '`'  -> 3
--     | x <= 'a'  -> 2
--     | otherwise -> 3
-- 1+ -> \x -> if
--     | x <= 'b'  -> 3
--     | x <= 'c'  -> 0
--     | otherwise -> 3
-- 2+ -> \x -> if
--     | x <= 'a'  -> 3
--     | x <= 'b'  -> 1
--     | otherwise -> 3
-- 3+ -> \_ -> 3 -- black hole
--
fromERE :: forall c. (Ord c, Enum c, Bounded c) => ERE.ERE c -> DFA c
fromERE :: forall c. (Ord c, Enum c, Bounded c) => ERE c -> DFA c
fromERE = ERE c -> DFA c
forall k c. (Ord k, Ord c, TransitionMap c k) => k -> DFA c
fromTM

-- | Create from 'TransitionMap'.
--
-- See 'fromRE' for a specific example.
fromTM :: forall k c. (Ord k, Ord c, TransitionMap c k) => k -> DFA c
fromTM :: forall k c. (Ord k, Ord c, TransitionMap c k) => k -> DFA c
fromTM = Maybe (k -> k -> Bool) -> k -> DFA c
forall k c.
(Ord k, Ord c, TransitionMap c k) =>
Maybe (k -> k -> Bool) -> k -> DFA c
fromTMImpl Maybe (k -> k -> Bool)
forall a. Maybe a
Nothing

-- | Create from 'TransitonMap' minimising states with 'Equivalent'.
--
-- See 'fromERE' for an example.
--
fromTMEquiv :: forall k c. (Ord k, Ord c, TransitionMap c k, Equivalent c k) => k -> DFA c
fromTMEquiv :: forall k c.
(Ord k, Ord c, TransitionMap c k, Equivalent c k) =>
k -> DFA c
fromTMEquiv = Maybe (k -> k -> Bool) -> k -> DFA c
forall k c.
(Ord k, Ord c, TransitionMap c k) =>
Maybe (k -> k -> Bool) -> k -> DFA c
fromTMImpl ((k -> k -> Bool) -> Maybe (k -> k -> Bool)
forall a. a -> Maybe a
Just k -> k -> Bool
forall c k. Equivalent c k => k -> k -> Bool
equivalent)

fromTMImpl :: forall k c. (Ord k, Ord c, TransitionMap c k)
    => Maybe (k ->  k -> Bool)
    -> k
    -> DFA c
fromTMImpl :: forall k c.
(Ord k, Ord c, TransitionMap c k) =>
Maybe (k -> k -> Bool) -> k -> DFA c
fromTMImpl Maybe (k -> k -> Bool)
mequiv k
re = DFA
    { dfaTransition :: IntMap (SF c Int)
dfaTransition = IntMap (SF c Int)
transition
    , dfaInitial :: Int
dfaInitial    = Int
0
    , dfaAcceptable :: IntSet
dfaAcceptable = [Int] -> IntSet
IntSet.fromList
        [ Int
i
        | (k
re', Int
i) <- Map k Int -> [(k, Int)]
forall k a. Map k a -> [(k, a)]
Map.toList Map k Int
lookupMap
        , k -> Bool
forall c k. Derivate c k => k -> Bool
nullable k
re'
        ]
    , dfaBlackholes :: IntSet
dfaBlackholes = IntSet
blackholes
    }
  where
    transition :: IntMap (SF c Int)
transition = [(Int, SF c Int)] -> IntMap (SF c Int)
forall a. [(Int, a)] -> IntMap a
IntMap.fromList
        [ (Int
i, SF c Int
js)
        | (k
re', SF c k
pm) <- Map k (SF c k) -> [(k, SF c k)]
forall k a. Map k a -> [(k, a)]
Map.toList Map k (SF c k)
tm
        , let i :: Int
i  = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ k -> Map k Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
re' Map k Int
lookupMap
        , let js :: SF c Int
js = SF c Int -> SF c Int
forall v k. Eq v => SF k v -> SF k v
SF.normalise (SF c Int -> SF c Int) -> SF c Int -> SF c Int
forall a b. (a -> b) -> a -> b
$ (k -> Int) -> SF c k -> SF c Int
forall a b. (a -> b) -> SF c a -> SF c b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\k
re'' -> Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ k -> Map k Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
re'' Map k Int
lookupMap) SF c k
pm
        ]

    blackholes :: IntSet
blackholes = [Int] -> IntSet
IntSet.fromList
        [ Int
i
        | (Int
i, SF c Int
sf) <- IntMap (SF c Int) -> [(Int, SF c Int)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (SF c Int)
transition
        , SF c Int
sf SF c Int -> SF c Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> SF c Int
forall a. a -> SF c a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
i
        ]

    tm :: Map k (SF c k)
tm = k -> Map k (SF c k)
forall c k. TransitionMap c k => k -> Map k (SF c k)
transitionMap k
re

    -- reversing makes error state go last, usually
    lookupMap :: Map k Int
    lookupMap :: Map k Int
lookupMap = Int -> Map k Int -> [(k, SF c k)] -> Map k Int
forall b. Int -> Map k Int -> [(k, b)] -> Map k Int
makeLookup Int
1 Map k Int
lookupMap' ([(k, SF c k)] -> [(k, SF c k)]
forall a. [a] -> [a]
reverse ([(k, SF c k)] -> [(k, SF c k)]) -> [(k, SF c k)] -> [(k, SF c k)]
forall a b. (a -> b) -> a -> b
$ Map k (SF c k) -> [(k, SF c k)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map k (SF c k) -> [(k, SF c k)])
-> Map k (SF c k) -> [(k, SF c k)]
forall a b. (a -> b) -> a -> b
$ k -> Map k (SF c k) -> Map k (SF c k)
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete k
re Map k (SF c k)
tm)

    lookupMap' :: Map k Int
    lookupMap' :: Map k Int
lookupMap' = case k -> Map k (SF c k) -> Maybe (SF c k)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
re Map k (SF c k)
tm of
        Maybe (SF c k)
Nothing -> Map k Int
forall k a. Map k a
Map.empty
        Just SF c k
_  -> k -> Int -> Map k Int
forall k a. k -> a -> Map k a
Map.singleton k
re Int
0

    makeLookup :: Int -> Map k Int -> [(k, b)] -> Map k Int
    makeLookup :: forall b. Int -> Map k Int -> [(k, b)] -> Map k Int
makeLookup = (Int -> Map k Int -> [(k, b)] -> Map k Int)
-> ((k -> k -> Bool) -> Int -> Map k Int -> [(k, b)] -> Map k Int)
-> Maybe (k -> k -> Bool)
-> Int
-> Map k Int
-> [(k, b)]
-> Map k Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int -> Map k Int -> [(k, b)] -> Map k Int
forall b. Int -> Map k Int -> [(k, b)] -> Map k Int
makeLookupEq (k -> k -> Bool) -> Int -> Map k Int -> [(k, b)] -> Map k Int
forall b.
(k -> k -> Bool) -> Int -> Map k Int -> [(k, b)] -> Map k Int
makeLookupEquiv Maybe (k -> k -> Bool)
mequiv

    makeLookupEq :: Int -> Map k Int -> [(k, b)] -> Map k Int
    makeLookupEq :: forall b. Int -> Map k Int -> [(k, b)] -> Map k Int
makeLookupEq !Int
_ !Map k Int
acc []            = Map k Int
acc
    makeLookupEq !Int
n Map k Int
acc ((k
x, b
_) : [(k, b)]
xs) = Int -> Map k Int -> [(k, b)] -> Map k Int
forall b. Int -> Map k Int -> [(k, b)] -> Map k Int
makeLookup (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (k -> Int -> Map k Int -> Map k Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
x Int
n Map k Int
acc) [(k, b)]
xs

    -- this differs from makeLookupEq. We don't insert new states right away,
    -- but check whether equivalent state is already in the map.
    --
    -- This causes n^2 of exp m operations, where n = number of states and
    -- m size of @k@.
    makeLookupEquiv :: (k -> k -> Bool) ->  Int -> Map k Int -> [(k, b)] -> Map k Int
    makeLookupEquiv :: forall b.
(k -> k -> Bool) -> Int -> Map k Int -> [(k, b)] -> Map k Int
makeLookupEquiv k -> k -> Bool
_  !Int
_ !Map k Int
acc []           = Map k Int
acc
    makeLookupEquiv k -> k -> Bool
eq !Int
n Map k Int
acc ((k
x, b
_) : [(k, b)]
xs) = case [(k, Int)]
ys of
        []           -> Int -> Map k Int -> [(k, b)] -> Map k Int
forall b. Int -> Map k Int -> [(k, b)] -> Map k Int
makeLookup (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (k -> Int -> Map k Int -> Map k Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
x Int
n Map k Int
acc) [(k, b)]
xs
        ((k
_, Int
i) : [(k, Int)]
_) -> Int -> Map k Int -> [(k, b)] -> Map k Int
forall b. Int -> Map k Int -> [(k, b)] -> Map k Int
makeLookup Int
n       (k -> Int -> Map k Int -> Map k Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
x Int
i Map k Int
acc) [(k, b)]
xs
      where
        ys :: [(k, Int)]
ys = [ (k, Int)
p | p :: (k, Int)
p@(k
y, Int
_) <- Map k Int -> [(k, Int)]
forall k a. Map k a -> [(k, a)]
Map.toList Map k Int
acc, k -> k -> Bool
eq k
x k
y ]

-------------------------------------------------------------------------------
-- Destruction
-------------------------------------------------------------------------------

-- | Convert 'DFA' to 'RE.RE'.
--
-- >>> putPretty $ toRE $ fromRE "foobar"
-- ^foobar$
--
-- For 'RE.string' regular expressions, @'toRE' . 'fromRE' = 'id'@:
--
-- prop> let s' = take 5 s in RE.string (s' :: String) === toRE (fromRE (RE.string s'))
--
-- But in general it isn't:
--
-- >>> let aToZ = RE.star $ RE.charRange 'a' 'z'
-- >>> traverse_ putPretty [aToZ, toRE $ fromRE aToZ]
-- ^[a-z]*$
-- ^([a-z]|[a-z]?[a-z]*[a-z]?)?$
--
-- @
-- not-prop> (re :: RE.RE Char) === toRE (fromRE re)
-- @
--
-- However, they are 'RE.equivalent':
--
-- >>> RE.equivalent aToZ (toRE (fromRE aToZ))
-- True
--
-- And so are others
--
-- >>> all (\re -> RE.equivalent re (toRE (fromRE re))) [RE.star "a", RE.star "ab"]
-- True
--
-- @
-- expensive-prop> RE.equivalent re (toRE (fromRE (re :: RE.RE Char)))
-- @
--
-- Note, that @'toRE' . 'fromRE'@ can, and usually makes regexp unrecognisable:
--
-- >>> putPretty $ toRE $ fromRE $ RE.star "ab"
-- ^(a(ba)*b)?$
--
-- We can 'complement' DFA, therefore we can complement 'RE.RE'.
-- For example. regular expression matching string containing an @a@:
--
-- >>> let withA = RE.star RE.anyChar <> "a" <> RE.star RE.anyChar
-- >>> let withoutA = toRE $ complement $ fromRE withA
-- >>> putPretty withoutA
-- ^([^a]|[^a]?[^a]*[^a]?)?$
--
-- >>> let withoutA' = RE.star $ RE.REChars $ RSet.complement $ RSet.singleton 'a'
-- >>> putPretty withoutA'
-- ^[^a]*$
--
-- >>> RE.equivalent withoutA withoutA'
-- True
--
-- Quite small, for example 2 state DFAs can result in big regular expressions:
--
-- >>> putPretty $ toRE $ complement $ fromRE $ star "ab"
-- ^([^]|a(ba)*(ba)?|a(ba)*([^b]|b[^a])|([^a]|a(ba)*([^b]|b[^a]))[^]*[^]?)$
--
-- We can use @'toRE' . 'fromERE'@ to convert 'ERE.ERE' to 'RE.RE':
--
-- >>> putPretty $ toRE $ fromERE $ complement $ star "ab"
-- ^([^]|a(ba)*(ba)?|a(ba)*([^b]|b[^a])|([^a]|a(ba)*([^b]|b[^a]))[^]*[^]?)$
--
-- >>> putPretty $ toRE $ fromERE $ "a" /\ "b"
-- ^[]$
--
-- See <https://mathoverflow.net/questions/45149/can-regular-expressions-be-made-unambiguous>
-- for the description of the algorithm used.
--
toRE :: (Ord c, Enum c, Bounded c) => DFA c -> RE.RE c
toRE :: forall c. (Ord c, Enum c, Bounded c) => DFA c -> RE c
toRE = DFA c -> RE c
forall k c.
(Ord c, Enum c, Bounded c, FiniteKleene c k) =>
DFA c -> k
toKleene

-- | Convert 'DFA' to 'ERE.ERE'.
toERE :: (Ord c, Enum c, Bounded c) => DFA c -> ERE.ERE c
toERE :: forall c. (Ord c, Enum c, Bounded c) => DFA c -> ERE c
toERE = DFA c -> ERE c
forall k c.
(Ord c, Enum c, Bounded c, FiniteKleene c k) =>
DFA c -> k
toKleene

-- | Convert to any 'Kleene'.
--
-- See 'toRE' for a specific example.
--
toKleene :: forall k c. (Ord c, Enum c, Bounded c, FiniteKleene c k) => DFA c -> k
toKleene :: forall k c.
(Ord c, Enum c, Bounded c, FiniteKleene c k) =>
DFA c -> k
toKleene (DFA IntMap (SF c Int)
tr Int
ini IntSet
acc IntSet
_) = [k] -> k
forall k. Kleene k => [k] -> k
unions
    [ Int -> Int -> Int -> k
re Int
ini Int
j Int
maxN
    | Int
j <- IntSet -> [Int]
IntSet.toList IntSet
acc
    ]
  where
    maxN :: Int
maxN | IntMap (SF c Int) -> Bool
forall a. IntMap a -> Bool
IntMap.null IntMap (SF c Int)
tr = Int
1
         | Bool
otherwise      = Int -> Int
forall a. Enum a => a -> a
succ (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ (Int, SF c Int) -> Int
forall a b. (a, b) -> a
fst ((Int, SF c Int) -> Int) -> (Int, SF c Int) -> Int
forall a b. (a -> b) -> a -> b
$ IntMap (SF c Int) -> (Int, SF c Int)
forall a. IntMap a -> (Int, a)
IntMap.findMax IntMap (SF c Int)
tr

    {-
    -- this is useful for debug
    table =
      [ show i ++ " " ++ show j ++ " " ++ show k ++ " = " ++ pretty (re i j k)
      | k <- [0..pred maxN]
      , i <- [0..pred maxN]
      , j <- [0..pred maxN]
      ]
    -}

    re :: Int -> Int -> Int -> k
re Int
i Int
j Int
k = ((Int, Int, Int) -> k) -> (Int, Int, Int) -> k
forall t a. HasTrie t => (t -> a) -> t -> a
MT.memo (Int, Int, Int) -> k
re' (Int
i, Int
j, Int
k)
    re' :: (Int, Int, Int) -> k
re' (Int
i, Int
j, Int
k)
        | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0    = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j then [k] -> k
forall k. Kleene k => [k] -> k
unions [k
forall k. Kleene k => k
eps, k
r] else k
r
        | Bool
otherwise = [k] -> k
forall k. Kleene k => [k] -> k
unions [Int -> Int -> Int -> k
re Int
i Int
j Int
k', [k] -> k
forall k. Kleene k => [k] -> k
appends [Int -> Int -> Int -> k
re Int
i Int
k' Int
k', k -> k
forall k. Kleene k => k -> k
star (Int -> Int -> Int -> k
re Int
k' Int
k' Int
k'), Int -> Int -> Int -> k
re Int
k' Int
j Int
k']]
      where
        r :: k
r = k -> (RSet c -> k) -> Maybe (RSet c) -> k
forall b a. b -> (a -> b) -> Maybe a -> b
maybe k
forall k. Kleene k => k
empty RSet c -> k
forall c k. FiniteKleene c k => RSet c -> k
fromRSet (Maybe (RSet c) -> k) -> Maybe (RSet c) -> k
forall a b. (a -> b) -> a -> b
$ (Int, Int) -> Map (Int, Int) (RSet c) -> Maybe (RSet c)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Int
i, Int
j) Map (Int, Int) (RSet c)
re0map
        k' :: Int
k' = Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1

    re0map :: Map (Int, Int) (RSet c)
    re0map :: Map (Int, Int) (RSet c)
re0map = (RSet c -> RSet c -> RSet c)
-> [((Int, Int), RSet c)] -> Map (Int, Int) (RSet c)
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith RSet c -> RSet c -> RSet c
forall a. (Ord a, Enum a) => RSet a -> RSet a -> RSet a
RSet.union
        [ ((Int
i, Int
j), (c, c) -> RSet c
forall a. Ord a => (a, a) -> RSet a
RSet.singletonRange (c
lo, c
hi))
        | (Int
i, SF c Int
tr') <- IntMap (SF c Int) -> [(Int, SF c Int)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (SF c Int)
tr
        , (c
lo, c
hi, Int
j) <- SF c Int -> [(c, c, Int)]
forall a b. (Enum a, Bounded a, Ord a) => SF a b -> [(a, a, b)]
toPieces SF c Int
tr'
        ]

toPieces :: (Enum a, Bounded a, Ord a) => SF.SF a b -> [(a, a, b)]
toPieces :: forall a b. (Enum a, Bounded a, Ord a) => SF a b -> [(a, a, b)]
toPieces (SF.SF Map a b
m b
v)
    | a
forall a. Bounded a => a
maxBound a -> Map a b -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map a b
m = Map a b -> [(a, a, b)]
forall a b. (Enum a, Bounded a) => Map a b -> [(a, a, b)]
toPieces' Map a b
m
    | Bool
otherwise               = Map a b -> [(a, a, b)]
forall a b. (Enum a, Bounded a) => Map a b -> [(a, a, b)]
toPieces' (a -> b -> Map a b -> Map a b
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert a
forall a. Bounded a => a
maxBound b
v Map a b
m)

toPieces' :: (Enum a, Bounded a) => Map a b -> [(a, a, b)]
toPieces' :: forall a b. (Enum a, Bounded a) => Map a b -> [(a, a, b)]
toPieces' = a -> [(a, b)] -> [(a, a, b)]
forall {t} {c}. Enum t => t -> [(t, c)] -> [(t, t, c)]
go a
forall a. Bounded a => a
minBound ([(a, b)] -> [(a, a, b)])
-> (Map a b -> [(a, b)]) -> Map a b -> [(a, a, b)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map a b -> [(a, b)]
forall k a. Map k a -> [(k, a)]
Map.toList where
    go :: t -> [(t, c)] -> [(t, t, c)]
go t
_lo []            = []
    go  t
lo ((t
k, c
v) : [(t, c)]
kv) = (t
lo, t
k, c
v) (t, t, c) -> [(t, t, c)] -> [(t, t, c)]
forall a. a -> [a] -> [a]
: t -> [(t, c)] -> [(t, t, c)]
go (t -> t
forall a. Enum a => a -> a
succ t
k) [(t, c)]
kv

-------------------------------------------------------------------------------
-- Operations
-------------------------------------------------------------------------------

-- | Run 'DFA' on the input.
--
-- Because we have analysed a language, in some cases we can determine a result
-- without traversing all of the input.
-- That's not the cases with 'RE.RE' 'match'.
--
-- >>> let dfa = fromRE $ RE.star "abc"
-- >>> map (match dfa) ["", "abc", "abcabc", "aa", 'a' : 'a' : undefined]
-- [True,True,True,False,False]
--
-- Holds:
--
-- @
-- 'match' ('fromRE' re) xs == 'match' re xs
-- @
--
-- prop> all (match (fromRE r)) $ take 10 $ RE.generate (curry QC.choose) 42 (r :: RE.RE Char)
--
instance Ord c => Match c (DFA c) where
    match :: DFA c -> [c] -> Bool
match (DFA IntMap (SF c Int)
tr Int
i IntSet
acc IntSet
bh) = Int -> [c] -> Bool
go Int
i where
        go :: Int -> [c] -> Bool
go !Int
s [c]
_ | Int -> IntSet -> Bool
IntSet.member Int
s IntSet
bh = Int -> IntSet -> Bool
IntSet.member Int
s IntSet
acc
        go !Int
s []                 = Int -> IntSet -> Bool
IntSet.member Int
s IntSet
acc
        go !Int
s (c
c : [c]
cs)           = case Int -> IntMap (SF c Int) -> Maybe (SF c Int)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
s IntMap (SF c Int)
tr of
            Maybe (SF c Int)
Nothing -> Bool
False
            Just SF c Int
sf -> Int -> [c] -> Bool
go (SF c Int
sf SF c Int -> c -> Int
forall k v. Ord k => SF k v -> k -> v
SF.! c
c) [c]
cs

    match8 :: (c ~ Word8) => DFA c -> ByteString -> Bool
match8 (DFA IntMap (SF c Int)
tr Int
i IntSet
acc IntSet
bh) = Int -> ByteString -> Bool
go Int
i where
        go :: Int -> ByteString -> Bool
go !Int
s !ByteString
_ | Int -> IntSet -> Bool
IntSet.member Int
s IntSet
bh = Int -> IntSet -> Bool
IntSet.member Int
s IntSet
acc
        go !Int
s ByteString
bs = case ByteString -> Maybe (Word8, ByteString)
BS.uncons ByteString
bs of
            Maybe (Word8, ByteString)
Nothing      -> Int -> IntSet -> Bool
IntSet.member Int
s IntSet
acc
            Just (Word8
c, ByteString
cs) -> case Int -> IntMap (SF c Int) -> Maybe (SF c Int)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
s IntMap (SF c Int)
tr of
                Maybe (SF c Int)
Nothing -> Bool
False
                Just SF c Int
sf -> Int -> ByteString -> Bool
go (SF c Int
sf SF c Int -> c -> Int
forall k v. Ord k => SF k v -> k -> v
SF.! c
Word8
c) ByteString
cs

-- | Complement DFA.
--
-- Complement of 'DFA' is way easier than of 'RE.RE': complement accept states.
--
-- >>> let dfa = complement $ fromRE $ RE.star "abc"
-- >>> putPretty dfa
-- 0 -> \x -> if
--     | x <= '`'  -> 3
--     | x <= 'a'  -> 2
--     | otherwise -> 3
-- 1+ -> \x -> if
--     | x <= 'b'  -> 3
--     | x <= 'c'  -> 0
--     | otherwise -> 3
-- 2+ -> \x -> if
--     | x <= 'a'  -> 3
--     | x <= 'b'  -> 1
--     | otherwise -> 3
-- 3+ -> \_ -> 3 -- black hole
--
-- >>> map (match dfa) ["", "abc", "abcabc", "aa","abca", 'a' : 'a' : undefined]
-- [False,False,False,True,True,True]
--
instance Complement c (DFA c) where
    complement :: DFA c -> DFA c
complement (DFA IntMap (SF c Int)
tr Int
ini IntSet
acc IntSet
bh) = IntMap (SF c Int) -> Int -> IntSet -> IntSet -> DFA c
forall c. IntMap (SF c Int) -> Int -> IntSet -> IntSet -> DFA c
DFA IntMap (SF c Int)
tr Int
ini IntSet
acc' IntSet
bh where
        acc' :: IntSet
acc' = IntSet -> IntSet -> IntSet
IntSet.difference (IntMap (SF c Int) -> IntSet
forall a. IntMap a -> IntSet
IntMap.keysSet IntMap (SF c Int)
tr) IntSet
acc

instance Ord c => Derivate c (DFA c) where
    nullable :: DFA c -> Bool
nullable (DFA IntMap (SF c Int)
_tr Int
ini IntSet
acc IntSet
_bh) = Int -> IntSet -> Bool
IntSet.member Int
ini IntSet
acc

    derivate :: c -> DFA c -> DFA c
derivate c
c (DFA IntMap (SF c Int)
tr Int
ini IntSet
acc IntSet
bh) = IntMap (SF c Int) -> Int -> IntSet -> IntSet -> DFA c
forall c. IntMap (SF c Int) -> Int -> IntSet -> IntSet -> DFA c
DFA IntMap (SF c Int)
tr Int
ini' IntSet
acc IntSet
bh where
        ini' :: Int
ini' = case Int -> IntMap (SF c Int) -> Maybe (SF c Int)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
ini IntMap (SF c Int)
tr of
            Maybe (SF c Int)
Nothing -> Int
ini -- in error case let's just stay in the same state.
            Just SF c Int
sf -> SF c Int
sf SF c Int -> c -> Int
forall k v. Ord k => SF k v -> k -> v
SF.! c
c

-------------------------------------------------------------------------------
-- toDot
-------------------------------------------------------------------------------

-- | Get Graphviz dot-code of DFA.
--
-- >>> let dfa = fromRE $ RE.star "abc"
-- >>> putStr $ toDot dfa
-- digraph dfa {
-- rankdir=LR;
-- // states
-- "0" [shape=doublecircle];
-- "1" [shape=circle];
-- "2" [shape=circle];
-- // initial state
-- "" [shape=none];
-- "" -> "0";
-- // transitions
-- "0" -> "2"[label="a"]
-- "1" -> "0"[label="c"]
-- "2" -> "1"[label="b"]
-- }
--
toDot :: DFA Char -> String
toDot :: DFA Char -> String
toDot = (Int -> String) -> (Char -> String) -> DFA Char -> String
forall c.
(Ord c, Enum c, Bounded c) =>
(Int -> String) -> (c -> String) -> DFA c -> String
toDot' Int -> String
forall a. Show a => a -> String
show Char -> String
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- | More flexible version of 'toDot'.
toDot' :: (Ord c, Enum c, Bounded c) => (Int -> String) -> (c -> String) -> DFA c -> String
toDot' :: forall c.
(Ord c, Enum c, Bounded c) =>
(Int -> String) -> (c -> String) -> DFA c -> String
toDot' Int -> String
showS c -> String
showC (DFA IntMap (SF c Int)
tr Int
ini IntSet
acc IntSet
bh)
    = String -> ShowS
showString String
"digraph dfa {\n"
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
"rankdir=LR;\n"
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
"// states\n"
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
showStates
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
"// initial state\n"
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
showInitial
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
"// transitions\n"
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
showTransitions
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
"}\n"
    ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
""
  where
    showStates :: ShowS
showStates  = (ShowS -> ShowS -> ShowS) -> ShowS -> [ShowS] -> ShowS
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) ShowS
forall a. a -> a
id
        [ Int -> ShowS
showState Int
i
        | Int
i <- IntMap (SF c Int) -> [Int]
forall a. IntMap a -> [Int]
IntMap.keys IntMap (SF c Int)
tr
        , Int -> IntSet -> Bool
IntSet.member Int
i IntSet
acc Bool -> Bool -> Bool
|| Int -> IntSet -> Bool
IntSet.notMember Int
i IntSet
bh
        ]
    showState :: Int -> ShowS
showState Int
s = Int -> ShowS
showS' Int
s ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
shape where
        shape :: ShowS
shape
            | Int -> IntSet -> Bool
IntSet.member Int
s IntSet
acc = String -> ShowS
showString String
" [shape=doublecircle];\n"
            | Bool
otherwise        = String -> ShowS
showString String
" [shape=circle];\n"

    showInitial :: ShowS
showInitial
        = String -> ShowS
showString String
"\"\" [shape=none];\n"
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
"\"\" -> "
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ShowS
showS' Int
ini
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
";\n"

    showTransitions :: ShowS
showTransitions = (ShowS -> ShowS -> ShowS) -> ShowS -> [ShowS] -> ShowS
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) ShowS
forall a. a -> a
id
        [ Int -> ShowS
showS' Int
i
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" -> "
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ShowS
showS' Int
j
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
"[label="
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
label
                ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
"]\n"
        | (Int
i, SF c Int
sf) <- IntMap (SF c Int) -> [(Int, SF c Int)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (SF c Int)
tr
        , (c
lo, c
hi, Int
j) <- SF c Int -> [(c, c, Int)]
forall a b. (Enum a, Bounded a, Ord a) => SF a b -> [(a, a, b)]
toPieces SF c Int
sf
        , Int -> IntSet -> Bool
IntSet.member Int
j IntSet
acc Bool -> Bool -> Bool
|| Int -> IntSet -> Bool
IntSet.notMember Int
j IntSet
bh
        , let label :: ShowS
label
                | c
lo c -> c -> Bool
forall a. Eq a => a -> a -> Bool
== c
hi
                    = String -> ShowS
forall a. Show a => a -> ShowS
shows (c -> String
showC c
lo)
                | c
lo c -> c -> Bool
forall a. Eq a => a -> a -> Bool
== c
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&& c
hi c -> c -> Bool
forall a. Eq a => a -> a -> Bool
== c
forall a. Bounded a => a
maxBound
                    = String -> ShowS
forall a. Show a => a -> ShowS
shows (String
"-any" :: String)
                | Bool
otherwise
                    = String -> ShowS
forall a. Show a => a -> ShowS
shows (c -> String
showC c
lo String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"-" String -> ShowS
forall a. [a] -> [a] -> [a]
++ c -> String
showC c
hi)
        ]

    showS' :: Int -> ShowS
showS' = String -> ShowS
forall a. Show a => a -> ShowS
shows (String -> ShowS) -> (Int -> String) -> Int -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
showS

-------------------------------------------------------------------------------
-- Orphans
-------------------------------------------------------------------------------

-- | __WARNING__: The '/\' is inefficient, it actually computes the conjunction:
--
-- >>> putPretty $ asREChar $ "a" /\ "b"
-- ^[]$
--
-- >>> putPretty $ asREChar $ "a" /\ star "a"
-- ^a$
--
-- >>> putPretty $ asREChar $ star "aa" /\ star "aaa"
-- ^(a(aaaaaa)*aaaaa)?$
--
instance (Ord c, Enum c, Bounded c) => Lattice (RE.RE c) where
    RE c
r /\ :: RE c -> RE c -> RE c
/\ RE c
r' = DFA c -> RE c
forall c. (Ord c, Enum c, Bounded c) => DFA c -> RE c
toRE (DFA c -> RE c) -> DFA c -> RE c
forall a b. (a -> b) -> a -> b
$ ERE c -> DFA c
forall c. (Ord c, Enum c, Bounded c) => ERE c -> DFA c
fromERE (ERE c -> DFA c) -> ERE c -> DFA c
forall a b. (a -> b) -> a -> b
$ RE c -> ERE c
forall c. Ord c => RE c -> ERE c
ERE.fromRE RE c
r ERE c -> ERE c -> ERE c
forall a. Lattice a => a -> a -> a
/\ RE c -> ERE c
forall c. Ord c => RE c -> ERE c
ERE.fromRE RE c
r'
    RE c
r \/ :: RE c -> RE c -> RE c
\/ RE c
r' = [RE c] -> RE c
forall k. Kleene k => [k] -> k
unions [RE c
r, RE c
r']

instance (Ord c, Enum c, Bounded c) => BoundedJoinSemiLattice (RE.RE c) where
    bottom :: RE c
bottom = RE c
forall k. Kleene k => k
empty

instance (Ord c, Enum c, Bounded c) => BoundedMeetSemiLattice (RE.RE c) where
    top :: RE c
top = RE c -> RE c
forall c. RE c -> RE c
RE.REStar (RSet c -> RE c
forall c. RSet c -> RE c
RE.REChars RSet c
forall a. Bounded a => RSet a
RSet.full)

instance (Ord c, Enum c, Bounded c) => Complement c (RE.RE c) where
    complement :: RE c -> RE c
complement = DFA c -> RE c
forall c. (Ord c, Enum c, Bounded c) => DFA c -> RE c
toRE (DFA c -> RE c) -> (RE c -> DFA c) -> RE c -> RE c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DFA c -> DFA c
forall c k. Complement c k => k -> k
complement (DFA c -> DFA c) -> (RE c -> DFA c) -> RE c -> DFA c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RE c -> DFA c
forall c. (Ord c, Enum c, Bounded c) => RE c -> DFA c
fromRE

-------------------------------------------------------------------------------
-- Debug
-------------------------------------------------------------------------------

instance Show c => Pretty (DFA c) where
    pretty :: DFA c -> String
pretty DFA c
dfa = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n"
        [ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
acc String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SF c Int -> String
forall a b. (Show a, Show b) => SF a b -> String
SF.showSF SF c Int
sf String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
bh
        | (Int
i, SF c Int
sf) <- IntMap (SF c Int) -> [(Int, SF c Int)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList (DFA c -> IntMap (SF c Int)
forall c. DFA c -> IntMap (SF c Int)
dfaTransition DFA c
dfa)
        , let acc :: String
acc = if Int -> IntSet -> Bool
IntSet.member Int
i (DFA c -> IntSet
forall c. DFA c -> IntSet
dfaAcceptable DFA c
dfa) then String
"+" else String
""
        , let bh :: String
bh = if Int -> IntSet -> Bool
IntSet.member Int
i (IntSet -> Bool) -> IntSet -> Bool
forall a b. (a -> b) -> a -> b
$ DFA c -> IntSet
forall c. DFA c -> IntSet
dfaBlackholes DFA c
dfa then String
" -- black hole" else String
""
        ]