adamc@193: (* Copyright (c) 2008, Adam Chlipala adamc@193: * All rights reserved. adamc@193: * adamc@193: * Redistribution and use in source and binary forms, with or without adamc@193: * modification, are permitted provided that the following conditions are met: adamc@193: * adamc@193: * - Redistributions of source code must retain the above copyright notice, adamc@193: * this list of conditions and the following disclaimer. adamc@193: * - Redistributions in binary form must reproduce the above copyright notice, adamc@193: * this list of conditions and the following disclaimer in the documentation adamc@193: * and/or other materials provided with the distribution. adamc@193: * - The names of contributors may not be used to endorse or promote products adamc@193: * derived from this software without specific prior written permission. adamc@193: * adamc@193: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@193: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@193: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@193: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@193: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@193: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@193: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@193: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@193: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@193: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@193: * POSSIBILITY OF SUCH DAMAGE. adamc@193: *) adamc@193: adamc@315: (* Simplify a Core program by repeating polymorphic definitions of datatypes *) adamc@193: adamc@193: structure Specialize :> SPECIALIZE = struct adamc@193: adamc@193: open Core adamc@193: adamc@193: structure E = CoreEnv adamc@193: structure U = CoreUtil adamc@193: adamc@193: val liftConInCon = E.liftConInCon adamc@193: val subConInCon = E.subConInCon adamc@193: adamc@193: structure CK = struct adamc@193: type ord_key = con list adamc@193: val compare = Order.joinL U.Con.compare adamc@193: end adamc@193: adamc@193: structure CM = BinaryMapFn(CK) adamc@193: structure IM = IntBinaryMap adamc@193: adamc@193: type datatyp' = { adamc@193: name : int, adamc@193: constructors : int IM.map adamc@193: } adamc@193: adamc@193: type datatyp = { adamc@193: name : string, adamc@193: params : int, adamc@193: constructors : (string * int * con option) list, adamc@193: specializations : datatyp' CM.map adamc@193: } adamc@193: adamc@193: type state = { adamc@193: count : int, adamc@193: datatypes : datatyp IM.map, adamc@193: constructors : int IM.map, adamc@315: decls : decl list adamc@193: } adamc@193: adamc@193: fun kind (k, st) = (k, st) adamc@193: adamc@193: val isOpen = U.Con.exists {kind = fn _ => false, adamc@193: con = fn c => adamc@193: case c of adamc@193: CRel _ => true adamc@193: | _ => false} adamc@193: adamc@193: fun considerSpecialization (st : state, n, args, dt : datatyp) = adamc@193: case CM.find (#specializations dt, args) of adamc@193: SOME dt' => (#name dt', #constructors dt', st) adamc@193: | NONE => adamc@193: let adamc@194: (*val () = Print.prefaces "Args" [("args", Print.p_list (CorePrint.p_con CoreEnv.empty) args)]*) adamc@194: adamc@193: val n' = #count st adamc@193: adamc@194: val nxs = length args - 1 adamc@193: fun sub t = ListUtil.foldli (fn (i, arg, t) => adamc@194: subConInCon (nxs - i, arg) t) t args adamc@193: adamc@193: val (cons, (count, cmap)) = adamc@193: ListUtil.foldlMap (fn ((x, n, to), (count, cmap)) => adamc@193: let adamc@193: val to = Option.map sub to adamc@193: in adamc@193: ((x, count, to), adamc@193: (count + 1, adamc@193: IM.insert (cmap, n, count))) adamc@193: end) (n' + 1, IM.empty) (#constructors dt) adamc@193: adamc@193: val st = {count = count, adamc@193: datatypes = IM.insert (#datatypes st, n, adamc@193: {name = #name dt, adamc@193: params = #params dt, adamc@193: constructors = #constructors dt, adamc@193: specializations = CM.insert (#specializations dt, adamc@193: args, adamc@193: {name = n', adamc@193: constructors = cmap})}), adamc@193: constructors = #constructors st, adamc@193: decls = #decls st} adamc@193: adamc@193: val (cons, st) = ListUtil.foldlMap (fn ((x, n, NONE), st) => ((x, n, NONE), st) adamc@193: | ((x, n, SOME t), st) => adamc@193: let adamc@193: val (t, st) = specCon st t adamc@193: in adamc@193: ((x, n, SOME t), st) adamc@193: end) st cons adamc@193: adamc@193: val d = (DDatatype (#name dt ^ "_s", adamc@193: n', adamc@193: [], adamc@193: cons), #2 (List.hd args)) adamc@193: in adamc@193: (n', cmap, {count = #count st, adamc@193: datatypes = #datatypes st, adamc@193: constructors = #constructors st, adamc@193: decls = d :: #decls st}) adamc@193: end adamc@193: adamc@193: and con (c, st : state) = adamc@193: let adamc@193: fun findApp (c, args) = adamc@193: case c of adamc@193: CApp ((c', _), arg) => findApp (c', arg :: args) adamc@193: | CNamed n => SOME (n, args) adamc@193: | _ => NONE adamc@193: in adamc@193: case findApp (c, []) of adamc@193: SOME (n, args as (_ :: _)) => adamc@193: if List.exists isOpen args then adamc@193: (c, st) adamc@193: else adamc@193: (case IM.find (#datatypes st, n) of adamc@193: NONE => (c, st) adamc@193: | SOME dt => adamc@193: if length args <> #params dt then adamc@193: (c, st) adamc@193: else adamc@193: let adamc@193: val (n, _, st) = considerSpecialization (st, n, args, dt) adamc@193: in adamc@193: (CNamed n, st) adamc@193: end) adamc@193: | _ => (c, st) adamc@193: end adamc@193: adamc@193: and specCon st = U.Con.foldMap {kind = kind, con = con} st adamc@193: adamc@193: fun pat (p, st) = adamc@193: case #1 p of adamc@193: PWild => (p, st) adamc@193: | PVar _ => (p, st) adamc@193: | PPrim _ => (p, st) adamc@193: | PCon (dk, PConVar pn, args as (_ :: _), po) => adamc@193: let adamc@193: val (po, st) = adamc@193: case po of adamc@193: NONE => (NONE, st) adamc@193: | SOME p => adamc@193: let adamc@193: val (p, st) = pat (p, st) adamc@193: in adamc@193: (SOME p, st) adamc@193: end adamc@193: val p = (PCon (dk, PConVar pn, args, po), #2 p) adamc@193: in adamc@193: if List.exists isOpen args then adamc@193: (p, st) adamc@193: else adamc@193: case IM.find (#constructors st, pn) of adamc@193: NONE => (p, st) adamc@193: | SOME n => adamc@193: case IM.find (#datatypes st, n) of adamc@193: NONE => (p, st) adamc@193: | SOME dt => adamc@193: let adamc@193: val (n, cmap, st) = considerSpecialization (st, n, args, dt) adamc@193: in adamc@193: case IM.find (cmap, pn) of adamc@193: NONE => raise Fail "Specialize: Missing datatype constructor (pat)" adamc@193: | SOME pn' => ((PCon (dk, PConVar pn', [], po), #2 p), st) adamc@193: end adamc@193: end adamc@193: | PCon _ => (p, st) adamc@193: | PRecord xps => adamc@193: let adamc@193: val (xps, st) = ListUtil.foldlMap (fn ((x, p, t), st) => adamc@193: let adamc@193: val (p, st) = pat (p, st) adamc@193: in adamc@193: ((x, p, t), st) adamc@193: end) adamc@193: st xps adamc@193: in adamc@193: ((PRecord xps, #2 p), st) adamc@193: end adamc@193: adamc@193: fun exp (e, st) = adamc@193: case e of adamc@193: ECon (dk, PConVar pn, args as (_ :: _), eo) => adamc@193: if List.exists isOpen args then adamc@193: (e, st) adamc@193: else adamc@193: (case IM.find (#constructors st, pn) of adamc@193: NONE => (e, st) adamc@193: | SOME n => adamc@193: case IM.find (#datatypes st, n) of adamc@193: NONE => (e, st) adamc@193: | SOME dt => adamc@193: let adamc@193: val (n, cmap, st) = considerSpecialization (st, n, args, dt) adamc@193: in adamc@193: case IM.find (cmap, pn) of adamc@193: NONE => raise Fail "Specialize: Missing datatype constructor" adamc@193: | SOME pn' => (ECon (dk, PConVar pn', [], eo), st) adamc@193: end) adamc@193: | ECase (e, pes, r) => adamc@193: let adamc@193: val (pes, st) = ListUtil.foldlMap (fn ((p, e), st) => adamc@193: let adamc@193: val (p, st) = pat (p, st) adamc@193: in adamc@193: ((p, e), st) adamc@193: end) st pes adamc@193: in adamc@193: (ECase (e, pes, r), st) adamc@193: end adamc@193: | _ => (e, st) adamc@193: adamc@193: fun decl (d, st) = (d, st) adamc@193: adamc@193: val specDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl} adamc@193: adamc@193: fun specialize file = adamc@193: let adamc@792: fun doDecl (d, st) = adamc@194: let adamc@194: (*val () = Print.preface ("decl:", CorePrint.p_decl CoreEnv.empty all)*) adamc@792: val (d, st) = specDecl st d adamc@194: in adamc@792: case #1 d of adamc@194: DDatatype (x, n, xs, xnts) => adamc@792: (rev (d :: #decls st), adamc@792: {count = #count st, adamc@792: datatypes = IM.insert (#datatypes st, n, adamc@792: {name = x, adamc@792: params = length xs, adamc@792: constructors = xnts, adamc@792: specializations = CM.empty}), adamc@792: constructors = foldl (fn ((_, n', _), constructors) => adamc@792: IM.insert (constructors, n', n)) adamc@792: (#constructors st) xnts, adamc@792: decls = []}) adamc@194: | _ => adamc@792: (rev (d :: #decls st), adamc@792: {count = #count st, adamc@792: datatypes = #datatypes st, adamc@792: constructors = #constructors st, adamc@792: decls = []}) adamc@194: end adamc@193: adamc@193: val (ds, _) = ListUtil.foldlMapConcat doDecl adamc@193: {count = U.File.maxName file + 1, adamc@193: datatypes = IM.empty, adamc@193: constructors = IM.empty, adamc@193: decls = []} file adamc@193: in adamc@193: ds adamc@193: end adamc@193: adamc@193: adamc@193: end