Mercurial > urweb

annotate src/unpoly.sml @ 316:04ebfe929a98

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Unpolyed a polymorphic function of two arguments
author Adam Chlipala <adamc@hcoop.net>
date Thu, 11 Sep 2008 10:14:59 -0400
parents e21d0dddda09
children e457d8972ff1
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@316 49 fun unpolyNamed (xn, rep) =
adamc@316 50 U.Exp.map {kind = fn k => k,
adamc@316 51 con = fn c => c,
adamc@316 52 exp = fn e =>
adamc@316 53 case e of
adamc@316 54 ENamed xn' =>
adamc@316 55 if xn' = xn then
adamc@316 56 rep
adamc@316 57 else
adamc@316 58 e
adamc@316 59 | ECApp (e, _) => #1 e
adamc@316 60 | _ => e}
adamc@316 61
adamc@315 62 type state = {
adamc@315 63 funcs : (kind list * (string * int * con * exp * string) list) IM.map,
adamc@315 64 decls : decl list,
adamc@315 65 nextName : int
adamc@315 66 }
adamc@315 67
adamc@315 68 fun kind (k, st) = (k, st)
adamc@315 69
adamc@315 70 fun con (c, st) = (c, st)
adamc@315 71
adamc@315 72 fun exp (e, st : state) =
adamc@315 73 case e of
adamc@315 74 ECApp _ =>
adamc@315 75 let
adamc@315 76 (*val () = Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty (e, ErrorMsg.dummySpan))]*)
adamc@315 77
adamc@315 78 fun unravel (e, cargs) =
adamc@315 79 case e of
adamc@315 80 ECApp ((e, _), c) => unravel (e, c :: cargs)
adamc@315 81 | ENamed n => SOME (n, rev cargs)
adamc@315 82 | _ => NONE
adamc@315 83 in
adamc@315 84 case unravel (e, []) of
adamc@315 85 NONE => (e, st)
adamc@315 86 | SOME (n, cargs) =>
adamc@315 87 case IM.find (#funcs st, n) of
adamc@315 88 NONE => (e, st)
adamc@315 89 | SOME (ks, vis) =>
adamc@315 90 let
adamc@315 91 val (vis, nextName) = ListUtil.foldlMap
adamc@315 92 (fn ((x, n, t, e, s), nextName) =>
adamc@315 93 ((x, nextName, n, t, e, s), nextName + 1))
adamc@315 94 (#nextName st) vis
adamc@315 95
adamc@315 96 fun specialize (x, n, n_old, t, e, s) =
adamc@315 97 let
adamc@315 98 fun trim (t, e, cargs) =
adamc@315 99 case (t, e, cargs) of
adamc@315 100 ((TCFun (_, _, t), _),
adamc@315 101 (ECAbs (_, _, e), _),
adamc@315 102 carg :: cargs) =>
adamc@315 103 let
adamc@315 104 val t = subConInCon (length cargs, carg) t
adamc@315 105 val e = subConInExp (length cargs, carg) e
adamc@315 106 in
adamc@315 107 trim (t, e, cargs)
adamc@315 108 end
adamc@316 109 | (_, _, []) =>
adamc@316 110 let
adamc@316 111 val e = foldl (fn ((_, n, n_old, _, _, _), e) =>
adamc@316 112 unpolyNamed (n_old, ENamed n) e)
adamc@316 113 e vis
adamc@316 114 in
adamc@316 115 SOME (t, e)
adamc@316 116 end
adamc@315 117 | _ => NONE
adamc@315 118 in
adamc@315 119 (*Print.prefaces "specialize"
adamc@315 120 [("t", CorePrint.p_con CoreEnv.empty t),
adamc@315 121 ("e", CorePrint.p_exp CoreEnv.empty e),
adamc@315 122 ("|cargs|", Print.PD.string (Int.toString (length cargs)))];*)
adamc@315 123 Option.map (fn (t, e) => (x, n, n_old, t, e, s))
adamc@315 124 (trim (t, e, cargs))
adamc@315 125 end
adamc@315 126
adamc@315 127 val vis = List.map specialize vis
adamc@315 128 in
adamc@316 129 if List.exists (not o Option.isSome) vis orelse length cargs > length ks then
adamc@315 130 (e, st)
adamc@315 131 else
adamc@315 132 let
adamc@315 133 val vis = List.mapPartial (fn x => x) vis
adamc@316 134 val vis = map (fn (x, n, n_old, t, e, s) =>
adamc@316 135 (x ^ "_unpoly", n, n_old, t, e, s)) vis
adamc@315 136 val vis' = map (fn (x, n, _, t, e, s) =>
adamc@316 137 (x, n, t, e, s)) vis
adamc@316 138
adamc@316 139 val ks' = List.drop (ks, length cargs)
adamc@315 140 in
adamc@315 141 case List.find (fn (_, _, n_old, _, _, _) => n_old = n) vis of
adamc@315 142 NONE => raise Fail "Unpoly: Inconsistent 'val rec' record"
adamc@315 143 | SOME (_, n, _, _, _, _) =>
adamc@315 144 (ENamed n,
adamc@316 145 {funcs = foldl (fn (vi, funcs) =>
adamc@316 146 IM.insert (funcs, #2 vi, (ks', vis')))
adamc@316 147 (#funcs st) vis',
adamc@315 148 decls = (DValRec vis', ErrorMsg.dummySpan) :: #decls st,
adamc@315 149 nextName = nextName})
adamc@315 150 end
adamc@315 151 end
adamc@315 152 end
adamc@315 153 | _ => (e, st)
adamc@315 154
adamc@315 155 fun decl (d, st : state) =
adamc@315 156 case d of
adamc@315 157 DValRec (vis as ((x, n, t, e, s) :: rest)) =>
adamc@315 158 let
adamc@315 159 fun unravel (e, cargs) =
adamc@315 160 case e of
adamc@315 161 (ECAbs (_, k, e), _) =>
adamc@315 162 unravel (e, k :: cargs)
adamc@315 163 | _ => rev cargs
adamc@315 164
adamc@315 165 val cargs = unravel (e, [])
adamc@315 166
adamc@315 167 fun unravel (e, cargs) =
adamc@315 168 case (e, cargs) of
adamc@315 169 ((ECAbs (_, k, e), _), k' :: cargs) =>
adamc@315 170 U.Kind.compare (k, k') = EQUAL
adamc@315 171 andalso unravel (e, cargs)
adamc@315 172 | (_, []) => true
adamc@315 173 | _ => false
adamc@315 174 in
adamc@315 175 if List.exists (fn vi => not (unravel (#4 vi, cargs))) rest then
adamc@315 176 (d, st)
adamc@315 177 else
adamc@315 178 let
adamc@315 179 val ns = IS.addList (IS.empty, map #2 vis)
adamc@315 180 val nargs = length cargs
adamc@315 181
adamc@315 182 fun deAbs (e, cargs) =
adamc@315 183 case (e, cargs) of
adamc@315 184 ((ECAbs (_, _, e), _), _ :: cargs) => deAbs (e, cargs)
adamc@315 185 | (_, []) => e
adamc@315 186 | _ => raise Fail "Unpoly: deAbs"
adamc@315 187
adamc@315 188 (** Verifying lack of polymorphic recursion *)
adamc@315 189
adamc@315 190 fun kind _ = false
adamc@315 191 fun con _ = false
adamc@315 192
adamc@315 193 fun exp e =
adamc@315 194 case e of
adamc@315 195 ECApp (e, c) =>
adamc@315 196 let
adamc@315 197 fun isIrregular (e, pos) =
adamc@315 198 case #1 e of
adamc@315 199 ENamed n =>
adamc@315 200 IS.member (ns, n)
adamc@315 201 andalso
adamc@315 202 (case #1 c of
adamc@315 203 CRel i => i <> nargs - pos
adamc@315 204 | _ => true)
adamc@315 205 | ECApp (e, _) => isIrregular (e, pos + 1)
adamc@315 206 | _ => false
adamc@315 207 in
adamc@315 208 isIrregular (e, 1)
adamc@315 209 end
adamc@315 210 | ECAbs _ => true
adamc@315 211 | _ => false
adamc@315 212
adamc@315 213 val irregular = U.Exp.exists {kind = kind, con = con, exp = exp}
adamc@315 214 in
adamc@315 215 if List.exists (fn x => irregular (deAbs (#4 x, cargs))) vis then
adamc@315 216 (d, st)
adamc@315 217 else
adamc@315 218 (d, {funcs = foldl (fn (vi, funcs) =>
adamc@315 219 IM.insert (funcs, #2 vi, (cargs, vis)))
adamc@315 220 (#funcs st) vis,
adamc@315 221 decls = #decls st,
adamc@315 222 nextName = #nextName st})
adamc@315 223 end
adamc@315 224 end
adamc@315 225
adamc@315 226 | _ => (d, st)
adamc@315 227
adamc@315 228 val polyDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl}
adamc@315 229
adamc@315 230 fun unpoly file =
adamc@315 231 let
adamc@315 232 fun doDecl (d : decl, st : state) =
adamc@315 233 let
adamc@315 234 val (d, st) = polyDecl st d
adamc@315 235 in
adamc@315 236 (rev (d :: #decls st),
adamc@315 237 {funcs = #funcs st,
adamc@315 238 decls = [],
adamc@315 239 nextName = #nextName st})
adamc@315 240 end
adamc@315 241
adamc@315 242 val (ds, _) = ListUtil.foldlMapConcat doDecl
adamc@315 243 {funcs = IM.empty,
adamc@315 244 decls = [],
adamc@315 245 nextName = U.File.maxName file + 1} file
adamc@315 246 in
adamc@315 247 ds
adamc@315 248 end
adamc@315 249
adamc@315 250 end