Mercurial > urweb

annotate src/specialize.sml @ 1886:b7cd3c7c7edd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Interpret 'table' signature items more flexibly, automatically adding (Ur) constraints to support a kind of subtyping over (SQL) constraint sets
author Adam Chlipala <adam@chlipala.net>
date Mon, 04 Nov 2013 15:14:23 -0500
parents 5b5c0b552f59
children
rev   line source
adamc@1276 1 (* Copyright (c) 2008-2010, Adam Chlipala
adamc@193 2 * All rights reserved.
adamc@193 3 *
adamc@193 4 * Redistribution and use in source and binary forms, with or without
adamc@193 5 * modification, are permitted provided that the following conditions are met:
adamc@193 6 *
adamc@193 7 * - Redistributions of source code must retain the above copyright notice,
adamc@193 8 * this list of conditions and the following disclaimer.
adamc@193 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@193 10 * this list of conditions and the following disclaimer in the documentation
adamc@193 11 * and/or other materials provided with the distribution.
adamc@193 12 * - The names of contributors may not be used to endorse or promote products
adamc@193 13 * derived from this software without specific prior written permission.
adamc@193 14 *
adamc@193 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@193 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@193 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@193 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@193 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@193 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@193 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@193 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@193 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@193 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@193 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@193 26 *)
adamc@193 27
adamc@315 28 (* Simplify a Core program by repeating polymorphic definitions of datatypes *)
adamc@193 29
adamc@193 30 structure Specialize :> SPECIALIZE = struct
adamc@193 31
adamc@193 32 open Core
adamc@193 33
adamc@193 34 structure E = CoreEnv
adamc@193 35 structure U = CoreUtil
adamc@193 36
adamc@193 37 val liftConInCon = E.liftConInCon
adamc@193 38 val subConInCon = E.subConInCon
adamc@193 39
adamc@193 40 structure CK = struct
adamc@193 41 type ord_key = con list
adamc@193 42 val compare = Order.joinL U.Con.compare
adamc@193 43 end
adamc@193 44
adamc@193 45 structure CM = BinaryMapFn(CK)
adamc@193 46 structure IM = IntBinaryMap
adamc@193 47
adamc@193 48 type datatyp' = {
adamc@193 49 name : int,
adamc@193 50 constructors : int IM.map
adamc@193 51 }
adamc@193 52
adamc@193 53 type datatyp = {
adamc@193 54 name : string,
adamc@193 55 params : int,
adamc@193 56 constructors : (string * int * con option) list,
adamc@193 57 specializations : datatyp' CM.map
adamc@193 58 }
adamc@193 59
adamc@193 60 type state = {
adamc@193 61 count : int,
adamc@193 62 datatypes : datatyp IM.map,
adamc@193 63 constructors : int IM.map,
adamc@846 64 decls : (string * int * string list * (string * int * con option) list) list
adamc@193 65 }
adamc@193 66
adamc@193 67 fun kind (k, st) = (k, st)
adamc@193 68
adamc@193 69 val isOpen = U.Con.exists {kind = fn _ => false,
adamc@193 70 con = fn c =>
adamc@193 71 case c of
adamc@193 72 CRel _ => true
adamc@193 73 | _ => false}
adamc@193 74
adamc@193 75 fun considerSpecialization (st : state, n, args, dt : datatyp) =
adamc@1276 76 let
adamc@1276 77 val args = map ReduceLocal.reduceCon args
adamc@1276 78 in
adamc@1276 79 case CM.find (#specializations dt, args) of
adamc@1276 80 SOME dt' => (#name dt', #constructors dt', st)
adamc@1276 81 | NONE =>
adamc@1276 82 let
adamc@1276 83 (*val () = Print.prefaces "Args" [("n", Print.PD.string (Int.toString n)),
adamc@1276 84 ("args", Print.p_list (CorePrint.p_con CoreEnv.empty) args)]*)
adamc@194 85
adamc@1276 86 val n' = #count st
adamc@193 87
adamc@1276 88 val nxs = length args - 1
adamc@1276 89 fun sub t = ListUtil.foldli (fn (i, arg, t) =>
adamc@1276 90 subConInCon (nxs - i, arg) t) t args
adamc@193 91
adamc@1276 92 val (cons, (count, cmap)) =
adamc@1276 93 ListUtil.foldlMap (fn ((x, n, to), (count, cmap)) =>
adamc@1276 94 let
adamc@1276 95 val to = Option.map sub to
adamc@1276 96 in
adamc@1276 97 ((x, count, to),
adamc@1276 98 (count + 1,
adamc@1276 99 IM.insert (cmap, n, count)))
adamc@1276 100 end) (n' + 1, IM.empty) (#constructors dt)
adamc@193 101
adamc@1276 102 val st = {count = count,
adamc@1276 103 datatypes = IM.insert (#datatypes st, n,
adamc@1276 104 {name = #name dt,
adamc@1276 105 params = #params dt,
adamc@1276 106 constructors = #constructors dt,
adamc@1276 107 specializations = CM.insert (#specializations dt,
adamc@1276 108 args,
adamc@1276 109 {name = n',
adamc@1276 110 constructors = cmap})}),
adamc@1276 111 constructors = #constructors st,
adamc@1276 112 decls = #decls st}
adamc@193 113
adamc@1276 114 val (cons, st) = ListUtil.foldlMap (fn ((x, n, NONE), st) => ((x, n, NONE), st)
adamc@1276 115 | ((x, n, SOME t), st) =>
adamc@1276 116 let
adamc@1276 117 val (t, st) = specCon st t
adamc@1276 118 in
adamc@1276 119 ((x, n, SOME t), st)
adamc@1276 120 end) st cons
adamc@193 121
adamc@1276 122 val dt = (#name dt ^ "_s",
adamc@1276 123 n',
adamc@1276 124 [],
adamc@1276 125 cons)
adamc@1276 126 in
adamc@1276 127 (n', cmap, {count = #count st,
adamc@1276 128 datatypes = #datatypes st,
adamc@1276 129 constructors = #constructors st,
adamc@1276 130 decls = dt :: #decls st})
adamc@1276 131 end
adamc@1276 132 end
adamc@193 133
adamc@193 134 and con (c, st : state) =
adamc@193 135 let
adamc@193 136 fun findApp (c, args) =
adamc@193 137 case c of
adamc@193 138 CApp ((c', _), arg) => findApp (c', arg :: args)
adamc@193 139 | CNamed n => SOME (n, args)
adamc@193 140 | _ => NONE
adamc@193 141 in
adamc@193 142 case findApp (c, []) of
adamc@193 143 SOME (n, args as (_ :: _)) =>
adamc@193 144 if List.exists isOpen args then
adamc@193 145 (c, st)
adamc@193 146 else
adamc@193 147 (case IM.find (#datatypes st, n) of
adamc@193 148 NONE => (c, st)
adamc@193 149 | SOME dt =>
adamc@193 150 if length args <> #params dt then
adamc@193 151 (c, st)
adamc@193 152 else
adamc@193 153 let
adamc@193 154 val (n, _, st) = considerSpecialization (st, n, args, dt)
adamc@193 155 in
adamc@193 156 (CNamed n, st)
adamc@193 157 end)
adamc@193 158 | _ => (c, st)
adamc@193 159 end
adamc@193 160
adamc@193 161 and specCon st = U.Con.foldMap {kind = kind, con = con} st
adamc@193 162
adamc@193 163 fun pat (p, st) =
adamc@193 164 case #1 p of
adamc@193 165 PWild => (p, st)
adamc@193 166 | PVar _ => (p, st)
adamc@193 167 | PPrim _ => (p, st)
adamc@193 168 | PCon (dk, PConVar pn, args as (_ :: _), po) =>
adamc@193 169 let
adamc@193 170 val (po, st) =
adamc@193 171 case po of
adamc@193 172 NONE => (NONE, st)
adamc@193 173 | SOME p =>
adamc@193 174 let
adamc@193 175 val (p, st) = pat (p, st)
adamc@193 176 in
adamc@193 177 (SOME p, st)
adamc@193 178 end
adamc@193 179 val p = (PCon (dk, PConVar pn, args, po), #2 p)
adamc@193 180 in
adamc@193 181 if List.exists isOpen args then
adamc@193 182 (p, st)
adamc@193 183 else
adamc@193 184 case IM.find (#constructors st, pn) of
adamc@193 185 NONE => (p, st)
adamc@193 186 | SOME n =>
adamc@193 187 case IM.find (#datatypes st, n) of
adamc@193 188 NONE => (p, st)
adamc@193 189 | SOME dt =>
adamc@193 190 let
adamc@193 191 val (n, cmap, st) = considerSpecialization (st, n, args, dt)
adamc@193 192 in
adamc@193 193 case IM.find (cmap, pn) of
adamc@193 194 NONE => raise Fail "Specialize: Missing datatype constructor (pat)"
adamc@193 195 | SOME pn' => ((PCon (dk, PConVar pn', [], po), #2 p), st)
adamc@193 196 end
adamc@193 197 end
adamc@851 198 | PCon (dk, pc, args, SOME p') =>
adamc@851 199 let
adamc@851 200 val (p', st) = pat (p', st)
adamc@851 201 in
adamc@851 202 ((PCon (dk, pc, args, SOME p'), #2 p), st)
adamc@851 203 end
adamc@193 204 | PCon _ => (p, st)
adamc@193 205 | PRecord xps =>
adamc@193 206 let
adamc@193 207 val (xps, st) = ListUtil.foldlMap (fn ((x, p, t), st) =>
adamc@193 208 let
adamc@193 209 val (p, st) = pat (p, st)
adamc@193 210 in
adamc@193 211 ((x, p, t), st)
adamc@193 212 end)
adamc@193 213 st xps
adamc@193 214 in
adamc@193 215 ((PRecord xps, #2 p), st)
adamc@193 216 end
adamc@193 217
adamc@193 218 fun exp (e, st) =
adamc@193 219 case e of
adamc@193 220 ECon (dk, PConVar pn, args as (_ :: _), eo) =>
adamc@193 221 if List.exists isOpen args then
adamc@193 222 (e, st)
adamc@193 223 else
adamc@193 224 (case IM.find (#constructors st, pn) of
adamc@193 225 NONE => (e, st)
adamc@193 226 | SOME n =>
adamc@193 227 case IM.find (#datatypes st, n) of
adamc@193 228 NONE => (e, st)
adamc@193 229 | SOME dt =>
adamc@193 230 let
adamc@193 231 val (n, cmap, st) = considerSpecialization (st, n, args, dt)
adamc@193 232 in
adamc@193 233 case IM.find (cmap, pn) of
adamc@193 234 NONE => raise Fail "Specialize: Missing datatype constructor"
adamc@193 235 | SOME pn' => (ECon (dk, PConVar pn', [], eo), st)
adamc@193 236 end)
adamc@193 237 | ECase (e, pes, r) =>
adamc@193 238 let
adamc@193 239 val (pes, st) = ListUtil.foldlMap (fn ((p, e), st) =>
adamc@193 240 let
adamc@193 241 val (p, st) = pat (p, st)
adamc@193 242 in
adamc@193 243 ((p, e), st)
adamc@193 244 end) st pes
adamc@193 245 in
adamc@193 246 (ECase (e, pes, r), st)
adamc@193 247 end
adamc@193 248 | _ => (e, st)
adamc@193 249
adamc@193 250 fun decl (d, st) = (d, st)
adamc@193 251
adamc@193 252 val specDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl}
adamc@193 253
adamc@193 254 fun specialize file =
adamc@193 255 let
adamc@792 256 fun doDecl (d, st) =
adamc@194 257 let
adamc@194 258 (*val () = Print.preface ("decl:", CorePrint.p_decl CoreEnv.empty all)*)
adamc@792 259 val (d, st) = specDecl st d
adamc@194 260 in
adamc@792 261 case #1 d of
adamc@846 262 DDatatype dts =>
adamc@847 263 ((case #decls st of
adamc@847 264 [] => [d]
adamc@847 265 | dts' => [(DDatatype (dts' @ dts), #2 d)]),
adamc@792 266 {count = #count st,
adamc@846 267 datatypes = foldl (fn ((x, n, xs, xnts), dts) =>
adamc@846 268 IM.insert (dts, n,
adamc@846 269 {name = x,
adamc@846 270 params = length xs,
adamc@846 271 constructors = xnts,
adamc@846 272 specializations = CM.empty}))
adamc@846 273 (#datatypes st) dts,
adamc@846 274 constructors = foldl (fn ((x, n, xs, xnts), cs) =>
adamc@846 275 foldl (fn ((_, n', _), constructors) =>
adamc@846 276 IM.insert (constructors, n', n))
adamc@846 277 cs xnts)
adamc@846 278 (#constructors st) dts,
adamc@792 279 decls = []})
adamc@194 280 | _ =>
adamc@847 281 (case #decls st of
adamc@847 282 [] => [d]
adamc@847 283 | dts => [(DDatatype dts, #2 d), d],
adamc@792 284 {count = #count st,
adamc@792 285 datatypes = #datatypes st,
adamc@792 286 constructors = #constructors st,
adamc@792 287 decls = []})
adamc@194 288 end
adamc@193 289
adamc@193 290 val (ds, _) = ListUtil.foldlMapConcat doDecl
adamc@193 291 {count = U.File.maxName file + 1,
adamc@193 292 datatypes = IM.empty,
adamc@193 293 constructors = IM.empty,
adamc@193 294 decls = []} file
adamc@193 295 in
adamc@193 296 ds
adamc@193 297 end
adamc@193 298
adamc@193 299 end