automata (empty) → 0.1.0.0

raw patch · 13 files changed

+1828/−0 lines, 13 filesdep +HUnitdep +QuickCheckdep +automatasetup-changed

Dependencies added: HUnit, QuickCheck, automata, base, bytestring, containers, contiguous, enum-types, leancheck, leancheck-enum-instances, primitive, primitive-containers, quickcheck-classes, quickcheck-enum-instances, semirings, tasty, tasty-hunit, tasty-leancheck, tasty-quickcheck, transformers

Files

ChangeLog.md +3/−0
LICENSE +30/−0
README.md +1/−0
Setup.hs +2/−0
automata.cabal +76/−0
src/Automata/Dfsa.hs +116/−0
src/Automata/Dfst.hs +190/−0
src/Automata/Internal.hs +443/−0
src/Automata/Internal/Transducer.hs +108/−0
src/Automata/Nfsa.hs +63/−0
src/Automata/Nfsa/Builder.hs +111/−0
src/Automata/Nfst.hs +218/−0
test/Main.hs +467/−0

+ ChangeLog.md view

@@ -0,0 +1,3 @@+# Changelog for automaton++## Unreleased changes

+ LICENSE view

@@ -0,0 +1,30 @@+Copyright Andrew Martin (c) 2018++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Andrew Martin nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

+ README.md view

@@ -0,0 +1,1 @@+# automaton

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ automata.cabal view

@@ -0,0 +1,76 @@+cabal-version: 2.2+name: automata+version: 0.1.0.0+synopsis: automata+description:+  This package implements the following:+  .+  Deterministic Finite State Automata (DFSA)+  .+  Non-Deterministic Finite State Automata (NFSA)+  .+  Deterministic Finite State Transducers (DFST)+  .+  Non-Deterministic Finite State Transducers (NFST)+category: Data, Math+homepage: https://github.com/andrewthad/automata+bug-reports: https://github.com/andrewthad/automata/issues+author: Andrew Martin+maintainer: andrew.thaddeus@gmail.com+copyright: 2018 Andrew Martin+license: BSD-3-Clause+license-file: LICENSE+build-type: Simple+extra-source-files:+  ChangeLog.md+  README.md++source-repository head+  type: git+  location: https://github.com/andrewthad/automata++library+  hs-source-dirs: src+  exposed-modules:+    Automata.Dfsa+    Automata.Nfsa+    Automata.Nfsa.Builder+    Automata.Internal+    Automata.Internal.Transducer+    Automata.Nfst+    Automata.Dfst+  build-depends:+    , base >=4.10.1.0 && <5+    , bytestring >= 0.10.8+    , primitive >= 0.6.4+    , primitive-containers >= 0.3+    , containers >= 0.5.9+    , contiguous+    , semirings >= 0.3.1.1+    , transformers+  ghc-options: -O2+  default-language: Haskell2010++test-suite test+  type: exitcode-stdio-1.0+  main-is: Main.hs+  hs-source-dirs:+      test+  ghc-options: -threaded -rtsopts -with-rtsopts=-N -O2+  build-depends:+    , HUnit+    , QuickCheck+    , automata+    , base >=4.7 && <5+    , containers+    , enum-types >= 0.1+    , leancheck+    , leancheck-enum-instances >= 0.1+    , primitive+    , quickcheck-classes+    , quickcheck-enum-instances >= 0.1+    , tasty+    , tasty-hunit+    , tasty-leancheck+    , tasty-quickcheck+  default-language: Haskell2010

+ src/Automata/Dfsa.hs view

