# HG changeset patch # User Adam Chlipala # Date 1225400334 14400 # Node ID bd9ee9aeca2fcaffcc021a76563f97a0f6ffe1f0 # Parent 9095a95a1bf93c7ab9774105938480202c3dd3ca Especialize diff -r 9095a95a1bf9 -r bd9ee9aeca2f lib/basis.urs --- a/lib/basis.urs Thu Oct 30 15:39:06 2008 -0400 +++ b/lib/basis.urs Thu Oct 30 16:58:54 2008 -0400 @@ -352,6 +352,9 @@ val font : bodyTag [Size = int, Face = string] val h1 : bodyTag [] +val h2 : bodyTag [] +val h3 : bodyTag [] +val h4 : bodyTag [] val li : bodyTag [] val hr : bodyTag [] diff -r 9095a95a1bf9 -r bd9ee9aeca2f src/compiler.sig --- a/src/compiler.sig Thu Oct 30 15:39:06 2008 -0400 +++ b/src/compiler.sig Thu Oct 30 16:58:54 2008 -0400 @@ -61,6 +61,7 @@ val termination : (Elab.file, Elab.file) phase val explify : (Elab.file, Expl.file) phase val corify : (Expl.file, Core.file) phase + val especialize : (Core.file, Core.file) phase val shake : (Core.file, Core.file) phase val tag : (Core.file, Core.file) phase val reduce : (Core.file, Core.file) phase @@ -82,6 +83,7 @@ val toTermination : (string, Elab.file) transform val toExplify : (string, Expl.file) transform val toCorify : (string, Core.file) transform + val toEspecialize : (string, Core.file) transform val toShake1 : (string, Core.file) transform val toTag : (string, Core.file) transform val toReduce : (string, Core.file) transform diff -r 9095a95a1bf9 -r bd9ee9aeca2f src/compiler.sml --- a/src/compiler.sml Thu Oct 30 15:39:06 2008 -0400 +++ b/src/compiler.sml Thu Oct 30 16:58:54 2008 -0400 @@ -404,12 +404,19 @@ val toCorify = transform corify "corify" o toExplify +val especialize = { + func = ESpecialize.specialize, + print = CorePrint.p_file CoreEnv.empty +} + +val toEspecialize = transform especialize "especialize" o toCorify + val shake = { func = Shake.shake, print = CorePrint.p_file CoreEnv.empty } -val toShake1 = transform shake "shake1" o toCorify +val toShake1 = transform shake "shake1" o toEspecialize val tag = { func = Tag.tag, diff -r 9095a95a1bf9 -r bd9ee9aeca2f src/core_env.sig --- a/src/core_env.sig Thu Oct 30 15:39:06 2008 -0400 +++ b/src/core_env.sig Thu Oct 30 16:58:54 2008 -0400 @@ -33,6 +33,9 @@ val liftConInExp : int -> Core.exp -> Core.exp val subConInExp : (int * Core.con) -> Core.exp -> Core.exp + val liftExpInExp : int -> Core.exp -> Core.exp + val subExpInExp : (int * Core.exp) -> Core.exp -> Core.exp + type env val empty : env diff -r 9095a95a1bf9 -r bd9ee9aeca2f src/core_env.sml --- a/src/core_env.sml Thu Oct 30 15:39:06 2008 -0400 +++ b/src/core_env.sml Thu Oct 30 16:58:54 2008 -0400 @@ -93,6 +93,35 @@ bind = fn ((xn, rep), U.Exp.RelC _) => (xn+1, liftConInCon 0 rep) | (ctx, _) => ctx} +val liftExpInExp = + U.Exp.mapB {kind = fn k => k, + con = fn _ => fn c => c, + exp = fn bound => fn e => + case e of + ERel xn => + if xn < bound then + e + else + ERel (xn + 1) + | _ => e, + bind = fn (bound, U.Exp.RelE _) => bound + 1 + | (bound, _) => bound} + +val subExpInExp = + U.Exp.mapB {kind = fn k => k, + con = fn _ => fn c => c, + exp = fn (xn, rep) => fn e => + case e of + ERel xn' => + (case Int.compare (xn', xn) of + EQUAL => #1 rep + | GREATER=> ERel (xn' - 1) + | LESS => e) + | _ => e, + bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep) + | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep) + | (ctx, _) => ctx} + (* Back to environments *) exception UnboundRel of int diff -r 9095a95a1bf9 -r bd9ee9aeca2f src/core_util.sig --- a/src/core_util.sig Thu Oct 30 15:39:06 2008 -0400 +++ b/src/core_util.sig Thu Oct 30 16:58:54 2008 -0400 @@ -107,6 +107,11 @@ val exists : {kind : Core.kind' -> bool, con : Core.con' -> bool, exp : Core.exp' -> bool} -> Core.exp -> bool + + val foldMap : {kind : Core.kind' * 'state -> Core.kind' * 'state, + con : Core.con' * 'state -> Core.con' * 'state, + exp : Core.exp' * 'state -> Core.exp' * 'state} + -> 'state -> Core.exp -> Core.exp * 'state end structure Decl : sig diff -r 9095a95a1bf9 -r bd9ee9aeca2f src/core_util.sml --- a/src/core_util.sml Thu Oct 30 15:39:06 2008 -0400 +++ b/src/core_util.sml Thu Oct 30 16:58:54 2008 -0400 @@ -578,6 +578,13 @@ S.Return _ => true | S.Continue _ => false +fun foldMap {kind, con, exp} s e = + case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)), + con = fn c => fn s => S.Continue (con (c, s)), + exp = fn e => fn s => S.Continue (exp (e, s))} e s of + S.Continue v => v + | S.Return _ => raise Fail "CoreUtil.Exp.foldMap: Impossible" + end structure Decl = struct diff -r 9095a95a1bf9 -r bd9ee9aeca2f src/especialize.sig --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/especialize.sig Thu Oct 30 16:58:54 2008 -0400 @@ -0,0 +1,32 @@ +(* Copyright (c) 2008, Adam Chlipala + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * - Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * - Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * - The names of contributors may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + *) + +signature ESPECIALIZE = sig + + val specialize : Core.file -> Core.file + +end diff -r 9095a95a1bf9 -r bd9ee9aeca2f src/especialize.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/especialize.sml Thu Oct 30 16:58:54 2008 -0400 @@ -0,0 +1,176 @@ +(* Copyright (c) 2008, Adam Chlipala + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * - Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * - Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * - The names of contributors may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + *) + +structure ESpecialize :> ESPECIALIZE = struct + +open Core + +structure E = CoreEnv +structure U = CoreUtil + +structure ILK = struct +type ord_key = int list +val compare = Order.joinL Int.compare +end + +structure ILM = BinaryMapFn(ILK) +structure IM = IntBinaryMap + +type func = { + name : string, + args : int ILM.map, + body : exp, + typ : con, + tag : string +} + +type state = { + maxName : int, + funcs : func IM.map, + decls : (string * int * con * exp * string) list +} + +fun kind (k, st) = (k, st) +fun con (c, st) = (c, st) + +fun exp (e, st : state) = + let + fun getApp e = + case e of + ENamed f => SOME (f, [], []) + | EApp (e1, (ENamed x, _)) => + (case getApp (#1 e1) of + NONE => NONE + | SOME (f, xs, xs') => SOME (f, xs @ [x], xs')) + | EApp (e1, e2) => + (case getApp (#1 e1) of + NONE => NONE + | SOME (f, xs, xs') => SOME (f, xs, xs' @ [e2])) + | _ => NONE + in + case getApp e of + NONE => (e, st) + | SOME (_, [], _) => (e, st) + | SOME (f, xs, xs') => + case IM.find (#funcs st, f) of + NONE => (e, st) + | SOME {name, args, body, typ, tag} => + case ILM.find (args, xs) of + SOME f' => (#1 (foldl (fn (e, arg) => (EApp (e, arg), ErrorMsg.dummySpan)) + (ENamed f', ErrorMsg.dummySpan) xs'), + st) + | NONE => + let + fun subBody (body, typ, xs) = + case (#1 body, #1 typ, xs) of + (_, _, []) => SOME (body, typ) + | (EAbs (_, _, _, body'), TFun (_, typ'), x :: xs) => + subBody (E.subExpInExp (0, (ENamed x, ErrorMsg.dummySpan)) body', + typ', + xs) + | _ => NONE + in + case subBody (body, typ, xs) of + NONE => (e, st) + | SOME (body', typ') => + let + val f' = #maxName st + val funcs = IM.insert (#funcs st, f, {name = name, + args = ILM.insert (args, xs, f'), + body = body, + typ = typ, + tag = tag}) + val st = { + maxName = f' + 1, + funcs = funcs, + decls = #decls st + } + + val (body', st) = specExp st body' + val e' = foldl (fn (e, arg) => (EApp (e, arg), ErrorMsg.dummySpan)) + (ENamed f', ErrorMsg.dummySpan) xs' + in + (#1 e', + {maxName = #maxName st, + funcs = #funcs st, + decls = (name, f', typ', body', tag ^ "_espec") :: #decls st}) + end + end + end + +and specExp st = U.Exp.foldMap {kind = kind, con = con, exp = exp} st + +fun decl (d, st) = (d, st) + +val specDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl} + +fun specialize file = + let + fun doDecl (d, st) = + let + val (d', st) = specDecl st d + + val funcs = #funcs st + val funcs = + case #1 d of + DVal (x, n, c, e as (EAbs _, _), tag) => + IM.insert (funcs, n, {name = x, + args = ILM.empty, + body = e, + typ = c, + tag = tag}) + | DValRec vis => + foldl (fn ((x, n, c, e, tag), funcs) => + IM.insert (funcs, n, {name = x, + args = ILM.empty, + body = e, + typ = c, + tag = tag})) + funcs vis + | _ => funcs + + val ds = + case #decls st of + [] => [d'] + | vis => [(DValRec vis, ErrorMsg.dummySpan), d'] + in + (ds, {maxName = #maxName st, + funcs = funcs, + decls = []}) + end + + val (ds, _) = ListUtil.foldlMapConcat doDecl + {maxName = U.File.maxName file + 1, + funcs = IM.empty, + decls = []} + file + in + ds + end + + +end diff -r 9095a95a1bf9 -r bd9ee9aeca2f src/reduce.sml --- a/src/reduce.sml Thu Oct 30 15:39:06 2008 -0400 +++ b/src/reduce.sml Thu Oct 30 16:58:54 2008 -0400 @@ -37,36 +37,8 @@ val liftConInCon = E.liftConInCon val subConInCon = E.subConInCon val liftConInExp = E.liftConInExp - -val liftExpInExp = - U.Exp.mapB {kind = fn k => k, - con = fn _ => fn c => c, - exp = fn bound => fn e => - case e of - ERel xn => - if xn < bound then - e - else - ERel (xn + 1) - | _ => e, - bind = fn (bound, U.Exp.RelE _) => bound + 1 - | (bound, _) => bound} - -val subExpInExp = - U.Exp.mapB {kind = fn k => k, - con = fn _ => fn c => c, - exp = fn (xn, rep) => fn e => - case e of - ERel xn' => - (case Int.compare (xn', xn) of - EQUAL => #1 rep - | GREATER=> ERel (xn' - 1) - | LESS => e) - | _ => e, - bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep) - | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep) - | (ctx, _) => ctx} - +val liftExpInExp = E.liftExpInExp +val subExpInExp = E.subExpInExp val liftConInExp = E.liftConInExp val subConInExp = E.subConInExp diff -r 9095a95a1bf9 -r bd9ee9aeca2f src/sources --- a/src/sources Thu Oct 30 15:39:06 2008 -0400 +++ b/src/sources Thu Oct 30 16:58:54 2008 -0400 @@ -93,6 +93,9 @@ specialize.sig specialize.sml +especialize.sig +especialize.sml + tag.sig tag.sml