aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-05-16 15:55:15 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-05-16 15:55:15 -0400
commit30b78a96ae699fa2282c07a2dbf3e6303f99e32c (patch)
tree42c21054472ff028fbeaba0f8af6534d23662ad0
parent41f7bb23ff2a9598f8f3bff1487f39f9e91f9f05 (diff)
Mutual datatypes through Pathcheck
-rw-r--r--src/cjrize.sml5
-rw-r--r--src/jscomp.sml15
-rw-r--r--src/mono.sml2
-rw-r--r--src/mono_env.sml19
-rw-r--r--src/mono_print.sml8
-rw-r--r--src/mono_shake.sml6
-rw-r--r--src/mono_util.sml59
-rw-r--r--src/monoize.sml35
8 files changed, 80 insertions, 69 deletions
diff --git a/src/cjrize.sml b/src/cjrize.sml
index 80d9842a..9c2128bc 100644
--- a/src/cjrize.sml
+++ b/src/cjrize.sml
@@ -483,7 +483,8 @@ fun cifyExp (eAll as (e, loc), sm) =
fun cifyDecl ((d, loc), sm) =
case d of
- L.DDatatype (x, n, xncs) =>
+ L.DDatatype _ => raise Fail "Cjrize DDatatype"
+ (*L.DDatatype (x, n, xncs) =>
let
val dk = ElabUtil.classifyDatatype xncs
val (xncs, sm) = ListUtil.foldlMap (fn ((x, n, to), sm) =>
@@ -497,7 +498,7 @@ fun cifyDecl ((d, loc), sm) =
end) sm xncs
in
(SOME (L'.DDatatype (dk, x, n, xncs), loc), NONE, sm)
- end
+ end*)
| L.DVal (x, n, t, e, _) =>
let
diff --git a/src/jscomp.sml b/src/jscomp.sml
index e0954ba0..20408cba 100644
--- a/src/jscomp.sml
+++ b/src/jscomp.sml
@@ -176,13 +176,14 @@ fun process file =
| ((DValRec vis, _), (someTs, nameds)) =>
(someTs, foldl (fn ((_, n, _, e, _), nameds) => IM.insert (nameds, n, e))
nameds vis)
- | ((DDatatype (_, _, cs), _), state as (someTs, nameds)) =>
- if ElabUtil.classifyDatatype cs = Option then
- (foldl (fn ((_, n, SOME t), someTs) => IM.insert (someTs, n, t)
- | (_, someTs) => someTs) someTs cs,
- nameds)
- else
- state
+ | ((DDatatype dts, _), state as (someTs, nameds)) =>
+ (foldl (fn ((_, _, cs), someTs) =>
+ if ElabUtil.classifyDatatype cs = Option then
+ foldl (fn ((_, n, SOME t), someTs) => IM.insert (someTs, n, t)
+ | (_, someTs) => someTs) someTs cs
+ else
+ someTs) someTs dts,
+ nameds)
| (_, state) => state)
(IM.empty, IM.empty) file
diff --git a/src/mono.sml b/src/mono.sml
index fa149b21..52d24998 100644
--- a/src/mono.sml
+++ b/src/mono.sml
@@ -121,7 +121,7 @@ datatype exp' =
withtype exp = exp' located
datatype decl' =
- DDatatype of string * int * (string * int * typ option) list
+ DDatatype of (string * int * (string * int * typ option) list) list
| DVal of string * int * typ * exp * string
| DValRec of (string * int * typ * exp * string) list
| DExport of export_kind * string * int * typ list * typ
diff --git a/src/mono_env.sml b/src/mono_env.sml
index 2397637a..3114176d 100644
--- a/src/mono_env.sml
+++ b/src/mono_env.sml
@@ -109,15 +109,16 @@ fun lookupENamed (env : env) n =
fun declBinds env (d, loc) =
case d of
- DDatatype (x, n, xncs) =>
- let
- val env = pushDatatype env x n xncs
- 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 "")
- env xncs
- end
+ DDatatype dts =>
+ foldl (fn ((x, n, xncs), env) =>
+ let
+ val env = pushDatatype env x n xncs
+ 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 "")
+ env xncs
+ end) env dts
| DVal (x, n, t, e, s) => pushENamed env x n t (SOME e) s
| DValRec vis => foldl (fn ((x, n, t, e, s), env) => pushENamed env x n t NONE s) env vis
| DExport _ => env
diff --git a/src/mono_print.sml b/src/mono_print.sml
index 2299bc56..0395a063 100644
--- a/src/mono_print.sml
+++ b/src/mono_print.sml
@@ -377,9 +377,7 @@ fun p_datatype env (x, n, cons) =
let
val env = E.pushDatatype env x n cons
in
- box [string "datatype",
- space,
- string x,
+ box [string x,
space,
string "=",
space,
@@ -393,7 +391,9 @@ fun p_datatype env (x, n, cons) =
fun p_decl env (dAll as (d, _) : decl) =
case d of
- DDatatype x => p_datatype env x
+ DDatatype x => box [string "datatype",
+ space,
+ p_list_sep (box [space, string "and", space]) (p_datatype (E.declBinds env dAll)) x]
| DVal vi => box [string "val",
space,
p_vali env vi]
diff --git a/src/mono_shake.sml b/src/mono_shake.sml
index 4764feb7..40b83934 100644
--- a/src/mono_shake.sml
+++ b/src/mono_shake.sml
@@ -48,8 +48,8 @@ fun shake file =
| ((DDatabase {expunge = n1, initialize = n2, ...}, _), page_es) => n1 :: n2 :: page_es
| (_, page_es) => page_es) [] file
- val (cdef, edef) = foldl (fn ((DDatatype (_, n, xncs), _), (cdef, edef)) =>
- (IM.insert (cdef, n, xncs), edef)
+ val (cdef, edef) = foldl (fn ((DDatatype dts, _), (cdef, edef)) =>
+ (foldl (fn ((_, n, xncs), cdef) => IM.insert (cdef, n, xncs)) cdef dts, edef)
| ((DVal (_, n, t, e, _), _), (cdef, edef)) =>
(cdef, IM.insert (edef, n, (t, e)))
| ((DValRec vis, _), (cdef, edef)) =>
@@ -111,7 +111,7 @@ fun shake file =
NONE => raise Fail "Shake: Couldn't find 'val'"
| SOME (t, e) => shakeExp s e) s page_es
in
- List.filter (fn (DDatatype (_, n, _), _) => IS.member (#con s, n)
+ List.filter (fn (DDatatype dts, _) => List.exists (fn (_, n, _) => IS.member (#con s, n)) dts
| (DVal (_, n, _, _, _), _) => IS.member (#exp s, n)
| (DValRec vis, _) => List.exists (fn (_, n, _, _, _) => IS.member (#exp s, n)) vis
| (DExport _, _) => true
diff --git a/src/mono_util.sml b/src/mono_util.sml
index ca074d9e..83621c99 100644
--- a/src/mono_util.sml
+++ b/src/mono_util.sml
@@ -466,15 +466,17 @@ fun mapfoldB {typ = fc, exp = fe, decl = fd, bind} =
and mfd' ctx (dAll as (d, loc)) =
case d of
- DDatatype (x, n, xncs) =>
- S.map2 (ListUtil.mapfold (fn (x, n, c) =>
- case c of
- NONE => S.return2 (x, n, c)
- | SOME c =>
- S.map2 (mft c,
- fn c' => (x, n, SOME c'))) xncs,
- fn xncs' =>
- (DDatatype (x, n, xncs'), loc))
+ DDatatype dts =>
+ S.map2 (ListUtil.mapfold (fn (x, n, xncs) =>
+ S.map2 (ListUtil.mapfold (fn (x, n, c) =>
+ case c of
+ NONE => S.return2 (x, n, c)
+ | SOME c =>
+ S.map2 (mft c,
+ fn c' => (x, n, SOME c'))) xncs,
+ fn xncs' => (x, n, xncs'))) dts,
+ fn dts' =>
+ (DDatatype dts', loc))
| DVal vi =>
S.map2 (mfvi ctx vi,
fn vi' =>
@@ -566,21 +568,23 @@ fun mapfoldB (all as {bind, ...}) =
let
val ctx' =
case #1 d' of
- DDatatype (x, n, xncs) =>
- let
- val ctx = bind (ctx, Datatype (x, n, xncs))
- val t = (TDatatype (n, ref (ElabUtil.classifyDatatype xncs, xncs)), #2 d')
- in
- foldl (fn ((x, n, to), ctx) =>
- let
- val t = case to of
- NONE => t
- | SOME t' => (TFun (t', t), #2 d')
- in
- bind (ctx, NamedE (x, n, t, NONE, ""))
- end)
- ctx xncs
- end
+ DDatatype dts =>
+ foldl (fn ((x, n, xncs), ctx) =>
+ let
+ val ctx = bind (ctx, Datatype (x, n, xncs))
+ val t = (TDatatype (n, ref (ElabUtil.classifyDatatype xncs, xncs)),
+ #2 d')
+ in
+ foldl (fn ((x, n, to), ctx) =>
+ let
+ val t = case to of
+ NONE => t
+ | SOME t' => (TFun (t', t), #2 d')
+ in
+ bind (ctx, NamedE (x, n, t, NONE, ""))
+ end)
+ ctx xncs
+ end) ctx dts
| DVal (x, n, t, e, s) => bind (ctx, NamedE (x, n, t, SOME e, s))
| DValRec vis => foldl (fn ((x, n, t, e, s), ctx) =>
bind (ctx, NamedE (x, n, t, NONE, s))) ctx vis
@@ -631,9 +635,10 @@ fun fold {typ, exp, decl} s d =
val maxName = foldl (fn ((d, _) : decl, count) =>
case d of
- DDatatype (_, n, ns) =>
- foldl (fn ((_, n', _), m) => Int.max (n', m))
- (Int.max (n, count)) ns
+ DDatatype dts =>
+ foldl (fn ((_, n, ns), count) =>
+ foldl (fn ((_, n', _), m) => Int.max (n', m))
+ (Int.max (n, count)) ns) count dts
| DVal (_, n, _, _, _) => Int.max (n, count)
| DValRec vis => foldl (fn ((_, n, _, _, _), count) => Int.max (n, count)) count vis
| DExport _ => count
diff --git a/src/monoize.sml b/src/monoize.sml
index e4175015..50bd04e8 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -3045,27 +3045,30 @@ fun monoDecl (env, fm) (all as (d, loc)) =
in
case d of
L.DCon _ => NONE
- | L.DDatatype _ => raise Fail "Monoize DDatatype"
- (*| L.DDatatype (x, n, [], xncs) =>
+ | L.DDatatype [("list", n, [_], [("Nil", _, NONE),
+ ("Cons", _, SOME (L.TRecord (L.CRecord (_,
+ [((L.CName "1", _),
+ (L.CRel 0, _)),
+ ((L.CName "2", _),
+ (L.CApp ((L.CNamed n', _),
+ (L.CRel 0, _)),
+ _))]), _), _))])] =>
+ if n = n' then
+ NONE
+ else
+ poly ()
+ | L.DDatatype dts =>
let
val env' = Env.declBinds env all
- val d = (L'.DDatatype (x, n, map (fn (x, n, to) => (x, n, Option.map (monoType env') to)) xncs), loc)
+ val dts = map (fn (x, n, [], xncs) =>
+ (x, n, map (fn (x, n, to) => (x, n, Option.map (monoType env') to)) xncs)
+ | _ => (E.errorAt loc "Polymorphic datatype needed too late";
+ Print.eprefaces' [("Declaration", CorePrint.p_decl env all)];
+ ("", 0, []))) dts
+ val d = (L'.DDatatype dts, loc)
in
SOME (env', fm, [d])
end
- | L.DDatatype ("list", n, [_], [("Nil", _, NONE),
- ("Cons", _, SOME (L.TRecord (L.CRecord (_,
- [((L.CName "1", _),
- (L.CRel 0, _)),
- ((L.CName "2", _),
- (L.CApp ((L.CNamed n', _),
- (L.CRel 0, _)),
- _))]), _), _))]) =>
- if n = n' then
- NONE
- else
- poly ()
- | L.DDatatype _ => poly ()*)
| L.DVal (x, n, t, e, s) =>
let
val (e, fm) = monoExp (env, St.empty, fm) e