Introduce FSTs & Generalize input/output

`toFST` is currently invalid

1 files changed, 170 insertions, 0 deletions

diff --git a/edit-lens/src/Control/DFST/Lens.lhs b/edit-lens/src/Control/DFST/Lens.lhs
new file mode 100644
index 0000000..0976314
--- /dev/null
+++ b/edit-lens/src/Control/DFST/Lens.lhs
@@ -0,0 +1,170 @@
+\begin{code}
+{-# LANGUAGE ScopedTypeVariables
+           , TemplateHaskell
+#-}
+
+module Control.DFST.Lens
+  ( StringEdit(..)
+  , StringEdits(..)
+  , insert, delete
+  , DFSTAction(..), DFSTComplement
+  , dfstLens
+  , module Control.DFST
+  , module Control.Lens.Edit
+  ) where
+
+import Control.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)
+import Data.Foldable (toList)
+
+
+data StringEdit char = Insert { _sePos :: Natural, _seInsertion :: char }
+                     | Delete { _sePos :: Natural }
+  deriving (Eq, Ord, Show, Read)
+
+makeLenses ''StringEdit
+
+data StringEdits char = StringEdits (Seq (StringEdit char))
+                      | SEFail
+  deriving (Eq, Ord, Show, Read)
+
+makePrisms ''StringEdits
+
+stringEdits :: Traversal' (StringEdits char) (StringEdit char)
+stringEdits = _StringEdits . traverse
+
+insert :: Natural -> char -> StringEdits char
+insert n c = StringEdits .  Seq.singleton $ Insert n c
+  
+delete :: Natural -> StringEdits char
+delete n = StringEdits .  Seq.singleton $ Delete n
+
+instance Monoid (StringEdits 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
+
+instance Module (StringEdits char) where
+  type Domain (StringEdits 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 `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.
+  
+% Stelle im bisherigen Lauf isolieren, an der edit im output-string passieren soll, breitensuche auf pfaden, die sich von dieser stelle aus unterscheiden?
+% Gegeben einen Pfad und eine markierte Transition, finde Liste aller Pfade aufsteigend sortiert nach Unterschied zu gegebenem Pfad, mit Unterschieden "nahe" der markierten Transition zuerst — zudem jeweils edit auf dem Eingabestring
+% Einfacher ist Breitensuche ab `stInitial` und zunächst diff auf eingabe-strings.
+  
+\begin{code}
+
+data DFSTAction state input output = DFSTAction { runDFSTAction :: state -> (state, Seq output) }
+
+instance Monoid (DFSTAction state input output) where
+  mempty = DFSTAction $ \x -> (x, Seq.empty)
+  (DFSTAction f) `mappend` (DFSTAction g) = DFSTAction $ \s -> let ((f -> (s', out')), out) = g s in (s', out <> out')
+
+type DFSTComplement state input output = Compositions (DFSTAction state input output)
+
+dfstLens :: forall state input output. (Ord state, Ord input, Ord output) => DFST state input output -> EditLens (DFSTComplement state input output) (StringEdits input) (StringEdits output)
+dfstLens dfst@DFST{..} = EditLens ground propR propL
+  where
+    ground :: DFSTComplement state input output
+    ground = Comp.fromList []
+
+    propR :: (DFSTComplement state input output, StringEdits input) -> (DFSTComplement state input output, StringEdits output)
+    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) Seq.empty)
+        (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 sOutput sOutput' & stringEdits . sePos . from enum +~ Seq.length pOutput
+    propR (c, StringEdits Seq.Empty) = (c, mempty)
+        
+
+    propL :: (DFSTComplement state input output, StringEdits output) -> (DFSTComplement state input output, StringEdits input)
+    propL = undefined
+
+strDiff :: forall sym. Eq sym => Seq sym -> Seq sym -> StringEdits sym
+-- ^ @strDiff a b@ calculates a set of edits, which, when applied to @a@, produce @b@
+strDiff a b = snd . foldr toEdit (0, mempty) $ (getDiff `on` toList) a b
+  where
+    toEdit :: Diff sym -> (Natural, StringEdits sym) -> (Natural, StringEdits sym)
+    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}