From 0186af3d727b1b92e7b63925500a21d5e412d7b4 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 9 Aug 2008 19:23:31 -0400 Subject: 'Option' datatype encoding --- src/c/lacweb.c | 4 +- src/cjr_print.sml | 164 ++++++++++++++++++++++++++++++++++++++++++++++++++---- src/cjrize.sml | 2 +- src/core_util.sig | 2 - src/core_util.sml | 6 -- src/corify.sml | 4 +- src/elab.sml | 1 + src/elab_util.sig | 2 +- src/elab_util.sml | 12 ++-- src/expl_util.sig | 2 - src/expl_util.sml | 6 -- src/mono_env.sml | 2 +- src/mono_util.sig | 2 - src/mono_util.sml | 8 +-- src/monoize.sml | 2 +- 15 files changed, 170 insertions(+), 49 deletions(-) (limited to 'src') diff --git a/src/c/lacweb.c b/src/c/lacweb.c index 12985b4f..9f17103a 100644 --- a/src/c/lacweb.c +++ b/src/c/lacweb.c @@ -471,11 +471,11 @@ lw_Basis_string lw_Basis_unurlifyString(lw_context ctx, char **s) { 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; } diff --git a/src/cjr_print.sml b/src/cjr_print.sml index 6d115fd1..be13461e 100644 --- a/src/cjr_print.sml +++ b/src/cjr_print.sml @@ -74,6 +74,14 @@ fun p_typ' par env (t, loc) = 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 @@ fun p_pat (env, exit, depth) (p, _) = 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 @@ fun p_pat (env, exit, depth) (p, _) = 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 @@ fun p_exp' par env (e, loc) = | 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 @@ fun p_decl env (dAll as (d, _) : decl) = 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 @@ fun p_file env (ds, ps) = 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 @@ fun p_file env (ds, ps) = 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)), diff --git a/src/cjrize.sml b/src/cjrize.sml index 166e5fcc..c745f43a 100644 --- a/src/cjrize.sml +++ b/src/cjrize.sml @@ -282,7 +282,7 @@ fun cifyDecl ((d, loc), sm) = 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) diff --git a/src/core_util.sig b/src/core_util.sig index aa957794..43750698 100644 --- a/src/core_util.sig +++ b/src/core_util.sig @@ -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 diff --git a/src/core_util.sml b/src/core_util.sml index e89a579b..f79e6d20 100644 --- a/src/core_util.sml +++ b/src/core_util.sml @@ -29,12 +29,6 @@ structure CoreUtil :> CORE_UTIL = struct open Core -fun classifyDatatype xncs = - if List.all (fn (_, _, NONE) => true | _ => false) xncs then - Enum - else - Default - structure S = Search structure Kind = struct diff --git a/src/corify.sml b/src/corify.sml index 9c350aee..eb46eec8 100644 --- a/src/corify.sml +++ b/src/corify.sml @@ -532,7 +532,7 @@ structure St : sig ((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 @@ structure St : sig | 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 diff --git a/src/elab.sml b/src/elab.sml index c04b5d23..011bc8d2 100644 --- a/src/elab.sml +++ b/src/elab.sml @@ -73,6 +73,7 @@ withtype con = con' located datatype datatype_kind = Enum + | Option | Default datatype patCon = diff --git a/src/elab_util.sig b/src/elab_util.sig index 5be47ed6..e33e956b 100644 --- a/src/elab_util.sig +++ b/src/elab_util.sig @@ -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 diff --git a/src/elab_util.sml b/src/elab_util.sml index 1c67fbb2..5fa0fa27 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -30,10 +30,14 @@ structure ElabUtil :> ELAB_UTIL = struct 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 diff --git a/src/expl_util.sig b/src/expl_util.sig index d15e7a76..2a6c7abe 100644 --- a/src/expl_util.sig +++ b/src/expl_util.sig @@ -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 diff --git a/src/expl_util.sml b/src/expl_util.sml index 8ec85b19..ef82af44 100644 --- a/src/expl_util.sml +++ b/src/expl_util.sml @@ -29,12 +29,6 @@ structure ExplUtil :> EXPL_UTIL = struct open Expl -fun classifyDatatype xncs = - if List.all (fn (_, _, NONE) => true | _ => false) xncs then - Enum - else - Default - structure S = Search structure Kind = struct diff --git a/src/mono_env.sml b/src/mono_env.sml index 60b22642..6baf8b07 100644 --- a/src/mono_env.sml +++ b/src/mono_env.sml @@ -98,7 +98,7 @@ fun declBinds env (d, loc) = 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 "") diff --git a/src/mono_util.sig b/src/mono_util.sig index 1e94403f..4e9d5d91 100644 --- a/src/mono_util.sig +++ b/src/mono_util.sig @@ -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 diff --git a/src/mono_util.sml b/src/mono_util.sml index 3c76e029..50927ac9 100644 --- a/src/mono_util.sml +++ b/src/mono_util.sml @@ -29,12 +29,6 @@ structure MonoUtil :> MONO_UTIL = struct 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 @@ fun mapfoldB (all as {bind, ...}) = 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 diff --git a/src/monoize.sml b/src/monoize.sml index 98b9075a..8d7fabb8 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -84,7 +84,7 @@ fun monoType env = 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) -- cgit v1.2.3