utils/ext-core/Language/Core/Core.hs

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