utils/ext-core/Core.hs

   1 module Core where
   2
   3 import Encoding
   4
   5 import List (elemIndex)
   6
   7 data Module
   8  = Module AnMname [Tdef] [Vdefg]
   9
  10 data Tdef
  11   = Data (Qual Tcon) [Tbind] [Cdef]
  12   | Newtype (Qual Tcon) [Tbind] Axiom (Maybe Ty)
  13
  14 data Cdef
  15   = Constr (Qual Dcon) [Tbind] [Ty]
  16
  17 -- Newtype coercion
  18 type Axiom = (Qual Tcon, [Tbind], (Ty,Ty))
  19
  20 data Vdefg
  21   = Rec [Vdef]
  22   | Nonrec Vdef
  23
  24 newtype Vdef = Vdef (Qual Var,Ty,Exp)
  25
  26 data Exp
  27   = Var (Qual Var)
  28   | Dcon (Qual Dcon)
  29   | Lit Lit
  30   | App Exp Exp
  31   | Appt Exp Ty
  32   | Lam Bind Exp
  33   | Let Vdefg Exp
  34   | Case Exp Vbind Ty [Alt] {- non-empty list -}
  35   | Cast Exp Ty
  36   | Note String Exp
  37   | External String Ty
  38
  39 data Bind
  40   = Vb Vbind
  41   | Tb Tbind
  42
  43 data Alt
  44   = Acon (Qual Dcon) [Tbind] [Vbind] Exp
  45   | Alit Lit Exp
  46   | Adefault Exp
  47
  48 type Vbind = (Var,Ty)
  49 type Tbind = (Tvar,Kind)
  50
  51 data Ty
  52   = Tvar Tvar
  53   | Tcon (Qual Tcon)
  54   | Tapp Ty Ty
  55   | Tforall Tbind Ty
  56 -- Wired-in coercions:
  57 -- These are primitive tycons in GHC, but in ext-core,
  58 -- we make them explicit, to make the typechecker
  59 -- somewhat more clear.
  60   | TransCoercion Ty Ty
  61   | SymCoercion Ty
  62   | UnsafeCoercion Ty Ty
  63   | InstCoercion Ty Ty
  64   | LeftCoercion Ty
  65   | RightCoercion Ty
  66
  67 data Kind
  68   = Klifted
  69   | Kunlifted
  70   | Kopen
  71   | Karrow Kind Kind
  72   | Keq Ty Ty
  73
  74 -- A CoercionKind isn't really a Kind at all, but rather,
  75 -- corresponds to an arbitrary user-declared axiom.
  76 -- A tycon whose CoercionKind is (DefinedCoercion <tbs> (from, to))
  77 -- represents a tycon with arity (length tbs), whose kind is
  78 -- (from :=: to) (modulo substituting type arguments.
  79 -- It's not a Kind because a coercion must always be fully applied:
  80 -- whenever we see a tycon that has such a CoercionKind, it must
  81 -- be fully applied if it's to be assigned an actual Kind.
  82 -- So, a CoercionKind *only* appears in the environment (mapping
  83 -- newtype axioms onto CoercionKinds).
  84 -- Was that clear??
  85 data CoercionKind =
  86    DefinedCoercion [Tbind] (Ty,Ty)
  87
  88 -- The type constructor environment maps names that are
  89 -- either type constructors or coercion names onto either
  90 -- kinds or coercion kinds.
  91 data KindOrCoercion = Kind Kind | Coercion CoercionKind
  92
  93 data Lit = Literal CoreLit Ty
  94   deriving Eq   -- with nearlyEqualTy
  95
  96 data CoreLit = Lint Integer
  97   | Lrational Rational
  98   | Lchar Char
  99   | Lstring String
 100   deriving Eq
 101
 102 -- Right now we represent module names as triples:
 103 -- (package name, hierarchical names, leaf name)
 104 -- An alternative to this would be to flatten the
 105 -- module namespace, either when printing out
 106 -- Core or (probably preferably) in a
 107 -- preprocessor.
 108 -- We represent the empty module name (as in an unqualified name)
 109 -- with Nothing.
 110
 111 type Mname = Maybe AnMname
 112 newtype AnMname = M (Pname, [Id], Id)
 113   deriving (Eq, Ord)
 114 type Pname = Id
 115 type Var = Id
 116 type Tvar = Id
 117 type Tcon = Id
 118 type Dcon = Id
 119
 120 type Qual t = (Mname,t)
 121
 122 qual :: AnMname -> t -> Qual t
 123 qual mn t = (Just mn, t)
 124
 125 unqual :: t -> Qual t
 126 unqual = (,) Nothing
 127
 128 type Id = String
 129
 130 eqKind :: Kind -> Kind -> Bool
 131 eqKind Klifted Klifted = True
 132 eqKind Kunlifted Kunlifted = True
 133 eqKind Kopen Kopen = True
 134 eqKind (Karrow k1 k2) (Karrow l1 l2) = k1 `eqKind` l1
 135                                    &&  k2 `eqKind` l2
 136 eqKind (Keq t1 t2) (Keq u1 u2) = t1 == u1
 137                               && t2 == u2
 138 eqKind _ _ = False
 139
 140 splitTyConApp_maybe :: Ty -> Maybe (Qual Tcon,[Ty])
 141 splitTyConApp_maybe (Tvar _) = Nothing
 142 splitTyConApp_maybe (Tcon t) = Just (t,[])
 143 splitTyConApp_maybe (Tapp rator rand) =
 144    case (splitTyConApp_maybe rator) of
 145       Just (r,rs) -> Just (r,rs++[rand])
 146       Nothing     -> case rator of
 147                        Tcon tc -> Just (tc,[rand])
 148                        _       -> Nothing
 149 splitTyConApp_maybe t@(Tforall _ _) = Nothing
 150
 151 {- Doesn't expand out fully applied newtype synonyms
 152    (for which an environment is needed). -}
 153 nearlyEqualTy t1 t2 =  eqTy [] [] t1 t2
 154   where eqTy e1 e2 (Tvar v1) (Tvar v2) =
 155              case (elemIndex v1 e1,elemIndex v2 e2) of
 156                (Just i1, Just i2) -> i1 == i2
 157                (Nothing, Nothing)  -> v1 == v2
 158                _ -> False
 159         eqTy e1 e2 (Tcon c1) (Tcon c2) = c1 == c2
 160         eqTy e1 e2 (Tapp t1a t1b) (Tapp t2a t2b) =
 161               eqTy e1 e2 t1a t2a && eqTy e1 e2 t1b t2b
 162         eqTy e1 e2 (Tforall (tv1,tk1) t1) (Tforall (tv2,tk2) t2) =
 163               tk1 `eqKind` tk2 && eqTy (tv1:e1) (tv2:e2) t1 t2
 164         eqTy _ _ _ _ = False
 165 instance Eq Ty where (==) = nearlyEqualTy
 166
 167
 168 subKindOf :: Kind -> Kind -> Bool
 169 _ `subKindOf` Kopen = True
 170 (Karrow a1 r1) `subKindOf` (Karrow a2 r2) =
 171   a2 `subKindOf` a1 && (r1 `subKindOf` r2)
 172 k1 `subKindOf` k2 = k1 `eqKind` k2  -- doesn't worry about higher kinds
 173
 174 baseKind :: Kind -> Bool
 175 baseKind (Karrow _ _ ) = False
 176 baseKind _ = True
 177
 178 isPrimVar (Just mn,_) = mn == primMname
 179 isPrimVar _ = False
 180
 181 primMname = mkPrimMname "Prim"
 182 errMname  = mkBaseMname "Err"
 183 mkBaseMname,mkPrimMname :: Id -> AnMname
 184 mkBaseMname mn = M (basePkg, ghcPrefix, mn)
 185 mkPrimMname mn = M (primPkg, ghcPrefix, mn)
 186 basePkg = "base"
 187 mainPkg = "main"
 188 primPkg = zEncodeString "ghc-prim"
 189 ghcPrefix = ["GHC"]
 190 mainPrefix = []
 191 baseMname = mkBaseMname "Base"
 192 boolMname = mkPrimMname "Bool"
 193 mainVar = qual mainMname "main"
 194 mainMname = M (mainPkg, mainPrefix, "Main")
 195 wrapperMainMname = Just $ M (mainPkg, mainPrefix, "ZCMain")
 196
 197 tcArrow :: Qual Tcon
 198 tcArrow = (Just primMname, "ZLzmzgZR")
 199
 200 tArrow :: Ty -> Ty -> Ty
 201 tArrow t1 t2 = Tapp (Tapp (Tcon tcArrow) t1) t2
 202
 203
 204 ktArrow :: Kind
 205 ktArrow = Karrow Kopen (Karrow Kopen Klifted)
 206
 207 {- Unboxed tuples -}
 208
 209 maxUtuple :: Int
 210 maxUtuple = 100
 211
 212 tcUtuple :: Int -> Qual Tcon
 213 tcUtuple n = (Just primMname,"Z"++ (show n) ++ "H")
 214
 215 ktUtuple :: Int -> Kind
 216 ktUtuple n = foldr Karrow Kunlifted (replicate n Kopen)
 217
 218 tUtuple :: [Ty] -> Ty
 219 tUtuple ts = foldl Tapp (Tcon (tcUtuple (length ts))) ts
 220
 221 isUtupleTy :: Ty -> Bool
 222 isUtupleTy (Tapp t _) = isUtupleTy t
 223 isUtupleTy (Tcon tc) = tc `elem` [tcUtuple n | n <- [1..maxUtuple]]
 224 isUtupleTy _ = False
 225
 226 dcUtuple :: Int -> Qual Dcon
 227 -- TODO: Seems like Z2H etc. appears in ext-core files,
 228 -- not $wZ2H etc. Is this right?
 229 dcUtuple n = (Just primMname,"Z" ++ (show n) ++ "H")
 230
 231 isUtupleDc :: Qual Dcon -> Bool
 232 isUtupleDc dc = dc `elem` [dcUtuple n | n <- [1..maxUtuple]]
 233
 234 dcUtupleTy :: Int -> Ty
 235 dcUtupleTy n =
 236      foldr ( \tv t -> Tforall (tv,Kopen) t)
 237            (foldr ( \tv t -> tArrow (Tvar tv) t)
 238                   (tUtuple (map Tvar tvs)) tvs)
 239            tvs
 240      where tvs = map ( \i -> ("a" ++ (show i))) [1..n]
 241
 242 utuple :: [Ty] -> [Exp] -> Exp
 243 utuple ts es = foldl App (foldl Appt (Dcon (dcUtuple (length es))) ts) es
 244
 245