examples/GArrowSkeleton.hs

   1 {-# LANGUAGE MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, TypeFamilies #-}
   2 -----------------------------------------------------------------------------
   3 -- |
   4 -- Module      :  GArrowSkeleton
   5 -- Copyright   :  none
   6 -- License     :  public domain
   7 --
   8 -- Maintainer  :  Adam Megacz <megacz@acm.org>
   9 -- Stability   :  experimental
  10 --
  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.
  14 --
  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.
  23 --
  24 module GArrowSkeleton (GArrowSkeleton(..), optimize, beautify)
  25 where
  26 import Prelude hiding ( id, (.), lookup, repeat )
  27 import Control.Category
  28 import GHC.HetMet.GArrow
  29 import Unify
  30 import Control.Monad.State
  31
  32 data GArrowSkeleton m :: * -> * -> *
  33  where
  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
  52
  53 instance Category (GArrowSkeleton m) where
  54   id           = GAS_id
  55   g . f        = GAS_comp f g
  56
  57 instance GArrow (GArrowSkeleton m) (,) () where
  58   ga_first     = GAS_first
  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
  64   ga_assoc     = GAS_assoc
  65   ga_unassoc   = GAS_unassoc
  66
  67 instance GArrowDrop (GArrowSkeleton m) (,) () where
  68   ga_drop      = GAS_drop
  69
  70 instance GArrowCopy (GArrowSkeleton m) (,) () where
  71   ga_copy      = GAS_copy
  72
  73 instance GArrowSwap (GArrowSkeleton m) (,) () where
  74   ga_swap      = GAS_swap
  75
  76 instance GArrowLoop (GArrowSkeleton m) (,) () where
  77   ga_loopl     = GAS_loopl
  78   ga_loopr     = GAS_loopr
  79
  80 type instance GArrowTensor      (GArrowSkeleton m) = (,)
  81 type instance GArrowUnit        (GArrowSkeleton m) = ()
  82 type instance GArrowExponent    (GArrowSkeleton m) = (->)
  83
  84 instance GArrowSTKCL (GArrowSkeleton m)
  85
  86 --
  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.
  90 --
  91 instance Eq ((GArrowSkeleton m) a b)
  92  where
  93   x == y = x === y
  94    where
  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'
 113     _ === _                                     = False
 114     -- FIXME: GAS_misc's are never equal!!!
 115
 116 --
 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.
 120 --
 121 optimize :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
 122 optimize = repeat (gasl2gas . optimizel . gas2gasl)
 123
 124 {-
 125 optimize x = let x' = optimize' x in if x == x' then x' else optimize x'
 126  where
 127   optimize' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
 128
 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))
 135
 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'
 139                                               where
 140                                                 f' = optimize' f
 141                                                 g' = optimize' g
 142                                                 h' = optimize' h
 143   optimize' (GAS_comp      f g     ) = case optimize_pair f g of
 144                                          Nothing   -> GAS_comp f' g'
 145                                          Just ret' -> ret'
 146                                         where
 147                                          f' = optimize' f
 148                                          g' = optimize' 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
 159   optimize' x                        = x
 160
 161   optimize_pair :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) b c -> Maybe ((GArrowSkeleton m) a c)
 162
 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
 172
 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
 178
 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
 185
 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
 190
 191
 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)
 195
 196   optimize_pair _ _                           = Nothing
 197 -}
 198
 199 repeat :: Eq a => (a -> a) -> a -> a
 200 repeat f x = let x' = f x in
 201              if x == x'
 202              then x
 203              else repeat f x'
 204
 205 --
 206 -- | Recursively turns @(ga_first x >>> first y)@ into @(ga_first (x >>> y))@, likewise for ga_second.
 207 --
 208 beautify :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
 209 beautify = optimize . (repeat beautify')
 210  where
 211   beautify' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
 212   beautify' (GAS_comp    (GAS_comp f g) h)              = GAS_comp f $ GAS_comp g            h
 213   beautify' (GAS_comp  f  (GAS_comp (GAS_comp g h) k))  = 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 g) = case (beautify' f, beautify' g) of
 219                               (GAS_first f' , GAS_first  g') -> GAS_first  (GAS_comp f' g')
 220                               (GAS_second f', GAS_second g') -> GAS_second (GAS_comp f' g')
 221                               (f'           , g'           ) -> GAS_comp f' g'
 222   beautify' (GAS_first f)  = GAS_first  $ beautify' f
 223   beautify' (GAS_second f) = GAS_second $ beautify' f
 224   beautify' (GAS_loopl f)  = GAS_loopl  $ beautify' f
 225   beautify' (GAS_loopr f)  = GAS_loopr  $ beautify' f
 226   beautify' q              = q
 227
 228
 229
 230
 231 gas2gasl :: GArrowSkeleton m x y -> GArrowSkeletonL m x y
 232 gas2gasl (GAS_const k    ) = GASL_Y $ GASY_X $ GASX_const k
 233 gas2gasl (GAS_id         ) = GASL_id
 234 gas2gasl (GAS_comp    f g) = gaslcat (gas2gasl f) (gas2gasl g)
 235 gas2gasl (GAS_first     f) = gasl_firstify  $ gas2gasl f
 236 gas2gasl (GAS_second    f) = gasl_secondify $ gas2gasl f
 237 gas2gasl (GAS_cancell    ) = GASL_Y $ GASY_X $ GASX_cancell
 238 gas2gasl (GAS_cancelr    ) = GASL_Y $ GASY_X $ GASX_cancelr
 239 gas2gasl (GAS_uncancell  ) = GASL_Y $ GASY_X $ GASX_uncancell
 240 gas2gasl (GAS_uncancelr  ) = GASL_Y $ GASY_X $ GASX_uncancelr
 241 gas2gasl (GAS_assoc      ) = GASL_Y $ GASY_X $ GASX_assoc
 242 gas2gasl (GAS_unassoc    ) = GASL_Y $ GASY_X $ GASX_unassoc
 243 gas2gasl (GAS_drop       ) = GASL_Y $ GASY_X $ GASX_drop
 244 gas2gasl (GAS_copy       ) = GASL_Y $ GASY_X $ GASX_copy
 245 gas2gasl (GAS_swap       ) = GASL_Y $ GASY_X $ GASX_swap
 246 gas2gasl (GAS_merge      ) = GASL_Y $ GASY_X $ GASX_merge
 247 gas2gasl (GAS_loopl     f) = GASL_Y $ GASY_X $ GASX_loopl $ gas2gasl f
 248 gas2gasl (GAS_loopr     f) = GASL_Y $ GASY_X $ GASX_loopr $ gas2gasl f
 249 gas2gasl (GAS_misc      m) = GASL_Y $ GASY_X $ GASX_misc m
 250
 251 -- apply "first" to a GASL
 252 gasl_firstify :: GArrowSkeletonL m x y -> GArrowSkeletonL m (x,z) (y,z)
 253 gasl_firstify (GASL_id          ) = GASL_id
 254 gasl_firstify (GASL_Y    gy     ) = GASL_Y $ GASY_first $ gy
 255 gasl_firstify (GASL_comp gxq gqy) = GASL_comp (GASY_first gxq) $ gasl_firstify gqy
 256
 257 -- apply "second" to a GASL
 258 gasl_secondify :: GArrowSkeletonL m x y -> GArrowSkeletonL m (z,x) (z,y)
 259 gasl_secondify (GASL_id          ) = GASL_id
 260 gasl_secondify (GASL_Y    gy     ) = GASL_Y $ GASY_second $ gy
 261 gasl_secondify (GASL_comp gxq gqy) = GASL_comp (GASY_second gxq) $ gasl_secondify gqy
 262
 263 -- concatenates two GASL's
 264 gaslcat :: GArrowSkeletonL m x y -> GArrowSkeletonL m y z -> GArrowSkeletonL m x z
 265 gaslcat (GASL_id          ) g' = g'
 266 gaslcat (GASL_Y    gy     ) g' = GASL_comp gy g'
 267 gaslcat (GASL_comp gxq gqy) g' = GASL_comp gxq (gaslcat gqy g')
 268
 269 data GArrowSkeletonL m :: * -> * -> *
 270  where
 271   GASL_id        ::                                                   GArrowSkeletonL m x x
 272   GASL_Y         :: GArrowSkeletonY m x y                          -> GArrowSkeletonL m x y
 273   GASL_comp      :: GArrowSkeletonY m x y -> GArrowSkeletonL m y z -> GArrowSkeletonL m x z
 274
 275 data GArrowSkeletonY m :: * -> * -> *
 276  where
 277   GASY_X         :: GArrowSkeletonX m x y                        -> GArrowSkeletonY m x y
 278   GASY_first     :: GArrowSkeletonY m x y                        -> GArrowSkeletonY m (x,z)  (y,z)
 279   GASY_second    :: GArrowSkeletonY m x y                        -> GArrowSkeletonY m (z,x)  (z,y)
 280
 281 data GArrowSkeletonX m :: * -> * -> *
 282  where
 283   GASX_const     ::                                          Int -> GArrowSkeletonX m () Int
 284   GASX_cancell   ::                                                 GArrowSkeletonX m ((),x) x
 285   GASX_cancelr   ::                                                 GArrowSkeletonX m (x,()) x
 286   GASX_uncancell ::                                                 GArrowSkeletonX m x ((),x)
 287   GASX_uncancelr ::                                                 GArrowSkeletonX m x (x,())
 288   GASX_assoc     ::                                                 GArrowSkeletonX m ((x,y),z) (x,(y,z))
 289   GASX_unassoc   ::                                                 GArrowSkeletonX m (x,(y,z)) ((x,y),z)
 290   GASX_drop      ::                                                 GArrowSkeletonX m x         ()
 291   GASX_copy      ::                                                 GArrowSkeletonX m x         (x,x)
 292   GASX_swap      ::                                                 GArrowSkeletonX m (x,y)     (y,x)
 293   GASX_merge     ::                                                 GArrowSkeletonX m (x,y)     z
 294   GASX_misc      ::                                        m x y -> GArrowSkeletonX m x y
 295   GASX_loopl     ::                GArrowSkeletonL m (z,x) (z,y) -> GArrowSkeletonX m x y
 296   GASX_loopr     ::                GArrowSkeletonL m (x,z) (y,z) -> GArrowSkeletonX m x y
 297
 298 -- TO DO: gather "maximal chunks" of ga_first/ga_second
 299 gasl2gas :: GArrowSkeletonL m x y -> GArrowSkeleton m x y
 300 gasl2gas GASL_id           = GAS_id
 301 gasl2gas (GASL_Y    gy   ) = gasy2gas gy
 302 gasl2gas (GASL_comp gy gl) = GAS_comp (gasy2gas gy) (gasl2gas gl)
 303
 304 gasy2gas :: GArrowSkeletonY m x y -> GArrowSkeleton m x y
 305 gasy2gas (GASY_X      gx)  = gasx2gas gx
 306 gasy2gas (GASY_first  gy)  = GAS_first (gasy2gas gy)
 307 gasy2gas (GASY_second gy)  = GAS_second (gasy2gas gy)
 308
 309 gasx2gas :: GArrowSkeletonX m x y -> GArrowSkeleton m x y
 310 gasx2gas (GASX_const k)    = GAS_const k
 311 gasx2gas (GASX_cancell)    = GAS_cancell
 312 gasx2gas (GASX_cancelr)    = GAS_cancelr
 313 gasx2gas (GASX_uncancell)  = GAS_uncancell
 314 gasx2gas (GASX_uncancelr)  = GAS_uncancelr
 315 gasx2gas (GASX_assoc)      = GAS_assoc
 316 gasx2gas (GASX_unassoc)    = GAS_unassoc
 317 gasx2gas (GASX_drop)       = GAS_drop
 318 gasx2gas (GASX_copy)       = GAS_copy
 319 gasx2gas (GASX_swap)       = GAS_swap
 320 gasx2gas (GASX_merge)      = GAS_merge
 321 gasx2gas (GASX_misc m)     = GAS_misc m
 322 gasx2gas (GASX_loopl gl)   = GAS_loopl $ gasl2gas gl
 323 gasx2gas (GASX_loopr gl)   = GAS_loopr $ gasl2gas gl
 324
 325
 326
 327 optimizel :: GArrowSkeletonL m x y -> GArrowSkeletonL m x y
 328 optimizel (GASL_id        )                                                                                = GASL_id
 329 optimizel (GASL_Y    gy   )                                                                                = GASL_Y $ optimizey gy
 330 optimizel (GASL_comp gy (GASL_comp gy' gl)) | pushright gy, not (pushright gy'), Just x <- pushpair gy gy' = optimizel $ gaslcat x gl
 331 optimizel (GASL_comp gy (GASL_Y gy'))       | pushright gy, not (pushright gy'), Just x <- pushpair gy gy' = GASL_comp (optimizey gy) (GASL_Y gy')
 332 optimizel (GASL_comp gy (GASL_comp gy' gl)) | Just x <- optpair gy gy'                                     = optimizel $ gaslcat x gl
 333 optimizel (GASL_comp gy (GASL_Y gy'))       | Just x <- optpair gy gy'                                     = GASL_comp (optimizey gy) (GASL_Y gy')
 334 optimizel (GASL_comp gy gl)                                                                                = GASL_comp (optimizey gy) (optimizel gl)
 335
 336 --optimize' (GAS_loopl     GAS_id  ) = GAS_id
 337 --optimize' (GAS_loopr     GAS_id  ) = GAS_id
 338 --optimize_pair f GAS_drop                    = Just $ GAS_drop
 339 {-
 340   optimize_pair (GAS_first f) GAS_cancelr     = Just $ GAS_comp   GAS_cancelr f
 341   optimize_pair (GAS_second f) GAS_cancell    = Just $ GAS_comp   GAS_cancell f
 342   optimize_pair GAS_uncancelr (GAS_first f)   = Just $ GAS_comp   f GAS_uncancelr
 343   optimize_pair GAS_uncancell (GAS_second f)  = Just $ GAS_comp   f GAS_uncancell
 344   optimize_pair (GAS_second f) GAS_swap       = Just $ GAS_comp   GAS_swap (GAS_first  f)
 345   optimize_pair (GAS_first f) GAS_swap        = Just $ GAS_comp   GAS_swap (GAS_second f)
 346   optimize_pair GAS_swap GAS_swap             = Just $ GAS_id
 347   optimize_pair GAS_swap GAS_cancell          = Just $ GAS_cancelr
 348   optimize_pair GAS_swap GAS_cancelr          = Just $ GAS_cancell
 349   optimize_pair GAS_assoc   GAS_cancell       = Just $ GAS_first GAS_cancell
 350   optimize_pair GAS_unassoc GAS_cancelr       = Just $ GAS_second GAS_cancelr
 351   optimize_pair GAS_assoc   (GAS_second GAS_cancell)  = Just $ GAS_first GAS_cancelr
 352   optimize_pair GAS_unassoc (GAS_first  GAS_cancell)  = Just $ GAS_cancell
 353 -}
 354
 355 optpair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z)
 356 optpair (GASY_first  gy1) (GASY_first  gy2)           = liftM gasl_firstify  $ optpair gy1 gy2
 357 optpair (GASY_second gy1) (GASY_second gy2)           = liftM gasl_secondify $ optpair gy1 gy2
 358 optpair (GASY_X GASX_uncancell) (GASY_X GASX_cancell) = Just $ GASL_id
 359 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_cancelr) = Just $ GASL_id
 360 optpair (GASY_X GASX_cancell) (GASY_X GASX_uncancell) = Just $ GASL_id
 361 optpair (GASY_X GASX_cancelr) (GASY_X GASX_uncancelr) = Just $ GASL_id
 362 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_cancell) = Just $ GASL_id
 363 optpair (GASY_X GASX_uncancell) (GASY_X GASX_cancelr) = Just $ GASL_id
 364 optpair _ _ = Nothing
 365
 366 pushpair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z)
 367 pushpair (GASY_first  gy1) (GASY_first  gy2)                 = liftM gasl_firstify  $ pushpair gy1 gy2
 368 pushpair (GASY_second gy1) (GASY_second gy2)                 = liftM gasl_secondify $ pushpair gy1 gy2
 369 pushpair (GASY_first  gy1) (GASY_second gy2)                 = Just $ GASL_comp (GASY_second gy2) (GASL_Y $ GASY_first  gy1)
 370 pushpair (GASY_second gy1) (GASY_first  gy2)                 = Just $ GASL_comp (GASY_first  gy2) (GASL_Y $ GASY_second gy1)
 371 pushpair (GASY_first  gy1) (GASY_X GASX_unassoc) = Just $ GASL_comp(GASY_X GASX_unassoc) (GASL_Y $ GASY_first  (GASY_first  gy1))
 372 pushpair (GASY_second gy1) (GASY_X GASX_assoc  ) = Just $ GASL_comp(GASY_X GASX_assoc  ) (GASL_Y $ GASY_second (GASY_second gy1))
 373 pushpair (GASY_second (GASY_X GASX_uncancelr)) (GASY_X GASX_unassoc  ) = Just $ GASL_Y $ GASY_X GASX_uncancelr
 374 pushpair (GASY_first  (GASY_X GASX_uncancell)) (GASY_X GASX_assoc    ) = Just $ GASL_Y $ GASY_X GASX_uncancell
 375 pushpair (GASY_X GASX_uncancelr) (GASY_first gy)  = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancelr)
 376 pushpair (GASY_X GASX_uncancell) (GASY_second gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancell)
 377 pushpair (GASY_first  (GASY_second gy)) (GASY_X GASX_assoc    ) = Just $ GASL_comp (GASY_X GASX_assoc  ) $ GASL_Y (GASY_second (GASY_first  gy))
 378 pushpair (GASY_second (GASY_first  gy)) (GASY_X GASX_unassoc  ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_first  (GASY_second gy))
 379 pushpair (GASY_second (GASY_second gy)) (GASY_X GASX_unassoc  ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_second gy)
 380 pushpair (GASY_first  (GASY_first  gy)) (GASY_X GASX_assoc    ) = Just $ GASL_comp (GASY_X GASX_assoc)   $ GASL_Y (GASY_first gy)
 381 pushpair (GASY_X GASX_uncancell) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first  $ GASY_X GASX_uncancell
 382 pushpair (GASY_X GASX_uncancelr) (GASY_X GASX_assoc   ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancelr
 383 pushpair (GASY_first  (GASY_X GASX_uncancelr)) (GASY_X GASX_assoc    ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancell
 384 pushpair (GASY_second (GASY_X GASX_uncancell)) (GASY_X GASX_unassoc  ) = Just $ GASL_Y $ GASY_first  $ GASY_X GASX_uncancelr
 385 pushpair (GASY_first  gy) (GASY_X GASX_swap    ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_second  gy)
 386 pushpair (GASY_second gy) (GASY_X GASX_swap    ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_first   gy)
 387 pushpair (GASY_X GASX_uncancell) (GASY_X GASX_swap    ) = Just $ GASL_Y $ GASY_X $ GASX_uncancelr
 388 pushpair (GASY_X GASX_uncancelr) (GASY_X GASX_swap    ) = Just $ GASL_Y $ GASY_X $ GASX_uncancell
 389 pushpair _ _                                 = Nothing
 390
 391 -- pushright can only return True for central morphisms
 392 pushright :: GArrowSkeletonY m x y -> Bool
 393 pushright (GASY_first  gy)              = pushright gy
 394 pushright (GASY_second gy)              = pushright gy
 395 pushright (GASY_X      GASX_uncancell)  = True
 396 pushright (GASY_X      GASX_uncancelr)  = True
 397 pushright (GASY_X      _             )  = False
 398
 399 optimizey :: GArrowSkeletonY m x y -> GArrowSkeletonY m x y
 400 optimizey (GASY_X      gx)  = GASY_X $ optimizex gx
 401 optimizey (GASY_first  gy)  = GASY_first (optimizey gy)
 402 optimizey (GASY_second gy)  = GASY_second (optimizey gy)
 403
 404 optimizex :: GArrowSkeletonX m x y -> GArrowSkeletonX m x y
 405 optimizex (GASX_const k)    = GASX_const k
 406 optimizex (GASX_cancell)    = GASX_cancell
 407 optimizex (GASX_cancelr)    = GASX_cancelr
 408 optimizex (GASX_uncancell)  = GASX_uncancell
 409 optimizex (GASX_uncancelr)  = GASX_uncancelr
 410 optimizex (GASX_assoc)      = GASX_assoc
 411 optimizex (GASX_unassoc)    = GASX_unassoc
 412 optimizex (GASX_drop)       = GASX_drop
 413 optimizex (GASX_copy)       = GASX_copy
 414 optimizex (GASX_swap)       = GASX_swap
 415 optimizex (GASX_merge)      = GASX_merge
 416 optimizex (GASX_misc m)     = GASX_misc m
 417 optimizex (GASX_loopl gl)   = GASX_loopl $ optimizel gl
 418 optimizex (GASX_loopr gl)   = GASX_loopr $ optimizel gl