summaryrefslogtreecommitdiff
path: root/edit-lens
diff options
context:
space:
mode:
Diffstat (limited to 'edit-lens')
-rw-r--r--edit-lens/src/Control/Edit/Container/Transducer.lhs139
1 files changed, 133 insertions, 6 deletions
diff --git a/edit-lens/src/Control/Edit/Container/Transducer.lhs b/edit-lens/src/Control/Edit/Container/Transducer.lhs
index 0173cc4..9db26db 100644
--- a/edit-lens/src/Control/Edit/Container/Transducer.lhs
+++ b/edit-lens/src/Control/Edit/Container/Transducer.lhs
@@ -1,8 +1,8 @@
1\begin{code} 1\begin{code}
2{-# LANGUAGE TemplateHaskell #-} 2{-# LANGUAGE ScopedTypeVariables #-}
3 3
4module Control.Edit.Container.Transducer 4module Control.Edit.Container.Transducer
5 ( ContainerTransducer{..}, ctStates 5 ( ContainerTransducer(..), ctStates
6 , runCT, stepCT 6 , runCT, stepCT
7 ) where 7 ) where
8 8
@@ -11,6 +11,8 @@ import Data.Map.Strict (Map, (!?))
11import qualified Data.Map.Strict as Map 11import qualified Data.Map.Strict as Map
12import Data.Set (Set) 12import Data.Set (Set)
13import qualified Data.Set as Set 13import qualified Data.Set as Set
14import Data.Sequence (Seq(..), (><))
15import qualified Data.Sequence as Seq
14 16
15import Control.Monad.RWS.Strict 17import Control.Monad.RWS.Strict
16 18
@@ -19,8 +21,10 @@ import Control.Monad.Reader.Class
19import Control.Monad.State.Class 21import Control.Monad.State.Class
20 22
21import Control.Lens 23import Control.Lens
24import Control.Lens.Edit
22 25
23import Data.Maybe 26import Data.Maybe
27import Data.Foldable
24 28
25 29
26data ContainerTransducer state input output = ContainerTransducer 30data ContainerTransducer state input output = ContainerTransducer
@@ -53,11 +57,134 @@ runCT ct@ContainerTransducer{ ctInitialState } input = runRWS (forMOf_ container
53\end{code} 57\end{code}
54 58
55\begin{code} 59\begin{code}
60class Ord a => HasRanges a where
61 data Range a :: *
62 bounds :: Getter (Range a) (a, a)
63 range :: Iso' (Set a) (Range a)
64 within :: a -> Range a -> Bool
65 within x xs = Set.member x $ xs ^. from range
66 below :: a -> Range a -> Bool
67 below x xs = x < min
68 where (min, _) = xs ^. bounds
69 above :: a -> Range a -> Bool
70 above x xs = x > max
71 where (_, max) = xs ^. bounds
72 insert :: Range a -> a -> Range a
73 insert xs x = xs & under range (Set.insert x)
74 singleton :: a -> Range a
75 singleton = view range . Set.singleton
56 76
57data CTComplement state input output = CTComplement 77type PositionAction state output = Map state (ContainerEdits output, state)
58 { 78
59 } 79data ContainerAction state input output
80 = CALeaf { caPos :: Position input
81 , caContent :: Content input
82 , caAction :: PositionAction state output
83 , caOutputPos :: Range Natural
84 }
85 | CABranch { caRange :: Range (Position input)
86 , caAction :: PositionAction state output
87 , caLeft :: ContainerAction state input output
88 , caRight :: ContainerAction state input output
89 , caOutputPos :: Range Natural
90 }
91 | CATip
92
93-- type ContainerAction state input output = Map ((Position input, Seq (Content input), Position input)) (Map state (ContainerEdits output, state))
94
95instance HasRanges Natural where
96 data Range Natural = NatInterval Natural Natural -- @NatInterval x y@ is the interval of natural numbers z such that x <= z < y
97 | NatSet (Set Natural)
98 bounds = to bounds'
99 where
100 bounds' (NatInterval min max) = (min, max)
101 bounds' (NatSet set) = (Set.findMin set, Set.findMax set)
102 range = iso fromSet toSet
103 where
104 fromSet set
105 | Set.null set = NatInterval 0 0
106 | otherwise = Set.foldl' insert (Set.empty ^. range) set
107 toSet (NatInterval x y)
108 | x < y = Set.fromAscList [x..pred y]
109 | otherwise = Set.empty
110 insert i@(NatInterval x y) z
111 | x < y
112 , z == pred x = NatInterval z y
113 | x < y
114 , z == succ y = NatInterval x z
115 | x >= y = NatInterval z (succ z)
116 | otherwise = NatSet $ (i ^. from range) `Set.union` Set.singleton z
117 insert (NatSet set) z = fromMaybe (NatSet $ Set.insert z set) $ foldlM insert' (NatInterval 0 0) set
118 where
119 insert' r x = case insert r x of
120 r'@(NatInterval _ _) -> Just r
121 _ -> Nothing
122
123caRange' :: HasRanges (Position input) => ContainerAction state input output -> Range (Position input)
124caRange' (CALeaf tPos _ _) = singleton tPos
125caRange' (CABranch r _ _ _) = r
126caRange' CATip = Set.empty ^. range
127
128caAction' :: ContainerAction state input output -> PositionAction state output
129caAction' CATip = Map.empty
130caAction' x = caAction x
131
132conc :: Ord state
133 => PositionAction state output
134 -> PositionAction state output
135 -> PositionAction state output
136f `conc` g = Map.fromList [ (st, fromMaybe (mempty, st') $ f !? st') | (st, x@(_, st')) <- Map.toAscList g ]
60 137
61-- Define edit-lens as span 138\end{code}
139
140Für die Zwecke eines Container-Transducers sehen wir Container als eine Sequenz von edits auf $\text{init}$.
141
142Das Komplement der transducer-edit-linse ist ein binärbaum dessen Zweige beschriftet sind mit der vom Teilbaum betrachteten input Container-Positionen, der Wirkung des gesamten Teilbaums (d.h. die Transitionsfunktion für den Zustand und den produzierten Output (eine Teilsequenz der edits des output containers)), und den betroffenen output Positionen.
143Die Blätter beschriften wir mit einer einzigen betrachteten Position im input-Container, dem beim verarbeiten angetroffenen Inhalt, der Wirkung dieses konkreten Inhalts, und den betroffenen output Positionen.
144
145Zur Verarbeitung eines edits auf dem input lokalisieren wir zunächst dessen Wirkung in unserem Komplement-Baum.
146Handelt es sich um einen edit auf einer Position im input können wir für das betroffene Blatt eine neue Wirkung berechnen, anhand der Transitionsfunktion des transducers und dem im komplement gespeicherten alten Wert.
147Wir können nun nicht vermeiden von den output edits zu fordern eine Gruppe zu sein, da wir gezwungen sind einen edit zu produzieren, der auf dem Resultat des vorherigen Laufes, zumindest den alten, bei der betroffenen transition edit rückgängig zu machen.
148
149Beweisskizze:
150 Betrachte als input den trivialen container mit nur einer shape und darin belegten position.
151 Als edits auf dem Inhalt jenes containers nehmen wir Replace.
152 Nimm $e_o$ einen edit auf dem output-Container.
153 Obda ist $e_o$ die Wirkung von $\text{Replace}(c)$ unter $\text{diffContTrans}$ auf $(\text{init}, \text{init_C}, \text{init})$ (Konstruiere hierfür einen geeigneten Transducer)
154 Betrachte nun $\text{Replace}(c)$ gefolgt von $\text{Replace}(\text{init})$ unter $\text{diffContTrans}$ auf $\text{init}$.
155 Für das Ergebnis $e_o^{-1}$ muss gelten, dass $e_o^{-1} \circ e_o = \text{id}$.
156 Wir haben also Inverse für beliebige Elemente des edit-monoiden auf dem Output; also eine Gruppe auf edits auf dem Output die kompatibel ist mit der bestehenden monoid struktur.
157
158\begin{code}
159diffContTrans :: forall state input output.
160 ( Container input, Container output
161 , Ord state, Ord (Content input)
162 , HasRanges (Position input)
163 )
164 => ContainerTransducer state input output
165 -> EditLens (ContainerAction state input output) (ContainerEdits input) (ContainerEdits output)
166diffContTrans ContainerTransducer{..} = EditLens CATip forward backward
167 where
168 forward (cAct, Seq.Empty) = (cAct, Seq.empty)
169 forward (cAct, xs) = foldr' (\x (cAct', ys) -> over _2 (ys ><) $ go cAct' x) (cAct, Seq.empty) xs
170 where
171 go :: ContainerAction state input output
172 -> ContainerEdit input
173 -> (ContainerAction state input output, ContainerEdits output)
174 go ca Fail = (ca, Seq.singleton Fail)
175 go CATip _ = (CATip, mempty)
176 go ca@(CALeaf tPos content pAct) (ModContent pos cEdit)
177 | pos == tPos
178 , Just content' <- content `apply` cEdit
179 = (CALeaf tPos content' $ Map.fromAscList [ (s, a) | ((s, c), a) <- Map.toAscList ctTransition, c == content' ], undefined)
180 | otherwise = (ca, Seq.singleton Fail)
181 go ca@(CABranch range act left right) e@(ModContent pos _)
182 | pos `within` caRange' left
183 = let (left', es) = go left e in (CABranch range (caAction' right `conc` caAction' left') left' right, es)
184 | pos `within` caRange' right
185 = let (right', es) = go right e in (CABranch range (caAction' right' `conc` caAction' left) left right', es)
186 | otherwise = (ca, Seq.singleton Fail)
187 go cAct (ModShape cShape perm) = undefined
62 188
189 backward = undefined
63\end{code} 190\end{code}