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 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(..), optimize, beautify)
28 import Prelude hiding ( id, (.), lookup, repeat )
29 import Control.Category
30 import GHC.HetMet.GArrow
32 import Control.Monad.State
34 data GArrowSkeleton m :: * -> * -> *
36 GAS_const :: Int -> GArrowSkeleton m () Int
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_merge :: GArrowSkeleton m (x,y) z
51 GAS_loopl :: GArrowSkeleton m (z,x) (z,y) -> GArrowSkeleton m x y
52 GAS_loopr :: GArrowSkeleton m (x,z) (y,z) -> GArrowSkeleton m x y
53 GAS_misc :: m x y -> GArrowSkeleton m x y
55 instance Category (GArrowSkeleton m) where
59 instance GArrow (GArrowSkeleton m) (,) () where
61 ga_second = GAS_second
62 ga_cancell = GAS_cancell
63 ga_cancelr = GAS_cancelr
64 ga_uncancell = GAS_uncancell
65 ga_uncancelr = GAS_uncancelr
67 ga_unassoc = GAS_unassoc
69 instance GArrowDrop (GArrowSkeleton m) (,) () where
72 instance GArrowCopy (GArrowSkeleton m) (,) () where
75 instance GArrowSwap (GArrowSkeleton m) (,) () where
78 instance GArrowLoop (GArrowSkeleton m) (,) () where
82 type instance GArrowTensor (GArrowSkeleton m) = (,)
83 type instance GArrowUnit (GArrowSkeleton m) = ()
84 type instance GArrowExponent (GArrowSkeleton m) = (->)
86 instance GArrowSTKCL (GArrowSkeleton m)
89 -- | Simple structural equality on skeletons. NOTE: two skeletons
90 -- with the same shape but different types will nonetheless be "equal";
91 -- there's no way around this since types are gone at runtime.
93 instance Eq ((GArrowSkeleton m) a b)
97 (===) :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) c d -> Bool
98 (GAS_id ) === (GAS_id ) = True
99 (GAS_comp g f) === (GAS_comp g' f') = f===f' && g===g'
100 (GAS_first f) === (GAS_first f') = f===f'
101 (GAS_second f) === (GAS_second f') = f===f'
102 GAS_cancell === GAS_cancell = True
103 GAS_cancelr === GAS_cancelr = True
104 GAS_uncancell === GAS_uncancell = True
105 GAS_uncancelr === GAS_uncancelr = True
106 GAS_drop === GAS_drop = True
107 (GAS_const i) === (GAS_const i') = i==i'
108 GAS_copy === GAS_copy = True
109 GAS_merge === GAS_merge = True
110 GAS_swap === GAS_swap = True
111 GAS_assoc === GAS_assoc = True
112 GAS_unassoc === GAS_unassoc = True
113 (GAS_loopl f) === (GAS_loopl f') = f === f'
114 (GAS_loopr f) === (GAS_loopr f') = f === f'
116 -- FIXME: GAS_misc's are never equal!!!
119 -- | Performs some very simple-minded optimizations on a
120 -- boxes-and-wires diagram. Preserves equivalence up to the GArrow
121 -- laws, but no guarantees about which optimizations actually happen.
123 optimize :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
124 optimize = repeat (gasl2gas . optimizel . {- FIXME -} optimizel . gas2gasl)
127 optimize x = let x' = optimize' x in if x == x' then x' else optimize x'
129 optimize' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
131 -- Some optimizations fail due to misparenthesization; we default to
132 -- left-associativity and hope for the best
133 optimize' (GAS_comp f (GAS_comp g h) ) = GAS_comp (GAS_comp f g) h
134 optimize' (GAS_comp (GAS_comp f (GAS_comp g h)) k) = GAS_comp (GAS_comp (GAS_comp f g) h) k
135 optimize' (GAS_comp (GAS_comp GAS_unassoc (GAS_second g)) GAS_assoc) = GAS_second (GAS_second g)
136 optimize' (GAS_comp (GAS_comp (GAS_comp f GAS_unassoc) (GAS_second g)) GAS_assoc) = GAS_comp f (GAS_second (GAS_second g))
138 optimize' (GAS_comp (GAS_comp f g) h) = case optimize_pair g h of
139 Nothing -> GAS_comp (optimize' (GAS_comp f g)) h'
140 Just ret' -> GAS_comp f' ret'
145 optimize' (GAS_comp f g ) = case optimize_pair f g of
146 Nothing -> GAS_comp f' g'
151 optimize' (GAS_first GAS_id ) = GAS_id
152 optimize' (GAS_second GAS_id ) = GAS_id
153 -- optimize' (GAS_first (GAS_comp f g)) = GAS_comp (GAS_first f) (GAS_first g)
154 -- optimize' (GAS_second (GAS_comp f g)) = GAS_comp (GAS_second f) (GAS_second g)
155 optimize' (GAS_first f ) = GAS_first $ optimize' f
156 optimize' (GAS_second f ) = GAS_second $ optimize' f
157 optimize' (GAS_loopl GAS_id ) = GAS_id
158 optimize' (GAS_loopr GAS_id ) = GAS_id
159 optimize' (GAS_loopl f ) = GAS_loopl $ optimize' f
160 optimize' (GAS_loopr f ) = GAS_loopr $ optimize' f
163 optimize_pair :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) b c -> Maybe ((GArrowSkeleton m) a c)
165 optimize_pair f GAS_drop = Just $ GAS_drop
166 optimize_pair GAS_id f = Just $ f
167 optimize_pair f GAS_id = Just $ f
168 optimize_pair GAS_uncancell GAS_cancell = Just $ GAS_id
169 optimize_pair GAS_uncancelr GAS_cancelr = Just $ GAS_id
170 optimize_pair GAS_cancell GAS_uncancell = Just $ GAS_id
171 optimize_pair GAS_cancelr GAS_uncancelr = Just $ GAS_id
172 optimize_pair GAS_uncancelr GAS_cancell = Just $ GAS_id
173 optimize_pair GAS_uncancell GAS_cancelr = Just $ GAS_id
175 -- first priority: eliminate GAS_first
176 optimize_pair (GAS_first f) GAS_cancelr = Just $ GAS_comp GAS_cancelr f
177 optimize_pair (GAS_second f) GAS_cancell = Just $ GAS_comp GAS_cancell f
178 optimize_pair GAS_uncancelr (GAS_first f) = Just $ GAS_comp f GAS_uncancelr
179 optimize_pair GAS_uncancell (GAS_second f) = Just $ GAS_comp f GAS_uncancell
181 -- second priority: push GAS_swap leftward
182 optimize_pair (GAS_second f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_first f)
183 optimize_pair (GAS_first f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_second f)
184 optimize_pair GAS_swap GAS_swap = Just $ GAS_id
185 optimize_pair GAS_swap GAS_cancell = Just $ GAS_cancelr
186 optimize_pair GAS_swap GAS_cancelr = Just $ GAS_cancell
188 optimize_pair GAS_assoc GAS_cancell = Just $ GAS_first GAS_cancell
189 optimize_pair GAS_unassoc GAS_cancelr = Just $ GAS_second GAS_cancelr
190 optimize_pair GAS_assoc (GAS_second GAS_cancell) = Just $ GAS_first GAS_cancelr
191 optimize_pair GAS_unassoc (GAS_first GAS_cancell) = Just $ GAS_cancell
194 -- FIXME: valid only for central morphisms
195 --optimize_pair (GAS_second f) (GAS_first g) = Just $ GAS_comp (GAS_first g) (GAS_second f)
196 optimize_pair (GAS_first g) (GAS_second f) = Just $ GAS_comp (GAS_second f) (GAS_first g)
198 optimize_pair _ _ = Nothing
201 repeat :: Eq a => (a -> a) -> a -> a
202 repeat f x = let x' = f x in
208 -- | Recursively turns @(ga_first x >>> first y)@ into @(ga_first (x >>> y))@, likewise for ga_second.
210 beautify :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
211 beautify = repeat beautify'
213 beautify' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
214 beautify' (GAS_comp (GAS_comp f g) h) = beautify' $ GAS_comp f $ GAS_comp g h
215 beautify' (GAS_comp f (GAS_comp (GAS_comp g h) k)) = beautify' $ GAS_comp f $ GAS_comp g $ GAS_comp h k
216 beautify' (GAS_comp f (GAS_comp g h)) = case (beautify' f, beautify' g) of
217 (GAS_first f' , GAS_first g') -> beautify' $ GAS_comp (GAS_first (GAS_comp f' g')) h
218 (GAS_second f', GAS_second g') -> beautify' $ GAS_comp (GAS_second (GAS_comp f' g')) h
219 (f' , g' ) -> GAS_comp f' (beautify' (GAS_comp g h))
220 beautify' (GAS_comp f GAS_id) = f
221 beautify' (GAS_comp GAS_id f) = f
222 beautify' (GAS_comp f g) = case (beautify' f, beautify' g) of
223 (GAS_first f' , GAS_first g') -> GAS_first (GAS_comp f' g')
224 (GAS_second f', GAS_second g') -> GAS_second (GAS_comp f' g')
225 (f' , g' ) -> GAS_comp f' g'
226 beautify' (GAS_first f) = GAS_first $ beautify' f
227 beautify' (GAS_second f) = GAS_second $ beautify' f
228 beautify' (GAS_loopl f) = GAS_loopl $ beautify' f
229 beautify' (GAS_loopr f) = GAS_loopr $ beautify' f
235 gas2gasl :: GArrowSkeleton m x y -> GArrowSkeletonL m x y
236 gas2gasl (GAS_const k ) = GASL_Y $ GASY_X $ GASX_const k
237 gas2gasl (GAS_id ) = GASL_id
238 gas2gasl (GAS_comp f g) = gaslcat (gas2gasl f) (gas2gasl g)
239 gas2gasl (GAS_first f) = gasl_firstify $ gas2gasl f
240 gas2gasl (GAS_second f) = gasl_secondify $ gas2gasl f
241 gas2gasl (GAS_cancell ) = GASL_Y $ GASY_X $ GASX_cancell
242 gas2gasl (GAS_cancelr ) = GASL_Y $ GASY_X $ GASX_cancelr
243 gas2gasl (GAS_uncancell ) = GASL_Y $ GASY_X $ GASX_uncancell
244 gas2gasl (GAS_uncancelr ) = GASL_Y $ GASY_X $ GASX_uncancelr
245 gas2gasl (GAS_assoc ) = GASL_Y $ GASY_X $ GASX_assoc
246 gas2gasl (GAS_unassoc ) = GASL_Y $ GASY_X $ GASX_unassoc
247 gas2gasl (GAS_drop ) = GASL_Y $ GASY_X $ GASX_drop
248 gas2gasl (GAS_copy ) = GASL_Y $ GASY_X $ GASX_copy
249 gas2gasl (GAS_swap ) = GASL_Y $ GASY_X $ GASX_swap
250 gas2gasl (GAS_merge ) = GASL_Y $ GASY_X $ GASX_merge
251 gas2gasl (GAS_loopl f) = GASL_Y $ GASY_X $ GASX_loopl $ gas2gasl f
252 gas2gasl (GAS_loopr f) = GASL_Y $ GASY_X $ GASX_loopr $ gas2gasl f
253 gas2gasl (GAS_misc m) = GASL_Y $ GASY_X $ GASX_misc m
255 -- apply "first" to a GASL
256 gasl_firstify :: GArrowSkeletonL m x y -> GArrowSkeletonL m (x,z) (y,z)
257 gasl_firstify (GASL_id ) = GASL_id
258 gasl_firstify (GASL_Y gy ) = GASL_Y $ GASY_first $ gy
259 gasl_firstify (GASL_comp gxq gqy) = GASL_comp (GASY_first gxq) $ gasl_firstify gqy
261 -- apply "second" to a GASL
262 gasl_secondify :: GArrowSkeletonL m x y -> GArrowSkeletonL m (z,x) (z,y)
263 gasl_secondify (GASL_id ) = GASL_id
264 gasl_secondify (GASL_Y gy ) = GASL_Y $ GASY_second $ gy
265 gasl_secondify (GASL_comp gxq gqy) = GASL_comp (GASY_second gxq) $ gasl_secondify gqy
267 -- concatenates two GASL's
268 gaslcat :: GArrowSkeletonL m x y -> GArrowSkeletonL m y z -> GArrowSkeletonL m x z
269 gaslcat (GASL_id ) g' = g'
270 gaslcat (GASL_Y gy ) g' = GASL_comp gy g'
271 gaslcat (GASL_comp gxq gqy) g' = GASL_comp gxq (gaslcat gqy g')
273 data GArrowSkeletonL m :: * -> * -> *
275 GASL_id :: GArrowSkeletonL m x x
276 GASL_Y :: GArrowSkeletonY m x y -> GArrowSkeletonL m x y
277 GASL_comp :: GArrowSkeletonY m x y -> GArrowSkeletonL m y z -> GArrowSkeletonL m x z
279 data GArrowSkeletonY m :: * -> * -> *
281 GASY_X :: GArrowSkeletonX m x y -> GArrowSkeletonY m x y
282 GASY_first :: GArrowSkeletonY m x y -> GArrowSkeletonY m (x,z) (y,z)
283 GASY_second :: GArrowSkeletonY m x y -> GArrowSkeletonY m (z,x) (z,y)
284 GASY_atomicl :: GArrowSkeletonY m () x -> GArrowSkeletonY m y (x,y)
285 GASY_atomicr :: GArrowSkeletonY m () x -> GArrowSkeletonY m y (y,x)
287 data GArrowSkeletonX m :: * -> * -> *
289 GASX_const :: Int -> GArrowSkeletonX m () Int
290 GASX_cancell :: GArrowSkeletonX m ((),x) x
291 GASX_cancelr :: GArrowSkeletonX m (x,()) x
292 GASX_uncancell :: GArrowSkeletonX m x ((),x)
293 GASX_uncancelr :: GArrowSkeletonX m x (x,())
294 GASX_assoc :: GArrowSkeletonX m ((x,y),z) (x,(y,z))
295 GASX_unassoc :: GArrowSkeletonX m (x,(y,z)) ((x,y),z)
296 GASX_drop :: GArrowSkeletonX m x ()
297 GASX_copy :: GArrowSkeletonX m x (x,x)
298 GASX_swap :: GArrowSkeletonX m (x,y) (y,x)
299 GASX_merge :: GArrowSkeletonX m (x,y) z
300 GASX_misc :: m x y -> GArrowSkeletonX m x y
301 GASX_loopl :: GArrowSkeletonL m (z,x) (z,y) -> GArrowSkeletonX m x y
302 GASX_loopr :: GArrowSkeletonL m (x,z) (y,z) -> GArrowSkeletonX m x y
304 -- TO DO: gather "maximal chunks" of ga_first/ga_second
305 gasl2gas :: GArrowSkeletonL m x y -> GArrowSkeleton m x y
306 gasl2gas GASL_id = GAS_id
307 gasl2gas (GASL_Y gy ) = gasy2gas gy
308 gasl2gas (GASL_comp gy gl) = GAS_comp (gasy2gas gy) (gasl2gas gl)
310 gasy2gas :: GArrowSkeletonY m x y -> GArrowSkeleton m x y
311 gasy2gas (GASY_X gx) = gasx2gas gx
312 gasy2gas (GASY_first gy) = GAS_first (gasy2gas gy)
313 gasy2gas (GASY_second gy) = GAS_second (gasy2gas gy)
314 gasy2gas (GASY_atomicl gy) = GAS_comp GAS_uncancell (GAS_first $ gasy2gas gy)
315 gasy2gas (GASY_atomicr gy) = GAS_comp GAS_uncancelr (GAS_second $ gasy2gas gy)
317 gasx2gas :: GArrowSkeletonX m x y -> GArrowSkeleton m x y
318 gasx2gas (GASX_const k) = GAS_const k
319 gasx2gas (GASX_cancell) = GAS_cancell
320 gasx2gas (GASX_cancelr) = GAS_cancelr
321 gasx2gas (GASX_uncancell) = GAS_uncancell
322 gasx2gas (GASX_uncancelr) = GAS_uncancelr
323 gasx2gas (GASX_assoc) = GAS_assoc
324 gasx2gas (GASX_unassoc) = GAS_unassoc
325 gasx2gas (GASX_drop) = GAS_drop
326 gasx2gas (GASX_copy) = GAS_copy
327 gasx2gas (GASX_swap) = GAS_swap
328 gasx2gas (GASX_merge) = GAS_merge
329 gasx2gas (GASX_misc m) = GAS_misc m
330 gasx2gas (GASX_loopl gl) = GAS_loopl $ gasl2gas gl
331 gasx2gas (GASX_loopr gl) = GAS_loopr $ gasl2gas gl
335 optimizel :: GArrowSkeletonL m x y -> GArrowSkeletonL m x y
336 optimizel (GASL_id ) = GASL_id
337 optimizel (GASL_Y gy ) = GASL_Y $ optimizey gy
338 optimizel (GASL_comp gy (GASL_comp gy' gl)) | Just x <- optpair gy gy' = optimizel $ gaslcat x gl
339 optimizel (GASL_comp gy (GASL_Y gy')) | Just x <- optpair gy gy' = x
340 optimizel (GASL_comp gy (GASL_comp gy' gl)) | pushright gy, not (pushright gy'), Just x <- swappair gy gy' = optimizel $ gaslcat x gl
341 optimizel (GASL_comp gy (GASL_Y gy')) | pushright gy, not (pushright gy'), Just x <- swappair gy gy' = GASL_comp (optimizey gy) (GASL_Y gy')
342 optimizel (GASL_comp gy gl) = GASL_comp (optimizey gy) (optimizel gl)
344 --optimize' (GAS_loopl GAS_id ) = GAS_id
345 --optimize' (GAS_loopr GAS_id ) = GAS_id
346 --optimize_pair f GAS_drop = Just $ GAS_drop
348 optimize_pair (GAS_first f) GAS_cancelr = Just $ GAS_comp GAS_cancelr f
349 optimize_pair (GAS_second f) GAS_cancell = Just $ GAS_comp GAS_cancell f
350 optimize_pair GAS_uncancelr (GAS_first f) = Just $ GAS_comp f GAS_uncancelr
351 optimize_pair GAS_uncancell (GAS_second f) = Just $ GAS_comp f GAS_uncancell
352 optimize_pair (GAS_second f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_first f)
353 optimize_pair (GAS_first f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_second f)
354 optimize_pair GAS_swap GAS_swap = Just $ GAS_id
355 optimize_pair GAS_swap GAS_cancell = Just $ GAS_cancelr
356 optimize_pair GAS_swap GAS_cancelr = Just $ GAS_cancell
357 optimize_pair GAS_assoc GAS_cancell = Just $ GAS_first GAS_cancell
358 optimize_pair GAS_unassoc GAS_cancelr = Just $ GAS_second GAS_cancelr
359 optimize_pair GAS_assoc (GAS_second GAS_cancell) = Just $ GAS_first GAS_cancelr
360 optimize_pair GAS_unassoc (GAS_first GAS_cancell) = Just $ GAS_cancell
363 optpair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z)
365 optpair (GASY_atomicl g) (GASY_X GASX_cancelr) = Just $ GASL_Y g
366 optpair (GASY_atomicr g) (GASY_X GASX_cancell) = Just $ GASL_Y g
368 optpair (GASY_X GASX_uncancell) (GASY_X GASX_cancell) = Just $ GASL_id
369 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_cancelr) = Just $ GASL_id
370 optpair (GASY_X GASX_cancell) (GASY_X GASX_uncancell) = Just $ GASL_id
371 optpair (GASY_X GASX_cancelr) (GASY_X GASX_uncancelr) = Just $ GASL_id
372 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_cancell) = Just $ GASL_id
373 optpair (GASY_X GASX_uncancell) (GASY_X GASX_cancelr) = Just $ GASL_id
374 optpair (GASY_X GASX_assoc) (GASY_X GASX_cancell) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_cancell
375 optpair (GASY_X GASX_unassoc) (GASY_X GASX_cancelr) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_cancelr
376 optpair (GASY_second (GASY_X GASX_uncancelr)) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_X GASX_uncancelr
377 optpair (GASY_first (GASY_X GASX_uncancell)) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_X GASX_uncancell
378 optpair (GASY_X GASX_uncancell) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_uncancell
379 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancelr
380 optpair (GASY_first (GASY_X GASX_uncancelr)) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancell
381 optpair (GASY_second (GASY_X GASX_uncancell)) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_uncancelr
382 optpair (GASY_X GASX_assoc) (GASY_second (GASY_X GASX_cancelr)) = Just $ GASL_Y $ GASY_X $ GASX_cancelr
383 optpair (GASY_X GASX_unassoc) (GASY_first (GASY_X GASX_cancell)) = Just $ GASL_Y $ GASY_X $ GASX_cancell
384 optpair (GASY_first g) (GASY_X GASX_cancelr) = Just $ GASL_comp (GASY_X GASX_cancelr) $ GASL_Y $ g
385 optpair (GASY_second g) (GASY_X GASX_cancell) = Just $ GASL_comp (GASY_X GASX_cancell) $ GASL_Y $ g
386 optpair (GASY_X GASX_uncancelr) (GASY_first g) = Just $ GASL_comp g $ GASL_Y (GASY_X GASX_uncancelr)
387 optpair (GASY_X GASX_uncancell) (GASY_second g) = Just $ GASL_comp g $ GASL_Y (GASY_X GASX_uncancell)
389 -- swap with an {un}cancel{l,r} before/after it
390 optpair (GASY_X GASX_uncancell) (GASY_X GASX_swap ) = Just $ GASL_Y $ GASY_X $ GASX_uncancelr
391 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_swap ) = Just $ GASL_Y $ GASY_X $ GASX_uncancell
392 optpair (GASY_X GASX_swap) (GASY_X GASX_cancell) = Just $ GASL_Y $ GASY_X $ GASX_cancelr
393 optpair (GASY_X GASX_swap) (GASY_X GASX_cancelr) = Just $ GASL_Y $ GASY_X $ GASX_cancell
396 optpair (GASY_X GASX_uncancelr) (GASY_X (GASX_loopl gl)) =
397 Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ GASY_X GASX_uncancelr) gl)
398 optpair (GASY_X GASX_uncancell) (GASY_X (GASX_loopl gl)) =
399 Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ GASY_X GASX_uncancell) gl)
400 optpair (GASY_X GASX_uncancelr) (GASY_X (GASX_loopr gl)) =
401 Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ GASY_X GASX_uncancelr) gl)
402 optpair (GASY_X GASX_uncancell) (GASY_X (GASX_loopr gl)) =
403 Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ GASY_X GASX_uncancell) gl)
405 optpair q (GASY_X (GASX_loopl gl)) | pushin q = Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ q) gl)
406 optpair q (GASY_X (GASX_loopr gl)) | pushin q = Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ q) gl)
408 optpair a@(GASY_X GASX_uncancell) (GASY_first b@(GASY_X (GASX_const c))) = Just $ GASL_Y $ GASY_atomicl b
409 optpair a@(GASY_X GASX_uncancelr) (GASY_second b@(GASY_X (GASX_const c))) = Just $ GASL_Y $ GASY_atomicr b
411 optpair (GASY_first gy1) (GASY_second gy2) | pushleft gy2, not (pushleft gy1)
412 = Just $ GASL_comp (GASY_second gy2) $ GASL_Y $ GASY_first gy1
413 optpair (GASY_second gy1) (GASY_first gy2) | pushleft gy2, not (pushleft gy1)
414 = Just $ GASL_comp (GASY_first gy2) $ GASL_Y $ GASY_second gy1
416 optpair (GASY_first gy1) (GASY_first gy2) = liftM gasl_firstify $ optpair gy1 gy2
417 optpair (GASY_second gy1) (GASY_second gy2) = liftM gasl_secondify $ optpair gy1 gy2
418 optpair _ _ = Nothing
420 swappair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z)
422 swappair q (GASY_atomicl g) = Just $ GASL_comp (GASY_atomicl g) $ GASL_Y $ GASY_second q
423 swappair q (GASY_atomicr g) = Just $ GASL_comp (GASY_atomicr g) $ GASL_Y $ GASY_first q
425 swappair (GASY_first gy1) (GASY_second gy2) = Just $ GASL_comp (GASY_second gy2) (GASL_Y $ GASY_first gy1)
426 swappair (GASY_second gy1) (GASY_first gy2) = Just $ GASL_comp (GASY_first gy2) (GASL_Y $ GASY_second gy1)
427 swappair (GASY_first gy1) (GASY_X GASX_unassoc) = Just $ GASL_comp(GASY_X GASX_unassoc) (GASL_Y $ GASY_first (GASY_first gy1))
428 swappair (GASY_second gy1) (GASY_X GASX_assoc ) = Just $ GASL_comp(GASY_X GASX_assoc ) (GASL_Y $ GASY_second (GASY_second gy1))
429 swappair (GASY_X GASX_uncancelr) (GASY_first gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancelr)
430 swappair (GASY_X GASX_uncancell) (GASY_second gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancell)
431 swappair (GASY_first (GASY_second gy)) (GASY_X GASX_assoc ) = Just $ GASL_comp (GASY_X GASX_assoc ) $ GASL_Y (GASY_second (GASY_first gy))
432 swappair (GASY_second (GASY_first gy)) (GASY_X GASX_unassoc ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_first (GASY_second gy))
433 swappair (GASY_second (GASY_second gy)) (GASY_X GASX_unassoc ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_second gy)
434 swappair (GASY_first (GASY_first gy)) (GASY_X GASX_assoc ) = Just $ GASL_comp (GASY_X GASX_assoc) $ GASL_Y (GASY_first gy)
435 swappair (GASY_first gy) (GASY_X GASX_swap ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_second gy)
436 swappair (GASY_second gy) (GASY_X GASX_swap ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_first gy)
437 swappair gy (GASY_X (GASX_loopl gl)) = Just $ GASL_Y $ GASY_X $ GASX_loopl $ GASL_comp (GASY_second gy) gl
438 swappair gy (GASY_X (GASX_loopr gl)) = Just $ GASL_Y $ GASY_X $ GASX_loopr $ GASL_comp (GASY_first gy) gl
440 swappair (GASY_first gy1) (GASY_first gy2) = liftM gasl_firstify $ swappair gy1 gy2
441 swappair (GASY_second gy1) (GASY_second gy2) = liftM gasl_secondify $ swappair gy1 gy2
442 swappair _ _ = Nothing
444 -- pushright can only return True for central morphisms
445 pushright :: GArrowSkeletonY m x y -> Bool
446 pushright (GASY_first gy) = pushright gy
447 pushright (GASY_second gy) = pushright gy
448 pushright (GASY_atomicl _) = False
449 pushright (GASY_atomicr _) = False
450 pushright (GASY_X GASX_uncancell) = True
451 pushright (GASY_X GASX_uncancelr) = True
452 pushright (GASY_X _ ) = False
454 -- says if we should push it into a loopl/r
455 pushin :: GArrowSkeletonY m x y -> Bool
456 pushin gy = pushright gy || pushin' gy
458 pushin' :: GArrowSkeletonY m a b -> Bool
459 pushin' (GASY_first gy) = pushin' gy
460 pushin' (GASY_second gy) = pushin' gy
461 pushin' (GASY_atomicl _) = False
462 pushin' (GASY_atomicr _) = False
464 -- not sure if these are a good idea
465 pushin' (GASY_X GASX_copy) = True
466 pushin' (GASY_X GASX_swap) = True
468 pushin' (GASY_X _ ) = False
470 optimizey :: GArrowSkeletonY m x y -> GArrowSkeletonY m x y
471 optimizey (GASY_X gx) = GASY_X $ optimizex gx
472 optimizey (GASY_first gy) = GASY_first (optimizey gy)
473 optimizey (GASY_second gy) = GASY_second (optimizey gy)
474 optimizey (GASY_atomicl gy) = GASY_atomicl $ optimizey gy
475 optimizey (GASY_atomicr gy) = GASY_atomicr $ optimizey gy
477 optimizex :: GArrowSkeletonX m x y -> GArrowSkeletonX m x y
478 optimizex (GASX_const k) = GASX_const k
479 optimizex (GASX_cancell) = GASX_cancell
480 optimizex (GASX_cancelr) = GASX_cancelr
481 optimizex (GASX_uncancell) = GASX_uncancell
482 optimizex (GASX_uncancelr) = GASX_uncancelr
483 optimizex (GASX_assoc) = GASX_assoc
484 optimizex (GASX_unassoc) = GASX_unassoc
485 optimizex (GASX_drop) = GASX_drop
486 optimizex (GASX_copy) = GASX_copy
487 optimizex (GASX_swap) = GASX_swap
488 optimizex (GASX_merge) = GASX_merge
489 optimizex (GASX_misc m) = GASX_misc m
490 optimizex (GASX_loopl (GASL_comp (GASY_first gy) gl))| pushleft gy = GASX_loopl $ gaslcat gl (GASL_Y $ GASY_first gy)
491 optimizex (GASX_loopr (GASL_comp (GASY_second gy) gl))| pushleft gy = GASX_loopr $ gaslcat gl (GASL_Y $ GASY_second gy)
492 optimizex (GASX_loopl gl) = GASX_loopl $ optimizel gl
493 optimizex (GASX_loopr gl) = GASX_loopr $ optimizel gl
495 pushleft :: GArrowSkeletonY m x y -> Bool
496 pushleft (GASY_first gy) = pushleft gy
497 pushleft (GASY_second gy) = pushleft gy
498 pushleft (GASY_atomicl _) = False
499 pushleft (GASY_atomicr _) = False
500 pushleft (GASY_X GASX_cancell) = True
501 pushleft (GASY_X GASX_cancelr) = True
502 pushleft (GASY_X _ ) = False