X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=utils%2Fext-core%2FCore.hs;h=9df300e010a3519522f4d2e9e2fe523149a59275;hb=eced5e4068f4cb5da397ca1fd4eeea462f197503;hp=2f94f80b3ef4a9e0baaccf0ecf78e5fc1c300e95;hpb=0065d5ab628975892cea1ec7303f968c3338cbe1;p=ghc-hetmet.git diff --git a/utils/ext-core/Core.hs b/utils/ext-core/Core.hs index 2f94f80..9df300e 100644 --- a/utils/ext-core/Core.hs +++ b/utils/ext-core/Core.hs @@ -1,22 +1,34 @@ module Core where +import Encoding + +import Data.Generics import List (elemIndex) data Module - = Module Mname [Tdef] [Vdefg] + = 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) @@ -26,19 +38,22 @@ data Exp | Appt Exp Ty | Lam Bind Exp | Let Vdefg Exp - | Case Exp Vbind [Alt] {- non-empty list -} - | Coerce Ty Exp + | Case Exp Vbind Ty [Alt] {- non-empty list -} + | 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) @@ -48,22 +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 - -type Mname = Id + | 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 (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. +-- We represent the empty module name (as in an unqualified name) +-- with Nothing. + +type Mname = Maybe AnMname +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 @@ -71,8 +132,38 @@ type Dcon = Id type Qual t = (Mname,t) +qual :: AnMname -> t -> Qual t +qual mn t = (Just mn, t) + +unqual :: t -> Qual t +unqual = (,) Nothing + +getModule :: Qual t -> Mname +getModule = fst + 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 @@ -85,29 +176,57 @@ 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 baseKind _ = True -primMname = "PrelGHC" +isPrimVar (Just mn,_) = mn == primMname +isPrimVar _ = False + +primMname = mkPrimMname "Prim" +errMname = mkBaseMname "Err" +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" +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 = (primMname, "ZLzmzgZR") +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) @@ -117,7 +236,7 @@ maxUtuple :: Int maxUtuple = 100 tcUtuple :: Int -> Qual Tcon -tcUtuple n = (primMname,"Z"++ (show n) ++ "H") +tcUtuple n = (Just primMname,"Z"++ (show n) ++ "H") ktUtuple :: Int -> Kind ktUtuple n = foldr Karrow Kunlifted (replicate n Kopen) @@ -131,7 +250,9 @@ isUtupleTy (Tcon tc) = tc `elem` [tcUtuple n | n <- [1..maxUtuple]] isUtupleTy _ = False dcUtuple :: Int -> Qual Dcon -dcUtuple n = (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]] @@ -147,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 [] = []