X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=examples%2FGArrowSkeleton.hs;h=a71486f32e2a9bea00481e832e61567ffff58726;hp=8775d4af31bdff04d5dbf43f7a6a2cb2a96038bf;hb=c700f5a65d664d4c0a3e76d33aa3769266bf330c;hpb=542be54b8968c631f0c397272cf05871ccef425b diff --git a/examples/GArrowSkeleton.hs b/examples/GArrowSkeleton.hs index 8775d4a..a71486f 100644 --- a/examples/GArrowSkeleton.hs +++ b/examples/GArrowSkeleton.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, TypeFamilies #-} +{-# LANGUAGE MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, TypeFamilies, RankNTypes #-} ----------------------------------------------------------------------------- -- | -- Module : GArrowSkeleton @@ -18,20 +18,22 @@ -- behavior below -- you'd get (GAS_comp f GAS_id) instead of f. In -- practice this means that the user must be prepared for the skeleton -- TikZ diagram to be a nondeterministically-chosen boxes-and-wires --- diagram which ks *equivalent to* the term, rather than structurally +-- diagram which is *equivalent to* the term, rather than structurally -- exactly equal to it. -- -module GArrowSkeleton (GArrowSkeleton(..), optimize, beautify) +-- A normal form theorem and normalization algorithm are being prepared. +-- +module GArrowSkeleton (GArrowSkeleton(..), mkSkeleton, OptimizeFlag(..), optimize, beautify, skelify) where import Prelude hiding ( id, (.), lookup, repeat ) import Control.Category -import GHC.HetMet.GArrow +import Control.GArrow import Unify import Control.Monad.State +import GArrowInclusion data GArrowSkeleton m :: * -> * -> * where - GAS_const :: Int -> GArrowSkeleton m () Int GAS_id :: GArrowSkeleton m x x GAS_comp :: GArrowSkeleton m x y -> GArrowSkeleton m y z -> GArrowSkeleton m x z GAS_first :: GArrowSkeleton m x y -> GArrowSkeleton m (x,z) (y,z) @@ -45,7 +47,6 @@ data GArrowSkeleton m :: * -> * -> * GAS_drop :: GArrowSkeleton m x () 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 (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 @@ -81,7 +82,13 @@ type instance GArrowTensor (GArrowSkeleton m) = (,) type instance GArrowUnit (GArrowSkeleton m) = () type instance GArrowExponent (GArrowSkeleton m) = (->) -instance GArrowSTKCL (GArrowSkeleton m) +instance GArrowCopyDropSwapLoop (GArrowSkeleton m) + +instance GArrowInclusion (GArrowSkeleton m) (,) () m where + ga_inc = GAS_misc + +skelify :: (forall g . (GArrowCopyDropSwapLoop g, GArrowInclusion g (,) () m) => g x y) -> GArrowSkeleton m x y +skelify = \g -> g -- -- | Simple structural equality on skeletons. NOTE: two skeletons @@ -102,16 +109,31 @@ instance Eq ((GArrowSkeleton m) a b) GAS_uncancell === GAS_uncancell = True GAS_uncancelr === GAS_uncancelr = True GAS_drop === GAS_drop = True - (GAS_const i) === (GAS_const i') = i==i' GAS_copy === GAS_copy = True - GAS_merge === GAS_merge = True GAS_swap === GAS_swap = True GAS_assoc === GAS_assoc = True GAS_unassoc === GAS_unassoc = True (GAS_loopl f) === (GAS_loopl f') = f === f' (GAS_loopr f) === (GAS_loopr f') = f === f' + (GAS_misc _) === (GAS_misc _) = True -- FIXME _ === _ = False - -- FIXME: GAS_misc's are never equal!!! + +data OptimizeFlag = DoOptimize | NoOptimize + +mkSkeleton :: OptimizeFlag -> + (forall g . + (GArrow g (,) () + ,GArrowCopy g (,) () + ,GArrowDrop g (,) () + ,GArrowSwap g (,) () + ,GArrowLoop g (,) () + ,GArrowInclusion g (,) () m) => + g x y) + -> GArrowSkeleton m x y +mkSkeleton DoOptimize = \g -> (beautify . optimize) g +mkSkeleton NoOptimize = \g -> g + + -- -- | Performs some very simple-minded optimizations on a @@ -119,7 +141,7 @@ 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 . gas2gasl) +optimize = repeat (gasl2gas . optimizel . {- FIXME -} optimizel . gas2gasl) {- optimize x = let x' = optimize' x in if x == x' then x' else optimize x' @@ -206,15 +228,17 @@ repeat f x = let x' = f x in -- | 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 = optimize . (repeat beautify') +beautify = repeat beautify' where beautify' :: (GArrowSkeleton m) a b -> (GArrowSkeleton m) a b - beautify' (GAS_comp (GAS_comp f g) h) = GAS_comp f $ GAS_comp g h - beautify' (GAS_comp f (GAS_comp (GAS_comp g h) k)) = GAS_comp f $ GAS_comp g $ GAS_comp h k + 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') @@ -229,7 +253,6 @@ beautify = optimize . (repeat beautify') 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 @@ -243,7 +266,6 @@ 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 @@ -277,10 +299,11 @@ data GArrowSkeletonY m :: * -> * -> * 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) @@ -290,7 +313,6 @@ data GArrowSkeletonX m :: * -> * -> * 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 @@ -305,9 +327,10 @@ 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 @@ -317,7 +340,6 @@ 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 @@ -325,12 +347,14 @@ gasx2gas (GASX_loopr gl) = GAS_loopr $ gasl2gas gl optimizel :: GArrowSkeletonL m x y -> GArrowSkeletonL m x y +--optimizel (GASL_comp (GASL_Y (GASY_X GAS_uncancelr)) (GASL_Y (GASY_X GASX_copy))) = +-- (GASL_comp (GASL_Y (GASY_X GAS_uncancelr)) (GASL_Y (GASY_X GASX_copy))) optimizel (GASL_id ) = GASL_id optimizel (GASL_Y gy ) = GASL_Y $ optimizey gy -optimizel (GASL_comp gy (GASL_comp gy' gl)) | pushright gy, not (pushright gy'), Just x <- pushpair gy gy' = optimizel $ gaslcat x gl -optimizel (GASL_comp gy (GASL_Y gy')) | pushright gy, not (pushright gy'), Just x <- pushpair gy gy' = GASL_comp (optimizey gy) (GASL_Y 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' = GASL_comp (optimizey gy) (GASL_Y gy') +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 @@ -353,56 +377,117 @@ optimizel (GASL_comp gy gl) -} optpair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z) -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 (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 _ _ = Nothing - -pushpair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z) -pushpair (GASY_first gy1) (GASY_first gy2) = liftM gasl_firstify $ pushpair gy1 gy2 -pushpair (GASY_second gy1) (GASY_second gy2) = liftM gasl_secondify $ pushpair gy1 gy2 -pushpair (GASY_first gy1) (GASY_second gy2) = Just $ GASL_comp (GASY_second gy2) (GASL_Y $ GASY_first gy1) -pushpair (GASY_second gy1) (GASY_first gy2) = Just $ GASL_comp (GASY_first gy2) (GASL_Y $ GASY_second gy1) -pushpair (GASY_first gy1) (GASY_X GASX_unassoc) = Just $ GASL_comp(GASY_X GASX_unassoc) (GASL_Y $ GASY_first (GASY_first gy1)) -pushpair (GASY_second gy1) (GASY_X GASX_assoc ) = Just $ GASL_comp(GASY_X GASX_assoc ) (GASL_Y $ GASY_second (GASY_second gy1)) -pushpair (GASY_second (GASY_X GASX_uncancelr)) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_X GASX_uncancelr -pushpair (GASY_first (GASY_X GASX_uncancell)) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_X GASX_uncancell -pushpair (GASY_X GASX_uncancelr) (GASY_first gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancelr) -pushpair (GASY_X GASX_uncancell) (GASY_second gy) = Just $ GASL_comp gy (GASL_Y $ GASY_X $ GASX_uncancell) -pushpair (GASY_first (GASY_second gy)) (GASY_X GASX_assoc ) = Just $ GASL_comp (GASY_X GASX_assoc ) $ GASL_Y (GASY_second (GASY_first gy)) -pushpair (GASY_second (GASY_first gy)) (GASY_X GASX_unassoc ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_first (GASY_second gy)) -pushpair (GASY_second (GASY_second gy)) (GASY_X GASX_unassoc ) = Just $ GASL_comp (GASY_X GASX_unassoc) $ GASL_Y (GASY_second gy) -pushpair (GASY_first (GASY_first gy)) (GASY_X GASX_assoc ) = Just $ GASL_comp (GASY_X GASX_assoc) $ GASL_Y (GASY_first gy) -pushpair (GASY_X GASX_uncancell) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_uncancell -pushpair (GASY_X GASX_uncancelr) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancelr -pushpair (GASY_first (GASY_X GASX_uncancelr)) (GASY_X GASX_assoc ) = Just $ GASL_Y $ GASY_second $ GASY_X GASX_uncancell -pushpair (GASY_second (GASY_X GASX_uncancell)) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_first $ GASY_X GASX_uncancelr -pushpair (GASY_first gy) (GASY_X GASX_swap ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_second gy) -pushpair (GASY_second gy) (GASY_X GASX_swap ) = Just $ GASL_comp (GASY_X GASX_swap) $ GASL_Y (GASY_first gy) -pushpair (GASY_X GASX_uncancell) (GASY_X GASX_swap ) = Just $ GASL_Y $ GASY_X $ GASX_uncancelr -pushpair (GASY_X GASX_uncancelr) (GASY_X GASX_swap ) = Just $ GASL_Y $ GASY_X $ GASX_uncancell -pushpair _ _ = Nothing +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 (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 @@ -412,7 +497,17 @@ 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