# HG changeset patch # User Adam Chlipala # Date 1227807284 18000 # Node ID 31aba58a5b5b67bd09e2e189715ceeb26ca37bc9 # Parent 3f20c22098aff71338e11b8adddc47135c6b5bb3 Ditch use of ElabEnv.env in Especialize, to realize big speed-up diff -r 3f20c22098af -r 31aba58a5b5b src/especialize.sml --- a/src/especialize.sml Thu Nov 27 12:04:54 2008 -0500 +++ b/src/especialize.sml Thu Nov 27 12:34:44 2008 -0500 @@ -104,7 +104,7 @@ decls : (string * int * con * exp * string) list } -fun kind x = x +fun id x = x fun default (_, x, st) = (x, st) fun specialize' file = @@ -140,10 +140,8 @@ fun bind (env, b) = case b of - U.Decl.RelC (x, k) => E.pushCRel env x k - | U.Decl.NamedC (x, n, k, co) => E.pushCNamed env x n k co - | U.Decl.RelE (x, t) => E.pushERel env x t - | U.Decl.NamedE (x, n, t, eo, s) => E.pushENamed env x n t eo s + U.Decl.RelE xt => xt :: env + | _ => env fun exp (env, e, st : state) = let @@ -249,7 +247,7 @@ ("e", CorePrint.p_exp env (e, loc))]*) val (body', typ') = IS.foldl (fn (n, (body', typ')) => let - val (x, xt) = E.lookupERel env n + val (x, xt) = List.nth (env, n) in ((EAbs (x, xt, typ', body'), loc), @@ -277,13 +275,13 @@ end end - and specExp env = U.Exp.foldMapB {kind = kind, con = default, exp = exp, bind = bind} env + and specExp env = U.Exp.foldMapB {kind = id, con = default, exp = exp, bind = bind} env - val specDecl = U.Decl.foldMapB {kind = kind, con = default, exp = exp, decl = default, bind = bind} + val specDecl = U.Decl.foldMapB {kind = id, con = default, exp = exp, decl = default, bind = bind} - fun doDecl (d, (env, st : state, changed)) = + fun doDecl (d, (st : state, changed)) = let - val env = E.declBinds env d + (*val befor = Time.now ()*) val funcs = #funcs st val funcs = @@ -303,7 +301,9 @@ decls = []} (*val () = Print.prefaces "decl" [("d", CorePrint.p_decl CoreEnv.empty d)]*) - val (d', st) = specDecl env st d + + val (d', st) = specDecl [] st d + (*val () = print "/decl\n"*) val funcs = #funcs st @@ -329,15 +329,16 @@ (DValRec vis', _) => [(DValRec (vis @ vis'), ErrorMsg.dummySpan)] | _ => [(DValRec vis, ErrorMsg.dummySpan), d']) in - (ds, (env, - {maxName = #maxName st, + (*Print.prefaces "doDecl" [("d", CorePrint.p_decl E.empty d), + ("t", Print.PD.string (Real.toString (Time.toReal + (Time.- (Time.now (), befor)))))];*) + (ds, ({maxName = #maxName st, funcs = funcs, decls = []}, changed)) end - val (ds, (_, _, changed)) = ListUtil.foldlMapConcat doDecl - (E.empty, - {maxName = U.File.maxName file + 1, + val (ds, (_, changed)) = ListUtil.foldlMapConcat doDecl + ({maxName = U.File.maxName file + 1, funcs = IM.empty, decls = []}, false)