Mercurial > urweb
comparison src/specialize.sml @ 846:0d30e6338c65
Some standard library reorgs and additions; handle mutual datatypes better in Specialize
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 09 Jun 2009 18:11:59 -0400 |
parents | 61a1f5c5ae2c |
children | 0f7e2cca6d9b |
comparison
equal
deleted
inserted
replaced
845:6725d73c3c31 | 846:0d30e6338c65 |
---|---|
59 | 59 |
60 type state = { | 60 type state = { |
61 count : int, | 61 count : int, |
62 datatypes : datatyp IM.map, | 62 datatypes : datatyp IM.map, |
63 constructors : int IM.map, | 63 constructors : int IM.map, |
64 decls : decl list | 64 decls : (string * int * string list * (string * int * con option) list) list |
65 } | 65 } |
66 | 66 |
67 fun kind (k, st) = (k, st) | 67 fun kind (k, st) = (k, st) |
68 | 68 |
69 val isOpen = U.Con.exists {kind = fn _ => false, | 69 val isOpen = U.Con.exists {kind = fn _ => false, |
113 val (t, st) = specCon st t | 113 val (t, st) = specCon st t |
114 in | 114 in |
115 ((x, n, SOME t), st) | 115 ((x, n, SOME t), st) |
116 end) st cons | 116 end) st cons |
117 | 117 |
118 val d = (DDatatype [(#name dt ^ "_s", | 118 val dt = (#name dt ^ "_s", |
119 n', | 119 n', |
120 [], | 120 [], |
121 cons)], #2 (List.hd args)) | 121 cons) |
122 in | 122 in |
123 (n', cmap, {count = #count st, | 123 (n', cmap, {count = #count st, |
124 datatypes = #datatypes st, | 124 datatypes = #datatypes st, |
125 constructors = #constructors st, | 125 constructors = #constructors st, |
126 decls = d :: #decls st}) | 126 decls = dt :: #decls st}) |
127 end | 127 end |
128 | 128 |
129 and con (c, st : state) = | 129 and con (c, st : state) = |
130 let | 130 let |
131 fun findApp (c, args) = | 131 fun findApp (c, args) = |
244 let | 244 let |
245 fun doDecl (d, st) = | 245 fun doDecl (d, st) = |
246 let | 246 let |
247 (*val () = Print.preface ("decl:", CorePrint.p_decl CoreEnv.empty all)*) | 247 (*val () = Print.preface ("decl:", CorePrint.p_decl CoreEnv.empty all)*) |
248 val (d, st) = specDecl st d | 248 val (d, st) = specDecl st d |
249 | |
250 val ds = | |
251 case #decls st of | |
252 [] => [] | |
253 | dts => [(DDatatype dts, #2 d)] | |
249 in | 254 in |
250 case #1 d of | 255 case #1 d of |
251 DDatatype [(x, n, xs, xnts)] => | 256 DDatatype dts => |
252 (rev (d :: #decls st), | 257 (rev (d :: ds), |
253 {count = #count st, | 258 {count = #count st, |
254 datatypes = IM.insert (#datatypes st, n, | 259 datatypes = foldl (fn ((x, n, xs, xnts), dts) => |
255 {name = x, | 260 IM.insert (dts, n, |
256 params = length xs, | 261 {name = x, |
257 constructors = xnts, | 262 params = length xs, |
258 specializations = CM.empty}), | 263 constructors = xnts, |
259 constructors = foldl (fn ((_, n', _), constructors) => | 264 specializations = CM.empty})) |
260 IM.insert (constructors, n', n)) | 265 (#datatypes st) dts, |
261 (#constructors st) xnts, | 266 constructors = foldl (fn ((x, n, xs, xnts), cs) => |
267 foldl (fn ((_, n', _), constructors) => | |
268 IM.insert (constructors, n', n)) | |
269 cs xnts) | |
270 (#constructors st) dts, | |
262 decls = []}) | 271 decls = []}) |
263 | _ => | 272 | _ => |
264 (rev (d :: #decls st), | 273 (rev (d :: ds), |
265 {count = #count st, | 274 {count = #count st, |
266 datatypes = #datatypes st, | 275 datatypes = #datatypes st, |
267 constructors = #constructors st, | 276 constructors = #constructors st, |
268 decls = []}) | 277 decls = []}) |
269 end | 278 end |