Further work

1 files changed, 137 insertions, 268 deletions

diff --git a/edit-lens/src/Control/DFST/Lens.lhs b/edit-lens/src/Control/DFST/Lens.lhs
index 1e5bbb1..8222db2 100644
--- a/edit-lens/src/Control/DFST/Lens.lhs
+++ b/edit-lens/src/Control/DFST/Lens.lhs
@@ -7,11 +7,9 @@
 #-}
 
 module Control.DFST.Lens
-  ( StringEdit(..), sePos, seInsertion
-  , StringEdits(..), _StringEdits, _SEFail, stringEdits
-  , insert, delete, replace
-  , DFSTAction(..), DFSTComplement
+  ( DFSTAction(..), DFSTComplement
   , dfstLens
+  , module Control.Edit.String
   , module Control.DFST
   , module Control.Lens.Edit
   ) where
@@ -20,9 +18,12 @@ 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
 
@@ -64,94 +65,8 @@ 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.
+\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.
 
@@ -175,13 +90,24 @@ instance Monoid (DFSTAction state input output) where
     }
 \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
-\end{code}
-\begin{comment}
-\begin{code}
 dfstAction dfst (Seq.singleton -> dfstaConsumes) = DFSTAction{..}
   where
     runDFSTAction :: state -> (Seq output, Maybe state)
@@ -193,11 +119,35 @@ dfstAction dfst (Seq.singleton -> dfstaConsumes) = DFSTAction{..}
 \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.
+\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 Automaten an den Pfaden innerhalb der Schaltbox annotieren.
+  
+  \begin{figure}[H]
+    \centering
+    \pinclude{presentation/comptree.tex}
+    \caption{Die Wirkung der Eingabe $spp$ auf den Automaten 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
@@ -208,6 +158,7 @@ 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 indem der input-String von allen gegebenen edits betroffen ist (\texttt{affected}) in einen unveränderten Prefix und einen womöglich betroffenen Suffix unterteilen.
 
@@ -229,6 +180,55 @@ Die input-edits können nun wiederum, unter Beachtung der Verschiebung der indic
 \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}
@@ -236,130 +236,12 @@ dfstLens :: forall state input output. (Ord state, Ord input, Ord output, Show s
 \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)
+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
+    -> ([(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 []
@@ -378,59 +260,46 @@ bfs outgoing predicate
       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.
+-- trace :: String -> a -> a
+-- {-# NOINLINE trace #-}
+-- trace str y = flip seq y . unsafePerformIO . withFile "lens.log" AppendMode $ \h ->
+--   hPutStrLn h str
 
-\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
-  
-  
+-- 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 \\
+    n & \mapsto (0\, 1\, \ldots\, 80, 80) \\
+    \text{other} & \mapsto (\epsilon, \bot)
+  \end{align*}
+\end{eg}