Mercurial > urweb
changeset 905:7a4b026e45dd
Library improvements; proper list [un]urlification; remove server-side ServerCalls; eta reduction in type inference
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 09 Aug 2009 16:13:27 -0400 |
| parents | 6d9538ce94d8 |
| children | c270fb847dc2 |
| files | lib/js/urweb.js lib/ur/monad.ur lib/ur/monad.urs lib/ur/top.ur lib/ur/top.urs src/cjr_print.sml src/cjrize.sml src/compiler.sml src/elab_ops.sml src/jscomp.sml src/mono.sml src/mono_opt.sig src/mono_opt.sml src/mono_print.sml src/mono_reduce.sml src/mono_util.sml src/monoize.sml |
| diffstat | 17 files changed, 243 insertions(+), 42 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/js/urweb.js Thu Aug 06 15:23:04 2009 -0400 +++ b/lib/js/urweb.js Sun Aug 09 16:13:27 2009 -0400 @@ -306,7 +306,7 @@ var arr = dummy.getElementsByTagName("tbody"); firstChild = null; - if (arr.length > 0) { + if (arr.length > 0 && table != null) { var tbody = arr[0], next; firstChild = document.createElement("script"); table.insertBefore(firstChild, x); @@ -323,7 +323,7 @@ var arr = dummy.getElementsByTagName("tr"); firstChild = null; - if (arr.length > 0) { + if (arr.length > 0 && table != null) { var tbody = arr[0], next; firstChild = document.createElement("script"); table.insertBefore(firstChild, x); @@ -468,7 +468,19 @@ } function uu(s) { - return unescape(s); + return unescape(s.replace(new RegExp ("\\+", "g"), " ")); +} + +function uul(getToken, getData) { + var tok = getToken(); + if (tok == "Nil") { + return null; + } else if (tok == "Cons") { + var d = getData(); + var l = uul(getToken, getData); + return {_1:d, _2:l}; + } else + throw ("Can't unmarshal list (" + tok + ")"); }
--- a/lib/ur/monad.ur Thu Aug 06 15:23:04 2009 -0400 +++ b/lib/ur/monad.ur Sun Aug 09 16:13:27 2009 -0400 @@ -7,3 +7,38 @@ (return {}) [ts] fd r fun ignore [m ::: Type -> Type] (_ : monad m) [t] (v : m t) = x <- v; return () + +fun foldR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: {K} -> Type] + (f : nm :: Name -> t :: K -> rest :: {K} + -> [[nm] ~ rest] => + tf t -> tr rest -> m (tr ([nm = t] ++ rest))) + (i : tr []) [r :: {K}] (fl : folder r) = + Top.fold [fn r :: {K} => $(map tf r) -> m (tr r)] + (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] + (acc : _ -> m (tr rest)) r => + acc' <- acc (r -- nm); + f [nm] [t] [rest] ! r.nm acc') + (fn _ => return i) + [_] fl + +fun foldR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: {K} -> Type] + (f : nm :: Name -> t :: K -> rest :: {K} + -> [[nm] ~ rest] => + tf1 t -> tf2 t -> tr rest -> m (tr ([nm = t] ++ rest))) + (i : tr []) [r :: {K}] (fl : folder r) = + Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m (tr r)] + (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] + (acc : _ -> _ -> m (tr rest)) r1 r2 => + acc' <- acc (r1 -- nm) (r2 -- nm); + f [nm] [t] [rest] ! r1.nm r2.nm acc') + (fn _ _ => return i) + [_] fl + +fun mapR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: K -> Type] + (f : nm :: Name -> t :: K -> tf t -> m (tr t)) = + @@foldR [m] _ [tf] [fn r => $(map tr r)] + (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (v : tf t) + (acc : $(map tr rest)) => + v' <- f [nm] [t] v; + return (acc ++ {nm = v'})) + {}
--- a/lib/ur/monad.urs Thu Aug 06 15:23:04 2009 -0400 +++ b/lib/ur/monad.urs Sun Aug 09 16:13:27 2009 -0400 @@ -3,3 +3,27 @@ val ignore : m ::: (Type -> Type) -> monad m -> t ::: Type -> m t -> m unit + +val foldR : K --> m ::: (Type -> Type) -> monad m + -> tf :: (K -> Type) + -> tr :: ({K} -> Type) + -> (nm :: Name -> t :: K -> rest :: {K} + -> [[nm] ~ rest] => + tf t -> tr rest -> m (tr ([nm = t] ++ rest))) + -> tr [] + -> r :: {K} -> folder r -> $(map tf r) -> m (tr r) + +val foldR2 : K --> m ::: (Type -> Type) -> monad m + -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) + -> tr :: ({K} -> Type) + -> (nm :: Name -> t :: K -> rest :: {K} + -> [[nm] ~ rest] => + tf1 t -> tf2 t -> tr rest -> m (tr ([nm = t] ++ rest))) + -> tr [] + -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m (tr r) + +val mapR : K --> m ::: (Type -> Type) -> monad m + -> tf :: (K -> Type) + -> tr :: (K -> Type) + -> (nm :: Name -> t :: K -> tf t -> m (tr t)) + -> r :: {K} -> folder r -> $(map tf r) -> m ($(map tr r))
--- a/lib/ur/top.ur Thu Aug 06 15:23:04 2009 -0400 +++ b/lib/ur/top.ur Sun Aug 09 16:13:27 2009 -0400 @@ -98,12 +98,12 @@ acc (r -- nm) ++ {nm = f r.nm}) (fn _ => {}) -fun map2 [K1] [K2] [tf1 :: K1 -> Type] [tf2 :: K2 -> Type] [tf :: K1 -> K2] - (f : t ::: K1 -> tf1 t -> tf2 (tf t)) [r :: {K1}] (fl : folder r) = - fl [fn r :: {K1} => $(map tf1 r) -> $(map tf2 (map tf r))] - (fn [nm :: Name] [t :: K1] [rest :: {K1}] [[nm] ~ rest] acc r => - acc (r -- nm) ++ {nm = f r.nm}) - (fn _ => {}) +fun map2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] + (f : t ::: K -> tf1 t -> tf2 t -> tf3 t) [r :: {K}] (fl : folder r) = + fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r)] + (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 => + acc (r1 -- nm) (r2 -- nm) ++ {nm = f r1.nm r2.nm}) + (fn _ _ => {}) fun foldUR [tf :: Type] [tr :: {Unit} -> Type] (f : nm :: Name -> rest :: {Unit}
--- a/lib/ur/top.urs Thu Aug 06 15:23:04 2009 -0400 +++ b/lib/ur/top.urs Sun Aug 09 16:13:27 2009 -0400 @@ -48,9 +48,9 @@ val mp : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> (t ::: K -> tf1 t -> tf2 t) -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -val map2 : K1 --> K2 --> tf1 :: (K1 -> Type) -> tf2 :: (K2 -> Type) -> tf :: (K1 -> K2) - -> (t ::: K1 -> tf1 t -> tf2 (tf t)) - -> r :: {K1} -> folder r -> $(map tf1 r) -> $(map tf2 (map tf r)) +val map2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) + -> (t ::: K -> tf1 t -> tf2 t -> tf3 t) + -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) val foldUR : tf :: Type -> tr :: ({Unit} -> Type) -> (nm :: Name -> rest :: {Unit}
--- a/src/cjr_print.sml Thu Aug 06 15:23:04 2009 -0400 +++ b/src/cjr_print.sml Sun Aug 09 16:13:27 2009 -0400 @@ -962,9 +962,11 @@ unurlify' IS.empty t end +val urlify1 = ref 0 + fun urlify env t = let - fun urlify' rf level (t as (_, loc)) = + fun urlify' rf rfl level (t as (_, loc)) = case #1 t of TFfi ("Basis", "unit") => box [] | TFfi (m, t) => box [string ("uw_" ^ ident m ^ "_urlify" ^ capitalize t @@ -1007,7 +1009,7 @@ newline] else []), - urlify' rf (level + 1) t, + urlify' rf rfl (level + 1) t, string "}", newline] :: blocks, true) @@ -1079,8 +1081,9 @@ string "it0) {", newline, box [string "if (it0) {", + newline, if isUnboxable t then - urlify' rf 0 t + urlify' rf rfl 0 t else box [p_typ env t, space, @@ -1094,11 +1097,12 @@ string has_arg, string "/\");", newline, - urlify' rf 1 t, + urlify' rf rfl 1 t, string ";", newline], string "} else {", - box [string "uw_write(ctx, \"", + box [newline, + string "uw_write(ctx, \"", string no_arg, string "\");", newline], @@ -1165,7 +1169,7 @@ string x', string ";", newline, - urlify' rf 1 t, + urlify' rf rfl 1 t, newline], string "} else {", newline, @@ -1208,7 +1212,7 @@ if isUnboxable t then box [string "uw_write(ctx, \"Some/\");", newline, - urlify' rf level t] + urlify' rf rfl level t] else box [p_typ env t, space, @@ -1223,19 +1227,84 @@ newline, string "uw_write(ctx, \"Some/\");", newline, - urlify' rf (level + 1) t, + urlify' rf rfl (level + 1) t, string ";", newline], string "} else {", - box [string "uw_write(ctx, \"None\");", + box [newline, + string "uw_write(ctx, \"None\");", newline], string "}", newline] + | TList (t, i) => + if IS.member (rfl, i) then + box [string "urlifyl_", + string (Int.toString i), + string "(it", + string (Int.toString level), + string ");", + newline] + else + let + val rfl = IS.add (rfl, i) + in + box [string "({", + space, + string "void", + space, + string "urlifyl_", + string (Int.toString i), + string "(struct __uws_", + string (Int.toString i), + space, + string "*it0) {", + newline, + box [string "if (it0) {", + newline, + p_typ env t, + space, + string "it1", + space, + string "=", + space, + string "it0->__uwf_1;", + newline, + string "uw_write(ctx, \"Cons/\");", + newline, + urlify' rf rfl 1 t, + string ";", + newline, + string "uw_write(ctx, \"/\");", + newline, + string "urlifyl_", + string (Int.toString i), + string "(it0->__uwf_2);", + newline, + string "} else {", + newline, + box [string "uw_write(ctx, \"Nil\");", + newline], + string "}", + newline], + string "}", + newline, + newline, + + string "urlifyl_", + string (Int.toString i), + string "(it", + string (Int.toString level), + string ");", + newline, + string "});", + newline] + end + | _ => (ErrorMsg.errorAt loc "Unable to choose a URL encoding function"; space) in - urlify' IS.empty 0 t + urlify' IS.empty IS.empty 0 t end fun sql_type_in env (tAll as (t, loc)) =
--- a/src/cjrize.sml Thu Aug 06 15:23:04 2009 -0400 +++ b/src/cjrize.sml Sun Aug 09 16:13:27 2009 -0400 @@ -112,6 +112,7 @@ end | L.TRecord xts => let + val xts = ListMergeSort.sort (fn ((x, _), (y, _)) => String.compare (x, y) = GREATER) xts val old_xts = xts val (xts, sm) = ListUtil.foldlMap (fn ((x, t), sm) => let
--- a/src/compiler.sml Thu Aug 06 15:23:04 2009 -0400 +++ b/src/compiler.sml Sun Aug 09 16:13:27 2009 -0400 @@ -805,7 +805,7 @@ val toMonoize = transform monoize "monoize" o toEffectize val mono_opt = { - func = MonoOpt.optimize, + func = (fn x => (MonoOpt.removeServerCalls := false; MonoOpt.optimize x)), print = MonoPrint.p_file MonoEnv.empty } @@ -841,7 +841,12 @@ val toJscomp = transform jscomp "jscomp" o toMono_opt2 -val toMono_opt3 = transform mono_opt "mono_opt3" o toJscomp +val mono_opt' = { + func = (fn x => (MonoOpt.removeServerCalls := true; MonoOpt.optimize x)), + print = MonoPrint.p_file MonoEnv.empty +} + +val toMono_opt3 = transform mono_opt' "mono_opt3" o toJscomp val fuse = { func = Fuse.fuse,
--- a/src/elab_ops.sml Thu Aug 06 15:23:04 2009 -0400 +++ b/src/elab_ops.sml Sun Aug 09 16:13:27 2009 -0400 @@ -131,6 +131,18 @@ sgn_item = fn sgi => sgi, sgn = fn sgn => sgn} +val occurs = + U.Con.existsB {kind = fn _ => false, + con = fn (n, c) => + case c of + CRel n' => n' = n + | _ => false, + bind = fn (n, b) => + case b of + U.Con.RelC _ => n + 1 + | _ => n} + 0 + fun hnormCon env (cAll as (c, loc)) = case c of @@ -156,6 +168,16 @@ | SOME (_, SOME c) => hnormCon env c end + (* Eta reduction *) + | CAbs (x, k, b) => + (case #1 (hnormCon (E.pushCRel env x k) b) of + CApp (f, (CRel 0, _)) => + if occurs f then + cAll + else + hnormCon env (subConInCon (0, (CUnit, loc)) f) + | _ => cAll) + | CApp (c1, c2) => (case #1 (hnormCon env c1) of CAbs (x, k, cb) =>
--- a/src/jscomp.sml Thu Aug 06 15:23:04 2009 -0400 +++ b/src/jscomp.sml Sun Aug 09 16:13:27 2009 -0400 @@ -86,7 +86,7 @@ | ESignalReturn e => varDepth e | ESignalBind (e1, e2) => Int.max (varDepth e1, varDepth e2) | ESignalSource e => varDepth e - | EServerCall (e, ek, _, _) => Int.max (varDepth e, varDepth ek) + | EServerCall (e, ek, _, _, _) => Int.max (varDepth e, varDepth ek) | ERecv (e, ek, _) => Int.max (varDepth e, varDepth ek) | ESleep (e, ek) => Int.max (varDepth e, varDepth ek) @@ -130,7 +130,7 @@ | ESignalReturn e => cu inner e | ESignalBind (e1, e2) => cu inner e1 andalso cu inner e2 | ESignalSource e => cu inner e - | EServerCall (e, ek, _, _) => cu inner e andalso cu inner ek + | EServerCall (e, ek, _, _, _) => cu inner e andalso cu inner ek | ERecv (e, ek, _) => cu inner e andalso cu inner ek | ESleep (e, ek) => cu inner e andalso cu inner ek in @@ -434,6 +434,13 @@ ("(t[i++]==\"Some\"?" ^ e ^ ":null)", st) end + | TList t => + let + val (e, st) = unurlifyExp loc (t, st) + in + ("uul(function(){return t[i++];},function(){return " ^ e ^ "})", st) + end + | TDatatype (n, ref (dk, cs)) => (case IM.find (#decoders st, n) of SOME n' => ("(tmp=_n" ^ Int.toString n' ^ "(t,i),i=tmp._1,tmp._2)", st) @@ -1034,7 +1041,7 @@ st) end - | EServerCall (e, ek, t, eff) => + | EServerCall (e, ek, t, eff, _) => let val (e, st) = jsE inner (e, st) val (ek, st) = jsE inner (ek, st) @@ -1313,12 +1320,13 @@ ((ESignalSource e, loc), st) end - | EServerCall (e1, e2, t, ef) => + | EServerCall (e1, e2, t, ef, ue) => let val (e1, st) = exp outer (e1, st) val (e2, st) = exp outer (e2, st) + val (ue, st) = exp outer (ue, st) in - ((EServerCall (e1, e2, t, ef), loc), st) + ((EServerCall (e1, e2, t, ef, ue), loc), st) end | ERecv (e1, e2, t) => let
--- a/src/mono.sml Thu Aug 06 15:23:04 2009 -0400 +++ b/src/mono.sml Sun Aug 09 16:13:27 2009 -0400 @@ -114,7 +114,7 @@ | ESignalBind of exp * exp | ESignalSource of exp - | EServerCall of exp * exp * typ * effect + | EServerCall of exp * exp * typ * effect * exp | ERecv of exp * exp * typ | ESleep of exp * exp
--- a/src/mono_opt.sig Thu Aug 06 15:23:04 2009 -0400 +++ b/src/mono_opt.sig Sun Aug 09 16:13:27 2009 -0400 @@ -30,4 +30,6 @@ val optimize : Mono.file -> Mono.file val optExp : Mono.exp -> Mono.exp + val removeServerCalls : bool ref + end
--- a/src/mono_opt.sml Thu Aug 06 15:23:04 2009 -0400 +++ b/src/mono_opt.sml Sun Aug 09 16:13:27 2009 -0400 @@ -30,6 +30,8 @@ open Mono structure U = MonoUtil +val removeServerCalls = ref false + fun typ t = t fun decl d = d @@ -480,6 +482,12 @@ | [] => raise Fail "MonoOpt impossible nil") | NONE => e end + + | EServerCall (_, _, _, _, ue) => + if !removeServerCalls then + optExp ue + else + e | _ => e
--- a/src/mono_print.sml Thu Aug 06 15:23:04 2009 -0400 +++ b/src/mono_print.sml Sun Aug 09 16:13:27 2009 -0400 @@ -335,11 +335,11 @@ p_exp env e, string ")"] - | EServerCall (n, e, _, _) => box [string "Server(", - p_exp env n, - string ")[", - p_exp env e, - string "]"] + | EServerCall (n, e, _, _, _) => box [string "Server(", + p_exp env n, + string ")[", + p_exp env e, + string "]"] | ERecv (n, e, _) => box [string "Recv(", p_exp env n, string ")[",
--- a/src/mono_reduce.sml Thu Aug 06 15:23:04 2009 -0400 +++ b/src/mono_reduce.sml Sun Aug 09 16:13:27 2009 -0400 @@ -354,7 +354,7 @@ | ESignalBind (e1, e2) => summarize d e1 @ summarize d e2 | ESignalSource e => summarize d e - | EServerCall (e, ek, _, _) => summarize d e @ summarize d ek @ [Unsure] + | EServerCall (e, ek, _, _, _) => summarize d e @ summarize d ek @ [Unsure] | ERecv (e, ek, _) => summarize d e @ summarize d ek @ [Unsure] | ESleep (e, ek) => summarize d e @ summarize d ek @ [Unsure] in
--- a/src/mono_util.sml Thu Aug 06 15:23:04 2009 -0400 +++ b/src/mono_util.sml Sun Aug 09 16:13:27 2009 -0400 @@ -362,14 +362,16 @@ fn e' => (ESignalSource e', loc)) - | EServerCall (s, ek, t, eff) => + | EServerCall (s, ek, t, eff, ue) => S.bind2 (mfe ctx s, fn s' => S.bind2 (mfe ctx ek, fn ek' => - S.map2 (mft t, + S.bind2 (mft t, fn t' => - (EServerCall (s', ek', t', eff), loc)))) + S.map2 (mfe ctx ue, + fn ue' => + (EServerCall (s', ek', t', eff, ue'), loc))))) | ERecv (s, ek, t) => S.bind2 (mfe ctx s, fn s' =>
--- a/src/monoize.sml Thu Aug 06 15:23:04 2009 -0400 +++ b/src/monoize.sml Sun Aug 09 16:13:27 2009 -0400 @@ -93,7 +93,12 @@ L.TFun (c1, c2) => (L'.TFun (mt env dtmap c1, mt env dtmap c2), loc) | L.TCFun _ => poly () | L.TRecord (L.CRecord ((L.KType, _), xcs), _) => - (L'.TRecord (map (fn (x, t) => (monoName env x, mt env dtmap t)) xcs), loc) + let + val xcs = map (fn (x, t) => (monoName env x, mt env dtmap t)) xcs + val xcs = ListMergeSort.sort (fn ((x, _), (y, _)) => String.compare (x, y) = GREATER) xcs + in + (L'.TRecord xcs, loc) + end | L.TRecord _ => poly () | L.CApp ((L.CFfi ("Basis", "option"), _), t) => @@ -3076,6 +3081,8 @@ e, monoType env t), fm) end) fm xes + + val xes = ListMergeSort.sort (fn ((x, _, _), (y, _, _)) => String.compare (x, y) = GREATER) xes in ((L'.ERecord xes, loc), fm) end @@ -3154,6 +3161,12 @@ val (ek, fm) = monoExp (env, st, fm) ek + val unRpced = foldl (fn (e1, e2) => (L'.EApp (e2, e1), loc)) (L'.ENamed n, loc) es + val unRpced = (L'.EApp (unRpced, (L'.ERecord [], loc)), loc) + val unRpced = (L'.EApp (ek, unRpced), loc) + val unRpced = (L'.EApp (unRpced, (L'.ERecord [], loc)), loc) + val unit = (L'.TRecord [], loc) + val ekf = (L'.EAbs ("f", (L'.TFun (t, (L'.TFun ((L'.TRecord [], loc), @@ -3171,9 +3184,9 @@ L'.ReadCookieWrite else L'.ReadOnly - val e = (L'.EServerCall (call, ek, t, eff), loc) + + val e = (L'.EServerCall (call, ek, t, eff, unRpced), loc) val e = liftExpInExp 0 e - val unit = (L'.TRecord [], loc) val e = (L'.EAbs ("_", unit, unit, e), loc) in (e, fm)