summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/cjr_print.sml158
-rw-r--r--src/elaborate.sml109
2 files changed, 154 insertions, 113 deletions
diff --git a/src/cjr_print.sml b/src/cjr_print.sml
index bfe6414f..f2af999b 100644
--- a/src/cjr_print.sml
+++ b/src/cjr_print.sml
@@ -1513,7 +1513,8 @@ fun p_file env (ds, ps) =
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 @@ fun p_file env (ds, ps) =
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)
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 9107f29a..1d793923 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1159,6 +1159,17 @@ fun c2s c =
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 @@ fun exhaustive (env, denv, t, ps) =
| [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 @@ fun exhaustive (env, denv, t, ps) =
(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 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
((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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-14 22:07:35 +0000