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

module Control.DFST.Lens
  ( DFSTAction(..), DFSTComplement
  , dfstLens
  , module Control.Edit.String
  , 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.Edit.ActionTree
import Control.Lens
import Control.Lens.TH
import Control.Edit
import Control.Edit.String
import Control.Edit.String.Affected

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}[Ausgabe-Wirkung von DFSTs]
Wir definieren zunächst die \emph{Ausgabe-Wirkung}\footnote{Wir schreiben im Folgenden auch nur \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}
\end{defn}

\begin{eg} \label{eg:linebreakonw100}
  Die Wirkung des DFST aus Beispiel~\ref{eg:linebreak} auf das Wort $w$ aus Beispiel~\ref{eg:w100} ist:

  \begin{align*}
    \text{act} & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\
    0 & \mapsto (0\, 1\, \ldots\, 80\, \text{\tt \textbackslash n}\, 81\, \ldots\, 98, 19) \\
    1 & \mapsto (0\, 1\, \ldots\, 79\, \text{\tt \textbackslash n}\, 80\, \ldots\, 98, 18) \\
    & \vdots
  \end{align*}
\end{eg}


\begin{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
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 hierbei ein balancierter Binärbaum, dessen innere Knoten mit der monoidalen Summe der Annotationen aller Blätter des jeweiligen Teilbaums annotiert sind.
\begin{code}
type DFSTComplement state input output = Compositions (DFSTAction state input output)
\end{code}

Wir bedienen uns hierbei einer bestehenden Programmbibliothek \cite{composition-tree} um das Balancieren bei Modifikation des Baums nicht implementieren zu müssen.

\begin{eg}
  Wir definieren zunächst einen weiteren, sehr einfachen, DFST:
  
  \begin{figure}[H]
    \centering
    \pinclude{presentation/switchdfst.tex}
    \caption{\label{fig:switchdfst} Ein einfacher DFST, der zwischen zwei Zustanden wechselt und Ausgabe abhängig vom aktuellen Zustand erzeugt}
  \end{figure}

  Auf $s$ wechselt der DFST seinen Zustand, auf $p$ produziert er, abhängig vom aktuellen Zustand, genau ein Zeichen.

  Wir stellen die Wirkung des DFST auf den Eingabe-String $spp$ grafisch analog zur Baumstruktur von \texttt{Compositions} dar.
  Wir bedienen uns hier der Darstellung von Automaten-Wirkungen als \emph{Schaltboxen} aus \cite{hofmann2011automatentheorie}, angepasst für DFSTs indem wir die Ausgabe des transducers an den Pfaden innerhalb der Schaltbox annotieren.
  
  \begin{figure}[H]
    \centering
    \pinclude{presentation/comptree.tex}
    \caption{Die Wirkung der Eingabe $spp$ auf den einfachen transducer aus Abbildung \ref{fig:switchdfst}}
  \end{figure}
\end{eg}

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

Für $\Rrightarrow$ können wir die alte DFST-Wirkung zunächst anhand des Intervalls in dem 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 akzeptierenden Zustand führt.

Wir verwenden dann gewöhnliche Breitensuche über die Zustände und Transitionen des soeben konstruierten FSTs um einen Lauffragment 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 akzeptierenden 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)))

instance (Ord state, Ord input, Ord output, Show state, Show input, Show output, Finite state) => Action (DFSTAction state input output) input output where
  type ActionParam (DFSTAction state input output) = DFST state input output
  type ActionState (DFSTAction state input output) = state

  actionFail = DFSTAction (\_ -> (Seq.empty, Nothing)) Seq.empty

  actionSingleInput = dfstAction

  actionGroundState = stInitial
  actionStateFinal DFST{..} final = final `Set.member` stAccept
  actionState _ act st = view _2 $ runDFSTAction' act st
  actionProduces _ act st = dfstaProduces act st

  actionConsumes _ = dfstaConsumes'

  actionFindPath DFST{..} iState affNewOut fState suffix = do
    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 ()
  
    return .  Seq.fromList . mapMaybe (\(_st, (inS, _outS)) -> inS) $ reverse newPath
\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 = treeLens

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

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

\begin{eg}
  Wir wollen einen edit $e^\prime = \rho_{80}$ anwenden auf das Ergebnis $w^\prime$ der Ausführung des Zeilenumbruch-DFST aus Beispiel \ref{eg:linebreak} auf das Wort $w = 0\, 1\, \ldots\, 80\, \text{\tt \textbackslash n}\, 81\, \ldots\, 98$ aus Beispiel \ref{eg:w100} und dabei $e^\prime$ mittels $\Lleftarrow$ nach links propagieren und den assoziierten edit $e$ auf $w$ konstruieren.

  \begin{equation*}
    w^\prime = w = 0\, 1\, \ldots\, 80\, \text{\textbackslash n}\, 81\, \ldots\, 98
  \end{equation*}

  Das von $e$ betroffene Intervall von $w^\prime$ ist $(80, 80)$.

  Das Komplement nach Anwendung des DFST auf $w$ ist, wie in Beispiel \ref{eg:linebreakonw100} dargelegt:

  \begin{align*}
    \text{act} & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\
    0 & \mapsto (0\, 1\, \ldots\, 80\, \text{\tt \textbackslash n}\, 81\, \ldots\, 98, 19) \\
    1 & \mapsto (0\, 1\, \ldots\, 79\, \text{\tt \textbackslash n}\, 80\, \ldots\, 98, 18) \\
  & \vdots
  \end{align*}

  Wir unterteilen $\text{act}$ an $(80, 80)$ in $\text{act}_\text{R} \circ \text{act}_e \circ \text{act}_\text{L}$:

  \begin{align*}
    \text{act}_\text{R} & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\
    n & \mapsto (81\, \ldots\, 98, \min ( 80, n + 19 ) ) \\
    & \\
    \text{act}_e & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\
    n & \mapsto ( \text{\tt \textbackslash n}, 0 ) \\
    & \\
    \text{act}_\text{L} & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\
    \text{other} & \mapsto (\epsilon, \bot)
  \end{align*}

  % TODO
\end{eg}