1 files changed, 160 insertions, 185 deletions

diff --git a/edit-lens/src/Control/DFST/Lens.lhs b/edit-lens/src/Control/DFST/Lens.lhs
index fe33bd6..1e5bbb1 100644
--- a/edit-lens/src/Control/DFST/Lens.lhs
+++ b/edit-lens/src/Control/DFST/Lens.lhs
@@ -37,6 +37,9 @@ 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
 
@@ -45,23 +48,26 @@ import qualified Data.Algorithm.Diff as Diff
 
 import Data.Monoid
 import Data.Bool (bool)
-import Data.Maybe (fromMaybe, maybeToList, listToMaybe, catMaybes, isNothing, isJust)
+import Data.Maybe (fromMaybe, maybeToList, listToMaybe, catMaybes, isNothing, isJust, mapMaybe)
 import Data.Function (on)
 import Data.Foldable (toList)
-import Data.List (partition)
+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}
 
 
-Wir betrachten, zur Einfachheit, ein minimiales Set von Edits auf Strings\footnote{Wie in der Konstruktion zum Longest Common Subsequence Problem}:
-
 \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 }
@@ -73,7 +79,6 @@ data StringEdit pos char = Insert { _sePos :: pos, _seInsertion :: char }
 -- @seInsertion :: Traversal' (StringEdits pos char) char@
 makeLenses ''StringEdit
 \end{code}
-\end{defn}
 
 Atomare edits werden, als Liste, zu edits komponiert.
 Wir führen einen speziellen edit ein, der nicht-Anwendbarkeit der edits repräsentiert:
@@ -86,32 +91,19 @@ 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
-\end{code}
-\end{comment}
-\begin{code}
+
 insert :: pos -> char -> StringEdits pos char
-\end{code}
-\begin{comment}
-\begin{code}
 insert n c = StringEdits .  Seq.singleton $ Insert n c
-\end{code}
-\end{comment}
-\begin{code}
+
 delete :: pos -> StringEdits pos char
-\end{code}
-\begin{comment}
-\begin{code}
 delete n = StringEdits .  Seq.singleton $ Delete n
-\end{code}
-\end{comment}
-\begin{code}
+
 replace :: Eq pos => pos -> char -> StringEdits pos char
-\end{code}
-\begin{comment}
-\begin{code}
 replace n c = insert n c <> delete n
 
 -- | Rudimentarily optimize edit composition
@@ -130,7 +122,7 @@ instance Eq pos => Monoid (StringEdits pos char) where
 \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:
+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
@@ -159,12 +151,6 @@ instance Module (StringEdits Natural char) where
 
 \end{code}
 
-% TODO Make notation mathy
-
-Um zunächst eine asymmetrische edit-lens \texttt{StringEdits -> StringEdits} mit akzeptabler Komplexität für einen bestimmten DFST (entlang der \emph{Richtung} des DFSTs) zu konstruieren möchten wir folgendes Verfahren anwenden:
-
-Gegeben eine Sequenz von zu übersetzenden Änderungen genügt es die Übersetzung eines einzelnen \texttt{StringEdit}s in eine womöglich längere Sequenz von \texttt{StringEdits} anzugeben, alle \texttt{StringEdits} aus der Sequenz derart 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 \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.
@@ -189,10 +175,30 @@ instance Monoid (DFSTAction state input output) where
     }
 \end{code}
 \end{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)
+    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 ein balancierter Binärbaum, dessen innere Knoten mit der monoidalen Summe der Annotationen aller Blätter annotiert sind.
+\begin{code}
 type DFSTComplement state input output = Compositions (DFSTAction state input output)
+\end{code}
 
+\begin{code}
 runDFSTAction' :: DFSTComplement state input output -> state -> (Seq output, Maybe state)
 runDFSTAction' = runDFSTAction . Comp.composed
 
@@ -203,28 +209,22 @@ dfstaProduces :: DFSTComplement state input output -> state -> Seq output
 dfstaProduces = fmap fst . runDFSTAction'
 \end{code}
 
-Die Unterliegende Idee von $\Rrightarrow$ 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.
-
-Wir können die alte DFST-Wirkung zunächst anhand des Intervalls indem der input-String von allen gegebenen edits betroffen ist in einen unveränderten Prefix und einen womöglich betroffenen Suffix unterteilen.
+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.
 
 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 eines iterative vergrößerten Intervalls:
