# HG changeset patch # User Adam Chlipala # Date 1227807808 18000 # Node ID 3162bbf8e30fa9a3186ff0b22404493b11fe29f1 # Parent 31aba58a5b5b67bd09e2e189715ceeb26ca37bc9 Avoid Especializing polymorphic code diff -r 31aba58a5b5b -r 3162bbf8e30f src/core_util.sig --- a/src/core_util.sig Thu Nov 27 12:34:44 2008 -0500 +++ b/src/core_util.sig Thu Nov 27 12:43:28 2008 -0500 @@ -165,6 +165,11 @@ decl : 'context * Core.decl' * 'state -> Core.decl' * 'state, bind : 'context * binder -> 'context} -> 'context -> 'state -> Core.decl -> Core.decl * 'state + + val exists : {kind : Core.kind' -> bool, + con : Core.con' -> bool, + exp : Core.exp' -> bool, + decl : Core.decl' -> bool} -> Core.decl -> bool end structure File : sig diff -r 31aba58a5b5b -r 3162bbf8e30f src/core_util.sml --- a/src/core_util.sml Thu Nov 27 12:34:44 2008 -0500 +++ b/src/core_util.sml Thu Nov 27 12:43:28 2008 -0500 @@ -900,6 +900,30 @@ S.Continue v => v | S.Return _ => raise Fail "CoreUtil.Decl.foldMapB: Impossible" +fun exists {kind, con, exp, decl} d = + case mapfold {kind = fn k => fn () => + if kind k then + S.Return () + else + S.Continue (k, ()), + con = fn c => fn () => + if con c then + S.Return () + else + S.Continue (c, ()), + exp = fn e => fn () => + if exp e then + S.Return () + else + S.Continue (e, ()), + decl = fn d => fn () => + if decl d then + S.Return () + else + S.Continue (d, ())} d () of + S.Return _ => true + | S.Continue _ => false + end structure File = struct diff -r 31aba58a5b5b -r 3162bbf8e30f src/especialize.sml --- a/src/especialize.sml Thu Nov 27 12:34:44 2008 -0500 +++ b/src/especialize.sml Thu Nov 27 12:43:28 2008 -0500 @@ -59,6 +59,12 @@ | _ => bound} 0 IS.empty +val isPoly = U.Decl.exists {kind = fn _ => false, + con = fn _ => false, + exp = fn ECAbs _ => true + | _ => false, + decl = fn _ => false} + fun positionOf (v : int, ls) = let fun pof (pos, ls) = @@ -302,7 +308,11 @@ (*val () = Print.prefaces "decl" [("d", CorePrint.p_decl CoreEnv.empty d)]*) - val (d', st) = specDecl [] st d + val (d', st) = + if isPoly d then + (d, st) + else + specDecl [] st d (*val () = print "/decl\n"*)