From fc9bdae87b05d1d1c99265ec8b370b37422b01d4 Mon Sep 17 00:00:00 2001 From: Gregor Kleen Date: Wed, 20 Dec 2017 15:29:54 +0100 Subject: Work on container transducers --- edit-lens/package.yaml | 5 ++ edit-lens/src/Control/Edit/Container.lhs | 32 +++++++++-- .../src/Control/Edit/Container/Transducer.lhs | 63 ++++++++++++++++++++++ edit-lens/src/Control/Lens/Edit.lhs | 5 +- stack.yaml | 3 +- 5 files changed, 102 insertions(+), 6 deletions(-) create mode 100644 edit-lens/src/Control/Edit/Container/Transducer.lhs diff --git a/edit-lens/package.yaml b/edit-lens/package.yaml index 61d1285..5bf7fba 100644 --- a/edit-lens/package.yaml +++ b/edit-lens/package.yaml @@ -21,14 +21,19 @@ library: - GADTs - TupleSections - ScopedTypeVariables + - RecordWildCards + - NamedFieldPuns + - ViewPatterns source-dirs: src dependencies: - base - lens - containers + - mtl exposed-modules: - Control.Edit - Control.Edit.Container + - Control.Edit.Container.Transducer - Control.Lens.Edit - Control.Lens.Edit.Generic diff --git a/edit-lens/src/Control/Edit/Container.lhs b/edit-lens/src/Control/Edit/Container.lhs index 32ec479..09040c8 100644 --- a/edit-lens/src/Control/Edit/Container.lhs +++ b/edit-lens/src/Control/Edit/Container.lhs @@ -2,7 +2,8 @@ \begin{code} module Control.Edit.Container ( Container(..), Shape, Content - , ContainerEdit(..) + , FoldableContainer(..) + , ContainerEdit(..), ContainerEdits , module Control.Edit ) where @@ -17,7 +18,7 @@ import Control.Lens \end{code} \end{comment} -\citeauthor{hofmann2012edit} stellen \emph{container} vor—eine systematische Sicht auf Datenstrukturen, die es erlaubt eine generische edit-language zu definieren. +\citeauthor{hofmann2012edit} stellen \emph{container} vor—eine systematische Sicht auf Datenstrukturen, die es erlaubt eine generische edit-language zu definieren, im folgenden wiederholen wir die dortigen Definitionen. Intuitiv zerlegt die Darstellung als container eine polymorphe Datenstruktur in ihre \emph{Form} (\emph{shape}), ordnet der Form eine Menge von \emph{Positionen} zu und belegt jede Position mit einem Wert: @@ -66,6 +67,12 @@ type Content c = Domain (ModContent c) \end{code} \end{defn} +TODO +\begin{code} +class Container c => FoldableContainer c where + containerContent :: Fold c (Content c) +\end{code} + \begin{defn}[Klassifikation von edits auf shapes] Für einen container-typ $(I, P, \text{postitions})$ klassifizieren wir die edits $\partial i \in \partial I$ wie folgt: @@ -74,10 +81,29 @@ Für einen container-typ $(I, P, \text{postitions})$ klassifizieren wir die edit \item[deletions] $\forall i \in \Dom (\partial i) \colon i \cdot \partial i \leq i$ \item[rearrangements] $\forall i \in \Dom (\partial i) \colon \size{\text{positions}(i \cdot \partial i)} = \size{\text{positions}(i)}$ \end{description} + +Für ein rearrangement $\partial i$ nennen wir eine Funktion $f \colon I \to P \to P$ \emph{kompatibel} mit $\partial i$ gdw: + +$$\forall i \in \Dom(\partial i) \colon f(i) \upharpoonright \text{positions}(i) \leftrightarrow \text{positions}(i \cdot \partial i)$$ + +D.h. $f(i)$ ist, eingeschränkt auf die Positionen, die in $i$ belegt sind, eine Bijektion auf die in $i \cdot \partial i$ belegten Positionen. \end{defn} \begin{defn}[container-edits] - TODO + Für eine Instanz eines container-typs $(I, P, \text{positions})$ dessen Inhalt Elemente eines Moduls $X$ sind können wir aus den edits auf die shapes $\partial I$ des containers und denen auf seinen Inhalt $\partial X$ edits für den container konstruieren: + +\[ +\begin{array}{lll} + & \{ \text{fail} \} & \\ + \cup & \{ \text{mod}(p, \partial x) & \mid p \in P, \partial x \in \partial X \} \\ + \cup & \{ \text{ins}(\partial i) & \mid \text{$\partial i$ ist insertion} \} \\ + \cup & \{ \text{del}(\partial i) & \mid \text{$\partial i$ ist deletion} \} \\ + \cup & \{ \text{rearr}(\partial i, f) & \mid \text{$\partial i$ ist rearrangement und kompatibel mit $f$} \} \\ +\end{array} +\] + +In Haskell verzichten wir auf die Klassifikation von shape-edits und fassen daher $\text{ins}$, $\text{del}$, und $\text{rearr}$ zusammen. + \begin{code} data ContainerEdit c where Fail :: ContainerEdit c diff --git a/edit-lens/src/Control/Edit/Container/Transducer.lhs b/edit-lens/src/Control/Edit/Container/Transducer.lhs new file mode 100644 index 0000000..0173cc4 --- /dev/null +++ b/edit-lens/src/Control/Edit/Container/Transducer.lhs @@ -0,0 +1,63 @@ +\begin{code} +{-# LANGUAGE TemplateHaskell #-} + +module Control.Edit.Container.Transducer + ( ContainerTransducer{..}, ctStates + , runCT, stepCT + ) where + +import Control.Edit.Container +import Data.Map.Strict (Map, (!?)) +import qualified Data.Map.Strict as Map +import Data.Set (Set) +import qualified Data.Set as Set + +import Control.Monad.RWS.Strict + +import Control.Monad.Writer.Class +import Control.Monad.Reader.Class +import Control.Monad.State.Class + +import Control.Lens + +import Data.Maybe + + +data ContainerTransducer state input output = ContainerTransducer + { ctInitialState :: state + , ctTransition :: Map (state, Content input) (ContainerEdits output, state) + -- ^ States are stable (and produce no output) by default + } + +ctStates :: Ord state => ContainerTransducer state input output -> Set state +ctStates ContainerTransducer{..} = Map.foldrWithKey' (\(s1, _) (_, s2) -> Set.insert s1 . Set.insert s2) (Set.singleton ctInitialState) ctTransition + +stepCT :: ( Ord state, Ord (Content input) + , MonadReader (ContainerTransducer state input output) m + , MonadState state m + , MonadWriter (ContainerEdits output) m + ) => Content input -> m () +stepCT x = do + ContainerTransducer{ ctTransition } <- ask + state <- get + let (output, newState) = fromMaybe (mempty, state) $ ctTransition !? (state, x) + put newState + tell output + +runCT :: ( Ord state, Ord (Content input) + , FoldableContainer input + ) => ContainerTransducer state input output + -> input + -> ContainerEdits output +runCT ct@ContainerTransducer{ ctInitialState } input = runRWS (forMOf_ containerContent input stepCT) ct ctInitialState ^. _3 +\end{code} + +\begin{code} + +data CTComplement state input output = CTComplement + { + } + +-- Define edit-lens as span + +\end{code} diff --git a/edit-lens/src/Control/Lens/Edit.lhs b/edit-lens/src/Control/Lens/Edit.lhs index 0a679cb..096b53d 100644 --- a/edit-lens/src/Control/Lens/Edit.lhs +++ b/edit-lens/src/Control/Lens/Edit.lhs @@ -44,7 +44,7 @@ Für Moduln $M$ und $N$ besteht eine symmetrische edit-lens zwischen $M$ und $N$ Wir schreiben auch nur \emph{edit-lens} für den symmetrischen Fall\footnote{Für den asymmetrischen Fall siehe \cite{johnson2016unifying}}. -In Haskell erwähnen wir die Konsistenzrelation nicht in der Erwartung, dass $\Rrightarrow$ und $\Lleftarrow$ nur auf konsistente Zustände angewandt werden (und somit auch entweder einen konsistenten Zustand erzeugen oder nichtt definiert sind): +In Haskell erwähnen wir die Konsistenzrelation nicht in der Erwartung, dass $\Rrightarrow$ und $\Lleftarrow$ nur auf konsistente Zustände angewandt werden (und somit auch entweder einen konsistenten Zustand erzeugen oder nicht definiert sind): \begin{code} data EditLens c m n where @@ -59,6 +59,9 @@ class (Module m, Module n) => HasEditLens l m n | l -> m, l -> n where propL :: l -> StateMonoidHom (Complement l) n m -- ^ Map edits of 'n' to changes of 'm', maintaining some state from 'Complement l' + editLens :: l -> EditLens (Complement l) m n + editLens l = EditLens (ground l) (propR l) (propL l) + -- | Inspect the components of an edit lens (e.g. 'EditLens') instance (Module m, Module n) => HasEditLens (EditLens c m n) m n where type Complement (EditLens c m n) = c diff --git a/stack.yaml b/stack.yaml index 125d9fb..6077ba9 100644 --- a/stack.yaml +++ b/stack.yaml @@ -1,7 +1,6 @@ -resolver: lts-9.9 +resolver: lts-10.0 packages: - edit-lens nix: packages: [] - pure: false shell-file: ./stack.nix -- cgit v1.2.3