adamc@16: (* Copyright (c) 2008, Adam Chlipala adamc@16: * All rights reserved. adamc@16: * adamc@16: * Redistribution and use in source and binary forms, with or without adamc@16: * modification, are permitted provided that the following conditions are met: adamc@16: * adamc@16: * - Redistributions of source code must retain the above copyright notice, adamc@16: * this list of conditions and the following disclaimer. adamc@16: * - Redistributions in binary form must reproduce the above copyright notice, adamc@16: * this list of conditions and the following disclaimer in the documentation adamc@16: * and/or other materials provided with the distribution. adamc@16: * - The names of contributors may not be used to endorse or promote products adamc@16: * derived from this software without specific prior written permission. adamc@16: * adamc@16: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@16: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@16: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@16: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@16: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@16: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@16: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@16: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@16: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@16: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@16: * POSSIBILITY OF SUCH DAMAGE. adamc@16: *) adamc@16: adamc@16: structure Corify :> CORIFY = struct adamc@16: adamc@16: structure EM = ErrorMsg adamc@39: structure L = Expl adamc@16: structure L' = Core adamc@16: adamc@39: structure IM = IntBinaryMap adamc@39: structure SM = BinaryMapFn(struct adamc@39: type ord_key = string adamc@39: val compare = String.compare adamc@39: end) adamc@39: adamc@39: local adamc@39: val count = ref 0 adamc@39: in adamc@39: adamc@39: fun reset v = count := v adamc@39: adamc@39: fun alloc () = adamc@39: let adamc@39: val r = !count adamc@39: in adamc@39: count := r + 1; adamc@39: r adamc@39: end adamc@39: adamc@39: end adamc@39: adamc@39: structure St : sig adamc@39: type t adamc@39: adamc@39: val empty : t adamc@39: adamc@39: val enter : t -> t adamc@39: val leave : t -> {outer : t, inner : t} adamc@39: adamc@39: val bindCore : t -> string -> int -> t * int adamc@39: val lookupCoreById : t -> int -> int option adamc@39: val lookupCoreByName : t -> string -> int adamc@39: adamc@39: val bindStr : t -> string -> int -> t -> t adamc@39: val lookupStrById : t -> int -> t adamc@39: val lookupStrByName : string * t -> t adamc@39: end = struct adamc@39: adamc@39: datatype flattening = F of { adamc@39: core : int SM.map, adamc@39: strs : flattening SM.map adamc@39: } adamc@39: adamc@39: type t = { adamc@39: core : int IM.map, adamc@39: strs : flattening IM.map, adamc@39: current : flattening, adamc@39: nested : flattening list adamc@39: } adamc@39: adamc@39: val empty = { adamc@39: core = IM.empty, adamc@39: strs = IM.empty, adamc@39: current = F { core = SM.empty, strs = SM.empty }, adamc@39: nested = [] adamc@39: } adamc@39: adamc@39: fun bindCore {core, strs, current, nested} s n = adamc@39: let adamc@39: val n' = alloc () adamc@39: adamc@39: val current = adamc@39: let adamc@39: val F {core, strs} = current adamc@39: in adamc@39: F {core = SM.insert (core, s, n'), adamc@39: strs = strs} adamc@39: end adamc@39: in adamc@39: ({core = IM.insert (core, n, n'), adamc@39: strs = strs, adamc@39: current = current, adamc@39: nested = nested}, adamc@39: n') adamc@39: end adamc@39: adamc@39: fun lookupCoreById ({core, ...} : t) n = IM.find (core, n) adamc@39: adamc@39: fun lookupCoreByName ({current = F {core, ...}, ...} : t) x = adamc@39: case SM.find (core, x) of adamc@39: NONE => raise Fail "Corify.St.lookupCoreByName" adamc@39: | SOME n => n adamc@39: adamc@39: fun enter {core, strs, current, nested} = adamc@39: {core = core, adamc@39: strs = strs, adamc@39: current = F {core = SM.empty, adamc@39: strs = SM.empty}, adamc@39: nested = current :: nested} adamc@39: adamc@39: fun dummy f = {core = IM.empty, adamc@39: strs = IM.empty, adamc@39: current = f, adamc@39: nested = []} adamc@39: adamc@39: fun leave {core, strs, current, nested = m1 :: rest} = adamc@39: {outer = {core = core, adamc@39: strs = strs, adamc@39: current = m1, adamc@39: nested = rest}, adamc@39: inner = dummy current} adamc@39: | leave _ = raise Fail "Corify.St.leave" adamc@39: adamc@39: fun bindStr ({core, strs, current = F {core = mcore, strs = mstrs}, nested} : t) x n ({current = f, ...} : t) = adamc@39: {core = core, adamc@39: strs = IM.insert (strs, n, f), adamc@39: current = F {core = mcore, adamc@39: strs = SM.insert (mstrs, x, f)}, adamc@39: nested = nested} adamc@39: adamc@39: fun lookupStrById ({strs, ...} : t) n = adamc@39: case IM.find (strs, n) of adamc@39: NONE => raise Fail "Corify.St.lookupStr" adamc@39: | SOME f => dummy f adamc@39: adamc@39: fun lookupStrByName (m, {current = F {strs, ...}, ...} : t) = adamc@39: case SM.find (strs, m) of adamc@39: NONE => raise Fail "Corify.St.lookupStrByName" adamc@39: | SOME f => dummy f adamc@39: adamc@39: end adamc@39: adamc@39: adamc@16: fun corifyKind (k, loc) = adamc@16: case k of adamc@16: L.KType => (L'.KType, loc) adamc@16: | L.KArrow (k1, k2) => (L'.KArrow (corifyKind k1, corifyKind k2), loc) adamc@16: | L.KName => (L'.KName, loc) adamc@16: | L.KRecord k => (L'.KRecord (corifyKind k), loc) adamc@16: adamc@39: fun corifyCon st (c, loc) = adamc@16: case c of adamc@39: L.TFun (t1, t2) => (L'.TFun (corifyCon st t1, corifyCon st t2), loc) adamc@39: | L.TCFun (x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon st t), loc) adamc@39: | L.TRecord c => (L'.TRecord (corifyCon st c), loc) adamc@16: adamc@16: | L.CRel n => (L'.CRel n, loc) adamc@39: | L.CNamed n => adamc@39: (case St.lookupCoreById st n of adamc@39: NONE => (L'.CNamed n, loc) adamc@39: | SOME n => (L'.CNamed n, loc)) adamc@39: | L.CModProj (m, ms, x) => adamc@39: let adamc@39: val st = St.lookupStrById st m adamc@39: val st = foldl St.lookupStrByName st ms adamc@39: val n = St.lookupCoreByName st x adamc@39: in adamc@39: (L'.CNamed n, loc) adamc@39: end adamc@34: adamc@39: | L.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc) adamc@39: | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon st c), loc) adamc@16: adamc@16: | L.CName s => (L'.CName s, loc) adamc@16: adamc@39: | L.CRecord (k, xcs) => adamc@39: (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc) adamc@39: | L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc) adamc@16: adamc@39: fun corifyExp st (e, loc) = adamc@16: case e of adamc@16: L.EPrim p => (L'.EPrim p, loc) adamc@16: | L.ERel n => (L'.ERel n, loc) adamc@39: | L.ENamed n => adamc@39: (case St.lookupCoreById st n of adamc@39: NONE => (L'.ENamed n, loc) adamc@39: | SOME n => (L'.ENamed n, loc)) adamc@39: | L.EModProj (m, ms, x) => adamc@39: let adamc@39: val st = St.lookupStrById st m adamc@39: val st = foldl St.lookupStrByName st ms adamc@39: val n = St.lookupCoreByName st x adamc@39: in adamc@39: (L'.ENamed n, loc) adamc@39: end adamc@39: | L.EApp (e1, e2) => (L'.EApp (corifyExp st e1, corifyExp st e2), loc) adamc@39: | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon st dom, corifyCon st ran, corifyExp st e1), loc) adamc@39: | L.ECApp (e1, c) => (L'.ECApp (corifyExp st e1, corifyCon st c), loc) adamc@39: | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc) adamc@16: adamc@39: | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) => (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc) adamc@39: | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c, adamc@39: {field = corifyCon st field, rest = corifyCon st rest}), loc) adamc@16: adamc@39: fun corifyDecl ((d, loc : EM.span), st) = adamc@39: case d of adamc@39: L.DCon (x, n, k, c) => adamc@39: let adamc@39: val (st, n) = St.bindCore st x n adamc@39: in adamc@39: ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st) adamc@39: end adamc@39: | L.DVal (x, n, t, e) => adamc@39: let adamc@39: val (st, n) = St.bindCore st x n adamc@39: in adamc@39: ([(L'.DVal (x, n, corifyCon st t, corifyExp st e), loc)], st) adamc@39: end adamc@39: adamc@39: | L.DSgn _ => ([], st) adamc@16: adamc@39: | L.DStr (x, n, _, str) => adamc@39: let adamc@39: val (ds, {inner, outer}) = corifyStr (str, st) adamc@39: val st = St.bindStr outer x n inner adamc@39: in adamc@39: (ds, st) adamc@39: end adamc@16: adamc@39: and corifyStr ((str, _), st) = adamc@39: case str of adamc@39: L.StrConst ds => adamc@39: let adamc@39: val st = St.enter st adamc@39: val (ds, st) = ListUtil.foldlMapConcat corifyDecl st ds adamc@39: in adamc@39: (ds, St.leave st) adamc@39: end adamc@39: | L.StrVar n => ([], {inner = St.lookupStrById st n, outer = st}) adamc@39: | L.StrProj (str, x) => adamc@39: let adamc@39: val (ds, {inner, outer}) = corifyStr (str, st) adamc@39: in adamc@39: (ds, {inner = St.lookupStrByName (x, inner), outer = outer}) adamc@39: end adamc@45: | L.StrFun _ => raise Fail "Corify functor" adamc@45: | L.StrApp _ => raise Fail "Corify functor app" adamc@31: adamc@39: fun maxName ds = foldl (fn ((d, _), n) => adamc@39: case d of adamc@39: L.DCon (_, n', _, _) => Int.max (n, n') adamc@39: | L.DVal (_, n', _ , _) => Int.max (n, n') adamc@39: | L.DSgn (_, n', _) => Int.max (n, n') adamc@39: | L.DStr (_, n', _, str) => Int.max (n, Int.max (n', maxNameStr str))) adamc@39: 0 ds adamc@39: adamc@39: and maxNameStr (str, _) = adamc@39: case str of adamc@39: L.StrConst ds => maxName ds adamc@39: | L.StrVar n => n adamc@39: | L.StrProj (str, _) => maxNameStr str adamc@45: | L.StrFun (_, _, _, _, str) => maxNameStr str adamc@45: | L.StrApp (str1, str2) => Int.max (maxNameStr str1, maxNameStr str2) adamc@39: adamc@39: fun corify ds = adamc@39: let adamc@39: val () = reset (maxName ds + 1) adamc@39: val (ds, _) = ListUtil.foldlMapConcat corifyDecl St.empty ds adamc@39: in adamc@39: ds adamc@39: end adamc@16: adamc@16: end