summaryrefslogtreecommitdiff
path: root/edit-lens/src/Control/DFST/Lens.lhs
diff options
context:
space:
mode:
authorGregor Kleen <gkleen@yggdrasil.li>2019-06-07 09:08:42 +0200
committerGregor Kleen <gkleen@yggdrasil.li>2019-06-07 09:08:42 +0200
commita29cce747f3717e32231c9a92b40be12832037b6 (patch)
tree70f399682dec8657719eae4358e87cdc24bbf42f /edit-lens/src/Control/DFST/Lens.lhs
parent9a02751c1e588a5bbb83bb7e543c26486d3079d5 (diff)
downloadincremental-dfsts-a29cce747f3717e32231c9a92b40be12832037b6.tar
incremental-dfsts-a29cce747f3717e32231c9a92b40be12832037b6.tar.gz
incremental-dfsts-a29cce747f3717e32231c9a92b40be12832037b6.tar.bz2
incremental-dfsts-a29cce747f3717e32231c9a92b40be12832037b6.tar.xz
incremental-dfsts-a29cce747f3717e32231c9a92b40be12832037b6.zip
Finish for submission
Diffstat (limited to 'edit-lens/src/Control/DFST/Lens.lhs')
-rw-r--r--edit-lens/src/Control/DFST/Lens.lhs25
1 files changed, 13 insertions, 12 deletions
diff --git a/edit-lens/src/Control/DFST/Lens.lhs b/edit-lens/src/Control/DFST/Lens.lhs
index 56f37a0..04dade5 100644
--- a/edit-lens/src/Control/DFST/Lens.lhs
+++ b/edit-lens/src/Control/DFST/Lens.lhs
@@ -68,7 +68,7 @@ import Data.Universe (Finite(..))
68\begin{defn}[Ausgabe-Wirkung von DFSTs] 68\begin{defn}[Ausgabe-Wirkung von DFSTs]
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 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.
70Wir annotieren Wirkungen zudem mit dem konsumierten String. 70Wir annotieren Wirkungen zudem mit dem konsumierten String.
71Diese 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 konkateniert werden.
72 72
73\begin{code} 73\begin{code}
74data DFSTAction state input output = DFSTAction 74data DFSTAction state input output = DFSTAction
@@ -132,13 +132,13 @@ Wir bedienen uns hierbei einer bestehenden Programmbibliothek \cite{composition-
132 \begin{figure}[H] 132 \begin{figure}[H]
133 \centering 133 \centering
134 \pinclude{presentation/switchdfst.tex} 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} 135 \caption{\label{fig:switchdfst} Ein einfacher DFST, der zwischen zwei Zuständen wechselt und Ausgabe abhängig vom aktuellen Zustand erzeugt}
136 \end{figure} 136 \end{figure}
137 137
138 Auf $s$ wechselt der DFST seinen Zustand, auf $p$ produziert er, abhängig vom aktuellen Zustand, genau ein Zeichen. 138 Auf $s$ wechselt der DFST seinen Zustand, auf $p$ produziert er, abhängig vom aktuellen Zustand, genau ein Zeichen.
139 139
140 Wir stellen die Wirkung des DFST auf den Eingabe-String $spp$ grafisch analog zur Baumstruktur von \texttt{Compositions} dar. 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 transducers an den Pfaden innerhalb der Schaltbox annotieren. 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 transducers an den Pfaden innerhalb der Schaltbox annotieren.
142 142
143 \begin{figure}[H] 143 \begin{figure}[H]
144 \centering 144 \centering
@@ -160,22 +160,23 @@ dfstaProduces = fmap fst . runDFSTAction'
160\end{code} 160\end{code}
161\end{comment} 161\end{comment}
162 162
163Für $\Rrightarrow$ können wir die alte DFST-Wirkung zunächst anhand des Intervalls in dem 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, in dem der input-String von allen gegebenen edits betroffen ist (\texttt{affected}), in einen unveränderten Prefix und einen womöglich betroffenen Suffix unterteilen.
164 164
165Da wir wissen welche Stelle im input-String vom ersten gegebenen edit betroffen ist können wir, anhand der Wirkung des Teilstücks bis zu jener Stelle, den betroffenen Suffix wiederum teilen. 165Da wir wissen welche Stelle im input-String vom ersten gegebenen edit betroffen ist, können wir, anhand der Wirkung des Teilstücks bis zu jener Stelle, den betroffenen Suffix wiederum teilen.
166Die Wirkung ab der betroffenen Stelle im input-String können wir als Komposition der Wirkung der durch den edit betroffenen Stelle und derer aller Zeichen danach bestimmen. 166Die Wirkung ab der betroffenen Stelle im input-String können wir als Komposition der Wirkung der durch den edit betroffenen Stelle und derer aller Zeichen danach bestimmen.
167Nun gilt es nur noch die Differenz (als `StringEdits`) des vorherigen Suffixes im output-String und des aus der gerade berechneten Wirkung zu bestimmen, wir bedienen uns hierzu dem Unix Standard-Diff-Algorithmus zwischen der ursprünglichen Ausgabe und dem Ergebnis der Iteration des Verfahrens auf alle gegebenen edits. 167Nun gilt es nur noch die Differenz (als `StringEdits`) des vorherigen Suffixes im output-String und des aus der gerade berechneten Wirkung zu bestimmen.
168Wir bedienen uns hierzu dem Unix Standard-Diff-Algorithmus zwischen der ursprünglichen Ausgabe und dem Ergebnis der Iteration des Verfahrens auf alle gegebenen edits.
168 169
169Für die asymmetrische edit-lens entgegen der DFST-Richtung $\Lleftarrow$ verwenden wir Breitensuche über die Zustände des DFST innerhalb des von allen gegeben edits betroffenen Intervalls: 170Für die asymmetrische edit-lens entgegen der DFST-Richtung $\Lleftarrow$ verwenden wir Breitensuche über die Zustände des DFST innerhalb des von allen gegeben edits betroffenen Intervalls:
170 171
171Wir unterteilen zunächst das Komplement an den Grenzen des betroffenen Intervalls im output-String in drei Teile (durch Akkumulation der Elemente des Komplements bis die gewünschte Länge erreicht ist). 172Wir unterteilen zunächst das Komplement an den Grenzen des betroffenen Intervalls im output-String in drei Teile durch Akkumulation der Elemente des Komplements bis die gewünschte Länge erreicht ist.
172 173
173Wir transformieren dann den DFST in einen FST, dessen Ausgabe wir mit \texttt{restrictOutput} auf das gewünschte Fragment einschränken, setzen als initialen Zustand des FST den Zustand am linken Rand des von den edits betroffenen Intervalls und akzeptieren jene Zustände, von denen aus das Komplement-Fragment ab dem rechten Rand des betroffenen Intervalls zu einem im ursprünglichen DFST akzeptierenden Zustand führt. 174Wir transformieren dann den DFST in einen FST, dessen Ausgabe wir mit \texttt{restrictOutput} auf das gewünschte Fragment einschränken, setzen als initialen Zustand des FST den Zustand am linken Rand des von den edits betroffenen Intervalls und akzeptieren jene Zustände, von denen aus das Komplement-Fragment ab dem rechten Rand des betroffenen Intervalls zu einem im ursprünglichen DFST akzeptierenden Zustand führt.
174 175
175Wir verwenden dann gewöhnliche Breitensuche über die Zustände und Transitionen des soeben konstruierten FSTs um einen Lauffragment zu bestimmen, dass wir in das betroffene Intervall einsetzen können. 176Wir verwenden dann gewöhnliche Breitensuche über die Zustände und Transitionen des soeben konstruierten FSTs, um einen Lauffragment zu bestimmen, das wir in das betroffene Intervall einsetzen können.
176Hierbei sind sämtliche Randbedingungen (korrekte Ausgabe, Übereinstimmung an den Intervallgrenzen) bereits in den FST kodiert sodass wir nur noch prüfen müssen, dass der gefunde Lauf in einem akzeptierenden Zustand endet. 177Hierbei sind sämtliche Randbedingungen (korrekte Ausgabe, Übereinstimmung an den Intervallgrenzen) bereits in den FST kodiert, sodass wir nur noch prüfen müssen, dass der gefundene Lauf in einem akzeptierenden Zustand endet.
177 178
178Die input-edits können nun wiederum, unter Beachtung der Verschiebung der Indices um die Länge der Eingabe vor der linken Intervallgrenze, mit dem Unix Standard-Diff-Algorithmus berechnet werden. 179Die input-edits können nun wiederum, unter Beachtung der Verschiebung der Indizes um die Länge der Eingabe vor der linken Intervallgrenze, mit dem Unix Standard-Diff-Algorithmus berechnet werden.
179 180
180\begin{comment} 181\begin{comment}
181\begin{code} 182\begin{code}
@@ -323,7 +324,7 @@ bfs outgoing predicate
323 Wie auch im ursprünglichen DFST sind alle Zustände akzeptierend. 324 Wie auch im ursprünglichen DFST sind alle Zustände akzeptierend.
324 325
325 Wir müssen nun bestimmen welche Zustände, unter $\text{act}_\text{R}$, zu einem akzeptierenden Zustand führen. 326 Wir müssen nun bestimmen welche Zustände, unter $\text{act}_\text{R}$, zu einem akzeptierenden Zustand führen.
326 Da alle Zustände akzeptieren ist hier jeder Zustand geeignet. 327 Da alle Zustände akzeptieren, ist hier jeder Zustand geeignet.
327 328
328 Wir müssen nun (vermöge Breitensuche) den kürzesten Pfad im Produkt-FST zwischen $Q_\text{L}$ und einem der Zustände finden, der unter $\text{act}_\text{R}$ zu einem akzeptierenden Zustand im ursprünglichen transducer führt. 329 Wir müssen nun (vermöge Breitensuche) den kürzesten Pfad im Produkt-FST zwischen $Q_\text{L}$ und einem der Zustände finden, der unter $\text{act}_\text{R}$ zu einem akzeptierenden Zustand im ursprünglichen transducer führt.
329 Der leere Pfad ist geeignet. 330 Der leere Pfad ist geeignet.
@@ -339,7 +340,7 @@ bfs outgoing predicate
339 \text{\tt \textbackslash n} \cdot e = \epsilon 340 \text{\tt \textbackslash n} \cdot e = \epsilon
340 \end{equation*} 341 \end{equation*}
341 Man beachte das $\text{\tt \textbackslash n}$ und $\epsilon$ hierbei die \emph{Eingaben} von $\text{act}_{e^\prime}$ bzw. $\text{act}_0$ sind. 342 Man beachte das $\text{\tt \textbackslash n}$ und $\epsilon$ hierbei die \emph{Eingaben} von $\text{act}_{e^\prime}$ bzw. $\text{act}_0$ sind.
342 Nach Behandlung der Indices ergibt sich $e = \rho_{80}$. 343 Nach Behandlung der Indizes ergibt sich $e = \rho_{80}$.
343 344
344 Als neues Komplement erhalten wir: 345 Als neues Komplement erhalten wir:
345 346