summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGregor Kleen <gkleen@yggdrasil.li>2019-05-30 12:18:08 +0200
committerGregor Kleen <gkleen@yggdrasil.li>2019-05-30 12:18:08 +0200
commitf4c419b9ddec15bad267a4463f0720d6e28042d2 (patch)
tree54a0259116476150247619c4410eae33f8669314
parent8afbe1f7df24034dd16fdf2e89b0665b2318ae2a (diff)
downloadincremental-dfsts-f4c419b9ddec15bad267a4463f0720d6e28042d2.tar
incremental-dfsts-f4c419b9ddec15bad267a4463f0720d6e28042d2.tar.gz
incremental-dfsts-f4c419b9ddec15bad267a4463f0720d6e28042d2.tar.bz2
incremental-dfsts-f4c419b9ddec15bad267a4463f0720d6e28042d2.tar.xz
incremental-dfsts-f4c419b9ddec15bad267a4463f0720d6e28042d2.zip
Further work
-rw-r--r--.gitignore1
-rw-r--r--edit-lens/package.yaml3
l---------edit-lens/src/Control/DFST.lhs.tex1
-rw-r--r--edit-lens/src/Control/DFST/Lens.lhs405
l---------edit-lens/src/Control/DFST/Lens.lhs.tex1
-rw-r--r--edit-lens/src/Control/Edit.lhs2
l---------edit-lens/src/Control/Edit.lhs.tex1
-rw-r--r--edit-lens/src/Control/Edit/String.lhs120
l---------edit-lens/src/Control/Edit/String.lhs.tex1
-rw-r--r--edit-lens/src/Control/Edit/String/Affected.lhs73
l---------edit-lens/src/Control/Edit/String/Affected.lhs.tex1
-rw-r--r--edit-lens/src/Control/FST.lhs22
l---------edit-lens/src/Control/FST.lhs.tex1
-rw-r--r--edit-lens/src/Control/Lens/Edit.lhs6
l---------edit-lens/src/Control/Lens/Edit.lhs.tex1
-rw-r--r--edit-lens/src/Control/Lens/Edit/ActionTree.lhs204
l---------edit-lens/src/Control/Lens/Edit/ActionTree.lhs.tex1
-rw-r--r--implementation.tex89
-rw-r--r--interactive-edit-lens/package.yaml1
-rw-r--r--interactive-edit-lens/src/Interact.hs142
-rw-r--r--interactive-edit-lens/src/Interact/Types.hs26
-rw-r--r--interactive-edit-lens/src/Main.hs17
-rw-r--r--intro.tex81
-rw-r--r--literature/automatentheorie.bibtex6
-rw-r--r--literature/composition-tree.bibtex7
-rw-r--r--presentation.deps3
-rw-r--r--presentation.meta.yml22
-rw-r--r--presentation.tex351
-rw-r--r--presentation/comptree.tex53
-rw-r--r--presentation/editconv.tex62
-rw-r--r--presentation/switchdfst.tex8
-rw-r--r--stack.yaml2
-rw-r--r--thesis.args1
-rw-r--r--thesis.deps3
-rw-r--r--thesis.meta.yml.gup19
-rwxr-xr-xthesis.pdf.gup4
-rw-r--r--thesis.tex46
37 files changed, 1445 insertions, 342 deletions
diff --git a/.gitignore b/.gitignore
index 8bf5f01..bf8d48a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -8,3 +8,4 @@ literature.pdf
8**.log 8**.log
9**.prof 9**.prof
10**.prof.* 10**.prof.*
11examples
diff --git a/edit-lens/package.yaml b/edit-lens/package.yaml
index 7455dcc..631e7ed 100644
--- a/edit-lens/package.yaml
+++ b/edit-lens/package.yaml
@@ -45,7 +45,10 @@ library:
45 source-dirs: src 45 source-dirs: src
46 exposed-modules: 46 exposed-modules:
47 - Control.Edit 47 - Control.Edit
48 - Control.Edit.String
49 - Control.Edit.String.Affected
48 - Control.Lens.Edit 50 - Control.Lens.Edit
51 - Control.Lens.Edit.ActionTree
49 - Control.DFST 52 - Control.DFST
50 - Control.FST 53 - Control.FST
51 - Control.DFST.Lens 54 - Control.DFST.Lens
diff --git a/edit-lens/src/Control/DFST.lhs.tex b/edit-lens/src/Control/DFST.lhs.tex
new file mode 120000
index 0000000..eb8c83e
--- /dev/null
+++ b/edit-lens/src/Control/DFST.lhs.tex
@@ -0,0 +1 @@
DFST.lhs \ No newline at end of file
diff --git a/edit-lens/src/Control/DFST/Lens.lhs b/edit-lens/src/Control/DFST/Lens.lhs
index 1e5bbb1..8222db2 100644
--- a/edit-lens/src/Control/DFST/Lens.lhs
+++ b/edit-lens/src/Control/DFST/Lens.lhs
@@ -7,11 +7,9 @@
7#-} 7#-}
8 8
9module Control.DFST.Lens 9module Control.DFST.Lens
10 ( StringEdit(..), sePos, seInsertion 10 ( DFSTAction(..), DFSTComplement
11 , StringEdits(..), _StringEdits, _SEFail, stringEdits
12 , insert, delete, replace
13 , DFSTAction(..), DFSTComplement
14 , dfstLens 11 , dfstLens
12 , module Control.Edit.String
15 , module Control.DFST 13 , module Control.DFST
16 , module Control.Lens.Edit 14 , module Control.Lens.Edit
17 ) where 15 ) where
@@ -20,9 +18,12 @@ import Control.DFST
20import Control.FST hiding (stInitial, stTransition, stAccept) 18import Control.FST hiding (stInitial, stTransition, stAccept)
21import qualified Control.FST as FST (stInitial, stTransition, stAccept, step) 19import qualified Control.FST as FST (stInitial, stTransition, stAccept, step)
22import Control.Lens.Edit 20import Control.Lens.Edit
21import Control.Lens.Edit.ActionTree
23import Control.Lens 22import Control.Lens
24import Control.Lens.TH 23import Control.Lens.TH
25import Control.Edit 24import Control.Edit
25import Control.Edit.String
26import Control.Edit.String.Affected
26 27
27import Control.Monad 28import Control.Monad
28 29
@@ -64,94 +65,8 @@ import Data.Universe (Finite(..))
64\end{code} 65\end{code}
65\end{comment} 66\end{comment}
66 67
67 68\begin{defn}[Ausgabe-Wirkung von DFSTs]
68\begin{defn}[Atomare edits of strings] 69Wir definieren zunächst die \emph{Ausgabe-Wirkung}\footnote{Wir schreiben im Folgenden auch nur \emph{Wirkung}} eines DFST auf einen festen String als eine Abbildung \texttt{state -> (Seq output, Maybe state)}, die den aktuellen Zustand vor dem Parsen des Strings auf den Zustand danach und die (womöglich leere) Ausgabe schickt.
69Wir betrachten, zur Einfachheit, ein minimiales Set von Edits auf Strings\footnote{Wie in der Konstruktion zum Longest Common Subsequence Problem}, bestehend nur aus Einfügung eines einzelnen Zeichens und löschen des Zeichens an einer einzelnen Position:
70
71\begin{code}
72data StringEdit pos char = Insert { _sePos :: pos, _seInsertion :: char }
73 | Delete { _sePos :: pos }
74 deriving (Eq, Ord, Show, Read)
75
76-- Automatically derive van-leerhoven-lenses:
77--
78-- @sePos :: Lens' (StringEdits pos char) pos@
79-- @seInsertion :: Traversal' (StringEdits pos char) char@
80makeLenses ''StringEdit
81\end{code}
82
83Atomare edits werden, als Liste, zu edits komponiert.
84Wir führen einen speziellen edit ein, der nicht-Anwendbarkeit der edits repräsentiert:
85\begin{code}
86data StringEdits pos char = StringEdits (Seq (StringEdit pos char))
87 | SEFail
88 deriving (Eq, Ord, Show, Read)
89
90makePrisms ''StringEdits
91
92stringEdits :: Traversal (StringEdits pos char) (StringEdits pos' char') (StringEdit pos char) (StringEdit pos' char')
93\end{code}
94\end{defn}
95
96\begin{comment}
97\begin{code}
98stringEdits = _StringEdits . traverse
99
100insert :: pos -> char -> StringEdits pos char
101insert n c = StringEdits . Seq.singleton $ Insert n c
102
103delete :: pos -> StringEdits pos char
104delete n = StringEdits . Seq.singleton $ Delete n
105
106replace :: Eq pos => pos -> char -> StringEdits pos char
107replace n c = insert n c <> delete n
108
109-- | Rudimentarily optimize edit composition
110instance Eq pos => Monoid (StringEdits pos char) where
111 mempty = StringEdits Seq.empty
112 SEFail `mappend` _ = SEFail
113 _ `mappend` SEFail = SEFail
114 (StringEdits Seq.Empty) `mappend` x = x
115 x `mappend` (StringEdits Seq.Empty) = x
116 (StringEdits x@(bs :|> b)) `mappend` (StringEdits y@(a :<| as))
117 | (Insert n _) <- a
118 , (Delete n') <- b
119 , n == n'
120 = StringEdits bs `mappend` StringEdits as
121 | otherwise = StringEdits $ x `mappend` y
122\end{code}
123\end{comment}
124
125Da wir ein minimales Set an atomaren edits gewählt haben, ist die Definiton der Modulnstruktur über Strings des passenden Alphabets recht einfach:
126\begin{code}
127instance Module (StringEdits Natural char) where
128 type Domain (StringEdits Natural char) = Seq char
129 apply str SEFail = Nothing
130 apply str (StringEdits Seq.Empty) = Just str
131 apply str (StringEdits (es :|> Insert n c)) = flip apply (StringEdits es) =<< go str n c
132 where
133 go Seq.Empty n c
134 | n == 0 = Just $ Seq.singleton c
135 | otherwise = Nothing
136 go str@(x :<| xs) n c
137 | n == 0 = Just $ c <| str
138 | otherwise = (x <|) <$> go xs (pred n) c
139 apply str (StringEdits (es :|> Delete n)) = flip apply (StringEdits es) =<< go str n
140 where
141 go Seq.Empty _ = Nothing
142 go (x :<| xs) n
143 | n == 0 = Just xs
144 | otherwise = (x <|) <$> go xs (pred n)
145
146 init = Seq.empty
147 divInit = StringEdits . Seq.unfoldl go . (0,)
148 where
149 go (_, Seq.Empty) = Nothing
150 go (n, c :<| cs ) = Just ((succ n, cs), Insert n c)
151
152\end{code}
153
154Wir definieren zunächst die \emph{Wirkung} eines DFST auf einen festen String als eine Abbildung \texttt{state -> (Seq output, Maybe state)}, die den aktuellen Zustand vor dem Parsen des Strings auf den Zustand danach und die (womöglich leere) Ausgabe schickt.
155Wir annotieren Wirkungen zudem mit dem konsumierten String. 70Wir annotieren Wirkungen zudem mit dem konsumierten String.
156Diese Wirkungen bilden einen Monoiden analog zu Endomorphismen, wobei die Resultat-Strings concateniert werden. 71Diese Wirkungen bilden einen Monoiden analog zu Endomorphismen, wobei die Resultat-Strings concateniert werden.
157 72
@@ -175,13 +90,24 @@ instance Monoid (DFSTAction state input output) where
175 } 90 }
176\end{code} 91\end{code}
177\end{comment} 92\end{comment}
93\end{defn}
178 94
95\begin{eg} \label{eg:linebreakonw100}
96 Die Wirkung des DFST aus Beispiel~\ref{eg:linebreak} auf das Wort $w$ aus Beispiel~\ref{eg:w100} ist:
97
98 \begin{align*}
99 \text{act} & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\
100 0 & \mapsto (0\, 1\, \ldots\, 80\, \text{\tt \textbackslash n}\, 81\, \ldots\, 98, 19) \\
101 1 & \mapsto (0\, 1\, \ldots\, 79\, \text{\tt \textbackslash n}\, 80\, \ldots\, 98, 18) \\
102 & \vdots
103 \end{align*}
104\end{eg}
105
106
107\begin{comment}
179\begin{code} 108\begin{code}
180dfstAction :: forall state input output. (Finite state, Ord state, Ord input) => DFST state input output -> input -> DFSTAction state input output 109dfstAction :: forall state input output. (Finite state, Ord state, Ord input) => DFST state input output -> input -> DFSTAction state input output
181-- | Smart constructor of `DFSTAction` ensuring that `Seq.length . dfstaConsumes == const 1` and that `runDFSTAction` has constant complexity 110-- | Smart constructor of `DFSTAction` ensuring that `Seq.length . dfstaConsumes == const 1` and that `runDFSTAction` has constant complexity
182\end{code}
183\begin{comment}
184\begin{code}
185dfstAction dfst (Seq.singleton -> dfstaConsumes) = DFSTAction{..} 111dfstAction dfst (Seq.singleton -> dfstaConsumes) = DFSTAction{..}
186 where 112 where
187 runDFSTAction :: state -> (Seq output, Maybe state) 113 runDFSTAction :: state -> (Seq output, Maybe state)
@@ -193,11 +119,35 @@ dfstAction dfst (Seq.singleton -> dfstaConsumes) = DFSTAction{..}
193\end{comment} 119\end{comment}
194 120
195Wir halten im Komplement der edit-lens einen Cache der monoidalen Summen aller kontinuirlichen Teillisten. 121Wir halten im Komplement der edit-lens einen Cache der monoidalen Summen aller kontinuirlichen Teillisten.
196\texttt{Compositions} ist ein balancierter Binärbaum, dessen innere Knoten mit der monoidalen Summe der Annotationen aller Blätter annotiert sind. 122\texttt{Compositions} ist hierbei ein balancierter Binärbaum, dessen innere Knoten mit der monoidalen Summe der Annotationen aller Blätter des jeweiligen Teilbaums annotiert sind.
197\begin{code} 123\begin{code}
198type DFSTComplement state input output = Compositions (DFSTAction state input output) 124type DFSTComplement state input output = Compositions (DFSTAction state input output)
199\end{code} 125\end{code}
200 126
127Wir bedienen uns hierbei einer bestehenden Programmbibliothek \cite{composition-tree} um das Balancieren bei Modifikation des Baums nicht implementieren zu müssen.
128
129\begin{eg}
130 Wir definieren zunächst einen weiteren, sehr einfachen, DFST:
131
132 \begin{figure}[H]
133 \centering
134 \pinclude{presentation/switchdfst.tex}
135 \caption{\label{fig:switchdfst} Ein einfacher DFST, der zwischen zwei Zustanden wechselt und Ausgabe abhängig vom aktuellen Zustand erzeugt}
136 \end{figure}
137
138 Auf $s$ wechselt der DFST seinen Zustand, auf $p$ produziert er, abhängig vom aktuellen Zustand, genau ein Zeichen.
139
140 Wir stellen die Wirkung des DFST auf den Eingabe-String $spp$ grafisch analog zur Baumstruktur von \texttt{Compositions} dar.
141 Wir bedienen uns hier der Darstellung von Automaten-Wirkungen als \emph{Schaltboxen} aus \cite{hofmann2011automatentheorie}, angepasst für DFSTs indem wir die Ausgabe des Automaten an den Pfaden innerhalb der Schaltbox annotieren.
142
143 \begin{figure}[H]
144 \centering
145 \pinclude{presentation/comptree.tex}
146 \caption{Die Wirkung der Eingabe $spp$ auf den Automaten aus Abbildung \ref{fig:switchdfst}}
147 \end{figure}
148\end{eg}
149
150\begin{comment}
201\begin{code} 151\begin{code}
202runDFSTAction' :: DFSTComplement state input output -> state -> (Seq output, Maybe state) 152runDFSTAction' :: DFSTComplement state input output -> state -> (Seq output, Maybe state)
203runDFSTAction' = runDFSTAction . Comp.composed 153runDFSTAction' = runDFSTAction . Comp.composed
@@ -208,6 +158,7 @@ dfstaConsumes' = dfstaConsumes . Comp.composed
208dfstaProduces :: DFSTComplement state input output -> state -> Seq output 158dfstaProduces :: DFSTComplement state input output -> state -> Seq output
209dfstaProduces = fmap fst . runDFSTAction' 159dfstaProduces = fmap fst . runDFSTAction'
210\end{code} 160\end{code}
161\end{comment}
211 162
212Für $\Rrightarrow$ können wir die alte DFST-Wirkung zunächst anhand des Intervalls indem der input-String von allen gegebenen edits betroffen ist (\texttt{affected}) in einen unveränderten Prefix und einen womöglich betroffenen Suffix unterteilen. 163Für $\Rrightarrow$ können wir die alte DFST-Wirkung zunächst anhand des Intervalls indem der input-String von allen gegebenen edits betroffen ist (\texttt{affected}) in einen unveränderten Prefix und einen womöglich betroffenen Suffix unterteilen.
213 164
@@ -229,6 +180,55 @@ Die input-edits können nun wiederum, unter Beachtung der Verschiebung der indic
229\begin{comment} 180\begin{comment}
230\begin{code} 181\begin{code}
231type LState state input output = (Natural, (state, Maybe (input, Natural))) 182type LState state input output = (Natural, (state, Maybe (input, Natural)))
183
184instance (Ord state, Ord input, Ord output, Show state, Show input, Show output, Finite state) => Action (DFSTAction state input output) input output where
185 type ActionParam (DFSTAction state input output) = DFST state input output
186 type ActionState (DFSTAction state input output) = state
187
188 actionFail = DFSTAction (\_ -> (Seq.empty, Nothing)) Seq.empty
189
190 actionSingleInput = dfstAction
191
192 actionGroundState = stInitial
193 actionStateFinal DFST{..} final = final `Set.member` stAccept
194 actionState _ act st = view _2 $ runDFSTAction' act st
195 actionProduces _ act st = dfstaProduces act st
196
197 actionConsumes _ = dfstaConsumes'
198
199 actionFindPath DFST{..} iState affNewOut fState suffix = do
200 let
201 outFST :: FST (LState state input output) input output
202 outFST = restrictOutput affNewOut $ toFST DFST
203 { stInitial = iState
204 , stTransition
205 , stAccept = Set.fromList $ do
206 fin <- Set.toList $ stAccept `Set.union` Set.map fst (Map.keysSet stTransition)
207 (suffOut, Just fin') <- return $ runDFSTAction' suffix fin
208 guard $ Set.member fin' stAccept
209 guard $ suffOut == dfstaProduces suffix fState
210 return fin
211 }
212 -- trace (show $ pretty outFST) $ Just ()
213
214 newPath <-
215 let
216 FST{..} = outFST
217 detOutgoing :: Maybe (LState state input output) -> [(LState state input output, (Maybe input, Maybe output))]
218 detOutgoing Nothing = concatMap detOutgoing . map Just $ toList stInitial
219 detOutgoing (Just st) = concatMap (\((_, inS), outs) -> map (\(st', outS) -> (st', (inS, outS))) $ toList outs) . Map.toList $ Map.filterWithKey (\(st', _) _ -> st == st') stTransition
220 predicate :: [(LState state input output, (Maybe input, Maybe output))] -> Maybe Bool
221 predicate []
222 | not . Set.null $ Set.intersection stInitial stAccept = Just True
223 | otherwise = Nothing
224 predicate ((lastSt, _) : _)
225 | Set.member lastSt stAccept = Just True
226 | otherwise = Nothing
227 in bfs detOutgoing predicate
228
229 -- trace (show newPath) $ Just ()
230
231 return . Seq.fromList . mapMaybe (\(_st, (inS, _outS)) -> inS) $ reverse newPath
232\end{code} 232\end{code}
233\end{comment} 233\end{comment}
234\begin{code} 234\begin{code}
@@ -236,130 +236,12 @@ dfstLens :: forall state input output. (Ord state, Ord input, Ord output, Show s
236\end{code} 236\end{code}
237\begin{comment} 237\begin{comment}
238\begin{code} 238\begin{code}
239dfstLens dfst@DFST{..} = EditLens ground propR propL 239dfstLens = treeLens
240 where
241 ground :: DFSTComplement state input output
242 ground = mempty
243
244 propR :: (DFSTComplement state input output, StringEdits Natural input) -> (DFSTComplement state input output, StringEdits Natural output)
245 propR (c, SEFail) = (c, SEFail)
246 propR (c, StringEdits Seq.Empty) = (c, mempty)
247 propR (c, lEs@(StringEdits (es :> e)))
248 | (_, Just final) <- runDFSTAction' c' stInitial
249 , final `Set.member` stAccept
250 = (c', rEs)
251 | otherwise
252 = (c, SEFail)
253 where
254 Just int = affected lEs
255 (cAffSuffix, cAffPrefix) = Comp.splitAt (Comp.length c - fromIntegral (Int.inf int)) c
256 (cSuffix, cPrefix) = Comp.splitAt (Comp.length c - (e ^. sePos . from enum)) c
257 cSuffix'
258 | Delete _ <- e
259 , Comp.length cSuffix > 0 = Comp.take (pred $ Comp.length cSuffix) cSuffix
260 | Insert _ nChar <- e = cSuffix <> Comp.singleton (dfstAction dfst nChar)
261 | otherwise = Comp.singleton $ DFSTAction (\_ -> (Seq.empty, Nothing)) Seq.empty
262 (c', _) = propR (cSuffix' <> cPrefix, StringEdits es)
263 (cAffSuffix', _) = Comp.splitAt (Comp.length c' - Comp.length cAffPrefix) c'
264 (_, Just pFinal) = runDFSTAction' cAffPrefix stInitial
265 rEs = strDiff (dfstaProduces cAffSuffix pFinal) (dfstaProduces cAffSuffix' pFinal) & stringEdits . sePos . from enum +~ length (dfstaProduces cAffPrefix stInitial)
266
267
268 propL :: (DFSTComplement state input output, StringEdits Natural output) -> (DFSTComplement state input output, StringEdits Natural input)
269 propL (c, StringEdits Seq.Empty) = (c, mempty)
270 propL (c, es) = fromMaybe (c, SEFail) $ do
271 -- Determine states @(iState, fState)@ at the boundary of the region affected by @es@
272 ((,) <$> Int.inf <*> Int.sup -> (minAff, maxAff)) <- affected es
273 trace (show (minAff, maxAff)) $ Just ()
274 let
275 prevTrans :: Natural -> Maybe ( DFSTComplement state input output -- ^ Run after chosen transition to accepting state
276 , (state, input, Seq output, state)
277 , DFSTComplement state input output -- ^ Run from `stInitial` up to chosen transition
278 )
279 -- ^ Given an index in the output, find the associated transition in @c@
280 prevTrans needle = do
281 let (after, before) = prevTrans' (c, mempty)
282 transSt <- view _2 $ runDFSTAction (Comp.composed before) stInitial
283 trace ("transSt = " ++ show transSt) $ Just ()
284 let (after', trans) = Comp.splitAt (pred $ Comp.length after) after
285 DFSTAction{..} = Comp.composed trans
286 [inS] <- return $ toList dfstaConsumes
287 (outSs , Just postTransSt) <- return $ runDFSTAction transSt
288 return (after', (transSt, inS, outSs, postTransSt), before)
289 where
290 -- | Move monoid summands from @after@ to @before@ until first transition of @after@ produces @needle@ or @after@ is a singleton
291 prevTrans' (after, before)
292 | producedNext > needle = (after, before)
293 | Comp.length after == 1 = (after, before)
294 | otherwise = prevTrans' (after', before')
295 where
296 producedNext = fromIntegral . Seq.length . traceShowId $ dfstaProduces before' stInitial
297 (after', nextTrans) = Comp.splitAt (pred $ Comp.length after) after
298 before' = nextTrans `mappend` before
299 (_, (iState, _, _, _), prefix) <- prevTrans minAff
300 trace (show (iState, Comp.length prefix)) $ Just ()
301 (suffix, (pfState, _, _, fState), _) <- prevTrans maxAff
302 trace (show (pfState, fState, Comp.length suffix)) $ Just ()
303
304 newOut <- dfstaProduces c stInitial `apply` es
305 let affNewOut = (\s -> Seq.take (Seq.length s - Seq.length (dfstaProduces suffix fState)) s) $ Seq.drop (Seq.length $ dfstaProduces prefix stInitial) newOut
306 trace (show (iState, fState, affNewOut)) $ Just ()
307
308 let outFST :: FST (LState state input output) input output
309 outFST = restrictOutput affNewOut $ toFST DFST
310 { stInitial = iState
311 , stTransition
312 , stAccept = Set.fromList $ do
313 fin <- Set.toList $ stAccept `Set.union` Set.map fst (Map.keysSet stTransition)
314 (suffOut, Just fin') <- return $ runDFSTAction' suffix fin
315 guard $ Set.member fin' stAccept
316 guard $ suffOut == dfstaProduces suffix fState
317 return fin
318 }
319 trace (show $ pretty outFST) $ Just ()
320
321 newPath <-
322 let
323 FST{ .. } = outFST
324 detOutgoing :: Maybe (LState state input output) -> [(LState state input output, (Maybe input, Maybe output))]
325 detOutgoing Nothing = concatMap detOutgoing . map Just $ toList stInitial
326 detOutgoing (Just st) = concatMap (\((_, inS), outs) -> map (\(st', outS) -> (st', (inS, outS))) $ toList outs) . Map.toList $ Map.filterWithKey (\(st', _) _ -> st == st') stTransition
327 predicate :: [(LState state input output, (Maybe input, Maybe output))] -> Maybe Bool
328 predicate []
329 | not . Set.null $ Set.intersection stInitial stAccept = Just True
330 | otherwise = Nothing
331 predicate ((lastSt, _) : _)
332 | Set.member lastSt stAccept = Just True
333 | otherwise = Nothing
334 in bfs detOutgoing predicate
335
336 trace (show newPath) $ Just ()
337
338 let oldIn = dfstaConsumes' . Comp.drop (Comp.length suffix) $ Comp.take (Comp.length c - Comp.length prefix) c
339 newIn = Seq.fromList . mapMaybe (\(_st, (inS, _outS)) -> inS) $ reverse newPath
340 inDiff = oldIn `strDiff` newIn
341 diffOffset = fromIntegral . Seq.length $ dfstaConsumes' prefix
342 inDiff' = inDiff & stringEdits . sePos +~ diffOffset
343
344 trace (show (oldIn, newIn, inDiff')) $ Just ()
345
346 let affComp = Comp.fromList [ dfstAction dfst inS | (_st, (Just inS, _outS)) <- newPath ]
347
348 return (suffix <> affComp <> prefix, inDiff')
349
350strDiff :: forall sym pos. (Eq sym, Integral pos) => Seq sym -> Seq sym -> StringEdits pos sym
351-- ^ @strDiff a b@ calculates a set of edits, which, when applied to @a@, produce @b@
352strDiff a b = snd . foldl toEdit (0, mempty) $ (getDiff `on` toList) a b
353 where
354 toEdit :: (pos, StringEdits pos sym) -> Diff sym -> (pos, StringEdits pos sym)
355 toEdit (n, es) (Diff.Both _ _) = (succ n, es)
356 toEdit (n, es) (Diff.First _ ) = (n, delete n <> es)
357 toEdit (n, es) (Diff.Second c) = (succ n, insert n c <> es)
358 240
359-- | Generic breadth-first search 241-- | Generic breadth-first search
360bfs :: forall state transition. Ord state 242bfs :: forall state transition. Ord state
361 => (Maybe state -> [(state, transition)]) -- ^ Find outgoing edges 243 => (Maybe state -> [(state, transition)]) -- ^ Find outgoing edges
362 -> ([(state, transition)] {- ^ Reverse path -} -> Maybe Bool {- ^ Continue search, finish successfully, or abort search on this branch -}) -- ^ Search predicate 244 -> ([(state, transition)] {- Reverse path -} -> Maybe Bool {- Continue search, finish successfully, or abort search on this branch -}) -- ^ Search predicate
363 -> Maybe [(state, transition)] -- ^ Reverse path 245 -> Maybe [(state, transition)] -- ^ Reverse path
364bfs outgoing predicate 246bfs outgoing predicate
365 | Just True <- emptyRes = Just [] 247 | Just True <- emptyRes = Just []
@@ -378,59 +260,46 @@ bfs outgoing predicate
378 Nothing -> bfs' visited' $ cs <> Seq.fromList (map (: c) . filter (\(st, _) -> not $ Set.member st visited) . outgoing $ Just lastSt) 260 Nothing -> bfs' visited' $ cs <> Seq.fromList (map (: c) . filter (\(st, _) -> not $ Set.member st visited) . outgoing $ Just lastSt)
379 where 261 where
380 visited' = Set.insert lastSt visited 262 visited' = Set.insert lastSt visited
381\end{code}
382\end{comment}
383 263
384Um eine obere Schranke an das von einer Serie von edits betroffene Intervall zu bestimmen ordnen wir zunächst jeder von mindestens einem atomaren edit betroffenen Position $n$ im Eingabe-Wort einen $\text{offset}_n = \text{\# deletions} - \text{\# inserts}$ zu. 264-- trace :: String -> a -> a
385Das gesuchte Intervall ist nun $(\text{minK}, \text{maxK})$, mit $\text{minK}$ der Position im Eingabe-Wort mit niedrigstem $\text{offset}$ und $\text{maxK}$ die Position im Eingabe-Wort mit höchstem $\text{offset}$, $\text{maxK}^\prime$, modifiziert um das Maximum aus $\{ 0 \} \cup \{ \text{maxK}_n \colon n \in \{ 0 \ldots \text{maxK}^\prime \} \}$ wobei $\text{maxK}_n = -1 \cdot (n + \text{offset}_n)$ an Position $n$ ist. 265-- {-# NOINLINE trace #-}
266-- trace str y = flip seq y . unsafePerformIO . withFile "lens.log" AppendMode $ \h ->
267-- hPutStrLn h str
386 268
387\begin{code} 269-- traceShowId :: Show a => a -> a
388affected :: forall char. StringEdits Natural char -> Maybe (Interval Natural) 270-- traceShowId x = trace (show x) x
389-- ^ For a given set of edits @es@ return the interval @i = a ... b@ such that for any given string @str@ of sufficient length the following holds:
390--
391-- - For all @n :: Natural@: @n < a ==> str ! n == (str `apply` es) ! n@
392-- - There exists a @k :: Integer@ such that for all @n :: Integer@: @n > b ==> str ! (n + k) == (str `apply` es) ! n@
393--
394-- Intuitively: for any character @c@ of the new string @str `apply` es@ there exists a corresponding character in @str@ (offset by either 0 or a constant shift @k@) if the index of @c@ is /not/ contained in @affected es@.
395\end{code}
396\begin{comment}
397\begin{code}
398affected SEFail = Nothing
399affected (StringEdits es) = Just . toInterval $ go es Map.empty
400 where
401 toInterval :: Map Natural Integer -> Interval Natural
402 toInterval map
403 | Just (((minK, _), _), ((maxK, _), _)) <- (,) <$> Map.minViewWithKey map <*> Map.maxViewWithKey map
404 = let
405 maxV' = maximum . (0 :) $ do
406 offset <- [0..maxK]
407 v <- maybeToList $ Map.lookup (maxK - offset) map
408 v' <- maybeToList . fmap fromInteger $ negate v <$ guard (v <= 0)
409 guard $ v' >= succ offset
410 return $ v' - offset
411 in (minK Int.... maxK + maxV')
412 | otherwise
413 = Int.empty
414 go :: Seq (StringEdit Natural char) -> Map Natural Integer -> Map Natural Integer
415 go Seq.Empty offsets = offsets
416 go (es :> e) offsets = go es offsets'
417 where
418 p = e ^. sePos
419 -- p' = fromIntegral $ Map.foldrWithKey (\k o p -> bool (fromIntegral p) (o + p) $ k < fromIntegral p) (fromIntegral p) offsets
420 offsets' = Map.alter (Just . myOffset . fromMaybe 0) p offsets
421 myOffset :: Integer -> Integer
422 myOffset
423 | Insert _ _ <- e = pred
424 | Delete _ <- e = succ
425
426trace :: String -> a -> a
427{-# NOINLINE trace #-}
428trace str y = flip seq y . unsafePerformIO . withFile "lens.log" AppendMode $ \h ->
429 hPutStrLn h str
430
431traceShowId :: Show a => a -> a
432traceShowId x = trace (show x) x
433
434
435\end{code} 271\end{code}
436\end{comment} 272\end{comment}
273
274\begin{eg}
275 Wir wollen einen edit $e^\prime = \rho_{80}$ anwenden auf das Ergebnis $w^\prime$ der Ausführung des Zeilenumbruch-DFST aus Beispiel \ref{eg:linebreak} auf das Wort $w = 0\, 1\, \ldots\, 80\, \text{\tt \textbackslash n}\, 81\, \ldots\, 98$ aus Beispiel \ref{eg:w100} und dabei $e^\prime$ mittels $\Lleftarrow$ nach links propagieren und den assoziierten edit $e$ auf $w$ konstruieren.
276
277 \begin{equation*}
278 w^\prime = w = 0\, 1\, \ldots\, 80\, \text{\textbackslash n}\, 81\, \ldots\, 98
279 \end{equation*}
280
281 Das von $e$ betroffene Intervall von $w^\prime$ ist $(80, 80)$.
282
283 Das Komplement nach Anwendung des DFST auf $w$ ist, wie in Beispiel \ref{eg:linebreakonw100} dargelegt:
284
285 \begin{align*}
286 \text{act} & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\
287 0 & \mapsto (0\, 1\, \ldots\, 80\, \text{\tt \textbackslash n}\, 81\, \ldots\, 98, 19) \\
288 1 & \mapsto (0\, 1\, \ldots\, 79\, \text{\tt \textbackslash n}\, 80\, \ldots\, 98, 18) \\
289 & \vdots
290 \end{align*}
291
292 Wir unterteilen $\text{act}$ an $(80, 80)$ in $\text{act}_\text{R} \circ \text{act}_e \circ \text{act}_\text{L}$:
293
294 \begin{align*}
295 \text{act}_\text{R} & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\
296 n & \mapsto (81\, \ldots\, 98, \min ( 80, n + 19 ) ) \\
297 & \\
298 \text{act}_e & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\
299 n & \mapsto ( \text{\tt \textbackslash n}, 0 ) \\
300 & \\
301 \text{act}_\text{L} & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\
302 n & \mapsto (0\, 1\, \ldots\, 80, 80) \\
303 \text{other} & \mapsto (\epsilon, \bot)
304 \end{align*}
305\end{eg}
diff --git a/edit-lens/src/Control/DFST/Lens.lhs.tex b/edit-lens/src/Control/DFST/Lens.lhs.tex
new file mode 120000
index 0000000..09aa15c
--- /dev/null
+++ b/edit-lens/src/Control/DFST/Lens.lhs.tex
@@ -0,0 +1 @@
Lens.lhs \ No newline at end of file
diff --git a/edit-lens/src/Control/Edit.lhs b/edit-lens/src/Control/Edit.lhs
index 8c4f045..ba4b8e6 100644
--- a/edit-lens/src/Control/Edit.lhs
+++ b/edit-lens/src/Control/Edit.lhs
@@ -6,6 +6,8 @@ module Control.Edit
6\end{code} 6\end{code}
7\end{comment} 7\end{comment}
8 8
9Um das Intuitive Verhalten von Änderungen auf Texten\footnote{Im folgenden \emph{edits}} und ihre interne algebraische Struktur zu fassen formalisieren wir sie als \emph{Moduln}:
10
9\begin{defn}[Moduln] 11\begin{defn}[Moduln]
10Ein Modul $M$ ist eine \emph{partielle Monoidwirkung} zusammen mit einem schwach-initialen Element\footnote{Gemeint ist hier die übliche Definition von \emph{schwach-initial} aus der Kategorientheorie—ein Modul $M$ bildet eine Kategorie mit Objekten aus $\Dom M$ und Morphismen von $x$ nach $y$ den Monoidelementen $\partial x \in \partial M$ sodass $x \cdot \partial x = y$} (bzgl. der Monoidwirkung) auf dem Träger, d.h. $M = (\Dom M, \partial M, \init_M)$ ist ein Tupel aus einer Trägermenge $\Dom M$, einem Monoid $\partial M$ zusammen mit mit einer partiellen Funktion $\cdot \colon \Dom M \times \partial M \to \Dom$, die \emph{kompatibel} ist mit der Monoid-Struktur: 12Ein Modul $M$ ist eine \emph{partielle Monoidwirkung} zusammen mit einem schwach-initialen Element\footnote{Gemeint ist hier die übliche Definition von \emph{schwach-initial} aus der Kategorientheorie—ein Modul $M$ bildet eine Kategorie mit Objekten aus $\Dom M$ und Morphismen von $x$ nach $y$ den Monoidelementen $\partial x \in \partial M$ sodass $x \cdot \partial x = y$} (bzgl. der Monoidwirkung) auf dem Träger, d.h. $M = (\Dom M, \partial M, \init_M)$ ist ein Tupel aus einer Trägermenge $\Dom M$, einem Monoid $\partial M$ zusammen mit mit einer partiellen Funktion $\cdot \colon \Dom M \times \partial M \to \Dom$, die \emph{kompatibel} ist mit der Monoid-Struktur:
11 13
diff --git a/edit-lens/src/Control/Edit.lhs.tex b/edit-lens/src/Control/Edit.lhs.tex
new file mode 120000
index 0000000..33d3341
--- /dev/null
+++ b/edit-lens/src/Control/Edit.lhs.tex
@@ -0,0 +1 @@
Edit.lhs \ No newline at end of file
diff --git a/edit-lens/src/Control/Edit/String.lhs b/edit-lens/src/Control/Edit/String.lhs
new file mode 100644
index 0000000..c1411cf
--- /dev/null
+++ b/edit-lens/src/Control/Edit/String.lhs
@@ -0,0 +1,120 @@
1\begin{comment}
2\begin{code}
3{-# LANGUAGE TemplateHaskell
4#-}
5
6module Control.Edit.String
7 ( StringEdit(..), sePos, seInsertion
8 , StringEdits(..), _StringEdits, _SEFail, stringEdits
9 , insert, delete, replace
10 ) where
11
12import Control.Lens
13import Control.Lens.TH
14
15import Control.Edit
16
17import Numeric.Natural
18
19import Data.Sequence (Seq((:<|), (:|>)))
20import qualified Data.Sequence as Seq
21
22import Data.Monoid
23\end{code}
24\end{comment}
25
26\begin{defn}[Atomare edits of strings]
27Wir betrachten, zur Einfachheit, ein minimiales Set von Edits auf Strings\footnote{Wie in der Konstruktion zum Longest Common Subsequence Problem}, bestehend nur aus Einfügung eines einzelnen Zeichens $\sigma$ an einer bestimmten Position $\iota_n(\sigma)$ und löschen des Zeichens an einer einzelnen Position $\rho_n$:
28
29\begin{code}
30data StringEdit pos char = Insert { _sePos :: pos, _seInsertion :: char }
31 | Delete { _sePos :: pos }
32 deriving (Eq, Ord, Show, Read)
33
34-- Automatically derive van-leerhoven-lenses:
35--
36-- @sePos :: Lens' (StringEdits pos char) pos@
37-- @seInsertion :: Traversal' (StringEdits pos char) char@
38makeLenses ''StringEdit
39\end{code}
40
41Atomare edits werden, als Liste, zu edits komponiert.
42Wir führen einen speziellen edit ein, der nicht-Anwendbarkeit der edits repräsentiert:
43\begin{code}
44data StringEdits pos char = StringEdits (Seq (StringEdit pos char))
45 | SEFail
46 deriving (Eq, Ord, Show, Read)
47
48makePrisms ''StringEdits
49
50stringEdits :: Traversal (StringEdits pos char) (StringEdits pos' char') (StringEdit pos char) (StringEdit pos' char')
51\end{code}
52\end{defn}
53
54\begin{comment}
55\begin{code}
56stringEdits = _StringEdits . traverse
57
58insert :: pos -> char -> StringEdits pos char
59insert n c = StringEdits . Seq.singleton $ Insert n c
60
61delete :: pos -> StringEdits pos char
62delete n = StringEdits . Seq.singleton $ Delete n
63
64replace :: Eq pos => pos -> char -> StringEdits pos char
65replace n c = insert n c <> delete n
66
67-- | Rudimentarily optimize edit composition
68instance Eq pos => Monoid (StringEdits pos char) where
69 mempty = StringEdits Seq.empty
70 SEFail `mappend` _ = SEFail
71 _ `mappend` SEFail = SEFail
72 (StringEdits Seq.Empty) `mappend` x = x
73 x `mappend` (StringEdits Seq.Empty) = x
74 (StringEdits x@(bs :|> b)) `mappend` (StringEdits y@(a :<| as))
75 | (Insert n _) <- a
76 , (Delete n') <- b
77 , n == n'
78 = StringEdits bs `mappend` StringEdits as
79 | otherwise = StringEdits $ x `mappend` y
80\end{code}
81\end{comment}
82
83Da wir ein minimales Set an atomaren edits gewählt haben, ist die Definiton der Modulnstruktur über Strings des passenden Alphabets recht einfach:
84\begin{code}
85instance Module (StringEdits Natural char) where
86 type Domain (StringEdits Natural char) = Seq char
87 apply str SEFail = Nothing
88 apply str (StringEdits Seq.Empty) = Just str
89 apply str (StringEdits (es :|> Insert n c)) = flip apply (StringEdits es) =<< go str n c
90 where
91 go str (fromIntegral -> n) c
92 | Seq.length str >= n
93 = Just $ Seq.insertAt n c str
94 | otherwise
95 = Nothing
96 apply str (StringEdits (es :|> Delete n)) = flip apply (StringEdits es) =<< go str n
97 where
98 go str (fromIntegral -> n)
99 | Seq.length str > n
100 = Just $ Seq.deleteAt n str
101 | otherwise
102 = Nothing
103
104 init = Seq.empty
105 divInit = StringEdits . Seq.unfoldl go . (0,)
106 where
107 go (_, Seq.Empty) = Nothing
108 go (n, c :<| cs ) = Just ((succ n, cs), Insert n c)
109
110\end{code}
111
112\begin{eg}
113 Wir wenden $\iota_{80}(100) \rho_{80}$ auf das Wort $w$ aus Beispiel~\ref{eg:w100} an:
114
115 \begin{align*}
116 w^\prime & = w \cdot \iota_{80}(100) \rho_{80} \\
117 & = 0\, 1\, \ldots\, 80\, 100\, 81\, 82\, \ldots\, 98
118 \end{align*}
119\end{eg}
120
diff --git a/edit-lens/src/Control/Edit/String.lhs.tex b/edit-lens/src/Control/Edit/String.lhs.tex
new file mode 120000
index 0000000..6a78642
--- /dev/null
+++ b/edit-lens/src/Control/Edit/String.lhs.tex
@@ -0,0 +1 @@
String.lhs \ No newline at end of file
diff --git a/edit-lens/src/Control/Edit/String/Affected.lhs b/edit-lens/src/Control/Edit/String/Affected.lhs
new file mode 100644
index 0000000..851267b
--- /dev/null
+++ b/edit-lens/src/Control/Edit/String/Affected.lhs
@@ -0,0 +1,73 @@
1\begin{comment}
2\begin{code}
3module Control.Edit.String.Affected
4 ( affected
5 ) where
6
7import Control.Lens
8import Control.Lens.TH
9
10import Control.Edit
11import Control.Edit.String
12
13import Numeric.Natural
14import Numeric.Interval (Interval, (...))
15import qualified Numeric.Interval as Int
16
17import Data.Sequence (Seq((:<|), (:|>)))
18import qualified Data.Sequence as Seq
19
20import Data.Map.Lazy (Map)
21import qualified Data.Map.Lazy as Map
22
23import Data.Monoid
24
25import Control.Monad
26
27import Data.Maybe (fromMaybe, maybeToList, listToMaybe, catMaybes, isNothing, isJust, mapMaybe)
28\end{code}
29\end{comment}
30
31Um eine obere Schranke an das von einer Serie von edits betroffene Intervall zu bestimmen ordnen wir zunächst jeder von mindestens einem atomaren edit betroffenen Position $n$ im Eingabe-Wort einen $\text{offset}_n = \text{\# deletions} - \text{\# inserts}$ zu.
32Das gesuchte Intervall ist nun $(\text{minK}, \text{maxK})$, mit $\text{minK}$ der Position im Eingabe-Wort mit niedrigstem $\text{offset}$ und $\text{maxK}$ die Position im Eingabe-Wort mit höchstem $\text{offset}$, $\text{maxK}^\prime$, modifiziert um das Maximum aus $\{ 0 \} \cup \{ \text{maxK}_n \colon n \in \{ 0 \ldots \text{maxK}^\prime \} \}$ wobei $\text{maxK}_n = -1 \cdot (n + \text{offset}_n)$ an Position $n$ ist.
33
34\begin{code}
35affected :: forall char. StringEdits Natural char -> Maybe (Interval Natural)
36-- ^ For a given set of edits @es@ return the interval @i = a ... b@ such that for any given string @str@ of sufficient length the following holds:
37--
38-- - For all @n :: Natural@: @n < a ==> str ! n == (str `apply` es) ! n@
39-- - There exists a @k :: Integer@ such that for all @n :: Integer@: @n > b ==> str ! (n + k) == (str `apply` es) ! n@
40--
41-- Intuitively: for any character @c@ of the new string @str `apply` es@ there exists a corresponding character in @str@ (offset by either 0 or a constant shift @k@) if the index of @c@ is /not/ contained in @affected es@.
42\end{code}
43\begin{comment}
44\begin{code}
45affected SEFail = Nothing
46affected (StringEdits es) = Just . toInterval $ go es Map.empty
47 where
48 toInterval :: Map Natural Integer -> Interval Natural
49 toInterval map
50 | Just (((minK, _), _), ((maxK, _), _)) <- (,) <$> Map.minViewWithKey map <*> Map.maxViewWithKey map
51 = let
52 maxV' = maximum . (0 :) $ do
53 offset <- [0..maxK]
54 v <- maybeToList $ Map.lookup (maxK - offset) map
55 v' <- maybeToList . fmap fromInteger $ negate v <$ guard (v <= 0)
56 guard $ v' >= succ offset
57 return $ v' - offset
58 in (minK Int.... maxK + maxV')
59 | otherwise
60 = Int.empty
61 go :: Seq (StringEdit Natural char) -> Map Natural Integer -> Map Natural Integer
62 go Seq.Empty offsets = offsets
63 go (es :> e) offsets = go es offsets'
64 where
65 p = e ^. sePos
66 -- p' = fromIntegral $ Map.foldrWithKey (\k o p -> bool (fromIntegral p) (o + p) $ k < fromIntegral p) (fromIntegral p) offsets
67 offsets' = Map.alter (Just . myOffset . fromMaybe 0) p offsets
68 myOffset :: Integer -> Integer
69 myOffset
70 | Insert _ _ <- e = pred
71 | Delete _ <- e = succ
72\end{code}
73\end{comment}
diff --git a/edit-lens/src/Control/Edit/String/Affected.lhs.tex b/edit-lens/src/Control/Edit/String/Affected.lhs.tex
new file mode 120000
index 0000000..b85cc7a
--- /dev/null
+++ b/edit-lens/src/Control/Edit/String/Affected.lhs.tex
@@ -0,0 +1 @@
Affected.lhs \ No newline at end of file
diff --git a/edit-lens/src/Control/FST.lhs b/edit-lens/src/Control/FST.lhs
index 9357da7..9739adc 100644
--- a/edit-lens/src/Control/FST.lhs
+++ b/edit-lens/src/Control/FST.lhs
@@ -77,7 +77,9 @@ data FST state input output = FST
77 & \cup \{ (80, \sigma, \sigma, 80) \mid \sigma \in \Sigma \mysetminus \{ \text{\tt ' '}, \text{\tt \textbackslash n} \} \} 77 & \cup \{ (80, \sigma, \sigma, 80) \mid \sigma \in \Sigma \mysetminus \{ \text{\tt ' '}, \text{\tt \textbackslash n} \} \}
78 \end{align*} 78 \end{align*}
79 79
80 \begin{figure}[p] 80 Siehe auch Abbildung~\ref{fig:linebreak}
81
82 \begin{figure}[h]
81 \centering 83 \centering
82 \begin{tikzpicture}[->,auto,node distance=5cm] 84 \begin{tikzpicture}[->,auto,node distance=5cm]
83 \node[initial,state,accepting] (0) {$0$}; 85 \node[initial,state,accepting] (0) {$0$};
@@ -101,7 +103,7 @@ data FST state input output = FST
101 \draw[-] (rest)--(i.north); 103 \draw[-] (rest)--(i.north);
102 \draw[-] (rest)--(si.west); 104 \draw[-] (rest)--(si.west);
103 \end{tikzpicture} 105 \end{tikzpicture}
104 \caption{Beispiel \ref{eg:linebreak} dargestellt als Graph} 106 \caption{\label{fig:linebreak} Ein Transducer der, durch Übersetzung zwischen Leerzeichen und Zeilenumbrüchen, sicher stellt, dass jede Zeile eines Texts mindestens 80 Zeichen hat}
105 \end{figure} 107 \end{figure}
106\end{eg} 108\end{eg}
107 109
@@ -314,7 +316,9 @@ wordFST inps outs = FST
314 & \cup \{ (i, \sigma, \epsilon, i) \mid \sigma \in \Sigma \cup \{ \epsilon \}, i \in Q \mysetminus \{ 99 \} \} 316 & \cup \{ (i, \sigma, \epsilon, i) \mid \sigma \in \Sigma \cup \{ \epsilon \}, i \in Q \mysetminus \{ 99 \} \}
315 \end{align*} 317 \end{align*}
316 318
317 \begin{figure}[p] 319 Siehe auch Abbildung~\ref{fig:w100}.
320
321 \begin{figure}[h]
318 \centering 322 \centering
319 \begin{tikzpicture}[->,auto,node distance=5cm] 323 \begin{tikzpicture}[->,auto,node distance=5cm]
320 \node[initial,state] (0) {$0$}; 324 \node[initial,state] (0) {$0$};
@@ -323,11 +327,11 @@ wordFST inps outs = FST
323 327
324 \path (0) edge [loop above] node {$\{(\sigma, \epsilon) \mid \sigma \in \Sigma \cup \{ \epsilon \} \}$} (0) 328 \path (0) edge [loop above] node {$\{(\sigma, \epsilon) \mid \sigma \in \Sigma \cup \{ \epsilon \} \}$} (0)
325 edge node {$\{ (\sigma, 1) \mid \sigma \in \Sigma \cup \{ \epsilon \} \}$} (rest) 329 edge node {$\{ (\sigma, 1) \mid \sigma \in \Sigma \cup \{ \epsilon \} \}$} (rest)
326 (rest) edge node {$\{ \sigma, 100 \} \mid \sigma \in \Sigma \cup \{ \epsilon \}$} (99) 330 (rest) edge node {$\{ (\sigma, 98) \mid \sigma \in \Sigma \cup \{ \epsilon \} \}$} (99)
327 (99) edge [loop above] node {$\{(\sigma, \epsilon) \mid \sigma \in \Sigma \}$} (99); 331 (99) edge [loop above] node {$\{(\sigma, \epsilon) \mid \sigma \in \Sigma \}$} (99);
328 \end{tikzpicture} 332 \end{tikzpicture}
329 333
330 \caption{Beispiel \ref{eg:w100} dargestellt als Graph} 334 \caption{\label{fig:w100} Der Wort-FST eines längeren Wortes}
331 \end{figure} 335 \end{figure}
332\end{eg} 336\end{eg}
333 337
@@ -351,7 +355,9 @@ restrictOutput :: forall state input output. (Ord state, Ord input, Ord output)
351 & \cup \{ ((80, 80), \text{\tt \textbackslash n}, \text{\tt \textbackslash n}, (81, 0)) \} 355 & \cup \{ ((80, 80), \text{\tt \textbackslash n}, \text{\tt \textbackslash n}, (81, 0)) \}
352 \end{align*} 356 \end{align*}
353 357
354 \begin{figure}[p] 358 Siehe auch Abbildung~\ref{fig:l80timesw100}.
359
360 \begin{figure}[h]
355 \centering 361 \centering
356 \begin{tikzpicture}[->,auto,node distance=5cm] 362 \begin{tikzpicture}[->,auto,node distance=5cm]
357 \node[initial,state] (0) {$0_{W_w}\, 0_{L_{80}}$}; 363 \node[initial,state] (0) {$0_{W_w}\, 0_{L_{80}}$};
@@ -368,12 +374,12 @@ restrictOutput :: forall state input output. (Ord state, Ord input, Ord output)
368 (rest2) edge node {$(98, 98)$} (99); 374 (rest2) edge node {$(98, 98)$} (99);
369 \end{tikzpicture} 375 \end{tikzpicture}
370 376
371 \caption{Beispiel \ref{eg:l80timesw100} dargestellt als Graph} 377 \caption{\label{fig:l80timesw100} Die Einschränkung des Automaten aus Abbildung \ref{fig:linebreak} auf das Wort aus Abbildung \ref{fig:w100}}
372 \end{figure} 378 \end{figure}
373\end{eg} 379\end{eg}
374 380
375\begin{rem} 381\begin{rem}
376 Es ist bemerkenswert, dass in Beispiel \ref{eg:l80timesw100} die Zirkuläre Struktur von $L_80$ durch Produkt mit einem Wort verloren geht. 382 Es ist bemerkenswert, dass in Beispiel \ref{eg:l80timesw100} die Zirkuläre Struktur von $L_{80}$ durch Produkt mit einem Wort verloren geht.
377 383
378 I.\@A.\@ ist das Produkt eines beliebigen FST mit einem Wort-FST zwar nicht azyklisch, erbt jedoch die lineare Struktur des Wort-FST in dem Sinne, dass Fortschritt in Richtung der akzeptierenden Zustände nur möglich ist indem der $(i, \sigma, w_i, i + 1)$-Klasse von Transitionen des Wort-FSTs gefolgt wird. 384 I.\@A.\@ ist das Produkt eines beliebigen FST mit einem Wort-FST zwar nicht azyklisch, erbt jedoch die lineare Struktur des Wort-FST in dem Sinne, dass Fortschritt in Richtung der akzeptierenden Zustände nur möglich ist indem der $(i, \sigma, w_i, i + 1)$-Klasse von Transitionen des Wort-FSTs gefolgt wird.
379\end{rem} 385\end{rem}
diff --git a/edit-lens/src/Control/FST.lhs.tex b/edit-lens/src/Control/FST.lhs.tex
new file mode 120000
index 0000000..b6f3a8f
--- /dev/null
+++ b/edit-lens/src/Control/FST.lhs.tex
@@ -0,0 +1 @@
FST.lhs \ No newline at end of file
diff --git a/edit-lens/src/Control/Lens/Edit.lhs b/edit-lens/src/Control/Lens/Edit.lhs
index 96b2114..6561528 100644
--- a/edit-lens/src/Control/Lens/Edit.lhs
+++ b/edit-lens/src/Control/Lens/Edit.lhs
@@ -12,7 +12,7 @@ import Control.Edit
12\end{comment} 12\end{comment}
13 13
14\begin{defn}[Zustandsbehaftete Monoidhomomorphismen] 14\begin{defn}[Zustandsbehaftete Monoidhomomorphismen]
15Gegeben eine Menge von Komplementen $C$ und Monoiden $M$ und $N$ nennen wir eine partielle Funktion $\psi \colon C \times M \to C \times N$ einen zustandsbehafteten Monoidhomomorphismus wenn sie den folgenden Ansprüchen genügt: 15Gegeben eine Menge $C$ von \emph{Komplementen} und zwei Monoiden $M$ und $N$ nennen wir eine partielle Funktion $\psi \colon C \times M \to C \times N$ einen zustandsbehafteten Monoidhomomorphismus wenn sie den folgenden Ansprüchen genügt:
16 16
17\begin{itemize} 17\begin{itemize}
18 \item $\forall c \in C \colon \psi(1_M, c) = (1_N, c)$ 18 \item $\forall c \in C \colon \psi(1_M, c) = (1_N, c)$
@@ -28,7 +28,7 @@ type StateMonoidHom s m n = (s, m) -> (s, n)
28\end{defn} 28\end{defn}
29 29
30\begin{defn}[edit-lenses] 30\begin{defn}[edit-lenses]
31Für Moduln $M$ und $N$ besteht eine symmetrische edit-lens zwischen $M$ und $N$ aus zwei zustandsbehafteten Monoidhomomorphismen $\Rrightarrow \colon C \times \partial M \to C \times \partial N$ und $\Lleftarrow \colon C \times \partial N \to C \times \partial M$, mit kompatiblem Komplement $C$, einem ausgezeichneten Element $\ground_C$ und einer \emph{Konsistenzrelation} $K \subset \Dom M \times C \times \Dom N$ sodass gilt: 31Für Moduln $M$ und $N$ besteht eine symmetrische edit-lens zwischen $M$ und $N$ aus zwei zustandsbehafteten Monoidhomomorphismen $\Rrightarrow \colon C \times \partial M \to C \times \partial N$ und $\Lleftarrow \colon C \times \partial N \to C \times \partial M$, mit kompatiblem Komplement $C$, einem ausgezeichneten Element $\ground_C \in C$ und einer \emph{Konsistenzrelation} $K \subset \Dom M \times C \times \Dom N$ sodass gilt:
32 32
33\begin{itemize} 33\begin{itemize}
34 \item $(\init_M, \ground_C, \init_N) \in K$ 34 \item $(\init_M, \ground_C, \init_N) \in K$
@@ -67,7 +67,7 @@ instance (Module m, Module n) => HasEditLens (EditLens c m n) m n where
67\end{code} 67\end{code}
68\end{defn} 68\end{defn}
69 69
70\paragraph{Kompatibilität mit bestehenden lens frameworks} 70\subsection{Kompatibilität mit bestehenden lens frameworks}
71 71
72Das einschlägige bestehende lens framework \cite{lens} konstruiert seine Linsen alá \citeauthor{laarhoven} wie folgt: 72Das einschlägige bestehende lens framework \cite{lens} konstruiert seine Linsen alá \citeauthor{laarhoven} wie folgt:
73 73
diff --git a/edit-lens/src/Control/Lens/Edit.lhs.tex b/edit-lens/src/Control/Lens/Edit.lhs.tex
new file mode 120000
index 0000000..33d3341
--- /dev/null
+++ b/edit-lens/src/Control/Lens/Edit.lhs.tex
@@ -0,0 +1 @@
Edit.lhs \ No newline at end of file
diff --git a/edit-lens/src/Control/Lens/Edit/ActionTree.lhs b/edit-lens/src/Control/Lens/Edit/ActionTree.lhs
new file mode 100644
index 0000000..6632dce
--- /dev/null
+++ b/edit-lens/src/Control/Lens/Edit/ActionTree.lhs
@@ -0,0 +1,204 @@
1\begin{comment}
2\begin{code}
3{-# LANGUAGE ScopedTypeVariables
4 , TypeApplications
5 , TypeFamilyDependencies
6 #-}
7
8module Control.Lens.Edit.ActionTree
9 ( Action(..)
10 , treeLens
11 ) where
12
13import Control.Edit
14import Control.Edit.String
15import Control.Edit.String.Affected
16import Control.Lens.Edit
17
18import Control.Lens
19
20import Numeric.Natural
21import Numeric.Interval (Interval, (...))
22import qualified Numeric.Interval as Int
23
24import Data.Compositions (Compositions)
25import qualified Data.Compositions as Comp
26
27import Data.Algorithm.Diff (Diff, getDiff)
28import qualified Data.Algorithm.Diff as Diff
29
30import Data.Sequence (Seq((:<|), (:|>)))
31import qualified Data.Sequence as Seq
32import Data.Set (Set)
33import qualified Data.Set as Set
34
35import Data.Monoid
36import Data.Function (on)
37import Data.Foldable (toList)
38import Data.Maybe (fromMaybe)
39
40import System.IO (Handle, hPutStrLn, IOMode(AppendMode), withFile)
41import System.IO.Unsafe
42\end{code}
43\end{comment}
44
45Das beschrieben Verfahren wurde prinzipiell agnostisch in Bezug auf die konkret gewählte Parser-Konstruktion gewählt.
46
47Hierfür wurden die benötigten Operationen auf der DFST-Wirkung und das in $\Lleftarrow$ verwendete Suchschema abstrakt als Typklasse angegeben:
48
49\begin{code}
50class Monoid action => Action action input output | action -> input, action -> output where
51\end{code}
52\begin{comment}
53\begin{code}
54 -- | Most operations of `Action` permit access to some underlying description of the parser (i.e. an automaton)
55 type ActionParam action = param | param -> action
56
57 -- | A full capture of the Parser-State (i.e. a state for a given automaton)
58 type ActionState action :: *
59
60 -- | `mempty` should be neutral under `(<>)`, `actionFail` should be absorptive
61 actionFail :: action
62
63 -- | Construct an @action@ from a single character of input
64 actionSingleInput :: ActionParam action -> input -> action
65 -- | Initial state of the parser
66 actionGroundState :: ActionParam action -> ActionState action
67 -- | Is a certain state acceptable as final?
68 actionStateFinal :: ActionParam action -> ActionState action -> Bool
69 -- | Run an @action@ (actually a binary tree thereof, use `Comp.composed` to extract the root) on a given state
70 actionState :: ActionParam action -> Compositions action -> ActionState action -> Maybe (ActionState action)
71 -- | What @output@ does running an @action@ on a given state produce?
72 actionProduces :: ActionParam action -> Compositions action -> ActionState action -> Seq output
73 -- | What @input@ does running an @action@ on a given state consume?
74 actionConsumes :: ActionParam action -> Compositions action -> Seq input
75
76 -- | Find a new string of @input@-symbols to travel between the given states while producing exactly the given @output@
77 --
78 -- @actionFindPath@ also has access to the remaining action to be run after it's new @input@ has been consumed.
79 -- This is necessary to further restrict the considered paths in such a way that the resulting run as a whole is acceptable in the sense of `actionStateFinal`.
80 actionFindPath :: ActionParam action
81 -> ActionState action -- ^ From
82 -> Seq output -- ^ New output to be produced
83 -> ActionState action -- ^ To
84 -> Compositions action -- ^ Suffix
85 -> Maybe (Seq input)
86\end{code}
87\end{comment}
88
89Das Verfahren kann nun auf andere Sorten von Parser angewendet werden, indem nur die oben aufgeführte \texttt{Action}-Typklasse implementiert wird:
90
91\begin{code}
92treeLens :: forall action input output.
93 ( Ord input, Ord output
94 , Show input, Show output
95 , Action action input output
96 , Show (ActionState action)
97 ) => ActionParam action -> EditLens (Compositions action) (StringEdits Natural input) (StringEdits Natural output)
98\end{code}
99\begin{comment}
100\begin{code}
101treeLens param = EditLens ground propR propL
102 where
103 ground :: Compositions action
104 ground = mempty
105
106 propR :: (Compositions action, StringEdits Natural input)
107 -> (Compositions action, StringEdits Natural output)
108 propR (c, SEFail) = (c, SEFail)
109 propR (c, StringEdits Seq.Empty) = (c, mempty)
110 propR (c, lEs@(StringEdits (es :> e)))
111 | Just final <- actionState param c' $ actionGroundState @action param
112 , actionStateFinal param final
113 = (c', rEs)
114 | otherwise
115 = (c, SEFail)
116 where
117 Just int = affected lEs
118 (cAffSuffix, cAffPrefix) = Comp.splitAt (Comp.length c - fromIntegral (Int.inf int)) c
119 (cSuffix, cPrefix) = Comp.splitAt (Comp.length c - (e ^. sePos . from enum)) c
120 cSuffix'
121 | Delete _ <- e
122 , Comp.length cSuffix > 0 = Comp.take (pred $ Comp.length cSuffix) cSuffix
123 | Insert _ nChar <- e = cSuffix <> Comp.singleton (actionSingleInput param nChar)
124 | otherwise = Comp.singleton actionFail
125 (c', _) = propR (cSuffix' <> cPrefix, StringEdits es)
126 (cAffSuffix', _) = Comp.splitAt (Comp.length c' - Comp.length cAffPrefix) c'
127 Just pFinal = actionState param cAffPrefix $ actionGroundState @action param
128 rEs = strDiff (actionProduces param cAffSuffix pFinal) (actionProduces param cAffSuffix' pFinal) & stringEdits . sePos . from enum +~ length (actionProduces param cAffPrefix $ actionGroundState @action param)
129
130 propL :: (Compositions action, StringEdits Natural output)
131 -> (Compositions action, StringEdits Natural input)
132 propL (c, StringEdits Seq.Empty) = (c, mempty)
133 propL (c, es) = fromMaybe (c, SEFail) $ do
134 -- Determine states @(iState, fState)@ at the boundary of the region affected by @es@
135 ((,) <$> Int.inf <*> Int.sup -> (minAff, maxAff)) <- affected es
136 trace (show (minAff, maxAff)) $ Just ()
137 let
138 prevTrans :: Natural -> Maybe ( Compositions action {- Run after chosen transition to accepting state -}
139 , (ActionState action, input, Seq output, ActionState action)
140 , Compositions action {- Run from `stInitial` up to chosen transition -}
141 )
142 -- ^ Given an index in the output, find the associated transition in @c@
143 prevTrans needle = do
144 let (after, before) = prevTrans' (c, mempty)
145 transSt <- actionState param before $ actionGroundState @action param
146 trace ("transSt = " ++ show transSt) $ Just ()
147 let (after', trans) = Comp.splitAt (pred $ Comp.length after) after
148 [inS] <- return . toList $ actionConsumes param trans
149 Just postTransSt <- return $ actionState param trans transSt
150 outSs <- return $ actionProduces param trans transSt
151 return (after', (transSt, inS, outSs, postTransSt), before)
152 where
153 -- | Move monoid summands from @after@ to @before@ until first transition of @after@ produces @needle@ or @after@ is a singleton
154 prevTrans' :: (Compositions action, Compositions action)
155 -> (Compositions action, Compositions action)
156 prevTrans' (after, before)
157 | producedNext > needle = (after, before)
158 | Comp.length after == 1 = (after, before)
159 | otherwise = prevTrans' (after', before')
160 where
161 producedNext = fromIntegral . Seq.length . traceShowId . actionProduces param before' $ actionGroundState @action param
162 (after', nextTrans) = Comp.splitAt (pred $ Comp.length after) after
163 before' = nextTrans `mappend` before
164 (_, (iState, _, _, _), prefix) <- prevTrans minAff
165 trace (show (iState, Comp.length prefix)) $ Just ()
166 (suffix, (pfState, _, _, fState), _) <- prevTrans maxAff
167 trace (show (pfState, fState, Comp.length suffix)) $ Just ()
168
169 newOut <- actionProduces param c (actionGroundState @action param) `apply` es
170 let affNewOut = (\s -> Seq.take (Seq.length s - Seq.length (actionProduces param suffix fState)) s) $ Seq.drop (Seq.length . actionProduces param prefix $ actionGroundState @action param) newOut
171 trace (show (iState, fState, affNewOut)) $ Just ()
172
173 newIn <- actionFindPath param iState affNewOut fState suffix
174
175 let oldIn = actionConsumes param . Comp.drop (Comp.length suffix) $ Comp.take (Comp.length c - Comp.length prefix) c
176 inDiff = oldIn `strDiff` newIn
177 diffOffset = fromIntegral . Seq.length $ actionConsumes param prefix
178 inDiff' = inDiff & stringEdits . sePos +~ diffOffset
179
180 trace (show (oldIn, newIn, inDiff')) $ Just ()
181
182 let affComp = Comp.fromList $ actionSingleInput param <$> toList newIn
183
184 return (suffix <> affComp <> prefix, inDiff')
185
186
187strDiff :: forall sym pos. (Eq sym, Integral pos) => Seq sym -> Seq sym -> StringEdits pos sym
188-- ^ @strDiff a b@ calculates a set of edits, which, when applied to @a@, produce @b@
189strDiff a b = snd . foldl toEdit (0, mempty) $ (getDiff `on` toList) a b
190 where
191 toEdit :: (pos, StringEdits pos sym) -> Diff sym -> (pos, StringEdits pos sym)
192 toEdit (n, es) (Diff.Both _ _) = (succ n, es)
193 toEdit (n, es) (Diff.First _ ) = (n, delete n <> es)
194 toEdit (n, es) (Diff.Second c) = (succ n, insert n c <> es)
195
196trace :: String -> a -> a
197{-# NOINLINE trace #-}
198trace str y = flip seq y . unsafePerformIO . withFile "lens.log" AppendMode $ \h ->
199 hPutStrLn h str
200
201traceShowId :: Show a => a -> a
202traceShowId x = trace (show x) x
203\end{code}
204\end{comment}
diff --git a/edit-lens/src/Control/Lens/Edit/ActionTree.lhs.tex b/edit-lens/src/Control/Lens/Edit/ActionTree.lhs.tex
new file mode 120000
index 0000000..6e3c68c
--- /dev/null
+++ b/edit-lens/src/Control/Lens/Edit/ActionTree.lhs.tex
@@ -0,0 +1 @@
ActionTree.lhs \ No newline at end of file
diff --git a/implementation.tex b/implementation.tex
new file mode 100644
index 0000000..f5e5e58
--- /dev/null
+++ b/implementation.tex
@@ -0,0 +1,89 @@
1Im Rahmen dieser Arbeit haben wir die in den vorherigen Abschnitten beschriebenen Verfahren und Konstruktionen in Haskell implementiert.
2
3Es hat sich hierbei die oben beschriebene Konstruktion von $\Lleftarrow$ als Komposition algebraischer Transformationen und generischer, wohlbekannter, Algorithmen (Breitensuche auf einem beliebigem Graph) ergeben.
4Unsere vorherigen Versuche $\Lleftarrow$ in einem imperativeren Stil zu implementieren blieben Erfolglos; größte Schwierigkeiten hat bereitet die diversen Randbedingungen (Anfangs- und Endzustand, zu produzierende Ausgabe) innerhalb des Algorithmus zur Breitensuche zu wahren.
5
6\subsubsection{Struktur der Implementierung}
7
8Die Implementierung ist aufgeteilt in zwei Stack\footnote{\url{https://haskellstack.org}}-Pakete: \texttt{edit-lens} und \texttt{interactive-edit-lens}.
9
10Die Module innerhalb von \texttt{edit-lens} entsprechen im wesentlichen den Sektionen dieser Arbeit:
11\begin{description}
12\item[Control.Edit]
13 Definition von Moduln
14\item[Control.Lens.Edit]
15 Definition von zustandsbehafteten Monoidhomomorphismen und, damit, edit-lenses sowohl als Typklasse als auch als existentiell quantifizierter Datentyp
16\item[Control.Edit.String]
17 Eine simple edit-Sprache auf Strings
18\item[Control.Edit.String.Affected]
19 Ein Algorithmus um die von einem edit aus \textbf{Control.Edit.String} betroffene Stelle in einem String einzuschränken
20\item[Control.FST]
21 Datentyp, schrittweise-, und vollständige Auswertung und die algebraischen Konstruktionen aus $\Lleftarrow$ für finite state transducer
22\item[Control.DFST]
23 Datentyp, schrittweise-, und vollständige Auswertung sowie Umwandlung zu einem FST für deterministische finite state transducer
24\item[Control.Lens.Edit.ActionTree]
25 Das beschriebene Verfahren zur Darstellung eines beliebigen DFST als edit-lens für jene edit-Sprache
26
27 Es ist hierbei jedoch der konkrete Typ der Wirkung und das Suchschema für $\Lleftarrow$ als Typklasse abstrahiert
28\item[Control.DFST.Lens]
29 Konkrete Anwendung von \textbf{Control.Lens.Edit.ActionTree} auf DFSTs
30\end{description}
31
32\texttt{edit-lens} enthält zudem eine rudimentäre suite von Tests, die die Korrektheit der FST- und DFST-Implementierung, sowie den Algorithmus zum Anwenden von String-Edits prüft.
33
34\texttt{interactive-edit-lens} besteht aus nur drei Modulen:
35\begin{description}
36\item[Interact]
37 Implementierung des interaktiven Editors als TUI\footnote{\url{https://hackage.haskell.org/package/brick-0.47}}
38\item[Interact.Types]
39 Unterliegende Datentypen für \texttt{Interact}
40\item[Main]
41 Aufruf von \texttt{Interact} und Implementierung der angebotenen DFSTs
42\end{description}
43
44\subsubsection{Verwendung des interaktiven Editors}
45
46\begin{figure}[h]
47 \begin{center}
48 \includegraphics{screenshot}
49 \caption{Der interaktive Editor (im Modus \texttt{json-newl}) nach import einer kleinen JSON-Datei}
50 \end{center}
51\end{figure}
52
53Der interaktive editor kann von der Befehlseingabe gestartet werden wie folgt:
54\begin{lstlisting}[language=bash]
55 $ stack build
56 $ stack exec interact <dfst
57\end{lstlisting}
58Hierbei ist \texttt{<dfst>} einer der in \texttt{Main} implementierten DFSTs:
59
60\begin{description}
61\item[linebreak]
62 Wandelt Zeilenumbrüche und Leerzeichen ineinander um, sodass alle Zeilen mindestens 80 Zeichen enthalten
63\item[json-newl]
64 Normalisiert Whitespace in einem JSON\footnote{\url{https://de.wikipedia.org/wiki/JSON}}-String.
65 JSON ist nicht regulär; Es lassen sich Klammern nicht prüfen und Einrückung nicht in Abhängigkeit der Verschachtelung implementieren
66\item[alternate]
67 Akzeptiert Strings gerader Länge, jeder zweite Buchstabe wird in den entsprechenden Großbuchstaben umgewandelt und verdoppelt
68\item[id]
69 Identität-DFST
70\item[double]
71 Verdoppelt jedes Zeichen
72\end{description}
73
74Alle DFSTs (außer \texttt{json-newl}) akzeptieren nur lateinische Buchstaben, Leerzeichen und das Ausrufezeichen.
75
76Der Text auf beiden Seiten kann frei bearbeitet werden.
77Hierbei wechselt \texttt{tab} zwischen den Seiten.
78
79\texttt{ctrl + p} setzt die Propagation aus, bis sie mit \texttt{ctrl + p} wieder eingeschaltet wird.
80Auf der Konsole werden hinterher Zeitmessungen der ersten Propagation nach dem Wiedereinsetzen ausgegeben.
81
82\texttt{ctrl + o} öffnet eine interaktive Dateiauswahl (\texttt{/} veranlasst eine Suche, \texttt{return} bestätigt die Auswahl).
83Nach Auswahl wird der Inhalt der Datei am Cursor eingefügt.
84
85\subsubsection{Performance}
86
87Bei der Implementierung wurde nicht auf Performance geachtet.
88Es ist daher die Laufzeit des interaktiven Editors bereits bei kleinen Eingabe inakzeptabel lang (mehrere Sekunden für ein Kilobyte JSON).
89Es lässt sich allerdings der Speedup beim Propagieren kleiner edits gut beobachten; die Propagation eines ein-Buchstaben-edits nach rechts ist ca. einen Faktor 200 schneller als das komplett neue Parsen einer Datei (ca. ein Kilobyte JSON).
diff --git a/interactive-edit-lens/package.yaml b/interactive-edit-lens/package.yaml
index 95e2464..80d2a31 100644
--- a/interactive-edit-lens/package.yaml
+++ b/interactive-edit-lens/package.yaml
@@ -38,6 +38,7 @@ dependencies:
38 - mtl 38 - mtl
39 - transformers 39 - transformers
40 - universe 40 - universe
41 - deepseq
41 42
42# ghc-options: [ -O2 ] 43# ghc-options: [ -O2 ]
43 44
diff --git a/interactive-edit-lens/src/Interact.hs b/interactive-edit-lens/src/Interact.hs
index 0074e86..662052b 100644
--- a/interactive-edit-lens/src/Interact.hs
+++ b/interactive-edit-lens/src/Interact.hs
@@ -14,6 +14,7 @@ import Interact.Types
14 14
15import Data.Text (Text) 15import Data.Text (Text)
16import qualified Data.Text as Text 16import qualified Data.Text as Text
17import qualified Data.Text.IO as Text
17 18
18import Data.Text.Zipper 19import Data.Text.Zipper
19 20
@@ -41,6 +42,7 @@ import Brick hiding (on)
41import Brick.Focus 42import Brick.Focus
42import Brick.Widgets.Center 43import Brick.Widgets.Center
43import Brick.Widgets.Border 44import Brick.Widgets.Border
45import Brick.Widgets.FileBrowser
44import Graphics.Vty hiding (showCursor) 46import Graphics.Vty hiding (showCursor)
45 47
46import Config.Dyre 48import Config.Dyre
@@ -48,14 +50,20 @@ import Config.Dyre
48import System.IO.Unsafe 50import System.IO.Unsafe
49import Debug.Trace 51import Debug.Trace
50 52
51interactiveEditLens :: (Params (InteractConfig c) -> Params (InteractConfig c)) -> InteractConfig c -> IO () 53import System.CPUTime
54import Text.Printf
55
56import Control.Exception (evaluate)
57import Control.DeepSeq
58
59interactiveEditLens :: forall c. NFData c => (Params (InteractConfig c) -> Params (InteractConfig c)) -> InteractConfig c -> IO ()
52interactiveEditLens f = wrapMain . f $ defaultParams 60interactiveEditLens f = wrapMain . f $ defaultParams
53 { projectName = "interact-edit-lens" 61 { projectName = "interact-edit-lens"
54 , showError = \s err -> s & compileError .~ Just err 62 , showError = \s err -> s & compileError .~ Just err
55 , realMain = interactiveEditLens' 63 , realMain = interactiveEditLens'
56 } 64 }
57 65
58interactiveEditLens' :: forall c. InteractConfig c -> IO () 66interactiveEditLens' :: forall c. NFData c => InteractConfig c -> IO ()
59interactiveEditLens' cfg@InteractConfig{..} 67interactiveEditLens' cfg@InteractConfig{..}
60 | Just err <- icfgCompileError 68 | Just err <- icfgCompileError
61 = hPutStrLn stderr err 69 = hPutStrLn stderr err
@@ -89,9 +97,8 @@ interactiveEditLens' cfg@InteractConfig{..}
89 where 97 where
90 infix 1 &?~ 98 infix 1 &?~
91 99
92 (&?~) :: a -> RWS (InteractConfig c) () a b -> a 100 (&?~), actOn :: a -> RWS (InteractConfig c) () a b -> a
93 st &?~ act = (\(s, ()) -> s) $ execRWS act cfg st 101 st &?~ act = (\(s, ()) -> s) $ execRWS act cfg st
94
95 actOn = (&?~) 102 actOn = (&?~)
96 103
97 initialState :: InteractState c 104 initialState :: InteractState c
@@ -101,6 +108,8 @@ interactiveEditLens' cfg@InteractConfig{..}
101 , istRight = (Last Valid, Last (init @(StringEdits Natural Char), 0), mempty) 108 , istRight = (Last Valid, Last (init @(StringEdits Natural Char), 0), mempty)
102 , istFocus = focusRing [LeftEditor, RightEditor] & 109 , istFocus = focusRing [LeftEditor, RightEditor] &
103 focusSetCurrent (case icfgInitial of InitialRight _ -> RightEditor; _other -> LeftEditor) 110 focusSetCurrent (case icfgInitial of InitialRight _ -> RightEditor; _other -> LeftEditor)
111 , istActive = True
112 , istLoadBrowser = Nothing
104 } 113 }
105 114
106 app :: InteractApp c 115 app :: InteractApp c
@@ -109,10 +118,15 @@ interactiveEditLens' cfg@InteractConfig{..}
109 appDraw :: InteractState c -> [Widget InteractName] 118 appDraw :: InteractState c -> [Widget InteractName]
110 appDraw InteractState{..} = [ editors ] 119 appDraw InteractState{..} = [ editors ]
111 where 120 where
112 editors = hBox 121 editors = vBox
113 [ mbInvalid (withFocusRing istFocus renderEditor') (istLeft `WithName` LeftEditor) 122 [ case istLoadBrowser of
114 , vBorder 123 Nothing -> hBox
115 , mbInvalid (withFocusRing istFocus renderEditor') (istRight `WithName` RightEditor) 124 [ mbInvalid (withFocusRing istFocus renderEditor') (istLeft `WithName` LeftEditor)
125 , vBorder
126 , mbInvalid (withFocusRing istFocus renderEditor') (istRight `WithName` RightEditor)
127 ]
128 Just lBrowser -> renderFileBrowser True lBrowser
129 , hCenter . str $ bool "Inactive" "" istActive
116 ] 130 ]
117 renderEditor' :: Bool -> (Seq Char, Int) `WithName` InteractName -> Widget InteractName 131 renderEditor' :: Bool -> (Seq Char, Int) `WithName` InteractName -> Widget InteractName
118 renderEditor' foc ((content, cPos) `WithName` n) 132 renderEditor' foc ((content, cPos) `WithName` n)
@@ -133,42 +147,75 @@ interactiveEditLens' cfg@InteractConfig{..}
133 mbInvalid f ((Last Valid , Last x, _) `WithName` n) = f $ x `WithName` n 147 mbInvalid f ((Last Valid , Last x, _) `WithName` n) = f $ x `WithName` n
134 148
135 appHandleEvent :: InteractState c -> BrickEvent InteractName InteractEvent -> EventM InteractName (Next (InteractState c)) 149 appHandleEvent :: InteractState c -> BrickEvent InteractName InteractEvent -> EventM InteractName (Next (InteractState c))
136 appHandleEvent st@InteractState{..} (VtyEvent ev) = case ev of 150 appHandleEvent st@InteractState{..} (VtyEvent ev)
137 EvKey KEsc [] -> halt st 151 | Nothing <- istLoadBrowser = case ev of
138 EvKey (KChar 'c') [MCtrl] -> halt st 152 EvKey KEsc [] -> halt st
139 EvKey (KChar '\t') [] -> continue $ st & focus %~ focusNext 153 EvKey (KChar 'c') [MCtrl] -> halt st
140 EvKey KBackTab [] -> continue $ st & focus %~ focusPrev 154 EvKey (KChar '\t') [] -> continue . actOn st . runMaybeT $ do
141 EvKey (KChar 'a') [MCtrl] -> continue $ st &?~ doMove 155 guard =<< use active
142 (moveSplit (== '\n') $ \(c, (l, p)) -> if any (== '\n') (c l) || Seq.null (c l) then (pred l, 0) else (l, 0)) 156 focus %= focusNext
143 EvKey (KChar 'e') [MCtrl] -> continue $ st &?~ doMove 157 EvKey KBackTab [] -> continue . actOn st . runMaybeT $ do
144 (moveSplit (== '\n') $ \(c, (l, p)) -> if any (== '\n') $ c l then (pred l, Seq.length . c $ pred l) else (l, Seq.length $ c l)) 158 guard =<< use active
145 EvKey KLeft [MCtrl] -> continue $ st &?~ doMove 159 focus %= focusPrev
146 (moveSplit isSpace $ \(c, (l, _)) -> if any isSpace (c l) || Seq.null (c l) then (pred l, 0) else (l - 2, 0)) 160 EvKey (KChar 'a') [MCtrl] -> continue $ st &?~ doMove
147 EvKey KRight [MCtrl] -> continue $ st &?~ doMove 161 (moveSplit (== '\n') $ \(c, (l, p)) -> if any (== '\n') (c l) || Seq.null (c l) then (pred l, 0) else (l, 0))
148 (moveSplit isSpace $ \(c, (l, _)) -> if any isSpace $ c l then (succ l, 0) else (l + 2, 0)) 162 EvKey (KChar 'e') [MCtrl] -> continue $ st &?~ doMove
149 EvKey KUp [] -> continue $ st &?~ doMove 163 (moveSplit (== '\n') $ \(c, (l, p)) -> if any (== '\n') $ c l then (pred l, Seq.length . c $ pred l) else (l, Seq.length $ c l))
150 (moveSplit (== '\n') $ \(c, (l, p)) -> if any (== '\n') (c l) || Seq.null (c l) then (pred l, p) else (l - 2, p)) 164 EvKey KLeft [MCtrl] -> continue $ st &?~ doMove
151 EvKey KDown [] -> continue $ st &?~ doMove 165 (moveSplit isSpace $ \(c, (l, _)) -> if any isSpace (c l) || Seq.null (c l) then (pred l, 0) else (l - 2, 0))
152 (moveSplit (== '\n') $ \(c, (l, p)) -> if any (== '\n') (c l) then (succ l, p) else (l + 2, p)) 166 EvKey KRight [MCtrl] -> continue $ st &?~ doMove
153 EvKey KLeft [] -> continue $ st &?~ doMove moveLeft 167 (moveSplit isSpace $ \(c, (l, _)) -> if any isSpace $ c l then (succ l, 0) else (l + 2, 0))
154 EvKey KRight [] -> continue $ st &?~ doMove moveRight 168 EvKey KUp [] -> continue $ st &?~ doMove
155 EvKey KDel [] -> continue $ st &?~ doEdit (delete 0) 169 (moveSplit (== '\n') $ \(c, (l, p)) -> if any (== '\n') (c l) || Seq.null (c l) then (pred l, p) else (l - 2, p))
156 EvKey KBS [] -> continue . actOn st $ do 170 EvKey KDown [] -> continue $ st &?~ doMove
157 focused' <- preuse $ focused . _2 . _Wrapped 171 (moveSplit (== '\n') $ \(c, (l, p)) -> if any (== '\n') (c l) then (succ l, p) else (l + 2, p))
158 doEdit . delete $ -1 172 EvKey KLeft [] -> continue $ st &?~ doMove moveLeft
159 unless (maybe False ((==) <$> view _2 <*> view (_1 . to Seq.length)) focused') $ 173 EvKey KRight [] -> continue $ st &?~ doMove moveRight
160 doMove moveLeft 174 EvKey KDel [] -> continue $ st &?~ doEdit (delete 0)
161 EvKey (KChar c) [] -> continue . actOn st $ do 175 EvKey KBS [] -> continue . actOn st $ do
162 doEdit $ insert 0 c 176 focused' <- preuse $ focused . _2 . _Wrapped
163 doMove moveRight 177 doEdit . delete $ -1
164 EvKey KEnter [] -> continue . actOn st $ do 178 unless (maybe False ((==) <$> view _2 <*> view (_1 . to Seq.length)) focused') $
165 doEdit $ insert 0 '\n' 179 doMove moveLeft
166 doMove moveRight 180 EvKey (KChar c) [] -> continue . actOn st $ do
167 other -> suspendAndResume $ do 181 doEdit $ insert 0 c
168 traceIO $ "Unhandled event:\n\t" ++ show other 182 doMove moveRight
169 return st 183 EvKey KEnter [] -> continue . actOn st $ do
170 -- where 184 doEdit $ insert 0 '\n'
171 -- editorMovement f = continue $ st & focused . _Just . editContentsL %~ f 185 doMove moveRight
186 EvKey (KChar 'p') [MCtrl]
187 | istActive -> do
188 void . liftIO . evaluate . force . ($ st) $ (,,) <$> view left <*> view right <*> view complement
189 continue $ st & active .~ False
190 | otherwise -> do
191 let st' = actOn st $ do
192 active .= True
193 doEdit mempty
194 before <- liftIO getCPUTime
195 void . liftIO . evaluate . force . ($ st') $ (,,) <$> view left <*> view right <*> view complement
196 after <- liftIO getCPUTime
197 suspendAndResume $ do
198 printf "Resume took %.12fs\n" (fromInteger (after - before) * 1e-12 :: Double)
199 return st'
200 EvKey (KChar 'o') [MCtrl] -> do
201 lBrowser <- liftIO $ newFileBrowser selectNonDirectories LoadBrowser Nothing
202 continue $ st & loadBrowser .~ Just lBrowser
203 other -> suspendAndResume $ do
204 traceIO $ "Unhandled event:\n\t" ++ show other
205 return st
206 -- where
207 -- editorMovement f = continue $ st & focused . _Just . editContentsL %~ f
208 | Just lBrowser <- istLoadBrowser = do
209 lBrowser' <- handleFileBrowserEvent ev lBrowser
210 case fileBrowserSelection lBrowser' of
211 [] -> continue $ st &?~ loadBrowser .= Just lBrowser'
212 (FileInfo{..} : _) -> do
213 insEdit <- divInit . view charseq <$> liftIO (Text.readFile fileInfoFilePath)
214 let st' = actOn st $ do
215 doEdit $ (insEdit :: StringEdits Natural Char) & stringEdits . sePos %~ fromIntegral
216 loadBrowser .= Nothing
217 continue st'
218
172 appHandleEvent st _ = continue st 219 appHandleEvent st _ = continue st
173 220
174 doMove = zoom $ focused . _2 . _Wrapped 221 doMove = zoom $ focused . _2 . _Wrapped
@@ -259,9 +306,10 @@ doEdit relativeEdit = void . runMaybeT $ do
259 | otherwise = currentPos 306 | otherwise = currentPos
260 aL . _2 %= (<> Last (newContent, currentPos')) 307 aL . _2 %= (<> Last (newContent, currentPos'))
261 absoluteEdit' <- uses (aL . _3) (absoluteEdit `mappend`) 308 absoluteEdit' <- uses (aL . _3) (absoluteEdit `mappend`)
262 bEdits <- prop direction absoluteEdit' 309 bRes <- runMaybeT $ do
263 bDom <- use $ bL . _2 . _Wrapped . _1 310 guard =<< use active
264 case bDom `apply` bEdits of 311 (,) <$> use (bL . _2 . _Wrapped . _1) <*> prop direction absoluteEdit'
312 case uncurry apply =<< bRes of
265 Nothing -> do 313 Nothing -> do
266 bL . _1 %= (<> Last Invalid) 314 bL . _1 %= (<> Last Invalid)
267 aL . _3 .= absoluteEdit' 315 aL . _3 .= absoluteEdit'
diff --git a/interactive-edit-lens/src/Interact/Types.hs b/interactive-edit-lens/src/Interact/Types.hs
index a4d08ac..67f9ae3 100644
--- a/interactive-edit-lens/src/Interact/Types.hs
+++ b/interactive-edit-lens/src/Interact/Types.hs
@@ -1,4 +1,4 @@
1{-# LANGUAGE TemplateHaskell #-} 1{-# LANGUAGE TemplateHaskell, DeriveGeneric, StandaloneDeriving #-}
2{-# OPTIONS_GHC -fno-warn-orphans #-} 2{-# OPTIONS_GHC -fno-warn-orphans #-}
3 3
4module Interact.Types 4module Interact.Types
@@ -6,7 +6,7 @@ module Interact.Types
6 , _LeftEditor, _RightEditor, _PrimitiveName 6 , _LeftEditor, _RightEditor, _PrimitiveName
7 , Validity, pattern Valid, pattern Invalid 7 , Validity, pattern Valid, pattern Invalid
8 , InteractState(..) 8 , InteractState(..)
9 , HasLeft(..), HasRight(..), HasComplement(..), HasFocus(..), HasFocused(..) 9 , HasLeft(..), HasRight(..), HasComplement(..), HasFocus(..), HasFocused(..), HasActive(..), HasLoadBrowser(..)
10 , InteractInitial(..) 10 , InteractInitial(..)
11 , _InitialLeft, _InitialRight, _InitialEmpty 11 , _InitialLeft, _InitialRight, _InitialEmpty
12 , InteractConfig(..) 12 , InteractConfig(..)
@@ -38,6 +38,7 @@ import Numeric.Natural
38import Brick 38import Brick
39import Brick.Focus 39import Brick.Focus
40import Brick.Widgets.Edit 40import Brick.Widgets.Edit
41import Brick.Widgets.FileBrowser
41 42
42import Control.Lens 43import Control.Lens
43import Control.Lens.TH 44import Control.Lens.TH
@@ -47,12 +48,29 @@ import Control.DFST.Lens
47 48
48import Data.Text.Zipper.Generic 49import Data.Text.Zipper.Generic
49 50
51import Control.DeepSeq
52import GHC.Generics (Generic)
53
54
55deriving instance Generic (StringEdit n c)
56instance (NFData n, NFData c) => NFData (StringEdit n c)
57
58deriving instance Generic (StringEdits n c)
59instance (NFData n, NFData c) => NFData (StringEdits n c)
60
61deriving instance Generic (DFSTAction s c c')
62instance (NFData s, NFData c, NFData c') => NFData (DFSTAction s c c')
63
64instance (NFData s, NFData c, NFData c') => NFData (DFSTComplement s c c') where
65 rnf = foldr deepseq ()
66
50 67
51data InteractName 68data InteractName
52 = LeftEditor 69 = LeftEditor
53 | RightEditor 70 | RightEditor
71 | LoadBrowser
54 | PrimitiveName !Text 72 | PrimitiveName !Text
55 deriving (Eq, Ord, Show, Read) 73 deriving (Eq, Ord, Show, Read, Generic)
56 74
57makePrisms ''InteractName 75makePrisms ''InteractName
58 76
@@ -64,6 +82,8 @@ data InteractState c = InteractState
64 { istLeft, istRight :: (Last Validity, Last (Seq Char, Int), StringEdits Natural Char) 82 { istLeft, istRight :: (Last Validity, Last (Seq Char, Int), StringEdits Natural Char)
65 , istComplement :: c 83 , istComplement :: c
66 , istFocus :: FocusRing InteractName 84 , istFocus :: FocusRing InteractName
85 , istActive :: Bool
86 , istLoadBrowser :: Maybe (FileBrowser InteractName)
67 } 87 }
68 88
69makeLensesWith abbreviatedFields ''InteractState 89makeLensesWith abbreviatedFields ''InteractState
diff --git a/interactive-edit-lens/src/Main.hs b/interactive-edit-lens/src/Main.hs
index 83c9725..c816515 100644
--- a/interactive-edit-lens/src/Main.hs
+++ b/interactive-edit-lens/src/Main.hs
@@ -1,5 +1,6 @@
1{-# LANGUAGE OverloadedStrings 1{-# LANGUAGE OverloadedStrings
2 , ExistentialQuantification 2 , ExistentialQuantification
3 , DeriveGeneric
3 #-} 4 #-}
4 5
5module Main where 6module Main where
@@ -30,18 +31,23 @@ import Debug.Trace
30 31
31import Data.Universe 32import Data.Universe
32 33
33data SomeDFST = forall state. (Ord state, Show state, Finite state) => SomeDFST { someDFST :: DFST state Char Char } 34import Control.DeepSeq
35import GHC.Generics (Generic)
36
37data SomeDFST = forall state. (Ord state, Show state, Finite state, NFData (DFSTComplement state Char Char)) => SomeDFST { someDFST :: DFST state Char Char }
34 38
35data JsonContext = JCInDet | JCDict | JCDictKey | JCDictVal | JCArray | JCArrayVal | JCTop 39data JsonContext = JCInDet | JCDict | JCDictKey | JCDictVal | JCArray | JCArrayVal | JCTop
36 deriving (Eq, Ord, Show, Read, Enum, Bounded) 40 deriving (Eq, Ord, Show, Read, Enum, Bounded, Generic)
37instance Universe JsonContext 41instance Universe JsonContext
38instance Finite JsonContext 42instance Finite JsonContext
39 43
44instance NFData JsonContext
45
40data JsonNewlState = JNElement JsonContext 46data JsonNewlState = JNElement JsonContext
41 | JNTrue String JsonContext | JNFalse String JsonContext | JNNull String JsonContext | JNLitEnd JsonContext 47 | JNTrue String JsonContext | JNFalse String JsonContext | JNNull String JsonContext | JNLitEnd JsonContext
42 | JNString JsonContext | JNStringEsc Int JsonContext | JNStringEnd JsonContext 48 | JNString JsonContext | JNStringEsc Int JsonContext | JNStringEnd JsonContext
43 | JNNumberDigits Bool JsonContext | JNNumberDecimal JsonContext | JNNumberDecimalDigits Bool JsonContext | JNNumberExpSign JsonContext | JNNumberExpDigits Bool JsonContext | JNNumberEnd JsonContext 49 | JNNumberDigits Bool JsonContext | JNNumberDecimal JsonContext | JNNumberDecimalDigits Bool JsonContext | JNNumberExpSign JsonContext | JNNumberExpDigits Bool JsonContext | JNNumberEnd JsonContext
44 deriving (Eq, Ord, Show, Read) 50 deriving (Eq, Ord, Show, Read, Generic)
45instance Universe JsonNewlState where 51instance Universe JsonNewlState where
46 universe = concat 52 universe = concat
47 [ JNElement <$> universeF 53 [ JNElement <$> universeF
@@ -63,6 +69,8 @@ instance Universe JsonNewlState where
63 inits' xs = inits xs \\ [""] 69 inits' xs = inits xs \\ [""]
64instance Finite JsonNewlState 70instance Finite JsonNewlState
65 71
72instance NFData JsonNewlState
73
66jsonStrEscapes :: [(Char, Seq Char)] 74jsonStrEscapes :: [(Char, Seq Char)]
67jsonStrEscapes = [ ('"', "\\\"") 75jsonStrEscapes = [ ('"', "\\\"")
68 , ('\\', "\\\\") 76 , ('\\', "\\\\")
@@ -78,10 +86,11 @@ hexDigits :: [Char]
78hexDigits = ['0'..'9'] ++ ['a'..'f'] 86hexDigits = ['0'..'9'] ++ ['a'..'f']
79 87
80data LineBreakState = LineBreak Int 88data LineBreakState = LineBreak Int
81 deriving (Eq, Ord, Show, Read) 89 deriving (Eq, Ord, Show, Read, Generic)
82instance Universe LineBreakState where 90instance Universe LineBreakState where
83 universe = [ LineBreak n | n <- [0..80] ] 91 universe = [ LineBreak n | n <- [0..80] ]
84instance Finite LineBreakState 92instance Finite LineBreakState
93instance NFData LineBreakState
85 94
86dfstMap :: String -> Maybe SomeDFST 95dfstMap :: String -> Maybe SomeDFST
87dfstMap "double" = Just . SomeDFST $ DFST 96dfstMap "double" = Just . SomeDFST $ DFST
diff --git a/intro.tex b/intro.tex
new file mode 100644
index 0000000..539a0a6
--- /dev/null
+++ b/intro.tex
@@ -0,0 +1,81 @@
1\subsubsection{Motivation}
2
3Unter einem inkrementellen Parser \cite{ghezzi1979incremental} verstehen wir ein Programm, das, nach einem initialen Parsevorgang, gegeben eine Spezifikation einer Änderung der textuellen Eingabe i.A. schneller ein neues Ergebnis erzeugt als es ohne zusätzlichen Kontext möglich wäre (gewöhnlicherweise in logarithmischer Zeit in der Länge der Eingabe).
4
5Es ist nun prinzipiell wünschenswert die algebraische Struktur derartiger Klassen von Programmen zu untersuchen, mit dem Ziel neue Parser mit generischen Mitteln aus bereits bekannten konstruieren zu können.
6
7In dieser Arbeit versuchen wir, anhand von Finite State Transducern als Spezialfall, inkrementelle Parser und die unterliegenden edits mit neuerer algebraischer Struktur, edit-lenses \cite{hofmann2012edit}, zu versehen um Komponierbarkeit zu vereinfachen.
8Vor allem versuchen wir somit zu demonstrieren, dass sich bekannte Klassen von Programmen, unter Erhalt ihrer vollen Struktur, als edit-lenses auffassen lassen, auch wenn die Darstellung als konventionelle funktionale Linse unzufriedenstellend wäre.
9
10\subsubsection{Inhalt}
11
12Wir stellen in Abschnitt \ref{edit-lenses} die Definitionen und Konstruktion von edit-lenses aus \cite{hofmann2012edit} vor und diskutieren kurz die Kompatibilität unserer Implementierung und edit-lenses im Allgemeinen mit etablierten frameworks für funktionale Linsen in Haskell.
13In Abschnitt \ref{finite-state-transducers} präsentieren wir eine etablierte Version von Finite State Transducern, für die folgenden Teile relevante Konstruktionen darauf, und einige assoziierte Beispiele.
14Abschnitt \ref{edit-lenses-fuxfcr-deterministic-finite-state-transducers} beschreibt eine Methode beliebige deterministische Finite State Transducers als edit-lenses aufzufassen und stellt somit eine non-triviale Anwendung der Methoden und Konzepte aus \cite{hofmann2012edit} dar.
15In Abschnitt \ref{ausblick-edit-lenses-fuxfcr-non-determinische-finite-state-transducers} stellen wir kurz einen Ansatz dar unsere Konstruktion aus \ref{edit-lenses-fuxfcr-deterministic-finite-state-transducers} auch auf non-deterministische Finite State Transducer zu erweitern.
16In Abschnitt \ref{implementierung} kommentieren wir den Implementierungs-Prozess der Arbeit und die Schlüsse, die wir aus der Implementierung als solche ziehen konnten.
17
18\subsection{Historischer Überblick}
19
20Bidirektionale, inkrementelle, und kombinierbare Parser und ihre Analyse sind ein vergleichsweise modernes Konzept und stützen sich in weiten Teilen auf vorhergehende Arbeit:
21
22% [x] a programmable editor
23% [x] bidirectional tree transformations
24% [x] boomerang
25% [x] combinator parser
26% [ ] ~~delta lenses & optifibrations~~
27% [x] edit languages for information trees
28% [x] edit lenses
29% [x] efficient and flexible incremental parsing
30% [x] general incremental lexical analysis
31% [ ] ~~incrementel analysis of real programming languages~~
32% [x] incremental parsing
33% [x] incremental semantic analysis
34% [x] lazy functional incremental parsing
35% [ ] ~~lenses and bidirectional programs~~
36% [ ] ~~parallel inceremntal compilation~~
37% [x] parsing in a broad sense
38% [ ] polish parsers
39% [x] symmetric lenses
40% [x] unifying lenses
41% [ ] ~~universal updates for symmetric lenses~~
42
43\begin{description} % TODO: more
44 \item[1979] \cite{ghezzi1979incremental} präsentieren, in einer der ersten Arbeiten zu dem Thema, einen Ansatz zum inkrementellen Parsen von deterministischen und Kontext-freien Sprachen basierend auf dem $LR$-Ansatz.
45 \item[1992] \cite{hedin1992incremental} präsentieren einen Formalismus zur inkrementellen \emph{semantischen} Analyse (d.h. das Versehen des Syntax-Baums eines Programms mit Attributen wie z.B. Typen) basierend auf (modifizierten) Attribut-Grammatiken.
46 \item[1997] \cite{wagner1997general} stellen einen Algorithmus zur inkrementellen lexikalischen Analyse (tokenizing) der auf den selben Spezifikationen arbeiten kann wie die UNIX-Tools \texttt{lex} und \texttt{flex}.
47 \item[1998] \cite{wagner1998efficient} stellen neue, Laufzeit- und Speicher-optimale, Methoden zur Konstruktion inkrementeller Parser auf Basis beliebiger $LR(k)$-Grammatiken vor.
48 \item[2001] \cite{swierstra2001combinator} demonstriert den Nutzen Kombinator-basierter Parser-Konstruktion in der Praxis
49 \item[2004] \cite{hu2004programmable} spezifizieren eine algebraisch strukturierte Sprache für bidirektionale Baum-Transformationen unter einer programmierbaren Konsistenzrelation mit Blick auf direkte Anwendung im Editieren von bestehenden Baum-Dokumenten
50 \item[2007] \cite{foster2007combinators} präsentieren sowohl eine Sprache bidirektionaler Baum-Transformationen als konventionelle funktionale Linsen im Speziellen, als auch mathematische Resultate für funktionale Linsen und Sammlungen davon im Allgemeinen.
51 Auch enthalten ist eine nützliche Klassifikation und ein historischer Überblick diverser bidirektionalen Programmiertechniken.
52 \item[2008] Analog zur Sprache bidirektionaler Baum-Transformation aus \cite{foster2007combinators} stellen \cite{bohannon2008boomerang} eine Sprache für semi-Strukturierten Text (als Serie von vertauschbaren Schlüssel-Wert-Assoziationen) vor.
53 \item[2009] \cite{bernardy2009lazy} implementieren, im Rahmen der Arbeit am Text-Editor Yi, eine Kombinator-basierte Programmbibliothek zum inkrementellen Parsen basierend auf lazy evaluation und aggressivem Caching in Haskell.
54 \item[2011] \cite{hofmann2011symmetric} definieren symmetrische \emph{set-based}-lenses (funktionale Linsen im konventionellen Sinn), d.h. ohne strukturierte edits.
55 Es wird auch die umfangreiche algebraische Struktur symmetrischer Linsen besprochen.
56 Vieles hiervon vererbt sich direkt auf edit-lenses als Spezialfall symmetrischer Linsen.
57 \item[2012] \cite{hofmann2012edit} definieren edit-lenses.
58 In Abgrenzung zu bestehenden Formalismen symmetrischer funktionaler Linsen arbeiten edit-lenses ausschließlich auf algebraisch strukturierten edit-Sprachen, was sie besonders attraktiv macht.
59 \item[2013] \cite{hofmann2013edit} stellen eine generelle edit-Sprache (zur Verwendung mit und basierend auf edit-lenses) für eine weite Klasse von container-Datentypen (Listen, Bäume, Graphen, ...) vor.
60 \item[2014] \cite{zaytsev2014parsing} geben einen nützlichen Überblick über die, historisch inkonsistente, Terminologie und Konzepte im Zusammenhang mit Parsing.
61 \item[2016] \cite{johnson2016unifying} betrachten Zusammenhänge von diversen Klassen funktionaler Linsen (inkl. edit-lenses) und geben dabei einen umfangreichen Überblick über die bestehende Forschung an funktionalen Linsen.
62 Ein relevantes Resultat ist hierbei ein Begriff von asymmetrischen edit-lenses kompatibel mit dem symmetrischen Fall.
63\end{description}
64
65\subsection{Begriffsverzeichnis}
66
67Obwohl wir detailliertere Definitionen der folgenden Konzepte im Laufe der Arbeit geben, ist es dennoch nützlich vorab die Bedeutung der verwendeten Begriffe kurz anzuschneiden:
68
69\begin{description}
70 \item[FST] \emph{Finite-State-Transducer} sind endliche Automaten, die bei jedem Zustandsübergang die Möglichkeit haben ein Zeichen an eine sich akkumulierende Ausgabe anzuhängen
71 \item[DFST] \emph{Deterministic finite-state-transducer} sind FSTs bei denen für jeden Zustand jedes gelesene Zeichen maximal einen Zustandsübergang zulässt
72 \item[Monoid] \emph{Monoiden} sind algebraisch zwischen Halbgruppen und Gruppen angesiedelt.
73 Wir sagen eine Menge hat Monoidstruktur bzgl. einer zweistelligen Verknüpfung auf jener Menge, wenn sie ein neutrales Element enthält und die Verknüpfung assoziativ ist.
74 \item[Moduln & edits] \emph{Moduln} verknüpfen eine Trägermenge mit einer Menge von \emph{edits} (mit monoidaler Struktur) auf jener Menge.
75 Edits beschreiben jeweils eine partielle Abbildung innerhalb der Trägermenge.
76 \item[Funktionale Linsen] Eine \emph{Funktionale Linse} von $s$ in $a$ in der üblichen Definition ist ein paar von Abbildungen $\searrow \colon s \to a$ und $\nearrow \colon (a \to a) \to (s \to s)$ mit umfangreicher algebraischer Struktur, die die Komposition komplexer Linsen aus einfacheren ermöglicht.
77 Wir finden es hilfreich von einer Projektion ($\searrow$) und einem \emph{edit-Propagator} ($\nearrow$) zu sprechen.
78 \item[Van-Laarhoven Linsen] In \cite{laarhoven} wurde eine Darstellung als eine (über einen Funktor parametrisierte) Funktion dargelegt, die unter anderem auch die soeben beschriebenen funktionalen Linsen einbetten kann
79 \item[edit-lenses] \emph{edit-lenses} verknüpfen zwei Moduln-Trägermengen indem sie edits des einen Modul in die des anderen übersetzen.
80 Hierbei wird ein, mit den jeweiligen Elementen der Trägermengen konsistenter, unterliegender Zustand, das \emph{Komplement} der edit-lens, gewahrt.
81\end{description}
diff --git a/literature/automatentheorie.bibtex b/literature/automatentheorie.bibtex
new file mode 100644
index 0000000..1b853a5
--- /dev/null
+++ b/literature/automatentheorie.bibtex
@@ -0,0 +1,6 @@
1@book{hofmann2011automatentheorie,
2 title={Automatentheorie und Logik},
3 author={Hofmann, Martin and Lange, Martin},
4 year={2011},
5 publisher={Springer-Verlag}
6}
diff --git a/literature/composition-tree.bibtex b/literature/composition-tree.bibtex
new file mode 100644
index 0000000..c9365d3
--- /dev/null
+++ b/literature/composition-tree.bibtex
@@ -0,0 +1,7 @@
1@manual{composition-tree,
2 title={Composition trees for arbitrary monoids},
3 author={Liam O'Connor},
4 month={7},
5 year={2015},
6 url={https://hackage.haskell.org/package/composition-tree}
7} \ No newline at end of file
diff --git a/presentation.deps b/presentation.deps
new file mode 100644
index 0000000..d187f80
--- /dev/null
+++ b/presentation.deps
@@ -0,0 +1,3 @@
1presentation/comptree.tex
2presentation/editconv.tex
3presentation/switchdfst.tex
diff --git a/presentation.meta.yml b/presentation.meta.yml
new file mode 100644
index 0000000..92a6f06
--- /dev/null
+++ b/presentation.meta.yml
@@ -0,0 +1,22 @@
1---
2title: Inkrementelle Parser als edit-lenses anhand von DFSTs
3abstract: |-
4 Inkrementelle Parser sind jene die bekannte Texte nach einer kleinen Änderung neu analysieren können ohne die ganze Eingabe erneut zu betrachten.
5
6 Inkrementelle Parser sind seit den 1970er-Jahren bekannt und inzwischen umfangreich erforscht.
7
8 Edit-lenses sind eine vergleichsweise neue algebraische Darstellung von Programmen, die algebraisch strukturierte Änderungen zwischen Strukturen übersetzen.
9
10 Wir demonstrieren, dass sich Inkrementelle Parser in der Sprache von edit-lenses fassen lassen, anhand einer besonders einfachen Klasse von Parsern, den deterministic finite state transducers.
11
12 Im Rahmen dessen stellen wir eine Implementierung von edit-lenses im Allgemeinen und unserem Verfahren in möglichst idiomatischem Haskell vor.
13author: Gregor Kleen
14lang: de-de
15link-citations: true
16theme: Montpellier
17colortheme: dove
18navigation: false
19toc: false
20section-titles: false
21bibliography: literature.bibtex
22...
diff --git a/presentation.tex b/presentation.tex
new file mode 100644
index 0000000..3eddd70
--- /dev/null
+++ b/presentation.tex
@@ -0,0 +1,351 @@
1\section{Einführung}
2
3\begin{frame}
4 \frametitle{Tl;dr}
5
6 \begin{itemize}
7 \item Inkrementelle Parser agieren auf \emph{edits} von Ein- und Ausgaben
8 \item Edit-Lenses sind algebraische Struktur für deartige Programme
9 \item DFSTs sind spezielle Parser, schwach genug um immer auch inkrementell zu sein
10 \item Darstellung von DFSTs als edit-lenses als Proof of Concept
11 \end{itemize}
12\end{frame}
13
14\begin{frame}
15 \frametitle{Struktur}
16 \begin{enumerate}
17 \item Begriffe/Definitionen
18 \begin{itemize}
19 \item Parser, Inkrementelle Parser
20 \item Funktionale Linsen, edit-lenses
21 \end{itemize}
22 \item Motivation
23 \item Inhalt der Arbeit
24 \begin{itemize}
25 \item Inkrementelle Parser als edit-lenses für DFSTs
26 \end{itemize}
27 \item Demonstration
28 \begin{itemize}
29 \item Interaktiver Editor unter einer edit-lens
30 \end{itemize}
31 \item Skizze des Verfahrens aus der Arbeit
32 \begin{itemize}
33 \item Komplement-Konstruktion für DFSTs
34 \item $\Rrightarrow$ und $\Lleftarrow$
35 \end{itemize}
36 \item Weiterführendes
37 \end{enumerate}
38\end{frame}
39
40\begin{frame}
41 \frametitle{Inkrementelle Parser}
42
43 \begin{defn}[Parser]
44 Jedes Programm vom Typ $\Sigma^\star \to a$
45 \note[item]{Programme, die Strings analysieren und eine Struktur produzieren}
46 \end{defn}
47
48 \begin{defn}[Inkrementelle Parser]
49 Vermeiden komplette Re-analyse bekannter Eingabe-Texte
50
51 Für unsere Zwecke\footnote{Mit $\delta(x)$ immer einer geeigneten Sprache von edits über $x$}:
52 \[
53 \delta ( \Sigma^\star ) \to \delta ( a )
54 \]
55 \end{defn}
56\end{frame}
57
58\begin{frame}
59 \begin{defn}[Funktionale Linsen]
60 Eine Linse auf ein $a$ \emph{innerhalb} eines größeren $s$:
61 \begin{align*}
62 G & \colon s \to a \\
63 P & \colon (a \to a) \to (s \to s)
64 \end{align*}
65 \note[item]{Zum Verständnis: nimm $s$ als Klasse/Struct und $a$ als Attribut davon}
66 \begin{itemize}
67 \item Bidirektional
68 \item \emph{fokussiert} Teil der großen Struktur $s$
69 \item Projektion und Update-Propagator
70 \item $P$ und $G$ sind \emph{well-behaved}
71 \end{itemize}
72 \end{defn}
73\end{frame}
74
75\begin{frame}
76 \begin{defn}[edit-lenses]
77 \begin{align*}
78 \Rrightarrow & \colon \delta(s) \times C \to \delta(a) \times C \\
79 \Lleftarrow & \colon \delta(a) \times C \to \delta(s) \times C
80 \end{align*}
81 Mit $C$ dem \emph{Komplement}\footnote{\emph{View-Update-Problem} für DBS}, die zusätzlich zu den Edits $\delta(s)$, bzw. $\delta(a)$ notwendige Information um neues $a$ bzw. $s$ zu konstruieren
82 \begin{itemize}
83 \item Bidirektional
84 \item Edit-Propagatoren in beide Richtungen
85 \item Edits haben \emph{Algebraische Struktur}
86 \item $\Rrightarrow$ und $\Lleftarrow$ sind \emph{well-behaved}
87 \end{itemize}
88 \note[item]{$\delta(s)$ ist Speziallfall von $s \to s$}
89 \end{defn}
90\end{frame}
91
92\begin{frame}[fragile]
93
94 \frametitle{Edit-Konversationen}
95 \framesubtitle{Vereinfacht, ohne Komplement}
96
97 \begin{figure}
98 \centering
99 \pinclude{presentation/editconv.tex}
100 \end{figure}
101
102\end{frame}
103
104\begin{frame}
105 \frametitle{FSTs}
106
107 \begin{defn}[Finite state transducer]
108 Endliche Automaten mit Ausgabe-Symbolen an Zustansübergängen annotiert.
109 \note[item]{\emph{Determinismus} analog zu DFAs}
110 \end{defn}
111
112%% \begin{eg}
113%% \centering
114%% \begin{tikzpicture}[->,auto,node distance=2.5cm]
115%% \node[initial,state] (0) {$A$};
116%% \node[state,accepting] (1) [right of=0] {$B$};
117%% \node[state,initial,accepting,initial where=right] (2) [right of=1] {$C$};
118
119%% \path (0) edge [loop above] node {$(a, x)$} (0)
120%% (0) edge node {$(a, y)$} (1)
121%% (1) edge [bend left=20] node [above] {$(a, z)$} (2)
122%% (1) edge [bend right=20] node [below] {$(b, z)$} (2)
123%% (2) edge [loop above] node {$(\epsilon, z)$} (2);
124%% \end{tikzpicture}
125%% \note[item]{Beispiel ist \emph{nicht} deterministisch}
126%% \note[item]{Beispiel hat zwei initiale Zustände}
127%% \note[item]{Beispiel hat zwei akzeptierende Zustände}
128%% \note[item]{$a^{+}(a \mid b)^{?} \to x^{n}(yz^{+})^{?} \mid z^\star$}
129%% %% \begin{tikzpicture}[->,auto,node distance=2.5cm]
130%% %% \node[initial,state] (0) {$A$};
131%% %% \node[state,accepting] (1) [right of=0] {$B$};
132%% %% \node[state,accepting] (2) [right of=1] {$C$};
133
134%% %% \path (0) edge node {$(a, y)$} (1)
135%% %% (1) edge [bend left=20] node [above] {$(a, z)$} (2)
136%% %% (1) edge [bend right=20] node [below] {$(b, z)$} (2);
137%% %% \end{tikzpicture}
138%% \end{eg}
139%% \end{frame}
140
141%% \begin{frame}
142%% \frametitle{Beispiel-DFST}
143
144 \begin{figure}
145 \centering
146 \pinclude{presentation/switchdfst.tex}
147 \end{figure}
148\end{frame}
149
150\section{Motivation}
151
152\begin{frame}
153 \frametitle{Motivation}
154
155 \begin{itemize}
156 \item edit-lenses (und unterliegende edits) haben umfangreiche algebraische Struktur
157 \item Inkrementelle Parser haben praktische Vorteile, wo anwendbar
158 \item Darstellung von inkrementellen Parsern als edit-lenses erlaubt Kompositions-basierte Konstruktion von Parsern
159 \end{itemize}
160
161 \begin{eg}
162 \begin{itemize}
163 \item Interaktive Programmierumgebung kann \emph{sofort} Feedback geben (Semantisches autocomplete, syntax highlighting, ...)
164 \item Grafische Konfigurations-Ansichten für unterliegende Konfigurationsdateien können Formatierung (z.B. Kommentare) erhalten
165 \end{itemize}
166 \end{eg}
167\end{frame}
168
169\section{Inhalt der Arbeit}
170
171\begin{frame}
172 \frametitle{Inhalt}
173
174 \begin{itemize}
175 \item edits, edit-lenses, und FSTs in Haskell
176 \item Verfahren zum automatischen Ableiten von edit-lenses aus DFSTs
177 \item Interaktiver editor für beliebige edit-lenses zwischen Strings
178 \end{itemize}
179\end{frame}
180
181\section{Demonstration}
182
183\begin{frame}
184 \frametitle{JSON-Normalisierer}
185 \framesubtitle{Demonstration}
186
187 \begin{itemize}
188 \item JSON-Normalisierung ausgedrückt als DFST
189 \item edit-lens aus DFST abgeleitet
190 \item Interaktiver editor akzeptiert edits auf einer Seite und propagiert in Gegenrichtung
191 \end{itemize}
192\end{frame}
193
194\section{Edit-lenses für DFSTs}
195
196\begin{frame}
197 \frametitle{Ansatz}
198
199 Als \emph{Komplement} genug Information um für jedes Intervall im Eingabe-String berechnen zu können:
200
201 \begin{itemize}
202 \item Gegeben einen Zustand auf der linken Seite des Intervalls, welche Ausgabe wird produziert und welcher Zustand wird auf der rechten Seite erreicht?
203
204 \[ \text{state} \to \text{outChar}^\star \times (\text{state} \cup \{ \bot \}) \]
205
206 \emph{Ausgabe-Wirkung} des FST
207 \item Welche Eingabe wurde im Intervall konsumiert?
208 \end{itemize}
209
210 Gegeben einen edit:
211
212 \begin{enumerate}
213 \item Intervall in Ausgabe/Eingabe bestimmen, die von edit betroffen ist
214 \item Betroffenes Teilstück des Komplements austauschen
215 \item Übertragenen edit Anhand von Differenz der Komplement-Stücke bestimmen
216 \end{enumerate}
217\end{frame}
218
219\begin{frame}
220 \frametitle{Composition-Trees}
221 \framesubtitle{Effiziente Berechnung von Wirkungen beliebiger Eingabe-Intervalle}
222
223 \begin{columns}[c]
224 \column{.5\textwidth}
225 \begin{center}
226 \scalebox{1}{\pinclude{presentation/switchdfst.tex}}
227 \end{center}
228 \column{.5\textwidth}
229 \begin{center}
230 \scalebox{0.65}{\pinclude{presentation/comptree.tex}}
231 \end{center}
232 \end{columns}
233\end{frame}
234
235\begin{frame}
236 \frametitle{$\Rrightarrow$}
237
238 \begin{align*}
239 \Rrightarrow & \colon \delta ( \text{inChar}^\star ) \times C \to \delta ( \text{outChar}^\star ) \times C \\
240 C & \colon \left ( \text{outChar}^\star \times (\text{state} \cup \{ \bot \}), \text{inChar}^\star \right )
241 \end{align*}
242
243 \begin{enumerate}
244 \item Bestimme Intervall in $\text{inChar}^\star$ betroffen von edit und asoziiertes Stück $c \subseteq C$
245 \item Lese in $C$ betroffenes Intervall in $\text{outChar}^\star$ ab
246 \item Berechne neues Stück $c^\prime$ durch Auswertung des DFST
247 \item Bestimme $\delta (\text{outChar}^\star)$ mit Standard-Diff auf $\text{inChar}^\star$-Komponenten von $c$ und $c^\prime$
248 \item Ersetze $c$ in $C$ mit $c^\prime$
249 \end{enumerate}
250\end{frame}
251
252\begin{frame}
253 \frametitle{$\Rrightarrow$}
254 \framesubtitle{Beispiel}
255
256 \begin{columns}[c]
257 \column{.33\textwidth}
258 \begin{enumerate}
259 \item Intervall im Eingabetext
260 \item Ausgabe-Stück aus Komplement
261 \item Neues Komplement-Stück durch Auswertung
262 \item Komplement-Stück ersetzen
263 \item Ausgabe-Differenz aus Komplement-Stücken
264 \end{enumerate}
265 \column{.33\textwidth}
266 \begin{center}
267 \scalebox{1}{\pinclude{presentation/switchdfst.tex}}
268 \end{center}
269 \column{.33\textwidth}
270 \begin{center}
271 \scalebox{0.6}{\pinclude{presentation/comptree.tex}}
272 \end{center}
273 \end{columns}
274\end{frame}
275
276\begin{frame}
277 \frametitle{$\Lleftarrow$}
278
279 \begin{align*}
280 \Lleftarrow & \colon \delta ( \text{outChar}^\star ) \times C \to \delta ( \text{inChar}^\star ) \times C \\
281 C & \colon \left ( \text{outChar}^\star \times (\text{state} \cup \{ \bot \}), \text{inChar}^\star \right )
282 \end{align*}
283
284 \begin{enumerate}
285 \item Bestimme Intervall in $\text{outChar}^\star$ betroffen von edit und asoziiertes Stück $c \subseteq C$
286 \item Bestimme neue Ausgabe durch Anwenden von $\delta ( \text{outChar}^\star )$
287 \item Finde, durch Breitensuche, Lauf in DFST mit passender Ausgabe und selben Grenzen wie $c$
288 \item Lese $c^\prime$ aus neuem Lauf ab
289 \item Bestimme $\delta ( \text{inChar}^\star )$ mit Standard-Diff
290 \item Ersetze $c$ in $C$ mit $c^\prime$
291 \end{enumerate}
292\end{frame}
293
294\begin{frame}
295 \frametitle{$\Lleftarrow$}
296 \framesubtitle{Beispiel}
297
298 \begin{columns}[c]
299 \column{.33\textwidth}
300 \begin{enumerate}
301 \item Intervall im Ausgabetext
302 \item Neue Ausgabe für Intervall
303 \item Breitensuche nach neuem Lauf-Stück
304 \item Neues Komplement-Stück
305 \item Komplement-Stück ersetzen
306 \item Eingabe-Differenz aus Komplement-Stücken
307 \end{enumerate}
308 \column{.33\textwidth}
309 \begin{center}
310 \scalebox{1}{\pinclude{presentation/switchdfst.tex}}
311 \end{center}
312 \column{.33\textwidth}
313 \begin{center}
314 \scalebox{0.6}{\pinclude{presentation/comptree.tex}}
315 \end{center}
316 \end{columns}
317\end{frame}
318
319\section{Resultate}
320
321\begin{frame}
322 \frametitle{Ergebnisse}
323
324 \begin{itemize}
325 \item Verfahren zum automatischen Ableiten von inkrementellen Parsern zu DFSTs
326 \item Inkl. Darstellung als edit-lens
327 \item Interaktive Demonstration von edit-lenses
328 \end{itemize}
329\end{frame}
330
331\begin{frame}
332 \frametitle{Implementierung}
333 \begin{itemize}
334 \item Diverse erfolglose Ansätze zur Implementierung von $\Lleftarrow$
335 \item Erfolgreiche Implementierung dann mit algebraischen FST-Transformationen und als Komposition kleiner Typ-gesteuerter und generischer Teile
336 \note[item]{Demonstriert Erfolg von algebraischer Programmierung: nicht optimale, aber ähnliche, Komplexitätsklasse und dafür leichter verständlich}
337 \item Demonstriert Kodierung von algorithmischen Voraussetzungen in Typen (z.B. Determinismus von FST)
338 \note[item]{Korrekte Kodierung in Typen erlaubt auslassen von wenig interessanten Spezialfällen}
339 \end{itemize}
340\end{frame}
341
342\begin{frame}
343 \frametitle{Weiterführendes}
344 \begin{itemize}
345 \item Analoges Verfahren für FSTs auch möglich; $\Lleftarrow$ und $\Rrightarrow$ dann symmetrisch und analog zum DFST-Fall von $\Lleftarrow$
346 \item Edit-Lenses sind nicht kompatibel mit bestehenden Lens-Frameworks (in Haskell), da kodierung der Update-Propagatoren nicht kompatibel mit algebraischer Struktur der Edits
347 \item Linsen bilden große Familie von funktionalen, bidirektionalen Programmen z.B.
348 Imperative accessors für rein-funktionale Datenstrukturen und nützliche Verallgemeinerungen
349 \item Inkrementelle Parser und assoziierte Algorithmen (gewöhnlich basierend auf formalen Grammatiken) sind bekannt seit den 70er-Jahren; neue Darstellungen mit algebraischer Struktur fassen besser die \emph{mostly-incremental}-Struktur der meisten Programmiersprachen
350 \end{itemize}
351\end{frame}
diff --git a/presentation/comptree.tex b/presentation/comptree.tex
new file mode 100644
index 0000000..e4e6767
--- /dev/null
+++ b/presentation/comptree.tex
@@ -0,0 +1,53 @@
1\begin{tikzpicture}[auto,sibling distance=3.5cm, level distance=3.5cm]
2 \node[] (top) { \begin{tikzpicture}
3 \node [fit={(0,0) (1,1.5)}, inner sep=0pt, thick, draw, label={$\text{s}\text{p}\text{p}$}] (rect) {};
4 \path [draw](0.1,1) -- (-0.1,1) node[left]{$A$};
5 \path [draw](0.1,0.25) -- (-0.1,0.25) node[left]{$B$};
6 \path (0.75,1) node[above]{$aa$} [draw]-- (1.1,1) node[right]{$A$};
7 \path (0.75,0.25) node[above]{$bb$} [draw]-- (1.1,0.25) node[right]{$B$};
8 \path [draw](0.1,1) -- (0.60,0.25) -- (0.75,0.25);
9 \path [draw](0.1,0.25) -- (0.60,1) -- (0.75,1);
10 \end{tikzpicture}
11 }
12 child { node (l) { \begin{tikzpicture}
13 \node [fit={(0,0) (1,1.5)}, inner sep=0pt, thick, draw, label={$\text{s}\text{p}$}] (rect) {};
14 \path [draw](0.1,1) -- (-0.1,1) node[left]{$A$};
15 \path [draw](0.1,0.25) -- (-0.1,0.25) node[left]{$B$};
16 \path (0.85,1) node[above]{$a$} [draw]-- (1.1,1) node[right]{$A$};
17 \path (0.85,0.25) node[above]{$b$} [draw]-- (1.1,0.25) node[right]{$B$};
18 \path [draw](0.1,1) -- (0.75,0.25) -- (0.85,0.25);
19 \path [draw](0.1,0.25) -- (0.75,1) -- (0.85,1);
20 \end{tikzpicture}
21 }
22 child { node (ll) { \begin{tikzpicture}
23 \node [fit={(0,0) (1,1.5)}, inner sep=0pt, thick, draw, label={$\text{s}$}] (rect) {};
24 \path [draw](0.1,1) -- (-0.1,1) node[left]{$A$};
25 \path [draw](0.1,0.25) -- (-0.1,0.25) node[left]{$B$};
26 \path (0.85,1) node[above]{$\epsilon$} [draw]-- (1.1,1) node[right]{$A$};
27 \path (0.85,0.25) node[above]{$\epsilon$} [draw]-- (1.1,0.25) node[right]{$B$};
28 \path [draw](0.1,1) -- (0.75,0.25) -- (0.85,0.25);
29 \path [draw](0.1,0.25) -- (0.75,1) -- (0.85,1);
30 \end{tikzpicture}
31 } }
32 child { node (lr) { \begin{tikzpicture}
33 \node [fit={(0,0) (1,1.5)}, inner sep=0pt, thick, draw, label={$\text{p}$}] (rect) {};
34 \path [draw](0.1,1) -- (-0.1,1) node[left]{$A$};
35 \path [draw](0.1,0.25) -- (-0.1,0.25) node[left]{$B$};
36 \path (0.85,1) node[above]{$a$} [draw]-- (1.1,1) node[right]{$A$};
37 \path (0.85,0.25) node[above]{$b$} [draw]-- (1.1,0.25) node[right]{$B$};
38 \path [draw](0.1,0.25) -- (0.75,0.25) -- (0.85,0.25);
39 \path [draw](0.1,1) -- (0.75,1) -- (0.85,1);
40 \end{tikzpicture}
41 } }
42 }
43 child { node (r) { \begin{tikzpicture}
44 \node [fit={(0,0) (1,1.5)}, inner sep=0pt, thick, draw, label={$\text{p}$}] (rect) {};
45 \path [draw](0.1,1) -- (-0.1,1) node[left]{$A$};
46 \path [draw](0.1,0.25) -- (-0.1,0.25) node[left]{$B$};
47 \path (0.85,1) node[above]{$a$} [draw]-- (1.1,1) node[right]{$A$};
48 \path (0.85,0.25) node[above]{$b$} [draw]-- (1.1,0.25) node[right]{$B$};
49 \path [draw](0.1,0.25) -- (0.75,0.25) -- (0.85,0.25);
50 \path [draw](0.1,1) -- (0.75,1) -- (0.85,1);
51 \end{tikzpicture}
52 } };
53\end{tikzpicture}
diff --git a/presentation/editconv.tex b/presentation/editconv.tex
new file mode 100644
index 0000000..26dbcc7
--- /dev/null
+++ b/presentation/editconv.tex
@@ -0,0 +1,62 @@
1\begin{tikzpicture}[node distance=2cm and 2cm,auto]
2 \tikzset{myptr/.style={decoration={markings,mark=at position 1 with %
3 {\arrow[scale=3,>=stealth]{>}}},postaction={decorate}}}
4
5 \coordinate[] (e1) {};
6
7 \node[shape=rectangle, draw, left = of e1] (l1)
8 { \begin{tabular}{l l}
9 Schubert & 1797–1828 \\
10 Shumann & 1810–1856
11 \end{tabular}
12 };
13
14 \node[shape=rectangle, draw, right = of e1] (r1)
15 { \begin{tabular}{l l}
16 Schubert & Austria \\
17 Shumann & Germany
18 \end{tabular}
19 };
20
21 \draw (l1) -- (e1) -- (r1);
22
23 \coordinate[below = of e1,label={$\iota_L \rightarrow \iota_R$}] (e2) {};
24
25 \node[shape=rectangle, draw, left = of e2] (l2)
26 { \begin{tabular}{l l}
27 Schubert & 1797–1828 \\
28 Shumann & 1810–1856 \\
29 \textcolor{blue}{Monteverdi} & \textcolor{blue}{1567–1643}
30 \end{tabular}
31 };
32
33 \node[shape=rectangle, draw, right = of e2] (r2)
34 { \begin{tabular}{l l}
35 Schubert & Austria \\
36 Shumann & Germany \\
37 \textcolor{red}{Monteverdi} & \textcolor{red}{\emph{null}}
38 \end{tabular}
39 };
40
41 \draw[myptr] (l2) -- (e2) |- (r2);
42
43 \coordinate[below = of e2,label={$\delta_R \leftarrow \delta_L$}] (e3) {};
44
45 \node[shape=rectangle, draw, left = of e3] (l3)
46 { \begin{tabular}{l l}
47 Schubert & 1797–1828 \\
48 \textcolor{red}{Schumann} & 1810–1856 \\
49 Monteverdi & 1567–1643
50 \end{tabular}
51 };
52
53 \node[shape=rectangle, draw, right = of e3] (r3)
54 { \begin{tabular}{l l}
55 Schubert & Austria \\
56 \textcolor{blue}{Schumann} & Germany \\
57 Monteverdi & \textcolor{blue}{Italy}
58 \end{tabular}
59 };
60
61 \draw[myptr] (r3) -- (e3) |- (l3);
62\end{tikzpicture}
diff --git a/presentation/switchdfst.tex b/presentation/switchdfst.tex
new file mode 100644
index 0000000..f27491c
--- /dev/null
+++ b/presentation/switchdfst.tex
@@ -0,0 +1,8 @@
1\begin{tikzpicture}[->,auto,node distance=2.5cm]
2 \node[initial,state,accepting] (a) {$A$};
3 \node[state,accepting] (b) [right of=a] {$B$};
4 \path (a) edge [bend left=20] node [above] {$(\text{s}, \epsilon)$} (b)
5 (b) edge [bend left=20] node [below] {$(\text{s}, \epsilon)$} (a)
6 (a) edge [loop above] node {$(\text{p}, a)$} (a)
7 (b) edge [loop above] node {$(\text{p}, b)$} (b);
8\end{tikzpicture}
diff --git a/stack.yaml b/stack.yaml
index 821983d..7ac94ae 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -16,3 +16,5 @@ build:
16 16
17extra-deps: 17extra-deps:
18 - dotgen-0.4.2 18 - dotgen-0.4.2
19 - brick-0.47
20 - vty-5.25.1
diff --git a/thesis.args b/thesis.args
new file mode 100644
index 0000000..bf836dc
--- /dev/null
+++ b/thesis.args
@@ -0,0 +1 @@
--table-of-contents \ No newline at end of file
diff --git a/thesis.deps b/thesis.deps
new file mode 100644
index 0000000..b1cfe6a
--- /dev/null
+++ b/thesis.deps
@@ -0,0 +1,3 @@
1presentation/switchdfst.tex
2presentation/comptree.tex
3screenshot.png \ No newline at end of file
diff --git a/thesis.meta.yml.gup b/thesis.meta.yml.gup
index 0ef84d6..27ce8cb 100644
--- a/thesis.meta.yml.gup
+++ b/thesis.meta.yml.gup
@@ -2,13 +2,26 @@
2 2
3gup -u literature.bibtex 3gup -u literature.bibtex
4 4
5cat >$1 <<EOF 5cat >$1 <<'EOF'
6--- 6---
7title: Inkrementelle Parser als edit-lenses anhand von DFSTs
8abstract: |-
9 Parser, die bekannte Texte nach einer kleinen Änderung neu analysieren können, ohne die ganze Eingabe erneut zu betrachten, nennt man inkrementell.
10
11 Inkrementelle Parser sind seit den 1970er-Jahren bekannt und inzwischen umfangreich erforscht.
12
13 Edit-lenses sind eine vergleichsweise neue algebraische Darstellung von Programmen, die algebraisch strukturierte Änderungen zwischen Strukturen übersetzen.
14
15 Wir demonstrieren, dass sich Inkrementelle Parser in der Sprache von edit-lenses fassen lassen, anhand einer besonders einfachen Klasse von Parsern, den deterministic finite state transducers.
16
17 Hierzu speichern wir im unterliegenden Zustand der assoziierten edit-lens die Ausgabe-Wirkung des DFST als balancierten Binärbaum um Teile davon effizient austauschen zu können.
18
19 Im Rahmen dessen stellen wir eine Implementierung von edit-lenses im Allgemeinen und unserem Verfahren in möglichst idiomatischem Haskell vor.
7lang: de-de 20lang: de-de
8link-citations: true 21link-citations: true
9bibliography: literature.bibtex 22bibliography: literature.bibtex
10title: Iterative Parser als edit-lenses
11author: Gregor Kleen 23author: Gregor Kleen
12date: \today 24date: \formatdate{01}{03}{2019}
25numbersections: true
13... 26...
14EOF 27EOF
diff --git a/thesis.pdf.gup b/thesis.pdf.gup
index 6e2fa65..bb611f4 100755
--- a/thesis.pdf.gup
+++ b/thesis.pdf.gup
@@ -1,10 +1,14 @@
1#!/usr/bin/env zsh 1#!/usr/bin/env zsh
2 2
3gup -u intro.tex
4gup -u implementation.tex
5
3gup -u edit-lens/src/Control/Edit.lhs 6gup -u edit-lens/src/Control/Edit.lhs
4gup -u edit-lens/src/Control/Lens/Edit.lhs 7gup -u edit-lens/src/Control/Lens/Edit.lhs
5gup -u edit-lens/src/Control/FST.lhs 8gup -u edit-lens/src/Control/FST.lhs
6gup -u edit-lens/src/Control/DFST.lhs 9gup -u edit-lens/src/Control/DFST.lhs
7gup -u edit-lens/src/Control/DFST/Lens.lhs 10gup -u edit-lens/src/Control/DFST/Lens.lhs
11gup -u edit-lens/src/Control/FST/Lens.tex
8 12
9bDir=$(pwd) 13bDir=$(pwd)
10 14
diff --git a/thesis.tex b/thesis.tex
index 4156751..2f0346b 100644
--- a/thesis.tex
+++ b/thesis.tex
@@ -1,18 +1,52 @@
1\vfill
2
3\noindent Ich erkläre hiermit, dass ich die vorliegende Arbeit
4selbstständig angefertigt, alle Zitate als solche kenntlich gemacht
5sowie alle benutzten Quellen und Hilfsmittel angegeben habe.
6
7\bigskip
8
9\makebox[.5\linewidth][r]{}{\xleaders\hbox to .2em{\d{}}\hfill\d{}}\smallskip \\
10\hspace*{.5\linewidth}Gregor Kleen \\
11\hspace*{.5\linewidth}München, \today
12
13%% \bigskip\noindent München, \today
14
15%% \vspace{4ex}\noindent\makebox[7cm]{\dotfill}
16
17
18\section{Einführung}
19\input{./intro.tex}
20
1\section{Edit-lenses} 21\section{Edit-lenses}
2 22
3Ziel ist es zunächst edit-lenses alá \cite{hofmann2012edit} in Haskell zur Verfügung zu stellen. 23Ziel ist es zunächst edit-lenses alá \cite{hofmann2012edit} in Haskell zur Verfügung zu stellen.
4Dabei werden wir die Definitionen aus \cite{hofmann2012edit} sowohl in natürlicher Sprache als auch in lauffähigem Haskell vorstellen: 24Dabei werden wir die Definitionen aus \cite{hofmann2012edit} sowohl in natürlicher Sprache als auch in lauffähigem Haskell vorstellen.
5 25
6\input{./edit-lens/src/Control/Edit.lhs} 26\input{./edit-lens/src/Control/Edit.lhs.tex}
7\input{./edit-lens/src/Control/Lens/Edit.lhs} 27\input{./edit-lens/src/Control/Lens/Edit.lhs.tex}
8 28
9\section{Finite state transducers} 29\section{Finite state transducers}
10 30
11\input{./edit-lens/src/Control/FST.lhs} 31\input{./edit-lens/src/Control/FST.lhs.tex}
12\input{./edit-lens/src/Control/DFST.lhs} 32\input{./edit-lens/src/Control/DFST.lhs.tex}
13 33
14\subsection{Edit-lenses für deterministic finite state transducers} 34\subsection{Edit-lenses für deterministic finite state transducers}
15\input{./edit-lens/src/Control/DFST/Lens.lhs} 35
36\input{./edit-lens/src/Control/Edit/String.lhs.tex}
37\input{./edit-lens/src/Control/DFST/Lens.lhs.tex}
38\input{./edit-lens/src/Control/Edit/String/Affected.lhs.tex}
16 39
17\subsection{Ausblick: Edit-lenses für non-determinische finite state transducers} 40\subsection{Ausblick: Edit-lenses für non-determinische finite state transducers}
41
18\input{./edit-lens/src/Control/FST/Lens.tex} 42\input{./edit-lens/src/Control/FST/Lens.tex}
43
44\section{Resultate}
45
46\subsection{Implementierung}
47
48\input{./implementation.tex}
49
50\subsection{Ausblick: Anwendbarkeit der Implementierung auf andere Parser}
51
52\input{./edit-lens/src/Control/Lens/Edit/ActionTree.lhs.tex}