adamc@1185: (* Copyright (c) 2008-2010, Adam Chlipala adamc@315: * All rights reserved. adamc@315: * adamc@315: * Redistribution and use in source and binary forms, with or without adamc@315: * modification, are permitted provided that the following conditions are met: adamc@315: * adamc@315: * - Redistributions of source code must retain the above copyright notice, adamc@315: * this list of conditions and the following disclaimer. adamc@315: * - Redistributions in binary form must reproduce the above copyright notice, adamc@315: * this list of conditions and the following disclaimer in the documentation adamc@315: * and/or other materials provided with the distribution. adamc@315: * - The names of contributors may not be used to endorse or promote products adamc@315: * derived from this software without specific prior written permission. adamc@315: * adamc@315: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@315: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@315: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@315: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@315: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@315: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@315: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@315: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@315: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@315: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@315: * POSSIBILITY OF SUCH DAMAGE. adamc@315: *) adamc@315: adamc@315: (* Simplify a Core program by repeating polymorphic function definitions *) adamc@315: adamc@315: structure Unpoly :> UNPOLY = struct adamc@315: adamc@315: open Core adamc@315: adamc@315: structure E = CoreEnv adamc@315: structure U = CoreUtil adamc@315: adamc@315: structure IS = IntBinarySet adamc@315: structure IM = IntBinaryMap adamc@315: adamc@315: adamc@315: (** The actual specialization *) adamc@315: adamc@315: val liftConInCon = E.liftConInCon adamc@315: val subConInCon = E.subConInCon adamc@315: adamc@315: val liftConInExp = E.liftConInExp adamc@315: val subConInExp = E.subConInExp adamc@315: adamc@1185: val isOpen = U.Con.existsB {kind = fn _ => false, adamc@1185: con = fn (n, c) => adamc@1185: case c of adamc@1185: CRel n' => n' >= n adamc@1185: | _ => false, adamc@1185: bind = fn (n, b) => adamc@1185: case b of adamc@1185: U.Con.RelC _ => n + 1 adamc@1185: | _ => n} 0 adamc@399: adamc@316: fun unpolyNamed (xn, rep) = adamc@316: U.Exp.map {kind = fn k => k, adamc@316: con = fn c => c, adamc@316: exp = fn e => adamc@316: case e of adamc@399: ECApp (e', _) => adamc@325: let adamc@325: fun isTheOne (e, _) = adamc@325: case e of adamc@325: ENamed xn' => xn' = xn adamc@325: | ECApp (e, _) => isTheOne e adamc@325: | _ => false adamc@325: in adamc@325: if isTheOne e' then adamc@399: rep adamc@325: else adamc@325: e adamc@325: end adamc@316: | _ => e} adamc@316: adamc@794: structure M = BinaryMapFn(struct adamc@794: type ord_key = con list adamc@794: val compare = Order.joinL U.Con.compare adamc@794: end) adamc@794: adamc@794: type func = { adamc@794: kinds : kind list, adamc@794: defs : (string * int * con * exp * string) list, adamc@794: replacements : int M.map adamc@794: } adamc@794: adamc@315: type state = { adamc@794: funcs : func IM.map, adamc@315: decls : decl list, adamc@315: nextName : int adamc@315: } adamc@315: adamc@315: fun kind (k, st) = (k, st) adamc@315: adamc@315: fun con (c, st) = (c, st) adamc@315: adamc@315: fun exp (e, st : state) = adamc@315: case e of adamc@315: ECApp _ => adamc@315: let adamc@315: fun unravel (e, cargs) = adamc@315: case e of adamc@315: ECApp ((e, _), c) => unravel (e, c :: cargs) adamc@315: | ENamed n => SOME (n, rev cargs) adamc@315: | _ => NONE adamc@315: in adamc@315: case unravel (e, []) of adamc@315: NONE => (e, st) adamc@315: | SOME (n, cargs) => adamc@399: if List.exists isOpen cargs then adamc@399: (e, st) adamc@399: else adamc@399: case IM.find (#funcs st, n) of adamc@399: NONE => (e, st) adamc@794: | SOME {kinds = ks, defs = vis, replacements} => adamc@794: case M.find (replacements, cargs) of adamc@794: SOME n => (ENamed n, st) adamc@794: | NONE => adamc@794: let adamc@794: val old_vis = vis adamc@794: val (vis, (thisName, nextName)) = adamc@794: ListUtil.foldlMap adamc@794: (fn ((x, n', t, e, s), (thisName, nextName)) => adamc@794: ((x, nextName, n', t, e, s), adamc@794: (if n' = n then nextName else thisName, adamc@794: nextName + 1))) adamc@794: (0, #nextName st) vis adamc@315: adamc@794: fun specialize (x, n, n_old, t, e, s) = adamc@794: let adamc@794: fun trim (t, e, cargs) = adamc@794: case (t, e, cargs) of adamc@794: ((TCFun (_, _, t), _), adamc@794: (ECAbs (_, _, e), _), adamc@794: carg :: cargs) => adamc@794: let adamc@794: val t = subConInCon (length cargs, carg) t adamc@794: val e = subConInExp (length cargs, carg) e adamc@794: in adamc@794: trim (t, e, cargs) adamc@794: end adamc@796: | (_, _, []) => SOME (t, e) adamc@794: | _ => NONE adamc@794: in adamc@794: (*Print.prefaces "specialize" adamc@1185: [("n", Print.PD.string (Int.toString n)), adamc@1185: ("nold", Print.PD.string (Int.toString n_old)), adamc@1185: ("t", CorePrint.p_con CoreEnv.empty t), adamc@1185: ("e", CorePrint.p_exp CoreEnv.empty e), adamc@1185: ("|cargs|", Print.PD.string (Int.toString (length cargs)))];*) adamc@794: Option.map (fn (t, e) => (x, n, n_old, t, e, s)) adamc@794: (trim (t, e, cargs)) adamc@794: end adamc@315: adamc@794: val vis = List.map specialize vis adamc@794: in adamc@794: if List.exists (not o Option.isSome) vis orelse length cargs > length ks then adamc@794: (e, st) adamc@794: else adamc@794: let adamc@794: val vis = List.mapPartial (fn x => x) vis adamc@316: adamc@794: val vis = map (fn (x, n, n_old, t, e, s) => adamc@794: (x ^ "_unpoly", n, n_old, t, e, s)) vis adamc@794: val vis' = map (fn (x, n, _, t, e, s) => adamc@794: (x, n, t, e, s)) vis adamc@794: adamc@1016: val funcs = foldl (fn ((_, n, n_old, _, _, _), funcs) => adamc@1016: let adamc@1016: val replacements = case IM.find (funcs, n_old) of adamc@1016: NONE => M.empty adamc@1016: | SOME {replacements = r, ...} => r adamc@1016: in adamc@1016: IM.insert (funcs, n_old, adamc@1016: {kinds = ks, adamc@1016: defs = old_vis, adamc@1016: replacements = M.insert (replacements, adamc@1016: cargs, adamc@1016: n)}) adamc@1016: end) (#funcs st) vis adamc@794: adamc@794: val ks' = List.drop (ks, length cargs) adamc@794: adamc@794: val st = {funcs = foldl (fn (vi, funcs) => adamc@794: IM.insert (funcs, #2 vi, adamc@794: {kinds = ks', adamc@794: defs = vis', adamc@794: replacements = M.empty})) adamc@794: funcs vis', adamc@794: decls = #decls st, adamc@794: nextName = nextName} adamc@794: adamc@794: val (vis', st) = ListUtil.foldlMap (fn ((x, n, t, e, s), st) => adamc@794: let adamc@794: val (e, st) = polyExp (e, st) adamc@794: in adamc@794: ((x, n, t, e, s), st) adamc@794: end) adamc@794: st vis' adamc@794: in adamc@794: (ENamed thisName, adamc@794: {funcs = #funcs st, adamc@399: decls = (DValRec vis', ErrorMsg.dummySpan) :: #decls st, adamc@794: nextName = #nextName st}) adamc@794: end adamc@794: end adamc@315: end adamc@315: | _ => (e, st) adamc@315: adamc@794: and polyExp (x, st) = U.Exp.foldMap {kind = kind, con = con, exp = exp} st x adamc@794: adamc@315: fun decl (d, st : state) = adamc@1122: let adamc@1122: fun unravel (e, cargs) = adamc@1122: case e of adamc@1122: (ECAbs (_, k, e), _) => adamc@1122: unravel (e, k :: cargs) adamc@1122: | _ => rev cargs adamc@1122: in adamc@1122: case d of adamc@1122: DVal (vi as (x, n, t, e, s)) => adamc@1122: let adamc@1122: val cargs = unravel (e, []) adamc@315: adamc@1122: val ns = IS.singleton n adamc@1122: in adamc@1122: (d, {funcs = IM.insert (#funcs st, n, {kinds = cargs, adamc@1122: defs = [vi], adamc@1122: replacements = M.empty}), adamc@1122: decls = #decls st, adamc@1122: nextName = #nextName st}) adamc@1122: end adamc@1122: | DValRec (vis as ((x, n, t, e, s) :: rest)) => adamc@1122: let adamc@1122: val cargs = unravel (e, []) adamc@315: adamc@1122: fun unravel (e, cargs) = adamc@1122: case (e, cargs) of adamc@1122: ((ECAbs (_, k, e), _), k' :: cargs) => adamc@1122: U.Kind.compare (k, k') = EQUAL adamc@1122: andalso unravel (e, cargs) adamc@1122: | (_, []) => true adamc@1122: | _ => false adamc@1122: adamc@1122: fun deAbs (e, cargs) = adamc@1122: case (e, cargs) of adamc@1122: ((ECAbs (_, _, e), _), _ :: cargs) => deAbs (e, cargs) adamc@1122: | (_, []) => e adamc@1122: | _ => raise Fail "Unpoly: deAbs" adamc@315: adamc@1122: in adamc@1122: if List.exists (fn vi => not (unravel (#4 vi, cargs))) rest then adamc@1122: (d, st) adamc@1122: else adamc@1122: let adamc@1122: val ns = IS.addList (IS.empty, map #2 vis) adamc@1122: val nargs = length cargs adamc@315: adamc@1122: (** Verifying lack of polymorphic recursion *) adamc@315: adamc@1122: fun kind _ = false adamc@1122: fun con _ = false adamc@315: adamc@1180: fun exp (cn, e) = adamc@1122: case e of adamc@1180: orig as ECApp (e, c) => adamc@1122: let adamc@1122: fun isIrregular (e, pos) = adamc@1122: case #1 e of adamc@1122: ENamed n => adamc@1122: IS.member (ns, n) adamc@1122: andalso adamc@1122: (case #1 c of adamc@1180: CRel i => i <> nargs - pos + cn adamc@1122: | _ => true) adamc@1122: | ECApp (e, _) => isIrregular (e, pos + 1) adamc@1122: | _ => false adamc@1122: in adamc@1122: isIrregular (e, 1) adamc@1122: end adamc@1122: | _ => false adamc@315: adamc@1180: fun bind (cn, b) = adamc@1180: case b of adamc@1180: U.Exp.RelC _ => cn+1 adamc@1180: | _ => cn adamc@1180: adamc@1180: val irregular = U.Exp.existsB {kind = kind, con = con, exp = exp, bind = bind} 0 adamc@1122: in adamc@1122: if List.exists (fn x => irregular (deAbs (#4 x, cargs))) vis then adamc@1185: (d, st) adamc@1122: else adamc@1122: (d, {funcs = foldl (fn (vi, funcs) => adamc@1122: IM.insert (funcs, #2 vi, {kinds = cargs, adamc@1122: defs = vis, adamc@1122: replacements = M.empty})) adamc@1122: (#funcs st) vis, adamc@1122: decls = #decls st, adamc@1122: nextName = #nextName st}) adamc@1122: end adamc@1122: end adamc@315: adamc@1122: | _ => (d, st) adamc@1122: end adamc@315: adamc@315: val polyDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl} adamc@315: adamc@315: fun unpoly file = adamc@315: let adamc@315: fun doDecl (d : decl, st : state) = adamc@315: let adamc@315: val (d, st) = polyDecl st d adamc@315: in adamc@315: (rev (d :: #decls st), adamc@315: {funcs = #funcs st, adamc@315: decls = [], adamc@315: nextName = #nextName st}) adamc@315: end adamc@315: adamc@315: val (ds, _) = ListUtil.foldlMapConcat doDecl adamc@315: {funcs = IM.empty, adamc@315: decls = [], adamc@315: nextName = U.File.maxName file + 1} file adamc@315: in adamc@315: ds adamc@315: end adamc@315: adamc@315: end