Mercurial > urweb

annotate src/specialize.sml @ 1327:1cc67fdac4d3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New argument to transactional free functions, to specify whether we are about to retry
author Adam Chlipala <adam@chlipala.net>
date Sat, 04 Dec 2010 11:15:20 -0500
parents 5b5c0b552f59
children
rev   line source
adamc@1276 1 (* Copyright (c) 2008-2010, Adam Chlipala
adamc@193 2 * All rights reserved.
adamc@193 3 *
adamc@193 4 * Redistribution and use in source and binary forms, with or without
adamc@193 5 * modification, are permitted provided that the following conditions are met:
adamc@193 6 *
adamc@193 7 * - Redistributions of source code must retain the above copyright notice,
adamc@193 8 * this list of conditions and the following disclaimer.
adamc@193 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@193 10 * this list of conditions and the following disclaimer in the documentation
adamc@193 11 * and/or other materials provided with the distribution.
adamc@193 12 * - The names of contributors may not be used to endorse or promote products
adamc@193 13 * derived from this software without specific prior written permission.
adamc@193 14 *
adamc@193 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@193 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@193 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@193 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@193 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@193 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@193 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@193 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@193 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@193 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@193 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@193 26 *)
adamc@193 27
adamc@315 28 (* Simplify a Core program by repeating polymorphic definitions of datatypes *)
adamc@193 29
adamc@193 30 structure Specialize :> SPECIALIZE = struct
adamc@193 31
adamc@193 32 open Core
adamc@193 33
adamc@193 34 structure E = CoreEnv
adamc@193 35 structure U = CoreUtil
adamc@193 36
adamc@193 37 val liftConInCon = E.liftConInCon
adamc@193 38 val subConInCon = E.subConInCon
adamc@193 39
adamc@193 40 structure CK = struct
adamc@193 41 type ord_key = con list
adamc@193 42 val compare = Order.joinL U.Con.compare
adamc@193 43 end
adamc@193 44
adamc@193 45 structure CM = BinaryMapFn(CK)
adamc@193 46 structure IM = IntBinaryMap
adamc@193 47
adamc@193 48 type datatyp' = {
adamc@193 49 name : int,
adamc@193 50 constructors : int IM.map
adamc@193 51 }
adamc@193 52
adamc@193 53 type datatyp = {
adamc@193 54 name : string,
adamc@193 55 params : int,
adamc@193 56 constructors : (string * int * con option) list,
adamc@193 57 specializations : datatyp' CM.map
adamc@193 58 }
adamc@193 59
adamc@193 60 type state = {
adamc@193 61 count : int,
adamc@193 62 datatypes : datatyp IM.map,
adamc@193 63 constructors : int IM.map,
adamc@846 64 decls : (string * int * string list * (string * int * con option) list) list
adamc@193 65 }
adamc@193 66
adamc@193 67 fun kind (k, st) = (k, st)
adamc@193 68
adamc@193 69 val isOpen = U.Con.exists {kind = fn _ => false,
adamc@193 70 con = fn c =>
adamc@193 71 case c of
adamc@193 72 CRel _ => true
adamc@193 73 | _ => false}
adamc@193 74
adamc@193 75 fun considerSpecialization (st : state, n, args, dt : datatyp) =
adamc@1276 76 let
adamc@1276 77 val args = map ReduceLocal.reduceCon args
adamc@1276 78 in
adamc@1276 79 case CM.find (#specializations dt, args) of
adamc@1276 80 SOME dt' => (#name dt', #constructors dt', st)
adamc@1276 81 | NONE =>
adamc@1276 82 let
adamc@1276 83 (*val () = Print.prefaces "Args" [("n", Print.PD.string (Int.toString n)),
adamc@1276 84 ("args", Print.p_list (CorePrint.p_con CoreEnv.empty) args)]*)
adamc@194 85
adamc@1276 86 val n' = #count st
adamc@193 87
adamc@1276 88 val nxs = length args - 1
adamc@1276 89 fun sub t = ListUtil.foldli (fn (i, arg, t) =>
adamc@1276 90 subConInCon (nxs - i, arg) t) t args
adamc@193 91
adamc@1276 92 val (cons, (count, cmap)) =
adamc@1276 93 ListUtil.foldlMap (fn ((x, n, to), (count, cmap)) =>
adamc@1276 94 let
adamc@1276 95 val to = Option.map sub to
adamc@1276 96 in
adamc@1276 97 ((x, count, to),
adamc@1276 98 (count + 1,
adamc@1276 99 IM.insert (cmap, n, count)))
adamc@1276 100 end) (n' + 1, IM.empty) (#constructors dt)
adamc@193 101
adamc@1276 102 val st = {count = count,
adamc@1276 103 datatypes = IM.insert (#datatypes st, n,
adamc@1276 104 {name = #name dt,
adamc@1276 105 params = #params dt,
adamc@1276 106 constructors = #constructors dt,
adamc@1276 107 specializations = CM.insert (#specializations dt,
adamc@1276 108 args,
adamc@1276 109 {name = n',
adamc@1276 110 constructors = cmap})}),
adamc@1276 111 constructors = #constructors st,
adamc@1276 112 decls = #decls st}
adamc@193 113
adamc@1276 114 val (cons, st) = ListUtil.foldlMap (fn ((x, n, NONE), st) => ((x, n, NONE), st)
adamc@1276 115 | ((x, n, SOME t), st) =>
adamc@1276 116 let
adamc@1276 117 val (t, st) = specCon st t
adamc@1276 118 in
adamc@1276 119 ((x, n, SOME t), st)
adamc@1276 120 end) st cons
adamc@193 121
adamc@1276 122 val dt = (#name dt ^ "_s",
adamc@1276 123 n',
adamc@1276 124 [],
adamc@1276 125 cons)
adamc@1276 126 in
adamc@1276 127 (n', cmap, {count = #count st,
adamc@1276 128 datatypes = #datatypes st,
adamc@1276 129 constructors = #constructors st,
adamc@1276 130 decls = dt :: #decls st})
adamc@1276 131 end
adamc@1276 132 end
adamc@193 133
adamc@193 134 and con (c, st : state) =
adamc@193 135 let
adamc@193 136 fun findApp (c, args) =
adamc@193 137 case c of
adamc@193 138 CApp ((c', _), arg) => findApp (c', arg :: args)
adamc@193 139 | CNamed n => SOME (n, args)
adamc@193 140 | _ => NONE
adamc@193 141 in
adamc@193 142 case findApp (c, []) of
adamc@193 143 SOME (n, args as (_ :: _)) =>
adamc@193 144 if List.exists isOpen args then
adamc@193 145 (c, st)
adamc@193 146 else
adamc@193 147 (case IM.find (#datatypes st, n) of
adamc@193 148 NONE => (c, st)
adamc@193 149 | SOME dt =>
adamc@193 150 if length args <> #params dt then
adamc@193 151 (c, st)
adamc@193 152 else
adamc@193 153 let
adamc@193 154 val (n, _, st) = considerSpecialization (st, n, args, dt)
adamc@193 155 in
adamc@193 156 (CNamed n, st)
adamc@193 157 end)
adamc@193 158 | _ => (c, st)
adamc@193 159 end
adamc@193 160
adamc@193 161 and specCon st = U.Con.foldMap {kind = kind, con = con} st
adamc@193 162
adamc@193 163 fun pat (p, st) =
adamc@193 164 case #1 p of
adamc@193 165 PWild => (p, st)
adamc@193 166 | PVar _ => (p, st)
adamc@193 167 | PPrim _ => (p, st)
adamc@193 168 | PCon (dk, PConVar pn, args as (_ :: _), po) =>
adamc@193 169 let
adamc@193 170 val (po, st) =
adamc@193 171 case po of
adamc@193 172 NONE => (NONE, st)
adamc@193 173 | SOME p =>
adamc@193 174 let
adamc@193 175 val (p, st) = pat (p, st)
adamc@193 176 in
adamc@193 177 (SOME p, st)
adamc@193 178 end
adamc@193 179 val p = (PCon (dk, PConVar pn, args, po), #2 p)
adamc@193 180 in
adamc@193 181 if List.exists isOpen args then
adamc@193 182 (p, st)
adamc@193 183 else
adamc@193 184 case IM.find (#constructors st, pn) of
adamc@193 185 NONE => (p, st)
adamc@193 186 | SOME n =>
adamc@193 187 case IM.find (#datatypes st, n) of
adamc@193 188 NONE => (p, st)
adamc@193 189 | SOME dt =>
adamc@193 190 let
adamc@193 191 val (n, cmap, st) = considerSpecialization (st, n, args, dt)
adamc@193 192 in
adamc@193 193 case IM.find (cmap, pn) of
adamc@193 194 NONE => raise Fail "Specialize: Missing datatype constructor (pat)"
adamc@193 195 | SOME pn' => ((PCon (dk, PConVar pn', [], po), #2 p), st)
adamc@193 196 end
adamc@193 197 end
adamc@851 198 | PCon (dk, pc, args, SOME p') =>
adamc@851 199 let
adamc@851 200 val (p', st) = pat (p', st)
adamc@851 201 in
adamc@851 202 ((PCon (dk, pc, args, SOME p'), #2 p), st)
adamc@851 203 end
adamc@193 204 | PCon _ => (p, st)
adamc@193 205 | PRecord xps =>
adamc@193 206 let
adamc@193 207 val (xps, st) = ListUtil.foldlMap (fn ((x, p, t), st) =>
adamc@193 208 let
adamc@193 209 val (p, st) = pat (p, st)
adamc@193 210 in
adamc@193 211 ((x, p, t), st)
adamc@193 212 end)
adamc@193 213 st xps
adamc@193 214 in
adamc@193 215 ((PRecord xps, #2 p), st)
adamc@193 216 end
adamc@193 217
adamc@193 218 fun exp (e, st) =
adamc@193 219 case e of
adamc@193 220 ECon (dk, PConVar pn, args as (_ :: _), eo) =>
adamc@193 221 if List.exists isOpen args then
adamc@193 222 (e, st)
adamc@193 223 else
adamc@193 224 (case IM.find (#constructors st, pn) of
adamc@193 225 NONE => (e, st)
adamc@193 226 | SOME n =>
adamc@193 227 case IM.find (#datatypes st, n) of
adamc@193 228 NONE => (e, st)
adamc@193 229 | SOME dt =>
adamc@193 230 let
adamc@193 231 val (n, cmap, st) = considerSpecialization (st, n, args, dt)
adamc@193 232 in
adamc@193 233 case IM.find (cmap, pn) of
adamc@193 234 NONE => raise Fail "Specialize: Missing datatype constructor"
adamc@193 235 | SOME pn' => (ECon (dk, PConVar pn', [], eo), st)
adamc@193 236 end)
adamc@193 237 | ECase (e, pes, r) =>
adamc@193 238 let
adamc@193 239 val (pes, st) = ListUtil.foldlMap (fn ((p, e), st) =>
adamc@193 240 let
adamc@193 241 val (p, st) = pat (p, st)
adamc@193 242 in
adamc@193 243 ((p, e), st)
adamc@193 244 end) st pes
adamc@193 245 in
adamc@193 246 (ECase (e, pes, r), st)
adamc@193 247 end
adamc@193 248 | _ => (e, st)
adamc@193 249
adamc@193 250 fun decl (d, st) = (d, st)
adamc@193 251
adamc@193 252 val specDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl}
adamc@193 253
adamc@193 254 fun specialize file =
adamc@193 255 let
adamc@792 256 fun doDecl (d, st) =
adamc@194 257 let
adamc@194 258 (*val () = Print.preface ("decl:", CorePrint.p_decl CoreEnv.empty all)*)
adamc@792 259 val (d, st) = specDecl st d
adamc@194 260 in
adamc@792 261 case #1 d of
adamc@846 262 DDatatype dts =>
adamc@847 263 ((case #decls st of
adamc@847 264 [] => [d]
adamc@847 265 | dts' => [(DDatatype (dts' @ dts), #2 d)]),
adamc@792 266 {count = #count st,
adamc@846 267 datatypes = foldl (fn ((x, n, xs, xnts), dts) =>
adamc@846 268 IM.insert (dts, n,
adamc@846 269 {name = x,
adamc@846 270 params = length xs,
adamc@846 271 constructors = xnts,
adamc@846 272 specializations = CM.empty}))
adamc@846 273 (#datatypes st) dts,
adamc@846 274 constructors = foldl (fn ((x, n, xs, xnts), cs) =>
adamc@846 275 foldl (fn ((_, n', _), constructors) =>
adamc@846 276 IM.insert (constructors, n', n))
adamc@846 277 cs xnts)
adamc@846 278 (#constructors st) dts,
adamc@792 279 decls = []})
adamc@194 280 | _ =>
adamc@847 281 (case #decls st of
adamc@847 282 [] => [d]
adamc@847 283 | dts => [(DDatatype dts, #2 d), d],
adamc@792 284 {count = #count st,
adamc@792 285 datatypes = #datatypes st,
adamc@792 286 constructors = #constructors st,
adamc@792 287 decls = []})
adamc@194 288 end
adamc@193 289
adamc@193 290 val (ds, _) = ListUtil.foldlMapConcat doDecl
adamc@193 291 {count = U.File.maxName file + 1,
adamc@193 292 datatypes = IM.empty,
adamc@193 293 constructors = IM.empty,
adamc@193 294 decls = []} file
adamc@193 295 in
adamc@193 296 ds
adamc@193 297 end
adamc@193 298
adamc@193 299 end