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@146: val debug : t -> unit adamc@146: adamc@39: val enter : t -> t adamc@39: val leave : t -> {outer : t, inner : t} adamc@192: val ffi : string -> L'.con SM.map -> (string * string list * L'.con option * L'.datatype_kind) 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@177: val bindConstructor : t -> string -> int -> L'.patCon -> t adamc@186: val lookupConstructorByNameOpt : t -> string -> L'.patCon option adamc@177: val lookupConstructorByName : t -> string -> L'.patCon adamc@177: val lookupConstructorById : t -> int -> L'.patCon adamc@177: adamc@188: datatype core_val = adamc@188: ENormal of int adamc@188: | EFfi of string * L'.con adamc@188: val bindVal : t -> string -> int -> t * int adamc@188: val bindConstructorVal : t -> string -> int -> t adamc@188: val lookupValById : t -> int -> int option adamc@188: val lookupValByName : t -> string -> core_val adamc@39: adamc@188: val bindStr : t -> string -> int -> t -> t adamc@188: val lookupStrById : t -> int -> t adamc@188: val lookupStrByName : string * t -> t adamc@46: adamc@188: val bindFunctor : t -> string -> int -> string -> int -> L.str -> t adamc@188: val lookupFunctorById : t -> int -> string * int * L.str adamc@188: val lookupFunctorByName : string * t -> string * int * L.str adamc@188: end = struct adamc@39: adamc@188: datatype flattening = adamc@188: FNormal of {cons : int SM.map, adamc@188: constructors : L'.patCon SM.map, adamc@188: vals : int SM.map, adamc@188: strs : flattening SM.map, adamc@188: funs : (string * int * L.str) SM.map} adamc@188: | FFfi of {mod : string, adamc@188: vals : L'.con SM.map, adamc@192: constructors : (string * string list * L'.con option * L'.datatype_kind) SM.map} adamc@39: adamc@188: type t = { adamc@188: cons : int IM.map, adamc@188: constructors : L'.patCon IM.map, adamc@188: vals : int IM.map, adamc@188: strs : flattening IM.map, adamc@188: funs : (string * int * L.str) IM.map, adamc@188: current : flattening, adamc@188: nested : flattening list adamc@188: } adamc@39: adamc@188: val empty = { adamc@188: cons = IM.empty, adamc@188: constructors = IM.empty, adamc@188: vals = IM.empty, adamc@188: strs = IM.empty, adamc@188: funs = IM.empty, adamc@188: current = FNormal { cons = SM.empty, constructors = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty }, adamc@188: nested = [] adamc@188: } adamc@146: adamc@188: fun debug ({current = FNormal {cons, constructors, vals, strs, funs}, ...} : t) = adamc@188: print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; " adamc@188: ^ "constructors: " ^ Int.toString (SM.numItems constructors) ^ "; " adamc@188: ^ "vals: " ^ Int.toString (SM.numItems vals) ^ "; " adamc@188: ^ "strs: " ^ Int.toString (SM.numItems strs) ^ "; " adamc@188: ^ "funs: " ^ Int.toString (SM.numItems funs) ^ "\n") adamc@188: | debug _ = print "Not normal!\n" adamc@48: adamc@188: datatype core_con = adamc@188: CNormal of int adamc@188: | CFfi of string adamc@73: adamc@188: datatype core_val = adamc@188: ENormal of int adamc@188: | EFfi of string * L'.con adamc@39: adamc@188: fun bindCon {cons, constructors, vals, strs, funs, current, nested} s n = adamc@188: let adamc@188: val n' = alloc () adamc@188: adamc@188: val current = adamc@188: case current of adamc@188: FFfi _ => raise Fail "Binding inside FFfi" adamc@188: | FNormal {cons, constructors, vals, strs, funs} => adamc@188: FNormal {cons = SM.insert (cons, s, n'), adamc@188: constructors = constructors, adamc@188: vals = vals, adamc@188: strs = strs, adamc@188: funs = funs} adamc@188: in adamc@188: ({cons = IM.insert (cons, n, n'), adamc@188: constructors = constructors, adamc@188: vals = vals, adamc@188: strs = strs, adamc@188: funs = funs, adamc@188: current = current, adamc@188: nested = nested}, adamc@188: n') adamc@188: end adamc@188: adamc@188: fun lookupConById ({cons, ...} : t) n = IM.find (cons, n) adamc@188: adamc@188: fun lookupConByName ({current, ...} : t) x = adamc@188: case current of adamc@188: FFfi {mod = m, ...} => CFfi m adamc@188: | FNormal {cons, ...} => adamc@188: case SM.find (cons, x) of adamc@188: NONE => raise Fail "Corify.St.lookupConByName" adamc@188: | SOME n => CNormal n adamc@188: adamc@188: fun bindVal {cons, constructors, vals, strs, funs, current, nested} s n = adamc@188: let adamc@188: val n' = alloc () adamc@188: adamc@188: val current = adamc@188: case current of adamc@188: FFfi _ => raise Fail "Binding inside FFfi" adamc@188: | FNormal {cons, constructors, vals, strs, funs} => adamc@188: FNormal {cons = cons, adamc@188: constructors = constructors, adamc@188: vals = SM.insert (vals, s, n'), adamc@188: strs = strs, adamc@188: funs = funs} adamc@188: in adamc@188: ({cons = cons, adamc@188: constructors = constructors, adamc@188: vals = IM.insert (vals, n, n'), adamc@188: strs = strs, adamc@188: funs = funs, adamc@188: current = current, adamc@188: nested = nested}, adamc@188: n') adamc@188: end adamc@188: adamc@188: fun bindConstructorVal {cons, constructors, vals, strs, funs, current, nested} s n = adamc@188: let adamc@188: val current = adamc@188: case current of adamc@188: FFfi _ => raise Fail "Binding inside FFfi" adamc@188: | FNormal {cons, constructors, vals, strs, funs} => adamc@188: FNormal {cons = cons, adamc@188: constructors = constructors, adamc@188: vals = SM.insert (vals, s, n), adamc@188: strs = strs, adamc@188: funs = funs} adamc@188: in adamc@188: {cons = cons, adamc@177: constructors = constructors, adamc@188: vals = IM.insert (vals, n, n), adamc@188: strs = strs, adamc@188: funs = funs, adamc@188: current = current, adamc@188: nested = nested} adamc@188: end adamc@188: adamc@188: adamc@188: fun lookupValById ({vals, ...} : t) n = IM.find (vals, n) adamc@188: adamc@188: fun lookupValByName ({current, ...} : t) x = adamc@188: case current of adamc@188: FFfi {mod = m, vals, ...} => adamc@188: (case SM.find (vals, x) of adamc@188: NONE => raise Fail "Corify.St.lookupValByName: no type for FFI val" adamc@188: | SOME t => EFfi (m, t)) adamc@188: | FNormal {vals, ...} => adamc@188: case SM.find (vals, x) of adamc@188: NONE => raise Fail "Corify.St.lookupValByName" adamc@188: | SOME n => ENormal n adamc@188: adamc@188: fun bindConstructor {cons, constructors, vals, strs, funs, current, nested} s n n' = adamc@188: let adamc@188: val current = adamc@188: case current of adamc@188: FFfi _ => raise Fail "Binding inside FFfi" adamc@188: | FNormal {cons, constructors, vals, strs, funs} => adamc@188: FNormal {cons = cons, adamc@188: constructors = SM.insert (constructors, s, n'), adamc@188: vals = vals, adamc@188: strs = strs, adamc@188: funs = funs} adamc@188: in adamc@188: {cons = cons, adamc@188: constructors = IM.insert (constructors, n, n'), adamc@73: vals = vals, adamc@39: strs = strs, adamc@46: funs = funs, adamc@39: current = current, adamc@188: nested = nested} adamc@188: end adamc@39: adamc@188: fun lookupConstructorById ({constructors, ...} : t) n = adamc@188: case IM.find (constructors, n) of adamc@188: NONE => raise Fail "Corify.St.lookupConstructorById" adamc@188: | SOME x => x adamc@39: adamc@188: fun lookupConstructorByNameOpt ({current, ...} : t) x = adamc@188: case current of adamc@188: FFfi {mod = m, constructors, ...} => adamc@188: (case SM.find (constructors, x) of adamc@188: NONE => NONE adamc@192: | SOME (n, xs, to, dk) => SOME (L'.PConFfi {mod = m, datatyp = n, params = xs, con = x, arg = to, kind = dk})) adamc@188: | FNormal {constructors, ...} => adamc@188: case SM.find (constructors, x) of adamc@188: NONE => NONE adamc@188: | SOME n => SOME n adamc@39: adamc@188: fun lookupConstructorByName ({current, ...} : t) x = adamc@188: case current of adamc@188: FFfi {mod = m, constructors, ...} => adamc@188: (case SM.find (constructors, x) of adamc@188: NONE => raise Fail "Corify.St.lookupConstructorByName [1]" adamc@192: | SOME (n, xs, to, dk) => L'.PConFfi {mod = m, datatyp = n, params = xs, con = x, arg = to, kind = dk}) adamc@188: | FNormal {constructors, ...} => adamc@188: case SM.find (constructors, x) of adamc@188: NONE => raise Fail "Corify.St.lookupConstructorByName [2]" adamc@188: | SOME n => n adamc@73: adamc@188: fun enter {cons, constructors, vals, strs, funs, current, nested} = adamc@188: {cons = cons, adamc@188: constructors = constructors, adamc@188: vals = vals, adamc@188: strs = strs, adamc@188: funs = funs, adamc@188: current = FNormal {cons = SM.empty, adamc@188: constructors = SM.empty, adamc@188: vals = SM.empty, adamc@188: strs = SM.empty, adamc@188: funs = SM.empty}, adamc@188: nested = current :: nested} adamc@73: adamc@188: fun dummy f = {cons = IM.empty, adamc@188: constructors = IM.empty, adamc@188: vals = IM.empty, adamc@188: strs = IM.empty, adamc@188: funs = IM.empty, adamc@188: current = f, adamc@188: nested = []} adamc@163: adamc@188: fun leave {cons, constructors, vals, strs, funs, current, nested = m1 :: rest} = adamc@188: {outer = {cons = cons, adamc@188: constructors = constructors, adamc@188: vals = vals, adamc@188: strs = strs, adamc@188: funs = funs, adamc@188: current = m1, adamc@188: nested = rest}, adamc@188: inner = dummy current} adamc@188: | leave _ = raise Fail "Corify.St.leave" adamc@177: adamc@188: fun ffi m vals constructors = dummy (FFfi {mod = m, vals = vals, constructors = constructors}) adamc@73: adamc@188: fun bindStr ({cons, constructors, vals, strs, funs, adamc@188: current = FNormal {cons = mcons, constructors = mconstructors, adamc@188: vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) adamc@188: x n ({current = f, ...} : t) = adamc@188: {cons = cons, adamc@188: constructors = constructors, adamc@188: vals = vals, adamc@188: strs = IM.insert (strs, n, f), adamc@188: funs = funs, adamc@188: current = FNormal {cons = mcons, adamc@188: constructors = mconstructors, adamc@188: vals = mvals, adamc@188: strs = SM.insert (mstrs, x, f), adamc@188: funs = mfuns}, adamc@188: nested = nested} adamc@188: | bindStr _ _ _ _ = raise Fail "Corify.St.bindStr" adamc@73: adamc@188: fun lookupStrById ({strs, ...} : t) n = adamc@188: case IM.find (strs, n) of adamc@188: NONE => raise Fail "Corify.St.lookupStrById" adamc@188: | SOME f => dummy f adamc@177: adamc@188: fun lookupStrByName (m, {current = FNormal {strs, ...}, ...} : t) = adamc@188: (case SM.find (strs, m) of adamc@188: NONE => raise Fail "Corify.St.lookupStrByName" adamc@188: | SOME f => dummy f) adamc@188: | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName" adamc@177: adamc@188: fun bindFunctor ({cons, constructors, vals, strs, funs, adamc@188: current = FNormal {cons = mcons, constructors = mconstructors, adamc@188: vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) adamc@188: x n xa na str = adamc@188: {cons = cons, adamc@188: constructors = constructors, adamc@188: vals = vals, adamc@188: strs = strs, adamc@188: funs = IM.insert (funs, n, (xa, na, str)), adamc@188: current = FNormal {cons = mcons, adamc@188: constructors = mconstructors, adamc@188: vals = mvals, adamc@188: strs = mstrs, adamc@188: funs = SM.insert (mfuns, x, (xa, na, str))}, adamc@188: nested = nested} adamc@188: | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor" adamc@186: adamc@188: fun lookupFunctorById ({funs, ...} : t) n = adamc@188: case IM.find (funs, n) of adamc@188: NONE => raise Fail "Corify.St.lookupFunctorById" adamc@188: | SOME v => v adamc@177: adamc@188: fun lookupFunctorByName (m, {current = FNormal {funs, ...}, ...} : t) = adamc@188: (case SM.find (funs, m) of adamc@188: NONE => raise Fail "Corify.St.lookupFunctorByName" adamc@188: | SOME v => v) adamc@188: | lookupFunctorByName _ = raise Fail "Corify.St.lookupFunctorByName" adamc@39: adamc@188: end adamc@39: adamc@39: adamc@188: fun corifyKind (k, loc) = adamc@188: case k of adamc@188: L.KType => (L'.KType, loc) adamc@188: | L.KArrow (k1, k2) => (L'.KArrow (corifyKind k1, corifyKind k2), loc) adamc@188: | L.KName => (L'.KName, loc) adamc@188: | L.KRecord k => (L'.KRecord (corifyKind k), loc) adamc@188: | L.KUnit => (L'.KUnit, loc) adamc@214: | L.KTuple ks => (L'.KTuple (map corifyKind ks), loc) adamc@48: adamc@188: fun corifyCon st (c, loc) = adamc@188: case c of adamc@188: L.TFun (t1, t2) => (L'.TFun (corifyCon st t1, corifyCon st t2), loc) adamc@188: | L.TCFun (x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon st t), loc) adamc@188: | L.TRecord c => (L'.TRecord (corifyCon st c), loc) adamc@39: adamc@188: | L.CRel n => (L'.CRel n, loc) adamc@188: | L.CNamed n => adamc@188: (case St.lookupConById st n of adamc@188: NONE => (L'.CNamed n, loc) adamc@188: | SOME n => (L'.CNamed n, loc)) adamc@188: | L.CModProj (m, ms, x) => adamc@188: let adamc@188: val st = St.lookupStrById st m adamc@188: val st = foldl St.lookupStrByName st ms adamc@188: in adamc@188: case St.lookupConByName st x of adamc@188: St.CNormal n => (L'.CNamed n, loc) adamc@188: | St.CFfi m => (L'.CFfi (m, x), loc) adamc@188: end adamc@39: adamc@188: | L.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc) adamc@188: | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon st c), loc) adamc@39: adamc@188: | L.CName s => (L'.CName s, loc) adamc@46: adamc@188: | L.CRecord (k, xcs) => adamc@188: (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc) adamc@188: | L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc) adamc@188: | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc) adamc@188: | L.CUnit => (L'.CUnit, loc) adamc@46: adamc@214: | L.CTuple cs => (L'.CTuple (map (corifyCon st) cs), loc) adamc@214: | L.CProj (c, n) => (L'.CProj (corifyCon st c, n), loc) adamc@213: adamc@188: fun corifyPatCon st pc = adamc@188: case pc of adamc@188: L.PConVar n => St.lookupConstructorById st n adamc@188: | L.PConProj (m1, ms, x) => adamc@188: let adamc@188: val st = St.lookupStrById st m1 adamc@188: val st = foldl St.lookupStrByName st ms adamc@188: in adamc@188: St.lookupConstructorByName st x adamc@188: end adamc@46: adamc@188: fun corifyPat st (p, loc) = adamc@188: case p of adamc@188: L.PWild => (L'.PWild, loc) adamc@188: | L.PVar (x, t) => (L'.PVar (x, corifyCon st t), loc) adamc@188: | L.PPrim p => (L'.PPrim p, loc) adamc@192: | L.PCon (dk, pc, ts, po) => (L'.PCon (dk, corifyPatCon st pc, map (corifyCon st) ts, adamc@192: Option.map (corifyPat st) po), loc) adamc@188: | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, corifyPat st p, corifyCon st t)) xps), loc) adamc@39: adamc@188: fun corifyExp st (e, loc) = adamc@188: case e of adamc@188: L.EPrim p => (L'.EPrim p, loc) adamc@188: | L.ERel n => (L'.ERel n, loc) adamc@188: | L.ENamed n => adamc@188: (case St.lookupValById st n of adamc@188: NONE => (L'.ENamed n, loc) adamc@188: | SOME n => (L'.ENamed n, loc)) adamc@188: | L.EModProj (m, ms, x) => adamc@188: let adamc@188: val st = St.lookupStrById st m adamc@188: val st = foldl St.lookupStrByName st ms adamc@188: in adamc@188: case St.lookupConstructorByNameOpt st x of adamc@192: SOME (pc as L'.PConFfi {mod = m, datatyp, params, arg, kind, ...}) => adamc@192: let adamc@192: val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) params adamc@192: val e = case arg of adamc@192: NONE => (L'.ECon (kind, pc, args, NONE), loc) adamc@192: | SOME dom => (L'.EAbs ("x", dom, (L'.CFfi (m, datatyp), loc), adamc@192: (L'.ECon (kind, pc, args, SOME (L'.ERel 0, loc)), loc)), loc) adamc@192: adamc@192: val k = (L'.KType, loc) adamc@192: in adamc@192: foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e params adamc@192: end adamc@188: | _ => adamc@188: case St.lookupValByName st x of adamc@188: St.ENormal n => (L'.ENamed n, loc) adamc@188: | St.EFfi (m, t) => adamc@188: case t of adamc@188: (L'.TFun (dom as (L'.TRecord (L'.CRecord (_, []), _), _), ran), _) => adamc@188: (L'.EAbs ("arg", dom, ran, (L'.EFfiApp (m, x, []), loc)), loc) adamc@188: | t as (L'.TFun _, _) => adamc@188: let adamc@188: fun getArgs (all as (t, _), args) = adamc@188: case t of adamc@188: L'.TFun (dom, ran) => getArgs (ran, dom :: args) adamc@188: | _ => (all, rev args) adamc@39: adamc@188: val (result, args) = getArgs (t, []) adamc@16: adamc@188: val (actuals, _) = foldr (fn (_, (actuals, n)) => adamc@188: ((L'.ERel n, loc) :: actuals, adamc@188: n + 1)) ([], 0) args adamc@188: val app = (L'.EFfiApp (m, x, actuals), loc) adamc@188: val (abs, _, _) = foldr (fn (t, (abs, ran, n)) => adamc@188: ((L'.EAbs ("arg" ^ Int.toString n, adamc@188: t, adamc@188: ran, adamc@188: abs), loc), adamc@188: (L'.TFun (t, ran), loc), adamc@188: n - 1)) (app, result, length args - 1) args adamc@188: in adamc@188: abs adamc@188: end adamc@188: | _ => (L'.EFfi (m, x), loc) adamc@188: end adamc@188: | L.EApp (e1, e2) => (L'.EApp (corifyExp st e1, corifyExp st e2), loc) adamc@188: | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon st dom, corifyCon st ran, corifyExp st e1), loc) adamc@188: | L.ECApp (e1, c) => (L'.ECApp (corifyExp st e1, corifyCon st c), loc) adamc@188: | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc) adamc@16: adamc@188: | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) => adamc@188: (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc) adamc@188: | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c, adamc@188: {field = corifyCon st field, rest = corifyCon st rest}), loc) adamc@188: | L.ECut (e1, c, {field, rest}) => (L'.ECut (corifyExp st e1, corifyCon st c, adamc@188: {field = corifyCon st field, rest = corifyCon st rest}), loc) adamc@188: | L.EFold k => (L'.EFold (corifyKind k), loc) adamc@34: adamc@188: | L.ECase (e, pes, {disc, result}) => adamc@188: (L'.ECase (corifyExp st e, adamc@188: map (fn (p, e) => (corifyPat st p, corifyExp st e)) pes, adamc@188: {disc = corifyCon st disc, result = corifyCon st result}), adamc@188: loc) adamc@16: adamc@188: | L.EWrite e => (L'.EWrite (corifyExp st e), loc) adamc@16: adamc@188: fun corifyDecl ((d, loc : EM.span), st) = adamc@188: case d of adamc@188: L.DCon (x, n, k, c) => adamc@188: let adamc@188: val (st, n) = St.bindCon st x n adamc@188: in adamc@188: ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st) adamc@188: end adamc@192: | L.DDatatype (x, n, xs, xncs) => adamc@192: let adamc@188: val (st, n) = St.bindCon st x n adamc@188: val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => adamc@188: let adamc@188: val st = St.bindConstructor st x n (L'.PConVar n) adamc@188: val st = St.bindConstructorVal st x n adamc@188: val co = Option.map (corifyCon st) co adamc@188: in adamc@188: ((x, n, co), st) adamc@188: end) st xncs adamc@16: adamc@198: val dk = ElabUtil.classifyDatatype xncs adamc@188: val t = (L'.CNamed n, loc) adamc@194: val nxs = length xs - 1 adamc@194: val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs adamc@192: val k = (L'.KType, loc) adamc@188: val dcons = map (fn (x, n, to) => adamc@188: let adamc@194: val args = ListUtil.mapi (fn (i, _) => (L'.CRel (nxs - i), loc)) xs adamc@188: val (e, t) = adamc@188: case to of adamc@192: NONE => ((L'.ECon (dk, L'.PConVar n, args, NONE), loc), t) adamc@188: | SOME t' => ((L'.EAbs ("x", t', t, adamc@192: (L'.ECon (dk, L'.PConVar n, args, adamc@192: SOME (L'.ERel 0, loc)), adamc@188: loc)), adamc@188: loc), adamc@188: (L'.TFun (t', t), loc)) adamc@192: adamc@192: val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs adamc@192: val e = foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs adamc@188: in adamc@188: (L'.DVal (x, n, t, e, ""), loc) adamc@188: end) xncs adamc@188: in adamc@192: ((L'.DDatatype (x, n, xs, xncs), loc) :: dcons, st) adamc@192: end adamc@192: | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) => adamc@192: let adamc@188: val (st, n) = St.bindCon st x n adamc@188: val c = corifyCon st (L.CModProj (m1, ms, s), loc) adamc@177: adamc@188: val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms adamc@188: val (_, {inner, ...}) = corifyStr (m, st) adamc@177: adamc@188: val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => adamc@188: let adamc@188: val n' = St.lookupConstructorByName inner x adamc@188: val st = St.bindConstructor st x n n' adamc@188: val (st, n) = St.bindVal st x n adamc@188: val co = Option.map (corifyCon st) co adamc@188: in adamc@188: ((x, n, co), st) adamc@188: end) st xncs adamc@49: adamc@194: val nxs = length xs - 1 adamc@194: val c = ListUtil.foldli (fn (i, _, c) => (L'.CApp (c, (L'.CRel (nxs - i), loc)), loc)) c xs adamc@192: val k = (L'.KType, loc) adamc@192: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@192: adamc@188: val cds = map (fn (x, n, co) => adamc@188: let adamc@188: val t = case co of adamc@188: NONE => c adamc@188: | SOME t' => (L'.TFun (t', c), loc) adamc@188: val e = corifyExp st (L.EModProj (m1, ms, x), loc) adamc@192: adamc@192: val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs adamc@188: in adamc@188: (L'.DVal (x, n, t, e, x), loc) adamc@188: end) xncs adamc@188: in adamc@192: ((L'.DCon (x, n, k', c), loc) :: cds, st) adamc@192: end adamc@188: | L.DVal (x, n, t, e) => adamc@188: let adamc@188: val (st, n) = St.bindVal st x n adamc@188: val s = adamc@188: if String.isPrefix "wrap_" x then adamc@188: String.extract (x, 5, NONE) adamc@188: else adamc@188: x adamc@188: in adamc@188: ([(L'.DVal (x, n, corifyCon st t, corifyExp st e, s), loc)], st) adamc@188: end adamc@188: | L.DValRec vis => adamc@188: let adamc@188: val (vis, st) = ListUtil.foldlMap adamc@188: (fn ((x, n, t, e), st) => adamc@188: let adamc@188: val (st, n) = St.bindVal st x n adamc@188: in adamc@188: ((x, n, t, e), st) adamc@188: end) adamc@188: st vis adamc@16: adamc@188: val vis = map adamc@188: (fn (x, n, t, e) => adamc@188: let adamc@188: val s = adamc@188: if String.isPrefix "wrap_" x then adamc@188: String.extract (x, 5, NONE) adamc@188: else adamc@188: x adamc@188: in adamc@188: (x, n, corifyCon st t, corifyExp st e, s) adamc@188: end) adamc@188: vis adamc@188: in adamc@188: ([(L'.DValRec vis, loc)], st) adamc@188: end adamc@188: | L.DSgn _ => ([], st) adamc@177: adamc@188: | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) => adamc@188: ([], St.bindFunctor st x n xa na str) adamc@177: adamc@188: | L.DStr (x, n, _, str) => adamc@188: let adamc@188: val (ds, {inner, outer}) = corifyStr (str, st) adamc@188: val st = St.bindStr outer x n inner adamc@188: in adamc@188: (ds, st) adamc@188: end adamc@16: adamc@188: | L.DFfiStr (m, n, (sgn, _)) => adamc@188: (case sgn of adamc@188: L.SgnConst sgis => adamc@188: let adamc@188: val (ds, cmap, conmap, st) = adamc@188: foldl (fn ((sgi, _), (ds, cmap, conmap, st)) => adamc@188: case sgi of adamc@188: L.SgiConAbs (x, n, k) => adamc@188: let adamc@188: val (st, n') = St.bindCon st x n adamc@188: in adamc@188: ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, adamc@188: cmap, adamc@188: conmap, adamc@188: st) adamc@188: end adamc@188: | L.SgiCon (x, n, k, _) => adamc@188: let adamc@188: val (st, n') = St.bindCon st x n adamc@188: in adamc@188: ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, adamc@188: cmap, adamc@188: conmap, adamc@188: st) adamc@188: end adamc@177: adamc@192: | L.SgiDatatype (x, n, xs, xnts) => adamc@192: let adamc@192: val k = (L'.KType, loc) adamc@198: val dk = ElabUtil.classifyDatatype xnts adamc@188: val (st, n') = St.bindCon st x n adamc@188: val (xnts, (ds', st, cmap, conmap)) = adamc@188: ListUtil.foldlMap adamc@188: (fn ((x', n, to), (ds', st, cmap, conmap)) => adamc@188: let adamc@188: val dt = (L'.CNamed n', loc) adamc@192: val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) xs adamc@163: adamc@188: val to = Option.map (corifyCon st) to adamc@177: adamc@188: val pc = L'.PConFfi {mod = m, adamc@188: datatyp = x, adamc@192: params = xs, adamc@188: con = x', adamc@188: arg = to, adamc@188: kind = dk} adamc@130: adamc@192: fun wrapT t = adamc@192: foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs adamc@192: fun wrapE e = adamc@192: foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs adamc@192: adamc@188: val (cmap, d) = adamc@188: case to of adamc@192: NONE => (SM.insert (cmap, x', wrapT dt), adamc@192: (L'.DVal (x', n, wrapT dt, adamc@192: wrapE adamc@192: (L'.ECon (dk, pc, args, NONE), adamc@192: loc), adamc@188: ""), loc)) adamc@188: | SOME t => adamc@188: let adamc@188: val tf = (L'.TFun (t, dt), loc) adamc@192: val e = wrapE (L'.EAbs ("x", t, tf, adamc@192: (L'.ECon (dk, pc, args, adamc@192: SOME (L'.ERel 0, adamc@192: loc)), adamc@192: loc)), loc) adamc@192: val d = (L'.DVal (x', n, wrapT tf, adamc@192: e, ""), loc) adamc@185: in adamc@192: (SM.insert (cmap, x', wrapT tf), d) adamc@185: end adamc@185: adamc@186: val st = St.bindConstructor st x' n pc adamc@186: adamc@192: val conmap = SM.insert (conmap, x', (x, xs, to, dk)) adamc@185: in adamc@185: ((x', n, to), adamc@186: (d :: ds', st, cmap, conmap)) adamc@186: end) ([], st, cmap, conmap) xnts adamc@185: in adamc@192: (ds' @ (L'.DDatatype (x, n', xs, xnts), loc) :: ds, adamc@185: cmap, adamc@185: conmap, adamc@49: st) adamc@192: end adamc@49: adamc@49: | L.SgiVal (x, _, c) => adamc@49: (ds, adamc@49: SM.insert (cmap, x, corifyCon st c), adamc@185: conmap, adamc@49: st) adamc@185: | _ => (ds, cmap, conmap, st)) ([], SM.empty, SM.empty, st) sgis adamc@49: adamc@185: val st = St.bindStr st m n (St.ffi m cmap conmap) adamc@49: in adamc@49: (rev ds, st) adamc@49: end adamc@49: | _ => raise Fail "Non-const signature for FFI structure") adamc@48: adamc@109: | L.DExport (en, sgn, str) => adamc@109: (case #1 sgn of adamc@109: L.SgnConst sgis => adamc@109: let adamc@109: fun pathify (str, _) = adamc@109: case str of adamc@109: L.StrVar m => SOME (m, []) adamc@109: | L.StrProj (str, s) => adamc@109: Option.map (fn (m, ms) => (m, ms @ [s])) (pathify str) adamc@109: | _ => NONE adamc@109: in adamc@109: case pathify str of adamc@109: NONE => (ErrorMsg.errorAt loc "Structure is too fancy to export"; adamc@109: ([], st)) adamc@109: | SOME (m, ms) => adamc@109: let adamc@109: fun wrapSgi ((sgi, _), (wds, eds)) = adamc@109: case sgi of adamc@109: L.SgiVal (s, _, t as (L.TFun (dom, ran), _)) => adamc@109: (case (#1 dom, #1 ran) of adamc@147: (L.TRecord (L.CRecord (_, []), _), adamc@139: L.CApp adamc@139: ((L.CApp adamc@139: ((L.CApp ((L.CModProj (_, [], "xml"), _), adamc@139: (L.CRecord (_, [((L.CName "Html", _), adamc@139: _)]), _)), _), _), _), _)) => adamc@109: let adamc@109: val ran = (L.TRecord (L.CRecord ((L.KType, loc), []), loc), loc) adamc@109: val e = (L.EModProj (m, ms, s), loc) adamc@109: val e = (L.EAbs ("vs", dom, ran, adamc@109: (L.EWrite (L.EApp (e, (L.ERel 0, loc)), loc), loc)), loc) adamc@109: in adamc@109: ((L.DVal ("wrap_" ^ s, 0, adamc@109: (L.TFun (dom, ran), loc), adamc@109: e), loc) :: wds, adamc@109: (fn st => adamc@109: case #1 (corifyExp st (L.EModProj (en, [], "wrap_" ^ s), loc)) of adamc@144: L'.ENamed n => (L'.DExport (L'.Link, n), loc) adamc@109: | _ => raise Fail "Corify: Value to export didn't corify properly") adamc@109: :: eds) adamc@109: end adamc@109: | _ => (wds, eds)) adamc@109: | _ => (wds, eds) adamc@102: adamc@109: val (wds, eds) = foldl wrapSgi ([], []) sgis adamc@109: val wrapper = (L.StrConst wds, loc) adamc@109: val (ds, {inner, outer}) = corifyStr (wrapper, st) adamc@109: val st = St.bindStr outer "wrapper" en inner adamc@109: adamc@109: val ds = ds @ map (fn f => f st) eds adamc@109: in adamc@109: (ds, st) adamc@109: end adamc@109: end adamc@109: | _ => raise Fail "Non-const signature for 'export'") 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@146: val (xa, na, body) = unwind str1 adamc@46: adamc@146: val (ds1, {inner = inner', outer}) = corifyStr (str2, st) adamc@146: val (ds2, {inner, outer}) = corifyStr (body, St.bindStr outer xa na inner') adamc@46: in adamc@146: (ds1 @ ds2, {inner = St.bindStr inner xa na inner', outer = outer}) 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@191: | L.DDatatype (_, n', _, _) => Int.max (n, n') adamc@191: | L.DDatatypeImp (_, n', _, _, _, _, _) => Int.max (n, n') adamc@124: | L.DVal (_, n', _, _) => Int.max (n, n') adamc@124: | L.DValRec vis => foldl (fn ((_, n', _, _), n) => Int.max (n, n)) n vis 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@109: | L.DExport _ => 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@146: adamc@39: val (ds, _) = ListUtil.foldlMapConcat corifyDecl St.empty ds adamc@39: in adamc@39: ds adamc@39: end adamc@16: adamc@16: end