diff options
Diffstat (limited to 'edit-lens/src/Data/String')
| -rw-r--r-- | edit-lens/src/Data/String/DFST/Lens.lhs | 78 |
1 files changed, 65 insertions, 13 deletions
diff --git a/edit-lens/src/Data/String/DFST/Lens.lhs b/edit-lens/src/Data/String/DFST/Lens.lhs index 2111ca4..9def01b 100644 --- a/edit-lens/src/Data/String/DFST/Lens.lhs +++ b/edit-lens/src/Data/String/DFST/Lens.lhs | |||
| @@ -1,6 +1,15 @@ | |||
| 1 | \begin{code} | 1 | \begin{code} |
| 2 | {-# LANGUAGE ScopedTypeVariables | ||
| 3 | #-} | ||
| 4 | |||
| 2 | module Data.String.DFST.Lens | 5 | module Data.String.DFST.Lens |
| 3 | ( | 6 | ( StringEdit(..) |
| 7 | , StringEdits(..) | ||
| 8 | , insert, delete | ||
| 9 | , DFSTAction(..), DFSTComplement | ||
| 10 | , dfstLens | ||
| 11 | , module Data.String.DFST | ||
| 12 | , module Control.Lens.Edit | ||
| 4 | ) where | 13 | ) where |
| 5 | 14 | ||
| 6 | import Data.String.DFST | 15 | import Data.String.DFST |
| @@ -11,10 +20,23 @@ import Numeric.Natural | |||
| 11 | import Data.Sequence (Seq((:<|), (:|>))) | 20 | import Data.Sequence (Seq((:<|), (:|>))) |
| 12 | import qualified Data.Sequence as Seq | 21 | import qualified Data.Sequence as Seq |
| 13 | 22 | ||
| 23 | import Data.Compositions.Snoc (Compositions) | ||
| 24 | import qualified Data.Compositions.Snoc as Comp | ||
| 25 | |||
| 26 | import Data.Algorithm.Diff (Diff, getDiff) | ||
| 27 | import qualified Data.Algorithm.Diff as Diff | ||
| 28 | |||
| 29 | import Data.Monoid | ||
| 30 | |||
| 31 | |||
| 14 | data StringEdit = Insert Natural Char | 32 | data StringEdit = Insert Natural Char |
| 15 | | Delete Natural | 33 | | Delete Natural |
| 16 | deriving (Eq, Ord, Show, Read) | 34 | deriving (Eq, Ord, Show, Read) |
| 17 | 35 | ||
| 36 | sePos :: StringEdit -> Natural | ||
| 37 | sePos (Insert pos _) = pos | ||
| 38 | sePos (Delete pos ) = pos | ||
| 39 | |||
| 18 | data StringEdits = StringEdits (Seq StringEdit) | 40 | data StringEdits = StringEdits (Seq StringEdit) |
| 19 | | SEFail | 41 | | SEFail |
| 20 | deriving (Eq, Ord, Show, Read) | 42 | deriving (Eq, Ord, Show, Read) |
| @@ -74,26 +96,56 @@ Gegeben eine Sequenz (`StringEdits`) von zu übersetzenden Änderungen genügt e | |||
| 74 | 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. | 96 | 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. |
| 75 | Diese Wirkungen bilden einen Monoiden analog zu Endomorphismen, wobei die Resultat-Strings concateniert werden. | 97 | Diese Wirkungen bilden einen Monoiden analog zu Endomorphismen, wobei die Resultat-Strings concateniert werden. |
| 76 | 98 | ||
| 77 | 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 möglich Präfixe und Suffixe zu halten. | 99 | 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. |
| 78 | 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. | 100 | 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. |
| 79 | 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. | 101 | 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. |
| 80 | 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. | 102 | 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. |
| 103 | |||
| 104 | % TODO propL | ||
| 81 | 105 | ||
| 82 | \begin{code} | 106 | \begin{code} |
| 83 | 107 | ||
| 84 | data DFSTAction state = DFSTBranch (Map state (state, String)) (DFSTAction state) (DFSTAction state) | 108 | data DFSTAction state = DFSTAction { runDFSTAction :: state -> (state, String -> String)} |
| 85 | 109 | ||
| 86 | % TODO propL, Transduktor invertieren? | 110 | instance Monoid (DFSTAction state) where |
| 87 | | DFSTLeaf | 111 | mempty = DFSTAction $ \x -> (x, id) |
| 112 | (DFSTAction f) `mappend` (DFSTAction g) = DFSTAction $ \s -> let ((f -> (s', out')), out) = g s in (s', out' . out) | ||
| 88 | 113 | ||
| 89 | dfstLens :: forall state. Ord state => DFST state -> EditLens (DFSTAction state) StringEdits StringEdits | 114 | type DFSTComplement state = Compositions (DFSTAction state) |
| 90 | dfstLens DFST{..} = EditLens ground propR propL | ||
| 91 | where | ||
| 92 | ground :: DFSTAction state | ||
| 93 | ground = DFSTLeaf | ||
| 94 | 115 | ||
| 95 | propR :: (DFSTAction state, StringEdits) -> (DFSTAction state, StringEdits) | 116 | dfstLens :: forall state. Ord state => DFST state -> EditLens (DFSTComplement state) StringEdits StringEdits |
| 96 | propR = undefined | 117 | dfstLens dfst@DFST{..} = EditLens ground propR propL |
| 97 | propL :: (DFSTAction state, StringEdits) -> (DFSTAction state, StringEdits) | 118 | where |
| 119 | ground :: DFSTComplement state | ||
| 120 | ground = Comp.fromList [] | ||
| 121 | |||
| 122 | propR :: (DFSTComplement state, StringEdits) -> (DFSTComplement state, StringEdits) | ||
| 123 | propR (c, SEFail) = (c, SEFail) | ||
| 124 | propR (c, StringEdits (es :|> e)) = (c', es' <> shiftBy (length $ pOutput []) (strDiff sOutput sOutput')) | ||
| 125 | where | ||
| 126 | (cSuffix, cPrefix) = Comp.splitAt (Comp.length c - (fromEnum $ sePos e)) c | ||
| 127 | cSuffix' | ||
| 128 | | Delete _ <- e = Comp.take (pred $ Comp.length cSuffix) cSuffix -- TODO unsafe | ||
| 129 | | Insert _ nChar <- e = cSuffix <> Comp.singleton (DFSTAction $ \x -> runDFST' dfst x (pure nChar) id) | ||
| 130 | (pState, pOutput) = runDFSTAction (Comp.composed cPrefix) stInitial | ||
| 131 | (_, sOutput ) = runDFSTAction (Comp.composed cSuffix ) pState | ||
| 132 | (_, sOutput') = runDFSTAction (Comp.composed cSuffix') pState | ||
| 133 | (c', es') = propR (cSuffix' <> cPrefix, StringEdits es) | ||
| 134 | shiftBy (toEnum -> n) (StringEdits es) = StringEdits $ shiftBy' n <$> es | ||
| 135 | shiftBy' n' (Insert n c) = Insert (n + n') c | ||
| 136 | shiftBy' n' (Delete n) = Delete (n + n') | ||
| 137 | propR (c, mempty) = (c, mempty) | ||
| 138 | |||
| 139 | |||
| 140 | propL :: (DFSTComplement state, StringEdits) -> (DFSTComplement state, StringEdits) | ||
| 98 | propL = undefined | 141 | propL = undefined |
| 142 | |||
| 143 | strDiff :: (String -> String) -> (String -> String) -> StringEdits | ||
| 144 | -- ^ @strDiff a b@ calculates a set of edits, which, when applied to @a@, produce @b@, where both @a@ and @b@ are given as diff-lists of chars | ||
| 145 | strDiff a b = snd . foldr toEdit (0, mempty) $ getDiff (a []) (b []) | ||
| 146 | where | ||
| 147 | toEdit :: Diff Char -> (Natural, StringEdits) -> (Natural, StringEdits) | ||
| 148 | toEdit (Diff.Both _ _) (n, es) = (succ n, es) | ||
| 149 | toEdit (Diff.First _ ) (n, es) = (succ n, delete n <> es) | ||
| 150 | toEdit (Diff.Second c) (n, es) = (succ (succ n), insert n c <> es) | ||
| 99 | \end{code} | 151 | \end{code} |
