From d3f6fdc3ea71386c2b9a9cd5a686455dbee3e60e Mon Sep 17 00:00:00 2001
From: Gregor Kleen <gkleen@yggdrasil.li>
Date: Mon, 21 May 2018 16:14:26 +0200
Subject: Introduce FSTs & Generalize input/output

`toFST` is currently invalid
---
 edit-lens/package.yaml                  |   6 +-
 edit-lens/src/Control/DFST.lhs          |  78 +++++++++++++++
 edit-lens/src/Control/DFST/Lens.lhs     | 170 ++++++++++++++++++++++++++++++++
 edit-lens/src/Control/FST.lhs           |  24 +++++
 edit-lens/src/Data/String/DFST.hs       |  42 --------
 edit-lens/src/Data/String/DFST/Lens.lhs | 165 -------------------------------
 6 files changed, 277 insertions(+), 208 deletions(-)
 create mode 100644 edit-lens/src/Control/DFST.lhs
 create mode 100644 edit-lens/src/Control/DFST/Lens.lhs
 create mode 100644 edit-lens/src/Control/FST.lhs
 delete mode 100644 edit-lens/src/Data/String/DFST.hs
 delete mode 100644 edit-lens/src/Data/String/DFST/Lens.lhs

(limited to 'edit-lens')

diff --git a/edit-lens/package.yaml b/edit-lens/package.yaml
index 970d50a..2374898 100644
--- a/edit-lens/package.yaml
+++ b/edit-lens/package.yaml
@@ -20,6 +20,7 @@ library:
     - TypeApplications
     - GADTs
     - RecordWildCards
+    - NamedFieldPuns
     - PatternGuards
     - TupleSections
     - RankNTypes
@@ -31,9 +32,12 @@ library:
     - containers
     - composition-tree
     - Diff
+    - mtl
   exposed-modules:
     - Control.Edit
-    - Data.String.DFST
     - Control.Lens.Edit
