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