# HG changeset patch # User Adam Chlipala # Date 1218232551 14400 # Node ID 8a70e2919e86ef053e3fad29eed6ba326bfff133 # Parent 9bbf4d383381a8894d4f5418d808adccab6bfe3e Specialization of single-parameter datatypes diff -r 9bbf4d383381 -r 8a70e2919e86 src/compiler.sig --- a/src/compiler.sig Fri Aug 08 10:59:06 2008 -0400 +++ b/src/compiler.sig Fri Aug 08 17:55:51 2008 -0400 @@ -46,6 +46,7 @@ val shake' : job -> Core.file option val tag : job -> Core.file option val reduce : job -> Core.file option + val specialize : job -> Core.file option val shake : job -> Core.file option val monoize : job -> Mono.file option val mono_opt' : job -> Mono.file option @@ -62,6 +63,7 @@ val testShake' : job -> unit val testTag : job -> unit val testReduce : job -> unit + val testSpecialize : job -> unit val testShake : job -> unit val testMonoize : job -> unit val testMono_opt' : job -> unit diff -r 9bbf4d383381 -r 8a70e2919e86 src/compiler.sml --- a/src/compiler.sml Fri Aug 08 10:59:06 2008 -0400 +++ b/src/compiler.sml Fri Aug 08 17:55:51 2008 -0400 @@ -214,10 +214,19 @@ if ErrorMsg.anyErrors () then NONE else - SOME (Reduce.reduce (Shake.shake file)) + SOME (Reduce.reduce file) + +fun specialize job = + case reduce job of + NONE => NONE + | SOME file => + if ErrorMsg.anyErrors () then + NONE + else + SOME (Specialize.specialize file) fun shake job = - case reduce job of + case specialize job of NONE => NONE | SOME file => if ErrorMsg.anyErrors () then @@ -332,8 +341,8 @@ handle CoreEnv.UnboundNamed n => print ("Unbound named " ^ Int.toString n ^ "\n") -fun testTag job = - (case tag job of +fun testReduce job = + (case reduce job of NONE => print "Failed\n" | SOME file => (Print.print (CorePrint.p_file CoreEnv.empty file); @@ -341,8 +350,17 @@ handle CoreEnv.UnboundNamed n => print ("Unbound named " ^ Int.toString n ^ "\n") -fun testReduce job = - (case reduce job of +fun testSpecialize job = + (case specialize job of + NONE => print "Failed\n" + | SOME file => + (Print.print (CorePrint.p_file CoreEnv.empty file); + print "\n")) + handle CoreEnv.UnboundNamed n => + print ("Unbound named " ^ Int.toString n ^ "\n") + +fun testTag job = + (case tag job of NONE => print "Failed\n" | SOME file => (Print.print (CorePrint.p_file CoreEnv.empty file); diff -r 9bbf4d383381 -r 8a70e2919e86 src/core_env.sig --- a/src/core_env.sig Fri Aug 08 10:59:06 2008 -0400 +++ b/src/core_env.sig Fri Aug 08 17:55:51 2008 -0400 @@ -28,6 +28,7 @@ signature CORE_ENV = sig val liftConInCon : int -> Core.con -> Core.con + val subConInCon : (int * Core.con) -> Core.con -> Core.con type env @@ -54,5 +55,6 @@ val lookupENamed : env -> int -> string * Core.con * Core.exp option * string val declBinds : env -> Core.decl -> env + val patBinds : env -> Core.pat -> env end diff -r 9bbf4d383381 -r 8a70e2919e86 src/core_env.sml --- a/src/core_env.sml Fri Aug 08 10:59:06 2008 -0400 +++ b/src/core_env.sml Fri Aug 08 17:55:51 2008 -0400 @@ -51,6 +51,19 @@ val lift = liftConInCon 0 +val subConInCon = + U.Con.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, + bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep) + | (ctx, _) => ctx} + (* Back to environments *) @@ -175,4 +188,13 @@ | DValRec vis => foldl (fn ((x, n, t, e, s), env) => pushENamed env x n t NONE s) env vis | DExport _ => env +fun patBinds env (p, loc) = + case p of + PWild => env + | PVar (x, t) => pushERel env x t + | PPrim _ => env + | PCon (_, _, _, NONE) => env + | PCon (_, _, _, SOME p) => patBinds env p + | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps + end diff -r 9bbf4d383381 -r 8a70e2919e86 src/core_print.sig --- a/src/core_print.sig Fri Aug 08 10:59:06 2008 -0400 +++ b/src/core_print.sig Fri Aug 08 17:55:51 2008 -0400 @@ -30,6 +30,7 @@ signature CORE_PRINT = sig val p_kind : Core.kind Print.printer val p_con : CoreEnv.env -> Core.con Print.printer + val p_pat : CoreEnv.env -> Core.pat Print.printer val p_exp : CoreEnv.env -> Core.exp Print.printer val p_decl : CoreEnv.env -> Core.decl Print.printer val p_file : CoreEnv.env -> Core.file Print.printer diff -r 9bbf4d383381 -r 8a70e2919e86 src/core_print.sml --- a/src/core_print.sml Fri Aug 08 10:59:06 2008 -0400 +++ b/src/core_print.sml Fri Aug 08 17:55:51 2008 -0400 @@ -199,10 +199,14 @@ string (#1 (E.lookupERel env n))) handle E.UnboundRel _ => string ("UNBOUND_" ^ Int.toString n)) | ENamed n => p_enamed env n - | ECon (_, pc, _, NONE) => p_patCon env pc - | ECon (_, pc, _, SOME e) => parenIf par (box [p_patCon env pc, - space, - p_exp' true env e]) + | ECon (_, pc, _, NONE) => box [string "[", + p_patCon env pc, + string "]"] + | ECon (_, pc, _, SOME e) => box [string "[", + p_patCon env pc, + space, + p_exp' true env e, + string "]"] | EFfi (m, x) => box [string "FFI(", string m, string ".", string x, string ")"] | EFfiApp (m, x, es) => box [string "FFI(", string m, @@ -301,7 +305,7 @@ space, string "=>", space, - p_exp env e]) pes]) + p_exp (E.patBinds env p) e]) pes]) | EWrite e => box [string "write(", p_exp env e, @@ -349,10 +353,15 @@ val k = (KType, ErrorMsg.dummySpan) val env = E.pushCNamed env x n (KType, ErrorMsg.dummySpan) NONE val env = foldl (fn (x, env) => E.pushCRel env x k) env xs + + val xp = if !debug then + string (x ^ "__" ^ Int.toString n) + else + string x in box [string "datatype", space, - string x, + xp, p_list_sep (box []) (fn x => box [space, string x]) xs, space, string "=", @@ -360,7 +369,7 @@ p_list_sep (box [space, string "|", space]) (fn (x, n, NONE) => if !debug then (string (x ^ "__" ^ Int.toString n)) else string x - | (x, _, SOME t) => box [if !debug then (string (x ^ "__" ^ Int.toString n)) + | (x, n, SOME t) => box [if !debug then (string (x ^ "__" ^ Int.toString n)) else string x, space, string "of", space, p_con env t]) cons] end diff -r 9bbf4d383381 -r 8a70e2919e86 src/core_util.sig --- a/src/core_util.sig Fri Aug 08 10:59:06 2008 -0400 +++ b/src/core_util.sig Fri Aug 08 17:55:51 2008 -0400 @@ -30,6 +30,8 @@ val classifyDatatype : (string * int * Core.con option) list -> Core.datatype_kind structure Kind : sig + val compare : Core.kind * Core.kind -> order + val mapfold : (Core.kind', 'state, 'abort) Search.mapfolder -> (Core.kind, 'state, 'abort) Search.mapfolder val map : (Core.kind' -> Core.kind') -> Core.kind -> Core.kind @@ -37,6 +39,8 @@ end structure Con : sig + val compare : Core.con * Core.con -> order + datatype binder = Rel of string * Core.kind | Named of string * int * Core.kind * Core.con option @@ -64,6 +68,10 @@ val exists : {kind : Core.kind' -> bool, con : Core.con' -> bool} -> Core.con -> bool + + val foldMap : {kind : Core.kind' * 'state -> Core.kind' * 'state, + con : Core.con' * 'state -> Core.con' * 'state} + -> 'state -> Core.con -> Core.con * 'state end structure Exp : sig diff -r 9bbf4d383381 -r 8a70e2919e86 src/core_util.sml --- a/src/core_util.sml Fri Aug 08 10:59:06 2008 -0400 +++ b/src/core_util.sml Fri Aug 08 17:55:51 2008 -0400 @@ -39,6 +39,28 @@ structure Kind = struct +open Order + +fun compare ((k1, _), (k2, _)) = + case (k1, k2) of + (KType, KType) => EQUAL + | (KType, _) => LESS + | (_, KType) => GREATER + + | (KArrow (d1, r1), KArrow (d2, r2)) => join (compare (d1, d2), fn () => compare (r1, r2)) + | (KArrow _, _) => LESS + | (_, KArrow _) => GREATER + + | (KName, KName) => EQUAL + | (KName, _) => LESS + | (_, KName) => GREATER + + | (KRecord k1, KRecord k2) => compare (k1, k2) + | (KRecord _, _) => LESS + | (_, KRecord _) => GREATER + + | (KUnit, KUnit) => EQUAL + fun mapfold f = let fun mfk k acc = @@ -85,6 +107,76 @@ structure Con = struct +open Order + +fun compare ((c1, _), (c2, _)) = + case (c1, c2) of + (TFun (d1, r1), TFun (d2, r2)) => join (compare (d1, d2), fn () => compare (r1, r2)) + | (TFun _, _) => LESS + | (_, TFun _) => GREATER + + | (TCFun (x1, k1, r1), TCFun (x2, k2, r2)) => + join (String.compare (x1, x2), + fn () => join (Kind.compare (k1, k2), + fn () => compare (r1, r2))) + | (TCFun _, _) => LESS + | (_, TCFun _) => GREATER + + | (TRecord c1, TRecord c2) => compare (c1, c2) + | (TRecord _, _) => LESS + | (_, TRecord _) => GREATER + + | (CRel n1, CRel n2) => Int.compare (n1, n2) + | (CRel _, _) => LESS + | (_, CRel _) => GREATER + + | (CNamed n1, CNamed n2) => Int.compare (n1, n2) + | (CNamed _, _) => LESS + | (_, CNamed _) => GREATER + + | (CFfi (m1, s1), CFfi (m2, s2)) => join (String.compare (m1, m2), + fn () => String.compare (s1, s2)) + | (CFfi _, _) => LESS + | (_, CFfi _) => GREATER + + | (CApp (f1, x1), CApp (f2, x2)) => join (compare (f1, f2), + fn () => compare (x1, x2)) + | (CApp _, _) => LESS + | (_, CApp _) => GREATER + + | (CAbs (x1, k1, b1), CAbs (x2, k2, b2)) => + join (String.compare (x1, x2), + fn () => join (Kind.compare (k1, k2), + fn () => compare (b1, b2))) + | (CAbs _, _) => LESS + | (_, CAbs _) => GREATER + + | (CName s1, CName s2) => String.compare (s1, s2) + | (CName _, _) => LESS + | (_, CName _) => GREATER + + | (CRecord (k1, xvs1), CRecord (k2, xvs2)) => + join (Kind.compare (k1, k2), + fn () => joinL (fn ((x1, v1), (x2, v2)) => + join (compare (x1, x2), + fn () => compare (v1, v2))) (xvs1, xvs2)) + | (CRecord _, _) => LESS + | (_, CRecord _) => GREATER + + | (CConcat (f1, s1), CConcat (f2, s2)) => + join (compare (f1, f2), + fn () => compare (s1, s2)) + | (CConcat _, _) => LESS + | (_, CConcat _) => GREATER + + | (CFold (d1, r1), CFold (d2, r2)) => + join (Kind.compare (d1, r2), + fn () => Kind.compare (r1, r2)) + | (CFold _, _) => LESS + | (_, CFold _) => GREATER + + | (CUnit, CUnit) => EQUAL + datatype binder = Rel of string * kind | Named of string * int * kind * con option @@ -201,6 +293,12 @@ S.Return _ => true | S.Continue _ => false +fun foldMap {kind, con} s c = + case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)), + con = fn c => fn s => S.Continue (con (c, s))} c s of + S.Continue v => v + | S.Return _ => raise Fail "CoreUtil.Con.foldMap: Impossible" + end structure Exp = struct @@ -317,8 +415,22 @@ S.bind2 (mfe ctx e, fn e' => S.bind2 (ListUtil.mapfold (fn (p, e) => - S.map2 (mfe ctx e, - fn e' => (p, e'))) pes, + let + fun pb ((p, _), ctx) = + case p of + PWild => ctx + | PVar (x, t) => bind (ctx, RelE (x, t)) + | PPrim _ => ctx + | PCon (_, _, _, NONE) => ctx + | PCon (_, _, _, SOME p) => pb (p, ctx) + | PRecord xps => foldl (fn ((_, p, _), ctx) => + pb (p, ctx)) ctx xps + in + S.bind2 (mfp ctx p, + fn p' => + S.map2 (mfe (pb (p', ctx)) e, + fn e' => (p', e'))) + end) pes, fn pes' => S.bind2 (mfc ctx disc, fn disc' => @@ -335,6 +447,45 @@ S.map2 (ListUtil.mapfold (mfe ctx) es, fn es' => (EClosure (n, es'), loc)) + + and mfp ctx (pAll as (p, loc)) = + case p of + PWild => S.return2 pAll + | PVar (x, t) => + S.map2 (mfc ctx t, + fn t' => + (PVar (x, t'), loc)) + | PPrim _ => S.return2 pAll + | PCon (dk, pc, args, po) => + S.bind2 (mfpc ctx pc, + fn pc' => + S.bind2 (ListUtil.mapfold (mfc ctx) args, + fn args' => + S.map2 ((case po of + NONE => S.return2 NONE + | SOME p => S.map2 (mfp ctx p, SOME)), + fn po' => + (PCon (dk, pc', args', po'), loc)))) + | PRecord xps => + S.map2 (ListUtil.mapfold (fn (x, p, c) => + S.bind2 (mfp ctx p, + fn p' => + S.map2 (mfc ctx c, + fn c' => + (x, p', c')))) xps, + fn xps' => + (PRecord xps', loc)) + + and mfpc ctx pc = + case pc of + PConVar _ => S.return2 pc + | PConFfi {mod = m, datatyp, params, con, arg, kind} => + S.map2 ((case arg of + NONE => S.return2 NONE + | SOME c => S.map2 (mfc ctx c, SOME)), + fn arg' => + PConFfi {mod = m, datatyp = datatyp, params = params, + con = con, arg = arg', kind = kind}) in mfe end diff -r 9bbf4d383381 -r 8a70e2919e86 src/corify.sml --- a/src/corify.sml Fri Aug 08 10:59:06 2008 -0400 +++ b/src/corify.sml Fri Aug 08 17:55:51 2008 -0400 @@ -538,7 +538,7 @@ val k = (L'.KType, loc) val dcons = map (fn (x, n, to) => let - val args = ListUtil.mapi (fn (i, _) => (L'.CRel n, loc)) xs + val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) xs val (e, t) = case to of NONE => ((L'.ECon (dk, L'.PConVar n, args, NONE), loc), t) diff -r 9bbf4d383381 -r 8a70e2919e86 src/expl_print.sml --- a/src/expl_print.sml Fri Aug 08 10:59:06 2008 -0400 +++ b/src/expl_print.sml Fri Aug 08 17:55:51 2008 -0400 @@ -345,7 +345,7 @@ p_list_sep (box [space, string "|", space]) (fn (x, n, NONE) => if !debug then (string (x ^ "__" ^ Int.toString n)) else string x - | (x, _, SOME t) => box [if !debug then (string (x ^ "__" ^ Int.toString n)) + | (x, n, SOME t) => box [if !debug then (string (x ^ "__" ^ Int.toString n)) else string x, space, string "of", space, p_con env t]) cons] end diff -r 9bbf4d383381 -r 8a70e2919e86 src/mono_util.sml --- a/src/mono_util.sml Fri Aug 08 10:59:06 2008 -0400 +++ b/src/mono_util.sml Fri Aug 08 17:55:51 2008 -0400 @@ -39,18 +39,7 @@ structure Typ = struct -fun join (o1, o2) = - case o1 of - EQUAL => o2 () - | v => v - -fun joinL f (os1, os2) = - case (os1, os2) of - (nil, nil) => EQUAL - | (nil, _) => LESS - | (h1 :: t1, h2 :: t2) => - join (f (h1, h2), fn () => joinL f (t1, t2)) - | (_ :: _, nil) => GREATER +open Order fun compare ((t1, _), (t2, _)) = case (t1, t2) of diff -r 9bbf4d383381 -r 8a70e2919e86 src/monoize.sml --- a/src/monoize.sml Fri Aug 08 10:59:06 2008 -0400 +++ b/src/monoize.sml Fri Aug 08 17:55:51 2008 -0400 @@ -67,14 +67,16 @@ (L'.TFfi ("Basis", "string"), loc) | L.CRel _ => poly () - | L.CNamed n => raise Fail "Monoize CNamed" - (*let - val (_, xncs) = Env.lookupDatatype env n + | L.CNamed n => + let + val (_, xs, xncs) = Env.lookupDatatype env n val xncs = map (fn (x, n, to) => (x, n, Option.map (monoType env) to)) xncs in - (L'.TDatatype (MonoUtil.classifyDatatype xncs, n, xncs), loc) - end*) + case xs of + [] => (L'.TDatatype (MonoUtil.classifyDatatype xncs, n, xncs), loc) + | _ => poly () + end | L.CFfi mx => (L'.TFfi mx, loc) | L.CApp _ => poly () | L.CAbs _ => poly () @@ -206,7 +208,7 @@ let fun makeDecl n fm = let - val (x, xncs) = raise Fail "Monoize TDataype" (*Env.lookupDatatype env i*) + val (x, _, xncs) = Env.lookupDatatype env i val (branches, fm) = ListUtil.foldlMap @@ -292,13 +294,23 @@ | L.PConFfi {mod = m, datatyp, con, arg, ...} => L'.PConFfi {mod = m, datatyp = datatyp, con = con, arg = Option.map (monoType env) arg} -fun monoPat env (p, loc) = - case p of - L.PWild => (L'.PWild, loc) - | L.PVar (x, t) => (L'.PVar (x, monoType env t), loc) - | L.PPrim p => (L'.PPrim p, loc) - | L.PCon (dk, pc, _, po) => raise Fail "Monoize PCon" (*(L'.PCon (dk, monoPatCon env pc, Option.map (monoPat env) po), loc)*) - | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, monoPat env p, monoType env t)) xps), loc) +val dummyPat = (L'.PPrim (Prim.Int 0), ErrorMsg.dummySpan) + +fun monoPat env (all as (p, loc)) = + let + fun poly () = + (E.errorAt loc "Unsupported pattern"; + Print.eprefaces' [("Pattern", CorePrint.p_pat env all)]; + dummyPat) + in + case p of + L.PWild => (L'.PWild, loc) + | L.PVar (x, t) => (L'.PVar (x, monoType env t), loc) + | L.PPrim p => (L'.PPrim p, loc) + | L.PCon (dk, pc, [], po) => (L'.PCon (dk, monoPatCon env pc, Option.map (monoPat env) po), loc) + | L.PCon _ => poly () + | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, monoPat env p, monoType env t)) xps), loc) + end fun monoExp (env, st, fm) (all as (e, loc)) = let @@ -311,8 +323,8 @@ L.EPrim p => ((L'.EPrim p, loc), fm) | L.ERel n => ((L'.ERel n, loc), fm) | L.ENamed n => ((L'.ENamed n, loc), fm) - | L.ECon (dk, pc, _, eo) => raise Fail "Monoize ECon" - (*let + | L.ECon (dk, pc, [], eo) => + let val (eo, fm) = case eo of NONE => (NONE, fm) @@ -324,7 +336,8 @@ end in ((L'.ECon (dk, monoPatCon env pc, eo), loc), fm) - end*) + end + | L.ECon _ => poly () | L.EFfi mx => ((L'.EFfi mx, loc), fm) | L.EFfiApp (m, x, es) => let @@ -718,12 +731,13 @@ in case d of L.DCon _ => NONE - | L.DDatatype (x, n, _, xncs) => raise Fail "Monoize DDatatype" - (*let + | L.DDatatype (x, n, [], xncs) => + let val d = (L'.DDatatype (x, n, map (fn (x, n, to) => (x, n, Option.map (monoType env) to)) xncs), loc) in SOME (Env.declBinds env all, fm, d) - end*) + end + | L.DDatatype _ => poly () | L.DVal (x, n, t, e, s) => let val (e, fm) = monoExp (env, St.empty, fm) e diff -r 9bbf4d383381 -r 8a70e2919e86 src/order.sig --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/order.sig Fri Aug 08 17:55:51 2008 -0400 @@ -0,0 +1,35 @@ +(* 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. + *) + +(* Utility code for implementing comparisons *) + +signature ORDER = sig + + val join : order * (unit -> order) -> order + val joinL : ('a * 'b -> order) -> 'a list * 'b list -> order + +end diff -r 9bbf4d383381 -r 8a70e2919e86 src/order.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/order.sml Fri Aug 08 17:55:51 2008 -0400 @@ -0,0 +1,45 @@ +(* 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. + *) + +(* Utility code for implementing comparisons *) + +structure Order :> ORDER = struct + +fun join (o1, o2) = + case o1 of + EQUAL => o2 () + | v => v + +fun joinL f (os1, os2) = + case (os1, os2) of + (nil, nil) => EQUAL + | (nil, _) => LESS + | (h1 :: t1, h2 :: t2) => + join (f (h1, h2), fn () => joinL f (t1, t2)) + | (_ :: _, nil) => GREATER + +end diff -r 9bbf4d383381 -r 8a70e2919e86 src/reduce.sml --- a/src/reduce.sml Fri Aug 08 10:59:06 2008 -0400 +++ b/src/reduce.sml Fri Aug 08 17:55:51 2008 -0400 @@ -35,19 +35,7 @@ structure U = CoreUtil val liftConInCon = E.liftConInCon - -val subConInCon = - U.Con.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, - bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep) - | (ctx, _) => ctx} +val subConInCon = E.subConInCon val liftExpInExp = U.Exp.mapB {kind = fn k => k, diff -r 9bbf4d383381 -r 8a70e2919e86 src/sources --- a/src/sources Fri Aug 08 10:59:06 2008 -0400 +++ b/src/sources Fri Aug 08 17:55:51 2008 -0400 @@ -4,6 +4,9 @@ list_util.sig list_util.sml +order.sig +order.sml + errormsg.sig errormsg.sml @@ -75,6 +78,9 @@ shake.sig shake.sml +specialize.sig +specialize.sml + tag.sig tag.sml diff -r 9bbf4d383381 -r 8a70e2919e86 src/specialize.sig --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/specialize.sig Fri Aug 08 17:55:51 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 definitions *) + +signature SPECIALIZE = sig + + val specialize : Core.file -> Core.file + +end diff -r 9bbf4d383381 -r 8a70e2919e86 src/specialize.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/specialize.sml Fri Aug 08 17:55:51 2008 -0400 @@ -0,0 +1,276 @@ +(* 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 algebraically *) + +structure Specialize :> SPECIALIZE = struct + +open Core + +structure E = CoreEnv +structure U = CoreUtil + +val liftConInCon = E.liftConInCon +val subConInCon = E.subConInCon + +structure CK = struct +type ord_key = con list +val compare = Order.joinL U.Con.compare +end + +structure CM = BinaryMapFn(CK) +structure IM = IntBinaryMap + +type datatyp' = { + name : int, + constructors : int IM.map +} + +type datatyp = { + name : string, + params : int, + constructors : (string * int * con option) list, + specializations : datatyp' CM.map +} + +type state = { + count : int, + datatypes : datatyp IM.map, + constructors : int IM.map, + decls : decl list +} + +fun kind (k, st) = (k, st) + +val isOpen = U.Con.exists {kind = fn _ => false, + con = fn c => + case c of + CRel _ => true + | _ => false} + +fun considerSpecialization (st : state, n, args, dt : datatyp) = + case CM.find (#specializations dt, args) of + SOME dt' => (#name dt', #constructors dt', st) + | NONE => + let + val n' = #count st + + fun sub t = ListUtil.foldli (fn (i, arg, t) => + subConInCon (i, arg) t) t args + + val (cons, (count, cmap)) = + ListUtil.foldlMap (fn ((x, n, to), (count, cmap)) => + let + val to = Option.map sub to + in + ((x, count, to), + (count + 1, + IM.insert (cmap, n, count))) + end) (n' + 1, IM.empty) (#constructors dt) + + val st = {count = count, + datatypes = IM.insert (#datatypes st, n, + {name = #name dt, + params = #params dt, + constructors = #constructors dt, + specializations = CM.insert (#specializations dt, + args, + {name = n', + constructors = cmap})}), + constructors = #constructors st, + decls = #decls st} + + val (cons, st) = ListUtil.foldlMap (fn ((x, n, NONE), st) => ((x, n, NONE), st) + | ((x, n, SOME t), st) => + let + val (t, st) = specCon st t + in + ((x, n, SOME t), st) + end) st cons + + val d = (DDatatype (#name dt ^ "_s", + n', + [], + cons), #2 (List.hd args)) + in + (n', cmap, {count = #count st, + datatypes = #datatypes st, + constructors = #constructors st, + decls = d :: #decls st}) + end + +and con (c, st : state) = + let + fun findApp (c, args) = + case c of + CApp ((c', _), arg) => findApp (c', arg :: args) + | CNamed n => SOME (n, args) + | _ => NONE + in + case findApp (c, []) of + SOME (n, args as (_ :: _)) => + if List.exists isOpen args then + (c, st) + else + (case IM.find (#datatypes st, n) of + NONE => (c, st) + | SOME dt => + if length args <> #params dt then + (c, st) + else + let + val (n, _, st) = considerSpecialization (st, n, args, dt) + in + (CNamed n, st) + end) + | _ => (c, st) + end + +and specCon st = U.Con.foldMap {kind = kind, con = con} st + +fun pat (p, st) = + case #1 p of + PWild => (p, st) + | PVar _ => (p, st) + | PPrim _ => (p, st) + | PCon (dk, PConVar pn, args as (_ :: _), po) => + let + val (po, st) = + case po of + NONE => (NONE, st) + | SOME p => + let + val (p, st) = pat (p, st) + in + (SOME p, st) + end + val p = (PCon (dk, PConVar pn, args, po), #2 p) + in + if List.exists isOpen args then + (p, st) + else + case IM.find (#constructors st, pn) of + NONE => (p, st) + | SOME n => + case IM.find (#datatypes st, n) of + NONE => (p, st) + | SOME dt => + let + val (n, cmap, st) = considerSpecialization (st, n, args, dt) + in + case IM.find (cmap, pn) of + NONE => raise Fail "Specialize: Missing datatype constructor (pat)" + | SOME pn' => ((PCon (dk, PConVar pn', [], po), #2 p), st) + end + end + | PCon _ => (p, st) + | PRecord xps => + let + val (xps, st) = ListUtil.foldlMap (fn ((x, p, t), st) => + let + val (p, st) = pat (p, st) + in + ((x, p, t), st) + end) + st xps + in + ((PRecord xps, #2 p), st) + end + +fun exp (e, st) = + case e of + ECon (dk, PConVar pn, args as (_ :: _), eo) => + if List.exists isOpen args then + (e, st) + else + (case IM.find (#constructors st, pn) of + NONE => (e, st) + | SOME n => + case IM.find (#datatypes st, n) of + NONE => (e, st) + | SOME dt => + let + val (n, cmap, st) = considerSpecialization (st, n, args, dt) + in + case IM.find (cmap, pn) of + NONE => raise Fail "Specialize: Missing datatype constructor" + | SOME pn' => (ECon (dk, PConVar pn', [], eo), st) + end) + | ECase (e, pes, r) => + let + val (pes, st) = ListUtil.foldlMap (fn ((p, e), st) => + let + val (p, st) = pat (p, st) + in + ((p, e), st) + end) st pes + in + (ECase (e, pes, r), st) + end + | _ => (e, 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 (all as (d, _), st : state) = + case d of + DDatatype (x, n, xs, xnts) => + ([all], {count = #count st, + datatypes = IM.insert (#datatypes st, n, + {name = x, + params = length xs, + constructors = xnts, + specializations = CM.empty}), + constructors = foldl (fn ((_, n', _), constructors) => + IM.insert (constructors, n', n)) + (#constructors st) xnts, + decls = []}) + | _ => + let + val (d, st) = specDecl st all + in + (rev (d :: #decls st), + {count = #count st, + datatypes = #datatypes st, + constructors = #constructors st, + decls = []}) + end + + val (ds, _) = ListUtil.foldlMapConcat doDecl + {count = U.File.maxName file + 1, + datatypes = IM.empty, + constructors = IM.empty, + decls = []} file + in + ds + end + + +end diff -r 9bbf4d383381 -r 8a70e2919e86 tests/datatypeP.lac --- a/tests/datatypeP.lac Fri Aug 08 10:59:06 2008 -0400 +++ b/tests/datatypeP.lac Fri Aug 08 17:55:51 2008 -0400 @@ -8,3 +8,14 @@ val none_again = f none val some_1_again = f some_1 + +val show = fn t ::: Type => fn x : option t => case x of None => "None" | Some _ => "Some" + +val page = fn x => + {cdata (show x)} + + +val main : unit -> page = fn () => +
  • None
    • +
  • Some 1
    • +