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

diff --git a/examples/GArrowSkeleton.hs b/examples/GArrowSkeleton.hs
index dd7937b..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