X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=examples%2FGArrowSkeleton.hs;h=2c53283659d75de50853c90fa6218740dd0e5fe6;hp=a64ed313873070c19336ad68f9b852e0791462e2;hb=a3592b805c570883fd63a5c75d6e16ea83f2e849;hpb=059b3febe62ca2735c22c57a051c86093b8f818e

diff --git a/examples/GArrowSkeleton.hs b/examples/GArrowSkeleton.hs
index a64ed31..2c53283 100644
--- a/examples/GArrowSkeleton.hs
+++ b/examples/GArrowSkeleton.hs
@@ -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
@@ -127,6 +127,10 @@ optimize x = let x' = optimize' x in if x == x' then x' else optimize x'
   -- 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    (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))
+
   optimize' (GAS_comp    (GAS_comp f g) h) = case optimize_pair g h of
                                                Nothing   -> GAS_comp (optimize' (GAS_comp f g)) h'
                                                Just ret' -> GAS_comp f' ret'
@@ -168,16 +172,25 @@ optimize x = let x' = optimize' x in if x == x' then x' else optimize x'
   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
 
-  -- second priority: push GAS_swap leftward... why isn't this working?
+  -- second priority: push GAS_swap leftward
   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_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
+  optimize_pair GAS_unassoc (GAS_first  GAS_cancell)  = Just $ GAS_cancell
+
+
+  -- FIXME: valid only for central morphisms
+  --optimize_pair (GAS_second f) (GAS_first g) = Just $ GAS_comp (GAS_first g) (GAS_second f)
+  optimize_pair (GAS_first g) (GAS_second f) = Just $ GAS_comp  (GAS_second f) (GAS_first g)
 
   optimize_pair _ _                           = Nothing