Improve External Core syntax for newtypes

[ghc-hetmet.git] / utils / ext-core / Core.hs

diff --git a/utils/ext-core/Core.hs b/utils/ext-core/Core.hs
index ce2a11d..0fb48b8 100644 (file)
--- a/utils/ext-core/Core.hs
+++ b/utils/ext-core/Core.hs
@@ -9,14 +9,15 @@ data Module
 
 data Tdef 
   = Data (Qual Tcon) [Tbind] [Cdef]
-  | Newtype (Qual Tcon) [Tbind] Axiom (Maybe Ty)
+    -- type constructor; coercion name; type arguments; type rep
+    -- If we have: (Newtype tc co tbs (Just t))
+    -- there is an implicit axiom:
+    --  co tbs :: tc tbs :=: t
+  | Newtype (Qual Tcon) (Qual Tcon) [Tbind] (Maybe Ty)
 
 data Cdef 
   = Constr (Qual Dcon) [Tbind] [Ty]
 
--- Newtype coercion
-type Axiom = (Qual Tcon, [Tbind], (Ty,Ty))
-
 data Vdefg 
   = Rec [Vdef]
   | Nonrec Vdef
@@ -60,6 +61,7 @@ data Ty
   | TransCoercion Ty Ty
   | SymCoercion Ty
   | UnsafeCoercion Ty Ty
+  | InstCoercion Ty Ty
   | LeftCoercion Ty
   | RightCoercion Ty
 
@@ -108,7 +110,8 @@ data CoreLit = Lint Integer
 -- with Nothing.
 
 type Mname = Maybe AnMname
-type AnMname = (Pname, [Id], Id)
+newtype AnMname = M (Pname, [Id], Id)
+  deriving (Eq, Ord)
 type Pname = Id
 type Var = Id
 type Tvar = Id
@@ -131,9 +134,9 @@ eqKind Kunlifted Kunlifted = True
 eqKind Kopen Kopen = True
 eqKind (Karrow k1 k2) (Karrow l1 l2) = k1 `eqKind` l1
                                    &&  k2 `eqKind` l2
-eqKind _ _ = False -- no Keq kind is ever equal to any other...
-                   -- maybe ok for now?
-
+eqKind (Keq t1 t2) (Keq u1 u2) = t1 == u1
+                              && t2 == u2
+eqKind _ _ = False
 
 splitTyConApp_maybe :: Ty -> Maybe (Qual Tcon,[Ty])
 splitTyConApp_maybe (Tvar _) = Nothing
@@ -179,8 +182,8 @@ isPrimVar _ = False
 primMname = mkPrimMname "Prim"
 errMname  = mkBaseMname "Err"
 mkBaseMname,mkPrimMname :: Id -> AnMname
-mkBaseMname mn = (basePkg, ghcPrefix, mn)
-mkPrimMname mn = (primPkg, ghcPrefix, mn)
+mkBaseMname mn = M (basePkg, ghcPrefix, mn)
+mkPrimMname mn = M (primPkg, ghcPrefix, mn)
 basePkg = "base"
 mainPkg = "main"
 primPkg = zEncodeString "ghc-prim"
@@ -189,8 +192,8 @@ mainPrefix = []
 baseMname = mkBaseMname "Base"
 boolMname = mkPrimMname "Bool"
 mainVar = qual mainMname "main"
-mainMname = (mainPkg, mainPrefix, "Main")
-wrapperMainMname = Just (mainPkg, mainPrefix, "ZCMain")
+mainMname = M (mainPkg, mainPrefix, "Main")
+wrapperMainMname = Just $ M (mainPkg, mainPrefix, "ZCMain")
 
 tcArrow :: Qual Tcon
 tcArrow = (Just primMname, "ZLzmzgZR")