Mercurial > urweb
changeset 146:80ac94b54e41
Fix opening and corifying of functors
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 22 Jul 2008 18:20:13 -0400 |
| parents | b1b33f7cf555 |
| children | eb16f2aadbe9 |
| files | src/corify.sml src/elaborate.sml src/expl_print.sml tests/gform.lac tests/open_functor.lac |
| diffstat | 5 files changed, 127 insertions(+), 56 deletions(-) [+] |
line wrap: on
line diff
--- a/src/corify.sml Tue Jul 22 15:22:34 2008 -0400 +++ b/src/corify.sml Tue Jul 22 18:20:13 2008 -0400 @@ -58,6 +58,8 @@ val empty : t + val debug : t -> unit + val enter : t -> t val leave : t -> {outer : t, inner : t} val ffi : string -> L'.con SM.map -> t @@ -80,16 +82,16 @@ val lookupStrById : t -> int -> t val lookupStrByName : string * t -> t - val bindFunctor : t -> string -> int -> int -> L.str -> t - val lookupFunctorById : t -> int -> int * L.str - val lookupFunctorByName : string * t -> int * L.str + 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, vals : int SM.map, strs : flattening SM.map, - funs : (int * L.str) SM.map} + funs : (string * int * L.str) SM.map} | FFfi of {mod : string, vals : L'.con SM.map} @@ -97,7 +99,7 @@ cons : int IM.map, vals : int IM.map, strs : flattening IM.map, - funs : (int * L.str) IM.map, + funs : (string * int * L.str) IM.map, current : flattening, nested : flattening list } @@ -111,6 +113,13 @@ nested = [] } +fun debug ({current = FNormal {cons, vals, strs, funs}, ...} : t) = + print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; " + ^ "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_con = CNormal of int | CFfi of string @@ -243,17 +252,17 @@ fun bindFunctor ({cons, vals, strs, funs, current = FNormal {cons = mcons, vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) - x n na str = + x n xa na str = {cons = cons, vals = vals, strs = strs, - funs = IM.insert (funs, n, (na, str)), + funs = IM.insert (funs, n, (xa, na, str)), current = FNormal {cons = mcons, vals = mvals, strs = mstrs, - funs = SM.insert (mfuns, x, (na, str))}, + funs = SM.insert (mfuns, x, (xa, na, str))}, nested = nested} - | bindFunctor _ _ _ _ _ = raise Fail "Corify.St.bindFunctor" + | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor" fun lookupFunctorById ({funs, ...} : t) n = case IM.find (funs, n) of @@ -412,8 +421,8 @@ end | L.DSgn _ => ([], st) - | L.DStr (x, n, _, (L.StrFun (_, na, _, _, str), _)) => - ([], St.bindFunctor st x n na str) + | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) => + ([], St.bindFunctor st x n xa na str) | L.DStr (x, n, _, str) => let @@ -514,7 +523,6 @@ end end | _ => raise Fail "Non-const signature for 'export'") - and corifyStr ((str, _), st) = case str of @@ -547,12 +555,12 @@ | L.StrProj (str, x) => St.lookupFunctorByName (x, unwind' str) | _ => raise Fail "Corify of fancy functor application [2]" - val (na, body) = unwind str1 + val (xa, na, body) = unwind str1 - val (ds1, {inner, outer}) = corifyStr (str2, st) - val (ds2, sts) = corifyStr (body, St.bindStr outer "ARG" na inner) + val (ds1, {inner = inner', outer}) = corifyStr (str2, st) + val (ds2, {inner, outer}) = corifyStr (body, St.bindStr outer xa na inner') in - (ds1 @ ds2, sts) + (ds1 @ ds2, {inner = St.bindStr inner xa na inner', outer = outer}) end fun maxName ds = foldl (fn ((d, _), n) => @@ -577,6 +585,7 @@ fun corify ds = let val () = reset (maxName ds + 1) + val (ds, _) = ListUtil.foldlMapConcat corifyDecl St.empty ds in ds
--- a/src/elaborate.sml Tue Jul 22 15:22:34 2008 -0400 +++ b/src/elaborate.sml Tue Jul 22 18:20:13 2008 -0400 @@ -1988,41 +1988,42 @@ case #1 (hnormSgn env sgn) of L'.SgnConst sgis => let - fun doOne (all as (sgi, _)) = - case sgi of - L'.SgiVal (x, n, t) => - (case hnormCon (env, denv) t of - ((L'.TFun (dom, ran), _), []) => - (case (hnormCon (env, denv) dom, hnormCon (env, denv) ran) of - (((L'.TRecord domR, _), []), - ((L'.CApp (tf, arg3), _), [])) => - (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of - (((L'.CApp (tf, arg2), _), []), - (((L'.CRecord (_, []), _), []))) => - (case (hnormCon (env, denv) tf) of - ((L'.CApp (tf, arg1), _), []) => - (case (hnormCon (env, denv) tf, - hnormCon (env, denv) domR, - hnormCon (env, denv) arg2) of - ((tf, []), (domR, []), - ((L'.CRecord (_, []), _), [])) => - let - val t = (L'.CApp (tf, arg1), loc) - val t = (L'.CApp (t, arg2), loc) - val t = (L'.CApp (t, arg3), loc) - in - (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR, loc), - t), - loc)), loc) - end - | _ => all) - | _ => all) - | _ => all) - | _ => all) - | _ => all) - | _ => all + fun doOne (all as (sgi, _), env) = + (case sgi of + L'.SgiVal (x, n, t) => + (case hnormCon (env, denv) t of + ((L'.TFun (dom, ran), _), []) => + (case (hnormCon (env, denv) dom, hnormCon (env, denv) ran) of + (((L'.TRecord domR, _), []), + ((L'.CApp (tf, arg3), _), [])) => + (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of + (((L'.CApp (tf, arg2), _), []), + (((L'.CRecord (_, []), _), []))) => + (case (hnormCon (env, denv) tf) of + ((L'.CApp (tf, arg1), _), []) => + (case (hnormCon (env, denv) tf, + hnormCon (env, denv) domR, + hnormCon (env, denv) arg2) of + ((tf, []), (domR, []), + ((L'.CRecord (_, []), _), [])) => + let + val t = (L'.CApp (tf, arg1), loc) + val t = (L'.CApp (t, arg2), loc) + val t = (L'.CApp (t, arg3), loc) + in + (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR, loc), + t), + loc)), loc) + end + | _ => all) + | _ => all) + | _ => all) + | _ => all) + | _ => all) + | _ => all, + E.sgiBinds env all) in - (L'.SgnConst (map doOne sgis), loc) + (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc) end | _ => sgn in
--- a/src/expl_print.sml Tue Jul 22 15:22:34 2008 -0400 +++ b/src/expl_print.sml Tue Jul 22 18:20:13 2008 -0400 @@ -100,7 +100,7 @@ else m1x in - p_list_sep (string ".") string (m1x :: ms @ [x]) + p_list_sep (string ".") string (m1s :: ms @ [x]) end | CApp (c1, c2) => parenIf par (box [p_con env c1, @@ -155,7 +155,7 @@ CName s => string s | _ => p_con env all -fun p_exp' par env (e, _) = +fun p_exp' par env (e, loc) = case e of EPrim p => Prim.p_t p | ERel n => @@ -171,13 +171,14 @@ | EModProj (m1, ms, x) => let val (m1x, sgn) = E.lookupStrNamed env m1 + handle E.UnboundNamed _ => ("UNBOUND", (SgnConst [], loc)) val m1s = if !debug then m1x ^ "__" ^ Int.toString m1 else m1x in - p_list_sep (string ".") string (m1x :: ms @ [x]) + p_list_sep (string ".") string (m1s :: ms @ [x]) end | EApp (e1, e2) => parenIf par (box [p_exp env e1, @@ -294,7 +295,7 @@ space, p_sgn env sgn] -and p_sgn env (sgn, _) = +and p_sgn env (sgn, loc) = case sgn of SgnConst sgis => box [string "sig", newline, @@ -308,7 +309,8 @@ end, newline, string "end"] - | SgnVar n => string (#1 (E.lookupSgnNamed env n)) + | SgnVar n => string ((#1 (E.lookupSgnNamed env n)) + handle E.UnboundNamed _ => "UNBOUND") | SgnFun (x, n, sgn, sgn') => box [string "functor", space, string "(", @@ -336,6 +338,7 @@ | SgnProj (m1, ms, x) => let val (m1x, sgn) = E.lookupStrNamed env m1 + handle E.UnboundNamed _ => ("UNBOUND", (SgnConst [], loc)) val m1s = if !debug then m1x ^ "__" ^ Int.toString m1 @@ -424,7 +427,18 @@ p_file env ds, newline, string "end"] - | StrVar n => string (#1 (E.lookupStrNamed env n)) + | StrVar n => + let + val x = #1 (E.lookupStrNamed env n) + handle E.UnboundNamed _ => "UNBOUND" + + val s = if !debug then + x ^ "__" ^ Int.toString n + else + x + in + string s + end | StrProj (str, s) => box [p_str env str, string ".", string s]
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/gform.lac Tue Jul 22 18:20:13 2008 -0400 @@ -0,0 +1,31 @@ +con stringify = fold (fn nm :: Name => fn u :: Unit => fn t :: {Type} => [nm = string] ++ t) [] + +signature S = sig + con rs :: {Unit} +end + +signature S' = sig + con rs :: {Unit} + + val handler : $(stringify rs) -> page + val page : unit -> page +end + +functor F (M : S) : S' where con rs = M.rs = struct + con rs = M.rs + + val handler = fn x : $(stringify M.rs) => <html><body> + OK. + </body></html> + + val page = fn () => <html><body> + + </body></html> +end + +structure M = F(struct + con rs = [] +end) + +open M +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/open_functor.lac Tue Jul 22 18:20:13 2008 -0400 @@ -0,0 +1,16 @@ +signature S = sig + type t + val x : t +end + +functor F (M : S) : S where type t = M.t = struct + type t = M.t + val x = M.x +end + +structure M = F(struct + type t = int + val x = 0 +end) + +open M