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 |