summaryrefslogtreecommitdiff
path: root/edit-lens/src/Data
diff options
context:
space:
mode:
authorGregor Kleen <gkleen@yggdrasil.li>2018-05-07 16:50:09 +0200
committerGregor Kleen <gkleen@yggdrasil.li>2018-05-07 16:50:09 +0200
commita5689e0dc96262a4df06b6363855d597ad377841 (patch)
tree754e82ecb4133eac783d28658340c2cbff011b53 /edit-lens/src/Data
parent27c83d26737ee597e03cd3787319b76b804d52eb (diff)
downloadincremental-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
Diffstat (limited to 'edit-lens/src/Data')
-rw-r--r--edit-lens/src/Data/String/DFST/Lens.lhs78
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
2module Data.String.DFST.Lens 5module 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
6import Data.String.DFST 15import Data.String.DFST
@@ -11,10 +20,23 @@ import Numeric.Natural
11import Data.Sequence (Seq((:<|), (:|>))) 20import Data.Sequence (Seq((:<|), (:|>)))
12import qualified Data.Sequence as Seq 21import qualified Data.Sequence as Seq
13 22
23import Data.Compositions.Snoc (Compositions)
24import qualified Data.Compositions.Snoc as Comp
25
26import Data.Algorithm.Diff (Diff, getDiff)
27import qualified Data.Algorithm.Diff as Diff
28
29import Data.Monoid
30
31
14data StringEdit = Insert Natural Char 32data StringEdit = Insert Natural Char
15 | Delete Natural 33 | Delete Natural
16 deriving (Eq, Ord, Show, Read) 34 deriving (Eq, Ord, Show, Read)
17 35
36sePos :: StringEdit -> Natural
37sePos (Insert pos _) = pos
38sePos (Delete pos ) = pos
39
18data StringEdits = StringEdits (Seq StringEdit) 40data 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
74Wir 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. 96Wir 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.
75Diese Wirkungen bilden einen Monoiden analog zu Endomorphismen, wobei die Resultat-Strings concateniert werden. 97Diese Wirkungen bilden einen Monoiden analog zu Endomorphismen, wobei die Resultat-Strings concateniert werden.
76 98
77Die 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. 99Die 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.
78Da 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. 100Da 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.
79Die 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. 101Die 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.
80Nun gilt es nur noch die Differenz (als `StringEdits`) des vorherigen Suffixes im output-String und des aus der gerade berechneten Wirkung Bestimmten zu bestimmen. 102Nun 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
84data DFSTAction state = DFSTBranch (Map state (state, String)) (DFSTAction state) (DFSTAction state) 108data DFSTAction state = DFSTAction { runDFSTAction :: state -> (state, String -> String)}
85 109
86% TODO propL, Transduktor invertieren? 110instance 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
89dfstLens :: forall state. Ord state => DFST state -> EditLens (DFSTAction state) StringEdits StringEdits 114type DFSTComplement state = Compositions (DFSTAction state)
90dfstLens DFST{..} = EditLens ground propR propL
91 where
92 ground :: DFSTAction state
93 ground = DFSTLeaf
94 115
95 propR :: (DFSTAction state, StringEdits) -> (DFSTAction state, StringEdits) 116dfstLens :: forall state. Ord state => DFST state -> EditLens (DFSTComplement state) StringEdits StringEdits
96 propR = undefined 117dfstLens 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
143strDiff :: (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
145strDiff 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}