From f4c419b9ddec15bad267a4463f0720d6e28042d2 Mon Sep 17 00:00:00 2001 From: Gregor Kleen Date: Thu, 30 May 2019 12:18:08 +0200 Subject: Further work --- .gitignore | 1 + edit-lens/package.yaml | 3 + edit-lens/src/Control/DFST.lhs.tex | 1 + edit-lens/src/Control/DFST/Lens.lhs | 405 +++++++-------------- edit-lens/src/Control/DFST/Lens.lhs.tex | 1 + edit-lens/src/Control/Edit.lhs | 2 + edit-lens/src/Control/Edit.lhs.tex | 1 + edit-lens/src/Control/Edit/String.lhs | 120 ++++++ edit-lens/src/Control/Edit/String.lhs.tex | 1 + edit-lens/src/Control/Edit/String/Affected.lhs | 73 ++++ edit-lens/src/Control/Edit/String/Affected.lhs.tex | 1 + edit-lens/src/Control/FST.lhs | 22 +- edit-lens/src/Control/FST.lhs.tex | 1 + edit-lens/src/Control/Lens/Edit.lhs | 6 +- edit-lens/src/Control/Lens/Edit.lhs.tex | 1 + edit-lens/src/Control/Lens/Edit/ActionTree.lhs | 204 +++++++++++ edit-lens/src/Control/Lens/Edit/ActionTree.lhs.tex | 1 + implementation.tex | 89 +++++ interactive-edit-lens/package.yaml | 1 + interactive-edit-lens/src/Interact.hs | 142 +++++--- interactive-edit-lens/src/Interact/Types.hs | 26 +- interactive-edit-lens/src/Main.hs | 17 +- intro.tex | 81 +++++ literature/automatentheorie.bibtex | 6 + literature/composition-tree.bibtex | 7 + presentation.deps | 3 + presentation.meta.yml | 22 ++ presentation.tex | 351 ++++++++++++++++++ presentation/comptree.tex | 53 +++ presentation/editconv.tex | 62 ++++ presentation/switchdfst.tex | 8 + stack.yaml | 2 + thesis.args | 1 + thesis.deps | 3 + thesis.meta.yml.gup | 19 +- thesis.pdf.gup | 4 + thesis.tex | 46 ++- 37 files changed, 1445 insertions(+), 342 deletions(-) create mode 120000 edit-lens/src/Control/DFST.lhs.tex create mode 120000 edit-lens/src/Control/DFST/Lens.lhs.tex create mode 120000 edit-lens/src/Control/Edit.lhs.tex create mode 100644 edit-lens/src/Control/Edit/String.lhs create mode 120000 edit-lens/src/Control/Edit/String.lhs.tex create mode 100644 edit-lens/src/Control/Edit/String/Affected.lhs create mode 120000 edit-lens/src/Control/Edit/String/Affected.lhs.tex create mode 120000 edit-lens/src/Control/FST.lhs.tex create mode 120000 edit-lens/src/Control/Lens/Edit.lhs.tex create mode 100644 edit-lens/src/Control/Lens/Edit/ActionTree.lhs create mode 120000 edit-lens/src/Control/Lens/Edit/ActionTree.lhs.tex create mode 100644 implementation.tex create mode 100644 intro.tex create mode 100644 literature/automatentheorie.bibtex create mode 100644 literature/composition-tree.bibtex create mode 100644 presentation.deps create mode 100644 presentation.meta.yml create mode 100644 presentation.tex create mode 100644 presentation/comptree.tex create mode 100644 presentation/editconv.tex create mode 100644 presentation/switchdfst.tex create mode 100644 thesis.args create mode 100644 thesis.deps diff --git a/.gitignore b/.gitignore index 8bf5f01..bf8d48a 100644 --- a/.gitignore +++ b/.gitignore @@ -8,3 +8,4 @@ literature.pdf **.log **.prof **.prof.* +examples 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: source-dirs: src exposed-modules: - Control.Edit + - Control.Edit.String + - Control.Edit.String.Affected - Control.Lens.Edit + - Control.Lens.Edit.ActionTree - Control.DFST - Control.FST - 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 @@ #-} module Control.DFST.Lens - ( StringEdit(..), sePos, seInsertion - , StringEdits(..), _StringEdits, _SEFail, stringEdits - , insert, delete, replace - , DFSTAction(..), DFSTComplement + ( DFSTAction(..), DFSTComplement , dfstLens + , module Control.Edit.String , module Control.DFST , module Control.Lens.Edit ) where @@ -20,9 +18,12 @@ import Control.DFST import Control.FST hiding (stInitial, stTransition, stAccept) import qualified Control.FST as FST (stInitial, stTransition, stAccept, step) import Control.Lens.Edit +import Control.Lens.Edit.ActionTree import Control.Lens import Control.Lens.TH import Control.Edit +import Control.Edit.String +import Control.Edit.String.Affected import Control.Monad @@ -64,94 +65,8 @@ import Data.Universe (Finite(..)) \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 und löschen des Zeichens an einer einzelnen Position: - -\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 Seq.Empty n c - | n == 0 = Just $ Seq.singleton c - | otherwise = Nothing - go str@(x :<| xs) n c - | n == 0 = Just $ c <| str - | otherwise = (x <|) <$> go xs (pred n) c - apply str (StringEdits (es :|> Delete n)) = flip apply (StringEdits es) =<< go str n - where - go Seq.Empty _ = Nothing - go (x :<| xs) n - | n == 0 = Just xs - | otherwise = (x <|) <$> go xs (pred n) - - 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} - -Wir 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. +\begin{defn}[Ausgabe-Wirkung von DFSTs] +Wir 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. Wir annotieren Wirkungen zudem mit dem konsumierten String. Diese Wirkungen bilden einen Monoiden analog zu Endomorphismen, wobei die Resultat-Strings concateniert werden. @@ -175,13 +90,24 @@ instance Monoid (DFSTAction state input output) where } \end{code} \end{comment} +\end{defn} +\begin{eg} \label{eg:linebreakonw100} + Die Wirkung des DFST aus Beispiel~\ref{eg:linebreak} auf das Wort $w$ aus Beispiel~\ref{eg:w100} ist: + + \begin{align*} + \text{act} & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\ + 0 & \mapsto (0\, 1\, \ldots\, 80\, \text{\tt \textbackslash n}\, 81\, \ldots\, 98, 19) \\ + 1 & \mapsto (0\, 1\, \ldots\, 79\, \text{\tt \textbackslash n}\, 80\, \ldots\, 98, 18) \\ + & \vdots + \end{align*} +\end{eg} + + +\begin{comment} \begin{code} dfstAction :: forall state input output. (Finite state, Ord state, Ord input) => DFST state input output -> input -> DFSTAction state input output -- | Smart constructor of `DFSTAction` ensuring that `Seq.length . dfstaConsumes == const 1` and that `runDFSTAction` has constant complexity -\end{code} -\begin{comment} -\begin{code} dfstAction dfst (Seq.singleton -> dfstaConsumes) = DFSTAction{..} where runDFSTAction :: state -> (Seq output, Maybe state) @@ -193,11 +119,35 @@ dfstAction dfst (Seq.singleton -> dfstaConsumes) = DFSTAction{..} \end{comment} Wir halten im Komplement der edit-lens einen Cache der monoidalen Summen aller kontinuirlichen Teillisten. -\texttt{Compositions} ist ein balancierter Binärbaum, dessen innere Knoten mit der monoidalen Summe der Annotationen aller Blätter annotiert sind. +\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. \begin{code} type DFSTComplement state input output = Compositions (DFSTAction state input output) \end{code} +Wir bedienen uns hierbei einer bestehenden Programmbibliothek \cite{composition-tree} um das Balancieren bei Modifikation des Baums nicht implementieren zu müssen. + +\begin{eg} + Wir definieren zunächst einen weiteren, sehr einfachen, DFST: + + \begin{figure}[H] + \centering + \pinclude{presentation/switchdfst.tex} + \caption{\label{fig:switchdfst} Ein einfacher DFST, der zwischen zwei Zustanden wechselt und Ausgabe abhängig vom aktuellen Zustand erzeugt} + \end{figure} + + Auf $s$ wechselt der DFST seinen Zustand, auf $p$ produziert er, abhängig vom aktuellen Zustand, genau ein Zeichen. + + Wir stellen die Wirkung des DFST auf den Eingabe-String $spp$ grafisch analog zur Baumstruktur von \texttt{Compositions} dar. + 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. + + \begin{figure}[H] + \centering + \pinclude{presentation/comptree.tex} + \caption{Die Wirkung der Eingabe $spp$ auf den Automaten aus Abbildung \ref{fig:switchdfst}} + \end{figure} +\end{eg} + +\begin{comment} \begin{code} runDFSTAction' :: DFSTComplement state input output -> state -> (Seq output, Maybe state) runDFSTAction' = runDFSTAction . Comp.composed @@ -208,6 +158,7 @@ dfstaConsumes' = dfstaConsumes . Comp.composed dfstaProduces :: DFSTComplement state input output -> state -> Seq output dfstaProduces = fmap fst . runDFSTAction' \end{code} +\end{comment} Fü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. @@ -229,6 +180,55 @@ Die input-edits können nun wiederum, unter Beachtung der Verschiebung der indic \begin{comment} \begin{code} type LState state input output = (Natural, (state, Maybe (input, Natural))) + +instance (Ord state, Ord input, Ord output, Show state, Show input, Show output, Finite state) => Action (DFSTAction state input output) input output where + type ActionParam (DFSTAction state input output) = DFST state input output + type ActionState (DFSTAction state input output) = state + + actionFail = DFSTAction (\_ -> (Seq.empty, Nothing)) Seq.empty + + actionSingleInput = dfstAction + + actionGroundState = stInitial + actionStateFinal DFST{..} final = final `Set.member` stAccept + actionState _ act st = view _2 $ runDFSTAction' act st + actionProduces _ act st = dfstaProduces act st + + actionConsumes _ = dfstaConsumes' + + actionFindPath DFST{..} iState affNewOut fState suffix = do + let + outFST :: FST (LState state input output) input output + outFST = restrictOutput affNewOut $ toFST DFST + { stInitial = iState + , stTransition + , stAccept = Set.fromList $ do + fin <- Set.toList $ stAccept `Set.union` Set.map fst (Map.keysSet stTransition) + (suffOut, Just fin') <- return $ runDFSTAction' suffix fin + guard $ Set.member fin' stAccept + guard $ suffOut == dfstaProduces suffix fState + return fin + } + -- trace (show $ pretty outFST) $ Just () + + newPath <- + let + FST{..} = outFST + detOutgoing :: Maybe (LState state input output) -> [(LState state input output, (Maybe input, Maybe output))] + detOutgoing Nothing = concatMap detOutgoing . map Just $ toList stInitial + detOutgoing (Just st) = concatMap (\((_, inS), outs) -> map (\(st', outS) -> (st', (inS, outS))) $ toList outs) . Map.toList $ Map.filterWithKey (\(st', _) _ -> st == st') stTransition + predicate :: [(LState state input output, (Maybe input, Maybe output))] -> Maybe Bool + predicate [] + | not . Set.null $ Set.intersection stInitial stAccept = Just True + | otherwise = Nothing + predicate ((lastSt, _) : _) + | Set.member lastSt stAccept = Just True + | otherwise = Nothing + in bfs detOutgoing predicate + + -- trace (show newPath) $ Just () + + return . Seq.fromList . mapMaybe (\(_st, (inS, _outS)) -> inS) $ reverse newPath \end{code} \end{comment} \begin{code} @@ -236,130 +236,12 @@ dfstLens :: forall state input output. (Ord state, Ord input, Ord output, Show s \end{code} \begin{comment} \begin{code} -dfstLens dfst@DFST{..} = EditLens ground propR propL - where - ground :: DFSTComplement state input output - ground = mempty - - propR :: (DFSTComplement state input output, StringEdits Natural input) -> (DFSTComplement state input output, StringEdits Natural output) - propR (c, SEFail) = (c, SEFail) - propR (c, StringEdits Seq.Empty) = (c, mempty) - propR (c, lEs@(StringEdits (es :> e))) - | (_, Just final) <- runDFSTAction' c' stInitial - , final `Set.member` stAccept - = (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 (dfstAction dfst nChar) - | otherwise = Comp.singleton $ DFSTAction (\_ -> (Seq.empty, Nothing)) Seq.empty - (c', _) = propR (cSuffix' <> cPrefix, StringEdits es) - (cAffSuffix', _) = Comp.splitAt (Comp.length c' - Comp.length cAffPrefix) c' - (_, Just pFinal) = runDFSTAction' cAffPrefix stInitial - rEs = strDiff (dfstaProduces cAffSuffix pFinal) (dfstaProduces cAffSuffix' pFinal) & stringEdits . sePos . from enum +~ length (dfstaProduces cAffPrefix stInitial) - - - propL :: (DFSTComplement state input output, StringEdits Natural output) -> (DFSTComplement state input output, 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 ( DFSTComplement state input output -- ^ Run after chosen transition to accepting state - , (state, input, Seq output, state) - , DFSTComplement state input output -- ^ 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 <- view _2 $ runDFSTAction (Comp.composed before) stInitial - trace ("transSt = " ++ show transSt) $ Just () - let (after', trans) = Comp.splitAt (pred $ Comp.length after) after - DFSTAction{..} = Comp.composed trans - [inS] <- return $ toList dfstaConsumes - (outSs , Just postTransSt) <- return $ runDFSTAction 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' (after, before) - | producedNext > needle = (after, before) - | Comp.length after == 1 = (after, before) - | otherwise = prevTrans' (after', before') - where - producedNext = fromIntegral . Seq.length . traceShowId $ dfstaProduces before' stInitial - (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 <- dfstaProduces c stInitial `apply` es - let affNewOut = (\s -> Seq.take (Seq.length s - Seq.length (dfstaProduces suffix fState)) s) $ Seq.drop (Seq.length $ dfstaProduces prefix stInitial) newOut - trace (show (iState, fState, affNewOut)) $ Just () - - let outFST :: FST (LState state input output) input output - outFST = restrictOutput affNewOut $ toFST DFST - { stInitial = iState - , stTransition - , stAccept = Set.fromList $ do - fin <- Set.toList $ stAccept `Set.union` Set.map fst (Map.keysSet stTransition) - (suffOut, Just fin') <- return $ runDFSTAction' suffix fin - guard $ Set.member fin' stAccept - guard $ suffOut == dfstaProduces suffix fState - return fin - } - trace (show $ pretty outFST) $ Just () - - newPath <- - let - FST{ .. } = outFST - detOutgoing :: Maybe (LState state input output) -> [(LState state input output, (Maybe input, Maybe output))] - detOutgoing Nothing = concatMap detOutgoing . map Just $ toList stInitial - detOutgoing (Just st) = concatMap (\((_, inS), outs) -> map (\(st', outS) -> (st', (inS, outS))) $ toList outs) . Map.toList $ Map.filterWithKey (\(st', _) _ -> st == st') stTransition - predicate :: [(LState state input output, (Maybe input, Maybe output))] -> Maybe Bool - predicate [] - | not . Set.null $ Set.intersection stInitial stAccept = Just True - | otherwise = Nothing - predicate ((lastSt, _) : _) - | Set.member lastSt stAccept = Just True - | otherwise = Nothing - in bfs detOutgoing predicate - - trace (show newPath) $ Just () - - let oldIn = dfstaConsumes' . Comp.drop (Comp.length suffix) $ Comp.take (Comp.length c - Comp.length prefix) c - newIn = Seq.fromList . mapMaybe (\(_st, (inS, _outS)) -> inS) $ reverse newPath - inDiff = oldIn `strDiff` newIn - diffOffset = fromIntegral . Seq.length $ dfstaConsumes' prefix - inDiff' = inDiff & stringEdits . sePos +~ diffOffset - - trace (show (oldIn, newIn, inDiff')) $ Just () - - let affComp = Comp.fromList [ dfstAction dfst inS | (_st, (Just inS, _outS)) <- newPath ] - - 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) +dfstLens = treeLens -- | Generic breadth-first search bfs :: forall state transition. Ord state => (Maybe state -> [(state, transition)]) -- ^ Find outgoing edges - -> ([(state, transition)] {- ^ Reverse path -} -> Maybe Bool {- ^ Continue search, finish successfully, or abort search on this branch -}) -- ^ Search predicate + -> ([(state, transition)] {- Reverse path -} -> Maybe Bool {- Continue search, finish successfully, or abort search on this branch -}) -- ^ Search predicate -> Maybe [(state, transition)] -- ^ Reverse path bfs outgoing predicate | Just True <- emptyRes = Just [] @@ -378,59 +260,46 @@ bfs outgoing predicate Nothing -> bfs' visited' $ cs <> Seq.fromList (map (: c) . filter (\(st, _) -> not $ Set.member st visited) . outgoing $ Just lastSt) where visited' = Set.insert lastSt visited -\end{code} -\end{comment} -Um 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. -Das 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. +-- trace :: String -> a -> a +-- {-# NOINLINE trace #-} +-- trace str y = flip seq y . unsafePerformIO . withFile "lens.log" AppendMode $ \h -> +-- hPutStrLn h str -\begin{code} -affected :: forall char. StringEdits Natural char -> Maybe (Interval Natural) --- ^ 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: --- --- - For all @n :: Natural@: @n < a ==> str ! n == (str `apply` es) ! n@ --- - There exists a @k :: Integer@ such that for all @n :: Integer@: @n > b ==> str ! (n + k) == (str `apply` es) ! n@ --- --- 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@. -\end{code} -\begin{comment} -\begin{code} -affected SEFail = Nothing -affected (StringEdits es) = Just . toInterval $ go es Map.empty - where - toInterval :: Map Natural Integer -> Interval Natural - toInterval map - | Just (((minK, _), _), ((maxK, _), _)) <- (,) <$> Map.minViewWithKey map <*> Map.maxViewWithKey map - = let - maxV' = maximum . (0 :) $ do - offset <- [0..maxK] - v <- maybeToList $ Map.lookup (maxK - offset) map - v' <- maybeToList . fmap fromInteger $ negate v <$ guard (v <= 0) - guard $ v' >= succ offset - return $ v' - offset - in (minK Int.... maxK + maxV') - | otherwise - = Int.empty - go :: Seq (StringEdit Natural char) -> Map Natural Integer -> Map Natural Integer - go Seq.Empty offsets = offsets - go (es :> e) offsets = go es offsets' - where - p = e ^. sePos - -- p' = fromIntegral $ Map.foldrWithKey (\k o p -> bool (fromIntegral p) (o + p) $ k < fromIntegral p) (fromIntegral p) offsets - offsets' = Map.alter (Just . myOffset . fromMaybe 0) p offsets - myOffset :: Integer -> Integer - myOffset - | Insert _ _ <- e = pred - | Delete _ <- e = succ - -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 - - +-- traceShowId :: Show a => a -> a +-- traceShowId x = trace (show x) x \end{code} \end{comment} + +\begin{eg} + 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. + + \begin{equation*} + w^\prime = w = 0\, 1\, \ldots\, 80\, \text{\textbackslash n}\, 81\, \ldots\, 98 + \end{equation*} + + Das von $e$ betroffene Intervall von $w^\prime$ ist $(80, 80)$. + + Das Komplement nach Anwendung des DFST auf $w$ ist, wie in Beispiel \ref{eg:linebreakonw100} dargelegt: + + \begin{align*} + \text{act} & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\ + 0 & \mapsto (0\, 1\, \ldots\, 80\, \text{\tt \textbackslash n}\, 81\, \ldots\, 98, 19) \\ + 1 & \mapsto (0\, 1\, \ldots\, 79\, \text{\tt \textbackslash n}\, 80\, \ldots\, 98, 18) \\ + & \vdots + \end{align*} + + Wir unterteilen $\text{act}$ an $(80, 80)$ in $\text{act}_\text{R} \circ \text{act}_e \circ \text{act}_\text{L}$: + + \begin{align*} + \text{act}_\text{R} & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\ + n & \mapsto (81\, \ldots\, 98, \min ( 80, n + 19 ) ) \\ + & \\ + \text{act}_e & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\ + n & \mapsto ( \text{\tt \textbackslash n}, 0 ) \\ + & \\ + \text{act}_\text{L} & \colon Q \to \Delta^\star \times \{ \bot \} \cup Q \\ + n & \mapsto (0\, 1\, \ldots\, 80, 80) \\ + \text{other} & \mapsto (\epsilon, \bot) + \end{align*} +\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 \end{code} \end{comment} +Um 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}: + \begin{defn}[Moduln] Ein 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: 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 @@ +\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} + 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 @@ +\begin{comment} +\begin{code} +module Control.Edit.String.Affected + ( affected + ) where + +import Control.Lens +import Control.Lens.TH + +import Control.Edit +import Control.Edit.String + +import Numeric.Natural +import Numeric.Interval (Interval, (...)) +import qualified Numeric.Interval as Int + +import Data.Sequence (Seq((:<|), (:|>))) +import qualified Data.Sequence as Seq + +import Data.Map.Lazy (Map) +import qualified Data.Map.Lazy as Map + +import Data.Monoid + +import Control.Monad + +import Data.Maybe (fromMaybe, maybeToList, listToMaybe, catMaybes, isNothing, isJust, mapMaybe) +\end{code} +\end{comment} + +Um 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. +Das 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. + +\begin{code} +affected :: forall char. StringEdits Natural char -> Maybe (Interval Natural) +-- ^ 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: +-- +-- - For all @n :: Natural@: @n < a ==> str ! n == (str `apply` es) ! n@ +-- - There exists a @k :: Integer@ such that for all @n :: Integer@: @n > b ==> str ! (n + k) == (str `apply` es) ! n@ +-- +-- 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@. +\end{code} +\begin{comment} +\begin{code} +affected SEFail = Nothing +affected (StringEdits es) = Just . toInterval $ go es Map.empty + where + toInterval :: Map Natural Integer -> Interval Natural + toInterval map + | Just (((minK, _), _), ((maxK, _), _)) <- (,) <$> Map.minViewWithKey map <*> Map.maxViewWithKey map + = let + maxV' = maximum . (0 :) $ do + offset <- [0..maxK] + v <- maybeToList $ Map.lookup (maxK - offset) map + v' <- maybeToList . fmap fromInteger $ negate v <$ guard (v <= 0) + guard $ v' >= succ offset + return $ v' - offset + in (minK Int.... maxK + maxV') + | otherwise + = Int.empty + go :: Seq (StringEdit Natural char) -> Map Natural Integer -> Map Natural Integer + go Seq.Empty offsets = offsets + go (es :> e) offsets = go es offsets' + where + p = e ^. sePos + -- p' = fromIntegral $ Map.foldrWithKey (\k o p -> bool (fromIntegral p) (o + p) $ k < fromIntegral p) (fromIntegral p) offsets + offsets' = Map.alter (Just . myOffset . fromMaybe 0) p offsets + myOffset :: Integer -> Integer + myOffset + | Insert _ _ <- e = pred + | Delete _ <- e = succ +\end{code} +\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 & \cup \{ (80, \sigma, \sigma, 80) \mid \sigma \in \Sigma \mysetminus \{ \text{\tt ' '}, \text{\tt \textbackslash n} \} \} \end{align*} - \begin{figure}[p] + Siehe auch Abbildung~\ref{fig:linebreak} + + \begin{figure}[h] \centering \begin{tikzpicture}[->,auto,node distance=5cm] \node[initial,state,accepting] (0) {$0$}; @@ -101,7 +103,7 @@ data FST state input output = FST \draw[-] (rest)--(i.north); \draw[-] (rest)--(si.west); \end{tikzpicture} - \caption{Beispiel \ref{eg:linebreak} dargestellt als Graph} + \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} \end{figure} \end{eg} @@ -314,7 +316,9 @@ wordFST inps outs = FST & \cup \{ (i, \sigma, \epsilon, i) \mid \sigma \in \Sigma \cup \{ \epsilon \}, i \in Q \mysetminus \{ 99 \} \} \end{align*} - \begin{figure}[p] + Siehe auch Abbildung~\ref{fig:w100}. + + \begin{figure}[h] \centering \begin{tikzpicture}[->,auto,node distance=5cm] \node[initial,state] (0) {$0$}; @@ -323,11 +327,11 @@ wordFST inps outs = FST \path (0) edge [loop above] node {$\{(\sigma, \epsilon) \mid \sigma \in \Sigma \cup \{ \epsilon \} \}$} (0) edge node {$\{ (\sigma, 1) \mid \sigma \in \Sigma \cup \{ \epsilon \} \}$} (rest) - (rest) edge node {$\{ \sigma, 100 \} \mid \sigma \in \Sigma \cup \{ \epsilon \}$} (99) + (rest) edge node {$\{ (\sigma, 98) \mid \sigma \in \Sigma \cup \{ \epsilon \} \}$} (99) (99) edge [loop above] node {$\{(\sigma, \epsilon) \mid \sigma \in \Sigma \}$} (99); \end{tikzpicture} - \caption{Beispiel \ref{eg:w100} dargestellt als Graph} + \caption{\label{fig:w100} Der Wort-FST eines längeren Wortes} \end{figure} \end{eg} @@ -351,7 +355,9 @@ restrictOutput :: forall state input output. (Ord state, Ord input, Ord output) & \cup \{ ((80, 80), \text{\tt \textbackslash n}, \text{\tt \textbackslash n}, (81, 0)) \} \end{align*} - \begin{figure}[p] + Siehe auch Abbildung~\ref{fig:l80timesw100}. + + \begin{figure}[h] \centering \begin{tikzpicture}[->,auto,node distance=5cm] \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) (rest2) edge node {$(98, 98)$} (99); \end{tikzpicture} - \caption{Beispiel \ref{eg:l80timesw100} dargestellt als Graph} + \caption{\label{fig:l80timesw100} Die Einschränkung des Automaten aus Abbildung \ref{fig:linebreak} auf das Wort aus Abbildung \ref{fig:w100}} \end{figure} \end{eg} \begin{rem} - Es ist bemerkenswert, dass in Beispiel \ref{eg:l80timesw100} die Zirkuläre Struktur von $L_80$ durch Produkt mit einem Wort verloren geht. + Es ist bemerkenswert, dass in Beispiel \ref{eg:l80timesw100} die Zirkuläre Struktur von $L_{80}$ durch Produkt mit einem Wort verloren geht. 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. \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 \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 diff --git a/implementation.tex b/implementation.tex new file mode 100644 index 0000000..f5e5e58 --- /dev/null +++ b/implementation.tex @@ -0,0 +1,89 @@ +Im Rahmen dieser Arbeit haben wir die in den vorherigen Abschnitten beschriebenen Verfahren und Konstruktionen in Haskell implementiert. + +Es hat sich hierbei die oben beschriebene Konstruktion von $\Lleftarrow$ als Komposition algebraischer Transformationen und generischer, wohlbekannter, Algorithmen (Breitensuche auf einem beliebigem Graph) ergeben. +Unsere 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. + +\subsubsection{Struktur der Implementierung} + +Die Implementierung ist aufgeteilt in zwei Stack\footnote{\url{https://haskellstack.org}}-Pakete: \texttt{edit-lens} und \texttt{interactive-edit-lens}. + +Die Module innerhalb von \texttt{edit-lens} entsprechen im wesentlichen den Sektionen dieser Arbeit: +\begin{description} +\item[Control.Edit] + Definition von Moduln +\item[Control.Lens.Edit] + Definition von zustandsbehafteten Monoidhomomorphismen und, damit, edit-lenses sowohl als Typklasse als auch als existentiell quantifizierter Datentyp +\item[Control.Edit.String] + Eine simple edit-Sprache auf Strings +\item[Control.Edit.String.Affected] + Ein Algorithmus um die von einem edit aus \textbf{Control.Edit.String} betroffene Stelle in einem String einzuschränken +\item[Control.FST] + Datentyp, schrittweise-, und vollständige Auswertung und die algebraischen Konstruktionen aus $\Lleftarrow$ für finite state transducer +\item[Control.DFST] + Datentyp, schrittweise-, und vollständige Auswertung sowie Umwandlung zu einem FST für deterministische finite state transducer +\item[Control.Lens.Edit.ActionTree] + Das beschriebene Verfahren zur Darstellung eines beliebigen DFST als edit-lens für jene edit-Sprache + + Es ist hierbei jedoch der konkrete Typ der Wirkung und das Suchschema für $\Lleftarrow$ als Typklasse abstrahiert +\item[Control.DFST.Lens] + Konkrete Anwendung von \textbf{Control.Lens.Edit.ActionTree} auf DFSTs +\end{description} + +\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. + +\texttt{interactive-edit-lens} besteht aus nur drei Modulen: +\begin{description} +\item[Interact] + Implementierung des interaktiven Editors als TUI\footnote{\url{https://hackage.haskell.org/package/brick-0.47}} +\item[Interact.Types] + Unterliegende Datentypen für \texttt{Interact} +\item[Main] + Aufruf von \texttt{Interact} und Implementierung der angebotenen DFSTs +\end{description} + +\subsubsection{Verwendung des interaktiven Editors} + +\begin{figure}[h] + \begin{center} + \includegraphics{screenshot} + \caption{Der interaktive Editor (im Modus \texttt{json-newl}) nach import einer kleinen JSON-Datei} + \end{center} +\end{figure} + +Der interaktive editor kann von der Befehlseingabe gestartet werden wie folgt: +\begin{lstlisting}[language=bash] + $ stack build + $ stack exec interact } einer der in \texttt{Main} implementierten DFSTs: + +\begin{description} +\item[linebreak] + Wandelt Zeilenumbrüche und Leerzeichen ineinander um, sodass alle Zeilen mindestens 80 Zeichen enthalten +\item[json-newl] + Normalisiert Whitespace in einem JSON\footnote{\url{https://de.wikipedia.org/wiki/JSON}}-String. + JSON ist nicht regulär; Es lassen sich Klammern nicht prüfen und Einrückung nicht in Abhängigkeit der Verschachtelung implementieren +\item[alternate] + Akzeptiert Strings gerader Länge, jeder zweite Buchstabe wird in den entsprechenden Großbuchstaben umgewandelt und verdoppelt +\item[id] + Identität-DFST +\item[double] + Verdoppelt jedes Zeichen +\end{description} + +Alle DFSTs (außer \texttt{json-newl}) akzeptieren nur lateinische Buchstaben, Leerzeichen und das Ausrufezeichen. + +Der Text auf beiden Seiten kann frei bearbeitet werden. +Hierbei wechselt \texttt{tab} zwischen den Seiten. + +\texttt{ctrl + p} setzt die Propagation aus, bis sie mit \texttt{ctrl + p} wieder eingeschaltet wird. +Auf der Konsole werden hinterher Zeitmessungen der ersten Propagation nach dem Wiedereinsetzen ausgegeben. + +\texttt{ctrl + o} öffnet eine interaktive Dateiauswahl (\texttt{/} veranlasst eine Suche, \texttt{return} bestätigt die Auswahl). +Nach Auswahl wird der Inhalt der Datei am Cursor eingefügt. + +\subsubsection{Performance} + +Bei der Implementierung wurde nicht auf Performance geachtet. +Es ist daher die Laufzeit des interaktiven Editors bereits bei kleinen Eingabe inakzeptabel lang (mehrere Sekunden für ein Kilobyte JSON). +Es 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: - mtl - transformers - universe + - deepseq # ghc-options: [ -O2 ] 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 import Data.Text (Text) import qualified Data.Text as Text +import qualified Data.Text.IO as Text import Data.Text.Zipper @@ -41,6 +42,7 @@ import Brick hiding (on) import Brick.Focus import Brick.Widgets.Center import Brick.Widgets.Border +import Brick.Widgets.FileBrowser import Graphics.Vty hiding (showCursor) import Config.Dyre @@ -48,14 +50,20 @@ import Config.Dyre import System.IO.Unsafe import Debug.Trace -interactiveEditLens :: (Params (InteractConfig c) -> Params (InteractConfig c)) -> InteractConfig c -> IO () +import System.CPUTime +import Text.Printf + +import Control.Exception (evaluate) +import Control.DeepSeq + +interactiveEditLens :: forall c. NFData c => (Params (InteractConfig c) -> Params (InteractConfig c)) -> InteractConfig c -> IO () interactiveEditLens f = wrapMain . f $ defaultParams { projectName = "interact-edit-lens" , showError = \s err -> s & compileError .~ Just err , realMain = interactiveEditLens' } -interactiveEditLens' :: forall c. InteractConfig c -> IO () +interactiveEditLens' :: forall c. NFData c => InteractConfig c -> IO () interactiveEditLens' cfg@InteractConfig{..} | Just err <- icfgCompileError = hPutStrLn stderr err @@ -89,9 +97,8 @@ interactiveEditLens' cfg@InteractConfig{..} where infix 1 &?~ - (&?~) :: a -> RWS (InteractConfig c) () a b -> a + (&?~), actOn :: a -> RWS (InteractConfig c) () a b -> a st &?~ act = (\(s, ()) -> s) $ execRWS act cfg st - actOn = (&?~) initialState :: InteractState c @@ -101,6 +108,8 @@ interactiveEditLens' cfg@InteractConfig{..} , istRight = (Last Valid, Last (init @(StringEdits Natural Char), 0), mempty) , istFocus = focusRing [LeftEditor, RightEditor] & focusSetCurrent (case icfgInitial of InitialRight _ -> RightEditor; _other -> LeftEditor) + , istActive = True + , istLoadBrowser = Nothing } app :: InteractApp c @@ -109,10 +118,15 @@ interactiveEditLens' cfg@InteractConfig{..} appDraw :: InteractState c -> [Widget InteractName] appDraw InteractState{..} = [ editors ] where - editors = hBox - [ mbInvalid (withFocusRing istFocus renderEditor') (istLeft `WithName` LeftEditor) - , vBorder - , mbInvalid (withFocusRing istFocus renderEditor') (istRight `WithName` RightEditor) + editors = vBox + [ case istLoadBrowser of + Nothing -> hBox + [ mbInvalid (withFocusRing istFocus renderEditor') (istLeft `WithName` LeftEditor) + , vBorder + , mbInvalid (withFocusRing istFocus renderEditor') (istRight `WithName` RightEditor) + ] + Just lBrowser -> renderFileBrowser True lBrowser + , hCenter . str $ bool "Inactive" "" istActive ] renderEditor' :: Bool -> (Seq Char, Int) `WithName` InteractName -> Widget InteractName renderEditor' foc ((content, cPos) `WithName` n) @@ -133,42 +147,75 @@ interactiveEditLens' cfg@InteractConfig{..} mbInvalid f ((Last Valid , Last x, _) `WithName` n) = f $ x `WithName` n appHandleEvent :: InteractState c -> BrickEvent InteractName InteractEvent -> EventM InteractName (Next (InteractState c)) - appHandleEvent st@InteractState{..} (VtyEvent ev) = case ev of - EvKey KEsc [] -> halt st - EvKey (KChar 'c') [MCtrl] -> halt st - EvKey (KChar '\t') [] -> continue $ st & focus %~ focusNext - EvKey KBackTab [] -> continue $ st & focus %~ focusPrev - EvKey (KChar 'a') [MCtrl] -> continue $ st &?~ doMove - (moveSplit (== '\n') $ \(c, (l, p)) -> if any (== '\n') (c l) || Seq.null (c l) then (pred l, 0) else (l, 0)) - EvKey (KChar 'e') [MCtrl] -> continue $ st &?~ doMove - (moveSplit (== '\n') $ \(c, (l, p)) -> if any (== '\n') $ c l then (pred l, Seq.length . c $ pred l) else (l, Seq.length $ c l)) - EvKey KLeft [MCtrl] -> continue $ st &?~ doMove - (moveSplit isSpace $ \(c, (l, _)) -> if any isSpace (c l) || Seq.null (c l) then (pred l, 0) else (l - 2, 0)) - EvKey KRight [MCtrl] -> continue $ st &?~ doMove - (moveSplit isSpace $ \(c, (l, _)) -> if any isSpace $ c l then (succ l, 0) else (l + 2, 0)) - EvKey KUp [] -> continue $ st &?~ doMove - (moveSplit (== '\n') $ \(c, (l, p)) -> if any (== '\n') (c l) || Seq.null (c l) then (pred l, p) else (l - 2, p)) - EvKey KDown [] -> continue $ st &?~ doMove - (moveSplit (== '\n') $ \(c, (l, p)) -> if any (== '\n') (c l) then (succ l, p) else (l + 2, p)) - EvKey KLeft [] -> continue $ st &?~ doMove moveLeft - EvKey KRight [] -> continue $ st &?~ doMove moveRight - EvKey KDel [] -> continue $ st &?~ doEdit (delete 0) - EvKey KBS [] -> continue . actOn st $ do - focused' <- preuse $ focused . _2 . _Wrapped - doEdit . delete $ -1 - unless (maybe False ((==) <$> view _2 <*> view (_1 . to Seq.length)) focused') $ - doMove moveLeft - EvKey (KChar c) [] -> continue . actOn st $ do - doEdit $ insert 0 c - doMove moveRight - EvKey KEnter [] -> continue . actOn st $ do - doEdit $ insert 0 '\n' - doMove moveRight - other -> suspendAndResume $ do - traceIO $ "Unhandled event:\n\t" ++ show other - return st - -- where - -- editorMovement f = continue $ st & focused . _Just . editContentsL %~ f + appHandleEvent st@InteractState{..} (VtyEvent ev) + | Nothing <- istLoadBrowser = case ev of + EvKey KEsc [] -> halt st + EvKey (KChar 'c') [MCtrl] -> halt st + EvKey (KChar '\t') [] -> continue . actOn st . runMaybeT $ do + guard =<< use active + focus %= focusNext + EvKey KBackTab [] -> continue . actOn st . runMaybeT $ do + guard =<< use active + focus %= focusPrev + EvKey (KChar 'a') [MCtrl] -> continue $ st &?~ doMove + (moveSplit (== '\n') $ \(c, (l, p)) -> if any (== '\n') (c l) || Seq.null (c l) then (pred l, 0) else (l, 0)) + EvKey (KChar 'e') [MCtrl] -> continue $ st &?~ doMove + (moveSplit (== '\n') $ \(c, (l, p)) -> if any (== '\n') $ c l then (pred l, Seq.length . c $ pred l) else (l, Seq.length $ c l)) + EvKey KLeft [MCtrl] -> continue $ st &?~ doMove + (moveSplit isSpace $ \(c, (l, _)) -> if any isSpace (c l) || Seq.null (c l) then (pred l, 0) else (l - 2, 0)) + EvKey KRight [MCtrl] -> continue $ st &?~ doMove + (moveSplit isSpace $ \(c, (l, _)) -> if any isSpace $ c l then (succ l, 0) else (l + 2, 0)) + EvKey KUp [] -> continue $ st &?~ doMove + (moveSplit (== '\n') $ \(c, (l, p)) -> if any (== '\n') (c l) || Seq.null (c l) then (pred l, p) else (l - 2, p)) + EvKey KDown [] -> continue $ st &?~ doMove + (moveSplit (== '\n') $ \(c, (l, p)) -> if any (== '\n') (c l) then (succ l, p) else (l + 2, p)) + EvKey KLeft [] -> continue $ st &?~ doMove moveLeft + EvKey KRight [] -> continue $ st &?~ doMove moveRight + EvKey KDel [] -> continue $ st &?~ doEdit (delete 0) + EvKey KBS [] -> continue . actOn st $ do + focused' <- preuse $ focused . _2 . _Wrapped + doEdit . delete $ -1 + unless (maybe False ((==) <$> view _2 <*> view (_1 . to Seq.length)) focused') $ + doMove moveLeft + EvKey (KChar c) [] -> continue . actOn st $ do + doEdit $ insert 0 c + doMove moveRight + EvKey KEnter [] -> continue . actOn st $ do + doEdit $ insert 0 '\n' + doMove moveRight + EvKey (KChar 'p') [MCtrl] + | istActive -> do + void . liftIO . evaluate . force . ($ st) $ (,,) <$> view left <*> view right <*> view complement + continue $ st & active .~ False + | otherwise -> do + let st' = actOn st $ do + active .= True + doEdit mempty + before <- liftIO getCPUTime + void . liftIO . evaluate . force . ($ st') $ (,,) <$> view left <*> view right <*> view complement + after <- liftIO getCPUTime + suspendAndResume $ do + printf "Resume took %.12fs\n" (fromInteger (after - before) * 1e-12 :: Double) + return st' + EvKey (KChar 'o') [MCtrl] -> do + lBrowser <- liftIO $ newFileBrowser selectNonDirectories LoadBrowser Nothing + continue $ st & loadBrowser .~ Just lBrowser + other -> suspendAndResume $ do + traceIO $ "Unhandled event:\n\t" ++ show other + return st + -- where + -- editorMovement f = continue $ st & focused . _Just . editContentsL %~ f + | Just lBrowser <- istLoadBrowser = do + lBrowser' <- handleFileBrowserEvent ev lBrowser + case fileBrowserSelection lBrowser' of + [] -> continue $ st &?~ loadBrowser .= Just lBrowser' + (FileInfo{..} : _) -> do + insEdit <- divInit . view charseq <$> liftIO (Text.readFile fileInfoFilePath) + let st' = actOn st $ do + doEdit $ (insEdit :: StringEdits Natural Char) & stringEdits . sePos %~ fromIntegral + loadBrowser .= Nothing + continue st' + appHandleEvent st _ = continue st doMove = zoom $ focused . _2 . _Wrapped @@ -259,9 +306,10 @@ doEdit relativeEdit = void . runMaybeT $ do | otherwise = currentPos aL . _2 %= (<> Last (newContent, currentPos')) absoluteEdit' <- uses (aL . _3) (absoluteEdit `mappend`) - bEdits <- prop direction absoluteEdit' - bDom <- use $ bL . _2 . _Wrapped . _1 - case bDom `apply` bEdits of + bRes <- runMaybeT $ do + guard =<< use active + (,) <$> use (bL . _2 . _Wrapped . _1) <*> prop direction absoluteEdit' + case uncurry apply =<< bRes of Nothing -> do bL . _1 %= (<> Last Invalid) 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 @@ -{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TemplateHaskell, DeriveGeneric, StandaloneDeriving #-} {-# OPTIONS_GHC -fno-warn-orphans #-} module Interact.Types @@ -6,7 +6,7 @@ module Interact.Types , _LeftEditor, _RightEditor, _PrimitiveName , Validity, pattern Valid, pattern Invalid , InteractState(..) - , HasLeft(..), HasRight(..), HasComplement(..), HasFocus(..), HasFocused(..) + , HasLeft(..), HasRight(..), HasComplement(..), HasFocus(..), HasFocused(..), HasActive(..), HasLoadBrowser(..) , InteractInitial(..) , _InitialLeft, _InitialRight, _InitialEmpty , InteractConfig(..) @@ -38,6 +38,7 @@ import Numeric.Natural import Brick import Brick.Focus import Brick.Widgets.Edit +import Brick.Widgets.FileBrowser import Control.Lens import Control.Lens.TH @@ -47,12 +48,29 @@ import Control.DFST.Lens import Data.Text.Zipper.Generic +import Control.DeepSeq +import GHC.Generics (Generic) + + +deriving instance Generic (StringEdit n c) +instance (NFData n, NFData c) => NFData (StringEdit n c) + +deriving instance Generic (StringEdits n c) +instance (NFData n, NFData c) => NFData (StringEdits n c) + +deriving instance Generic (DFSTAction s c c') +instance (NFData s, NFData c, NFData c') => NFData (DFSTAction s c c') + +instance (NFData s, NFData c, NFData c') => NFData (DFSTComplement s c c') where + rnf = foldr deepseq () + data InteractName = LeftEditor | RightEditor + | LoadBrowser | PrimitiveName !Text - deriving (Eq, Ord, Show, Read) + deriving (Eq, Ord, Show, Read, Generic) makePrisms ''InteractName @@ -64,6 +82,8 @@ data InteractState c = InteractState { istLeft, istRight :: (Last Validity, Last (Seq Char, Int), StringEdits Natural Char) , istComplement :: c , istFocus :: FocusRing InteractName + , istActive :: Bool + , istLoadBrowser :: Maybe (FileBrowser InteractName) } makeLensesWith 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 @@ {-# LANGUAGE OverloadedStrings , ExistentialQuantification + , DeriveGeneric #-} module Main where @@ -30,18 +31,23 @@ import Debug.Trace import Data.Universe -data SomeDFST = forall state. (Ord state, Show state, Finite state) => SomeDFST { someDFST :: DFST state Char Char } +import Control.DeepSeq +import GHC.Generics (Generic) + +data SomeDFST = forall state. (Ord state, Show state, Finite state, NFData (DFSTComplement state Char Char)) => SomeDFST { someDFST :: DFST state Char Char } data JsonContext = JCInDet | JCDict | JCDictKey | JCDictVal | JCArray | JCArrayVal | JCTop - deriving (Eq, Ord, Show, Read, Enum, Bounded) + deriving (Eq, Ord, Show, Read, Enum, Bounded, Generic) instance Universe JsonContext instance Finite JsonContext +instance NFData JsonContext + data JsonNewlState = JNElement JsonContext | JNTrue String JsonContext | JNFalse String JsonContext | JNNull String JsonContext | JNLitEnd JsonContext | JNString JsonContext | JNStringEsc Int JsonContext | JNStringEnd JsonContext | JNNumberDigits Bool JsonContext | JNNumberDecimal JsonContext | JNNumberDecimalDigits Bool JsonContext | JNNumberExpSign JsonContext | JNNumberExpDigits Bool JsonContext | JNNumberEnd JsonContext - deriving (Eq, Ord, Show, Read) + deriving (Eq, Ord, Show, Read, Generic) instance Universe JsonNewlState where universe = concat [ JNElement <$> universeF @@ -63,6 +69,8 @@ instance Universe JsonNewlState where inits' xs = inits xs \\ [""] instance Finite JsonNewlState +instance NFData JsonNewlState + jsonStrEscapes :: [(Char, Seq Char)] jsonStrEscapes = [ ('"', "\\\"") , ('\\', "\\\\") @@ -78,10 +86,11 @@ hexDigits :: [Char] hexDigits = ['0'..'9'] ++ ['a'..'f'] data LineBreakState = LineBreak Int - deriving (Eq, Ord, Show, Read) + deriving (Eq, Ord, Show, Read, Generic) instance Universe LineBreakState where universe = [ LineBreak n | n <- [0..80] ] instance Finite LineBreakState +instance NFData LineBreakState dfstMap :: String -> Maybe SomeDFST dfstMap "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 @@ +\subsubsection{Motivation} + +Unter 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). + +Es 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. + +In 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. +Vor 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. + +\subsubsection{Inhalt} + +Wir 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. +In 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. +Abschnitt \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. +In 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. +In Abschnitt \ref{implementierung} kommentieren wir den Implementierungs-Prozess der Arbeit und die Schlüsse, die wir aus der Implementierung als solche ziehen konnten. + +\subsection{Historischer Überblick} + +Bidirektionale, inkrementelle, und kombinierbare Parser und ihre Analyse sind ein vergleichsweise modernes Konzept und stützen sich in weiten Teilen auf vorhergehende Arbeit: + +% [x] a programmable editor +% [x] bidirectional tree transformations +% [x] boomerang +% [x] combinator parser +% [ ] ~~delta lenses & optifibrations~~ +% [x] edit languages for information trees +% [x] edit lenses +% [x] efficient and flexible incremental parsing +% [x] general incremental lexical analysis +% [ ] ~~incrementel analysis of real programming languages~~ +% [x] incremental parsing +% [x] incremental semantic analysis +% [x] lazy functional incremental parsing +% [ ] ~~lenses and bidirectional programs~~ +% [ ] ~~parallel inceremntal compilation~~ +% [x] parsing in a broad sense +% [ ] polish parsers +% [x] symmetric lenses +% [x] unifying lenses +% [ ] ~~universal updates for symmetric lenses~~ + +\begin{description} % TODO: more + \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. + \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. + \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}. + \item[1998] \cite{wagner1998efficient} stellen neue, Laufzeit- und Speicher-optimale, Methoden zur Konstruktion inkrementeller Parser auf Basis beliebiger $LR(k)$-Grammatiken vor. + \item[2001] \cite{swierstra2001combinator} demonstriert den Nutzen Kombinator-basierter Parser-Konstruktion in der Praxis + \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 + \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. + Auch enthalten ist eine nützliche Klassifikation und ein historischer Überblick diverser bidirektionalen Programmiertechniken. + \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. + \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. + \item[2011] \cite{hofmann2011symmetric} definieren symmetrische \emph{set-based}-lenses (funktionale Linsen im konventionellen Sinn), d.h. ohne strukturierte edits. + Es wird auch die umfangreiche algebraische Struktur symmetrischer Linsen besprochen. + Vieles hiervon vererbt sich direkt auf edit-lenses als Spezialfall symmetrischer Linsen. + \item[2012] \cite{hofmann2012edit} definieren edit-lenses. + In Abgrenzung zu bestehenden Formalismen symmetrischer funktionaler Linsen arbeiten edit-lenses ausschließlich auf algebraisch strukturierten edit-Sprachen, was sie besonders attraktiv macht. + \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. + \item[2014] \cite{zaytsev2014parsing} geben einen nützlichen Überblick über die, historisch inkonsistente, Terminologie und Konzepte im Zusammenhang mit Parsing. + \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. + Ein relevantes Resultat ist hierbei ein Begriff von asymmetrischen edit-lenses kompatibel mit dem symmetrischen Fall. +\end{description} + +\subsection{Begriffsverzeichnis} + +Obwohl wir detailliertere Definitionen der folgenden Konzepte im Laufe der Arbeit geben, ist es dennoch nützlich vorab die Bedeutung der verwendeten Begriffe kurz anzuschneiden: + +\begin{description} + \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 + \item[DFST] \emph{Deterministic finite-state-transducer} sind FSTs bei denen für jeden Zustand jedes gelesene Zeichen maximal einen Zustandsübergang zulässt + \item[Monoid] \emph{Monoiden} sind algebraisch zwischen Halbgruppen und Gruppen angesiedelt. + 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. + \item[Moduln & edits] \emph{Moduln} verknüpfen eine Trägermenge mit einer Menge von \emph{edits} (mit monoidaler Struktur) auf jener Menge. + Edits beschreiben jeweils eine partielle Abbildung innerhalb der Trägermenge. + \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. + Wir finden es hilfreich von einer Projektion ($\searrow$) und einem \emph{edit-Propagator} ($\nearrow$) zu sprechen. + \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 + \item[edit-lenses] \emph{edit-lenses} verknüpfen zwei Moduln-Trägermengen indem sie edits des einen Modul in die des anderen übersetzen. + Hierbei wird ein, mit den jeweiligen Elementen der Trägermengen konsistenter, unterliegender Zustand, das \emph{Komplement} der edit-lens, gewahrt. +\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 @@ +@book{hofmann2011automatentheorie, + title={Automatentheorie und Logik}, + author={Hofmann, Martin and Lange, Martin}, + year={2011}, + publisher={Springer-Verlag} +} 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 @@ +@manual{composition-tree, + title={Composition trees for arbitrary monoids}, + author={Liam O'Connor}, + month={7}, + year={2015}, + url={https://hackage.haskell.org/package/composition-tree} +} \ 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 @@ +presentation/comptree.tex +presentation/editconv.tex +presentation/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 @@ +--- +title: Inkrementelle Parser als edit-lenses anhand von DFSTs +abstract: |- + Inkrementelle Parser sind jene die bekannte Texte nach einer kleinen Änderung neu analysieren können ohne die ganze Eingabe erneut zu betrachten. + + Inkrementelle Parser sind seit den 1970er-Jahren bekannt und inzwischen umfangreich erforscht. + + Edit-lenses sind eine vergleichsweise neue algebraische Darstellung von Programmen, die algebraisch strukturierte Änderungen zwischen Strukturen übersetzen. + + 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. + + Im Rahmen dessen stellen wir eine Implementierung von edit-lenses im Allgemeinen und unserem Verfahren in möglichst idiomatischem Haskell vor. +author: Gregor Kleen +lang: de-de +link-citations: true +theme: Montpellier +colortheme: dove +navigation: false +toc: false +section-titles: false +bibliography: literature.bibtex +... diff --git a/presentation.tex b/presentation.tex new file mode 100644 index 0000000..3eddd70 --- /dev/null +++ b/presentation.tex @@ -0,0 +1,351 @@ +\section{Einführung} + +\begin{frame} + \frametitle{Tl;dr} + + \begin{itemize} + \item Inkrementelle Parser agieren auf \emph{edits} von Ein- und Ausgaben + \item Edit-Lenses sind algebraische Struktur für deartige Programme + \item DFSTs sind spezielle Parser, schwach genug um immer auch inkrementell zu sein + \item Darstellung von DFSTs als edit-lenses als Proof of Concept + \end{itemize} +\end{frame} + +\begin{frame} + \frametitle{Struktur} + \begin{enumerate} + \item Begriffe/Definitionen + \begin{itemize} + \item Parser, Inkrementelle Parser + \item Funktionale Linsen, edit-lenses + \end{itemize} + \item Motivation + \item Inhalt der Arbeit + \begin{itemize} + \item Inkrementelle Parser als edit-lenses für DFSTs + \end{itemize} + \item Demonstration + \begin{itemize} + \item Interaktiver Editor unter einer edit-lens + \end{itemize} + \item Skizze des Verfahrens aus der Arbeit + \begin{itemize} + \item Komplement-Konstruktion für DFSTs + \item $\Rrightarrow$ und $\Lleftarrow$ + \end{itemize} + \item Weiterführendes + \end{enumerate} +\end{frame} + +\begin{frame} + \frametitle{Inkrementelle Parser} + + \begin{defn}[Parser] + Jedes Programm vom Typ $\Sigma^\star \to a$ + \note[item]{Programme, die Strings analysieren und eine Struktur produzieren} + \end{defn} + + \begin{defn}[Inkrementelle Parser] + Vermeiden komplette Re-analyse bekannter Eingabe-Texte + + Für unsere Zwecke\footnote{Mit $\delta(x)$ immer einer geeigneten Sprache von edits über $x$}: + \[ + \delta ( \Sigma^\star ) \to \delta ( a ) + \] + \end{defn} +\end{frame} + +\begin{frame} + \begin{defn}[Funktionale Linsen] + Eine Linse auf ein $a$ \emph{innerhalb} eines größeren $s$: + \begin{align*} + G & \colon s \to a \\ + P & \colon (a \to a) \to (s \to s) + \end{align*} + \note[item]{Zum Verständnis: nimm $s$ als Klasse/Struct und $a$ als Attribut davon} + \begin{itemize} + \item Bidirektional + \item \emph{fokussiert} Teil der großen Struktur $s$ + \item Projektion und Update-Propagator + \item $P$ und $G$ sind \emph{well-behaved} + \end{itemize} + \end{defn} +\end{frame} + +\begin{frame} + \begin{defn}[edit-lenses] + \begin{align*} + \Rrightarrow & \colon \delta(s) \times C \to \delta(a) \times C \\ + \Lleftarrow & \colon \delta(a) \times C \to \delta(s) \times C + \end{align*} + 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 + \begin{itemize} + \item Bidirektional + \item Edit-Propagatoren in beide Richtungen + \item Edits haben \emph{Algebraische Struktur} + \item $\Rrightarrow$ und $\Lleftarrow$ sind \emph{well-behaved} + \end{itemize} + \note[item]{$\delta(s)$ ist Speziallfall von $s \to s$} + \end{defn} +\end{frame} + +\begin{frame}[fragile] + + \frametitle{Edit-Konversationen} + \framesubtitle{Vereinfacht, ohne Komplement} + + \begin{figure} + \centering + \pinclude{presentation/editconv.tex} + \end{figure} + +\end{frame} + +\begin{frame} + \frametitle{FSTs} + + \begin{defn}[Finite state transducer] + Endliche Automaten mit Ausgabe-Symbolen an Zustansübergängen annotiert. + \note[item]{\emph{Determinismus} analog zu DFAs} + \end{defn} + +%% \begin{eg} +%% \centering +%% \begin{tikzpicture}[->,auto,node distance=2.5cm] +%% \node[initial,state] (0) {$A$}; +%% \node[state,accepting] (1) [right of=0] {$B$}; +%% \node[state,initial,accepting,initial where=right] (2) [right of=1] {$C$}; + +%% \path (0) edge [loop above] node {$(a, x)$} (0) +%% (0) edge node {$(a, y)$} (1) +%% (1) edge [bend left=20] node [above] {$(a, z)$} (2) +%% (1) edge [bend right=20] node [below] {$(b, z)$} (2) +%% (2) edge [loop above] node {$(\epsilon, z)$} (2); +%% \end{tikzpicture} +%% \note[item]{Beispiel ist \emph{nicht} deterministisch} +%% \note[item]{Beispiel hat zwei initiale Zustände} +%% \note[item]{Beispiel hat zwei akzeptierende Zustände} +%% \note[item]{$a^{+}(a \mid b)^{?} \to x^{n}(yz^{+})^{?} \mid z^\star$} +%% %% \begin{tikzpicture}[->,auto,node distance=2.5cm] +%% %% \node[initial,state] (0) {$A$}; +%% %% \node[state,accepting] (1) [right of=0] {$B$}; +%% %% \node[state,accepting] (2) [right of=1] {$C$}; + +%% %% \path (0) edge node {$(a, y)$} (1) +%% %% (1) edge [bend left=20] node [above] {$(a, z)$} (2) +%% %% (1) edge [bend right=20] node [below] {$(b, z)$} (2); +%% %% \end{tikzpicture} +%% \end{eg} +%% \end{frame} + +%% \begin{frame} +%% \frametitle{Beispiel-DFST} + + \begin{figure} + \centering + \pinclude{presentation/switchdfst.tex} + \end{figure} +\end{frame} + +\section{Motivation} + +\begin{frame} + \frametitle{Motivation} + + \begin{itemize} + \item edit-lenses (und unterliegende edits) haben umfangreiche algebraische Struktur + \item Inkrementelle Parser haben praktische Vorteile, wo anwendbar + \item Darstellung von inkrementellen Parsern als edit-lenses erlaubt Kompositions-basierte Konstruktion von Parsern + \end{itemize} + + \begin{eg} + \begin{itemize} + \item Interaktive Programmierumgebung kann \emph{sofort} Feedback geben (Semantisches autocomplete, syntax highlighting, ...) + \item Grafische Konfigurations-Ansichten für unterliegende Konfigurationsdateien können Formatierung (z.B. Kommentare) erhalten + \end{itemize} + \end{eg} +\end{frame} + +\section{Inhalt der Arbeit} + +\begin{frame} + \frametitle{Inhalt} + + \begin{itemize} + \item edits, edit-lenses, und FSTs in Haskell + \item Verfahren zum automatischen Ableiten von edit-lenses aus DFSTs + \item Interaktiver editor für beliebige edit-lenses zwischen Strings + \end{itemize} +\end{frame} + +\section{Demonstration} + +\begin{frame} + \frametitle{JSON-Normalisierer} + \framesubtitle{Demonstration} + + \begin{itemize} + \item JSON-Normalisierung ausgedrückt als DFST + \item edit-lens aus DFST abgeleitet + \item Interaktiver editor akzeptiert edits auf einer Seite und propagiert in Gegenrichtung + \end{itemize} +\end{frame} + +\section{Edit-lenses für DFSTs} + +\begin{frame} + \frametitle{Ansatz} + + Als \emph{Komplement} genug Information um für jedes Intervall im Eingabe-String berechnen zu können: + + \begin{itemize} + \item Gegeben einen Zustand auf der linken Seite des Intervalls, welche Ausgabe wird produziert und welcher Zustand wird auf der rechten Seite erreicht? + + \[ \text{state} \to \text{outChar}^\star \times (\text{state} \cup \{ \bot \}) \] + + \emph{Ausgabe-Wirkung} des FST + \item Welche Eingabe wurde im Intervall konsumiert? + \end{itemize} + + Gegeben einen edit: + + \begin{enumerate} + \item Intervall in Ausgabe/Eingabe bestimmen, die von edit betroffen ist + \item Betroffenes Teilstück des Komplements austauschen + \item Übertragenen edit Anhand von Differenz der Komplement-Stücke bestimmen + \end{enumerate} +\end{frame} + +\begin{frame} + \frametitle{Composition-Trees} + \framesubtitle{Effiziente Berechnung von Wirkungen beliebiger Eingabe-Intervalle} + + \begin{columns}[c] + \column{.5\textwidth} + \begin{center} + \scalebox{1}{\pinclude{presentation/switchdfst.tex}} + \end{center} + \column{.5\textwidth} + \begin{center} + \scalebox{0.65}{\pinclude{presentation/comptree.tex}} + \end{center} + \end{columns} +\end{frame} + +\begin{frame} + \frametitle{$\Rrightarrow$} + + \begin{align*} + \Rrightarrow & \colon \delta ( \text{inChar}^\star ) \times C \to \delta ( \text{outChar}^\star ) \times C \\ + C & \colon \left ( \text{outChar}^\star \times (\text{state} \cup \{ \bot \}), \text{inChar}^\star \right ) + \end{align*} + + \begin{enumerate} + \item Bestimme Intervall in $\text{inChar}^\star$ betroffen von edit und asoziiertes Stück $c \subseteq C$ + \item Lese in $C$ betroffenes Intervall in $\text{outChar}^\star$ ab + \item Berechne neues Stück $c^\prime$ durch Auswertung des DFST + \item Bestimme $\delta (\text{outChar}^\star)$ mit Standard-Diff auf $\text{inChar}^\star$-Komponenten von $c$ und $c^\prime$ + \item Ersetze $c$ in $C$ mit $c^\prime$ + \end{enumerate} +\end{frame} + +\begin{frame} + \frametitle{$\Rrightarrow$} + \framesubtitle{Beispiel} + + \begin{columns}[c] + \column{.33\textwidth} + \begin{enumerate} + \item Intervall im Eingabetext + \item Ausgabe-Stück aus Komplement + \item Neues Komplement-Stück durch Auswertung + \item Komplement-Stück ersetzen + \item Ausgabe-Differenz aus Komplement-Stücken + \end{enumerate} + \column{.33\textwidth} + \begin{center} + \scalebox{1}{\pinclude{presentation/switchdfst.tex}} + \end{center} + \column{.33\textwidth} + \begin{center} + \scalebox{0.6}{\pinclude{presentation/comptree.tex}} + \end{center} + \end{columns} +\end{frame} + +\begin{frame} + \frametitle{$\Lleftarrow$} + + \begin{align*} + \Lleftarrow & \colon \delta ( \text{outChar}^\star ) \times C \to \delta ( \text{inChar}^\star ) \times C \\ + C & \colon \left ( \text{outChar}^\star \times (\text{state} \cup \{ \bot \}), \text{inChar}^\star \right ) + \end{align*} + + \begin{enumerate} + \item Bestimme Intervall in $\text{outChar}^\star$ betroffen von edit und asoziiertes Stück $c \subseteq C$ + \item Bestimme neue Ausgabe durch Anwenden von $\delta ( \text{outChar}^\star )$ + \item Finde, durch Breitensuche, Lauf in DFST mit passender Ausgabe und selben Grenzen wie $c$ + \item Lese $c^\prime$ aus neuem Lauf ab + \item Bestimme $\delta ( \text{inChar}^\star )$ mit Standard-Diff + \item Ersetze $c$ in $C$ mit $c^\prime$ + \end{enumerate} +\end{frame} + +\begin{frame} + \frametitle{$\Lleftarrow$} + \framesubtitle{Beispiel} + + \begin{columns}[c] + \column{.33\textwidth} + \begin{enumerate} + \item Intervall im Ausgabetext + \item Neue Ausgabe für Intervall + \item Breitensuche nach neuem Lauf-Stück + \item Neues Komplement-Stück + \item Komplement-Stück ersetzen + \item Eingabe-Differenz aus Komplement-Stücken + \end{enumerate} + \column{.33\textwidth} + \begin{center} + \scalebox{1}{\pinclude{presentation/switchdfst.tex}} + \end{center} + \column{.33\textwidth} + \begin{center} + \scalebox{0.6}{\pinclude{presentation/comptree.tex}} + \end{center} + \end{columns} +\end{frame} + +\section{Resultate} + +\begin{frame} + \frametitle{Ergebnisse} + + \begin{itemize} + \item Verfahren zum automatischen Ableiten von inkrementellen Parsern zu DFSTs + \item Inkl. Darstellung als edit-lens + \item Interaktive Demonstration von edit-lenses + \end{itemize} +\end{frame} + +\begin{frame} + \frametitle{Implementierung} + \begin{itemize} + \item Diverse erfolglose Ansätze zur Implementierung von $\Lleftarrow$ + \item Erfolgreiche Implementierung dann mit algebraischen FST-Transformationen und als Komposition kleiner Typ-gesteuerter und generischer Teile + \note[item]{Demonstriert Erfolg von algebraischer Programmierung: nicht optimale, aber ähnliche, Komplexitätsklasse und dafür leichter verständlich} + \item Demonstriert Kodierung von algorithmischen Voraussetzungen in Typen (z.B. Determinismus von FST) + \note[item]{Korrekte Kodierung in Typen erlaubt auslassen von wenig interessanten Spezialfällen} + \end{itemize} +\end{frame} + +\begin{frame} + \frametitle{Weiterführendes} + \begin{itemize} + \item Analoges Verfahren für FSTs auch möglich; $\Lleftarrow$ und $\Rrightarrow$ dann symmetrisch und analog zum DFST-Fall von $\Lleftarrow$ + \item Edit-Lenses sind nicht kompatibel mit bestehenden Lens-Frameworks (in Haskell), da kodierung der Update-Propagatoren nicht kompatibel mit algebraischer Struktur der Edits + \item Linsen bilden große Familie von funktionalen, bidirektionalen Programmen z.B. + Imperative accessors für rein-funktionale Datenstrukturen und nützliche Verallgemeinerungen + \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 + \end{itemize} +\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 @@ +\begin{tikzpicture}[auto,sibling distance=3.5cm, level distance=3.5cm] + \node[] (top) { \begin{tikzpicture} + \node [fit={(0,0) (1,1.5)}, inner sep=0pt, thick, draw, label={$\text{s}\text{p}\text{p}$}] (rect) {}; + \path [draw](0.1,1) -- (-0.1,1) node[left]{$A$}; + \path [draw](0.1,0.25) -- (-0.1,0.25) node[left]{$B$}; + \path (0.75,1) node[above]{$aa$} [draw]-- (1.1,1) node[right]{$A$}; + \path (0.75,0.25) node[above]{$bb$} [draw]-- (1.1,0.25) node[right]{$B$}; + \path [draw](0.1,1) -- (0.60,0.25) -- (0.75,0.25); + \path [draw](0.1,0.25) -- (0.60,1) -- (0.75,1); + \end{tikzpicture} + } + child { node (l) { \begin{tikzpicture} + \node [fit={(0,0) (1,1.5)}, inner sep=0pt, thick, draw, label={$\text{s}\text{p}$}] (rect) {}; + \path [draw](0.1,1) -- (-0.1,1) node[left]{$A$}; + \path [draw](0.1,0.25) -- (-0.1,0.25) node[left]{$B$}; + \path (0.85,1) node[above]{$a$} [draw]-- (1.1,1) node[right]{$A$}; + \path (0.85,0.25) node[above]{$b$} [draw]-- (1.1,0.25) node[right]{$B$}; + \path [draw](0.1,1) -- (0.75,0.25) -- (0.85,0.25); + \path [draw](0.1,0.25) -- (0.75,1) -- (0.85,1); + \end{tikzpicture} + } + child { node (ll) { \begin{tikzpicture} + \node [fit={(0,0) (1,1.5)}, inner sep=0pt, thick, draw, label={$\text{s}$}] (rect) {}; + \path [draw](0.1,1) -- (-0.1,1) node[left]{$A$}; + \path [draw](0.1,0.25) -- (-0.1,0.25) node[left]{$B$}; + \path (0.85,1) node[above]{$\epsilon$} [draw]-- (1.1,1) node[right]{$A$}; + \path (0.85,0.25) node[above]{$\epsilon$} [draw]-- (1.1,0.25) node[right]{$B$}; + \path [draw](0.1,1) -- (0.75,0.25) -- (0.85,0.25); + \path [draw](0.1,0.25) -- (0.75,1) -- (0.85,1); + \end{tikzpicture} + } } + child { node (lr) { \begin{tikzpicture} + \node [fit={(0,0) (1,1.5)}, inner sep=0pt, thick, draw, label={$\text{p}$}] (rect) {}; + \path [draw](0.1,1) -- (-0.1,1) node[left]{$A$}; + \path [draw](0.1,0.25) -- (-0.1,0.25) node[left]{$B$}; + \path (0.85,1) node[above]{$a$} [draw]-- (1.1,1) node[right]{$A$}; + \path (0.85,0.25) node[above]{$b$} [draw]-- (1.1,0.25) node[right]{$B$}; + \path [draw](0.1,0.25) -- (0.75,0.25) -- (0.85,0.25); + \path [draw](0.1,1) -- (0.75,1) -- (0.85,1); + \end{tikzpicture} + } } + } + child { node (r) { \begin{tikzpicture} + \node [fit={(0,0) (1,1.5)}, inner sep=0pt, thick, draw, label={$\text{p}$}] (rect) {}; + \path [draw](0.1,1) -- (-0.1,1) node[left]{$A$}; + \path [draw](0.1,0.25) -- (-0.1,0.25) node[left]{$B$}; + \path (0.85,1) node[above]{$a$} [draw]-- (1.1,1) node[right]{$A$}; + \path (0.85,0.25) node[above]{$b$} [draw]-- (1.1,0.25) node[right]{$B$}; + \path [draw](0.1,0.25) -- (0.75,0.25) -- (0.85,0.25); + \path [draw](0.1,1) -- (0.75,1) -- (0.85,1); + \end{tikzpicture} + } }; +\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 @@ +\begin{tikzpicture}[node distance=2cm and 2cm,auto] + \tikzset{myptr/.style={decoration={markings,mark=at position 1 with % + {\arrow[scale=3,>=stealth]{>}}},postaction={decorate}}} + + \coordinate[] (e1) {}; + + \node[shape=rectangle, draw, left = of e1] (l1) + { \begin{tabular}{l l} + Schubert & 1797–1828 \\ + Shumann & 1810–1856 + \end{tabular} + }; + + \node[shape=rectangle, draw, right = of e1] (r1) + { \begin{tabular}{l l} + Schubert & Austria \\ + Shumann & Germany + \end{tabular} + }; + + \draw (l1) -- (e1) -- (r1); + + \coordinate[below = of e1,label={$\iota_L \rightarrow \iota_R$}] (e2) {}; + + \node[shape=rectangle, draw, left = of e2] (l2) + { \begin{tabular}{l l} + Schubert & 1797–1828 \\ + Shumann & 1810–1856 \\ + \textcolor{blue}{Monteverdi} & \textcolor{blue}{1567–1643} + \end{tabular} + }; + + \node[shape=rectangle, draw, right = of e2] (r2) + { \begin{tabular}{l l} + Schubert & Austria \\ + Shumann & Germany \\ + \textcolor{red}{Monteverdi} & \textcolor{red}{\emph{null}} + \end{tabular} + }; + + \draw[myptr] (l2) -- (e2) |- (r2); + + \coordinate[below = of e2,label={$\delta_R \leftarrow \delta_L$}] (e3) {}; + + \node[shape=rectangle, draw, left = of e3] (l3) + { \begin{tabular}{l l} + Schubert & 1797–1828 \\ + \textcolor{red}{Schumann} & 1810–1856 \\ + Monteverdi & 1567–1643 + \end{tabular} + }; + + \node[shape=rectangle, draw, right = of e3] (r3) + { \begin{tabular}{l l} + Schubert & Austria \\ + \textcolor{blue}{Schumann} & Germany \\ + Monteverdi & \textcolor{blue}{Italy} + \end{tabular} + }; + + \draw[myptr] (r3) -- (e3) |- (l3); +\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 @@ +\begin{tikzpicture}[->,auto,node distance=2.5cm] + \node[initial,state,accepting] (a) {$A$}; + \node[state,accepting] (b) [right of=a] {$B$}; + \path (a) edge [bend left=20] node [above] {$(\text{s}, \epsilon)$} (b) + (b) edge [bend left=20] node [below] {$(\text{s}, \epsilon)$} (a) + (a) edge [loop above] node {$(\text{p}, a)$} (a) + (b) edge [loop above] node {$(\text{p}, b)$} (b); +\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: extra-deps: - dotgen-0.4.2 + - brick-0.47 + - 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 @@ +presentation/switchdfst.tex +presentation/comptree.tex +screenshot.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 @@ gup -u literature.bibtex -cat >$1 <$1 <<'EOF' --- +title: Inkrementelle Parser als edit-lenses anhand von DFSTs +abstract: |- + Parser, die bekannte Texte nach einer kleinen Änderung neu analysieren können, ohne die ganze Eingabe erneut zu betrachten, nennt man inkrementell. + + Inkrementelle Parser sind seit den 1970er-Jahren bekannt und inzwischen umfangreich erforscht. + + Edit-lenses sind eine vergleichsweise neue algebraische Darstellung von Programmen, die algebraisch strukturierte Änderungen zwischen Strukturen übersetzen. + + 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. + + 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. + + Im Rahmen dessen stellen wir eine Implementierung von edit-lenses im Allgemeinen und unserem Verfahren in möglichst idiomatischem Haskell vor. lang: de-de link-citations: true bibliography: literature.bibtex -title: Iterative Parser als edit-lenses author: Gregor Kleen -date: \today +date: \formatdate{01}{03}{2019} +numbersections: true ... EOF 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 @@ #!/usr/bin/env zsh +gup -u intro.tex +gup -u implementation.tex + gup -u edit-lens/src/Control/Edit.lhs gup -u edit-lens/src/Control/Lens/Edit.lhs gup -u edit-lens/src/Control/FST.lhs gup -u edit-lens/src/Control/DFST.lhs gup -u edit-lens/src/Control/DFST/Lens.lhs +gup -u edit-lens/src/Control/FST/Lens.tex bDir=$(pwd) diff --git a/thesis.tex b/thesis.tex index 4156751..2f0346b 100644 --- a/thesis.tex +++ b/thesis.tex @@ -1,18 +1,52 @@ +\vfill + +\noindent Ich erkläre hiermit, dass ich die vorliegende Arbeit +selbstständig angefertigt, alle Zitate als solche kenntlich gemacht +sowie alle benutzten Quellen und Hilfsmittel angegeben habe. + +\bigskip + +\makebox[.5\linewidth][r]{}{\xleaders\hbox to .2em{\d{}}\hfill\d{}}\smallskip \\ +\hspace*{.5\linewidth}Gregor Kleen \\ +\hspace*{.5\linewidth}München, \today + +%% \bigskip\noindent München, \today + +%% \vspace{4ex}\noindent\makebox[7cm]{\dotfill} + + +\section{Einführung} +\input{./intro.tex} + \section{Edit-lenses} Ziel ist es zunächst edit-lenses alá \cite{hofmann2012edit} in Haskell zur Verfügung zu stellen. -Dabei werden wir die Definitionen aus \cite{hofmann2012edit} sowohl in natürlicher Sprache als auch in lauffähigem Haskell vorstellen: +Dabei werden wir die Definitionen aus \cite{hofmann2012edit} sowohl in natürlicher Sprache als auch in lauffähigem Haskell vorstellen. -\input{./edit-lens/src/Control/Edit.lhs} -\input{./edit-lens/src/Control/Lens/Edit.lhs} +\input{./edit-lens/src/Control/Edit.lhs.tex} +\input{./edit-lens/src/Control/Lens/Edit.lhs.tex} \section{Finite state transducers} -\input{./edit-lens/src/Control/FST.lhs} -\input{./edit-lens/src/Control/DFST.lhs} +\input{./edit-lens/src/Control/FST.lhs.tex} +\input{./edit-lens/src/Control/DFST.lhs.tex} \subsection{Edit-lenses für deterministic finite state transducers} -\input{./edit-lens/src/Control/DFST/Lens.lhs} + +\input{./edit-lens/src/Control/Edit/String.lhs.tex} +\input{./edit-lens/src/Control/DFST/Lens.lhs.tex} +\input{./edit-lens/src/Control/Edit/String/Affected.lhs.tex} \subsection{Ausblick: Edit-lenses für non-determinische finite state transducers} + \input{./edit-lens/src/Control/FST/Lens.tex} + +\section{Resultate} + +\subsection{Implementierung} + +\input{./implementation.tex} + +\subsection{Ausblick: Anwendbarkeit der Implementierung auf andere Parser} + +\input{./edit-lens/src/Control/Lens/Edit/ActionTree.lhs.tex} -- cgit v1.2.3