\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 qualified Data.Map as Strict (Map)
import qualified Data.Map.Strict as Strict.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, mapMaybe)
import Data.Function (on)
import Data.Foldable (toList)
import Data.List (partition, isPrefixOf)

import Control.Exception (assert)

import System.IO (Handle, hPutStrLn, IOMode(AppendMode), withFile)
import System.IO.Unsafe
import Text.PrettyPrint.Leijen (Pretty(..))

import Data.Universe (Finite(..))

\end{code}
\end{comment}


\begin{defn}[Atomare edits of strings]
Wir betrachten, zur Einfachheit, ein minimiales Set von Edits auf Strings\footnote{Wie in der Konstruktion zum Longest Common Subsequence Problem}, bestehend nur aus Einfügung eines einzelnen Zeichens und löschen des Zeichens an einer einzelnen Position:

\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}

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}
\end{defn}

\begin{comment}
\begin{code}
stringEdits = _StringEdits . traverse

insert :: pos -> char -> StringEdits pos char
insert n c = StringEdits .  Seq.singleton $ Insert n c

delete :: pos -> StringEdits pos char
delete n = StringEdits .  Seq.singleton $ Delete n

replace :: Eq pos => pos -> char -> StringEdits pos char
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}

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}
dfstAction :: forall state input output. (Finite state, Ord state, Ord input) => DFST state input output -> input -> DFSTAction state input output
-- | Smart constructor of `DFSTAction` ensuring that `Seq.length . dfstaConsumes == const 1` and that `runDFSTAction` has constant complexity
\end{code}
\begin{comment}
\begin{code}
dfstAction dfst (Seq.singleton -> dfstaConsumes) = DFSTAction{..}
  where
    runDFSTAction :: state -> (Seq output, Maybe state)
    runDFSTAction = (actionMap Strict.Map.!)

    actionMap :: Strict.Map state (Seq output, Maybe state)
    actionMap = Strict.Map.fromSet (\st -> runDFST' dfst st dfstaConsumes Seq.empty) $ Set.fromList universeF
\end{code}
\end{comment}

Wir halten im Komplement der edit-lens einen Cache der monoidalen Summen aller kontinuirlichen Teillisten.
\texttt{Compositions} ist ein balancierter Binärbaum, dessen innere Knoten mit der monoidalen Summe der Annotationen aller Blätter annotiert sind.
\begin{code}
type DFSTComplement state input output = Compositions (DFSTAction state input output)
\end{code}

\begin{code}
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}

Für $\Rrightarrow$ können wir die alte DFST-Wirkung zunächst anhand des Intervalls indem der input-String von allen gegebenen edits betroffen ist (\texttt{affected}) 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 des von allen gegeben edits betroffenen Intervalls:

Wir unterteilen zunächst das Komplement an den Grenzen des betroffenen Intervalls im output-String in drei Teile (durch Akkumulation der Elemente des Komplements bis die gewünschte Länge erreicht ist).

Wir transformieren dann den DFST in einen FST, dessen Ausgabe wir mit \texttt{restrictOutput} auf das gewünschte Fragment einschränken, setzen als initialen Zustand des FST den Zustand am linken Rand des von den edits betroffenen Intervalls und akzeptieren jene Zustände, von denen aus das Komplement-Fragment ab dem rechten Rand des betroffenen Intervalls zu einem im ursprünglichen DFST akzeptierten Zustand führt.

Wir verwenden dann gewöhnliche Breitensuche über die Zustände und Transitionen des soeben konstruierten FSTs um einen Lauf-Fragment zu bestimmen, dass wir in das betroffene Intervall einsetzen können.
Hierbei sind sämtliche Randbedingungen (korrekte Ausgabe, Übereinstimmung an den Intervallgrenzen) bereits in den FST kodiert sodass wir nur noch prüfen müssen, dass der gefunde Lauf in einem akzeptierten Zustand endet.

Die input-edits können nun wiederum, unter Beachtung der Verschiebung der indices um die Länge der Eingabe vor der linken Intervallgrenze, mit dem Unix Standard-Diff-Algorithmus berechnet werden.

