diff options
| -rw-r--r-- | edit-lens/package.yaml | 5 | ||||
| -rw-r--r-- | edit-lens/src/Control/Edit/Container.lhs | 32 | ||||
| -rw-r--r-- | edit-lens/src/Control/Edit/Container/Transducer.lhs | 63 | ||||
| -rw-r--r-- | edit-lens/src/Control/Lens/Edit.lhs | 5 | ||||
| -rw-r--r-- | stack.yaml | 3 |
5 files changed, 102 insertions, 6 deletions
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: | |||
| 21 | - GADTs | 21 | - GADTs |
| 22 | - TupleSections | 22 | - TupleSections |
| 23 | - ScopedTypeVariables | 23 | - ScopedTypeVariables |
| 24 | - RecordWildCards | ||
| 25 | - NamedFieldPuns | ||
| 26 | - ViewPatterns | ||
| 24 | source-dirs: src | 27 | source-dirs: src |
| 25 | dependencies: | 28 | dependencies: |
| 26 | - base | 29 | - base |
| 27 | - lens | 30 | - lens |
| 28 | - containers | 31 | - containers |
| 32 | - mtl | ||
| 29 | exposed-modules: | 33 | exposed-modules: |
| 30 | - Control.Edit | 34 | - Control.Edit |
| 31 | - Control.Edit.Container | 35 | - Control.Edit.Container |
| 36 | - Control.Edit.Container.Transducer | ||
| 32 | - Control.Lens.Edit | 37 | - Control.Lens.Edit |
| 33 | - Control.Lens.Edit.Generic | 38 | - Control.Lens.Edit.Generic |
| 34 | 39 | ||
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 @@ | |||
| 2 | \begin{code} | 2 | \begin{code} |
| 3 | module Control.Edit.Container | 3 | module Control.Edit.Container |
| 4 | ( Container(..), Shape, Content | 4 | ( Container(..), Shape, Content |
| 5 | , ContainerEdit(..) | 5 | , FoldableContainer(..) |
| 6 | , ContainerEdit(..), ContainerEdits | ||
| 6 | , module Control.Edit | 7 | , module Control.Edit |
| 7 | ) where | 8 | ) where |
| 8 | 9 | ||
| @@ -17,7 +18,7 @@ import Control.Lens | |||
| 17 | \end{code} | 18 | \end{code} |
| 18 | \end{comment} | 19 | \end{comment} |
| 19 | 20 | ||
| 20 | \citeauthor{hofmann2012edit} stellen \emph{container} vor—eine systematische Sicht auf Datenstrukturen, die es erlaubt eine generische edit-language zu definieren. | 21 | \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. |
| 21 | 22 | ||
| 22 | 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: | 23 | 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: |
| 23 | 24 | ||
| @@ -66,6 +67,12 @@ type Content c = Domain (ModContent c) | |||
| 66 | \end{code} | 67 | \end{code} |
| 67 | \end{defn} | 68 | \end{defn} |
| 68 | 69 | ||
| 70 | TODO | ||
| 71 | \begin{code} | ||
| 72 | class Container c => FoldableContainer c where | ||
| 73 | containerContent :: Fold c (Content c) | ||
| 74 | \end{code} | ||
| 75 | |||
| 69 | \begin{defn}[Klassifikation von edits auf shapes] | 76 | \begin{defn}[Klassifikation von edits auf shapes] |
| 70 | Für einen container-typ $(I, P, \text{postitions})$ klassifizieren wir die edits $\partial i \in \partial I$ wie folgt: | 77 | Für einen container-typ $(I, P, \text{postitions})$ klassifizieren wir die edits $\partial i \in \partial I$ wie folgt: |
| 71 | 78 | ||
| @@ -74,10 +81,29 @@ Für einen container-typ $(I, P, \text{postitions})$ klassifizieren wir die edit | |||
| 74 | \item[deletions] $\forall i \in \Dom (\partial i) \colon i \cdot \partial i \leq i$ | 81 | \item[deletions] $\forall i \in \Dom (\partial i) \colon i \cdot \partial i \leq i$ |
| 75 | \item[rearrangements] $\forall i \in \Dom (\partial i) \colon \size{\text{positions}(i \cdot \partial i)} = \size{\text{positions}(i)}$ | 82 | \item[rearrangements] $\forall i \in \Dom (\partial i) \colon \size{\text{positions}(i \cdot \partial i)} = \size{\text{positions}(i)}$ |
| 76 | \end{description} | 83 | \end{description} |
| 84 | |||
| 85 | Für ein rearrangement $\partial i$ nennen wir eine Funktion $f \colon I \to P \to P$ \emph{kompatibel} mit $\partial i$ gdw: | ||
| 86 | |||
| 87 | $$\forall i \in \Dom(\partial i) \colon f(i) \upharpoonright \text{positions}(i) \leftrightarrow \text{positions}(i \cdot \partial i)$$ | ||
| 88 | |||
| 89 | 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. | ||
| 77 | \end{defn} | 90 | \end{defn} |
| 78 | 91 | ||
| 79 | \begin{defn}[container-edits] | 92 | \begin{defn}[container-edits] |
| 80 | TODO | 93 | 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: |
| 94 | |||
| 95 | \[ | ||
| 96 | \begin{array}{lll} | ||
| 97 | & \{ \text{fail} \} & \\ | ||
| 98 | \cup & \{ \text{mod}(p, \partial x) & \mid p \in P, \partial x \in \partial X \} \\ | ||
| 99 | \cup & \{ \text{ins}(\partial i) & \mid \text{$\partial i$ ist insertion} \} \\ | ||
| 100 | \cup & \{ \text{del}(\partial i) & \mid \text{$\partial i$ ist deletion} \} \\ | ||
| 101 | \cup & \{ \text{rearr}(\partial i, f) & \mid \text{$\partial i$ ist rearrangement und kompatibel mit $f$} \} \\ | ||
| 102 | \end{array} | ||
| 103 | \] | ||
| 104 | |||
| 105 | In Haskell verzichten wir auf die Klassifikation von shape-edits und fassen daher $\text{ins}$, $\text{del}$, und $\text{rearr}$ zusammen. | ||
| 106 | |||
| 81 | \begin{code} | 107 | \begin{code} |
| 82 | data ContainerEdit c where | 108 | data ContainerEdit c where |
| 83 | Fail :: ContainerEdit c | 109 | 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 @@ | |||
| 1 | \begin{code} | ||
| 2 | {-# LANGUAGE TemplateHaskell #-} | ||
| 3 | |||
| 4 | module Control.Edit.Container.Transducer | ||
| 5 | ( ContainerTransducer{..}, ctStates | ||
| 6 | , runCT, stepCT | ||
| 7 | ) where | ||
| 8 | |||
| 9 | import Control.Edit.Container | ||
| 10 | import Data.Map.Strict (Map, (!?)) | ||
| 11 | import qualified Data.Map.Strict as Map | ||
| 12 | import Data.Set (Set) | ||
| 13 | import qualified Data.Set as Set | ||
| 14 | |||
| 15 | import Control.Monad.RWS.Strict | ||
| 16 | |||
| 17 | import Control.Monad.Writer.Class | ||
| 18 | import Control.Monad.Reader.Class | ||
| 19 | import Control.Monad.State.Class | ||
| 20 | |||
| 21 | import Control.Lens | ||
| 22 | |||
| 23 | import Data.Maybe | ||
| 24 | |||
| 25 | |||
| 26 | data ContainerTransducer state input output = ContainerTransducer | ||
| 27 | { ctInitialState :: state | ||
| 28 | , ctTransition :: Map (state, Content input) (ContainerEdits output, state) | ||
| 29 | -- ^ States are stable (and produce no output) by default | ||
| 30 | } | ||
| 31 | |||
| 32 | ctStates :: Ord state => ContainerTransducer state input output -> Set state | ||
| 33 | ctStates ContainerTransducer{..} = Map.foldrWithKey' (\(s1, _) (_, s2) -> Set.insert s1 . Set.insert s2) (Set.singleton ctInitialState) ctTransition | ||
| 34 | |||
| 35 | stepCT :: ( Ord state, Ord (Content input) | ||
| 36 | , MonadReader (ContainerTransducer state input output) m | ||
| 37 | , MonadState state m | ||
| 38 | , MonadWriter (ContainerEdits output) m | ||
| 39 | ) => Content input -> m () | ||
| 40 | stepCT x = do | ||
| 41 | ContainerTransducer{ ctTransition } <- ask | ||
| 42 | state <- get | ||
| 43 | let (output, newState) = fromMaybe (mempty, state) $ ctTransition !? (state, x) | ||
| 44 | put newState | ||
| 45 | tell output | ||
| 46 | |||
| 47 | runCT :: ( Ord state, Ord (Content input) | ||
| 48 | , FoldableContainer input | ||
| 49 | ) => ContainerTransducer state input output | ||
| 50 | -> input | ||
| 51 | -> ContainerEdits output | ||
| 52 | runCT ct@ContainerTransducer{ ctInitialState } input = runRWS (forMOf_ containerContent input stepCT) ct ctInitialState ^. _3 | ||
| 53 | \end{code} | ||
| 54 | |||
| 55 | \begin{code} | ||
| 56 | |||
| 57 | data CTComplement state input output = CTComplement | ||
| 58 | { | ||
| 59 | } | ||
| 60 | |||
| 61 | -- Define edit-lens as span | ||
| 62 | |||
| 63 | \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$ | |||
| 44 | 44 | ||
| 45 | Wir schreiben auch nur \emph{edit-lens} für den symmetrischen Fall\footnote{Für den asymmetrischen Fall siehe \cite{johnson2016unifying}}. | 45 | Wir schreiben auch nur \emph{edit-lens} für den symmetrischen Fall\footnote{Für den asymmetrischen Fall siehe \cite{johnson2016unifying}}. |
| 46 | 46 | ||
| 47 | 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): | 47 | 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): |
| 48 | 48 | ||
| 49 | \begin{code} | 49 | \begin{code} |
| 50 | data EditLens c m n where | 50 | data EditLens c m n where |
| @@ -59,6 +59,9 @@ class (Module m, Module n) => HasEditLens l m n | l -> m, l -> n where | |||
| 59 | propL :: l -> StateMonoidHom (Complement l) n m | 59 | propL :: l -> StateMonoidHom (Complement l) n m |
| 60 | -- ^ Map edits of 'n' to changes of 'm', maintaining some state from 'Complement l' | 60 | -- ^ Map edits of 'n' to changes of 'm', maintaining some state from 'Complement l' |
| 61 | 61 | ||
| 62 | editLens :: l -> EditLens (Complement l) m n | ||
| 63 | editLens l = EditLens (ground l) (propR l) (propL l) | ||
| 64 | |||
| 62 | -- | Inspect the components of an edit lens (e.g. 'EditLens') | 65 | -- | Inspect the components of an edit lens (e.g. 'EditLens') |
| 63 | instance (Module m, Module n) => HasEditLens (EditLens c m n) m n where | 66 | instance (Module m, Module n) => HasEditLens (EditLens c m n) m n where |
| 64 | type Complement (EditLens c m n) = c | 67 | type Complement (EditLens c m n) = c |
| @@ -1,7 +1,6 @@ | |||
| 1 | resolver: lts-9.9 | 1 | resolver: lts-10.0 |
| 2 | packages: | 2 | packages: |
| 3 | - edit-lens | 3 | - edit-lens |
| 4 | nix: | 4 | nix: |
| 5 | packages: [] | 5 | packages: [] |
| 6 | pure: false | ||
| 7 | shell-file: ./stack.nix | 6 | shell-file: ./stack.nix |
