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