\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, Finite state) => 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, lEs@(StringEdits (es :> e)))
      | (_, Just final) <- runDFSTAction' c' stInitial
      , final `Set.member` stAccept
      = (c', rEs)
      | otherwise
      = (c, SEFail)
      where
        Just int = affected lEs
        (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 dfst 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' cAffPrefix stInitial
        rEs = strDiff (dfstaProduces cAffSuffix pFinal) (dfstaProduces 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
      -- Determine states @(iState, fState)@ at the boundary of the region affected by @es@
      ((,) <$> Int.inf <*> Int.sup -> (minAff, maxAff)) <- affected es
      trace (show (minAff, maxAff)) $ Just ()
      let
        prevTrans :: Natural -> Maybe ( DFSTComplement state input output -- ^ Run after chosen transition to accepting state
                                      , (state, input, Seq output, state)
                                      , DFSTComplement state input output -- ^ Run from `stInitial` up to chosen transition
                                      )
        -- ^ Given an index in the output, find the associated transition in @c@
        prevTrans needle = do
          let (after, before) = prevTrans' (c, mempty)
          transSt <- view _2 $ runDFSTAction (Comp.composed before) stInitial
          trace ("transSt = " ++ show transSt) $ Just ()
          let (after', trans) = Comp.splitAt (pred $ Comp.length after) after
              DFSTAction{..} = Comp.composed trans
          [inS] <- return $ toList dfstaConsumes
          (outSs , Just postTransSt) <- return $ runDFSTAction transSt
          return (after', (transSt, inS, outSs, postTransSt), before)
          where
            -- | Move monoid summands from @after@ to @before@ until first transition of @after@ produces @needle@ or @after@ is a singleton
            prevTrans' (after, before)
              | producedNext > needle = (after, before)
              | Comp.length after == 1 = (after, before)
              | otherwise = prevTrans' (after', before')
              where
                producedNext = fromIntegral . Seq.length . traceShowId $ dfstaProduces before' stInitial
                (after', nextTrans) = Comp.splitAt (pred $ Comp.length after) after
                before' = nextTrans `mappend` before
      (_, (iState, _, _, _), prefix) <- prevTrans minAff 
      trace (show (iState, Comp.length prefix)) $ Just ()
      (suffix, (pfState, _, _, fState), _) <- prevTrans maxAff
      trace (show (pfState, fState, Comp.length suffix)) $ Just ()

      newOut <- dfstaProduces c stInitial `apply` es
      let affNewOut = (\s -> Seq.take (Seq.length s - Seq.length (dfstaProduces suffix fState)) s) $ Seq.drop (Seq.length $ dfstaProduces prefix stInitial) newOut
      trace (show (iState, fState, affNewOut)) $ Just ()

      let outFST :: FST (LState state input output) input output
          outFST = restrictOutput affNewOut $ toFST DFST
            { stInitial = iState
            , stTransition
            , stAccept = Set.fromList $ do
                fin <- Set.toList $ stAccept `Set.union` Set.map fst (Map.keysSet stTransition)
                (suffOut, Just fin') <- return $ runDFSTAction' suffix fin
                guard $ Set.member fin' stAccept
                guard $ suffOut == dfstaProduces suffix fState
                return fin
            }
      trace (show $ pretty outFST) $ Just ()

      newPath <-
        let
          FST{ .. } = outFST
          detOutgoing :: Maybe (LState state input output) -> [(LState state input output, (Maybe input, Maybe output))]
          detOutgoing Nothing = concatMap detOutgoing . map Just $ toList stInitial
          detOutgoing (Just st) = concatMap (\((_, inS), outs) -> map (\(st', outS) -> (st', (inS, outS))) $ toList outs) . Map.toList $ Map.filterWithKey (\(st', _) _ -> st == st') stTransition
          predicate :: [(LState state input output, (Maybe input, Maybe output))] -> Maybe Bool
          predicate []
            | not . Set.null $ Set.intersection stInitial stAccept = Just True
            | otherwise = Nothing
          predicate ((lastSt, _) : _)
            | Set.member lastSt stAccept = Just True
            | otherwise = Nothing
        in bfs detOutgoing predicate

      trace (show newPath) $ Just ()

      let oldIn = dfstaConsumes' . Comp.drop (Comp.length suffix) $ Comp.take (Comp.length c - Comp.length prefix) c
          newIn = Seq.fromList . mapMaybe (\(_st, (inS, _outS)) -> inS) $ reverse newPath
          inDiff = oldIn `strDiff` newIn
          diffOffset = fromIntegral . Seq.length $ dfstaConsumes' prefix
          inDiff' = inDiff & stringEdits . sePos +~ diffOffset

      trace (show (oldIn, newIn, inDiff')) $ Just ()

      let affComp = Comp.fromList [ dfstAction dfst inS | (_st, (Just inS, _outS)) <- newPath ]
  
      return (suffix <> affComp <> prefix, inDiff')

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)

-- | Generic breadth-first search
bfs :: forall state transition. Ord state
    => (Maybe state -> [(state, transition)]) -- ^ Find outgoing edges
    -> ([(state, transition)] {- ^ Reverse path -} -> Maybe Bool {- ^ Continue search, finish successfully, or abort search on this branch -}) -- ^ Search predicate
    -> Maybe [(state, transition)] -- ^ Reverse path
bfs outgoing predicate
  | Just True  <- emptyRes = Just []
  | Just False <- emptyRes = Nothing
  | otherwise = bfs' Set.empty . Seq.fromList . map pure $ outgoing Nothing
  where
    emptyRes = predicate []
    
    bfs' :: Set state -- ^ Visited states, not to be checked again
         -> Seq [(state, transition)] -- ^ Search queue of paths to continue
         -> Maybe [(state, transition)]
    bfs' _ Seq.Empty = Nothing
    bfs' visited (c@((lastSt, _) : _) :< cs) = case predicate c of
      Just True  -> Just c
      Just False -> bfs' visited cs
      Nothing -> bfs' visited' $ cs <> Seq.fromList (map (: c) . filter (\(st, _) -> not $ Set.member st visited) . outgoing $ Just lastSt)
      where
        visited' = Set.insert lastSt visited
\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

trace :: String -> a -> a
{-# NOINLINE trace #-}
trace str y = flip seq y . unsafePerformIO . withFile "lens.log" AppendMode $ \h ->
  hPutStrLn h str

traceShowId :: Show a => a -> a
traceShowId x = trace (show x) x
  
  
\end{code}
\end{comment}