swap <[]> and <{}> syntax

diff --git a/GHC/HetMet/CodeTypes.hs b/GHC/HetMet/CodeTypes.hs
index 18d8579..1d7357d 100644 (file)
--- a/GHC/HetMet/CodeTypes.hs
+++ b/GHC/HetMet/CodeTypes.hs
@@ -17,10 +17,10 @@ module GHC.HetMet.CodeTypes (
   GuestCharLiteral, guestCharLiteral
 ) where
 
-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
@@ -30,8 +30,8 @@ hetmet_csp = Prelude.error "hetmet_csp should never be evaluated; did you forget
 -- compilation*; in the future I would like to use Template Haskell to
 -- do that.
 class GuestIntegerLiteral c where
-  guestIntegerLiteral :: Integer -> <[ Integer ]>@c
+  guestIntegerLiteral :: Integer -> <{ Integer }>@c
 class GuestStringLiteral c where
-  guestStringLiteral :: String -> <[ String ]>@c
+  guestStringLiteral :: String -> <{ String }>@c
 class GuestCharLiteral c where
-  guestCharLiteral :: Char -> <[ Char ]>@c
+  guestCharLiteral :: Char -> <{ Char }>@c

diff --git a/GHC/HetMet/GuestLanguage.hs b/GHC/HetMet/GuestLanguage.hs
index 43a391e..8d9be47 100644 (file)
--- a/GHC/HetMet/GuestLanguage.hs
+++ b/GHC/HetMet/GuestLanguage.hs
@@ -10,11 +10,11 @@
 -- Portability :  portable
 
 module GHC.HetMet.GuestLanguage (
-  GuestLanguageMult, <[ (*) ]>,
-  GuestLanguageAdd,  <[ (+) ]>,
-  GuestLanguageSub,  <[ (-) ]>, <[ negate ]>,
-  GuestLanguageFromInteger, <[ fromInteger ]>,
-  GuestLanguageBool, <[ (||) ]>, <[ (&&) ]>, <[ true ]>, <[ false ]>, <[ ifThenElse ]>,
+  GuestLanguageMult, <{ (*) }>,
+  GuestLanguageAdd,  <{ (+) }>,
+  GuestLanguageSub,  <{ (-) }>, <{ negate }>,
+  GuestLanguageFromInteger, <{ fromInteger }>,
+  GuestLanguageBool, <{ (||) }>, <{ (&&) }>, <{ true }>, <{ false }>, <{ ifThenElse }>,
   GuestIntegerLiteral, guestIntegerLiteral,
   GuestStringLiteral, guestStringLiteral,
   GuestCharLiteral, guestCharLiteral
@@ -29,24 +29,24 @@ import GHC.HetMet.CodeTypes
 -- syntactical depth 0.
 
 class GuestLanguageMult c t where
-  <[ (*)    ]> :: <[ t -> t -> t ]>@c
+  <{ (*)    }> :: <{ t -> t -> t }>@c
 
 class GuestLanguageAdd c t where
-  <[ (+)    ]> :: <[ t -> t -> t ]>@c
+  <{ (+)    }> :: <{ t -> t -> t }>@c
 
 class GuestLanguageSub c t where
-  <[ (-)    ]> :: <[ t -> t -> t ]>@c
-  <[ negate ]> :: <[ t -> t      ]>@c   -- used for unary (-)
+  <{ (-)    }> :: <{ t -> t -> t }>@c
+  <{ negate }> :: <{ t -> t      }>@c   -- used for unary (-)
 
 class GuestLanguageFromInteger c t where
-  <[ fromInteger ]> :: <[ Integer -> t ]>@c
+  <{ fromInteger }> :: <{ Integer -> t }>@c
 
 class GuestLanguageBool c where
-  <[ (||) ]>       :: <[ Bool -> Bool -> Bool ]>@c
-  <[ (&&) ]>       :: <[ Bool -> Bool -> Bool ]>@c
-  <[ true ]>       :: <[ Bool ]>@c
-  <[ false ]>      :: <[ Bool ]>@c
-  <[ ifThenElse ]> :: <[ Bool -> t -> t -> t ]>@c
+  <{ (||) }>       :: <{ Bool -> Bool -> Bool }>@c
+  <{ (&&) }>       :: <{ Bool -> Bool -> Bool }>@c
+  <{ true }>       :: <{ Bool }>@c
+  <{ false }>      :: <{ Bool }>@c
+  <{ ifThenElse }> :: <{ Bool -> t -> t -> t }>@c
 
 -- For heterogeneous metaprogramming, the meaning of "running" a
 -- program is fairly ambiguous, and moreover is highly sensitive to
@@ -54,13 +54,13 @@ class GuestLanguageBool c where
 -- dealing with.  For example, in homogeneous metaprogramming, "run"
 -- has this type:
 --
---  ga_run :: forall a. (forall c. <[a]>@c) -> a
+--  ga_run :: forall a. (forall c. <{a}>@c) -> a
 --
 -- However, an expression which uses, say (*) at level 1 will never
 -- be able to be passed to this expression, since
 --
---   square :: forall c t. GuestLanguageMult ct => <[t]>@c -> <[t]>@c
---   square x = <[ ~~x * ~~x ]>
+--   square :: forall c t. GuestLanguageMult ct => <{t}>@c -> <{t}>@c
+--   square x = <{ ~~x * ~~x }>
 --
 
 -- So even though this expression is polymorphic in the environment
@@ -72,7 +72,7 @@ class GuestLanguageBool c where
 -- The upshot is that we can define special-purpose "run" classes such as:
 --
 --   class GuestLanguageRunMult t where
---     ga_runMult :: forall a. (forall c. GuestLanguageMult c t => <[a]>@c) -> a
+--     ga_runMult :: forall a. (forall c. GuestLanguageMult c t => <{a}>@c) -> a
 --
 -- Any implementation of this class will need to know how to interpret
 -- the (*) operator.  Unfortunately, to my knowledge, there is no way
@@ -81,7 +81,7 @@ class GuestLanguageBool c where
 -- GuestLanguageRun class; if we could do that, then we would have:
 --
 --   class GuestLanguageRun ( t ::: * -> TYPECLASS ) where
---     ga_runMult :: forall a. (forall c. TYPECLASS c => <[a]>@c) -> a
+--     ga_runMult :: forall a. (forall c. TYPECLASS c => <{a}>@c) -> a
 --
 -- It might be possible to pull this of using type families; I need to
 -- look into that.