+    - Control.DFST
+    - Control.FST
+    - Control.DFST.Lens
     
   
diff --git a/edit-lens/src/Control/DFST.lhs b/edit-lens/src/Control/DFST.lhs
new file mode 100644
index 0000000..aec7bbb
--- /dev/null
+++ b/edit-lens/src/Control/DFST.lhs
@@ -0,0 +1,78 @@
+\begin{code}
+{-# LANGUAGE ScopedTypeVariables
+#-}
+
+{-|
+Description: Deterministic finite state transducers
+-}
+module Control.DFST
+  ( DFST(..)
+  , runDFST, runDFST'
+  , toFST
+  ) where
+
+import Data.Map.Strict (Map, (!?))
+import qualified Data.Map.Strict as Map
+
+import Data.Set (Set)
+import qualified Data.Set as Set
+
+import Data.Sequence (Seq(..))
+import qualified Data.Sequence as Seq
+
+import Data.Monoid
+
+import Numeric.Natural
+
+import Control.Monad
+import Control.Monad.State
+
+import Control.FST (FST(FST))
+import qualified Control.FST as FST
+
+
+data DFST state input output = DFST
+  { stInitial :: state
+  , stTransition :: Map (state, input) (state, Seq output)
+    -- ^ All @(s, c)@-combinations not mapped are assumed to map to @(s, Nothing)@
+  , stAccept :: Set state
+  }
+
+
+toFST :: forall state input output. (Ord state, Ord input, Ord output) => DFST state input output -> FST (state, Natural) input output
+-- ^ Split apart non-singleton outputs into a series of epsilon-transitions
+--
+-- This function is currently invalid since multiple out-edges in the `DFST` visit the same intermediate states (we should label intermediate states not only with an ordinal but also with the input Symbol from the `DFST`)
+toFST DFST{..} = flip execState initialFST $ forM_ (Map.toList stTransition) handleTransition
+  where
+    initialFST = FST
+      { stInitial = (stInitial, 0)
+      , stTransition = Map.empty
+      , stAccept = Set.map (,0) stAccept
+      }
+    addTransition :: forall state input output. (Ord state, Ord input, Ord output) => (state, Maybe input) -> (state, Maybe output) -> State (FST state input output) ()
+    addTransition k v = modify $ \f@FST{ stTransition } -> f { FST.stTransition = Map.insertWith Set.union k (Set.singleton v) stTransition }
+    handleTransition :: ((state, input), (state, Seq output)) -> State (FST (state, Natural) input output) ()
+    handleTransition ((st, inS), (st', outs)) = handleTransition' (st, 0) (Just inS) outs (st', 0)
+    handleTransition' :: (state, Natural) -> Maybe input -> Seq output -> (state, Natural) -> State (FST (state, Natural) input output) ()
+    handleTransition' from inS Empty to = addTransition (from, inS) (to, Nothing)
+    handleTransition' from inS (outS :<| Empty) to = addTransition (from, inS) (to, Just outS)
+    handleTransition' from@(st, i) inS (outS :<| oo) to = addTransition (from, inS) ((st, succ i), Just outS) >> handleTransition' (st, succ i) Nothing oo to
+  
+runDFST :: forall state input output. (Ord state, Ord input) => DFST state input output -> Seq input -> Maybe (Seq output)
+runDFST dfst@DFST{..} str = let (finalState, str') = runDFST' dfst stInitial str Seq.empty
+                            in str' <$ guard (finalState `Set.member` stAccept)
+
+runDFST' :: forall state input output. (Ord state, Ord input)
+         => DFST state input output
+         -> state               -- ^ Current state
+         -> Seq input           -- ^ Remaining input
+         -> Seq output          -- ^ Accumulator containing previous output
+         -> (state, Seq output) -- ^ Next state, altered output
+runDFST' _             st  Empty     acc = (st, acc)
+runDFST' dfst@DFST{..} st (c :<| cs) acc
+  | Just (st', mc') <- stTransition !? (st, c)
+  = runDFST' dfst st' cs $ acc <> mc'
+  | otherwise
+  = runDFST' dfst st cs acc
+\end{code}
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}
diff --git a/edit-lens/src/Control/FST.lhs b/edit-lens/src/Control/FST.lhs
new file mode 100644
index 0000000..d3c8ca9
--- /dev/null
+++ b/edit-lens/src/Control/FST.lhs
@@ -0,0 +1,24 @@
+\begin{code}
+
+{-|
+Description: Finite state transducers with epsilon-transitions
+-}
+module Control.FST
+  ( FST(..)
+  ) where
+
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
+
+import Data.Set (Set)
+
+import Data.Sequence (Seq)
+
+import Control.Lens.TH
+
+data FST state input output = FST
+  { stInitial :: state
+  , stTransition :: Map (state, Maybe input) (Set (state, Maybe output))
+  , stAccept :: Set state
+  }
+\end{code}
diff --git a/edit-lens/src/Data/String/DFST.hs b/edit-lens/src/Data/String/DFST.hs
deleted file mode 100644
index 54a1336..0000000
--- a/edit-lens/src/Data/String/DFST.hs
+++ /dev/null
@@ -1,42 +0,0 @@
-{-# LANGUAGE ScopedTypeVariables
-#-}
-
-{-|
-Description: Deterministic finite state transducers
--}
-module Data.String.DFST
-  ( DFST(..)
-  , runDFST, runDFST'
-  ) where
-
-import Data.Map.Strict (Map, (!?))
-import qualified Data.Map.Strict as Map
-
-import Data.Set (Set)
-import qualified Data.Set as Set
-
-import Control.Monad
-
-data DFST state = DFST
-  { stInitial :: state
-  , stTransition :: Map (state, Char) (state, String)
-    -- ^ All @(s, c)@-combinations not mapped are assumed to map to @(s, Nothing)@
-  , stAccept :: Set state
-  }
-  
-runDFST :: forall state. Ord state => DFST state -> String -> Maybe String
-runDFST dfst@DFST{..} str = let (finalState, str') = runDFST' dfst stInitial str id
-                            in str' "" <$ guard (finalState `Set.member` stAccept)
-
-runDFST' :: forall state. Ord state
-         => DFST state
-         -> state -- ^ Current state
-         -> String -- ^ Remaining input
-         -> (String -> String) -- ^ Output as difference list
-         -> (state, (String -> String)) -- ^ Next state, altered output
-runDFST' _ st [] acc = (st, acc)
-runDFST' dfst@DFST{..} st (c:cs) acc
-  | Just (st', mc') <- stTransition !? (st, c)
-  = runDFST' dfst st' cs $ acc . (mc' ++)
-  | otherwise
-  = runDFST' dfst st cs acc
diff --git a/edit-lens/src/Data/String/DFST/Lens.lhs b/edit-lens/src/Data/String/DFST/Lens.lhs
deleted file mode 100644
index bf06f53..0000000
--- a/edit-lens/src/Data/String/DFST/Lens.lhs
+++ /dev/null
@@ -1,165 +0,0 @@
-\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}
-- 
cgit v1.2.3