X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=utils%2Fext-core%2FCore.hs;h=0fb48b81d4f3200a83cf3fa72e2ce45a28be3b1a;hp=89f8294c25feb4fa9bdfdb58925395d64ae46f40;hb=e4417dcd4679da9c6b18c02ff667199c572bed89;hpb=276585028d51a2516a31b91a91a1f4bba5c9f8ba diff --git a/utils/ext-core/Core.hs b/utils/ext-core/Core.hs index 89f8294..0fb48b8 100644 --- a/utils/ext-core/Core.hs +++ b/utils/ext-core/Core.hs @@ -1,5 +1,7 @@ module Core where +import Encoding + import List (elemIndex) data Module @@ -7,7 +9,11 @@ data Module 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) data Cdef = Constr (Qual Dcon) [Tbind] [Ty] @@ -22,15 +28,11 @@ 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 @@ -52,33 +54,64 @@ 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 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 + +-- A CoercionKind isn't really a Kind at all, but rather, +-- corresponds to an arbitrary user-declared axiom. +-- A tycon whose CoercionKind is (DefinedCoercion (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 Eq -- with nearlyEqualTy + +data CoreLit = Lint Integer + | Lrational Rational + | Lchar Char + | Lstring String + deriving 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) +newtype AnMname = M (Pname, [Id], Id) + deriving (Eq, Ord) type Pname = Id type Var = Id type Tvar = Id @@ -95,8 +128,27 @@ unqual = (,) Nothing type Id = String ---- tjc: I haven't looked at the rest of this file. --- - +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 +161,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 +179,21 @@ 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) +mkBaseMname,mkPrimMname :: Id -> AnMname +mkBaseMname mn = M (basePkg, ghcPrefix, mn) +mkPrimMname mn = M (primPkg, ghcPrefix, mn) basePkg = "base" mainPkg = "main" +primPkg = zEncodeString "ghc-prim" ghcPrefix = ["GHC"] mainPrefix = [] baseMname = mkBaseMname "Base" +boolMname = mkPrimMname "Bool" mainVar = qual mainMname "main" -mainMname = (mainPkg, mainPrefix, "Main") +mainMname = M (mainPkg, mainPrefix, "Main") +wrapperMainMname = Just $ M (mainPkg, mainPrefix, "ZCMain") tcArrow :: Qual Tcon tcArrow = (Just primMname, "ZLzmzgZR") @@ -151,8 +207,6 @@ ktArrow = Karrow Kopen (Karrow Kopen Klifted) {- Unboxed tuples -} --- tjc: not sure whether anything that follows is right - maxUtuple :: Int maxUtuple = 100 @@ -171,7 +225,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]]