X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=GHC%2FHetMet%2FCodeTypes.hs;h=d6291195753ccad07178b4d4e5295b82d46db2c7;hb=11dca0057d71161c2b93af91f7921a648e6d9558;hp=cf0dc12a23b7e2644230dd88d30c1c9a6c2fc408;hpb=c8af1c7edf31a45aa6f71620a5408cfacb8d52c6;p=ghc-base.git

diff --git a/GHC/HetMet/CodeTypes.hs b/GHC/HetMet/CodeTypes.hs
index cf0dc12..d629119 100644
--- a/GHC/HetMet/CodeTypes.hs
+++ b/GHC/HetMet/CodeTypes.hs
@@ -1,8 +1,12 @@
-{-# OPTIONS -XModalTypes -XMultiParamTypeClasses #-}
+{-# OPTIONS -XModalTypes -XMultiParamTypeClasses -XKindSignatures -XFlexibleContexts #-}
 module GHC.HetMet.CodeTypes (
   hetmet_brak,
   hetmet_esc,
   hetmet_csp,
+  hetmet_flatten,
+  pga_flatten,
+  pga_unflatten,
+  pga_flattened_id,
   GuestIntegerLiteral, guestIntegerLiteral,
   GuestStringLiteral, guestStringLiteral,
   GuestCharLiteral, guestCharLiteral,
@@ -14,45 +18,65 @@ 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 :: forall (c :: * -> * -> *). forall a. a -> <[a]>@c
 hetmet_brak = Prelude.error "hetmet_brak should never be evaluated; did you forget to compile with -fcoqpass?"
 
-hetmet_esc  :: forall c. forall a. <[a]>@c -> a
+hetmet_esc  :: forall (c :: * -> * -> *). forall a. <[a]>@c -> a
 hetmet_esc = Prelude.error "hetmet_esc should never be evaluated; did you forget to compile with -fcoqpass?"
 
-hetmet_csp :: forall c. forall a. a -> a
+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_unflatten ::
+   forall g x y.
+     PGArrow g x y ->
+     <[ x -> y ]>@g
+pga_unflatten = 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.
+
+-- Technically these functions ought to be invoked *during
+-- compilation*; in the future I would like to use Template Haskell to
+-- do that.
 class GuestIntegerLiteral c where
   guestIntegerLiteral :: Integer -> <[ Integer ]>@c
-
 class GuestStringLiteral c where
   guestStringLiteral :: String -> <[ String ]>@c
-
 class GuestCharLiteral c where
   guestCharLiteral :: Char -> <[ Char ]>@c
 
+
+class GuestLanguageConstant c t where
+  guestLanguageConstant :: t -> <[ t ]>@c
+
 -- Note that stringwise-identical identifiers at different syntactic
 -- depths are different identifiers; for this reason the operators
 -- below can have a different type at syntactical depth 1 than at