Mercurial > urweb

annotate src/unpoly.sml @ 2201:1091227f535a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Unnest properly in presence of kind polymorphism
author Adam Chlipala <adam@chlipala.net>
date Sun, 20 Dec 2015 13:41:35 -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