Mercurial > urweb

annotate src/unpoly.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@1185 1 (* Copyright (c) 2008-2010, Adam Chlipala
adamc@315 2 * All rights reserved.
adamc@315 3 *
adamc@315 4 * Redistribution and use in source and binary forms, with or without
adamc@315 5 * modification, are permitted provided that the following conditions are met:
adamc@315 6 *
adamc@315 7 * - Redistributions of source code must retain the above copyright notice,
adamc@315 8 * this list of conditions and the following disclaimer.
adamc@315 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@315 10 * this list of conditions and the following disclaimer in the documentation
adamc@315 11 * and/or other materials provided with the distribution.
adamc@315 12 * - The names of contributors may not be used to endorse or promote products
adamc@315 13 * derived from this software without specific prior written permission.
adamc@315 14 *
adamc@315 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@315 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@315 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@315 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@315 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@315 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@315 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@315 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@315 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@315 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@315 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@315 26 *)
adamc@315 27
adamc@315 28 (* Simplify a Core program by repeating polymorphic function definitions *)
adamc@315 29
adamc@315 30 structure Unpoly :> UNPOLY = struct
adamc@315 31
adamc@315 32 open Core
adamc@315 33
adamc@315 34 structure E = CoreEnv
adamc@315 35 structure U = CoreUtil
adamc@315 36
adamc@315 37 structure IS = IntBinarySet
adamc@315 38 structure IM = IntBinaryMap
adamc@315 39
adamc@315 40
adamc@315 41 (** The actual specialization *)
adamc@315 42
adamc@315 43 val liftConInCon = E.liftConInCon
adamc@315 44 val subConInCon = E.subConInCon
adamc@315 45
adamc@315 46 val liftConInExp = E.liftConInExp
adamc@315 47 val subConInExp = E.subConInExp
adamc@315 48
adamc@1185 49 val isOpen = U.Con.existsB {kind = fn _ => false,
adamc@1185 50 con = fn (n, c) =>
adamc@1185 51 case c of
adamc@1185 52 CRel n' => n' >= n
adamc@1185 53 | _ => false,
adamc@1185 54 bind = fn (n, b) =>
adamc@1185 55 case b of
adamc@1185 56 U.Con.RelC _ => n + 1
adamc@1185 57 | _ => n} 0
adamc@399 58
adamc@316 59 fun unpolyNamed (xn, rep) =
adamc@316 60 U.Exp.map {kind = fn k => k,
adamc@316 61 con = fn c => c,
adamc@316 62 exp = fn e =>
adamc@316 63 case e of
adamc@399 64 ECApp (e', _) =>
adamc@325 65 let
adamc@325 66 fun isTheOne (e, _) =
adamc@325 67 case e of
adamc@325 68 ENamed xn' => xn' = xn
adamc@325 69 | ECApp (e, _) => isTheOne e
adamc@325 70 | _ => false
adamc@325 71 in
adamc@325 72 if isTheOne e' then
adamc@399 73 rep
adamc@325 74 else
adamc@325 75 e
adamc@325 76 end
adamc@316 77 | _ => e}
adamc@316 78
adamc@794 79 structure M = BinaryMapFn(struct
adamc@794 80 type ord_key = con list
adamc@794 81 val compare = Order.joinL U.Con.compare
adamc@794 82 end)
adamc@794 83
adamc@794 84 type func = {
adamc@794 85 kinds : kind list,
adamc@794 86 defs : (string * int * con * exp * string) list,
adamc@794 87 replacements : int M.map
adamc@794 88 }
adamc@794 89
adamc@315 90 type state = {
adamc@794 91 funcs : func IM.map,
adamc@315 92 decls : decl list,
adamc@315 93 nextName : int
adamc@315 94 }
adamc@315 95
adamc@315 96 fun kind (k, st) = (k, st)
adamc@315 97
adamc@315 98 fun con (c, st) = (c, st)
adamc@315 99
adamc@315 100 fun exp (e, st : state) =
adamc@315 101 case e of
adamc@315 102 ECApp _ =>
adamc@315 103 let
adamc@315 104 fun unravel (e, cargs) =
adamc@315 105 case e of
adamc@315 106 ECApp ((e, _), c) => unravel (e, c :: cargs)
adamc@315 107 | ENamed n => SOME (n, rev cargs)
adamc@315 108 | _ => NONE
adamc@315 109 in
adamc@315 110 case unravel (e, []) of
adamc@315 111 NONE => (e, st)
adamc@315 112 | SOME (n, cargs) =>
adamc@399 113 if List.exists isOpen cargs then
adamc@399 114 (e, st)
adamc@399 115 else
adamc@399 116 case IM.find (#funcs st, n) of
adamc@399 117 NONE => (e, st)
adamc@794 118 | SOME {kinds = ks, defs = vis, replacements} =>
adamc@1276 119 let
adamc@1276 120 val cargs = map ReduceLocal.reduceCon cargs
adamc@1276 121 in
adamc@1276 122 case M.find (replacements, cargs) of
adamc@1276 123 SOME n => (ENamed n, st)
adamc@1276 124 | NONE =>
adamc@1276 125 let
adamc@1276 126 val old_vis = vis
adamc@1276 127 val (vis, (thisName, nextName)) =
adamc@1276 128 ListUtil.foldlMap
adamc@1276 129 (fn ((x, n', t, e, s), (thisName, nextName)) =>
adamc@1276 130 ((x, nextName, n', t, e, s),
adamc@1276 131 (if n' = n then nextName else thisName,
adamc@1276 132 nextName + 1)))
adamc@1276 133 (0, #nextName st) vis
adamc@315 134
adamc@1276 135 fun specialize (x, n, n_old, t, e, s) =
adamc@1276 136 let
adamc@1276 137 fun trim (t, e, cargs) =
adamc@1276 138 case (t, e, cargs) of
adamc@1276 139 ((TCFun (_, _, t), _),
adamc@1276 140 (ECAbs (_, _, e), _),
adamc@1276 141 carg :: cargs) =>
adamc@1276 142 let
adamc@1276 143 val t = subConInCon (length cargs, carg) t
adamc@1276 144 val e = subConInExp (length cargs, carg) e
adamc@1276 145 in
adamc@1276 146 trim (t, e, cargs)
adamc@1276 147 end
adamc@1276 148 | (_, _, []) => SOME (t, e)
adamc@1276 149 | _ => NONE
adamc@1276 150 in
adamc@1276 151 (*Print.prefaces "specialize"
adamc@1276 152 [("n", Print.PD.string (Int.toString n)),
adamc@1276 153 ("nold", Print.PD.string (Int.toString n_old)),
adamc@1276 154 ("t", CorePrint.p_con CoreEnv.empty t),
adamc@1276 155 ("e", CorePrint.p_exp CoreEnv.empty e),
adamc@1276 156 ("|cargs|", Print.PD.string (Int.toString (length cargs)))];*)
adamc@1276 157 Option.map (fn (t, e) => (x, n, n_old, t, e, s))
adamc@1276 158 (trim (t, e, cargs))
adamc@1276 159 end
adamc@315 160
adamc@1276 161 val vis = List.map specialize vis
adamc@1276 162 in
adamc@1276 163 if List.exists (not o Option.isSome) vis orelse length cargs > length ks then
adamc@1276 164 (e, st)
adamc@1276 165 else
adamc@1276 166 let
adamc@1276 167 val vis = List.mapPartial (fn x => x) vis
adamc@316 168
adamc@1276 169 val vis = map (fn (x, n, n_old, t, e, s) =>
adamc@1276 170 (x ^ "_unpoly", n, n_old, t, e, s)) vis
adamc@1276 171 val vis' = map (fn (x, n, _, t, e, s) =>
adamc@1276 172 (x, n, t, e, s)) vis
adamc@794 173
adamc@1276 174 val funcs = foldl (fn ((_, n, n_old, _, _, _), funcs) =>
adamc@1276 175 let
adamc@1276 176 val replacements = case IM.find (funcs, n_old) of
adamc@1276 177 NONE => M.empty
adamc@1276 178 | SOME {replacements = r,
adamc@1276 179 ...} => r
adamc@1276 180 in
adamc@1276 181 IM.insert (funcs, n_old,
adamc@1276 182 {kinds = ks,
adamc@1276 183 defs = old_vis,
adamc@1276 184 replacements = M.insert (replacements,
adamc@1276 185 cargs,
adamc@1276 186 n)})
adamc@1276 187 end) (#funcs st) vis
adamc@794 188
adamc@1276 189 val ks' = List.drop (ks, length cargs)
adamc@794 190
adamc@1276 191 val st = {funcs = foldl (fn (vi, funcs) =>
adamc@1276 192 IM.insert (funcs, #2 vi,
adamc@1276 193 {kinds = ks',
adamc@1276 194 defs = vis',
adamc@1276 195 replacements = M.empty}))
adamc@1276 196 funcs vis',
adamc@1276 197 decls = #decls st,
adamc@1276 198 nextName = nextName}
adamc@794 199
adamc@1276 200 val (vis', st) = ListUtil.foldlMap (fn ((x, n, t, e, s), st) =>
adamc@1276 201 let
adamc@1276 202 val (e, st) = polyExp (e, st)
adamc@1276 203 in
adamc@1276 204 ((x, n, t, e, s), st)
adamc@1276 205 end)
adamc@1276 206 st vis'
adamc@1276 207 in
adamc@1276 208 (ENamed thisName,
adamc@1276 209 {funcs = #funcs st,
adamc@1276 210 decls = (DValRec vis', ErrorMsg.dummySpan) :: #decls st,
adamc@1276 211 nextName = #nextName st})
adamc@1276 212 end
adamc@1276 213 end
adamc@1276 214 end
adamc@315 215 end
adamc@315 216 | _ => (e, st)
adamc@315 217
adamc@794 218 and polyExp (x, st) = U.Exp.foldMap {kind = kind, con = con, exp = exp} st x
adamc@794 219
adamc@315 220 fun decl (d, st : state) =
adamc@1122 221 let
adamc@1122 222 fun unravel (e, cargs) =
adamc@1122 223 case e of
adamc@1122 224 (ECAbs (_, k, e), _) =>
adamc@1122 225 unravel (e, k :: cargs)
adamc@1122 226 | _ => rev cargs
adamc@1122 227 in
adamc@1122 228 case d of
adamc@1122 229 DVal (vi as (x, n, t, e, s)) =>
adamc@1122 230 let
adamc@1122 231 val cargs = unravel (e, [])
adamc@315 232
adamc@1122 233 val ns = IS.singleton n
adamc@1122 234 in
adamc@1122 235 (d, {funcs = IM.insert (#funcs st, n, {kinds = cargs,
adamc@1122 236 defs = [vi],
adamc@1122 237 replacements = M.empty}),
adamc@1122 238 decls = #decls st,
adamc@1122 239 nextName = #nextName st})
adamc@1122 240 end
adamc@1122 241 | DValRec (vis as ((x, n, t, e, s) :: rest)) =>
adamc@1122 242 let
adamc@1122 243 val cargs = unravel (e, [])
adamc@315 244
adamc@1122 245 fun unravel (e, cargs) =
adamc@1122 246 case (e, cargs) of
adamc@1122 247 ((ECAbs (_, k, e), _), k' :: cargs) =>
adamc@1122 248 U.Kind.compare (k, k') = EQUAL
adamc@1122 249 andalso unravel (e, cargs)
adamc@1122 250 | (_, []) => true
adamc@1122 251 | _ => false
adamc@1122 252
adamc@1122 253 fun deAbs (e, cargs) =
adamc@1122 254 case (e, cargs) of
adamc@1122 255 ((ECAbs (_, _, e), _), _ :: cargs) => deAbs (e, cargs)
adamc@1122 256 | (_, []) => e
adamc@1122 257 | _ => raise Fail "Unpoly: deAbs"
adamc@315 258
adamc@1122 259 in
adamc@1122 260 if List.exists (fn vi => not (unravel (#4 vi, cargs))) rest then
adamc@1122 261 (d, st)
adamc@1122 262 else
adamc@1122 263 let
adamc@1122 264 val ns = IS.addList (IS.empty, map #2 vis)
adamc@1122 265 val nargs = length cargs
adamc@315 266
adamc@1122 267 (** Verifying lack of polymorphic recursion *)
adamc@315 268
adamc@1122 269 fun kind _ = false
adamc@1122 270 fun con _ = false
adamc@315 271
adamc@1180 272 fun exp (cn, e) =
adamc@1122 273 case e of
adamc@1180 274 orig as ECApp (e, c) =>
adamc@1122 275 let
adamc@1122 276 fun isIrregular (e, pos) =
adamc@1122 277 case #1 e of
adamc@1122 278 ENamed n =>
adamc@1122 279 IS.member (ns, n)
adamc@1122 280 andalso
adamc@1122 281 (case #1 c of
adamc@1180 282 CRel i => i <> nargs - pos + cn
adamc@1122 283 | _ => true)
adamc@1122 284 | ECApp (e, _) => isIrregular (e, pos + 1)
adamc@1122 285 | _ => false
adamc@1122 286 in
adamc@1122 287 isIrregular (e, 1)
adamc@1122 288 end
adamc@1122 289 | _ => false
adamc@315 290
adamc@1180 291 fun bind (cn, b) =
adamc@1180 292 case b of
adamc@1180 293 U.Exp.RelC _ => cn+1
adamc@1180 294 | _ => cn
adamc@1180 295
adamc@1180 296 val irregular = U.Exp.existsB {kind = kind, con = con, exp = exp, bind = bind} 0
adamc@1122 297 in
adamc@1122 298 if List.exists (fn x => irregular (deAbs (#4 x, cargs))) vis then
adamc@1185 299 (d, st)
adamc@1122 300 else
adamc@1122 301 (d, {funcs = foldl (fn (vi, funcs) =>
adamc@1122 302 IM.insert (funcs, #2 vi, {kinds = cargs,
adamc@1122 303 defs = vis,
adamc@1122 304 replacements = M.empty}))
adamc@1122 305 (#funcs st) vis,
adamc@1122 306 decls = #decls st,
adamc@1122 307 nextName = #nextName st})
adamc@1122 308 end
adamc@1122 309 end
adamc@315 310
adamc@1122 311 | _ => (d, st)
adamc@1122 312 end
adamc@315 313
adamc@315 314 val polyDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl}
adamc@315 315
adamc@315 316 fun unpoly file =
adamc@315 317 let
adamc@315 318 fun doDecl (d : decl, st : state) =
adamc@315 319 let
adamc@315 320 val (d, st) = polyDecl st d
adamc@315 321 in
adamc@315 322 (rev (d :: #decls st),
adamc@315 323 {funcs = #funcs st,
adamc@315 324 decls = [],
adamc@315 325 nextName = #nextName st})
adamc@315 326 end
adamc@315 327
adamc@315 328 val (ds, _) = ListUtil.foldlMapConcat doDecl
adamc@315 329 {funcs = IM.empty,
adamc@315 330 decls = [],
adamc@315 331 nextName = U.File.maxName file + 1} file
adamc@315 332 in
adamc@315 333 ds
adamc@315 334 end
adamc@315 335
adamc@315 336 end