@@ -0,0 +1,116 @@+{-# language BangPatterns #-}+{-# language DeriveFunctor #-}+{-# language DerivingStrategies #-}+{-# language MagicHash #-}+{-# language RankNTypes #-}+{-# language ScopedTypeVariables #-}+{-# language UnboxedTuples #-}++module Automata.Dfsa+  ( -- * Static+    -- ** Types+    Dfsa+    -- ** Evaluation+  , evaluate+    -- ** Composition+  , union+  , intersection+    -- ** Special DFA+  , acceptance+  , rejection+    -- * Builder+    -- ** Types+  , Builder+  , State+    -- ** Functions+  , build+  , state+  , transition+  , accept+  ) where++import Automata.Internal (Dfsa(..),State(..),union,intersection,acceptance,rejection,minimize)+import Data.Foldable (foldl',for_)+import Data.Primitive (Array)+import Data.Semigroup (Last(..))+import Control.Monad.ST (runST)++import qualified Data.Primitive.Contiguous as C+import qualified Data.Map.Interval.DBTSLL as DM+import qualified Data.Set.Unboxed as SU++-- | Evaluate a foldable collection of tokens against the DFA. This+-- returns true if the string is accepted by the language.+evaluate :: (Foldable f, Ord t) => Dfsa t -> f t -> Bool+evaluate (Dfsa transitions finals) tokens = SU.member+  (foldl' (\(active :: Int) token -> DM.lookup token (C.index transitions active)) 0 tokens)+  finals++newtype Builder t s a = Builder (Int -> [Edge t] -> [Int] -> Result t a)+  deriving stock (Functor)++instance Applicative (Builder t s) where+  pure a = Builder (\i es fs -> Result i es fs a)+  Builder f <*> Builder g = Builder $ \i es fs -> case f i es fs of+    Result i' es' fs' x -> case g i' es' fs' of+      Result i'' es'' fs'' y -> Result i'' es'' fs'' (x y)++instance Monad (Builder t s) where+  Builder f >>= g = Builder $ \i es fs -> case f i es fs of+    Result i' es' fs' a -> case g a of+      Builder g' -> g' i' es' fs'++data Result t a = Result !Int ![Edge t] ![Int] a+  deriving stock (Functor)++data Edge t = Edge !Int !Int !t !t++data EdgeDest t = EdgeDest !Int t t++-- | The argument function takes a start state and builds an NFA. This+-- function will execute the builder.+build :: forall t a. (Bounded t, Ord t, Enum t) => (forall s. State s -> Builder t s a) -> Dfsa t+build fromStartState =+  case state >>= fromStartState of+    Builder f -> case f 0 [] [] of+      Result totalStates edges final _ ->+        let ts = runST $ do+              transitions <- C.replicateM totalStates (DM.pure Nothing)+              outbounds <- C.replicateM totalStates []+              for_ edges $ \(Edge source destination lo hi) -> do+                edgeDests0 <- C.read outbounds source+                let !edgeDests1 = EdgeDest destination lo hi : edgeDests0+                C.write outbounds source edgeDests1+              (outbounds' :: Array [EdgeDest t]) <- C.unsafeFreeze outbounds+              flip C.imapMutable' transitions $ \i _ ->+                let dests = C.index outbounds' i+                 in mconcat+                      ( map+                        (\(EdgeDest dest lo hi) -> DM.singleton Nothing lo hi (Just (Last dest)))+                        dests+                      )+              C.unsafeFreeze transitions+         in minimize (fmap (DM.map (maybe 0 getLast)) ts) (SU.fromList final)+  +-- | Generate a new state in the NFA. On any input, the state transitions to+--   the start state.+state :: Builder t s (State s)+state = Builder $ \i edges final ->+  Result (i + 1) edges final (State i)++-- | Mark a state as being an accepting state. +accept :: State s -> Builder t s ()+accept (State n) = Builder $ \i edges final -> Result i edges (n : final) ()++-- | Add a transition from one state to another when the input token+--   is inside the inclusive range. If multiple transitions from+--   a state are given, the last one given wins.+transition ::+     t -- ^ inclusive lower bound+  -> t -- ^ inclusive upper bound+  -> State s -- ^ from state+  -> State s -- ^ to state+  -> Builder t s ()+transition lo hi (State source) (State dest) =+  Builder $ \i edges final -> Result i (Edge source dest lo hi : edges) final ()+

+ src/Automata/Dfst.hs view

@@ -0,0 +1,190 @@+{-# language BangPatterns #-}+{-# language DeriveFunctor #-}+{-# language DerivingStrategies #-}+{-# language MagicHash #-}+{-# language RankNTypes #-}+{-# language ScopedTypeVariables #-}+{-# language UnboxedTuples #-}++module Automata.Dfst+  ( -- * Static+    -- ** Types+    Dfst+    -- ** Functions+  , evaluate+  , evaluateAscii+  , union+  , map+    -- ** Special Transducers+  , rejection+    -- * Builder+    -- ** Types+  , Builder+  , State+    -- ** Functions+  , build+  , state+  , transition+  , accept+  ) where++import Prelude hiding (map)++import Automata.Internal (State(..),Dfsa(..),composeMapping)+import Automata.Internal.Transducer (Dfst(..),MotionDfst(..),Edge(..),EdgeDest(..))+import Control.Monad.ST (runST)+import Data.Foldable (foldl',for_)+import Data.Map.Strict (Map)+import Data.Maybe (fromMaybe)+import Data.Primitive (Array,indexArray)+import Data.Semigroup (Last(..))+import Data.Set (Set)+import Data.ByteString (ByteString)++import qualified Data.ByteString.Char8 as BC+import qualified Data.List as L+import qualified Data.Map.Interval.DBTSLL as DM+import qualified Data.Map.Strict as M+import qualified Data.Primitive.Contiguous as C+import qualified Data.Set as S+import qualified Data.Set.Unboxed as SU+import qualified GHC.Exts as E++-- | Map over the output tokens.+map :: Eq n => (m -> n) -> Dfst t m -> Dfst t n+map f (Dfst t m) =+  -- Revisit this implementation if we ever start supporting the canonization+  -- and minimization of DFST.+  Dfst (fmap (DM.map (\(MotionDfst s x) -> MotionDfst s (f x))) t) m++-- | Rejects all input, producing the monoidal identity as its output.+rejection :: (Bounded t, Monoid m) => Dfst t m+rejection = Dfst (C.singleton (DM.pure (MotionDfst 0 mempty))) SU.empty++union :: forall t m. (Ord t, Bounded t, Enum t, Monoid m) => Dfst t m -> Dfst t m -> Dfst t m+union a@(Dfst ax _) b@(Dfst bx _) =+  let (mapping, Dfsa t0 f) = composeMapping (||) (unsafeToDfsa a) (unsafeToDfsa b)+      -- The revMapping goes from a new state to all a-b old state pairs.+      revMapping :: Map Int (Set (Int,Int))+      revMapping = M.foldlWithKey' (\acc k v -> M.insertWith (<>) v (S.singleton k) acc) M.empty mapping+      t1 :: Array (DM.Map t (MotionDfst m))+      t1 = C.imap+        (\source m -> DM.mapBijection+          (\dest ->+            let oldSources = fromMaybe (error "Automata.Nfst.toDfst: missing old source") (M.lookup source revMapping)+                oldDests = fromMaybe (error "Automata.Nfst.toDfst: missing old dest") (M.lookup dest revMapping)+                -- Do we need to deal with epsilon stuff in here? I don't think so.+                newOutput = foldMap+                  (\(oldSourceA,oldSourceB) -> mconcat $ E.toList $ do+                    MotionDfst oldDestA outA <- DM.elems (indexArray ax oldSourceA)+                    MotionDfst oldDestB outB <- DM.elems (indexArray bx oldSourceB)+                    if S.member (oldDestA,oldDestB) oldDests then pure (outA <> outB) else mempty+                  ) oldSources+             in MotionDfst dest newOutput+          ) m+        ) t0+   in Dfst t1 f++-- | Returns @Nothing@ if the transducer did not end up in an+--   accepting state. Returns @Just@ if it did. The array of+--   output tokens always matches the length of the input.+evaluate :: (Foldable f, Ord t) => Dfst t m -> f t -> Maybe (Array m)+evaluate (Dfst transitions finals) tokens =+  let !(!finalState,!totalSize,!allOutput) = foldl'+        (\(!active,!sz,!output) token ->+          let MotionDfst nextState outputToken = DM.lookup token (indexArray transitions active)+           in (nextState,sz + 1,outputToken : output)+        ) (0,0,[]) tokens+   in if SU.member finalState finals+        then Just (C.unsafeFromListReverseN totalSize allOutput)+        else Nothing++evaluateAscii :: forall m. Ord m => Dfst Char m -> ByteString -> Maybe (Array m)+evaluateAscii (Dfst transitions finals) !tokens =+  let !(!finalState,!allOutput) = BC.foldl'+        (\(!active,!output) token ->+          let MotionDfst nextState outputToken = DM.lookup token (indexArray transitions active)+           in (nextState,outputToken : output)+        ) (0,[]) tokens+   in if SU.member finalState finals+        then Just (C.unsafeFromListReverseN (BC.length tokens) allOutput)+        else Nothing++newtype Builder t m s a = Builder (Int -> [Edge t m] -> [Int] -> Result t m a)+  deriving stock (Functor)++data Result t m a = Result !Int ![Edge t m] ![Int] a+  deriving stock (Functor)++instance Applicative (Builder t m s) where+  pure a = Builder (\i es fs -> Result i es fs a)+  Builder f <*> Builder g = Builder $ \i es fs -> case f i es fs of+    Result i' es' fs' x -> case g i' es' fs' of+      Result i'' es'' fs'' y -> Result i'' es'' fs'' (x y)++instance Monad (Builder t m s) where+  Builder f >>= g = Builder $ \i es fs -> case f i es fs of+    Result i' es' fs' a -> case g a of+      Builder g' -> g' i' es' fs'++-- | Generate a new state in the NFA. On any input, the state transitions to+--   the start state.+state :: Builder t m s (State s)+state = Builder $ \i edges final ->+  Result (i + 1) edges final (State i)++-- | Mark a state as being an accepting state. +accept :: State s -> Builder t m s ()+accept (State n) = Builder $ \i edges final -> Result i edges (n : final) ()++-- | Add a transition from one state to another when the input token+--   is inside the inclusive range. If multiple transitions from+--   a state are given, the last one given wins.+transition ::+     t -- ^ inclusive lower bound+  -> t -- ^ inclusive upper bound+  -> m -- ^ output token+  -> State s -- ^ from state+  -> State s -- ^ to state+  -> Builder t m s ()+transition lo hi output (State source) (State dest) =+  Builder $ \i edges final -> Result i (Edge source dest lo hi output : edges) final ()++-- | The argument function turns a start state into an NFST builder. This+-- function converts the builder to a usable transducer.+build :: forall t m a. (Bounded t, Ord t, Enum t, Monoid m, Ord m) => (forall s. State s -> Builder t m s a) -> Dfst t m+build fromStartState =+  case state >>= fromStartState of+    Builder f -> case f 0 [] [] of+      Result totalStates edges final _ ->+        let ts0 = runST $ do+              transitions <- C.replicateM totalStates (DM.pure Nothing)+              outbounds <- C.replicateM totalStates []+              for_ edges $ \(Edge source destination lo hi output) -> do+                edgeDests0 <- C.read outbounds source+                let !edgeDests1 = EdgeDest destination lo hi output : edgeDests0+                C.write outbounds source edgeDests1+              (outbounds' :: Array [EdgeDest t m]) <- C.unsafeFreeze outbounds+              flip C.imapMutable' transitions $ \i _ -> +                let dests = C.index outbounds' i+                 in mconcat+                      ( L.map+                        (\(EdgeDest dest lo hi output) ->+                          DM.singleton mempty lo hi (Just (Last (MotionDfst dest output)))+                        )+                        dests+                      )+              C.unsafeFreeze transitions+         in Dfst (fmap (DM.map (maybe (MotionDfst 0 mempty) getLast)) ts0) (SU.fromList final)++-- collapse :: Dfst t m -> Dfst t m+-- collapse = MotionDfst ++-- Convert a DFST to a DFSA. However, the DFSA is not necessarily minimal, so+-- equality on it is incorrect. Its states have a one-to-one mapping with the+-- states on the DFST.+unsafeToDfsa :: Dfst t m -> Dfsa t+unsafeToDfsa (Dfst t f) = Dfsa (fmap (DM.map motionDfstState) t) f+++

+ src/Automata/Internal.hs view

@@ -0,0 +1,443 @@+{-# language BangPatterns #-}+{-# language LambdaCase #-}+{-# language MagicHash #-}+{-# language UnboxedTuples #-}+{-# language ScopedTypeVariables #-}++module Automata.Internal+  ( -- * Types+    Dfsa(..)+  , Nfsa(..)+  , TransitionNfsa(..)+    -- * Builder Types+  , State(..)+  , Epsilon(..)+    -- * NFA Functions +  , toDfsa+  , toDfsaMapping+  , append+  , empty+  , rejectionNfsa+  , unionNfsa+  , epsilonClosure+    -- * DFA Functions+  , union+  , intersection+  , acceptance+  , rejection+  , minimize+  , minimizeMapping+  , composeMapping+  ) where++import Control.Applicative (liftA2)+import Control.Monad (forM_,(<=<))+import Control.Monad.ST (runST)+import Data.Foldable (foldl',toList)+import Data.Map (Map)+import Data.Maybe (fromMaybe,isNothing,mapMaybe)+import Data.Primitive (Array,indexArray)+import Data.Semigroup (First(..))+import Data.Semiring (Semiring)+import Data.Set (Set)++import Debug.Trace++import qualified Data.List as L+import qualified Data.Set as S+import qualified Data.Set.Unboxed as SU+import qualified Data.Map.Strict as M+import qualified Control.Monad.Trans.State.Strict as State+import qualified Data.Map.Interval.DBTSLL as DM+import qualified Data.Map.Unboxed.Lifted as MUL+import qualified Data.Primitive.Contiguous as C+import qualified Data.Primitive as PM+import qualified Data.Map.Lifted.Lifted as MLL+import qualified GHC.Exts as E+import qualified Data.Semiring++-- | Deterministic Finite State Automaton.+--+-- The start state is always zero.+data Dfsa t = Dfsa+  { dfaTransition :: !(Array (DM.Map t Int))+    -- ^ Given a state and transition, this field tells you what+    --   state to go to next. The length of this array must match+    --   the total number of states.+  , dfaFinal :: !(SU.Set Int)+    -- ^ A string that ends in any of these set of states is+    --   considered to have been accepted by the grammar.+  } deriving (Eq,Show)++-- | Non-Deterministic Finite State Automaton.+--+-- Some notes on the implementation and design:+--+-- * You can transition to any non-negative number of states (including 0).+-- * There is only one start state.+-- * We use the Thompson encoding. This means that there is an epsilon+--   transition that consumes no input.+-- * We store the full epsilon closure for every state. This means that,+--   when evaluating the NFA, we do not ever need to compute the closure.+-- * There is no Eq instance for NFA. In general, this can take exponential+--   time. If you really need to do this, convert the NFA to a DFA.+--+-- Invariants:+-- +-- * The start state is always the state at position 0.+-- * The length of nfaTransition is given by nfaStates.+data Nfsa t = Nfsa+  { nfaTransition :: !(Array (TransitionNfsa t))+    -- ^ Given a state and transition, this field tells you what+    --   state to go to next. The length of this array must match+    --   the total number of states. The data structure inside is+    --   a diet map. This is capable of collapsing adjacent key-value+    --   pairs into ranges.+  , nfaFinal :: !(SU.Set Int)+    -- ^ A string that ends in any of these set of states is+    --   considered to have been accepted by the grammar.+  } deriving (Show)++data TransitionNfsa t = TransitionNfsa+  { transitionNfsaEpsilon :: {-# UNPACK #-} !(SU.Set Int)+  , transitionNfsaConsume :: {-# UNPACK #-} !(DM.Map t (SU.Set Int))+  } deriving (Eq,Show)++data Conversion = Conversion+  { conversionLabel :: !Int+    -- The state identifier to be assigned to the next state.+  , conversionResolutions :: !(Map (SU.Set Int) Int)+    -- The map from subsets of states to new state identifiers.+    -- This is a bidirectional map.+  , conversionTraversed :: !(Set Int)+    -- The new state identifiers that have already been dealt with.+    -- This must be a subset of the keys of resolutions.+  , conversionPending :: !(Map Int (SU.Set Int))+    -- Newly created states that we need to consider transitions for.+    -- The keys in this should all be less than the label.+  }++data Pairing = Pairing+  { pairingMap :: !(Map (Int,Int) Int)+  , pairingReversedOld :: ![(Int,Int)]+  , pairingState :: !Int+  }++append :: Nfsa t -> Nfsa t -> Nfsa t+append (Nfsa t1 f1) (Nfsa t2 f2) = +  let n1 = C.size t1+      n2 = C.size t2+      n3 = n1 + n2+      f3 = SU.mapMonotonic (+n1) f2+      t3 = fmap (\(TransitionNfsa eps consume) -> TransitionNfsa (SU.mapMonotonic (+n1) eps) (DM.mapBijection (SU.mapMonotonic (+n1)) consume)) t2+      t4 = fmap (\(TransitionNfsa eps consume) -> TransitionNfsa eps (DM.mapBijection (\states -> if SU.null (SU.intersection states f1) then states else states <> transitionNfsaEpsilon (C.index t3 0)) consume)) t1+      !(# placeholder #) = C.index# t1 0+      t5 = runST $ do+        m <- C.replicateM n3 placeholder+        C.copy m 0 t4 0 n1+        C.copy m n1 t3 0 n2+        flip SU.traverse_ f1 $ \ix -> do+          TransitionNfsa epsilon consume <- C.read m ix+          let transition = TransitionNfsa (epsilon <> transitionNfsaEpsilon (C.index t3 0)) consume+          C.write m ix transition+        C.unsafeFreeze m+   in Nfsa t5 f3++nextIdentifier :: State.State Conversion Int+nextIdentifier = do+  Conversion n a b c <- State.get +  State.put (Conversion (n + 1) a b c)+  return n++-- Mark a new state as having been completed.+complete :: Int -> State.State Conversion ()+complete s = do+  c <- State.get+  State.put c+    { conversionTraversed = S.insert s (conversionTraversed c)+    , conversionPending = M.delete s (conversionPending c)+    }++-- Convert the subset of NFA states to a single DFA state.+resolveSubset :: Array (TransitionNfsa t) -> SU.Set Int -> State.State Conversion Int+resolveSubset transitions s0 = do+  let s = epsilonClosure transitions s0+  Conversion _ resolutions0 _ _ <- State.get+  case M.lookup s resolutions0 of+    Nothing -> do+      ident <- nextIdentifier+      c <- State.get+      State.put c+        { conversionResolutions = M.insert s ident (conversionResolutions c)+        , conversionPending = M.insert ident s (conversionPending c)+        }+      return ident+    Just ident -> return ident+  +epsilonClosure :: Array (TransitionNfsa t) -> SU.Set Int -> SU.Set Int+epsilonClosure s states = go states SU.empty where+  go new old = if new == old+    then new+    else+      let together = old <> new+       in go (mconcat (map (\ident -> transitionNfsaEpsilon (indexArray s ident)) (SU.toList together)) <> together) together++data Node t = Node+  !Int -- identifier+  !(DM.Map t Int) -- transitions++-- | Convert an NFSA to a DFSA. For certain inputs, this causes+--   the number of states to blow up expontentially, so do not+--   call this on untrusted input.+toDfsa :: (Ord t, Bounded t, Enum t) => Nfsa t -> Dfsa t+toDfsa = snd . toDfsaMapping++toDfsaMapping :: forall t. (Ord t, Bounded t, Enum t) => Nfsa t -> (Map (SU.Set Int) Int, Dfsa t)+toDfsaMapping (Nfsa t0 f0) = runST $ do+  let ((len,nodes),c) = State.runState+        (go 0 [])+        (Conversion 1 (M.singleton startClosure 0) S.empty (M.singleton 0 startClosure))+      resolutions = conversionResolutions c+  marr <- C.new len+  forM_ nodes $ \(Node ident transitions) -> C.write marr ident transitions+  arr <- C.unsafeFreeze marr+  let f1 = SU.fromList (M.foldrWithKey (\k v xs -> if SU.null (SU.intersection k f0) then xs else v : xs) [] resolutions)+  let (canonB,r) = minimizeMapping arr f1+      canon = fmap (fromMaybe (error "toDfsaMapping: missing canon value") . flip M.lookup canonB) resolutions+  return (canon,r)+  where+  startClosure :: SU.Set Int+  startClosure = epsilonClosure t0 (SU.singleton 0)+  go :: Int -> [Node t] -> State.State Conversion (Int, [Node t])+  go !n !edges0 = do+    Conversion _ _ _ pending <- State.get+    case M.foldMapWithKey (\k v -> Just (First (k,v))) pending of+      Nothing -> return (n, edges0)+      Just (First (m,states)) -> do+        t <- DM.traverseBijection (resolveSubset t0) (mconcat (map (transitionNfsaConsume . indexArray t0) (SU.toList states)))+        complete m+        go (n + 1) (Node m t : edges0)++-- | This uses Hopcroft's Algorithm. It is like a smart constructor for Dfsa.+minimize :: (Ord t, Bounded t, Enum t) => Array (DM.Map t Int) -> SU.Set Int -> Dfsa t+minimize t0 f0 = snd (minimizeMapping t0 f0)++-- | This uses Hopcroft's Algorithm. It also provides the mapping from old+--   state number to new state number. We need this mapping for a special+--   NFST to DFST minimizer.+minimizeMapping :: forall t. (Ord t, Bounded t, Enum t) => Array (DM.Map t Int) -> SU.Set Int -> (Map Int Int, Dfsa t)+minimizeMapping t0 f0 =+  let partitions0 = go (S.fromList [f1,S.difference q0 f1]) (S.singleton f1)+      -- We move the partition containing the start state to the front.+      partitions1 = case L.find (S.member 0) partitions0 of+        Just startStates -> startStates : deletePredicate (\s -> S.member 0 s || S.null s) (S.toList partitions0)+        Nothing -> error "Automata.Nfsa.minimize: incorrect"+      -- Creates a map from old state to new state. This is not a bijection+      -- since two old states may map to the same new state. However, we+      -- may treat it as a bijection since at most one of the old states+      -- is preserved.+      assign :: Int -> Map Int Int -> [Set Int] -> Map Int Int+      assign !_ !m [] = m+      assign !ix !m (s : ss) = assign (ix + 1) (M.union (M.fromSet (const ix) s) m) ss+      assignments = assign 0 M.empty partitions1+      newTransitions0 = E.fromList (map (\s -> DM.map (\oldState -> fromMaybe (error "Automata.Nfsa.minimize: missing state") (M.lookup oldState assignments)) (PM.indexArray t1 (S.findMin s))) partitions1)+      canonization = establishOrder newTransitions0+      description = "[canonization=" ++ show canonization ++ "][assignments=" ++ show assignments ++ "]"+      newTransitions1 :: Array (DM.Map t Int) = C.map' (DM.mapBijection (\s -> fromMaybe (error ("Automata.Nfsa.minimize: canonization missing state [state=" ++ show s ++ "]" ++ description)) (M.lookup s canonization))) newTransitions0+      newTransitions2 = runST $ do+        marr <- C.replicateM (M.size canonization) (error ("Automata.Nfsa.minimize: uninitialized element " ++ description))+        flip C.itraverse_ newTransitions1 $ \ix dm -> C.write marr (fromMaybe (error ("Automata.Nfsa.minimize: missing state while rearranging [state=" ++ show ix ++ "]" ++ description)) (M.lookup ix canonization)) dm+        C.unsafeFreeze marr+      newAcceptingStates = foldMap (maybe SU.empty SU.singleton . (flip M.lookup canonization <=< flip M.lookup assignments)) f1+      finalCanonization = fmap (fromMaybe (error ("minimizeMapping: failed to connect the canons.\npartitions:\n" ++ show partitions1 ++ "\ninitial canon:\n" ++ show initialCanonization ++ "\nsecond canon:\n" ++ show canonization)) . (flip M.lookup canonization <=< flip M.lookup assignments)) initialCanonization+   in (finalCanonization,Dfsa newTransitions2 newAcceptingStates)+  where+  q0 = S.fromList (enumFromTo 0 (C.size t1 - 1))+  f1 = S.fromList (mapMaybe (\x -> M.lookup x initialCanonization) (SU.toList f0))+  -- Do we actually need to canonize the states twice? Yes, we do.+  t1' :: Array (DM.Map t Int)+  t1' = C.map' (DM.mapBijection (\s -> fromMaybe (error "Automata.Nfsa.minimize: t1 prime") (M.lookup s initialCanonization))) t0+  t1 = runST $ do+    marr <- C.replicateM (M.size initialCanonization) (error "Automata.Nfsa.minimize: t1 uninitialized element")+    flip C.itraverse_ t1' $ \ix dm -> case M.lookup ix initialCanonization of+      Nothing -> return ()+      Just newIx -> C.write marr newIx dm+    C.unsafeFreeze marr+  initialCanonization = establishOrder t0+  -- The inverted transitions has the destination state as well as+  -- all source states that lead to it when the token is consumed. +  invertedTransitions :: DM.Map t (MLL.Map Int (Set Int))+  invertedTransitions = mconcat (toList (C.imap (\ix m -> DM.mapBijection (\dest -> MLL.singleton dest (S.singleton ix)) m) t1 :: Array (DM.Map t (MLL.Map Int (Set Int)))))+  -- The result of go is set of disjoint sets. It represents the equivalence classes+  -- that have been established. All references to any state in an equivalence class+  -- can be replaced with any of the other states in the same equivalence class.+  go :: Set (Set Int) -> Set (Set Int) -> Set (Set Int)+  go p1 w1 = case S.minView w1 of+    Nothing -> p1+    Just (a,w2) ->+      let (p2,w3) = DM.foldl'+            (\(p3,w4) m ->+              let x = foldMap (\s -> fromMaybe S.empty (MLL.lookup s m)) a+               in foldl'+                    (\(p4, w5) y ->+                      let diffYX = S.difference y x+                          intersectYX = S.intersection y x+                       in if not (S.disjoint x y) && not (S.null diffYX)+                            then+                              ( S.insert diffYX (S.insert intersectYX (S.delete y p4))+                              , if S.member y w5+                                  then S.insert diffYX (S.insert intersectYX (S.delete y w5))+                                  else if S.size intersectYX <= S.size diffYX+                                    then S.insert intersectYX w5+                                    else S.insert diffYX w5+                              )+                            else (S.insert y p4, w5)+                    ) (S.empty, w4) p3+            ) (p1,w2) invertedTransitions+       in go p2 w3++-- This gives a canonical order to the states. Any state missing from+-- the resulting map was not reachable. The map goes from old state+-- identifiers to new state identifiers. It is a bijection.+establishOrder :: Array (DM.Map t Int) -> Map Int Int+establishOrder t = go 0 [0] M.empty where+  go :: Int -> [Int] -> Map Int Int -> Map Int Int+  go !ident !unvisited0 !assignments = case unvisited0 of+    [] -> assignments+    state : unvisited1 -> if isNothing (M.lookup state assignments)+      then+        let unvisited2 = DM.foldl'+             (\unvisited s -> if isNothing (M.lookup s assignments) then s : unvisited else unvisited)+             unvisited1+             (PM.indexArray t state)+         in go (ident + 1) unvisited2 (M.insert state ident assignments)+      else go ident unvisited1 assignments++-- removeUnreachable :: Array (DM.Map t Int) -> SU.Set Int -> (Array (DM.Map t Int), SU.Set Int)++deletePredicate :: (a -> Bool) -> [a] -> [a]+deletePredicate _ [] = []+deletePredicate p (y:ys) = if p y then deletePredicate p ys else y : deletePredicate p ys++-- | Accepts input that is accepted by both of the two argument DFAs. This is also known+--   as completely synchronous composition in the literature.+intersection :: (Ord t, Bounded t, Enum t) => Dfsa t -> Dfsa t -> Dfsa t+intersection = compose (&&)++-- Adjusts all the values in the first interval map by multiplying+-- them by the number of states in the second automaton. Then,+-- adds these to the states numbers from the second automaton+scoot :: Ord t => Int -> DM.Map t Int -> DM.Map t Int -> DM.Map t Int+scoot n2 d1 d2 = DM.unionWith (\s1 s2 -> n2 * s1 + s2) d1 d2++{-# NOINLINE errorThunkUnion #-}+errorThunkUnion :: a+errorThunkUnion = error "Automata.Dfsa.union: slot not filled"++-- | Accepts input that is accepted by either of the two argument DFAs. This is also known+--   as synchronous composition in the literature.+union :: (Ord t, Bounded t, Enum t) => Dfsa t -> Dfsa t -> Dfsa t+union = compose (||)++composeMapping :: (Ord t, Bounded t, Enum t) => (Bool -> Bool -> Bool) -> Dfsa t -> Dfsa t -> (Map (Int,Int) Int, Dfsa t)+composeMapping combineFinalMembership (Dfsa t1 f1) (Dfsa t2 f2) = runST $ do+  let Pairing oldToNew reversedOld n3 = compositionReachable t1 t2+  m <- PM.newArray n3 errorThunkUnion+  let go !_ [] = return ()+      go !ix (statePair@(stateA,stateB) : xs) = do+        PM.writeArray m ix (DM.unionWith (\x y -> fromMaybe (error "Automata.Dfsa.union: could not find pair in oldToNew") (M.lookup (x,y) oldToNew)) (PM.indexArray t1 stateA) (PM.indexArray t2 stateB))+        go (ix - 1) xs+  go (n3 - 1) reversedOld+  frozen <- PM.unsafeFreezeArray m+  let finals = SU.fromList (M.foldrWithKey (\(stateA,stateB) stateNew xs -> if combineFinalMembership (SU.member stateA f1) (SU.member stateB f2) then stateNew : xs else xs) [] oldToNew)+  let (secondMapping, r) = minimizeMapping frozen finals+  return (M.map (\x -> fromMaybe (error "composeMapping: bad lookup") (M.lookup x secondMapping)) oldToNew, r)++compose :: (Ord t, Bounded t, Enum t) => (Bool -> Bool -> Bool) -> Dfsa t -> Dfsa t -> Dfsa t+compose combineFinalMembership a b = snd (composeMapping combineFinalMembership a b)++compositionReachable :: Ord t => Array (DM.Map t Int) -> Array (DM.Map t Int) -> Pairing+compositionReachable a b = State.execState (go 0 0) (Pairing M.empty [] 0) where+  !szA = PM.sizeofArray a+  !szB = PM.sizeofArray b+  go :: Int -> Int -> State.State Pairing ()+  go !stateA !stateB = do+    Pairing m xs s <- State.get+    case M.lookup (stateA,stateB) m of+      Just _ -> return ()+      Nothing -> do+        State.put (Pairing (M.insert (stateA,stateB) s m) ((stateA,stateB) : xs) (s + 1))+        DM.traverse_ (uncurry go) (DM.unionWith (,) (PM.indexArray a stateA) (PM.indexArray b stateB))+    ++-- | Docs for this are at @Automata.Nfsa.union@.+unionNfsa :: (Bounded t) => Nfsa t -> Nfsa t -> Nfsa t+unionNfsa (Nfsa t1 f1) (Nfsa t2 f2) = Nfsa+  ( runST $ do+      m <- C.replicateM (n1 + n2 + 1)+        ( TransitionNfsa+          (mconcat+            [ SU.mapMonotonic (+1) (transitionNfsaEpsilon (C.index t1 0))+            , SU.mapMonotonic (\x -> 1 + n1) (transitionNfsaEpsilon (C.index t2 0))+            , SU.tripleton 0 1 (1 + n1)+            ]+          )+          (DM.pure SU.empty)+        )+      C.copy m 1 (fmap (translateTransitionNfsa 1) t1) 0 n1+      C.copy m (1 + n1) (fmap (translateTransitionNfsa (1 + n1)) t2) 0 n2+      C.unsafeFreeze m+  )+  (SU.mapMonotonic (+1) f1 <> SU.mapMonotonic (\x -> 1 + n1 + x) f2)+  where+  !n1 = PM.sizeofArray t1+  !n2 = PM.sizeofArray t2++translateTransitionNfsa :: Int -> TransitionNfsa t -> TransitionNfsa t+translateTransitionNfsa n (TransitionNfsa eps m) = TransitionNfsa+  (SU.mapMonotonic (+n) eps)+  (DM.mapBijection (SU.mapMonotonic (+n)) m)++-- | Automaton that accepts all input. This is the identity+-- for 'intersection'.+acceptance :: Bounded t => Dfsa t+acceptance = Dfsa (C.singleton (DM.pure 0)) (SU.singleton 0)++-- | Automaton that rejects all input. This is the identity+-- for 'union'.+rejection :: Bounded t => Dfsa t+rejection = Dfsa (C.singleton (DM.pure 0)) SU.empty++-- | Automaton that accepts the empty string and rejects all+-- other strings. This is the identity for 'append'.+empty :: Bounded t => Nfsa t+empty = Nfsa+  ( C.doubleton+    (TransitionNfsa (SU.singleton 0) (DM.pure (SU.singleton 1)))+    (TransitionNfsa (SU.singleton 1) (DM.pure SU.empty))+  )+  (SU.singleton 0)++-- | Docs for this are at @Automata.Nfsa.rejection@.+rejectionNfsa :: Bounded t => Nfsa t+rejectionNfsa = Nfsa+  (C.singleton (TransitionNfsa (SU.singleton 0) (DM.pure SU.empty)))+  SU.empty++-- | This uses 'union' for @plus@ and 'intersection' for @times@.+instance (Ord t, Enum t, Bounded t) => Semiring (Dfsa t) where+  plus = union+  times = intersection+  zero = rejection+  one = acceptance++-- | This uses @union@ for @plus@ and @append@ for @times@.+instance (Bounded t) => Semiring (Nfsa t) where+  plus = unionNfsa+  times = append+  zero = rejectionNfsa+  one = empty+  +data Epsilon = Epsilon !Int !Int++newtype State s = State Int

+ src/Automata/Internal/Transducer.hs view

@@ -0,0 +1,108 @@+{-# language BangPatterns #-}++module Automata.Internal.Transducer+  ( Nfst(..)+  , TransitionNfst(..)+  , Dfst(..)+  , MotionDfst(..)+  , Edge(..)+  , EdgeDest(..)+  , epsilonClosure+  , rejection+  , union+  ) where++import Control.Monad.ST (runST)+import Data.Primitive (Array)+import Data.Primitive (indexArray)+import qualified Data.Primitive as PM+import qualified Data.Primitive.Contiguous as C+import qualified Data.Set.Unboxed as SU+import qualified Data.Map.Interval.DBTSLL as DM+import qualified Data.Map.Lifted.Unlifted as MLN++-- | A deterministic finite state transducer.+data Dfst t m = Dfst+  { dfstTransition :: !(Array (DM.Map t (MotionDfst m)))+    -- ^ Given a state and transition, this field tells you what+    --   state to go to next. The length of this array must match+    --   the total number of states.+  , dfstFinal :: !(SU.Set Int)+    -- ^ A string that ends in any of these set of states is+    --   considered to have been accepted by the grammar.+  } deriving (Eq,Show)++data MotionDfst m = MotionDfst+  { motionDfstState :: !Int+  , motionDfstOutput :: !m+  } deriving (Eq,Show)++-- | A nondeterministic finite state transducer. The @t@ represents the input token on+-- which a transition occurs. The @m@ represents the output token that+-- is generated when a transition is taken. On an epsilon transation,+-- no output is generated.+data Nfst t m = Nfst+  { nfstTransition :: !(Array (TransitionNfst t m))+    -- ^ Given a state and transition, this field tells you what+    --   state to go to next. The length of this array must match+    --   the total number of states. The data structure inside is+    --   an interval map. This is capable of collapsing adjacent key-value+    --   pairs into ranges.+  , nfstFinal :: !(SU.Set Int)+    -- ^ A string that ends in any of these set of states is+    --   considered to have been accepted by the grammar.+  } deriving (Eq,Show)++data TransitionNfst t m = TransitionNfst+  { transitionNfstEpsilon :: {-# UNPACK #-} !(SU.Set Int)+  , transitionNfstConsume :: {-# UNPACK #-} !(DM.Map t (MLN.Map m (SU.Set Int)))+  } deriving (Eq,Show)++epsilonClosure :: Array (TransitionNfst m t) -> SU.Set Int -> SU.Set Int+epsilonClosure s states = go states SU.empty where+  go new old = if new == old+    then new+    else+      let together = old <> new+       in go (mconcat (map (\ident -> transitionNfstEpsilon (indexArray s ident)) (SU.toList together)) <> together) together++data Edge t m = Edge !Int !Int !t !t !m++data EdgeDest t m = EdgeDest !Int !t !t !m++-- | Transducer that rejects all input, generating the monoid identity as output.+-- This is the identity for 'union'.+rejection :: (Ord t, Bounded t, Monoid m, Ord m) => Nfst t m+rejection = Nfst+  (C.singleton (TransitionNfst (SU.singleton 0) (DM.pure mempty)))+  SU.empty++-- | Accepts input that is accepts by either of the transducers, producing the+--   output of both of them.+union :: (Bounded t, Ord m) => Nfst t m -> Nfst t m -> Nfst t m+union (Nfst t1 f1) (Nfst t2 f2) = Nfst+  ( runST $ do+      m <- C.replicateM (n1 + n2 + 1)+        ( TransitionNfst+          (mconcat+            [ SU.mapMonotonic (+1) (transitionNfstEpsilon (C.index t1 0))+            , SU.mapMonotonic (\x -> 1 + n1) (transitionNfstEpsilon (C.index t2 0))+            , SU.tripleton 0 1 (1 + n1)+            ]+          )+          (DM.pure mempty)+        )+      C.copy m 1 (fmap (translateTransitionNfst 1) t1) 0 n1+      C.copy m (1 + n1) (fmap (translateTransitionNfst (1 + n1)) t2) 0 n2+      C.unsafeFreeze m+  )+  (SU.mapMonotonic (+1) f1 <> SU.mapMonotonic (\x -> 1 + n1 + x) f2)+  where+  !n1 = PM.sizeofArray t1+  !n2 = PM.sizeofArray t2++translateTransitionNfst :: Int -> TransitionNfst t m -> TransitionNfst t m+translateTransitionNfst n (TransitionNfst eps m) = TransitionNfst+  (SU.mapMonotonic (+n) eps)+  (DM.mapBijection (MLN.map (SU.mapMonotonic (+n))) m)+

+ src/Automata/Nfsa.hs view

@@ -0,0 +1,63 @@+{-# language BangPatterns #-}+{-# language LambdaCase #-}+{-# language MagicHash #-}+{-# language UnboxedTuples #-}+{-# language ScopedTypeVariables #-}++module Automata.Nfsa+  ( -- * Types+    Nfsa+    -- * Conversion+  , toDfsa+    -- * Evaluation+  , evaluate+    -- * Composition+  , AI.append+  , union+    -- * Special NFA+  , rejection+  , AI.empty+  ) where++import Automata.Internal (Nfsa(..),Dfsa(..),TransitionNfsa(..),toDfsa)+import Data.Semigroup (First(..))+import Control.Monad.Trans.State.Strict (State)+import Data.Set (Set)+import Data.Map (Map)+import Control.Monad.ST (runST)+import Data.Primitive (Array,indexArray)+import Control.Monad (forM_)+import Data.Foldable (foldl')++import qualified Automata.Internal as AI+import qualified Data.Set as S+import qualified Data.Set.Unboxed as SU+import qualified Data.Map.Strict as M+import qualified Control.Monad.Trans.State.Strict as State+import qualified Data.Map.Interval.DBTSLL as DM+import qualified Data.Map.Unboxed.Lifted as MUL+import qualified Data.Primitive.Contiguous as C+import qualified Data.Primitive as PM++fromDfsa :: Dfsa t -> Nfsa t+fromDfsa (Dfsa t f) =+  Nfsa (fmap (TransitionNfsa SU.empty . DM.mapBijection SU.singleton) t) f++rejection :: Bounded t => Nfsa t+rejection = AI.rejectionNfsa++union :: (Bounded t) => Nfsa t -> Nfsa t -> Nfsa t+union = AI.unionNfsa++-- note: turn foldl' + mconcat into single foldMap?+evaluate :: (Foldable f, Ord t) => Nfsa t -> f t -> Bool+evaluate (Nfsa transitions finals) tokens = not $ SU.null $ SU.intersection+  ( foldl'+    ( \(active :: SU.Set Int) token -> mconcat $ SU.foldl'+      (\xs state -> DM.lookup token (transitionNfsaConsume (C.index transitions state)) : xs)+      ([] :: [SU.Set Int])+      active+    ) (transitionNfsaEpsilon (C.index transitions 0)) tokens+  )+  finals+

+ src/Automata/Nfsa/Builder.hs view

@@ -0,0 +1,111 @@+{-# language BangPatterns #-}+{-# language DeriveFunctor #-}+{-# language DerivingStrategies #-}+{-# language RankNTypes #-}+{-# language ScopedTypeVariables #-}++module Automata.Nfsa.Builder+  ( Builder+  , run+  , state+  , transition+  , accept+  , epsilon+  ) where++import Automata.Internal (Nfsa(..),TransitionNfsa(..),epsilonClosure)+import Control.Monad.ST (runST)+import Data.Foldable (for_)+import Data.Primitive (Array)+import qualified Data.Map.Interval.DBTSLL as DM+import qualified Data.Primitive.Contiguous as C+import qualified Data.Set.Unboxed as SU++newtype Builder t s a = Builder (Int -> [Edge t] -> [Epsilon] -> [Int] -> Result t a)+  deriving stock (Functor)++instance Applicative (Builder t s) where+  pure a = Builder (\i es eps fs -> Result i es eps fs a)+  Builder f <*> Builder g = Builder $ \i es eps fs -> case f i es eps fs of+    Result i' es' eps' fs' x -> case g i' es' eps' fs' of+      Result i'' es'' eps'' fs'' y -> Result i'' es'' eps'' fs'' (x y)++instance Monad (Builder t s) where+  Builder f >>= g = Builder $ \i es eps fs -> case f i es eps fs of+    Result i' es' eps' fs' a -> case g a of+      Builder g' -> g' i' es' eps' fs'++data Result t a = Result !Int ![Edge t] ![Epsilon] ![Int] a+  deriving stock (Functor)++data Edge t = Edge !Int !Int !t !t++data EdgeDest t = EdgeDest !Int !t !t++data Epsilon = Epsilon !Int !Int++newtype State s = State Int++-- | The argument function takes a start state and builds an NFSA. This+-- function will execute the builder.+run :: forall t a. (Bounded t, Ord t, Enum t) => (forall s. State s -> Builder t s a) -> Nfsa t+run fromStartState =+  case state >>= fromStartState of+    Builder f -> case f 0 [] [] [] of+      Result totalStates edges epsilons final _ ->+        let ts0 = runST $ do+              transitions <- C.replicateM totalStates (TransitionNfsa SU.empty (DM.pure SU.empty))+              outbounds <- C.replicateM totalStates []+              epsilonArr <- C.replicateM totalStates []+              for_ epsilons $ \(Epsilon source destination) -> do+                edgeDests0 <- C.read epsilonArr source+                let !edgeDests1 = destination : edgeDests0+                C.write epsilonArr source edgeDests1+              (epsilonArr' :: Array [Int]) <- C.unsafeFreeze epsilonArr+              for_ edges $ \(Edge source destination lo hi) -> do+                edgeDests0 <- C.read outbounds source+                let !edgeDests1 = EdgeDest destination lo hi : edgeDests0+                C.write outbounds source edgeDests1+              (outbounds' :: Array [EdgeDest t]) <- C.unsafeFreeze outbounds+              flip C.imapMutable' transitions $ \i (TransitionNfsa _ _) -> +                let dests = C.index outbounds' i+                    eps = C.index epsilonArr' i+                 in TransitionNfsa (SU.fromList eps)+                      ( mconcat+                        ( map+                          (\(EdgeDest dest lo hi) -> DM.singleton SU.empty lo hi (SU.singleton dest))+                          dests+                        )+                      )+              C.unsafeFreeze transitions+            ts1 = C.imap (\s (TransitionNfsa eps consume) -> TransitionNfsa (epsilonClosure ts0 (SU.singleton s <> eps)) (DM.map (epsilonClosure ts0) consume)) ts0+         in Nfsa ts1 (SU.fromList final)+  +-- | Generate a new state in the NFA. On any input, the+--   state transitions to zero states.+state :: Builder t s (State s)+state = Builder $ \i edges eps final -> Result (i + 1) edges eps final (State i)++-- | Mark a state as being an accepting state. +accept :: State s -> Builder t s ()+accept (State n) = Builder $ \i edges eps final -> Result i edges eps (n : final) ()++-- | Add a transition from one state to another when the input token+--   is inside the inclusive range.+transition ::+     t -- ^ inclusive lower bound+  -> t -- ^ inclusive upper bound+  -> State s -- ^ from state+  -> State s -- ^ to state+  -> Builder t s ()+transition lo hi (State source) (State dest) =+  Builder $ \i edges eps final -> Result i (Edge source dest lo hi : edges) eps final ()++-- | Add a transition from one state to another that consumes no input.+epsilon ::+     State s -- ^ from state+  -> State s -- ^ to state+  -> Builder t s ()+epsilon (State source) (State dest) = +  Builder $ \i edges eps final -> Result i edges (if source /= dest then Epsilon source dest : eps else eps) final ()+

+ src/Automata/Nfst.hs view

@@ -0,0 +1,218 @@+{-# language BangPatterns #-}+{-# language DeriveFunctor #-}+{-# language DerivingStrategies #-}+{-# language LambdaCase #-}+{-# language MagicHash #-}+{-# language UnboxedTuples #-}+{-# language RankNTypes #-}+{-# language ScopedTypeVariables #-}++module Automata.Nfst+  ( -- * Static+    -- ** Types+    Nfst+    -- ** Functions+  , evaluate+  , evaluateAscii+  , union+  , toDfst+  , toNfsa+    -- ** Special Transducers+  , rejection+    -- * Builder+    -- ** Types+  , Builder+  , State+    -- ** Functions+  , build+  , state+  , transition+  , epsilon+  , accept+  ) where++import Automata.Internal (State(..),Epsilon(..),Nfsa(..),Dfsa(..),TransitionNfsa(..),toDfsaMapping)+import Automata.Internal.Transducer (Nfst(..),Dfst(..),TransitionNfst(..),MotionDfst(..),Edge(..),EdgeDest(..),epsilonClosure,rejection,union)+import Control.Monad.ST (runST)+import Data.ByteString (ByteString)+import Data.Foldable (for_,fold)+import Data.Map.Strict (Map)+import Data.Maybe (fromMaybe)+import Data.Monoid (Any(..))+import Data.Primitive (Array,indexArray)+import Data.Set (Set)++import Debug.Trace++import qualified Data.ByteString.Char8 as BC+import qualified Data.Map.Strict as M+import qualified Data.Set as S+import qualified Data.Set.Unboxed as SU+import qualified Data.Map.Interval.DBTSLL as DM+import qualified Data.Map.Lifted.Unlifted as MLN+import qualified Data.Primitive.Contiguous as C+import qualified Data.Foldable as F++debugTrace :: Show a => a -> a+debugTrace = id++-- | Evaluate an NFST. If the output is the empty set, the input string+-- did not belong to the language. Otherwise, all possible outputs given.+-- The output token lists are in reverse order, and they are all the exact+-- same length as the input string. The reversed order is done to maximize+-- opportunities for sharing common output prefixes. To get the output tokens+-- in the right order, reverse the NFST before evaluating an input string+-- against it. Then, the output tokens will be in the right order, and they will+-- share common suffixes in memory.+evaluate :: forall f t m. (Foldable f, Ord t, Ord m) => Nfst t m -> f t -> Set [m]+evaluate (Nfst transitions finals) tokens = S.unions $ M.elems $ M.filterWithKey+  (\k _ -> SU.member k finals)+  (F.foldl' step (M.unionsWith (<>) (map (\s -> M.singleton s (S.singleton [])) (SU.toList (transitionNfstEpsilon (C.index transitions 0))))) tokens)+  where+  step :: Map Int (Set [m]) -> t -> Map Int (Set [m])+  step active token = M.unionsWith (<>) $ M.foldlWithKey'+    ( \xs state outputSets -> MLN.foldlWithKey'+        (\zs outputTokenNext nextStates -> M.unionsWith (<>) (map (\s -> M.singleton s (S.mapMonotonic (outputTokenNext:) outputSets)) (SU.toList nextStates)) : zs)+        xs+        (DM.lookup token (transitionNfstConsume (C.index transitions state)))+    ) [] active++evaluateAscii :: forall m. Ord m => Nfst Char m -> ByteString -> Set [m]+evaluateAscii (Nfst transitions finals) tokens = S.unions $ M.elems $ M.filterWithKey+  (\k _ -> SU.member k finals)+  (BC.foldl' step (M.unionsWith (<>) (map (\s -> M.singleton s (S.singleton [])) (SU.toList (transitionNfstEpsilon (C.index transitions 0))))) tokens)+  where+  step :: Map Int (Set [m]) -> Char -> Map Int (Set [m])+  step active token = M.unionsWith (<>) $ M.foldlWithKey'+    ( \xs state outputSets -> MLN.foldlWithKey'+        (\zs outputTokenNext nextStates -> M.unionsWith (<>) (map (\s -> M.singleton s (S.mapMonotonic (outputTokenNext:) outputSets)) (SU.toList nextStates)) : zs)+        xs+        (DM.lookup token (transitionNfstConsume (C.index transitions state)))+    ) [] active++-- | Convert an NFST to a DFST that accepts the same input and produces+--   output. Since NFST are more powerful than DFST, it is not possible+--   to preserve output of the NFST during this conversion. However,+--   this function makes the guarantee that if the NFST would accepts+--   an input string and produces the output+--+--   > [[a1,a2,a3,...],[b1,b2,b3,...],...]+--+--   Then DFST will accept the same input and produce an output of+--+--   > ∃ ω1 ω2. [ω1 <> a1 <> b1 <> ..., ω2 <> a1 <> b1 <> ...]+--+--   This must be a commutative semigroup, and the existentially+--   quantified values appended to the output cannot be easily+--   predicted.+toDfst :: forall t m. (Ord t, Bounded t, Enum t, Monoid m) => Nfst t m -> Dfst t m+toDfst x@(Nfst tx _) =+  let (mapping,Dfsa t0 f) = toDfsaMapping (toNfsa x)+      mapping' = debugTrace mapping+      -- The revMapping goes from new state id to a set of old state subsets+      revMapping :: Map Int (SU.Set Int)+      revMapping = debugTrace $ M.foldlWithKey' (\acc k v -> M.insertWith (<>) v k acc) M.empty mapping'+      t1 = C.imap+        (\source m -> DM.mapBijection+          (\dest ->+            let oldSources = fromMaybe (error "Automata.Nfst.toDfst: missing old source") (M.lookup source revMapping)+                oldDests = fromMaybe (error "Automata.Nfst.toDfst: missing old dest") (M.lookup dest revMapping)+                -- Do we need to deal with epsilon stuff in here? I don't think so.+                -- Also, this part could be greatly improved. We are using a very simple heuristic,+                -- and we could prune out far more outputs if we were more clever about this.+                newOutput = SU.foldMap (\oldSource -> DM.foldMap (MLN.foldMapWithKey' (\output oldDestStates -> if getAny (SU.foldMap (\oldDest -> Any (SU.member oldDest oldDests)) oldDestStates) then output else mempty)) (transitionNfstConsume (indexArray tx oldSource))) oldSources+             in MotionDfst dest newOutput+          ) m+        ) t0+   in Dfst t1 f++-- | Discard information about output tokens.+toNfsa :: Nfst t m -> Nfsa t+toNfsa (Nfst t f) = Nfsa+  (fmap (\(TransitionNfst eps m) -> TransitionNfsa eps (DM.map (MLN.foldlWithKey' (\acc _ x -> acc <> x) mempty) m)) t)+  f++newtype Builder t m s a = Builder (Int -> [Edge t m] -> [Epsilon] -> [Int] -> Result t m a)+  deriving stock (Functor)++data Result t m a = Result !Int ![Edge t m] ![Epsilon] ![Int] a+  deriving stock (Functor)++instance Applicative (Builder t m s) where+  pure a = Builder (\i es eps fs -> Result i es eps fs a)+  Builder f <*> Builder g = Builder $ \i es eps fs -> case f i es eps fs of+    Result i' es' eps' fs' x -> case g i' es' eps' fs' of+      Result i'' es'' eps'' fs'' y -> Result i'' es'' eps'' fs'' (x y)++instance Monad (Builder t m s) where+  Builder f >>= g = Builder $ \i es eps fs -> case f i es eps fs of+    Result i' es' eps' fs' a -> case g a of+      Builder g' -> g' i' es' eps' fs'++-- | Generate a new state in the NFA. On any input, the+--   state transitions to zero states.+state :: Builder t m s (State s)+state = Builder $ \i edges eps final -> Result (i + 1) edges eps final (State i)++-- | Mark a state as being an accepting state. +accept :: State s -> Builder t m s ()+accept (State n) = Builder $ \i edges eps final -> Result i edges eps (n : final) ()++-- | Add a transition from one state to another when the input token+--   is inside the inclusive range.+transition ::+     t -- ^ inclusive lower bound+  -> t -- ^ inclusive upper bound+  -> m -- ^ output token+  -> State s -- ^ from state+  -> State s -- ^ to state+  -> Builder t m s ()+transition lo hi output (State source) (State dest) =+  Builder $ \i edges eps final -> Result i (Edge source dest lo hi output : edges) eps final ()++-- | Add a transition from one state to another that consumes no input.+--   No output is generated on such a transition.+epsilon ::+     State s -- ^ from state+  -> State s -- ^ to state+  -> Builder t m s ()+epsilon (State source) (State dest) = +  Builder $ \i edges eps final -> Result i edges (if source /= dest then Epsilon source dest : eps else eps) final ()++-- | The argument function turns a start state into an NFST builder. This+-- function converts the builder to a usable transducer.+build :: forall t m a. (Bounded t, Ord t, Enum t, Monoid m, Ord m) => (forall s. State s -> Builder t m s a) -> Nfst t m+build fromStartState =+  case state >>= fromStartState of+    Builder f -> case f 0 [] [] [] of+      Result totalStates edges epsilons final _ ->+        let ts0 = runST $ do+              transitions <- C.replicateM totalStates (TransitionNfst SU.empty (DM.pure mempty))+              outbounds <- C.replicateM totalStates []+              epsilonArr <- C.replicateM totalStates []+              for_ epsilons $ \(Epsilon source destination) -> do+                edgeDests0 <- C.read epsilonArr source+                let !edgeDests1 = destination : edgeDests0+                C.write epsilonArr source edgeDests1+              (epsilonArr' :: Array [Int]) <- C.unsafeFreeze epsilonArr+              for_ edges $ \(Edge source destination lo hi output) -> do+                edgeDests0 <- C.read outbounds source+                let !edgeDests1 = EdgeDest destination lo hi output : edgeDests0+                C.write outbounds source edgeDests1+              (outbounds' :: Array [EdgeDest t m]) <- C.unsafeFreeze outbounds+              flip C.imapMutable' transitions $ \i (TransitionNfst _ _) -> +                let dests = C.index outbounds' i+                    eps = C.index epsilonArr' i+                 in TransitionNfst+                      ( SU.fromList eps )+                      ( mconcat+                        ( map+                          (\(EdgeDest dest lo hi output) ->+                            DM.singleton mempty lo hi (MLN.singleton output (SU.singleton dest)) :: DM.Map t (MLN.Map m (SU.Set Int))+                          )+                          dests+                        )+                      )+              C.unsafeFreeze transitions+            ts1 = C.imap (\s (TransitionNfst eps consume) -> TransitionNfst (epsilonClosure ts0 (SU.singleton s <> eps)) (DM.map (MLN.map (epsilonClosure ts0)) consume)) ts0+         in Nfst ts1 (SU.fromList final)

+ test/Main.hs view

@@ -0,0 +1,467 @@+{-# language DerivingStrategies #-}+{-# language LambdaCase #-}+{-# language ScopedTypeVariables #-}++import Automata.Dfsa (Dfsa)+import Automata.Dfst (Dfst)+import Automata.Nfsa (Nfsa)+import Automata.Nfst (Nfst)+import Control.Monad (forM_,replicateM)+import Data.Enum.Types (B(..),D(..))+import Data.Monoid (All(..))+import Data.Primitive (Array)+import Data.Proxy (Proxy(..))+import Data.Set (Set)+import Test.HUnit ((@?=),assertBool)+import Test.LeanCheck (Listable,(\/),cons0)+import Test.LeanCheck.Instances.Enum ()+import Test.QuickCheck (Arbitrary)+import Test.QuickCheck.Instances.Enum ()+import Test.Tasty (TestTree,defaultMain,testGroup,adjustOption)+import Test.Tasty.HUnit (testCase)++import qualified Automata.Nfsa as Nfsa+import qualified Automata.Nfst as Nfst+import qualified Automata.Dfsa as Dfsa+import qualified Automata.Dfst as Dfst+import qualified Automata.Nfsa.Builder as B+import qualified Data.Set as S+import qualified Data.List as L+import qualified GHC.Exts as E+import qualified Test.Tasty.LeanCheck as TL+import qualified Test.QuickCheck as QC+import qualified Test.Tasty.QuickCheck as TQC+import qualified Test.QuickCheck.Classes as QCC++main :: IO ()+main = defaultMain+  $ adjustOption (\_ -> TL.LeanCheckTests 5000)+  $ tests ++tests :: TestTree+tests = testGroup "Automata"+  [ testGroup "Nfsa"+    [ testGroup "evaluate"+      [ testCase "A" (Nfsa.evaluate ex1 [D3,D1] @?= False)+      , testCase "B" (Nfsa.evaluate ex1 [D0,D1,D3] @?= True)+      , testCase "C" (Nfsa.evaluate ex1 [D1,D3,D3] @?= True)+      , testCase "D" (Nfsa.evaluate ex1 [D0,D0,D0] @?= False)+      , testCase "E" (Nfsa.evaluate ex1 [D0,D0] @?= False)+      , testCase "F" (Nfsa.evaluate ex1 [D1] @?= True)+      , testCase "G" (Nfsa.evaluate ex1 [D1,D3] @?= True)+      , testCase "H" (Nfsa.evaluate ex2 [D3,D3,D0] @?= False)+      , testCase "I" (Nfsa.evaluate ex2 [D3,D3,D2] @?= True)+      , testCase "J" (Nfsa.evaluate ex3 [D1] @?= False)+      , testCase "K" (Nfsa.evaluate ex3 [D1,D3] @?= True)+      , testCase "L" (Nfsa.evaluate ex3 [D1,D3,D0] @?= False)+      , testCase "M" (Nfsa.evaluate ex3 [D1,D3,D0,D2,D3] @?= True)+      , testCase "N" (Nfsa.evaluate ex3 [D1,D3,D3] @?= True)+      ]+    , testGroup "append"+      [ testCase "A" (Nfsa.evaluate (Nfsa.append ex1 ex2) [D0,D1,D3,D3,D3,D2] @?= True)+      , testCase "B" (Nfsa.evaluate (Nfsa.append ex1 ex2) [D0,D0,D3,D0] @?= False)+      , testCase "C" (Nfsa.evaluate (Nfsa.append ex1 ex2) [D1,D3] @?= True)+      , testCase "D" (Nfsa.evaluate (Nfsa.append ex2 ex3) [D3,D3,D2,D1,D3,D3] @?= True)+      , testCase "E" (Nfsa.evaluate (Nfsa.append ex2 ex3) [D3,D3,D2] @?= False)+      ]+    , testGroup "union"+      [ testGroup "unit"+        [ testCase "A" (Nfsa.evaluate (Nfsa.union ex1 ex2) [D3,D1] @?= True)+        , testCase "B" (Nfsa.evaluate (Nfsa.union ex1 ex2) [D3,D3,D2] @?= True)+        , testCase "C" (Nfsa.evaluate (Nfsa.union ex1 ex2) [D0,D0,D0] @?= False)+        ]+      ]+    , testGroup "toDfsa"+      [ testGroup "unit"+        [ testCase "A" (Dfsa.evaluate (Nfsa.toDfsa ex1) [D0,D1,D3] @?= True)+        , testCase "B" (Dfsa.evaluate (Nfsa.toDfsa ex1) [D3,D1] @?= False)+        , testCase "C" (Dfsa.evaluate (Nfsa.toDfsa (Nfsa.append ex1 ex2)) [D0,D1,D3,D3,D3,D2] @?= True)+        , testCase "D" (Dfsa.evaluate (Nfsa.toDfsa (Nfsa.append ex2 ex3)) [D3,D3,D2,D1,D3,D3] @?= True)+        , testCase "E" (Dfsa.evaluate (Nfsa.toDfsa (Nfsa.append ex1 ex2)) [D0,D0,D3,D0] @?= False)+        , testCase "F" (Nfsa.toDfsa ex1 == Nfsa.toDfsa ex4 @?= True)+        , testCase "G" (Nfsa.toDfsa ex1 == Nfsa.toDfsa ex2 @?= False)+        , testCase "H" (Nfsa.toDfsa ex5 == Nfsa.toDfsa ex6 @?= True)+        ]+      , testGroup "evaluation"+        [ TL.testProperty "1" $ \(a,b,c,d) -> Dfsa.evaluate (Nfsa.toDfsa ex1) [a,b,c,d] == Nfsa.evaluate ex1 [a,b,c,d]+        , TL.testProperty "2" $ \(a,b,c,d) -> Dfsa.evaluate (Nfsa.toDfsa ex2) [a,b,c,d] == Nfsa.evaluate ex2 [a,b,c,d]+        , TL.testProperty "3" $ \(a,b,c,d) -> Dfsa.evaluate (Nfsa.toDfsa ex3) [a,b,c,d] == Nfsa.evaluate ex3 [a,b,c,d]+        , TL.testProperty "4" $ \(a,b,c,d) -> Dfsa.evaluate (Nfsa.toDfsa ex4) [a,b,c,d] == Nfsa.evaluate ex4 [a,b,c,d]+        , TL.testProperty "5" $ \(a,b,c,d) -> Dfsa.evaluate (Nfsa.toDfsa ex5) [a,b,c,d] == Nfsa.evaluate ex5 [a,b,c,d]+        , TL.testProperty "6" $ \(a,b,c,d) -> Dfsa.evaluate (Nfsa.toDfsa ex6) [a,b,c,d] == Nfsa.evaluate ex6 [a,b,c,d]+        , TL.testProperty "7" $ \(a,b,c,d) -> Dfsa.evaluate (Nfsa.toDfsa ex7) [a,b,c,d] == Nfsa.evaluate ex7 [a,b,c,d]+        ]+      , lawsToTest (QCC.semiringLaws (Proxy :: Proxy (Nfsa D)))+      ]+    ]+  , testGroup "Dfsa"+    [ testGroup "evaluate"+      [ testCase "A" (Dfsa.evaluate exDfsa1 [D1] @?= True)+      , testCase "B" (Dfsa.evaluate exDfsa1 [D3,D2,D1,D2,D0] @?= True)+      , testCase "C" (Dfsa.evaluate exDfsa2 [D3,D3] @?= False)+      , testCase "D" (Dfsa.evaluate exDfsa2 [D1] @?= True)+      , testCase "E" (Dfsa.evaluate exDfsa2 [D0,D2] @?= True)+      ]+    , testGroup "union"+      [ testGroup "unit"+        [ testCase "A" (Dfsa.evaluate (Dfsa.union (Nfsa.toDfsa ex1) (Nfsa.toDfsa ex3)) [D0,D1,D3] @?= True)+        , testCase "B" (Dfsa.evaluate (Dfsa.union (Nfsa.toDfsa ex1) (Nfsa.toDfsa ex3)) [D2,D3] @?= True)+        , testCase "C" (Dfsa.evaluate (Dfsa.union (Nfsa.toDfsa ex1) (Nfsa.toDfsa ex3)) [D1,D3] @?= True)+        , testCase "D" (Dfsa.evaluate (Dfsa.union (Nfsa.toDfsa ex1) (Nfsa.toDfsa ex3)) [D1,D3,D0] @?= False)+        , testCase "E" (Dfsa.evaluate (Dfsa.union (Nfsa.toDfsa ex1) (Nfsa.toDfsa ex3)) [D1] @?= True)+        , testCase "F" (Dfsa.evaluate (Dfsa.union (Nfsa.toDfsa ex1) (Nfsa.toDfsa ex3)) [D3] @?= False)+        , testCase "G" (Dfsa.union (Nfsa.toDfsa ex1) (Nfsa.toDfsa ex3) @?= Dfsa.union (Nfsa.toDfsa ex3) (Nfsa.toDfsa ex1))+        , testCase "H" (Dfsa.union (Nfsa.toDfsa ex1) (Nfsa.toDfsa ex1) @?= (Nfsa.toDfsa ex1))+        , testCase "I" (Dfsa.union (Nfsa.toDfsa ex3) (Nfsa.toDfsa ex3) @?= (Nfsa.toDfsa ex3))+        ]+      , TL.testProperty "idempotent" $ \x -> let y = mkBinDfsa x in y == Dfsa.union y y+      , testGroup "identity"+        [ TL.testProperty "left" $ \x -> let y = mkBinDfsa x in y == Dfsa.union Dfsa.rejection y+        , TL.testProperty "right" $ \x -> let y = mkBinDfsa x in y == Dfsa.union y Dfsa.rejection+        ]+      ]+    , testGroup "intersection"+      [ TL.testProperty "idempotent" $ \x -> let y = mkBinDfsa x in y == Dfsa.intersection y y+      , testGroup "identity"+        [ TL.testProperty "left" $ \x -> let y = mkBinDfsa x in y == Dfsa.intersection Dfsa.acceptance y+        , TL.testProperty "right" $ \x -> let y = mkBinDfsa x in y == Dfsa.intersection y Dfsa.acceptance+        ]+      ]+    , lawsToTest (QCC.semiringLaws (Proxy :: Proxy (Dfsa D)))+    ]+  , testGroup "Nfst"+    [ testGroup "evaluate"+      [ testCase "A" (Nfst.evaluate exNfst1 [D0,D1] @?= S.singleton [B1,B0])+      , testCase "B" (Nfst.evaluate exNfst1 [D2,D1,D3] @?= S.singleton [B1,B1,B1])+      , testCase "C" (Nfst.evaluate exNfst2 [D0,D0] @?= S.singleton [B0,B0])+      , testCase "D" (Nfst.evaluate exNfst2 [D1,D0] @?= S.fromList [[B0,B0],[B0,B1]])+      , testCase "E" (Nfst.evaluate exNfst3 [D0,D2] @?= S.singleton [B1,B0])+      , testCase "F" (Nfst.evaluate exNfst3 [D0,D1] @?= S.singleton [B0,B1])+      , testCase "G" (Nfst.evaluate (Nfst.union Nfst.rejection exNfst3) [D0,D1] @?= S.singleton [B0,B1])+      , testCase "H" (Nfst.evaluate (Nfst.union exNfst1 exNfst3) [D0,D1] @?= S.fromList [[B1,B0],[B0,B1]])+      , testCase "I" (Nfst.evaluate (Nfst.union exNfst3 exNfst1) [D0,D1] @?= S.fromList [[B1,B0],[B0,B1]])+      ]+    , testGroup "toDfst"+      [ testGroup "unit"+        [ testCase "A" (let x = Dfst.evaluate (Nfst.toDfst exNfst4) [D0,D1] in assertBool (show x) (setSubresult [B1, B0] x))+        , testCase "B" (let x = Dfst.evaluate (Nfst.toDfst exNfst5) [D1,D2] in assertBool (show x) (setSubresult [B0, B1] x))+        ]+      , testGroup "evaluation"+        [ TL.testProperty "4" $ \(input :: [D]) -> getAll (foldMap (\x -> All (subresult (L.reverse x) (Dfst.evaluate (Nfst.toDfst exNfst4) input))) (Nfst.evaluate exNfst4 input))+        , TL.testProperty "5" $ \(input :: [D]) -> getAll (foldMap (\x -> All (subresult (L.reverse x) (Dfst.evaluate (Nfst.toDfst exNfst5) input))) (Nfst.evaluate exNfst5 input))+        , TL.testProperty "6" $ \(input :: [D]) -> getAll (foldMap (\x -> All (subresult (L.reverse x) (Dfst.evaluate (Nfst.toDfst exNfst6) input))) (Nfst.evaluate exNfst6 input))+        ]+      ]+    ]+  , testGroup "Dfst"+    [ testGroup "evaluate"+      [ testCase "A" (Dfst.evaluate exDfst1 [D0,D2] @?= Nothing)+      , testCase "B" (Dfst.evaluate exDfst1 [D0,D1] @?= Just (E.fromList [B1,B0]))+      ]+    , testGroup "union"+      [ testGroup "unit"+        [ testCase "A" (let x = Dfst.evaluate (Dfst.union (Dfst.map S.singleton exDfst1) (Dfst.map S.singleton exDfst2)) [D0,D1] in assertBool (show x) (setSubresult [B0, B1] x))+        , testCase "B" (let x = Dfst.evaluate (Dfst.union (Dfst.map S.singleton exDfst1) (Dfst.map S.singleton exDfst2)) [D0,D3] in assertBool (show x) (setSubresult [B0, B0] x))+        ]+      ]+    ]+  ]++subresult :: Ord a => [Set a] -> Maybe (Array (Set a)) -> Bool+subresult xs = \case+  Nothing -> False+  Just ys -> length xs == length ys && all (uncurry S.isSubsetOf) (zip xs (E.toList ys))++setSubresult :: Ord a => [a] -> Maybe (Array (Set a)) -> Bool+setSubresult xs = \case+  Nothing -> False+  Just ys -> length xs == length ys && all (uncurry S.member) (zip xs (E.toList ys))++lawsToTest :: QCC.Laws -> TestTree+lawsToTest (QCC.Laws name pairs) = testGroup name (map (uncurry TQC.testProperty) pairs)++instance Semigroup B where+  (<>) = max++instance Monoid B where+  mempty = minBound++instance (Arbitrary t, Bounded t, Enum t, Ord t) => Arbitrary (Dfsa t) where+  arbitrary = do+    let states = 6+    n <- QC.choose (0,30)+    (ts :: [(Int,Int,t,t)]) <- QC.vectorOf n $ (,,,)+      <$> QC.choose (0,states)+      <*> QC.choose (0,states)+      <*> QC.arbitrary+      <*> QC.arbitrary+    return $ Dfsa.build $ \s0 -> do+      states <- fmap (s0:) (replicateM states Dfsa.state)+      Dfsa.accept (states L.!! 3)+      forM_ ts $ \(source,dest,a,b) -> do+        let lo = min a b+            hi = max a b+        Dfsa.transition lo hi (states L.!! source) (states L.!! dest)++instance (Arbitrary t, Bounded t, Enum t, Ord t) => Arbitrary (Nfsa t) where+  arbitrary = do+    let states = 3+    n <- QC.choose (0,20)+    (ts :: [(Int,Int,t,t,Bool)]) <- QC.vectorOf n $ (,,,,)+      <$> QC.choose (0,states)+      <*> QC.choose (0,states)+      <*> QC.arbitrary+      <*> QC.arbitrary+      <*> QC.frequency [(975,pure False),(25,pure True)]+    return $ B.run $ \s0 -> do+      states <- fmap (s0:) (replicateM states B.state)+      B.accept (states L.!! 1)+      forM_ ts $ \(source,dest,a,b,epsilon) -> do+        let lo = min a b+            hi = max a b+        if epsilon+          then B.epsilon (states L.!! source) (states L.!! dest)+          else B.transition lo hi (states L.!! source) (states L.!! dest)++-- This instance is provided for testing. The library does not provide+-- an Eq instance for Nfsa since there is no efficent algorithm to do this+-- in general.+instance (Ord t, Bounded t, Enum t) => Eq (Nfsa t) where+  a == b = Nfsa.toDfsa a == Nfsa.toDfsa b++ex1 :: Nfsa D+ex1 = B.run $ \s0 -> do+  s1 <- B.state+  B.accept s1+  B.transition D1 D2 s0 s1+  B.transition D0 D0 s0 s0+  B.transition D3 D3 s1 s1++ex2 :: Nfsa D+ex2 = B.run $ \s0 -> do+  s1 <- B.state+  B.accept s1+  B.transition D1 D2 s0 s1+  B.transition D0 D0 s0 s0+  B.transition D3 D3 s0 s0+  B.transition D3 D3 s0 s1+  B.transition D3 D3 s1 s1++ex3 :: Nfsa D+ex3 = B.run $ \s0 -> do+  s1 <- B.state+  s2 <- B.state+  B.accept s2+  B.transition D1 D2 s0 s1+  B.transition D3 D3 s1 s2+  B.transition D2 D3 s1 s0+  B.transition D0 D0 s2 s0+  B.epsilon s2 s1++ex4 :: Nfsa D+ex4 = B.run $ \s0 -> do+  s1 <- B.state+  s2 <- B.state+  B.accept s1+  B.accept s2+  B.transition D1 D2 s0 s1+  B.transition D0 D0 s0 s0+  B.transition D3 D3 s1 s1+  B.transition D1 D2 s0 s2+  B.transition D3 D3 s2 s2++ex5 :: Nfsa D+ex5 = B.run $ \s0 -> do+  s1 <- B.state+  s2 <- B.state+  B.accept s2+  B.transition D0 D1 s0 s1+  B.transition D1 D2 s1 s2++-- Note: ex5 and ex6 accept the same inputs.+ex6 :: Nfsa D+ex6 = B.run $ \s0 -> do+  -- s3, s4, and s5 are unreachable+  s3 <- B.state+  s4 <- B.state+  s5 <- B.state+  s2 <- B.state+  s1 <- B.state+  B.accept s2+  B.transition D0 D1 s0 s1+  B.transition D1 D2 s1 s2+  B.epsilon s3 s4+  B.transition D0 D2 s4 s5+  B.transition D2 D2 s5 s3+  B.transition D1 D2 s5 s3++ex7 :: Nfsa D+ex7 = B.run $ \s0 -> do+  s1 <- B.state+  s2 <- B.state+  s3 <- B.state+  s4 <- B.state+  s5 <- B.state+  B.accept s3+  B.accept s4+  B.transition D0 D0 s0 s1+  B.transition D0 D0 s0 s2+  B.transition D2 D2 s1 s3+  B.transition D0 D0 s1 s4+  B.transition D1 D1 s2 s4+  B.transition D3 D3 s1 s3+  B.transition D3 D3 s2 s5+  B.transition D2 D3 s4 s4+  B.epsilon s4 s5+  B.epsilon s5 s4+++exDfsa1 :: Dfsa D+exDfsa1 = Dfsa.build $ \s0 -> do+  s1 <- Dfsa.state+  Dfsa.accept s1+  Dfsa.transition D0 D1 s0 s1++exDfsa2 :: Dfsa D+exDfsa2 = Dfsa.build $ \s0 -> do+  s1 <- Dfsa.state+  s2 <- Dfsa.state+  Dfsa.accept s2+  Dfsa.transition D0 D3 s0 s1+  Dfsa.transition D1 D2 s0 s2+  Dfsa.transition D2 D3 s1 s1+  Dfsa.transition D2 D2 s1 s2+  Dfsa.transition D3 D3 s2 s2++exNfst1 :: Nfst D B+exNfst1 = Nfst.build $ \s0 -> do+  s1 <- Nfst.state+  Nfst.accept s1+  Nfst.transition D0 D1 B0 s0 s1 +  Nfst.transition D2 D3 B1 s0 s1 +  Nfst.transition D0 D3 B1 s1 s1 ++exNfst2 :: Nfst D B+exNfst2 = Nfst.build $ \s0 -> do+  s1 <- Nfst.state+  s2 <- Nfst.state+  Nfst.epsilon s0 s1+  Nfst.accept s2+  Nfst.transition D0 D1 B0 s0 s1 +  Nfst.transition D2 D3 B1 s0 s1 +  Nfst.transition D0 D0 B0 s1 s2 +  Nfst.transition D1 D3 B1 s1 s1+  Nfst.transition D0 D0 B0 s2 s2+  Nfst.transition D1 D3 B1 s2 s0++exNfst3 :: Nfst D B+exNfst3 = Nfst.build $ \s0 -> do+  s1 <- Nfst.state+  s2 <- Nfst.state+  s3 <- Nfst.state+  s4 <- Nfst.state+  Nfst.accept s3+  Nfst.accept s4+  Nfst.transition D0 D0 B0 s0 s1+  Nfst.transition D0 D0 B1 s0 s2+  Nfst.transition D2 D2 B1 s1 s3+  Nfst.transition D1 D1 B0 s2 s4+  Nfst.transition D3 D3 B0 s1 s3+  Nfst.transition D3 D3 B0 s2 s4++exNfst4 :: Nfst D (Set B)+exNfst4 = Nfst.build $ \s0 -> do+  s1 <- Nfst.state+  s2 <- Nfst.state+  s3 <- Nfst.state+  s4 <- Nfst.state+  s5 <- Nfst.state+  Nfst.accept s3+  Nfst.accept s4+  Nfst.transition D0 D0 (S.singleton B0) s0 s1+  Nfst.transition D0 D0 (S.singleton B1) s0 s2+  Nfst.transition D2 D2 (S.singleton B1) s1 s3+  Nfst.transition D0 D0 (S.singleton B0) s1 s4+  Nfst.transition D1 D1 (S.singleton B0) s2 s4+  Nfst.transition D3 D3 (S.singleton B0) s1 s3+  Nfst.transition D3 D3 (S.singleton B0) s2 s5+  Nfst.transition D2 D3 (S.singleton B1) s4 s4+  Nfst.epsilon s4 s5+  Nfst.epsilon s5 s4++exNfst5 :: Nfst D (Set B)+exNfst5 = Nfst.build $ \s0 -> do+  s1 <- Nfst.state+  s2 <- Nfst.state+  Nfst.accept s2+  Nfst.transition D1 D1 (S.singleton B0) s0 s1+  Nfst.transition D2 D2 (S.singleton B1) s1 s2++exNfst6 :: Nfst D (Set B)+exNfst6 = Nfst.build $ \s0 -> do+  s1 <- Nfst.state+  s2 <- Nfst.state+  s3 <- Nfst.state+  s4 <- Nfst.state+  s5 <- Nfst.state+  s6 <- Nfst.state+  Nfst.epsilon s0 s4+  Nfst.accept s2+  Nfst.accept s6+  Nfst.transition D1 D1 (S.singleton B1) s0 s1+  Nfst.transition D3 D3 (S.singleton B0) s0 s4+  Nfst.transition D2 D2 (S.singleton B1) s1 s2+  Nfst.transition D3 D3 (S.singleton B0) s1 s4+  Nfst.transition D2 D2 (S.singleton B1) s1 s2+  Nfst.transition D0 D1 (S.singleton B0) s4 s6+  Nfst.transition D1 D1 (S.singleton B1) s6 s4+  Nfst.transition D0 D0 (S.singleton B0) s4 s1++exDfst1 :: Dfst D B+exDfst1 = Dfst.build $ \s0 -> do+  s1 <- Dfst.state+  s2 <- Dfst.state+  s3 <- Dfst.state+  s4 <- Dfst.state+  Dfst.accept s3+  Dfst.accept s4+  Dfst.transition D0 D0 B0 s0 s1+  Dfst.transition D0 D0 B1 s0 s2+  Dfst.transition D2 D2 B1 s1 s3+  Dfst.transition D1 D1 B0 s2 s4+  Dfst.transition D3 D3 B0 s1 s3+  Dfst.transition D3 D3 B0 s2 s4++exDfst2 :: Dfst D B+exDfst2 = Dfst.build $ \s0 -> do+  s1 <- Dfst.state+  s2 <- Dfst.state+  Dfst.accept s2+  Dfst.transition D0 D0 B0 s0 s1+  Dfst.transition D1 D1 B1 s1 s2+  Dfst.transition D2 D2 B0 s2 s0++-- This uses s3 as a dead state. So, we are roughly testing+-- all DFA with three nodes, a binary transition function,+-- and a single fixed end state.+mkBinDfsa :: ((D,D),(D,D),(D,D)) -> Dfsa B+mkBinDfsa (ws,xs,ys) = Dfsa.build $ \s0 -> do+  s1 <- Dfsa.state+  s2 <- Dfsa.state+  s3 <- Dfsa.state+  Dfsa.accept s1+  let resolve = \case+        D0 -> s0+        D1 -> s1+        D2 -> s2+        D3 -> s3+      binTransitions (a,b) s = do+        Dfsa.transition B0 B0 s (resolve a)+        Dfsa.transition B1 B1 s (resolve b)+  binTransitions ws s0+  binTransitions xs s1+  binTransitions ys s2+  Dfsa.transition B0 B1 s3 s3+++