Mercurial > urweb

annotate src/unpoly.sml @ 851:20a364c4a6dc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix a bug with 'Some p' patterns, where 'p' needs specialization
author Adam Chlipala <adamc@hcoop.net>
date Thu, 18 Jun 2009 18:06:15 -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