Further work

4 files changed, 209 insertions, 3 deletions

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
 \end{comment}
 
 \begin{defn}[Zustandsbehaftete Monoidhomomorphismen]
-Gegeben 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:
+Gegeben 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:
 
 \begin{itemize}
    \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)
 \end{defn}
 
 \begin{defn}[edit-lenses]
-Fü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:
+Fü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:
 
 \begin{itemize}
   \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
 \end{code}
 \end{defn}
 
-\paragraph{Kompatibilität mit bestehenden lens frameworks}
+\subsection{Kompatibilität mit bestehenden lens frameworks}
 
 Das einschlägige bestehende lens framework \cite{lens} konstruiert seine Linsen alá \citeauthor{laarhoven} wie folgt:
 
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 @@
+\begin{comment}
+\begin{code}
+{-# LANGUAGE ScopedTypeVariables
+           , TypeApplications
+           , TypeFamilyDependencies
+  #-}
+
+module Control.Lens.Edit.ActionTree
+  ( Action(..)
+  , treeLens
+  ) where
+
+import Control.Edit
+import Control.Edit.String
+import Control.Edit.String.Affected
+import Control.Lens.Edit
+
+import Control.Lens
+
+import Numeric.Natural
+import Numeric.Interval (Interval, (...))
+import qualified Numeric.Interval as Int
+
+import Data.Compositions (Compositions)
+import qualified Data.Compositions as Comp
+
+import Data.Algorithm.Diff (Diff, getDiff)
+import qualified Data.Algorithm.Diff as Diff
+
+import Data.Sequence (Seq((:<|), (:|>)))
+import qualified Data.Sequence as Seq
+import Data.Set (Set)
+import qualified Data.Set as Set
+
+import Data.Monoid
+import Data.Function (on)
+import Data.Foldable (toList)
+import Data.Maybe (fromMaybe)
+
+import System.IO (Handle, hPutStrLn, IOMode(AppendMode), withFile)
+import System.IO.Unsafe
+\end{code}
+\end{comment}
+
+Das beschrieben Verfahren wurde prinzipiell agnostisch in Bezug auf die konkret gewählte Parser-Konstruktion gewählt.
+
+Hierfür wurden die benötigten Operationen auf der DFST-Wirkung und das in $\Lleftarrow$ verwendete Suchschema abstrakt als Typklasse angegeben:
+
+\begin{code}
+class Monoid action => Action action input output | action -> input, action -> output where
+\end{code}
+\begin{comment}
+\begin{code}
+  -- | Most operations of `Action` permit access to some underlying description of the parser (i.e. an automaton)
+  type ActionParam action = param | param -> action
+
+  -- | A full capture of the Parser-State (i.e. a state for a given automaton)
+  type ActionState action :: *
+
+  -- | `mempty` should be neutral under `(<>)`, `actionFail` should be absorptive
+  actionFail :: action
+
+  -- | Construct an @action@ from a single character of input
+  actionSingleInput :: ActionParam action -> input -> action
+  -- | Initial state of the parser
+  actionGroundState :: ActionParam action -> ActionState action
+  -- | Is a certain state acceptable as final?
+  actionStateFinal :: ActionParam action -> ActionState action -> Bool
+  -- | Run an @action@ (actually a binary tree thereof, use `Comp.composed` to extract the root) on a given state
+  actionState :: ActionParam action -> Compositions action -> ActionState action -> Maybe (ActionState action)
+  -- | What @output@ does running an @action@ on a given state produce?
+  actionProduces :: ActionParam action -> Compositions action -> ActionState action -> Seq output
+  -- | What @input@ does running an @action@ on a given state consume?
+  actionConsumes :: ActionParam action -> Compositions action -> Seq input
+
+  -- | Find a new string of @input@-symbols to travel between the given states while producing exactly the given @output@
+  --
+  -- @actionFindPath@ also has access to the remaining action to be run after it's new @input@ has been consumed.
+  -- 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`.
+  actionFindPath :: ActionParam action
+                 -> ActionState action -- ^ From
+                 -> Seq output -- ^ New output to be produced
+                 -> ActionState action -- ^ To
+                 -> Compositions action -- ^ Suffix
+                 -> Maybe (Seq input)
+\end{code}
+\end{comment}
+
+Das Verfahren kann nun auf andere Sorten von Parser angewendet werden, indem nur die oben aufgeführte \texttt{Action}-Typklasse implementiert wird:
+
+\begin{code}
+treeLens :: forall action input output.
+            ( Ord input, Ord output
+            , Show input, Show output
+            , Action action input output
+            , Show (ActionState action)
+            ) => ActionParam action -> EditLens (Compositions action) (StringEdits Natural input) (StringEdits Natural output)
+\end{code}
+\begin{comment}
+\begin{code}
+treeLens param = EditLens ground propR propL
+  where
+    ground :: Compositions action
+    ground = mempty
+
+    propR :: (Compositions action, StringEdits Natural input)
+          -> (Compositions action, StringEdits Natural output)
+    propR (c, SEFail) = (c, SEFail)
+    propR (c, StringEdits Seq.Empty) = (c, mempty)
+    propR (c, lEs@(StringEdits (es :> e)))
+      | Just final <- actionState param c' $ actionGroundState @action param
+      , actionStateFinal param final
+      = (c', rEs)
+      | otherwise
+      = (c, SEFail)
+      where
+        Just int = affected lEs
+        (cAffSuffix, cAffPrefix) = Comp.splitAt (Comp.length c - fromIntegral (Int.inf int)) c
+        (cSuffix, cPrefix) = Comp.splitAt (Comp.length c - (e ^. sePos . from enum)) c
+        cSuffix'
+          | Delete _       <- e
+          , Comp.length cSuffix > 0 = Comp.take (pred $ Comp.length cSuffix) cSuffix
+          | Insert _ nChar <- e = cSuffix <> Comp.singleton (actionSingleInput param nChar)
+          | otherwise = Comp.singleton actionFail
+        (c', _) = propR (cSuffix' <> cPrefix, StringEdits es)
+        (cAffSuffix', _) = Comp.splitAt (Comp.length c' - Comp.length cAffPrefix) c'
+        Just pFinal = actionState param cAffPrefix $ actionGroundState @action param
+        rEs = strDiff (actionProduces param cAffSuffix pFinal) (actionProduces param cAffSuffix' pFinal) & stringEdits . sePos . from enum +~ length (actionProduces param cAffPrefix $ actionGroundState @action param)
+
+    propL :: (Compositions action, StringEdits Natural output)
+          -> (Compositions action, StringEdits Natural input)
+    propL (c, StringEdits Seq.Empty) = (c, mempty)
+    propL (c, es) = fromMaybe (c, SEFail) $ do
+      -- Determine states @(iState, fState)@ at the boundary of the region affected by @es@
+      ((,) <$> Int.inf <*> Int.sup -> (minAff, maxAff)) <- affected es
+      trace (show (minAff, maxAff)) $ Just ()
+      let
+        prevTrans :: Natural -> Maybe ( Compositions action {- Run after chosen transition to accepting state -}
+                                      , (ActionState action, input, Seq output, ActionState action)
+                                      , Compositions action {- Run from `stInitial` up to chosen transition -}
+                                      )
+        -- ^ Given an index in the output, find the associated transition in @c@
+        prevTrans needle = do
+          let (after, before) = prevTrans' (c, mempty)
+          transSt <- actionState param before $ actionGroundState @action param
+          trace ("transSt = " ++ show transSt) $ Just ()
+          let (after', trans) = Comp.splitAt (pred $ Comp.length after) after
+          [inS] <- return . toList $ actionConsumes param trans
+          Just postTransSt <- return $ actionState param trans transSt
+          outSs <- return $ actionProduces param trans transSt
+          return (after', (transSt, inS, outSs, postTransSt), before)
+          where
+            -- | Move monoid summands from @after@ to @before@ until first transition of @after@ produces @needle@ or @after@ is a singleton
+            prevTrans' :: (Compositions action, Compositions action)
+                       -> (Compositions action, Compositions action)
+            prevTrans' (after, before)
+              | producedNext > needle = (after, before)
+              | Comp.length after == 1 = (after, before)
+              | otherwise = prevTrans' (after', before')
+              where
+                producedNext = fromIntegral . Seq.length . traceShowId . actionProduces param before' $ actionGroundState @action param
+                (after', nextTrans) = Comp.splitAt (pred $ Comp.length after) after
+                before' = nextTrans `mappend` before
+      (_, (iState, _, _, _), prefix) <- prevTrans minAff 
+      trace (show (iState, Comp.length prefix)) $ Just ()
+      (suffix, (pfState, _, _, fState), _) <- prevTrans maxAff
+      trace (show (pfState, fState, Comp.length suffix)) $ Just ()
+
+      newOut <- actionProduces param c (actionGroundState @action param) `apply` es
+      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
+      trace (show (iState, fState, affNewOut)) $ Just ()
+
+      newIn <- actionFindPath param iState affNewOut fState suffix 
+
+      let oldIn = actionConsumes param . Comp.drop (Comp.length suffix) $ Comp.take (Comp.length c - Comp.length prefix) c
+          inDiff = oldIn `strDiff` newIn
+          diffOffset = fromIntegral . Seq.length $ actionConsumes param prefix
+          inDiff' = inDiff & stringEdits . sePos +~ diffOffset
+
+      trace (show (oldIn, newIn, inDiff')) $ Just ()
+
+      let affComp = Comp.fromList $ actionSingleInput param <$> toList newIn
+  
+      return (suffix <> affComp <> prefix, inDiff')
+
+
+strDiff :: forall sym pos. (Eq sym, Integral pos) => Seq sym -> Seq sym -> StringEdits pos sym
+-- ^ @strDiff a b@ calculates a set of edits, which, when applied to @a@, produce @b@
+strDiff a b = snd . foldl toEdit (0, mempty) $ (getDiff `on` toList) a b
+  where
+    toEdit :: (pos, StringEdits pos sym) -> Diff sym -> (pos, StringEdits pos sym)
+    toEdit (n, es) (Diff.Both _ _) = (succ n, es)
+    toEdit (n, es) (Diff.First _ ) = (n, delete n <> es)
+    toEdit (n, es) (Diff.Second c) = (succ n, insert n c <> es)
+
+trace :: String -> a -> a
+{-# NOINLINE trace #-}
+trace str y = flip seq y . unsafePerformIO . withFile "lens.log" AppendMode $ \h ->
+  hPutStrLn h str
+
+traceShowId :: Show a => a -> a
+traceShowId x = trace (show x) x
+\end{code}
+\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