Mercurial > urweb

annotate src/reduce.sml @ 909:1d3f60e74ec7

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