Mercurial > urweb

annotate src/unpoly.sml @ 1034:a779402841f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hooks for measuring how much interesting proving is going on in elaboration
author Adam Chlipala <adamc@hcoop.net>
date Tue, 17 Nov 2009 12:44:14 -0500
parents 065ce3252090
children 85d194409b17
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@1016 165 val funcs = foldl (fn ((_, n, n_old, _, _, _), funcs) =>
adamc@1016 166 let
adamc@1016 167 val replacements = case IM.find (funcs, n_old) of
adamc@1016 168 NONE => M.empty
adamc@1016 169 | SOME {replacements = r, ...} => r
adamc@1016 170 in
adamc@1016 171 IM.insert (funcs, n_old,
adamc@1016 172 {kinds = ks,
adamc@1016 173 defs = old_vis,
adamc@1016 174 replacements = M.insert (replacements,
adamc@1016 175 cargs,
adamc@1016 176 n)})
adamc@1016 177 end) (#funcs st) vis
adamc@794 178
adamc@794 179 val ks' = List.drop (ks, length cargs)
adamc@794 180
adamc@794 181 val st = {funcs = foldl (fn (vi, funcs) =>
adamc@794 182 IM.insert (funcs, #2 vi,
adamc@794 183 {kinds = ks',
adamc@794 184 defs = vis',
adamc@794 185 replacements = M.empty}))
adamc@794 186 funcs vis',
adamc@794 187 decls = #decls st,
adamc@794 188 nextName = nextName}
adamc@794 189
adamc@794 190 val (vis', st) = ListUtil.foldlMap (fn ((x, n, t, e, s), st) =>
adamc@794 191 let
adamc@794 192 val (e, st) = polyExp (e, st)
adamc@794 193 in
adamc@794 194 ((x, n, t, e, s), st)
adamc@794 195 end)
adamc@794 196 st vis'
adamc@794 197 in
adamc@794 198 (ENamed thisName,
adamc@794 199 {funcs = #funcs st,
adamc@399 200 decls = (DValRec vis', ErrorMsg.dummySpan) :: #decls st,
adamc@794 201 nextName = #nextName st})
adamc@794 202 end
adamc@794 203 end
adamc@315 204 end
adamc@315 205 | _ => (e, st)
adamc@315 206
adamc@794 207 and polyExp (x, st) = U.Exp.foldMap {kind = kind, con = con, exp = exp} st x
adamc@794 208
adamc@315 209 fun decl (d, st : state) =
adamc@315 210 case d of
adamc@315 211 DValRec (vis as ((x, n, t, e, s) :: rest)) =>
adamc@315 212 let
adamc@315 213 fun unravel (e, cargs) =
adamc@315 214 case e of
adamc@315 215 (ECAbs (_, k, e), _) =>
adamc@315 216 unravel (e, k :: cargs)
adamc@315 217 | _ => rev cargs
adamc@315 218
adamc@315 219 val cargs = unravel (e, [])
adamc@315 220
adamc@315 221 fun unravel (e, cargs) =
adamc@315 222 case (e, cargs) of
adamc@315 223 ((ECAbs (_, k, e), _), k' :: cargs) =>
adamc@315 224 U.Kind.compare (k, k') = EQUAL
adamc@315 225 andalso unravel (e, cargs)
adamc@315 226 | (_, []) => true
adamc@315 227 | _ => false
adamc@315 228 in
adamc@315 229 if List.exists (fn vi => not (unravel (#4 vi, cargs))) rest then
adamc@315 230 (d, st)
adamc@315 231 else
adamc@315 232 let
adamc@315 233 val ns = IS.addList (IS.empty, map #2 vis)
adamc@315 234 val nargs = length cargs
adamc@315 235
adamc@315 236 fun deAbs (e, cargs) =
adamc@315 237 case (e, cargs) of
adamc@315 238 ((ECAbs (_, _, e), _), _ :: cargs) => deAbs (e, cargs)
adamc@315 239 | (_, []) => e
adamc@315 240 | _ => raise Fail "Unpoly: deAbs"
adamc@315 241
adamc@315 242 (** Verifying lack of polymorphic recursion *)
adamc@315 243
adamc@315 244 fun kind _ = false
adamc@315 245 fun con _ = false
adamc@315 246
adamc@315 247 fun exp e =
adamc@315 248 case e of
adamc@315 249 ECApp (e, c) =>
adamc@315 250 let
adamc@315 251 fun isIrregular (e, pos) =
adamc@315 252 case #1 e of
adamc@315 253 ENamed n =>
adamc@315 254 IS.member (ns, n)
adamc@315 255 andalso
adamc@315 256 (case #1 c of
adamc@315 257 CRel i => i <> nargs - pos
adamc@315 258 | _ => true)
adamc@315 259 | ECApp (e, _) => isIrregular (e, pos + 1)
adamc@315 260 | _ => false
adamc@315 261 in
adamc@315 262 isIrregular (e, 1)
adamc@315 263 end
adamc@315 264 | ECAbs _ => true
adamc@315 265 | _ => false
adamc@315 266
adamc@315 267 val irregular = U.Exp.exists {kind = kind, con = con, exp = exp}
adamc@315 268 in
adamc@315 269 if List.exists (fn x => irregular (deAbs (#4 x, cargs))) vis then
adamc@315 270 (d, st)
adamc@315 271 else
adamc@315 272 (d, {funcs = foldl (fn (vi, funcs) =>
adamc@794 273 IM.insert (funcs, #2 vi, {kinds = cargs,
adamc@794 274 defs = vis,
adamc@794 275 replacements = M.empty}))
adamc@315 276 (#funcs st) vis,
adamc@315 277 decls = #decls st,
adamc@315 278 nextName = #nextName st})
adamc@315 279 end
adamc@315 280 end
adamc@315 281
adamc@315 282 | _ => (d, st)
adamc@315 283
adamc@315 284 val polyDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl}
adamc@315 285
adamc@315 286 fun unpoly file =
adamc@315 287 let
adamc@315 288 fun doDecl (d : decl, st : state) =
adamc@315 289 let
adamc@315 290 val (d, st) = polyDecl st d
adamc@315 291 in
adamc@315 292 (rev (d :: #decls st),
adamc@315 293 {funcs = #funcs st,
adamc@315 294 decls = [],
adamc@315 295 nextName = #nextName st})
adamc@315 296 end
adamc@315 297
adamc@315 298 val (ds, _) = ListUtil.foldlMapConcat doDecl
adamc@315 299 {funcs = IM.empty,
adamc@315 300 decls = [],
adamc@315 301 nextName = U.File.maxName file + 1} file
adamc@315 302 in
adamc@315 303 ds
adamc@315 304 end
adamc@315 305
adamc@315 306 end