changeset 198:ab86aa858e6c

'Option' datatype encoding
author Adam Chlipala <adamc@hcoop.net>
date Sat, 09 Aug 2008 19:23:31 -0400
parents b1b9bcfd8c42
children c938fe391c84
files src/c/lacweb.c src/cjr_print.sml src/cjrize.sml src/core_util.sig src/core_util.sml src/corify.sml src/elab.sml src/elab_util.sig src/elab_util.sml src/expl_util.sig src/expl_util.sml src/mono_env.sml src/mono_util.sig src/mono_util.sml src/monoize.sml tests/option.lac
diffstat 16 files changed, 195 insertions(+), 49 deletions(-) [+]
line wrap: on
line diff
--- a/src/c/lacweb.c	Sat Aug 09 16:54:04 2008 -0400
+++ b/src/c/lacweb.c	Sat Aug 09 19:23:31 2008 -0400
@@ -471,11 +471,11 @@
   char *r, *s1, *s2;
   int len, n;
 
-  len = strlen(*s);
+  len = strlen(new_s);
   lw_check_heap(ctx, len + 1);
 
   r = ctx->heap_front;
-  ctx->heap_front = lw_unurlifyString_to(ctx, ctx->heap_front, *s);
+  ctx->heap_front = lw_unurlifyString_to(ctx, ctx->heap_front, new_s);
   *s = new_s;
   return r;
 }
--- a/src/cjr_print.sml	Sat Aug 09 16:54:04 2008 -0400
+++ b/src/cjr_print.sml	Sat Aug 09 19:23:31 2008 -0400
@@ -74,6 +74,14 @@
               space,
               string ("__lwe_" ^ #1 (E.lookupDatatype env n) ^ "_" ^ Int.toString n)]
          handle CjrEnv.UnboundNamed _ => string ("__lwd_UNBOUND__" ^ Int.toString n))
