X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=examples%2FGArrowSkeleton.hs;h=dd7937ba61ab5412cd4669a4f2514a9e702763f5;hp=c63fd151a43840df2b6f7d369a7c68be243498c2;hb=63abf29c05f4c3cc510ad56050542579084e63c3;hpb=aaad4c11e0da05d9daa683bbf61f56769c0d68fb diff --git a/examples/GArrowSkeleton.hs b/examples/GArrowSkeleton.hs index c63fd15..dd7937b 100644 --- a/examples/GArrowSkeleton.hs +++ b/examples/GArrowSkeleton.hs @@ -21,9 +21,9 @@ -- diagram which ks *equivalent to* the term, rather than structurally -- exactly equal to it. -- -module GArrowSkeleton (GArrowSkeleton(..), optimize) +module GArrowSkeleton (GArrowSkeleton(..), optimize, beautify) where -import Prelude hiding ( id, (.), lookup ) +import Prelude hiding ( id, (.), lookup, repeat ) import Control.Category import GHC.HetMet.GArrow import Unify @@ -46,8 +46,8 @@ data GArrowSkeleton m :: * -> * -> * GAS_copy :: GArrowSkeleton m x (x,x) GAS_swap :: GArrowSkeleton m (x,y) (y,x) GAS_merge :: GArrowSkeleton m (x,y) z - GAS_loopl :: GArrowSkeleton m (x,z) (y,z) -> GArrowSkeleton m x y - GAS_loopr :: GArrowSkeleton m (z,x) (z,y) -> GArrowSkeleton m x y + GAS_loopl :: GArrowSkeleton m (z,x) (z,y) -> GArrowSkeleton m x y + GAS_loopr :: GArrowSkeleton m (x,z) (y,z) -> GArrowSkeleton m x y GAS_misc :: m x y -> GArrowSkeleton m x y instance Category (GArrowSkeleton m) where @@ -81,7 +81,7 @@ type instance GArrowTensor (GArrowSkeleton m) = (,) type instance GArrowUnit (GArrowSkeleton m) = () type instance GArrowExponent (GArrowSkeleton m) = (->) -instance GArrowSTKC (GArrowSkeleton m) +instance GArrowSTKCL (GArrowSkeleton m) -- -- | Simple structural equality on skeletons. NOTE: two skeletons @@ -119,15 +119,17 @@ instance Eq ((GArrowSkeleton m) a b) -- laws, but no guarantees about which optimizations actually happen. -- optimize :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b +optimize = repeat (gasl2gas . optimizel . {- FIXME -} optimizel . gas2gasl) + +{- optimize x = let x' = optimize' x in if x == x' then x' else optimize x' where optimize' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b -- Some optimizations fail due to misparenthesization; we default to -- left-associativity and hope for the best - optimize' (GAS_comp f (GAS_comp g h)) = GAS_comp (GAS_comp f g) h + optimize' (GAS_comp f (GAS_comp g h) ) = GAS_comp (GAS_comp f g) h optimize' (GAS_comp (GAS_comp f (GAS_comp g h)) k) = GAS_comp (GAS_comp (GAS_comp f g) h) k - optimize' (GAS_comp (GAS_comp GAS_unassoc (GAS_second g)) GAS_assoc) = GAS_second (GAS_second g) optimize' (GAS_comp (GAS_comp (GAS_comp f GAS_unassoc) (GAS_second g)) GAS_assoc) = GAS_comp f (GAS_second (GAS_second g)) @@ -146,13 +148,15 @@ optimize x = let x' = optimize' x in if x == x' then x' else optimize x' g' = optimize' g optimize' (GAS_first GAS_id ) = GAS_id optimize' (GAS_second GAS_id ) = GAS_id +-- optimize' (GAS_first (GAS_comp f g)) = GAS_comp (GAS_first f) (GAS_first g) +-- optimize' (GAS_second (GAS_comp f g)) = GAS_comp (GAS_second f) (GAS_second g) optimize' (GAS_first f ) = GAS_first $ optimize' f optimize' (GAS_second f ) = GAS_second $ optimize' f - optimize' (GAS_loopl GAS_id) = GAS_id - optimize' (GAS_loopr GAS_id) = GAS_id - optimize' (GAS_loopl f ) = GAS_loopl $ optimize' f - optimize' (GAS_loopr f ) = GAS_loopr $ optimize' f - optimize' x = x + optimize' (GAS_loopl GAS_id ) = GAS_id + optimize' (GAS_loopr GAS_id ) = GAS_id + optimize' (GAS_loopl f ) = GAS_loopl $ optimize' f + optimize' (GAS_loopr f ) = GAS_loopr $ optimize' f + optimize' x = x optimize_pair :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) b c -> Maybe ((GArrowSkeleton m) a c) @@ -179,9 +183,6 @@ optimize x = let x' = optimize' x in if x == x' then x' else optimize x' optimize_pair GAS_swap GAS_cancell = Just $ GAS_cancelr optimize_pair GAS_swap GAS_cancelr = Just $ GAS_cancell - optimize_pair (GAS_first f) (GAS_first g) = Just $ GAS_first (GAS_comp f g) - optimize_pair (GAS_second f) (GAS_second g) = Just $ GAS_second (GAS_comp f g) - optimize_pair GAS_assoc GAS_cancell = Just $ GAS_first GAS_cancell optimize_pair GAS_unassoc GAS_cancelr = Just $ GAS_second GAS_cancelr optimize_pair GAS_assoc (GAS_second GAS_cancell) = Just $ GAS_first GAS_cancelr @@ -193,5 +194,307 @@ optimize x = let x' = optimize' x in if x == x' then x' else optimize x' optimize_pair (GAS_first g) (GAS_second f) = Just $ GAS_comp (GAS_second f) (GAS_first g) optimize_pair _ _ = Nothing +-} + +repeat :: Eq a => (a -> a) -> a -> a +repeat f x = let x' = f x in + if x == x' + then x + else repeat f x' + +-- +-- | Recursively turns @(ga_first x >>> first y)@ into @(ga_first (x >>> y))@, likewise for ga_second. +-- +beautify :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b +beautify = repeat beautify' + where + beautify' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b + beautify' (GAS_comp (GAS_comp f g) h) = beautify' $ GAS_comp f $ GAS_comp g h + beautify' (GAS_comp f (GAS_comp (GAS_comp g h) k)) = beautify' $ GAS_comp f $ GAS_comp g $ GAS_comp h k + beautify' (GAS_comp f (GAS_comp g h)) = case (beautify' f, beautify' g) of + (GAS_first f' , GAS_first g') -> beautify' $ GAS_comp (GAS_first (GAS_comp f' g')) h + (GAS_second f', GAS_second g') -> beautify' $ GAS_comp (GAS_second (GAS_comp f' g')) h + (f' , g' ) -> GAS_comp f' (beautify' (GAS_comp g h)) + beautify' (GAS_comp f GAS_id) = f + beautify' (GAS_comp GAS_id f) = f + beautify' (GAS_comp f g) = case (beautify' f, beautify' g) of + (GAS_first f' , GAS_first g') -> GAS_first (GAS_comp f' g') + (GAS_second f', GAS_second g') -> GAS_second (GAS_comp f' g') + (f' , g' ) -> GAS_comp f' g' + beautify' (GAS_first f) = GAS_first $ beautify' f + beautify' (GAS_second f) = GAS_second $ beautify' f + beautify' (GAS_loopl f) = GAS_loopl $ beautify' f + beautify' (GAS_loopr f) = GAS_loopr $ beautify' f + beautify' q = q + + + + +gas2gasl :: GArrowSkeleton m x y -> GArrowSkeletonL m x y +gas2gasl (GAS_const k ) = GASL_Y $ GASY_X $ GASX_const k +gas2gasl (GAS_id ) = GASL_id +gas2gasl (GAS_comp f g) = gaslcat (gas2gasl f) (gas2gasl g) +gas2gasl (GAS_first f) = gasl_firstify $ gas2gasl f +gas2gasl (GAS_second f) = gasl_secondify $ gas2gasl f +gas2gasl (GAS_cancell ) = GASL_Y $ GASY_X $ GASX_cancell +gas2gasl (GAS_cancelr ) = GASL_Y $ GASY_X $ GASX_cancelr +gas2gasl (GAS_uncancell ) = GASL_Y $ GASY_X $ GASX_uncancell +gas2gasl (GAS_uncancelr ) = GASL_Y $ GASY_X $ GASX_uncancelr +gas2gasl (GAS_assoc ) = GASL_Y $ GASY_X $ GASX_assoc +gas2gasl (GAS_unassoc ) = GASL_Y $ GASY_X $ GASX_unassoc +gas2gasl (GAS_drop ) = GASL_Y $ GASY_X $ GASX_drop +gas2gasl (GAS_copy ) = GASL_Y $ GASY_X $ GASX_copy +gas2gasl (GAS_swap ) = GASL_Y $ GASY_X $ GASX_swap +gas2gasl (GAS_merge ) = GASL_Y $ GASY_X $ GASX_merge +gas2gasl (GAS_loopl f) = GASL_Y $ GASY_X $ GASX_loopl $ gas2gasl f +gas2gasl (GAS_loopr f) = GASL_Y $ GASY_X $ GASX_loopr $ gas2gasl f +gas2gasl (GAS_misc m) = GASL_Y $ GASY_X $ GASX_misc m + +-- apply "first" to a GASL +gasl_firstify :: GArrowSkeletonL m x y -> GArrowSkeletonL m (x,z) (y,z) +gasl_firstify (GASL_id ) = GASL_id +gasl_firstify (GASL_Y gy ) = GASL_Y $ GASY_first $ gy +gasl_firstify (GASL_comp gxq gqy) = GASL_comp (GASY_first gxq) $ gasl_firstify gqy + +-- apply "second" to a GASL +gasl_secondify :: GArrowSkeletonL m x y -> GArrowSkeletonL m (z,x) (z,y) +gasl_secondify (GASL_id ) = GASL_id +gasl_secondify (GASL_Y gy ) = GASL_Y $ GASY_second $ gy +gasl_secondify (GASL_comp gxq gqy) = GASL_comp (GASY_second gxq) $ gasl_secondify gqy + +-- concatenates two GASL's +gaslcat :: GArrowSkeletonL m x y -> GArrowSkeletonL m y z -> GArrowSkeletonL m x z +gaslcat (GASL_id ) g' = g' +gaslcat (GASL_Y gy ) g' = GASL_comp gy g' +gaslcat (GASL_comp gxq gqy) g' = GASL_comp gxq (gaslcat gqy g') + +data GArrowSkeletonL m :: * -> * -> * + where + GASL_id :: GArrowSkeletonL m x x + GASL_Y :: GArrowSkeletonY m x y -> GArrowSkeletonL m x y + GASL_comp :: GArrowSkeletonY m x y -> GArrowSkeletonL m y z -> GArrowSkeletonL m x z + +data GArrowSkeletonY m :: * -> * -> * + where + GASY_X :: GArrowSkeletonX m x y -> GArrowSkeletonY m x y + GASY_first :: GArrowSkeletonY m x y -> GArrowSkeletonY m (x,z) (y,z) + GASY_second :: GArrowSkeletonY m x y -> GArrowSkeletonY m (z,x) (z,y) + GASY_atomicl :: GArrowSkeletonY m () x -> GArrowSkeletonY m y (x,y) + GASY_atomicr :: GArrowSkeletonY m () x -> GArrowSkeletonY m y (y,x) + +data GArrowSkeletonX m :: * -> * -> * + where + GASX_const :: Int -> GArrowSkeletonX m () Int + GASX_cancell :: GArrowSkeletonX m ((),x) x + GASX_cancelr :: GArrowSkeletonX m (x,()) x + GASX_uncancell :: GArrowSkeletonX m x ((),x) + GASX_uncancelr :: GArrowSkeletonX m x (x,()) + GASX_assoc :: GArrowSkeletonX m ((x,y),z) (x,(y,z)) + GASX_unassoc :: GArrowSkeletonX m (x,(y,z)) ((x,y),z) + GASX_drop :: GArrowSkeletonX m x () + GASX_copy :: GArrowSkeletonX m x (x,x) + GASX_swap :: GArrowSkeletonX m (x,y) (y,x) + GASX_merge :: GArrowSkeletonX m (x,y) z + GASX_misc :: m x y -> GArrowSkeletonX m x y + GASX_loopl :: GArrowSkeletonL m (z,x) (z,y) -> GArrowSkeletonX m x y + GASX_loopr :: GArrowSkeletonL m (x,z) (y,z) -> GArrowSkeletonX m x y + +-- TO DO: gather "maximal chunks" of ga_first/ga_second +gasl2gas :: GArrowSkeletonL m x y -> GArrowSkeleton m x y +gasl2gas GASL_id = GAS_id +gasl2gas (GASL_Y gy ) = gasy2gas gy +gasl2gas (GASL_comp gy gl) = GAS_comp (gasy2gas gy) (gasl2gas gl) + +gasy2gas :: GArrowSkeletonY m x y -> GArrowSkeleton m x y +gasy2gas (GASY_X gx) = gasx2gas gx +gasy2gas (GASY_first gy) = GAS_first (gasy2gas gy) +gasy2gas (GASY_second gy) = GAS_second (gasy2gas gy) +gasy2gas (GASY_atomicl gy) = GAS_comp GAS_uncancell (GAS_first $ gasy2gas gy) +gasy2gas (GASY_atomicr gy) = GAS_comp GAS_uncancelr (GAS_second $ gasy2gas gy) + +gasx2gas :: GArrowSkeletonX m x y -> GArrowSkeleton m x y +gasx2gas (GASX_const k) = GAS_const k +gasx2gas (GASX_cancell) = GAS_cancell +gasx2gas (GASX_cancelr) = GAS_cancelr +gasx2gas (GASX_uncancell) = GAS_uncancell +gasx2gas (GASX_uncancelr) = GAS_uncancelr +gasx2gas (GASX_assoc) = GAS_assoc +gasx2gas (GASX_unassoc) = GAS_unassoc +gasx2gas (GASX_drop) = GAS_drop +gasx2gas (GASX_copy) = GAS_copy +gasx2gas (GASX_swap) = GAS_swap +gasx2gas (GASX_merge) = GAS_merge +gasx2gas (GASX_misc m) = GAS_misc m +gasx2gas (GASX_loopl gl) = GAS_loopl $ gasl2gas gl +gasx2gas (GASX_loopr gl) = GAS_loopr $ gasl2gas gl + + + +optimizel :: GArrowSkeletonL m x y -> GArrowSkeletonL m x y +optimizel (GASL_id ) = GASL_id +optimizel (GASL_Y gy ) = GASL_Y $ optimizey gy +optimizel (GASL_comp gy (GASL_comp gy' gl)) | Just x <- optpair gy gy' = optimizel $ gaslcat x gl +optimizel (GASL_comp gy (GASL_Y gy')) | Just x <- optpair gy gy' = x +optimizel (GASL_comp gy (GASL_comp gy' gl)) | pushright gy, not (pushright gy'), Just x <- swappair gy gy' = optimizel $ gaslcat x gl +optimizel (GASL_comp gy (GASL_Y gy')) | pushright gy, not (pushright gy'), Just x <- swappair gy gy' = GASL_comp (optimizey gy) (GASL_Y gy') +optimizel (GASL_comp gy gl) = GASL_comp (optimizey gy) (optimizel gl) + +--optimize' (GAS_loopl GAS_id ) = GAS_id +--optimize' (GAS_loopr GAS_id ) = GAS_id +--optimize_pair f GAS_drop = Just $ GAS_drop +{- + optimize_pair (GAS_first f) GAS_cancelr = Just $ GAS_comp GAS_cancelr f + optimize_pair (GAS_second f) GAS_cancell = Just $ GAS_comp GAS_cancell f + optimize_pair GAS_uncancelr (GAS_first f) = Just $ GAS_comp f GAS_uncancelr + optimize_pair GAS_uncancell (GAS_second f) = Just $ GAS_comp f GAS_uncancell + optimize_pair (GAS_second f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_first f) + optimize_pair (GAS_first f) GAS_swap = Just $ GAS_comp GAS_swap (GAS_second f) + optimize_pair GAS_swap GAS_swap = Just $ GAS_id + optimize_pair GAS_swap GAS_cancell = Just $ GAS_cancelr + optimize_pair GAS_swap GAS_cancelr = Just $ GAS_cancell + optimize_pair GAS_assoc GAS_cancell = Just $ GAS_first GAS_cancell + optimize_pair GAS_unassoc GAS_cancelr = Just $ GAS_second GAS_cancelr + optimize_pair GAS_assoc (GAS_second GAS_cancell) = Just $ GAS_first GAS_cancelr + optimize_pair GAS_unassoc (GAS_first GAS_cancell) = Just $ GAS_cancell +-} + +optpair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z) + +optpair (GASY_atomicl g) (GASY_X GASX_cancelr) = Just $ GASL_Y g +optpair (GASY_atomicr g) (GASY_X GASX_cancell) = Just $ GASL_Y g + +optpair (GASY_X GASX_uncancell) (GASY_X GASX_cancell) = Just $ GASL_id +optpair (GASY_X GASX_uncancelr) (GASY_X GASX_cancelr) = Just $ GASL_id +optpair (GASY_X GASX_cancell) (GASY_X GASX_uncancell) = Just $ GASL_id +optpair (GASY_X GASX_cancelr) (GASY_X GASX_uncancelr) = Just $ GASL_id +optpair (GASY_X GASX_uncancelr) (GASY_X GASX_cancell) = Just $ GASL_id +optpair (GASY_X GASX_uncancell) (GASY_X GASX_cancelr) = Just $ GASL_id +optpair (GASY_X GASX_assoc) (GASY_X GASX_cancell) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_cancell +optpair (GASY_X GASX_unassoc) (GASY_X GASX_cancelr) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_cancelr +optpair (GASY_second (GASY_X GASX_uncancelr)) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_X GASX_uncancelr +optpair (GASY_first (GASY_X GASX_uncancell)) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_X GASX_uncancell +optpair (GASY_X GASX_uncancell) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_uncancell +optpair (GASY_X GASX_uncancelr) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancelr +optpair (GASY_first (GASY_X GASX_uncancelr)) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancell +optpair (GASY_second (GASY_X GASX_uncancell)) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_uncancelr +optpair (GASY_X GASX_assoc) (GASY_second (GASY_X GASX_cancelr)) = Just $ GASL_Y $ GASY_X $ GASX_cancelr +optpair (GASY_X GASX_unassoc) (GASY_first (GASY_X GASX_cancell)) = Just $ GASL_Y $ GASY_X $ GASX_cancell +optpair (GASY_first g) (GASY_X GASX_cancelr) = Just $ GASL_comp (GASY_X GASX_cancelr) $ GASL_Y $ g +optpair (GASY_second g) (GASY_X GASX_cancell) = Just $ GASL_comp (GASY_X GASX_cancell) $ GASL_Y $ g +optpair (GASY_X GASX_uncancelr) (GASY_first g) = Just $ GASL_comp g $ GASL_Y (GASY_X GASX_uncancelr) +optpair (GASY_X GASX_uncancell) (GASY_second g) = Just $ GASL_comp g $ GASL_Y (GASY_X GASX_uncancell) + +-- swap with an {un}cancel{l,r} before/after it +optpair (GASY_X GASX_uncancell) (GASY_X GASX_swap ) = Just $ GASL_Y $ GASY_X $ GASX_uncancelr +optpair (GASY_X GASX_uncancelr) (GASY_X GASX_swap ) = Just $ GASL_Y $ GASY_X $ GASX_uncancell +optpair (GASY_X GASX_swap) (GASY_X GASX_cancell) = Just $ GASL_Y $ GASY_X $ GASX_cancelr +optpair (GASY_X GASX_swap) (GASY_X GASX_cancelr) = Just $ GASL_Y $ GASY_X $ GASX_cancell + +{- +optpair (GASY_X GASX_uncancelr) (GASY_X (GASX_loopl gl)) = + Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ GASY_X GASX_uncancelr) gl) +optpair (GASY_X GASX_uncancell) (GASY_X (GASX_loopl gl)) = + Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ GASY_X GASX_uncancell) gl) +optpair (GASY_X GASX_uncancelr) (GASY_X (GASX_loopr gl)) = + Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ GASY_X GASX_uncancelr) gl) +optpair (GASY_X GASX_uncancell) (GASY_X (GASX_loopr gl)) = + Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ GASY_X GASX_uncancell) gl) +-} +optpair q (GASY_X (GASX_loopl gl)) | pushin q = Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ q) gl) +optpair q (GASY_X (GASX_loopr gl)) | pushin q = Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ q) gl) + +optpair a@(GASY_X GASX_uncancell) (GASY_first b@(GASY_X (GASX_const c))) = Just $ GASL_Y $ GASY_atomicl b +optpair a@(GASY_X GASX_uncancelr) (GASY_second b@(GASY_X (GASX_const c))) = Just $ GASL_Y $ GASY_atomicr b + +optpair (GASY_first gy1) (GASY_second gy2) | pushleft gy2, not (pushleft gy1) + = Just $ GASL_comp (GASY_second gy2) $ GASL_Y $ GASY_first gy1 +optpair (GASY_second gy1) (GASY_first gy2) | pushleft gy2, not (pushleft gy1) + = Just $ GASL_comp (GASY_first gy2) $ GASL_Y $ GASY_second gy1 + +optpair (GASY_first gy1) (GASY_first gy2) = liftM gasl_firstify $ optpair gy1 gy2 +optpair (GASY_second gy1) (GASY_second gy2) = liftM gasl_secondify $ optpair gy1 gy2 +optpair _ _ = Nothing + +swappair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z) + +swappair q (GASY_atomicl g) = Just $ GASL_comp (GASY_atomicl g) $ GASL_Y $ GASY_second q +swappair q (GASY_atomicr g) = Just $ GASL_comp (GASY_atomicr g) $ GASL_Y $ GASY_first q + +swappair (GASY_first gy1) (GASY_second gy2) = Just $ GASL_comp (GASY_second gy2) (GASL_Y $ GASY_first gy1) +swappair (GASY_second gy1) (GASY_first gy2) = Just $ GASL_comp (GASY_first gy2) (GASL_Y $ GASY_second gy1) +swappair (GASY_first gy1) (GASY_X GASX_unassoc) = Just $ GASL_comp(GASY_X GASX_unassoc) (GASL_Y $ GASY_first (GASY_first gy1)) +swappair (GASY_second gy1) (GASY_X GASX_assoc ) = Just $ GASL_comp(GASY_X GASX_assoc ) (GASL_Y $ GASY_second (GASY_second gy1)) +swappair (GASY_X GASX_uncancelr) (GASY_first gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancelr) +swappair (GASY_X GASX_uncancell) (GASY_second gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancell) +swappair (GASY_first (GASY_second gy)) (GASY_X GASX_assoc ) = Just $ GASL_comp (GASY_X GASX_assoc ) $ GASL_Y (GASY_second (GASY_first gy)) +swappair (GASY_second (GASY_first gy)) (GASY_X GASX_unassoc ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_first (GASY_second gy)) +swappair (GASY_second (GASY_second gy)) (GASY_X GASX_unassoc ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_second gy) +swappair (GASY_first (GASY_first gy)) (GASY_X GASX_assoc ) = Just $ GASL_comp (GASY_X GASX_assoc) $ GASL_Y (GASY_first gy) +swappair (GASY_first gy) (GASY_X GASX_swap ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_second gy) +swappair (GASY_second gy) (GASY_X GASX_swap ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_first gy) +swappair gy (GASY_X (GASX_loopl gl)) = Just $ GASL_Y $ GASY_X $ GASX_loopl $ GASL_comp (GASY_second gy) gl +swappair gy (GASY_X (GASX_loopr gl)) = Just $ GASL_Y $ GASY_X $ GASX_loopr $ GASL_comp (GASY_first gy) gl + +swappair (GASY_first gy1) (GASY_first gy2) = liftM gasl_firstify $ swappair gy1 gy2 +swappair (GASY_second gy1) (GASY_second gy2) = liftM gasl_secondify $ swappair gy1 gy2 +swappair _ _ = Nothing + +-- pushright can only return True for central morphisms +pushright :: GArrowSkeletonY m x y -> Bool +pushright (GASY_first gy) = pushright gy +pushright (GASY_second gy) = pushright gy +pushright (GASY_atomicl _) = False +pushright (GASY_atomicr _) = False +pushright (GASY_X GASX_uncancell) = True +pushright (GASY_X GASX_uncancelr) = True +pushright (GASY_X _ ) = False + +-- says if we should push it into a loopl/r +pushin :: GArrowSkeletonY m x y -> Bool +pushin gy = pushright gy || pushin' gy + where + pushin' :: GArrowSkeletonY m a b -> Bool + pushin' (GASY_first gy) = pushin' gy + pushin' (GASY_second gy) = pushin' gy + pushin' (GASY_atomicl _) = False + pushin' (GASY_atomicr _) = False + + -- not sure if these are a good idea + pushin' (GASY_X GASX_copy) = True + pushin' (GASY_X GASX_swap) = True + + pushin' (GASY_X _ ) = False + +optimizey :: GArrowSkeletonY m x y -> GArrowSkeletonY m x y +optimizey (GASY_X gx) = GASY_X $ optimizex gx +optimizey (GASY_first gy) = GASY_first (optimizey gy) +optimizey (GASY_second gy) = GASY_second (optimizey gy) +optimizey (GASY_atomicl gy) = GASY_atomicl $ optimizey gy +optimizey (GASY_atomicr gy) = GASY_atomicr $ optimizey gy +optimizex :: GArrowSkeletonX m x y -> GArrowSkeletonX m x y +optimizex (GASX_const k) = GASX_const k +optimizex (GASX_cancell) = GASX_cancell +optimizex (GASX_cancelr) = GASX_cancelr +optimizex (GASX_uncancell) = GASX_uncancell +optimizex (GASX_uncancelr) = GASX_uncancelr +optimizex (GASX_assoc) = GASX_assoc +optimizex (GASX_unassoc) = GASX_unassoc +optimizex (GASX_drop) = GASX_drop +optimizex (GASX_copy) = GASX_copy +optimizex (GASX_swap) = GASX_swap +optimizex (GASX_merge) = GASX_merge +optimizex (GASX_misc m) = GASX_misc m +optimizex (GASX_loopl (GASL_comp (GASY_first gy) gl))| pushleft gy = GASX_loopl $ gaslcat gl (GASL_Y $ GASY_first gy) +optimizex (GASX_loopr (GASL_comp (GASY_second gy) gl))| pushleft gy = GASX_loopr $ gaslcat gl (GASL_Y $ GASY_second gy) +optimizex (GASX_loopl gl) = GASX_loopl $ optimizel gl +optimizex (GASX_loopr gl) = GASX_loopr $ optimizel gl +pushleft :: GArrowSkeletonY m x y -> Bool +pushleft (GASY_first gy) = pushleft gy +pushleft (GASY_second gy) = pushleft gy +pushleft (GASY_atomicl _) = False +pushleft (GASY_atomicr _) = False +pushleft (GASY_X GASX_cancell) = True +pushleft (GASY_X GASX_cancelr) = True +pushleft (GASY_X _ ) = False