add support for hetmet_flatten casting variable

diff --git a/GHC/HetMet/CodeTypes.hs b/GHC/HetMet/CodeTypes.hs
index 31daddb..424551b 100644 (file)
--- a/GHC/HetMet/CodeTypes.hs
+++ b/GHC/HetMet/CodeTypes.hs
@@ -1,8 +1,11 @@
-{-# OPTIONS -XModalTypes -XMultiParamTypeClasses -XKindSignatures #-}
+{-# OPTIONS -XModalTypes -XMultiParamTypeClasses -XKindSignatures -XFlexibleContexts #-}
 module GHC.HetMet.CodeTypes (
   hetmet_brak,
   hetmet_esc,
   hetmet_csp,
+  hetmet_flatten,
+  pga_flatten,
+  pga_flattened_id,
   GuestIntegerLiteral, guestIntegerLiteral,
   GuestStringLiteral, guestStringLiteral,
   GuestCharLiteral, guestCharLiteral,
@@ -14,6 +17,7 @@ module GHC.HetMet.CodeTypes (
 ) where
 import Prelude (Integer, String, Char, Bool, error)
 import GHC.HetMet.GArrow
+import GHC.HetMet.Private
 
 hetmet_brak :: forall (c :: * -> * -> *). forall a. a -> <[a]>@c
 hetmet_brak = Prelude.error "hetmet_brak should never be evaluated; did you forget to compile with -fcoqpass?"
@@ -24,25 +28,31 @@ hetmet_esc = Prelude.error "hetmet_esc should never be evaluated; did you forget
 hetmet_csp :: forall (c :: * -> * -> *). forall a. a -> a
 hetmet_csp = Prelude.error "hetmet_csp should never be evaluated; did you forget to compile with -fcoqpass?"
 
-{-
--- After the flattening pass the argument and result types of this
--- function are identical (for any instantiation), so the flattener
--- simply turns it into the identity function.  Its only purpose is to
--- act as a "safe type cast" during pre-flattening
--- type-inference/checking:
 hetmet_flatten ::
-   forall g.
-    GArrow     g (**) =>
-    GArrowDrop g (**) =>
-    GArrowCopy g (**) =>
-    GArrowSwap g (**) =>
-    GArrowLoop g (**) =>
+   forall g .
+    GArrowSTKC g (,) () =>
       forall x y.
          <[ x -> y ]>@g
          ->
          (g x y)
-hetmet_flatten _ = Prelude.error "hetmet_flatten should never be evaluated; did you forget to compile with -fcoqpass?"
--}
+hetmet_flatten x = unG (pga_flatten x)
+
+-- After the flattening pass the argument and result types of this
+-- function are identical (for any instantiation), so the flattener
+-- simply turns it into the identity function (pga_flattened_id).
+-- Its only purpose is to act as a "safe type cast" during pre-flattening
+-- type-inference/checking:
+pga_flatten ::
+   forall g x y.
+     <[ x -> y ]>@g ->
+     PGArrow g x y
+pga_flatten = error "hetmet_flatten should never be evaluated; did you forget to compile with -fcoqpass?"
+
+pga_flattened_id ::
+   forall g x y.
+     PGArrow g x y ->
+     PGArrow g x y
+pga_flattened_id x = x
 
 
 -- FIXME: move these and the three above to "prim" or something like that.

diff --git a/GHC/HetMet/Private.hs b/GHC/HetMet/Private.hs
index c27f78b..68861a0 100644 (file)
--- a/GHC/HetMet/Private.hs
+++ b/GHC/HetMet/Private.hs
@@ -10,7 +10,7 @@
 -- Portability :  portable
 
 module GHC.HetMet.Private (
-  PGArrow,
+  PGArrow (unG),
   pga_id,
   pga_comp,
   pga_first,
@@ -27,7 +27,8 @@ module GHC.HetMet.Private (
   pga_applyl,
   pga_applyr,
   pga_curryl,
-  pga_curryr
+  pga_curryr,
+  pga_kappa
 ) where
 import Control.Category ( (>>>) )
 import qualified Control.Category
@@ -72,5 +73,5 @@ pga_curryl    :: forall g x y z . PGArrow g (x,y) z  ->  PGArrow g x (y->z)
 pga_curryl    =  error "not implemented"
 pga_curryr    :: forall g x y z . PGArrow g (x,y) z  ->  PGArrow g y (x->z)
 pga_curryr    =  error "not implemented"
---pga_kappa     :: forall g x y . (g u x -> g u y) -> g x y
---pga_kappa     =  error "not implemented"
+pga_kappa     :: forall g x y . (g () x -> g () y) -> g x y
+pga_kappa     =  error "not implemented"