diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,3 @@
+# Changelog for automaton
+
+## Unreleased changes
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -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.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,1 @@
+# automaton
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/automata.cabal b/automata.cabal
new file mode 100644
--- /dev/null
+++ b/automata.cabal
@@ -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
diff --git a/src/Automata/Dfsa.hs b/src/Automata/Dfsa.hs
new file mode 100644
--- /dev/null
+++ b/src/Automata/Dfsa.hs
@@ -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 ()
+
diff --git a/src/Automata/Dfst.hs b/src/Automata/Dfst.hs
new file mode 100644
--- /dev/null
+++ b/src/Automata/Dfst.hs
@@ -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
+
+
+
diff --git a/src/Automata/Internal.hs b/src/Automata/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Automata/Internal.hs
@@ -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
diff --git a/src/Automata/Internal/Transducer.hs b/src/Automata/Internal/Transducer.hs
new file mode 100644
--- /dev/null
+++ b/src/Automata/Internal/Transducer.hs
@@ -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)
+
diff --git a/src/Automata/Nfsa.hs b/src/Automata/Nfsa.hs
new file mode 100644
--- /dev/null
+++ b/src/Automata/Nfsa.hs
@@ -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
+
diff --git a/src/Automata/Nfsa/Builder.hs b/src/Automata/Nfsa/Builder.hs
new file mode 100644
--- /dev/null
+++ b/src/Automata/Nfsa/Builder.hs
@@ -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 ()
+
diff --git a/src/Automata/Nfst.hs b/src/Automata/Nfst.hs
new file mode 100644
--- /dev/null
+++ b/src/Automata/Nfst.hs
@@ -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)
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -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
+
+
+