[MLton] cvs commit: datatype declarations with free type variables
Stephen Weeks
sweeks@mlton.org
Thu, 29 Jan 2004 17:56:01 -0800
sweeks 04/01/29 17:56:01
Modified: doc/user-guide bugs.tex
mlton/defunctorize defunctorize.fun
mlton/elaborate scope.fun
Added: regression datatype-with-free-tyvars.ok
datatype-with-free-tyvars.sml
Removed: regression/fail 5.sml
Log:
MAIL datatype declarations with free type variables
Allow datatype declarations with free type variables. This is now
sound because we implement the rule that prevents a local datatype
from escaping its defining let. It is implemented in the translation
from CoreML to XML, which is where datatypes are lifted to top level.
The translation adds any free type variables as extra arguments to the
type constructor and value constructors. For example
fun 'a f () =
let
...
datatype 'b t = T of 'a * 'b
...
e : int t
moves the datatype to the top level as
datatype ('a, 'b) t = T of 'a * 'b
and replaces "int t" with "('a, int) t".
Revision Changes Path
1.13 +0 -13 mlton/doc/user-guide/bugs.tex
Index: bugs.tex
===================================================================
RCS file: /cvsroot/mlton/mlton/doc/user-guide/bugs.tex,v
retrieving revision 1.12
retrieving revision 1.13
diff -u -r1.12 -r1.13
--- bugs.tex 29 Jan 2004 03:05:17 -0000 1.12
+++ bugs.tex 30 Jan 2004 01:56:00 -0000 1.13
@@ -14,19 +14,6 @@
\begin{itemize}
\item
-{\mlton} rejects datatype declarations with type variables bound at
-an outer level. For example, the following program is rejected,
-although it is allowed by the Definition.
-\begin{verbatim}
-fun 'a f (x : 'a) =
- let datatype t = T of 'a * int
- in 13
- end
-\end{verbatim}
-This may be an oversight in the Definition, since unchecked use of
-this feature can lead to type unsoundness.
-
-\item
{\mlton} rejects rebinding of constructors with {\tt val rec}
declarations, as in
\begin{verbatim}
1.10 +107 -30 mlton/mlton/defunctorize/defunctorize.fun
Index: defunctorize.fun
===================================================================
RCS file: /cvsroot/mlton/mlton/mlton/defunctorize/defunctorize.fun,v
retrieving revision 1.9
retrieving revision 1.10
diff -u -r1.9 -r1.10
--- defunctorize.fun 31 Dec 2003 09:55:15 -0000 1.9
+++ defunctorize.fun 30 Jan 2004 01:56:00 -0000 1.10
@@ -329,8 +329,34 @@
fun defunctorize (CoreML.Program.T {decs}) =
let
- val {destroy, hom = loopTy} =
- Ctype.makeHom {con = Xtype.con, var = Xtype.var}
+ val {get = conExtraArgs: Con.t -> Xtype.t vector option,
+ set = setConExtraArgs, destroy = destroy1, ...} =
+ Property.destGetSetOnce (Con.plist, Property.initConst NONE)
+ val {get = tyconExtraArgs: Tycon.t -> Xtype.t vector option,
+ set = setTyconExtraArgs, destroy = destroy2, ...} =
+ Property.destGetSetOnce (Tycon.plist, Property.initConst NONE)
+ val {destroy = destroy3, hom = loopTy} =
+ let
+ fun con (c, ts) =
+ let
+ val ts =
+ case tyconExtraArgs c of
+ NONE => ts
+ | SOME ts' => Vector.concat [ts', ts]
+ in
+ Xtype.con (c, ts)
+ end
+ in
+ Ctype.makeHom {con = con, var = Xtype.var}
+ end
+ fun conTargs (c: Con.t, ts: Ctype.t vector): Xtype.t vector =
+ let
+ val ts = Vector.map (ts, loopTy)
+ in
+ case conExtraArgs c of
+ NONE => ts
+ | SOME ts' => Vector.concat [ts', ts]
+ end
val {get = conTycon, set = setConTycon, ...} =
Property.getSetOnce (Con.plist,
Property.initRaise ("conTycon", Con.layout))
@@ -352,30 +378,81 @@
in
case d of
Datatype dbs =>
- Vector.foreach
- (dbs, fn {cons, tycon, tyvars} =>
- let
- val _ =
- setTyconCons (tycon,
- Vector.map (cons, fn {arg, con} =>
- {con = con,
- hasArg = isSome arg}))
- val cons =
- Vector.map
- (cons, fn {arg, con} =>
- (setConTycon (con, tycon)
- ; {arg = Option.map (arg, loopTy),
- con = con}))
- val _ =
- if Tycon.equals (tycon, Tycon.reff)
- then ()
- else
- List.push (datatypes, {cons = cons,
- tycon = tycon,
- tyvars = tyvars})
- in
- ()
- end)
+ let
+ val frees: Tyvar.t list ref = ref []
+ val _ =
+ Vector.foreach
+ (dbs, fn {cons, tycon, tyvars} =>
+ let
+ fun var (a: Tyvar.t): unit =
+ let
+ fun eq a' = Tyvar.equals (a, a')
+ in
+ if Vector.exists (tyvars, eq)
+ orelse List.exists (!frees, eq)
+ then ()
+ else List.push (frees, a)
+ end
+ val {destroy, hom} =
+ Ctype.makeHom {con = fn _ => (),
+ var = var}
+ val _ =
+ Vector.foreach (cons, fn {arg, ...} =>
+ Option.app (arg, hom))
+ val _ = destroy ()
+ in
+ ()
+ end)
+ val frees = !frees
+ val dbs =
+ if List.isEmpty frees
+ then dbs
+ else
+ let
+ val frees = Vector.fromList frees
+ val extra = Vector.map (frees, Xtype.var)
+ in
+ Vector.map
+ (dbs, fn {cons, tycon, tyvars} =>
+ let
+ val _ = setTyconExtraArgs (tycon, SOME extra)
+ val _ =
+ Vector.foreach
+ (cons, fn {con, ...} =>
+ setConExtraArgs (con, SOME extra))
+ in
+ {cons = cons,
+ tycon = tycon,
+ tyvars = Vector.concat [frees, tyvars]}
+ end)
+ end
+ in
+ Vector.foreach
+ (dbs, fn {cons, tycon, tyvars} =>
+ let
+ val _ =
+ setTyconCons (tycon,
+ Vector.map (cons, fn {arg, con} =>
+ {con = con,
+ hasArg = isSome arg}))
+ val cons =
+ Vector.map
+ (cons, fn {arg, con} =>
+ (setConTycon (con, tycon)
+ ; {arg = Option.map (arg, loopTy),
+ con = con}))
+
+ val _ =
+ if Tycon.equals (tycon, Tycon.reff)
+ then ()
+ else
+ List.push (datatypes, {cons = cons,
+ tycon = tycon,
+ tyvars = tyvars})
+ in
+ ()
+ end)
+ end
| Exception {con, ...} => setConTycon (con, Tycon.exn)
| Fun {decs, ...} => Vector.foreach (decs, loopLambda o #lambda)
| Val {rvbs, vbs, ...} =>
@@ -416,7 +493,7 @@
Con {arg, con, targs} =>
NestedPat.Con {arg = Option.map (arg, loopPat),
con = con,
- targs = Vector.map (targs, loopTy)}
+ targs = conTargs (con, targs)}
| Const f =>
NestedPat.Const {const = f (),
isChar = Ctype.isChar t}
@@ -637,7 +714,7 @@
Con (con, targs) =>
conApp {arg = e2,
con = con,
- targs = Vector.map (targs, loopTy),
+ targs = conTargs (con, targs),
ty = ty}
| _ =>
Xexp.app {arg = e2,
@@ -662,7 +739,7 @@
tyconCons = tyconCons}
| Con (con, targs) =>
let
- val targs = Vector.map (targs, loopTy)
+ val targs = conTargs (con, targs)
in
case Xtype.deArrowOpt ty of
NONE =>
@@ -794,7 +871,7 @@
end
val body = Xexp.toExp (loopDecs (decs, (Xexp.unit (), Xtype.unit)))
val _ = List.foreach (!warnings, fn f => f ())
- val _ = destroy ()
+ val _ = (destroy1 (); destroy2 (); destroy3 ())
in
Xml.Program.T {body = body,
datatypes = Vector.fromList (!datatypes),
1.10 +5 -51 mlton/mlton/elaborate/scope.fun
Index: scope.fun
===================================================================
RCS file: /cvsroot/mlton/mlton/mlton/elaborate/scope.fun,v
retrieving revision 1.9
retrieving revision 1.10
diff -u -r1.9 -r1.10
--- scope.fun 23 Jan 2004 02:30:23 -0000 1.9
+++ scope.fun 30 Jan 2004 01:56:00 -0000 1.10
@@ -39,13 +39,7 @@
fun ('down, 'up)
processDec (d: Dec.t,
- {
- (* bindDatatype is used at datatype declarations. *)
- bindDatatype: ('down * Tyvar.t vector * Region.t
- -> ('down
- * Tyvar.t vector
- * ('up -> 'up))),
- (* bindType is used at type declarations. *)
+ {(* bindType is used at datatype and type declarations. *)
bindType: ('down * Tyvar.t vector
-> 'down * Tyvar.t vector * ('up -> 'up)),
(* bindFunVal is used at fun, overload, and val declarations. *)
@@ -130,8 +124,7 @@
loops
(datatypes, fn {cons, tycon, tyvars} =>
let
- val (d, tyvars, up) =
- bindDatatype (d, tyvars, DatBind.region db)
+ val (d, tyvars, up) = bindType (d, tyvars)
val (cons, u) =
loops (cons, fn (con, arg) =>
let
@@ -443,42 +436,6 @@
let
type up = {free: Tyvars.t,
mayNotBind: Tyvar.t list}
- (* Walk down the tree and rename all explicitly bound tyvars. On the way
- * back up, bind implicitly scoped tyvars at each possible point.
- *)
- fun bindDatatype (_, tyvars, region) =
- let
- val (env, tyvars) = Env.rename (Env.empty, tyvars)
- fun finish ({free, ...}: up): up =
- let
- val free =
- Tyvars.toList
- (Tyvars.- (free, Tyvars.fromList (Vector.toList tyvars)))
- val _ =
- if 0 = List.length free
- then ()
- else
- let
- open Layout
- in
- Control.error
- (region,
- seq [str (concat ["free type variable",
- if List.length free > 1
- then "s"
- else "",
- " in datatype declaration: "]),
- seq (separate (List.map (free, Tyvar.layout),
- ", "))],
- empty)
- end
- in
- {free = Tyvars.empty,
- mayNotBind = []}
- end
- in
- (env, tyvars, finish)
- end
fun bindFunVal (env, tyvars) =
let
val (env, tyvars) = Env.rename (env, tyvars)
@@ -519,7 +476,7 @@
val (env, tyvars) = Env.rename (env, tyvars)
fun finish {free, mayNotBind} =
{free = Tyvars.- (free, Tyvars.fromList (Vector.toList tyvars)),
- mayNotBind = Tyvars.empty}
+ mayNotBind = []}
in
(env, tyvars, finish)
end
@@ -537,8 +494,7 @@
{free = Tyvars.+ (f, f'),
mayNotBind = List.append (m, m')}
val (dec, {free = unguarded, ...}) =
- processDec (dec, {bindDatatype = bindDatatype,
- bindFunVal = bindFunVal,
+ processDec (dec, {bindFunVal = bindFunVal,
bindType = bindType,
combineUp = combineUp,
initDown = Env.empty,
@@ -572,11 +528,9 @@
in
(env, tyvars, fn () => ())
end
- fun bindDatatype (env, tyvars, _) = bindType (env, tyvars)
fun tyvar (a, env) = (Env.lookup (env, a), ())
val (dec, ()) =
- processDec (dec, {bindDatatype = bindDatatype,
- bindFunVal = bindFunVal,
+ processDec (dec, {bindFunVal = bindFunVal,
bindType = bindType,
combineUp = fn ((), ()) => (),
initDown = Env.empty,
1.1 mlton/regression/datatype-with-free-tyvars.ok
Index: datatype-with-free-tyvars.ok
===================================================================
true 13
false foo
1.1 mlton/regression/datatype-with-free-tyvars.sml
Index: datatype-with-free-tyvars.sml
===================================================================
fun 'a f (x1: 'a, x2: 'a, aToString: 'a -> string): unit =
let
datatype 'b t = T of 'a * 'b
and u = U of int t
val y1: int t = T (x1, 13)
val _: u = U y1
val y2 = T (x2, "foo")
fun 'b g (T (a, b), bToString: 'b -> string): unit =
print (concat [aToString a, " ", bToString b, "\n"])
val _ = g (y1, Int.toString)
val _ = g (y2, fn s => s)
in
()
end
val _ = f (true, false, Bool.toString)