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@49: val ffi : string -> L'.con SM.map -> t adamc@39: adamc@73: datatype core_con = adamc@73: CNormal of int adamc@73: | CFfi of string adamc@73: val bindCon : t -> string -> int -> t * int adamc@73: val lookupConById : t -> int -> int option adamc@73: val lookupConByName : t -> string -> core_con adamc@48: adamc@73: datatype core_val = adamc@73: ENormal of int adamc@73: | EFfi of string * L'.con adamc@73: val bindVal : t -> string -> int -> t * int adamc@73: val lookupValById : t -> int -> int option adamc@73: val lookupValByName : t -> string -> core_val 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@46: adamc@46: val bindFunctor : t -> string -> int -> int -> L.str -> t adamc@46: val lookupFunctorById : t -> int -> int * L.str adamc@46: val lookupFunctorByName : string * t -> int * L.str adamc@39: end = struct adamc@39: adamc@48: datatype flattening = adamc@73: FNormal of {cons : int SM.map, adamc@73: vals : int SM.map, adamc@48: strs : flattening SM.map, adamc@48: funs : (int * L.str) SM.map} adamc@73: | FFfi of {mod : string, adamc@73: vals : L'.con SM.map} adamc@39: adamc@39: type t = { adamc@73: cons : int IM.map, adamc@73: vals : int IM.map, adamc@39: strs : flattening IM.map, adamc@46: funs : (int * L.str) IM.map, adamc@39: current : flattening, adamc@39: nested : flattening list adamc@39: } adamc@39: adamc@39: val empty = { adamc@73: cons = IM.empty, adamc@73: vals = IM.empty, adamc@39: strs = IM.empty, adamc@46: funs = IM.empty, adamc@73: current = FNormal { cons = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty }, adamc@39: nested = [] adamc@39: } adamc@39: adamc@73: datatype core_con = adamc@73: CNormal of int adamc@73: | CFfi of string adamc@48: adamc@73: datatype core_val = adamc@73: ENormal of int adamc@73: | EFfi of string * L'.con adamc@73: adamc@73: fun bindCon {cons, vals, strs, funs, current, nested} s n = adamc@39: let adamc@39: val n' = alloc () adamc@39: adamc@39: val current = adamc@48: case current of adamc@48: FFfi _ => raise Fail "Binding inside FFfi" adamc@73: | FNormal {cons, vals, strs, funs} => adamc@73: FNormal {cons = SM.insert (cons, s, n'), adamc@73: vals = vals, adamc@48: strs = strs, adamc@48: funs = funs} adamc@39: in adamc@73: ({cons = IM.insert (cons, n, n'), adamc@73: vals = vals, adamc@39: strs = strs, adamc@46: funs = funs, adamc@39: current = current, adamc@39: nested = nested}, adamc@39: n') adamc@39: end adamc@39: adamc@73: fun lookupConById ({cons, ...} : t) n = IM.find (cons, n) adamc@39: adamc@73: fun lookupConByName ({current, ...} : t) x = adamc@48: case current of adamc@73: FFfi {mod = m, ...} => CFfi m adamc@73: | FNormal {cons, ...} => adamc@73: case SM.find (cons, x) of adamc@73: NONE => raise Fail "Corify.St.lookupConByName" adamc@73: | SOME n => CNormal n adamc@39: adamc@73: fun bindVal {cons, vals, strs, funs, current, nested} s n = adamc@73: let adamc@73: val n' = alloc () adamc@73: adamc@73: val current = adamc@73: case current of adamc@73: FFfi _ => raise Fail "Binding inside FFfi" adamc@73: | FNormal {cons, vals, strs, funs} => adamc@73: FNormal {cons = cons, adamc@73: vals = SM.insert (vals, s, n'), adamc@73: strs = strs, adamc@73: funs = funs} adamc@73: in adamc@73: ({cons = cons, adamc@73: vals = IM.insert (vals, n, n'), adamc@73: strs = strs, adamc@73: funs = funs, adamc@73: current = current, adamc@73: nested = nested}, adamc@73: n') adamc@73: end adamc@73: adamc@73: fun lookupValById ({vals, ...} : t) n = IM.find (vals, n) adamc@73: adamc@73: fun lookupValByName ({current, ...} : t) x = adamc@73: case current of adamc@73: FFfi {mod = m, vals, ...} => adamc@73: (case SM.find (vals, x) of adamc@73: NONE => raise Fail "Corify.St.lookupValByName: no type for FFI val" adamc@73: | SOME t => EFfi (m, t)) adamc@73: | FNormal {vals, ...} => adamc@73: case SM.find (vals, x) of adamc@73: NONE => raise Fail "Corify.St.lookupValByName" adamc@73: | SOME n => ENormal n adamc@73: adamc@73: fun enter {cons, vals, strs, funs, current, nested} = adamc@73: {cons = cons, adamc@73: vals = vals, adamc@39: strs = strs, adamc@46: funs = funs, adamc@73: current = FNormal {cons = SM.empty, adamc@73: vals = SM.empty, adamc@48: strs = SM.empty, adamc@48: funs = SM.empty}, adamc@39: nested = current :: nested} adamc@39: adamc@73: fun dummy f = {cons = IM.empty, adamc@73: vals = IM.empty, adamc@39: strs = IM.empty, adamc@46: funs = IM.empty, adamc@39: current = f, adamc@39: nested = []} adamc@39: adamc@73: fun leave {cons, vals, strs, funs, current, nested = m1 :: rest} = adamc@73: {outer = {cons = cons, adamc@73: vals = vals, adamc@39: strs = strs, adamc@46: funs = funs, adamc@39: current = m1, adamc@39: nested = rest}, adamc@39: inner = dummy current} adamc@39: | leave _ = raise Fail "Corify.St.leave" adamc@39: adamc@73: fun ffi m vals = dummy (FFfi {mod = m, vals = vals}) adamc@48: adamc@73: fun bindStr ({cons, vals, strs, funs, adamc@73: current = FNormal {cons = mcons, vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) adamc@46: x n ({current = f, ...} : t) = adamc@73: {cons = cons, adamc@73: vals = vals, adamc@39: strs = IM.insert (strs, n, f), adamc@46: funs = funs, adamc@73: current = FNormal {cons = mcons, adamc@73: vals = mvals, adamc@73: strs = SM.insert (mstrs, x, f), adamc@73: funs = mfuns}, adamc@39: nested = nested} adamc@48: | bindStr _ _ _ _ = raise Fail "Corify.St.bindStr" adamc@39: adamc@39: fun lookupStrById ({strs, ...} : t) n = adamc@39: case IM.find (strs, n) of adamc@46: NONE => raise Fail "Corify.St.lookupStrById" adamc@39: | SOME f => dummy f adamc@39: adamc@48: fun lookupStrByName (m, {current = FNormal {strs, ...}, ...} : t) = adamc@48: (case SM.find (strs, m) of adamc@48: NONE => raise Fail "Corify.St.lookupStrByName" adamc@48: | SOME f => dummy f) adamc@48: | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName" adamc@39: adamc@73: fun bindFunctor ({cons, vals, strs, funs, adamc@73: current = FNormal {cons = mcons, vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) adamc@46: x n na str = adamc@73: {cons = cons, adamc@73: vals = vals, adamc@46: strs = strs, adamc@46: funs = IM.insert (funs, n, (na, str)), adamc@73: current = FNormal {cons = mcons, adamc@73: vals = mvals, adamc@48: strs = mstrs, adamc@48: funs = SM.insert (mfuns, x, (na, str))}, adamc@46: nested = nested} adamc@48: | bindFunctor _ _ _ _ _ = raise Fail "Corify.St.bindFunctor" adamc@46: adamc@46: fun lookupFunctorById ({funs, ...} : t) n = adamc@46: case IM.find (funs, n) of adamc@46: NONE => raise Fail "Corify.St.lookupFunctorById" adamc@46: | SOME v => v adamc@46: adamc@48: fun lookupFunctorByName (m, {current = FNormal {funs, ...}, ...} : t) = adamc@48: (case SM.find (funs, m) of adamc@48: NONE => raise Fail "Corify.St.lookupFunctorByName" adamc@48: | SOME v => v) adamc@48: | lookupFunctorByName _ = raise Fail "Corify.St.lookupFunctorByName" adamc@46: 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@87: | L.KUnit => (L'.KUnit, 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@73: (case St.lookupConById 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: in adamc@73: case St.lookupConByName st x of adamc@73: St.CNormal n => (L'.CNamed n, loc) adamc@73: | St.CFfi m => (L'.CFfi (m, x), 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@69: | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc) adamc@87: | L.CUnit => (L'.CUnit, 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@73: (case St.lookupValById 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: in adamc@73: case St.lookupValByName st x of adamc@73: St.ENormal n => (L'.ENamed n, loc) adamc@73: | St.EFfi (m, t) => adamc@49: case t of adamc@50: (L'.TFun (dom as (L'.TRecord (L'.CRecord (_, []), _), _), ran), _) => adamc@50: (L'.EAbs ("arg", dom, ran, (L'.EFfiApp (m, x, []), loc)), loc) adamc@50: | t as (L'.TFun _, _) => adamc@49: let adamc@49: fun getArgs (all as (t, _), args) = adamc@49: case t of adamc@49: L'.TFun (dom, ran) => getArgs (ran, dom :: args) adamc@49: | _ => (all, rev args) adamc@49: adamc@49: val (result, args) = getArgs (t, []) adamc@49: adamc@50: val (actuals, _) = foldr (fn (_, (actuals, n)) => adamc@50: ((L'.ERel n, loc) :: actuals, adamc@50: n + 1)) ([], 0) args adamc@50: val app = (L'.EFfiApp (m, x, actuals), loc) adamc@49: val (abs, _, _) = foldr (fn (t, (abs, ran, n)) => adamc@49: ((L'.EAbs ("arg" ^ Int.toString n, adamc@49: t, adamc@49: ran, adamc@49: abs), loc), adamc@49: (L'.TFun (t, ran), loc), adamc@49: n - 1)) (app, result, length args - 1) args adamc@49: in adamc@49: abs adamc@49: end adamc@49: | _ => (L'.EFfi (m, x), 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@73: | L.EFold k => (L'.EFold (corifyKind k), 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@73: val (st, n) = St.bindCon 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@73: val (st, n) = St.bindVal 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@46: | L.DStr (x, n, _, (L.StrFun (_, na, _, _, str), _)) => adamc@46: ([], St.bindFunctor st x n na str) adamc@46: 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@49: | L.DFfiStr (m, n, (sgn, _)) => adamc@49: (case sgn of adamc@49: L.SgnConst sgis => adamc@49: let adamc@49: val (ds, cmap, st) = adamc@49: foldl (fn ((sgi, _), (ds, cmap, st)) => adamc@49: case sgi of adamc@49: L.SgiConAbs (x, n, k) => adamc@49: let adamc@73: val (st, n') = St.bindCon st x n adamc@49: in adamc@49: ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, adamc@49: cmap, adamc@49: st) adamc@49: end adamc@49: | L.SgiCon (x, n, k, _) => adamc@49: let adamc@73: val (st, n') = St.bindCon st x n adamc@49: in adamc@49: ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, adamc@49: cmap, adamc@49: st) adamc@49: end adamc@49: adamc@49: | L.SgiVal (x, _, c) => adamc@49: (ds, adamc@49: SM.insert (cmap, x, corifyCon st c), adamc@49: st) adamc@49: | _ => (ds, cmap, st)) ([], SM.empty, st) sgis adamc@49: adamc@49: val st = St.bindStr st m n (St.ffi m cmap) adamc@49: in adamc@49: (rev ds, st) adamc@49: end adamc@49: | _ => raise Fail "Non-const signature for FFI structure") adamc@48: adamc@102: | L.DPage (c, e) => adamc@102: let adamc@102: val c = corifyCon st c adamc@102: val e = corifyExp st e adamc@102: adamc@102: val dom = (L'.TRecord c, loc) adamc@102: val ran = (L'.TRecord (L'.CRecord ((L'.KType, loc), []), loc), loc) adamc@102: val e = (L'.EAbs ("vs", dom, ran, adamc@102: (L'.EWrite (L'.EApp (e, (L'.ERel 0, loc)), loc), loc)), loc) adamc@102: adamc@102: in adamc@102: ([(L'.DPage (c, e), loc)], st) adamc@102: end adamc@48: 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@46: | L.StrFun _ => raise Fail "Corify of nested functor definition" adamc@46: | L.StrApp (str1, str2) => adamc@46: let adamc@46: fun unwind' (str, _) = adamc@46: case str of adamc@46: L.StrVar n => St.lookupStrById st n adamc@46: | L.StrProj (str, x) => St.lookupStrByName (x, unwind' str) adamc@46: | _ => raise Fail "Corify of fancy functor application [1]" adamc@46: adamc@46: fun unwind (str, _) = adamc@46: case str of adamc@46: L.StrVar n => St.lookupFunctorById st n adamc@46: | L.StrProj (str, x) => St.lookupFunctorByName (x, unwind' str) adamc@46: | _ => raise Fail "Corify of fancy functor application [2]" adamc@46: adamc@46: val (na, body) = unwind str1 adamc@46: adamc@46: val (ds1, {inner, outer}) = corifyStr (str2, st) adamc@46: val (ds2, sts) = corifyStr (body, St.bindStr outer "ARG" na inner) adamc@46: in adamc@46: (ds1 @ ds2, sts) adamc@46: end 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@48: | L.DStr (_, n', _, str) => Int.max (n, Int.max (n', maxNameStr str)) adamc@100: | L.DFfiStr (_, n', _) => Int.max (n, n') adamc@100: | L.DPage _ => n) 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