Mercurial > urweb

annotate src/reduce.sml @ 908:ed06e25c70ef

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Convert to requiring explicit 'rpc' marker
author Adam Chlipala <adamc@hcoop.net>
date Sat, 22 Aug 2009 12:55:18 -0400
parents 669ac5e9a69e
children 1d3f60e74ec7
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@508 44 datatype env_item =
adamc@626 45 UnknownK
adamc@626 46 | KnownK of kind
adamc@626 47
adamc@626 48 | UnknownC
adamc@508 49 | KnownC of con
adamc@21 50
adamc@508 51 | UnknownE
adamc@508 52 | KnownE of exp
adamc@20 53
adamc@626 54 | Lift of int * int * int
adamc@20 55
adamc@508 56 type env = env_item list
adamc@20 57
adamc@510 58 fun ei2s ei =
adamc@510 59 case ei of
adamc@626 60 UnknownK => "UK"
adamc@626 61 | KnownK _ => "KK"
adamc@626 62 | UnknownC => "UC"
adamc@510 63 | KnownC _ => "KC"
adamc@510 64 | UnknownE => "UE"
adamc@510 65 | KnownE _ => "KE"
adamc@626 66 | Lift (_, n1, n2) => "(" ^ Int.toString n1 ^ ", " ^ Int.toString n2 ^ ")"
adamc@510 67
adamc@510 68 fun e2s env = String.concatWith " " (map ei2s env)
adamc@510 69
adamc@510 70 val deKnown = List.filter (fn KnownC _ => false
adamc@510 71 | KnownE _ => false
adamc@626 72 | KnownK _ => false
adamc@510 73 | _ => true)
adamc@510 74
adamc@626 75 fun kindConAndExp (namedC, namedE) =
adamc@508 76 let
adamc@626 77 fun kind env (all as (k, loc)) =
adamc@626 78 case k of
adamc@626 79 KType => all
adamc@626 80 | KArrow (k1, k2) => (KArrow (kind env k1, kind env k2), loc)
adamc@626 81 | KName => all
adamc@626 82 | KRecord k => (KRecord (kind env k), loc)
adamc@626 83 | KUnit => all
adamc@626 84 | KTuple ks => (KTuple (map (kind env) ks), loc)
adamc@626 85
adamc@626 86 | KRel n =>
adamc@626 87 let
adamc@626 88 fun find (n', env, nudge, lift) =
adamc@626 89 case env of
adamc@626 90 [] => raise Fail "Reduce.kind: KRel"
adamc@626 91 | UnknownC :: rest => find (n', rest, nudge, lift)
adamc@626 92 | KnownC _ :: rest => find (n', rest, nudge, lift)
adamc@626 93 | UnknownE :: rest => find (n', rest, nudge, lift)
adamc@626 94 | KnownE _ :: rest => find (n', rest, nudge, lift)
adamc@626 95 | Lift (lift', _, _) :: rest => find (n', rest, nudge + lift', lift + lift')
adamc@626 96 | UnknownK :: rest =>
adamc@626 97 if n' = 0 then
adamc@626 98 (KRel (n + nudge), loc)
adamc@626 99 else
adamc@626 100 find (n' - 1, rest, nudge, lift + 1)
adamc@626 101 | KnownK k :: rest =>
adamc@626 102 if n' = 0 then
adamc@626 103 kind (Lift (lift, 0, 0) :: rest) k
adamc@626 104 else
adamc@626 105 find (n' - 1, rest, nudge - 1, lift)
adamc@626 106 in
adamc@626 107 find (n, env, 0, 0)
adamc@626 108 end
adamc@626 109 | KFun (x, k) => (KFun (x, kind (UnknownK :: env) k), loc)
adamc@626 110
adamc@508 111 fun con env (all as (c, loc)) =
adamc@510 112 ((*Print.prefaces "con" [("c", CorePrint.p_con CoreEnv.empty all)];*)
adamc@508 113 case c of
adamc@508 114 TFun (c1, c2) => (TFun (con env c1, con env c2), loc)
adamc@626 115 | TCFun (x, k, c2) => (TCFun (x, kind env k, con (UnknownC :: env) c2), loc)
adamc@626 116 | TKFun (x, c2) => (TKFun (x, con (UnknownK :: env) c2), loc)
adamc@508 117 | TRecord c => (TRecord (con env c), loc)
adamc@215 118
adamc@508 119 | CRel n =>
adamc@508 120 let
adamc@626 121 fun find (n', env, nudge, liftK, liftC) =
adamc@510 122 case env of
adamc@510 123 [] => raise Fail "Reduce.con: CRel"
adamc@626 124 | UnknownK :: rest => find (n', rest, nudge, liftK + 1, liftC)
adamc@626 125 | KnownK _ :: rest => find (n', rest, nudge, liftK, liftC)
adamc@626 126 | UnknownE :: rest => find (n', rest, nudge, liftK, liftC)
adamc@626 127 | KnownE _ :: rest => find (n', rest, nudge, liftK, liftC)
adamc@626 128 | Lift (liftK', liftC', _) :: rest => find (n', rest, nudge + liftC',
adamc@626 129 liftK + liftK', liftC + liftC')
adamc@510 130 | UnknownC :: rest =>
adamc@510 131 if n' = 0 then
adamc@510 132 (CRel (n + nudge), loc)
adamc@510 133 else
adamc@626 134 find (n' - 1, rest, nudge, liftK, liftC + 1)
adamc@510 135 | KnownC c :: rest =>
adamc@510 136 if n' = 0 then
adamc@626 137 con (Lift (liftK, liftC, 0) :: rest) c
adamc@510 138 else
adamc@626 139 find (n' - 1, rest, nudge - 1, liftK, liftC)
adamc@508 140 in
adamc@510 141 (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*)
adamc@626 142 find (n, env, 0, 0, 0)
adamc@508 143 end
adamc@508 144 | CNamed n =>
adamc@508 145 (case IM.find (namedC, n) of
adamc@508 146 NONE => all
adamc@508 147 | SOME c => c)
adamc@508 148 | CFfi _ => all
adamc@508 149 | CApp (c1, c2) =>
adamc@508 150 let
adamc@508 151 val c1 = con env c1
adamc@508 152 val c2 = con env c2
adamc@508 153 in
adamc@508 154 case #1 c1 of
adamc@508 155 CAbs (_, _, b) =>
adamc@510 156 con (KnownC c2 :: deKnown env) b
adamc@215 157
adamc@621 158 | CApp ((CMap (dom, ran), _), f) =>
adamc@508 159 (case #1 c2 of
adamc@626 160 CRecord (_, []) => (CRecord (kind env ran, []), loc)
adamc@621 161 | CRecord (_, (x, c) :: rest) =>
adamc@510 162 con (deKnown env)
adamc@621 163 (CConcat ((CRecord (ran, [(x, (CApp (f, c), loc))]), loc),
adamc@626 164 (CApp (c1, (CRecord (kind env dom, rest), loc)), loc)), loc)
adamc@508 165 | _ => (CApp (c1, c2), loc))
adamc@20 166
adamc@508 167 | _ => (CApp (c1, c2), loc)
adamc@508 168 end
adamc@626 169 | CAbs (x, k, b) => (CAbs (x, kind env k, con (UnknownC :: env) b), loc)
adamc@626 170
adamc@626 171 | CKApp (c1, k) =>
adamc@626 172 let
adamc@626 173 val c1 = con env c1
adamc@626 174 in
adamc@626 175 case #1 c1 of
adamc@626 176 CKAbs (_, b) =>
adamc@626 177 con (KnownK k :: deKnown env) b
adamc@626 178
adamc@626 179 | _ => (CKApp (c1, kind env k), loc)
adamc@626 180 end
adamc@626 181 | CKAbs (x, b) => (CKAbs (x, con (UnknownK :: env) b), loc)
adamc@20 182
adamc@508 183 | CName _ => all
adamc@21 184
adamc@626 185 | CRecord (k, xcs) => (CRecord (kind env k, map (fn (x, c) => (con env x, con env c)) xcs), loc)
adamc@508 186 | CConcat (c1, c2) =>
adamc@508 187 let
adamc@508 188 val c1 = con env c1
adamc@508 189 val c2 = con env c2
adamc@508 190 in
adamc@508 191 case (#1 c1, #1 c2) of
adamc@508 192 (CRecord (k, xcs1), CRecord (_, xcs2)) =>
adamc@626 193 (CRecord (kind env k, xcs1 @ xcs2), loc)
adamc@508 194 | _ => (CConcat (c1, c2), loc)
adamc@508 195 end
adamc@626 196 | CMap (dom, ran) => (CMap (kind env dom, kind env ran), loc)
adamc@74 197
adamc@508 198 | CUnit => all
adamc@21 199
adamc@508 200 | CTuple cs => (CTuple (map (con env) cs), loc)
adamc@508 201 | CProj (c, n) =>
adamc@508 202 let
adamc@508 203 val c = con env c
adamc@508 204 in
adamc@508 205 case #1 c of
adamc@508 206 CTuple cs => List.nth (cs, n - 1)
adamc@508 207 | _ => (CProj (c, n), loc)
adamc@510 208 end)
adamc@22 209
adamc@509 210 fun patCon pc =
adamc@509 211 case pc of
adamc@509 212 PConVar _ => pc
adamc@509 213 | PConFfi {mod = m, datatyp, params, con = c, arg, kind} =>
adamc@509 214 PConFfi {mod = m, datatyp = datatyp, params = params, con = c,
adamc@509 215 arg = Option.map (con (map (fn _ => UnknownC) params)) arg,
adamc@509 216 kind = kind}
adamc@509 217
adamc@509 218
adamc@509 219 val k = (KType, ErrorMsg.dummySpan)
adamc@509 220 fun doPart e (this as (x, t), rest) =
adamc@509 221 ((x, (EField (e, x, {field = t, rest = (CRecord (k, rest), #2 t)}), #2 t), t),
adamc@509 222 this :: rest)
adamc@509 223
adamc@509 224 fun exp env (all as (e, loc)) =
adamc@510 225 ((*Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all),
adamc@510 226 ("env", Print.PD.string (e2s env))];*)
adamc@509 227 case e of
adamc@509 228 EPrim _ => all
adamc@509 229 | ERel n =>
adamc@509 230 let
adamc@626 231 fun find (n', env, nudge, liftK, liftC, liftE) =
adamc@510 232 case env of
adamc@510 233 [] => raise Fail "Reduce.exp: ERel"
adamc@626 234 | UnknownK :: rest => find (n', rest, nudge, liftK + 1, liftC, liftE)
adamc@626 235 | KnownK _ :: rest => find (n', rest, nudge, liftK, liftC, liftE)
adamc@626 236 | UnknownC :: rest => find (n', rest, nudge, liftK, liftC + 1, liftE)
adamc@626 237 | KnownC _ :: rest => find (n', rest, nudge, liftK, liftC, liftE)
adamc@626 238 | Lift (liftK', liftC', liftE') :: rest =>
adamc@626 239 find (n', rest, nudge + liftE',
adamc@626 240 liftK + liftK', liftC + liftC', liftE + liftE')
adamc@510 241 | UnknownE :: rest =>
adamc@510 242 if n' = 0 then
adamc@510 243 (ERel (n + nudge), loc)
adamc@510 244 else
adamc@626 245 find (n' - 1, rest, nudge, liftK, liftC, liftE + 1)
adamc@510 246 | KnownE e :: rest =>
adamc@510 247 if n' = 0 then
adamc@510 248 ((*print "SUBSTITUTING\n";*)
adamc@626 249 exp (Lift (liftK, liftC, liftE) :: rest) e)
adamc@510 250 else
adamc@626 251 find (n' - 1, rest, nudge - 1, liftK, liftC, liftE)
adamc@509 252 in
adamc@510 253 (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*)
adamc@626 254 find (n, env, 0, 0, 0, 0)
adamc@509 255 end
adamc@509 256 | ENamed n =>
adamc@509 257 (case IM.find (namedE, n) of
adamc@509 258 NONE => all
adamc@509 259 | SOME e => e)
adamc@509 260 | ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc,
adamc@509 261 map (con env) cs, Option.map (exp env) eo), loc)
adamc@509 262 | EFfi _ => all
adamc@509 263 | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc)
adamc@509 264
adamc@908 265 | EApp (
adamc@908 266 (EApp
adamc@908 267 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _),
adamc@908 268 _), _),
adamc@908 269 (EApp (
adamc@908 270 (EApp (
adamc@908 271 (ECApp (
adamc@908 272 (ECApp ((EFfi ("Basis", "return"), _), _), _),
adamc@908 273 _), _),
adamc@908 274 _), _), v), _)), _), trans2) => exp env (EApp (trans2, v), loc)
adamc@908 275
adamc@908 276 (*| EApp (
adamc@908 277 (EApp
adamc@908 278 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _),
adamc@908 279 (EFfi ("Basis", "transaction_monad"), _)), _),
adamc@908 280 (ECase (ed, pes, {disc, ...}), _)), _),
adamc@908 281 trans2) =>
adamc@908 282 let
adamc@908 283 val e' = (EFfi ("Basis", "bind"), loc)
adamc@908 284 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
adamc@908 285 val e' = (ECApp (e', t1), loc)
adamc@908 286 val e' = (ECApp (e', t2), loc)
adamc@908 287 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
adamc@908 288
adamc@908 289 val pes = map (fn (p, e) =>
adamc@908 290 let
adamc@908 291 val e' = (EApp (e', e), loc)
adamc@908 292 val e' = (EApp (e',
adamc@908 293 multiLiftExpInExp (E.patBindsN p)
adamc@908 294 trans2), loc)
adamc@908 295 val e' = exp env e'
adamc@908 296 in
adamc@908 297 (p, e')
adamc@908 298 end) pes
adamc@908 299 in
adamc@908 300 (ECase (exp env ed,
adamc@908 301 pes,
adamc@908 302 {disc = con env disc,
adamc@908 303 result = (CApp ((CFfi ("Basis", "transaction"), loc), con env t2), loc)}),
adamc@908 304 loc)
adamc@908 305 end*)
adamc@908 306
adamc@908 307 | EApp (
adamc@908 308 (EApp
adamc@908 309 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _),
adamc@908 310 (EFfi ("Basis", "transaction_monad"), _)), _),
adamc@908 311 (EServerCall (n, es, ke, dom, ran), _)), _),
adamc@908 312 trans2) =>
adamc@908 313 let
adamc@908 314 val e' = (EFfi ("Basis", "bind"), loc)
adamc@908 315 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
adamc@908 316 val e' = (ECApp (e', dom), loc)
adamc@908 317 val e' = (ECApp (e', t2), loc)
adamc@908 318 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
adamc@908 319 val e' = (EApp (e', (EApp (E.liftExpInExp 0 ke, (ERel 0, loc)), loc)), loc)
adamc@908 320 val e' = (EApp (e', E.liftExpInExp 0 trans2), loc)
adamc@908 321 val e' = (EAbs ("x", dom, t2, e'), loc)
adamc@908 322 val e' = (EServerCall (n, es, e', dom, t2), loc)
adamc@908 323 in
adamc@908 324 exp env e'
adamc@908 325 end
adamc@908 326
adamc@908 327 | EApp (
adamc@908 328 (EApp
adamc@908 329 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), _), _), t3), _),
adamc@908 330 (EFfi ("Basis", "transaction_monad"), _)), _),
adamc@908 331 (EApp ((EApp
adamc@908 332 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), _), _), _), t1), _), t2), _),
adamc@908 333 (EFfi ("Basis", "transaction_monad"), _)), _),
adamc@908 334 trans1), _), trans2), _)), _),
adamc@908 335 trans3) =>
adamc@908 336 let
adamc@908 337 val e'' = (EFfi ("Basis", "bind"), loc)
adamc@908 338 val e'' = (ECApp (e'', (CFfi ("Basis", "transaction"), loc)), loc)
adamc@908 339 val e'' = (ECApp (e'', t2), loc)
adamc@908 340 val e'' = (ECApp (e'', t3), loc)
adamc@908 341 val e'' = (EApp (e'', (EFfi ("Basis", "transaction_monad"), loc)), loc)
adamc@908 342 val e'' = (EApp (e'', (EApp (E.liftExpInExp 0 trans2, (ERel 0, loc)), loc)), loc)
adamc@908 343 val e'' = (EApp (e'', E.liftExpInExp 0 trans3), loc)
adamc@908 344 val e'' = (EAbs ("x", t1, (CApp ((CFfi ("Basis", "transaction"), loc), t3), loc), e''), loc)
adamc@908 345
adamc@908 346 val e' = (EFfi ("Basis", "bind"), loc)
adamc@908 347 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
adamc@908 348 val e' = (ECApp (e', t1), loc)
adamc@908 349 val e' = (ECApp (e', t3), loc)
adamc@908 350 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
adamc@908 351 val e' = (EApp (e', trans1), loc)
adamc@908 352 val e' = (EApp (e', e''), loc)
adamc@908 353 in
adamc@908 354 exp env e'
adamc@908 355 end
adamc@908 356
adamc@509 357 | EApp (e1, e2) =>
adamc@509 358 let
adamc@509 359 val e1 = exp env e1
adamc@509 360 val e2 = exp env e2
adamc@509 361 in
adamc@509 362 case #1 e1 of
adamc@510 363 EAbs (_, _, _, b) => exp (KnownE e2 :: deKnown env) b
adamc@509 364 | _ => (EApp (e1, e2), loc)
adamc@509 365 end
adamc@509 366
adamc@509 367 | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (UnknownE :: env) e), loc)
adamc@509 368
adamc@509 369 | ECApp (e, c) =>
adamc@509 370 let
adamc@509 371 val e = exp env e
adamc@509 372 val c = con env c
adamc@509 373 in
adamc@509 374 case #1 e of
adamc@510 375 ECAbs (_, _, b) => exp (KnownC c :: deKnown env) b
adamc@509 376 | _ => (ECApp (e, c), loc)
adamc@509 377 end
adamc@509 378
adamc@626 379 | ECAbs (x, k, e) => (ECAbs (x, kind env k, exp (UnknownC :: env) e), loc)
adamc@626 380
adamc@626 381 | EKApp (e, k) =>
adamc@626 382 let
adamc@626 383 val e = exp env e
adamc@626 384 in
adamc@626 385 case #1 e of
adamc@626 386 EKAbs (_, b) => exp (KnownK k :: deKnown env) b
adamc@626 387 | _ => (EKApp (e, kind env k), loc)
adamc@626 388 end
adamc@626 389
adamc@626 390 | EKAbs (x, e) => (EKAbs (x, exp (UnknownK :: env) e), loc)
adamc@509 391
adamc@509 392 | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc)
adamc@509 393 | EField (e, c, {field, rest}) =>
adamc@509 394 let
adamc@509 395 val e = exp env e
adamc@509 396 val c = con env c
adamc@509 397
adamc@509 398 fun default () = (EField (e, c, {field = con env field, rest = con env rest}), loc)
adamc@509 399 in
adamc@509 400 case (#1 e, #1 c) of
adamc@509 401 (ERecord xcs, CName x) =>
adamc@509 402 (case List.find (fn ((CName x', _), _, _) => x' = x | _ => false) xcs of
adamc@509 403 NONE => default ()
adamc@509 404 | SOME (_, e, _) => e)
adamc@509 405 | _ => default ()
adamc@509 406 end
adamc@509 407
adamc@509 408 | EConcat (e1, c1, e2, c2) =>
adamc@509 409 let
adamc@509 410 val e1 = exp env e1
adamc@509 411 val e2 = exp env e2
adamc@509 412 in
adamc@509 413 case (#1 e1, #1 e2) of
adamc@509 414 (ERecord xes1, ERecord xes2) => (ERecord (xes1 @ xes2), loc)
adamc@509 415 | _ =>
adamc@509 416 let
adamc@509 417 val c1 = con env c1
adamc@509 418 val c2 = con env c2
adamc@509 419 in
adamc@509 420 case (#1 c1, #1 c2) of
adamc@509 421 (CRecord (k, xcs1), CRecord (_, xcs2)) =>
adamc@509 422 let
adamc@509 423 val (xes1, rest) = ListUtil.foldlMap (doPart e1) [] xcs1
adamc@509 424 val (xes2, _) = ListUtil.foldlMap (doPart e2) rest xcs2
adamc@509 425 in
adamc@510 426 exp (deKnown env) (ERecord (xes1 @ xes2), loc)
adamc@509 427 end
adamc@509 428 | _ => (EConcat (e1, c1, e2, c2), loc)
adamc@509 429 end
adamc@509 430 end
adamc@509 431
adamc@509 432 | ECut (e, c, {field, rest}) =>
adamc@509 433 let
adamc@509 434 val e = exp env e
adamc@509 435 val c = con env c
adamc@509 436
adamc@509 437 fun default () =
adamc@509 438 let
adamc@509 439 val rest = con env rest
adamc@509 440 in
adamc@509 441 case #1 rest of
adamc@509 442 CRecord (k, xcs) =>
adamc@509 443 let
adamc@509 444 val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs
adamc@509 445 in
adamc@510 446 exp (deKnown env) (ERecord xes, loc)
adamc@509 447 end
adamc@509 448 | _ => (ECut (e, c, {field = con env field, rest = rest}), loc)
adamc@509 449 end
adamc@509 450 in
adamc@509 451 case (#1 e, #1 c) of
adamc@509 452 (ERecord xes, CName x) =>
adamc@509 453 if List.all (fn ((CName _, _), _, _) => true | _ => false) xes then
adamc@509 454 (ERecord (List.filter (fn ((CName x', _), _, _) => x' <> x
adamc@509 455 | _ => raise Fail "Reduce: ECut") xes), loc)
adamc@509 456 else
adamc@509 457 default ()
adamc@509 458 | _ => default ()
adamc@509 459 end
adamc@509 460
adamc@509 461 | ECutMulti (e, c, {rest}) =>
adamc@509 462 let
adamc@509 463 val e = exp env e
adamc@509 464 val c = con env c
adamc@509 465
adamc@509 466 fun default () =
adamc@509 467 let
adamc@509 468 val rest = con env rest
adamc@509 469 in
adamc@509 470 case #1 rest of
adamc@509 471 CRecord (k, xcs) =>
adamc@509 472 let
adamc@509 473 val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs
adamc@509 474 in
adamc@510 475 exp (deKnown env) (ERecord xes, loc)
adamc@509 476 end
adamc@509 477 | _ => (ECutMulti (e, c, {rest = rest}), loc)
adamc@509 478 end
adamc@509 479 in
adamc@509 480 case (#1 e, #1 c) of
adamc@509 481 (ERecord xes, CRecord (_, xcs)) =>
adamc@509 482 if List.all (fn ((CName _, _), _, _) => true | _ => false) xes
adamc@509 483 andalso List.all (fn ((CName _, _), _) => true | _ => false) xcs then
adamc@509 484 (ERecord (List.filter (fn ((CName x', _), _, _) =>
adamc@509 485 List.all (fn ((CName x, _), _) => x' <> x
adamc@509 486 | _ => raise Fail "Reduce: ECutMulti [1]") xcs
adamc@509 487 | _ => raise Fail "Reduce: ECutMulti [2]") xes), loc)
adamc@509 488 else
adamc@509 489 default ()
adamc@509 490 | _ => default ()
adamc@509 491 end
adamc@509 492
adamc@823 493 | ECase (_, [((PRecord [], _), e)], _) => exp env e
adamc@823 494 | ECase (_, [((PWild, _), e)], _) => exp env e
adamc@823 495
adamc@509 496 | ECase (e, pes, {disc, result}) =>
adamc@509 497 let
adamc@509 498 fun patBinds (p, _) =
adamc@509 499 case p of
adamc@509 500 PWild => 0
adamc@509 501 | PVar _ => 1
adamc@509 502 | PPrim _ => 0
adamc@509 503 | PCon (_, _, _, NONE) => 0
adamc@509 504 | PCon (_, _, _, SOME p) => patBinds p
adamc@509 505 | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts
adamc@509 506
adamc@509 507 fun pat (all as (p, loc)) =
adamc@509 508 case p of
adamc@509 509 PWild => all
adamc@509 510 | PVar (x, t) => (PVar (x, con env t), loc)
adamc@509 511 | PPrim _ => all
adamc@509 512 | PCon (dk, pc, cs, po) =>
adamc@509 513 (PCon (dk, patCon pc, map (con env) cs, Option.map pat po), loc)
adamc@509 514 | PRecord xpts => (PRecord (map (fn (x, p, t) => (x, pat p, con env t)) xpts), loc)
adamc@509 515 in
adamc@509 516 (ECase (exp env e,
adamc@509 517 map (fn (p, e) => (pat p,
adamc@509 518 exp (List.tabulate (patBinds p, fn _ => UnknownE) @ env) e))
adamc@509 519 pes, {disc = con env disc, result = con env result}), loc)
adamc@509 520 end
adamc@509 521
adamc@509 522 | EWrite e => (EWrite (exp env e), loc)
adamc@509 523 | EClosure (n, es) => (EClosure (n, map (exp env) es), loc)
adamc@509 524
adamc@607 525 | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (UnknownE :: env) e2), loc)
adamc@607 526
adamc@908 527 | EServerCall (n, es, e, t1, t2) => (EServerCall (n, map (exp env) es, exp env e,
adamc@908 528 con env t1, con env t2), loc))
adamc@417 529 in
adamc@626 530 {kind = kind, con = con, exp = exp}
adamc@417 531 end
adamc@21 532
adamc@626 533 fun kind namedC env k = #kind (kindConAndExp (namedC, IM.empty)) env k
adamc@626 534 fun con namedC env c = #con (kindConAndExp (namedC, IM.empty)) env c
adamc@626 535 fun exp (namedC, namedE) env e = #exp (kindConAndExp (namedC, namedE)) env e
adamc@20 536
adamc@508 537 fun reduce file =
adamc@508 538 let
adamc@508 539 fun doDecl (d as (_, loc), st as (namedC, namedE)) =
adamc@508 540 case #1 d of
adamc@508 541 DCon (x, n, k, c) =>
adamc@508 542 let
adamc@626 543 val k = kind namedC [] k
adamc@509 544 val c = con namedC [] c
adamc@508 545 in
adamc@508 546 ((DCon (x, n, k, c), loc),
adamc@508 547 (IM.insert (namedC, n, c), namedE))
adamc@508 548 end
adamc@807 549 | DDatatype dts =>
adamc@807 550 ((DDatatype (map (fn (x, n, ps, cs) =>
adamc@807 551 let
adamc@807 552 val env = map (fn _ => UnknownC) ps
adamc@807 553 in
adamc@807 554 (x, n, ps, map (fn (x, n, co) => (x, n, Option.map (con namedC env) co)) cs)
adamc@807 555 end) dts), loc),
adamc@807 556 st)
adamc@508 557 | DVal (x, n, t, e, s) =>
adamc@508 558 let
adamc@509 559 val t = con namedC [] t
adamc@509 560 val e = exp (namedC, namedE) [] e
adamc@508 561 in
adamc@508 562 ((DVal (x, n, t, e, s), loc),
adamc@508 563 (namedC, IM.insert (namedE, n, e)))
adamc@508 564 end
adamc@508 565 | DValRec vis =>
adamc@509 566 ((DValRec (map (fn (x, n, t, e, s) => (x, n, con namedC [] t, exp (namedC, namedE) [] e, s)) vis), loc),
adamc@508 567 st)
adamc@508 568 | DExport _ => (d, st)
adamc@707 569 | DTable (s, n, c, s', pe, pc, ce, cc) => ((DTable (s, n, con namedC [] c, s',
adamc@707 570 exp (namedC, namedE) [] pe,
adamc@707 571 con namedC [] pc,
adamc@707 572 exp (namedC, namedE) [] ce,
adamc@707 573 con namedC [] cc), loc), st)
adamc@508 574 | DSequence _ => (d, st)
adamc@754 575 | DView (s, n, s', e, c) => ((DView (s, n, s', exp (namedC, namedE) [] e, con namedC [] c), loc), st)
adamc@508 576 | DDatabase _ => (d, st)
adamc@509 577 | DCookie (s, n, c, s') => ((DCookie (s, n, con namedC [] c, s'), loc), st)
adamc@720 578 | DStyle (s, n, s') => ((DStyle (s, n, s'), loc), st)
adamc@20 579
adamc@508 580 val (file, _) = ListUtil.foldlMap doDecl (IM.empty, IM.empty) file
adamc@508 581 in
adamc@508 582 file
adamc@508 583 end
adamc@20 584
adamc@20 585 end