Mercurial > urweb
comparison src/corify.sml @ 1704:21ecf340f05c
Fix defunctorization of modules containing datatype definitions
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Thu, 29 Mar 2012 09:55:04 -0400 |
parents | 6a4461757829 |
children | df6a040f5389 |
comparison
equal
deleted
inserted
replaced
1703:6f2f74cc4ead | 1704:21ecf340f05c |
---|---|
1 (* Copyright (c) 2008-2010, Adam Chlipala | 1 (* Copyright (c) 2008-2012, Adam Chlipala |
2 * All rights reserved. | 2 * All rights reserved. |
3 * | 3 * |
4 * Redistribution and use in source and binary forms, with or without | 4 * Redistribution and use in source and binary forms, with or without |
5 * modification, are permitted provided that the following conditions are met: | 5 * modification, are permitted provided that the following conditions are met: |
6 * | 6 * |
89 | CFfi of string | 89 | CFfi of string |
90 val bindCon : t -> string -> int -> t * int | 90 val bindCon : t -> string -> int -> t * int |
91 val lookupConById : t -> int -> int option | 91 val lookupConById : t -> int -> int option |
92 val lookupConByName : t -> string -> core_con | 92 val lookupConByName : t -> string -> core_con |
93 | 93 |
94 val bindConstructor : t -> string -> int -> L'.patCon -> t | 94 val bindConstructor : t -> string -> int -> t * int |
95 val bindConstructorAs : t -> string -> int -> L'.patCon -> t | |
95 val lookupConstructorByNameOpt : t -> string -> L'.patCon option | 96 val lookupConstructorByNameOpt : t -> string -> L'.patCon option |
96 val lookupConstructorByName : t -> string -> L'.patCon | 97 val lookupConstructorByName : t -> string -> L'.patCon |
97 val lookupConstructorById : t -> int -> L'.patCon | 98 val lookupConstructorById : t -> int -> L'.patCon |
98 | 99 |
99 datatype core_val = | 100 datatype core_val = |
100 ENormal of int | 101 ENormal of int |
101 | EFfi of string * L'.con | 102 | EFfi of string * L'.con |
102 val bindVal : t -> string -> int -> t * int | 103 val bindVal : t -> string -> int -> t * int |
103 val bindConstructorVal : t -> string -> int -> t | 104 val bindConstructorVal : t -> string -> int -> int -> t |
104 val lookupValById : t -> int -> int option | 105 val lookupValById : t -> int -> int option |
105 val lookupValByName : t -> string -> core_val | 106 val lookupValByName : t -> string -> core_val |
106 | 107 |
107 val bindStr : t -> string -> int -> t -> t | 108 val bindStr : t -> string -> int -> t -> t |
108 val lookupStrById : t -> int -> t | 109 val lookupStrById : t -> int -> t |
239 current = current, | 240 current = current, |
240 nested = nested}, | 241 nested = nested}, |
241 n') | 242 n') |
242 end | 243 end |
243 | 244 |
244 fun bindConstructorVal {basis, cons, constructors, vals, strs, funs, current, nested} s n = | 245 fun bindConstructorVal {basis, cons, constructors, vals, strs, funs, current, nested} s n n' = |
245 let | 246 let |
246 val current = | 247 val current = |
247 case current of | 248 case current of |
248 FFfi _ => raise Fail "Binding inside FFfi" | 249 FFfi _ => raise Fail "Binding inside FFfi" |
249 | FNormal {name, cons, constructors, vals, strs, funs} => | 250 | FNormal {name, cons, constructors, vals, strs, funs} => |
250 FNormal {name = name, | 251 FNormal {name = name, |
251 cons = cons, | 252 cons = cons, |
252 constructors = constructors, | 253 constructors = constructors, |
253 vals = SM.insert (vals, s, n), | 254 vals = SM.insert (vals, s, n'), |
254 strs = strs, | 255 strs = strs, |
255 funs = funs} | 256 funs = funs} |
256 in | 257 in |
257 {basis = basis, | 258 {basis = basis, |
258 cons = cons, | 259 cons = cons, |
259 constructors = constructors, | 260 constructors = constructors, |
260 vals = IM.insert (vals, n, n), | 261 vals = IM.insert (vals, n, n'), |
261 strs = strs, | 262 strs = strs, |
262 funs = funs, | 263 funs = funs, |
263 current = current, | 264 current = current, |
264 nested = nested} | 265 nested = nested} |
265 end | 266 end |
276 | FNormal {name, vals, ...} => | 277 | FNormal {name, vals, ...} => |
277 case SM.find (vals, x) of | 278 case SM.find (vals, x) of |
278 NONE => raise Fail ("Corify.St.lookupValByName " ^ String.concatWith "." (rev name) ^ "." ^ x) | 279 NONE => raise Fail ("Corify.St.lookupValByName " ^ String.concatWith "." (rev name) ^ "." ^ x) |
279 | SOME n => ENormal n | 280 | SOME n => ENormal n |
280 | 281 |
281 fun bindConstructor {basis, cons, constructors, vals, strs, funs, current, nested} s n n' = | 282 fun bindConstructorAs {basis, cons, constructors, vals, strs, funs, current, nested} s n c' = |
282 let | 283 let |
283 val current = | 284 val current = |
284 case current of | 285 case current of |
285 FFfi _ => raise Fail "Binding inside FFfi" | 286 FFfi _ => raise Fail "Binding inside FFfi" |
286 | FNormal {name, cons, constructors, vals, strs, funs} => | 287 | FNormal {name, cons, constructors, vals, strs, funs} => |
287 FNormal {name = name, | 288 FNormal {name = name, |
288 cons = cons, | 289 cons = cons, |
289 constructors = SM.insert (constructors, s, n'), | 290 constructors = SM.insert (constructors, s, c'), |
290 vals = vals, | 291 vals = vals, |
291 strs = strs, | 292 strs = strs, |
292 funs = funs} | 293 funs = funs} |
293 in | 294 in |
294 {basis = basis, | 295 {basis = basis, |
295 cons = cons, | 296 cons = cons, |
296 constructors = IM.insert (constructors, n, n'), | 297 constructors = IM.insert (constructors, n, c'), |
297 vals = vals, | 298 vals = vals, |
298 strs = strs, | 299 strs = strs, |
299 funs = funs, | 300 funs = funs, |
300 current = current, | 301 current = current, |
301 nested = nested} | 302 nested = nested} |
303 end | |
304 | |
305 fun bindConstructor st s n = | |
306 let | |
307 val n' = alloc () | |
308 val c' = L'.PConVar n' | |
309 in | |
310 (bindConstructorAs st s n c', n') | |
302 end | 311 end |
303 | 312 |
304 fun lookupConstructorById ({constructors, ...} : t) n = | 313 fun lookupConstructorById ({constructors, ...} : t) n = |
305 case IM.find (constructors, n) of | 314 case IM.find (constructors, n) of |
306 NONE => raise Fail "Corify.St.lookupConstructorById" | 315 NONE => raise Fail "Corify.St.lookupConstructorById" |
640 (fn ((x, n, xs, xncs), (st, dcons)) => | 649 (fn ((x, n, xs, xncs), (st, dcons)) => |
641 let | 650 let |
642 val (xncs, st) = ListUtil.foldlMap | 651 val (xncs, st) = ListUtil.foldlMap |
643 (fn ((x, n, co), st) => | 652 (fn ((x, n, co), st) => |
644 let | 653 let |
645 val st = St.bindConstructor st x n (L'.PConVar n) | 654 val (st, n') = St.bindConstructor st x n |
646 val st = St.bindConstructorVal st x n | 655 val st = St.bindConstructorVal st x n n' |
647 val co = Option.map (corifyCon st) co | 656 val co = Option.map (corifyCon st) co |
648 in | 657 in |
649 ((x, n, co), st) | 658 ((x, n', co), st) |
650 end) st xncs | 659 end) st xncs |
651 | 660 |
652 val dk = ElabUtil.classifyDatatype xncs | 661 val dk = ElabUtil.classifyDatatype xncs |
653 val t = (L'.CNamed n, loc) | 662 val t = (L'.CNamed n, loc) |
654 val nxs = length xs - 1 | 663 val nxs = length xs - 1 |
693 val (_, {inner, ...}) = corifyStr mods (m, st) | 702 val (_, {inner, ...}) = corifyStr mods (m, st) |
694 | 703 |
695 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => | 704 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => |
696 let | 705 let |
697 val n' = St.lookupConstructorByName inner x | 706 val n' = St.lookupConstructorByName inner x |
698 val st = St.bindConstructor st x n n' | 707 val st = St.bindConstructorAs st x n n' |
699 val (st, n) = St.bindVal st x n | 708 val (st, n) = St.bindVal st x n |
700 val co = Option.map (corifyCon st) co | 709 val co = Option.map (corifyCon st) co |
701 in | 710 in |
702 ((x, n, co), st) | 711 ((x, n, co), st) |
703 end) st xncs | 712 end) st xncs |
882 e, ""), loc) | 891 e, ""), loc) |
883 in | 892 in |
884 (SM.insert (cmap, x', wrapT tf), d) | 893 (SM.insert (cmap, x', wrapT tf), d) |
885 end | 894 end |
886 | 895 |
887 val st = St.bindConstructor st x' n pc | 896 val st = St.bindConstructorAs st x' n pc |
888 | 897 |
889 val conmap = SM.insert (conmap, x', | 898 val conmap = SM.insert (conmap, x', |
890 (x, xs, to, dk)) | 899 (x, xs, to, dk)) |
891 in | 900 in |
892 ((x', n, to), | 901 ((x', n, to), |