-
-Wir bestimmen zunächst (`affected`) eine obere Schranke an das Intervall in dem der Ausgabe-String vom edit betroffen ist und generieren eine von dort quadratisch wachsende Serie von Intervallen.
+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:
 
-Für jedes Intervall ("lokalere" Änderungen werden präferiert) schränken wir zunächst den DFST (zur einfachereren Implementierung in seiner Darstellung als FST) vermöge \texttt{restrictOutput} derart ein, dass nur die gewünschte Ausgabe produziert werden kann.
+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 betrachten dann in jedem Schritt (beginnend mit dem initialen Zustand des DFST) alle ausgehenden Transitionen und ziehen hierbei jene vor, die im vorherigen Lauf (gespeichert im Komplement der edit-lens), ebenfalls genommen wurden.
-Abweichungen vom im Komplement gespeicherten Lauf lassen wir nur innerhalb des betrachteten Intervalls zu und wählen in diesem Fall einen Edit auf der Eingabe, der die gewählte Abweichung produziert.
-Es wird zudem, wie für Breitensuche üblich, jeder besuchte Zustand markiert und ausgehende Transitionen nicht ein zweites mal betrachtet.
+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 akzeptierten Zustand führt.
 
-Erreichen wir einen finalen Zustand (wegen der Einschränkung des DFSTs wurde dann auch genau die gewünschte Ausgabe produziert), so fügen wir an die gesammelten Eingabe-edits eine Serie von deletions an, die den noch nicht konsumierten suffix der Eingabe verwerfen und brechen die Suche unter Rückgabe der Eingabe-edits und des neuen Laufs ab.
+Wir verwenden dann gewöhnliche Breitensuche über die Zustände und Transitionen des soeben konstruierten FSTs um einen Lauf-Fragment 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 akzeptierten Zustand endet.
 
-In Haskell formulieren wir das vorzeitige Abbrechen der Suche indem wir eine vollständige Liste von Rückgabe-Kandidaten konstruieren und dann immer ihr erstes Element zurück geben.
-Wegen der verzögerten Auswertungsstrategie von Haskell wird auch tatsächlich nur der erste Rückgabe-Kandidat konstruiert.
+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}
@@ -232,7 +232,7 @@ type LState state input output = (Natural, (state, Maybe (input, Natural)))
 \end{code}
 \end{comment}
 \begin{code}
-dfstLens :: forall state input output. (Ord state, Ord input, Ord output, Show state, Show input, Show output) => DFST state input output -> EditLens (DFSTComplement state input output) (StringEdits Natural input) (StringEdits Natural output)
+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}
@@ -244,166 +244,108 @@ dfstLens dfst@DFST{..} = EditLens ground propR propL
     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, es'@(StringEdits (es :> e)))
