1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
|
\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.FST hiding (stInitial, stTransition, stAccept)
import qualified Control.FST as FST (stInitial, stTransition, stAccept)
import Control.Lens.Edit
import Control.Lens
import Control.Lens.TH
import Control.Edit
import Control.Monad
import Numeric.Natural
import Numeric.Interval (Interval, (...))
import qualified Numeric.Interval as Int
import Data.Sequence (Seq((:<|), (:|>)))
import qualified Data.Sequence as Seq
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Map (Map)
import qualified Data.Map as Map
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.Bool (bool)
import Data.Maybe (fromMaybe)
import Data.Function (on)
import Data.Foldable (toList)
import Debug.Trace
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
affected :: forall char. StringEdits char -> Maybe (Interval Natural)
-- ^ For a given set of edits @es@ return the interval @i = a ... b@ such that for any given string @str@ 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@
--
-- TODO
affected SEFail = Nothing
affected (StringEdits es) = Just $ go es Map.empty
where
go :: Seq (StringEdit char) -> Map Natural Integer -> Interval Natural
go Seq.Empty _ = Int.empty
go (es :> e) offsets = traceShow offsets $ Int.hull (Int.singleton p') $ 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 ((\i -> i <$ guard (i /= 0)) . myOffset . fromMaybe 0) p offsets
myOffset :: Integer -> Integer
myOffset
| Insert _ _ <- e = pred
| Delete _ <- e = succ
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)
runDFSTAction' :: DFSTComplement state input output -> state -> (state, Seq output)
runDFSTAction' = runDFSTAction . Comp.composed
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 Seq.Empty) = (c, mempty)
propR (c, StringEdits (es :> e))
| fst (runDFSTAction' c' stInitial) `Set.member` stAccept = (c', es' <> es'')
| otherwise = (c', SEFail)
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
propL :: (DFSTComplement state input output, StringEdits output) -> (DFSTComplement state input output, StringEdits input)
propL (c, SEFail) = (c, SEFail)
propL (c, StringEdits Seq.Empty) = (c, mempty)
propL (c, es) = fromMaybe (c, SEFail) $ do
newOut <- prevOut `apply` es
let outFST = wordFST newOut `productFST` toFST dfst
return undefined
where
(_, prevOut) = runDFSTAction (Comp.composed c) stInitial
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}
|
