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, skelify)
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
90 skelify :: (forall g . (GArrowCopyDropSwapLoop g, GArrowInclusion g (,) () m) => g x y) -> GArrowSkeleton m x y
94 -- | Simple structural equality on skeletons. NOTE: two skeletons
95 -- with the same shape but different types will nonetheless be "equal";
96 -- there's no way around this since types are gone at runtime.
98 instance Eq ((GArrowSkeleton m) a b)
102 (===) :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) c d -> Bool
103 (GAS_id ) === (GAS_id ) = True
104 (GAS_comp g f) === (GAS_comp g' f') = f===f' && g===g'
105 (GAS_first f) === (GAS_first f') = f===f'
106 (GAS_second f) === (GAS_second f') = f===f'
107 GAS_cancell === GAS_cancell = True
108 GAS_cancelr === GAS_cancelr = True
109 GAS_uncancell === GAS_uncancell = True
110 GAS_uncancelr === GAS_uncancelr = True
111 GAS_drop === GAS_drop = True
112 GAS_copy === GAS_copy = True
113 GAS_swap === GAS_swap = True
114 GAS_assoc === GAS_assoc = True
115 GAS_unassoc === GAS_unassoc = True
116 (GAS_loopl f) === (GAS_loopl f') = f === f'
117 (GAS_loopr f) === (GAS_loopr f') = f === f'
118 (GAS_misc _) === (GAS_misc _) = True -- FIXME
121 data OptimizeFlag = DoOptimize | NoOptimize
123 mkSkeleton :: OptimizeFlag ->
130 ,GArrowInclusion g (,) () m) =>
132 -> GArrowSkeleton m x y
133 mkSkeleton DoOptimize = \g -> (beautify . optimize) g
134 mkSkeleton NoOptimize = \g -> g
139 -- | Performs some very simple-minded optimizations on a
140 -- boxes-and-wires diagram. Preserves equivalence up to the GArrow
141 -- laws, but no guarantees about which optimizations actually happen.
143 optimize :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
144 optimize = repeat (gasl2gas . optimizel . {- FIXME -} optimizel . gas2gasl)
147 optimize x = let x' = optimize' x in if x == x' then x' else optimize x'
149 optimize' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
151 -- Some optimizations fail due to misparenthesization; we default to
152 -- left-associativity and hope for the best
153 optimize' (GAS_comp f (GAS_comp g h) ) = GAS_comp (GAS_comp f g) h
154 optimize' (GAS_comp (GAS_comp f (GAS_comp g h)) k) = GAS_comp (GAS_comp (GAS_comp f g) h) k
155 optimize' (GAS_comp (GAS_comp GAS_unassoc (GAS_second g)) GAS_assoc) = GAS_second (GAS_second g)
156 optimize' (GAS_comp (GAS_comp (GAS_comp f GAS_unassoc) (GAS_second g)) GAS_assoc) = GAS_comp f (GAS_second (GAS_second g))
158 optimize' (GAS_comp (GAS_comp f g) h) = case optimize_pair g h of
159 Nothing -> GAS_comp (optimize' (GAS_comp f g)) h'
160 Just ret' -> GAS_comp f' ret'
165 optimize' (GAS_comp f g ) = case optimize_pair f g of
166 Nothing -> GAS_comp f' g'
171 optimize' (GAS_first GAS_id ) = GAS_id
172 optimize' (GAS_second GAS_id ) = GAS_id
173 -- optimize' (GAS_first (GAS_comp f g)) = GAS_comp (GAS_first f) (GAS_first g)
174 -- optimize' (GAS_second (GAS_comp f g)) = GAS_comp (GAS_second f) (GAS_second g)
175 optimize' (GAS_first f ) = GAS_first $ optimize' f
176 optimize' (GAS_second f ) = GAS_second $ optimize' f
177 optimize' (GAS_loopl GAS_id ) = GAS_id
178 optimize' (GAS_loopr GAS_id ) = GAS_id
179 optimize' (GAS_loopl f ) = GAS_loopl $ optimize' f
180 optimize' (GAS_loopr f ) = GAS_loopr $ optimize' f
183 optimize_pair :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) b c -> Maybe ((GArrowSkeleton m) a c)
185 optimize_pair f GAS_drop = Just $ GAS_drop
186 optimize_pair GAS_id f = Just $ f
187 optimize_pair f GAS_id = Just $ f
188 optimize_pair GAS_uncancell GAS_cancell = Just $ GAS_id
189 optimize_pair GAS_uncancelr GAS_cancelr = Just $ GAS_id
190 optimize_pair GAS_cancell GAS_uncancell = Just $ GAS_id
191 optimize_pair GAS_cancelr GAS_uncancelr = Just $ GAS_id
192 optimize_pair GAS_uncancelr GAS_cancell = Just $ GAS_id
193 optimize_pair GAS_uncancell GAS_cancelr = Just $ GAS_id
195 -- first priority: eliminate GAS_first
196 optimize_pair (GAS_first f) GAS_cancelr = Just $ GAS_comp GAS_cancelr f
197 optimize_pair (GAS_second f) GAS_cancell = Just $ GAS_comp GAS_cancell f
198 optimize_pair GAS_uncancelr (GAS_first f) = Just $ GAS_comp f GAS_uncancelr
199 optimize_pair GAS_uncancell (GAS_second f) = Just $ GAS_comp f GAS_uncancell
201 -- second priority: push GAS_swap leftward
202 optimize_pair (GAS_second f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_first f)
203 optimize_pair (GAS_first f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_second f)
204 optimize_pair GAS_swap GAS_swap = Just $ GAS_id
205 optimize_pair GAS_swap GAS_cancell = Just $ GAS_cancelr
206 optimize_pair GAS_swap GAS_cancelr = Just $ GAS_cancell
208 optimize_pair GAS_assoc GAS_cancell = Just $ GAS_first GAS_cancell
209 optimize_pair GAS_unassoc GAS_cancelr = Just $ GAS_second GAS_cancelr
210 optimize_pair GAS_assoc (GAS_second GAS_cancell) = Just $ GAS_first GAS_cancelr
211 optimize_pair GAS_unassoc (GAS_first GAS_cancell) = Just $ GAS_cancell
214 -- FIXME: valid only for central morphisms
215 --optimize_pair (GAS_second f) (GAS_first g) = Just $ GAS_comp (GAS_first g) (GAS_second f)
216 optimize_pair (GAS_first g) (GAS_second f) = Just $ GAS_comp (GAS_second f) (GAS_first g)
218 optimize_pair _ _ = Nothing
221 repeat :: Eq a => (a -> a) -> a -> a
222 repeat f x = let x' = f x in
228 -- | Recursively turns @(ga_first x >>> first y)@ into @(ga_first (x >>> y))@, likewise for ga_second.
230 beautify :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
231 beautify = repeat beautify'
233 beautify' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
234 beautify' (GAS_comp (GAS_comp f g) h) = beautify' $ GAS_comp f $ GAS_comp g h
235 beautify' (GAS_comp f (GAS_comp (GAS_comp g h) k)) = beautify' $ GAS_comp f $ GAS_comp g $ GAS_comp h k
236 beautify' (GAS_comp f (GAS_comp g h)) = case (beautify' f, beautify' g) of
237 (GAS_first f' , GAS_first g') -> beautify' $ GAS_comp (GAS_first (GAS_comp f' g')) h
238 (GAS_second f', GAS_second g') -> beautify' $ GAS_comp (GAS_second (GAS_comp f' g')) h
239 (f' , g' ) -> GAS_comp f' (beautify' (GAS_comp g h))
240 beautify' (GAS_comp f GAS_id) = f
241 beautify' (GAS_comp GAS_id f) = f
242 beautify' (GAS_comp f g) = case (beautify' f, beautify' g) of
243 (GAS_first f' , GAS_first g') -> GAS_first (GAS_comp f' g')
244 (GAS_second f', GAS_second g') -> GAS_second (GAS_comp f' g')
245 (f' , g' ) -> GAS_comp f' g'
246 beautify' (GAS_first f) = GAS_first $ beautify' f
247 beautify' (GAS_second f) = GAS_second $ beautify' f
248 beautify' (GAS_loopl f) = GAS_loopl $ beautify' f
249 beautify' (GAS_loopr f) = GAS_loopr $ beautify' f
255 gas2gasl :: GArrowSkeleton m x y -> GArrowSkeletonL m x y
256 gas2gasl (GAS_id ) = GASL_id
257 gas2gasl (GAS_comp f g) = gaslcat (gas2gasl f) (gas2gasl g)
258 gas2gasl (GAS_first f) = gasl_firstify $ gas2gasl f
259 gas2gasl (GAS_second f) = gasl_secondify $ gas2gasl f
260 gas2gasl (GAS_cancell ) = GASL_Y $ GASY_X $ GASX_cancell
261 gas2gasl (GAS_cancelr ) = GASL_Y $ GASY_X $ GASX_cancelr
262 gas2gasl (GAS_uncancell ) = GASL_Y $ GASY_X $ GASX_uncancell
263 gas2gasl (GAS_uncancelr ) = GASL_Y $ GASY_X $ GASX_uncancelr
264 gas2gasl (GAS_assoc ) = GASL_Y $ GASY_X $ GASX_assoc
265 gas2gasl (GAS_unassoc ) = GASL_Y $ GASY_X $ GASX_unassoc
266 gas2gasl (GAS_drop ) = GASL_Y $ GASY_X $ GASX_drop
267 gas2gasl (GAS_copy ) = GASL_Y $ GASY_X $ GASX_copy
268 gas2gasl (GAS_swap ) = GASL_Y $ GASY_X $ GASX_swap
269 gas2gasl (GAS_loopl f) = GASL_Y $ GASY_X $ GASX_loopl $ gas2gasl f
270 gas2gasl (GAS_loopr f) = GASL_Y $ GASY_X $ GASX_loopr $ gas2gasl f
271 gas2gasl (GAS_misc m) = GASL_Y $ GASY_X $ GASX_misc m
273 -- apply "first" to a GASL
274 gasl_firstify :: GArrowSkeletonL m x y -> GArrowSkeletonL m (x,z) (y,z)
275 gasl_firstify (GASL_id ) = GASL_id
276 gasl_firstify (GASL_Y gy ) = GASL_Y $ GASY_first $ gy
277 gasl_firstify (GASL_comp gxq gqy) = GASL_comp (GASY_first gxq) $ gasl_firstify gqy
279 -- apply "second" to a GASL
280 gasl_secondify :: GArrowSkeletonL m x y -> GArrowSkeletonL m (z,x) (z,y)
281 gasl_secondify (GASL_id ) = GASL_id
282 gasl_secondify (GASL_Y gy ) = GASL_Y $ GASY_second $ gy
283 gasl_secondify (GASL_comp gxq gqy) = GASL_comp (GASY_second gxq) $ gasl_secondify gqy
285 -- concatenates two GASL's
286 gaslcat :: GArrowSkeletonL m x y -> GArrowSkeletonL m y z -> GArrowSkeletonL m x z
287 gaslcat (GASL_id ) g' = g'
288 gaslcat (GASL_Y gy ) g' = GASL_comp gy g'
289 gaslcat (GASL_comp gxq gqy) g' = GASL_comp gxq (gaslcat gqy g')
291 data GArrowSkeletonL m :: * -> * -> *
293 GASL_id :: GArrowSkeletonL m x x
294 GASL_Y :: GArrowSkeletonY m x y -> GArrowSkeletonL m x y
295 GASL_comp :: GArrowSkeletonY m x y -> GArrowSkeletonL m y z -> GArrowSkeletonL m x z
297 data GArrowSkeletonY m :: * -> * -> *
299 GASY_X :: GArrowSkeletonX m x y -> GArrowSkeletonY m x y
300 GASY_first :: GArrowSkeletonY m x y -> GArrowSkeletonY m (x,z) (y,z)
301 GASY_second :: GArrowSkeletonY m x y -> GArrowSkeletonY m (z,x) (z,y)
302 GASY_atomicl :: GArrowSkeletonY m () x -> GArrowSkeletonY m y (x,y)
303 GASY_atomicr :: GArrowSkeletonY m () x -> GArrowSkeletonY m y (y,x)
305 data GArrowSkeletonX m :: * -> * -> *
307 GASX_cancell :: GArrowSkeletonX m ((),x) x
308 GASX_cancelr :: GArrowSkeletonX m (x,()) x
309 GASX_uncancell :: GArrowSkeletonX m x ((),x)
310 GASX_uncancelr :: GArrowSkeletonX m x (x,())
311 GASX_assoc :: GArrowSkeletonX m ((x,y),z) (x,(y,z))
312 GASX_unassoc :: GArrowSkeletonX m (x,(y,z)) ((x,y),z)
313 GASX_drop :: GArrowSkeletonX m x ()
314 GASX_copy :: GArrowSkeletonX m x (x,x)
315 GASX_swap :: GArrowSkeletonX m (x,y) (y,x)
316 GASX_misc :: m x y -> GArrowSkeletonX m x y
317 GASX_loopl :: GArrowSkeletonL m (z,x) (z,y) -> GArrowSkeletonX m x y
318 GASX_loopr :: GArrowSkeletonL m (x,z) (y,z) -> GArrowSkeletonX m x y
320 -- TO DO: gather "maximal chunks" of ga_first/ga_second
321 gasl2gas :: GArrowSkeletonL m x y -> GArrowSkeleton m x y
322 gasl2gas GASL_id = GAS_id
323 gasl2gas (GASL_Y gy ) = gasy2gas gy
324 gasl2gas (GASL_comp gy gl) = GAS_comp (gasy2gas gy) (gasl2gas gl)
326 gasy2gas :: GArrowSkeletonY m x y -> GArrowSkeleton m x y
327 gasy2gas (GASY_X gx) = gasx2gas gx
328 gasy2gas (GASY_first gy) = GAS_first (gasy2gas gy)
329 gasy2gas (GASY_second gy) = GAS_second (gasy2gas gy)
330 gasy2gas (GASY_atomicl gy) = GAS_comp GAS_uncancell (GAS_first $ gasy2gas gy)
331 gasy2gas (GASY_atomicr gy) = GAS_comp GAS_uncancelr (GAS_second $ gasy2gas gy)
333 gasx2gas :: GArrowSkeletonX m x y -> GArrowSkeleton m x y
334 gasx2gas (GASX_cancell) = GAS_cancell
335 gasx2gas (GASX_cancelr) = GAS_cancelr
336 gasx2gas (GASX_uncancell) = GAS_uncancell
337 gasx2gas (GASX_uncancelr) = GAS_uncancelr
338 gasx2gas (GASX_assoc) = GAS_assoc
339 gasx2gas (GASX_unassoc) = GAS_unassoc
340 gasx2gas (GASX_drop) = GAS_drop
341 gasx2gas (GASX_copy) = GAS_copy
342 gasx2gas (GASX_swap) = GAS_swap
343 gasx2gas (GASX_misc m) = GAS_misc m
344 gasx2gas (GASX_loopl gl) = GAS_loopl $ gasl2gas gl
345 gasx2gas (GASX_loopr gl) = GAS_loopr $ gasl2gas gl
349 optimizel :: GArrowSkeletonL m x y -> GArrowSkeletonL m x y
350 --optimizel (GASL_comp (GASL_Y (GASY_X GAS_uncancelr)) (GASL_Y (GASY_X GASX_copy))) =
351 -- (GASL_comp (GASL_Y (GASY_X GAS_uncancelr)) (GASL_Y (GASY_X GASX_copy)))
352 optimizel (GASL_id ) = GASL_id
353 optimizel (GASL_Y gy ) = GASL_Y $ optimizey gy
354 optimizel (GASL_comp gy (GASL_comp gy' gl)) | Just x <- optpair gy gy' = optimizel $ gaslcat x gl
355 optimizel (GASL_comp gy (GASL_Y gy')) | Just x <- optpair gy gy' = x
356 optimizel (GASL_comp gy (GASL_comp gy' gl)) | pushright gy, not (pushright gy'), Just x <- swappair gy gy' = optimizel $ gaslcat x gl
357 optimizel (GASL_comp gy (GASL_Y gy')) | pushright gy, not (pushright gy'), Just x <- swappair gy gy' = GASL_comp (optimizey gy) (GASL_Y gy')
358 optimizel (GASL_comp gy gl) = GASL_comp (optimizey gy) (optimizel gl)
360 --optimize' (GAS_loopl GAS_id ) = GAS_id
361 --optimize' (GAS_loopr GAS_id ) = GAS_id
362 --optimize_pair f GAS_drop = Just $ GAS_drop
364 optimize_pair (GAS_first f) GAS_cancelr = Just $ GAS_comp GAS_cancelr f
365 optimize_pair (GAS_second f) GAS_cancell = Just $ GAS_comp GAS_cancell f
366 optimize_pair GAS_uncancelr (GAS_first f) = Just $ GAS_comp f GAS_uncancelr
367 optimize_pair GAS_uncancell (GAS_second f) = Just $ GAS_comp f GAS_uncancell
368 optimize_pair (GAS_second f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_first f)
369 optimize_pair (GAS_first f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_second f)
370 optimize_pair GAS_swap GAS_swap = Just $ GAS_id
371 optimize_pair GAS_swap GAS_cancell = Just $ GAS_cancelr
372 optimize_pair GAS_swap GAS_cancelr = Just $ GAS_cancell
373 optimize_pair GAS_assoc GAS_cancell = Just $ GAS_first GAS_cancell
374 optimize_pair GAS_unassoc GAS_cancelr = Just $ GAS_second GAS_cancelr
375 optimize_pair GAS_assoc (GAS_second GAS_cancell) = Just $ GAS_first GAS_cancelr
376 optimize_pair GAS_unassoc (GAS_first GAS_cancell) = Just $ GAS_cancell
379 optpair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z)
381 optpair (GASY_atomicl g) (GASY_X GASX_cancelr) = Just $ GASL_Y g
382 optpair (GASY_atomicr g) (GASY_X GASX_cancell) = Just $ GASL_Y g
384 optpair (GASY_X GASX_uncancell) (GASY_X GASX_cancell) = Just $ GASL_id
385 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_cancelr) = Just $ GASL_id
386 optpair (GASY_X GASX_cancell) (GASY_X GASX_uncancell) = Just $ GASL_id
387 optpair (GASY_X GASX_cancelr) (GASY_X GASX_uncancelr) = Just $ GASL_id
388 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_cancell) = Just $ GASL_id
389 optpair (GASY_X GASX_uncancell) (GASY_X GASX_cancelr) = Just $ GASL_id
390 optpair (GASY_X GASX_assoc) (GASY_X GASX_cancell) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_cancell
391 optpair (GASY_X GASX_unassoc) (GASY_X GASX_cancelr) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_cancelr
392 optpair (GASY_second (GASY_X GASX_uncancelr)) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_X GASX_uncancelr
393 optpair (GASY_first (GASY_X GASX_uncancell)) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_X GASX_uncancell
394 optpair (GASY_X GASX_uncancell) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_uncancell
395 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancelr
396 optpair (GASY_first (GASY_X GASX_uncancelr)) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancell
397 optpair (GASY_second (GASY_X GASX_uncancell)) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_uncancelr
398 optpair (GASY_X GASX_assoc) (GASY_second (GASY_X GASX_cancelr)) = Just $ GASL_Y $ GASY_X $ GASX_cancelr
399 optpair (GASY_X GASX_unassoc) (GASY_first (GASY_X GASX_cancell)) = Just $ GASL_Y $ GASY_X $ GASX_cancell
400 optpair (GASY_first g) (GASY_X GASX_cancelr) = Just $ GASL_comp (GASY_X GASX_cancelr) $ GASL_Y $ g
401 optpair (GASY_second g) (GASY_X GASX_cancell) = Just $ GASL_comp (GASY_X GASX_cancell) $ GASL_Y $ g
402 optpair (GASY_X GASX_uncancelr) (GASY_first g) = Just $ GASL_comp g $ GASL_Y (GASY_X GASX_uncancelr)
403 optpair (GASY_X GASX_uncancell) (GASY_second g) = Just $ GASL_comp g $ GASL_Y (GASY_X GASX_uncancell)
405 -- swap with an {un}cancel{l,r} before/after it
406 optpair (GASY_X GASX_uncancell) (GASY_X GASX_swap ) = Just $ GASL_Y $ GASY_X $ GASX_uncancelr
407 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_swap ) = Just $ GASL_Y $ GASY_X $ GASX_uncancell
408 optpair (GASY_X GASX_swap) (GASY_X GASX_cancell) = Just $ GASL_Y $ GASY_X $ GASX_cancelr
409 optpair (GASY_X GASX_swap) (GASY_X GASX_cancelr) = Just $ GASL_Y $ GASY_X $ GASX_cancell
412 optpair (GASY_X GASX_uncancelr) (GASY_X (GASX_loopl gl)) =
413 Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ GASY_X GASX_uncancelr) gl)
414 optpair (GASY_X GASX_uncancell) (GASY_X (GASX_loopl gl)) =
415 Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ GASY_X GASX_uncancell) gl)
416 optpair (GASY_X GASX_uncancelr) (GASY_X (GASX_loopr gl)) =
417 Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ GASY_X GASX_uncancelr) gl)
418 optpair (GASY_X GASX_uncancell) (GASY_X (GASX_loopr gl)) =
419 Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ GASY_X GASX_uncancell) gl)
421 optpair q (GASY_X (GASX_loopl gl)) | pushin q = Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ q) gl)
422 optpair q (GASY_X (GASX_loopr gl)) | pushin q = Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ q) gl)
424 optpair (GASY_first gy1) (GASY_second gy2) | pushleft gy2, not (pushleft gy1)
425 = Just $ GASL_comp (GASY_second gy2) $ GASL_Y $ GASY_first gy1
426 optpair (GASY_second gy1) (GASY_first gy2) | pushleft gy2, not (pushleft gy1)
427 = Just $ GASL_comp (GASY_first gy2) $ GASL_Y $ GASY_second gy1
429 optpair (GASY_first gy1) (GASY_first gy2) = liftM gasl_firstify $ optpair gy1 gy2
430 optpair (GASY_second gy1) (GASY_second gy2) = liftM gasl_secondify $ optpair gy1 gy2
431 optpair _ _ = Nothing
433 swappair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z)
435 swappair q (GASY_atomicl g) = Just $ GASL_comp (GASY_atomicl g) $ GASL_Y $ GASY_second q
436 swappair q (GASY_atomicr g) = Just $ GASL_comp (GASY_atomicr g) $ GASL_Y $ GASY_first q
438 swappair (GASY_first gy1) (GASY_second gy2) = Just $ GASL_comp (GASY_second gy2) (GASL_Y $ GASY_first gy1)
439 swappair (GASY_second gy1) (GASY_first gy2) = Just $ GASL_comp (GASY_first gy2) (GASL_Y $ GASY_second gy1)
440 swappair (GASY_first gy1) (GASY_X GASX_unassoc) = Just $ GASL_comp(GASY_X GASX_unassoc) (GASL_Y $ GASY_first (GASY_first gy1))
441 swappair (GASY_second gy1) (GASY_X GASX_assoc ) = Just $ GASL_comp(GASY_X GASX_assoc ) (GASL_Y $ GASY_second (GASY_second gy1))
442 swappair (GASY_X GASX_uncancelr) (GASY_first gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancelr)
443 swappair (GASY_X GASX_uncancell) (GASY_second gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancell)
444 swappair (GASY_first (GASY_second gy)) (GASY_X GASX_assoc ) = Just $ GASL_comp (GASY_X GASX_assoc ) $ GASL_Y (GASY_second (GASY_first gy))
445 swappair (GASY_second (GASY_first gy)) (GASY_X GASX_unassoc ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_first (GASY_second gy))
446 swappair (GASY_second (GASY_second gy)) (GASY_X GASX_unassoc ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_second gy)
447 swappair (GASY_first (GASY_first gy)) (GASY_X GASX_assoc ) = Just $ GASL_comp (GASY_X GASX_assoc) $ GASL_Y (GASY_first gy)
448 swappair (GASY_first gy) (GASY_X GASX_swap ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_second gy)
449 swappair (GASY_second gy) (GASY_X GASX_swap ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_first gy)
450 swappair gy (GASY_X (GASX_loopl gl)) = Just $ GASL_Y $ GASY_X $ GASX_loopl $ GASL_comp (GASY_second gy) gl
451 swappair gy (GASY_X (GASX_loopr gl)) = Just $ GASL_Y $ GASY_X $ GASX_loopr $ GASL_comp (GASY_first gy) gl
453 swappair (GASY_first gy1) (GASY_first gy2) = liftM gasl_firstify $ swappair gy1 gy2
454 swappair (GASY_second gy1) (GASY_second gy2) = liftM gasl_secondify $ swappair gy1 gy2
455 swappair _ _ = Nothing
457 -- pushright can only return True for central morphisms
458 pushright :: GArrowSkeletonY m x y -> Bool
459 pushright (GASY_first gy) = pushright gy
460 pushright (GASY_second gy) = pushright gy
461 pushright (GASY_atomicl _) = False
462 pushright (GASY_atomicr _) = False
463 pushright (GASY_X GASX_uncancell) = True
464 pushright (GASY_X GASX_uncancelr) = True
465 pushright (GASY_X _ ) = False
467 -- says if we should push it into a loopl/r
468 pushin :: GArrowSkeletonY m x y -> Bool
469 pushin gy = pushright gy || pushin' gy
471 pushin' :: GArrowSkeletonY m a b -> Bool
472 pushin' (GASY_first gy) = pushin' gy
473 pushin' (GASY_second gy) = pushin' gy
474 pushin' (GASY_atomicl _) = False
475 pushin' (GASY_atomicr _) = False
477 -- not sure if these are a good idea
478 pushin' (GASY_X GASX_copy) = True
479 pushin' (GASY_X GASX_swap) = True
481 pushin' (GASY_X _ ) = False
483 optimizey :: GArrowSkeletonY m x y -> GArrowSkeletonY m x y
484 optimizey (GASY_X gx) = GASY_X $ optimizex gx
485 optimizey (GASY_first gy) = GASY_first (optimizey gy)
486 optimizey (GASY_second gy) = GASY_second (optimizey gy)
487 optimizey (GASY_atomicl gy) = GASY_atomicl $ optimizey gy
488 optimizey (GASY_atomicr gy) = GASY_atomicr $ optimizey gy
490 optimizex :: GArrowSkeletonX m x y -> GArrowSkeletonX m x y
491 optimizex (GASX_cancell) = GASX_cancell
492 optimizex (GASX_cancelr) = GASX_cancelr
493 optimizex (GASX_uncancell) = GASX_uncancell
494 optimizex (GASX_uncancelr) = GASX_uncancelr
495 optimizex (GASX_assoc) = GASX_assoc
496 optimizex (GASX_unassoc) = GASX_unassoc
497 optimizex (GASX_drop) = GASX_drop
498 optimizex (GASX_copy) = GASX_copy
499 optimizex (GASX_swap) = GASX_swap
500 optimizex (GASX_misc m) = GASX_misc m
501 optimizex (GASX_loopl (GASL_comp (GASY_first gy) gl))| pushleft gy = GASX_loopl $ gaslcat gl (GASL_Y $ GASY_first gy)
502 optimizex (GASX_loopr (GASL_comp (GASY_second gy) gl))| pushleft gy = GASX_loopr $ gaslcat gl (GASL_Y $ GASY_second gy)
503 optimizex (GASX_loopl gl) = GASX_loopl $ optimizel gl
504 optimizex (GASX_loopr gl) = GASX_loopr $ optimizel gl
506 pushleft :: GArrowSkeletonY m x y -> Bool
507 pushleft (GASY_first gy) = pushleft gy
508 pushleft (GASY_second gy) = pushleft gy
509 pushleft (GASY_atomicl _) = False
510 pushleft (GASY_atomicr _) = False
511 pushleft (GASY_X GASX_cancell) = True
512 pushleft (GASY_X GASX_cancelr) = True
513 pushleft (GASY_X _ ) = False