Mercurial > urweb

comparison src/especialize.sml @ 1667:833402503855

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tweak Especialize heuristic to prevent non-termination
author Adam Chlipala <adam@chlipala.net>
date Mon, 09 Jan 2012 09:51:39 -0500
parents 0577be31a435
children 4cacced4a6da
comparison
equal deleted inserted replaced
1666:df8f18d50746 1667:833402503855
119 specialized : IS.set 119 specialized : IS.set
120 } 120 }
121 121
122 fun default (_, x, st) = (x, st) 122 fun default (_, x, st) = (x, st)
123 123
124 structure SS = BinarySetFn(struct
125 type ord_key = string
126 val compare = String.compare
127 end)
128
129 val mayNotSpec = ref SS.empty
130
131 val functionInside = U.Con.exists {kind = fn _ => false, 124 val functionInside = U.Con.exists {kind = fn _ => false,
132 con = fn TFun _ => true 125 con = fn TFun _ => true
133 | CFfi ("Basis", "transaction") => true 126 | CFfi ("Basis", "transaction") => true
134 | CFfi ("Basis", "eq") => true 127 | CFfi ("Basis", "eq") => true
135 | CFfi ("Basis", "num") => true 128 | CFfi ("Basis", "num") => true
349 342
350 val vts = map (fn n => #2 (List.nth (env, n))) (IS.listItems fvs) 343 val vts = map (fn n => #2 (List.nth (env, n))) (IS.listItems fvs)
351 val fxs' = map (squish (IS.listItems fvs)) fxs 344 val fxs' = map (squish (IS.listItems fvs)) fxs
352 345
353 val p_bool = Print.PD.string o Bool.toString 346 val p_bool = Print.PD.string o Bool.toString
347
348 fun bumpCount n =
349 if IS.member (#specialized st, f) then
350 n
351 else
352 5 + 2 *n
354 in 353 in
355 (*Print.prefaces "Func" [("name", Print.PD.string name), 354 (*Print.prefaces "Func" [("name", Print.PD.string name),
356 ("e", CorePrint.p_exp CoreEnv.empty e), 355 ("e", CorePrint.p_exp CoreEnv.empty e),
357 ("fxs'", Print.p_list (CorePrint.p_exp CoreEnv.empty) fxs')];*) 356 ("fxs'", Print.p_list (CorePrint.p_exp CoreEnv.empty) fxs')];*)
358 if not fin 357 if not fin
359 orelse List.all (fn (ERel _, _) => true 358 orelse List.all (fn (ERel _, _) => true
360 | _ => false) fxs' 359 | _ => false) fxs'
361 orelse List.exists (not o valueish) fxs' 360 orelse List.exists (not o valueish) fxs'
362 orelse (IS.numItems fvs >= length fxs 361 orelse IS.numItems fvs >= bumpCount (length fxs) then
363 andalso IS.exists (fn n => functionInside (#2 (List.nth (env, n)))) fvs) then
364 ((*Print.prefaces "No" [("name", Print.PD.string name), 362 ((*Print.prefaces "No" [("name", Print.PD.string name),
365 ("f", Print.PD.string (Int.toString f)), 363 ("f", Print.PD.string (Int.toString f)),
366 ("fxs'", 364 ("fxs'",
367 Print.p_list (CorePrint.p_exp CoreEnv.empty) fxs'), 365 Print.p_list (CorePrint.p_exp CoreEnv.empty) fxs'),
368 ("b1", p_bool (not fin)), 366 ("b1", p_bool (not fin)),
371 ("b3", p_bool (List.exists (not o valueish) fxs')), 369 ("b3", p_bool (List.exists (not o valueish) fxs')),
372 ("b4", p_bool (IS.numItems fvs >= length fxs 370 ("b4", p_bool (IS.numItems fvs >= length fxs
373 andalso IS.exists (fn n => functionInside (#2 (List.nth (env, n)))) fvs))];*) 371 andalso IS.exists (fn n => functionInside (#2 (List.nth (env, n)))) fvs))];*)
374 default ()) 372 default ())
375 else 373 else
376 case (KM.find (args, (vts, fxs')), 374 case KM.find (args, (vts, fxs')) of
377 SS.member (!mayNotSpec, name) (*orelse IS.member (#specialized st, f)*)) of 375 SOME f' =>
378 (SOME f', _) =>
379 let 376 let
380 val e = (ENamed f', loc) 377 val e = (ENamed f', loc)
381 val e = IS.foldr (fn (arg, e) => (EApp (e, (ERel arg, loc)), loc)) 378 val e = IS.foldr (fn (arg, e) => (EApp (e, (ERel arg, loc)), loc))
382 e fvs 379 e fvs
383 val e = foldl (fn (arg, e) => (EApp (e, arg), loc)) 380 val e = foldl (fn (arg, e) => (EApp (e, arg), loc))
385 in 382 in
386 (*Print.prefaces "Brand new (reuse)" 383 (*Print.prefaces "Brand new (reuse)"
387 [("e'", CorePrint.p_exp CoreEnv.empty e)];*) 384 [("e'", CorePrint.p_exp CoreEnv.empty e)];*)
388 (e, st) 385 (e, st)
389 end 386 end
390 | (_, true) => ((*Print.prefaces ("No!(" ^ name ^ ")") 387 | NONE =>
391 [("fxs'",
392 Print.p_list (CorePrint.p_exp CoreEnv.empty) fxs')];*)
393 default ())
394 | (NONE, false) =>
395 let 388 let
396 (*val () = Print.prefaces "New one" 389 (*val () = Print.prefaces "New one"
397 [("f", Print.PD.string (Int.toString f)), 390 [("name", Print.PD.string name),
398 ("mns", Print.p_list Print.PD.string 391 ("f", Print.PD.string (Int.toString f)),
399 (SS.listItems (!mayNotSpec)))]*) 392 ("|fvs|", Print.PD.string (Int.toString (IS.numItems fvs))),
393 ("|fxs|", Print.PD.string (Int.toString (length fxs))),
394 ("spec", Print.PD.string (Bool.toString (IS.member (#specialized st, f))))]*)
400 395
401 (*val () = Print.prefaces ("Yes(" ^ name ^ ")") 396 (*val () = Print.prefaces ("Yes(" ^ name ^ ")")
402 [("fxs'", 397 [("fxs'",
403 Print.p_list (CorePrint.p_exp CoreEnv.empty) fxs')]*) 398 Print.p_list (CorePrint.p_exp CoreEnv.empty) fxs')]*)
404 399
448 ((EAbs (x, xt, typ', body'), 443 ((EAbs (x, xt, typ', body'),
449 loc), 444 loc),
450 (TFun (xt, typ'), loc)) 445 (TFun (xt, typ'), loc))
451 end) 446 end)
452 (body', typ') fvs 447 (body', typ') fvs
453 val mns = !mayNotSpec
454 (*val () = mayNotSpec := SS.add (mns, name)*)
455 (*val () = print ("NEW: " ^ name ^ "__" ^ Int.toString f' ^ "\n");*) 448 (*val () = print ("NEW: " ^ name ^ "__" ^ Int.toString f' ^ "\n");*)
456 val body' = ReduceLocal.reduceExp body' 449 val body' = ReduceLocal.reduceExp body'
457 (*val () = Print.preface ("PRE", CorePrint.p_exp CoreEnv.empty body')*) 450 (*val () = Print.preface ("PRE", CorePrint.p_exp CoreEnv.empty body')*)
458 val (body', st) = exp (env, body', st) 451 val (body', st) = exp (env, body', st)
459 val () = mayNotSpec := mns
460 452
461 val e' = (ENamed f', loc) 453 val e' = (ENamed f', loc)
462 val e' = IS.foldr (fn (arg, e) => (EApp (e, (ERel arg, loc)), loc)) 454 val e' = IS.foldr (fn (arg, e) => (EApp (e, (ERel arg, loc)), loc))
463 e' fvs 455 e' fvs
464 val e' = foldl (fn (arg, e) => (EApp (e, arg), loc)) 456 val e' = foldl (fn (arg, e) => (EApp (e, arg), loc))
500 funcs = funcs, 492 funcs = funcs,
501 decls = [], 493 decls = [],
502 specialized = #specialized st} 494 specialized = #specialized st}
503 495
504 (*val () = Print.prefaces "decl" [("d", CorePrint.p_decl CoreEnv.empty d)]*) 496 (*val () = Print.prefaces "decl" [("d", CorePrint.p_decl CoreEnv.empty d)]*)
505
506 val () = mayNotSpec := SS.empty
507 497
508 val (d', st) = 498 val (d', st) =
509 if isPoly d then 499 if isPoly d then
510 (d, st) 500 (d, st)
511 else 501 else
534 CorePrint.p_con CoreEnv.empty (#3 vi)]) 524 CorePrint.p_con CoreEnv.empty (#3 vi)])
535 vis)*) 525 vis)*)
536 526
537 val (vis, st) = ListUtil.foldlMap (fn ((x, n, t, e, s), st) => 527 val (vis, st) = ListUtil.foldlMap (fn ((x, n, t, e, s), st) =>
538 let 528 let
539 val () = mayNotSpec := SS.empty
540 val (e, st) = exp ([], e, st) 529 val (e, st) = exp ([], e, st)
541 in 530 in
542 ((x, n, t, e, s), st) 531 ((x, n, t, e, s), st)
543 end) st vis 532 end) st vis
544 in 533 in
564 in 553 in
565 ((DTask (e1, e2), #2 d), st) 554 ((DTask (e1, e2), #2 d), st)
566 end 555 end
567 | _ => (d, st) 556 | _ => (d, st)
568 557
569 val () = mayNotSpec := SS.empty
570
571 (*val () = print "/decl\n"*) 558 (*val () = print "/decl\n"*)
572 559
573 val funcs = #funcs st 560 val funcs = #funcs st
574 val funcs = 561 val funcs =
575 case #1 d of 562 case #1 d of