Fix External Core interpreter
[ghc-hetmet.git] / utils / ext-core / Core.hs
index 89f8294..9df300e 100644 (file)
@@ -1,48 +1,59 @@
 module Core where
 
+import Encoding
+
+import Data.Generics
 import List (elemIndex)
 
 data Module 
  = Module AnMname [Tdef] [Vdefg]
+  deriving (Data, Typeable)
 
 data Tdef 
   = Data (Qual Tcon) [Tbind] [Cdef]
-  | Newtype (Qual Tcon) [Tbind] (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)
+ deriving (Data, Typeable)
 
 data Cdef 
   = Constr (Qual Dcon) [Tbind] [Ty]
+  deriving (Data, Typeable)
 
 data Vdefg 
   = Rec [Vdef]
   | Nonrec Vdef
+  deriving (Data, Typeable)
 
 newtype Vdef = Vdef (Qual Var,Ty,Exp)
+  deriving (Data, Typeable)
 
 data Exp 
   = Var (Qual Var)
   | Dcon (Qual Dcon)
   | Lit Lit
--- Why were type apps and value apps distinguished,
--- but not type lambdas and value lambdas?
   | App Exp Exp
   | Appt Exp Ty
   | Lam Bind Exp         
   | Let Vdefg Exp
--- Ty is new
   | Case Exp Vbind Ty [Alt] {- non-empty list -}
--- Renamed to Cast; switched order
   | Cast Exp Ty
   | Note String Exp
   | External String Ty
+  deriving (Data, Typeable)
 
 data Bind 
   = Vb Vbind
   | Tb Tbind
+  deriving (Data, Typeable)
 
 data Alt 
   = Acon (Qual Dcon) [Tbind] [Vbind] Exp
   | Alit Lit Exp
   | Adefault Exp
+  deriving (Data, Typeable)
 
 type Vbind = (Var,Ty)
 type Tbind = (Tvar,Kind)
@@ -52,34 +63,68 @@ data Ty
   | Tcon (Qual Tcon)
   | Tapp Ty Ty
   | Tforall Tbind Ty 
+-- Wired-in coercions:
+-- These are primitive tycons in GHC, but in ext-core,
+-- we make them explicit, to make the typechecker
+-- somewhat more clear. 
+  | TransCoercion Ty Ty
+  | SymCoercion Ty
+  | UnsafeCoercion Ty Ty
+  | InstCoercion Ty Ty
+  | LeftCoercion Ty
+  | RightCoercion Ty
+  deriving (Data, Typeable)
 
 data Kind 
   = Klifted
   | Kunlifted
   | Kopen
   | Karrow Kind Kind
