diff options
Diffstat (limited to 'edit-lens/src')
| -rw-r--r-- | edit-lens/src/Control/Edit.lhs | 10 | ||||
| -rw-r--r-- | edit-lens/src/Control/Edit/Container.lhs | 74 | ||||
| -rw-r--r-- | edit-lens/src/Control/Edit/Tree.lhs | 9 |
3 files changed, 78 insertions, 15 deletions
diff --git a/edit-lens/src/Control/Edit.lhs b/edit-lens/src/Control/Edit.lhs index 7be8db4..11f2c12 100644 --- a/edit-lens/src/Control/Edit.lhs +++ b/edit-lens/src/Control/Edit.lhs | |||
| @@ -2,6 +2,7 @@ | |||
| 2 | \begin{code} | 2 | \begin{code} |
| 3 | module Control.Edit | 3 | module Control.Edit |
| 4 | ( Module(..) | 4 | ( Module(..) |
| 5 | , ModuleHom | ||
| 5 | ) where | 6 | ) where |
| 6 | \end{code} | 7 | \end{code} |
| 7 | \end{comment} | 8 | \end{comment} |
| @@ -26,12 +27,12 @@ Eine Repräsentierung als Typklasse bietet sich an: | |||
| 26 | \begin{code} | 27 | \begin{code} |
| 27 | class Monoid m => Module m where | 28 | class Monoid m => Module m where |
| 28 | type Domain m :: * | 29 | type Domain m :: * |
| 29 | apply :: Domain m -> m -> Maybe (Domain m) | 30 | apply :: m -> Domain m -> Maybe (Domain m) |
| 30 | -- ^ A partial monoid-action of `m` on `Domain m` | 31 | -- ^ A partial monoid-action of `m` on `Domain m` |
| 31 | -- | 32 | -- |
| 32 | -- prop> m `apply` mempty = m | 33 | -- prop> m `apply` mempty = m |
| 33 | -- prop> m `apply` (e `mappend` e') = (m `apply` e) `apply` e' | 34 | -- prop> m `apply` (e `mappend` e') = (m `apply` e) `apply` e' |
| 34 | init :: Domain m | 35 | initial :: Domain m |
| 35 | -- ^ 'init @m' (TypeApplication) is the initial element of 'm' | 36 | -- ^ 'init @m' (TypeApplication) is the initial element of 'm' |
| 36 | divInit :: Domain m -> m | 37 | divInit :: Domain m -> m |
| 37 | -- ^ Calculate a representation of an element of 'Domain m' in 'Del m' | 38 | -- ^ Calculate a representation of an element of 'Domain m' in 'Del m' |
| @@ -42,7 +43,6 @@ class Monoid m => Module m where | |||
| 42 | 43 | ||
| 43 | Wir weichen von der originalen Definition von Moduln aus \cite{hofmann2012edit} darin ab, dass wir für das ausgezeichnete Element $\init_X$ des Trägers explizit (und konstruktiv) fordern, dass es ein schwach-initiales Element bzgl. der Monoidwirkung sei. | 44 | Wir weichen von der originalen Definition von Moduln aus \cite{hofmann2012edit} darin ab, dass wir für das ausgezeichnete Element $\init_X$ des Trägers explizit (und konstruktiv) fordern, dass es ein schwach-initiales Element bzgl. der Monoidwirkung sei. |
| 44 | 45 | ||
| 45 | \begin{comment} | ||
| 46 | \begin{defn}[Modulhomomorphismen] | 46 | \begin{defn}[Modulhomomorphismen] |
| 47 | Unter einem Modulhomomorphismus zwischen Moduln $M$ und $M^\prime$ verstehen wir ein Paar $(f, \phi$) bestehend aus Abbildungen $f \colon \Dom M \to \Dom M^\prime$ und $\phi \colon \partial M \to \partial M^\prime$, sodass gilt: | 47 | Unter einem Modulhomomorphismus zwischen Moduln $M$ und $M^\prime$ verstehen wir ein Paar $(f, \phi$) bestehend aus Abbildungen $f \colon \Dom M \to \Dom M^\prime$ und $\phi \colon \partial M \to \partial M^\prime$, sodass gilt: |
| 48 | \begin{itemize} | 48 | \begin{itemize} |
| @@ -61,11 +61,9 @@ Unter einem Modulhomomorphismus zwischen Moduln $M$ und $M^\prime$ verstehen wir | |||
| 61 | \end{itemize} | 61 | \end{itemize} |
| 62 | 62 | ||
| 63 | \begin{code} | 63 | \begin{code} |
| 64 | {- | 64 | -- | A homomorphism between 'Module's |
| 65 | data ModuleHom m n where | 65 | data ModuleHom m n where |
| 66 | ModuleHom :: (Module m, Module n) => (Domain m -> Domain n) -> (m -> n) -> ModuleHom m n | 66 | ModuleHom :: (Module m, Module n) => (Domain m -> Domain n) -> (m -> n) -> ModuleHom m n |
| 67 | -} | ||
| 68 | \end{code} | 67 | \end{code} |
| 69 | \end{defn} | 68 | \end{defn} |
| 70 | \end{comment} | ||
| 71 | 69 | ||
diff --git a/edit-lens/src/Control/Edit/Container.lhs b/edit-lens/src/Control/Edit/Container.lhs new file mode 100644 index 0000000..7d0d57c --- /dev/null +++ b/edit-lens/src/Control/Edit/Container.lhs | |||
| @@ -0,0 +1,74 @@ | |||
| 1 | \begin{comment} | ||
| 2 | \begin{code} | ||
| 3 | module Control.Edit.Container | ||
| 4 | ( Container(..), Shape, Content | ||
| 5 | , ContainerEdit(..) | ||
| 6 | ) where | ||
| 7 | |||
| 8 | import Control.Edit | ||
| 9 | import Data.Set (Set) | ||
| 10 | import Data.Sequence (Seq) | ||
| 11 | import qualified Data.Sequence as Seq | ||
| 12 | |||
| 13 | import Control.Monad | ||
| 14 | |||
| 15 | import Control.Lens | ||
| 16 | \end{code} | ||
| 17 | \end{comment} | ||
| 18 | |||
| 19 | \begin{defn}[Container] | ||
| 20 | \begin{code} | ||
| 21 | class ( Module (ModShape c) | ||
| 22 | , Module (ModContent c) | ||
| 23 | , Ord (Position c) | ||
| 24 | ) => Container c where | ||
| 25 | type ModShape c :: * | ||
| 26 | type Position c :: * | ||
| 27 | type ModContent c :: * | ||
| 28 | positions :: Shape c -> Set (Position c) | ||
| 29 | deconstructed :: Iso' c (Shape c, Position c -> Content c) | ||
| 30 | |||
| 31 | constructed :: Container c => Iso' (Shape c, Position c -> Content c) c | ||
| 32 | constructed = from deconstructed | ||
| 33 | |||
| 34 | type Shape c = Domain (ModShape c) | ||
| 35 | type Content c = Domain (ModContent c) | ||
| 36 | \end{code} | ||
| 37 | \end{defn} | ||
| 38 | |||
| 39 | \begin{defn}[container-edits] | ||
| 40 | \begin{code} | ||
| 41 | data ContainerEdit c where | ||
| 42 | Fail :: ContainerEdit c | ||
| 43 | ModContent :: Position c -> ModContent c -> ContainerEdit c | ||
| 44 | ModShape :: ModShape c -> (Shape c -> Position c -> Position c) -> ContainerEdit c | ||
| 45 | \end{code} | ||
| 46 | \end{defn} | ||
| 47 | |||
| 48 | \begin{defn}[Wirkung von container-edits] | ||
| 49 | \begin{code} | ||
| 50 | instance Container c => Module (Seq (ContainerEdit c)) where | ||
| 51 | type Domain (Seq (ContainerEdit c)) = c | ||
| 52 | apply fs = over mapped (view constructed) . flip (foldM apply') fs . view deconstructed | ||
| 53 | where | ||
| 54 | apply' :: Container c | ||
| 55 | => (Shape c, Position c -> Content c) | ||
| 56 | -> ContainerEdit c | ||
| 57 | -> Maybe (Shape c, Position c -> Content c) | ||
| 58 | apply' _ Fail = Nothing | ||
| 59 | apply' (s, cf) (ModContent p dc) = do | ||
| 60 | c' <- dc `apply` cf p | ||
| 61 | let cf' x | ||
| 62 | | x == p = c' | ||
| 63 | | otherwise = cf x | ||
| 64 | return (s, cf') | ||
| 65 | apply' (s, cf) (ModShape ds dcf) = (, cf . dcf s) <$> ds `apply` s | ||
| 66 | initial = view constructed (initial @(ModShape c), \_ -> initial @(ModContent c)) | ||
| 67 | divInit x = | ||
| 68 | let | ||
| 69 | x'@(s, cf) = x ^. deconstructed | ||
| 70 | (ds, dcf) = over _1 divInit $ over (_2.mapped) divInit x' | ||
| 71 | in | ||
| 72 | foldMap (\p -> Seq.singleton . ModContent p $ dcf p) (positions @c s) |> (ModShape ds $ const id) | ||
| 73 | \end{code} | ||
| 74 | \end{defn} | ||
diff --git a/edit-lens/src/Control/Edit/Tree.lhs b/edit-lens/src/Control/Edit/Tree.lhs deleted file mode 100644 index 28320c5..0000000 --- a/edit-lens/src/Control/Edit/Tree.lhs +++ /dev/null | |||
| @@ -1,9 +0,0 @@ | |||
| 1 | \begin{comment} | ||
| 2 | \begin{code} | ||
| 3 | module Control.Edit.Tree | ||
| 4 | ( | ||
| 5 | ) where | ||
| 6 | |||
| 7 | import Control.Edit | ||
| 8 | \end{code} | ||
| 9 | \end{comment} | ||
