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_const :: Int -> GArrowSkeleton m () Int
38 GAS_id :: GArrowSkeleton m x x
39 GAS_comp :: GArrowSkeleton m x y -> GArrowSkeleton m y z -> GArrowSkeleton m x z
40 GAS_first :: GArrowSkeleton m x y -> GArrowSkeleton m (x,z) (y,z)
41 GAS_second :: GArrowSkeleton m x y -> GArrowSkeleton m (z,x) (z,y)
42 GAS_cancell :: GArrowSkeleton m ((),x) x
43 GAS_cancelr :: GArrowSkeleton m (x,()) x
44 GAS_uncancell :: GArrowSkeleton m x ((),x)
45 GAS_uncancelr :: GArrowSkeleton m x (x,())
46 GAS_assoc :: GArrowSkeleton m ((x,y),z) (x,(y,z))
47 GAS_unassoc :: GArrowSkeleton m (x,(y,z)) ((x,y),z)
48 GAS_drop :: GArrowSkeleton m x ()
49 GAS_copy :: GArrowSkeleton m x (x,x)
50 GAS_swap :: GArrowSkeleton m (x,y) (y,x)
51 GAS_merge :: GArrowSkeleton m (x,y) z
52 GAS_loopl :: GArrowSkeleton m (z,x) (z,y) -> GArrowSkeleton m x y
53 GAS_loopr :: GArrowSkeleton m (x,z) (y,z) -> GArrowSkeleton m x y
54 GAS_misc :: m x y -> GArrowSkeleton m x y
56 instance Category (GArrowSkeleton m) where
60 instance GArrow (GArrowSkeleton m) (,) () where
62 ga_second = GAS_second
63 ga_cancell = GAS_cancell
64 ga_cancelr = GAS_cancelr
65 ga_uncancell = GAS_uncancell
66 ga_uncancelr = GAS_uncancelr
68 ga_unassoc = GAS_unassoc
70 instance GArrowDrop (GArrowSkeleton m) (,) () where
73 instance GArrowCopy (GArrowSkeleton m) (,) () where
76 instance GArrowSwap (GArrowSkeleton m) (,) () where
79 instance GArrowLoop (GArrowSkeleton m) (,) () where
83 type instance GArrowTensor (GArrowSkeleton m) = (,)
84 type instance GArrowUnit (GArrowSkeleton m) = ()
85 type instance GArrowExponent (GArrowSkeleton m) = (->)
87 instance GArrowCopyDropSwapLoop (GArrowSkeleton m)
89 instance GArrowInclusion (GArrowSkeleton m) (,) () m where
93 -- | Simple structural equality on skeletons. NOTE: two skeletons
94 -- with the same shape but different types will nonetheless be "equal";
95 -- there's no way around this since types are gone at runtime.
97 instance Eq ((GArrowSkeleton m) a b)
101 (===) :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) c d -> Bool
102 (GAS_id ) === (GAS_id ) = True
103 (GAS_comp g f) === (GAS_comp g' f') = f===f' && g===g'
104 (GAS_first f) === (GAS_first f') = f===f'
105 (GAS_second f) === (GAS_second f') = f===f'
106 GAS_cancell === GAS_cancell = True
107 GAS_cancelr === GAS_cancelr = True
108 GAS_uncancell === GAS_uncancell = True
109 GAS_uncancelr === GAS_uncancelr = True
110 GAS_drop === GAS_drop = True
111 (GAS_const i) === (GAS_const i') = i==i'
112 GAS_copy === GAS_copy = True
113 GAS_merge === GAS_merge = True
114 GAS_swap === GAS_swap = True
115 GAS_assoc === GAS_assoc = True
116 GAS_unassoc === GAS_unassoc = True
117 (GAS_loopl f) === (GAS_loopl f') = f === f'
118 (GAS_loopr f) === (GAS_loopr f') = f === f'
119 (GAS_misc _) === (GAS_misc _) = True -- FIXME
122 data OptimizeFlag = DoOptimize | NoOptimize
124 mkSkeleton :: OptimizeFlag ->
131 ,GArrowInclusion g (,) () m) =>
133 -> GArrowSkeleton m x y
134 mkSkeleton DoOptimize = \g -> (beautify . optimize) g
135 mkSkeleton NoOptimize = \g -> g
140 -- | Performs some very simple-minded optimizations on a
141 -- boxes-and-wires diagram. Preserves equivalence up to the GArrow
142 -- laws, but no guarantees about which optimizations actually happen.
144 optimize :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
145 optimize = repeat (gasl2gas . optimizel . {- FIXME -} optimizel . gas2gasl)
148 optimize x = let x' = optimize' x in if x == x' then x' else optimize x'
150 optimize' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
152 -- Some optimizations fail due to misparenthesization; we default to
153 -- left-associativity and hope for the best
154 optimize' (GAS_comp f (GAS_comp g h) ) = GAS_comp (GAS_comp f g) h
155 optimize' (GAS_comp (GAS_comp f (GAS_comp g h)) k) = GAS_comp (GAS_comp (GAS_comp f g) h) k
156 optimize' (GAS_comp (GAS_comp GAS_unassoc (GAS_second g)) GAS_assoc) = GAS_second (GAS_second g)
157 optimize' (GAS_comp (GAS_comp (GAS_comp f GAS_unassoc) (GAS_second g)) GAS_assoc) = GAS_comp f (GAS_second (GAS_second g))
159 optimize' (GAS_comp (GAS_comp f g) h) = case optimize_pair g h of
160 Nothing -> GAS_comp (optimize' (GAS_comp f g)) h'
161 Just ret' -> GAS_comp f' ret'
166 optimize' (GAS_comp f g ) = case optimize_pair f g of
167 Nothing -> GAS_comp f' g'
172 optimize' (GAS_first GAS_id ) = GAS_id
173 optimize' (GAS_second GAS_id ) = GAS_id
174 -- optimize' (GAS_first (GAS_comp f g)) = GAS_comp (GAS_first f) (GAS_first g)
175 -- optimize' (GAS_second (GAS_comp f g)) = GAS_comp (GAS_second f) (GAS_second g)
176 optimize' (GAS_first f ) = GAS_first $ optimize' f
177 optimize' (GAS_second f ) = GAS_second $ optimize' f
178 optimize' (GAS_loopl GAS_id ) = GAS_id
179 optimize' (GAS_loopr GAS_id ) = GAS_id
180 optimize' (GAS_loopl f ) = GAS_loopl $ optimize' f
181 optimize' (GAS_loopr f ) = GAS_loopr $ optimize' f
184 optimize_pair :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) b c -> Maybe ((GArrowSkeleton m) a c)
186 optimize_pair f GAS_drop = Just $ GAS_drop
187 optimize_pair GAS_id f = Just $ f
188 optimize_pair f GAS_id = Just $ f
189 optimize_pair GAS_uncancell GAS_cancell = Just $ GAS_id
190 optimize_pair GAS_uncancelr GAS_cancelr = Just $ GAS_id
191 optimize_pair GAS_cancell GAS_uncancell = Just $ GAS_id
192 optimize_pair GAS_cancelr GAS_uncancelr = Just $ GAS_id
193 optimize_pair GAS_uncancelr GAS_cancell = Just $ GAS_id
194 optimize_pair GAS_uncancell GAS_cancelr = Just $ GAS_id
196 -- first priority: eliminate GAS_first
197 optimize_pair (GAS_first f) GAS_cancelr = Just $ GAS_comp GAS_cancelr f
198 optimize_pair (GAS_second f) GAS_cancell = Just $ GAS_comp GAS_cancell f
199 optimize_pair GAS_uncancelr (GAS_first f) = Just $ GAS_comp f GAS_uncancelr
200 optimize_pair GAS_uncancell (GAS_second f) = Just $ GAS_comp f GAS_uncancell
202 -- second priority: push GAS_swap leftward
203 optimize_pair (GAS_second f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_first f)
204 optimize_pair (GAS_first f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_second f)
205 optimize_pair GAS_swap GAS_swap = Just $ GAS_id
206 optimize_pair GAS_swap GAS_cancell = Just $ GAS_cancelr
207 optimize_pair GAS_swap GAS_cancelr = Just $ GAS_cancell
209 optimize_pair GAS_assoc GAS_cancell = Just $ GAS_first GAS_cancell
210 optimize_pair GAS_unassoc GAS_cancelr = Just $ GAS_second GAS_cancelr
211 optimize_pair GAS_assoc (GAS_second GAS_cancell) = Just $ GAS_first GAS_cancelr
212 optimize_pair GAS_unassoc (GAS_first GAS_cancell) = Just $ GAS_cancell
215 -- FIXME: valid only for central morphisms
216 --optimize_pair (GAS_second f) (GAS_first g) = Just $ GAS_comp (GAS_first g) (GAS_second f)
217 optimize_pair (GAS_first g) (GAS_second f) = Just $ GAS_comp (GAS_second f) (GAS_first g)
219 optimize_pair _ _ = Nothing
222 repeat :: Eq a => (a -> a) -> a -> a
223 repeat f x = let x' = f x in
229 -- | Recursively turns @(ga_first x >>> first y)@ into @(ga_first (x >>> y))@, likewise for ga_second.
231 beautify :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
232 beautify = repeat beautify'
234 beautify' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
235 beautify' (GAS_comp (GAS_comp f g) h) = beautify' $ GAS_comp f $ GAS_comp g h
236 beautify' (GAS_comp f (GAS_comp (GAS_comp g h) k)) = beautify' $ GAS_comp f $ GAS_comp g $ GAS_comp h k
237 beautify' (GAS_comp f (GAS_comp g h)) = case (beautify' f, beautify' g) of
238 (GAS_first f' , GAS_first g') -> beautify' $ GAS_comp (GAS_first (GAS_comp f' g')) h
239 (GAS_second f', GAS_second g') -> beautify' $ GAS_comp (GAS_second (GAS_comp f' g')) h
240 (f' , g' ) -> GAS_comp f' (beautify' (GAS_comp g h))
241 beautify' (GAS_comp f GAS_id) = f
242 beautify' (GAS_comp GAS_id f) = f
243 beautify' (GAS_comp f g) = case (beautify' f, beautify' g) of
244 (GAS_first f' , GAS_first g') -> GAS_first (GAS_comp f' g')
245 (GAS_second f', GAS_second g') -> GAS_second (GAS_comp f' g')
246 (f' , g' ) -> GAS_comp f' g'
247 beautify' (GAS_first f) = GAS_first $ beautify' f
248 beautify' (GAS_second f) = GAS_second $ beautify' f
249 beautify' (GAS_loopl f) = GAS_loopl $ beautify' f
250 beautify' (GAS_loopr f) = GAS_loopr $ beautify' f
256 gas2gasl :: GArrowSkeleton m x y -> GArrowSkeletonL m x y
257 gas2gasl (GAS_const k ) = GASL_Y $ GASY_X $ GASX_const k
258 gas2gasl (GAS_id ) = GASL_id
259 gas2gasl (GAS_comp f g) = gaslcat (gas2gasl f) (gas2gasl g)
260 gas2gasl (GAS_first f) = gasl_firstify $ gas2gasl f
261 gas2gasl (GAS_second f) = gasl_secondify $ gas2gasl f
262 gas2gasl (GAS_cancell ) = GASL_Y $ GASY_X $ GASX_cancell
263 gas2gasl (GAS_cancelr ) = GASL_Y $ GASY_X $ GASX_cancelr
264 gas2gasl (GAS_uncancell ) = GASL_Y $ GASY_X $ GASX_uncancell
265 gas2gasl (GAS_uncancelr ) = GASL_Y $ GASY_X $ GASX_uncancelr
266 gas2gasl (GAS_assoc ) = GASL_Y $ GASY_X $ GASX_assoc
267 gas2gasl (GAS_unassoc ) = GASL_Y $ GASY_X $ GASX_unassoc
268 gas2gasl (GAS_drop ) = GASL_Y $ GASY_X $ GASX_drop
269 gas2gasl (GAS_copy ) = GASL_Y $ GASY_X $ GASX_copy
270 gas2gasl (GAS_swap ) = GASL_Y $ GASY_X $ GASX_swap
271 gas2gasl (GAS_merge ) = GASL_Y $ GASY_X $ GASX_merge
272 gas2gasl (GAS_loopl f) = GASL_Y $ GASY_X $ GASX_loopl $ gas2gasl f
273 gas2gasl (GAS_loopr f) = GASL_Y $ GASY_X $ GASX_loopr $ gas2gasl f
274 gas2gasl (GAS_misc m) = GASL_Y $ GASY_X $ GASX_misc m
276 -- apply "first" to a GASL
277 gasl_firstify :: GArrowSkeletonL m x y -> GArrowSkeletonL m (x,z) (y,z)
278 gasl_firstify (GASL_id ) = GASL_id
279 gasl_firstify (GASL_Y gy ) = GASL_Y $ GASY_first $ gy
280 gasl_firstify (GASL_comp gxq gqy) = GASL_comp (GASY_first gxq) $ gasl_firstify gqy
282 -- apply "second" to a GASL
283 gasl_secondify :: GArrowSkeletonL m x y -> GArrowSkeletonL m (z,x) (z,y)
284 gasl_secondify (GASL_id ) = GASL_id
285 gasl_secondify (GASL_Y gy ) = GASL_Y $ GASY_second $ gy
286 gasl_secondify (GASL_comp gxq gqy) = GASL_comp (GASY_second gxq) $ gasl_secondify gqy
288 -- concatenates two GASL's
289 gaslcat :: GArrowSkeletonL m x y -> GArrowSkeletonL m y z -> GArrowSkeletonL m x z
290 gaslcat (GASL_id ) g' = g'
291 gaslcat (GASL_Y gy ) g' = GASL_comp gy g'
292 gaslcat (GASL_comp gxq gqy) g' = GASL_comp gxq (gaslcat gqy g')
294 data GArrowSkeletonL m :: * -> * -> *
296 GASL_id :: GArrowSkeletonL m x x
297 GASL_Y :: GArrowSkeletonY m x y -> GArrowSkeletonL m x y
298 GASL_comp :: GArrowSkeletonY m x y -> GArrowSkeletonL m y z -> GArrowSkeletonL m x z
300 data GArrowSkeletonY m :: * -> * -> *
302 GASY_X :: GArrowSkeletonX m x y -> GArrowSkeletonY m x y
303 GASY_first :: GArrowSkeletonY m x y -> GArrowSkeletonY m (x,z) (y,z)
304 GASY_second :: GArrowSkeletonY m x y -> GArrowSkeletonY m (z,x) (z,y)
305 GASY_atomicl :: GArrowSkeletonY m () x -> GArrowSkeletonY m y (x,y)
306 GASY_atomicr :: GArrowSkeletonY m () x -> GArrowSkeletonY m y (y,x)
308 data GArrowSkeletonX m :: * -> * -> *
310 GASX_const :: Int -> GArrowSkeletonX m () Int
311 GASX_cancell :: GArrowSkeletonX m ((),x) x
312 GASX_cancelr :: GArrowSkeletonX m (x,()) x
313 GASX_uncancell :: GArrowSkeletonX m x ((),x)
314 GASX_uncancelr :: GArrowSkeletonX m x (x,())
315 GASX_assoc :: GArrowSkeletonX m ((x,y),z) (x,(y,z))
316 GASX_unassoc :: GArrowSkeletonX m (x,(y,z)) ((x,y),z)
317 GASX_drop :: GArrowSkeletonX m x ()
318 GASX_copy :: GArrowSkeletonX m x (x,x)
319 GASX_swap :: GArrowSkeletonX m (x,y) (y,x)
320 GASX_merge :: GArrowSkeletonX m (x,y) z
321 GASX_misc :: m x y -> GArrowSkeletonX m x y
322 GASX_loopl :: GArrowSkeletonL m (z,x) (z,y) -> GArrowSkeletonX m x y
323 GASX_loopr :: GArrowSkeletonL m (x,z) (y,z) -> GArrowSkeletonX m x y
325 -- TO DO: gather "maximal chunks" of ga_first/ga_second
326 gasl2gas :: GArrowSkeletonL m x y -> GArrowSkeleton m x y
327 gasl2gas GASL_id = GAS_id
328 gasl2gas (GASL_Y gy ) = gasy2gas gy
329 gasl2gas (GASL_comp gy gl) = GAS_comp (gasy2gas gy) (gasl2gas gl)
331 gasy2gas :: GArrowSkeletonY m x y -> GArrowSkeleton m x y
332 gasy2gas (GASY_X gx) = gasx2gas gx
333 gasy2gas (GASY_first gy) = GAS_first (gasy2gas gy)
334 gasy2gas (GASY_second gy) = GAS_second (gasy2gas gy)
335 gasy2gas (GASY_atomicl gy) = GAS_comp GAS_uncancell (GAS_first $ gasy2gas gy)
336 gasy2gas (GASY_atomicr gy) = GAS_comp GAS_uncancelr (GAS_second $ gasy2gas gy)
338 gasx2gas :: GArrowSkeletonX m x y -> GArrowSkeleton m x y
339 gasx2gas (GASX_const k) = GAS_const k
340 gasx2gas (GASX_cancell) = GAS_cancell
341 gasx2gas (GASX_cancelr) = GAS_cancelr
342 gasx2gas (GASX_uncancell) = GAS_uncancell
343 gasx2gas (GASX_uncancelr) = GAS_uncancelr
344 gasx2gas (GASX_assoc) = GAS_assoc
345 gasx2gas (GASX_unassoc) = GAS_unassoc
346 gasx2gas (GASX_drop) = GAS_drop
347 gasx2gas (GASX_copy) = GAS_copy
348 gasx2gas (GASX_swap) = GAS_swap
349 gasx2gas (GASX_merge) = GAS_merge
350 gasx2gas (GASX_misc m) = GAS_misc m
351 gasx2gas (GASX_loopl gl) = GAS_loopl $ gasl2gas gl
352 gasx2gas (GASX_loopr gl) = GAS_loopr $ gasl2gas gl
356 optimizel :: GArrowSkeletonL m x y -> GArrowSkeletonL m x y
357 optimizel (GASL_id ) = GASL_id
358 optimizel (GASL_Y gy ) = GASL_Y $ optimizey gy
359 optimizel (GASL_comp gy (GASL_comp gy' gl)) | Just x <- optpair gy gy' = optimizel $ gaslcat x gl
360 optimizel (GASL_comp gy (GASL_Y gy')) | Just x <- optpair gy gy' = x
361 optimizel (GASL_comp gy (GASL_comp gy' gl)) | pushright gy, not (pushright gy'), Just x <- swappair gy gy' = optimizel $ gaslcat x gl
362 optimizel (GASL_comp gy (GASL_Y gy')) | pushright gy, not (pushright gy'), Just x <- swappair gy gy' = GASL_comp (optimizey gy) (GASL_Y gy')
363 optimizel (GASL_comp gy gl) = GASL_comp (optimizey gy) (optimizel gl)
365 --optimize' (GAS_loopl GAS_id ) = GAS_id
366 --optimize' (GAS_loopr GAS_id ) = GAS_id
367 --optimize_pair f GAS_drop = Just $ GAS_drop
369 optimize_pair (GAS_first f) GAS_cancelr = Just $ GAS_comp GAS_cancelr f
370 optimize_pair (GAS_second f) GAS_cancell = Just $ GAS_comp GAS_cancell f
371 optimize_pair GAS_uncancelr (GAS_first f) = Just $ GAS_comp f GAS_uncancelr
372 optimize_pair GAS_uncancell (GAS_second f) = Just $ GAS_comp f GAS_uncancell
373 optimize_pair (GAS_second f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_first f)
374 optimize_pair (GAS_first f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_second f)
375 optimize_pair GAS_swap GAS_swap = Just $ GAS_id
376 optimize_pair GAS_swap GAS_cancell = Just $ GAS_cancelr
377 optimize_pair GAS_swap GAS_cancelr = Just $ GAS_cancell
378 optimize_pair GAS_assoc GAS_cancell = Just $ GAS_first GAS_cancell
379 optimize_pair GAS_unassoc GAS_cancelr = Just $ GAS_second GAS_cancelr
380 optimize_pair GAS_assoc (GAS_second GAS_cancell) = Just $ GAS_first GAS_cancelr
381 optimize_pair GAS_unassoc (GAS_first GAS_cancell) = Just $ GAS_cancell
384 optpair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z)
386 optpair (GASY_atomicl g) (GASY_X GASX_cancelr) = Just $ GASL_Y g
387 optpair (GASY_atomicr g) (GASY_X GASX_cancell) = Just $ GASL_Y g
389 optpair (GASY_X GASX_uncancell) (GASY_X GASX_cancell) = Just $ GASL_id
390 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_cancelr) = Just $ GASL_id
391 optpair (GASY_X GASX_cancell) (GASY_X GASX_uncancell) = Just $ GASL_id
392 optpair (GASY_X GASX_cancelr) (GASY_X GASX_uncancelr) = Just $ GASL_id
393 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_cancell) = Just $ GASL_id
394 optpair (GASY_X GASX_uncancell) (GASY_X GASX_cancelr) = Just $ GASL_id
395 optpair (GASY_X GASX_assoc) (GASY_X GASX_cancell) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_cancell
396 optpair (GASY_X GASX_unassoc) (GASY_X GASX_cancelr) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_cancelr
397 optpair (GASY_second (GASY_X GASX_uncancelr)) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_X GASX_uncancelr
398 optpair (GASY_first (GASY_X GASX_uncancell)) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_X GASX_uncancell
399 optpair (GASY_X GASX_uncancell) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_uncancell
400 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancelr
401 optpair (GASY_first (GASY_X GASX_uncancelr)) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancell
402 optpair (GASY_second (GASY_X GASX_uncancell)) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_uncancelr
403 optpair (GASY_X GASX_assoc) (GASY_second (GASY_X GASX_cancelr)) = Just $ GASL_Y $ GASY_X $ GASX_cancelr
404 optpair (GASY_X GASX_unassoc) (GASY_first (GASY_X GASX_cancell)) = Just $ GASL_Y $ GASY_X $ GASX_cancell
405 optpair (GASY_first g) (GASY_X GASX_cancelr) = Just $ GASL_comp (GASY_X GASX_cancelr) $ GASL_Y $ g
406 optpair (GASY_second g) (GASY_X GASX_cancell) = Just $ GASL_comp (GASY_X GASX_cancell) $ GASL_Y $ g
407 optpair (GASY_X GASX_uncancelr) (GASY_first g) = Just $ GASL_comp g $ GASL_Y (GASY_X GASX_uncancelr)
408 optpair (GASY_X GASX_uncancell) (GASY_second g) = Just $ GASL_comp g $ GASL_Y (GASY_X GASX_uncancell)
410 -- swap with an {un}cancel{l,r} before/after it
411 optpair (GASY_X GASX_uncancell) (GASY_X GASX_swap ) = Just $ GASL_Y $ GASY_X $ GASX_uncancelr
412 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_swap ) = Just $ GASL_Y $ GASY_X $ GASX_uncancell
413 optpair (GASY_X GASX_swap) (GASY_X GASX_cancell) = Just $ GASL_Y $ GASY_X $ GASX_cancelr
414 optpair (GASY_X GASX_swap) (GASY_X GASX_cancelr) = Just $ GASL_Y $ GASY_X $ GASX_cancell
417 optpair (GASY_X GASX_uncancelr) (GASY_X (GASX_loopl gl)) =
418 Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ GASY_X GASX_uncancelr) gl)
419 optpair (GASY_X GASX_uncancell) (GASY_X (GASX_loopl gl)) =
420 Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ GASY_X GASX_uncancell) gl)
421 optpair (GASY_X GASX_uncancelr) (GASY_X (GASX_loopr gl)) =
422 Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ GASY_X GASX_uncancelr) gl)
423 optpair (GASY_X GASX_uncancell) (GASY_X (GASX_loopr gl)) =
424 Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ GASY_X GASX_uncancell) gl)
426 optpair q (GASY_X (GASX_loopl gl)) | pushin q = Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ q) gl)
427 optpair q (GASY_X (GASX_loopr gl)) | pushin q = Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ q) gl)
429 optpair a@(GASY_X GASX_uncancell) (GASY_first b@(GASY_X (GASX_const c))) = Just $ GASL_Y $ GASY_atomicl b
430 optpair a@(GASY_X GASX_uncancelr) (GASY_second b@(GASY_X (GASX_const c))) = Just $ GASL_Y $ GASY_atomicr b
432 optpair (GASY_first gy1) (GASY_second gy2) | pushleft gy2, not (pushleft gy1)
433 = Just $ GASL_comp (GASY_second gy2) $ GASL_Y $ GASY_first gy1
434 optpair (GASY_second gy1) (GASY_first gy2) | pushleft gy2, not (pushleft gy1)
435 = Just $ GASL_comp (GASY_first gy2) $ GASL_Y $ GASY_second gy1
437 optpair (GASY_first gy1) (GASY_first gy2) = liftM gasl_firstify $ optpair gy1 gy2
438 optpair (GASY_second gy1) (GASY_second gy2) = liftM gasl_secondify $ optpair gy1 gy2
439 optpair _ _ = Nothing
441 swappair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z)
443 swappair q (GASY_atomicl g) = Just $ GASL_comp (GASY_atomicl g) $ GASL_Y $ GASY_second q
444 swappair q (GASY_atomicr g) = Just $ GASL_comp (GASY_atomicr g) $ GASL_Y $ GASY_first q
446 swappair (GASY_first gy1) (GASY_second gy2) = Just $ GASL_comp (GASY_second gy2) (GASL_Y $ GASY_first gy1)
447 swappair (GASY_second gy1) (GASY_first gy2) = Just $ GASL_comp (GASY_first gy2) (GASL_Y $ GASY_second gy1)
448 swappair (GASY_first gy1) (GASY_X GASX_unassoc) = Just $ GASL_comp(GASY_X GASX_unassoc) (GASL_Y $ GASY_first (GASY_first gy1))
449 swappair (GASY_second gy1) (GASY_X GASX_assoc ) = Just $ GASL_comp(GASY_X GASX_assoc ) (GASL_Y $ GASY_second (GASY_second gy1))
450 swappair (GASY_X GASX_uncancelr) (GASY_first gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancelr)
451 swappair (GASY_X GASX_uncancell) (GASY_second gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancell)
452 swappair (GASY_first (GASY_second gy)) (GASY_X GASX_assoc ) = Just $ GASL_comp (GASY_X GASX_assoc ) $ GASL_Y (GASY_second (GASY_first gy))
453 swappair (GASY_second (GASY_first gy)) (GASY_X GASX_unassoc ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_first (GASY_second gy))
454 swappair (GASY_second (GASY_second gy)) (GASY_X GASX_unassoc ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_second gy)
455 swappair (GASY_first (GASY_first gy)) (GASY_X GASX_assoc ) = Just $ GASL_comp (GASY_X GASX_assoc) $ GASL_Y (GASY_first gy)
456 swappair (GASY_first gy) (GASY_X GASX_swap ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_second gy)
457 swappair (GASY_second gy) (GASY_X GASX_swap ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_first gy)
458 swappair gy (GASY_X (GASX_loopl gl)) = Just $ GASL_Y $ GASY_X $ GASX_loopl $ GASL_comp (GASY_second gy) gl
459 swappair gy (GASY_X (GASX_loopr gl)) = Just $ GASL_Y $ GASY_X $ GASX_loopr $ GASL_comp (GASY_first gy) gl
461 swappair (GASY_first gy1) (GASY_first gy2) = liftM gasl_firstify $ swappair gy1 gy2
462 swappair (GASY_second gy1) (GASY_second gy2) = liftM gasl_secondify $ swappair gy1 gy2
463 swappair _ _ = Nothing
465 -- pushright can only return True for central morphisms
466 pushright :: GArrowSkeletonY m x y -> Bool
467 pushright (GASY_first gy) = pushright gy
468 pushright (GASY_second gy) = pushright gy
469 pushright (GASY_atomicl _) = False
470 pushright (GASY_atomicr _) = False
471 pushright (GASY_X GASX_uncancell) = True
472 pushright (GASY_X GASX_uncancelr) = True
473 pushright (GASY_X _ ) = False
475 -- says if we should push it into a loopl/r
476 pushin :: GArrowSkeletonY m x y -> Bool
477 pushin gy = pushright gy || pushin' gy
479 pushin' :: GArrowSkeletonY m a b -> Bool
480 pushin' (GASY_first gy) = pushin' gy
481 pushin' (GASY_second gy) = pushin' gy
482 pushin' (GASY_atomicl _) = False
483 pushin' (GASY_atomicr _) = False
485 -- not sure if these are a good idea
486 pushin' (GASY_X GASX_copy) = True
487 pushin' (GASY_X GASX_swap) = True
489 pushin' (GASY_X _ ) = False
491 optimizey :: GArrowSkeletonY m x y -> GArrowSkeletonY m x y
492 optimizey (GASY_X gx) = GASY_X $ optimizex gx
493 optimizey (GASY_first gy) = GASY_first (optimizey gy)
494 optimizey (GASY_second gy) = GASY_second (optimizey gy)
495 optimizey (GASY_atomicl gy) = GASY_atomicl $ optimizey gy
496 optimizey (GASY_atomicr gy) = GASY_atomicr $ optimizey gy
498 optimizex :: GArrowSkeletonX m x y -> GArrowSkeletonX m x y
499 optimizex (GASX_const k) = GASX_const k
500 optimizex (GASX_cancell) = GASX_cancell
501 optimizex (GASX_cancelr) = GASX_cancelr
502 optimizex (GASX_uncancell) = GASX_uncancell
503 optimizex (GASX_uncancelr) = GASX_uncancelr
504 optimizex (GASX_assoc) = GASX_assoc
505 optimizex (GASX_unassoc) = GASX_unassoc
506 optimizex (GASX_drop) = GASX_drop
507 optimizex (GASX_copy) = GASX_copy
508 optimizex (GASX_swap) = GASX_swap
509 optimizex (GASX_merge) = GASX_merge
510 optimizex (GASX_misc m) = GASX_misc m
511 optimizex (GASX_loopl (GASL_comp (GASY_first gy) gl))| pushleft gy = GASX_loopl $ gaslcat gl (GASL_Y $ GASY_first gy)
512 optimizex (GASX_loopr (GASL_comp (GASY_second gy) gl))| pushleft gy = GASX_loopr $ gaslcat gl (GASL_Y $ GASY_second gy)
513 optimizex (GASX_loopl gl) = GASX_loopl $ optimizel gl
514 optimizex (GASX_loopr gl) = GASX_loopr $ optimizel gl
516 pushleft :: GArrowSkeletonY m x y -> Bool
517 pushleft (GASY_first gy) = pushleft gy
518 pushleft (GASY_second gy) = pushleft gy
519 pushleft (GASY_atomicl _) = False
520 pushleft (GASY_atomicr _) = False
521 pushleft (GASY_X GASX_cancell) = True
522 pushleft (GASY_X GASX_cancelr) = True
523 pushleft (GASY_X _ ) = False