Mercurial > urweb
changeset 808:d8f58d488cfb
Mutual datatypes through Pathcheck
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 16 May 2009 15:55:15 -0400 |
| parents | 61a1f5c5ae2c |
| children | 81fce435e255 |
| files | src/cjrize.sml src/jscomp.sml src/mono.sml src/mono_env.sml src/mono_print.sml src/mono_shake.sml src/mono_util.sml src/monoize.sml |
| diffstat | 8 files changed, 81 insertions(+), 70 deletions(-) [+] |
line wrap: on
line diff
--- a/src/cjrize.sml Sat May 16 15:45:12 2009 -0400 +++ b/src/cjrize.sml Sat May 16 15:55:15 2009 -0400 @@ -483,7 +483,8 @@ 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 @@ end) sm xncs in (SOME (L'.DDatatype (dk, x, n, xncs), loc), NONE, sm) - end + end*) | L.DVal (x, n, t, e, _) => let
--- a/src/jscomp.sml Sat May 16 15:45:12 2009 -0400 +++ b/src/jscomp.sml Sat May 16 15:55:15 2009 -0400 @@ -176,13 +176,14 @@ | ((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
--- a/src/mono.sml Sat May 16 15:45:12 2009 -0400 +++ b/src/mono.sml Sat May 16 15:55:15 2009 -0400 @@ -121,7 +121,7 @@ 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
--- a/src/mono_env.sml Sat May 16 15:45:12 2009 -0400 +++ b/src/mono_env.sml Sat May 16 15:55:15 2009 -0400 @@ -109,15 +109,16 @@ 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
--- a/src/mono_print.sml Sat May 16 15:45:12 2009 -0400 +++ b/src/mono_print.sml Sat May 16 15:55:15 2009 -0400 @@ -377,9 +377,7 @@ 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_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]
--- a/src/mono_shake.sml Sat May 16 15:45:12 2009 -0400 +++ b/src/mono_shake.sml Sat May 16 15:55:15 2009 -0400 @@ -48,8 +48,8 @@ | ((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 @@ 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
--- a/src/mono_util.sml Sat May 16 15:45:12 2009 -0400 +++ b/src/mono_util.sml Sat May 16 15:55:15 2009 -0400 @@ -466,15 +466,17 @@ 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 @@ 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 @@ 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
--- a/src/monoize.sml Sat May 16 15:45:12 2009 -0400 +++ b/src/monoize.sml Sat May 16 15:55:15 2009 -0400 @@ -3045,27 +3045,30 @@ in case d of L.DCon _ => NONE - | L.DDatatype _ => raise Fail "Monoize DDatatype" - (*| L.DDatatype (x, n, [], xncs) => - 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) - 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, _)), - _))]), _), _))]) => + | 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.DDatatype dts => + let + val env' = Env.declBinds env all + 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.DVal (x, n, t, e, s) => let val (e, fm) = monoExp (env, St.empty, fm) e