Mercurial > urweb

annotate src/reduce_local.sml @ 1327:1cc67fdac4d3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New argument to transactional free functions, to specify whether we are about to retry
author Adam Chlipala <adam@chlipala.net>
date Sat, 04 Dec 2010 11:15:20 -0500
parents b4480a56cab7
children 0577be31a435
rev   line source
adamc@1272 1 (* Copyright (c) 2008-2010, Adam Chlipala
adamc@482 2 * All rights reserved.
adamc@482 3 *
adamc@482 4 * Redistribution and use in source and binary forms, with or without
adamc@482 5 * modification, are permitted provided that the following conditions are met:
adamc@482 6 *
adamc@482 7 * - Redistributions of source code must retain the above copyright notice,
adamc@482 8 * this list of conditions and the following disclaimer.
adamc@482 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@482 10 * this list of conditions and the following disclaimer in the documentation
adamc@482 11 * and/or other materials provided with the distribution.
adamc@482 12 * - The names of contributors may not be used to endorse or promote products
adamc@482 13 * derived from this software without specific prior written permission.
adamc@482 14 *
adamc@482 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@482 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@482 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@482 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@482 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@482 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@482 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@482 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@482 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@482 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@482 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@482 26 *)
adamc@482 27
adamc@482 28 (* Simplify a Core program algebraically, without unfolding definitions *)
adamc@482 29
adamc@482 30 structure ReduceLocal :> REDUCE_LOCAL = struct
adamc@482 31
adamc@482 32 open Core
adamc@482 33
adamc@512 34 structure IM = IntBinaryMap
adamc@482 35
adamc@1062 36 fun multiLiftExpInExp n e =
adamc@1062 37 if n = 0 then
adamc@1062 38 e
adamc@1062 39 else
adamc@1062 40 multiLiftExpInExp (n - 1) (CoreEnv.liftExpInExp 0 e)
adamc@1062 41
adamc@512 42 datatype env_item =
adamc@512 43 Unknown
adamc@512 44 | Known of exp
adamc@482 45
adamc@1272 46 | UnknownC
adamc@1272 47 | KnownC of con
adamc@1272 48
adamc@1272 49 | Lift of int * int
adamc@482 50
adamc@512 51 type env = env_item list
adamc@512 52
adamc@512 53 val deKnown = List.filter (fn Known _ => false
adamc@1272 54 | KnownC _ => false
adamc@512 55 | _ => true)
adamc@512 56
adamc@1062 57 datatype result = Yes of env | No | Maybe
adamc@1062 58
adamc@1062 59 fun match (env, p : pat, e : exp) =
adamc@1062 60 let
adamc@1062 61 val baseline = length env
adamc@1062 62
adamc@1062 63 fun match (env, p, e) =
adamc@1062 64 case (#1 p, #1 e) of
adamc@1062 65 (PWild, _) => Yes env
adamc@1062 66 | (PVar (x, t), _) => Yes (Known (multiLiftExpInExp (length env - baseline) e) :: env)
adamc@1062 67
adamc@1062 68 | (PPrim p, EPrim p') =>
adamc@1062 69 if Prim.equal (p, p') then
adamc@1062 70 Yes env
adamc@1062 71 else
adamc@1062 72 No
adamc@1062 73
adamc@1062 74 | (PCon (_, PConVar n1, _, NONE), ECon (_, PConVar n2, _, NONE)) =>
adamc@1062 75 if n1 = n2 then
adamc@1062 76 Yes env
adamc@1062 77 else
adamc@1062 78 No
adamc@1062 79
adamc@1062 80 | (PCon (_, PConVar n1, _, SOME p), ECon (_, PConVar n2, _, SOME e)) =>
adamc@1062 81 if n1 = n2 then
adamc@1062 82 match (env, p, e)
adamc@1062 83 else
adamc@1062 84 No
adamc@1062 85
adamc@1062 86 | (PCon (_, PConFfi {mod = m1, con = con1, ...}, _, NONE),
adamc@1062 87 ECon (_, PConFfi {mod = m2, con = con2, ...}, _, NONE)) =>
adamc@1062 88 if m1 = m2 andalso con1 = con2 then
adamc@1062 89 Yes env
adamc@1062 90 else
adamc@1062 91 No
adamc@1062 92
adamc@1062 93 | (PCon (_, PConFfi {mod = m1, con = con1, ...}, _, SOME ep),
adamc@1062 94 ECon (_, PConFfi {mod = m2, con = con2, ...}, _, SOME e)) =>
adamc@1062 95 if m1 = m2 andalso con1 = con2 then
adamc@1062 96 match (env, p, e)
adamc@1062 97 else
adamc@1062 98 No
adamc@1062 99
adamc@1062 100 | (PRecord xps, ERecord xes) =>
adamc@1062 101 if List.exists (fn ((CName _, _), _, _) => false
adamc@1062 102 | _ => true) xes then
adamc@1062 103 Maybe
adamc@1062 104 else
adamc@1062 105 let
adamc@1062 106 fun consider (xps, env) =
adamc@1062 107 case xps of
adamc@1062 108 [] => Yes env
adamc@1062 109 | (x, p, _) :: rest =>
adamc@1062 110 case List.find (fn ((CName x', _), _, _) => x' = x
adamc@1062 111 | _ => false) xes of
adamc@1062 112 NONE => No
adamc@1062 113 | SOME (_, e, _) =>
adamc@1062 114 case match (env, p, e) of
adamc@1062 115 No => No
adamc@1062 116 | Maybe => Maybe
adamc@1062 117 | Yes env => consider (rest, env)
adamc@1062 118 in
adamc@1062 119 consider (xps, env)
adamc@1062 120 end
adamc@1062 121
adamc@1062 122 | _ => Maybe
adamc@1062 123 in
adamc@1062 124 match (env, p, e)
adamc@1062 125 end
adamc@1062 126
adamc@1272 127 fun con env (all as (c, loc)) =
adamc@1272 128 ((*Print.prefaces "con" [("c", CorePrint.p_con CoreEnv.empty all)];*)
adamc@1272 129 case c of
adamc@1272 130 TFun (c1, c2) => (TFun (con env c1, con env c2), loc)
adamc@1272 131 | TCFun (x, k, c2) => (TCFun (x, k, con (UnknownC :: env) c2), loc)
adamc@1272 132 | TKFun (x, c2) => (TKFun (x, con env c2), loc)
adamc@1272 133 | TRecord c => (TRecord (con env c), loc)
adamc@1272 134
adamc@1272 135 | CRel n =>
adamc@1272 136 let
adamc@1272 137 fun find (n', env, nudge, liftC) =
adamc@1272 138 case env of
adam@1289 139 [] => raise Fail "ReduceLocal.con: CRel"
adamc@1272 140 | Unknown :: rest => find (n', rest, nudge, liftC)
adamc@1272 141 | Known _ :: rest => find (n', rest, nudge, liftC)
adamc@1272 142 | Lift (liftC', _) :: rest => find (n', rest, nudge + liftC',
adamc@1272 143 liftC + liftC')
adamc@1272 144 | UnknownC :: rest =>
adamc@1272 145 if n' = 0 then
adamc@1272 146 (CRel (n + nudge), loc)
adamc@1272 147 else
adamc@1272 148 find (n' - 1, rest, nudge, liftC + 1)
adamc@1272 149 | KnownC c :: rest =>
adamc@1272 150 if n' = 0 then
adamc@1272 151 con (Lift (liftC, 0) :: rest) c
adamc@1272 152 else
adamc@1272 153 find (n' - 1, rest, nudge - 1, liftC)
adamc@1272 154 in
adamc@1272 155 (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*)
adamc@1272 156 find (n, env, 0, 0)
adamc@1272 157 end
adamc@1272 158 | CNamed _ => all
adamc@1272 159 | CFfi _ => all
adamc@1272 160 | CApp (c1, c2) =>
adamc@1272 161 let
adamc@1272 162 val c1 = con env c1
adamc@1272 163 val c2 = con env c2
adamc@1272 164 in
adamc@1272 165 case #1 c1 of
adamc@1272 166 CAbs (_, _, b) =>
adamc@1272 167 con (KnownC c2 :: deKnown env) b
adamc@1272 168
adamc@1272 169 | CApp ((CMap (dom, ran), _), f) =>
adamc@1272 170 (case #1 c2 of
adamc@1272 171 CRecord (_, []) => (CRecord (ran, []), loc)
adamc@1272 172 | CRecord (_, (x, c) :: rest) =>
adamc@1272 173 con (deKnown env)
adamc@1272 174 (CConcat ((CRecord (ran, [(x, (CApp (f, c), loc))]), loc),
adamc@1272 175 (CApp (c1, (CRecord (dom, rest), loc)), loc)), loc)
adamc@1272 176 | _ => (CApp (c1, c2), loc))
adamc@1272 177
adamc@1272 178 | _ => (CApp (c1, c2), loc)
adamc@1272 179 end
adamc@1272 180 | CAbs (x, k, b) => (CAbs (x, k, con (UnknownC :: env) b), loc)
adamc@1272 181
adamc@1272 182 | CKApp (c1, k) =>
adamc@1272 183 let
adamc@1272 184 val c1 = con env c1
adamc@1272 185 in
adamc@1272 186 case #1 c1 of
adamc@1272 187 CKAbs (_, b) =>
adamc@1272 188 con (deKnown env) b
adamc@1272 189
adamc@1272 190 | _ => (CKApp (c1, k), loc)
adamc@1272 191 end
adamc@1272 192 | CKAbs (x, b) => (CKAbs (x, con env b), loc)
adamc@1272 193
adamc@1272 194 | CName _ => all
adamc@1272 195
adamc@1272 196 | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (con env x, con env c)) xcs), loc)
adamc@1272 197 | CConcat (c1, c2) =>
adamc@1272 198 let
adamc@1272 199 val c1 = con env c1
adamc@1272 200 val c2 = con env c2
adamc@1272 201 in
adamc@1272 202 case (#1 c1, #1 c2) of
adamc@1272 203 (CRecord (k, xcs1), CRecord (_, xcs2)) =>
adamc@1272 204 (CRecord (k, xcs1 @ xcs2), loc)
adamc@1272 205 | (CRecord (_, []), _) => c2
adamc@1272 206 | (_, CRecord (_, [])) => c1
adamc@1272 207 | _ => (CConcat (c1, c2), loc)
adamc@1272 208 end
adamc@1272 209 | CMap _ => all
adamc@1272 210
adamc@1272 211 | CUnit => all
adamc@1272 212
adamc@1272 213 | CTuple cs => (CTuple (map (con env) cs), loc)
adamc@1272 214 | CProj (c, n) =>
adamc@1272 215 let
adamc@1272 216 val c = con env c
adamc@1272 217 in
adamc@1272 218 case #1 c of
adamc@1272 219 CTuple cs => List.nth (cs, n - 1)
adamc@1272 220 | _ => (CProj (c, n), loc)
adamc@1272 221 end)
adamc@1272 222
adamc@1272 223 fun patCon pc =
adamc@1272 224 case pc of
adamc@1272 225 PConVar _ => pc
adamc@1272 226 | PConFfi {mod = m, datatyp, params, con = c, arg, kind} =>
adamc@1272 227 PConFfi {mod = m, datatyp = datatyp, params = params, con = c,
adamc@1272 228 arg = Option.map (con (map (fn _ => UnknownC) params)) arg,
adamc@1272 229 kind = kind}
adamc@1272 230
adamc@512 231 fun exp env (all as (e, loc)) =
adamc@512 232 case e of
adamc@512 233 EPrim _ => all
adamc@512 234 | ERel n =>
adamc@512 235 let
adamc@1272 236 fun find (n', env, nudge, liftC, liftE) =
adamc@512 237 case env of
adamc@642 238 [] => (ERel (n + nudge), loc)
adamc@1272 239 | Lift (liftC', liftE') :: rest => find (n', rest, nudge + liftE', liftC + liftC', liftE + liftE')
adamc@1272 240 | UnknownC :: rest => find (n', rest, nudge, liftC + 1, liftE)
adamc@1272 241 | KnownC _ :: rest => find (n', rest, nudge, liftC, liftE)
adamc@512 242 | Unknown :: rest =>
adamc@512 243 if n' = 0 then
adamc@512 244 (ERel (n + nudge), loc)
adamc@512 245 else
adamc@1272 246 find (n' - 1, rest, nudge, liftC, liftE + 1)
adamc@512 247 | Known e :: rest =>
adamc@512 248 if n' = 0 then
adamc@512 249 ((*print "SUBSTITUTING\n";*)
adamc@1272 250 exp (Lift (liftC, liftE) :: rest) e)
adamc@512 251 else
adamc@1272 252 find (n' - 1, rest, nudge - 1, liftC, liftE)
adamc@512 253 in
adamc@1272 254 find (n, env, 0, 0, 0)
adamc@512 255 end
adamc@512 256 | ENamed _ => all
adamc@1272 257 | ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc, map (con env) cs, Option.map (exp env) eo), loc)
adamc@512 258 | EFfi _ => all
adamc@512 259 | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc)
adamc@512 260
adamc@512 261 | EApp (e1, e2) =>
adamc@512 262 let
adamc@512 263 val e1 = exp env e1
adamc@512 264 val e2 = exp env e2
adamc@512 265 in
adamc@512 266 case #1 e1 of
adamc@512 267 EAbs (_, _, _, b) => exp (Known e2 :: deKnown env) b
adamc@512 268 | _ => (EApp (e1, e2), loc)
adamc@512 269 end
adamc@512 270
adamc@1272 271 | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (Unknown :: env) e), loc)
adamc@512 272
adamc@1272 273 | ECApp (e, c) =>
adamc@1272 274 let
adamc@1272 275 val e = exp env e
adamc@1272 276 val c = con env c
adamc@1272 277 in
adamc@1272 278 case #1 e of
adamc@1272 279 ECAbs (_, _, b) => exp (KnownC c :: deKnown env) b
adamc@1272 280 | _ => (ECApp (e, c), loc)
adamc@1272 281 end
adamc@721 282
adamc@1272 283 | ECAbs (x, k, e) => (ECAbs (x, k, exp (UnknownC :: env) e), loc)
adamc@512 284
adamc@626 285 | EKApp (e, k) => (EKApp (exp env e, k), loc)
adamc@626 286 | EKAbs (x, e) => (EKAbs (x, exp env e), loc)
adamc@512 287
adamc@1272 288 | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc)
adamc@1278 289 | EField (e, c, {field = f, rest = r}) =>
adamc@512 290 let
adamc@512 291 val e = exp env e
adamc@1272 292 val c = con env c
adamc@512 293
adamc@1278 294 fun default () = (EField (e, c, {field = con env f, rest = con env r}), loc)
adamc@512 295 in
adamc@512 296 case (#1 e, #1 c) of
adamc@512 297 (ERecord xcs, CName x) =>
adamc@512 298 (case List.find (fn ((CName x', _), _, _) => x' = x | _ => false) xcs of
adamc@512 299 NONE => default ()
adamc@512 300 | SOME (_, e, _) => e)
adamc@512 301 | _ => default ()
adamc@512 302 end
adamc@512 303
adamc@1272 304 | EConcat (e1, c1, e2, c2) => (EConcat (exp env e1, con env c1, exp env e2, con env c2), loc)
adamc@1272 305 | ECut (e, c, {field = f, rest = r}) => (ECut (exp env e,
adamc@1272 306 con env c,
adamc@1272 307 {field = con env f, rest = con env r}), loc)
adamc@1272 308 | ECutMulti (e, c, {rest = r}) => (ECutMulti (exp env e, con env c, {rest = con env r}), loc)
adamc@512 309
adamc@1272 310 | ECase (e, pes, {disc = d, result = r}) =>
adamc@512 311 let
adamc@1272 312 val others = {disc = con env d, result = con env r}
adamc@1272 313
adamc@512 314 fun patBinds (p, _) =
adamc@512 315 case p of
adamc@512 316 PWild => 0
adamc@512 317 | PVar _ => 1
adamc@512 318 | PPrim _ => 0
adamc@512 319 | PCon (_, _, _, NONE) => 0
adamc@512 320 | PCon (_, _, _, SOME p) => patBinds p
adamc@512 321 | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts
adamc@1062 322
adamc@1272 323 fun pat (all as (p, loc)) =
adamc@1272 324 case p of
adamc@1272 325 PWild => all
adamc@1272 326 | PVar (x, t) => (PVar (x, con env t), loc)
adamc@1272 327 | PPrim _ => all
adamc@1272 328 | PCon (dk, pc, cs, po) =>
adamc@1272 329 (PCon (dk, patCon pc, map (con env) cs, Option.map pat po), loc)
adamc@1272 330 | PRecord xpts => (PRecord (map (fn (x, p, t) => (x, pat p, con env t)) xpts), loc)
adamc@1272 331
adamc@1062 332 fun push () =
adamc@1062 333 (ECase (exp env e,
adamc@1272 334 map (fn (p, e) => (pat p,
adamc@1062 335 exp (List.tabulate (patBinds p,
adamc@1062 336 fn _ => Unknown) @ env) e))
adamc@1062 337 pes, others), loc)
adamc@1062 338
adamc@1062 339 fun search pes =
adamc@1062 340 case pes of
adamc@1062 341 [] => push ()
adamc@1062 342 | (p, body) :: pes =>
adamc@1062 343 case match (env, p, e) of
adamc@1062 344 No => search pes
adamc@1062 345 | Maybe => push ()
adamc@1062 346 | Yes env' => exp env' body
adamc@512 347 in
adamc@1062 348 search pes
adamc@512 349 end
adamc@512 350
adamc@512 351 | EWrite e => (EWrite (exp env e), loc)
adamc@512 352 | EClosure (n, es) => (EClosure (n, map (exp env) es), loc)
adamc@512 353
adamc@1272 354 | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (Unknown :: env) e2), loc)
adamc@512 355
adamc@1272 356 | EServerCall (n, es, t) => (EServerCall (n, map (exp env) es, con env t), loc)
adamc@607 357
adamc@512 358 fun reduce file =
adamc@482 359 let
adamc@512 360 fun doDecl (d as (_, loc)) =
adamc@512 361 case #1 d of
adamc@512 362 DCon _ => d
adamc@512 363 | DDatatype _ => d
adamc@512 364 | DVal (x, n, t, e, s) =>
adamc@512 365 let
adamc@512 366 val e = exp [] e
adamc@512 367 in
adamc@512 368 (DVal (x, n, t, e, s), loc)
adamc@512 369 end
adamc@512 370 | DValRec vis =>
adamc@512 371 (DValRec (map (fn (x, n, t, e, s) => (x, n, t, exp [] e, s)) vis), loc)
adamc@512 372 | DExport _ => d
adamc@512 373 | DTable _ => d
adamc@512 374 | DSequence _ => d
adamc@754 375 | DView _ => d
adamc@512 376 | DDatabase _ => d
adamc@512 377 | DCookie _ => d
adamc@718 378 | DStyle _ => d
adamc@1075 379 | DTask (e1, e2) => (DTask (exp [] e1, exp [] e2), loc)
adamc@1199 380 | DPolicy e1 => (DPolicy (exp [] e1), loc)
adam@1294 381 | DOnError _ => d
adamc@482 382 in
adamc@512 383 map doDecl file
adamc@482 384 end
adamc@482 385
adamc@642 386 val reduceExp = exp []
adamc@1276 387 val reduceCon = con []
adamc@642 388
adamc@482 389 end