Mercurial > urweb
changeset 402:ebf27030ae3b
Recursive unurlify for Default datatypes
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 21 Oct 2008 15:11:42 -0400 |
| parents | cc71fb7e5e54 |
| children | 8084fa9216de |
| files | src/cjr_print.sml src/elaborate.sml tests/unurlify.ur |
| diffstat | 3 files changed, 168 insertions(+), 114 deletions(-) [+] |
line wrap: on
line diff
--- a/src/cjr_print.sml Tue Oct 21 13:56:38 2008 -0400 +++ b/src/cjr_print.sml Tue Oct 21 15:11:42 2008 -0400 @@ -1513,7 +1513,8 @@ fun doEm xncs = case xncs of - [] => string ("(uw_error(ctx, FATAL, \"Error unurlifying datatype " ^ x ^ "\"), (enum __uwe_" + [] => string ("(uw_error(ctx, FATAL, \"Error unurlifying datatype " + ^ x ^ "\"), (enum __uwe_" ^ x ^ "_" ^ Int.toString i ^ ")0)") | (x', n, to) :: rest => box [string "((!strncmp(request, \"", @@ -1636,70 +1637,99 @@ end | TDatatype (Default, i, _) => - let - val (x, xncs) = E.lookupDatatype env i + if IS.member (rf, i) then + box [string "unurlify_", + string (Int.toString i), + string "()"] + else + let + val (x, xncs) = E.lookupDatatype env i - fun doEm xncs = - case xncs of - [] => string ("(uw_error(ctx, FATAL, \"Error unurlifying datatype " ^ x ^ "\"), NULL)") - | (x', n, to) :: rest => - box [string "((!strncmp(request, \"", - string x', - string "\", ", - string (Int.toString (size x')), - string ") && (request[", - string (Int.toString (size x')), - string "] == 0 || request[", - string (Int.toString (size x')), - string "] == '/')) ? ({", - newline, - string "struct", - space, - string ("__uwd_" ^ ident x ^ "_" ^ Int.toString i), - space, - string "*tmp = uw_malloc(ctx, sizeof(struct __uwd_", - string x, - string "_", - string (Int.toString i), - string "));", - newline, - string "tmp->tag", - space, - string "=", - space, - string ("__uwc_" ^ ident x' ^ "_" ^ Int.toString n), - string ";", - newline, - string "request", - space, - string "+=", - space, - string (Int.toString (size x')), - string ";", - newline, - string "if (request[0] == '/') ++request;", - newline, - case to of - NONE => box [] - | SOME (t, _) => box [string "tmp->data.uw_", - p_ident x', - space, - string "=", - space, - unurlify' rf t, - string ";", - newline], - string "tmp;", - newline, - string "})", - space, - string ":", - space, - doEm rest, - string ")"] - in - doEm xncs - end + val rf = IS.add (rf, i) + + fun doEm xncs = + case xncs of + [] => string ("(uw_error(ctx, FATAL, \"Error unurlifying datatype " + ^ x ^ "\"), NULL)") + | (x', n, to) :: rest => + box [string "((!strncmp(request, \"", + string x', + string "\", ", + string (Int.toString (size x')), + string ") && (request[", + string (Int.toString (size x')), + string "] == 0 || request[", + string (Int.toString (size x')), + string "] == '/')) ? ({", + newline, + string "struct", + space, + string ("__uwd_" ^ ident x ^ "_" ^ Int.toString i), + space, + string "*tmp = uw_malloc(ctx, sizeof(struct __uwd_", + string x, + string "_", + string (Int.toString i), + string "));", + newline, + string "tmp->tag", + space, + string "=", + space, + string ("__uwc_" ^ ident x' ^ "_" ^ Int.toString n), + string ";", + newline, + string "request", + space, + string "+=", + space, + string (Int.toString (size x')), + string ";", + newline, + string "if (request[0] == '/') ++request;", + newline, + case to of + NONE => box [] + | SOME (t, _) => box [string "tmp->data.uw_", + p_ident x', + space, + string "=", + space, + unurlify' rf t, + string ";", + newline], + string "tmp;", + newline, + string "})", + space, + string ":", + space, + doEm rest, + string ")"] + in + box [string "({", + space, + p_typ env (t, ErrorMsg.dummySpan), + space, + string "unurlify_", + string (Int.toString i), + string "(void) {", + newline, + box [string "return", + space, + doEm xncs, + string ";", + newline], + string "}", + newline, + newline, + + string "unurlify_", + string (Int.toString i), + string "();", + newline, + string "})"] + end | _ => (ErrorMsg.errorAt loc "Unable to choose a URL decoding function"; space)
--- a/src/elaborate.sml Tue Oct 21 13:56:38 2008 -0400 +++ b/src/elaborate.sml Tue Oct 21 15:11:42 2008 -0400 @@ -1159,6 +1159,17 @@ fun exhaustive (env, denv, t, ps) = let + fun depth (p, _) = + case p of + L'.PWild => 0 + | L'.PVar _ => 0 + | L'.PPrim _ => 0 + | L'.PCon (_, _, _, NONE) => 1 + | L'.PCon (_, _, _, SOME p) => 1 + depth p + | L'.PRecord xps => foldl (fn ((_, p, _), n) => Int.max (depth p, n)) 0 xps + + val depth = 1 + foldl (fn (p, n) => Int.max (depth p, n)) 0 ps + fun pcCoverage pc = case pc of L'.PConVar n => n @@ -1201,51 +1212,54 @@ | [p] => coverage p | p :: ps => merge (coverage p, combinedCoverage ps) - fun enumerateCases t = - let - fun dtype cons = - ListUtil.mapConcat (fn (_, n, to) => - case to of - NONE => [Datatype (IM.insert (IM.empty, n, Wild))] - | SOME t => map (fn c => Datatype (IM.insert (IM.empty, n, c))) - (enumerateCases t)) cons - in - case #1 (#1 (hnormCon (env, denv) t)) of - L'.CNamed n => - (let - val dt = E.lookupDatatype env n - val cons = E.constructors dt - in - dtype cons - end handle E.UnboundNamed _ => [Wild]) - | L'.TRecord c => - (case #1 (#1 (hnormCon (env, denv) c)) of - L'.CRecord (_, xts) => - let - val xts = map (fn (x, t) => (#1 (hnormCon (env, denv) x), t)) xts - - fun exponentiate fs = - case fs of - [] => [SM.empty] - | ((L'.CName x, _), t) :: rest => - let - val this = enumerateCases t - val rest = exponentiate rest - in - ListUtil.mapConcat (fn fmap => - map (fn c => SM.insert (fmap, x, c)) this) rest - end - | _ => raise Fail "exponentiate: Not CName" + fun enumerateCases depth t = + if depth = 0 then + [Wild] + else + let + fun dtype cons = + ListUtil.mapConcat (fn (_, n, to) => + case to of + NONE => [Datatype (IM.insert (IM.empty, n, Wild))] + | SOME t => map (fn c => Datatype (IM.insert (IM.empty, n, c))) + (enumerateCases (depth-1) t)) cons + in + case #1 (#1 (hnormCon (env, denv) t)) of + L'.CNamed n => + (let + val dt = E.lookupDatatype env n + val cons = E.constructors dt in - if List.exists (fn ((L'.CName _, _), _) => false - | (c, _) => true) xts then - [Wild] - else - map (fn ls => Record [ls]) (exponentiate xts) - end - | _ => [Wild]) - | _ => [Wild] - end + dtype cons + end handle E.UnboundNamed _ => [Wild]) + | L'.TRecord c => + (case #1 (#1 (hnormCon (env, denv) c)) of + L'.CRecord (_, xts) => + let + val xts = map (fn (x, t) => (#1 (hnormCon (env, denv) x), t)) xts + + fun exponentiate fs = + case fs of + [] => [SM.empty] + | ((L'.CName x, _), t) :: rest => + let + val this = enumerateCases depth t + val rest = exponentiate rest + in + ListUtil.mapConcat (fn fmap => + map (fn c => SM.insert (fmap, x, c)) this) rest + end + | _ => raise Fail "exponentiate: Not CName" + in + if List.exists (fn ((L'.CName _, _), _) => false + | (c, _) => true) xts then + [Wild] + else + map (fn ls => Record [ls]) (exponentiate xts) + end + | _ => [Wild]) + | _ => [Wild] + end fun coverageImp (c1, c2) = let @@ -1331,7 +1345,7 @@ (prefaces "Not a datatype" [("c", p_con env (c, ErrorMsg.dummySpan))]; raise Fail "isTotal: Not a datatype") end - | Record _ => (List.all (fn c2 => coverageImp (c, c2)) (enumerateCases t), []) + | Record _ => (List.all (fn c2 => coverageImp (c, c2)) (enumerateCases depth t), []) in isTotal (combinedCoverage ps, t) end @@ -1640,11 +1654,8 @@ ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, enD gs' @ gs) end - - (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 r)*) in - (*prefaces "elabExp" [("e", SourcePrint.p_exp eAll), - ("|tcs|", PD.string (Int.toString (length tcs)))];*) + (*prefaces "/elabExp" [("e", SourcePrint.p_exp eAll)];*) r end
--- a/tests/unurlify.ur Tue Oct 21 13:56:38 2008 -0400 +++ b/tests/unurlify.ur Tue Oct 21 15:11:42 2008 -0400 @@ -2,6 +2,19 @@ fun handler (ls : list bool) = return <xml/> +datatype wlist = WNil | Empty | WCons of bool * wlist + +fun whandler' (ls : wlist) = + case ls of + WNil => <xml>Nil</xml> + | Empty => <xml>Empty</xml> + | WCons (x, ls') => <xml>{[x]} :: {whandler' ls'}</xml> + +fun whandler ls = return (whandler' ls) + fun main () : transaction page = return <xml><body> - <a link={handler Nil}>!</a> + <a link={handler Nil}>!</a><br/> + <a link={whandler WNil}>Nil</a><br/> + <a link={whandler Empty}>Empty</a><br/> + <a link={whandler (WCons (True, WCons (False, Empty)))}>True :: False :: Empty</a><br/> </body></xml>