\begin{comment}
\begin{code}
{-# LANGUAGE ScopedTypeVariables
           , TemplateHaskell
           , ConstraintKinds
           , GeneralizedNewtypeDeriving
#-}

module Control.DFST.Lens
  ( StringEdit(..), sePos, seInsertion
  , StringEdits(..), _StringEdits, _SEFail, stringEdits
  , insert, delete, replace
  , DFSTAction(..), DFSTComplement
  , dfstLens
  , module Control.DFST
  , module Control.Lens.Edit
  ) where

import Control.DFST
import Control.FST hiding (stInitial, stTransition, stAccept)
import qualified Control.FST as FST (stInitial, stTransition, stAccept, step)
import Control.Lens.Edit
import Control.Lens
import Control.Lens.TH
import Control.Edit

import Control.Monad

import Numeric.Natural
import Numeric.Interval (Interval, (...))
import qualified Numeric.Interval as Int

import Data.Sequence (Seq((:<|), (:|>)))
import qualified Data.Sequence as Seq
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Map.Lazy (Map)
import qualified Data.Map.Lazy as Map

import Data.Compositions (Compositions)
import qualified Data.Compositions as Comp

import Data.Algorithm.Diff (Diff, getDiff)
import qualified Data.Algorithm.Diff as Diff

import Data.Monoid
import Data.Bool (bool)
import Data.Maybe (fromMaybe, maybeToList, listToMaybe, catMaybes, isNothing, isJust)
import Data.Function (on)
import Data.Foldable (toList)
import Data.List (partition)

import Control.Exception (assert)

import System.IO.Unsafe
import Text.PrettyPrint.Leijen (Pretty(..))

\end{code}
\end{comment}


Wir betrachten, zur Einfachheit, ein minimiales Set von Edits auf Strings\footnote{Wie in der Konstruktion zum Longest Common Subsequence Problem}:

\begin{defn}[Atomare edits of strings]
\begin{code}
data StringEdit pos char = Insert { _sePos :: pos, _seInsertion :: char }
                         | Delete { _sePos :: pos }
  deriving (Eq, Ord, Show, Read)

-- Automatically derive van-leerhoven-lenses:
--
-- @sePos :: Lens' (StringEdits pos char) pos@
-- @seInsertion :: Traversal' (StringEdits pos char) char@
makeLenses ''StringEdit
\end{code}
\end{defn}

Atomare edits werden, als Liste, zu edits komponiert.
Wir führen einen speziellen edit ein, der nicht-Anwendbarkeit der edits repräsentiert:
\begin{code}
data StringEdits pos char = StringEdits (Seq (StringEdit pos char))
                          | SEFail
  deriving (Eq, Ord, Show, Read)

makePrisms ''StringEdits

stringEdits :: Traversal (StringEdits pos char) (StringEdits pos' char') (StringEdit pos char) (StringEdit pos' char')
\end{code}
\begin{comment}
\begin{code}
stringEdits = _StringEdits . traverse
\end{code}
\end{comment}
\begin{code}
insert :: pos -> char -> StringEdits pos char
\end{code}
\begin{comment}
\begin{code}
insert n c = StringEdits .  Seq.singleton $ Insert n c
\end{code}
\end{comment}
\begin{code}
delete :: pos -> StringEdits pos char
\end{code}
\begin{comment}
\begin{code}
delete n = StringEdits .  Seq.singleton $ Delete n
\end{code}
\end{comment}
\begin{code}
replace :: Eq pos => pos -> char -> StringEdits pos char
\end{code}
\begin{comment}
\begin{code}
replace n c = insert n c <> delete n

-- | Rudimentarily optimize edit composition
instance Eq pos => Monoid (StringEdits pos char) where
  mempty = StringEdits Seq.empty
  SEFail `mappend` _ = SEFail
  _ `mappend` SEFail = SEFail
  (StringEdits Seq.Empty) `mappend` x = x
  x `mappend` (StringEdits Seq.Empty) = x
  (StringEdits x@(bs :|> b)) `mappend` (StringEdits y@(a :<| as))
    | (Insert n _) <- a
    , (Delete n') <- b
    , n == n'
    = StringEdits bs `mappend` StringEdits as
    | otherwise = StringEdits $ x `mappend` y
\end{code}
\end{comment}

Da wir ein minimales set an atomaren edits gewählt haben, ist die Definiton der Modulnstruktur über Strings des passenden Alphabets recht einfach:
\begin{code}
instance Module (StringEdits Natural char) where
  type Domain (StringEdits Natural char) = Seq char
  apply str SEFail = Nothing
  apply str (StringEdits Seq.Empty) = Just str
  apply str (StringEdits (es :|> Insert n c)) = flip apply (StringEdits es) =<< go str n c
    where
      go Seq.Empty n c
        | n == 0 = Just $ Seq.singleton c
        | otherwise = Nothing
      go str@(x :<| xs) n c
        | n == 0 = Just $ c <| str
        | otherwise = (x <|) <$> go xs (pred n) c
  apply str (StringEdits (es :|> Delete n)) = flip apply (StringEdits es) =<< go str n
    where
      go Seq.Empty _ = Nothing
      go (x :<| xs) n
        | n == 0 = Just xs
        | otherwise = (x <|) <$> go xs (pred n)

  init = Seq.empty
  divInit = StringEdits . Seq.unfoldl go . (0,)
    where
      go (_, Seq.Empty) = Nothing
      go (n, c :<| cs ) = Just ((succ n, cs), Insert n c)

\end{code}

% TODO Make notation mathy

Um zunächst eine asymmetrische edit-lens \texttt{StringEdits -> StringEdits} mit akzeptabler Komplexität für einen bestimmten DFST (entlang der \emph{Richtung} des DFSTs) zu konstruieren möchten wir folgendes Verfahren anwenden:

Gegeben eine Sequenz von zu übersetzenden Änderungen genügt es die Übersetzung eines einzelnen \texttt{StringEdit}s in eine womöglich längere Sequenz von \texttt{StringEdits} anzugeben, alle \texttt{StringEdits} aus der Sequenz derart zu übersetzen (hierbei muss auf die korrekte Handhabung des Komplements geachtet werden) und jene Übersetzungen dann zu concatenieren.

Wir definieren zunächst die \emph{Wirkung} eines DFST auf einen festen String als eine Abbildung \texttt{state -> (Seq output, Maybe state)}, die den aktuellen Zustand vor dem Parsen des Strings auf den Zustand danach und die (womöglich leere) Ausgabe schickt.
Wir annotieren Wirkungen zudem mit dem konsumierten String.
Diese Wirkungen bilden einen Monoiden analog zu Endomorphismen, wobei die Resultat-Strings concateniert werden.

\begin{code}
data DFSTAction state input output = DFSTAction
  { runDFSTAction :: state -> (Seq output, Maybe state)
  , dfstaConsumes :: Seq input
  }

instance Monoid (DFSTAction state input output) where
\end{code}
\begin{comment}
\begin{code}
  mempty = DFSTAction (\x -> (Seq.empty, Just x)) Seq.empty
  DFSTAction f cf `mappend` DFSTAction g cg = DFSTAction
    { runDFSTAction = \x ->
        let (outG, x') = g x
            (outF, x'') = maybe (mempty, Nothing) f x'
         in (outG <> outF, x'')
    , dfstaConsumes = cg <> cf
    }
\end{code}
\end{comment}
\begin{code}

type DFSTComplement state input output = Compositions (DFSTAction state input output)

runDFSTAction' :: DFSTComplement state input output -> state -> (Seq output, Maybe state)
runDFSTAction' = runDFSTAction . Comp.composed

dfstaConsumes' :: DFSTComplement state input output -> Seq input
dfstaConsumes' = dfstaConsumes . Comp.composed

dfstaProduces :: DFSTComplement state input output -> state -> Seq output
dfstaProduces = fmap fst . runDFSTAction'
\end{code}

Die Unterliegende Idee von $\Rrightarrow$ ist nun im Komplement der edit-lens eine Liste von Wirkungen (eine für jedes Zeichen der Eingabe des DFSTs) und einen Cache der monoidalen Summen aller kontinuirlichen Teillisten zu halten.

Wir können die alte DFST-Wirkung zunächst anhand des Intervalls indem der input-String von allen gegebenen edits betroffen ist in einen unveränderten Prefix und einen womöglich betroffenen Suffix unterteilen.

Da wir wissen welche Stelle im input-String vom ersten gegebenen edit betroffen ist können wir, anhand der Wirkung des Teilstücks bis zu jener Stelle, den betroffenen Suffix wiederum teilen.
Die Wirkung ab der betroffenen Stelle im input-String können wir als Komposition der Wirkung der durch den edit betroffenen Stelle und derer aller Zeichen danach bestimmen.
Nun gilt es nur noch die Differenz (als `StringEdits`) des vorherigen Suffixes im output-String und des aus der gerade berechneten Wirkung zu bestimmen, wir bedienen uns hierzu dem Unix Standard-Diff-Algorithmus zwischen der ursprünglichen Ausgabe und dem Ergebnis der Iteration des Verfahrens auf alle gegebenen edits.

Für die asymmetrische edit-lens entgegen der DFST-Richtung $\Lleftarrow$ verwenden wir Breitensuche über die Zustände des DFST innerhalb eines iterative vergrößerten Intervalls:

Wir bestimmen zunächst (`affected`) eine obere Schranke an das Intervall in dem der Ausgabe-String vom edit betroffen ist und generieren eine von dort quadratisch wachsende Serie von Intervallen.

Für jedes Intervall ("lokalere" Änderungen werden präferiert) schränken wir zunächst den DFST (zur einfachereren Implementierung in seiner Darstellung als FST) vermöge \texttt{restrictOutput} derart ein, dass nur die gewünschte Ausgabe produziert werden kann.

Wir betrachten dann in jedem Schritt (beginnend mit dem initialen Zustand des DFST) alle ausgehenden Transitionen und ziehen hierbei jene vor, die im vorherigen Lauf (gespeichert im Komplement der edit-lens), ebenfalls genommen wurden.
Abweichungen vom im Komplement gespeicherten Lauf lassen wir nur innerhalb des betrachteten Intervalls zu und wählen in diesem Fall einen Edit auf der Eingabe, der die gewählte Abweichung produziert.
Es wird zudem, wie für Breitensuche üblich, jeder besuchte Zustand markiert und ausgehende Transitionen nicht ein zweites mal betrachtet.

Erreichen wir einen finalen Zustand (wegen der Einschränkung des DFSTs wurde dann auch genau die gewünschte Ausgabe produziert), so fügen wir an die gesammelten Eingabe-edits eine Serie von deletions an, die den noch nicht konsumierten suffix der Eingabe verwerfen und brechen die Suche unter Rückgabe der Eingabe-edits und des neuen Laufs ab.

In Haskell formulieren wir das vorzeitige Abbrechen der Suche indem wir eine vollständige Liste von Rückgabe-Kandidaten konstruieren und dann immer ihr erstes Element zurück geben.
Wegen der verzögerten Auswertungsstrategie von Haskell wird auch tatsächlich nur der erste Rückgabe-Kandidat konstruiert.

\begin{comment}
\begin{code}
type LState state input output = (Natural, (state, Maybe (input, Natural)))
\end{code}
\end{comment}
\begin{code}
dfstLens :: forall state input output. (Ord state, Ord input, Ord output, Show state, Show input, Show output) => DFST state input output -> EditLens (DFSTComplement state input output) (StringEdits Natural input) (StringEdits Natural output)
\end{code}
\begin{comment}
\begin{code}
dfstLens dfst@DFST{..} = EditLens ground propR propL
  where
    ground :: DFSTComplement state input output
    ground = mempty

    propR :: (DFSTComplement state input output, StringEdits Natural input) -> (DFSTComplement state input output, StringEdits Natural output)
    propR (c, SEFail) = (c, SEFail)
    propR (c, StringEdits Seq.Empty) = (c, mempty)
    propR (c, es'@(StringEdits (es :> e)))
      | (_, Just final) <- runDFSTAction' c' stInitial
      , final `Set.member` stAccept
      = (c', rEs)
      | otherwise
      = (c, SEFail)
      where
        Just int = affected es'
        (cAffSuffix, cAffPrefix) = Comp.splitAt (Comp.length c - fromIntegral (Int.inf int)) c
        (cSuffix, cPrefix) = Comp.splitAt (Comp.length c - (e ^. sePos . from enum)) c
        cSuffix'
          | Delete _       <- e
          , Comp.length cSuffix > 0 = Comp.take (pred $ Comp.length cSuffix) cSuffix
          | Insert _ nChar <- e = cSuffix <> Comp.singleton (DFSTAction (\x -> runDFST' dfst x (pure nChar) Seq.empty) (Seq.singleton nChar))
          | otherwise = Comp.singleton $ DFSTAction (\_ -> (Seq.empty, Nothing)) Seq.empty
        (c', _) = propR (cSuffix' <> cPrefix, StringEdits es)
        (cAffSuffix', _) = Comp.splitAt (Comp.length c' - Comp.length cAffPrefix) c'
        (_, Just pFinal) = runDFSTAction' cPrefix stInitial
        rEs = strDiff (fst $ runDFSTAction' cAffSuffix pFinal) (fst $ runDFSTAction' cAffSuffix' pFinal) & stringEdits . sePos . from enum +~ length (dfstaProduces cAffPrefix stInitial)
        

    propL :: (DFSTComplement state input output, StringEdits Natural output) -> (DFSTComplement state input output, StringEdits Natural input)
    propL (c, StringEdits Seq.Empty) = (c, mempty)
    propL (c, es) = fromMaybe (c, SEFail) $ do
      let prevOut = dfstaProduces c stInitial
      newOut <- prevOut `apply` es
      affected' <- affected es
      let outFST :: FST (LState state input output) input output
          -- outFST = wordFST newOut `productFST` toFST dfst
          outFST = restrictOutput newOut $ toFST dfst
      
          trace x y = flip seq y . unsafePerformIO $ appendFile "lens.log" (x <> "\n\n")

          inflate by int
            | Int.null int = Int.empty
            | inf >= by = inf - by Int.... sup + by
            | otherwise = 0 Int.... sup + by
            where
              (inf, sup) = (,) <$> Int.inf <*> Int.sup $ int
          fragmentIntervals = (++ [all]) . takeWhile (not . Int.isSubsetOf (0 Int.... max)) $ inflate <$> 0 : [ 2^n | n <- [0..ceiling (logBase 2.0 max)] ] <*> pure affected'
            where
              max :: Num a => a
              max = fromIntegral $ Seq.length newOut
              all = 0 Int.... max
          runCandidates :: Interval Natural -- ^ Departure from complement-run only permitted within interval (to guarantee locality)
                        -> [ ( Seq (LState state input output, Maybe output) -- ^ Computed run
                             , StringEdits Natural input
                             , DFSTComplement state input output
                             )
                           ]
          runCandidates focus = map ((,,) <$> view _1 <*> view _2 <*> view (_3 . _2)) $ go Set.empty [(Seq.empty, mempty, (c, mempty), 0)]
            where
              go _ [] = []
              go visited (args@(run, edits, compZipper, inP) : alts) = 
                  [ (run', finalizeEdits remC inP' edits', compZipper', inP') | (run', edits', compZipper'@(remC, _), inP') <- args : conts, isFinal run' ]
                  ++ go visited' (alts ++ conts)
                where
                  conts
                    | lastSt <- view _1 <$> Seq.lookup (pred $ Seq.length run) run
                    , lastSt `Set.member` visited = []
                    | otherwise = continueRun edits compZipper inP run
                  visited' = Set.insert (view _1 <$> Seq.lookup (pred $ Seq.length run) run) visited

              isFinal :: Seq (LState state input output, Maybe output) -> Bool
              -- ^ Is the final state of the run a final state of the DFST?
              isFinal Seq.Empty = (0, (stInitial, Nothing)) `Set.member` FST.stAccept outFST
                               && (0 Int.... fromIntegral (Seq.length newOut)) `Int.isSubsetOf` focus
              isFinal (_ :> (lastSt, _)) = lastSt `Set.member` FST.stAccept outFST

              finalizeEdits :: DFSTComplement state input output -- ^ Remaining complement
                            -> Natural -- ^ Input position
                            -> StringEdits Natural input -> StringEdits Natural input
              finalizeEdits remC inP = mappend . mconcat . replicate (Seq.length $ dfstaConsumes' remC) $ delete inP
              
              continueRun :: StringEdits Natural input
                          -> (DFSTComplement state input output, DFSTComplement state input output) -- ^ Zipper into complement
                          -> Natural -- ^ Input position
                          -> Seq (LState state input output, Maybe output)
                          -> [ ( Seq (LState state input output, Maybe output)
                               , StringEdits Natural input
                               , (DFSTComplement state input output, DFSTComplement state input output)
                               , Natural
                               )
                             ]
              -- ^ Nondeterministically make a single further step, continueing a given run
              continueRun inEdits (c', remC) inP run = do
                let
                  pos :: Natural
                  -- pos = fromIntegral $ Comp.length c - Comp.length c' -- FIXME: should use length of dfstaProduces
                  pos = fromIntegral . Seq.length $ dfstaProduces remC stInitial
                  (c'', step) = Comp.splitAt (pred $ Comp.length c') c' -- TODO: unsafe?
                  current :: LState state input output
                  current
                    | Seq.Empty <- run      = (0, (stInitial, Nothing))
                    | (_ :> (st, _)) <- run = st
                  current' :: state
                  oldIn :: Maybe input
                  (current', oldIn)
                    | (_ :> ((_, (st, _)), _)) <- rest
                    , (_ :> ((_, (_, Just (partialIn, _))), _)) <- partial = (st, Just partialIn)
                    | (_ :> ((_, (_, Just (partialIn, _))), _)) <- partial = (stInitial, Just partialIn)
                    | Seq.Empty <- rest = (stInitial, Seq.lookup 0 $ dfstaConsumes' step)
                    | (_ :> ((_, (st, _)), _)) <- rest = (st, Seq.lookup 0 $ dfstaConsumes' step)
                    where
                      (partial, rest) = Seq.spanr (\((_, (_, inp)), _) -> isJust inp) run
                next' <- trace (show ("next'", pos, focus, run, (current', oldIn), current, dfstaConsumes' step, runDFST' dfst current' (maybe Seq.empty Seq.singleton oldIn) Seq.empty)) . maybeToList . snd $ runDFST' dfst current' (maybe Seq.empty Seq.singleton oldIn) Seq.empty
                let
                  outgoing :: LState state input output -> [(LState state input output, Maybe input, Maybe output)]
                  outgoing current = let go (st, minS) outs acc
                                           | st == current = Set.foldr (\(st', moutS) -> ((st', minS, moutS) :)) acc outs
                                           | otherwise     = acc
                                      in Map.foldrWithKey go [] $ FST.stTransition outFST 
                  isPreferred :: (LState state input output, Maybe input, Maybe output) -> Bool
                  isPreferred ((_, (st, Nothing)), _, _) = st == next'
                  isPreferred (st@(_, (_, Just (inS , _))), _, _) = maybe True (== inS) oldIn && any isPreferred (outgoing st) -- By construction of `outFST`, `outgoing st` is a singleton in this case
                  (preferred, alternate) = partition isPreferred $ outgoing current
                  assocEdit :: (LState state input output, Maybe input, Maybe output) -- ^ Transition
                            -> [ ( (DFSTComplement state input output, DFSTComplement state input output) -- ^ new `(c', remC)`, i.e. complement-zipper `(c', remC)` but with edit applied
                                 , StringEdits Natural input
                                 , Natural
                                 )
                               ]
                  assocEdit (_, Just inS, _)
                    | oldIn == Just inS = [ ((c'', step <> remC), mempty, succ inP) ]
                    | isJust oldIn      = [ ((c', altStep inS <> remC), insert inP inS, succ inP)
                                          , ((c'', altStep inS <> remC), replace inP inS, succ inP)
                                          ]
                    | otherwise         = [ ((c', altStep inS <> remC), insert inP inS, succ inP) ]
                  assocEdit (_, Nothing, _) = [((c', remC), mempty, inP)]
                  altStep :: input -> DFSTComplement state input output
                  altStep inS = Comp.singleton DFSTAction{..}
                    where
                      dfstaConsumes = Seq.singleton inS
                      runDFSTAction x = runDFST' dfst x (pure inS) Seq.empty
                  options
                    | pos `Int.member` focus = preferred ++ alternate
                    | otherwise              = preferred
                choice@(next, inS, outS) <- trace (unlines $ show (pretty outFST) : map show options) options
                ((c3, remC'), inEdits', inP') <- assocEdit choice
                -- let
                --   -- | Replace prefix of old complement to reflect current candidate
                --   -- TODO: smarter?
                --   (_, ((c3 <>) -> newComplement')) = Comp.splitAt (Comp.length c') c -- TODO: unsafe?
                --   acc = (run :> (next, outS), inEdits' <> inEdits, newComplement')
                --   dropSuffix = mconcat (replicate (Seq.length $ dfstaConsumes' c3) $ delete inP')
                --   fin
                --     | (trans, inEs, newComplement) <- acc = (trans, dropSuffix <> inEs, newComplement)
                let
                  trans = run :> (next, outS)
                  inEs = inEdits' <> inEdits
                --   dropSuffix = mconcat (replicate (Seq.length $ dfstaConsumes' c3) $ delete inP')
                --   fin
                --     | (trans, inEs) <- acc = (trans, dropSuffix <> inEs, remC')
                -- bool id (over _BFS $ cons fin) (next `Set.member` FST.stAccept outFST) $ continueRun acc (c3, remC') inP'
                return (trans, inEs, (c3, remC'), inP')
              
      -- Properties of the edits computed are determined mostly by the order candidates are generated below
      -- (_, inEs, c') <- (\xs -> foldr (\x f -> x `seq` f) listToMaybe xs $ xs) $ traceShowId fragmentIntervals >>= (\x -> (\y@(y1, y2, _) -> traceShow (y1, y2) y) <$> runCandidates x)

      fmap ((,) <$> view _3 <*> view _2) .  listToMaybe $ runCandidates =<< fragmentIntervals

strDiff :: forall sym pos. (Eq sym, Integral pos) => Seq sym -> Seq sym -> StringEdits pos sym
-- ^ @strDiff a b@ calculates a set of edits, which, when applied to @a@, produce @b@
strDiff a b = snd . foldl toEdit (0, mempty) $ (getDiff `on` toList) a b
  where
    toEdit :: (pos, StringEdits pos sym) -> Diff sym -> (pos, StringEdits pos sym)
    toEdit (n, es) (Diff.Both _ _) = (succ n, es)
    toEdit (n, es) (Diff.First _ ) = (n, delete n <> es)
    toEdit (n, es) (Diff.Second c) = (succ n, insert n c <> es)
\end{code}
\end{comment}

Um eine obere Schranke an das von einer Serie von edits betroffene Intervall zu bestimmen ordnen wir zunächst jeder von mindestens einem atomaren edit betroffenen Position $n$ im Eingabe-Wort einen $\text{offset}_n = \text{\# deletions} - \text{\# inserts}$ zu.
Das gesuchte Intervall ist nun $(\text{minK}, \text{maxK})$, mit $\text{minK}$ der Position im Eingabe-Wort mit niedrigstem $\text{offset}$ und $\text{maxK}$ die Position im Eingabe-Wort mit höchstem $\text{offset}$, $\text{maxK}^\prime$, modifiziert um das Maximum aus $\{ 0 \} \cup \{ \text{maxK}_n \colon n \in \{ 0 \ldots \text{maxK}^\prime \} \}$ wobei $\text{maxK}_n = -1 \cdot (n + \text{offset}_n)$ an Position $n$ ist.

\begin{code}
affected :: forall char. StringEdits Natural char -> Maybe (Interval Natural)
-- ^ For a given set of edits @es@ return the interval @i = a ... b@ such that for any given string @str@ of sufficient length the following holds:
--
--   - For all @n :: Natural@: @n < a ==> str ! n == (str `apply` es) ! n@
--   - There exists a @k :: Integer@ such that for all @n :: Integer@: @n > b ==> str ! (n + k) == (str `apply` es) ! n@
--
-- Intuitively: for any character @c@ of the new string @str `apply` es@ there exists a corresponding character in @str@ (offset by either 0 or a constant shift @k@) if the index of @c@ is /not/ contained in @affected es@.
\end{code}
\begin{comment}
\begin{code}
affected SEFail = Nothing
affected (StringEdits es) = Just . toInterval $ go es Map.empty
  where
    toInterval :: Map Natural Integer -> Interval Natural
    toInterval map
      | Just (((minK, _), _), ((maxK, _), _)) <- (,) <$> Map.minViewWithKey map <*> Map.maxViewWithKey map
      = let
          maxV' = maximum . (0 :) $ do
            offset <- [0..maxK]
            v <- maybeToList $ Map.lookup (maxK - offset) map
            v' <- maybeToList . fmap fromInteger $ negate v <$ guard (v <= 0)
            guard $ v' >= succ offset
            return $ v' - offset
        in (minK Int.... maxK + maxV')
      | otherwise
      = Int.empty
    go :: Seq (StringEdit Natural char) -> Map Natural Integer -> Map Natural Integer
    go Seq.Empty offsets = offsets
    go (es :> e) offsets = go es offsets'
      where
        p = e ^. sePos
        -- p' = fromIntegral $ Map.foldrWithKey (\k o p -> bool (fromIntegral p) (o + p) $ k < fromIntegral p) (fromIntegral p) offsets
        offsets' = Map.alter (Just . myOffset . fromMaybe 0) p offsets
        myOffset :: Integer -> Integer
        myOffset
          | Insert _ _ <- e = pred
          | Delete _   <- e = succ
\end{code}
\end{comment}