Mercurial > urweb

comparison src/specialize.sml @ 846:0d30e6338c65

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