diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,11 @@
+## 0.1
+
+* Drop superclasses from `Kleene`.
+* Rearrange classes. Introduce `CharKleene`, `FiniteKleene`.
+* Add `ToLatin1` and ability to match on `ByteString`.
+* Add `Derivate c (DFA c)` instance.
+* Add `toDot` to output `DFA` to be rendered by *graphviz*.
+* Add `fromRE :: RE c -> ERE c`
+* Add `nullableProof :: RE c -> Maybe (RE c)` which returns non-nullable part
+  of given regular expression.
+* Support/require `lattices-2`: `RE` is now a `Lattice`, `M` isn't.
diff --git a/example.png b/example.png
new file mode 100644
Binary files /dev/null and b/example.png differ
diff --git a/kleene.cabal b/kleene.cabal
--- a/kleene.cabal
+++ b/kleene.cabal
@@ -1,9 +1,8 @@
-cabal-version:  2.0
-name:           kleene
-version:        0
-
-synopsis:       Kleene algebra
-category:       Math
+cabal-version:      1.24
+name:               kleene
+version:            0.1
+synopsis:           Kleene algebra
+category:           Math
 description:
   Kleene algebra
   .
@@ -13,53 +12,57 @@
   Scott Owens, John Reppy and Aaron Turon
   <https://doi.org/10.1017/S0956796808007090>
 
-homepage:       https://github.com/phadej/kleene
-bug-reports:    https://github.com/phadej/kleene/issues
-author:         Oleg Grenrus <oleg.grenrus@iki.fi>
-maintainer:     Oleg Grenrus <oleg.grenrus@iki.fi>
-license:        BSD3
-license-file:   LICENSE
-build-type:     Simple
-
+homepage:           https://github.com/phadej/kleene
+bug-reports:        https://github.com/phadej/kleene/issues
+author:             Oleg Grenrus <oleg.grenrus@iki.fi>
+maintainer:         Oleg Grenrus <oleg.grenrus@iki.fi>
+license:            BSD3
+license-file:       LICENSE
+build-type:         Simple
+extra-source-files: CHANGELOG.md
+extra-doc-files:    example.png
 tested-with:
-  GHC ==7.8.4
-   || ==7.10.3
-   || ==8.0.2
-   || ==8.2.2
-   || ==8.4.2
+  GHC ==7.8.4 || ==7.10.3 || ==8.0.2 || ==8.2.2 || ==8.4.4 || ==8.6.5 || ==8.8.1
 
 source-repository head
-  type: git
+  type:     git
   location: https://github.com/phadej/kleene
 
 library
   -- GHC boot libraries
   build-depends:
-    base                  >=4.7.0.2 && <4.12,
-    containers            >=0.5.5.1 && <0.6,
-    text                  >=1.2.3.0 && <1.3,
-    transformers          >=0.3.0.0 && <0.6
+      base          >=4.7.0.2  && <4.13
+    , bytestring    >=0.10.4.0 && <0.11
+    , containers    >=0.5.5.1  && <0.7
+    , text          >=1.2.3.0  && <1.3
+    , transformers  >=0.3.0.0  && <0.6
 
+  if !impl(ghc >=8.0)
+    build-depends: semigroups >=0.18.5 && <0.19
+
   -- Other dependencies
   build-depends:
-    base-compat-batteries >=0.10.1  && <0.11,
-    lattices              >=1.7.1   && <1.8,
-    MemoTrie              >=0.6.9   && <0.7,
-    range-set-list        >=0.1.3   && <0.2,
-    step-function         >=0.2     && <0.3,
-    regex-applicative     >=0.3.3   && <0.4,
-    QuickCheck            >=2.11.3  && <2.12
+      attoparsec
+    , base-compat        >=0.10.5   && <0.11
+    , lattices           >=2        && <2.1
+    , MemoTrie           >=0.6.9    && <0.7
+    , QuickCheck         >=2.12.6.1 && <2.13
+    , range-set-list     >=0.1.3    && <0.2
+    , regex-applicative  >=0.3.3    && <0.4
+    , semigroupoids      >=5.3.2    && <5.4
+    , step-function      >=0.2      && <0.3
 
   other-extensions:
     CPP
-    DeriveFunctor
+    DefaultSignatures
     DeriveFoldable
+    DeriveFunctor
     DeriveTraversable
-    GADTs
-    OverloadedStrings
     FlexibleInstances
     FunctionalDependencies
+    GADTs
     GeneralizedNewtypeDeriving
+    OverloadedStrings
     StandaloneDeriving
     UndecidableInstances
 
@@ -70,6 +73,7 @@
     Kleene.ERE
     Kleene.Equiv
     Kleene.Functor
+    Kleene.Functor.NonEmpty
     Kleene.Monad
     Kleene.RE
 
@@ -79,6 +83,10 @@
     Kleene.Internal.Pretty
     Kleene.Internal.Sets
 
-  ghc-options: -Wall
-  hs-source-dirs: src
+  other-modules:
+    Kleene.Internal.Functor
+    Kleene.Internal.RE
+
+  ghc-options:      -Wall
+  hs-source-dirs:   src
   default-language: Haskell2010
diff --git a/src/Kleene.hs b/src/Kleene.hs
--- a/src/Kleene.hs
+++ b/src/Kleene.hs
@@ -25,7 +25,8 @@
 --
 -- We can convert it to 'DFA' (there are 8 states)
 --
--- >>> putPretty $ fromTM re
+-- >>> let dfa = fromTM re
+-- >>> putPretty dfa
 -- 0 -> \x -> if
 --     | x <= '`'  -> 8
 --     | x <= 'a'  -> 5
@@ -40,9 +41,18 @@
 -- 2 -> ...
 -- ...
 --
+-- It's also possible to graphically visualise DFAs
+--
+-- @
+-- λ> writeFile "example.dot' ('toDot' dfa)
+-- %  dot -Tpng -oexample.png example.dot
+-- @
+--
+-- ![example.png](example.png)
+--
 -- And we can convert back from 'DFA' to 'RE':
 --
--- >>> let re' = toKleene (fromTM re) :: RE Char
+-- >>> let re' = toKleene dfa :: RE Char
 -- >>> putPretty re'
 -- ^(a(bca)*bcdefx|defx|(a(bca)*bcdefy|defy)z)$
 --
@@ -134,7 +144,7 @@
     RE,
     ERE,
 
-    -- * Equivalance (and partial order)
+    -- * Equivalence (and partial order)
     Equiv (..),
 
     -- * Deterministic finite automaton
@@ -142,6 +152,7 @@
     fromTM,
     fromTMEquiv,
     toKleene,
+    toDot,
 
     -- * Classes
     --
@@ -149,10 +160,13 @@
     --
     -- See "Kleene.RE" module for a specific version with examples.
     Kleene (..),
+    CharKleene (..),
+    FiniteKleene (..),
     Derivate (..),
     Match (..),
     TransitionMap (..),
     Complement (..),
+    ToLatin1 (..),
 
     -- * Functor
     --
@@ -163,7 +177,7 @@
     ) where
 
 import Kleene.Classes
-import Kleene.DFA     (DFA (..), fromTM, fromTMEquiv, toKleene)
+import Kleene.DFA     (DFA (..), fromTM, fromTMEquiv, toDot, toKleene)
 import Kleene.Equiv
 import Kleene.ERE     (ERE)
 import Kleene.Functor (K)
diff --git a/src/Kleene/Classes.hs b/src/Kleene/Classes.hs
--- a/src/Kleene/Classes.hs
+++ b/src/Kleene/Classes.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE DefaultSignatures      #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE GADTs                  #-}
 module Kleene.Classes where
@@ -5,42 +6,54 @@
 import Prelude ()
 import Prelude.Compat
 
-import Algebra.Lattice                    (BoundedJoinSemiLattice (..), joins)
+import Data.Char                          (ord)
 import Data.Foldable                      (toList)
 import Data.Function.Step.Discrete.Closed (SF)
 import Data.Map                           (Map)
+import Data.Maybe                         (mapMaybe)
 import Data.RangeSet.Map                  (RSet)
+import Data.Word                          (Word8)
 
+import qualified Data.ByteString   as BS
+import qualified Data.RangeSet.Map as RSet
+
 import Kleene.Internal.Sets (dotRSet)
 
