X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=examples%2FGArrowSkeleton.hs;h=963eb45b4246a8460d1d4a627bf982b3b336ff93;hp=16898068a26e01d7e59d9989d0dc5f822090b4c5;hb=ec996e8cb550676d89d187061db7d018af9ec88d;hpb=e8c9ed9dc1c5b6d107a6dd6b2a04e82052818be3

diff --git a/examples/GArrowSkeleton.hs b/examples/GArrowSkeleton.hs
index 1689806..963eb45 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,16 +18,19 @@
 -- 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)
 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
@@ -81,7 +84,10 @@ 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
 
 --
 -- | Simple structural equality on skeletons.  NOTE: two skeletons
@@ -110,8 +116,25 @@ instance Eq ((GArrowSkeleton m) a b)
     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 +142,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'
@@ -279,6 +302,8 @@ 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
@@ -307,6 +332,8 @@ 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
@@ -355,6 +382,10 @@ optimizel (GASL_comp gy gl)
 -}
 
 optpair :: GArrowSkeletonY m x y -> GArrowSkeletonY m y z -> Maybe (GArrowSkeletonL m x z)
+
+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
@@ -369,14 +400,19 @@ optpair (GASY_X GASX_uncancell) (GASY_X GASX_unassoc ) = Just $ GASL_Y $ GASY_fi
 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_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_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)
@@ -387,15 +423,26 @@ optpair (GASY_X GASX_uncancelr) (GASY_X (GASX_loopr 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)) | pushright q =
-    Just $ GASL_Y $ (GASY_X $ GASX_loopl $ GASL_comp (GASY_second $ q) gl)
-optpair q (GASY_X (GASX_loopr gl)) | pushright q =
-    Just $ GASL_Y $ (GASY_X $ GASX_loopr $ GASL_comp (GASY_first $ q) 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 a@(GASY_X GASX_uncancell) (GASY_first  b@(GASY_X (GASX_const c))) = Just $ GASL_Y $ GASY_atomicl b
+optpair a@(GASY_X GASX_uncancelr) (GASY_second b@(GASY_X (GASX_const c))) = Just $ GASL_Y $ GASY_atomicr b
+
+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
+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))
@@ -410,6 +457,7 @@ swappair (GASY_first  gy) (GASY_X GASX_swap    ) = Just $ GASL_comp (GASY_X GASX
 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
@@ -418,14 +466,34 @@ swappair _ _                                 = Nothing
 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
@@ -448,6 +516,8 @@ 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