1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
|
\begin{code}
{-# LANGUAGE ScopedTypeVariables #-}
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 Data.Sequence (Seq(..), (><))
import qualified Data.Sequence as Seq
import Control.Monad.RWS.Strict
import Control.Monad.Writer.Class
import Control.Monad.Reader.Class
import Control.Monad.State.Class
import Control.Lens
import Control.Lens.Edit
import Data.Maybe
import Data.Foldable
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}
class Ord a => HasRanges a where
data Range a :: *
bounds :: Getter (Range a) (a, a)
range :: Iso' (Set a) (Range a)
within :: a -> Range a -> Bool
within x xs = Set.member x $ xs ^. from range
below :: a -> Range a -> Bool
below x xs = x < min
where (min, _) = xs ^. bounds
above :: a -> Range a -> Bool
above x xs = x > max
where (_, max) = xs ^. bounds
insert :: Range a -> a -> Range a
insert xs x = xs & under range (Set.insert x)
singleton :: a -> Range a
singleton = view range . Set.singleton
type PositionAction state output = Map state (ContainerEdits output, state)
data ContainerAction state input output
= CALeaf { caPos :: Position input
, caContent :: Content input
, caAction :: PositionAction state output
, caOutputPos :: Range Natural
}
| CABranch { caRange :: Range (Position input)
, caAction :: PositionAction state output
, caLeft :: ContainerAction state input output
, caRight :: ContainerAction state input output
, caOutputPos :: Range Natural
}
| CATip
-- type ContainerAction state input output = Map ((Position input, Seq (Content input), Position input)) (Map state (ContainerEdits output, state))
instance HasRanges Natural where
data Range Natural = NatInterval Natural Natural -- @NatInterval x y@ is the interval of natural numbers z such that x <= z < y
| NatSet (Set Natural)
bounds = to bounds'
where
bounds' (NatInterval min max) = (min, max)
bounds' (NatSet set) = (Set.findMin set, Set.findMax set)
range = iso fromSet toSet
where
fromSet set
| Set.null set = NatInterval 0 0
| otherwise = Set.foldl' insert (Set.empty ^. range) set
toSet (NatInterval x y)
| x < y = Set.fromAscList [x..pred y]
| otherwise = Set.empty
insert i@(NatInterval x y) z
| x < y
, z == pred x = NatInterval z y
| x < y
, z == succ y = NatInterval x z
| x >= y = NatInterval z (succ z)
| otherwise = NatSet $ (i ^. from range) `Set.union` Set.singleton z
insert (NatSet set) z = fromMaybe (NatSet $ Set.insert z set) $ foldlM insert' (NatInterval 0 0) set
where
insert' r x = case insert r x of
r'@(NatInterval _ _) -> Just r
_ -> Nothing
caRange' :: HasRanges (Position input) => ContainerAction state input output -> Range (Position input)
caRange' (CALeaf tPos _ _) = singleton tPos
caRange' (CABranch r _ _ _) = r
caRange' CATip = Set.empty ^. range
caAction' :: ContainerAction state input output -> PositionAction state output
caAction' CATip = Map.empty
caAction' x = caAction x
conc :: Ord state
=> PositionAction state output
-> PositionAction state output
-> PositionAction state output
f `conc` g = Map.fromList [ (st, fromMaybe (mempty, st') $ f !? st') | (st, x@(_, st')) <- Map.toAscList g ]
\end{code}
Für die Zwecke eines Container-Transducers sehen wir Container als eine Sequenz von edits auf $\text{init}$.
Das 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.
Die 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.
Zur Verarbeitung eines edits auf dem input lokalisieren wir zunächst dessen Wirkung in unserem Komplement-Baum.
Handelt 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.
Wir 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.
Beweisskizze:
Betrachte als input den trivialen container mit nur einer shape und darin belegten position.
Als edits auf dem Inhalt jenes containers nehmen wir Replace.
Nimm $e_o$ einen edit auf dem output-Container.
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)
Betrachte nun $\text{Replace}(c)$ gefolgt von $\text{Replace}(\text{init})$ unter $\text{diffContTrans}$ auf $\text{init}$.
Für das Ergebnis $e_o^{-1}$ muss gelten, dass $e_o^{-1} \circ e_o = \text{id}$.
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.
Beweis:
Nimm an edits auf dem output-container $N$ bilden einen Monoiden, jedoch keine Gruppe, d.h. es existiert $e_o$ sodass für alle $e_o^\prime$, edits auf dem output-container, gilt, dass $e_o \cdot e_o^prime \neq 1$.
Es sei $M$ der Container mit genau einer Shape und belegten Position und ${\text{init}, c}$ als Inhalt mit $\text{Replace}$ als Modul-Struktur.
Es sei $T$ der Container-Transducer mit zwei Zuständen $A$ und $B$ und folgender Transitions-Funktion:
\begin{align*}
(A, \init) & \mapsto (1_{\partial N}, A)
(A, c) & \mapsto ((\text{init}_N \cdot)^{-1}(e_o), B)
(B, \init) & \mapsto (1_{\partial N}, B)
(B, c) & \mapsto (1_{\partial N}, B)
\end{align*}
Wir bezeichnen mit $T(x)$ den output des transducers beim Lauf auf $x$.
Betrachte nun die edit-linse $(\Rrightarrow, \Lleftarrow)$ für $T$ und insbesondere $e_o^{-1} = \pi_2(\Rrightarrow(\pi_1(\Rrightarrow(\ground, \text{Replace}(c))), \text{Replace}(\text{init})))$.
Da $T(\text{init}_M) = \text{init}_N$ und $T(c) = e_o$ muss nun gelten, dass $e_o^{-1} \cdot e_o = \init_N$, also $\partial N$ eine Gruppe.
\begin{code}
diffContTrans :: forall state input output.
( Container input, Container output
, Ord state, Ord (Content input)
, HasRanges (Position input)
)
=> ContainerTransducer state input output
-> EditLens (ContainerAction state input output) (ContainerEdits input) (ContainerEdits output)
diffContTrans ContainerTransducer{..} = EditLens CATip forward backward
where
forward (cAct, Seq.Empty) = (cAct, Seq.empty)
forward (cAct, xs) = foldr' (\x (cAct', ys) -> over _2 (ys ><) $ go cAct' x) (cAct, Seq.empty) xs
where
go :: ContainerAction state input output
-> ContainerEdit input
-> (ContainerAction state input output, ContainerEdits output)
go ca Fail = (ca, Seq.singleton Fail)
go CATip _ = (CATip, mempty)
go ca@(CALeaf tPos content pAct) (ModContent pos cEdit)
| pos == tPos
, Just content' <- content `apply` cEdit
= (CALeaf tPos content' $ Map.fromAscList [ (s, a) | ((s, c), a) <- Map.toAscList ctTransition, c == content' ], undefined)
| otherwise = (ca, Seq.singleton Fail)
go ca@(CABranch range act left right) e@(ModContent pos _)
| pos `within` caRange' left
= let (left', es) = go left e in (CABranch range (caAction' right `conc` caAction' left') left' right, es)
| pos `within` caRange' right
= let (right', es) = go right e in (CABranch range (caAction' right' `conc` caAction' left) left right', es)
| otherwise = (ca, Seq.singleton Fail)
go cAct (ModShape cShape perm) = undefined
backward = undefined
\end{code}
|
