Mercurial > urweb
changeset 194:df5fd8f6913a
A multi-parameter datatype all the way through
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 09 Aug 2008 08:47:36 -0400 (2008-08-09) |
parents | 8a70e2919e86 |
children | 85b5f663bb86 |
files | src/core_print.sml src/corify.sml src/elaborate.sml src/specialize.sml tests/datatypeP2.lac |
diffstat | 5 files changed, 62 insertions(+), 33 deletions(-) [+] |
line wrap: on
line diff
--- a/src/core_print.sml Fri Aug 08 17:55:51 2008 -0400 +++ b/src/core_print.sml Sat Aug 09 08:47:36 2008 -0400 @@ -199,13 +199,15 @@ string (#1 (E.lookupERel env n))) handle E.UnboundRel _ => string ("UNBOUND_" ^ Int.toString n)) | ENamed n => p_enamed env n - | ECon (_, pc, _, NONE) => box [string "[", - p_patCon env pc, - string "]"] - | ECon (_, pc, _, SOME e) => box [string "[", + | ECon (_, pc, ts, NONE) => box [string "[", + p_patCon env pc, + p_list_sep (box []) (fn t => box [space, string "[", p_con env t, string "]"]) ts, + string "]"] + | ECon (_, pc, ts, SOME e) => box [string "[", p_patCon env pc, space, p_exp' true env e, + p_list_sep (box []) (fn t => box [space, string "[", p_con env t, string "]"]) ts, string "]"] | EFfi (m, x) => box [string "FFI(", string m, string ".", string x, string ")"] | EFfiApp (m, x, es) => box [string "FFI(",
--- a/src/corify.sml Fri Aug 08 17:55:51 2008 -0400 +++ b/src/corify.sml Sat Aug 09 08:47:36 2008 -0400 @@ -534,11 +534,12 @@ val dk = CoreUtil.classifyDatatype xncs val t = (L'.CNamed n, loc) - val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel i, loc)), loc)) t xs + val nxs = length xs - 1 + val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs val k = (L'.KType, loc) val dcons = map (fn (x, n, to) => let - val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) xs + val args = ListUtil.mapi (fn (i, _) => (L'.CRel (nxs - i), loc)) xs val (e, t) = case to of NONE => ((L'.ECon (dk, L'.PConVar n, args, NONE), loc), t) @@ -575,7 +576,8 @@ ((x, n, co), st) end) st xncs - val c = ListUtil.foldli (fn (i, _, c) => (L'.CApp (c, (L'.CRel i, loc)), loc)) c xs + val nxs = length xs - 1 + val c = ListUtil.foldli (fn (i, _, c) => (L'.CApp (c, (L'.CRel (nxs - i), loc)), loc)) c xs val k = (L'.KType, loc) val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
--- a/src/elaborate.sml Fri Aug 08 17:55:51 2008 -0400 +++ b/src/elaborate.sml Sat Aug 09 08:47:36 2008 -0400 @@ -954,7 +954,8 @@ val k = (L'.KType, loc) val unifs = map (fn _ => cunif (loc, k)) xs - val t = ListUtil.foldli (fn (i, u, t) => subConInCon (i, u) t) t unifs + val nxs = length unifs - 1 + val t = ListUtil.foldli (fn (i, u, t) => subConInCon (nxs - i, u) t) t unifs val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs in ignore (checkPatCon (env, denv) p' pt t); @@ -1600,7 +1601,8 @@ val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs val (env, n) = E.pushCNamed env x k' NONE val t = (L'.CNamed n, loc) - val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel i, loc)), loc)) t xs + val nxs = length xs - 1 + val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs val (xcs, (used, env, gs)) = ListUtil.foldlMap @@ -2269,7 +2271,8 @@ val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs val (env, n) = E.pushCNamed env x k' NONE val t = (L'.CNamed n, loc) - val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel i, loc)), loc)) t xs + val nxs = length xs - 1 + val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs val (env', denv') = foldl (fn (x, (env', denv')) => (E.pushCRel env' x k,
--- a/src/specialize.sml Fri Aug 08 17:55:51 2008 -0400 +++ b/src/specialize.sml Sat Aug 09 08:47:36 2008 -0400 @@ -77,10 +77,13 @@ SOME dt' => (#name dt', #constructors dt', st) | NONE => let + (*val () = Print.prefaces "Args" [("args", Print.p_list (CorePrint.p_con CoreEnv.empty) args)]*) + val n' = #count st + val nxs = length args - 1 fun sub t = ListUtil.foldli (fn (i, arg, t) => - subConInCon (i, arg) t) t args + subConInCon (nxs - i, arg) t) t args val (cons, (count, cmap)) = ListUtil.foldlMap (fn ((x, n, to), (count, cmap)) => @@ -240,28 +243,32 @@ fun specialize file = let fun doDecl (all as (d, _), st : state) = - case d of - DDatatype (x, n, xs, xnts) => - ([all], {count = #count st, - datatypes = IM.insert (#datatypes st, n, - {name = x, - params = length xs, - constructors = xnts, - specializations = CM.empty}), - constructors = foldl (fn ((_, n', _), constructors) => - IM.insert (constructors, n', n)) - (#constructors st) xnts, - decls = []}) - | _ => - let - val (d, st) = specDecl st all - in - (rev (d :: #decls st), - {count = #count st, - datatypes = #datatypes st, - constructors = #constructors st, - decls = []}) - end + let + (*val () = Print.preface ("decl:", CorePrint.p_decl CoreEnv.empty all)*) + in + case d of + DDatatype (x, n, xs, xnts) => + ([all], {count = #count st, + datatypes = IM.insert (#datatypes st, n, + {name = x, + params = length xs, + constructors = xnts, + specializations = CM.empty}), + constructors = foldl (fn ((_, n', _), constructors) => + IM.insert (constructors, n', n)) + (#constructors st) xnts, + decls = []}) + | _ => + let + val (d, st) = specDecl st all + in + (rev (d :: #decls st), + {count = #count st, + datatypes = #datatypes st, + constructors = #constructors st, + decls = []}) + end + end val (ds, _) = ListUtil.foldlMapConcat doDecl {count = U.File.maxName file + 1,
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/datatypeP2.lac Sat Aug 09 08:47:36 2008 -0400 @@ -0,0 +1,15 @@ +datatype sum a b = Left of a | Right of b + +val l : sum int string = Left 5 +val r : sum int string = Right "Hi" + +val show = fn x : sum int string => case x of Left _ => "Left _" | Right s => s + +val page = fn x => <html><body> + {cdata (show x)} +</body></html> + +val main : unit -> page = fn () => <html><body> + <li><a link={page l}>Left</a></li> + <li><a link={page r}>Right</a></li> +</body></html>