From 7bc788c67ed9331773355ceeae4ace7923a6e914 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 11 Sep 2008 09:36:47 -0400 Subject: Unpoly non-recursive function --- src/compiler.sig | 4 +- src/compiler.sml | 9 ++- src/core_env.sig | 3 + src/core_env.sml | 28 +++++++ src/reduce.sml | 29 +------ src/sources | 3 + src/specialize.sig | 2 +- src/specialize.sml | 4 +- src/unpoly.sig | 34 ++++++++ src/unpoly.sml | 224 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 10 files changed, 308 insertions(+), 32 deletions(-) create mode 100644 src/unpoly.sig create mode 100644 src/unpoly.sml (limited to 'src') diff --git a/src/compiler.sig b/src/compiler.sig index 2312a047..1388537f 100644 --- a/src/compiler.sig +++ b/src/compiler.sig @@ -62,6 +62,7 @@ signature COMPILER = sig val shake : (Core.file, Core.file) phase val tag : (Core.file, Core.file) phase val reduce : (Core.file, Core.file) phase + val unpoly : (Core.file, Core.file) phase val specialize : (Core.file, Core.file) phase val monoize : (Core.file, Mono.file) phase val mono_opt : (Mono.file, Mono.file) phase @@ -81,7 +82,8 @@ signature COMPILER = sig val toShake1 : (string, Core.file) transform val toTag : (string, Core.file) transform val toReduce : (string, Core.file) transform - val toSpecialize : (string, Core.file) transform + val toUnpoly : (string, Core.file) transform + val toSpecialize : (string, Core.file) transform val toShake2 : (string, Core.file) transform val toMonoize : (string, Mono.file) transform val toMono_opt1 : (string, Mono.file) transform diff --git a/src/compiler.sml b/src/compiler.sml index f408837d..aad6bdf3 100644 --- a/src/compiler.sml +++ b/src/compiler.sml @@ -405,12 +405,19 @@ val reduce = { val toReduce = transform reduce "reduce" o toTag +val unpoly = { + func = Unpoly.unpoly, + print = CorePrint.p_file CoreEnv.empty +} + +val toUnpoly = transform unpoly "unpoly" o toReduce + val specialize = { func = Specialize.specialize, print = CorePrint.p_file CoreEnv.empty } -val toSpecialize = transform specialize "specialize" o toReduce +val toSpecialize = transform specialize "specialize" o toUnpoly val toShake2 = transform shake "shake2" o toSpecialize diff --git a/src/core_env.sig b/src/core_env.sig index 7b72235f..cdbf5946 100644 --- a/src/core_env.sig +++ b/src/core_env.sig @@ -30,6 +30,9 @@ signature CORE_ENV = sig val liftConInCon : int -> Core.con -> Core.con val subConInCon : (int * Core.con) -> Core.con -> Core.con + val liftConInExp : int -> Core.exp -> Core.exp + val subConInExp : (int * Core.con) -> Core.exp -> Core.exp + type env val empty : env diff --git a/src/core_env.sml b/src/core_env.sml index e2a3c40f..a4d5fc50 100644 --- a/src/core_env.sml +++ b/src/core_env.sml @@ -65,6 +65,34 @@ val subConInCon = | (ctx, _) => ctx} +val liftConInExp = + U.Exp.mapB {kind = fn k => k, + con = fn bound => fn c => + case c of + CRel xn => + if xn < bound then + c + else + CRel (xn + 1) + | _ => c, + exp = fn _ => fn e => e, + bind = fn (bound, U.Exp.RelC _) => bound + 1 + | (bound, _) => bound} + +val subConInExp = + U.Exp.mapB {kind = fn k => k, + con = fn (xn, rep) => fn c => + case c of + CRel xn' => + (case Int.compare (xn', xn) of + EQUAL => #1 rep + | GREATER => CRel (xn' - 1) + | LESS => c) + | _ => c, + exp = fn _ => fn e => e, + bind = fn ((xn, rep), U.Exp.RelC _) => (xn+1, liftConInCon 0 rep) + | (ctx, _) => ctx} + (* Back to environments *) exception UnboundRel of int diff --git a/src/reduce.sml b/src/reduce.sml index e8d51da7..89b9b30e 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -65,33 +65,8 @@ val subExpInExp = bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep) | (ctx, _) => ctx} -val liftConInExp = - U.Exp.mapB {kind = fn k => k, - con = fn bound => fn c => - case c of - CRel xn => - if xn < bound then - c - else - CRel (xn + 1) - | _ => c, - exp = fn _ => fn e => e, - bind = fn (bound, U.Exp.RelC _) => bound + 1 - | (bound, _) => bound} - -val subConInExp = - U.Exp.mapB {kind = fn k => k, - con = fn (xn, rep) => fn c => - case c of - CRel xn' => - (case Int.compare (xn', xn) of - EQUAL => #1 rep - | GREATER => CRel (xn' - 1) - | LESS => c) - | _ => c, - exp = fn _ => fn e => e, - bind = fn ((xn, rep), U.Exp.RelC _) => (xn+1, liftConInCon 0 rep) - | (ctx, _) => ctx} +val liftConInExp = E.liftConInExp +val subConInExp = E.subConInExp fun bindC (env, b) = case b of diff --git a/src/sources b/src/sources index 0a3761d5..a30626a8 100644 --- a/src/sources +++ b/src/sources @@ -81,6 +81,9 @@ reduce.sml shake.sig shake.sml +unpoly.sig +unpoly.sml + specialize.sig specialize.sml diff --git a/src/specialize.sig b/src/specialize.sig index f45c8b19..9b0d1e81 100644 --- a/src/specialize.sig +++ b/src/specialize.sig @@ -25,7 +25,7 @@ * POSSIBILITY OF SUCH DAMAGE. *) -(* Simplify a Core program by repeating polymorphic definitions *) +(* Simplify a Core program by repeating polymorphic definitions of datatypes *) signature SPECIALIZE = sig diff --git a/src/specialize.sml b/src/specialize.sml index c8af5199..ddaff92e 100644 --- a/src/specialize.sml +++ b/src/specialize.sml @@ -25,7 +25,7 @@ * POSSIBILITY OF SUCH DAMAGE. *) -(* Simplify a Core program algebraically *) +(* Simplify a Core program by repeating polymorphic definitions of datatypes *) structure Specialize :> SPECIALIZE = struct @@ -61,7 +61,7 @@ type state = { count : int, datatypes : datatyp IM.map, constructors : int IM.map, - decls : decl list + decls : decl list } fun kind (k, st) = (k, st) diff --git a/src/unpoly.sig b/src/unpoly.sig new file mode 100644 index 00000000..aba38254 --- /dev/null +++ b/src/unpoly.sig @@ -0,0 +1,34 @@ +(* 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. + *) + +(* Simplify a Core program by repeating polymorphic function definitions *) + +signature UNPOLY = sig + + val unpoly : Core.file -> Core.file + +end diff --git a/src/unpoly.sml b/src/unpoly.sml new file mode 100644 index 00000000..917a8cc8 --- /dev/null +++ b/src/unpoly.sml @@ -0,0 +1,224 @@ +(* 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. + *) + +(* Simplify a Core program by repeating polymorphic function definitions *) + +structure Unpoly :> UNPOLY = struct + +open Core + +structure E = CoreEnv +structure U = CoreUtil + +structure IS = IntBinarySet +structure IM = IntBinaryMap + + +(** The actual specialization *) + +val liftConInCon = E.liftConInCon +val subConInCon = E.subConInCon + +val liftConInExp = E.liftConInExp +val subConInExp = E.subConInExp + +type state = { + funcs : (kind list * (string * int * con * exp * string) list) IM.map, + decls : decl list, + nextName : int +} + +fun kind (k, st) = (k, st) + +fun con (c, st) = (c, st) + +fun exp (e, st : state) = + case e of + ECApp _ => + let + (*val () = Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty (e, ErrorMsg.dummySpan))]*) + + fun unravel (e, cargs) = + case e of + ECApp ((e, _), c) => unravel (e, c :: cargs) + | ENamed n => SOME (n, rev cargs) + | _ => NONE + in + case unravel (e, []) of + NONE => (e, st) + | SOME (n, cargs) => + case IM.find (#funcs st, n) of + NONE => (e, st) + | SOME (ks, vis) => + let + val (vis, nextName) = ListUtil.foldlMap + (fn ((x, n, t, e, s), nextName) => + ((x, nextName, n, t, e, s), nextName + 1)) + (#nextName st) vis + + fun specialize (x, n, n_old, t, e, s) = + let + fun trim (t, e, cargs) = + case (t, e, cargs) of + ((TCFun (_, _, t), _), + (ECAbs (_, _, e), _), + carg :: cargs) => + let + val t = subConInCon (length cargs, carg) t + val e = subConInExp (length cargs, carg) e + in + trim (t, e, cargs) + end + | (_, _, []) => SOME (t, e) + | _ => NONE + in + (*Print.prefaces "specialize" + [("t", CorePrint.p_con CoreEnv.empty t), + ("e", CorePrint.p_exp CoreEnv.empty e), + ("|cargs|", Print.PD.string (Int.toString (length cargs)))];*) + Option.map (fn (t, e) => (x, n, n_old, t, e, s)) + (trim (t, e, cargs)) + end + + val vis = List.map specialize vis + in + if List.exists (not o Option.isSome) vis then + (e, st) + else + let + val vis = List.mapPartial (fn x => x) vis + val vis' = map (fn (x, n, _, t, e, s) => + (x ^ "_unpoly", n, t, e, s)) vis + in + case List.find (fn (_, _, n_old, _, _, _) => n_old = n) vis of + NONE => raise Fail "Unpoly: Inconsistent 'val rec' record" + | SOME (_, n, _, _, _, _) => + (ENamed n, + {funcs = #funcs st, + decls = (DValRec vis', ErrorMsg.dummySpan) :: #decls st, + nextName = nextName}) + end + end + end + | _ => (e, st) + +fun decl (d, st : state) = + case d of + DValRec (vis as ((x, n, t, e, s) :: rest)) => + let + fun unravel (e, cargs) = + case e of + (ECAbs (_, k, e), _) => + unravel (e, k :: cargs) + | _ => rev cargs + + val cargs = unravel (e, []) + + fun unravel (e, cargs) = + case (e, cargs) of + ((ECAbs (_, k, e), _), k' :: cargs) => + U.Kind.compare (k, k') = EQUAL + andalso unravel (e, cargs) + | (_, []) => true + | _ => false + in + if List.exists (fn vi => not (unravel (#4 vi, cargs))) rest then + (d, st) + else + let + val ns = IS.addList (IS.empty, map #2 vis) + val nargs = length cargs + + fun deAbs (e, cargs) = + case (e, cargs) of + ((ECAbs (_, _, e), _), _ :: cargs) => deAbs (e, cargs) + | (_, []) => e + | _ => raise Fail "Unpoly: deAbs" + + (** Verifying lack of polymorphic recursion *) + + fun kind _ = false + fun con _ = false + + fun exp e = + case e of + ECApp (e, c) => + let + fun isIrregular (e, pos) = + case #1 e of + ENamed n => + IS.member (ns, n) + andalso + (case #1 c of + CRel i => i <> nargs - pos + | _ => true) + | ECApp (e, _) => isIrregular (e, pos + 1) + | _ => false + in + isIrregular (e, 1) + end + | ECAbs _ => true + | _ => false + + val irregular = U.Exp.exists {kind = kind, con = con, exp = exp} + in + if List.exists (fn x => irregular (deAbs (#4 x, cargs))) vis then + (d, st) + else + (d, {funcs = foldl (fn (vi, funcs) => + IM.insert (funcs, #2 vi, (cargs, vis))) + (#funcs st) vis, + decls = #decls st, + nextName = #nextName st}) + end + end + + | _ => (d, st) + +val polyDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl} + +fun unpoly file = + let + fun doDecl (d : decl, st : state) = + let + val (d, st) = polyDecl st d + in + (rev (d :: #decls st), + {funcs = #funcs st, + decls = [], + nextName = #nextName st}) + end + + val (ds, _) = ListUtil.foldlMapConcat doDecl + {funcs = IM.empty, + decls = [], + nextName = U.File.maxName file + 1} file + in + ds + end + +end -- cgit v1.2.3