Mercurial > urweb
changeset 177:5d030ee143e2
Case through corify
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 02 Aug 2008 11:15:32 -0400 |
| parents | 33d4a8eea484 |
| children | eb3f9913bf31 |
| files | src/core.sml src/core_env.sig src/core_env.sml src/core_print.sml src/core_util.sml src/corify.sml src/monoize.sml tests/caseMod.lac |
| diffstat | 8 files changed, 247 insertions(+), 22 deletions(-) [+] |
line wrap: on
line diff
--- a/src/core.sml Thu Jul 31 16:28:55 2008 -0400 +++ b/src/core.sml Sat Aug 02 11:15:32 2008 -0400 @@ -59,10 +59,24 @@ withtype con = con' located +datatype patCon = + PConVar of int + | PConFfi of string * string + +datatype pat' = + PWild + | PVar of string + | PPrim of Prim.t + | PCon of patCon * pat option + | PRecord of (string * pat) list + +withtype pat = pat' located + datatype exp' = EPrim of Prim.t | ERel of int | ENamed of int + | ECon of int * exp option | EFfi of string * string | EFfiApp of string * string * exp list | EApp of exp * exp @@ -75,6 +89,8 @@ | ECut of exp * con * { field : con, rest : con } | EFold of kind + | ECase of exp * (pat * exp) list * con + | EWrite of exp | EClosure of int * exp list
--- a/src/core_env.sig Thu Jul 31 16:28:55 2008 -0400 +++ b/src/core_env.sig Sat Aug 02 11:15:32 2008 -0400 @@ -45,6 +45,8 @@ val pushDatatype : env -> string -> int -> (string * int * Core.con option) list -> env val lookupDatatype : env -> int -> string * (string * int * Core.con option) list + val lookupConstructor : env -> int -> string * Core.con option * int + val pushERel : env -> string -> Core.con -> env val lookupERel : env -> int -> string * Core.con
--- a/src/core_env.sml Thu Jul 31 16:28:55 2008 -0400 +++ b/src/core_env.sml Sat Aug 02 11:15:32 2008 -0400 @@ -62,6 +62,7 @@ namedC : (string * kind * con option) IM.map, datatypes : (string * (string * int * con option) list) IM.map, + constructors : (string * con option * int) IM.map, relE : (string * con) list, namedE : (string * con * exp option * string) IM.map @@ -72,6 +73,7 @@ namedC = IM.empty, datatypes = IM.empty, + constructors = IM.empty, relE = [], namedE = IM.empty @@ -82,6 +84,7 @@ namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), datatypes = #datatypes env, + constructors = #constructors env, relE = map (fn (x, c) => (x, lift c)) (#relE env), namedE = IM.map (fn (x, c, eo, s) => (x, lift c, eo, s)) (#namedE env)} @@ -95,6 +98,7 @@ namedC = IM.insert (#namedC env, n, (x, k, co)), datatypes = #datatypes env, + constructors = #constructors env, relE = #relE env, namedE = #namedE env} @@ -109,6 +113,9 @@ namedC = #namedC env, datatypes = IM.insert (#datatypes env, n, (x, xncs)), + constructors = foldl (fn ((x, n, to), constructors) => + IM.insert (constructors, n, (x, to, n))) + (#constructors env) xncs, relE = #relE env, namedE = #namedE env} @@ -118,11 +125,17 @@ NONE => raise UnboundNamed n | SOME x => x +fun lookupConstructor (env : env) n = + case IM.find (#constructors env, n) of + NONE => raise UnboundNamed n + | SOME x => x + fun pushERel (env : env) x t = {relC = #relC env, namedC = #namedC env, datatypes = #datatypes env, + constructors = #constructors env, relE = (x, t) :: #relE env, namedE = #namedE env} @@ -136,6 +149,7 @@ namedC = #namedC env, datatypes = #datatypes env, + constructors = #constructors env, relE = #relE env, namedE = IM.insert (#namedE env, n, (x, t, eo, s))}
--- a/src/core_print.sml Thu Jul 31 16:28:55 2008 -0400 +++ b/src/core_print.sml Sat Aug 02 11:15:32 2008 -0400 @@ -152,6 +152,43 @@ string (#1 (E.lookupENamed env n))) handle E.UnboundNamed _ => string ("UNBOUNDN_" ^ Int.toString n) +fun p_con_named env n = + (if !debug then + string (#1 (E.lookupConstructor env n) ^ "__" ^ Int.toString n) + else + string (#1 (E.lookupConstructor env n))) + handle E.UnboundNamed _ => string ("CONSTRUCTOR_" ^ Int.toString n) + +fun p_patCon env pc = + case pc of + PConVar n => p_con_named env n + | PConFfi (m, x) => box [string "FFI(", + string m, + string ".", + string x, + string ")"] + +fun p_pat' par env (p, _) = + case p of + PWild => string "_" + | PVar s => string s + | PPrim p => Prim.p_t p + | PCon (n, NONE) => p_patCon env n + | PCon (n, SOME p) => parenIf par (box [p_patCon env n, + space, + p_pat' true env p]) + | PRecord xps => + box [string "{", + p_list_sep (box [string ",", space]) (fn (x, p) => + box [string x, + space, + string "=", + space, + p_pat env p]) xps, + string "}"] + +and p_pat x = p_pat' false x + fun p_exp' par env (e, _) = case e of EPrim p => Prim.p_t p @@ -162,6 +199,10 @@ string (#1 (E.lookupERel env n))) handle E.UnboundRel _ => string ("UNBOUND_" ^ Int.toString n)) | ENamed n => p_enamed env n + | ECon (n, NONE) => p_con_named env n + | ECon (n, SOME e) => parenIf par (box [p_con_named env n, + space, + p_exp' true env e]) | EFfi (m, x) => box [string "FFI(", string m, string ".", string x, string ")"] | EFfiApp (m, x, es) => box [string "FFI(", string m, @@ -249,6 +290,19 @@ p_con' true env c]) | EFold _ => string "fold" + | ECase (e, pes, _) => parenIf par (box [string "case", + space, + p_exp env e, + space, + string "of", + space, + p_list_sep (box [space, string "|", space]) + (fn (p, e) => box [p_pat env p, + space, + string "=>", + space, + p_exp env e]) pes]) + | EWrite e => box [string "write(", p_exp env e, string ")"]
--- a/src/core_util.sml Thu Jul 31 16:28:55 2008 -0400 +++ b/src/core_util.sml Sat Aug 02 11:15:32 2008 -0400 @@ -227,6 +227,11 @@ EPrim _ => S.return2 eAll | ERel _ => S.return2 eAll | ENamed _ => S.return2 eAll + | ECon (_, NONE) => S.return2 eAll + | ECon (n, SOME e) => + S.map2 (mfe ctx e, + fn e' => + (ECon (n, SOME e'), loc)) | EFfi _ => S.return2 eAll | EFfiApp (m, x, es) => S.map2 (ListUtil.mapfold (fn e => mfe ctx e) es, @@ -297,6 +302,17 @@ fn k' => (EFold k', loc)) + | ECase (e, pes, t) => + S.bind2 (mfe ctx e, + fn e' => + S.bind2 (ListUtil.mapfold (fn (p, e) => + S.map2 (mfe ctx e, + fn e' => (p, e'))) pes, + fn pes' => + S.map2 (mfc ctx t, + fn t' => + (ECase (e', pes', t'), loc)))) + | EWrite e => S.map2 (mfe ctx e, fn e' =>
--- a/src/corify.sml Thu Jul 31 16:28:55 2008 -0400 +++ b/src/corify.sml Sat Aug 02 11:15:32 2008 -0400 @@ -71,11 +71,15 @@ val lookupConById : t -> int -> int option val lookupConByName : t -> string -> core_con + val bindConstructor : t -> string -> int -> L'.patCon -> t + 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 bindConstructor : t -> string -> int -> t + val bindConstructorVal : t -> string -> int -> t val lookupValById : t -> int -> int option val lookupValByName : t -> string -> core_val @@ -90,6 +94,7 @@ 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} @@ -98,6 +103,7 @@ 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, @@ -107,15 +113,17 @@ val empty = { cons = IM.empty, + constructors = IM.empty, vals = IM.empty, strs = IM.empty, funs = IM.empty, - current = FNormal { cons = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty }, + current = FNormal { cons = SM.empty, constructors = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty }, nested = [] } -fun debug ({current = FNormal {cons, vals, strs, funs}, ...} : t) = +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") @@ -129,20 +137,22 @@ ENormal of int | EFfi of string * L'.con -fun bindCon {cons, vals, strs, funs, current, nested} s 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, vals, strs, funs} => + | 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, @@ -161,20 +171,22 @@ NONE => raise Fail "Corify.St.lookupConByName" | SOME n => CNormal n -fun bindVal {cons, vals, strs, funs, current, nested} s 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, vals, strs, funs} => + | 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, @@ -183,18 +195,20 @@ n') end -fun bindConstructor {cons, vals, strs, funs, current, nested} s n = +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, vals, strs, funs} => + | 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, @@ -202,6 +216,7 @@ nested = nested} end + fun lookupValById ({vals, ...} : t) n = IM.find (vals, n) fun lookupValByName ({current, ...} : t) x = @@ -215,26 +230,64 @@ NONE => raise Fail "Corify.St.lookupValByName" | SOME n => ENormal n -fun enter {cons, vals, strs, funs, current, nested} = +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 lookupConstructorById ({constructors, ...} : t) n = + case IM.find (constructors, n) of + NONE => raise Fail "Corify.St.lookupConstructorById" + | SOME x => x + +fun lookupConstructorByName ({current, ...} : t) x = + case current of + FFfi {mod = m, ...} => L'.PConFfi (m, x) + | FNormal {constructors, ...} => + case SM.find (constructors, x) of + NONE => raise Fail "Corify.St.lookupConstructorByName" + | SOME n => n + +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 dummy f = {cons = IM.empty, + constructors = IM.empty, vals = IM.empty, strs = IM.empty, funs = IM.empty, current = f, nested = []} -fun leave {cons, vals, strs, funs, current, nested = m1 :: rest} = +fun leave {cons, constructors, vals, strs, funs, current, nested = m1 :: rest} = {outer = {cons = cons, + constructors = constructors, vals = vals, strs = strs, funs = funs, @@ -245,14 +298,17 @@ fun ffi m vals = dummy (FFfi {mod = m, vals = vals}) -fun bindStr ({cons, vals, strs, funs, - current = FNormal {cons = mcons, vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) +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}, @@ -270,14 +326,17 @@ | SOME f => dummy f) | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName" -fun bindFunctor ({cons, vals, strs, funs, - current = FNormal {cons = mcons, vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) +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))}, @@ -338,6 +397,25 @@ | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc) | L.CUnit => (L'.CUnit, loc) +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 + +fun corifyPat st (p, loc) = + case p of + L.PWild => (L'.PWild, loc) + | L.PVar x => (L'.PVar x, 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) => (x, corifyPat st p)) xps), loc) + fun corifyExp st (e, loc) = case e of L.EPrim p => (L'.EPrim p, loc) @@ -394,7 +472,12 @@ | 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.ECase _ => raise Fail "Corify ECase" + + | L.ECase (e, pes, t) => (L'.ECase (corifyExp st e, + map (fn (p, e) => (corifyPat st p, corifyExp st e)) pes, + corifyCon st t), + loc) + | L.EWrite e => (L'.EWrite (corifyExp st e), loc) fun corifyDecl ((d, loc : EM.span), st) = @@ -410,27 +493,47 @@ 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 + 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 + + val t = (L'.CNamed n, loc) + val dcons = map (fn (x, n, to) => + let + val (e, t) = + case to of + NONE => ((L'.ECon (n, NONE), loc), t) + | SOME t' => ((L'.EAbs ("x", t', t, + (L'.ECon (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)], st) + ((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) + val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms + val (_, {inner, ...}) = corifyStr (m, st) + 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
--- a/src/monoize.sml Thu Jul 31 16:28:55 2008 -0400 +++ b/src/monoize.sml Sat Aug 02 11:15:32 2008 -0400 @@ -171,6 +171,7 @@ L.EPrim p => (L'.EPrim p, loc) | L.ERel n => (L'.ERel n, loc) | L.ENamed n => (L'.ENamed n, loc) + | L.ECon _ => raise Fail "Monoize ECon" | L.EFfi mx => (L'.EFfi mx, loc) | L.EFfiApp (m, x, es) => (L'.EFfiApp (m, x, map (monoExp (env, st)) es), loc) @@ -448,6 +449,9 @@ | L.EField (e, x, _) => (L'.EField (monoExp (env, st) e, monoName env x), loc) | L.ECut _ => poly () | L.EFold _ => poly () + + | L.ECase _ => raise Fail "Monoize ECase" + | L.EWrite e => (L'.EWrite (monoExp (env, st) e), loc) | L.EClosure (n, es) => (L'.EClosure (n, map (monoExp (env, st)) es), loc)
--- a/tests/caseMod.lac Thu Jul 31 16:28:55 2008 -0400 +++ b/tests/caseMod.lac Sat Aug 02 11:15:32 2008 -0400 @@ -9,11 +9,27 @@ val g = fn x : t => case x of M.A => B | B => M.A structure N = struct - datatype t = C of t | D + datatype u = C of t | D end -val h = fn x : N.t => case x of N.C x => x | N.D => M.A +val h = fn x : N.u => case x of N.C x => x | N.D => M.A -datatype u = datatype N.t +datatype u = datatype N.u val i = fn x : u => case x of N.C x => x | D => M.A + +val toString = fn x => + case x of + C A => "C A" + | C B => "C B" + | D => "D" + +val page = fn x => <html><body> + {cdata (toString x)} +</body></html> + +val main : unit -> page = fn () => <html><body> + <li> <a link={page (C A)}>C A</a></li> + <li> <a link={page (C B)}>C B</a></li> + <li> <a link={page D}>D</a></li> +</body></html>