Mercurial > urweb

comparison src/corify.sml @ 177:5d030ee143e2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Case through corify
author Adam Chlipala <adamc@hcoop.net>
date Sat, 02 Aug 2008 11:15:32 -0400
parents 33d4a8eea484
children d11754ffe252
comparison
equal deleted inserted replaced
176:33d4a8eea484 177:5d030ee143e2
69 | CFfi of string 69 | CFfi of string
70 val bindCon : t -> string -> int -> t * int 70 val bindCon : t -> string -> int -> t * int
71 val lookupConById : t -> int -> int option 71 val lookupConById : t -> int -> int option
72 val lookupConByName : t -> string -> core_con 72 val lookupConByName : t -> string -> core_con
73 73
74 val bindConstructor : t -> string -> int -> L'.patCon -> t
75 val lookupConstructorByName : t -> string -> L'.patCon
76 val lookupConstructorById : t -> int -> L'.patCon
77
74 datatype core_val = 78 datatype core_val =
75 ENormal of int 79 ENormal of int
76 | EFfi of string * L'.con 80 | EFfi of string * L'.con
77 val bindVal : t -> string -> int -> t * int 81 val bindVal : t -> string -> int -> t * int
78 val bindConstructor : t -> string -> int -> t 82 val bindConstructorVal : t -> string -> int -> t
79 val lookupValById : t -> int -> int option 83 val lookupValById : t -> int -> int option
80 val lookupValByName : t -> string -> core_val 84 val lookupValByName : t -> string -> core_val
81 85
82 val bindStr : t -> string -> int -> t -> t 86 val bindStr : t -> string -> int -> t -> t
83 val lookupStrById : t -> int -> t 87 val lookupStrById : t -> int -> t
88 val lookupFunctorByName : string * t -> string * int * L.str 92 val lookupFunctorByName : string * t -> string * int * L.str
89 end = struct 93 end = struct
90 94
91 datatype flattening = 95 datatype flattening =
92 FNormal of {cons : int SM.map, 96 FNormal of {cons : int SM.map,
97 constructors : L'.patCon SM.map,
93 vals : int SM.map, 98 vals : int SM.map,
94 strs : flattening SM.map, 99 strs : flattening SM.map,
95 funs : (string * int * L.str) SM.map} 100 funs : (string * int * L.str) SM.map}
96 | FFfi of {mod : string, 101 | FFfi of {mod : string,
97 vals : L'.con SM.map} 102 vals : L'.con SM.map}
98 103
99 type t = { 104 type t = {
100 cons : int IM.map, 105 cons : int IM.map,
106 constructors : L'.patCon IM.map,
101 vals : int IM.map, 107 vals : int IM.map,
102 strs : flattening IM.map, 108 strs : flattening IM.map,
103 funs : (string * int * L.str) IM.map, 109 funs : (string * int * L.str) IM.map,
104 current : flattening, 110 current : flattening,
105 nested : flattening list 111 nested : flattening list
106 } 112 }
107 113
108 val empty = { 114 val empty = {
109 cons = IM.empty, 115 cons = IM.empty,
116 constructors = IM.empty,
110 vals = IM.empty, 117 vals = IM.empty,
111 strs = IM.empty, 118 strs = IM.empty,
112 funs = IM.empty, 119 funs = IM.empty,
113 current = FNormal { cons = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty }, 120 current = FNormal { cons = SM.empty, constructors = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty },
114 nested = [] 121 nested = []
115 } 122 }
116 123
117 fun debug ({current = FNormal {cons, vals, strs, funs}, ...} : t) = 124 fun debug ({current = FNormal {cons, constructors, vals, strs, funs}, ...} : t) =
118 print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; " 125 print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; "
126 ^ "constructors: " ^ Int.toString (SM.numItems constructors) ^ "; "
119 ^ "vals: " ^ Int.toString (SM.numItems vals) ^ "; " 127 ^ "vals: " ^ Int.toString (SM.numItems vals) ^ "; "
120 ^ "strs: " ^ Int.toString (SM.numItems strs) ^ "; " 128 ^ "strs: " ^ Int.toString (SM.numItems strs) ^ "; "
121 ^ "funs: " ^ Int.toString (SM.numItems funs) ^ "\n") 129 ^ "funs: " ^ Int.toString (SM.numItems funs) ^ "\n")
122 | debug _ = print "Not normal!\n" 130 | debug _ = print "Not normal!\n"
123 131
127 135
128 datatype core_val = 136 datatype core_val =
129 ENormal of int 137 ENormal of int
130 | EFfi of string * L'.con 138 | EFfi of string * L'.con
131 139
132 fun bindCon {cons, vals, strs, funs, current, nested} s n = 140 fun bindCon {cons, constructors, vals, strs, funs, current, nested} s n =
133 let 141 let
134 val n' = alloc () 142 val n' = alloc ()
135 143
136 val current = 144 val current =
137 case current of 145 case current of
138 FFfi _ => raise Fail "Binding inside FFfi" 146 FFfi _ => raise Fail "Binding inside FFfi"
139 | FNormal {cons, vals, strs, funs} => 147 | FNormal {cons, constructors, vals, strs, funs} =>
140 FNormal {cons = SM.insert (cons, s, n'), 148 FNormal {cons = SM.insert (cons, s, n'),
149 constructors = constructors,
141 vals = vals, 150 vals = vals,
142 strs = strs, 151 strs = strs,
143 funs = funs} 152 funs = funs}
144 in 153 in
145 ({cons = IM.insert (cons, n, n'), 154 ({cons = IM.insert (cons, n, n'),
155 constructors = constructors,
146 vals = vals, 156 vals = vals,
147 strs = strs, 157 strs = strs,
148 funs = funs, 158 funs = funs,
149 current = current, 159 current = current,
150 nested = nested}, 160 nested = nested},
159 | FNormal {cons, ...} => 169 | FNormal {cons, ...} =>
160 case SM.find (cons, x) of 170 case SM.find (cons, x) of
161 NONE => raise Fail "Corify.St.lookupConByName" 171 NONE => raise Fail "Corify.St.lookupConByName"
162 | SOME n => CNormal n 172 | SOME n => CNormal n
163 173
164 fun bindVal {cons, vals, strs, funs, current, nested} s n = 174 fun bindVal {cons, constructors, vals, strs, funs, current, nested} s n =
165 let 175 let
166 val n' = alloc () 176 val n' = alloc ()
167 177
168 val current = 178 val current =
169 case current of 179 case current of
170 FFfi _ => raise Fail "Binding inside FFfi" 180 FFfi _ => raise Fail "Binding inside FFfi"
171 | FNormal {cons, vals, strs, funs} => 181 | FNormal {cons, constructors, vals, strs, funs} =>
172 FNormal {cons = cons, 182 FNormal {cons = cons,
183 constructors = constructors,
173 vals = SM.insert (vals, s, n'), 184 vals = SM.insert (vals, s, n'),
174 strs = strs, 185 strs = strs,
175 funs = funs} 186 funs = funs}
176 in 187 in
177 ({cons = cons, 188 ({cons = cons,
189 constructors = constructors,
178 vals = IM.insert (vals, n, n'), 190 vals = IM.insert (vals, n, n'),
179 strs = strs, 191 strs = strs,
180 funs = funs, 192 funs = funs,
181 current = current, 193 current = current,
182 nested = nested}, 194 nested = nested},
183 n') 195 n')
184 end 196 end
185 197
186 fun bindConstructor {cons, vals, strs, funs, current, nested} s n = 198 fun bindConstructorVal {cons, constructors, vals, strs, funs, current, nested} s n =
187 let 199 let
188 val current = 200 val current =
189 case current of 201 case current of
190 FFfi _ => raise Fail "Binding inside FFfi" 202 FFfi _ => raise Fail "Binding inside FFfi"
191 | FNormal {cons, vals, strs, funs} => 203 | FNormal {cons, constructors, vals, strs, funs} =>
192 FNormal {cons = cons, 204 FNormal {cons = cons,
205 constructors = constructors,
193 vals = SM.insert (vals, s, n), 206 vals = SM.insert (vals, s, n),
194 strs = strs, 207 strs = strs,
195 funs = funs} 208 funs = funs}
196 in 209 in
197 {cons = cons, 210 {cons = cons,
211 constructors = constructors,
198 vals = IM.insert (vals, n, n), 212 vals = IM.insert (vals, n, n),
199 strs = strs, 213 strs = strs,
200 funs = funs, 214 funs = funs,
201 current = current, 215 current = current,
202 nested = nested} 216 nested = nested}
203 end 217 end
218
204 219
205 fun lookupValById ({vals, ...} : t) n = IM.find (vals, n) 220 fun lookupValById ({vals, ...} : t) n = IM.find (vals, n)
206 221
207 fun lookupValByName ({current, ...} : t) x = 222 fun lookupValByName ({current, ...} : t) x =
208 case current of 223 case current of
213 | FNormal {vals, ...} => 228 | FNormal {vals, ...} =>
214 case SM.find (vals, x) of 229 case SM.find (vals, x) of
215 NONE => raise Fail "Corify.St.lookupValByName" 230 NONE => raise Fail "Corify.St.lookupValByName"
216 | SOME n => ENormal n 231 | SOME n => ENormal n
217 232
218 fun enter {cons, vals, strs, funs, current, nested} = 233 fun bindConstructor {cons, constructors, vals, strs, funs, current, nested} s n n' =
234 let
235 val current =
236 case current of
237 FFfi _ => raise Fail "Binding inside FFfi"
238 | FNormal {cons, constructors, vals, strs, funs} =>
239 FNormal {cons = cons,
240 constructors = SM.insert (constructors, s, n'),
241 vals = vals,
242 strs = strs,
243 funs = funs}
244 in
245 {cons = cons,
246 constructors = IM.insert (constructors, n, n'),
247 vals = vals,
248 strs = strs,
249 funs = funs,
250 current = current,
251 nested = nested}
252 end
253
254 fun lookupConstructorById ({constructors, ...} : t) n =
255 case IM.find (constructors, n) of
256 NONE => raise Fail "Corify.St.lookupConstructorById"
257 | SOME x => x
258
259 fun lookupConstructorByName ({current, ...} : t) x =
260 case current of
261 FFfi {mod = m, ...} => L'.PConFfi (m, x)
262 | FNormal {constructors, ...} =>
263 case SM.find (constructors, x) of
264 NONE => raise Fail "Corify.St.lookupConstructorByName"
265 | SOME n => n
266
267 fun enter {cons, constructors, vals, strs, funs, current, nested} =
219 {cons = cons, 268 {cons = cons,
269 constructors = constructors,
220 vals = vals, 270 vals = vals,
221 strs = strs, 271 strs = strs,
222 funs = funs, 272 funs = funs,
223 current = FNormal {cons = SM.empty, 273 current = FNormal {cons = SM.empty,
274 constructors = SM.empty,
224 vals = SM.empty, 275 vals = SM.empty,
225 strs = SM.empty, 276 strs = SM.empty,
226 funs = SM.empty}, 277 funs = SM.empty},
227 nested = current :: nested} 278 nested = current :: nested}
228 279
229 fun dummy f = {cons = IM.empty, 280 fun dummy f = {cons = IM.empty,
281 constructors = IM.empty,
230 vals = IM.empty, 282 vals = IM.empty,
231 strs = IM.empty, 283 strs = IM.empty,
232 funs = IM.empty, 284 funs = IM.empty,
233 current = f, 285 current = f,
234 nested = []} 286 nested = []}
235 287
236 fun leave {cons, vals, strs, funs, current, nested = m1 :: rest} = 288 fun leave {cons, constructors, vals, strs, funs, current, nested = m1 :: rest} =
237 {outer = {cons = cons, 289 {outer = {cons = cons,
290 constructors = constructors,
238 vals = vals, 291 vals = vals,
239 strs = strs, 292 strs = strs,
240 funs = funs, 293 funs = funs,
241 current = m1, 294 current = m1,
242 nested = rest}, 295 nested = rest},
243 inner = dummy current} 296 inner = dummy current}
244 | leave _ = raise Fail "Corify.St.leave" 297 | leave _ = raise Fail "Corify.St.leave"
245 298
246 fun ffi m vals = dummy (FFfi {mod = m, vals = vals}) 299 fun ffi m vals = dummy (FFfi {mod = m, vals = vals})
247 300
248 fun bindStr ({cons, vals, strs, funs, 301 fun bindStr ({cons, constructors, vals, strs, funs,
249 current = FNormal {cons = mcons, vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) 302 current = FNormal {cons = mcons, constructors = mconstructors,
303 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
250 x n ({current = f, ...} : t) = 304 x n ({current = f, ...} : t) =
251 {cons = cons, 305 {cons = cons,
306 constructors = constructors,
252 vals = vals, 307 vals = vals,
253 strs = IM.insert (strs, n, f), 308 strs = IM.insert (strs, n, f),
254 funs = funs, 309 funs = funs,
255 current = FNormal {cons = mcons, 310 current = FNormal {cons = mcons,
311 constructors = mconstructors,
256 vals = mvals, 312 vals = mvals,
257 strs = SM.insert (mstrs, x, f), 313 strs = SM.insert (mstrs, x, f),
258 funs = mfuns}, 314 funs = mfuns},
259 nested = nested} 315 nested = nested}
260 | bindStr _ _ _ _ = raise Fail "Corify.St.bindStr" 316 | bindStr _ _ _ _ = raise Fail "Corify.St.bindStr"
268 (case SM.find (strs, m) of 324 (case SM.find (strs, m) of
269 NONE => raise Fail "Corify.St.lookupStrByName" 325 NONE => raise Fail "Corify.St.lookupStrByName"
270 | SOME f => dummy f) 326 | SOME f => dummy f)
271 | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName" 327 | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName"
272 328
273 fun bindFunctor ({cons, vals, strs, funs, 329 fun bindFunctor ({cons, constructors, vals, strs, funs,
274 current = FNormal {cons = mcons, vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) 330 current = FNormal {cons = mcons, constructors = mconstructors,
331 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
275 x n xa na str = 332 x n xa na str =
276 {cons = cons, 333 {cons = cons,
334 constructors = constructors,
277 vals = vals, 335 vals = vals,
278 strs = strs, 336 strs = strs,
279 funs = IM.insert (funs, n, (xa, na, str)), 337 funs = IM.insert (funs, n, (xa, na, str)),
280 current = FNormal {cons = mcons, 338 current = FNormal {cons = mcons,
339 constructors = mconstructors,
281 vals = mvals, 340 vals = mvals,
282 strs = mstrs, 341 strs = mstrs,
283 funs = SM.insert (mfuns, x, (xa, na, str))}, 342 funs = SM.insert (mfuns, x, (xa, na, str))},
284 nested = nested} 343 nested = nested}
285 | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor" 344 | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor"
335 | L.CRecord (k, xcs) => 394 | L.CRecord (k, xcs) =>
336 (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc) 395 (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc)
337 | L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc) 396 | L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc)
338 | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc) 397 | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc)
339 | L.CUnit => (L'.CUnit, loc) 398 | L.CUnit => (L'.CUnit, loc)
399
400 fun corifyPatCon st pc =
401 case pc of
402 L.PConVar n => St.lookupConstructorById st n
403 | L.PConProj (m1, ms, x) =>
404 let
405 val st = St.lookupStrById st m1
406 val st = foldl St.lookupStrByName st ms
407 in
408 St.lookupConstructorByName st x
409 end
410
411 fun corifyPat st (p, loc) =
412 case p of
413 L.PWild => (L'.PWild, loc)
414 | L.PVar x => (L'.PVar x, loc)
415 | L.PPrim p => (L'.PPrim p, loc)
416 | L.PCon (pc, po) => (L'.PCon (corifyPatCon st pc, Option.map (corifyPat st) po), loc)
417 | L.PRecord xps => (L'.PRecord (map (fn (x, p) => (x, corifyPat st p)) xps), loc)
340 418
341 fun corifyExp st (e, loc) = 419 fun corifyExp st (e, loc) =
342 case e of 420 case e of
343 L.EPrim p => (L'.EPrim p, loc) 421 L.EPrim p => (L'.EPrim p, loc)
344 | L.ERel n => (L'.ERel n, loc) 422 | L.ERel n => (L'.ERel n, loc)
392 | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c, 470 | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c,
393 {field = corifyCon st field, rest = corifyCon st rest}), loc) 471 {field = corifyCon st field, rest = corifyCon st rest}), loc)
394 | L.ECut (e1, c, {field, rest}) => (L'.ECut (corifyExp st e1, corifyCon st c, 472 | L.ECut (e1, c, {field, rest}) => (L'.ECut (corifyExp st e1, corifyCon st c,
395 {field = corifyCon st field, rest = corifyCon st rest}), loc) 473 {field = corifyCon st field, rest = corifyCon st rest}), loc)
396 | L.EFold k => (L'.EFold (corifyKind k), loc) 474 | L.EFold k => (L'.EFold (corifyKind k), loc)
397 | L.ECase _ => raise Fail "Corify ECase" 475
476 | L.ECase (e, pes, t) => (L'.ECase (corifyExp st e,
477 map (fn (p, e) => (corifyPat st p, corifyExp st e)) pes,
478 corifyCon st t),
479 loc)
480
398 | L.EWrite e => (L'.EWrite (corifyExp st e), loc) 481 | L.EWrite e => (L'.EWrite (corifyExp st e), loc)
399 482
400 fun corifyDecl ((d, loc : EM.span), st) = 483 fun corifyDecl ((d, loc : EM.span), st) =
401 case d of 484 case d of
402 L.DCon (x, n, k, c) => 485 L.DCon (x, n, k, c) =>
408 | L.DDatatype (x, n, xncs) => 491 | L.DDatatype (x, n, xncs) =>
409 let 492 let
410 val (st, n) = St.bindCon st x n 493 val (st, n) = St.bindCon st x n
411 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => 494 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
412 let 495 let
413 val st = St.bindConstructor st x n 496 val st = St.bindConstructor st x n (L'.PConVar n)
497 val st = St.bindConstructorVal st x n
414 val co = Option.map (corifyCon st) co 498 val co = Option.map (corifyCon st) co
415 in 499 in
416 ((x, n, co), st) 500 ((x, n, co), st)
417 end) st xncs 501 end) st xncs
418 in 502
419 ([(L'.DDatatype (x, n, xncs), loc)], st) 503 val t = (L'.CNamed n, loc)
504 val dcons = map (fn (x, n, to) =>
505 let
506 val (e, t) =
507 case to of
508 NONE => ((L'.ECon (n, NONE), loc), t)
509 | SOME t' => ((L'.EAbs ("x", t', t,
510 (L'.ECon (n, SOME (L'.ERel 0, loc)), loc)),
511 loc),
512 (L'.TFun (t', t), loc))
513 in
514 (L'.DVal (x, n, t, e, ""), loc)
515 end) xncs
516 in
517 ((L'.DDatatype (x, n, xncs), loc) :: dcons, st)
420 end 518 end
421 | L.DDatatypeImp (x, n, m1, ms, s, xncs) => 519 | L.DDatatypeImp (x, n, m1, ms, s, xncs) =>
422 let 520 let
423 val (st, n) = St.bindCon st x n 521 val (st, n) = St.bindCon st x n
424 val c = corifyCon st (L.CModProj (m1, ms, s), loc) 522 val c = corifyCon st (L.CModProj (m1, ms, s), loc)
425 523
524 val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms
525 val (_, {inner, ...}) = corifyStr (m, st)
526
426 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => 527 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
427 let 528 let
529 val n' = St.lookupConstructorByName inner x
530 val st = St.bindConstructor st x n n'
428 val (st, n) = St.bindVal st x n 531 val (st, n) = St.bindVal st x n
429 val co = Option.map (corifyCon st) co 532 val co = Option.map (corifyCon st) co
430 in 533 in
431 ((x, n, co), st) 534 ((x, n, co), st)
432 end) st xncs 535 end) st xncs
433 536
434 val cds = map (fn (x, n, co) => 537 val cds = map (fn (x, n, co) =>
435 let 538 let
436 val t = case co of 539 val t = case co of
437 NONE => c 540 NONE => c
438 | SOME t' => (L'.TFun (t', c), loc) 541 | SOME t' => (L'.TFun (t', c), loc)