Mercurial > urweb

annotate src/reduce.sml @ 1122:85d194409b17

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