X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=examples%2FGArrowSkeleton.hs;h=2c53283659d75de50853c90fa6218740dd0e5fe6;hp=c07c64ab20583c8dc40aac3bd9d10c36a0b06346;hb=a663de9a349ffe83a6c4fc10f1259f2fa6a915ed;hpb=cb76623a15c668453a369b06698c6896ba3075ee diff --git a/examples/GArrowSkeleton.hs b/examples/GArrowSkeleton.hs index c07c64a..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' @@ -181,6 +185,8 @@ optimize x = let x' = optimize' x in if x == x' then x' else optimize x' 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)