+      | TDatatype (Option, n, xncs) =>
+        (case ListUtil.search #3 (!xncs) of
+             NONE => raise Fail "CjrPrint: TDatatype marked Option has no constructor with an argument"
+           | SOME t =>
+             case #1 t of
+                 TDatatype _ => p_typ' par env t
+               | _ => box [p_typ' par env t,
+                           string "*"])
       | TDatatype (Default, n, _) =>
         (box [string "struct",
               space,
@@ -198,10 +206,18 @@
                               space,
                               string "=",
                               space,
-                              string "disc",
-                              string (Int.toString depth),
-                              string "->data.",
-                              string x,
+                              case dk of
+                                  Enum => raise Fail "CjrPrint: Looking at argument of no-argument constructor"
+                                | Default => box [string "disc",
+                                                  string (Int.toString depth),
+                                                  string "->data.",
+                                                  string x]
+                                | Option =>
+                                  case #1 t of
+                                      TDatatype _ => box [string "disc",
+                                                          string (Int.toString depth)]
+                                    | _ => box [string "*disc",
+                                                string (Int.toString depth)],
                               string ";",
                               newline,
                               p,
@@ -214,13 +230,24 @@
                   space,
                   string "(disc",
                   string (Int.toString depth),
-                  case dk of
-                      Enum => box []
-                    | Default => string "->tag",
-                  space,
-                  string "!=",
-                  space,
-                  p_patCon env pc,
+                  case (dk, po) of
+                      (Enum, _) => box [space,
+                                        string "!=",
+                                        space,
+                                        p_patCon env pc]
+                    | (Default, _) => box [string "->tag",
+                                           space,
+                                           string "!=",
+                                           space,
+                                           p_patCon env pc]
+                    | (Option, NONE) => box [space,
+                                             string "!=",
+                                             space,
+                                             string "NULL"]
+                    | (Option, SOME _) => box [space,
+                                               string "==",
+                                               space,
+                                               string "NULL"],
                   string ")",
                   space,
                   exit,
@@ -296,6 +323,41 @@
       | ERel n => p_rel env n
       | ENamed n => p_enamed env n
       | ECon (Enum, pc, _) => p_patCon env pc
+      | ECon (Option, pc, NONE) => string "NULL"
+      | ECon (Option, pc, SOME e) =>
+        let
+            val to = case pc of
+                         PConVar n => #2 (E.lookupConstructor env n)
+                       | PConFfi {arg, ...} => arg
+
+            val t = case to of
+                        NONE => raise Fail "CjrPrint: ECon argument status mismatch"
+                      | SOME t => t
+        in
+            case #1 t of
+                TDatatype _ => p_exp' par env e
+              | _ => box [string "({",
+                          newline,
+                          p_typ env t,
+                          space,
+                          string "*tmp",
+                          space,
+                          string "=",
+                          space,
+                          string "lw_malloc(ctx, sizeof(",
+                          p_typ env t,
+                          string "));",
+                          newline,
+                          string "*tmp",
+                          space,
+                          string "=",
+                          p_exp' par env e,
+                          string ";",
+                          newline,
+                          string "tmp;",
+                          newline,
+                          string "})"]
+        end
       | ECon (Default, pc, eo) =>
         let
             val (xd, xc, xn) = patConInfo env pc
@@ -522,6 +584,7 @@
              p_list_sep (box [string ",", space]) (fn (x, n, _) => string ("__lwc_" ^ x ^ "_" ^ Int.toString n)) xncs,
              space,
              string "};"]
+      | DDatatype (Option, _, _, _) => box []
       | DDatatype (Default, x, n, xncs) =>
         let
             val xncsArgs = List.mapPartial (fn (x, n, NONE) => NONE
@@ -807,6 +870,79 @@
                     doEm xncs
                 end
 
+              | TDatatype (Option, i, xncs) =>
+                let
+                    val (x, _) = E.lookupDatatype env i
+
+                    val (no_arg, has_arg, t) =
+                        case !xncs of
+                            [(no_arg, _, NONE), (has_arg, _, SOME t)] =>
+                            (no_arg, has_arg, t)
+                          | [(has_arg, _, SOME t), (no_arg, _, NONE)] =>
+                            (no_arg, has_arg, t)
+                          | _ => raise Fail "CjrPrint: unfooify misclassified Option datatype"
+                in
+                    box [string "(request[0] == '/' ? ++request : request,",
+                         newline,
+                         string "((!strncmp(request, \"",
+                         string no_arg,
+                         string "\", ",
+                         string (Int.toString (size no_arg)),
+                         string ") && (request[",
+                         string (Int.toString (size no_arg)),
+                         string "] == 0 || request[",
+                         string (Int.toString (size no_arg)),
+                         string "] == '/')) ? (request",
+                         space,
+                         string "+=",
+                         space,
+                         string (Int.toString (size no_arg)),
+                         string ", NULL) : ((!strncmp(request, \"",
+                         string has_arg,
+                         string "\", ",
+                         string (Int.toString (size has_arg)),
+                         string ") && (request[",
+                         string (Int.toString (size has_arg)),
+                         string "] == 0 || request[",
+                         string (Int.toString (size has_arg)),
+                         string "] == '/')) ? (request",
+                         space,
+                         string "+=",
+                         space,
+                         string (Int.toString (size has_arg)),
+                         string ", ",
+                         
+                         case #1 t of
+                             TDatatype _ => unurlify t
+                           | _ => box [string "({",
+                                       newline,
+                                       p_typ env t,
+                                       space,
+                                       string "*tmp",
+                                       space,
+                                       string "=",
+                                       space,
+                                       string "lw_malloc(ctx, sizeof(",
+                                       p_typ env t,
+                                       string "));",
+                                       newline,
+                                       string "*tmp",
+                                       space,
+                                       string "=",
+                                       space,
+                                       unurlify t,
+                                       string ";",
+                                       newline,
+                                       string "tmp;",
+                                       newline,
+                                       string "})"],
+                         string ")",
+                         newline,
+                         string ":",
+                         space,
+                         string ("(lw_error(ctx, FATAL, \"Error unurlifying datatype " ^ x ^ "\"), NULL))))")]
+                end                     
+
               | TDatatype (Default, i, _) =>
                 let
                     val (x, xncs) = E.lookupDatatype env i
@@ -955,7 +1091,11 @@
                      string (String.toString s),
                      string "\", ",
                      string (Int.toString (size s)),
-                     string ")) {",
+                     string ") && (request[",
+                     string (Int.toString (size s)),
+                     string "] == 0 || request[",
+                     string (Int.toString (size s)),
+                     string "] == '/')) {",
                      newline,
                      string "request += ",
                      string (Int.toString (size s)),
--- a/src/cjrize.sml	Sat Aug 09 16:54:04 2008 -0400
+++ b/src/cjrize.sml	Sat Aug 09 19:23:31 2008 -0400
@@ -282,7 +282,7 @@
     case d of
         L.DDatatype (x, n, xncs) =>
         let
-            val dk = MonoUtil.classifyDatatype xncs
+            val dk = ElabUtil.classifyDatatype xncs
             val (xncs, sm) = ListUtil.foldlMap (fn ((x, n, to), sm) =>
                                                    case to of
                                                        NONE => ((x, n, NONE), sm)
--- a/src/core_util.sig	Sat Aug 09 16:54:04 2008 -0400
+++ b/src/core_util.sig	Sat Aug 09 19:23:31 2008 -0400
@@ -27,8 +27,6 @@
 
 signature CORE_UTIL = sig
 
-val classifyDatatype : (string * int * Core.con option) list -> Core.datatype_kind
-
 structure Kind : sig
     val compare : Core.kind * Core.kind -> order
 
--- a/src/core_util.sml	Sat Aug 09 16:54:04 2008 -0400
+++ b/src/core_util.sml	Sat Aug 09 19:23:31 2008 -0400
@@ -29,12 +29,6 @@
 
 open Core
 
-fun classifyDatatype xncs =
-    if List.all (fn (_, _, NONE) => true | _ => false) xncs then
-        Enum
-    else
-        Default
-
 structure S = Search
 
 structure Kind = struct
--- a/src/corify.sml	Sat Aug 09 16:54:04 2008 -0400
+++ b/src/corify.sml	Sat Aug 09 19:23:31 2008 -0400
@@ -532,7 +532,7 @@
                                                         ((x, n, co), st)
                                                     end) st xncs
 
-             val dk = CoreUtil.classifyDatatype xncs
+             val dk = ElabUtil.classifyDatatype xncs
              val t = (L'.CNamed n, loc)
              val nxs = length xs - 1
              val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
@@ -674,7 +674,7 @@
                                   | L.SgiDatatype (x, n, xs, xnts) =>
                                     let
                                         val k = (L'.KType, loc)
-                                        val dk = ExplUtil.classifyDatatype xnts
+                                        val dk = ElabUtil.classifyDatatype xnts
                                         val (st, n') = St.bindCon st x n
                                         val (xnts, (ds', st, cmap, conmap)) =
                                             ListUtil.foldlMap
--- a/src/elab.sml	Sat Aug 09 16:54:04 2008 -0400
+++ b/src/elab.sml	Sat Aug 09 19:23:31 2008 -0400
@@ -73,6 +73,7 @@
 
 datatype datatype_kind =
          Enum
+       | Option
        | Default
 
 datatype patCon =
--- a/src/elab_util.sig	Sat Aug 09 16:54:04 2008 -0400
+++ b/src/elab_util.sig	Sat Aug 09 19:23:31 2008 -0400
@@ -27,7 +27,7 @@
 
 signature ELAB_UTIL = sig
 
-val classifyDatatype : (string * int * Elab.con option) list -> Elab.datatype_kind
+val classifyDatatype : (string * int * 'a option) list -> Elab.datatype_kind
 
 structure Kind : sig
     val mapfold : (Elab.kind', 'state, 'abort) Search.mapfolder
--- a/src/elab_util.sml	Sat Aug 09 16:54:04 2008 -0400
+++ b/src/elab_util.sml	Sat Aug 09 19:23:31 2008 -0400
@@ -30,10 +30,14 @@
 open Elab
 
 fun classifyDatatype xncs =
-    if List.all (fn (_, _, NONE) => true | _ => false) xncs then
-        Enum
-    else
-        Default
+    case xncs of
+        [(_, _, NONE), (_, _, SOME _)] => Option
+      | [(_, _, SOME _), (_, _, NONE)] => Option
+      | _ =>
+        if List.all (fn (_, _, NONE) => true | _ => false) xncs then
+            Enum
+        else
+            Default
 
 structure S = Search
 
--- a/src/expl_util.sig	Sat Aug 09 16:54:04 2008 -0400
+++ b/src/expl_util.sig	Sat Aug 09 19:23:31 2008 -0400
@@ -27,8 +27,6 @@
 
 signature EXPL_UTIL = sig
 
-val classifyDatatype : (string * int * Expl.con option) list -> Expl.datatype_kind
-
 structure Kind : sig
     val mapfold : (Expl.kind', 'state, 'abort) Search.mapfolder
                   -> (Expl.kind, 'state, 'abort) Search.mapfolder
--- a/src/expl_util.sml	Sat Aug 09 16:54:04 2008 -0400
+++ b/src/expl_util.sml	Sat Aug 09 19:23:31 2008 -0400
@@ -29,12 +29,6 @@
 
 open Expl
 
-fun classifyDatatype xncs =
-    if List.all (fn (_, _, NONE) => true | _ => false) xncs then
-        Enum
-    else
-        Default
-
 structure S = Search
 
 structure Kind = struct
--- a/src/mono_env.sml	Sat Aug 09 16:54:04 2008 -0400
+++ b/src/mono_env.sml	Sat Aug 09 19:23:31 2008 -0400
@@ -98,7 +98,7 @@
         DDatatype (x, n, xncs) =>
         let
             val env = pushDatatype env x n xncs
-            val dt = (TDatatype (n, ref (MonoUtil.classifyDatatype xncs, xncs)), loc)
+            val dt = (TDatatype (n, ref (ElabUtil.classifyDatatype xncs, xncs)), loc)
         in
             foldl (fn ((x', n', NONE), env) => pushENamed env x' n' dt NONE ""
                     | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, dt), loc) NONE "")
--- a/src/mono_util.sig	Sat Aug 09 16:54:04 2008 -0400
+++ b/src/mono_util.sig	Sat Aug 09 19:23:31 2008 -0400
@@ -27,8 +27,6 @@
 
 signature MONO_UTIL = sig
 
-val classifyDatatype : (string * int * Mono.typ option) list -> Mono.datatype_kind
-
 structure Typ : sig
     val compare : Mono.typ * Mono.typ -> order
     val sortFields : (string * Mono.typ) list -> (string * Mono.typ) list
--- a/src/mono_util.sml	Sat Aug 09 16:54:04 2008 -0400
+++ b/src/mono_util.sml	Sat Aug 09 19:23:31 2008 -0400
@@ -29,12 +29,6 @@
 
 open Mono
 
-fun classifyDatatype xncs =
-    if List.all (fn (_, _, NONE) => true | _ => false) xncs then
-        Enum
-    else
-        Default
-
 structure S = Search
 
 structure Typ = struct
@@ -354,7 +348,7 @@
                                         DDatatype (x, n, xncs) =>
                                         let
                                             val ctx = bind (ctx, Datatype (x, n, xncs))
-                                            val t = (TDatatype (n, ref (classifyDatatype xncs, xncs)), #2 d')
+                                            val t = (TDatatype (n, ref (ElabUtil.classifyDatatype xncs, xncs)), #2 d')
                                         in
                                             foldl (fn ((x, n, to), ctx) =>
                                                       let
--- a/src/monoize.sml	Sat Aug 09 16:54:04 2008 -0400
+++ b/src/monoize.sml	Sat Aug 09 19:23:31 2008 -0400
@@ -84,7 +84,7 @@
                              val xncs = map (fn (x, n, to) => (x, n, Option.map (mt env dtmap') to)) xncs
                          in
                              case xs of
-                                 [] =>(r := (MonoUtil.classifyDatatype xncs, xncs);
+                                 [] =>(r := (ElabUtil.classifyDatatype xncs, xncs);
                                        (L'.TDatatype (n, r), loc))
                                | _ => poly ()
                          end)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/option.lac	Sat Aug 09 19:23:31 2008 -0400
@@ -0,0 +1,25 @@
+datatype option a = None | Some of a
+
+val none_Hi : option string = None
+val some_Hi = Some "Hi"
+val none_some_Hi : option (option string) = None
+val some_some_Hi = Some some_Hi
+
+val show = fn x => case x of None => "None" | Some x => x
+
+val show2 = fn x => case x of None => "None'" | Some x => show x
+
+val page = fn x => <html><body>
+        {cdata (show x)}
+</body></html>
+
+val page2 = fn x => <html><body>
+        {cdata (show2 x)}
+</body></html>
+
+val main : unit -> page = fn () => <html><body>
+        <li><a link={page none_Hi}>None1</a></li>
+        <li><a link={page some_Hi}>Some1</a></li>
+        <li><a link={page2 none_some_Hi}>None2</a></li>
+        <li><a link={page2 some_some_Hi}>Some2</a></li>
+</body></html>