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 . {- FIXME -} 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)
282 GASY_atomicl :: GArrowSkeletonY m () x -> GArrowSkeletonY m y (x,y)
283 GASY_atomicr :: GArrowSkeletonY m () x -> GArrowSkeletonY m y (y,x)
285 data GArrowSkeletonX m :: * -> * -> *
287 GASX_const :: Int -> GArrowSkeletonX m () Int
288 GASX_cancell :: GArrowSkeletonX m ((),x) x
289 GASX_cancelr :: GArrowSkeletonX m (x,()) x
290 GASX_uncancell :: GArrowSkeletonX m x ((),x)
291 GASX_uncancelr :: GArrowSkeletonX m x (x,())
292 GASX_assoc :: GArrowSkeletonX m ((x,y),z) (x,(y,z))
293 GASX_unassoc :: GArrowSkeletonX m (x,(y,z)) ((x,y),z)
294 GASX_drop :: GArrowSkeletonX m x ()
295 GASX_copy :: GArrowSkeletonX m x (x,x)
296 GASX_swap :: GArrowSkeletonX m (x,y) (y,x)
297 GASX_merge :: GArrowSkeletonX m (x,y) z
298 GASX_misc :: m x y -> GArrowSkeletonX m x y
299 GASX_loopl :: GArrowSkeletonL m (z,x) (z,y) -> GArrowSkeletonX m x y
300 GASX_loopr :: GArrowSkeletonL m (x,z) (y,z) -> GArrowSkeletonX m x y
302 -- TO DO: gather "maximal chunks" of ga_first/ga_second
303 gasl2gas :: GArrowSkeletonL m x y -> GArrowSkeleton m x y
304 gasl2gas GASL_id = GAS_id
305 gasl2gas (GASL_Y gy ) = gasy2gas gy
306 gasl2gas (GASL_comp gy gl) = GAS_comp (gasy2gas gy) (gasl2gas gl)
308 gasy2gas :: GArrowSkeletonY m x y -> GArrowSkeleton m x y
309 gasy2gas (GASY_X gx) = gasx2gas gx
310 gasy2gas (GASY_first gy) = GAS_first (gasy2gas gy)
311 gasy2gas (GASY_second gy) = GAS_second (gasy2gas gy)
312 gasy2gas (GASY_atomicl gy) = GAS_comp GAS_uncancell (GAS_first $ gasy2gas gy)
313 gasy2gas (GASY_atomicr gy) = GAS_comp GAS_uncancelr (GAS_second $ gasy2gas gy)
315 gasx2gas :: GArrowSkeletonX m x y -> GArrowSkeleton m x y
316 gasx2gas (GASX_const k) = GAS_const k
317 gasx2gas (GASX_cancell) = GAS_cancell
318 gasx2gas (GASX_cancelr) = GAS_cancelr
319 gasx2gas (GASX_uncancell) = GAS_uncancell
320 gasx2gas (GASX_uncancelr) = GAS_uncancelr
321 gasx2gas (GASX_assoc) = GAS_assoc
322 gasx2gas (GASX_unassoc) = GAS_unassoc
323 gasx2gas (GASX_drop) = GAS_drop
324 gasx2gas (GASX_copy) = GAS_copy
325 gasx2gas (GASX_swap) = GAS_swap
326 gasx2gas (GASX_merge) = GAS_merge
327 gasx2gas (GASX_misc m) = GAS_misc m
328 gasx2gas (GASX_loopl gl) = GAS_loopl $ gasl2gas gl
329 gasx2gas (GASX_loopr gl) = GAS_loopr $ gasl2gas gl
333 optimizel :: GArrowSkeletonL m x y -> GArrowSkeletonL m x y
334 optimizel (GASL_id ) = GASL_id
335 optimizel (GASL_Y gy ) = GASL_Y $ optimizey gy
336 optimizel (GASL_comp gy (GASL_comp gy' gl)) | Just x <- optpair gy gy' = optimizel $ gaslcat x gl
337 optimizel (GASL_comp gy (GASL_Y gy')) | Just x <- optpair gy gy' = x
338 optimizel (GASL_comp gy (GASL_comp gy' gl)) | pushright gy, not (pushright gy'), Just x <- swappair gy gy' = optimizel $ gaslcat x gl
339 optimizel (GASL_comp gy (GASL_Y gy')) | pushright gy, not (pushright gy'), Just x <- swappair gy gy' = GASL_comp (optimizey gy) (GASL_Y gy')
340 optimizel (GASL_comp gy gl) = GASL_comp (optimizey gy) (optimizel gl)
342 --optimize' (GAS_loopl GAS_id ) = GAS_id
343 --optimize' (GAS_loopr GAS_id ) = GAS_id
344 --optimize_pair f GAS_drop = Just $ GAS_drop
346 optimize_pair (GAS_first f) GAS_cancelr = Just $ GAS_comp GAS_cancelr f
347 optimize_pair (GAS_second f) GAS_cancell = Just $ GAS_comp GAS_cancell f
348 optimize_pair GAS_uncancelr (GAS_first f) = Just $ GAS_comp f GAS_uncancelr
349 optimize_pair GAS_uncancell (GAS_second f) = Just $ GAS_comp f GAS_uncancell
350 optimize_pair (GAS_second f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_first f)
351 optimize_pair (GAS_first f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_second f)
352 optimize_pair GAS_swap GAS_swap = Just $ GAS_id
353 optimize_pair GAS_swap GAS_cancell = Just $ GAS_cancelr
354 optimize_pair GAS_swap GAS_cancelr = Just $ GAS_cancell
355 optimize_pair GAS_assoc GAS_cancell = Just $ GAS_first GAS_cancell
356 optimize_pair GAS_unassoc GAS_cancelr = Just $ GAS_second GAS_cancelr
357 optimize_pair GAS_assoc (GAS_second GAS_cancell) = Just $ GAS_first GAS_cancelr
358 optimize_pair GAS_unassoc (GAS_first GAS_cancell) = Just $ GAS_cancell
361 optpair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z)
363 optpair (GASY_atomicl g) (GASY_X GASX_cancelr) = Just $ GASL_Y g
364 optpair (GASY_atomicr g) (GASY_X GASX_cancell) = Just $ GASL_Y g
366 optpair (GASY_X GASX_uncancell) (GASY_X GASX_cancell) = Just $ GASL_id
367 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_cancelr) = Just $ GASL_id
368 optpair (GASY_X GASX_cancell) (GASY_X GASX_uncancell) = Just $ GASL_id
369 optpair (GASY_X GASX_cancelr) (GASY_X GASX_uncancelr) = Just $ GASL_id
370 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_cancell) = Just $ GASL_id
371 optpair (GASY_X GASX_uncancell) (GASY_X GASX_cancelr) = Just $ GASL_id
372 optpair (GASY_X GASX_assoc) (GASY_X GASX_cancell) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_cancell
373 optpair (GASY_X GASX_unassoc) (GASY_X GASX_cancelr) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_cancelr
374 optpair (GASY_second (GASY_X GASX_uncancelr)) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_X GASX_uncancelr
375 optpair (GASY_first (GASY_X GASX_uncancell)) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_X GASX_uncancell
376 optpair (GASY_X GASX_uncancell) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_uncancell
377 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancelr
378 optpair (GASY_first (GASY_X GASX_uncancelr)) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancell
379 optpair (GASY_second (GASY_X GASX_uncancell)) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_uncancelr
380 optpair (GASY_X GASX_assoc) (GASY_second (GASY_X GASX_cancelr)) = Just $ GASL_Y $ GASY_X $ GASX_cancelr
381 optpair (GASY_X GASX_unassoc) (GASY_first (GASY_X GASX_cancell)) = Just $ GASL_Y $ GASY_X $ GASX_cancell
382 optpair (GASY_first g) (GASY_X GASX_cancelr) = Just $ GASL_comp (GASY_X GASX_cancelr) $ GASL_Y $ g
383 optpair (GASY_second g) (GASY_X GASX_cancell) = Just $ GASL_comp (GASY_X GASX_cancell) $ GASL_Y $ g
384 optpair (GASY_X GASX_uncancelr) (GASY_first g) = Just $ GASL_comp g $ GASL_Y (GASY_X GASX_uncancelr)
385 optpair (GASY_X GASX_uncancell) (GASY_second g) = Just $ GASL_comp g $ GASL_Y (GASY_X GASX_uncancell)
387 -- swap with an {un}cancel{l,r} before/after it
388 optpair (GASY_X GASX_uncancell) (GASY_X GASX_swap ) = Just $ GASL_Y $ GASY_X $ GASX_uncancelr
389 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_swap ) = Just $ GASL_Y $ GASY_X $ GASX_uncancell
390 optpair (GASY_X GASX_swap) (GASY_X GASX_cancell) = Just $ GASL_Y $ GASY_X $ GASX_cancelr
391 optpair (GASY_X GASX_swap) (GASY_X GASX_cancelr) = Just $ GASL_Y $ GASY_X $ GASX_cancell
394 optpair (GASY_X GASX_uncancelr) (GASY_X (GASX_loopl gl)) =
395 Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ GASY_X GASX_uncancelr) gl)
396 optpair (GASY_X GASX_uncancell) (GASY_X (GASX_loopl gl)) =
397 Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ GASY_X GASX_uncancell) gl)
398 optpair (GASY_X GASX_uncancelr) (GASY_X (GASX_loopr gl)) =
399 Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ GASY_X GASX_uncancelr) gl)
400 optpair (GASY_X GASX_uncancell) (GASY_X (GASX_loopr gl)) =
401 Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ GASY_X GASX_uncancell) gl)
403 optpair q (GASY_X (GASX_loopl gl)) | pushin q = Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ q) gl)
404 optpair q (GASY_X (GASX_loopr gl)) | pushin q = Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ q) gl)
406 optpair a@(GASY_X GASX_uncancell) (GASY_first b@(GASY_X (GASX_const c))) = Just $ GASL_Y $ GASY_atomicl b
407 optpair a@(GASY_X GASX_uncancelr) (GASY_second b@(GASY_X (GASX_const c))) = Just $ GASL_Y $ GASY_atomicr b
409 optpair (GASY_first gy1) (GASY_second gy2) | pushleft gy2, not (pushleft gy1)
410 = Just $ GASL_comp (GASY_second gy2) $ GASL_Y $ GASY_first gy1
411 optpair (GASY_second gy1) (GASY_first gy2) | pushleft gy2, not (pushleft gy1)
412 = Just $ GASL_comp (GASY_first gy2) $ GASL_Y $ GASY_second gy1
414 optpair (GASY_first gy1) (GASY_first gy2) = liftM gasl_firstify $ optpair gy1 gy2
415 optpair (GASY_second gy1) (GASY_second gy2) = liftM gasl_secondify $ optpair gy1 gy2
416 optpair _ _ = Nothing
418 swappair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z)
420 swappair q (GASY_atomicl g) = Just $ GASL_comp (GASY_atomicl g) $ GASL_Y $ GASY_second q
421 swappair q (GASY_atomicr g) = Just $ GASL_comp (GASY_atomicr g) $ GASL_Y $ GASY_first q
423 swappair (GASY_first gy1) (GASY_second gy2) = Just $ GASL_comp (GASY_second gy2) (GASL_Y $ GASY_first gy1)
424 swappair (GASY_second gy1) (GASY_first gy2) = Just $ GASL_comp (GASY_first gy2) (GASL_Y $ GASY_second gy1)
425 swappair (GASY_first gy1) (GASY_X GASX_unassoc) = Just $ GASL_comp(GASY_X GASX_unassoc) (GASL_Y $ GASY_first (GASY_first gy1))
426 swappair (GASY_second gy1) (GASY_X GASX_assoc ) = Just $ GASL_comp(GASY_X GASX_assoc ) (GASL_Y $ GASY_second (GASY_second gy1))
427 swappair (GASY_X GASX_uncancelr) (GASY_first gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancelr)
428 swappair (GASY_X GASX_uncancell) (GASY_second gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancell)
429 swappair (GASY_first (GASY_second gy)) (GASY_X GASX_assoc ) = Just $ GASL_comp (GASY_X GASX_assoc ) $ GASL_Y (GASY_second (GASY_first gy))
430 swappair (GASY_second (GASY_first gy)) (GASY_X GASX_unassoc ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_first (GASY_second gy))
431 swappair (GASY_second (GASY_second gy)) (GASY_X GASX_unassoc ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_second gy)
432 swappair (GASY_first (GASY_first gy)) (GASY_X GASX_assoc ) = Just $ GASL_comp (GASY_X GASX_assoc) $ GASL_Y (GASY_first gy)
433 swappair (GASY_first gy) (GASY_X GASX_swap ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_second gy)
434 swappair (GASY_second gy) (GASY_X GASX_swap ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_first gy)
435 swappair gy (GASY_X (GASX_loopl gl)) = Just $ GASL_Y $ GASY_X $ GASX_loopl $ GASL_comp (GASY_second gy) gl
436 swappair gy (GASY_X (GASX_loopr gl)) = Just $ GASL_Y $ GASY_X $ GASX_loopr $ GASL_comp (GASY_first gy) gl
438 swappair (GASY_first gy1) (GASY_first gy2) = liftM gasl_firstify $ swappair gy1 gy2
439 swappair (GASY_second gy1) (GASY_second gy2) = liftM gasl_secondify $ swappair gy1 gy2
440 swappair _ _ = Nothing
442 -- pushright can only return True for central morphisms
443 pushright :: GArrowSkeletonY m x y -> Bool
444 pushright (GASY_first gy) = pushright gy
445 pushright (GASY_second gy) = pushright gy
446 pushright (GASY_atomicl _) = False
447 pushright (GASY_atomicr _) = False
448 pushright (GASY_X GASX_uncancell) = True
449 pushright (GASY_X GASX_uncancelr) = True
450 pushright (GASY_X _ ) = False
452 -- says if we should push it into a loopl/r
453 pushin :: GArrowSkeletonY m x y -> Bool
454 pushin gy = pushright gy || pushin' gy
456 pushin' :: GArrowSkeletonY m a b -> Bool
457 pushin' (GASY_first gy) = pushin' gy
458 pushin' (GASY_second gy) = pushin' gy
459 pushin' (GASY_atomicl _) = False
460 pushin' (GASY_atomicr _) = False
462 -- not sure if these are a good idea
463 pushin' (GASY_X GASX_copy) = True
464 pushin' (GASY_X GASX_swap) = True
466 pushin' (GASY_X _ ) = False
468 optimizey :: GArrowSkeletonY m x y -> GArrowSkeletonY m x y
469 optimizey (GASY_X gx) = GASY_X $ optimizex gx
470 optimizey (GASY_first gy) = GASY_first (optimizey gy)
471 optimizey (GASY_second gy) = GASY_second (optimizey gy)
472 optimizey (GASY_atomicl gy) = GASY_atomicl $ optimizey gy
473 optimizey (GASY_atomicr gy) = GASY_atomicr $ optimizey gy
475 optimizex :: GArrowSkeletonX m x y -> GArrowSkeletonX m x y
476 optimizex (GASX_const k) = GASX_const k
477 optimizex (GASX_cancell) = GASX_cancell
478 optimizex (GASX_cancelr) = GASX_cancelr
479 optimizex (GASX_uncancell) = GASX_uncancell
480 optimizex (GASX_uncancelr) = GASX_uncancelr
481 optimizex (GASX_assoc) = GASX_assoc
482 optimizex (GASX_unassoc) = GASX_unassoc
483 optimizex (GASX_drop) = GASX_drop
484 optimizex (GASX_copy) = GASX_copy
485 optimizex (GASX_swap) = GASX_swap
486 optimizex (GASX_merge) = GASX_merge
487 optimizex (GASX_misc m) = GASX_misc m
488 optimizex (GASX_loopl (GASL_comp (GASY_first gy) gl))| pushleft gy = GASX_loopl $ gaslcat gl (GASL_Y $ GASY_first gy)
489 optimizex (GASX_loopr (GASL_comp (GASY_second gy) gl))| pushleft gy = GASX_loopr $ gaslcat gl (GASL_Y $ GASY_second gy)
490 optimizex (GASX_loopl gl) = GASX_loopl $ optimizel gl
491 optimizex (GASX_loopr gl) = GASX_loopr $ optimizel gl
493 pushleft :: GArrowSkeletonY m x y -> Bool
494 pushleft (GASY_first gy) = pushleft gy
495 pushleft (GASY_second gy) = pushleft gy
496 pushleft (GASY_atomicl _) = False
497 pushleft (GASY_atomicr _) = False
498 pushleft (GASY_X GASX_cancell) = True
499 pushleft (GASY_X GASX_cancelr) = True
500 pushleft (GASY_X _ ) = False