Mercurial > urweb
diff src/corify.sml @ 188:8e9f97508f0d
Datatype representation optimization
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 03 Aug 2008 19:49:21 -0400 |
| parents | 88d46972de53 |
| children | aa54250f58ac |
line wrap: on
line diff
--- a/src/corify.sml Sun Aug 03 19:01:16 2008 -0400 +++ b/src/corify.sml Sun Aug 03 19:49:21 2008 -0400 @@ -62,7 +62,7 @@ val enter : t -> t val leave : t -> {outer : t, inner : t} - val ffi : string -> L'.con SM.map -> (string * L'.con option) SM.map -> t + val ffi : string -> L'.con SM.map -> (string * L'.con option * L'.datatype_kind) SM.map -> t datatype core_con = CNormal of int @@ -76,605 +76,609 @@ val lookupConstructorByName : t -> string -> L'.patCon val lookupConstructorById : t -> int -> L'.patCon - datatype core_val = - ENormal of int - | EFfi of string * L'.con - val bindVal : t -> string -> int -> t * int - val bindConstructorVal : t -> string -> int -> t - val lookupValById : t -> int -> int option - val lookupValByName : t -> string -> core_val + datatype core_val = + ENormal of int + | EFfi of string * L'.con + val bindVal : t -> string -> int -> t * int + val bindConstructorVal : t -> string -> int -> t + val lookupValById : t -> int -> int option + val lookupValByName : t -> string -> core_val - val bindStr : t -> string -> int -> t -> t - val lookupStrById : t -> int -> t - val lookupStrByName : string * t -> t + val bindStr : t -> string -> int -> t -> t + val lookupStrById : t -> int -> t + val lookupStrByName : string * t -> t - val bindFunctor : t -> string -> int -> string -> int -> L.str -> t - val lookupFunctorById : t -> int -> string * int * L.str - val lookupFunctorByName : string * t -> string * int * L.str -end = struct + val bindFunctor : t -> string -> int -> string -> int -> L.str -> t + val lookupFunctorById : t -> int -> string * int * L.str + val lookupFunctorByName : string * t -> string * int * L.str + end = struct -datatype flattening = - FNormal of {cons : int SM.map, - constructors : L'.patCon SM.map, - vals : int SM.map, - strs : flattening SM.map, - funs : (string * int * L.str) SM.map} - | FFfi of {mod : string, - vals : L'.con SM.map, - constructors : (string * L'.con option) SM.map} - -type t = { - cons : int IM.map, - constructors : L'.patCon IM.map, - vals : int IM.map, - strs : flattening IM.map, - funs : (string * int * L.str) IM.map, - current : flattening, - nested : flattening list -} + datatype flattening = + FNormal of {cons : int SM.map, + constructors : L'.patCon SM.map, + vals : int SM.map, + strs : flattening SM.map, + funs : (string * int * L.str) SM.map} + | FFfi of {mod : string, + vals : L'.con SM.map, + constructors : (string * L'.con option * L'.datatype_kind) SM.map} -val empty = { - cons = IM.empty, - constructors = IM.empty, - vals = IM.empty, - strs = IM.empty, - funs = IM.empty, - current = FNormal { cons = SM.empty, constructors = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty }, - nested = [] -} + type t = { + cons : int IM.map, + constructors : L'.patCon IM.map, + vals : int IM.map, + strs : flattening IM.map, + funs : (string * int * L.str) IM.map, + current : flattening, + nested : flattening list + } -fun debug ({current = FNormal {cons, constructors, vals, strs, funs}, ...} : t) = - print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; " - ^ "constructors: " ^ Int.toString (SM.numItems constructors) ^ "; " - ^ "vals: " ^ Int.toString (SM.numItems vals) ^ "; " - ^ "strs: " ^ Int.toString (SM.numItems strs) ^ "; " - ^ "funs: " ^ Int.toString (SM.numItems funs) ^ "\n") - | debug _ = print "Not normal!\n" + val empty = { + cons = IM.empty, + constructors = IM.empty, + vals = IM.empty, + strs = IM.empty, + funs = IM.empty, + current = FNormal { cons = SM.empty, constructors = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty }, + nested = [] + } -datatype core_con = - CNormal of int - | CFfi of string + fun debug ({current = FNormal {cons, constructors, vals, strs, funs}, ...} : t) = + print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; " + ^ "constructors: " ^ Int.toString (SM.numItems constructors) ^ "; " + ^ "vals: " ^ Int.toString (SM.numItems vals) ^ "; " + ^ "strs: " ^ Int.toString (SM.numItems strs) ^ "; " + ^ "funs: " ^ Int.toString (SM.numItems funs) ^ "\n") + | debug _ = print "Not normal!\n" -datatype core_val = - ENormal of int - | EFfi of string * L'.con + datatype core_con = + CNormal of int + | CFfi of string -fun bindCon {cons, constructors, vals, strs, funs, current, nested} s n = - let - val n' = alloc () + datatype core_val = + ENormal of int + | EFfi of string * L'.con - val current = - case current of - FFfi _ => raise Fail "Binding inside FFfi" - | FNormal {cons, constructors, vals, strs, funs} => - FNormal {cons = SM.insert (cons, s, n'), - constructors = constructors, - vals = vals, - strs = strs, - funs = funs} - in - ({cons = IM.insert (cons, n, n'), + fun bindCon {cons, constructors, vals, strs, funs, current, nested} s n = + let + val n' = alloc () + + val current = + case current of + FFfi _ => raise Fail "Binding inside FFfi" + | FNormal {cons, constructors, vals, strs, funs} => + FNormal {cons = SM.insert (cons, s, n'), + constructors = constructors, + vals = vals, + strs = strs, + funs = funs} + in + ({cons = IM.insert (cons, n, n'), + constructors = constructors, + vals = vals, + strs = strs, + funs = funs, + current = current, + nested = nested}, + n') + end + + fun lookupConById ({cons, ...} : t) n = IM.find (cons, n) + + fun lookupConByName ({current, ...} : t) x = + case current of + FFfi {mod = m, ...} => CFfi m + | FNormal {cons, ...} => + case SM.find (cons, x) of + NONE => raise Fail "Corify.St.lookupConByName" + | SOME n => CNormal n + + fun bindVal {cons, constructors, vals, strs, funs, current, nested} s n = + let + val n' = alloc () + + val current = + case current of + FFfi _ => raise Fail "Binding inside FFfi" + | FNormal {cons, constructors, vals, strs, funs} => + FNormal {cons = cons, + constructors = constructors, + vals = SM.insert (vals, s, n'), + strs = strs, + funs = funs} + in + ({cons = cons, + constructors = constructors, + vals = IM.insert (vals, n, n'), + strs = strs, + funs = funs, + current = current, + nested = nested}, + n') + end + + fun bindConstructorVal {cons, constructors, vals, strs, funs, current, nested} s n = + let + val current = + case current of + FFfi _ => raise Fail "Binding inside FFfi" + | FNormal {cons, constructors, vals, strs, funs} => + FNormal {cons = cons, + constructors = constructors, + vals = SM.insert (vals, s, n), + strs = strs, + funs = funs} + in + {cons = cons, constructors = constructors, + vals = IM.insert (vals, n, n), + strs = strs, + funs = funs, + current = current, + nested = nested} + end + + + fun lookupValById ({vals, ...} : t) n = IM.find (vals, n) + + fun lookupValByName ({current, ...} : t) x = + case current of + FFfi {mod = m, vals, ...} => + (case SM.find (vals, x) of + NONE => raise Fail "Corify.St.lookupValByName: no type for FFI val" + | SOME t => EFfi (m, t)) + | FNormal {vals, ...} => + case SM.find (vals, x) of + NONE => raise Fail "Corify.St.lookupValByName" + | SOME n => ENormal n + + fun bindConstructor {cons, constructors, vals, strs, funs, current, nested} s n n' = + let + val current = + case current of + FFfi _ => raise Fail "Binding inside FFfi" + | FNormal {cons, constructors, vals, strs, funs} => + FNormal {cons = cons, + constructors = SM.insert (constructors, s, n'), + vals = vals, + strs = strs, + funs = funs} + in + {cons = cons, + constructors = IM.insert (constructors, n, n'), vals = vals, strs = strs, funs = funs, current = current, - nested = nested}, - n') - end + nested = nested} + end -fun lookupConById ({cons, ...} : t) n = IM.find (cons, n) + fun lookupConstructorById ({constructors, ...} : t) n = + case IM.find (constructors, n) of + NONE => raise Fail "Corify.St.lookupConstructorById" + | SOME x => x -fun lookupConByName ({current, ...} : t) x = - case current of - FFfi {mod = m, ...} => CFfi m - | FNormal {cons, ...} => - case SM.find (cons, x) of - NONE => raise Fail "Corify.St.lookupConByName" - | SOME n => CNormal n + fun lookupConstructorByNameOpt ({current, ...} : t) x = + case current of + FFfi {mod = m, constructors, ...} => + (case SM.find (constructors, x) of + NONE => NONE + | SOME (n, to, dk) => SOME (L'.PConFfi {mod = m, datatyp = n, con = x, arg = to, kind = dk})) + | FNormal {constructors, ...} => + case SM.find (constructors, x) of + NONE => NONE + | SOME n => SOME n -fun bindVal {cons, constructors, vals, strs, funs, current, nested} s n = - let - val n' = alloc () + fun lookupConstructorByName ({current, ...} : t) x = + case current of + FFfi {mod = m, constructors, ...} => + (case SM.find (constructors, x) of + NONE => raise Fail "Corify.St.lookupConstructorByName [1]" + | SOME (n, to, dk) => L'.PConFfi {mod = m, datatyp = n, con = x, arg = to, kind = dk}) + | FNormal {constructors, ...} => + case SM.find (constructors, x) of + NONE => raise Fail "Corify.St.lookupConstructorByName [2]" + | SOME n => n - val current = - case current of - FFfi _ => raise Fail "Binding inside FFfi" - | FNormal {cons, constructors, vals, strs, funs} => - FNormal {cons = cons, - constructors = constructors, - vals = SM.insert (vals, s, n'), - strs = strs, - funs = funs} - in - ({cons = cons, - constructors = constructors, - vals = IM.insert (vals, n, n'), - strs = strs, - funs = funs, - current = current, - nested = nested}, - n') - end + fun enter {cons, constructors, vals, strs, funs, current, nested} = + {cons = cons, + constructors = constructors, + vals = vals, + strs = strs, + funs = funs, + current = FNormal {cons = SM.empty, + constructors = SM.empty, + vals = SM.empty, + strs = SM.empty, + funs = SM.empty}, + nested = current :: nested} -fun bindConstructorVal {cons, constructors, vals, strs, funs, current, nested} s n = - let - val current = - case current of - FFfi _ => raise Fail "Binding inside FFfi" - | FNormal {cons, constructors, vals, strs, funs} => - FNormal {cons = cons, - constructors = constructors, - vals = SM.insert (vals, s, n), - strs = strs, - funs = funs} - in - {cons = cons, - constructors = constructors, - vals = IM.insert (vals, n, n), - strs = strs, - funs = funs, - current = current, - nested = nested} - end + fun dummy f = {cons = IM.empty, + constructors = IM.empty, + vals = IM.empty, + strs = IM.empty, + funs = IM.empty, + current = f, + nested = []} + fun leave {cons, constructors, vals, strs, funs, current, nested = m1 :: rest} = + {outer = {cons = cons, + constructors = constructors, + vals = vals, + strs = strs, + funs = funs, + current = m1, + nested = rest}, + inner = dummy current} + | leave _ = raise Fail "Corify.St.leave" -fun lookupValById ({vals, ...} : t) n = IM.find (vals, n) + fun ffi m vals constructors = dummy (FFfi {mod = m, vals = vals, constructors = constructors}) -fun lookupValByName ({current, ...} : t) x = - case current of - FFfi {mod = m, vals, ...} => - (case SM.find (vals, x) of - NONE => raise Fail "Corify.St.lookupValByName: no type for FFI val" - | SOME t => EFfi (m, t)) - | FNormal {vals, ...} => - case SM.find (vals, x) of - NONE => raise Fail "Corify.St.lookupValByName" - | SOME n => ENormal n + fun bindStr ({cons, constructors, vals, strs, funs, + current = FNormal {cons = mcons, constructors = mconstructors, + vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) + x n ({current = f, ...} : t) = + {cons = cons, + constructors = constructors, + vals = vals, + strs = IM.insert (strs, n, f), + funs = funs, + current = FNormal {cons = mcons, + constructors = mconstructors, + vals = mvals, + strs = SM.insert (mstrs, x, f), + funs = mfuns}, + nested = nested} + | bindStr _ _ _ _ = raise Fail "Corify.St.bindStr" -fun bindConstructor {cons, constructors, vals, strs, funs, current, nested} s n n' = - let - val current = - case current of - FFfi _ => raise Fail "Binding inside FFfi" - | FNormal {cons, constructors, vals, strs, funs} => - FNormal {cons = cons, - constructors = SM.insert (constructors, s, n'), - vals = vals, - strs = strs, - funs = funs} - in - {cons = cons, - constructors = IM.insert (constructors, n, n'), - vals = vals, - strs = strs, - funs = funs, - current = current, - nested = nested} - end + fun lookupStrById ({strs, ...} : t) n = + case IM.find (strs, n) of + NONE => raise Fail "Corify.St.lookupStrById" + | SOME f => dummy f -fun lookupConstructorById ({constructors, ...} : t) n = - case IM.find (constructors, n) of - NONE => raise Fail "Corify.St.lookupConstructorById" - | SOME x => x + fun lookupStrByName (m, {current = FNormal {strs, ...}, ...} : t) = + (case SM.find (strs, m) of + NONE => raise Fail "Corify.St.lookupStrByName" + | SOME f => dummy f) + | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName" -fun lookupConstructorByNameOpt ({current, ...} : t) x = - case current of - FFfi {mod = m, constructors, ...} => - (case SM.find (constructors, x) of - NONE => NONE - | SOME (n, to) => SOME (L'.PConFfi {mod = m, datatyp = n, con = x, arg = to})) - | FNormal {constructors, ...} => - case SM.find (constructors, x) of - NONE => NONE - | SOME n => SOME n + fun bindFunctor ({cons, constructors, vals, strs, funs, + current = FNormal {cons = mcons, constructors = mconstructors, + vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) + x n xa na str = + {cons = cons, + constructors = constructors, + vals = vals, + strs = strs, + funs = IM.insert (funs, n, (xa, na, str)), + current = FNormal {cons = mcons, + constructors = mconstructors, + vals = mvals, + strs = mstrs, + funs = SM.insert (mfuns, x, (xa, na, str))}, + nested = nested} + | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor" -fun lookupConstructorByName ({current, ...} : t) x = - case current of - FFfi {mod = m, constructors, ...} => - (case SM.find (constructors, x) of - NONE => raise Fail "Corify.St.lookupConstructorByName [1]" - | SOME (n, to) => L'.PConFfi {mod = m, datatyp = n, con = x, arg = to}) - | FNormal {constructors, ...} => - case SM.find (constructors, x) of - NONE => raise Fail "Corify.St.lookupConstructorByName [2]" - | SOME n => n + fun lookupFunctorById ({funs, ...} : t) n = + case IM.find (funs, n) of + NONE => raise Fail "Corify.St.lookupFunctorById" + | SOME v => v -fun enter {cons, constructors, vals, strs, funs, current, nested} = - {cons = cons, - constructors = constructors, - vals = vals, - strs = strs, - funs = funs, - current = FNormal {cons = SM.empty, - constructors = SM.empty, - vals = SM.empty, - strs = SM.empty, - funs = SM.empty}, - nested = current :: nested} + fun lookupFunctorByName (m, {current = FNormal {funs, ...}, ...} : t) = + (case SM.find (funs, m) of + NONE => raise Fail "Corify.St.lookupFunctorByName" + | SOME v => v) + | lookupFunctorByName _ = raise Fail "Corify.St.lookupFunctorByName" -fun dummy f = {cons = IM.empty, - constructors = IM.empty, - vals = IM.empty, - strs = IM.empty, - funs = IM.empty, - current = f, - nested = []} + end -fun leave {cons, constructors, vals, strs, funs, current, nested = m1 :: rest} = - {outer = {cons = cons, - constructors = constructors, - vals = vals, - strs = strs, - funs = funs, - current = m1, - nested = rest}, - inner = dummy current} - | leave _ = raise Fail "Corify.St.leave" -fun ffi m vals constructors = dummy (FFfi {mod = m, vals = vals, constructors = constructors}) + fun corifyKind (k, loc) = + case k of + L.KType => (L'.KType, loc) + | L.KArrow (k1, k2) => (L'.KArrow (corifyKind k1, corifyKind k2), loc) + | L.KName => (L'.KName, loc) + | L.KRecord k => (L'.KRecord (corifyKind k), loc) + | L.KUnit => (L'.KUnit, loc) -fun bindStr ({cons, constructors, vals, strs, funs, - current = FNormal {cons = mcons, constructors = mconstructors, - vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) - x n ({current = f, ...} : t) = - {cons = cons, - constructors = constructors, - vals = vals, - strs = IM.insert (strs, n, f), - funs = funs, - current = FNormal {cons = mcons, - constructors = mconstructors, - vals = mvals, - strs = SM.insert (mstrs, x, f), - funs = mfuns}, - nested = nested} - | bindStr _ _ _ _ = raise Fail "Corify.St.bindStr" + fun corifyCon st (c, loc) = + case c of + L.TFun (t1, t2) => (L'.TFun (corifyCon st t1, corifyCon st t2), loc) + | L.TCFun (x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon st t), loc) + | L.TRecord c => (L'.TRecord (corifyCon st c), loc) -fun lookupStrById ({strs, ...} : t) n = - case IM.find (strs, n) of - NONE => raise Fail "Corify.St.lookupStrById" - | SOME f => dummy f + | L.CRel n => (L'.CRel n, loc) + | L.CNamed n => + (case St.lookupConById st n of + NONE => (L'.CNamed n, loc) + | SOME n => (L'.CNamed n, loc)) + | L.CModProj (m, ms, x) => + let + val st = St.lookupStrById st m + val st = foldl St.lookupStrByName st ms + in + case St.lookupConByName st x of + St.CNormal n => (L'.CNamed n, loc) + | St.CFfi m => (L'.CFfi (m, x), loc) + end -fun lookupStrByName (m, {current = FNormal {strs, ...}, ...} : t) = - (case SM.find (strs, m) of - NONE => raise Fail "Corify.St.lookupStrByName" - | SOME f => dummy f) - | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName" + | L.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc) + | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon st c), loc) -fun bindFunctor ({cons, constructors, vals, strs, funs, - current = FNormal {cons = mcons, constructors = mconstructors, - vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) - x n xa na str = - {cons = cons, - constructors = constructors, - vals = vals, - strs = strs, - funs = IM.insert (funs, n, (xa, na, str)), - current = FNormal {cons = mcons, - constructors = mconstructors, - vals = mvals, - strs = mstrs, - funs = SM.insert (mfuns, x, (xa, na, str))}, - nested = nested} - | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor" + | L.CName s => (L'.CName s, loc) -fun lookupFunctorById ({funs, ...} : t) n = - case IM.find (funs, n) of - NONE => raise Fail "Corify.St.lookupFunctorById" - | SOME v => v + | L.CRecord (k, xcs) => + (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc) + | L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc) + | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc) + | L.CUnit => (L'.CUnit, loc) -fun lookupFunctorByName (m, {current = FNormal {funs, ...}, ...} : t) = - (case SM.find (funs, m) of - NONE => raise Fail "Corify.St.lookupFunctorByName" - | SOME v => v) - | lookupFunctorByName _ = raise Fail "Corify.St.lookupFunctorByName" + fun corifyPatCon st pc = + case pc of + L.PConVar n => St.lookupConstructorById st n + | L.PConProj (m1, ms, x) => + let + val st = St.lookupStrById st m1 + val st = foldl St.lookupStrByName st ms + in + St.lookupConstructorByName st x + end -end + fun corifyPat st (p, loc) = + case p of + L.PWild => (L'.PWild, loc) + | L.PVar (x, t) => (L'.PVar (x, corifyCon st t), loc) + | L.PPrim p => (L'.PPrim p, loc) + | L.PCon (dk, pc, po) => (L'.PCon (dk, corifyPatCon st pc, Option.map (corifyPat st) po), loc) + | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, corifyPat st p, corifyCon st t)) xps), loc) + fun corifyExp st (e, loc) = + case e of + L.EPrim p => (L'.EPrim p, loc) + | L.ERel n => (L'.ERel n, loc) + | L.ENamed n => + (case St.lookupValById st n of + NONE => (L'.ENamed n, loc) + | SOME n => (L'.ENamed n, loc)) + | L.EModProj (m, ms, x) => + let + val st = St.lookupStrById st m + val st = foldl St.lookupStrByName st ms + in + case St.lookupConstructorByNameOpt st x of + SOME (pc as L'.PConFfi {mod = m, datatyp, arg, kind, ...}) => + (case arg of + NONE => (L'.ECon (kind, pc, NONE), loc) + | SOME dom => (L'.EAbs ("x", dom, (L'.CFfi (m, datatyp), loc), + (L'.ECon (kind, pc, SOME (L'.ERel 0, loc)), loc)), loc)) + | _ => + case St.lookupValByName st x of + St.ENormal n => (L'.ENamed n, loc) + | St.EFfi (m, t) => + case t of + (L'.TFun (dom as (L'.TRecord (L'.CRecord (_, []), _), _), ran), _) => + (L'.EAbs ("arg", dom, ran, (L'.EFfiApp (m, x, []), loc)), loc) + | t as (L'.TFun _, _) => + let + fun getArgs (all as (t, _), args) = + case t of + L'.TFun (dom, ran) => getArgs (ran, dom :: args) + | _ => (all, rev args) -fun corifyKind (k, loc) = - case k of - L.KType => (L'.KType, loc) - | L.KArrow (k1, k2) => (L'.KArrow (corifyKind k1, corifyKind k2), loc) - | L.KName => (L'.KName, loc) - | L.KRecord k => (L'.KRecord (corifyKind k), loc) - | L.KUnit => (L'.KUnit, loc) + val (result, args) = getArgs (t, []) -fun corifyCon st (c, loc) = - case c of - L.TFun (t1, t2) => (L'.TFun (corifyCon st t1, corifyCon st t2), loc) - | L.TCFun (x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon st t), loc) - | L.TRecord c => (L'.TRecord (corifyCon st c), loc) + val (actuals, _) = foldr (fn (_, (actuals, n)) => + ((L'.ERel n, loc) :: actuals, + n + 1)) ([], 0) args + val app = (L'.EFfiApp (m, x, actuals), loc) + val (abs, _, _) = foldr (fn (t, (abs, ran, n)) => + ((L'.EAbs ("arg" ^ Int.toString n, + t, + ran, + abs), loc), + (L'.TFun (t, ran), loc), + n - 1)) (app, result, length args - 1) args + in + abs + end + | _ => (L'.EFfi (m, x), loc) + end + | L.EApp (e1, e2) => (L'.EApp (corifyExp st e1, corifyExp st e2), loc) + | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon st dom, corifyCon st ran, corifyExp st e1), loc) + | L.ECApp (e1, c) => (L'.ECApp (corifyExp st e1, corifyCon st c), loc) + | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc) - | L.CRel n => (L'.CRel n, loc) - | L.CNamed n => - (case St.lookupConById st n of - NONE => (L'.CNamed n, loc) - | SOME n => (L'.CNamed n, loc)) - | L.CModProj (m, ms, x) => - let - val st = St.lookupStrById st m - val st = foldl St.lookupStrByName st ms - in - case St.lookupConByName st x of - St.CNormal n => (L'.CNamed n, loc) - | St.CFfi m => (L'.CFfi (m, x), loc) - end + | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) => + (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc) + | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c, + {field = corifyCon st field, rest = corifyCon st rest}), loc) + | L.ECut (e1, c, {field, rest}) => (L'.ECut (corifyExp st e1, corifyCon st c, + {field = corifyCon st field, rest = corifyCon st rest}), loc) + | L.EFold k => (L'.EFold (corifyKind k), loc) - | L.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc) - | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon st c), loc) + | L.ECase (e, pes, {disc, result}) => + (L'.ECase (corifyExp st e, + map (fn (p, e) => (corifyPat st p, corifyExp st e)) pes, + {disc = corifyCon st disc, result = corifyCon st result}), + loc) - | L.CName s => (L'.CName s, loc) + | L.EWrite e => (L'.EWrite (corifyExp st e), loc) - | L.CRecord (k, xcs) => - (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc) - | L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc) - | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc) - | L.CUnit => (L'.CUnit, loc) + fun corifyDecl ((d, loc : EM.span), st) = + case d of + L.DCon (x, n, k, c) => + let + val (st, n) = St.bindCon st x n + in + ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st) + end + | L.DDatatype (x, n, xncs) => + let + val (st, n) = St.bindCon st x n + val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => + let + val st = St.bindConstructor st x n (L'.PConVar n) + val st = St.bindConstructorVal st x n + val co = Option.map (corifyCon st) co + in + ((x, n, co), st) + end) st xncs -fun corifyPatCon st pc = - case pc of - L.PConVar n => St.lookupConstructorById st n - | L.PConProj (m1, ms, x) => - let - val st = St.lookupStrById st m1 - val st = foldl St.lookupStrByName st ms - in - St.lookupConstructorByName st x - end + val dk = CoreUtil.classifyDatatype xncs + val t = (L'.CNamed n, loc) + val dcons = map (fn (x, n, to) => + let + val (e, t) = + case to of + NONE => ((L'.ECon (dk, L'.PConVar n, NONE), loc), t) + | SOME t' => ((L'.EAbs ("x", t', t, + (L'.ECon (dk, L'.PConVar n, SOME (L'.ERel 0, loc)), + loc)), + loc), + (L'.TFun (t', t), loc)) + in + (L'.DVal (x, n, t, e, ""), loc) + end) xncs + in + ((L'.DDatatype (x, n, xncs), loc) :: dcons, st) + end + | L.DDatatypeImp (x, n, m1, ms, s, xncs) => + let + val (st, n) = St.bindCon st x n + val c = corifyCon st (L.CModProj (m1, ms, s), loc) -fun corifyPat st (p, loc) = - case p of - L.PWild => (L'.PWild, loc) - | L.PVar (x, t) => (L'.PVar (x, corifyCon st t), loc) - | L.PPrim p => (L'.PPrim p, loc) - | L.PCon (pc, po) => (L'.PCon (corifyPatCon st pc, Option.map (corifyPat st) po), loc) - | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, corifyPat st p, corifyCon st t)) xps), loc) + val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms + val (_, {inner, ...}) = corifyStr (m, st) -fun corifyExp st (e, loc) = - case e of - L.EPrim p => (L'.EPrim p, loc) - | L.ERel n => (L'.ERel n, loc) - | L.ENamed n => - (case St.lookupValById st n of - NONE => (L'.ENamed n, loc) - | SOME n => (L'.ENamed n, loc)) - | L.EModProj (m, ms, x) => - let - val st = St.lookupStrById st m - val st = foldl St.lookupStrByName st ms - in - case St.lookupConstructorByNameOpt st x of - SOME (pc as L'.PConFfi {mod = m, datatyp, arg, ...}) => - (case arg of - NONE => (L'.ECon (pc, NONE), loc) - | SOME dom => (L'.EAbs ("x", dom, (L'.CFfi (m, datatyp), loc), - (L'.ECon (pc, SOME (L'.ERel 0, loc)), loc)), loc)) - | _ => - case St.lookupValByName st x of - St.ENormal n => (L'.ENamed n, loc) - | St.EFfi (m, t) => - case t of - (L'.TFun (dom as (L'.TRecord (L'.CRecord (_, []), _), _), ran), _) => - (L'.EAbs ("arg", dom, ran, (L'.EFfiApp (m, x, []), loc)), loc) - | t as (L'.TFun _, _) => - let - fun getArgs (all as (t, _), args) = - case t of - L'.TFun (dom, ran) => getArgs (ran, dom :: args) - | _ => (all, rev args) - - val (result, args) = getArgs (t, []) + val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => + let + val n' = St.lookupConstructorByName inner x + val st = St.bindConstructor st x n n' + val (st, n) = St.bindVal st x n + val co = Option.map (corifyCon st) co + in + ((x, n, co), st) + end) st xncs - val (actuals, _) = foldr (fn (_, (actuals, n)) => - ((L'.ERel n, loc) :: actuals, - n + 1)) ([], 0) args - val app = (L'.EFfiApp (m, x, actuals), loc) - val (abs, _, _) = foldr (fn (t, (abs, ran, n)) => - ((L'.EAbs ("arg" ^ Int.toString n, - t, - ran, - abs), loc), - (L'.TFun (t, ran), loc), - n - 1)) (app, result, length args - 1) args - in - abs - end - | _ => (L'.EFfi (m, x), loc) - end - | L.EApp (e1, e2) => (L'.EApp (corifyExp st e1, corifyExp st e2), loc) - | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon st dom, corifyCon st ran, corifyExp st e1), loc) - | L.ECApp (e1, c) => (L'.ECApp (corifyExp st e1, corifyCon st c), loc) - | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc) + val cds = map (fn (x, n, co) => + let + val t = case co of + NONE => c + | SOME t' => (L'.TFun (t', c), loc) + val e = corifyExp st (L.EModProj (m1, ms, x), loc) + in + (L'.DVal (x, n, t, e, x), loc) + end) xncs + in + ((L'.DCon (x, n, (L'.KType, loc), c), loc) :: cds, st) + end + | L.DVal (x, n, t, e) => + let + val (st, n) = St.bindVal st x n + val s = + if String.isPrefix "wrap_" x then + String.extract (x, 5, NONE) + else + x + in + ([(L'.DVal (x, n, corifyCon st t, corifyExp st e, s), loc)], st) + end + | L.DValRec vis => + let + val (vis, st) = ListUtil.foldlMap + (fn ((x, n, t, e), st) => + let + val (st, n) = St.bindVal st x n + in + ((x, n, t, e), st) + end) + st vis - | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) => - (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc) - | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c, - {field = corifyCon st field, rest = corifyCon st rest}), loc) - | L.ECut (e1, c, {field, rest}) => (L'.ECut (corifyExp st e1, corifyCon st c, - {field = corifyCon st field, rest = corifyCon st rest}), loc) - | L.EFold k => (L'.EFold (corifyKind k), loc) + val vis = map + (fn (x, n, t, e) => + let + val s = + if String.isPrefix "wrap_" x then + String.extract (x, 5, NONE) + else + x + in + (x, n, corifyCon st t, corifyExp st e, s) + end) + vis + in + ([(L'.DValRec vis, loc)], st) + end + | L.DSgn _ => ([], st) - | L.ECase (e, pes, {disc, result}) => - (L'.ECase (corifyExp st e, - map (fn (p, e) => (corifyPat st p, corifyExp st e)) pes, - {disc = corifyCon st disc, result = corifyCon st result}), - loc) + | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) => + ([], St.bindFunctor st x n xa na str) - | L.EWrite e => (L'.EWrite (corifyExp st e), loc) + | L.DStr (x, n, _, str) => + let + val (ds, {inner, outer}) = corifyStr (str, st) + val st = St.bindStr outer x n inner + in + (ds, st) + end -fun corifyDecl ((d, loc : EM.span), st) = - case d of - L.DCon (x, n, k, c) => - let - val (st, n) = St.bindCon st x n - in - ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st) - end - | L.DDatatype (x, n, xncs) => - let - val (st, n) = St.bindCon st x n - val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => - let - val st = St.bindConstructor st x n (L'.PConVar n) - val st = St.bindConstructorVal st x n - val co = Option.map (corifyCon st) co - in - ((x, n, co), st) - end) st xncs + | L.DFfiStr (m, n, (sgn, _)) => + (case sgn of + L.SgnConst sgis => + let + val (ds, cmap, conmap, st) = + foldl (fn ((sgi, _), (ds, cmap, conmap, st)) => + case sgi of + L.SgiConAbs (x, n, k) => + let + val (st, n') = St.bindCon st x n + in + ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, + cmap, + conmap, + st) + end + | L.SgiCon (x, n, k, _) => + let + val (st, n') = St.bindCon st x n + in + ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, + cmap, + conmap, + st) + end - val t = (L'.CNamed n, loc) - val dcons = map (fn (x, n, to) => - let - val (e, t) = - case to of - NONE => ((L'.ECon (L'.PConVar n, NONE), loc), t) - | SOME t' => ((L'.EAbs ("x", t', t, - (L'.ECon (L'.PConVar n, SOME (L'.ERel 0, loc)), loc)), - loc), - (L'.TFun (t', t), loc)) - in - (L'.DVal (x, n, t, e, ""), loc) - end) xncs - in - ((L'.DDatatype (x, n, xncs), loc) :: dcons, st) - end - | L.DDatatypeImp (x, n, m1, ms, s, xncs) => - let - val (st, n) = St.bindCon st x n - val c = corifyCon st (L.CModProj (m1, ms, s), loc) + | L.SgiDatatype (x, n, xnts) => + let + val dk = ExplUtil.classifyDatatype xnts + val (st, n') = St.bindCon st x n + val (xnts, (ds', st, cmap, conmap)) = + ListUtil.foldlMap + (fn ((x', n, to), (ds', st, cmap, conmap)) => + let + val dt = (L'.CNamed n', loc) - val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms - val (_, {inner, ...}) = corifyStr (m, st) + val to = Option.map (corifyCon st) to - val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => - let - val n' = St.lookupConstructorByName inner x - val st = St.bindConstructor st x n n' - val (st, n) = St.bindVal st x n - val co = Option.map (corifyCon st) co - in - ((x, n, co), st) - end) st xncs - - val cds = map (fn (x, n, co) => - let - val t = case co of - NONE => c - | SOME t' => (L'.TFun (t', c), loc) - val e = corifyExp st (L.EModProj (m1, ms, x), loc) - in - (L'.DVal (x, n, t, e, x), loc) - end) xncs - in - ((L'.DCon (x, n, (L'.KType, loc), c), loc) :: cds, st) - end - | L.DVal (x, n, t, e) => - let - val (st, n) = St.bindVal st x n - val s = - if String.isPrefix "wrap_" x then - String.extract (x, 5, NONE) - else - x - in - ([(L'.DVal (x, n, corifyCon st t, corifyExp st e, s), loc)], st) - end - | L.DValRec vis => - let - val (vis, st) = ListUtil.foldlMap - (fn ((x, n, t, e), st) => - let - val (st, n) = St.bindVal st x n - in - ((x, n, t, e), st) - end) - st vis + val pc = L'.PConFfi {mod = m, + datatyp = x, + con = x', + arg = to, + kind = dk} - val vis = map - (fn (x, n, t, e) => - let - val s = - if String.isPrefix "wrap_" x then - String.extract (x, 5, NONE) - else - x - in - (x, n, corifyCon st t, corifyExp st e, s) - end) - vis - in - ([(L'.DValRec vis, loc)], st) - end - | L.DSgn _ => ([], st) - - | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) => - ([], St.bindFunctor st x n xa na str) - - | L.DStr (x, n, _, str) => - let - val (ds, {inner, outer}) = corifyStr (str, st) - val st = St.bindStr outer x n inner - in - (ds, st) - end - - | L.DFfiStr (m, n, (sgn, _)) => - (case sgn of - L.SgnConst sgis => - let - val (ds, cmap, conmap, st) = - foldl (fn ((sgi, _), (ds, cmap, conmap, st)) => - case sgi of - L.SgiConAbs (x, n, k) => - let - val (st, n') = St.bindCon st x n - in - ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, - cmap, - conmap, - st) - end - | L.SgiCon (x, n, k, _) => - let - val (st, n') = St.bindCon st x n - in - ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, - cmap, - conmap, - st) - end - - | L.SgiDatatype (x, n, xnts) => - let - val (st, n') = St.bindCon st x n - val (xnts, (ds', st, cmap, conmap)) = - ListUtil.foldlMap - (fn ((x', n, to), (ds', st, cmap, conmap)) => - let - val dt = (L'.CNamed n', loc) - - val to = Option.map (corifyCon st) to - - val pc = L'.PConFfi {mod = m, - datatyp = x, - con = x', - arg = to} - - val (cmap, d) = - case to of - NONE => (SM.insert (cmap, x', dt), - (L'.DVal (x', n, dt, - (L'.ECon (pc, NONE), loc), - ""), loc)) - | SOME t => - let - val tf = (L'.TFun (t, dt), loc) - val d = (L'.DVal (x', n, tf, - (L'.EAbs ("x", t, tf, - (L'.ECon (pc, - SOME (L'.ERel 0, + val (cmap, d) = + case to of + NONE => (SM.insert (cmap, x', dt), + (L'.DVal (x', n, dt, + (L'.ECon (dk, pc, NONE), loc), + ""), loc)) + | SOME t => + let + val tf = (L'.TFun (t, dt), loc) + val d = (L'.DVal (x', n, tf, + (L'.EAbs ("x", t, tf, + (L'.ECon (dk, pc, + SOME (L'.ERel 0, loc)), loc)), loc), ""), loc) in @@ -684,7 +688,7 @@ val st = St.bindConstructor st x' n pc (*val st = St.bindConstructorVal st x' n*) - val conmap = SM.insert (conmap, x', (x, to)) + val conmap = SM.insert (conmap, x', (x, to, dk)) in ((x', n, to), (d :: ds', st, cmap, conmap))