Mercurial > urweb

annotate src/reduce.sml @ 1535:27190faa36a3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Handle case where shakeExp can remove datatype.
author Karn Kallio <kkallio@eka>
date Sat, 13 Aug 2011 00:07:28 -0430
parents 89d7b1c3199a
children a99b743a3087
rev   line source
adamc@20 1 (* Copyright (c) 2008, Adam Chlipala
adamc@20 2 * All rights reserved.
adamc@20 3 *
adamc@20 4 * Redistribution and use in source and binary forms, with or without
adamc@20 5 * modification, are permitted provided that the following conditions are met:
adamc@20 6 *
adamc@20 7 * - Redistributions of source code must retain the above copyright notice,
adamc@20 8 * this list of conditions and the following disclaimer.
adamc@20 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@20 10 * this list of conditions and the following disclaimer in the documentation
adamc@20 11 * and/or other materials provided with the distribution.
adamc@20 12 * - The names of contributors may not be used to endorse or promote products
adamc@20 13 * derived from this software without specific prior written permission.
adamc@20 14 *
adamc@20 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@20 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@20 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@20 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@20 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@20 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@20 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@20 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@20 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@20 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@20 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@20 26 *)
adamc@20 27
adamc@20 28 (* Simplify a Core program algebraically *)
adamc@20 29
adamc@20 30 structure Reduce :> REDUCE = struct
adamc@20 31
adamc@20 32 open Core
adamc@20 33
adamc@1016 34 structure IS = IntBinarySet
adamc@508 35 structure IM = IntBinaryMap
adamc@20 36
adamc@908 37 structure E = CoreEnv
adamc@908 38
adamc@908 39 fun multiLiftExpInExp n e =
adamc@908 40 if n = 0 then
adamc@908 41 e
adamc@908 42 else
adamc@908 43 multiLiftExpInExp (n - 1) (E.liftExpInExp 0 e)
adamc@908 44
adamc@1179 45 val count = CoreUtil.Exp.foldB {kind = fn (_, _, c) => c,
adamc@1179 46 con = fn (_, _, c) => c,
adamc@1179 47 exp = fn (x, e, c) =>
adamc@1179 48 case e of
adamc@1179 49 ERel x' => if x = x' then c + 1 else c
adamc@1179 50 | _ => c,
adamc@1179 51 bind = fn (x, b) =>
adamc@1179 52 case b of
adamc@1179 53 CoreUtil.Exp.RelE _ => x+1
adamc@1179 54 | _ => x} 0 0
adamc@1179 55
adamc@909 56 val dangling =
adamc@909 57 CoreUtil.Exp.existsB {kind = fn _ => false,
adamc@909 58 con = fn _ => false,
adamc@909 59 exp = fn (n, e) =>
adamc@909 60 case e of
adamc@909 61 ERel n' => n' >= n
adamc@909 62 | _ => false,
adamc@909 63 bind = fn (n, b) =>
adamc@909 64 case b of
adamc@909 65 CoreUtil.Exp.RelE _ => n + 1
adamc@909 66 | _ => n}
adamc@909 67
adamc@1272 68 val cdangling =
adamc@1272 69 CoreUtil.Exp.existsB {kind = fn _ => false,
adamc@1272 70 con = fn (n, c) =>
adamc@1272 71 case c of
adamc@1272 72 CRel n' => n' >= n
adamc@1272 73 | _ => false,
adamc@1272 74 exp = fn _ => false,
adamc@1272 75 bind = fn (n, b) =>
adamc@1272 76 case b of
adamc@1272 77 CoreUtil.Exp.RelC _ => n + 1
adamc@1272 78 | _ => n}
adamc@1272 79
adamc@508 80 datatype env_item =
adamc@626 81 UnknownK
adamc@626 82 | KnownK of kind
adamc@626 83
adamc@626 84 | UnknownC
adamc@508 85 | KnownC of con
adamc@21 86
adamc@508 87 | UnknownE
adamc@508 88 | KnownE of exp
adamc@20 89
adamc@626 90 | Lift of int * int * int
adamc@20 91
adamc@909 92 val edepth = foldl (fn (UnknownE, n) => n + 1
adamc@909 93 | (KnownE _, n) => n + 1
adamc@909 94 | (_, n) => n) 0
adamc@909 95
adamc@909 96 val edepth' = foldl (fn (UnknownE, n) => n + 1
adamc@909 97 | (KnownE _, n) => n + 1
adamc@909 98 | (Lift (_, _, n'), n) => n + n'
adamc@909 99 | (_, n) => n) 0
adamc@909 100
adamc@1272 101 val cdepth = foldl (fn (UnknownC, n) => n + 1
adamc@1272 102 | (KnownC _, n) => n + 1
adamc@1272 103 | (_, n) => n) 0
adamc@1272 104
adamc@1272 105 val cdepth' = foldl (fn (UnknownC, n) => n + 1
adamc@1272 106 | (KnownC _, n) => n + 1
adamc@1272 107 | (Lift (_, n', _), n) => n + n'
adamc@1272 108 | (_, n) => n) 0
adamc@1272 109
adamc@508 110 type env = env_item list
adamc@20 111
adamc@510 112 fun ei2s ei =
adamc@510 113 case ei of
adamc@626 114 UnknownK => "UK"
adamc@626 115 | KnownK _ => "KK"
adamc@626 116 | UnknownC => "UC"
adamc@510 117 | KnownC _ => "KC"
adamc@510 118 | UnknownE => "UE"
adamc@510 119 | KnownE _ => "KE"
adamc@626 120 | Lift (_, n1, n2) => "(" ^ Int.toString n1 ^ ", " ^ Int.toString n2 ^ ")"
adamc@510 121
adamc@510 122 fun e2s env = String.concatWith " " (map ei2s env)
adamc@510 123
adamc@909 124 (*val deKnown = List.filter (fn KnownC _ => false
adamc@510 125 | KnownE _ => false
adamc@626 126 | KnownK _ => false
adamc@909 127 | _ => true)*)
adamc@909 128
adamc@909 129 val deKnown = ListUtil.mapConcat (fn KnownC _ => []
adamc@909 130 | KnownE _ => []
adamc@909 131 | KnownK _ => []
adamc@909 132 | Lift (nk, nc, ne) => List.tabulate (nk, fn _ => UnknownK)
adamc@909 133 @ List.tabulate (nc, fn _ => UnknownC)
adamc@909 134 @ List.tabulate (ne, fn _ => UnknownE)
adamc@909 135 | x => [x])
adamc@510 136
adamc@930 137 datatype result = Yes of env | No | Maybe
adamc@930 138
adamc@930 139 fun match (env, p : pat, e : exp) =
adamc@942 140 let
adamc@942 141 val baseline = length env
adamc@930 142
adamc@942 143 fun match (env, p, e) =
adamc@942 144 case (#1 p, #1 e) of
adamc@942 145 (PWild, _) => Yes env
adamc@942 146 | (PVar (x, t), _) => Yes (KnownE (multiLiftExpInExp (length env - baseline) e) :: env)
adamc@930 147
adamc@942 148 | (PPrim p, EPrim p') =>
adamc@942 149 if Prim.equal (p, p') then
adamc@942 150 Yes env
adamc@942 151 else
adamc@942 152 No
adamc@930 153
adamc@942 154 | (PCon (_, PConVar n1, _, NONE), ECon (_, PConVar n2, _, NONE)) =>
adamc@942 155 if n1 = n2 then
adamc@942 156 Yes env
adamc@942 157 else
adamc@942 158 No
adamc@930 159
adamc@942 160 | (PCon (_, PConVar n1, _, SOME p), ECon (_, PConVar n2, _, SOME e)) =>
adamc@942 161 if n1 = n2 then
adamc@942 162 match (env, p, e)
adamc@942 163 else
adamc@942 164 No
adamc@930 165
adamc@942 166 | (PCon (_, PConFfi {mod = m1, con = con1, ...}, _, NONE),
adamc@942 167 ECon (_, PConFfi {mod = m2, con = con2, ...}, _, NONE)) =>
adamc@942 168 if m1 = m2 andalso con1 = con2 then
adamc@942 169 Yes env
adamc@942 170 else
adamc@942 171 No
adamc@930 172
adamc@942 173 | (PCon (_, PConFfi {mod = m1, con = con1, ...}, _, SOME ep),
adamc@942 174 ECon (_, PConFfi {mod = m2, con = con2, ...}, _, SOME e)) =>
adamc@942 175 if m1 = m2 andalso con1 = con2 then
adamc@942 176 match (env, p, e)
adamc@942 177 else
adamc@942 178 No
adamc@930 179
adamc@942 180 | (PRecord xps, ERecord xes) =>
adamc@942 181 if List.exists (fn ((CName _, _), _, _) => false
adamc@942 182 | _ => true) xes then
adamc@942 183 Maybe
adamc@942 184 else
adamc@942 185 let
adamc@942 186 fun consider (xps, env) =
adamc@942 187 case xps of
adamc@942 188 [] => Yes env
adamc@942 189 | (x, p, _) :: rest =>
adamc@942 190 case List.find (fn ((CName x', _), _, _) => x' = x
adamc@942 191 | _ => false) xes of
adamc@942 192 NONE => No
adamc@942 193 | SOME (_, e, _) =>
adamc@942 194 case match (env, p, e) of
adamc@942 195 No => No
adamc@942 196 | Maybe => Maybe
adamc@942 197 | Yes env => consider (rest, env)
adamc@942 198 in
adamc@942 199 consider (xps, env)
adamc@942 200 end
adamc@942 201
adamc@942 202 | _ => Maybe
adamc@942 203 in
adamc@942 204 match (env, p, e)
adamc@942 205 end
adamc@930 206
adamc@626 207 fun kindConAndExp (namedC, namedE) =
adamc@508 208 let
adamc@626 209 fun kind env (all as (k, loc)) =
adamc@626 210 case k of
adamc@626 211 KType => all
adamc@626 212 | KArrow (k1, k2) => (KArrow (kind env k1, kind env k2), loc)
adamc@626 213 | KName => all
adamc@626 214 | KRecord k => (KRecord (kind env k), loc)
adamc@626 215 | KUnit => all
adamc@626 216 | KTuple ks => (KTuple (map (kind env) ks), loc)
adamc@626 217
adamc@626 218 | KRel n =>
adamc@626 219 let
adamc@626 220 fun find (n', env, nudge, lift) =
adamc@626 221 case env of
adamc@626 222 [] => raise Fail "Reduce.kind: KRel"
adamc@626 223 | UnknownC :: rest => find (n', rest, nudge, lift)
adamc@626 224 | KnownC _ :: rest => find (n', rest, nudge, lift)
adamc@626 225 | UnknownE :: rest => find (n', rest, nudge, lift)
adamc@626 226 | KnownE _ :: rest => find (n', rest, nudge, lift)
adamc@626 227 | Lift (lift', _, _) :: rest => find (n', rest, nudge + lift', lift + lift')
adamc@626 228 | UnknownK :: rest =>
adamc@626 229 if n' = 0 then
adamc@626 230 (KRel (n + nudge), loc)
adamc@626 231 else
adamc@626 232 find (n' - 1, rest, nudge, lift + 1)
adamc@626 233 | KnownK k :: rest =>
adamc@626 234 if n' = 0 then
adamc@626 235 kind (Lift (lift, 0, 0) :: rest) k
adamc@626 236 else
adamc@626 237 find (n' - 1, rest, nudge - 1, lift)
adamc@626 238 in
adamc@626 239 find (n, env, 0, 0)
adamc@626 240 end
adamc@626 241 | KFun (x, k) => (KFun (x, kind (UnknownK :: env) k), loc)
adamc@626 242
adamc@508 243 fun con env (all as (c, loc)) =
adamc@510 244 ((*Print.prefaces "con" [("c", CorePrint.p_con CoreEnv.empty all)];*)
adamc@508 245 case c of
adamc@508 246 TFun (c1, c2) => (TFun (con env c1, con env c2), loc)
adamc@626 247 | TCFun (x, k, c2) => (TCFun (x, kind env k, con (UnknownC :: env) c2), loc)
adamc@626 248 | TKFun (x, c2) => (TKFun (x, con (UnknownK :: env) c2), loc)
adamc@508 249 | TRecord c => (TRecord (con env c), loc)
adamc@215 250
adamc@508 251 | CRel n =>
adamc@508 252 let
adamc@626 253 fun find (n', env, nudge, liftK, liftC) =
adamc@510 254 case env of
adamc@510 255 [] => raise Fail "Reduce.con: CRel"
adamc@626 256 | UnknownK :: rest => find (n', rest, nudge, liftK + 1, liftC)
adamc@626 257 | KnownK _ :: rest => find (n', rest, nudge, liftK, liftC)
adamc@626 258 | UnknownE :: rest => find (n', rest, nudge, liftK, liftC)
adamc@626 259 | KnownE _ :: rest => find (n', rest, nudge, liftK, liftC)
adamc@626 260 | Lift (liftK', liftC', _) :: rest => find (n', rest, nudge + liftC',
adamc@626 261 liftK + liftK', liftC + liftC')
adamc@510 262 | UnknownC :: rest =>
adamc@510 263 if n' = 0 then
adamc@510 264 (CRel (n + nudge), loc)
adamc@510 265 else
adamc@626 266 find (n' - 1, rest, nudge, liftK, liftC + 1)
adamc@510 267 | KnownC c :: rest =>
adamc@510 268 if n' = 0 then
adamc@626 269 con (Lift (liftK, liftC, 0) :: rest) c
adamc@510 270 else
adamc@626 271 find (n' - 1, rest, nudge - 1, liftK, liftC)
adamc@508 272 in
adamc@510 273 (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*)
adamc@626 274 find (n, env, 0, 0, 0)
adamc@508 275 end
adamc@508 276 | CNamed n =>
adamc@508 277 (case IM.find (namedC, n) of
adamc@508 278 NONE => all
adamc@508 279 | SOME c => c)
adamc@508 280 | CFfi _ => all
adamc@508 281 | CApp (c1, c2) =>
adamc@508 282 let
adamc@508 283 val c1 = con env c1
adamc@508 284 val c2 = con env c2
adamc@508 285 in
adamc@508 286 case #1 c1 of
adamc@508 287 CAbs (_, _, b) =>
adamc@510 288 con (KnownC c2 :: deKnown env) b
adamc@215 289
adamc@621 290 | CApp ((CMap (dom, ran), _), f) =>
adamc@508 291 (case #1 c2 of
adamc@626 292 CRecord (_, []) => (CRecord (kind env ran, []), loc)
adamc@621 293 | CRecord (_, (x, c) :: rest) =>
adamc@510 294 con (deKnown env)
adamc@621 295 (CConcat ((CRecord (ran, [(x, (CApp (f, c), loc))]), loc),
adamc@626 296 (CApp (c1, (CRecord (kind env dom, rest), loc)), loc)), loc)
adamc@508 297 | _ => (CApp (c1, c2), loc))
adamc@20 298
adamc@508 299 | _ => (CApp (c1, c2), loc)
adamc@508 300 end
adamc@626 301 | CAbs (x, k, b) => (CAbs (x, kind env k, con (UnknownC :: env) b), loc)
adamc@626 302
adamc@626 303 | CKApp (c1, k) =>
adamc@626 304 let
adamc@626 305 val c1 = con env c1
adamc@626 306 in
adamc@626 307 case #1 c1 of
adamc@626 308 CKAbs (_, b) =>
adamc@626 309 con (KnownK k :: deKnown env) b
adamc@626 310
adamc@626 311 | _ => (CKApp (c1, kind env k), loc)
adamc@626 312 end
adamc@626 313 | CKAbs (x, b) => (CKAbs (x, con (UnknownK :: env) b), loc)
adamc@20 314
adamc@508 315 | CName _ => all
adamc@21 316
adamc@626 317 | CRecord (k, xcs) => (CRecord (kind env k, map (fn (x, c) => (con env x, con env c)) xcs), loc)
adamc@508 318 | CConcat (c1, c2) =>
adamc@508 319 let
adamc@508 320 val c1 = con env c1
adamc@508 321 val c2 = con env c2
adamc@508 322 in
adamc@508 323 case (#1 c1, #1 c2) of
adamc@508 324 (CRecord (k, xcs1), CRecord (_, xcs2)) =>
adamc@626 325 (CRecord (kind env k, xcs1 @ xcs2), loc)
adamc@1122 326 | (CRecord (_, []), _) => c2
adamc@1122 327 | (_, CRecord (_, [])) => c1
adamc@508 328 | _ => (CConcat (c1, c2), loc)
adamc@508 329 end
adamc@626 330 | CMap (dom, ran) => (CMap (kind env dom, kind env ran), loc)
adamc@74 331
adamc@508 332 | CUnit => all
adamc@21 333
adamc@508 334 | CTuple cs => (CTuple (map (con env) cs), loc)
adamc@508 335 | CProj (c, n) =>
adamc@508 336 let
adamc@508 337 val c = con env c
adamc@508 338 in
adamc@508 339 case #1 c of
adamc@508 340 CTuple cs => List.nth (cs, n - 1)
adamc@508 341 | _ => (CProj (c, n), loc)
adamc@510 342 end)
adamc@22 343
adamc@509 344 fun patCon pc =
adamc@509 345 case pc of
adamc@509 346 PConVar _ => pc
adamc@509 347 | PConFfi {mod = m, datatyp, params, con = c, arg, kind} =>
adamc@509 348 PConFfi {mod = m, datatyp = datatyp, params = params, con = c,
adamc@509 349 arg = Option.map (con (map (fn _ => UnknownC) params)) arg,
adamc@509 350 kind = kind}
adamc@509 351
adamc@509 352
adamc@509 353 val k = (KType, ErrorMsg.dummySpan)
adamc@509 354 fun doPart e (this as (x, t), rest) =
adamc@509 355 ((x, (EField (e, x, {field = t, rest = (CRecord (k, rest), #2 t)}), #2 t), t),
adamc@509 356 this :: rest)
adamc@509 357
adamc@509 358 fun exp env (all as (e, loc)) =
adamc@909 359 let
adamc@909 360 (*val () = Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all),
adamc@909 361 ("env", Print.PD.string (e2s env))]*)
adamc@1176 362 (*val () = if dangling (edepth env) all then
adamc@909 363 (Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all),
adamc@909 364 ("env", Print.PD.string (e2s env))];
adamc@909 365 raise Fail "!")
adamc@909 366 else
adamc@1176 367 ()*)
adamc@1272 368 (*val () = if cdangling (cdepth env) all then
adamc@1272 369 Print.prefaces "Bad exp" [("e", CorePrint.p_exp CoreEnv.empty all),
adamc@1272 370 ("env", Print.PD.string (e2s env))]
adamc@1272 371 else
adamc@1272 372 ()*)
adamc@509 373
kkallio@1533 374 fun patBinds (p, _) =
kkallio@1533 375 case p of
kkallio@1533 376 PWild => 0
kkallio@1533 377 | PVar _ => 1
kkallio@1533 378 | PPrim _ => 0
kkallio@1533 379 | PCon (_, _, _, NONE) => 0
kkallio@1533 380 | PCon (_, _, _, SOME p) => patBinds p
kkallio@1533 381 | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts
kkallio@1533 382
adamc@909 383 val r = case e of
adamc@909 384 EPrim _ => all
adamc@909 385 | ERel n =>
adamc@909 386 let
adamc@909 387 fun find (n', env, nudge, liftK, liftC, liftE) =
adamc@909 388 case env of
adamc@909 389 [] => raise Fail ("Reduce.exp: ERel (" ^ ErrorMsg.spanToString loc ^ ")")
adamc@909 390 | UnknownK :: rest => find (n', rest, nudge, liftK + 1, liftC, liftE)
adamc@909 391 | KnownK _ :: rest => find (n', rest, nudge, liftK, liftC, liftE)
adamc@909 392 | UnknownC :: rest => find (n', rest, nudge, liftK, liftC + 1, liftE)
adamc@909 393 | KnownC _ :: rest => find (n', rest, nudge, liftK, liftC, liftE)
adamc@909 394 | Lift (liftK', liftC', liftE') :: rest =>
adamc@909 395 find (n', rest, nudge + liftE',
adamc@909 396 liftK + liftK', liftC + liftC', liftE + liftE')
adamc@909 397 | UnknownE :: rest =>
adamc@909 398 if n' = 0 then
adamc@909 399 (ERel (n + nudge), loc)
adamc@909 400 else
adamc@909 401 find (n' - 1, rest, nudge, liftK, liftC, liftE + 1)
adamc@909 402 | KnownE e :: rest =>
adamc@909 403 if n' = 0 then
adamc@909 404 ((*print "SUBSTITUTING\n";*)
adamc@909 405 exp (Lift (liftK, liftC, liftE) :: rest) e)
adamc@909 406 else
adamc@909 407 find (n' - 1, rest, nudge - 1, liftK, liftC, liftE)
adamc@909 408 in
adamc@909 409 (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*)
adamc@909 410 find (n, env, 0, 0, 0, 0)
adamc@909 411 end
adamc@909 412 | ENamed n =>
adamc@909 413 (case IM.find (namedE, n) of
adamc@909 414 NONE => all
adamc@909 415 | SOME e => e)
adamc@909 416 | ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc,
adamc@909 417 map (con env) cs, Option.map (exp env) eo), loc)
adamc@909 418 | EFfi _ => all
adamc@909 419 | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc)
adamc@908 420
adamc@909 421 (*| EApp (
adamc@909 422 (EApp
adamc@909 423 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _),
adamc@909 424 (EFfi ("Basis", "transaction_monad"), _)), _),
adamc@909 425 (ECase (ed, pes, {disc, ...}), _)), _),
adamc@909 426 trans2) =>
adamc@909 427 let
adamc@909 428 val e' = (EFfi ("Basis", "bind"), loc)
adamc@909 429 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
adamc@909 430 val e' = (ECApp (e', t1), loc)
adamc@909 431 val e' = (ECApp (e', t2), loc)
adamc@909 432 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
adamc@908 433
adamc@909 434 val pes = map (fn (p, e) =>
adamc@909 435 let
adamc@909 436 val e' = (EApp (e', e), loc)
adamc@909 437 val e' = (EApp (e',
adamc@909 438 multiLiftExpInExp (E.patBindsN p)
adamc@909 439 trans2), loc)
adamc@909 440 val e' = exp env e'
adamc@909 441 in
adamc@909 442 (p, e')
adamc@909 443 end) pes
adamc@909 444 in
adamc@909 445 (ECase (exp env ed,
adamc@909 446 pes,
adamc@909 447 {disc = con env disc,
adamc@909 448 result = (CApp ((CFfi ("Basis", "transaction"), loc), con env t2), loc)}),
adamc@909 449 loc)
adamc@909 450 end*)
adamc@908 451
adamc@909 452 | EApp (e1, e2) =>
adamc@909 453 let
adamc@910 454 val env' = deKnown env
adamc@910 455
adamc@909 456 val e1 = exp env e1
adamc@909 457 val e2 = exp env e2
adamc@909 458 in
adamc@1179 459 case #1 e1 of
adamc@1179 460 EAbs (_, _, _, b) =>
adamc@1181 461 let
adamc@1181 462 val r = exp (KnownE e2 :: env') b
adamc@1181 463 in
adamc@1181 464 (*Print.prefaces "eapp" [("b", CorePrint.p_exp CoreEnv.empty b),
adamc@1181 465 ("env", Print.PD.string (e2s env')),
adamc@1181 466 ("e2", CorePrint.p_exp CoreEnv.empty e2),
adamc@1181 467 ("r", CorePrint.p_exp CoreEnv.empty r)];*)
adamc@1181 468 r
adamc@1181 469 end
kkallio@1533 470 | ECase (e, pes, cc as {disc, result = res as (TFun (_, c2), _)}) =>
kkallio@1533 471 let
kkallio@1533 472 val pes' = map (fn (p, body) =>
kkallio@1533 473 let
adam@1534 474 val env' = List.tabulate (patBinds p, fn _ => UnknownE) @ deKnown env
kkallio@1533 475 val body' = exp env' (EApp (body, multiLiftExpInExp (patBinds p) e2), #2 body)
kkallio@1533 476 in
kkallio@1533 477 (p, body')
kkallio@1533 478 end) pes
kkallio@1533 479
kkallio@1533 480 val cc' = {disc = disc, result = c2}
kkallio@1533 481 in
kkallio@1533 482 (ECase (e, pes', cc'), loc)
kkallio@1533 483 end
adamc@1179 484 | _ => (EApp (e1, e2), loc)
adamc@909 485 end
adamc@509 486
adamc@909 487 | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (UnknownE :: env) e), loc)
adamc@509 488
adamc@909 489 | ECApp (e, c) =>
adamc@909 490 let
adamc@909 491 val e = exp env e
adamc@909 492 val c = con env c
adamc@909 493 in
adamc@909 494 case #1 e of
adamc@1181 495 ECAbs (_, _, b) =>
adamc@1181 496 let
adamc@1181 497 val r = exp (KnownC c :: deKnown env) b
adamc@1181 498 in
adamc@1181 499 (*Print.prefaces "csub" [("l", Print.PD.string (ErrorMsg.spanToString loc)),
adamc@1181 500 ("env", Print.PD.string (e2s (deKnown env))),
adamc@1181 501 ("b", CorePrint.p_exp CoreEnv.empty b),
adamc@1181 502 ("c", CorePrint.p_con CoreEnv.empty c),
adamc@1181 503 ("r", CorePrint.p_exp CoreEnv.empty r)];*)
adamc@1181 504 r
adamc@1181 505 end
kkallio@1533 506 | ECase (e, pes, cc as {disc, result = res as (TCFun (_, _, c'), _)}) =>
kkallio@1533 507 let
kkallio@1533 508 val pes' = map (fn (p, body) =>
kkallio@1533 509 let
adam@1534 510 val env' = List.tabulate (patBinds p, fn _ => UnknownE) @ deKnown env
kkallio@1533 511
kkallio@1533 512 val body' = exp env' (ECApp (body, c), #2 body)
kkallio@1533 513 in
kkallio@1533 514 (p, body')
kkallio@1533 515 end) pes
kkallio@1533 516
kkallio@1533 517 val c' = E.subConInCon (0, c) c'
kkallio@1533 518 val cc' = {disc = disc, result = c'}
kkallio@1533 519 in
kkallio@1533 520 (ECase (e, pes', cc'), loc)
kkallio@1533 521 end
adamc@909 522 | _ => (ECApp (e, c), loc)
adamc@909 523 end
adamc@626 524
adamc@909 525 | ECAbs (x, k, e) => (ECAbs (x, kind env k, exp (UnknownC :: env) e), loc)
adamc@626 526
adamc@909 527 | EKApp (e, k) =>
adamc@909 528 let
adamc@909 529 val e = exp env e
adamc@909 530 in
adamc@909 531 case #1 e of
adamc@1181 532 EKAbs (_, b) =>
adamc@1181 533 let
adamc@1181 534 val r = exp (KnownK k :: deKnown env) b
adamc@1181 535 in
adamc@1181 536 (*Print.prefaces "ksub" [("l", Print.PD.string (ErrorMsg.spanToString loc)),
adamc@1181 537 ("b", CorePrint.p_exp CoreEnv.empty b),
adamc@1181 538 ("k", CorePrint.p_kind CoreEnv.empty k),
adamc@1181 539 ("r", CorePrint.p_exp CoreEnv.empty r)];*)
adamc@1181 540 r
adamc@1181 541 end
adamc@909 542 | _ => (EKApp (e, kind env k), loc)
adamc@909 543 end
adamc@509 544
adamc@909 545 | EKAbs (x, e) => (EKAbs (x, exp (UnknownK :: env) e), loc)
adamc@509 546
adamc@909 547 | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc)
adamc@909 548 | EField (e, c, {field, rest}) =>
adamc@909 549 let
adamc@909 550 val e = exp env e
adamc@909 551 val c = con env c
adamc@509 552
adamc@909 553 fun default () = (EField (e, c, {field = con env field, rest = con env rest}), loc)
adamc@909 554 in
adamc@909 555 case (#1 e, #1 c) of
adamc@909 556 (ERecord xcs, CName x) =>
adamc@909 557 (case List.find (fn ((CName x', _), _, _) => x' = x | _ => false) xcs of
adamc@909 558 NONE => default ()
adamc@909 559 | SOME (_, e, _) => e)
adamc@909 560 | _ => default ()
adamc@909 561 end
adamc@509 562
adamc@909 563 | EConcat (e1, c1, e2, c2) =>
adamc@909 564 let
adamc@909 565 val e1 = exp env e1
adamc@909 566 val e2 = exp env e2
adamc@909 567 in
adamc@909 568 case (#1 e1, #1 e2) of
adamc@909 569 (ERecord xes1, ERecord xes2) => (ERecord (xes1 @ xes2), loc)
adamc@909 570 | _ =>
adamc@909 571 let
adamc@909 572 val c1 = con env c1
adamc@909 573 val c2 = con env c2
adamc@909 574 in
adamc@909 575 case (#1 c1, #1 c2) of
adamc@909 576 (CRecord (k, xcs1), CRecord (_, xcs2)) =>
adamc@909 577 let
adamc@909 578 val (xes1, rest) = ListUtil.foldlMap (doPart e1) [] xcs1
adamc@909 579 val (xes2, _) = ListUtil.foldlMap (doPart e2) rest xcs2
adamc@909 580 in
adamc@909 581 exp (deKnown env) (ERecord (xes1 @ xes2), loc)
adamc@909 582 end
adamc@909 583 | _ => (EConcat (e1, c1, e2, c2), loc)
adamc@909 584 end
adamc@909 585 end
adamc@509 586
adamc@909 587 | ECut (e, c, {field, rest}) =>
adamc@909 588 let
adamc@909 589 val e = exp env e
adamc@909 590 val c = con env c
adamc@509 591
adamc@909 592 fun default () =
adamc@909 593 let
adamc@909 594 val rest = con env rest
adamc@909 595 in
adamc@909 596 case #1 rest of
adamc@909 597 CRecord (k, xcs) =>
adamc@909 598 let
adamc@909 599 val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs
adamc@909 600 in
adamc@909 601 exp (deKnown env) (ERecord xes, loc)
adamc@909 602 end
adamc@909 603 | _ => (ECut (e, c, {field = con env field, rest = rest}), loc)
adamc@909 604 end
adamc@909 605 in
adamc@909 606 case (#1 e, #1 c) of
adamc@909 607 (ERecord xes, CName x) =>
adamc@909 608 if List.all (fn ((CName _, _), _, _) => true | _ => false) xes then
adamc@909 609 (ERecord (List.filter (fn ((CName x', _), _, _) => x' <> x
adamc@909 610 | _ => raise Fail "Reduce: ECut") xes), loc)
adamc@909 611 else
adamc@909 612 default ()
adamc@909 613 | _ => default ()
adamc@909 614 end
adamc@509 615
adamc@909 616 | ECutMulti (e, c, {rest}) =>
adamc@909 617 let
adamc@909 618 val e = exp env e
adamc@909 619 val c = con env c
adamc@509 620
adamc@909 621 fun default () =
adamc@909 622 let
adamc@909 623 val rest = con env rest
adamc@909 624 in
adamc@909 625 case #1 rest of
adamc@909 626 CRecord (k, xcs) =>
adamc@909 627 let
adamc@909 628 val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs
adamc@909 629 in
adamc@909 630 exp (deKnown env) (ERecord xes, loc)
adamc@909 631 end
adamc@909 632 | _ => (ECutMulti (e, c, {rest = rest}), loc)
adamc@909 633 end
adamc@909 634 in
adamc@909 635 case (#1 e, #1 c) of
adamc@909 636 (ERecord xes, CRecord (_, xcs)) =>
adamc@909 637 if List.all (fn ((CName _, _), _, _) => true | _ => false) xes
adamc@909 638 andalso List.all (fn ((CName _, _), _) => true | _ => false) xcs then
adamc@909 639 (ERecord (List.filter (fn ((CName x', _), _, _) =>
adamc@909 640 List.all (fn ((CName x, _), _) => x' <> x
adamc@909 641 | _ => raise Fail "Reduce: ECutMulti [1]") xcs
adamc@909 642 | _ => raise Fail "Reduce: ECutMulti [2]") xes), loc)
adamc@909 643 else
adamc@909 644 default ()
adamc@909 645 | _ => default ()
adamc@909 646 end
adamc@823 647
adamc@909 648 | ECase (_, [((PRecord [], _), e)], _) => exp env e
adamc@909 649 | ECase (_, [((PWild, _), e)], _) => exp env e
adamc@509 650
adamc@909 651 | ECase (e, pes, {disc, result}) =>
adamc@909 652 let
adamc@909 653 fun pat (all as (p, loc)) =
adamc@909 654 case p of
adamc@909 655 PWild => all
adamc@909 656 | PVar (x, t) => (PVar (x, con env t), loc)
adamc@909 657 | PPrim _ => all
adamc@909 658 | PCon (dk, pc, cs, po) =>
adamc@909 659 (PCon (dk, patCon pc, map (con env) cs, Option.map pat po), loc)
adamc@909 660 | PRecord xpts => (PRecord (map (fn (x, p, t) => (x, pat p, con env t)) xpts), loc)
adamc@930 661
adamc@930 662 fun push () =
adamc@930 663 (ECase (exp env e,
adamc@930 664 map (fn (p, e) => (pat p,
adamc@930 665 exp (List.tabulate (patBinds p,
adamc@930 666 fn _ => UnknownE) @ env) e))
adamc@930 667 pes, {disc = con env disc, result = con env result}), loc)
adamc@930 668
adamc@930 669 fun search pes =
adamc@930 670 case pes of
adamc@930 671 [] => push ()
adamc@930 672 | (p, body) :: pes =>
adamc@930 673 case match (env, p, e) of
adamc@930 674 No => search pes
adamc@930 675 | Maybe => push ()
adamc@930 676 | Yes env' => exp env' body
adamc@909 677 in
adamc@930 678 search pes
adamc@909 679 end
adamc@509 680
adamc@909 681 | EWrite e => (EWrite (exp env e), loc)
adamc@909 682 | EClosure (n, es) => (EClosure (n, map (exp env) es), loc)
adamc@607 683
adamc@910 684 | ELet (x, t, e1, e2) =>
adam@1289 685 let
adam@1289 686 val t = con env t
adam@1289 687 in
adam@1289 688 if ESpecialize.functionInside t then
adam@1289 689 exp (KnownE e1 :: env) e2
adam@1289 690 else
adam@1314 691 (ELet (x, t, exp env e1, exp (UnknownE :: env) e2), loc)
adam@1289 692 end
adamc@909 693
adamc@1020 694 | EServerCall (n, es, t) => (EServerCall (n, map (exp env) es, con env t), loc)
adamc@909 695 in
adamc@909 696 (*if dangling (edepth' (deKnown env)) r then
adamc@909 697 (Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all),
adamc@909 698 ("r", CorePrint.p_exp CoreEnv.empty r)];
adamc@909 699 raise Fail "!!")
adamc@909 700 else
adamc@909 701 ();*)
adamc@1272 702 (*if cdangling (cdepth' (deKnown env)) r then
adamc@1272 703 (Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all),
adamc@1272 704 ("r", CorePrint.p_exp CoreEnv.empty r)];
adamc@1272 705 raise Fail "!!")
adamc@1272 706 else
adamc@1272 707 ();*)
adamc@909 708 r
adamc@909 709 end
adamc@417 710 in
adamc@626 711 {kind = kind, con = con, exp = exp}
adamc@417 712 end
adamc@21 713
adamc@626 714 fun kind namedC env k = #kind (kindConAndExp (namedC, IM.empty)) env k
adamc@626 715 fun con namedC env c = #con (kindConAndExp (namedC, IM.empty)) env c
adamc@626 716 fun exp (namedC, namedE) env e = #exp (kindConAndExp (namedC, namedE)) env e
adamc@20 717
adamc@508 718 fun reduce file =
adamc@508 719 let
adamc@1016 720 val uses = CoreUtil.File.fold {kind = fn (_, m) => m,
adamc@1016 721 con = fn (_, m) => m,
adamc@1016 722 exp = fn (e, m) =>
adamc@1016 723 case e of
adamc@1016 724 ENamed n => IM.insert (m, n, 1 + Option.getOpt (IM.find (m, n), 0))
adamc@1016 725 | _ => m,
adamc@1016 726 decl = fn (_, m) => m}
adamc@1016 727 IM.empty file
adamc@1016 728
adamc@1016 729 fun isPoly names = CoreUtil.Con.exists {kind = fn _ => false,
adamc@1016 730 con = fn TCFun _ => true
adamc@1016 731 | TKFun _ => true
adamc@1016 732 | CNamed n => IS.member (names, n)
adamc@1016 733 | _ => false}
adamc@1016 734
adamc@1016 735 val size = CoreUtil.Exp.fold {kind = fn (_, n) => n,
adamc@1016 736 con = fn (_, n) => n,
adamc@1016 737 exp = fn (_, n) => n + 1} 0
adamc@1016 738
adamc@1016 739 fun mayInline (polyC, n, t, e) =
adamc@1240 740 let
adamc@1240 741 fun isPolicy t =
adamc@1240 742 case #1 t of
adamc@1240 743 CFfi ("Basis", "sql_policy") => true
adamc@1240 744 | TFun (_, t) => isPolicy t
adamc@1240 745 | _ => false
adamc@1240 746 in
adamc@1240 747 case IM.find (uses, n) of
adamc@1240 748 NONE => false
adamc@1240 749 | SOME count => count <= 1
adamc@1240 750 orelse (case #1 e of
adamc@1240 751 ERecord _ => true
adamc@1240 752 | _ => false)
adamc@1240 753 orelse isPolicy t
adamc@1240 754 orelse isPoly polyC t
adamc@1240 755 orelse size e <= Settings.getCoreInline ()
adamc@1240 756 end
adamc@1016 757
adamc@1016 758 fun doDecl (d as (_, loc), st as (polyC, namedC, namedE)) =
adamc@508 759 case #1 d of
adamc@508 760 DCon (x, n, k, c) =>
adamc@508 761 let
adamc@626 762 val k = kind namedC [] k
adamc@509 763 val c = con namedC [] c
adamc@508 764 in
adamc@508 765 ((DCon (x, n, k, c), loc),
adamc@1016 766 (if isPoly polyC c then
adamc@1016 767 IS.add (polyC, n)
adamc@1016 768 else
adamc@1016 769 polyC,
adamc@1016 770 IM.insert (namedC, n, c),
adamc@1016 771 namedE))
adamc@508 772 end
adamc@807 773 | DDatatype dts =>
adamc@807 774 ((DDatatype (map (fn (x, n, ps, cs) =>
adamc@807 775 let
adamc@807 776 val env = map (fn _ => UnknownC) ps
adamc@807 777 in
adamc@807 778 (x, n, ps, map (fn (x, n, co) => (x, n, Option.map (con namedC env) co)) cs)
adamc@807 779 end) dts), loc),
adamc@1016 780 (if List.exists (fn (_, _, _, cs) => List.exists (fn (_, _, co) => case co of
adamc@1016 781 NONE => false
adamc@1016 782 | SOME c => isPoly polyC c) cs)
adamc@1016 783 dts then
adamc@1016 784 foldl (fn ((_, n, _, _), polyC) => IS.add (polyC, n)) polyC dts
adamc@1016 785 else
adamc@1016 786 polyC,
adamc@1016 787 namedC,
adamc@1016 788 namedE))
adamc@508 789 | DVal (x, n, t, e, s) =>
adamc@508 790 let
adamc@509 791 val t = con namedC [] t
adamc@509 792 val e = exp (namedC, namedE) [] e
adamc@508 793 in
adamc@508 794 ((DVal (x, n, t, e, s), loc),
adamc@1016 795 (polyC,
adamc@1016 796 namedC,
adamc@1016 797 if mayInline (polyC, n, t, e) then
adamc@1016 798 IM.insert (namedE, n, e)
adamc@1016 799 else
adamc@1016 800 namedE))
adamc@508 801 end
adamc@508 802 | DValRec vis =>
adamc@910 803 ((DValRec (map (fn (x, n, t, e, s) => (x, n, con namedC [] t,
adamc@910 804 exp (namedC, namedE) [] e, s)) vis), loc),
adamc@508 805 st)
adamc@508 806 | DExport _ => (d, st)
adamc@707 807 | DTable (s, n, c, s', pe, pc, ce, cc) => ((DTable (s, n, con namedC [] c, s',
adamc@707 808 exp (namedC, namedE) [] pe,
adamc@707 809 con namedC [] pc,
adamc@707 810 exp (namedC, namedE) [] ce,
adamc@707 811 con namedC [] cc), loc), st)
adamc@508 812 | DSequence _ => (d, st)
adamc@754 813 | DView (s, n, s', e, c) => ((DView (s, n, s', exp (namedC, namedE) [] e, con namedC [] c), loc), st)
adamc@508 814 | DDatabase _ => (d, st)
adamc@509 815 | DCookie (s, n, c, s') => ((DCookie (s, n, con namedC [] c, s'), loc), st)
adamc@720 816 | DStyle (s, n, s') => ((DStyle (s, n, s'), loc), st)
adamc@1075 817 | DTask (e1, e2) =>
adamc@1073 818 let
adamc@1075 819 val e1 = exp (namedC, namedE) [] e1
adamc@1075 820 val e2 = exp (namedC, namedE) [] e2
adamc@1073 821 in
adamc@1075 822 ((DTask (e1, e2), loc),
adamc@1073 823 (polyC,
adamc@1073 824 namedC,
adamc@1073 825 namedE))
adamc@1073 826 end
adamc@1199 827 | DPolicy e1 =>
adamc@1199 828 let
adamc@1199 829 val e1 = exp (namedC, namedE) [] e1
adamc@1199 830 in
adamc@1199 831 ((DPolicy e1, loc),
adamc@1199 832 (polyC,
adamc@1199 833 namedC,
adamc@1199 834 namedE))
adamc@1199 835 end
adam@1294 836 | DOnError _ => (d, st)
adamc@20 837
adamc@1016 838 val (file, _) = ListUtil.foldlMap doDecl (IS.empty, IM.empty, IM.empty) file
adamc@508 839 in
adamc@508 840 file
adamc@508 841 end
adamc@20 842
adamc@20 843 end