summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/c/lacweb.c4
-rw-r--r--src/cjr_print.sml164
-rw-r--r--src/cjrize.sml2
-rw-r--r--src/core_util.sig2
-rw-r--r--src/core_util.sml6
-rw-r--r--src/corify.sml4
-rw-r--r--src/elab.sml1
-rw-r--r--src/elab_util.sig2
-rw-r--r--src/elab_util.sml12
-rw-r--r--src/expl_util.sig2
-rw-r--r--src/expl_util.sml6
-rw-r--r--src/mono_env.sml2
-rw-r--r--src/mono_util.sig2
-rw-r--r--src/mono_util.sml8
-rw-r--r--src/monoize.sml2
15 files changed, 170 insertions, 49 deletions
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)
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-17 06:22:56 +0000