module Core where
+import Encoding
+
import List (elemIndex)
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]
= 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
| 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 <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 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
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
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
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")
{- Unboxed tuples -}
--- tjc: not sure whether anything that follows is right
-
maxUtuple :: Int
maxUtuple = 100
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]]
projects / ghc-hetmet.git / blobdiff