1 {-# LANGUAGE MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, TypeFamilies, RankNTypes #-}
2 -----------------------------------------------------------------------------
4 -- Module : GArrowSkeleton
6 -- License : public domain
8 -- Maintainer : Adam Megacz <megacz@acm.org>
9 -- Stability : experimental
11 -- | Sometimes it is convenient to be able to get your hands on the
12 -- explicit boxes-and-wires representation of a GArrow-polymorphic
13 -- term. GArrowSkeleton lets you do that.
15 -- HOWEVER: technically this instance violates the laws (and RULEs)
16 -- for Control.Category; the compiler might choose to optimize (f >>>
17 -- id) into f, and this optimization would produce a change in
18 -- behavior below -- you'd get (GAS_comp f GAS_id) instead of f. In
19 -- practice this means that the user must be prepared for the skeleton
20 -- TikZ diagram to be a nondeterministically-chosen boxes-and-wires
21 -- diagram which is *equivalent to* the term, rather than structurally
22 -- exactly equal to it.
24 -- A normal form theorem and normalization algorithm are being prepared.
26 module GArrowSkeleton (GArrowSkeleton(..), mkSkeleton, OptimizeFlag(..), optimize, beautify)
28 import Prelude hiding ( id, (.), lookup, repeat )
29 import Control.Category
32 import Control.Monad.State
33 import GArrowInclusion
35 data GArrowSkeleton m :: * -> * -> *
37 GAS_id :: GArrowSkeleton m x x
38 GAS_comp :: GArrowSkeleton m x y -> GArrowSkeleton m y z -> GArrowSkeleton m x z
39 GAS_first :: GArrowSkeleton m x y -> GArrowSkeleton m (x,z) (y,z)
40 GAS_second :: GArrowSkeleton m x y -> GArrowSkeleton m (z,x) (z,y)
41 GAS_cancell :: GArrowSkeleton m ((),x) x
42 GAS_cancelr :: GArrowSkeleton m (x,()) x
43 GAS_uncancell :: GArrowSkeleton m x ((),x)
44 GAS_uncancelr :: GArrowSkeleton m x (x,())
45 GAS_assoc :: GArrowSkeleton m ((x,y),z) (x,(y,z))
46 GAS_unassoc :: GArrowSkeleton m (x,(y,z)) ((x,y),z)
47 GAS_drop :: GArrowSkeleton m x ()
48 GAS_copy :: GArrowSkeleton m x (x,x)
49 GAS_swap :: GArrowSkeleton m (x,y) (y,x)
50 GAS_loopl :: GArrowSkeleton m (z,x) (z,y) -> GArrowSkeleton m x y
51 GAS_loopr :: GArrowSkeleton m (x,z) (y,z) -> GArrowSkeleton m x y
52 GAS_misc :: m x y -> GArrowSkeleton m x y
54 instance Category (GArrowSkeleton m) where
58 instance GArrow (GArrowSkeleton m) (,) () where
60 ga_second = GAS_second
61 ga_cancell = GAS_cancell
62 ga_cancelr = GAS_cancelr
63 ga_uncancell = GAS_uncancell
64 ga_uncancelr = GAS_uncancelr
66 ga_unassoc = GAS_unassoc
68 instance GArrowDrop (GArrowSkeleton m) (,) () where
71 instance GArrowCopy (GArrowSkeleton m) (,) () where
74 instance GArrowSwap (GArrowSkeleton m) (,) () where
77 instance GArrowLoop (GArrowSkeleton m) (,) () where
81 type instance GArrowTensor (GArrowSkeleton m) = (,)
82 type instance GArrowUnit (GArrowSkeleton m) = ()
83 type instance GArrowExponent (GArrowSkeleton m) = (->)
85 instance GArrowCopyDropSwapLoop (GArrowSkeleton m)
87 instance GArrowInclusion (GArrowSkeleton m) (,) () m where
91 -- | Simple structural equality on skeletons. NOTE: two skeletons
92 -- with the same shape but different types will nonetheless be "equal";
93 -- there's no way around this since types are gone at runtime.
95 instance Eq ((GArrowSkeleton m) a b)
99 (===) :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) c d -> Bool
100 (GAS_id ) === (GAS_id ) = True
101 (GAS_comp g f) === (GAS_comp g' f') = f===f' && g===g'
102 (GAS_first f) === (GAS_first f') = f===f'
103 (GAS_second f) === (GAS_second f') = f===f'
104 GAS_cancell === GAS_cancell = True
105 GAS_cancelr === GAS_cancelr = True
106 GAS_uncancell === GAS_uncancell = True
107 GAS_uncancelr === GAS_uncancelr = True
108 GAS_drop === GAS_drop = True
109 GAS_copy === GAS_copy = True
110 GAS_swap === GAS_swap = True
111 GAS_assoc === GAS_assoc = True
112 GAS_unassoc === GAS_unassoc = True
113 (GAS_loopl f) === (GAS_loopl f') = f === f'
114 (GAS_loopr f) === (GAS_loopr f') = f === f'
115 (GAS_misc _) === (GAS_misc _) = True -- FIXME
118 data OptimizeFlag = DoOptimize | NoOptimize
120 mkSkeleton :: OptimizeFlag ->
127 ,GArrowInclusion g (,) () m) =>
129 -> GArrowSkeleton m x y
130 mkSkeleton DoOptimize = \g -> (beautify . optimize) g
131 mkSkeleton NoOptimize = \g -> g
136 -- | Performs some very simple-minded optimizations on a
137 -- boxes-and-wires diagram. Preserves equivalence up to the GArrow
138 -- laws, but no guarantees about which optimizations actually happen.
140 optimize :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
141 optimize = repeat (gasl2gas . optimizel . {- FIXME -} optimizel . gas2gasl)
144 optimize x = let x' = optimize' x in if x == x' then x' else optimize x'
146 optimize' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
148 -- Some optimizations fail due to misparenthesization; we default to
149 -- left-associativity and hope for the best
150 optimize' (GAS_comp f (GAS_comp g h) ) = GAS_comp (GAS_comp f g) h
151 optimize' (GAS_comp (GAS_comp f (GAS_comp g h)) k) = GAS_comp (GAS_comp (GAS_comp f g) h) k
152 optimize' (GAS_comp (GAS_comp GAS_unassoc (GAS_second g)) GAS_assoc) = GAS_second (GAS_second g)
153 optimize' (GAS_comp (GAS_comp (GAS_comp f GAS_unassoc) (GAS_second g)) GAS_assoc) = GAS_comp f (GAS_second (GAS_second g))
155 optimize' (GAS_comp (GAS_comp f g) h) = case optimize_pair g h of
156 Nothing -> GAS_comp (optimize' (GAS_comp f g)) h'
157 Just ret' -> GAS_comp f' ret'
162 optimize' (GAS_comp f g ) = case optimize_pair f g of
163 Nothing -> GAS_comp f' g'
168 optimize' (GAS_first GAS_id ) = GAS_id
169 optimize' (GAS_second GAS_id ) = GAS_id
170 -- optimize' (GAS_first (GAS_comp f g)) = GAS_comp (GAS_first f) (GAS_first g)
171 -- optimize' (GAS_second (GAS_comp f g)) = GAS_comp (GAS_second f) (GAS_second g)
172 optimize' (GAS_first f ) = GAS_first $ optimize' f
173 optimize' (GAS_second f ) = GAS_second $ optimize' f
174 optimize' (GAS_loopl GAS_id ) = GAS_id
175 optimize' (GAS_loopr GAS_id ) = GAS_id
176 optimize' (GAS_loopl f ) = GAS_loopl $ optimize' f
177 optimize' (GAS_loopr f ) = GAS_loopr $ optimize' f
180 optimize_pair :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) b c -> Maybe ((GArrowSkeleton m) a c)
182 optimize_pair f GAS_drop = Just $ GAS_drop
183 optimize_pair GAS_id f = Just $ f
184 optimize_pair f GAS_id = Just $ f
185 optimize_pair GAS_uncancell GAS_cancell = Just $ GAS_id
186 optimize_pair GAS_uncancelr GAS_cancelr = Just $ GAS_id
187 optimize_pair GAS_cancell GAS_uncancell = Just $ GAS_id
188 optimize_pair GAS_cancelr GAS_uncancelr = Just $ GAS_id
189 optimize_pair GAS_uncancelr GAS_cancell = Just $ GAS_id
190 optimize_pair GAS_uncancell GAS_cancelr = Just $ GAS_id
192 -- first priority: eliminate GAS_first
193 optimize_pair (GAS_first f) GAS_cancelr = Just $ GAS_comp GAS_cancelr f
194 optimize_pair (GAS_second f) GAS_cancell = Just $ GAS_comp GAS_cancell f
195 optimize_pair GAS_uncancelr (GAS_first f) = Just $ GAS_comp f GAS_uncancelr
196 optimize_pair GAS_uncancell (GAS_second f) = Just $ GAS_comp f GAS_uncancell
198 -- second priority: push GAS_swap leftward
199 optimize_pair (GAS_second f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_first f)
200 optimize_pair (GAS_first f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_second f)
201 optimize_pair GAS_swap GAS_swap = Just $ GAS_id
202 optimize_pair GAS_swap GAS_cancell = Just $ GAS_cancelr
203 optimize_pair GAS_swap GAS_cancelr = Just $ GAS_cancell
205 optimize_pair GAS_assoc GAS_cancell = Just $ GAS_first GAS_cancell
206 optimize_pair GAS_unassoc GAS_cancelr = Just $ GAS_second GAS_cancelr
207 optimize_pair GAS_assoc (GAS_second GAS_cancell) = Just $ GAS_first GAS_cancelr
208 optimize_pair GAS_unassoc (GAS_first GAS_cancell) = Just $ GAS_cancell
211 -- FIXME: valid only for central morphisms
212 --optimize_pair (GAS_second f) (GAS_first g) = Just $ GAS_comp (GAS_first g) (GAS_second f)
213 optimize_pair (GAS_first g) (GAS_second f) = Just $ GAS_comp (GAS_second f) (GAS_first g)
215 optimize_pair _ _ = Nothing
218 repeat :: Eq a => (a -> a) -> a -> a
219 repeat f x = let x' = f x in
225 -- | Recursively turns @(ga_first x >>> first y)@ into @(ga_first (x >>> y))@, likewise for ga_second.
227 beautify :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
228 beautify = repeat beautify'
230 beautify' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
231 beautify' (GAS_comp (GAS_comp f g) h) = beautify' $ GAS_comp f $ GAS_comp g h
232 beautify' (GAS_comp f (GAS_comp (GAS_comp g h) k)) = beautify' $ GAS_comp f $ GAS_comp g $ GAS_comp h k
233 beautify' (GAS_comp f (GAS_comp g h)) = case (beautify' f, beautify' g) of
234 (GAS_first f' , GAS_first g') -> beautify' $ GAS_comp (GAS_first (GAS_comp f' g')) h
235 (GAS_second f', GAS_second g') -> beautify' $ GAS_comp (GAS_second (GAS_comp f' g')) h
236 (f' , g' ) -> GAS_comp f' (beautify' (GAS_comp g h))
237 beautify' (GAS_comp f GAS_id) = f
238 beautify' (GAS_comp GAS_id f) = f
239 beautify' (GAS_comp f g) = case (beautify' f, beautify' g) of
240 (GAS_first f' , GAS_first g') -> GAS_first (GAS_comp f' g')
241 (GAS_second f', GAS_second g') -> GAS_second (GAS_comp f' g')
242 (f' , g' ) -> GAS_comp f' g'
243 beautify' (GAS_first f) = GAS_first $ beautify' f
244 beautify' (GAS_second f) = GAS_second $ beautify' f
245 beautify' (GAS_loopl f) = GAS_loopl $ beautify' f
246 beautify' (GAS_loopr f) = GAS_loopr $ beautify' f
252 gas2gasl :: GArrowSkeleton m x y -> GArrowSkeletonL m x y
253 gas2gasl (GAS_id ) = GASL_id
254 gas2gasl (GAS_comp f g) = gaslcat (gas2gasl f) (gas2gasl g)
255 gas2gasl (GAS_first f) = gasl_firstify $ gas2gasl f
256 gas2gasl (GAS_second f) = gasl_secondify $ gas2gasl f
257 gas2gasl (GAS_cancell ) = GASL_Y $ GASY_X $ GASX_cancell
258 gas2gasl (GAS_cancelr ) = GASL_Y $ GASY_X $ GASX_cancelr
259 gas2gasl (GAS_uncancell ) = GASL_Y $ GASY_X $ GASX_uncancell
260 gas2gasl (GAS_uncancelr ) = GASL_Y $ GASY_X $ GASX_uncancelr
261 gas2gasl (GAS_assoc ) = GASL_Y $ GASY_X $ GASX_assoc
262 gas2gasl (GAS_unassoc ) = GASL_Y $ GASY_X $ GASX_unassoc
263 gas2gasl (GAS_drop ) = GASL_Y $ GASY_X $ GASX_drop
264 gas2gasl (GAS_copy ) = GASL_Y $ GASY_X $ GASX_copy
265 gas2gasl (GAS_swap ) = GASL_Y $ GASY_X $ GASX_swap
266 gas2gasl (GAS_loopl f) = GASL_Y $ GASY_X $ GASX_loopl $ gas2gasl f
267 gas2gasl (GAS_loopr f) = GASL_Y $ GASY_X $ GASX_loopr $ gas2gasl f
268 gas2gasl (GAS_misc m) = GASL_Y $ GASY_X $ GASX_misc m
270 -- apply "first" to a GASL
271 gasl_firstify :: GArrowSkeletonL m x y -> GArrowSkeletonL m (x,z) (y,z)
272 gasl_firstify (GASL_id ) = GASL_id
273 gasl_firstify (GASL_Y gy ) = GASL_Y $ GASY_first $ gy
274 gasl_firstify (GASL_comp gxq gqy) = GASL_comp (GASY_first gxq) $ gasl_firstify gqy
276 -- apply "second" to a GASL
277 gasl_secondify :: GArrowSkeletonL m x y -> GArrowSkeletonL m (z,x) (z,y)
278 gasl_secondify (GASL_id ) = GASL_id
279 gasl_secondify (GASL_Y gy ) = GASL_Y $ GASY_second $ gy
280 gasl_secondify (GASL_comp gxq gqy) = GASL_comp (GASY_second gxq) $ gasl_secondify gqy
282 -- concatenates two GASL's
283 gaslcat :: GArrowSkeletonL m x y -> GArrowSkeletonL m y z -> GArrowSkeletonL m x z
284 gaslcat (GASL_id ) g' = g'
285 gaslcat (GASL_Y gy ) g' = GASL_comp gy g'
286 gaslcat (GASL_comp gxq gqy) g' = GASL_comp gxq (gaslcat gqy g')
288 data GArrowSkeletonL m :: * -> * -> *
290 GASL_id :: GArrowSkeletonL m x x
291 GASL_Y :: GArrowSkeletonY m x y -> GArrowSkeletonL m x y
292 GASL_comp :: GArrowSkeletonY m x y -> GArrowSkeletonL m y z -> GArrowSkeletonL m x z
294 data GArrowSkeletonY m :: * -> * -> *
296 GASY_X :: GArrowSkeletonX m x y -> GArrowSkeletonY m x y
297 GASY_first :: GArrowSkeletonY m x y -> GArrowSkeletonY m (x,z) (y,z)
298 GASY_second :: GArrowSkeletonY m x y -> GArrowSkeletonY m (z,x) (z,y)
299 GASY_atomicl :: GArrowSkeletonY m () x -> GArrowSkeletonY m y (x,y)
300 GASY_atomicr :: GArrowSkeletonY m () x -> GArrowSkeletonY m y (y,x)
302 data GArrowSkeletonX m :: * -> * -> *
304 GASX_cancell :: GArrowSkeletonX m ((),x) x
305 GASX_cancelr :: GArrowSkeletonX m (x,()) x
306 GASX_uncancell :: GArrowSkeletonX m x ((),x)
307 GASX_uncancelr :: GArrowSkeletonX m x (x,())
308 GASX_assoc :: GArrowSkeletonX m ((x,y),z) (x,(y,z))
309 GASX_unassoc :: GArrowSkeletonX m (x,(y,z)) ((x,y),z)
310 GASX_drop :: GArrowSkeletonX m x ()
311 GASX_copy :: GArrowSkeletonX m x (x,x)
312 GASX_swap :: GArrowSkeletonX m (x,y) (y,x)
313 GASX_misc :: m x y -> GArrowSkeletonX m x y
314 GASX_loopl :: GArrowSkeletonL m (z,x) (z,y) -> GArrowSkeletonX m x y
315 GASX_loopr :: GArrowSkeletonL m (x,z) (y,z) -> GArrowSkeletonX m x y
317 -- TO DO: gather "maximal chunks" of ga_first/ga_second
318 gasl2gas :: GArrowSkeletonL m x y -> GArrowSkeleton m x y
319 gasl2gas GASL_id = GAS_id
320 gasl2gas (GASL_Y gy ) = gasy2gas gy
321 gasl2gas (GASL_comp gy gl) = GAS_comp (gasy2gas gy) (gasl2gas gl)
323 gasy2gas :: GArrowSkeletonY m x y -> GArrowSkeleton m x y
324 gasy2gas (GASY_X gx) = gasx2gas gx
325 gasy2gas (GASY_first gy) = GAS_first (gasy2gas gy)
326 gasy2gas (GASY_second gy) = GAS_second (gasy2gas gy)
327 gasy2gas (GASY_atomicl gy) = GAS_comp GAS_uncancell (GAS_first $ gasy2gas gy)
328 gasy2gas (GASY_atomicr gy) = GAS_comp GAS_uncancelr (GAS_second $ gasy2gas gy)
330 gasx2gas :: GArrowSkeletonX m x y -> GArrowSkeleton m x y
331 gasx2gas (GASX_cancell) = GAS_cancell
332 gasx2gas (GASX_cancelr) = GAS_cancelr
333 gasx2gas (GASX_uncancell) = GAS_uncancell
334 gasx2gas (GASX_uncancelr) = GAS_uncancelr
335 gasx2gas (GASX_assoc) = GAS_assoc
336 gasx2gas (GASX_unassoc) = GAS_unassoc
337 gasx2gas (GASX_drop) = GAS_drop
338 gasx2gas (GASX_copy) = GAS_copy
339 gasx2gas (GASX_swap) = GAS_swap
340 gasx2gas (GASX_misc m) = GAS_misc m
341 gasx2gas (GASX_loopl gl) = GAS_loopl $ gasl2gas gl
342 gasx2gas (GASX_loopr gl) = GAS_loopr $ gasl2gas gl
346 optimizel :: GArrowSkeletonL m x y -> GArrowSkeletonL m x y
347 optimizel (GASL_id ) = GASL_id
348 optimizel (GASL_Y gy ) = GASL_Y $ optimizey gy
349 optimizel (GASL_comp gy (GASL_comp gy' gl)) | Just x <- optpair gy gy' = optimizel $ gaslcat x gl
350 optimizel (GASL_comp gy (GASL_Y gy')) | Just x <- optpair gy gy' = x
351 optimizel (GASL_comp gy (GASL_comp gy' gl)) | pushright gy, not (pushright gy'), Just x <- swappair gy gy' = optimizel $ gaslcat x gl
352 optimizel (GASL_comp gy (GASL_Y gy')) | pushright gy, not (pushright gy'), Just x <- swappair gy gy' = GASL_comp (optimizey gy) (GASL_Y gy')
353 optimizel (GASL_comp gy gl) = GASL_comp (optimizey gy) (optimizel gl)
355 --optimize' (GAS_loopl GAS_id ) = GAS_id
356 --optimize' (GAS_loopr GAS_id ) = GAS_id
357 --optimize_pair f GAS_drop = Just $ GAS_drop
359 optimize_pair (GAS_first f) GAS_cancelr = Just $ GAS_comp GAS_cancelr f
360 optimize_pair (GAS_second f) GAS_cancell = Just $ GAS_comp GAS_cancell f
361 optimize_pair GAS_uncancelr (GAS_first f) = Just $ GAS_comp f GAS_uncancelr
362 optimize_pair GAS_uncancell (GAS_second f) = Just $ GAS_comp f GAS_uncancell
363 optimize_pair (GAS_second f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_first f)
364 optimize_pair (GAS_first f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_second f)
365 optimize_pair GAS_swap GAS_swap = Just $ GAS_id
366 optimize_pair GAS_swap GAS_cancell = Just $ GAS_cancelr
367 optimize_pair GAS_swap GAS_cancelr = Just $ GAS_cancell
368 optimize_pair GAS_assoc GAS_cancell = Just $ GAS_first GAS_cancell
369 optimize_pair GAS_unassoc GAS_cancelr = Just $ GAS_second GAS_cancelr
370 optimize_pair GAS_assoc (GAS_second GAS_cancell) = Just $ GAS_first GAS_cancelr
371 optimize_pair GAS_unassoc (GAS_first GAS_cancell) = Just $ GAS_cancell
374 optpair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z)
376 optpair (GASY_atomicl g) (GASY_X GASX_cancelr) = Just $ GASL_Y g
377 optpair (GASY_atomicr g) (GASY_X GASX_cancell) = Just $ GASL_Y g
379 optpair (GASY_X GASX_uncancell) (GASY_X GASX_cancell) = Just $ GASL_id
380 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_cancelr) = Just $ GASL_id
381 optpair (GASY_X GASX_cancell) (GASY_X GASX_uncancell) = Just $ GASL_id
382 optpair (GASY_X GASX_cancelr) (GASY_X GASX_uncancelr) = Just $ GASL_id
383 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_cancell) = Just $ GASL_id
384 optpair (GASY_X GASX_uncancell) (GASY_X GASX_cancelr) = Just $ GASL_id
385 optpair (GASY_X GASX_assoc) (GASY_X GASX_cancell) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_cancell
386 optpair (GASY_X GASX_unassoc) (GASY_X GASX_cancelr) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_cancelr
387 optpair (GASY_second (GASY_X GASX_uncancelr)) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_X GASX_uncancelr
388 optpair (GASY_first (GASY_X GASX_uncancell)) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_X GASX_uncancell
389 optpair (GASY_X GASX_uncancell) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_uncancell
390 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancelr
391 optpair (GASY_first (GASY_X GASX_uncancelr)) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancell
392 optpair (GASY_second (GASY_X GASX_uncancell)) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_uncancelr
393 optpair (GASY_X GASX_assoc) (GASY_second (GASY_X GASX_cancelr)) = Just $ GASL_Y $ GASY_X $ GASX_cancelr
394 optpair (GASY_X GASX_unassoc) (GASY_first (GASY_X GASX_cancell)) = Just $ GASL_Y $ GASY_X $ GASX_cancell
395 optpair (GASY_first g) (GASY_X GASX_cancelr) = Just $ GASL_comp (GASY_X GASX_cancelr) $ GASL_Y $ g
396 optpair (GASY_second g) (GASY_X GASX_cancell) = Just $ GASL_comp (GASY_X GASX_cancell) $ GASL_Y $ g
397 optpair (GASY_X GASX_uncancelr) (GASY_first g) = Just $ GASL_comp g $ GASL_Y (GASY_X GASX_uncancelr)
398 optpair (GASY_X GASX_uncancell) (GASY_second g) = Just $ GASL_comp g $ GASL_Y (GASY_X GASX_uncancell)
400 -- swap with an {un}cancel{l,r} before/after it
401 optpair (GASY_X GASX_uncancell) (GASY_X GASX_swap ) = Just $ GASL_Y $ GASY_X $ GASX_uncancelr
402 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_swap ) = Just $ GASL_Y $ GASY_X $ GASX_uncancell
403 optpair (GASY_X GASX_swap) (GASY_X GASX_cancell) = Just $ GASL_Y $ GASY_X $ GASX_cancelr
404 optpair (GASY_X GASX_swap) (GASY_X GASX_cancelr) = Just $ GASL_Y $ GASY_X $ GASX_cancell
407 optpair (GASY_X GASX_uncancelr) (GASY_X (GASX_loopl gl)) =
408 Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ GASY_X GASX_uncancelr) gl)
409 optpair (GASY_X GASX_uncancell) (GASY_X (GASX_loopl gl)) =
410 Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ GASY_X GASX_uncancell) gl)
411 optpair (GASY_X GASX_uncancelr) (GASY_X (GASX_loopr gl)) =
412 Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ GASY_X GASX_uncancelr) gl)
413 optpair (GASY_X GASX_uncancell) (GASY_X (GASX_loopr gl)) =
414 Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ GASY_X GASX_uncancell) gl)
416 optpair q (GASY_X (GASX_loopl gl)) | pushin q = Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ q) gl)
417 optpair q (GASY_X (GASX_loopr gl)) | pushin q = Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ q) gl)
419 optpair (GASY_first gy1) (GASY_second gy2) | pushleft gy2, not (pushleft gy1)
420 = Just $ GASL_comp (GASY_second gy2) $ GASL_Y $ GASY_first gy1
421 optpair (GASY_second gy1) (GASY_first gy2) | pushleft gy2, not (pushleft gy1)
422 = Just $ GASL_comp (GASY_first gy2) $ GASL_Y $ GASY_second gy1
424 optpair (GASY_first gy1) (GASY_first gy2) = liftM gasl_firstify $ optpair gy1 gy2
425 optpair (GASY_second gy1) (GASY_second gy2) = liftM gasl_secondify $ optpair gy1 gy2
426 optpair _ _ = Nothing
428 swappair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z)
430 swappair q (GASY_atomicl g) = Just $ GASL_comp (GASY_atomicl g) $ GASL_Y $ GASY_second q
431 swappair q (GASY_atomicr g) = Just $ GASL_comp (GASY_atomicr g) $ GASL_Y $ GASY_first q
433 swappair (GASY_first gy1) (GASY_second gy2) = Just $ GASL_comp (GASY_second gy2) (GASL_Y $ GASY_first gy1)
434 swappair (GASY_second gy1) (GASY_first gy2) = Just $ GASL_comp (GASY_first gy2) (GASL_Y $ GASY_second gy1)
435 swappair (GASY_first gy1) (GASY_X GASX_unassoc) = Just $ GASL_comp(GASY_X GASX_unassoc) (GASL_Y $ GASY_first (GASY_first gy1))
436 swappair (GASY_second gy1) (GASY_X GASX_assoc ) = Just $ GASL_comp(GASY_X GASX_assoc ) (GASL_Y $ GASY_second (GASY_second gy1))
437 swappair (GASY_X GASX_uncancelr) (GASY_first gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancelr)
438 swappair (GASY_X GASX_uncancell) (GASY_second gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancell)
439 swappair (GASY_first (GASY_second gy)) (GASY_X GASX_assoc ) = Just $ GASL_comp (GASY_X GASX_assoc ) $ GASL_Y (GASY_second (GASY_first gy))
440 swappair (GASY_second (GASY_first gy)) (GASY_X GASX_unassoc ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_first (GASY_second gy))
441 swappair (GASY_second (GASY_second gy)) (GASY_X GASX_unassoc ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_second gy)
442 swappair (GASY_first (GASY_first gy)) (GASY_X GASX_assoc ) = Just $ GASL_comp (GASY_X GASX_assoc) $ GASL_Y (GASY_first gy)
443 swappair (GASY_first gy) (GASY_X GASX_swap ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_second gy)
444 swappair (GASY_second gy) (GASY_X GASX_swap ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_first gy)
445 swappair gy (GASY_X (GASX_loopl gl)) = Just $ GASL_Y $ GASY_X $ GASX_loopl $ GASL_comp (GASY_second gy) gl
446 swappair gy (GASY_X (GASX_loopr gl)) = Just $ GASL_Y $ GASY_X $ GASX_loopr $ GASL_comp (GASY_first gy) gl
448 swappair (GASY_first gy1) (GASY_first gy2) = liftM gasl_firstify $ swappair gy1 gy2
449 swappair (GASY_second gy1) (GASY_second gy2) = liftM gasl_secondify $ swappair gy1 gy2
450 swappair _ _ = Nothing
452 -- pushright can only return True for central morphisms
453 pushright :: GArrowSkeletonY m x y -> Bool
454 pushright (GASY_first gy) = pushright gy
455 pushright (GASY_second gy) = pushright gy
456 pushright (GASY_atomicl _) = False
457 pushright (GASY_atomicr _) = False
458 pushright (GASY_X GASX_uncancell) = True
459 pushright (GASY_X GASX_uncancelr) = True
460 pushright (GASY_X _ ) = False
462 -- says if we should push it into a loopl/r
463 pushin :: GArrowSkeletonY m x y -> Bool
464 pushin gy = pushright gy || pushin' gy
466 pushin' :: GArrowSkeletonY m a b -> Bool
467 pushin' (GASY_first gy) = pushin' gy
468 pushin' (GASY_second gy) = pushin' gy
469 pushin' (GASY_atomicl _) = False
470 pushin' (GASY_atomicr _) = False
472 -- not sure if these are a good idea
473 pushin' (GASY_X GASX_copy) = True
474 pushin' (GASY_X GASX_swap) = True
476 pushin' (GASY_X _ ) = False
478 optimizey :: GArrowSkeletonY m x y -> GArrowSkeletonY m x y
479 optimizey (GASY_X gx) = GASY_X $ optimizex gx
480 optimizey (GASY_first gy) = GASY_first (optimizey gy)
481 optimizey (GASY_second gy) = GASY_second (optimizey gy)
482 optimizey (GASY_atomicl gy) = GASY_atomicl $ optimizey gy
483 optimizey (GASY_atomicr gy) = GASY_atomicr $ optimizey gy
485 optimizex :: GArrowSkeletonX m x y -> GArrowSkeletonX m x y
486 optimizex (GASX_cancell) = GASX_cancell
487 optimizex (GASX_cancelr) = GASX_cancelr
488 optimizex (GASX_uncancell) = GASX_uncancell
489 optimizex (GASX_uncancelr) = GASX_uncancelr
490 optimizex (GASX_assoc) = GASX_assoc
491 optimizex (GASX_unassoc) = GASX_unassoc
492 optimizex (GASX_drop) = GASX_drop
493 optimizex (GASX_copy) = GASX_copy
494 optimizex (GASX_swap) = GASX_swap
495 optimizex (GASX_misc m) = GASX_misc m
496 optimizex (GASX_loopl (GASL_comp (GASY_first gy) gl))| pushleft gy = GASX_loopl $ gaslcat gl (GASL_Y $ GASY_first gy)
497 optimizex (GASX_loopr (GASL_comp (GASY_second gy) gl))| pushleft gy = GASX_loopr $ gaslcat gl (GASL_Y $ GASY_second gy)
498 optimizex (GASX_loopl gl) = GASX_loopl $ optimizel gl
499 optimizex (GASX_loopr gl) = GASX_loopr $ optimizel gl
501 pushleft :: GArrowSkeletonY m x y -> Bool
502 pushleft (GASY_first gy) = pushleft gy
503 pushleft (GASY_second gy) = pushleft gy
504 pushleft (GASY_atomicl _) = False
505 pushleft (GASY_atomicr _) = False
506 pushleft (GASY_X GASX_cancell) = True
507 pushleft (GASY_X GASX_cancelr) = True
508 pushleft (GASY_X _ ) = False