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 = repeat beautify'
211 beautify' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
212 beautify' (GAS_comp (GAS_comp f g) h) = beautify' $ GAS_comp f $ GAS_comp g h
213 beautify' (GAS_comp f (GAS_comp (GAS_comp g h) k)) = beautify' $ 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 GAS_id) = f
219 beautify' (GAS_comp GAS_id f) = f
220 beautify' (GAS_comp f g) = case (beautify' f, beautify' g) of
221 (GAS_first f' , GAS_first g') -> GAS_first (GAS_comp f' g')
222 (GAS_second f', GAS_second g') -> GAS_second (GAS_comp f' g')
223 (f' , g' ) -> GAS_comp f' g'
224 beautify' (GAS_first f) = GAS_first $ beautify' f
225 beautify' (GAS_second f) = GAS_second $ beautify' f
226 beautify' (GAS_loopl f) = GAS_loopl $ beautify' f
227 beautify' (GAS_loopr f) = GAS_loopr $ beautify' f
233 gas2gasl :: GArrowSkeleton m x y -> GArrowSkeletonL m x y
234 gas2gasl (GAS_const k ) = GASL_Y $ GASY_X $ GASX_const k
235 gas2gasl (GAS_id ) = GASL_id
236 gas2gasl (GAS_comp f g) = gaslcat (gas2gasl f) (gas2gasl g)
237 gas2gasl (GAS_first f) = gasl_firstify $ gas2gasl f
238 gas2gasl (GAS_second f) = gasl_secondify $ gas2gasl f
239 gas2gasl (GAS_cancell ) = GASL_Y $ GASY_X $ GASX_cancell
240 gas2gasl (GAS_cancelr ) = GASL_Y $ GASY_X $ GASX_cancelr
241 gas2gasl (GAS_uncancell ) = GASL_Y $ GASY_X $ GASX_uncancell
242 gas2gasl (GAS_uncancelr ) = GASL_Y $ GASY_X $ GASX_uncancelr
243 gas2gasl (GAS_assoc ) = GASL_Y $ GASY_X $ GASX_assoc
244 gas2gasl (GAS_unassoc ) = GASL_Y $ GASY_X $ GASX_unassoc
245 gas2gasl (GAS_drop ) = GASL_Y $ GASY_X $ GASX_drop
246 gas2gasl (GAS_copy ) = GASL_Y $ GASY_X $ GASX_copy
247 gas2gasl (GAS_swap ) = GASL_Y $ GASY_X $ GASX_swap
248 gas2gasl (GAS_merge ) = GASL_Y $ GASY_X $ GASX_merge
249 gas2gasl (GAS_loopl f) = GASL_Y $ GASY_X $ GASX_loopl $ gas2gasl f
250 gas2gasl (GAS_loopr f) = GASL_Y $ GASY_X $ GASX_loopr $ gas2gasl f
251 gas2gasl (GAS_misc m) = GASL_Y $ GASY_X $ GASX_misc m
253 -- apply "first" to a GASL
254 gasl_firstify :: GArrowSkeletonL m x y -> GArrowSkeletonL m (x,z) (y,z)
255 gasl_firstify (GASL_id ) = GASL_id
256 gasl_firstify (GASL_Y gy ) = GASL_Y $ GASY_first $ gy
257 gasl_firstify (GASL_comp gxq gqy) = GASL_comp (GASY_first gxq) $ gasl_firstify gqy
259 -- apply "second" to a GASL
260 gasl_secondify :: GArrowSkeletonL m x y -> GArrowSkeletonL m (z,x) (z,y)
261 gasl_secondify (GASL_id ) = GASL_id
262 gasl_secondify (GASL_Y gy ) = GASL_Y $ GASY_second $ gy
263 gasl_secondify (GASL_comp gxq gqy) = GASL_comp (GASY_second gxq) $ gasl_secondify gqy
265 -- concatenates two GASL's
266 gaslcat :: GArrowSkeletonL m x y -> GArrowSkeletonL m y z -> GArrowSkeletonL m x z
267 gaslcat (GASL_id ) g' = g'
268 gaslcat (GASL_Y gy ) g' = GASL_comp gy g'
269 gaslcat (GASL_comp gxq gqy) g' = GASL_comp gxq (gaslcat gqy g')
271 data GArrowSkeletonL m :: * -> * -> *
273 GASL_id :: GArrowSkeletonL m x x
274 GASL_Y :: GArrowSkeletonY m x y -> GArrowSkeletonL m x y
275 GASL_comp :: GArrowSkeletonY m x y -> GArrowSkeletonL m y z -> GArrowSkeletonL m x z
277 data GArrowSkeletonY m :: * -> * -> *
279 GASY_X :: GArrowSkeletonX m x y -> GArrowSkeletonY m x y
280 GASY_first :: GArrowSkeletonY m x y -> GArrowSkeletonY m (x,z) (y,z)
281 GASY_second :: GArrowSkeletonY m x y -> GArrowSkeletonY m (z,x) (z,y)
283 data GArrowSkeletonX m :: * -> * -> *
285 GASX_const :: Int -> GArrowSkeletonX m () Int
286 GASX_cancell :: GArrowSkeletonX m ((),x) x
287 GASX_cancelr :: GArrowSkeletonX m (x,()) x
288 GASX_uncancell :: GArrowSkeletonX m x ((),x)
289 GASX_uncancelr :: GArrowSkeletonX m x (x,())
290 GASX_assoc :: GArrowSkeletonX m ((x,y),z) (x,(y,z))
291 GASX_unassoc :: GArrowSkeletonX m (x,(y,z)) ((x,y),z)
292 GASX_drop :: GArrowSkeletonX m x ()
293 GASX_copy :: GArrowSkeletonX m x (x,x)
294 GASX_swap :: GArrowSkeletonX m (x,y) (y,x)
295 GASX_merge :: GArrowSkeletonX m (x,y) z
296 GASX_misc :: m x y -> GArrowSkeletonX m x y
297 GASX_loopl :: GArrowSkeletonL m (z,x) (z,y) -> GArrowSkeletonX m x y
298 GASX_loopr :: GArrowSkeletonL m (x,z) (y,z) -> GArrowSkeletonX m x y
300 -- TO DO: gather "maximal chunks" of ga_first/ga_second
301 gasl2gas :: GArrowSkeletonL m x y -> GArrowSkeleton m x y
302 gasl2gas GASL_id = GAS_id
303 gasl2gas (GASL_Y gy ) = gasy2gas gy
304 gasl2gas (GASL_comp gy gl) = GAS_comp (gasy2gas gy) (gasl2gas gl)
306 gasy2gas :: GArrowSkeletonY m x y -> GArrowSkeleton m x y
307 gasy2gas (GASY_X gx) = gasx2gas gx
308 gasy2gas (GASY_first gy) = GAS_first (gasy2gas gy)
309 gasy2gas (GASY_second gy) = GAS_second (gasy2gas gy)
311 gasx2gas :: GArrowSkeletonX m x y -> GArrowSkeleton m x y
312 gasx2gas (GASX_const k) = GAS_const k
313 gasx2gas (GASX_cancell) = GAS_cancell
314 gasx2gas (GASX_cancelr) = GAS_cancelr
315 gasx2gas (GASX_uncancell) = GAS_uncancell
316 gasx2gas (GASX_uncancelr) = GAS_uncancelr
317 gasx2gas (GASX_assoc) = GAS_assoc
318 gasx2gas (GASX_unassoc) = GAS_unassoc
319 gasx2gas (GASX_drop) = GAS_drop
320 gasx2gas (GASX_copy) = GAS_copy
321 gasx2gas (GASX_swap) = GAS_swap
322 gasx2gas (GASX_merge) = GAS_merge
323 gasx2gas (GASX_misc m) = GAS_misc m
324 gasx2gas (GASX_loopl gl) = GAS_loopl $ gasl2gas gl
325 gasx2gas (GASX_loopr gl) = GAS_loopr $ gasl2gas gl
329 optimizel :: GArrowSkeletonL m x y -> GArrowSkeletonL m x y
330 optimizel (GASL_id ) = GASL_id
331 optimizel (GASL_Y gy ) = GASL_Y $ optimizey 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' = x
334 optimizel (GASL_comp gy (GASL_comp gy' gl)) | pushright gy, not (pushright gy'), Just x <- swappair gy gy' = optimizel $ gaslcat x gl
335 optimizel (GASL_comp gy (GASL_Y gy')) | pushright gy, not (pushright gy'), Just x <- swappair gy gy' = GASL_comp (optimizey gy) (GASL_Y gy')
336 optimizel (GASL_comp gy gl) = GASL_comp (optimizey gy) (optimizel gl)
338 --optimize' (GAS_loopl GAS_id ) = GAS_id
339 --optimize' (GAS_loopr GAS_id ) = GAS_id
340 --optimize_pair f GAS_drop = Just $ GAS_drop
342 optimize_pair (GAS_first f) GAS_cancelr = Just $ GAS_comp GAS_cancelr f
343 optimize_pair (GAS_second f) GAS_cancell = Just $ GAS_comp GAS_cancell f
344 optimize_pair GAS_uncancelr (GAS_first f) = Just $ GAS_comp f GAS_uncancelr
345 optimize_pair GAS_uncancell (GAS_second f) = Just $ GAS_comp f GAS_uncancell
346 optimize_pair (GAS_second f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_first f)
347 optimize_pair (GAS_first f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_second f)
348 optimize_pair GAS_swap GAS_swap = Just $ GAS_id
349 optimize_pair GAS_swap GAS_cancell = Just $ GAS_cancelr
350 optimize_pair GAS_swap GAS_cancelr = Just $ GAS_cancell
351 optimize_pair GAS_assoc GAS_cancell = Just $ GAS_first GAS_cancell
352 optimize_pair GAS_unassoc GAS_cancelr = Just $ GAS_second GAS_cancelr
353 optimize_pair GAS_assoc (GAS_second GAS_cancell) = Just $ GAS_first GAS_cancelr
354 optimize_pair GAS_unassoc (GAS_first GAS_cancell) = Just $ GAS_cancell
357 optpair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z)
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 (GASY_X GASX_assoc) (GASY_X GASX_cancell) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_cancell
365 optpair (GASY_X GASX_unassoc) (GASY_X GASX_cancelr) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_cancelr
366 optpair (GASY_second (GASY_X GASX_uncancelr)) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_X GASX_uncancelr
367 optpair (GASY_first (GASY_X GASX_uncancell)) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_X GASX_uncancell
368 optpair (GASY_X GASX_uncancell) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_uncancell
369 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancelr
370 optpair (GASY_first (GASY_X GASX_uncancelr)) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancell
371 optpair (GASY_second (GASY_X GASX_uncancell)) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_uncancelr
372 optpair (GASY_X GASX_uncancell) (GASY_X GASX_swap ) = Just $ GASL_Y $ GASY_X $ GASX_uncancelr
373 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_swap ) = Just $ GASL_Y $ GASY_X $ GASX_uncancell
374 optpair (GASY_X GASX_assoc) (GASY_second (GASY_X GASX_cancelr)) = Just $ GASL_Y $ GASY_X $ GASX_cancelr
375 optpair (GASY_X GASX_unassoc) (GASY_first (GASY_X GASX_cancell)) = Just $ GASL_Y $ GASY_X $ GASX_cancell
376 optpair (GASY_first g) (GASY_X GASX_cancelr) = Just $ GASL_comp (GASY_X GASX_cancelr) $ GASL_Y $ g
377 optpair (GASY_second g) (GASY_X GASX_cancell) = Just $ GASL_comp (GASY_X GASX_cancell) $ GASL_Y $ g
378 optpair (GASY_X GASX_uncancelr) (GASY_first g) = Just $ GASL_comp g $ GASL_Y (GASY_X GASX_uncancelr)
379 optpair (GASY_X GASX_uncancell) (GASY_second g) = Just $ GASL_comp g $ GASL_Y (GASY_X GASX_uncancell)
381 optpair (GASY_X GASX_uncancelr) (GASY_X (GASX_loopl gl)) =
382 Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ GASY_X GASX_uncancelr) gl)
383 optpair (GASY_X GASX_uncancell) (GASY_X (GASX_loopl gl)) =
384 Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ GASY_X GASX_uncancell) gl)
385 optpair (GASY_X GASX_uncancelr) (GASY_X (GASX_loopr gl)) =
386 Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ GASY_X GASX_uncancelr) gl)
387 optpair (GASY_X GASX_uncancell) (GASY_X (GASX_loopr gl)) =
388 Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ GASY_X GASX_uncancell) gl)
390 optpair q (GASY_X (GASX_loopl gl)) | pushright q =
391 Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ q) gl)
392 optpair q (GASY_X (GASX_loopr gl)) | pushright q =
393 Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ q) gl)
394 optpair (GASY_first gy1) (GASY_first gy2) = liftM gasl_firstify $ optpair gy1 gy2
395 optpair (GASY_second gy1) (GASY_second gy2) = liftM gasl_secondify $ optpair gy1 gy2
396 optpair _ _ = Nothing
398 swappair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z)
399 swappair (GASY_first gy1) (GASY_second gy2) = Just $ GASL_comp (GASY_second gy2) (GASL_Y $ GASY_first gy1)
400 swappair (GASY_second gy1) (GASY_first gy2) = Just $ GASL_comp (GASY_first gy2) (GASL_Y $ GASY_second gy1)
401 swappair (GASY_first gy1) (GASY_X GASX_unassoc) = Just $ GASL_comp(GASY_X GASX_unassoc) (GASL_Y $ GASY_first (GASY_first gy1))
402 swappair (GASY_second gy1) (GASY_X GASX_assoc ) = Just $ GASL_comp(GASY_X GASX_assoc ) (GASL_Y $ GASY_second (GASY_second gy1))
403 swappair (GASY_X GASX_uncancelr) (GASY_first gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancelr)
404 swappair (GASY_X GASX_uncancell) (GASY_second gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancell)
405 swappair (GASY_first (GASY_second gy)) (GASY_X GASX_assoc ) = Just $ GASL_comp (GASY_X GASX_assoc ) $ GASL_Y (GASY_second (GASY_first gy))
406 swappair (GASY_second (GASY_first gy)) (GASY_X GASX_unassoc ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_first (GASY_second gy))
407 swappair (GASY_second (GASY_second gy)) (GASY_X GASX_unassoc ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_second gy)
408 swappair (GASY_first (GASY_first gy)) (GASY_X GASX_assoc ) = Just $ GASL_comp (GASY_X GASX_assoc) $ GASL_Y (GASY_first gy)
409 swappair (GASY_first gy) (GASY_X GASX_swap ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_second gy)
410 swappair (GASY_second gy) (GASY_X GASX_swap ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_first gy)
411 swappair gy (GASY_X (GASX_loopl gl)) = Just $ GASL_Y $ GASY_X $ GASX_loopl $ GASL_comp (GASY_second gy) gl
412 swappair gy (GASY_X (GASX_loopr gl)) = Just $ GASL_Y $ GASY_X $ GASX_loopr $ GASL_comp (GASY_first gy) gl
413 swappair (GASY_first gy1) (GASY_first gy2) = liftM gasl_firstify $ swappair gy1 gy2
414 swappair (GASY_second gy1) (GASY_second gy2) = liftM gasl_secondify $ swappair gy1 gy2
415 swappair _ _ = Nothing
417 -- pushright can only return True for central morphisms
418 pushright :: GArrowSkeletonY m x y -> Bool
419 pushright (GASY_first gy) = pushright gy
420 pushright (GASY_second gy) = pushright gy
421 pushright (GASY_X GASX_uncancell) = True
422 pushright (GASY_X GASX_uncancelr) = True
423 pushright (GASY_X _ ) = False
425 optimizey :: GArrowSkeletonY m x y -> GArrowSkeletonY m x y
426 optimizey (GASY_X gx) = GASY_X $ optimizex gx
427 optimizey (GASY_first gy) = GASY_first (optimizey gy)
428 optimizey (GASY_second gy) = GASY_second (optimizey gy)
430 optimizex :: GArrowSkeletonX m x y -> GArrowSkeletonX m x y
431 optimizex (GASX_const k) = GASX_const k
432 optimizex (GASX_cancell) = GASX_cancell
433 optimizex (GASX_cancelr) = GASX_cancelr
434 optimizex (GASX_uncancell) = GASX_uncancell
435 optimizex (GASX_uncancelr) = GASX_uncancelr
436 optimizex (GASX_assoc) = GASX_assoc
437 optimizex (GASX_unassoc) = GASX_unassoc
438 optimizex (GASX_drop) = GASX_drop
439 optimizex (GASX_copy) = GASX_copy
440 optimizex (GASX_swap) = GASX_swap
441 optimizex (GASX_merge) = GASX_merge
442 optimizex (GASX_misc m) = GASX_misc m
443 optimizex (GASX_loopl (GASL_comp (GASY_first gy) gl))| pushleft gy = GASX_loopl $ gaslcat gl (GASL_Y $ GASY_first gy)
444 optimizex (GASX_loopr (GASL_comp (GASY_second gy) gl))| pushleft gy = GASX_loopr $ gaslcat gl (GASL_Y $ GASY_second gy)
445 optimizex (GASX_loopl gl) = GASX_loopl $ optimizel gl
446 optimizex (GASX_loopr gl) = GASX_loopr $ optimizel gl
448 pushleft :: GArrowSkeletonY m x y -> Bool
449 pushleft (GASY_first gy) = pushleft gy
450 pushleft (GASY_second gy) = pushleft gy
451 pushleft (GASY_X GASX_cancell) = True
452 pushleft (GASY_X GASX_cancelr) = True
453 pushleft (GASY_X _ ) = False