diff options
author | Gregor Kleen <gkleen@yggdrasil.li> | 2018-05-07 16:50:09 +0200 |
---|---|---|
committer | Gregor Kleen <gkleen@yggdrasil.li> | 2018-05-07 16:50:09 +0200 |
commit | a5689e0dc96262a4df06b6363855d597ad377841 (patch) | |
tree | 754e82ecb4133eac783d28658340c2cbff011b53 | |
parent | 27c83d26737ee597e03cd3787319b76b804d52eb (diff) | |
download | incremental-dfsts-a5689e0dc96262a4df06b6363855d597ad377841.tar incremental-dfsts-a5689e0dc96262a4df06b6363855d597ad377841.tar.gz incremental-dfsts-a5689e0dc96262a4df06b6363855d597ad377841.tar.bz2 incremental-dfsts-a5689e0dc96262a4df06b6363855d597ad377841.tar.xz incremental-dfsts-a5689e0dc96262a4df06b6363855d597ad377841.zip |
DFST lenses now pass some rudimentary tests
-rw-r--r-- | edit-lens/package.yaml | 4 | ||||
-rw-r--r-- | edit-lens/src/Data/String/DFST/Lens.lhs | 78 | ||||
-rw-r--r-- | stack.yaml | 4 |
3 files changed, 73 insertions, 13 deletions
diff --git a/edit-lens/package.yaml b/edit-lens/package.yaml index 0030420..970d50a 100644 --- a/edit-lens/package.yaml +++ b/edit-lens/package.yaml | |||
@@ -22,11 +22,15 @@ library: | |||
22 | - RecordWildCards | 22 | - RecordWildCards |
23 | - PatternGuards | 23 | - PatternGuards |
24 | - TupleSections | 24 | - TupleSections |
25 | - RankNTypes | ||
26 | - ViewPatterns | ||
25 | source-dirs: src | 27 | source-dirs: src |
26 | dependencies: | 28 | dependencies: |
27 | - base | 29 | - base |
28 | - lens | 30 | - lens |
29 | - containers | 31 | - containers |
32 | - composition-tree | ||
33 | - Diff | ||
30 | exposed-modules: | 34 | exposed-modules: |
31 | - Control.Edit | 35 | - Control.Edit |
32 | - Data.String.DFST | 36 | - Data.String.DFST |
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} |
@@ -1,6 +1,10 @@ | |||
1 | resolver: lts-11.7 | 1 | resolver: lts-11.7 |
2 | packages: | 2 | packages: |
3 | - edit-lens | 3 | - edit-lens |
4 | - location: | ||
5 | git: https://github.com/pngwjpgh/composition-tree | ||
6 | commit: c9c1c11f6820bbbe1ac96513a66609599483bdb6 | ||
7 | extra-dep: true | ||
4 | nix: | 8 | nix: |
5 | packages: [] | 9 | packages: [] |
6 | pure: false | 10 | pure: false |