# HG changeset patch # User Adam Chlipala # Date 1214494349 14400 # Node ID 8b611ecc5f2d47ef32ec9f15e24633d0a2aa8494 # Parent 0ee10f4d73cf92b3e8d26993c3aa10a0b2a10798 Corify efold diff -r 0ee10f4d73cf -r 8b611ecc5f2d src/core.sml --- a/src/core.sml Thu Jun 26 11:11:13 2008 -0400 +++ b/src/core.sml Thu Jun 26 11:32:29 2008 -0400 @@ -69,6 +69,7 @@ | ERecord of (con * exp * con) list | EField of exp * con * { field : con, rest : con } + | EFold of kind withtype exp = exp' located diff -r 0ee10f4d73cf -r 8b611ecc5f2d src/core_print.sml --- a/src/core_print.sml Thu Jun 26 11:11:13 2008 -0400 +++ b/src/core_print.sml Thu Jun 26 11:32:29 2008 -0400 @@ -222,6 +222,7 @@ box [p_exp' true env e, string ".", p_con' true env c] + | EFold _ => string "fold" and p_exp env = p_exp' false env diff -r 0ee10f4d73cf -r 8b611ecc5f2d src/core_util.sml --- a/src/core_util.sml Thu Jun 26 11:11:13 2008 -0400 +++ b/src/core_util.sml Thu Jun 26 11:32:29 2008 -0400 @@ -278,6 +278,10 @@ S.map2 (mfc ctx rest, fn rest' => (EField (e', c', {field = field', rest = rest'}), loc))))) + | EFold k => + S.map2 (mfk k, + fn k' => + (EFold k', loc)) in mfe end diff -r 0ee10f4d73cf -r 8b611ecc5f2d src/corify.sml --- a/src/corify.sml Thu Jun 26 11:11:13 2008 -0400 +++ b/src/corify.sml Thu Jun 26 11:32:29 2008 -0400 @@ -62,13 +62,19 @@ val leave : t -> {outer : t, inner : t} val ffi : string -> L'.con SM.map -> t - val bindCore : t -> string -> int -> t * int - val lookupCoreById : t -> int -> int option + datatype core_con = + CNormal of int + | CFfi of string + val bindCon : t -> string -> int -> t * int + val lookupConById : t -> int -> int option + val lookupConByName : t -> string -> core_con - datatype core = - Normal of int - | Ffi of string * L'.con option - val lookupCoreByName : t -> string -> core + datatype core_val = + ENormal of int + | EFfi of string * L'.con + val bindVal : t -> string -> int -> t * int + val lookupValById : t -> int -> int option + val lookupValByName : t -> string -> core_val val bindStr : t -> string -> int -> t -> t val lookupStrById : t -> int -> t @@ -80,13 +86,16 @@ end = struct datatype flattening = - FNormal of {core : int SM.map, + FNormal of {cons : int SM.map, + vals : int SM.map, strs : flattening SM.map, funs : (int * L.str) SM.map} - | FFfi of string * L'.con SM.map + | FFfi of {mod : string, + vals : L'.con SM.map} type t = { - core : int IM.map, + cons : int IM.map, + vals : int IM.map, strs : flattening IM.map, funs : (int * L.str) IM.map, current : flattening, @@ -94,30 +103,37 @@ } val empty = { - core = IM.empty, + cons = IM.empty, + vals = IM.empty, strs = IM.empty, funs = IM.empty, - current = FNormal { core = SM.empty, strs = SM.empty, funs = SM.empty }, + current = FNormal { cons = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty }, nested = [] } -datatype core = - Normal of int - | Ffi of string * L'.con option +datatype core_con = + CNormal of int + | CFfi of string -fun bindCore {core, strs, funs, current, nested} s n = +datatype core_val = + ENormal of int + | EFfi of string * L'.con + +fun bindCon {cons, vals, strs, funs, current, nested} s n = let val n' = alloc () val current = case current of FFfi _ => raise Fail "Binding inside FFfi" - | FNormal {core, strs, funs} => - FNormal {core = SM.insert (core, s, n'), + | FNormal {cons, vals, strs, funs} => + FNormal {cons = SM.insert (cons, s, n'), + vals = vals, strs = strs, funs = funs} in - ({core = IM.insert (core, n, n'), + ({cons = IM.insert (cons, n, n'), + vals = vals, strs = strs, funs = funs, current = current, @@ -125,33 +141,72 @@ n') end -fun lookupCoreById ({core, ...} : t) n = IM.find (core, n) +fun lookupConById ({cons, ...} : t) n = IM.find (cons, n) -fun lookupCoreByName ({current, ...} : t) x = +fun lookupConByName ({current, ...} : t) x = case current of - FFfi (m, cmap) => Ffi (m, SM.find (cmap, x)) - | FNormal {core, ...} => - case SM.find (core, x) of - NONE => raise Fail "Corify.St.lookupCoreByName" - | SOME n => Normal n + FFfi {mod = m, ...} => CFfi m + | FNormal {cons, ...} => + case SM.find (cons, x) of + NONE => raise Fail "Corify.St.lookupConByName" + | SOME n => CNormal n -fun enter {core, strs, funs, current, nested} = - {core = core, +fun bindVal {cons, vals, strs, funs, current, nested} s n = + let + val n' = alloc () + + val current = + case current of + FFfi _ => raise Fail "Binding inside FFfi" + | FNormal {cons, vals, strs, funs} => + FNormal {cons = cons, + vals = SM.insert (vals, s, n'), + strs = strs, + funs = funs} + in + ({cons = cons, + vals = IM.insert (vals, n, n'), + strs = strs, + funs = funs, + current = current, + nested = nested}, + n') + 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 enter {cons, vals, strs, funs, current, nested} = + {cons = cons, + vals = vals, strs = strs, funs = funs, - current = FNormal {core = SM.empty, + current = FNormal {cons = SM.empty, + vals = SM.empty, strs = SM.empty, funs = SM.empty}, nested = current :: nested} -fun dummy f = {core = IM.empty, +fun dummy f = {cons = IM.empty, + vals = IM.empty, strs = IM.empty, funs = IM.empty, current = f, nested = []} -fun leave {core, strs, funs, current, nested = m1 :: rest} = - {outer = {core = core, +fun leave {cons, vals, strs, funs, current, nested = m1 :: rest} = + {outer = {cons = cons, + vals = vals, strs = strs, funs = funs, current = m1, @@ -159,16 +214,19 @@ inner = dummy current} | leave _ = raise Fail "Corify.St.leave" -fun ffi m cmap = dummy (FFfi (m, cmap)) +fun ffi m vals = dummy (FFfi {mod = m, vals = vals}) -fun bindStr ({core, strs, funs, current = FNormal {core = mcore, strs = mstrs, funs = mfuns}, nested} : t) +fun bindStr ({cons, vals, strs, funs, + current = FNormal {cons = mcons, vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) x n ({current = f, ...} : t) = - {core = core, + {cons = cons, + vals = vals, strs = IM.insert (strs, n, f), funs = funs, - current = FNormal {core = mcore, - strs = SM.insert (mstrs, x, f), - funs = mfuns}, + current = FNormal {cons = mcons, + vals = mvals, + strs = SM.insert (mstrs, x, f), + funs = mfuns}, nested = nested} | bindStr _ _ _ _ = raise Fail "Corify.St.bindStr" @@ -183,12 +241,15 @@ | SOME f => dummy f) | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName" -fun bindFunctor ({core, strs, funs, current = FNormal {core = mcore, strs = mstrs, funs = mfuns}, nested} : t) +fun bindFunctor ({cons, vals, strs, funs, + current = FNormal {cons = mcons, vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) x n na str = - {core = core, + {cons = cons, + vals = vals, strs = strs, funs = IM.insert (funs, n, (na, str)), - current = FNormal {core = mcore, + current = FNormal {cons = mcons, + vals = mvals, strs = mstrs, funs = SM.insert (mfuns, x, (na, str))}, nested = nested} @@ -223,7 +284,7 @@ | L.CRel n => (L'.CRel n, loc) | L.CNamed n => - (case St.lookupCoreById st n of + (case St.lookupConById st n of NONE => (L'.CNamed n, loc) | SOME n => (L'.CNamed n, loc)) | L.CModProj (m, ms, x) => @@ -231,9 +292,9 @@ val st = St.lookupStrById st m val st = foldl St.lookupStrByName st ms in - case St.lookupCoreByName st x of - St.Normal n => (L'.CNamed n, loc) - | St.Ffi (m, _) => (L'.CFfi (m, x), loc) + case St.lookupConByName st x of + St.CNormal n => (L'.CNamed n, loc) + | St.CFfi m => (L'.CFfi (m, x), loc) end | L.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc) @@ -251,7 +312,7 @@ L.EPrim p => (L'.EPrim p, loc) | L.ERel n => (L'.ERel n, loc) | L.ENamed n => - (case St.lookupCoreById st n of + (case St.lookupValById st n of NONE => (L'.ENamed n, loc) | SOME n => (L'.ENamed n, loc)) | L.EModProj (m, ms, x) => @@ -259,10 +320,9 @@ val st = St.lookupStrById st m val st = foldl St.lookupStrByName st ms in - case St.lookupCoreByName st x of - St.Normal n => (L'.ENamed n, loc) - | St.Ffi (_, NONE) => raise Fail "corifyExp: Unknown type for FFI expression variable" - | St.Ffi (m, SOME t) => + 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) @@ -299,19 +359,19 @@ | 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.EFold _ => raise Fail "Corify EFold" + | L.EFold k => (L'.EFold (corifyKind k), loc) fun corifyDecl ((d, loc : EM.span), st) = case d of L.DCon (x, n, k, c) => let - val (st, n) = St.bindCore st x n + val (st, n) = St.bindCon st x n in ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st) end | L.DVal (x, n, t, e) => let - val (st, n) = St.bindCore st x n + val (st, n) = St.bindVal st x n in ([(L'.DVal (x, n, corifyCon st t, corifyExp st e), loc)], st) end @@ -338,7 +398,7 @@ case sgi of L.SgiConAbs (x, n, k) => let - val (st, n') = St.bindCore st x n + val (st, n') = St.bindCon st x n in ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, cmap, @@ -346,7 +406,7 @@ end | L.SgiCon (x, n, k, _) => let - val (st, n') = St.bindCore st x n + val (st, n') = St.bindCon st x n in ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, cmap, diff -r 0ee10f4d73cf -r 8b611ecc5f2d src/monoize.sml --- a/src/monoize.sml Thu Jun 26 11:11:13 2008 -0400 +++ b/src/monoize.sml Thu Jun 26 11:32:29 2008 -0400 @@ -97,6 +97,7 @@ | L.ERecord xes => (L'.ERecord (map (fn (x, e, t) => (monoName env x, monoExp env e, monoType env t)) xes), loc) | L.EField (e, x, _) => (L'.EField (monoExp env e, monoName env x), loc) + | L.EFold _ => poly () end fun monoDecl env (all as (d, loc)) = diff -r 0ee10f4d73cf -r 8b611ecc5f2d tests/efold.lac --- a/tests/efold.lac Thu Jun 26 11:11:13 2008 -0400 +++ b/tests/efold.lac Thu Jun 26 11:32:29 2008 -0400 @@ -4,3 +4,5 @@ val greenCurry : Cfold.greenCurry = currier [Cfold.greenCurryIngredients] val redCurry : Cfold.redCurry = currier [Cfold.redCurryIngredients] val yellowCurry : Cfold.yellowCurry = currier [Cfold.yellowCurryIngredients] + +val main = yellowCurry