X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=examples%2FGArrowSkeleton.hs;fp=examples%2FGArrowSkeleton.hs;h=a71486f32e2a9bea00481e832e61567ffff58726;hp=b320336778fe753f10e70eee3bdfa71cf424fc21;hb=c700f5a65d664d4c0a3e76d33aa3769266bf330c;hpb=9238cdac094f9be01ee8978ddb18b6404a6d9ade

diff --git a/examples/GArrowSkeleton.hs b/examples/GArrowSkeleton.hs
index b320336..a71486f 100644
--- a/examples/GArrowSkeleton.hs
+++ b/examples/GArrowSkeleton.hs
@@ -23,7 +23,7 @@
 --
 -- A normal form theorem and normalization algorithm are being prepared.
 --
-module GArrowSkeleton (GArrowSkeleton(..), mkSkeleton, OptimizeFlag(..), optimize, beautify)
+module GArrowSkeleton (GArrowSkeleton(..), mkSkeleton, OptimizeFlag(..), optimize, beautify, skelify)
 where
 import Prelude hiding ( id, (.), lookup, repeat )
 import Control.Category
@@ -87,6 +87,9 @@ 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
 --   with the same shape but different types will nonetheless be "equal";
@@ -344,6 +347,8 @@ 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)) | Just x <- optpair gy gy'                                     = optimizel $ gaslcat x gl