Mercurial > urweb
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>