examples/GArrowSkeleton.hs

   1 {-# LANGUAGE MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, TypeFamilies, RankNTypes #-}
   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 is *equivalent to* the term, rather than structurally
  22 -- exactly equal to it.
  23 --
  24 -- A normal form theorem and normalization algorithm are being prepared.
  25 --
  26 module GArrowSkeleton (GArrowSkeleton(..), mkSkeleton, OptimizeFlag(..), optimize, beautify, skelify)
  27 where
  28 import Prelude hiding ( id, (.), lookup, repeat )
  29 import Control.Category
  30 import Control.GArrow
  31 import Unify
  32 import Control.Monad.State
  33 import GArrowInclusion
  34
  35 data GArrowSkeleton m :: * -> * -> *
  36  where
  37   GAS_id        ::                                                 GArrowSkeleton m x x
  38   GAS_comp      :: GArrowSkeleton m x y -> GArrowSkeleton m y z -> GArrowSkeleton m x z
  39   GAS_first     :: GArrowSkeleton m x y                         -> GArrowSkeleton m (x,z)  (y,z)
  40   GAS_second    :: GArrowSkeleton m x y                         -> GArrowSkeleton m (z,x)  (z,y)
  41   GAS_cancell   ::                                                 GArrowSkeleton m ((),x) x
  42   GAS_cancelr   ::                                                 GArrowSkeleton m (x,()) x
  43   GAS_uncancell ::                                                 GArrowSkeleton m x ((),x)
  44   GAS_uncancelr ::                                                 GArrowSkeleton m x (x,())
  45   GAS_assoc     ::                                                 GArrowSkeleton m ((x,y),z) (x,(y,z))
  46   GAS_unassoc   ::                                                 GArrowSkeleton m (x,(y,z)) ((x,y),z)
  47   GAS_drop      ::                                                 GArrowSkeleton m x         ()
  48   GAS_copy      ::                                                 GArrowSkeleton m x         (x,x)
  49   GAS_swap      ::                                                 GArrowSkeleton m (x,y)     (y,x)
  50   GAS_loopl     ::                 GArrowSkeleton m (z,x) (z,y) -> GArrowSkeleton m x y
  51   GAS_loopr     ::                 GArrowSkeleton m (x,z) (y,z) -> GArrowSkeleton m x y
  52   GAS_misc      ::                                        m x y -> GArrowSkeleton m x y
  53
  54 instance Category (GArrowSkeleton m) where
  55   id           = GAS_id
  56   g . f        = GAS_comp f g
  57
  58 instance GArrow (GArrowSkeleton m) (,) () where
  59   ga_first     = GAS_first
  60   ga_second    = GAS_second
  61   ga_cancell   = GAS_cancell
  62   ga_cancelr   = GAS_cancelr
  63   ga_uncancell = GAS_uncancell
  64   ga_uncancelr = GAS_uncancelr
  65   ga_assoc     = GAS_assoc
  66   ga_unassoc   = GAS_unassoc
  67
  68 instance GArrowDrop (GArrowSkeleton m) (,) () where
  69   ga_drop      = GAS_drop
  70
  71 instance GArrowCopy (GArrowSkeleton m) (,) () where
  72   ga_copy      = GAS_copy
  73
  74 instance GArrowSwap (GArrowSkeleton m) (,) () where
  75   ga_swap      = GAS_swap
  76
  77 instance GArrowLoop (GArrowSkeleton m) (,) () where
  78   ga_loopl     = GAS_loopl
  79   ga_loopr     = GAS_loopr
  80
  81 type instance GArrowTensor      (GArrowSkeleton m) = (,)
  82 type instance GArrowUnit        (GArrowSkeleton m) = ()
  83 type instance GArrowExponent    (GArrowSkeleton m) = (->)
  84
  85 instance GArrowCopyDropSwapLoop (GArrowSkeleton m)
  86
  87 instance GArrowInclusion (GArrowSkeleton m) (,) () m where
  88   ga_inc = GAS_misc
  89
  90 skelify :: (forall g . (GArrowCopyDropSwapLoop g, GArrowInclusion g (,) () m) => g x y) -> GArrowSkeleton m x y
  91 skelify = \g -> g
  92
  93 --
  94 -- | Simple structural equality on skeletons.  NOTE: two skeletons
  95 --   with the same shape but different types will nonetheless be "equal";
  96 --   there's no way around this since types are gone at runtime.
  97 --
  98 instance Eq ((GArrowSkeleton m) a b)
  99  where
 100   x == y = x === y
 101    where
 102     (===) :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) c d -> Bool
 103     (GAS_id           ) === (GAS_id           ) = True
 104     (GAS_comp      g f) === (GAS_comp    g' f') = f===f' && g===g'
 105     (GAS_first       f) === (GAS_first  f')     = f===f'
 106     (GAS_second      f) === (GAS_second f')     = f===f'
 107     GAS_cancell         === GAS_cancell         = True
 108     GAS_cancelr         === GAS_cancelr         = True
 109     GAS_uncancell       === GAS_uncancell       = True
 110     GAS_uncancelr       === GAS_uncancelr       = True
 111     GAS_drop            === GAS_drop            = True
 112     GAS_copy            === GAS_copy            = True
 113     GAS_swap            === GAS_swap            = True
 114     GAS_assoc           === GAS_assoc           = True
 115     GAS_unassoc         === GAS_unassoc         = True
 116     (GAS_loopl f)       === (GAS_loopl f')      = f === f'
 117     (GAS_loopr f)       === (GAS_loopr f')      = f === f'
 118     (GAS_misc _)        === (GAS_misc _)        = True      -- FIXME
 119     _ === _                                     = False
 120
 121 data OptimizeFlag = DoOptimize | NoOptimize
 122
 123 mkSkeleton :: OptimizeFlag ->
 124                (forall g .
 125                         (GArrow          g (,) ()
 126                         ,GArrowCopy      g (,) ()
 127                         ,GArrowDrop      g (,) ()
 128                         ,GArrowSwap      g (,) ()
 129                         ,GArrowLoop      g (,) ()
 130                         ,GArrowInclusion g (,) () m) =>
 131                  g x y)
 132                 -> GArrowSkeleton m x y
 133 mkSkeleton DoOptimize = \g -> (beautify . optimize) g
 134 mkSkeleton NoOptimize = \g ->                       g
 135
 136
 137
 138 --
 139 -- | Performs some very simple-minded optimizations on a
 140 --   boxes-and-wires diagram.  Preserves equivalence up to the GArrow
 141 --   laws, but no guarantees about which optimizations actually happen.
 142 --
 143 optimize :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
 144 optimize = repeat (gasl2gas . optimizel . {- FIXME -} optimizel . gas2gasl)
 145
 146 {-
 147 optimize x = let x' = optimize' x in if x == x' then x' else optimize x'
 148  where
 149   optimize' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
 150
 151   -- Some optimizations fail due to misparenthesization; we default to
 152   -- left-associativity and hope for the best
 153   optimize' (GAS_comp              f (GAS_comp g h)   ) = GAS_comp (GAS_comp f g) h
 154   optimize' (GAS_comp    (GAS_comp f (GAS_comp g h)) k) = GAS_comp (GAS_comp (GAS_comp f g) h) k
 155   optimize' (GAS_comp    (GAS_comp             GAS_unassoc  (GAS_second g)) GAS_assoc)   = GAS_second (GAS_second g)
 156   optimize' (GAS_comp    (GAS_comp (GAS_comp f GAS_unassoc) (GAS_second g)) GAS_assoc)   = GAS_comp f (GAS_second (GAS_second g))
 157
 158   optimize' (GAS_comp    (GAS_comp f g) h) = case optimize_pair g h of
 159                                                Nothing   -> GAS_comp (optimize' (GAS_comp f g)) h'
 160                                                Just ret' -> GAS_comp f' ret'
 161                                               where
 162                                                 f' = optimize' f
 163                                                 g' = optimize' g
 164                                                 h' = optimize' h
 165   optimize' (GAS_comp      f g     ) = case optimize_pair f g of
 166                                          Nothing   -> GAS_comp f' g'
 167                                          Just ret' -> ret'
 168                                         where
 169                                          f' = optimize' f
 170                                          g' = optimize' g
 171   optimize' (GAS_first     GAS_id  ) = GAS_id
 172   optimize' (GAS_second    GAS_id  ) = GAS_id
 173 --  optimize' (GAS_first     (GAS_comp f g)) = GAS_comp (GAS_first  f) (GAS_first g)
 174 --  optimize' (GAS_second    (GAS_comp f g)) = GAS_comp (GAS_second f) (GAS_second g)
 175   optimize' (GAS_first     f       ) = GAS_first  $ optimize' f
 176   optimize' (GAS_second    f       ) = GAS_second $ optimize' f
 177   optimize' (GAS_loopl     GAS_id  ) = GAS_id
 178   optimize' (GAS_loopr     GAS_id  ) = GAS_id
 179   optimize' (GAS_loopl     f       ) = GAS_loopl $ optimize' f
 180   optimize' (GAS_loopr     f       ) = GAS_loopr $ optimize' f
 181   optimize' x                        = x
 182
 183   optimize_pair :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) b c -> Maybe ((GArrowSkeleton m) a c)
 184
 185   optimize_pair f GAS_drop                    = Just $ GAS_drop
 186   optimize_pair GAS_id f                      = Just $ f
 187   optimize_pair f GAS_id                      = Just $ f
 188   optimize_pair GAS_uncancell GAS_cancell     = Just $ GAS_id
 189   optimize_pair GAS_uncancelr GAS_cancelr     = Just $ GAS_id
 190   optimize_pair GAS_cancell GAS_uncancell     = Just $ GAS_id
 191   optimize_pair GAS_cancelr GAS_uncancelr     = Just $ GAS_id
 192   optimize_pair GAS_uncancelr GAS_cancell     = Just $ GAS_id
 193   optimize_pair GAS_uncancell GAS_cancelr     = Just $ GAS_id
 194
 195   -- first priority: eliminate GAS_first
 196   optimize_pair (GAS_first f) GAS_cancelr     = Just $ GAS_comp   GAS_cancelr f
 197   optimize_pair (GAS_second f) GAS_cancell    = Just $ GAS_comp   GAS_cancell f
 198   optimize_pair GAS_uncancelr (GAS_first f)   = Just $ GAS_comp   f GAS_uncancelr
 199   optimize_pair GAS_uncancell (GAS_second f)  = Just $ GAS_comp   f GAS_uncancell
 200
 201   -- second priority: push GAS_swap leftward
 202   optimize_pair (GAS_second f) GAS_swap       = Just $ GAS_comp   GAS_swap (GAS_first  f)
 203   optimize_pair (GAS_first f) GAS_swap        = Just $ GAS_comp   GAS_swap (GAS_second f)
 204   optimize_pair GAS_swap GAS_swap             = Just $ GAS_id
 205   optimize_pair GAS_swap GAS_cancell          = Just $ GAS_cancelr
 206   optimize_pair GAS_swap GAS_cancelr          = Just $ GAS_cancell
 207
 208   optimize_pair GAS_assoc   GAS_cancell       = Just $ GAS_first GAS_cancell
 209   optimize_pair GAS_unassoc GAS_cancelr       = Just $ GAS_second GAS_cancelr
 210   optimize_pair GAS_assoc   (GAS_second GAS_cancell)  = Just $ GAS_first GAS_cancelr
 211   optimize_pair GAS_unassoc (GAS_first  GAS_cancell)  = Just $ GAS_cancell
 212
 213
 214   -- FIXME: valid only for central morphisms
 215   --optimize_pair (GAS_second f) (GAS_first g) = Just $ GAS_comp (GAS_first g) (GAS_second f)
 216   optimize_pair (GAS_first g) (GAS_second f) = Just $ GAS_comp  (GAS_second f) (GAS_first g)
 217
 218   optimize_pair _ _                           = Nothing
 219 -}
 220
 221 repeat :: Eq a => (a -> a) -> a -> a
 222 repeat f x = let x' = f x in
 223              if x == x'
 224              then x
 225              else repeat f x'
 226
 227 --
 228 -- | Recursively turns @(ga_first x >>> first y)@ into @(ga_first (x >>> y))@, likewise for ga_second.
 229 --
 230 beautify :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
 231 beautify = repeat beautify'
 232  where
 233   beautify' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b
 234   beautify' (GAS_comp    (GAS_comp f g) h)              = beautify' $ GAS_comp f $ GAS_comp g            h
 235   beautify' (GAS_comp  f  (GAS_comp (GAS_comp g h) k))  = beautify' $ GAS_comp f $ GAS_comp g $ GAS_comp h k
 236   beautify' (GAS_comp f (GAS_comp g h)) = case (beautify' f, beautify' g) of
 237                                             (GAS_first f' , GAS_first  g') -> beautify' $ GAS_comp (GAS_first  (GAS_comp f' g')) h
 238                                             (GAS_second f', GAS_second g') -> beautify' $ GAS_comp (GAS_second (GAS_comp f' g')) h
 239                                             (f'           , g'           ) -> GAS_comp f' (beautify' (GAS_comp g h))
 240   beautify' (GAS_comp f GAS_id) = f
 241   beautify' (GAS_comp GAS_id f) = f
 242   beautify' (GAS_comp f g) = case (beautify' f, beautify' g) of
 243                               (GAS_first f' , GAS_first  g') -> GAS_first  (GAS_comp f' g')
 244                               (GAS_second f', GAS_second g') -> GAS_second (GAS_comp f' g')
 245                               (f'           , g'           ) -> GAS_comp f' g'
 246   beautify' (GAS_first f)  = GAS_first  $ beautify' f
 247   beautify' (GAS_second f) = GAS_second $ beautify' f
 248   beautify' (GAS_loopl f)  = GAS_loopl  $ beautify' f
 249   beautify' (GAS_loopr f)  = GAS_loopr  $ beautify' f
 250   beautify' q              = q
 251
 252
 253
 254
 255 gas2gasl :: GArrowSkeleton m x y -> GArrowSkeletonL m x y
 256 gas2gasl (GAS_id         ) = GASL_id
 257 gas2gasl (GAS_comp    f g) = gaslcat (gas2gasl f) (gas2gasl g)
 258 gas2gasl (GAS_first     f) = gasl_firstify  $ gas2gasl f
 259 gas2gasl (GAS_second    f) = gasl_secondify $ gas2gasl f
 260 gas2gasl (GAS_cancell    ) = GASL_Y $ GASY_X $ GASX_cancell
 261 gas2gasl (GAS_cancelr    ) = GASL_Y $ GASY_X $ GASX_cancelr
 262 gas2gasl (GAS_uncancell  ) = GASL_Y $ GASY_X $ GASX_uncancell
 263 gas2gasl (GAS_uncancelr  ) = GASL_Y $ GASY_X $ GASX_uncancelr
 264 gas2gasl (GAS_assoc      ) = GASL_Y $ GASY_X $ GASX_assoc
 265 gas2gasl (GAS_unassoc    ) = GASL_Y $ GASY_X $ GASX_unassoc
 266 gas2gasl (GAS_drop       ) = GASL_Y $ GASY_X $ GASX_drop
 267 gas2gasl (GAS_copy       ) = GASL_Y $ GASY_X $ GASX_copy
 268 gas2gasl (GAS_swap       ) = GASL_Y $ GASY_X $ GASX_swap
 269 gas2gasl (GAS_loopl     f) = GASL_Y $ GASY_X $ GASX_loopl $ gas2gasl f
 270 gas2gasl (GAS_loopr     f) = GASL_Y $ GASY_X $ GASX_loopr $ gas2gasl f
 271 gas2gasl (GAS_misc      m) = GASL_Y $ GASY_X $ GASX_misc m
 272
 273 -- apply "first" to a GASL
 274 gasl_firstify :: GArrowSkeletonL m x y -> GArrowSkeletonL m (x,z) (y,z)
 275 gasl_firstify (GASL_id          ) = GASL_id
 276 gasl_firstify (GASL_Y    gy     ) = GASL_Y $ GASY_first $ gy
 277 gasl_firstify (GASL_comp gxq gqy) = GASL_comp (GASY_first gxq) $ gasl_firstify gqy
 278
 279 -- apply "second" to a GASL
 280 gasl_secondify :: GArrowSkeletonL m x y -> GArrowSkeletonL m (z,x) (z,y)
 281 gasl_secondify (GASL_id          ) = GASL_id
 282 gasl_secondify (GASL_Y    gy     ) = GASL_Y $ GASY_second $ gy
 283 gasl_secondify (GASL_comp gxq gqy) = GASL_comp (GASY_second gxq) $ gasl_secondify gqy
 284
 285 -- concatenates two GASL's
 286 gaslcat :: GArrowSkeletonL m x y -> GArrowSkeletonL m y z -> GArrowSkeletonL m x z
 287 gaslcat (GASL_id          ) g' = g'
 288 gaslcat (GASL_Y    gy     ) g' = GASL_comp gy g'
 289 gaslcat (GASL_comp gxq gqy) g' = GASL_comp gxq (gaslcat gqy g')
 290
 291 data GArrowSkeletonL m :: * -> * -> *
 292  where
 293   GASL_id        ::                                                   GArrowSkeletonL m x x
 294   GASL_Y         :: GArrowSkeletonY m x y                          -> GArrowSkeletonL m x y
 295   GASL_comp      :: GArrowSkeletonY m x y -> GArrowSkeletonL m y z -> GArrowSkeletonL m x z
 296
 297 data GArrowSkeletonY m :: * -> * -> *
 298  where
 299   GASY_X         :: GArrowSkeletonX m x y                        -> GArrowSkeletonY m x y
 300   GASY_first     :: GArrowSkeletonY m x y                        -> GArrowSkeletonY m (x,z)  (y,z)
 301   GASY_second    :: GArrowSkeletonY m x y                        -> GArrowSkeletonY m (z,x)  (z,y)
 302   GASY_atomicl   :: GArrowSkeletonY m () x                       -> GArrowSkeletonY m y (x,y)
 303   GASY_atomicr   :: GArrowSkeletonY m () x                       -> GArrowSkeletonY m y (y,x)
 304
 305 data GArrowSkeletonX m :: * -> * -> *
 306  where
 307   GASX_cancell   ::                                                 GArrowSkeletonX m ((),x) x
 308   GASX_cancelr   ::                                                 GArrowSkeletonX m (x,()) x
 309   GASX_uncancell ::                                                 GArrowSkeletonX m x ((),x)
 310   GASX_uncancelr ::                                                 GArrowSkeletonX m x (x,())
 311   GASX_assoc     ::                                                 GArrowSkeletonX m ((x,y),z) (x,(y,z))
 312   GASX_unassoc   ::                                                 GArrowSkeletonX m (x,(y,z)) ((x,y),z)
 313   GASX_drop      ::                                                 GArrowSkeletonX m x         ()
 314   GASX_copy      ::                                                 GArrowSkeletonX m x         (x,x)
 315   GASX_swap      ::                                                 GArrowSkeletonX m (x,y)     (y,x)
 316   GASX_misc      ::                                        m x y -> GArrowSkeletonX m x y
 317   GASX_loopl     ::                GArrowSkeletonL m (z,x) (z,y) -> GArrowSkeletonX m x y
 318   GASX_loopr     ::                GArrowSkeletonL m (x,z) (y,z) -> GArrowSkeletonX m x y
 319
 320 -- TO DO: gather "maximal chunks" of ga_first/ga_second
 321 gasl2gas :: GArrowSkeletonL m x y -> GArrowSkeleton m x y
 322 gasl2gas GASL_id           = GAS_id
 323 gasl2gas (GASL_Y    gy   ) = gasy2gas gy
 324 gasl2gas (GASL_comp gy gl) = GAS_comp (gasy2gas gy) (gasl2gas gl)
 325
 326 gasy2gas :: GArrowSkeletonY m x y -> GArrowSkeleton m x y
 327 gasy2gas (GASY_X      gx)  = gasx2gas gx
 328 gasy2gas (GASY_first  gy)  = GAS_first (gasy2gas gy)
 329 gasy2gas (GASY_second gy)  = GAS_second (gasy2gas gy)
 330 gasy2gas (GASY_atomicl gy) = GAS_comp GAS_uncancell (GAS_first  $ gasy2gas gy)
 331 gasy2gas (GASY_atomicr gy) = GAS_comp GAS_uncancelr (GAS_second $ gasy2gas gy)
 332
 333 gasx2gas :: GArrowSkeletonX m x y -> GArrowSkeleton m x y
 334 gasx2gas (GASX_cancell)    = GAS_cancell
 335 gasx2gas (GASX_cancelr)    = GAS_cancelr
 336 gasx2gas (GASX_uncancell)  = GAS_uncancell
 337 gasx2gas (GASX_uncancelr)  = GAS_uncancelr
 338 gasx2gas (GASX_assoc)      = GAS_assoc
 339 gasx2gas (GASX_unassoc)    = GAS_unassoc
 340 gasx2gas (GASX_drop)       = GAS_drop
 341 gasx2gas (GASX_copy)       = GAS_copy
 342 gasx2gas (GASX_swap)       = GAS_swap
 343 gasx2gas (GASX_misc m)     = GAS_misc m
 344 gasx2gas (GASX_loopl gl)   = GAS_loopl $ gasl2gas gl
 345 gasx2gas (GASX_loopr gl)   = GAS_loopr $ gasl2gas gl
 346
 347
 348
 349 optimizel :: GArrowSkeletonL m x y -> GArrowSkeletonL m x y
 350 --optimizel (GASL_comp (GASL_Y (GASY_X GAS_uncancelr)) (GASL_Y (GASY_X      GASX_copy))) =
 351 --  (GASL_comp (GASL_Y (GASY_X GAS_uncancelr)) (GASL_Y (GASY_X      GASX_copy)))
 352 optimizel (GASL_id        )                                                                                = GASL_id
 353 optimizel (GASL_Y    gy   )                                                                                = GASL_Y $ optimizey gy
 354 optimizel (GASL_comp gy (GASL_comp gy' gl)) | Just x <- optpair gy gy'                                     = optimizel $ gaslcat x gl
 355 optimizel (GASL_comp gy (GASL_Y gy'))       | Just x <- optpair gy gy'                                     = x
 356 optimizel (GASL_comp gy (GASL_comp gy' gl)) | pushright gy, not (pushright gy'), Just x <- swappair gy gy' = optimizel $ gaslcat x gl
 357 optimizel (GASL_comp gy (GASL_Y gy'))       | pushright gy, not (pushright gy'), Just x <- swappair gy gy' = GASL_comp (optimizey gy) (GASL_Y gy')
 358 optimizel (GASL_comp gy gl)                                                                                = GASL_comp (optimizey gy) (optimizel gl)
 359
 360 --optimize' (GAS_loopl     GAS_id  ) = GAS_id
 361 --optimize' (GAS_loopr     GAS_id  ) = GAS_id
 362 --optimize_pair f GAS_drop                    = Just $ GAS_drop
 363 {-
 364   optimize_pair (GAS_first f) GAS_cancelr     = Just $ GAS_comp   GAS_cancelr f
 365   optimize_pair (GAS_second f) GAS_cancell    = Just $ GAS_comp   GAS_cancell f
 366   optimize_pair GAS_uncancelr (GAS_first f)   = Just $ GAS_comp   f GAS_uncancelr
 367   optimize_pair GAS_uncancell (GAS_second f)  = Just $ GAS_comp   f GAS_uncancell
 368   optimize_pair (GAS_second f) GAS_swap       = Just $ GAS_comp   GAS_swap (GAS_first  f)
 369   optimize_pair (GAS_first f) GAS_swap        = Just $ GAS_comp   GAS_swap (GAS_second f)
 370   optimize_pair GAS_swap GAS_swap             = Just $ GAS_id
 371   optimize_pair GAS_swap GAS_cancell          = Just $ GAS_cancelr
 372   optimize_pair GAS_swap GAS_cancelr          = Just $ GAS_cancell
 373   optimize_pair GAS_assoc   GAS_cancell       = Just $ GAS_first GAS_cancell
 374   optimize_pair GAS_unassoc GAS_cancelr       = Just $ GAS_second GAS_cancelr
 375   optimize_pair GAS_assoc   (GAS_second GAS_cancell)  = Just $ GAS_first GAS_cancelr
 376   optimize_pair GAS_unassoc (GAS_first  GAS_cancell)  = Just $ GAS_cancell
 377 -}
 378
 379 optpair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z)
 380
 381 optpair (GASY_atomicl g) (GASY_X GASX_cancelr) = Just $ GASL_Y g
 382 optpair (GASY_atomicr g) (GASY_X GASX_cancell) = Just $ GASL_Y g
 383
 384 optpair (GASY_X GASX_uncancell) (GASY_X GASX_cancell) = Just $ GASL_id
 385 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_cancelr) = Just $ GASL_id
 386 optpair (GASY_X GASX_cancell) (GASY_X GASX_uncancell) = Just $ GASL_id
 387 optpair (GASY_X GASX_cancelr) (GASY_X GASX_uncancelr) = Just $ GASL_id
 388 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_cancell) = Just $ GASL_id
 389 optpair (GASY_X GASX_uncancell) (GASY_X GASX_cancelr) = Just $ GASL_id
 390 optpair (GASY_X GASX_assoc)     (GASY_X GASX_cancell) = Just $ GASL_Y $ GASY_first  $ GASY_X GASX_cancell
 391 optpair (GASY_X GASX_unassoc)   (GASY_X GASX_cancelr) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_cancelr
 392 optpair (GASY_second (GASY_X GASX_uncancelr)) (GASY_X GASX_unassoc  ) = Just $ GASL_Y $ GASY_X GASX_uncancelr
 393 optpair (GASY_first  (GASY_X GASX_uncancell)) (GASY_X GASX_assoc    ) = Just $ GASL_Y $ GASY_X GASX_uncancell
 394 optpair (GASY_X GASX_uncancell) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first  $ GASY_X GASX_uncancell
 395 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_assoc   ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancelr
 396 optpair (GASY_first  (GASY_X GASX_uncancelr)) (GASY_X GASX_assoc    ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancell
 397 optpair (GASY_second (GASY_X GASX_uncancell)) (GASY_X GASX_unassoc  ) = Just $ GASL_Y $ GASY_first  $ GASY_X GASX_uncancelr
 398 optpair (GASY_X GASX_assoc)     (GASY_second (GASY_X GASX_cancelr)) = Just $ GASL_Y $ GASY_X $ GASX_cancelr
 399 optpair (GASY_X GASX_unassoc)   (GASY_first  (GASY_X GASX_cancell)) = Just $ GASL_Y $ GASY_X $ GASX_cancell
 400 optpair (GASY_first  g) (GASY_X GASX_cancelr) = Just $ GASL_comp (GASY_X GASX_cancelr) $ GASL_Y $ g
 401 optpair (GASY_second g) (GASY_X GASX_cancell) = Just $ GASL_comp (GASY_X GASX_cancell) $ GASL_Y $ g
 402 optpair (GASY_X GASX_uncancelr) (GASY_first  g) = Just $ GASL_comp g $ GASL_Y (GASY_X GASX_uncancelr)
 403 optpair (GASY_X GASX_uncancell) (GASY_second g) = Just $ GASL_comp g $ GASL_Y (GASY_X GASX_uncancell)
 404
 405 -- swap with an {un}cancel{l,r} before/after it
 406 optpair (GASY_X GASX_uncancell) (GASY_X GASX_swap    ) = Just $ GASL_Y $ GASY_X $ GASX_uncancelr
 407 optpair (GASY_X GASX_uncancelr) (GASY_X GASX_swap    ) = Just $ GASL_Y $ GASY_X $ GASX_uncancell
 408 optpair (GASY_X GASX_swap) (GASY_X GASX_cancell) = Just $ GASL_Y $ GASY_X $ GASX_cancelr
 409 optpair (GASY_X GASX_swap) (GASY_X GASX_cancelr) = Just $ GASL_Y $ GASY_X $ GASX_cancell
 410
 411 {-
 412 optpair (GASY_X GASX_uncancelr) (GASY_X (GASX_loopl gl)) =
 413     Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ GASY_X GASX_uncancelr) gl)
 414 optpair (GASY_X GASX_uncancell) (GASY_X (GASX_loopl gl)) =
 415     Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ GASY_X GASX_uncancell) gl)
 416 optpair (GASY_X GASX_uncancelr) (GASY_X (GASX_loopr gl)) =
 417     Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ GASY_X GASX_uncancelr) gl)
 418 optpair (GASY_X GASX_uncancell) (GASY_X (GASX_loopr gl)) =
 419     Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ GASY_X GASX_uncancell) gl)
 420 -}
 421 optpair q (GASY_X (GASX_loopl gl)) | pushin q = Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ q) gl)
 422 optpair q (GASY_X (GASX_loopr gl)) | pushin q = Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ q) gl)
 423
 424 optpair (GASY_first  gy1) (GASY_second  gy2) | pushleft gy2, not (pushleft gy1)
 425                                                  = Just $ GASL_comp (GASY_second gy2) $ GASL_Y $ GASY_first  gy1
 426 optpair (GASY_second gy1) (GASY_first   gy2) | pushleft gy2, not (pushleft gy1)
 427                                                  = Just $ GASL_comp (GASY_first  gy2) $ GASL_Y $ GASY_second gy1
 428
 429 optpair (GASY_first  gy1) (GASY_first  gy2)           = liftM gasl_firstify  $ optpair gy1 gy2
 430 optpair (GASY_second gy1) (GASY_second gy2)           = liftM gasl_secondify $ optpair gy1 gy2
 431 optpair _ _                                           = Nothing
 432
 433 swappair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z)
 434
 435 swappair q (GASY_atomicl g) = Just $ GASL_comp (GASY_atomicl g) $ GASL_Y $ GASY_second q
 436 swappair q (GASY_atomicr g) = Just $ GASL_comp (GASY_atomicr g) $ GASL_Y $ GASY_first  q
 437
 438 swappair (GASY_first  gy1) (GASY_second gy2)                 = Just $ GASL_comp (GASY_second gy2) (GASL_Y $ GASY_first  gy1)
 439 swappair (GASY_second gy1) (GASY_first  gy2)                 = Just $ GASL_comp (GASY_first  gy2) (GASL_Y $ GASY_second gy1)
 440 swappair (GASY_first  gy1) (GASY_X GASX_unassoc) = Just $ GASL_comp(GASY_X GASX_unassoc) (GASL_Y $ GASY_first  (GASY_first  gy1))
 441 swappair (GASY_second gy1) (GASY_X GASX_assoc  ) = Just $ GASL_comp(GASY_X GASX_assoc  ) (GASL_Y $ GASY_second (GASY_second gy1))
 442 swappair (GASY_X GASX_uncancelr) (GASY_first gy)  = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancelr)
 443 swappair (GASY_X GASX_uncancell) (GASY_second gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancell)
 444 swappair (GASY_first  (GASY_second gy)) (GASY_X GASX_assoc    ) = Just $ GASL_comp (GASY_X GASX_assoc  ) $ GASL_Y (GASY_second (GASY_first  gy))
 445 swappair (GASY_second (GASY_first  gy)) (GASY_X GASX_unassoc  ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_first  (GASY_second gy))
 446 swappair (GASY_second (GASY_second gy)) (GASY_X GASX_unassoc  ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_second gy)
 447 swappair (GASY_first  (GASY_first  gy)) (GASY_X GASX_assoc    ) = Just $ GASL_comp (GASY_X GASX_assoc)   $ GASL_Y (GASY_first gy)
 448 swappair (GASY_first  gy) (GASY_X GASX_swap    ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_second  gy)
 449 swappair (GASY_second gy) (GASY_X GASX_swap    ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_first   gy)
 450 swappair gy          (GASY_X (GASX_loopl gl))  = Just $ GASL_Y $ GASY_X $ GASX_loopl $ GASL_comp (GASY_second gy) gl
 451 swappair gy          (GASY_X (GASX_loopr gl))  = Just $ GASL_Y $ GASY_X $ GASX_loopr $ GASL_comp (GASY_first gy) gl
 452
 453 swappair (GASY_first  gy1) (GASY_first  gy2)                 = liftM gasl_firstify  $ swappair gy1 gy2
 454 swappair (GASY_second gy1) (GASY_second gy2)                 = liftM gasl_secondify $ swappair gy1 gy2
 455 swappair _ _                                 = Nothing
 456
 457 -- pushright can only return True for central morphisms
 458 pushright :: GArrowSkeletonY m x y -> Bool
 459 pushright (GASY_first  gy)              = pushright gy
 460 pushright (GASY_second gy)              = pushright gy
 461 pushright (GASY_atomicl _)              = False
 462 pushright (GASY_atomicr _)              = False
 463 pushright (GASY_X      GASX_uncancell)  = True
 464 pushright (GASY_X      GASX_uncancelr)  = True
 465 pushright (GASY_X      _             )  = False
 466
 467 -- says if we should push it into a loopl/r
 468 pushin :: GArrowSkeletonY m x y -> Bool
 469 pushin gy = pushright gy || pushin' gy
 470  where
 471   pushin' :: GArrowSkeletonY m a b -> Bool
 472   pushin' (GASY_first  gy)              = pushin' gy
 473   pushin' (GASY_second gy)              = pushin' gy
 474   pushin' (GASY_atomicl _)              = False
 475   pushin' (GASY_atomicr _)              = False
 476
 477   -- not sure if these are a good idea
 478   pushin' (GASY_X      GASX_copy)       = True
 479   pushin' (GASY_X      GASX_swap)       = True
 480
 481   pushin' (GASY_X      _             )  = False
 482
 483 optimizey :: GArrowSkeletonY m x y -> GArrowSkeletonY m x y
 484 optimizey (GASY_X      gx)  = GASY_X $ optimizex gx
 485 optimizey (GASY_first  gy)  = GASY_first (optimizey gy)
 486 optimizey (GASY_second gy)  = GASY_second (optimizey gy)
 487 optimizey (GASY_atomicl gy) = GASY_atomicl $ optimizey gy
 488 optimizey (GASY_atomicr gy) = GASY_atomicr $ optimizey gy
 489
 490 optimizex :: GArrowSkeletonX m x y -> GArrowSkeletonX m x y
 491 optimizex (GASX_cancell)    = GASX_cancell
 492 optimizex (GASX_cancelr)    = GASX_cancelr
 493 optimizex (GASX_uncancell)  = GASX_uncancell
 494 optimizex (GASX_uncancelr)  = GASX_uncancelr
 495 optimizex (GASX_assoc)      = GASX_assoc
 496 optimizex (GASX_unassoc)    = GASX_unassoc
 497 optimizex (GASX_drop)       = GASX_drop
 498 optimizex (GASX_copy)       = GASX_copy
 499 optimizex (GASX_swap)       = GASX_swap
 500 optimizex (GASX_misc m)     = GASX_misc m
 501 optimizex (GASX_loopl (GASL_comp (GASY_first gy) gl))| pushleft gy  = GASX_loopl $ gaslcat gl (GASL_Y $ GASY_first gy)
 502 optimizex (GASX_loopr (GASL_comp (GASY_second gy) gl))| pushleft gy  = GASX_loopr $ gaslcat gl (GASL_Y $ GASY_second gy)
 503 optimizex (GASX_loopl gl)   = GASX_loopl $ optimizel gl
 504 optimizex (GASX_loopr gl)   = GASX_loopr $ optimizel gl
 505
 506 pushleft :: GArrowSkeletonY m x y -> Bool
 507 pushleft (GASY_first  gy)            = pushleft gy
 508 pushleft (GASY_second gy)            = pushleft gy
 509 pushleft (GASY_atomicl _)            = False
 510 pushleft (GASY_atomicr _)            = False
 511 pushleft (GASY_X      GASX_cancell)  = True
 512 pushleft (GASY_X      GASX_cancelr)  = True
 513 pushleft (GASY_X      _           )  = False