Mercurial > urweb

annotate src/reduce_local.sml @ 1658:de0a34e28bfa

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tweak new unification heuristic
author Adam Chlipala <adam@chlipala.net>
date Thu, 05 Jan 2012 19:13:31 -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