X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=examples%2FGArrowSkeleton.hs;h=c07c64ab20583c8dc40aac3bd9d10c36a0b06346;hp=a64ed313873070c19336ad68f9b852e0791462e2;hb=2444f0cbf7ed5c744c43dbca114a4f400cd1522f;hpb=059b3febe62ca2735c22c57a051c86093b8f818e diff --git a/examples/GArrowSkeleton.hs b/examples/GArrowSkeleton.hs index a64ed31..c07c64a 100644 --- a/examples/GArrowSkeleton.hs +++ b/examples/GArrowSkeleton.hs @@ -168,16 +168,23 @@ 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 + + -- 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