summaryrefslogtreecommitdiff
path: root/edit-lens/src/Control/DFST/Lens.lhs
diff options
context:
space:
mode:
authorGregor Kleen <gkleen@yggdrasil.li>2019-02-19 11:39:51 +0100
committerGregor Kleen <gkleen@yggdrasil.li>2019-02-19 11:39:51 +0100
commit8afbe1f7df24034dd16fdf2e89b0665b2318ae2a (patch)
tree095be830c34c4aa9682a7047f4b0e412178ab24b /edit-lens/src/Control/DFST/Lens.lhs
parent46ae60eaca841b554ba20c6a2b7a15b43c12b4df (diff)
downloadincremental-dfsts-8afbe1f7df24034dd16fdf2e89b0665b2318ae2a.tar
incremental-dfsts-8afbe1f7df24034dd16fdf2e89b0665b2318ae2a.tar.gz
incremental-dfsts-8afbe1f7df24034dd16fdf2e89b0665b2318ae2a.tar.bz2
incremental-dfsts-8afbe1f7df24034dd16fdf2e89b0665b2318ae2a.tar.xz
incremental-dfsts-8afbe1f7df24034dd16fdf2e89b0665b2318ae2a.zip
Stuff...
Diffstat (limited to 'edit-lens/src/Control/DFST/Lens.lhs')
-rw-r--r--edit-lens/src/Control/DFST/Lens.lhs345
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
37import Data.Map.Lazy (Map) 37import Data.Map.Lazy (Map)
38import qualified Data.Map.Lazy as Map 38import qualified Data.Map.Lazy as Map
39 39
40import qualified Data.Map as Strict (Map)
41import qualified Data.Map.Strict as Strict.Map
42
40import Data.Compositions (Compositions) 43import Data.Compositions (Compositions)
41import qualified Data.Compositions as Comp 44import qualified Data.Compositions as Comp
42 45
@@ -45,23 +48,26 @@ import qualified Data.Algorithm.Diff as Diff
45 48
46import Data.Monoid 49import Data.Monoid
47import Data.Bool (bool) 50import Data.Bool (bool)
48import Data.Maybe (fromMaybe, maybeToList, listToMaybe, catMaybes, isNothing, isJust) 51import Data.Maybe (fromMaybe, maybeToList, listToMaybe, catMaybes, isNothing, isJust, mapMaybe)
49import Data.Function (on) 52import Data.Function (on)
50import Data.Foldable (toList) 53import Data.Foldable (toList)
51import Data.List (partition) 54import Data.List (partition, isPrefixOf)
52 55
53import Control.Exception (assert) 56import Control.Exception (assert)
54 57
58import System.IO (Handle, hPutStrLn, IOMode(AppendMode), withFile)
55import System.IO.Unsafe 59import System.IO.Unsafe
56import Text.PrettyPrint.Leijen (Pretty(..)) 60import Text.PrettyPrint.Leijen (Pretty(..))
57 61
62import Data.Universe (Finite(..))
63
58\end{code} 64\end{code}
59\end{comment} 65\end{comment}
60 66
61 67
62Wir betrachten, zur Einfachheit, ein minimiales Set von Edits auf Strings\footnote{Wie in der Konstruktion zum Longest Common Subsequence Problem}:
63
64\begin{defn}[Atomare edits of strings] 68\begin{defn}[Atomare edits of strings]
69Wir 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:
70
65\begin{code} 71\begin{code}
66data StringEdit pos char = Insert { _sePos :: pos, _seInsertion :: char } 72data StringEdit pos char = Insert { _sePos :: pos, _seInsertion :: char }
67 | Delete { _sePos :: pos } 73 | Delete { _sePos :: pos }
@@ -73,7 +79,6 @@ data StringEdit pos char = Insert { _sePos :: pos, _seInsertion :: char }
73-- @seInsertion :: Traversal' (StringEdits pos char) char@ 79-- @seInsertion :: Traversal' (StringEdits pos char) char@
74makeLenses ''StringEdit 80makeLenses ''StringEdit
75\end{code} 81\end{code}
76\end{defn}
77 82
78Atomare edits werden, als Liste, zu edits komponiert. 83Atomare edits werden, als Liste, zu edits komponiert.
79Wir führen einen speziellen edit ein, der nicht-Anwendbarkeit der edits repräsentiert: 84Wir führen einen speziellen edit ein, der nicht-Anwendbarkeit der edits repräsentiert:
@@ -86,32 +91,19 @@ makePrisms ''StringEdits
86 91
87stringEdits :: Traversal (StringEdits pos char) (StringEdits pos' char') (StringEdit pos char) (StringEdit pos' char') 92stringEdits :: Traversal (StringEdits pos char) (StringEdits pos' char') (StringEdit pos char) (StringEdit pos' char')
88\end{code} 93\end{code}
94\end{defn}
95
89\begin{comment} 96\begin{comment}
90\begin{code} 97\begin{code}
91stringEdits = _StringEdits . traverse 98stringEdits = _StringEdits . traverse
92\end{code} 99
93\end{comment}
94\begin{code}
95insert :: pos -> char -> StringEdits pos char 100insert :: pos -> char -> StringEdits pos char
96\end{code}
97\begin{comment}
98\begin{code}
99insert n c = StringEdits . Seq.singleton $ Insert n c 101insert n c = StringEdits . Seq.singleton $ Insert n c
100\end{code} 102
101\end{comment}
102\begin{code}
103delete :: pos -> StringEdits pos char 103delete :: pos -> StringEdits pos char
104\end{code}
105\begin{comment}
106\begin{code}
107delete n = StringEdits . Seq.singleton $ Delete n 104delete n = StringEdits . Seq.singleton $ Delete n
108\end{code} 105
109\end{comment}
110\begin{code}
111replace :: Eq pos => pos -> char -> StringEdits pos char 106replace :: Eq pos => pos -> char -> StringEdits pos char
112\end{code}
113\begin{comment}
114\begin{code}
115replace n c = insert n c <> delete n 107replace n c = insert n c <> delete n
116 108
117-- | Rudimentarily optimize edit composition 109-- | Rudimentarily optimize edit composition
@@ -130,7 +122,7 @@ instance Eq pos => Monoid (StringEdits pos char) where
130\end{code} 122\end{code}
131\end{comment} 123\end{comment}
132 124
133Da wir ein minimales set an atomaren edits gewählt haben, ist die Definiton der Modulnstruktur über Strings des passenden Alphabets recht einfach: 125Da wir ein minimales Set an atomaren edits gewählt haben, ist die Definiton der Modulnstruktur über Strings des passenden Alphabets recht einfach:
134\begin{code} 126\begin{code}
135instance Module (StringEdits Natural char) where 127instance Module (StringEdits Natural char) where
136 type Domain (StringEdits Natural char) = Seq char 128 type Domain (StringEdits Natural char) = Seq char
@@ -159,12 +151,6 @@ instance Module (StringEdits Natural char) where
159 151
160\end{code} 152\end{code}
161 153
162% TODO Make notation mathy
163
164Um 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:
165
166Gegeben 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.
167
168Wir 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. 154Wir 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.
169Wir annotieren Wirkungen zudem mit dem konsumierten String. 155Wir annotieren Wirkungen zudem mit dem konsumierten String.
170Diese Wirkungen bilden einen Monoiden analog zu Endomorphismen, wobei die Resultat-Strings concateniert werden. 156Diese Wirkungen bilden einen Monoiden analog zu Endomorphismen, wobei die Resultat-Strings concateniert werden.
@@ -189,10 +175,30 @@ instance Monoid (DFSTAction state input output) where
189 } 175 }
190\end{code} 176\end{code}
191\end{comment} 177\end{comment}
178
192\begin{code} 179\begin{code}
180dfstAction :: forall state input output. (Finite state, Ord state, Ord input) => DFST state input output -> input -> DFSTAction state input output
181-- | Smart constructor of `DFSTAction` ensuring that `Seq.length . dfstaConsumes == const 1` and that `runDFSTAction` has constant complexity
182\end{code}
183\begin{comment}
184\begin{code}
185dfstAction dfst (Seq.singleton -> dfstaConsumes) = DFSTAction{..}
186 where
187 runDFSTAction :: state -> (Seq output, Maybe state)
188 runDFSTAction = (actionMap Strict.Map.!)
189
190 actionMap :: Strict.Map state (Seq output, Maybe state)
191 actionMap = Strict.Map.fromSet (\st -> runDFST' dfst st dfstaConsumes Seq.empty) $ Set.fromList universeF
192\end{code}
193\end{comment}
193 194
195Wir halten im Komplement der edit-lens einen Cache der monoidalen Summen aller kontinuirlichen Teillisten.
196\texttt{Compositions} ist ein balancierter Binärbaum, dessen innere Knoten mit der monoidalen Summe der Annotationen aller Blätter annotiert sind.
197\begin{code}
194type DFSTComplement state input output = Compositions (DFSTAction state input output) 198type DFSTComplement state input output = Compositions (DFSTAction state input output)
199\end{code}
195 200
201\begin{code}
196runDFSTAction' :: DFSTComplement state input output -> state -> (Seq output, Maybe state) 202runDFSTAction' :: DFSTComplement state input output -> state -> (Seq output, Maybe state)
197runDFSTAction' = runDFSTAction . Comp.composed 203runDFSTAction' = runDFSTAction . Comp.composed
198 204
@@ -203,28 +209,22 @@ dfstaProduces :: DFSTComplement state input output -> state -> Seq output
203dfstaProduces = fmap fst . runDFSTAction' 209dfstaProduces = fmap fst . runDFSTAction'
204\end{code} 210\end{code}
205 211
206Die 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. 212Fü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.
207
208Wir 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.
209 213
210Da 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. 214Da 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.
211Die 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. 215Die 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.
212Nun 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. 216Nun 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.
213 217
214Fü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: 218Fü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:
215
216Wir 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.
217 219
218Fü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. 220Wir 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).
219 221
220Wir 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. 222Wir 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.
221Abweichungen 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.
222Es wird zudem, wie für Breitensuche üblich, jeder besuchte Zustand markiert und ausgehende Transitionen nicht ein zweites mal betrachtet.
223 223
224Erreichen 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. 224Wir 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.
225Hierbei 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.
225 226
226In 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. 227Die 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.
227Wegen der verzögerten Auswertungsstrategie von Haskell wird auch tatsächlich nur der erste Rückgabe-Kandidat konstruiert.
228 228
229\begin{comment} 229\begin{comment}
230\begin{code} 230\begin{code}
@@ -232,7 +232,7 @@ type LState state input output = (Natural, (state, Maybe (input, Natural)))
232\end{code} 232\end{code}
233\end{comment} 233\end{comment}
234\begin{code} 234\begin{code}
235dfstLens :: 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) 235dfstLens :: 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)
236\end{code} 236\end{code}
237\begin{comment} 237\begin{comment}
238\begin{code} 238\begin{code}
@@ -244,166 +244,108 @@ dfstLens dfst@DFST{..} = EditLens ground propR propL
244 propR :: (DFSTComplement state input output, StringEdits Natural input) -> (DFSTComplement state input output, StringEdits Natural output) 244 propR :: (DFSTComplement state input output, StringEdits Natural input) -> (DFSTComplement state input output, StringEdits Natural output)
245 propR (c, SEFail) = (c, SEFail) 245 propR (c, SEFail) = (c, SEFail)
246 propR (c, StringEdits Seq.Empty) = (c, mempty) 246 propR (c, StringEdits Seq.Empty) = (c, mempty)
247 propR (c, es'@(StringEdits (es :> e))) 247 propR (c, lEs@(StringEdits (es :> e)))
248 | (_, Just final) <- runDFSTAction' c' stInitial 248 | (_, Just final) <- runDFSTAction' c' stInitial
249 , final `Set.member` stAccept 249 , final `Set.member` stAccept
250 = (c', rEs) 250 = (c', rEs)
251 | otherwise 251 | otherwise
252 = (c, SEFail) 252 = (c, SEFail)
253 where 253 where
254 Just int = affected es' 254 Just int = affected lEs
255 (cAffSuffix, cAffPrefix) = Comp.splitAt (Comp.length c - fromIntegral (Int.inf int)) c 255 (cAffSuffix, cAffPrefix) = Comp.splitAt (Comp.length c - fromIntegral (Int.inf int)) c
256 (cSuffix, cPrefix) = Comp.splitAt (Comp.length c - (e ^. sePos . from enum)) c 256 (cSuffix, cPrefix) = Comp.splitAt (Comp.length c - (e ^. sePos . from enum)) c
257 cSuffix' 257 cSuffix'
258 | Delete _ <- e 258 | Delete _ <- e
259 , Comp.length cSuffix > 0 = Comp.take (pred $ Comp.length cSuffix) cSuffix 259 , Comp.length cSuffix > 0 = Comp.take (pred $ Comp.length cSuffix) cSuffix
260 | Insert _ nChar <- e = cSuffix <> Comp.singleton (DFSTAction (\x -> runDFST' dfst x (pure nChar) Seq.empty) (Seq.singleton nChar)) 260 | Insert _ nChar <- e = cSuffix <> Comp.singleton (dfstAction dfst nChar)
261 | otherwise = Comp.singleton $ DFSTAction (\_ -> (Seq.empty, Nothing)) Seq.empty 261 | otherwise = Comp.singleton $ DFSTAction (\_ -> (Seq.empty, Nothing)) Seq.empty
262 (c', _) = propR (cSuffix' <> cPrefix, StringEdits es) 262 (c', _) = propR (cSuffix' <> cPrefix, StringEdits es)
263 (cAffSuffix', _) = Comp.splitAt (Comp.length c' - Comp.length cAffPrefix) c' 263 (cAffSuffix', _) = Comp.splitAt (Comp.length c' - Comp.length cAffPrefix) c'
264 (_, Just pFinal) = runDFSTAction' cPrefix stInitial 264 (_, Just pFinal) = runDFSTAction' cAffPrefix stInitial
265 rEs = strDiff (fst $ runDFSTAction' cAffSuffix pFinal) (fst $ runDFSTAction' cAffSuffix' pFinal) & stringEdits . sePos . from enum +~ length (dfstaProduces cAffPrefix stInitial) 265 rEs = strDiff (dfstaProduces cAffSuffix pFinal) (dfstaProduces cAffSuffix' pFinal) & stringEdits . sePos . from enum +~ length (dfstaProduces cAffPrefix stInitial)
266 266
267 267
268 propL :: (DFSTComplement state input output, StringEdits Natural output) -> (DFSTComplement state input output, StringEdits Natural input) 268 propL :: (DFSTComplement state input output, StringEdits Natural output) -> (DFSTComplement state input output, StringEdits Natural input)
269 propL (c, StringEdits Seq.Empty) = (c, mempty) 269 propL (c, StringEdits Seq.Empty) = (c, mempty)
270 propL (c, es) = fromMaybe (c, SEFail) $ do 270 propL (c, es) = fromMaybe (c, SEFail) $ do
271 let prevOut = dfstaProduces c stInitial 271 -- Determine states @(iState, fState)@ at the boundary of the region affected by @es@
272 newOut <- prevOut `apply` es 272 ((,) <$> Int.inf <*> Int.sup -> (minAff, maxAff)) <- affected es
273 affected' <- affected es 273 trace (show (minAff, maxAff)) $ Just ()
274 let
275 prevTrans :: Natural -> Maybe ( DFSTComplement state input output -- ^ Run after chosen transition to accepting state
276 , (state, input, Seq output, state)
277 , DFSTComplement state input output -- ^ Run from `stInitial` up to chosen transition
278 )
279 -- ^ Given an index in the output, find the associated transition in @c@
280 prevTrans needle = do
281 let (after, before) = prevTrans' (c, mempty)
282 transSt <- view _2 $ runDFSTAction (Comp.composed before) stInitial
283 trace ("transSt = " ++ show transSt) $ Just ()
284 let (after', trans) = Comp.splitAt (pred $ Comp.length after) after
285 DFSTAction{..} = Comp.composed trans
286 [inS] <- return $ toList dfstaConsumes
287 (outSs , Just postTransSt) <- return $ runDFSTAction transSt
288 return (after', (transSt, inS, outSs, postTransSt), before)
289 where
290 -- | Move monoid summands from @after@ to @before@ until first transition of @after@ produces @needle@ or @after@ is a singleton
291 prevTrans' (after, before)
292 | producedNext > needle = (after, before)
293 | Comp.length after == 1 = (after, before)
294 | otherwise = prevTrans' (after', before')
295 where
296 producedNext = fromIntegral . Seq.length . traceShowId $ dfstaProduces before' stInitial
297 (after', nextTrans) = Comp.splitAt (pred $ Comp.length after) after
298 before' = nextTrans `mappend` before
299 (_, (iState, _, _, _), prefix) <- prevTrans minAff
300 trace (show (iState, Comp.length prefix)) $ Just ()
301 (suffix, (pfState, _, _, fState), _) <- prevTrans maxAff
302 trace (show (pfState, fState, Comp.length suffix)) $ Just ()
303
304 newOut <- dfstaProduces c stInitial `apply` es
305 let affNewOut = (\s -> Seq.take (Seq.length s - Seq.length (dfstaProduces suffix fState)) s) $ Seq.drop (Seq.length $ dfstaProduces prefix stInitial) newOut
306 trace (show (iState, fState, affNewOut)) $ Just ()
307
274 let outFST :: FST (LState state input output) input output 308 let outFST :: FST (LState state input output) input output
275 -- outFST = wordFST newOut `productFST` toFST dfst 309 outFST = restrictOutput affNewOut $ toFST DFST
276 outFST = restrictOutput newOut $ toFST dfst 310 { stInitial = iState
277 311 , stTransition
278 trace x y = flip seq y . unsafePerformIO $ appendFile "lens.log" (x <> "\n\n") 312 , stAccept = Set.fromList $ do
279 313 fin <- Set.toList $ stAccept `Set.union` Set.map fst (Map.keysSet stTransition)
280 inflate by int 314 (suffOut, Just fin') <- return $ runDFSTAction' suffix fin
281 | Int.null int = Int.empty 315 guard $ Set.member fin' stAccept
282 | inf >= by = inf - by Int.... sup + by 316 guard $ suffOut == dfstaProduces suffix fState
283 | otherwise = 0 Int.... sup + by 317 return fin
284 where 318 }
285 (inf, sup) = (,) <$> Int.inf <*> Int.sup $ int 319 trace (show $ pretty outFST) $ Just ()
286 fragmentIntervals = (++ [all]) . takeWhile (not . Int.isSubsetOf (0 Int.... max)) $ inflate <$> 0 : [ 2^n | n <- [0..ceiling (logBase 2.0 max)] ] <*> pure affected' 320
287 where 321 newPath <-
288 max :: Num a => a 322 let
289 max = fromIntegral $ Seq.length newOut 323 FST{ .. } = outFST
290 all = 0 Int.... max 324 detOutgoing :: Maybe (LState state input output) -> [(LState state input output, (Maybe input, Maybe output))]
291 runCandidates :: Interval Natural -- ^ Departure from complement-run only permitted within interval (to guarantee locality) 325 detOutgoing Nothing = concatMap detOutgoing . map Just $ toList stInitial
292 -> [ ( Seq (LState state input output, Maybe output) -- ^ Computed run 326 detOutgoing (Just st) = concatMap (\((_, inS), outs) -> map (\(st', outS) -> (st', (inS, outS))) $ toList outs) . Map.toList $ Map.filterWithKey (\(st', _) _ -> st == st') stTransition
293 , StringEdits Natural input 327 predicate :: [(LState state input output, (Maybe input, Maybe output))] -> Maybe Bool
294 , DFSTComplement state input output 328 predicate []
295 ) 329 | not . Set.null $ Set.intersection stInitial stAccept = Just True
296 ] 330 | otherwise = Nothing
297 runCandidates focus = map ((,,) <$> view _1 <*> view _2 <*> view (_3 . _2)) $ go Set.empty [(Seq.empty, mempty, (c, mempty), 0)] 331 predicate ((lastSt, _) : _)
298 where 332 | Set.member lastSt stAccept = Just True
299 go _ [] = [] 333 | otherwise = Nothing
300 go visited (args@(run, edits, compZipper, inP) : alts) = 334 in bfs detOutgoing predicate
301 [ (run', finalizeEdits remC inP' edits', compZipper', inP') | (run', edits', compZipper'@(remC, _), inP') <- args : conts, isFinal run' ] 335
302 ++ go visited' (alts ++ conts) 336 trace (show newPath) $ Just ()
303 where 337
304 conts 338 let oldIn = dfstaConsumes' . Comp.drop (Comp.length suffix) $ Comp.take (Comp.length c - Comp.length prefix) c
305 | lastSt <- view _1 <$> Seq.lookup (pred $ Seq.length run) run 339 newIn = Seq.fromList . mapMaybe (\(_st, (inS, _outS)) -> inS) $ reverse newPath
306 , lastSt `Set.member` visited = [] 340 inDiff = oldIn `strDiff` newIn
307 | otherwise = continueRun edits compZipper inP run 341 diffOffset = fromIntegral . Seq.length $ dfstaConsumes' prefix
308 visited' = Set.insert (view _1 <$> Seq.lookup (pred $ Seq.length run) run) visited 342 inDiff' = inDiff & stringEdits . sePos +~ diffOffset
309 343
310 isFinal :: Seq (LState state input output, Maybe output) -> Bool 344 trace (show (oldIn, newIn, inDiff')) $ Just ()
311 -- ^ Is the final state of the run a final state of the DFST? 345
312 isFinal Seq.Empty = (0, (stInitial, Nothing)) `Set.member` FST.stAccept outFST 346 let affComp = Comp.fromList [ dfstAction dfst inS | (_st, (Just inS, _outS)) <- newPath ]
313 && (0 Int.... fromIntegral (Seq.length newOut)) `Int.isSubsetOf` focus 347
314 isFinal (_ :> (lastSt, _)) = lastSt `Set.member` FST.stAccept outFST 348 return (suffix <> affComp <> prefix, inDiff')
315
316 finalizeEdits :: DFSTComplement state input output -- ^ Remaining complement
317 -> Natural -- ^ Input position
318 -> StringEdits Natural input -> StringEdits Natural input
319 finalizeEdits remC inP = mappend . mconcat . replicate (Seq.length $ dfstaConsumes' remC) $ delete inP
320
321 continueRun :: StringEdits Natural input
322 -> (DFSTComplement state input output, DFSTComplement state input output) -- ^ Zipper into complement
323 -> Natural -- ^ Input position
324 -> Seq (LState state input output, Maybe output)
325 -> [ ( Seq (LState state input output, Maybe output)
326 , StringEdits Natural input
327 , (DFSTComplement state input output, DFSTComplement state input output)
328 , Natural
329 )
330 ]
331 -- ^ Nondeterministically make a single further step, continueing a given run
332 continueRun inEdits (c', remC) inP run = do
333 let
334 pos :: Natural
335 -- pos = fromIntegral $ Comp.length c - Comp.length c' -- FIXME: should use length of dfstaProduces
336 pos = fromIntegral . Seq.length $ dfstaProduces remC stInitial
337 (c'', step) = Comp.splitAt (pred $ Comp.length c') c' -- TODO: unsafe?
338 current :: LState state input output
339 current
340 | Seq.Empty <- run = (0, (stInitial, Nothing))
341 | (_ :> (st, _)) <- run = st
342 current' :: state
343 oldIn :: Maybe input
344 (current', oldIn)
345 | (_ :> ((_, (st, _)), _)) <- rest
346 , (_ :> ((_, (_, Just (partialIn, _))), _)) <- partial = (st, Just partialIn)
347 | (_ :> ((_, (_, Just (partialIn, _))), _)) <- partial = (stInitial, Just partialIn)
348 | Seq.Empty <- rest = (stInitial, Seq.lookup 0 $ dfstaConsumes' step)
349 | (_ :> ((_, (st, _)), _)) <- rest = (st, Seq.lookup 0 $ dfstaConsumes' step)
350 where
351 (partial, rest) = Seq.spanr (\((_, (_, inp)), _) -> isJust inp) run
352 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
353 let
354 outgoing :: LState state input output -> [(LState state input output, Maybe input, Maybe output)]
355 outgoing current = let go (st, minS) outs acc
356 | st == current = Set.foldr (\(st', moutS) -> ((st', minS, moutS) :)) acc outs
357 | otherwise = acc
358 in Map.foldrWithKey go [] $ FST.stTransition outFST
359 isPreferred :: (LState state input output, Maybe input, Maybe output) -> Bool
360 isPreferred ((_, (st, Nothing)), _, _) = st == next'
361 isPreferred (st@(_, (_, Just (inS , _))), _, _) = maybe True (== inS) oldIn && any isPreferred (outgoing st) -- By construction of `outFST`, `outgoing st` is a singleton in this case
362 (preferred, alternate) = partition isPreferred $ outgoing current
363 assocEdit :: (LState state input output, Maybe input, Maybe output) -- ^ Transition
364 -> [ ( (DFSTComplement state input output, DFSTComplement state input output) -- ^ new `(c', remC)`, i.e. complement-zipper `(c', remC)` but with edit applied
365 , StringEdits Natural input
366 , Natural
367 )
368 ]
369 assocEdit (_, Just inS, _)
370 | oldIn == Just inS = [ ((c'', step <> remC), mempty, succ inP) ]
371 | isJust oldIn = [ ((c', altStep inS <> remC), insert inP inS, succ inP)
372 , ((c'', altStep inS <> remC), replace inP inS, succ inP)
373 ]
374 | otherwise = [ ((c', altStep inS <> remC), insert inP inS, succ inP) ]
375 assocEdit (_, Nothing, _) = [((c', remC), mempty, inP)]
376 altStep :: input -> DFSTComplement state input output
377 altStep inS = Comp.singleton DFSTAction{..}
378 where
379 dfstaConsumes = Seq.singleton inS
380 runDFSTAction x = runDFST' dfst x (pure inS) Seq.empty
381 options
382 | pos `Int.member` focus = preferred ++ alternate
383 | otherwise = preferred
384 choice@(next, inS, outS) <- trace (unlines $ show (pretty outFST) : map show options) options
385 ((c3, remC'), inEdits', inP') <- assocEdit choice
386 -- let
387 -- -- | Replace prefix of old complement to reflect current candidate
388 -- -- TODO: smarter?
389 -- (_, ((c3 <>) -> newComplement')) = Comp.splitAt (Comp.length c') c -- TODO: unsafe?
390 -- acc = (run :> (next, outS), inEdits' <> inEdits, newComplement')
391 -- dropSuffix = mconcat (replicate (Seq.length $ dfstaConsumes' c3) $ delete inP')
392 -- fin
393 -- | (trans, inEs, newComplement) <- acc = (trans, dropSuffix <> inEs, newComplement)
394 let
395 trans = run :> (next, outS)
396 inEs = inEdits' <> inEdits
397 -- dropSuffix = mconcat (replicate (Seq.length $ dfstaConsumes' c3) $ delete inP')
398 -- fin
399 -- | (trans, inEs) <- acc = (trans, dropSuffix <> inEs, remC')
400 -- bool id (over _BFS $ cons fin) (next `Set.member` FST.stAccept outFST) $ continueRun acc (c3, remC') inP'
401 return (trans, inEs, (c3, remC'), inP')
402
403 -- Properties of the edits computed are determined mostly by the order candidates are generated below
404 -- (_, inEs, c') <- (\xs -> foldr (\x f -> x `seq` f) listToMaybe xs $ xs) $ traceShowId fragmentIntervals >>= (\x -> (\y@(y1, y2, _) -> traceShow (y1, y2) y) <$> runCandidates x)
405
406 fmap ((,) <$> view _3 <*> view _2) . listToMaybe $ runCandidates =<< fragmentIntervals
407 349
408strDiff :: forall sym pos. (Eq sym, Integral pos) => Seq sym -> Seq sym -> StringEdits pos sym 350strDiff :: forall sym pos. (Eq sym, Integral pos) => Seq sym -> Seq sym -> StringEdits pos sym
409-- ^ @strDiff a b@ calculates a set of edits, which, when applied to @a@, produce @b@ 351-- ^ @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
413 toEdit (n, es) (Diff.Both _ _) = (succ n, es) 355 toEdit (n, es) (Diff.Both _ _) = (succ n, es)
414 toEdit (n, es) (Diff.First _ ) = (n, delete n <> es) 356 toEdit (n, es) (Diff.First _ ) = (n, delete n <> es)
415 toEdit (n, es) (Diff.Second c) = (succ n, insert n c <> es) 357 toEdit (n, es) (Diff.Second c) = (succ n, insert n c <> es)
358
359-- | Generic breadth-first search
360bfs :: forall state transition. Ord state
361 => (Maybe state -> [(state, transition)]) -- ^ Find outgoing edges
362 -> ([(state, transition)] {- ^ Reverse path -} -> Maybe Bool {- ^ Continue search, finish successfully, or abort search on this branch -}) -- ^ Search predicate
363 -> Maybe [(state, transition)] -- ^ Reverse path
364bfs outgoing predicate
365 | Just True <- emptyRes = Just []
366 | Just False <- emptyRes = Nothing
367 | otherwise = bfs' Set.empty . Seq.fromList . map pure $ outgoing Nothing
368 where
369 emptyRes = predicate []
370
371 bfs' :: Set state -- ^ Visited states, not to be checked again
372 -> Seq [(state, transition)] -- ^ Search queue of paths to continue
373 -> Maybe [(state, transition)]
374 bfs' _ Seq.Empty = Nothing
375 bfs' visited (c@((lastSt, _) : _) :< cs) = case predicate c of
376 Just True -> Just c
377 Just False -> bfs' visited cs
378 Nothing -> bfs' visited' $ cs <> Seq.fromList (map (: c) . filter (\(st, _) -> not $ Set.member st visited) . outgoing $ Just lastSt)
379 where
380 visited' = Set.insert lastSt visited
416\end{code} 381\end{code}
417\end{comment} 382\end{comment}
418 383
@@ -457,5 +422,15 @@ affected (StringEdits es) = Just . toInterval $ go es Map.empty
457 myOffset 422 myOffset
458 | Insert _ _ <- e = pred 423 | Insert _ _ <- e = pred
459 | Delete _ <- e = succ 424 | Delete _ <- e = succ
425
426trace :: String -> a -> a
427{-# NOINLINE trace #-}
428trace str y = flip seq y . unsafePerformIO . withFile "lens.log" AppendMode $ \h ->
429 hPutStrLn h str
430
431traceShowId :: Show a => a -> a
432traceShowId x = trace (show x) x
433
434
460\end{code} 435\end{code}
461\end{comment} 436\end{comment}