From c37395089c3a5dfc32406685ac5b0102050a8aa1 Mon Sep 17 00:00:00 2001 From: Gregor Kleen Date: Mon, 7 May 2018 10:35:14 +0200 Subject: Describe algorithm for `propR` of DFST-lens --- edit-lens/src/Data/String/DFST/Lens.lhs | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'edit-lens/src/Data/String') diff --git a/edit-lens/src/Data/String/DFST/Lens.lhs b/edit-lens/src/Data/String/DFST/Lens.lhs index e4d9083..51ce970 100644 --- a/edit-lens/src/Data/String/DFST/Lens.lhs +++ b/edit-lens/src/Data/String/DFST/Lens.lhs @@ -63,6 +63,24 @@ instance Module StringEdits where go (_, []) = Nothing go (n, (c:cs)) = Just ((succ n, cs), Insert n c) +\end{code} + +% TODO Make notation mathy + +Um zunächst eine asymmetrische edit-lens `StringEdits -> StringEdits` mit akzeptabler Komplexität für einen bestimmten `DFST s` (entlang der \emph{Richtung} des DFSTs) zu konstruieren möchten wir folgendes Verfahren anwenden: + +Gegeben eine Sequenz (`StringEdits`) von zu übersetzenden Änderungen genügt es die Übersetzung eines einzelnen `StringEdit`s in eine womöglich längere Sequenz von `StringEdits` anzugeben, alle `StringEdits` aus der Sequenz zu übersetzen (hierbei muss auf die korrekte Handhabung des Komplements geachtet werden) und jene Übersetzungen dann zu concatenieren. + +Wir definieren zunächst die \emph{Wirkung} eines DFST auf einen festen String als eine Abbildung `state -> (state, String)`, die den aktuellen Zustand vorm Parsen des Strings auf den Zustand danach und die (womöglich leere) Ausgabe schickt. +Diese Wirkungen bilden einen Monoiden analog zu Endomorphismen, wobei die Resultat-Strings concateniert werden. + +Die Unterliegende Idee ist nun im Komplement der edit-lens eine Liste von Wirkungen (eine für jedes Zeichen der Eingabe des DFSTs) und einen Cache aller möglichen monoidalen Summen von zusammenhängenden Teilstücke zu halten. +Da wir wissen welche Stelle im input-String von einem gegebenen edit betroffen ist können wir, anhand der Wirkung des Teilstücks bis zu jener Stelle, den output-String in einen durch den edit unveränderten Prefix und einen womöglich betroffenen Suffix unterteilen. +Die Wirkung ab der betroffenen Stelle im input-String können wir also Komposition der Wirkung der durch den edit betroffenen Stelle und derer aller Zeichen danach bestimmen. +Nun gilt es nur noch die Differenz (als `StringEdits`) des vorherigen Suffixes im output-String und des aus der gerade berechneten Wirkung Bestimmten zu bestimmen. + +\begin{code} + data DFSTAction state = DFSTBranch (Map state (state, String)) (DFSTAction state) (DFSTAction state) | DFSTLeaf -- cgit v1.2.3