Mercurial > urweb

comparison src/corify.sml @ 1704:21ecf340f05c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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),