\begin{code}
{-# LANGUAGE ScopedTypeVariables
           , TemplateHaskell
#-}

module Data.String.DFST.Lens
  ( StringEdit(..)
  , StringEdits(..)
  , insert, delete
  , DFSTAction(..), DFSTComplement
  , dfstLens
  , module Data.String.DFST
  , module Control.Lens.Edit
  ) where

import Data.String.DFST
import Control.Lens.Edit
import Control.Lens
import Control.Lens.TH
import Control.Edit

import Numeric.Natural
import Data.Sequence (Seq((:<|), (:|>)))
import qualified Data.Sequence as Seq

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

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

import Data.Monoid
import Data.Function (on)


data StringEdit = Insert { _sePos :: Natural, _seInsertion :: Char }
                | Delete { _sePos :: Natural }
  deriving (Eq, Ord, Show, Read)

makeLenses ''StringEdit

data StringEdits = StringEdits (Seq StringEdit)
                 | SEFail
  deriving (Eq, Ord, Show, Read)

makePrisms ''StringEdits

stringEdits :: Traversal' StringEdits StringEdit
stringEdits = _StringEdits . traverse

insert :: Natural -> Char -> StringEdits
insert n c = StringEdits .  Seq.singleton $ Insert n c
  
delete :: Natural -> StringEdits
delete n = StringEdits .  Seq.singleton $ Delete n

instance Monoid StringEdits 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

instance Module StringEdits where
  type Domain StringEdits = String
  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 [] n c
        | n == 0 = Just [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 [] _ = Nothing
      go (x:xs) n
        | n == 0 = Just xs
        | otherwise = (x:) <$> go xs (pred n)

  init = ""
  divInit = StringEdits . Seq.unfoldl go . (0,)
    where
      go (_, []) = 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 `StringEdits -> StringEdits` mit akzeptabler Komplexität für einen bestimmten `DFST s` (entlang der \emph{Richtung} des DFSTs) zu konstruieren möchten wir folgendes Verfahren anwenden:

Gegeben eine Sequenz (`StringEdits`) von zu übersetzenden Änderungen genügt es die Übersetzung eines einzelnen `StringEdit`s in eine womöglich längere Sequenz von `StringEdits` anzugeben, alle `StringEdits` aus der Sequenz 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 `state -> (state, String)`, die den aktuellen Zustand vorm Parsen des Strings auf den Zustand danach und die (womöglich leere) Ausgabe schickt.
Diese Wirkungen bilden einen Monoiden analog zu Endomorphismen, wobei die Resultat-Strings concateniert werden.

Die Unterliegende Idee 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.
Da wir wissen welche Stelle im input-String von einem gegebenen edit betroffen ist können wir, anhand der Wirkung des Teilstücks bis zu jener Stelle, den output-String in einen durch den edit unveränderten Prefix und einen womöglich betroffenen Suffix unterteilen.
Die Wirkung ab der betroffenen Stelle im input-String können wir also 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 Bestimmten zu bestimmen.


% Für die Rückrichtung bietet es sich an eine Art primitive Invertierung des DFSTs zu berechnen.
% Gegeben den aktuellen DFST $A$ möchten wir einen anderen $A^{-1}$ finden, sodass gilt:

% \begin{itemize}
%   \item $A^{-1}$ akzeptiert einen String $s^{-1}$ (endet seinen Lauf in einem finalen Zustand) gdw. es einen String $s$ gibt, der unter $A$ die Ausgabe $s^{-1}$ produziert.
%   \item Wenn $A^{-1}$ einen String $s^{-1}$ akzeptiert so produziert die resultierende Ausgabe $s$ unter $A$ die Ausgabe $s^{-1}$.
% \end{itemize}

% Kann nicht funktionieren, denn $A^{-1}$ ist notwendigerweise nondeterministisch. Wird $A^{-1}$ dann zu einem DFST forciert (durch arbiträre Wahl einer Transition pro Zustand) gehen Informationen verloren—$A^{-1}$ produziert nicht den minimale edit auf dem input string (in der Tat beliebig schlecht) für einen gegeben edit auf dem output string.
  
\begin{code}

data DFSTAction state = DFSTAction { runDFSTAction :: state -> (state, String -> String) }

instance Monoid (DFSTAction state) where
  mempty = DFSTAction $ \x -> (x, id)
  (DFSTAction f) `mappend` (DFSTAction g) = DFSTAction $ \s -> let ((f -> (s', out')), out) = g s in (s', out' . out)

type DFSTComplement state = Compositions (DFSTAction state)

dfstLens :: forall state. Ord state => DFST state -> EditLens (DFSTComplement state) StringEdits StringEdits
dfstLens dfst@DFST{..} = EditLens ground propR propL
  where
    ground :: DFSTComplement state
    ground = Comp.fromList []

    propR :: (DFSTComplement state, StringEdits) -> (DFSTComplement state, StringEdits)
    propR (c, SEFail) = (c, SEFail)
    propR (c, StringEdits (es :|> e)) = (c', es' <> es'')
      where
        (cSuffix, cPrefix) = Comp.splitAt (Comp.length c - (e ^. sePos . from enum)) c
        cSuffix'
          | Delete _       <- e = Comp.take (pred $ Comp.length cSuffix) cSuffix -- TODO unsafe
          | Insert _ nChar <- e = cSuffix <> Comp.singleton (DFSTAction $ \x -> runDFST' dfst x (pure nChar) id)
        (pState, pOutput)  = runDFSTAction (Comp.composed cPrefix) stInitial
        (_, sOutput ) = runDFSTAction (Comp.composed cSuffix ) pState
        (_, sOutput') = runDFSTAction (Comp.composed cSuffix') pState
        (c', es') = propR (cSuffix' <> cPrefix, StringEdits es)
        es'' = (strDiff `on` ($ "")) sOutput sOutput' & stringEdits . sePos . from enum +~ (length $ pOutput [])
    propR (c, mempty) = (c, mempty)
        

    propL :: (DFSTComplement state, StringEdits) -> (DFSTComplement state, StringEdits)
    propL = undefined

strDiff :: String -> String -> StringEdits
-- ^ @strDiff a b@ calculates a set of edits, which, when applied to @a@, produce @b@
strDiff a b = snd . foldr toEdit (0, mempty) $ getDiff a b
  where
    toEdit :: Diff Char -> (Natural, StringEdits) -> (Natural, StringEdits)
    toEdit (Diff.Both _ _) (n, es) = (succ n, es)
    toEdit (Diff.First _ ) (n, es) = (succ n, delete n <> es)
    toEdit (Diff.Second c) (n, es) = (succ (succ n), insert n c <> es)
\end{code}