diff options
Diffstat (limited to 'edit-lens/src/Data/String/DFST/Lens.lhs')
-rw-r--r-- | edit-lens/src/Data/String/DFST/Lens.lhs | 165 |
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 | |||
6 | module 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 | |||
16 | import Data.String.DFST | ||
17 | import Control.Lens.Edit | ||
18 | import Control.Lens | ||
19 | import Control.Lens.TH | ||
20 | import Control.Edit | ||
21 | |||
22 | import Numeric.Natural | ||
23 | import Data.Sequence (Seq((:<|), (:|>))) | ||
24 | import qualified Data.Sequence as Seq | ||
25 | |||
26 | import Data.Compositions.Snoc (Compositions) | ||
27 | import qualified Data.Compositions.Snoc as Comp | ||
28 | |||
29 | import Data.Algorithm.Diff (Diff, getDiff) | ||
30 | import qualified Data.Algorithm.Diff as Diff | ||
31 | |||
32 | import Data.Monoid | ||
33 | import Data.Function (on) | ||
34 | |||
35 | |||
36 | data StringEdit = Insert { _sePos :: Natural, _seInsertion :: Char } | ||
37 | | Delete { _sePos :: Natural } | ||
38 | deriving (Eq, Ord, Show, Read) | ||
39 | |||
40 | makeLenses ''StringEdit | ||
41 | |||
42 | data StringEdits = StringEdits (Seq StringEdit) | ||
43 | | SEFail | ||
44 | deriving (Eq, Ord, Show, Read) | ||
45 | |||
46 | makePrisms ''StringEdits | ||
47 | |||
48 | stringEdits :: Traversal' StringEdits StringEdit | ||
49 | stringEdits = _StringEdits . traverse | ||
50 | |||
51 | insert :: Natural -> Char -> StringEdits | ||
52 | insert n c = StringEdits . Seq.singleton $ Insert n c | ||
53 | |||
54 | delete :: Natural -> StringEdits | ||
55 | delete n = StringEdits . Seq.singleton $ Delete n | ||
56 | |||
57 | instance 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 | |||
70 | instance 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 | |||
99 | 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: | ||
100 | |||
101 | 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. | ||
102 | |||
103 | 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. | ||
104 | Diese Wirkungen bilden einen Monoiden analog zu Endomorphismen, wobei die Resultat-Strings concateniert werden. | ||
105 | |||
106 | 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. | ||
107 | 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. | ||
108 | 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. | ||
109 | 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. | ||
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 | |||
124 | data DFSTAction state = DFSTAction { runDFSTAction :: state -> (state, String -> String) } | ||
125 | |||
126 | instance 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 | |||
130 | type DFSTComplement state = Compositions (DFSTAction state) | ||
131 | |||
132 | dfstLens :: forall state. Ord state => DFST state -> EditLens (DFSTComplement state) StringEdits StringEdits | ||
133 | dfstLens 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 | |||
157 | strDiff :: String -> String -> StringEdits | ||
158 | -- ^ @strDiff a b@ calculates a set of edits, which, when applied to @a@, produce @b@ | ||
159 | strDiff 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} | ||