Recursive unurlify for Default datatypes

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