diff options
Diffstat (limited to 'edit-lens/src/Data/String/DFST')
| -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} | ||
