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