1 {-# LANGUAGE MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, TypeFamilies #-}
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 ks *equivalent to* the term, rather than structurally
22 -- exactly equal to it.
24 module GArrowSkeleton (GArrowSkeleton(..), optimize, beautify)
26 import Prelude hiding ( id, (.), lookup, repeat )
27 import Control.Category
28 import GHC.HetMet.GArrow
30 import Control.Monad.State
32 data GArrowSkeleton m :: * -> * -> *
34 GAS_const :: Int -> GArrowSkeleton m () Int
35 GAS_id :: GArrowSkeleton m x x
36 GAS_comp :: GArrowSkeleton m x y -> GArrowSkeleton m y z -> GArrowSkeleton m x z
37 GAS_first :: GArrowSkeleton m x y -> GArrowSkeleton m (x,z) (y,z)
38 GAS_second :: GArrowSkeleton m x y -> GArrowSkeleton m (z,x) (z,y)
39 GAS_cancell :: GArrowSkeleton m ((),x) x
40 GAS_cancelr :: GArrowSkeleton m (x,()) x
41 GAS_uncancell :: GArrowSkeleton m x ((),x)
42 GAS_uncancelr :: GArrowSkeleton m x (x,())
43 GAS_assoc :: GArrowSkeleton m ((x,y),z) (x,(y,z))
44 GAS_unassoc :: GArrowSkeleton m (x,(y,z)) ((x,y),z)
45 GAS_drop :: GArrowSkeleton m x ()
46 GAS_copy :: GArrowSkeleton m x (x,x)
47 GAS_swap :: GArrowSkeleton m (x,y) (y,x)
48 GAS_merge :: GArrowSkeleton m (x,y) z
49 GAS_loopl :: GArrowSkeleton m (z,x) (z,y) -> GArrowSkeleton m x y
50 GAS_loopr :: GArrowSkeleton m (x,z) (y,z) -> GArrowSkeleton m x y
51 GAS_misc :: m x y -> GArrowSkeleton m x y
53 instance Category (GArrowSkeleton m) where
57 instance GArrow (GArrowSkeleton m) (,) () where
59 ga_second = GAS_second
60 ga_cancell = GAS_cancell
61 ga_cancelr = GAS_cancelr
62 ga_uncancell = GAS_uncancell
63 ga_uncancelr = GAS_uncancelr
65 ga_unassoc = GAS_unassoc
67 instance GArrowDrop (GArrowSkeleton m) (,) () where
70 instance GArrowCopy (GArrowSkeleton m) (,) () where
73 instance GArrowSwap (GArrowSkeleton m) (,) () where
76 instance GArrowLoop (GArrowSkeleton m) (,) () where
80 type instance GArrowTensor (GArrowSkeleton m) = (,)
81 type instance GArrowUnit (GArrowSkeleton m) = ()
82 type instance GArrowExponent (GArrowSkeleton m) = (->)
84 instance GArrowSTKCL (GArrowSkeleton m)
87 -- | Simple structural equality on skeletons. NOTE: two skeletons
88 -- with the same shape but different types will nonetheless be "equal";
89 -- there's no way around this since types are gone at runtime.
91 instance Eq ((GArrowSkeleton m) a b)
95 (===) :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) c d -> Bool
96 (GAS_id ) === (GAS_id ) = True
97 (GAS_comp g f) === (GAS_comp g' f') = f===f' && g===g'
98 (GAS_first f) === (GAS_first f') = f===f'
99 (GAS_second f) === (GAS_second f') = f===f'
100 GAS_cancell === GAS_cancell = True
101 GAS_cancelr === GAS_cancelr = True
102 GAS_uncancell === GAS_uncancell = True
103 GAS_uncancelr === GAS_uncancelr = True
104 GAS_drop === GAS_drop = True
105 (GAS_const i) === (GAS_const i') = i==i'
106 GAS_copy === GAS_copy = True
107 GAS_merge === GAS_merge = True
108 GAS_swap === GAS_swap = True
109 GAS_assoc === GAS_assoc = True
110 GAS_unassoc === GAS_unassoc = True
111 (GAS_loopl f) === (GAS_loopl f') = f === f'
112 (GAS_loopr f) === (GAS_loopr f') = f === f'
114 -- FIXME: GAS_misc's are never equal!!!
117 -- | Performs some very simple-minded optimizations on a
118 -- boxes-and-wires diagram. Preserves equivalence up to the GArrow
119 -- laws, but no guarantees about which optimizations actually happen.
121 optimize :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
122 optimize = repeat (gasl2gas . optimizel . gas2gasl)
125 optimize x = let x' = optimize' x in if x == x' then x' else optimize x'
127 optimize' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
129 -- Some optimizations fail due to misparenthesization; we default to
130 -- left-associativity and hope for the best
131 optimize' (GAS_comp f (GAS_comp g h) ) = GAS_comp (GAS_comp f g) h
132 optimize' (GAS_comp (GAS_comp f (GAS_comp g h)) k) = GAS_comp (GAS_comp (GAS_comp f g) h) k
133 optimize' (GAS_comp (GAS_comp GAS_unassoc (GAS_second g)) GAS_assoc) = GAS_second (GAS_second g)
134 optimize' (GAS_comp (GAS_comp (GAS_comp f GAS_unassoc) (GAS_second g)) GAS_assoc) = GAS_comp f (GAS_second (GAS_second g))
136 optimize' (GAS_comp (GAS_comp f g) h) = case optimize_pair g h of
137 Nothing -> GAS_comp (optimize' (GAS_comp f g)) h'
138 Just ret' -> GAS_comp f' ret'
143 optimize' (GAS_comp f g ) = case optimize_pair f g of
144 Nothing -> GAS_comp f' g'
149 optimize' (GAS_first GAS_id ) = GAS_id
150 optimize' (GAS_second GAS_id ) = GAS_id
151 -- optimize' (GAS_first (GAS_comp f g)) = GAS_comp (GAS_first f) (GAS_first g)
152 -- optimize' (GAS_second (GAS_comp f g)) = GAS_comp (GAS_second f) (GAS_second g)
153 optimize' (GAS_first f ) = GAS_first $ optimize' f
154 optimize' (GAS_second f ) = GAS_second $ optimize' f
155 optimize' (GAS_loopl GAS_id ) = GAS_id
156 optimize' (GAS_loopr GAS_id ) = GAS_id
157 optimize' (GAS_loopl f ) = GAS_loopl $ optimize' f
158 optimize' (GAS_loopr f ) = GAS_loopr $ optimize' f
161 optimize_pair :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) b c -> Maybe ((GArrowSkeleton m) a c)
163 optimize_pair f GAS_drop = Just $ GAS_drop
164 optimize_pair GAS_id f = Just $ f
165 optimize_pair f GAS_id = Just $ f
166 optimize_pair GAS_uncancell GAS_cancell = Just $ GAS_id
167 optimize_pair GAS_uncancelr GAS_cancelr = Just $ GAS_id
168 optimize_pair GAS_cancell GAS_uncancell = Just $ GAS_id
169 optimize_pair GAS_cancelr GAS_uncancelr = Just $ GAS_id
170 optimize_pair GAS_uncancelr GAS_cancell = Just $ GAS_id
171 optimize_pair GAS_uncancell GAS_cancelr = Just $ GAS_id
173 -- first priority: eliminate GAS_first
174 optimize_pair (GAS_first f) GAS_cancelr = Just $ GAS_comp GAS_cancelr f
175 optimize_pair (GAS_second f) GAS_cancell = Just $ GAS_comp GAS_cancell f
176 optimize_pair GAS_uncancelr (GAS_first f) = Just $ GAS_comp f GAS_uncancelr
177 optimize_pair GAS_uncancell (GAS_second f) = Just $ GAS_comp f GAS_uncancell
179 -- second priority: push GAS_swap leftward
180 optimize_pair (GAS_second f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_first f)
181 optimize_pair (GAS_first f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_second f)
182 optimize_pair GAS_swap GAS_swap = Just $ GAS_id
183 optimize_pair GAS_swap GAS_cancell = Just $ GAS_cancelr
184 optimize_pair GAS_swap GAS_cancelr = Just $ GAS_cancell
186 optimize_pair GAS_assoc GAS_cancell = Just $ GAS_first GAS_cancell
187 optimize_pair GAS_unassoc GAS_cancelr = Just $ GAS_second GAS_cancelr
188 optimize_pair GAS_assoc (GAS_second GAS_cancell) = Just $ GAS_first GAS_cancelr
189 optimize_pair GAS_unassoc (GAS_first GAS_cancell) = Just $ GAS_cancell
192 -- FIXME: valid only for central morphisms
193 --optimize_pair (GAS_second f) (GAS_first g) = Just $ GAS_comp (GAS_first g) (GAS_second f)
194 optimize_pair (GAS_first g) (GAS_second f) = Just $ GAS_comp (GAS_second f) (GAS_first g)
196 optimize_pair _ _ = Nothing
199 repeat :: Eq a => (a -> a) -> a -> a
200 repeat f x = let x' = f x in
206 -- | Recursively turns @(ga_first x >>> first y)@ into @(ga_first (x >>> y))@, likewise for ga_second.
208 beautify :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
209 beautify = optimize . (repeat beautify')
211 beautify' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
212 beautify' (GAS_comp (GAS_comp f g) h) = GAS_comp f $ GAS_comp g h
213 beautify' (GAS_comp f (GAS_comp (GAS_comp g h) k)) = GAS_comp f $ GAS_comp g $ GAS_comp h k
214 beautify' (GAS_comp f (GAS_comp g h)) = case (beautify' f, beautify' g) of
215 (GAS_first f' , GAS_first g') -> beautify' $ GAS_comp (GAS_first (GAS_comp f' g')) h
216 (GAS_second f', GAS_second g') -> beautify' $ GAS_comp (GAS_second (GAS_comp f' g')) h
217 (f' , g' ) -> GAS_comp f' (beautify' (GAS_comp g h))
218 beautify' (GAS_comp f g) = case (beautify' f, beautify' g) of
219 (GAS_first f' , GAS_first g') -> GAS_first (GAS_comp f' g')
220 (GAS_second f', GAS_second g') -> GAS_second (GAS_comp f' g')
221 (f' , g' ) -> GAS_comp f' g'
222 beautify' (GAS_first f) = GAS_first $ beautify' f
223 beautify' (GAS_second f) = GAS_second $ beautify' f
224 beautify' (GAS_loopl f) = GAS_loopl $ beautify' f
225 beautify' (GAS_loopr f) = GAS_loopr $ beautify' f
231 gas2gasl :: GArrowSkeleton m x y -> GArrowSkeletonL m x y
232 gas2gasl (GAS_const k ) = GASL_Y $ GASY_X $ GASX_const k
233 gas2gasl (GAS_id ) = GASL_id
234 gas2gasl (GAS_comp f g) = gaslcat (gas2gasl f) (gas2gasl g)
235 gas2gasl (GAS_first f) = gasl_firstify $ gas2gasl f
236 gas2gasl (GAS_second f) = gasl_secondify $ gas2gasl f
237 gas2gasl (GAS_cancell ) = GASL_Y $ GASY_X $ GASX_cancell
238 gas2gasl (GAS_cancelr ) = GASL_Y $ GASY_X $ GASX_cancelr
239 gas2gasl (GAS_uncancell ) = GASL_Y $ GASY_X $ GASX_uncancell
240 gas2gasl (GAS_uncancelr ) = GASL_Y $ GASY_X $ GASX_uncancelr
241 gas2gasl (GAS_assoc ) = GASL_Y $ GASY_X $ GASX_assoc
242 gas2gasl (GAS_unassoc ) = GASL_Y $ GASY_X $ GASX_unassoc
243 gas2gasl (GAS_drop ) = GASL_Y $ GASY_X $ GASX_drop
244 gas2gasl (GAS_copy ) = GASL_Y $ GASY_X $ GASX_copy
245 gas2gasl (GAS_swap ) = GASL_Y $ GASY_X $ GASX_swap
246 gas2gasl (GAS_merge ) = GASL_Y $ GASY_X $ GASX_merge
247 gas2gasl (GAS_loopl f) = GASL_Y $ GASY_X $ GASX_loopl $ gas2gasl f
248 gas2gasl (GAS_loopr f) = GASL_Y $ GASY_X $ GASX_loopr $ gas2gasl f
249 gas2gasl (GAS_misc m) = GASL_Y $ GASY_X $ GASX_misc m
251 -- apply "first" to a GASL
252 gasl_firstify :: GArrowSkeletonL m x y -> GArrowSkeletonL m (x,z) (y,z)
253 gasl_firstify (GASL_id ) = GASL_id
254 gasl_firstify (GASL_Y gy ) = GASL_Y $ GASY_first $ gy
255 gasl_firstify (GASL_comp gxq gqy) = GASL_comp (GASY_first gxq) $ gasl_firstify gqy
257 -- apply "second" to a GASL
258 gasl_secondify :: GArrowSkeletonL m x y -> GArrowSkeletonL m (z,x) (z,y)
259 gasl_secondify (GASL_id ) = GASL_id
260 gasl_secondify (GASL_Y gy ) = GASL_Y $ GASY_second $ gy
261 gasl_secondify (GASL_comp gxq gqy) = GASL_comp (GASY_second gxq) $ gasl_secondify gqy
263 -- concatenates two GASL's
264 gaslcat :: GArrowSkeletonL m x y -> GArrowSkeletonL m y z -> GArrowSkeletonL m x z
265 gaslcat (GASL_id ) g' = g'
266 gaslcat (GASL_Y gy ) g' = GASL_comp gy g'
267 gaslcat (GASL_comp gxq gqy) g' = GASL_comp gxq (gaslcat gqy g')
269 data GArrowSkeletonL m :: * -> * -> *
271 GASL_id :: GArrowSkeletonL m x x
272 GASL_Y :: GArrowSkeletonY m x y -> GArrowSkeletonL m x y
273 GASL_comp :: GArrowSkeletonY m x y -> GArrowSkeletonL m y z -> GArrowSkeletonL m x z
275 data GArrowSkeletonY m :: * -> * -> *
277 GASY_X :: GArrowSkeletonX m x y -> GArrowSkeletonY m x y
278 GASY_first :: GArrowSkeletonY m x y -> GArrowSkeletonY m (x,z) (y,z)
279 GASY_second :: GArrowSkeletonY m x y -> GArrowSkeletonY m (z,x) (z,y)
281 data GArrowSkeletonX m :: * -> * -> *
283 GASX_const :: Int -> GArrowSkeletonX m () Int
284 GASX_cancell :: GArrowSkeletonX m ((),x) x
285 GASX_cancelr :: GArrowSkeletonX m (x,()) x
286 GASX_uncancell :: GArrowSkeletonX m x ((),x)
287 GASX_uncancelr :: GArrowSkeletonX m x (x,())
288 GASX_assoc :: GArrowSkeletonX m ((x,y),z) (x,(y,z))
289 GASX_unassoc :: GArrowSkeletonX m (x,(y,z)) ((x,y),z)
290 GASX_drop :: GArrowSkeletonX m x ()
291 GASX_copy :: GArrowSkeletonX m x (x,x)
292 GASX_swap :: GArrowSkeletonX m (x,y) (y,x)
293 GASX_merge :: GArrowSkeletonX m (x,y) z
294 GASX_misc :: m x y -> GArrowSkeletonX m x y
295 GASX_loopl :: GArrowSkeletonL m (z,x) (z,y) -> GArrowSkeletonX m x y
296 GASX_loopr :: GArrowSkeletonL m (x,z) (y,z) -> GArrowSkeletonX m x y
298 -- TO DO: gather "maximal chunks" of ga_first/ga_second
299 gasl2gas :: GArrowSkeletonL m x y -> GArrowSkeleton m x y
300 gasl2gas GASL_id = GAS_id
301 gasl2gas (GASL_Y gy ) = gasy2gas gy
302 gasl2gas (GASL_comp gy gl) = GAS_comp (gasy2gas gy) (gasl2gas gl)
304 gasy2gas :: GArrowSkeletonY m x y -> GArrowSkeleton m x y
305 gasy2gas (GASY_X gx) = gasx2gas gx
306 gasy2gas (GASY_first gy) = GAS_first (gasy2gas gy)
307 gasy2gas (GASY_second gy) = GAS_second (gasy2gas gy)
309 gasx2gas :: GArrowSkeletonX m x y -> GArrowSkeleton m x y
310 gasx2gas (GASX_const k) = GAS_const k
311 gasx2gas (GASX_cancell) = GAS_cancell
312 gasx2gas (GASX_cancelr) = GAS_cancelr
313 gasx2gas (GASX_uncancell) = GAS_uncancell
314 gasx2gas (GASX_uncancelr) = GAS_uncancelr
315 gasx2gas (GASX_assoc) = GAS_assoc
316 gasx2gas (GASX_unassoc) = GAS_unassoc
317 gasx2gas (GASX_drop) = GAS_drop
318 gasx2gas (GASX_copy) = GAS_copy
319 gasx2gas (GASX_swap) = GAS_swap
320 gasx2gas (GASX_merge) = GAS_merge
321 gasx2gas (GASX_misc m) = GAS_misc m
322 gasx2gas (GASX_loopl gl) = GAS_loopl $ gasl2gas gl
323 gasx2gas (GASX_loopr gl) = GAS_loopr $ gasl2gas gl
327 optimizel :: GArrowSkeletonL m x y -> GArrowSkeletonL m x y
328 optimizel (GASL_id ) = GASL_id
329 optimizel (GASL_Y gy ) = GASL_Y $ optimizey gy
330 optimizel (GASL_comp gy (GASL_comp gy' gl)) | pushright gy, not (pushright gy'), Just x <- pushpair gy gy' = optimizel $ gaslcat x gl
331 optimizel (GASL_comp gy (GASL_Y gy')) | pushright gy, not (pushright gy'), Just x <- pushpair gy gy' = GASL_comp (optimizey gy) (GASL_Y gy')
332 optimizel (GASL_comp gy (GASL_comp gy' gl)) | Just x <- optpair gy gy' = optimizel $ gaslcat x gl
333 optimizel (GASL_comp gy (GASL_Y gy')) | Just x <- optpair gy gy' = GASL_comp (optimizey gy) (GASL_Y gy')
334 optimizel (GASL_comp gy gl) = GASL_comp (optimizey gy) (optimizel gl)
336 --optimize' (GAS_loopl GAS_id ) = GAS_id
337 --optimize' (GAS_loopr GAS_id ) = GAS_id
338 --optimize_pair f GAS_drop = Just $ GAS_drop
340 optimize_pair (GAS_first f) GAS_cancelr = Just $ GAS_comp GAS_cancelr f
341 optimize_pair (GAS_second f) GAS_cancell = Just $ GAS_comp GAS_cancell f
342 optimize_pair GAS_uncancelr (GAS_first f) = Just $ GAS_comp f GAS_uncancelr
343 optimize_pair GAS_uncancell (GAS_second f) = Just $ GAS_comp f GAS_uncancell
344 optimize_pair (GAS_second f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_first f)
345 optimize_pair (GAS_first f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_second f)
346 optimize_pair GAS_swap GAS_swap = Just $ GAS_id
347 optimize_pair GAS_swap GAS_cancell = Just $ GAS_cancelr
348 optimize_pair GAS_swap GAS_cancelr = Just $ GAS_cancell
349 optimize_pair GAS_assoc GAS_cancell = Just $ GAS_first GAS_cancell
350 optimize_pair GAS_unassoc GAS_cancelr = Just $ GAS_second GAS_cancelr
351 optimize_pair GAS_assoc (GAS_second GAS_cancell) = Just $ GAS_first GAS_cancelr
352 optimize_pair GAS_unassoc (GAS_first GAS_cancell) = Just $ GAS_cancell
355 optpair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z)
356 optpair (GASY_first gy1) (GASY_first gy2) = liftM gasl_firstify $ optpair gy1 gy2
357 optpair (GASY_second gy1) (GASY_second gy2) = liftM gasl_secondify $ optpair gy1 gy2
358 optpair (GASY_X GASX_uncancell) (GASY_X GASX_cancell) = Just $ GASL_id
359 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_cancelr) = Just $ GASL_id
360 optpair (GASY_X GASX_cancell) (GASY_X GASX_uncancell) = Just $ GASL_id
361 optpair (GASY_X GASX_cancelr) (GASY_X GASX_uncancelr) = Just $ GASL_id
362 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_cancell) = Just $ GASL_id
363 optpair (GASY_X GASX_uncancell) (GASY_X GASX_cancelr) = Just $ GASL_id
364 optpair _ _ = Nothing
366 pushpair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z)
367 pushpair (GASY_first gy1) (GASY_first gy2) = liftM gasl_firstify $ pushpair gy1 gy2
368 pushpair (GASY_second gy1) (GASY_second gy2) = liftM gasl_secondify $ pushpair gy1 gy2
369 pushpair (GASY_first gy1) (GASY_second gy2) = Just $ GASL_comp (GASY_second gy2) (GASL_Y $ GASY_first gy1)
370 pushpair (GASY_second gy1) (GASY_first gy2) = Just $ GASL_comp (GASY_first gy2) (GASL_Y $ GASY_second gy1)
371 pushpair (GASY_first gy1) (GASY_X GASX_unassoc) = Just $ GASL_comp(GASY_X GASX_unassoc) (GASL_Y $ GASY_first (GASY_first gy1))
372 pushpair (GASY_second gy1) (GASY_X GASX_assoc ) = Just $ GASL_comp(GASY_X GASX_assoc ) (GASL_Y $ GASY_second (GASY_second gy1))
373 pushpair (GASY_second (GASY_X GASX_uncancelr)) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_X GASX_uncancelr
374 pushpair (GASY_first (GASY_X GASX_uncancell)) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_X GASX_uncancell
375 pushpair (GASY_X GASX_uncancelr) (GASY_first gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancelr)
376 pushpair (GASY_X GASX_uncancell) (GASY_second gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancell)
377 pushpair (GASY_first (GASY_second gy)) (GASY_X GASX_assoc ) = Just $ GASL_comp (GASY_X GASX_assoc ) $ GASL_Y (GASY_second (GASY_first gy))
378 pushpair (GASY_second (GASY_first gy)) (GASY_X GASX_unassoc ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_first (GASY_second gy))
379 pushpair (GASY_second (GASY_second gy)) (GASY_X GASX_unassoc ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_second gy)
380 pushpair (GASY_first (GASY_first gy)) (GASY_X GASX_assoc ) = Just $ GASL_comp (GASY_X GASX_assoc) $ GASL_Y (GASY_first gy)
381 pushpair (GASY_X GASX_uncancell) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_uncancell
382 pushpair (GASY_X GASX_uncancelr) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancelr
383 pushpair (GASY_first (GASY_X GASX_uncancelr)) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancell
384 pushpair (GASY_second (GASY_X GASX_uncancell)) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_uncancelr
385 pushpair (GASY_first gy) (GASY_X GASX_swap ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_second gy)
386 pushpair (GASY_second gy) (GASY_X GASX_swap ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_first gy)
387 pushpair (GASY_X GASX_uncancell) (GASY_X GASX_swap ) = Just $ GASL_Y $ GASY_X $ GASX_uncancelr
388 pushpair (GASY_X GASX_uncancelr) (GASY_X GASX_swap ) = Just $ GASL_Y $ GASY_X $ GASX_uncancell
389 pushpair _ _ = Nothing
391 -- pushright can only return True for central morphisms
392 pushright :: GArrowSkeletonY m x y -> Bool
393 pushright (GASY_first gy) = pushright gy
394 pushright (GASY_second gy) = pushright gy
395 pushright (GASY_X GASX_uncancell) = True
396 pushright (GASY_X GASX_uncancelr) = True
397 pushright (GASY_X _ ) = False
399 optimizey :: GArrowSkeletonY m x y -> GArrowSkeletonY m x y
400 optimizey (GASY_X gx) = GASY_X $ optimizex gx
401 optimizey (GASY_first gy) = GASY_first (optimizey gy)
402 optimizey (GASY_second gy) = GASY_second (optimizey gy)
404 optimizex :: GArrowSkeletonX m x y -> GArrowSkeletonX m x y
405 optimizex (GASX_const k) = GASX_const k
406 optimizex (GASX_cancell) = GASX_cancell
407 optimizex (GASX_cancelr) = GASX_cancelr
408 optimizex (GASX_uncancell) = GASX_uncancell
409 optimizex (GASX_uncancelr) = GASX_uncancelr
410 optimizex (GASX_assoc) = GASX_assoc
411 optimizex (GASX_unassoc) = GASX_unassoc
412 optimizex (GASX_drop) = GASX_drop
413 optimizex (GASX_copy) = GASX_copy
414 optimizex (GASX_swap) = GASX_swap
415 optimizex (GASX_merge) = GASX_merge
416 optimizex (GASX_misc m) = GASX_misc m
417 optimizex (GASX_loopl gl) = GASX_loopl $ optimizel gl
418 optimizex (GASX_loopr gl) = GASX_loopr $ optimizel gl