Mercurial > urweb

comparison src/corify.sml @ 188:8e9f97508f0d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Datatype representation optimization
author Adam Chlipala <adamc@hcoop.net>
date Sun, 03 Aug 2008 19:49:21 -0400
parents 88d46972de53
children aa54250f58ac
comparison
equal deleted inserted replaced
187:fb6ed259f5bd 188:8e9f97508f0d
60 60
61 val debug : t -> unit 61 val debug : t -> unit
62 62
63 val enter : t -> t 63 val enter : t -> t
64 val leave : t -> {outer : t, inner : t} 64 val leave : t -> {outer : t, inner : t}
65 val ffi : string -> L'.con SM.map -> (string * L'.con option) SM.map -> t 65 val ffi : string -> L'.con SM.map -> (string * L'.con option * L'.datatype_kind) SM.map -> t
66 66
67 datatype core_con = 67 datatype core_con =
68 CNormal of int 68 CNormal of int
69 | CFfi of string 69 | CFfi of string
70 val bindCon : t -> string -> int -> t * int 70 val bindCon : t -> string -> int -> t * int
74 val bindConstructor : t -> string -> int -> L'.patCon -> t 74 val bindConstructor : t -> string -> int -> L'.patCon -> t
75 val lookupConstructorByNameOpt : t -> string -> L'.patCon option 75 val lookupConstructorByNameOpt : t -> string -> L'.patCon option
76 val lookupConstructorByName : t -> string -> L'.patCon 76 val lookupConstructorByName : t -> string -> L'.patCon
77 val lookupConstructorById : t -> int -> L'.patCon 77 val lookupConstructorById : t -> int -> L'.patCon
78 78
79 datatype core_val = 79 datatype core_val =
80 ENormal of int 80 ENormal of int
81 | EFfi of string * L'.con 81 | EFfi of string * L'.con
82 val bindVal : t -> string -> int -> t * int 82 val bindVal : t -> string -> int -> t * int
83 val bindConstructorVal : t -> string -> int -> t 83 val bindConstructorVal : t -> string -> int -> t
84 val lookupValById : t -> int -> int option 84 val lookupValById : t -> int -> int option
85 val lookupValByName : t -> string -> core_val 85 val lookupValByName : t -> string -> core_val
86 86
87 val bindStr : t -> string -> int -> t -> t 87 val bindStr : t -> string -> int -> t -> t
88 val lookupStrById : t -> int -> t 88 val lookupStrById : t -> int -> t
89 val lookupStrByName : string * t -> t 89 val lookupStrByName : string * t -> t
90 90
91 val bindFunctor : t -> string -> int -> string -> int -> L.str -> t 91 val bindFunctor : t -> string -> int -> string -> int -> L.str -> t
92 val lookupFunctorById : t -> int -> string * int * L.str 92 val lookupFunctorById : t -> int -> string * int * L.str
93 val lookupFunctorByName : string * t -> string * int * L.str 93 val lookupFunctorByName : string * t -> string * int * L.str
94 end = struct 94 end = struct
95 95
96 datatype flattening = 96 datatype flattening =
97 FNormal of {cons : int SM.map, 97 FNormal of {cons : int SM.map,
98 constructors : L'.patCon SM.map, 98 constructors : L'.patCon SM.map,
99 vals : int SM.map, 99 vals : int SM.map,
100 strs : flattening SM.map, 100 strs : flattening SM.map,
101 funs : (string * int * L.str) SM.map} 101 funs : (string * int * L.str) SM.map}
102 | FFfi of {mod : string, 102 | FFfi of {mod : string,
103 vals : L'.con SM.map, 103 vals : L'.con SM.map,
104 constructors : (string * L'.con option) SM.map} 104 constructors : (string * L'.con option * L'.datatype_kind) SM.map}
105 105
106 type t = { 106 type t = {
107 cons : int IM.map, 107 cons : int IM.map,
108 constructors : L'.patCon IM.map, 108 constructors : L'.patCon IM.map,
109 vals : int IM.map, 109 vals : int IM.map,
110 strs : flattening IM.map, 110 strs : flattening IM.map,
111 funs : (string * int * L.str) IM.map, 111 funs : (string * int * L.str) IM.map,
112 current : flattening, 112 current : flattening,
113 nested : flattening list 113 nested : flattening list
114 } 114 }
115 115
116 val empty = { 116 val empty = {
117 cons = IM.empty, 117 cons = IM.empty,
118 constructors = IM.empty, 118 constructors = IM.empty,
119 vals = IM.empty, 119 vals = IM.empty,
120 strs = IM.empty, 120 strs = IM.empty,
121 funs = IM.empty, 121 funs = IM.empty,
122 current = FNormal { cons = SM.empty, constructors = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty }, 122 current = FNormal { cons = SM.empty, constructors = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty },
123 nested = [] 123 nested = []
124 } 124 }
125 125
126 fun debug ({current = FNormal {cons, constructors, vals, strs, funs}, ...} : t) = 126 fun debug ({current = FNormal {cons, constructors, vals, strs, funs}, ...} : t) =
127 print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; " 127 print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; "
128 ^ "constructors: " ^ Int.toString (SM.numItems constructors) ^ "; " 128 ^ "constructors: " ^ Int.toString (SM.numItems constructors) ^ "; "
129 ^ "vals: " ^ Int.toString (SM.numItems vals) ^ "; " 129 ^ "vals: " ^ Int.toString (SM.numItems vals) ^ "; "
130 ^ "strs: " ^ Int.toString (SM.numItems strs) ^ "; " 130 ^ "strs: " ^ Int.toString (SM.numItems strs) ^ "; "
131 ^ "funs: " ^ Int.toString (SM.numItems funs) ^ "\n") 131 ^ "funs: " ^ Int.toString (SM.numItems funs) ^ "\n")
132 | debug _ = print "Not normal!\n" 132 | debug _ = print "Not normal!\n"
133 133
134 datatype core_con = 134 datatype core_con =
135 CNormal of int 135 CNormal of int
136 | CFfi of string 136 | CFfi of string
137 137
138 datatype core_val = 138 datatype core_val =
139 ENormal of int 139 ENormal of int
140 | EFfi of string * L'.con 140 | EFfi of string * L'.con
141 141
142 fun bindCon {cons, constructors, vals, strs, funs, current, nested} s n = 142 fun bindCon {cons, constructors, vals, strs, funs, current, nested} s n =
143 let 143 let
144 val n' = alloc () 144 val n' = alloc ()
145 145
146 val current = 146 val current =
147 case current of 147 case current of
148 FFfi _ => raise Fail "Binding inside FFfi" 148 FFfi _ => raise Fail "Binding inside FFfi"
149 | FNormal {cons, constructors, vals, strs, funs} => 149 | FNormal {cons, constructors, vals, strs, funs} =>
150 FNormal {cons = SM.insert (cons, s, n'), 150 FNormal {cons = SM.insert (cons, s, n'),
151 constructors = constructors, 151 constructors = constructors,
152 vals = vals, 152 vals = vals,
153 strs = strs, 153 strs = strs,
154 funs = funs} 154 funs = funs}
155 in 155 in
156 ({cons = IM.insert (cons, n, n'), 156 ({cons = IM.insert (cons, n, n'),
157 constructors = constructors,
158 vals = vals,
159 strs = strs,
160 funs = funs,
161 current = current,
162 nested = nested},
163 n')
164 end
165
166 fun lookupConById ({cons, ...} : t) n = IM.find (cons, n)
167
168 fun lookupConByName ({current, ...} : t) x =
169 case current of
170 FFfi {mod = m, ...} => CFfi m
171 | FNormal {cons, ...} =>
172 case SM.find (cons, x) of
173 NONE => raise Fail "Corify.St.lookupConByName"
174 | SOME n => CNormal n
175
176 fun bindVal {cons, constructors, vals, strs, funs, current, nested} s n =
177 let
178 val n' = alloc ()
179
180 val current =
181 case current of
182 FFfi _ => raise Fail "Binding inside FFfi"
183 | FNormal {cons, constructors, vals, strs, funs} =>
184 FNormal {cons = cons,
185 constructors = constructors,
186 vals = SM.insert (vals, s, n'),
187 strs = strs,
188 funs = funs}
189 in
190 ({cons = cons,
191 constructors = constructors,
192 vals = IM.insert (vals, n, n'),
193 strs = strs,
194 funs = funs,
195 current = current,
196 nested = nested},
197 n')
198 end
199
200 fun bindConstructorVal {cons, constructors, vals, strs, funs, current, nested} s n =
201 let
202 val current =
203 case current of
204 FFfi _ => raise Fail "Binding inside FFfi"
205 | FNormal {cons, constructors, vals, strs, funs} =>
206 FNormal {cons = cons,
207 constructors = constructors,
208 vals = SM.insert (vals, s, n),
209 strs = strs,
210 funs = funs}
211 in
212 {cons = cons,
157 constructors = constructors, 213 constructors = constructors,
214 vals = IM.insert (vals, n, n),
215 strs = strs,
216 funs = funs,
217 current = current,
218 nested = nested}
219 end
220
221
222 fun lookupValById ({vals, ...} : t) n = IM.find (vals, n)
223
224 fun lookupValByName ({current, ...} : t) x =
225 case current of
226 FFfi {mod = m, vals, ...} =>
227 (case SM.find (vals, x) of
228 NONE => raise Fail "Corify.St.lookupValByName: no type for FFI val"
229 | SOME t => EFfi (m, t))
230 | FNormal {vals, ...} =>
231 case SM.find (vals, x) of
232 NONE => raise Fail "Corify.St.lookupValByName"
233 | SOME n => ENormal n
234
235 fun bindConstructor {cons, constructors, vals, strs, funs, current, nested} s n n' =
236 let
237 val current =
238 case current of
239 FFfi _ => raise Fail "Binding inside FFfi"
240 | FNormal {cons, constructors, vals, strs, funs} =>
241 FNormal {cons = cons,
242 constructors = SM.insert (constructors, s, n'),
243 vals = vals,
244 strs = strs,
245 funs = funs}
246 in
247 {cons = cons,
248 constructors = IM.insert (constructors, n, n'),
158 vals = vals, 249 vals = vals,
159 strs = strs, 250 strs = strs,
160 funs = funs, 251 funs = funs,
161 current = current, 252 current = current,
162 nested = nested}, 253 nested = nested}
163 n') 254 end
164 end 255
165 256 fun lookupConstructorById ({constructors, ...} : t) n =
166 fun lookupConById ({cons, ...} : t) n = IM.find (cons, n) 257 case IM.find (constructors, n) of
167 258 NONE => raise Fail "Corify.St.lookupConstructorById"
168 fun lookupConByName ({current, ...} : t) x = 259 | SOME x => x
169 case current of 260
170 FFfi {mod = m, ...} => CFfi m 261 fun lookupConstructorByNameOpt ({current, ...} : t) x =
171 | FNormal {cons, ...} => 262 case current of
172 case SM.find (cons, x) of 263 FFfi {mod = m, constructors, ...} =>
173 NONE => raise Fail "Corify.St.lookupConByName" 264 (case SM.find (constructors, x) of
174 | SOME n => CNormal n 265 NONE => NONE
175 266 | SOME (n, to, dk) => SOME (L'.PConFfi {mod = m, datatyp = n, con = x, arg = to, kind = dk}))
176 fun bindVal {cons, constructors, vals, strs, funs, current, nested} s n = 267 | FNormal {constructors, ...} =>
177 let 268 case SM.find (constructors, x) of
178 val n' = alloc ()
179
180 val current =
181 case current of
182 FFfi _ => raise Fail "Binding inside FFfi"
183 | FNormal {cons, constructors, vals, strs, funs} =>
184 FNormal {cons = cons,
185 constructors = constructors,
186 vals = SM.insert (vals, s, n'),
187 strs = strs,
188 funs = funs}
189 in
190 ({cons = cons,
191 constructors = constructors,
192 vals = IM.insert (vals, n, n'),
193 strs = strs,
194 funs = funs,
195 current = current,
196 nested = nested},
197 n')
198 end
199
200 fun bindConstructorVal {cons, constructors, vals, strs, funs, current, nested} s n =
201 let
202 val current =
203 case current of
204 FFfi _ => raise Fail "Binding inside FFfi"
205 | FNormal {cons, constructors, vals, strs, funs} =>
206 FNormal {cons = cons,
207 constructors = constructors,
208 vals = SM.insert (vals, s, n),
209 strs = strs,
210 funs = funs}
211 in
212 {cons = cons,
213 constructors = constructors,
214 vals = IM.insert (vals, n, n),
215 strs = strs,
216 funs = funs,
217 current = current,
218 nested = nested}
219 end
220
221
222 fun lookupValById ({vals, ...} : t) n = IM.find (vals, n)
223
224 fun lookupValByName ({current, ...} : t) x =
225 case current of
226 FFfi {mod = m, vals, ...} =>
227 (case SM.find (vals, x) of
228 NONE => raise Fail "Corify.St.lookupValByName: no type for FFI val"
229 | SOME t => EFfi (m, t))
230 | FNormal {vals, ...} =>
231 case SM.find (vals, x) of
232 NONE => raise Fail "Corify.St.lookupValByName"
233 | SOME n => ENormal n
234
235 fun bindConstructor {cons, constructors, vals, strs, funs, current, nested} s n n' =
236 let
237 val current =
238 case current of
239 FFfi _ => raise Fail "Binding inside FFfi"
240 | FNormal {cons, constructors, vals, strs, funs} =>
241 FNormal {cons = cons,
242 constructors = SM.insert (constructors, s, n'),
243 vals = vals,
244 strs = strs,
245 funs = funs}
246 in
247 {cons = cons,
248 constructors = IM.insert (constructors, n, n'),
249 vals = vals,
250 strs = strs,
251 funs = funs,
252 current = current,
253 nested = nested}
254 end
255
256 fun lookupConstructorById ({constructors, ...} : t) n =
257 case IM.find (constructors, n) of
258 NONE => raise Fail "Corify.St.lookupConstructorById"
259 | SOME x => x
260
261 fun lookupConstructorByNameOpt ({current, ...} : t) x =
262 case current of
263 FFfi {mod = m, constructors, ...} =>
264 (case SM.find (constructors, x) of
265 NONE => NONE 269 NONE => NONE
266 | SOME (n, to) => SOME (L'.PConFfi {mod = m, datatyp = n, con = x, arg = to})) 270 | SOME n => SOME n
267 | FNormal {constructors, ...} => 271
268 case SM.find (constructors, x) of 272 fun lookupConstructorByName ({current, ...} : t) x =
269 NONE => NONE 273 case current of
270 | SOME n => SOME n 274 FFfi {mod = m, constructors, ...} =>
271 275 (case SM.find (constructors, x) of
272 fun lookupConstructorByName ({current, ...} : t) x = 276 NONE => raise Fail "Corify.St.lookupConstructorByName [1]"
273 case current of 277 | SOME (n, to, dk) => L'.PConFfi {mod = m, datatyp = n, con = x, arg = to, kind = dk})
274 FFfi {mod = m, constructors, ...} => 278 | FNormal {constructors, ...} =>
275 (case SM.find (constructors, x) of 279 case SM.find (constructors, x) of
276 NONE => raise Fail "Corify.St.lookupConstructorByName [1]" 280 NONE => raise Fail "Corify.St.lookupConstructorByName [2]"
277 | SOME (n, to) => L'.PConFfi {mod = m, datatyp = n, con = x, arg = to}) 281 | SOME n => n
278 | FNormal {constructors, ...} => 282
279 case SM.find (constructors, x) of 283 fun enter {cons, constructors, vals, strs, funs, current, nested} =
280 NONE => raise Fail "Corify.St.lookupConstructorByName [2]" 284 {cons = cons,
281 | SOME n => n 285 constructors = constructors,
282 286 vals = vals,
283 fun enter {cons, constructors, vals, strs, funs, current, nested} = 287 strs = strs,
284 {cons = cons, 288 funs = funs,
285 constructors = constructors, 289 current = FNormal {cons = SM.empty,
286 vals = vals, 290 constructors = SM.empty,
287 strs = strs, 291 vals = SM.empty,
288 funs = funs, 292 strs = SM.empty,
289 current = FNormal {cons = SM.empty, 293 funs = SM.empty},
290 constructors = SM.empty, 294 nested = current :: nested}
291 vals = SM.empty, 295
292 strs = SM.empty, 296 fun dummy f = {cons = IM.empty,
293 funs = SM.empty}, 297 constructors = IM.empty,
294 nested = current :: nested} 298 vals = IM.empty,
295 299 strs = IM.empty,
296 fun dummy f = {cons = IM.empty, 300 funs = IM.empty,
297 constructors = IM.empty, 301 current = f,
298 vals = IM.empty, 302 nested = []}
299 strs = IM.empty, 303
300 funs = IM.empty, 304 fun leave {cons, constructors, vals, strs, funs, current, nested = m1 :: rest} =
301 current = f, 305 {outer = {cons = cons,
302 nested = []} 306 constructors = constructors,
303 307 vals = vals,
304 fun leave {cons, constructors, vals, strs, funs, current, nested = m1 :: rest} = 308 strs = strs,
305 {outer = {cons = cons, 309 funs = funs,
306 constructors = constructors, 310 current = m1,
307 vals = vals, 311 nested = rest},
308 strs = strs, 312 inner = dummy current}
309 funs = funs, 313 | leave _ = raise Fail "Corify.St.leave"
310 current = m1, 314
311 nested = rest}, 315 fun ffi m vals constructors = dummy (FFfi {mod = m, vals = vals, constructors = constructors})
312 inner = dummy current} 316
313 | leave _ = raise Fail "Corify.St.leave" 317 fun bindStr ({cons, constructors, vals, strs, funs,
314 318 current = FNormal {cons = mcons, constructors = mconstructors,
315 fun ffi m vals constructors = dummy (FFfi {mod = m, vals = vals, constructors = constructors}) 319 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
316 320 x n ({current = f, ...} : t) =
317 fun bindStr ({cons, constructors, vals, strs, funs, 321 {cons = cons,
318 current = FNormal {cons = mcons, constructors = mconstructors, 322 constructors = constructors,
319 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) 323 vals = vals,
320 x n ({current = f, ...} : t) = 324 strs = IM.insert (strs, n, f),
321 {cons = cons, 325 funs = funs,
322 constructors = constructors, 326 current = FNormal {cons = mcons,
323 vals = vals, 327 constructors = mconstructors,
324 strs = IM.insert (strs, n, f), 328 vals = mvals,
325 funs = funs, 329 strs = SM.insert (mstrs, x, f),
326 current = FNormal {cons = mcons, 330 funs = mfuns},
327 constructors = mconstructors, 331 nested = nested}
328 vals = mvals, 332 | bindStr _ _ _ _ = raise Fail "Corify.St.bindStr"
329 strs = SM.insert (mstrs, x, f), 333
330 funs = mfuns}, 334 fun lookupStrById ({strs, ...} : t) n =
331 nested = nested} 335 case IM.find (strs, n) of
332 | bindStr _ _ _ _ = raise Fail "Corify.St.bindStr" 336 NONE => raise Fail "Corify.St.lookupStrById"
333 337 | SOME f => dummy f
334 fun lookupStrById ({strs, ...} : t) n = 338
335 case IM.find (strs, n) of 339 fun lookupStrByName (m, {current = FNormal {strs, ...}, ...} : t) =
336 NONE => raise Fail "Corify.St.lookupStrById" 340 (case SM.find (strs, m) of
337 | SOME f => dummy f 341 NONE => raise Fail "Corify.St.lookupStrByName"
338 342 | SOME f => dummy f)
339 fun lookupStrByName (m, {current = FNormal {strs, ...}, ...} : t) = 343 | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName"
340 (case SM.find (strs, m) of 344
341 NONE => raise Fail "Corify.St.lookupStrByName" 345 fun bindFunctor ({cons, constructors, vals, strs, funs,
342 | SOME f => dummy f) 346 current = FNormal {cons = mcons, constructors = mconstructors,
343 | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName" 347 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
344 348 x n xa na str =
345 fun bindFunctor ({cons, constructors, vals, strs, funs, 349 {cons = cons,
346 current = FNormal {cons = mcons, constructors = mconstructors, 350 constructors = constructors,
347 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) 351 vals = vals,
348 x n xa na str = 352 strs = strs,
349 {cons = cons, 353 funs = IM.insert (funs, n, (xa, na, str)),
350 constructors = constructors, 354 current = FNormal {cons = mcons,
351 vals = vals, 355 constructors = mconstructors,
352 strs = strs, 356 vals = mvals,
353 funs = IM.insert (funs, n, (xa, na, str)), 357 strs = mstrs,
354 current = FNormal {cons = mcons, 358 funs = SM.insert (mfuns, x, (xa, na, str))},
355 constructors = mconstructors, 359 nested = nested}
356 vals = mvals, 360 | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor"
357 strs = mstrs, 361
358 funs = SM.insert (mfuns, x, (xa, na, str))}, 362 fun lookupFunctorById ({funs, ...} : t) n =
359 nested = nested} 363 case IM.find (funs, n) of
360 | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor" 364 NONE => raise Fail "Corify.St.lookupFunctorById"
361 365 | SOME v => v
362 fun lookupFunctorById ({funs, ...} : t) n = 366
363 case IM.find (funs, n) of 367 fun lookupFunctorByName (m, {current = FNormal {funs, ...}, ...} : t) =
364 NONE => raise Fail "Corify.St.lookupFunctorById" 368 (case SM.find (funs, m) of
365 | SOME v => v 369 NONE => raise Fail "Corify.St.lookupFunctorByName"
366 370 | SOME v => v)
367 fun lookupFunctorByName (m, {current = FNormal {funs, ...}, ...} : t) = 371 | lookupFunctorByName _ = raise Fail "Corify.St.lookupFunctorByName"
368 (case SM.find (funs, m) of 372
369 NONE => raise Fail "Corify.St.lookupFunctorByName" 373 end
370 | SOME v => v) 374
371 | lookupFunctorByName _ = raise Fail "Corify.St.lookupFunctorByName" 375
372 376 fun corifyKind (k, loc) =
373 end 377 case k of
374 378 L.KType => (L'.KType, loc)
375 379 | L.KArrow (k1, k2) => (L'.KArrow (corifyKind k1, corifyKind k2), loc)
376 fun corifyKind (k, loc) = 380 | L.KName => (L'.KName, loc)
377 case k of 381 | L.KRecord k => (L'.KRecord (corifyKind k), loc)
378 L.KType => (L'.KType, loc) 382 | L.KUnit => (L'.KUnit, loc)
379 | L.KArrow (k1, k2) => (L'.KArrow (corifyKind k1, corifyKind k2), loc) 383
380 | L.KName => (L'.KName, loc) 384 fun corifyCon st (c, loc) =
381 | L.KRecord k => (L'.KRecord (corifyKind k), loc) 385 case c of
382 | L.KUnit => (L'.KUnit, loc) 386 L.TFun (t1, t2) => (L'.TFun (corifyCon st t1, corifyCon st t2), loc)
383 387 | L.TCFun (x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon st t), loc)
384 fun corifyCon st (c, loc) = 388 | L.TRecord c => (L'.TRecord (corifyCon st c), loc)
385 case c of 389
386 L.TFun (t1, t2) => (L'.TFun (corifyCon st t1, corifyCon st t2), loc) 390 | L.CRel n => (L'.CRel n, loc)
387 | L.TCFun (x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon st t), loc) 391 | L.CNamed n =>
388 | L.TRecord c => (L'.TRecord (corifyCon st c), loc) 392 (case St.lookupConById st n of
389 393 NONE => (L'.CNamed n, loc)
390 | L.CRel n => (L'.CRel n, loc) 394 | SOME n => (L'.CNamed n, loc))
391 | L.CNamed n => 395 | L.CModProj (m, ms, x) =>
392 (case St.lookupConById st n of 396 let
393 NONE => (L'.CNamed n, loc) 397 val st = St.lookupStrById st m
394 | SOME n => (L'.CNamed n, loc)) 398 val st = foldl St.lookupStrByName st ms
395 | L.CModProj (m, ms, x) => 399 in
396 let 400 case St.lookupConByName st x of
397 val st = St.lookupStrById st m 401 St.CNormal n => (L'.CNamed n, loc)
398 val st = foldl St.lookupStrByName st ms 402 | St.CFfi m => (L'.CFfi (m, x), loc)
399 in 403 end
400 case St.lookupConByName st x of 404
401 St.CNormal n => (L'.CNamed n, loc) 405 | L.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc)
402 | St.CFfi m => (L'.CFfi (m, x), loc) 406 | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon st c), loc)
403 end 407
404 408 | L.CName s => (L'.CName s, loc)
405 | L.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc) 409
406 | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon st c), loc) 410 | L.CRecord (k, xcs) =>
407 411 (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc)
408 | L.CName s => (L'.CName s, loc) 412 | L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc)
409 413 | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc)
410 | L.CRecord (k, xcs) => 414 | L.CUnit => (L'.CUnit, loc)
411 (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc) 415
412 | L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc) 416 fun corifyPatCon st pc =
413 | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc) 417 case pc of
414 | L.CUnit => (L'.CUnit, loc) 418 L.PConVar n => St.lookupConstructorById st n
415 419 | L.PConProj (m1, ms, x) =>
416 fun corifyPatCon st pc = 420 let
417 case pc of 421 val st = St.lookupStrById st m1
418 L.PConVar n => St.lookupConstructorById st n 422 val st = foldl St.lookupStrByName st ms
419 | L.PConProj (m1, ms, x) => 423 in
420 let 424 St.lookupConstructorByName st x
421 val st = St.lookupStrById st m1 425 end
422 val st = foldl St.lookupStrByName st ms 426
423 in 427 fun corifyPat st (p, loc) =
424 St.lookupConstructorByName st x 428 case p of
425 end 429 L.PWild => (L'.PWild, loc)
426 430 | L.PVar (x, t) => (L'.PVar (x, corifyCon st t), loc)
427 fun corifyPat st (p, loc) = 431 | L.PPrim p => (L'.PPrim p, loc)
428 case p of 432 | L.PCon (dk, pc, po) => (L'.PCon (dk, corifyPatCon st pc, Option.map (corifyPat st) po), loc)
429 L.PWild => (L'.PWild, loc) 433 | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, corifyPat st p, corifyCon st t)) xps), loc)
430 | L.PVar (x, t) => (L'.PVar (x, corifyCon st t), loc) 434
431 | L.PPrim p => (L'.PPrim p, loc) 435 fun corifyExp st (e, loc) =
432 | L.PCon (pc, po) => (L'.PCon (corifyPatCon st pc, Option.map (corifyPat st) po), loc) 436 case e of
433 | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, corifyPat st p, corifyCon st t)) xps), loc) 437 L.EPrim p => (L'.EPrim p, loc)
434 438 | L.ERel n => (L'.ERel n, loc)
435 fun corifyExp st (e, loc) = 439 | L.ENamed n =>
436 case e of 440 (case St.lookupValById st n of
437 L.EPrim p => (L'.EPrim p, loc) 441 NONE => (L'.ENamed n, loc)
438 | L.ERel n => (L'.ERel n, loc) 442 | SOME n => (L'.ENamed n, loc))
439 | L.ENamed n => 443 | L.EModProj (m, ms, x) =>
440 (case St.lookupValById st n of 444 let
441 NONE => (L'.ENamed n, loc) 445 val st = St.lookupStrById st m
442 | SOME n => (L'.ENamed n, loc)) 446 val st = foldl St.lookupStrByName st ms
443 | L.EModProj (m, ms, x) => 447 in
444 let 448 case St.lookupConstructorByNameOpt st x of
445 val st = St.lookupStrById st m 449 SOME (pc as L'.PConFfi {mod = m, datatyp, arg, kind, ...}) =>
446 val st = foldl St.lookupStrByName st ms 450 (case arg of
447 in 451 NONE => (L'.ECon (kind, pc, NONE), loc)
448 case St.lookupConstructorByNameOpt st x of 452 | SOME dom => (L'.EAbs ("x", dom, (L'.CFfi (m, datatyp), loc),
449 SOME (pc as L'.PConFfi {mod = m, datatyp, arg, ...}) => 453 (L'.ECon (kind, pc, SOME (L'.ERel 0, loc)), loc)), loc))
450 (case arg of 454 | _ =>
451 NONE => (L'.ECon (pc, NONE), loc) 455 case St.lookupValByName st x of
452 | SOME dom => (L'.EAbs ("x", dom, (L'.CFfi (m, datatyp), loc), 456 St.ENormal n => (L'.ENamed n, loc)
453 (L'.ECon (pc, SOME (L'.ERel 0, loc)), loc)), loc)) 457 | St.EFfi (m, t) =>
454 | _ => 458 case t of
455 case St.lookupValByName st x of 459 (L'.TFun (dom as (L'.TRecord (L'.CRecord (_, []), _), _), ran), _) =>
456 St.ENormal n => (L'.ENamed n, loc) 460 (L'.EAbs ("arg", dom, ran, (L'.EFfiApp (m, x, []), loc)), loc)
457 | St.EFfi (m, t) => 461 | t as (L'.TFun _, _) =>
458 case t of 462 let
459 (L'.TFun (dom as (L'.TRecord (L'.CRecord (_, []), _), _), ran), _) => 463 fun getArgs (all as (t, _), args) =
460 (L'.EAbs ("arg", dom, ran, (L'.EFfiApp (m, x, []), loc)), loc) 464 case t of
461 | t as (L'.TFun _, _) => 465 L'.TFun (dom, ran) => getArgs (ran, dom :: args)
462 let 466 | _ => (all, rev args)
463 fun getArgs (all as (t, _), args) = 467
464 case t of 468 val (result, args) = getArgs (t, [])
465 L'.TFun (dom, ran) => getArgs (ran, dom :: args) 469
466 | _ => (all, rev args) 470 val (actuals, _) = foldr (fn (_, (actuals, n)) =>
467 471 ((L'.ERel n, loc) :: actuals,
468 val (result, args) = getArgs (t, []) 472 n + 1)) ([], 0) args
469 473 val app = (L'.EFfiApp (m, x, actuals), loc)
470 val (actuals, _) = foldr (fn (_, (actuals, n)) => 474 val (abs, _, _) = foldr (fn (t, (abs, ran, n)) =>
471 ((L'.ERel n, loc) :: actuals, 475 ((L'.EAbs ("arg" ^ Int.toString n,
472 n + 1)) ([], 0) args 476 t,
473 val app = (L'.EFfiApp (m, x, actuals), loc) 477 ran,
474 val (abs, _, _) = foldr (fn (t, (abs, ran, n)) => 478 abs), loc),
475 ((L'.EAbs ("arg" ^ Int.toString n, 479 (L'.TFun (t, ran), loc),
476 t, 480 n - 1)) (app, result, length args - 1) args
477 ran, 481 in
478 abs), loc), 482 abs
479 (L'.TFun (t, ran), loc), 483 end
480 n - 1)) (app, result, length args - 1) args 484 | _ => (L'.EFfi (m, x), loc)
481 in 485 end
482 abs 486 | L.EApp (e1, e2) => (L'.EApp (corifyExp st e1, corifyExp st e2), loc)
483 end 487 | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon st dom, corifyCon st ran, corifyExp st e1), loc)
484 | _ => (L'.EFfi (m, x), loc) 488 | L.ECApp (e1, c) => (L'.ECApp (corifyExp st e1, corifyCon st c), loc)
485 end 489 | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc)
486 | L.EApp (e1, e2) => (L'.EApp (corifyExp st e1, corifyExp st e2), loc) 490
487 | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon st dom, corifyCon st ran, corifyExp st e1), loc) 491 | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) =>
488 | L.ECApp (e1, c) => (L'.ECApp (corifyExp st e1, corifyCon st c), loc) 492 (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc)
489 | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc) 493 | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c,
490 494 {field = corifyCon st field, rest = corifyCon st rest}), loc)
491 | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) => 495 | L.ECut (e1, c, {field, rest}) => (L'.ECut (corifyExp st e1, corifyCon st c,
492 (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc) 496 {field = corifyCon st field, rest = corifyCon st rest}), loc)
493 | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c, 497 | L.EFold k => (L'.EFold (corifyKind k), loc)
494 {field = corifyCon st field, rest = corifyCon st rest}), loc) 498
495 | L.ECut (e1, c, {field, rest}) => (L'.ECut (corifyExp st e1, corifyCon st c, 499 | L.ECase (e, pes, {disc, result}) =>
496 {field = corifyCon st field, rest = corifyCon st rest}), loc) 500 (L'.ECase (corifyExp st e,
497 | L.EFold k => (L'.EFold (corifyKind k), loc) 501 map (fn (p, e) => (corifyPat st p, corifyExp st e)) pes,
498 502 {disc = corifyCon st disc, result = corifyCon st result}),
499 | L.ECase (e, pes, {disc, result}) => 503 loc)
500 (L'.ECase (corifyExp st e, 504
501 map (fn (p, e) => (corifyPat st p, corifyExp st e)) pes, 505 | L.EWrite e => (L'.EWrite (corifyExp st e), loc)
502 {disc = corifyCon st disc, result = corifyCon st result}), 506
503 loc) 507 fun corifyDecl ((d, loc : EM.span), st) =
504 508 case d of
505 | L.EWrite e => (L'.EWrite (corifyExp st e), loc) 509 L.DCon (x, n, k, c) =>
506 510 let
507 fun corifyDecl ((d, loc : EM.span), st) = 511 val (st, n) = St.bindCon st x n
508 case d of 512 in
509 L.DCon (x, n, k, c) => 513 ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st)
510 let 514 end
511 val (st, n) = St.bindCon st x n 515 | L.DDatatype (x, n, xncs) =>
512 in 516 let
513 ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st) 517 val (st, n) = St.bindCon st x n
514 end 518 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
515 | L.DDatatype (x, n, xncs) => 519 let
516 let 520 val st = St.bindConstructor st x n (L'.PConVar n)
517 val (st, n) = St.bindCon st x n 521 val st = St.bindConstructorVal st x n
518 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => 522 val co = Option.map (corifyCon st) co
519 let 523 in
520 val st = St.bindConstructor st x n (L'.PConVar n) 524 ((x, n, co), st)
521 val st = St.bindConstructorVal st x n 525 end) st xncs
522 val co = Option.map (corifyCon st) co 526
523 in 527 val dk = CoreUtil.classifyDatatype xncs
524 ((x, n, co), st) 528 val t = (L'.CNamed n, loc)
525 end) st xncs 529 val dcons = map (fn (x, n, to) =>
526 530 let
527 val t = (L'.CNamed n, loc) 531 val (e, t) =
528 val dcons = map (fn (x, n, to) => 532 case to of
529 let 533 NONE => ((L'.ECon (dk, L'.PConVar n, NONE), loc), t)
530 val (e, t) = 534 | SOME t' => ((L'.EAbs ("x", t', t,
531 case to of 535 (L'.ECon (dk, L'.PConVar n, SOME (L'.ERel 0, loc)),
532 NONE => ((L'.ECon (L'.PConVar n, NONE), loc), t) 536 loc)),
533 | SOME t' => ((L'.EAbs ("x", t', t, 537 loc),
534 (L'.ECon (L'.PConVar n, SOME (L'.ERel 0, loc)), loc)), 538 (L'.TFun (t', t), loc))
535 loc), 539 in
536 (L'.TFun (t', t), loc)) 540 (L'.DVal (x, n, t, e, ""), loc)
537 in 541 end) xncs
538 (L'.DVal (x, n, t, e, ""), loc) 542 in
539 end) xncs 543 ((L'.DDatatype (x, n, xncs), loc) :: dcons, st)
540 in 544 end
541 ((L'.DDatatype (x, n, xncs), loc) :: dcons, st) 545 | L.DDatatypeImp (x, n, m1, ms, s, xncs) =>
542 end 546 let
543 | L.DDatatypeImp (x, n, m1, ms, s, xncs) => 547 val (st, n) = St.bindCon st x n
544 let 548 val c = corifyCon st (L.CModProj (m1, ms, s), loc)
545 val (st, n) = St.bindCon st x n 549
546 val c = corifyCon st (L.CModProj (m1, ms, s), loc) 550 val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms
547 551 val (_, {inner, ...}) = corifyStr (m, st)
548 val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms 552
549 val (_, {inner, ...}) = corifyStr (m, st) 553 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
550 554 let
551 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => 555 val n' = St.lookupConstructorByName inner x
552 let 556 val st = St.bindConstructor st x n n'
553 val n' = St.lookupConstructorByName inner x 557 val (st, n) = St.bindVal st x n
554 val st = St.bindConstructor st x n n' 558 val co = Option.map (corifyCon st) co
555 val (st, n) = St.bindVal st x n 559 in
556 val co = Option.map (corifyCon st) co 560 ((x, n, co), st)
557 in 561 end) st xncs
558 ((x, n, co), st) 562
559 end) st xncs 563 val cds = map (fn (x, n, co) =>
560 564 let
561 val cds = map (fn (x, n, co) => 565 val t = case co of
562 let 566 NONE => c
563 val t = case co of 567 | SOME t' => (L'.TFun (t', c), loc)
564 NONE => c 568 val e = corifyExp st (L.EModProj (m1, ms, x), loc)
565 | SOME t' => (L'.TFun (t', c), loc) 569 in
566 val e = corifyExp st (L.EModProj (m1, ms, x), loc) 570 (L'.DVal (x, n, t, e, x), loc)
567 in 571 end) xncs
568 (L'.DVal (x, n, t, e, x), loc) 572 in
569 end) xncs 573 ((L'.DCon (x, n, (L'.KType, loc), c), loc) :: cds, st)
570 in 574 end
571 ((L'.DCon (x, n, (L'.KType, loc), c), loc) :: cds, st) 575 | L.DVal (x, n, t, e) =>
572 end 576 let
573 | L.DVal (x, n, t, e) => 577 val (st, n) = St.bindVal st x n
574 let 578 val s =
575 val (st, n) = St.bindVal st x n 579 if String.isPrefix "wrap_" x then
576 val s = 580 String.extract (x, 5, NONE)
577 if String.isPrefix "wrap_" x then 581 else
578 String.extract (x, 5, NONE) 582 x
579 else 583 in
580 x 584 ([(L'.DVal (x, n, corifyCon st t, corifyExp st e, s), loc)], st)
581 in 585 end
582 ([(L'.DVal (x, n, corifyCon st t, corifyExp st e, s), loc)], st) 586 | L.DValRec vis =>
583 end 587 let
584 | L.DValRec vis => 588 val (vis, st) = ListUtil.foldlMap
585 let 589 (fn ((x, n, t, e), st) =>
586 val (vis, st) = ListUtil.foldlMap 590 let
587 (fn ((x, n, t, e), st) => 591 val (st, n) = St.bindVal st x n
592 in
593 ((x, n, t, e), st)
594 end)
595 st vis
596
597 val vis = map
598 (fn (x, n, t, e) =>
599 let
600 val s =
601 if String.isPrefix "wrap_" x then
602 String.extract (x, 5, NONE)
603 else
604 x
605 in
606 (x, n, corifyCon st t, corifyExp st e, s)
607 end)
608 vis
609 in
610 ([(L'.DValRec vis, loc)], st)
611 end
612 | L.DSgn _ => ([], st)
613
614 | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) =>
615 ([], St.bindFunctor st x n xa na str)
616
617 | L.DStr (x, n, _, str) =>
618 let
619 val (ds, {inner, outer}) = corifyStr (str, st)
620 val st = St.bindStr outer x n inner
621 in
622 (ds, st)
623 end
624
625 | L.DFfiStr (m, n, (sgn, _)) =>
626 (case sgn of
627 L.SgnConst sgis =>
628 let
629 val (ds, cmap, conmap, st) =
630 foldl (fn ((sgi, _), (ds, cmap, conmap, st)) =>
631 case sgi of
632 L.SgiConAbs (x, n, k) =>
588 let 633 let
589 val (st, n) = St.bindVal st x n 634 val (st, n') = St.bindCon st x n
590 in 635 in
591 ((x, n, t, e), st) 636 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
592 end) 637 cmap,
593 st vis 638 conmap,
594 639 st)
595 val vis = map 640 end
596 (fn (x, n, t, e) => 641 | L.SgiCon (x, n, k, _) =>
597 let 642 let
598 val s = 643 val (st, n') = St.bindCon st x n
599 if String.isPrefix "wrap_" x then 644 in
600 String.extract (x, 5, NONE) 645 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
601 else 646 cmap,
602 x 647 conmap,
603 in 648 st)
604 (x, n, corifyCon st t, corifyExp st e, s) 649 end
605 end) 650
606 vis 651 | L.SgiDatatype (x, n, xnts) =>
607 in 652 let
608 ([(L'.DValRec vis, loc)], st) 653 val dk = ExplUtil.classifyDatatype xnts
609 end 654 val (st, n') = St.bindCon st x n
610 | L.DSgn _ => ([], st) 655 val (xnts, (ds', st, cmap, conmap)) =
611 656 ListUtil.foldlMap
612 | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) => 657 (fn ((x', n, to), (ds', st, cmap, conmap)) =>
613 ([], St.bindFunctor st x n xa na str) 658 let
614 659 val dt = (L'.CNamed n', loc)
615 | L.DStr (x, n, _, str) => 660
616 let 661 val to = Option.map (corifyCon st) to
617 val (ds, {inner, outer}) = corifyStr (str, st) 662
618 val st = St.bindStr outer x n inner 663 val pc = L'.PConFfi {mod = m,
619 in 664 datatyp = x,
620 (ds, st) 665 con = x',
621 end 666 arg = to,
622 667 kind = dk}
623 | L.DFfiStr (m, n, (sgn, _)) => 668
624 (case sgn of 669 val (cmap, d) =
625 L.SgnConst sgis => 670 case to of
626 let 671 NONE => (SM.insert (cmap, x', dt),
627 val (ds, cmap, conmap, st) = 672 (L'.DVal (x', n, dt,
628 foldl (fn ((sgi, _), (ds, cmap, conmap, st)) => 673 (L'.ECon (dk, pc, NONE), loc),
629 case sgi of 674 ""), loc))
630 L.SgiConAbs (x, n, k) => 675 | SOME t =>
631 let 676 let
632 val (st, n') = St.bindCon st x n 677 val tf = (L'.TFun (t, dt), loc)
633 in 678 val d = (L'.DVal (x', n, tf,
634 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, 679 (L'.EAbs ("x", t, tf,
635 cmap, 680 (L'.ECon (dk, pc,
636 conmap, 681 SOME (L'.ERel 0,
637 st)
638 end
639 | L.SgiCon (x, n, k, _) =>
640 let
641 val (st, n') = St.bindCon st x n
642 in
643 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
644 cmap,
645 conmap,
646 st)
647 end
648
649 | L.SgiDatatype (x, n, xnts) =>
650 let
651 val (st, n') = St.bindCon st x n
652 val (xnts, (ds', st, cmap, conmap)) =
653 ListUtil.foldlMap
654 (fn ((x', n, to), (ds', st, cmap, conmap)) =>
655 let
656 val dt = (L'.CNamed n', loc)
657
658 val to = Option.map (corifyCon st) to
659
660 val pc = L'.PConFfi {mod = m,
661 datatyp = x,
662 con = x',
663 arg = to}
664
665 val (cmap, d) =
666 case to of
667 NONE => (SM.insert (cmap, x', dt),
668 (L'.DVal (x', n, dt,
669 (L'.ECon (pc, NONE), loc),
670 ""), loc))
671 | SOME t =>
672 let
673 val tf = (L'.TFun (t, dt), loc)
674 val d = (L'.DVal (x', n, tf,
675 (L'.EAbs ("x", t, tf,
676 (L'.ECon (pc,
677 SOME (L'.ERel 0,
678 loc)), 682 loc)),
679 loc)), loc), ""), loc) 683 loc)), loc), ""), loc)
680 in 684 in
681 (SM.insert (cmap, x', tf), d) 685 (SM.insert (cmap, x', tf), d)
682 end 686 end
683 687
684 val st = St.bindConstructor st x' n pc 688 val st = St.bindConstructor st x' n pc
685 (*val st = St.bindConstructorVal st x' n*) 689 (*val st = St.bindConstructorVal st x' n*)
686 690
687 val conmap = SM.insert (conmap, x', (x, to)) 691 val conmap = SM.insert (conmap, x', (x, to, dk))
688 in 692 in
689 ((x', n, to), 693 ((x', n, to),
690 (d :: ds', st, cmap, conmap)) 694 (d :: ds', st, cmap, conmap))
691 end) ([], st, cmap, conmap) xnts 695 end) ([], st, cmap, conmap) xnts
692 in 696 in