Mercurial > urweb

annotate src/reduce.sml @ 930:51bc7681c47e

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