Mercurial > urweb

annotate src/unpoly.sml @ 925:552c989c1601

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Change string URLification to avoid using the empty string, which confuses Apache no2slash()
author Adam Chlipala <adamc@hcoop.net>
date Sat, 12 Sep 2009 09:31:50 -0400
parents 6271f0e3c272
children 065ce3252090
rev   line source
adamc@315 1 (* Copyright (c) 2008, 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@399 49 val isOpen = U.Con.exists {kind = fn _ => false,
adamc@399 50 con = fn c =>
adamc@399 51 case c of
adamc@399 52 CRel _ => true
adamc@399 53 | _ => false}
adamc@399 54
adamc@316 55 fun unpolyNamed (xn, rep) =
adamc@316 56 U.Exp.map {kind = fn k => k,
adamc@316 57 con = fn c => c,
adamc@316 58 exp = fn e =>
adamc@316 59 case e of
adamc@399 60 ECApp (e', _) =>
adamc@325 61 let
adamc@325 62 fun isTheOne (e, _) =
adamc@325 63 case e of
adamc@325 64 ENamed xn' => xn' = xn
adamc@325 65 | ECApp (e, _) => isTheOne e
adamc@325 66 | _ => false
adamc@325 67 in
adamc@325 68 if isTheOne e' then
adamc@399 69 rep
adamc@325 70 else
adamc@325 71 e
adamc@325 72 end
adamc@316 73 | _ => e}
adamc@316 74
adamc@794 75 structure M = BinaryMapFn(struct
adamc@794 76 type ord_key = con list
adamc@794 77 val compare = Order.joinL U.Con.compare
adamc@794 78 end)
adamc@794 79
adamc@794 80 type func = {
adamc@794 81 kinds : kind list,
adamc@794 82 defs : (string * int * con * exp * string) list,
adamc@794 83 replacements : int M.map
adamc@794 84 }
adamc@794 85
adamc@315 86 type state = {
adamc@794 87 funcs : func IM.map,
adamc@315 88 decls : decl list,
adamc@315 89 nextName : int
adamc@315 90 }
adamc@315 91
adamc@315 92 fun kind (k, st) = (k, st)
adamc@315 93
adamc@315 94 fun con (c, st) = (c, st)
adamc@315 95
adamc@315 96 fun exp (e, st : state) =
adamc@315 97 case e of
adamc@315 98 ECApp _ =>
adamc@315 99 let
adamc@315 100 fun unravel (e, cargs) =
adamc@315 101 case e of
adamc@315 102 ECApp ((e, _), c) => unravel (e, c :: cargs)
adamc@315 103 | ENamed n => SOME (n, rev cargs)
adamc@315 104 | _ => NONE
adamc@315 105 in
adamc@315 106 case unravel (e, []) of
adamc@315 107 NONE => (e, st)
adamc@315 108 | SOME (n, cargs) =>
adamc@399 109 if List.exists isOpen cargs then
adamc@399 110 (e, st)
adamc@399 111 else
adamc@399 112 case IM.find (#funcs st, n) of
adamc@399 113 NONE => (e, st)
adamc@794 114 | SOME {kinds = ks, defs = vis, replacements} =>
adamc@794 115 case M.find (replacements, cargs) of
adamc@794 116 SOME n => (ENamed n, st)
adamc@794 117 | NONE =>
adamc@794 118 let
adamc@794 119 val old_vis = vis
adamc@794 120 val (vis, (thisName, nextName)) =
adamc@794 121 ListUtil.foldlMap
adamc@794 122 (fn ((x, n', t, e, s), (thisName, nextName)) =>
adamc@794 123 ((x, nextName, n', t, e, s),
adamc@794 124 (if n' = n then nextName else thisName,
adamc@794 125 nextName + 1)))
adamc@794 126 (0, #nextName st) vis
adamc@315 127
adamc@794 128 fun specialize (x, n, n_old, t, e, s) =
adamc@794 129 let
adamc@794 130 fun trim (t, e, cargs) =
adamc@794 131 case (t, e, cargs) of
adamc@794 132 ((TCFun (_, _, t), _),
adamc@794 133 (ECAbs (_, _, e), _),
adamc@794 134 carg :: cargs) =>
adamc@794 135 let
adamc@794 136 val t = subConInCon (length cargs, carg) t
adamc@794 137 val e = subConInExp (length cargs, carg) e
adamc@794 138 in
adamc@794 139 trim (t, e, cargs)
adamc@794 140 end
adamc@796 141 | (_, _, []) => SOME (t, e)
adamc@794 142 | _ => NONE
adamc@794 143 in
adamc@794 144 (*Print.prefaces "specialize"
adamc@794 145 [("t", CorePrint.p_con CoreEnv.empty t),
adamc@794 146 ("e", CorePrint.p_exp CoreEnv.empty e),
adamc@794 147 ("|cargs|", Print.PD.string (Int.toString (length cargs)))];*)
adamc@794 148 Option.map (fn (t, e) => (x, n, n_old, t, e, s))
adamc@794 149 (trim (t, e, cargs))
adamc@794 150 end
adamc@315 151
adamc@794 152 val vis = List.map specialize vis
adamc@794 153 in
adamc@794 154 if List.exists (not o Option.isSome) vis orelse length cargs > length ks then
adamc@794 155 (e, st)
adamc@794 156 else
adamc@794 157 let
adamc@794 158 val vis = List.mapPartial (fn x => x) vis
adamc@316 159
adamc@794 160 val vis = map (fn (x, n, n_old, t, e, s) =>
adamc@794 161 (x ^ "_unpoly", n, n_old, t, e, s)) vis
adamc@794 162 val vis' = map (fn (x, n, _, t, e, s) =>
adamc@794 163 (x, n, t, e, s)) vis
adamc@794 164
adamc@794 165 val funcs = IM.insert (#funcs st, n,
adamc@794 166 {kinds = ks,
adamc@794 167 defs = old_vis,
adamc@794 168 replacements = M.insert (replacements,
adamc@794 169 cargs,
adamc@794 170 thisName)})
adamc@794 171
adamc@794 172 val ks' = List.drop (ks, length cargs)
adamc@794 173
adamc@794 174 val st = {funcs = foldl (fn (vi, funcs) =>
adamc@794 175 IM.insert (funcs, #2 vi,
adamc@794 176 {kinds = ks',
adamc@794 177 defs = vis',
adamc@794 178 replacements = M.empty}))
adamc@794 179 funcs vis',
adamc@794 180 decls = #decls st,
adamc@794 181 nextName = nextName}
adamc@794 182
adamc@794 183 val (vis', st) = ListUtil.foldlMap (fn ((x, n, t, e, s), st) =>
adamc@794 184 let
adamc@794 185 val (e, st) = polyExp (e, st)
adamc@794 186 in
adamc@794 187 ((x, n, t, e, s), st)
adamc@794 188 end)
adamc@794 189 st vis'
adamc@794 190 in
adamc@794 191 (ENamed thisName,
adamc@794 192 {funcs = #funcs st,
adamc@399 193 decls = (DValRec vis', ErrorMsg.dummySpan) :: #decls st,
adamc@794 194 nextName = #nextName st})
adamc@794 195 end
adamc@794 196 end
adamc@315 197 end
adamc@315 198 | _ => (e, st)
adamc@315 199
adamc@794 200 and polyExp (x, st) = U.Exp.foldMap {kind = kind, con = con, exp = exp} st x
adamc@794 201
adamc@315 202 fun decl (d, st : state) =
adamc@315 203 case d of
adamc@315 204 DValRec (vis as ((x, n, t, e, s) :: rest)) =>
adamc@315 205 let
adamc@315 206 fun unravel (e, cargs) =
adamc@315 207 case e of
adamc@315 208 (ECAbs (_, k, e), _) =>
adamc@315 209 unravel (e, k :: cargs)
adamc@315 210 | _ => rev cargs
adamc@315 211
adamc@315 212 val cargs = unravel (e, [])
adamc@315 213
adamc@315 214 fun unravel (e, cargs) =
adamc@315 215 case (e, cargs) of
adamc@315 216 ((ECAbs (_, k, e), _), k' :: cargs) =>
adamc@315 217 U.Kind.compare (k, k') = EQUAL
adamc@315 218 andalso unravel (e, cargs)
adamc@315 219 | (_, []) => true
adamc@315 220 | _ => false
adamc@315 221 in
adamc@315 222 if List.exists (fn vi => not (unravel (#4 vi, cargs))) rest then
adamc@315 223 (d, st)
adamc@315 224 else
adamc@315 225 let
adamc@315 226 val ns = IS.addList (IS.empty, map #2 vis)
adamc@315 227 val nargs = length cargs
adamc@315 228
adamc@315 229 fun deAbs (e, cargs) =
adamc@315 230 case (e, cargs) of
adamc@315 231 ((ECAbs (_, _, e), _), _ :: cargs) => deAbs (e, cargs)
adamc@315 232 | (_, []) => e
adamc@315 233 | _ => raise Fail "Unpoly: deAbs"
adamc@315 234
adamc@315 235 (** Verifying lack of polymorphic recursion *)
adamc@315 236
adamc@315 237 fun kind _ = false
adamc@315 238 fun con _ = false
adamc@315 239
adamc@315 240 fun exp e =
adamc@315 241 case e of
adamc@315 242 ECApp (e, c) =>
adamc@315 243 let
adamc@315 244 fun isIrregular (e, pos) =
adamc@315 245 case #1 e of
adamc@315 246 ENamed n =>
adamc@315 247 IS.member (ns, n)
adamc@315 248 andalso
adamc@315 249 (case #1 c of
adamc@315 250 CRel i => i <> nargs - pos
adamc@315 251 | _ => true)
adamc@315 252 | ECApp (e, _) => isIrregular (e, pos + 1)
adamc@315 253 | _ => false
adamc@315 254 in
adamc@315 255 isIrregular (e, 1)
adamc@315 256 end
adamc@315 257 | ECAbs _ => true
adamc@315 258 | _ => false
adamc@315 259
adamc@315 260 val irregular = U.Exp.exists {kind = kind, con = con, exp = exp}
adamc@315 261 in
adamc@315 262 if List.exists (fn x => irregular (deAbs (#4 x, cargs))) vis then
adamc@315 263 (d, st)
adamc@315 264 else
adamc@315 265 (d, {funcs = foldl (fn (vi, funcs) =>
adamc@794 266 IM.insert (funcs, #2 vi, {kinds = cargs,
adamc@794 267 defs = vis,
adamc@794 268 replacements = M.empty}))
adamc@315 269 (#funcs st) vis,
adamc@315 270 decls = #decls st,
adamc@315 271 nextName = #nextName st})
adamc@315 272 end
adamc@315 273 end
adamc@315 274
adamc@315 275 | _ => (d, st)
adamc@315 276
adamc@315 277 val polyDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl}
adamc@315 278
adamc@315 279 fun unpoly file =
adamc@315 280 let
adamc@315 281 fun doDecl (d : decl, st : state) =
adamc@315 282 let
adamc@315 283 val (d, st) = polyDecl st d
adamc@315 284 in
adamc@315 285 (rev (d :: #decls st),
adamc@315 286 {funcs = #funcs st,
adamc@315 287 decls = [],
adamc@315 288 nextName = #nextName st})
adamc@315 289 end
adamc@315 290
adamc@315 291 val (ds, _) = ListUtil.foldlMapConcat doDecl
adamc@315 292 {funcs = IM.empty,
adamc@315 293 decls = [],
adamc@315 294 nextName = U.File.maxName file + 1} file
adamc@315 295 in
adamc@315 296 ds
adamc@315 297 end
adamc@315 298
adamc@315 299 end