-class (BoundedJoinSemiLattice k, Semigroup k, Monoid k) => Kleene c k | k -> c where
+-- | Kleene algebra.
+--
+-- If 'k' is 'Monoid' it's expected that @'appends' = 'mappend'@;
+-- if 'k' is 'Algebra.Lattice.Lattice' it's expected that @'unions' = 'Algebra.Lattice.joins'@.
+--
+-- [Wikipedia: Kleene Algebra](https://en.wikipedia.org/wiki/Kleene_algebra).
+--
+class Kleene k where
     -- | Empty regex. Doesn't accept anything.
     empty :: k
-    empty = bottom
 
-    -- | Empty string. /Note:/ different than 'empty'
+    -- | Empty string. /Note:/ different than 'empty'.
     eps :: k
-    eps = mempty
 
-    -- | Single character
-    char :: c -> k
-
     -- | Concatenation.
     appends :: [k] -> k
-    appends = mconcat
 
     -- | Union.
     unions :: [k] -> k
-    unions = joins
 
-    -- | Kleene star
+    -- | Kleene star.
     star :: k -> k
 
+class Kleene k => CharKleene c k | k -> c where
+    -- | Single character
+    char :: c -> k
+
+    string :: [c] -> k
+    string = appends . map char
+
 -- | One of the characters.
-oneof :: (Kleene c k, Foldable f) => f c -> k
+oneof :: (CharKleene c k, Foldable f) => f c -> k
 oneof = unions . map char . toList
 
-class Kleene c k => FiniteKleene c k | k -> c where
+class CharKleene c k => FiniteKleene c k | k -> c where
     -- | Everything. \(\Sigma^\star\).
     everything :: k
     everything = star anyChar
@@ -51,13 +64,17 @@
     -- | Generalisation of 'charRange'.
     fromRSet :: RSet c -> k
 
-    -- | @.$. Every character except new line @\\n@.
+    -- | @.@ Every character except new line @\\n@.
     dot :: c ~ Char => k
     dot = fromRSet dotRSet
 
-    -- | Any character. /Note:/ different than dot!
+    -- | Any character. /Note:/ different than 'dot'!
     anyChar :: k
 
+    notChar :: c -> k
+    default notChar :: (Ord c, Enum c, Bounded c) => c -> k
+    notChar = fromRSet . RSet.complement . RSet.singleton
+
 class Derivate c k | k -> c where
     -- | Does language contain an empty string?
     nullable :: k -> Bool
@@ -69,12 +86,15 @@
 class Match c k | k -> c where
     match :: k -> [c] -> Bool
 
--- | Equivalence induced by 'Matches'.
+    match8 :: c ~ Word8 => k -> BS.ByteString -> Bool
+    match8 k = match k . BS.unpack
+
+-- | Equivalence induced by 'Match'.
 --
 -- /Law:/
 --
 -- @
--- 'equivalent' re1 re2 <=> forall s. 'matches' re1 s == 'matches' re1 s
+-- 'equivalent' re1 re2 <=> forall s. 'match' re1 s == 'match' re1 s
 -- @
 --
 class Match c k => Equivalent c k | k -> c  where
@@ -89,7 +109,17 @@
 -- /Law:/
 --
 -- @
--- 'matches' ('complement' f) xs = 'not' ('matches' f) xs
+-- 'match' ('complement' f) xs = 'not' ('match' f) xs
 -- @
 class Complement c k | k -> c where
     complement :: k -> k
+
+class ToLatin1 k where
+    toLatin1 :: k Char -> k Word8
+
+instance ToLatin1 RSet where
+    toLatin1 = RSet.fromRangeList . mapMaybe f . RSet.toRangeList where
+        f :: (Char, Char) -> Maybe (Word8, Word8)
+        f (a, b)
+            | ord a >= 256 = Nothing
+            | otherwise    = Just (fromIntegral (ord a), fromIntegral (min 255 (ord b)))
diff --git a/src/Kleene/DFA.hs b/src/Kleene/DFA.hs
--- a/src/Kleene/DFA.hs
+++ b/src/Kleene/DFA.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE GADTs                  #-}
 {-# LANGUAGE Safe                   #-}
 {-# LANGUAGE ScopedTypeVariables    #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
 module Kleene.DFA (
     DFA (..),
     -- * Conversions
@@ -14,12 +15,15 @@
     fromTM,
     fromTMEquiv,
     toKleene,
+    toDot,
+    toDot',
     ) where
 
 import Prelude ()
 import Prelude.Compat
 
-import Algebra.Lattice   ((\/))
+import Algebra.Lattice
+       (BoundedJoinSemiLattice (..), BoundedMeetSemiLattice (..), Lattice (..))
 import Data.IntMap       (IntMap)
 import Data.IntSet       (IntSet)
 import Data.List         (intercalate)
@@ -27,9 +31,10 @@
 import Data.Maybe        (fromMaybe)
 import Data.RangeSet.Map (RSet)
 
+import qualified Data.ByteString                    as BS
 import qualified Data.Function.Step.Discrete.Closed as SF
-import qualified Data.IntMap                        as IM
-import qualified Data.IntSet                        as IS
+import qualified Data.IntMap                        as IntMap
+import qualified Data.IntSet                        as IntSet
 import qualified Data.Map                           as Map
 import qualified Data.MemoTrie                      as MT
 import qualified Data.RangeSet.Map                  as RSet
@@ -37,15 +42,15 @@
 import           Kleene.Classes
 import qualified Kleene.ERE             as ERE
 import           Kleene.Internal.Pretty
-import qualified Kleene.RE              as RE
+import qualified Kleene.Internal.RE     as RE
 
 -- | Deterministic finite automaton.
 --
 -- A deterministic finite automaton (DFA) over an alphabet \(\Sigma\) (type
 -- variable @c@) is 4-tuple \(Q\), \(q_0\) , \(F\), \(\delta\), where
 --
--- * \(Q\) is a finite set of states (subset of 'Int'),
--- * \(q_0 \in Q\) is the distinguised start state (@0@),
+-- * \(Q\) is a finite set of states (subset of 's'),
+-- * \(q_0 \in Q\) is the distinguised start state ('dfaInitial'),
 -- * \(F \subset Q\) is a set of final (or  accepting) states ('dfaAcceptable'), and
 -- * \(\delta : Q \times \Sigma \to Q\) is a function called the state
 -- transition function ('dfaTransition').
@@ -53,6 +58,8 @@
 data DFA c = DFA
     { dfaTransition   :: !(IntMap (SF.SF c Int))
       -- ^ transition function
+    , dfaInitial      :: !Int
+      -- ^ initial state
     , dfaAcceptable   :: !IntSet
       -- ^ accept states
     , dfaBlackholes   :: !IntSet
@@ -112,15 +119,15 @@
 
 -- | Convert 'ERE.ERE' to 'DFA'.
 --
--- We don't always generate minimal automata:
+-- We don't always generate a minimal automata:
 --
 -- >>> putPretty $ fromERE $ "a" /\ "b"
 -- 0 -> \_ -> 1
 -- 1 -> \_ -> 1 -- black hole
 --
--- Compare this to an @complement@ example
+-- Compare this to a 'complement' example
 --
--- Using 'fromTMEquiv', we can get minimal automaton, for the cost of higher
+-- Using 'fromTMEquiv', we can get a minimal automaton, for the cost of higher
 -- complexity (slow!).
 --
 -- >>> putPretty $ fromTMEquiv $ ("a" /\ "b" :: ERE.ERE Char)
@@ -163,7 +170,8 @@
     -> DFA c
 fromTMImpl mequiv re = DFA
     { dfaTransition = transition
-    , dfaAcceptable = IS.fromList
+    , dfaInitial    = 0
+    , dfaAcceptable = IntSet.fromList
         [ i
         | (re', i) <- Map.toList lookupMap
         , nullable re'
@@ -171,16 +179,16 @@
     , dfaBlackholes = blackholes
     }
   where
-    transition = IM.fromList
+    transition = IntMap.fromList
         [ (i, js)
         | (re', pm) <- Map.toList tm
         , let i  = fromMaybe 0 $ Map.lookup re' lookupMap
         , let js = SF.normalise $ fmap (\re'' -> fromMaybe 0 $ Map.lookup re'' lookupMap) pm
         ]
 
-    blackholes = IS.fromList
+    blackholes = IntSet.fromList
         [ i
-        | (i, sf) <- IM.toList transition
+        | (i, sf) <- IntMap.toList transition
         , sf == pure i
         ]
 
@@ -289,11 +297,11 @@
 -- See <https://mathoverflow.net/questions/45149/can-regular-expressions-be-made-unambiguous>
 -- for the description of the algorithm used.
 --
-toRE :: forall c. (Ord c, Enum c, Bounded c) => DFA c -> RE.RE c
+toRE :: (Ord c, Enum c, Bounded c) => DFA c -> RE.RE c
 toRE = toKleene
 
 -- | Convert 'DFA' to 'ERE.ERE'.
-toERE :: forall c. (Ord c, Enum c, Bounded c) => DFA c -> ERE.ERE c
+toERE :: (Ord c, Enum c, Bounded c) => DFA c -> ERE.ERE c
 toERE = toKleene
 
 -- | Convert to any 'Kleene'.
@@ -301,13 +309,13 @@
 -- See 'toRE' for a specific example.
 --
 toKleene :: forall k c. (Ord c, Enum c, Bounded c, FiniteKleene c k) => DFA c -> k
-toKleene (DFA tr acc _) = unions
-    [ re 0 j maxN
-    | j <- IS.toList acc
+toKleene (DFA tr ini acc _) = unions
+    [ re ini j maxN
+    | j <- IntSet.toList acc
     ]
   where
-    maxN | IM.null tr = 1
-         | otherwise = succ $ fst $ IM.findMax tr
+    maxN | IntMap.null tr = 1
+         | otherwise      = succ $ fst $ IntMap.findMax tr
 
     {-
     -- this is useful for debug
@@ -321,8 +329,8 @@
 
     re i j k = MT.memo re' (i, j, k)
     re' (i, j, k)
-        | k <= 0    = if i == j then eps \/ r else r
-        | otherwise = re i j k' \/ (re i k' k' <> star (re k' k' k') <> re k' j k')
+        | k <= 0    = if i == j then unions [eps, r] else r
+        | otherwise = unions [re i j k', appends [re i k' k', star (re k' k' k'), re k' j k']]
       where
         r = maybe empty fromRSet $ Map.lookup (i, j) re0map
         k' = k - 1
@@ -330,7 +338,7 @@
     re0map :: Map (Int, Int) (RSet c)
     re0map = Map.fromListWith RSet.union
         [ ((i, j), RSet.singletonRange (lo, hi))
-        | (i, tr') <- IM.toList tr
+        | (i, tr') <- IntMap.toList tr
         , (lo, hi, j) <- toPieces tr'
         ]
 
@@ -350,7 +358,7 @@
 
 -- | Run 'DFA' on the input.
 --
--- Because we have analysed a language, in some cases we can determine an input
+-- Because we have analysed a language, in some cases we can determine a result
 -- without traversing all of the input.
 -- That's not the cases with 'RE.RE' 'match'.
 --
@@ -367,13 +375,21 @@
 -- prop> all (match (fromRE r)) $ take 10 $ RE.generate (curry QC.choose) 42 (r :: RE.RE Char)
 --
 instance Ord c => Match c (DFA c) where
-    match (DFA tr acc bh) = go (0 :: Int) where
-        go s _ | IS.member s bh = IS.member s acc
-        go s []                 = IS.member s acc
-        go s (c : cs)           = case IM.lookup s tr of
+    match (DFA tr i acc bh) = go i where
+        go !s _ | IntSet.member s bh = IntSet.member s acc
+        go !s []                 = IntSet.member s acc
+        go !s (c : cs)           = case IntMap.lookup s tr of
             Nothing -> False
             Just sf -> go (sf SF.! c) cs
 
+    match8 (DFA tr i acc bh) = go i where
+        go !s !_ | IntSet.member s bh = IntSet.member s acc
+        go !s bs = case BS.uncons bs of
+            Nothing      -> IntSet.member s acc
+            Just (c, cs) -> case IntMap.lookup s tr of
+                Nothing -> False
+                Just sf -> go (sf SF.! c) cs
+
 -- | Complement DFA.
 --
 -- Complement of 'DFA' is way easier than of 'RE.RE': complement accept states.
@@ -398,19 +414,132 @@
 -- [False,False,False,True,True,True]
 --
 instance Complement c (DFA c) where
-    complement (DFA tr acc err) = DFA tr acc' err where
-        acc' = IS.difference (IM.keysSet tr) acc
+    complement (DFA tr ini acc bh) = DFA tr ini acc' bh where
+        acc' = IntSet.difference (IntMap.keysSet tr) acc
 
+instance Ord c => Derivate c (DFA c) where
+    nullable (DFA _tr ini acc _bh) = IntSet.member ini acc
+
+    derivate c (DFA tr ini acc bh) = DFA tr ini' acc bh where
+        ini' = case IntMap.lookup ini tr of
+            Nothing -> ini -- in error case let's just stay in the same state.
+            Just sf -> sf SF.! c
+
 -------------------------------------------------------------------------------
+-- toDot
+-------------------------------------------------------------------------------
+
+-- | Get Graphviz dot-code of DFA.
+--
+-- >>> let dfa = fromRE $ RE.star "abc"
+-- >>> putStr $ toDot dfa
+-- digraph dfa {
+-- rankdir=LR;
+-- // states
+-- "0" [shape=doublecircle];
+-- "1" [shape=circle];
+-- "2" [shape=circle];
+-- // initial state
+-- "" [shape=none];
+-- "" -> "0";
+-- // transitions
+-- "0" -> "2"[label="a"]
+-- "1" -> "0"[label="c"]
+-- "2" -> "1"[label="b"]
+-- }
+--
+toDot :: DFA Char -> String
+toDot = toDot' show pure
+
+-- | More flexible version of 'toDot'.
+toDot' :: (Ord c, Enum c, Bounded c) => (Int -> String) -> (c -> String) -> DFA c -> String
+toDot' showS showC (DFA tr ini acc bh)
+    = showString "digraph dfa {\n"
+    . showString "rankdir=LR;\n"
+    . showString "// states\n"
+    . showStates
+    . showString "// initial state\n"
+    . showInitial
+    . showString "// transitions\n"
+    . showTransitions
+    . showString "}\n"
+    $ ""
+  where
+    showStates  = foldr (.) id
+        [ showState i
+        | i <- IntMap.keys tr
+        , IntSet.member i acc || IntSet.notMember i bh
+        ]
+    showState s = showS' s . shape where
+        shape
+            | IntSet.member s acc = showString " [shape=doublecircle];\n"
+            | otherwise        = showString " [shape=circle];\n"
+
+    showInitial
+        = showString "\"\" [shape=none];\n"
+        . showString "\"\" -> "
+        . showS' ini
+        . showString ";\n"
+
+    showTransitions = foldr (.) id
+        [ showS' i
+        . showString " -> "
+        . showS' j
+        . showString "[label="
+        . label
+                . showString "]\n"
+        | (i, sf) <- IntMap.toList tr
+        , (lo, hi, j) <- toPieces sf
+        , IntSet.member j acc || IntSet.notMember j bh
+        , let label
+                | lo == hi
+                    = shows (showC lo)
+                | lo == minBound && hi == maxBound
+                    = shows ("-any" :: String)
+                | otherwise
+                    = shows (showC lo ++ "-" ++ showC hi)
+        ]
+
+    showS' = shows . showS
+
+-------------------------------------------------------------------------------
+-- Orphans
+-------------------------------------------------------------------------------
+
+-- | __WARNING__: The '/\' is inefficient, it actually computes the conjunction:
+--
+-- >>> putPretty $ asREChar $ "a" /\ "b"
+-- ^[]$
+--
+-- >>> putPretty $ asREChar $ "a" /\ star "a"
+-- ^a$
+--
+-- >>> putPretty $ asREChar $ star "aa" /\ star "aaa"
+-- ^(a(aaaaaa)*aaaaa)?$
+--
+instance (Ord c, Enum c, Bounded c) => Lattice (RE.RE c) where
+    r /\ r' = toRE $ fromERE $ ERE.fromRE r /\ ERE.fromRE r'
+    r \/ r' = unions [r, r']
+
+instance (Ord c, Enum c, Bounded c) => BoundedJoinSemiLattice (RE.RE c) where
+    bottom = empty
+
+instance (Ord c, Enum c, Bounded c) => BoundedMeetSemiLattice (RE.RE c) where
+    top = RE.REStar (RE.REChars RSet.full)
+
+instance (Ord c, Enum c, Bounded c) => Complement c (RE.RE c) where
+    complement = toRE . complement . fromRE
+
+-------------------------------------------------------------------------------
 -- Debug
 -------------------------------------------------------------------------------
 
 instance Show c => Pretty (DFA c) where
     pretty dfa = intercalate "\n"
         [ show i ++ acc ++ " -> " ++ SF.showSF sf ++ bh
-        | (i, sf) <- IM.toList (dfaTransition dfa)
-        , let acc = if IS.member i (dfaAcceptable dfa) then "+" else ""
-        , let bh = if IS.member i $ dfaBlackholes dfa then " -- black hole" else ""
+        | (i, sf) <- IntMap.toList (dfaTransition dfa)
+        , let acc = if IntSet.member i (dfaAcceptable dfa) then "+" else ""
+        , let bh = if IntSet.member i $ dfaBlackholes dfa then " -- black hole" else ""
         ]
 
 -- $setup
@@ -424,3 +553,5 @@
 -- >>> newtype Smaller a = Smaller a deriving (Show)
 -- >>> let intLog2 = (`div` 10)
 -- >>> instance QC.Arbitrary a => QC.Arbitrary (Smaller a) where arbitrary = QC.scale intLog2 QC.arbitrary; shrink (Smaller a) = map Smaller (QC.shrink a)
+--
+-- >>> let asREChar :: RE.RE Char -> RE.RE Char; asREChar = id
diff --git a/src/Kleene/ERE.hs b/src/Kleene/ERE.hs
--- a/src/Kleene/ERE.hs
+++ b/src/Kleene/ERE.hs
@@ -28,6 +28,8 @@
     -- * Derivative
     nullable,
     derivate,
+    -- * Conversion
+    fromRE,
     -- * Transition map
     transitionMap,
     leadingChars,
@@ -38,13 +40,12 @@
     isEverything,
     ) where
 
+import Data.Semigroup (Semigroup (..))
 import Prelude ()
 import Prelude.Compat
 
 import Algebra.Lattice
-       (BoundedJoinSemiLattice (..), BoundedLattice,
-       BoundedMeetSemiLattice (..), JoinSemiLattice (..), Lattice,
-       MeetSemiLattice (..))
+       (BoundedJoinSemiLattice (..), BoundedMeetSemiLattice (..), Lattice (..))
 import Control.Applicative (liftA2)
 import Data.Foldable       (toList)
 import Data.List           (foldl')
@@ -62,6 +63,7 @@
 import qualified Kleene.Classes            as C
 import qualified Kleene.Internal.Partition as P
 import           Kleene.Internal.Pretty
+import qualified Kleene.Internal.RE        as RE
 
 -- | Extended regular expression
 --
@@ -85,6 +87,18 @@
   deriving (Eq, Ord, Show)
 
 -------------------------------------------------------------------------------
+-- fromRE
+-------------------------------------------------------------------------------
+
+-- | Convert from ordinary regular expression, 'RE.RE'.
+--
+fromRE :: Ord c => RE.RE c -> ERE c
+fromRE (RE.REChars rs)   = EREChars rs
+fromRE (RE.REAppend rs)  = EREAppend (map fromRE rs)
+fromRE (RE.REUnion r rs) = EREUnion r (Set.map fromRE rs)
+fromRE (RE.REStar r)     = EREStar (fromRE r)
+
+-------------------------------------------------------------------------------
 -- Smart constructor
 -------------------------------------------------------------------------------
 
@@ -182,8 +196,8 @@
 -- prop> empty \/ asEREChar r === r
 -- prop> asEREChar r \/ empty === r
 --
--- prop> everything \/ asREChar r === everything
--- prop> asREChar r \/ everything === everything
+-- prop> everything \/ asEREChar r === everything
+-- prop> asEREChar r \/ everything === everything
 --
 unions :: (Ord c, Enum c) => [ERE c] -> ERE c
 unions = uncurry mk . foldMap f where
@@ -209,8 +223,8 @@
 -- prop> empty /\ asEREChar r === empty
 -- prop> asEREChar r /\ empty === empty
 --
--- prop> everything /\ asREChar r === r
--- prop> asREChar r /\ everything === r
+-- prop> everything /\ asEREChar r === r
+-- prop> asEREChar r /\ everything === r
 --
 intersections :: (Ord c, Enum c) => [ERE c] -> ERE c
 intersections = complement . unions . map complement
@@ -232,7 +246,7 @@
 -- prop> star empty   === asEREChar eps
 -- prop> star anyChar === asEREChar everything
 --
--- prop> star (asREChar r \/ eps) === star r
+-- prop> star (asEREChar r \/ eps) === star r
 -- prop> star (char c \/ eps) === star (char (c :: Char))
 -- prop> star (empty \/ eps) === eps
 --
@@ -263,14 +277,16 @@
 string [c] = EREChars (RSet.singleton c)
 string cs  = EREAppend $ map (EREChars . RSet.singleton) cs
 
-instance (Ord c, Enum c, Bounded c) => C.Kleene c (ERE c) where
+instance (Ord c, Enum c, Bounded c) => C.Kleene (ERE c) where
     empty      = empty
     eps        = eps
-    char       = char
     appends    = appends
     unions     = unions
     star       = star
 
+instance (Ord c, Enum c, Bounded c) => C.CharKleene c (ERE c) where
+    char       = char
+
 instance (Ord c, Enum c, Bounded c) => C.FiniteKleene c (ERE c) where
     everything = everything
     charRange  = charRange
@@ -508,21 +524,16 @@
     mappend = (<>)
     mconcat = appends
 
-instance (Ord c, Enum c) => JoinSemiLattice (ERE c) where
+instance (Ord c, Enum c) => Lattice (ERE c) where
     r \/ r' = unions [r, r']
+    r /\ r' = intersections [r, r']
 
 instance (Ord c, Enum c) => BoundedJoinSemiLattice (ERE c) where
     bottom = empty
 
-instance (Ord c, Enum c) => MeetSemiLattice (ERE c) where
-    r /\ r' = intersections [r, r']
-
 instance (Ord c, Enum c) => BoundedMeetSemiLattice (ERE c) where
     top = everything
 
-instance  (Ord c, Enum c) => Lattice (ERE c)
-instance  (Ord c, Enum c) => BoundedLattice (ERE c)
-
 instance c ~ Char => IsString (ERE c) where
     fromString = string
 
@@ -592,6 +603,17 @@
         parens :: Bool -> ShowS -> ShowS
         parens True  s = showString "(" . s . showChar ')'
         parens False s = s
+
+-------------------------------------------------------------------------------
+-- Latin1
+-------------------------------------------------------------------------------
+
+instance C.ToLatin1 ERE where
+    toLatin1 (EREChars rs)    = C.fromRSet (C.toLatin1 rs)
+    toLatin1 (EREAppend xs)   = appends (map C.toLatin1 xs)
+    toLatin1 (EREUnion rs xs) = C.fromRSet (C.toLatin1 rs) \/ unions (map C.toLatin1 (Set.toList  xs))
+    toLatin1 (EREStar r)      = star (C.toLatin1 r)
+    toLatin1 (ERENot r)       = complement (C.toLatin1 r)
 
 -------------------------------------------------------------------------------
 -- Doctest
diff --git a/src/Kleene/Equiv.hs b/src/Kleene/Equiv.hs
--- a/src/Kleene/Equiv.hs
+++ b/src/Kleene/Equiv.hs
@@ -10,12 +10,12 @@
 import Prelude ()
 import Prelude.Compat
 
-import Algebra.Lattice
-       (BoundedJoinSemiLattice (..), JoinSemiLattice (..), joinLeq)
+import Algebra.Lattice    (BoundedJoinSemiLattice (..), BoundedMeetSemiLattice (..), Lattice (..), joinLeq)
 import Algebra.PartialOrd (PartialOrd (..))
+import Data.Semigroup     (Semigroup (..))
 
 import Kleene.Classes
-import           Kleene.Internal.Pretty
+import Kleene.Internal.Pretty
 
 -- | Regular-expressions for which '==' is 'equivalent'.
 --
@@ -41,16 +41,17 @@
 -- (False,False)
 --
 newtype Equiv r c = Equiv (r c)
-  deriving (Show, Semigroup, Monoid, BoundedJoinSemiLattice, JoinSemiLattice, Pretty)
+  deriving (Show, Semigroup, Monoid, BoundedJoinSemiLattice, BoundedMeetSemiLattice, Lattice, Pretty)
 
 instance Equivalent c (r c) => Eq (Equiv r c) where
     (==) = equivalent
 
 -- | \(a \preceq b := a \lor b = b \)
-instance (JoinSemiLattice (r c), Equivalent c (r c)) => PartialOrd (Equiv r c) where
+instance (Lattice (r c), Equivalent c (r c)) => PartialOrd (Equiv r c) where
     leq = joinLeq
 
-deriving instance Kleene     c (r c) => Kleene     c (Equiv r c)
+deriving instance Kleene       (r c) => Kleene       (Equiv r c)
+deriving instance CharKleene c (r c) => CharKleene c (Equiv r c)
 deriving instance Derivate   c (r c) => Derivate   c (Equiv r c)
 deriving instance Match      c (r c) => Match      c (Equiv r c)
 deriving instance Equivalent c (r c) => Equivalent c (Equiv r c)
diff --git a/src/Kleene/Functor.hs b/src/Kleene/Functor.hs
--- a/src/Kleene/Functor.hs
+++ b/src/Kleene/Functor.hs
@@ -1,5 +1,3 @@
-{-# LANGUAGE CPP   #-}
-{-# LANGUAGE GADTs #-}
 {-# LANGUAGE Safe  #-}
 module Kleene.Functor (
     K,
@@ -25,249 +23,4 @@
     toRA,
     ) where
 
-import Prelude ()
-import Prelude.Compat
-
-import Algebra.Lattice     ((\/))
-import Control.Applicative (Alternative (..), liftA2)
-import Data.Foldable       (toList)
-import Data.RangeSet.Map   (RSet)
-import Data.String         (IsString (..))
-
-import qualified Data.RangeSet.Map      as RSet
-import qualified Text.Regex.Applicative as R
-
-import qualified Kleene.Classes         as C
-import           Kleene.Internal.Pretty
-import           Kleene.Internal.Sets
-import qualified Kleene.RE              as RE
-
--- | Star behaviour
-data Greediness
-    = Greedy    -- ^ 'many'
-    | NonGreedy -- ^ 'few'
-  deriving (Eq, Ord, Show, Enum, Bounded)
-
--- | 'Applicative' 'Functor' regular expression.
-data K c a where
-    KEmpty  :: K c a
-    KPure   :: a -> K c a
-    KChar   :: (Ord c, Enum c) => RSet c -> K c c
-    KAppend :: (a -> b -> r) -> K c a -> K c b -> K c r
-    KUnion  :: K c a -> K c a -> K c a
-    KStar   :: Greediness -> K c a -> K c [a]
-
-    -- optimisations
-    KMap    :: (a -> b) -> K c a -> K c b -- could use Pure and Append
-    KString :: Eq c => [c] -> K c [c]     -- could use Char and Append
-
-instance (c ~ Char, IsString a) => IsString (K c a) where
-    fromString s = KMap fromString (KString s)
-
-instance Functor (K c) where
-    fmap _ KEmpty          = KEmpty
-    fmap f (KPure x)       = KPure (f x)
-    fmap f (KMap g k)      = KMap (f . g) k
-    fmap f (KAppend g a b) = KAppend (\x y -> f (g x y)) a b
-    fmap f k                    = KMap f k
-
-instance Applicative (K c) where
-    pure = KPure
-
-    KEmpty <*> _ = KEmpty
-    _ <*> KEmpty = KEmpty
-
-    KPure f <*> k = fmap f k
-    k <*> KPure x = fmap ($ x) k
-
-    f <*> x = KAppend ($) f x
-
-#if MIN_VERSION_base(4,10,0)
-    liftA2 = KAppend
-#endif
-
-instance Alternative (K c) where
-    empty = KEmpty
-
-    KEmpty <|> k = k
-    k <|> KEmpty = k
-    KChar a <|> KChar b = KChar (RSet.union a b)
-
-    a <|> b = KUnion a b
-
-    many KEmpty      = KPure []
-    many (KStar _ k) = KMap pure (KStar Greedy k)
-    many k           = KStar Greedy k
-
-    some KEmpty      = KEmpty
-    some (KStar _ k) = KMap pure (KStar Greedy k)
-    some k           = liftA2 (:) k (KStar Greedy k)
-
--- | 'few', not 'many'.
---
--- Let's define two similar regexps
---
--- >>> let re1 = liftA2 (,) (few  $ char 'a') (many $ char 'a')
--- >>> let re2 = liftA2 (,) (many $ char 'a') (few  $ char 'a')
---
--- Their 'RE' behaviour is the same:
---
--- >>> C.equivalent (toRE re1) (toRE re2)
--- True
---
--- >>> map (C.match $ toRE re1) ["aaa","bbb"]
--- [True,False]
---
--- However, the 'RA' behaviour is different!
---
--- >>> R.match (toRA re1) "aaaa"
--- Just ("","aaaa")
---
--- >>> R.match (toRA re2) "aaaa"
--- Just ("aaaa","")
---
-few :: K c a -> K c [a]
-few KEmpty      = KPure []
-few (KStar _ k) = KMap pure (KStar NonGreedy k)
-few k           = KStar NonGreedy k
-
--------------------------------------------------------------------------------
---
--------------------------------------------------------------------------------
-
--- | >>> putPretty anyChar
--- ^[^]$
-anyChar :: (Ord c, Enum c, Bounded c) => K c c
-anyChar = KChar RSet.full
-
--- | >>> putPretty $ oneof ("foobar" :: [Char])
--- ^[a-bfor]$
-oneof :: (Ord c, Enum c, Foldable f) => f c -> K c c
-oneof = KChar . RSet.fromList . toList
-
--- | >>> putPretty $ char 'x'
--- ^x$
-char :: (Ord c, Enum c) => c -> K c c
-char = KChar . RSet.singleton
-
--- | >>> putPretty $ charRange 'a' 'z'
--- ^[a-z]$
-charRange :: (Enum c, Ord c) => c -> c -> K c c
-charRange a b = KChar (RSet.singletonRange (a, b))
-
--- | >>> putPretty dot
--- ^.$
-dot :: K Char Char
-dot = KChar dotRSet
-
--- | >>> putPretty everything
--- ^[^]*$
-everything :: (Ord c, Enum c, Bounded c) => K c [c]
-everything = many anyChar
-
--- | >>> putPretty everything1
--- ^[^][^]*$
-everything1 :: (Ord c, Enum c, Bounded c) => K c [c]
-everything1 = some anyChar
-
--- | Matches nothing?
-isEmpty :: (Ord c, Enum c, Bounded c) => K c a -> Bool
-isEmpty k = C.equivalent (toRE k) C.empty
-
--- | Matches whole input?
-isEverything :: (Ord c, Enum c, Bounded c) => K c a -> Bool
-isEverything k = C.equivalent (toRE k) C.everything
-
--------------------------------------------------------------------------------
--- Matching
--------------------------------------------------------------------------------
-
--- | Match using @regex-applicative@
-match :: K c a -> [c] -> Maybe a
-match = R.match . toRA
-
--------------------------------------------------------------------------------
--- RE
--------------------------------------------------------------------------------
-
--- | Convert to 'RE'.
---
--- >>> putPretty (toRE $ many "foo" :: RE.RE Char)
--- ^(foo)*$
---
-toRE :: (Ord c, Enum c, Bounded c) => K c a -> RE.RE c
-toRE = toKleene
-
--- | Convert to any 'Kleene'
-toKleene :: C.FiniteKleene c k => K c a -> k
-toKleene (KMap _ a)      = toKleene a
-toKleene (KUnion a b)    = toKleene a \/ toKleene b
-toKleene (KAppend _ a b) = toKleene a <> toKleene b
-toKleene (KStar _ a)     = C.star (toKleene a)
-toKleene (KString s)     = C.appends (map C.char s)
-toKleene KEmpty          = C.empty
-toKleene (KPure _)       = C.eps
-toKleene (KChar cs)      = C.fromRSet cs
-
--- | Convert from 'RE'.
---
--- /Note:/ all 'RE.REStar's are converted to 'Greedy' ones,
--- it doesn't matter, as we don't capture anything.
---
--- >>> match (fromRE "foobar") "foobar"
--- Just "foobar"
---
--- >>> match (fromRE $ C.star "a" <> C.star "a") "aaaa"
--- Just "aaaa"
---
-fromRE :: (Ord c, Enum c) => RE.RE c -> K c [c]
-fromRE (RE.REChars cs)    = pure <$> KChar cs
-fromRE (RE.REAppend rs)   = concat <$> traverse fromRE rs
-fromRE (RE.REUnion cs rs) = foldr (KUnion . fromRE) (pure <$> KChar cs) (toList rs)
-fromRE (RE.REStar r)      = concat <$> KStar Greedy (fromRE r)
-
--------------------------------------------------------------------------------
--- regex-applicative
--------------------------------------------------------------------------------
-
--- | Convert 'K' to 'R.RE' from @regex-applicative@.
---
--- >>> R.match (toRA ("xx" *> everything <* "zz" :: K Char String)) "xxyyyzz"
--- Just "yyy"
---
--- See also 'match'.
---
-toRA :: K c a -> R.RE c a
-toRA KEmpty              = empty
-toRA (KPure x)           = pure x
-toRA (KChar cs)          = R.psym (\c -> RSet.member c cs)
-toRA (KAppend f a b)     = liftA2 f (toRA a) (toRA b)
-toRA (KUnion a b)        = toRA a <|> toRA b
-toRA (KStar Greedy a)    = many (toRA a)
-toRA (KStar NonGreedy a) = R.few (toRA a)
-toRA (KMap f a)          = fmap f (toRA a)
-toRA (KString s)         = R.string s
-
--------------------------------------------------------------------------------
--- JavaScript
--------------------------------------------------------------------------------
-
--- | Convert to non-matching JavaScript string which can be used
--- as an argument to @new RegExp@
---
--- >>> putPretty ("foobar" :: K Char String)
--- ^foobar$
---
--- >>> putPretty $ many ("foobar" :: K Char String)
--- ^(foobar)*$
---
-instance c ~ Char => Pretty (K c a) where
-    pretty = pretty . toRE
-
--------------------------------------------------------------------------------
--- Doctest
--------------------------------------------------------------------------------
-
--- $setup
---
--- >>> :set -XOverloadedStrings
+import Kleene.Internal.Functor
diff --git a/src/Kleene/Functor/NonEmpty.hs b/src/Kleene/Functor/NonEmpty.hs
new file mode 100644
--- /dev/null
+++ b/src/Kleene/Functor/NonEmpty.hs
@@ -0,0 +1,287 @@
+{-# LANGUAGE CPP   #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE Safe  #-}
+module Kleene.Functor.NonEmpty (
+    K1,
+    Greediness (..),
+    -- * Constructors
+    some1,
+    anyChar,
+    oneof,
+    char,
+    charRange,
+    dot,
+    everything1,
+    string,
+    -- * Queries
+    isEmpty,
+    isEverything,
+    -- * Matching
+    match,
+    -- * Conversions
+    toRE,
+    toKleene,
+    toRA,
+    nullableProof,
+    ) where
+
+import Prelude ()
+import Prelude.Compat
+
+import Control.Applicative (Alternative (..), liftA2)
+import Data.Foldable       (toList)
+import Data.Functor.Alt    ((<!>))
+import Data.Functor.Apply  (Apply (..))
+import Data.List.NonEmpty  (NonEmpty (..))
+import Data.RangeSet.Map   (RSet)
+
+import qualified Data.Functor.Alt       as Alt
+import qualified Data.List.NonEmpty     as NE
+import qualified Data.RangeSet.Map      as RSet
+import qualified Text.Regex.Applicative as R
+
+import qualified Kleene.Classes          as C
+import           Kleene.Internal.Functor (Greediness (..), K (..))
+import           Kleene.Internal.Pretty
+import           Kleene.Internal.Sets
+import qualified Kleene.RE               as RE
+
+-- | 'Applicative' 'Functor' regular expression.
+data K1 c a where
+    K1Empty  :: K1 c a
+    K1Char   :: (Ord c, Enum c) => RSet c -> K1 c c
+    K1Append :: (a -> b -> r) -> K1 c a -> K1 c b -> K1 c r
+    K1Union  :: K1 c a -> K1 c a -> K1 c a
+    KPlus    :: Greediness -> K1 c a -> K1 c (NonEmpty a)
+
+    -- optimisations
+    K1Map    :: (a -> b) -> K1 c a -> K1 c b -- could use Pure and Append
+    K1String :: Eq c => NonEmpty c -> K1 c (NonEmpty c)     -- could use Char and Append
+
+instance Functor (K1 c) where
+    fmap _ K1Empty          = K1Empty
+    fmap f (K1Map g k)      = K1Map (f . g) k
+    fmap f (K1Append g a b) = K1Append (\x y -> f (g x y)) a b
+    fmap f k                = K1Map f k
+
+instance Apply (K1 c) where
+    K1Empty <.> _ = K1Empty
+    _ <.> K1Empty = K1Empty
+
+    f <.> x = K1Append ($) f x
+
+    liftF2 = K1Append
+
+instance Alt.Alt (K1 c) where
+    K1Empty <!> k = k
+    k <!> K1Empty = k
+    K1Char a <!> K1Char b = K1Char (RSet.union a b)
+
+    a <!> b = K1Union a b
+
+--
+some1 :: K1 c a -> K1 c (NonEmpty a)
+some1 K1Empty     = K1Empty
+some1 (KPlus _ k) = K1Map pure (KPlus Greedy k)
+some1 k           = KPlus Greedy k
+
+-- | 'few1', not 'some1'.
+--
+-- Let's define two similar regexps
+--
+-- >>> let re1 = liftF2 (,) (few1 $ char 'a')  (some1 $ char 'a')
+-- >>> let re2 = liftF2 (,) (some1 $ char 'a') (few1  $ char 'a')
+--
+-- Their 'RE' behaviour is the same:
+--
+-- >>> C.equivalent (toRE re1) (toRE re2)
+-- True
+--
+-- >>> map (C.match $ toRE re1) ["aaa","bbb"]
+-- [True,False]
+--
+-- However, the 'RA' behaviour is different!
+--
+-- >>> R.match (toRA re1) "aaaaa"
+-- Just ('a' :| "",'a' :| "aaa")
+--
+-- >>> R.match (toRA re2) "aaaaa"
+-- Just ('a' :| "aaa",'a' :| "")
+--
+few1 :: K1 c a -> K1 c (NonEmpty a)
+few1 K1Empty     = K1Empty
+few1 (KPlus _ k) = K1Map pure (KPlus NonGreedy k)
+few1 k           = KPlus NonGreedy k
+
+-------------------------------------------------------------------------------
+--
+-------------------------------------------------------------------------------
+
+-- | >>> putPretty anyChar
+-- ^[^]$
+anyChar :: (Ord c, Enum c, Bounded c) => K1 c c
+anyChar = K1Char RSet.full
+
+-- | >>> putPretty $ oneof ("foobar" :: [Char])
+-- ^[a-bfor]$
+oneof :: (Ord c, Enum c, Foldable f) => f c -> K1 c c
+oneof = K1Char . RSet.fromList . toList
+
+-- | >>> putPretty $ char 'x'
+-- ^x$
+char :: (Ord c, Enum c) => c -> K1 c c
+char = K1Char . RSet.singleton
+
+-- | >>> putPretty $ charRange 'a' 'z'
+-- ^[a-z]$
+charRange :: (Enum c, Ord c) => c -> c -> K1 c c
+charRange a b = K1Char (RSet.singletonRange (a, b))
+
+-- | >>> putPretty dot
+-- ^.$
+dot :: K1 Char Char
+dot = K1Char dotRSet
+
+-- | >>> putPretty everything1
+-- ^[^][^]*$
+everything1 :: (Ord c, Enum c, Bounded c) => K1 c (NonEmpty c)
+everything1 = some1 anyChar
+
+-- | Matches nothing?
+isEmpty :: (Ord c, Enum c, Bounded c) => K1 c a -> Bool
+isEmpty k = C.equivalent (toRE k) C.empty
+
+-- | Matches whole input?
+isEverything :: (Ord c, Enum c, Bounded c) => K1 c a -> Bool
+isEverything k = C.equivalent (toRE k) C.everything
+
+string :: String -> K1 Char (NonEmpty Char)
+string []       = error "panic! K1.string []"
+string (x : xs) = K1String (x :| xs)
+
+-------------------------------------------------------------------------------
+-- Matching
+-------------------------------------------------------------------------------
+
+-- | Match using @regex-applicative@
+match :: K1 c a -> [c] -> Maybe a
+match = R.match . toRA
+
+-------------------------------------------------------------------------------
+-- RE
+-------------------------------------------------------------------------------
+
+-- | Convert to 'RE'.
+--
+-- >>> putPretty (toRE $ some1 (string "foo") :: RE.RE Char)
+-- ^foo(foo)*$
+--
+toRE :: (Ord c, Enum c, Bounded c) => K1 c a -> RE.RE c
+toRE = toKleene
+
+-- | Convert to any 'Kleene'
+toKleene :: C.FiniteKleene c k => K1 c a -> k
+toKleene (K1Map _ a)      = toKleene a
+toKleene (K1Union a b)    = C.unions [toKleene a, toKleene b]
+toKleene (K1Append _ a b) = C.appends [toKleene a, toKleene b]
+toKleene (KPlus _ a)      = let k = toKleene a in C.appends [k, C.star k]
+toKleene (K1String s)     = C.appends (map C.char $ NE.toList s)
+toKleene K1Empty          = C.empty
+toKleene (K1Char cs)      = C.fromRSet cs
+
+-------------------------------------------------------------------------------
+-- regex-applicative
+-------------------------------------------------------------------------------
+
+-- | Convert 'K' to 'R.RE' from @regex-applicative@.
+--
+-- >>> R.match (toRA (string "xx" .> everything1 <. string "zz" :: K1 Char (NonEmpty Char))) "xxyyzyyzz"
+-- Just ('y' :| "yzyy")
+--
+-- See also 'match'.
+--
+toRA :: K1 c a -> R.RE c a
+toRA K1Empty              = empty
+toRA (K1Char cs)          = R.psym (\c -> RSet.member c cs)
+toRA (K1Append f a b)     = liftA2 f (toRA a) (toRA b)
+toRA (K1Union a b)        = toRA a <|> toRA b
+toRA (KPlus Greedy a)     = (:|) <$> toRA a <*> many (toRA a)
+toRA (KPlus NonGreedy a)  = (:|) <$> toRA a <*> R.few (toRA a)
+toRA (K1Map f a)          = fmap f (toRA a)
+toRA (K1String (x :| xs)) = (:|) <$> R.sym x <*> R.string xs
+
+-------------------------------------------------------------------------------
+-- nullableProof
+-------------------------------------------------------------------------------
+
+-- |
+-- >>> putPretty $ nullableProof (pure True)
+-- Right 1 , ^[]$
+--
+-- >>> putPretty $ nullableProof (many "xyz" :: K Char [String])
+-- Right [] , ^xyz(xyz)*$
+--
+-- >>> putPretty $ nullableProof (many $ toList <$> optional "x" <|> many "yz" :: K Char [[String]])
+-- Right [] , ^(x|yz(yz)*)(x|yz(yz)*)*$
+--
+nullableProof :: K c a -> Either (K1 c a) (a, K1 c a)
+nullableProof KEmpty    = Left K1Empty
+nullableProof (KPure x) = Right (x, K1Empty)
+nullableProof (KChar c) = Left (K1Char c)
+
+nullableProof (KAppend f a b) = case (nullableProof a, nullableProof b) of
+    (Left x, Left y)               -> Left (K1Append f x y)
+    (Left x, Right (y', y))        -> Left ((`f` y') <$> x <!> K1Append f x y)
+    (Right (x', x), Left y)        -> Left (K1Append f x y <!> f x' <$> y)
+    (Right (x', x), Right (y', y)) -> Right
+        (f x' y'
+        , K1Append f x y
+        <!> flip f y' <$> x
+        <!> f x' <$> y
+        )
+
+nullableProof (KUnion a b) = case (nullableProof a, nullableProof b) of
+    (Left x', Left _)              -> Left x'
+    (Right (x, x'), Left y')       -> Right (x, x' <!> y')
+    (Left x', Right (y, y'))       -> Right (y, x' <!> y')
+    (Right (x, x'), Right (_, y')) -> Right (x, x' <!> y')
+
+nullableProof (KStar g a) = case nullableProof a of
+    Left x       -> Right ([], NE.toList <$> star1 x)
+    Right (_, x) -> Right ([], NE.toList <$> star1 x) -- note, we don't left recurse
+  where
+    star1 = case g of
+        Greedy    -> some1
+        NonGreedy -> few1
+
+nullableProof (KMap f a) = case nullableProof a of
+    Right (x, x') -> Right (f x, fmap f x')
+    Left x'       -> Left (fmap f x')
+
+nullableProof (KString [])       = Right ([], K1Empty)
+nullableProof (KString (c : cs)) = Left (NE.toList <$> K1String (c :| cs))
+
+-------------------------------------------------------------------------------
+-- JavaScript
+-------------------------------------------------------------------------------
+
+-- | Convert to non-matching JavaScript string which can be used
+-- as an argument to @new RegExp@
+--
+-- >>> putPretty ("foobar" :: K Char String)
+-- ^foobar$
+--
+-- >>> putPretty $ many ("foobar" :: K Char String)
+-- ^(foobar)*$
+--
+instance c ~ Char => Pretty (K1 c a) where
+    pretty = pretty . toRE
+
+-------------------------------------------------------------------------------
+-- Doctest
+-------------------------------------------------------------------------------
+
+-- $setup
+--
+-- >>> :set -XOverloadedStrings
+-- >>> import Control.Applicative (optional)
diff --git a/src/Kleene/Internal/Functor.hs b/src/Kleene/Internal/Functor.hs
new file mode 100644
--- /dev/null
+++ b/src/Kleene/Internal/Functor.hs
@@ -0,0 +1,282 @@
+{-# LANGUAGE CPP   #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE Safe  #-}
+module Kleene.Internal.Functor (
+    K (..),
+    Greediness (..),
+    -- * Constructors
+    few,
+    anyChar,
+    oneof,
+    char,
+    charRange,
+    dot,
+    everything,
+    everything1,
+    -- * Queries
+    isEmpty,
+    isEverything,
+    -- * Matching
+    match,
+    -- * Conversions
+    toRE,
+    toKleene,
+    fromRE,
+    toRA,
+    ) where
+
+import Prelude ()
+import Prelude.Compat
+
+import Control.Applicative (Alternative (..), liftA2)
+import Data.Foldable       (toList)
+import Data.Functor.Apply  (Apply (..))
+import Data.RangeSet.Map   (RSet)
+import Data.String         (IsString (..))
+
+import qualified Data.RangeSet.Map      as RSet
+import qualified Text.Regex.Applicative as R
+import qualified Data.Functor.Alt       as Alt
+
+import qualified Kleene.Classes         as C
+import           Kleene.Internal.Pretty
+import           Kleene.Internal.Sets
+import qualified Kleene.RE              as RE
+
+-- | Star behaviour
+data Greediness
+    = Greedy    -- ^ 'many'
+    | NonGreedy -- ^ 'few'
+  deriving (Eq, Ord, Show, Enum, Bounded)
+
+-- | 'Applicative' 'Functor' regular expression.
+data K c a where
+    KEmpty  :: K c a
+    KPure   :: a -> K c a
+    KChar   :: (Ord c, Enum c) => RSet c -> K c c
+    KAppend :: (a -> b -> r) -> K c a -> K c b -> K c r
+    KUnion  :: K c a -> K c a -> K c a
+    KStar   :: Greediness -> K c a -> K c [a]
+
+    -- optimisations
+    KMap    :: (a -> b) -> K c a -> K c b -- could use Pure and Append
+    KString :: Eq c => [c] -> K c [c]     -- could use Char and Append
+
+instance (c ~ Char, IsString a) => IsString (K c a) where
+    fromString s = KMap fromString (KString s)
+
+instance Functor (K c) where
+    fmap _ KEmpty          = KEmpty
+    fmap f (KPure x)       = KPure (f x)
+    fmap f (KMap g k)      = KMap (f . g) k
+    fmap f (KAppend g a b) = KAppend (\x y -> f (g x y)) a b
+    fmap f k                    = KMap f k
+
+instance Apply (K c) where
+    KEmpty <.> _ = KEmpty
+    _ <.> KEmpty = KEmpty
+
+    KPure f <.> k = fmap f k
+    k <.> KPure x = fmap ($ x) k
+
+    f <.> x = KAppend ($) f x
+
+    liftF2 = KAppend
+
+instance Applicative (K c) where
+    pure  = KPure
+    (<*>) = (<.>)
+
+#if MIN_VERSION_base(4,10,0)
+    liftA2 = liftF2
+#endif
+
+instance Alt.Alt (K c) where
+    KEmpty <!> k = k
+    k <!> KEmpty = k
+    KChar a <!> KChar b = KChar (RSet.union a b)
+
+    a <!> b = KUnion a b
+
+    many KEmpty      = KPure []
+    many (KStar _ k) = KMap pure (KStar Greedy k)
+    many k           = KStar Greedy k
+
+    some KEmpty      = KEmpty
+    some (KStar _ k) = KMap pure (KStar Greedy k)
+    some k           = liftA2 (:) k (KStar Greedy k)
+
+instance Alternative (K c) where
+    empty = KEmpty
+    (<|>) = (Alt.<!>)
+    some  = Alt.some
+    many  = Alt.many
+
+-- | 'few', not 'many'.
+--
+-- Let's define two similar regexps
+--
+-- >>> let re1 = liftA2 (,) (few  $ char 'a') (many $ char 'a')
+-- >>> let re2 = liftA2 (,) (many $ char 'a') (few  $ char 'a')
+--
+-- Their 'RE' behaviour is the same:
+--
+-- >>> C.equivalent (toRE re1) (toRE re2)
+-- True
+--
+-- >>> map (C.match $ toRE re1) ["aaa","bbb"]
+-- [True,False]
+--
+-- However, the 'RA' behaviour is different!
+--
+-- >>> R.match (toRA re1) "aaaa"
+-- Just ("","aaaa")
+--
+-- >>> R.match (toRA re2) "aaaa"
+-- Just ("aaaa","")
+--
+few :: K c a -> K c [a]
+few KEmpty      = KPure []
+few (KStar _ k) = KMap pure (KStar NonGreedy k)
+few k           = KStar NonGreedy k
+
+-------------------------------------------------------------------------------
+--
+-------------------------------------------------------------------------------
+
+-- | >>> putPretty anyChar
+-- ^[^]$
+anyChar :: (Ord c, Enum c, Bounded c) => K c c
+anyChar = KChar RSet.full
+
+-- | >>> putPretty $ oneof ("foobar" :: [Char])
+-- ^[a-bfor]$
+oneof :: (Ord c, Enum c, Foldable f) => f c -> K c c
+oneof = KChar . RSet.fromList . toList
+
+-- | >>> putPretty $ char 'x'
+-- ^x$
+char :: (Ord c, Enum c) => c -> K c c
+char = KChar . RSet.singleton
+
+-- | >>> putPretty $ charRange 'a' 'z'
+-- ^[a-z]$
+charRange :: (Enum c, Ord c) => c -> c -> K c c
+charRange a b = KChar (RSet.singletonRange (a, b))
+
+-- | >>> putPretty dot
+-- ^.$
+dot :: K Char Char
+dot = KChar dotRSet
+
+-- | >>> putPretty everything
+-- ^[^]*$
+everything :: (Ord c, Enum c, Bounded c) => K c [c]
+everything = many anyChar
+
+-- | >>> putPretty everything1
+-- ^[^][^]*$
+everything1 :: (Ord c, Enum c, Bounded c) => K c [c]
+everything1 = some anyChar
+
+-- | Matches nothing?
+isEmpty :: (Ord c, Enum c, Bounded c) => K c a -> Bool
+isEmpty k = C.equivalent (toRE k) C.empty
+
+-- | Matches whole input?
+isEverything :: (Ord c, Enum c, Bounded c) => K c a -> Bool
+isEverything k = C.equivalent (toRE k) C.everything
+
+-------------------------------------------------------------------------------
+-- Matching
+-------------------------------------------------------------------------------
+
+-- | Match using @regex-applicative@
+match :: K c a -> [c] -> Maybe a
+match = R.match . toRA
+
+-------------------------------------------------------------------------------
+-- RE
+-------------------------------------------------------------------------------
+
+-- | Convert to 'RE'.
+--
+-- >>> putPretty (toRE $ many "foo" :: RE.RE Char)
+-- ^(foo)*$
+--
+toRE :: (Ord c, Enum c, Bounded c) => K c a -> RE.RE c
+toRE = toKleene
+
+-- | Convert to any 'Kleene'
+toKleene :: C.FiniteKleene c k => K c a -> k
+toKleene (KMap _ a)      = toKleene a
+toKleene (KUnion a b)    = C.unions [toKleene a, toKleene b]
+toKleene (KAppend _ a b) = C.appends [toKleene a, toKleene b]
+toKleene (KStar _ a)     = C.star (toKleene a)
+toKleene (KString s)     = C.appends (map C.char s)
+toKleene KEmpty          = C.empty
+toKleene (KPure _)       = C.eps
+toKleene (KChar cs)      = C.fromRSet cs
+
+-- | Convert from 'RE'.
+--
+-- /Note:/ all 'RE.REStar's are converted to 'Greedy' ones,
+-- it doesn't matter, as we don't capture anything.
+--
+-- >>> match (fromRE "foobar") "foobar"
+-- Just "foobar"
+--
+-- >>> match (fromRE $ C.star "a" <> C.star "a") "aaaa"
+-- Just "aaaa"
+--
+fromRE :: (Ord c, Enum c) => RE.RE c -> K c [c]
+fromRE (RE.REChars cs)    = pure <$> KChar cs
+fromRE (RE.REAppend rs)   = concat <$> traverse fromRE rs
+fromRE (RE.REUnion cs rs) = foldr (KUnion . fromRE) (pure <$> KChar cs) (toList rs)
+fromRE (RE.REStar r)      = concat <$> KStar Greedy (fromRE r)
+
+-------------------------------------------------------------------------------
+-- regex-applicative
+-------------------------------------------------------------------------------
+
+-- | Convert 'K' to 'R.RE' from @regex-applicative@.
+--
+-- >>> R.match (toRA ("xx" *> everything <* "zz" :: K Char String)) "xxyyyzz"
+-- Just "yyy"
+--
+-- See also 'match'.
+--
+toRA :: K c a -> R.RE c a
+toRA KEmpty              = empty
+toRA (KPure x)           = pure x
+toRA (KChar cs)          = R.psym (\c -> RSet.member c cs)
+toRA (KAppend f a b)     = liftA2 f (toRA a) (toRA b)
+toRA (KUnion a b)        = toRA a <|> toRA b
+toRA (KStar Greedy a)    = many (toRA a)
+toRA (KStar NonGreedy a) = R.few (toRA a)
+toRA (KMap f a)          = fmap f (toRA a)
+toRA (KString s)         = R.string s
+
+-------------------------------------------------------------------------------
+-- JavaScript
+-------------------------------------------------------------------------------
+
+-- | Convert to non-matching JavaScript string which can be used
+-- as an argument to @new RegExp@
+--
+-- >>> putPretty ("foobar" :: K Char String)
+-- ^foobar$
+--
+-- >>> putPretty $ many ("foobar" :: K Char String)
+-- ^(foobar)*$
+--
+instance c ~ Char => Pretty (K c a) where
+    pretty = pretty . toRE
+
+-------------------------------------------------------------------------------
+-- Doctest
+-------------------------------------------------------------------------------
+
+-- $setup
+--
+-- >>> :set -XOverloadedStrings
diff --git a/src/Kleene/Internal/Partition.hs b/src/Kleene/Internal/Partition.hs
--- a/src/Kleene/Internal/Partition.hs
+++ b/src/Kleene/Internal/Partition.hs
@@ -3,14 +3,15 @@
 
 import Prelude ()
 import Prelude.Compat
+import Data.Semigroup (Semigroup (..))
 
-import Data.Foldable             (toList)
-import Data.List.NonEmpty.Compat (NonEmpty (..))
-import Data.RangeSet.Map         (RSet)
-import Data.Set                  (Set)
+import Data.Foldable      (toList)
+import Data.List.NonEmpty (NonEmpty (..))
+import Data.RangeSet.Map  (RSet)
+import Data.Set           (Set)
 
 import qualified Data.Function.Step.Discrete.Closed as SF
-import qualified Data.List.NonEmpty.Compat          as NE
+import qualified Data.List.NonEmpty          as NE
 import qualified Data.RangeSet.Map                  as RSet
 import qualified Data.Set                           as Set
 
@@ -125,7 +126,7 @@
 
 -- |
 --
--- prop> all (curry (<=)) $ intervals $ asPartitionChar p
+-- prop> all (uncurry (<=)) $ intervals $ asPartitionChar p
 intervals :: (Enum a, Bounded a, Ord a) => Partition a -> NonEmpty (a, a)
 intervals (Partition xs) = go minBound (toList xs) where
     go x []       = (x, maxBound) :| []
diff --git a/src/Kleene/Internal/Pretty.hs b/src/Kleene/Internal/Pretty.hs
--- a/src/Kleene/Internal/Pretty.hs
+++ b/src/Kleene/Internal/Pretty.hs
@@ -80,3 +80,17 @@
 
 instance Pretty () where
     prettyS _ = showChar '.'
+
+instance Pretty a => Pretty (Maybe a) where
+    prettyS Nothing  = showString "Nothing"
+    prettyS (Just x) = prettyS x
+
+instance (Pretty a, Pretty b) => Pretty (Either a b) where
+    prettyS (Left x)  = showString "Left " . prettyS x
+    prettyS (Right x) = showString "Right " . prettyS x
+
+instance (Pretty a, Pretty b) => Pretty (a, b) where
+    prettyS (x, y) = prettyS x . showString " , " . prettyS y
+
+instance Show a => Pretty [a] where
+    prettyS = showList
diff --git a/src/Kleene/Internal/RE.hs b/src/Kleene/Internal/RE.hs
new file mode 100644
--- /dev/null
+++ b/src/Kleene/Internal/RE.hs
@@ -0,0 +1,676 @@
+{-# LANGUAGE BangPatterns           #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GADTs                  #-}
+{-# LANGUAGE Safe                   #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+module Kleene.Internal.RE (
+    RE (..),
+    -- * Construction
+    --
+    -- | Binary operators are
+    --
+    -- * '<>' for append
+    -- * '\/' for union
+    --
+    empty,
+    eps,
+    char,
+    charRange,
+    anyChar,
+    appends,
+    unions,
+    star,
+    string,
+    -- * Derivative
+    nullable,
+    derivate,
+    -- * Transition map
+    transitionMap,
+    leadingChars,
+    -- * Equivalence
+    equivalent,
+    -- * Generation
+    generate,
+    -- * Other
+    isEmpty,
+    nullableProof,
+    ) where
+
+import Prelude ()
+import Prelude.Compat
+import Data.Semigroup (Semigroup (..))
+
+import Control.Applicative (liftA2)
+import Data.Foldable       (toList)
+import Data.List           (foldl')
+import Data.Map            (Map)
+import Data.RangeSet.Map   (RSet)
+import Data.Set            (Set)
+import Data.String         (IsString (..))
+
+import qualified Data.Function.Step.Discrete.Closed as SF
+import qualified Data.Map                           as Map
+import qualified Data.RangeSet.Map                  as RSet
+import qualified Data.Set                           as Set
+import qualified Test.QuickCheck                    as QC
+import qualified Test.QuickCheck.Gen                as QC (unGen)
+import qualified Test.QuickCheck.Random             as QC (mkQCGen)
+
+import qualified Kleene.Classes            as C
+import qualified Kleene.Internal.Partition as P
+import           Kleene.Internal.Pretty
+
+-- | Regular expression
+--
+-- Constructors are exposed, but you should use
+-- smart constructors in this module to construct 'RE'.
+--
+-- The 'Eq' and 'Ord' instances are structural.
+-- The 'Kleene' etc constructors do "weak normalisation", so for values
+-- constructed using those operations 'Eq' witnesses "weak equivalence".
+-- See 'equivalent' for regular-expression equivalence.
+--
+-- Structure is exposed in "Kleene.RE" module but consider constructors as
+-- half-internal.  There are soft-invariants, but violating them shouldn't
+-- break anything in the package. (e.g. 'transitionMap' will eventually
+-- terminate, but may create more redundant states if starting regexp is not
+-- "weakly normalised").
+--
+data RE c
+    = REChars (RSet c)               -- ^ Single character
+    | REAppend [RE c]                -- ^ Concatenation
+    | REUnion (RSet c) (Set (RE c))  -- ^ Union
+    | REStar (RE c)                  -- ^ Kleene star
+  deriving (Eq, Ord, Show)
+
+-------------------------------------------------------------------------------
+-- Smart constructor
+-------------------------------------------------------------------------------
+
+-- | Empty regex. Doesn't accept anything.
+--
+-- >>> putPretty (empty :: RE Char)
+-- ^[]$
+--
+-- >>> putPretty (bottom :: RE Char)
+-- ^[]$
+--
+-- prop> match (empty :: RE Char) (s :: String) === False
+--
+empty :: RE c
+empty = REChars RSet.empty
+
+-- | Everything.
+--
+-- >>> putPretty everything
+-- ^[^]*$
+--
+-- prop> match (everything :: RE Char) (s :: String) === True
+--
+everything :: Bounded c => RE c
+everything = REStar (REChars RSet.full)
+
+-- | Empty string. /Note:/ different than 'empty'.
+--
+-- >>> putPretty eps
+-- ^$
+--
+-- >>> putPretty (mempty :: RE Char)
+-- ^$
+--
+-- prop> match (eps :: RE Char) s === null (s :: String)
+--
+eps :: RE c
+eps = REAppend []
+
+-- |
+--
+-- >>> putPretty (char 'x')
+-- ^x$
+--
+char :: c -> RE c
+char = REChars . RSet.singleton
+
+-- |
+--
+-- >>> putPretty $ charRange 'a' 'z'
+-- ^[a-z]$
+--
+charRange :: Ord c => c -> c -> RE c
+charRange c c' = REChars $ RSet.singletonRange (c, c')
+
+-- | Any character. /Note:/ different than dot!
+--
+-- >>> putPretty anyChar
+-- ^[^]$
+--
+anyChar :: Bounded c => RE c
+anyChar = REChars RSet.full
+
+-- | Concatenate regular expressions.
+--
+-- prop> (asREChar r <> s) <> t === r <> (s <> t)
+--
+-- prop> asREChar r <> empty === empty
+-- prop> empty <> asREChar r === empty
+--
+-- prop> asREChar r <> eps === r
+-- prop> eps <> asREChar r === r
+--
+appends :: Eq c => [RE c] -> RE c
+appends rs0
+    | elem empty rs1 = empty
+    | otherwise = case rs1 of
+        [r] -> r
+        rs  -> REAppend rs
+  where
+    -- flatten one level of REAppend
+    rs1 = concatMap f rs0
+
+    f (REAppend rs) = rs
+    f r             = [r]
+
+-- | Union of regular expressions.
+--
+-- prop> asREChar r \/ r === r
+-- prop> asREChar r \/ s === s \/ r
+-- prop> (asREChar r \/ s) \/ t === r \/ (s \/ t)
+--
+-- prop> empty \/ asREChar r === r
+-- prop> asREChar r \/ empty === r
+--
+-- prop> everything \/ asREChar r === everything
+-- prop> asREChar r \/ everything === everything
+--
+unions :: (Ord c, Enum c, Bounded c) => [RE c] -> RE c
+unions = uncurry mk . foldMap f where
+    mk cs rss
+        | Set.null rss = REChars cs
+        | Set.member everything rss = everything
+        | RSet.null cs = case Set.toList rss of
+            []  -> empty
+            [r] -> r
+            _   -> REUnion cs rss
+        | otherwise    = REUnion cs rss
+
+    f (REUnion cs rs) = (cs, rs)
+    f (REChars cs)    = (cs, Set.empty)
+    f r               = (mempty, Set.singleton r)
+
+-- | Kleene star.
+--
+-- prop> star (star r) === star (asREChar r)
+--
+-- prop> star eps     === asREChar eps
+-- prop> star empty   === asREChar eps
+-- prop> star anyChar === asREChar everything
+--
+-- prop> star (r      \/ eps) === star (asREChar r)
+-- prop> star (char c \/ eps) === star (asREChar (char c))
+-- prop> star (empty  \/ eps) === asREChar eps
+--
+star :: Ord c => RE c -> RE c
+star r = case r of
+    REStar _                          -> r
+    REAppend []                       -> eps
+    REChars cs | RSet.null cs         -> eps
+    REUnion cs rs | Set.member eps rs -> case Set.toList rs' of
+        []                  -> star (REChars cs)
+        [r'] | RSet.null cs -> star r'
+        _                   -> REStar (REUnion cs rs')
+      where
+        rs' = Set.delete eps rs
+    _                                 -> REStar r
+
+-- | Literal string.
+--
+-- >>> putPretty ("foobar" :: RE Char)
+-- ^foobar$
+--
+-- >>> putPretty ("(.)" :: RE Char)
+-- ^\(\.\)$
+--
+string :: [c] -> RE c
+string []  = eps
+string [c] = REChars (RSet.singleton c)
+string cs  = REAppend $ map (REChars . RSet.singleton) cs
+
+instance (Ord c, Enum c, Bounded c) => C.Kleene (RE c) where
+    empty      = empty
+    eps        = eps
+    appends    = appends
+    unions     = unions
+    star       = star
+
+instance (Ord c, Enum c, Bounded c) => C.CharKleene c (RE c) where
+    char       = char
+
+instance (Ord c, Enum c, Bounded c) => C.FiniteKleene c (RE c) where
+    everything = everything
+    charRange  = charRange
+    fromRSet   = REChars
+    anyChar    = anyChar
+
+-------------------------------------------------------------------------------
+-- Pseudo lattice
+-------------------------------------------------------------------------------
+
+(\/) :: (Ord c, Enum c, Bounded c) => RE c -> RE c -> RE c
+r \/ r' = unions [r, r']
+
+-------------------------------------------------------------------------------
+-- derivative
+-------------------------------------------------------------------------------
+
+-- | We say that a regular expression r is nullable if the language it defines
+-- contains the empty string.
+--
+-- >>> nullable eps
+-- True
+--
+-- >>> nullable (star "x")
+-- True
+--
+-- >>> nullable "foo"
+-- False
+--
+nullable :: RE c -> Bool
+nullable (REChars _)      = False
+nullable (REAppend rs)    = all nullable rs
+nullable (REUnion _cs rs) = any nullable rs
+nullable (REStar _)       = True
+
+-- | Intuitively, the derivative of a language \(\mathcal{L} \subset \Sigma^\star\)
+-- with respect to a symbol \(a \in \Sigma\) is the language that includes only
+-- those suffixes of strings with a leading symbol \(a\) in \(\mathcal{L}\).
+--
+-- >>> putPretty $ derivate 'f' "foobar"
+-- ^oobar$
+--
+-- >>> putPretty $ derivate 'x' $ "xyz" \/ "abc"
+-- ^yz$
+--
+-- >>> putPretty $ derivate 'x' $ star "xyz"
+-- ^yz(xyz)*$
+--
+derivate :: (Ord c, Enum c, Bounded c) => c -> RE c -> RE c
+derivate c (REChars cs)     = derivateChars c cs
+derivate c (REUnion cs rs)  = unions $ derivateChars c cs : [ derivate c r | r <- toList rs]
+derivate c (REAppend rs)    = derivateAppend c rs
+derivate c rs@(REStar r)    = derivate c r <> rs
+
+derivateAppend :: (Ord c, Enum c, Bounded c) => c -> [RE c] -> RE c
+derivateAppend _ []      = empty
+derivateAppend c [r]     = derivate c r
+derivateAppend c (r:rs)
+    | nullable r         = unions [r' <> appends rs, rs']
+    | otherwise          = r' <> appends rs
+  where
+    r'  = derivate c r
+    rs' = derivateAppend c rs
+
+derivateChars :: Ord c =>  c -> RSet c -> RE c
+derivateChars c cs
+    | c `RSet.member` cs      = eps
+    | otherwise               = empty
+
+instance (Ord c, Enum c, Bounded c) => C.Derivate c (RE c) where
+    nullable = nullable
+    derivate = derivate
+
+instance (Ord c, Enum c, Bounded c) => C.Match c (RE c) where
+    match r = nullable . foldl' (flip derivate) r
+
+-------------------------------------------------------------------------------
+-- Nullable with proof
+-------------------------------------------------------------------------------
+
+-- | Not only we can decide whether 'RE' is nullable, we can also
+-- remove the empty string:
+--
+-- >>> putPretty $ nullableProof eps
+-- ^[]$
+--
+-- >>> putPretty $ nullableProof $ star "x"
+-- ^xx*$
+--
+-- >>> putPretty $ nullableProof "foo"
+-- Nothing
+--
+-- 'nullableProof' is consistent with 'nullable':
+--
+-- prop> isJust (nullableProof r) === nullable (asREChar r)
+--
+-- The returned regular expression is not nullable:
+--
+-- prop> maybe True (not . nullable) $ nullableProof $ asREChar r
+--
+-- If we union with empty regex, we get a equivalent regular expression
+-- we started with:
+--
+-- prop> maybe r (eps \/) (nullableProof r) `equivalent` (asREChar r)
+--
+nullableProof :: forall c. (Ord c, Enum c, Bounded c) => RE c -> Maybe (RE c)
+nullableProof (REChars _)   = Nothing
+
+nullableProof (REAppend []) = Just empty
+nullableProof (REAppend xs)
+    | Just ys <- traverse (\x -> (,) x <$> nullableProof x) xs = Just (go ys)
+    | otherwise = Nothing
+  where
+    go :: [(RE c, RE c)] -> RE c
+    go rs = unions $ map appends $ tail $ traverse (\(r,r') -> [r,r']) rs
+
+nullableProof (REUnion cs rs)
+    | any nullable rs = Just $ REUnion cs $ Set.map (\r -> maybe r id $ nullableProof r) rs
+    | otherwise       = Nothing
+
+nullableProof (REStar r)
+    | Just r' <- nullableProof r = Just (r' <> REStar r')
+    | otherwise                  = Just (r <> REStar r) 
+
+-------------------------------------------------------------------------------
+-- isEmpty
+-------------------------------------------------------------------------------
+
+-- | Whether 'RE' is (structurally) equal to 'empty'.
+--
+-- prop> isEmpty r === all (not . nullable) (Map.keys $ transitionMap $ asREChar r)
+isEmpty :: RE c -> Bool
+isEmpty (REChars rs) = RSet.null rs
+isEmpty _            = False
+
+-------------------------------------------------------------------------------
+-- States
+-------------------------------------------------------------------------------
+
+-- | Transition map. Used to construct 'Kleene.DFA.DFA'.
+--
+-- >>> void $ Map.traverseWithKey (\k v -> putStrLn $ pretty k ++ " : " ++ SF.showSF (fmap pretty v)) $ transitionMap ("ab" :: RE Char)
+-- ^[]$ : \_ -> "^[]$"
+-- ^b$ : \x -> if
+--     | x <= 'a'  -> "^[]$"
+--     | x <= 'b'  -> "^$"
+--     | otherwise -> "^[]$"
+-- ^$ : \_ -> "^[]$"
+-- ^ab$ : \x -> if
+--     | x <= '`'  -> "^[]$"
+--     | x <= 'a'  -> "^b$"
+--     | otherwise -> "^[]$"
+--
+transitionMap
+    :: forall c. (Ord c, Enum c, Bounded c)
+    => RE c
+    -> Map (RE c) (SF.SF c (RE c))
+transitionMap re = go Map.empty [re] where
+    go :: Map (RE c) (SF.SF c (RE c))
+       -> [RE c]
+       -> Map (RE c) (SF.SF c (RE c))
+    go !acc [] = acc
+    go acc (r : rs)
+        | r `Map.member` acc = go acc rs
+        | otherwise = go (Map.insert r pm acc) (SF.values pm ++ rs)
+      where
+        pm = P.toSF (\c -> derivate c r) (leadingChars r)
+
+instance (Ord c, Enum c, Bounded c) => C.TransitionMap c (RE c) where
+    transitionMap = transitionMap
+
+-- | Leading character sets of regular expression.
+--
+-- >>> leadingChars "foo"
+-- fromSeparators "ef"
+--
+-- >>> leadingChars (star "b" <> star "e")
+-- fromSeparators "abde"
+--
+-- >>> leadingChars (charRange 'b' 'z')
+-- fromSeparators "az"
+--
+leadingChars :: (Ord c, Enum c, Bounded c) => RE c -> P.Partition c
+leadingChars (REChars cs)    = P.fromRSet cs
+leadingChars (REUnion cs rs) = P.fromRSet cs <> foldMap leadingChars rs
+leadingChars (REStar r)      = leadingChars r
+leadingChars (REAppend rs)   = leadingCharsAppend rs
+
+leadingCharsAppend :: (Ord c, Enum c, Bounded c) => [RE c] -> P.Partition c
+leadingCharsAppend [] = P.whole
+leadingCharsAppend (r : rs)
+    | nullable r = leadingChars r <> leadingCharsAppend rs
+    | otherwise  = leadingChars r
+
+-------------------------------------------------------------------------------
+-- Equivalence
+-------------------------------------------------------------------------------
+
+-- | Whether two regexps are equivalent.
+--
+-- @
+-- 'equivalent' re1 re2 <=> forall s. 'match' re1 s === 'match' re1 s
+-- @
+--
+-- >>> let re1 = star "a" <> "a"
+-- >>> let re2 = "a" <> star "a"
+--
+-- These are different regular expressions, even we perform
+-- some normalisation-on-construction:
+--
+-- >>> re1 == re2
+-- False
+--
+-- They are however equivalent:
+--
+-- >>> equivalent re1 re2
+-- True
+--
+-- The algorithm works by executing 'states' on "product" regexp,
+-- and checking whether all resulting states are both accepting or rejecting.
+--
+-- @
+-- re1 == re2 ==> 'equivalent' re1 re2
+-- @
+--
+-- === More examples
+--
+-- >>> let example re1 re2 = putPretty re1 >> putPretty re2 >> return (equivalent re1 re2)
+-- >>> example re1 re2
+-- ^a*a$
+-- ^aa*$
+-- True
+--
+-- >>> example (star "aa") (star "aaa")
+-- ^(aa)*$
+-- ^(aaa)*$
+-- False
+--
+-- >>> example (star "aa" <> star "aaa") (star "aaa" <> star "aa")
+-- ^(aa)*(aaa)*$
+-- ^(aaa)*(aa)*$
+-- True
+--
+-- >>> example (star ("a" \/ "b")) (star $ star "a" <> star "b")
+-- ^[a-b]*$
+-- ^(a*b*)*$
+-- True
+--
+equivalent :: forall c. (Ord c, Enum c, Bounded c) => RE c -> RE c -> Bool
+equivalent x0 y0 = go mempty [(x0, y0)] where
+    go :: Set (RE c, RE c) -> [(RE c, RE c)] -> Bool
+    go !_ [] = True
+    go acc (p@(x, y) : zs)
+        | p `Set.member` acc = go acc zs
+        -- if two regexps are structurally the same, we don't need to recurse.
+        | x == y             = go (Set.insert p acc) zs
+        | all agree ps       = go (Set.insert p acc) (ps ++ zs)
+        | otherwise = False
+      where
+        cs = toList $ P.examples $ leadingChars x `P.wedge` leadingChars y
+        ps = map (\c -> (derivate c x, derivate c y)) cs
+
+    agree :: (RE c, RE c) -> Bool
+    agree (x, y) = nullable x == nullable y
+
+instance (Ord c, Enum c, Bounded c) => C.Equivalent c (RE c) where
+    equivalent = equivalent
+
+-------------------------------------------------------------------------------
+-- Generation
+-------------------------------------------------------------------------------
+
+-- | Generate random strings of the language @RE c@ describes.
+--
+-- >>> let example = traverse_ print . take 3 . generate (curry QC.choose) 42
+-- >>> example "abc"
+-- "abc"
+-- "abc"
+-- "abc"
+--
+-- >>> example $ star $ "a" \/ "b"
+-- "aaaaba"
+-- "bbba"
+-- "abbbbaaaa"
+--
+-- >>> example empty
+--
+-- prop> all (match r) $ take 10 $ generate (curry QC.choose) 42 (r :: RE Char)
+--
+generate
+    :: (c -> c -> QC.Gen c) -- ^ character range generator
+    -> Int    -- ^ seed
+    -> RE c
+    -> [[c]]  -- ^ infinite list of results
+generate c seed re
+    | isEmpty re = []
+    | otherwise  = QC.unGen (QC.infiniteListOf (generator c re)) (QC.mkQCGen seed) 10
+
+generator
+    :: (c -> c -> QC.Gen c)
+    -> RE c
+    -> QC.Gen [c]
+generator c = go where
+    go (REChars cs)    = goChars cs
+    go (REAppend rs)   = concat <$> traverse go rs
+    go (REUnion cs rs)
+        | RSet.null  cs = QC.oneof [ go r | r <- toList rs ]
+        | otherwise     = QC.oneof $ goChars cs : [ go r | r <- toList rs ]
+    go (REStar r)      = QC.sized $ \n -> do
+        n' <- QC.choose (0, n)
+        concat <$> sequence (replicate n' (go r))
+
+    goChars cs = pure <$> QC.oneof [ c x y | (x,y) <- RSet.toRangeList cs ]
+
+-------------------------------------------------------------------------------
+-- Instances
+-------------------------------------------------------------------------------
+
+instance Eq c => Semigroup (RE c) where
+    r <> r' = appends [r, r']
+
+instance Eq c => Monoid (RE c) where
+    mempty  = eps
+    mappend = (<>)
+    mconcat = appends
+
+
+
+instance c ~ Char => IsString (RE c) where
+    fromString = string
+
+instance (Ord c, Enum c, Bounded c, QC.Arbitrary c) => QC.Arbitrary (RE c) where
+    arbitrary = QC.sized arb where
+        c :: QC.Gen (RE c)
+        c = REChars . RSet.fromRangeList <$> QC.arbitrary
+
+        arb :: Int -> QC.Gen (RE c)
+        arb n | n <= 0    = QC.oneof [c, fmap char QC.arbitrary, pure eps]
+              | otherwise = QC.oneof
+            [ c
+            , pure eps
+            , fmap char QC.arbitrary
+            , liftA2 (<>) (arb n2) (arb n2)
+            , liftA2 (\/) (arb n2) (arb n2)
+            , fmap star (arb n2)
+            ]
+          where
+            n2 = n `div` 2
+
+    shrink (REUnion _cs rs) = Set.toList rs
+    shrink (REAppend rs)    = rs ++ map appends (QC.shrink rs)
+    shrink (REStar r)       = r : map star (QC.shrink r)
+    shrink _                = []
+
+instance (QC.CoArbitrary c) => QC.CoArbitrary (RE c) where
+    coarbitrary (REChars cs)    = QC.variant (0 :: Int) . QC.coarbitrary (RSet.toRangeList cs)
+    coarbitrary (REAppend rs)   = QC.variant (1 :: Int) . QC.coarbitrary rs
+    coarbitrary (REUnion cs rs) = QC.variant (2 :: Int) . QC.coarbitrary (RSet.toRangeList cs, Set.toList rs)
+    coarbitrary (REStar r)      = QC.variant (3 :: Int) . QC.coarbitrary r
+
+-------------------------------------------------------------------------------
+-- JavaScript
+-------------------------------------------------------------------------------
+
+instance c ~ Char => Pretty (RE c) where
+    prettyS x = showChar '^' . go False x . showChar '$'
+      where
+        go :: Bool -> RE Char -> ShowS
+        go p (REStar a)
+            = parens p
+            $ go True a . showChar '*'
+        go p (REAppend rs)
+            = parens p $ goMany id rs
+        go p (REUnion cs rs)
+            | RSet.null cs = goUnion p rs
+            | Set.null rs  = prettyS cs
+            | otherwise    = goUnion p (Set.insert (REChars cs) rs)
+        go _ (REChars cs)
+            = prettyS cs
+
+        goUnion p rs
+            | Set.member eps rs = parens p $ goUnion' True . showChar '?'
+            | otherwise         = goUnion' p
+          where
+            goUnion' p' = case Set.toList (Set.delete eps rs) of
+                [] -> go True empty
+                [r] -> go p' r
+                (r:rs') -> parens True $ goSome1 (showChar '|') r rs'
+
+        goMany :: ShowS -> [RE Char] -> ShowS
+        goMany sep = foldr (\a b -> go False a . sep . b) id
+
+        goSome1 :: ShowS -> RE Char -> [RE Char] -> ShowS
+        goSome1 sep r = foldl (\a b -> a . sep . go False b) (go False r)
+
+        parens :: Bool -> ShowS -> ShowS
+        parens True  s = showString "(" . s . showChar ')'
+        parens False s = s
+
+-------------------------------------------------------------------------------
+-- Latin1
+-------------------------------------------------------------------------------
+
+instance C.ToLatin1 RE where
+    toLatin1 (REChars rs)    = C.fromRSet (C.toLatin1 rs)
+    toLatin1 (REAppend xs)   = appends (map C.toLatin1 xs)
+    toLatin1 (REUnion rs xs) = C.fromRSet (C.toLatin1 rs) \/ unions (map C.toLatin1 (Set.toList  xs))
+    toLatin1 (REStar r)      = star (C.toLatin1 r)
+
+-------------------------------------------------------------------------------
+-- Doctest
+-------------------------------------------------------------------------------
+
+-- $setup
+-- >>> :set -XOverloadedStrings
+-- >>> import Control.Monad (void)
+-- >>> import Data.Foldable (traverse_)
+-- >>> import Data.List (sort)
+-- >>> import Data.Maybe (isJust)
+--
+-- >>> import Test.QuickCheck ((===))
+-- >>> import qualified Test.QuickCheck as QC
+--
+-- >>> import Kleene.Classes (match)
+-- >>> import Algebra.Lattice (bottom)
+-- >>> import Kleene.RE ()
+--
+-- >>> let asREChar :: RE Char -> RE Char; asREChar = id
diff --git a/src/Kleene/Monad.hs b/src/Kleene/Monad.hs
--- a/src/Kleene/Monad.hs
+++ b/src/Kleene/Monad.hs
@@ -13,8 +13,9 @@
     -- | Binary operators are
     --
     -- * '<>' for append
-    -- * '\/' for union
     --
+    -- There are no binary operator for union. Use 'unions'.
+    --
     empty,
     eps,
     char,
@@ -38,8 +39,8 @@
 
 import Prelude ()
 import Prelude.Compat
+import Data.Semigroup (Semigroup (..))
 
-import Algebra.Lattice     (BoundedJoinSemiLattice (..), JoinSemiLattice (..))
 import Control.Applicative (liftA2)
 import Control.Monad       (ap)
 import Data.Foldable       (toList)
@@ -98,10 +99,7 @@
 -- >>> putPretty (empty :: M Bool)
 -- ^[]$
 --
--- >>> putPretty (bottom :: M Bool)
--- ^[]$
---
--- prop> match (empty :: M Bool) (s :: String) === False
+-- prop> match (empty :: M Char) (s :: String) === False
 --
 empty :: M c
 empty = MChars []
@@ -114,7 +112,7 @@
 -- >>> putPretty (mempty :: M Bool)
 -- ^$
 --
--- prop> match (eps :: M Bool) s === null (s :: String)
+-- prop> match (eps :: M Char) s === null (s :: String)
 --
 eps :: M c
 eps = MAppend []
@@ -208,14 +206,16 @@
 string [c] = MChars [c]
 string cs  = MAppend $ map (MChars . pure) cs
 
-instance C.Kleene c (M c) where
+instance C.Kleene  (M c) where
     empty      = empty
     eps        = eps
-    char       = char
     appends    = appends
     unions     = unions
     star       = star
 
+instance C.CharKleene c (M c) where
+    char       = char
+
 -------------------------------------------------------------------------------
 -- derivative
 -------------------------------------------------------------------------------
@@ -245,7 +245,7 @@
 -- >>> putPretty $ derivate 'f' "foobar"
 -- ^oobar$
 --
--- >>> putPretty $ derivate 'x' $ "xyz" \/ "abc"
+-- >>> putPretty $ derivate 'x' $ unions ["xyz", "abc"]
 -- ^yz$
 --
 -- >>> putPretty $ derivate 'x' $ star "xyz"
@@ -305,7 +305,7 @@
 -- "abc"
 -- "abc"
 --
--- >>> example $ star $ "a" \/ "b"
+-- >>> example $ star $ unions ["a", "b"]
 -- "ababbb"
 -- "baab"
 -- "abbababaa"
@@ -348,7 +348,7 @@
 -- >>> putPretty (toKleene re :: RE Char)
 -- ^[a-z]$
 --
-toKleene :: C.Kleene c k => M c -> k
+toKleene :: C.CharKleene c k => M c -> k
 toKleene (MChars cs)    = C.oneof cs
 toKleene (MAppend rs)   = C.appends (map toKleene rs)
 toKleene (MUnion cs rs) = C.unions (C.oneof cs : map toKleene rs)
@@ -366,12 +366,6 @@
     mappend = (<>)
     mconcat = appends
 
-instance JoinSemiLattice (M c) where
-    r \/ r' = unions [r, r']
-
-instance BoundedJoinSemiLattice (M c) where
-    bottom = empty
-
 instance c ~ Char => IsString (M c) where
     fromString = string
 
@@ -387,7 +381,7 @@
             , pure eps
             , fmap char QC.arbitrary
             , liftA2 (<>) (arb n2) (arb n2)
-            , liftA2 (\/) (arb n2) (arb n2)
+            , liftA2 (\x y -> unions [x,y]) (arb n2) (arb n2)
             , fmap star (arb n2)
             ]
           where
diff --git a/src/Kleene/RE.hs b/src/Kleene/RE.hs
--- a/src/Kleene/RE.hs
+++ b/src/Kleene/RE.hs
@@ -1,9 +1,3 @@
-{-# LANGUAGE BangPatterns           #-}
-{-# LANGUAGE FlexibleInstances      #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE GADTs                  #-}
-{-# LANGUAGE Safe                   #-}
-{-# LANGUAGE ScopedTypeVariables    #-}
 module Kleene.RE (
     RE (..),
     -- * Construction
@@ -34,570 +28,9 @@
     generate,
     -- * Other
     isEmpty,
+    nullableProof,
     ) where
 
-import Prelude ()
-import Prelude.Compat
-
-import Algebra.Lattice     (BoundedJoinSemiLattice (..), JoinSemiLattice (..))
-import Control.Applicative (liftA2)
-import Data.Foldable       (toList)
-import Data.List           (foldl')
-import Data.Map            (Map)
-import Data.RangeSet.Map   (RSet)
-import Data.Set            (Set)
-import Data.String         (IsString (..))
-
-import qualified Data.Function.Step.Discrete.Closed as SF
-import qualified Data.Map                           as Map
-import qualified Data.RangeSet.Map                  as RSet
-import qualified Data.Set                           as Set
-import qualified Test.QuickCheck                    as QC
-import qualified Test.QuickCheck.Gen                as QC (unGen)
-import qualified Test.QuickCheck.Random             as QC (mkQCGen)
-
-import qualified Kleene.Classes            as C
-import qualified Kleene.Internal.Partition as P
-import           Kleene.Internal.Pretty
-
--- | Regular expression
---
--- Constructors are exposed, but you should use
--- smart constructors in this module to construct 'RE'.
---
--- The 'Eq' and 'Ord' instances are structural.
--- The 'Kleene' etc constructors do "weak normalisation", so for values
--- constructed using those operations 'Eq' witnesses "weak equivalence".
--- See 'equivalent' for regular-expression equivalence.
---
--- Structure is exposed in "Kleene.RE" module but consider constructors as
--- half-internal.  There are soft-invariants, but violating them shouldn't
--- break anything in the package. (e.g. 'transitionMap' will eventually
--- terminate, but may create more redundant states if starting regexp is not
--- "weakly normalised").
---
-data RE c
-    = REChars (RSet c)               -- ^ Single character
-    | REAppend [RE c]                -- ^ Concatenation
-    | REUnion (RSet c) (Set (RE c))  -- ^ Union
-    | REStar (RE c)                  -- ^ Kleene star
-  deriving (Eq, Ord, Show)
-
--------------------------------------------------------------------------------
--- Smart constructor
--------------------------------------------------------------------------------
-
--- | Empty regex. Doesn't accept anything.
---
--- >>> putPretty (empty :: RE Char)
--- ^[]$
---
--- >>> putPretty (bottom :: RE Char)
--- ^[]$
---
--- prop> match (empty :: RE Char) (s :: String) === False
---
-empty :: RE c
-empty = REChars RSet.empty
-
--- | Everything.
---
--- >>> putPretty everything
--- ^[^]*$
---
--- prop> match (everything :: RE Char) (s :: String) === True
---
-everything :: Bounded c => RE c
-everything = REStar (REChars RSet.full)
-
--- | Empty string. /Note:/ different than 'empty'.
---
--- >>> putPretty eps
--- ^$
---
--- >>> putPretty (mempty :: RE Char)
--- ^$
---
--- prop> match (eps :: RE Char) s === null (s :: String)
---
-eps :: RE c
-eps = REAppend []
-
--- |
---
--- >>> putPretty (char 'x')
--- ^x$
---
-char :: c -> RE c
-char = REChars . RSet.singleton
-
--- |
---
--- >>> putPretty $ charRange 'a' 'z'
--- ^[a-z]$
---
-charRange :: Ord c => c -> c -> RE c
-charRange c c' = REChars $ RSet.singletonRange (c, c')
-
--- | Any character. /Note:/ different than dot!
---
--- >>> putPretty anyChar
--- ^[^]$
---
-anyChar :: Bounded c => RE c
-anyChar = REChars RSet.full
-
--- | Concatenate regular expressions.
---
--- prop> (asREChar r <> s) <> t === r <> (s <> t)
---
--- prop> asREChar r <> empty === empty
--- prop> empty <> asREChar r === empty
---
--- prop> asREChar r <> eps === r
--- prop> eps <> asREChar r === r
---
-appends :: Eq c => [RE c] -> RE c
-appends rs0
-    | elem empty rs1 = empty
-    | otherwise = case rs1 of
-        [r] -> r
-        rs  -> REAppend rs
-  where
-    -- flatten one level of REAppend
-    rs1 = concatMap f rs0
-
-    f (REAppend rs) = rs
-    f r             = [r]
-
--- | Union of regular expressions.
---
--- prop> asREChar r \/ r === r
--- prop> asREChar r \/ s === s \/ r
--- prop> (asREChar r \/ s) \/ t === r \/ (s \/ t)
---
--- prop> empty \/ asREChar r === r
--- prop> asREChar r \/ empty === r
---
--- prop> everything \/ asREChar r === everything
--- prop> asREChar r \/ everything === everything
---
-unions :: (Ord c, Enum c, Bounded c) => [RE c] -> RE c
-unions = uncurry mk . foldMap f where
-    mk cs rss
-        | Set.null rss = REChars cs
-        | Set.member everything rss = everything
-        | RSet.null cs = case Set.toList rss of
-            []  -> empty
-            [r] -> r
-            _   -> REUnion cs rss
-        | otherwise    = REUnion cs rss
-
-    f (REUnion cs rs) = (cs, rs)
-    f (REChars cs)    = (cs, Set.empty)
-    f r               = (mempty, Set.singleton r)
-
--- | Kleene star.
---
--- prop> star (star r) === star (asREChar r)
---
--- prop> star eps     === asREChar eps
--- prop> star empty   === asREChar eps
--- prop> star anyChar === asREChar everything
---
--- prop> star (r      \/ eps) === star (asREChar r)
--- prop> star (char c \/ eps) === star (asREChar (char c))
--- prop> star (empty  \/ eps) === asREChar eps
---
-star :: Ord c => RE c -> RE c
-star r = case r of
-    REStar _                          -> r
-    REAppend []                       -> eps
-    REChars cs | RSet.null cs         -> eps
-    REUnion cs rs | Set.member eps rs -> case Set.toList rs' of
-        []                  -> star (REChars cs)
-        [r'] | RSet.null cs -> star r'
-        _                   -> REStar (REUnion cs rs')
-      where
-        rs' = Set.delete eps rs
-    _                                 -> REStar r
-
--- | Literal string.
---
--- >>> putPretty ("foobar" :: RE Char)
--- ^foobar$
---
--- >>> putPretty ("(.)" :: RE Char)
--- ^\(\.\)$
---
-string :: [c] -> RE c
-string []  = eps
-string [c] = REChars (RSet.singleton c)
-string cs  = REAppend $ map (REChars . RSet.singleton) cs
-
-instance (Ord c, Enum c, Bounded c) => C.Kleene c (RE c) where
-    empty      = empty
-    eps        = eps
-    char       = char
-    appends    = appends
-    unions     = unions
-    star       = star
-
-instance (Ord c, Enum c, Bounded c) => C.FiniteKleene c (RE c) where
-    everything = everything
-    charRange  = charRange
-    fromRSet   = REChars
-    anyChar    = anyChar
-
--------------------------------------------------------------------------------
--- derivative
--------------------------------------------------------------------------------
-
--- | We say that a regular expression r is nullable if the language it defines
--- contains the empty string.
---
--- >>> nullable eps
--- True
---
--- >>> nullable (star "x")
--- True
---
--- >>> nullable "foo"
--- False
---
-nullable :: RE c -> Bool
-nullable (REChars _)      = False
-nullable (REAppend rs)    = all nullable rs
-nullable (REUnion _cs rs) = any nullable rs
-nullable (REStar _)       = True
-
--- | Intuitively, the derivative of a language \(\mathcal{L} \subset \Sigma^\star\)
--- with respect to a symbol \(a \in \Sigma\) is the language that includes only
--- those suffixes of strings with a leading symbol \(a\) in \(\mathcal{L}\).
---
--- >>> putPretty $ derivate 'f' "foobar"
--- ^oobar$
---
--- >>> putPretty $ derivate 'x' $ "xyz" \/ "abc"
--- ^yz$
---
--- >>> putPretty $ derivate 'x' $ star "xyz"
--- ^yz(xyz)*$
---
-derivate :: (Ord c, Enum c, Bounded c) => c -> RE c -> RE c
-derivate c (REChars cs)     = derivateChars c cs
-derivate c (REUnion cs rs)  = unions $ derivateChars c cs : [ derivate c r | r <- toList rs]
-derivate c (REAppend rs)    = derivateAppend c rs
-derivate c rs@(REStar r)    = derivate c r <> rs
-
-derivateAppend :: (Ord c, Enum c, Bounded c) => c -> [RE c] -> RE c
-derivateAppend _ []      = empty
-derivateAppend c [r]     = derivate c r
-derivateAppend c (r:rs)
-    | nullable r         = unions [r' <> appends rs, rs']
-    | otherwise          = r' <> appends rs
-  where
-    r'  = derivate c r
-    rs' = derivateAppend c rs
-
-derivateChars :: Ord c =>  c -> RSet c -> RE c
-derivateChars c cs
-    | c `RSet.member` cs      = eps
-    | otherwise               = empty
-
-instance (Ord c, Enum c, Bounded c) => C.Derivate c (RE c) where
-    nullable = nullable
-    derivate = derivate
-
-instance (Ord c, Enum c, Bounded c) => C.Match c (RE c) where
-    match r = nullable . foldl' (flip derivate) r
-
--------------------------------------------------------------------------------
--- isEmpty
--------------------------------------------------------------------------------
-
--- | Whether 'RE' is (structurally) equal to 'empty'.
---
--- prop> isEmpty r === all (not . nullable) (Map.keys $ transitionMap $ asREChar r)
-isEmpty :: RE c -> Bool
-isEmpty (REChars rs) = RSet.null rs
-isEmpty _            = False
-
--------------------------------------------------------------------------------
--- States
--------------------------------------------------------------------------------
-
--- | Transition map. Used to construct 'Kleene.DFA.DFA'.
---
--- >>> void $ Map.traverseWithKey (\k v -> putStrLn $ pretty k ++ " : " ++ SF.showSF (fmap pretty v)) $ transitionMap ("ab" :: RE Char)
--- ^[]$ : \_ -> "^[]$"
--- ^b$ : \x -> if
---     | x <= 'a'  -> "^[]$"
---     | x <= 'b'  -> "^$"
---     | otherwise -> "^[]$"
--- ^$ : \_ -> "^[]$"
--- ^ab$ : \x -> if
---     | x <= '`'  -> "^[]$"
---     | x <= 'a'  -> "^b$"
---     | otherwise -> "^[]$"
---
-transitionMap
-    :: forall c. (Ord c, Enum c, Bounded c)
-    => RE c
-    -> Map (RE c) (SF.SF c (RE c))
-transitionMap re = go Map.empty [re] where
-    go :: Map (RE c) (SF.SF c (RE c))
-       -> [RE c]
-       -> Map (RE c) (SF.SF c (RE c))
-    go !acc [] = acc
-    go acc (r : rs)
-        | r `Map.member` acc = go acc rs
-        | otherwise = go (Map.insert r pm acc) (SF.values pm ++ rs)
-      where
-        pm = P.toSF (\c -> derivate c r) (leadingChars r)
-
-instance (Ord c, Enum c, Bounded c) => C.TransitionMap c (RE c) where
-    transitionMap = transitionMap
-
--- | Leading character sets of regular expression.
---
--- >>> leadingChars "foo"
--- fromSeparators "ef"
---
--- >>> leadingChars (star "b" <> star "e")
--- fromSeparators "abde"
---
--- >>> leadingChars (charRange 'b' 'z')
--- fromSeparators "az"
---
-leadingChars :: (Ord c, Enum c, Bounded c) => RE c -> P.Partition c
-leadingChars (REChars cs)    = P.fromRSet cs
-leadingChars (REUnion cs rs) = P.fromRSet cs <> foldMap leadingChars rs
-leadingChars (REStar r)      = leadingChars r
-leadingChars (REAppend rs)   = leadingCharsAppend rs
-
-leadingCharsAppend :: (Ord c, Enum c, Bounded c) => [RE c] -> P.Partition c
-leadingCharsAppend [] = P.whole
-leadingCharsAppend (r : rs)
-    | nullable r = leadingChars r <> leadingCharsAppend rs
-    | otherwise  = leadingChars r
-
--------------------------------------------------------------------------------
--- Equivalence
--------------------------------------------------------------------------------
-
--- | Whether two regexps are equivalent.
---
--- @
--- 'equivalent' re1 re2 <=> forall s. 'match' re1 s === 'match' re1 s
--- @
---
--- >>> let re1 = star "a" <> "a"
--- >>> let re2 = "a" <> star "a"
---
--- These are different regular expressions, even we perform
--- some normalisation-on-construction:
---
--- >>> re1 == re2
--- False
---
--- They are however equivalent:
---
--- >>> equivalent re1 re2
--- True
---
--- The algorithm works by executing 'states' on "product" regexp,
--- and checking whether all resulting states are both accepting or rejecting.
---
--- @
--- re1 == re2 ==> 'equivalent' re1 re2
--- @
---
--- === More examples
---
--- >>> let example re1 re2 = putPretty re1 >> putPretty re2 >> return (equivalent re1 re2)
--- >>> example re1 re2
--- ^a*a$
--- ^aa*$
--- True
---
--- >>> example (star "aa") (star "aaa")
--- ^(aa)*$
--- ^(aaa)*$
--- False
---
--- >>> example (star "aa" <> star "aaa") (star "aaa" <> star "aa")
--- ^(aa)*(aaa)*$
--- ^(aaa)*(aa)*$
--- True
---
--- >>> example (star ("a" \/ "b")) (star $ star "a" <> star "b")
--- ^[a-b]*$
--- ^(a*b*)*$
--- True
---
-equivalent :: forall c. (Ord c, Enum c, Bounded c) => RE c -> RE c -> Bool
-equivalent x0 y0 = go mempty [(x0, y0)] where
-    go :: Set (RE c, RE c) -> [(RE c, RE c)] -> Bool
-    go !_ [] = True
-    go acc (p@(x, y) : zs)
-        | p `Set.member` acc = go acc zs
-        -- if two regexps are structurally the same, we don't need to recurse.
-        | x == y             = go (Set.insert p acc) zs
-        | all agree ps       = go (Set.insert p acc) (ps ++ zs)
-        | otherwise = False
-      where
-        cs = toList $ P.examples $ leadingChars x `P.wedge` leadingChars y
-        ps = map (\c -> (derivate c x, derivate c y)) cs
-
-    agree :: (RE c, RE c) -> Bool
-    agree (x, y) = nullable x == nullable y
-
-instance (Ord c, Enum c, Bounded c) => C.Equivalent c (RE c) where
-    equivalent = equivalent
-
--------------------------------------------------------------------------------
--- Generation
--------------------------------------------------------------------------------
-
--- | Generate random strings of the language @RE c@ describes.
---
--- >>> let example = traverse_ print . take 3 . generate (curry QC.choose) 42
--- >>> example "abc"
--- "abc"
--- "abc"
--- "abc"
---
--- >>> example $ star $ "a" \/ "b"
--- "aaaaba"
--- "bbba"
--- "abbbbaaaa"
---
--- >>> example empty
---
--- prop> all (match r) $ take 10 $ generate (curry QC.choose) 42 (r :: RE Char)
---
-generate
-    :: (c -> c -> QC.Gen c) -- ^ character range generator
-    -> Int    -- ^ seed
-    -> RE c
-    -> [[c]]  -- ^ infinite list of results
-generate c seed re
-    | isEmpty re = []
-    | otherwise  = QC.unGen (QC.infiniteListOf (generator c re)) (QC.mkQCGen seed) 10
-
-generator
-    :: (c -> c -> QC.Gen c)
-    -> RE c
-    -> QC.Gen [c]
-generator c = go where
-    go (REChars cs)    = goChars cs
-    go (REAppend rs)   = concat <$> traverse go rs
-    go (REUnion cs rs)
-        | RSet.null  cs = QC.oneof [ go r | r <- toList rs ]
-        | otherwise     = QC.oneof $ goChars cs : [ go r | r <- toList rs ]
-    go (REStar r)      = QC.sized $ \n -> do
-        n' <- QC.choose (0, n)
-        concat <$> sequence (replicate n' (go r))
-
-    goChars cs = pure <$> QC.oneof [ c x y | (x,y) <- RSet.toRangeList cs ]
-
--------------------------------------------------------------------------------
--- Instances
--------------------------------------------------------------------------------
-
-instance Eq c => Semigroup (RE c) where
-    r <> r' = appends [r, r']
-
-instance Eq c => Monoid (RE c) where
-    mempty  = eps
-    mappend = (<>)
-    mconcat = appends
-
-instance (Ord c, Enum c, Bounded c) => JoinSemiLattice (RE c) where
-    r \/ r' = unions [r, r']
-
-instance (Ord c, Enum c, Bounded c) => BoundedJoinSemiLattice (RE c) where
-    bottom = empty
-
-instance c ~ Char => IsString (RE c) where
-    fromString = string
-
-instance (Ord c, Enum c, Bounded c, QC.Arbitrary c) => QC.Arbitrary (RE c) where
-    arbitrary = QC.sized arb where
-        c :: QC.Gen (RE c)
-        c = REChars . RSet.fromRangeList <$> QC.arbitrary
-
-        arb :: Int -> QC.Gen (RE c)
-        arb n | n <= 0    = QC.oneof [c, fmap char QC.arbitrary, pure eps]
-              | otherwise = QC.oneof
-            [ c
-            , pure eps
-            , fmap char QC.arbitrary
-            , liftA2 (<>) (arb n2) (arb n2)
-            , liftA2 (\/) (arb n2) (arb n2)
-            , fmap star (arb n2)
-            ]
-          where
-            n2 = n `div` 2
-
-instance (QC.CoArbitrary c) => QC.CoArbitrary (RE c) where
-    coarbitrary (REChars cs)    = QC.variant (0 :: Int) . QC.coarbitrary (RSet.toRangeList cs)
-    coarbitrary (REAppend rs)   = QC.variant (1 :: Int) . QC.coarbitrary rs
-    coarbitrary (REUnion cs rs) = QC.variant (2 :: Int) . QC.coarbitrary (RSet.toRangeList cs, Set.toList rs)
-    coarbitrary (REStar r)      = QC.variant (3 :: Int) . QC.coarbitrary r
-
--------------------------------------------------------------------------------
--- JavaScript
--------------------------------------------------------------------------------
-
-instance c ~ Char => Pretty (RE c) where
-    prettyS x = showChar '^' . go False x . showChar '$'
-      where
-        go :: Bool -> RE Char -> ShowS
-        go p (REStar a)
-            = parens p
-            $ go True a . showChar '*'
-        go p (REAppend rs)
-            = parens p $ goMany id rs
-        go p (REUnion cs rs)
-            | RSet.null cs = goUnion p rs
-            | Set.null rs  = prettyS cs
-            | otherwise    = goUnion p (Set.insert (REChars cs) rs)
-        go _ (REChars cs)
-            = prettyS cs
-
-        goUnion p rs
-            | Set.member eps rs = parens p $ goUnion' True . showChar '?'
-            | otherwise         = goUnion' p
-          where
-            goUnion' p' = case Set.toList (Set.delete eps rs) of
-                [] -> go True empty
-                [r] -> go p' r
-                (r:rs') -> parens True $ goSome1 (showChar '|') r rs'
-
-        goMany :: ShowS -> [RE Char] -> ShowS
-        goMany sep = foldr (\a b -> go False a . sep . b) id
-
-        goSome1 :: ShowS -> RE Char -> [RE Char] -> ShowS
-        goSome1 sep r = foldl (\a b -> a . sep . go False b) (go False r)
-
-        parens :: Bool -> ShowS -> ShowS
-        parens True  s = showString "(" . s . showChar ')'
-        parens False s = s
-
--------------------------------------------------------------------------------
--- Doctest
--------------------------------------------------------------------------------
-
--- $setup
--- >>> :set -XOverloadedStrings
--- >>> import Control.Monad (void)
--- >>> import Data.Foldable (traverse_)
--- >>> import Data.List (sort)
---
--- >>> import Test.QuickCheck ((===))
--- >>> import qualified Test.QuickCheck as QC
---
--- >>> import Kleene.Classes (match)
--- >>> let asREChar :: RE Char -> RE Char; asREChar = id
+-- This to include orphans.
+import Kleene.Internal.RE
+import Kleene.DFA ()