+    propR (c, lEs@(StringEdits (es :> e)))
       | (_, Just final) <- runDFSTAction' c' stInitial
       , final `Set.member` stAccept
       = (c', rEs)
       | otherwise
       = (c, SEFail)
       where
-        Just int = affected es'
+        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 (\x -> runDFST' dfst x (pure nChar) Seq.empty) (Seq.singleton nChar))
+          | 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' cPrefix stInitial
-        rEs = strDiff (fst $ runDFSTAction' cAffSuffix pFinal) (fst $ runDFSTAction' cAffSuffix' pFinal) & stringEdits . sePos . from enum +~ length (dfstaProduces cAffPrefix stInitial)
-        
+        (_, 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
-      let prevOut = dfstaProduces c stInitial
-      newOut <- prevOut `apply` es
-      affected' <- affected es
+      -- 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 = wordFST newOut `productFST` toFST dfst
-          outFST = restrictOutput newOut $ toFST dfst
-      
-          trace x y = flip seq y . unsafePerformIO $ appendFile "lens.log" (x <> "\n\n")
-
-          inflate by int
-            | Int.null int = Int.empty
-            | inf >= by = inf - by Int.... sup + by
-            | otherwise = 0 Int.... sup + by
-            where
-              (inf, sup) = (,) <$> Int.inf <*> Int.sup $ int
-          fragmentIntervals = (++ [all]) . takeWhile (not . Int.isSubsetOf (0 Int.... max)) $ inflate <$> 0 : [ 2^n | n <- [0..ceiling (logBase 2.0 max)] ] <*> pure affected'
-            where
-              max :: Num a => a
-              max = fromIntegral $ Seq.length newOut
-              all = 0 Int.... max
-          runCandidates :: Interval Natural -- ^ Departure from complement-run only permitted within interval (to guarantee locality)
-                        -> [ ( Seq (LState state input output, Maybe output) -- ^ Computed run
-                             , StringEdits Natural input
-                             , DFSTComplement state input output
-                             )
-                           ]
-          runCandidates focus = map ((,,) <$> view _1 <*> view _2 <*> view (_3 . _2)) $ go Set.empty [(Seq.empty, mempty, (c, mempty), 0)]
-            where
-              go _ [] = []
-              go visited (args@(run, edits, compZipper, inP) : alts) = 
-                  [ (run', finalizeEdits remC inP' edits', compZipper', inP') | (run', edits', compZipper'@(remC, _), inP') <- args : conts, isFinal run' ]
-                  ++ go visited' (alts ++ conts)
-                where
-                  conts
-                    | lastSt <- view _1 <$> Seq.lookup (pred $ Seq.length run) run
-                    , lastSt `Set.member` visited = []
-                    | otherwise = continueRun edits compZipper inP run
-                  visited' = Set.insert (view _1 <$> Seq.lookup (pred $ Seq.length run) run) visited
-
-              isFinal :: Seq (LState state input output, Maybe output) -> Bool
-              -- ^ Is the final state of the run a final state of the DFST?
-              isFinal Seq.Empty = (0, (stInitial, Nothing)) `Set.member` FST.stAccept outFST
-                               && (0 Int.... fromIntegral (Seq.length newOut)) `Int.isSubsetOf` focus
-              isFinal (_ :> (lastSt, _)) = lastSt `Set.member` FST.stAccept outFST
-
-              finalizeEdits :: DFSTComplement state input output -- ^ Remaining complement
-                            -> Natural -- ^ Input position
-                            -> StringEdits Natural input -> StringEdits Natural input
-              finalizeEdits remC inP = mappend . mconcat . replicate (Seq.length $ dfstaConsumes' remC) $ delete inP
-              
-              continueRun :: StringEdits Natural input
-                          -> (DFSTComplement state input output, DFSTComplement state input output) -- ^ Zipper into complement
-                          -> Natural -- ^ Input position
-                          -> Seq (LState state input output, Maybe output)
-                          -> [ ( Seq (LState state input output, Maybe output)
-                               , StringEdits Natural input
-                               , (DFSTComplement state input output, DFSTComplement state input output)
-                               , Natural
-                               )
-                             ]
-              -- ^ Nondeterministically make a single further step, continueing a given run
-              continueRun inEdits (c', remC) inP run = do
-                let
-                  pos :: Natural
-                  -- pos = fromIntegral $ Comp.length c - Comp.length c' -- FIXME: should use length of dfstaProduces
-                  pos = fromIntegral . Seq.length $ dfstaProduces remC stInitial
-                  (c'', step) = Comp.splitAt (pred $ Comp.length c') c' -- TODO: unsafe?
-                  current :: LState state input output
-                  current
-                    | Seq.Empty <- run      = (0, (stInitial, Nothing))
-                    | (_ :> (st, _)) <- run = st
-                  current' :: state
-                  oldIn :: Maybe input
-                  (current', oldIn)
-                    | (_ :> ((_, (st, _)), _)) <- rest
-                    , (_ :> ((_, (_, Just (partialIn, _))), _)) <- partial = (st, Just partialIn)
-                    | (_ :> ((_, (_, Just (partialIn, _))), _)) <- partial = (stInitial, Just partialIn)
-                    | Seq.Empty <- rest = (stInitial, Seq.lookup 0 $ dfstaConsumes' step)
-                    | (_ :> ((_, (st, _)), _)) <- rest = (st, Seq.lookup 0 $ dfstaConsumes' step)
-                    where
-                      (partial, rest) = Seq.spanr (\((_, (_, inp)), _) -> isJust inp) run
-                next' <- trace (show ("next'", pos, focus, run, (current', oldIn), current, dfstaConsumes' step, runDFST' dfst current' (maybe Seq.empty Seq.singleton oldIn) Seq.empty)) . maybeToList . snd $ runDFST' dfst current' (maybe Seq.empty Seq.singleton oldIn) Seq.empty
-                let
-                  outgoing :: LState state input output -> [(LState state input output, Maybe input, Maybe output)]
-                  outgoing current = let go (st, minS) outs acc
-                                           | st == current = Set.foldr (\(st', moutS) -> ((st', minS, moutS) :)) acc outs
-                                           | otherwise     = acc
-                                      in Map.foldrWithKey go [] $ FST.stTransition outFST 
-                  isPreferred :: (LState state input output, Maybe input, Maybe output) -> Bool
-                  isPreferred ((_, (st, Nothing)), _, _) = st == next'
-                  isPreferred (st@(_, (_, Just (inS , _))), _, _) = maybe True (== inS) oldIn && any isPreferred (outgoing st) -- By construction of `outFST`, `outgoing st` is a singleton in this case
-                  (preferred, alternate) = partition isPreferred $ outgoing current
-                  assocEdit :: (LState state input output, Maybe input, Maybe output) -- ^ Transition
-                            -> [ ( (DFSTComplement state input output, DFSTComplement state input output) -- ^ new `(c', remC)`, i.e. complement-zipper `(c', remC)` but with edit applied
-                                 , StringEdits Natural input
-                                 , Natural
-                                 )
-                               ]
-                  assocEdit (_, Just inS, _)
-                    | oldIn == Just inS = [ ((c'', step <> remC), mempty, succ inP) ]
-                    | isJust oldIn      = [ ((c', altStep inS <> remC), insert inP inS, succ inP)
-                                          , ((c'', altStep inS <> remC), replace inP inS, succ inP)
-                                          ]
-                    | otherwise         = [ ((c', altStep inS <> remC), insert inP inS, succ inP) ]
-                  assocEdit (_, Nothing, _) = [((c', remC), mempty, inP)]
-                  altStep :: input -> DFSTComplement state input output
-                  altStep inS = Comp.singleton DFSTAction{..}
-                    where
-                      dfstaConsumes = Seq.singleton inS
-                      runDFSTAction x = runDFST' dfst x (pure inS) Seq.empty
-                  options
-                    | pos `Int.member` focus = preferred ++ alternate
-                    | otherwise              = preferred
-                choice@(next, inS, outS) <- trace (unlines $ show (pretty outFST) : map show options) options
-                ((c3, remC'), inEdits', inP') <- assocEdit choice
-                -- let
-                --   -- | Replace prefix of old complement to reflect current candidate
-                --   -- TODO: smarter?
-                --   (_, ((c3 <>) -> newComplement')) = Comp.splitAt (Comp.length c') c -- TODO: unsafe?
-                --   acc = (run :> (next, outS), inEdits' <> inEdits, newComplement')
-                --   dropSuffix = mconcat (replicate (Seq.length $ dfstaConsumes' c3) $ delete inP')
-                --   fin
-                --     | (trans, inEs, newComplement) <- acc = (trans, dropSuffix <> inEs, newComplement)
-                let
-                  trans = run :> (next, outS)
-                  inEs = inEdits' <> inEdits
-                --   dropSuffix = mconcat (replicate (Seq.length $ dfstaConsumes' c3) $ delete inP')
-                --   fin
-                --     | (trans, inEs) <- acc = (trans, dropSuffix <> inEs, remC')
-                -- bool id (over _BFS $ cons fin) (next `Set.member` FST.stAccept outFST) $ continueRun acc (c3, remC') inP'
-                return (trans, inEs, (c3, remC'), inP')
-              
-      -- Properties of the edits computed are determined mostly by the order candidates are generated below
-      -- (_, inEs, c') <- (\xs -> foldr (\x f -> x `seq` f) listToMaybe xs $ xs) $ traceShowId fragmentIntervals >>= (\x -> (\y@(y1, y2, _) -> traceShow (y1, y2) y) <$> runCandidates x)
-
-      fmap ((,) <$> view _3 <*> view _2) .  listToMaybe $ runCandidates =<< fragmentIntervals
+          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@
@@ -413,6 +355,29 @@ strDiff a b = snd . foldl toEdit (0, mempty) $ (getDiff `on` toList) a b
     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)
+
+-- | 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
 \end{code}
 \end{comment}
 
@@ -457,5 +422,15 @@ affected (StringEdits es) = Just . toInterval $ go es Map.empty
         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
+  
+  
 \end{code}
 \end{comment}