-  deriving (Eq)
-
-data Lit 
-  = Lint Integer Ty
-  | Lrational Rational Ty
-  | Lchar Char Ty
-  | Lstring String Ty
-  deriving (Eq)  -- with nearlyEqualTy 
-
--- new: Pnames
--- this requires at least one module name,
--- and possibly other hierarchical names
--- an alternative would be to flatten the
+  | Keq Ty Ty
+  deriving (Data, Typeable)
+
+-- A CoercionKind isn't really a Kind at all, but rather,
+-- corresponds to an arbitrary user-declared axiom.
+-- A tycon whose CoercionKind is (DefinedCoercion <tbs> (from, to))
+-- represents a tycon with arity (length tbs), whose kind is
+-- (from :=: to) (modulo substituting type arguments.
+-- It's not a Kind because a coercion must always be fully applied:
+-- whenever we see a tycon that has such a CoercionKind, it must
+-- be fully applied if it's to be assigned an actual Kind.
+-- So, a CoercionKind *only* appears in the environment (mapping
+-- newtype axioms onto CoercionKinds).
+-- Was that clear??
+data CoercionKind = 
+   DefinedCoercion [Tbind] (Ty,Ty)
+
+-- The type constructor environment maps names that are
+-- either type constructors or coercion names onto either
+-- kinds or coercion kinds.
+data KindOrCoercion = Kind Kind | Coercion CoercionKind
+  
+data Lit = Literal CoreLit Ty
+  deriving (Data, Typeable, Eq)   -- with nearlyEqualTy 
+
+data CoreLit = Lint Integer
+  | Lrational Rational
+  | Lchar Char
+  | Lstring String 
+  deriving (Data, Typeable, Eq)
+
+-- Right now we represent module names as triples:
+-- (package name, hierarchical names, leaf name)
+-- An alternative to this would be to flatten the
 -- module namespace, either when printing out
 -- Core or (probably preferably) in a 
 -- preprocessor.
--- Maybe because the empty module name is a module name (represented as
--- Nothing.)
+-- We represent the empty module name (as in an unqualified name)
+-- with Nothing.
 
 type Mname = Maybe AnMname
-type AnMname = (Pname, [Id], Id)
-type Pname = Id
+newtype AnMname = M (Pname, [Id], Id)
+  deriving (Eq, Ord, Data, Typeable)
+newtype Pname = P Id
+  deriving (Eq, Ord, Data, Typeable)
 type Var = Id
 type Tvar = Id
 type Tcon = Id
@@ -93,10 +138,32 @@ qual mn t = (Just mn, t)
 unqual :: t -> Qual t
 unqual = (,) Nothing
 
-type Id = String
+getModule :: Qual t -> Mname
+getModule = fst
 
---- tjc: I haven't looked at the rest of this file. ---
+type Id = String
 
+eqKind :: Kind -> Kind -> Bool
+eqKind Klifted Klifted = True
+eqKind Kunlifted Kunlifted = True
+eqKind Kopen Kopen = True
+eqKind (Karrow k1 k2) (Karrow l1 l2) = k1 `eqKind` l1
+                                   &&  k2 `eqKind` l2
+eqKind (Keq t1 t2) (Keq u1 u2) = t1 == u1
+                              && t2 == u2
+eqKind _ _ = False
+
+splitTyConApp_maybe :: Ty -> Maybe (Qual Tcon,[Ty])
+splitTyConApp_maybe (Tvar _) = Nothing
+splitTyConApp_maybe (Tcon t) = Just (t,[])
+splitTyConApp_maybe (Tapp rator rand) = 
+   case (splitTyConApp_maybe rator) of
+      Just (r,rs) -> Just (r,rs++[rand])
+      Nothing     -> case rator of
+                       Tcon tc -> Just (tc,[rand])
+                       _       -> Nothing
+splitTyConApp_maybe t@(Tforall _ _) = Nothing
+           
 {- Doesn't expand out fully applied newtype synonyms
    (for which an environment is needed). -}
 nearlyEqualTy t1 t2 =  eqTy [] [] t1 t2 
@@ -109,16 +176,16 @@ nearlyEqualTy t1 t2 =  eqTy [] [] t1 t2
         eqTy e1 e2 (Tapp t1a t1b) (Tapp t2a t2b) =
              eqTy e1 e2 t1a t2a && eqTy e1 e2 t1b t2b
         eqTy e1 e2 (Tforall (tv1,tk1) t1) (Tforall (tv2,tk2) t2) =
-             tk1 == tk2 && eqTy (tv1:e1) (tv2:e2) t1 t2 
+             tk1 `eqKind` tk2 && eqTy (tv1:e1) (tv2:e2) t1 t2 
        eqTy _ _ _ _ = False
 instance Eq Ty where (==) = nearlyEqualTy
 
 
 subKindOf :: Kind -> Kind -> Bool
 _ `subKindOf` Kopen = True
-k1 `subKindOf` k2 = k1 == k2  -- doesn't worry about higher kinds
-
-instance Ord Kind where (<=) = subKindOf
+(Karrow a1 r1) `subKindOf` (Karrow a2 r2) = 
+  a2 `subKindOf` a1 && (r1 `subKindOf` r2)
+k1 `subKindOf` k2 = k1 `eqKind` k2  -- doesn't worry about higher kinds
 
 baseKind :: Kind -> Bool
 baseKind (Karrow _ _ ) = False
@@ -127,17 +194,28 @@ baseKind _ = True
 isPrimVar (Just mn,_) = mn == primMname
 isPrimVar _ = False
 
-primMname = mkBaseMname "Prim"
+primMname = mkPrimMname "Prim"
 errMname  = mkBaseMname "Err"
-mkBaseMname :: Id -> AnMname
-mkBaseMname mn = (basePkg, ghcPrefix, mn)
-basePkg = "base"
-mainPkg = "main"
+mkBaseMname,mkPrimMname :: Id -> AnMname
+mkBaseMname mn = M (basePkg, ghcPrefix, mn)
+mkPrimMname mn = M (primPkg, ghcPrefix, mn)
+basePkg = P "base"
+mainPkg = P "main"
+primPkg = P $ zEncodeString "ghc-prim"
 ghcPrefix = ["GHC"]
 mainPrefix = []
 baseMname = mkBaseMname "Base"
+boolMname = mkPrimMname "Bool"
 mainVar = qual mainMname "main"
-mainMname = (mainPkg, mainPrefix, "Main")
+wrapperMainVar = qual wrapperMainMname "main"
+mainMname = M (mainPkg, mainPrefix, "Main")
+wrapperMainMname = M (mainPkg, mainPrefix, "ZCMain")
+wrapperMainAnMname = Just wrapperMainMname
+
+dcTrue :: Dcon
+dcTrue = "True"
+dcFalse :: Dcon
+dcFalse = "False"
 
 tcArrow :: Qual Tcon
 tcArrow = (Just primMname, "ZLzmzgZR")
@@ -145,14 +223,15 @@ tcArrow = (Just primMname, "ZLzmzgZR")
 tArrow :: Ty -> Ty -> Ty
 tArrow t1 t2 = Tapp (Tapp (Tcon tcArrow) t1) t2
 
+mkFunTy :: Ty -> Ty -> Ty
+mkFunTy randTy resultTy =
+  Tapp (Tapp (Tcon tcArrow) randTy) resultTy
 
 ktArrow :: Kind
 ktArrow = Karrow Kopen (Karrow Kopen Klifted)
 
 {- Unboxed tuples -}
 
--- tjc: not sure whether anything that follows is right
-
 maxUtuple :: Int
 maxUtuple = 100
 
@@ -171,7 +250,9 @@ isUtupleTy (Tcon tc) = tc `elem` [tcUtuple n | n <- [1..maxUtuple]]
 isUtupleTy _ = False
 
 dcUtuple :: Int -> Qual Dcon
-dcUtuple n = (Just primMname,"ZdwZ" ++ (show n) ++ "H")
+-- TODO: Seems like Z2H etc. appears in ext-core files,
+-- not $wZ2H etc. Is this right?
+dcUtuple n = (Just primMname,"Z" ++ (show n) ++ "H")
 
 isUtupleDc :: Qual Dcon -> Bool
 isUtupleDc dc = dc `elem` [dcUtuple n | n <- [1..maxUtuple]]
@@ -187,4 +268,8 @@ dcUtupleTy n =
 utuple :: [Ty] -> [Exp] -> Exp
 utuple ts es = foldl App (foldl Appt (Dcon (dcUtuple (length es))) ts) es
 
-
+---- snarfed from GHC's CoreSyn
+flattenBinds :: [Vdefg] -> [Vdef]      -- Get all the lhs/rhs pairs
+flattenBinds (Nonrec vd : binds) = vd : flattenBinds binds
+flattenBinds (Rec prs1   : binds) = prs1 ++ flattenBinds binds
+flattenBinds []                          = []