From f4c419b9ddec15bad267a4463f0720d6e28042d2 Mon Sep 17 00:00:00 2001
From: Gregor Kleen <gkleen@yggdrasil.li>
Date: Thu, 30 May 2019 12:18:08 +0200
Subject: Further work

---
 edit-lens/src/Control/Edit/String.lhs | 120 ++++++++++++++++++++++++++++++++++
 1 file changed, 120 insertions(+)
 create mode 100644 edit-lens/src/Control/Edit/String.lhs

(limited to 'edit-lens/src/Control/Edit/String.lhs')

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 @@
+\begin{comment}
+\begin{code}
+{-# LANGUAGE TemplateHaskell
+#-}
+
+module Control.Edit.String
+  ( StringEdit(..), sePos, seInsertion
+  , StringEdits(..), _StringEdits, _SEFail, stringEdits
+  , insert, delete, replace
+  ) where
+
+import Control.Lens
+import Control.Lens.TH
+
+import Control.Edit
+
+import Numeric.Natural
+
+import Data.Sequence (Seq((:<|), (:|>)))
+import qualified Data.Sequence as Seq
+
+import Data.Monoid
+\end{code}
+\end{comment}
+
+\begin{defn}[Atomare edits of strings]
+Wir 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$:
+
+\begin{code}
+data StringEdit pos char = Insert { _sePos :: pos, _seInsertion :: char }
+                         | Delete { _sePos :: pos }
+  deriving (Eq, Ord, Show, Read)
+
+-- Automatically derive van-leerhoven-lenses:
+--
+-- @sePos :: Lens' (StringEdits pos char) pos@
+-- @seInsertion :: Traversal' (StringEdits pos char) char@
+makeLenses ''StringEdit
+\end{code}
+
+Atomare edits werden, als Liste, zu edits komponiert.
+Wir führen einen speziellen edit ein, der nicht-Anwendbarkeit der edits repräsentiert:
+\begin{code}
+data StringEdits pos char = StringEdits (Seq (StringEdit pos char))
+                          | SEFail
+  deriving (Eq, Ord, Show, Read)
+
+makePrisms ''StringEdits
+
+stringEdits :: Traversal (StringEdits pos char) (StringEdits pos' char') (StringEdit pos char) (StringEdit pos' char')
+\end{code}
+\end{defn}
+
+\begin{comment}
+\begin{code}
+stringEdits = _StringEdits . traverse
+
+insert :: pos -> char -> StringEdits pos char
+insert n c = StringEdits .  Seq.singleton $ Insert n c
+
+delete :: pos -> StringEdits pos char
+delete n = StringEdits .  Seq.singleton $ Delete n
+
+replace :: Eq pos => pos -> char -> StringEdits pos char
+replace n c = insert n c <> delete n
+
+-- | Rudimentarily optimize edit composition
+instance Eq pos => Monoid (StringEdits pos char) where
+  mempty = StringEdits Seq.empty
+  SEFail `mappend` _ = SEFail
+  _ `mappend` SEFail = SEFail
+  (StringEdits Seq.Empty) `mappend` x = x
+  x `mappend` (StringEdits Seq.Empty) = x
+  (StringEdits x@(bs :|> b)) `mappend` (StringEdits y@(a :<| as))
+    | (Insert n _) <- a
+    , (Delete n') <- b
+    , n == n'
+    = StringEdits bs `mappend` StringEdits as
+    | otherwise = StringEdits $ x `mappend` y
+\end{code}
+\end{comment}
+
+Da wir ein minimales Set an atomaren edits gewählt haben, ist die Definiton der Modulnstruktur über Strings des passenden Alphabets recht einfach:
+\begin{code}
+instance Module (StringEdits Natural char) where
+  type Domain (StringEdits Natural char) = Seq char
+  apply str SEFail = Nothing
+  apply str (StringEdits Seq.Empty) = Just str
+  apply str (StringEdits (es :|> Insert n c)) = flip apply (StringEdits es) =<< go str n c
+    where
+      go str (fromIntegral -> n) c
+        | Seq.length str >= n
+        = Just $ Seq.insertAt n c str
+        | otherwise
+        = Nothing
+  apply str (StringEdits (es :|> Delete n)) = flip apply (StringEdits es) =<< go str n
+    where
+      go str (fromIntegral -> n)
+        | Seq.length str  > n
+        = Just $ Seq.deleteAt n str
+        | otherwise
+        = Nothing
+
+  init = Seq.empty
+  divInit = StringEdits . Seq.unfoldl go . (0,)
+    where
+      go (_, Seq.Empty) = Nothing
+      go (n, c :<| cs ) = Just ((succ n, cs), Insert n c)
+
+\end{code}
+
+\begin{eg}
+  Wir wenden $\iota_{80}(100) \rho_{80}$ auf das Wort $w$ aus Beispiel~\ref{eg:w100} an:
+
+  \begin{align*}
+    w^\prime & = w \cdot \iota_{80}(100) \rho_{80} \\
+             & = 0\, 1\, \ldots\, 80\, 100\, 81\, 82\, \ldots\, 98
+  \end{align*}
+\end{eg}
+
-- 
cgit v1.2.3