summaryrefslogtreecommitdiff
path: root/edit-lens/src/Data/String/DFST/Lens.lhs
diff options
context:
space:
mode:
Diffstat (limited to 'edit-lens/src/Data/String/DFST/Lens.lhs')
-rw-r--r--edit-lens/src/Data/String/DFST/Lens.lhs165
1 files changed, 0 insertions, 165 deletions
diff --git a/edit-lens/src/Data/String/DFST/Lens.lhs b/edit-lens/src/Data/String/DFST/Lens.lhs
deleted file mode 100644
index bf06f53..0000000
--- a/edit-lens/src/Data/String/DFST/Lens.lhs
+++ /dev/null
@@ -1,165 +0,0 @@
1\begin{code}
2{-# LANGUAGE ScopedTypeVariables
3 , TemplateHaskell
4#-}
5
6module Data.String.DFST.Lens
7 ( StringEdit(..)
8 , StringEdits(..)
9 , insert, delete
10 , DFSTAction(..), DFSTComplement
11 , dfstLens
12 , module Data.String.DFST
13 , module Control.Lens.Edit
14 ) where
15
16import Data.String.DFST
17import Control.Lens.Edit
18import Control.Lens
19import Control.Lens.TH
20import Control.Edit
21
22import Numeric.Natural
23import Data.Sequence (Seq((:<|), (:|>)))
24import qualified Data.Sequence as Seq
25
26import Data.Compositions.Snoc (Compositions)
27import qualified Data.Compositions.Snoc as Comp
28
29import Data.Algorithm.Diff (Diff, getDiff)
30import qualified Data.Algorithm.Diff as Diff
31
32import Data.Monoid
33import Data.Function (on)
34
35
36data StringEdit = Insert { _sePos :: Natural, _seInsertion :: Char }
37 | Delete { _sePos :: Natural }
38 deriving (Eq, Ord, Show, Read)
39
40makeLenses ''StringEdit
41
42data StringEdits = StringEdits (Seq StringEdit)
43 | SEFail
44 deriving (Eq, Ord, Show, Read)
45
46makePrisms ''StringEdits
47
48stringEdits :: Traversal' StringEdits StringEdit
49stringEdits = _StringEdits . traverse
50
51insert :: Natural -> Char -> StringEdits
52insert n c = StringEdits . Seq.singleton $ Insert n c
53
54delete :: Natural -> StringEdits
55delete n = StringEdits . Seq.singleton $ Delete n
56
57instance Monoid StringEdits where
58 mempty = StringEdits Seq.empty
59 SEFail `mappend` _ = SEFail
60 _ `mappend` SEFail = SEFail
61 (StringEdits Seq.Empty) `mappend` x = x
62 x `mappend` (StringEdits Seq.Empty) = x
63 (StringEdits x@(bs :|> b)) `mappend` (StringEdits y@(a :<| as))
64 | (Insert n _) <- a
65 , (Delete n') <- b
66 , n == n'
67 = StringEdits bs `mappend` StringEdits as
68 | otherwise = StringEdits $ x `mappend` y
69
70instance Module StringEdits where
71 type Domain StringEdits = String
72 apply str SEFail = Nothing
73 apply str (StringEdits Seq.Empty) = Just str
74 apply str (StringEdits (es :|> Insert n c)) = (flip apply) (StringEdits es) =<< go str n c
75 where
76 go [] n c
77 | n == 0 = Just [c]
78 | otherwise = Nothing
79 go str@(x:xs) n c
80 | n == 0 = Just $ c : str
81 | otherwise = (x:) <$> go xs (pred n) c
82 apply str (StringEdits (es :|> Delete n)) = (flip apply) (StringEdits es) =<< go str n
83 where
84 go [] _ = Nothing
85 go (x:xs) n
86 | n == 0 = Just xs
87 | otherwise = (x:) <$> go xs (pred n)
88
89 init = ""
90 divInit = StringEdits . Seq.unfoldl go . (0,)
91 where
92 go (_, []) = Nothing
93 go (n, (c:cs)) = Just ((succ n, cs), Insert n c)
94
95\end{code}
96
97% TODO Make notation mathy
98
99Um 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:
100
101Gegeben 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.
102
103Wir 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.
104Diese Wirkungen bilden einen Monoiden analog zu Endomorphismen, wobei die Resultat-Strings concateniert werden.
105
106Die 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.
107Da 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.
108Die 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.
109Nun gilt es nur noch die Differenz (als `StringEdits`) des vorherigen Suffixes im output-String und des aus der gerade berechneten Wirkung Bestimmten zu bestimmen.
110
111
112% Für die Rückrichtung bietet es sich an eine Art primitive Invertierung des DFSTs zu berechnen.
113% Gegeben den aktuellen DFST $A$ möchten wir einen anderen $A^{-1}$ finden, sodass gilt:
114
115% \begin{itemize}
116% \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.
117% \item Wenn $A^{-1}$ einen String $s^{-1}$ akzeptiert so produziert die resultierende Ausgabe $s$ unter $A$ die Ausgabe $s^{-1}$.
118% \end{itemize}
119
120% 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.
121
122\begin{code}
123
124data DFSTAction state = DFSTAction { runDFSTAction :: state -> (state, String -> String) }
125
126instance Monoid (DFSTAction state) where
127 mempty = DFSTAction $ \x -> (x, id)
128 (DFSTAction f) `mappend` (DFSTAction g) = DFSTAction $ \s -> let ((f -> (s', out')), out) = g s in (s', out' . out)
129
130type DFSTComplement state = Compositions (DFSTAction state)
131
132dfstLens :: forall state. Ord state => DFST state -> EditLens (DFSTComplement state) StringEdits StringEdits
133dfstLens dfst@DFST{..} = EditLens ground propR propL
134 where
135 ground :: DFSTComplement state
136 ground = Comp.fromList []
137
138 propR :: (DFSTComplement state, StringEdits) -> (DFSTComplement state, StringEdits)
139 propR (c, SEFail) = (c, SEFail)
140 propR (c, StringEdits (es :|> e)) = (c', es' <> es'')
141 where
142 (cSuffix, cPrefix) = Comp.splitAt (Comp.length c - (e ^. sePos . from enum)) c
143 cSuffix'
144 | Delete _ <- e = Comp.take (pred $ Comp.length cSuffix) cSuffix -- TODO unsafe
145 | Insert _ nChar <- e = cSuffix <> Comp.singleton (DFSTAction $ \x -> runDFST' dfst x (pure nChar) id)
146 (pState, pOutput) = runDFSTAction (Comp.composed cPrefix) stInitial
147 (_, sOutput ) = runDFSTAction (Comp.composed cSuffix ) pState
148 (_, sOutput') = runDFSTAction (Comp.composed cSuffix') pState
149 (c', es') = propR (cSuffix' <> cPrefix, StringEdits es)
150 es'' = (strDiff `on` ($ "")) sOutput sOutput' & stringEdits . sePos . from enum +~ (length $ pOutput [])
151 propR (c, mempty) = (c, mempty)
152
153
154 propL :: (DFSTComplement state, StringEdits) -> (DFSTComplement state, StringEdits)
155 propL = undefined
156
157strDiff :: String -> String -> StringEdits
158-- ^ @strDiff a b@ calculates a set of edits, which, when applied to @a@, produce @b@
159strDiff a b = snd . foldr toEdit (0, mempty) $ getDiff a b
160 where
161 toEdit :: Diff Char -> (Natural, StringEdits) -> (Natural, StringEdits)
162 toEdit (Diff.Both _ _) (n, es) = (succ n, es)
163 toEdit (Diff.First _ ) (n, es) = (succ n, delete n <> es)
164 toEdit (Diff.Second c) (n, es) = (succ (succ n), insert n c <> es)
165\end{code}