# HG changeset patch # User Adam Chlipala # Date 1221140207 14400 # Node ID e21d0dddda09a9dcd07f7ace8e90f6be302aefe6 # Parent a07f476d9b618072377bccf611303ad2bb76f40e Unpoly non-recursive function diff -r a07f476d9b61 -r e21d0dddda09 src/compiler.sig --- a/src/compiler.sig Tue Sep 09 12:36:13 2008 -0400 +++ b/src/compiler.sig Thu Sep 11 09:36:47 2008 -0400 @@ -62,6 +62,7 @@ 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 @@ 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 -r a07f476d9b61 -r e21d0dddda09 src/compiler.sml --- a/src/compiler.sml Tue Sep 09 12:36:13 2008 -0400 +++ b/src/compiler.sml Thu Sep 11 09:36:47 2008 -0400 @@ -405,12 +405,19 @@ 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 -r a07f476d9b61 -r e21d0dddda09 src/core_env.sig --- a/src/core_env.sig Tue Sep 09 12:36:13 2008 -0400 +++ b/src/core_env.sig Thu Sep 11 09:36:47 2008 -0400 @@ -30,6 +30,9 @@ 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 -r a07f476d9b61 -r e21d0dddda09 src/core_env.sml --- a/src/core_env.sml Tue Sep 09 12:36:13 2008 -0400 +++ b/src/core_env.sml Thu Sep 11 09:36:47 2008 -0400 @@ -65,6 +65,34 @@ | (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 -r a07f476d9b61 -r e21d0dddda09 src/reduce.sml --- a/src/reduce.sml Tue Sep 09 12:36:13 2008 -0400 +++ b/src/reduce.sml Thu Sep 11 09:36:47 2008 -0400 @@ -65,33 +65,8 @@ 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 -r a07f476d9b61 -r e21d0dddda09 src/sources --- a/src/sources Tue Sep 09 12:36:13 2008 -0400 +++ b/src/sources Thu Sep 11 09:36:47 2008 -0400 @@ -81,6 +81,9 @@ shake.sig shake.sml +unpoly.sig +unpoly.sml + specialize.sig specialize.sml diff -r a07f476d9b61 -r e21d0dddda09 src/specialize.sig --- a/src/specialize.sig Tue Sep 09 12:36:13 2008 -0400 +++ b/src/specialize.sig Thu Sep 11 09:36:47 2008 -0400 @@ -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 -r a07f476d9b61 -r e21d0dddda09 src/specialize.sml --- a/src/specialize.sml Tue Sep 09 12:36:13 2008 -0400 +++ b/src/specialize.sml Thu Sep 11 09:36:47 2008 -0400 @@ -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 @@ count : int, datatypes : datatyp IM.map, constructors : int IM.map, - decls : decl list + decls : decl list } fun kind (k, st) = (k, st) diff -r a07f476d9b61 -r e21d0dddda09 src/unpoly.sig --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/unpoly.sig Thu Sep 11 09:36:47 2008 -0400 @@ -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 -r a07f476d9b61 -r e21d0dddda09 src/unpoly.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/unpoly.sml Thu Sep 11 09:36:47 2008 -0400 @@ -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 diff -r a07f476d9b61 -r e21d0dddda09 tests/specialize.ur --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/specialize.ur Thu Sep 11 09:36:47 2008 -0400 @@ -0,0 +1,26 @@ +datatype list a = Nil | Cons of a * list a + +fun isNil (t ::: Type) (ls : list t) : bool = + case ls of + Nil => True + | Cons _ => False + +(*fun append (t ::: Type) (ls1 : list t) (ls2 : list t) : list t = + case ls1 of + Nil => ls2 + | Cons (x, ls1') => Cons (x, append ls1' ls2) + +fun delist (ls : list string) : xml body [] [] = + case ls of + Nil => Nil + | Cons (h, t) => {cdata h} :: {delist t}*) + +val ls = Cons ("X", Cons ("Y", Cons ("Z", Nil))) + +fun main () : transaction page = return + {if isNil ls then It's Nil. else It's not Nil.} + + + +(*

{delist ls}

*) + diff -r a07f476d9b61 -r e21d0dddda09 tests/specialize.urp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/specialize.urp Thu Sep 11 09:36:47 2008 -0400 @@ -0,0 +1,6 @@ +debug +database dbname=test +exe /tmp/webapp + +specialize +