summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/core.sml2
-rw-r--r--src/core_env.sml19
-rw-r--r--src/core_print.sml8
-rw-r--r--src/core_util.sml87
-rw-r--r--src/corify.sml217
-rw-r--r--src/marshalcheck.sml13
-rw-r--r--src/monoize.sml5
-rw-r--r--src/reduce.sml15
-rw-r--r--src/shake.sml7
-rw-r--r--src/specialize.sml10
-rw-r--r--tests/mutual.ur8
-rw-r--r--tests/mutual.urs1
12 files changed, 224 insertions, 168 deletions
diff --git a/src/core.sml b/src/core.sml
index 131bcc6f..e7466746 100644
--- a/src/core.sml
+++ b/src/core.sml
@@ -124,7 +124,7 @@ datatype export_kind = datatype Export.export_kind
datatype decl' =
DCon of string * int * kind * con
- | DDatatype of string * int * string list * (string * int * con option) list
+ | DDatatype of (string * int * string list * (string * int * con option) list) list
| DVal of string * int * con * exp * string
| DValRec of (string * int * con * exp * string) list
| DExport of export_kind * int
diff --git a/src/core_env.sml b/src/core_env.sml
index 0630fef2..e8cd139f 100644
--- a/src/core_env.sml
+++ b/src/core_env.sml
@@ -301,15 +301,16 @@ fun lookupENamed (env : env) n =
fun declBinds env (d, loc) =
case d of
DCon (x, n, k, c) => pushCNamed env x n k (SOME c)
- | DDatatype (x, n, xs, xncs) =>
- let
- val env = pushDatatype env x n xs xncs
- val env = pushCNamed env x n (KType, loc) NONE
- in
- foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc) NONE ""
- | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc) NONE "")
- env xncs
- end
+ | DDatatype dts =>
+ foldl (fn ((x, n, xs, xncs), env) =>
+ let
+ val env = pushDatatype env x n xs xncs
+ val env = pushCNamed env x n (KType, loc) NONE
+ in
+ foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc) NONE ""
+ | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), 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/core_print.sml b/src/core_print.sml
index 8dcb3228..08739aea 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -496,9 +496,7 @@ fun p_datatype env (x, n, xs, cons) =
else
string x
in
- box [string "datatype",
- space,
- xp,
+ box [xp,
p_list_sep (box []) (fn x => box [space, string x]) xs,
space,
string "=",
@@ -534,7 +532,9 @@ fun p_decl env (dAll as (d, _) : decl) =
space,
p_con env c]
end
- | 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/core_util.sml b/src/core_util.sml
index 96a05b2d..db1eab1a 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -910,21 +910,23 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, decl = fd, bind} =
S.map2 (mfc ctx c,
fn c' =>
(DCon (x, n, k', c'), loc)))
- | DDatatype (x, n, xs, xncs) =>
- let
- val k = (KType, loc)
- val k' = foldl (fn (_, k') => (KArrow (k, k'), loc)) k xs
- val ctx' = bind (ctx, NamedC (x, n, k', NONE))
- in
- S.map2 (ListUtil.mapfold (fn (x, n, c) =>
- case c of
- NONE => S.return2 (x, n, c)
- | SOME c =>
- S.map2 (mfc ctx' c,
- fn c' => (x, n, SOME c'))) xncs,
- fn xncs' =>
- (DDatatype (x, n, xs, xncs'), loc))
- end
+ | DDatatype dts =>
+ S.map2 (ListUtil.mapfold (fn (x, n, xs, xncs) =>
+ let
+ val k = (KType, loc)
+ val k' = foldl (fn (_, k') => (KArrow (k, k'), loc)) k xs
+ val ctx' = bind (ctx, NamedC (x, n, k', NONE))
+ in
+ S.map2 (ListUtil.mapfold (fn (x, n, c) =>
+ case c of
+ NONE => S.return2 (x, n, c)
+ | SOME c =>
+ S.map2 (mfc ctx' c,
+ fn c' => (x, n, SOME c'))) xncs,
+ fn xncs' => (x, n, xs, xncs'))
+ end) dts,
+ fn dts' =>
+ (DDatatype dts', loc))
| DVal vi =>
S.map2 (mfvi ctx vi,
fn vi' =>
@@ -1059,29 +1061,32 @@ fun mapfoldB (all as {bind, ...}) =
val ctx' =
case #1 d' of
DCon (x, n, k, c) => bind (ctx, NamedC (x, n, k, SOME c))
- | DDatatype (x, n, xs, xncs) =>
- let
- val loc = #2 d'
- val k = (KType, loc)
- val k' = foldl (fn (_, k') => (KArrow (k, k'), loc)) k xs
-
- val ctx = bind (ctx, NamedC (x, n, k', NONE))
- val t = (CNamed n, #2 d')
- val t = ListUtil.foldli (fn (i, _, t) => (CApp (t, (CRel i, loc)), loc))
- t xs
- in
- foldl (fn ((x, n, to), ctx) =>
- let
- val t = case to of
- NONE => t
- | SOME t' => (TFun (t', t), #2 d')
- val t = foldr (fn (x, t) => (TCFun (x, k, t), loc))
- t xs
- in
- bind (ctx, NamedE (x, n, t, NONE, ""))
- end)
- ctx xncs
- end
+ | DDatatype dts =>
+ foldl (fn ((x, n, xs, xncs), ctx) =>
+ let
+ val loc = #2 d'
+ val k = (KType, loc)
+ val k' = foldl (fn (_, k') => (KArrow (k, k'), loc)) k xs
+
+ val ctx = bind (ctx, NamedC (x, n, k', NONE))
+ val t = (CNamed n, #2 d')
+ val t = ListUtil.foldli (fn (i, _, t) =>
+ (CApp (t, (CRel i, loc)), loc))
+ t xs
+ in
+ foldl (fn ((x, n, to), ctx) =>
+ let
+ val t = case to of
+ NONE => t
+ | SOME t' => (TFun (t', t), #2 d')
+ val t = foldr (fn (x, t) => (TCFun (x, k, t), loc))
+ t xs
+ 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)))
@@ -1174,9 +1179,9 @@ fun foldMap {kind, con, exp, decl} s d =
val maxName = foldl (fn ((d, _) : decl, count) =>
case d of
DCon (_, n, _, _) => Int.max (n, count)
- | 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/corify.sml b/src/corify.sml
index 9ac5c84e..6793cd32 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -621,45 +621,65 @@ fun corifyDecl mods (all as (d, loc : EM.span), st) =
in
([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st)
end
- | L.DDatatype _ => raise Fail "Corify DDatatype"
- (*| L.DDatatype (x, n, xs, xncs) =>
+ | L.DDatatype dts =>
let
- val (st, n) = St.bindCon st x n
- val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
- let
- val st = St.bindConstructor st x n (L'.PConVar n)
- val st = St.bindConstructorVal st x n
- val co = Option.map (corifyCon st) co
- in
- ((x, n, co), st)
- end) st 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
- val k = (L'.KType, loc)
- val dcons = map (fn (x, n, to) =>
- let
- val args = ListUtil.mapi (fn (i, _) => (L'.CRel (nxs - i), loc)) xs
- val (e, t) =
- case to of
- NONE => ((L'.ECon (dk, L'.PConVar n, args, NONE), loc), t)
- | SOME t' => ((L'.EAbs ("x", t', t,
- (L'.ECon (dk, L'.PConVar n, args,
- SOME (L'.ERel 0, loc)),
- loc)),
- loc),
- (L'.TFun (t', t), loc))
-
- val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs
- val e = foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs
- in
- (L'.DVal (x, n, t, e, ""), loc)
- end) xncs
+ val (dts, st) = ListUtil.foldlMap (fn ((x, n, xs, xncs), st) =>
+ let
+ val (st, n) = St.bindCon st x n
+ in
+ ((x, n, xs, xncs), st)
+ end)
+ st dts
+
+ val (dts, (st, dcons)) =
+ ListUtil.foldlMap
+ (fn ((x, n, xs, xncs), (st, dcons)) =>
+ let
+ val (xncs, st) = ListUtil.foldlMap
+ (fn ((x, n, co), st) =>
+ let
+ val st = St.bindConstructor st x n (L'.PConVar n)
+ val st = St.bindConstructorVal st x n
+ val co = Option.map (corifyCon st) co
+ in
+ ((x, n, co), st)
+ end) st 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
+ val k = (L'.KType, loc)
+ val dcons' = map (fn (x, n, to) =>
+ let
+ val args = ListUtil.mapi
+ (fn (i, _) => (L'.CRel (nxs - i), loc)) xs
+ val (e, t) =
+ case to of
+ NONE => ((L'.ECon (dk, L'.PConVar n, args, NONE),
+ loc), t)
+ | SOME t' => ((L'.EAbs ("x", t', t,
+ (L'.ECon (dk, L'.PConVar n,
+ args,
+ SOME (L'.ERel 0,
+ loc)),
+ loc)),
+ loc),
+ (L'.TFun (t', t), loc))
+
+ val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs
+ val e = foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs
+ in
+ (L'.DVal (x, n, t, e, ""), loc)
+ end) xncs
+ in
+ ((x, n, xs, xncs), (st, dcons' @ dcons))
+ end)
+ (st, []) dts
in
- ((L'.DDatatype (x, n, xs, xncs), loc) :: dcons, st)
- end*)
+ ((L'.DDatatype dts, loc) :: dcons, st)
+ end
| L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
let
val (st, n) = St.bindCon st x n
@@ -796,69 +816,86 @@ fun corifyDecl mods (all as (d, loc : EM.span), st) =
trans)
end
- | L.SgiDatatype _ => raise Fail "Corify SgiDatatype"
- (*| L.SgiDatatype (x, n, xs, xnts) =>
+ | L.SgiDatatype dts =>
let
val k = (L'.KType, loc)
- val dk = ElabUtil.classifyDatatype xnts
- val (st, n') = St.bindCon st x n
- val (xnts, (ds', st, cmap, conmap)) =
+
+ val (dts, (ds', st, cmap, conmap)) =
ListUtil.foldlMap
- (fn ((x', n, to), (ds', st, cmap, conmap)) =>
+ (fn ((x, n, xs, xnts), (ds', st, cmap, conmap)) =>
let
- val dt = (L'.CNamed n', loc)
- val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) xs
-
- val to = Option.map (corifyCon st) to
-
- val pc = L'.PConFfi {mod = m,
- datatyp = x,
- params = xs,
- con = x',
- arg = to,
- kind = dk}
-
- fun wrapT t =
- foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs
- fun wrapE e =
- foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs
-
- val (cmap, d) =
- case to of
- NONE => (SM.insert (cmap, x', wrapT dt),
- (L'.DVal (x', n, wrapT dt,
- wrapE
- (L'.ECon (dk, pc, args, NONE),
- loc),
- ""), loc))
- | SOME t =>
- let
- val tf = (L'.TFun (t, dt), loc)
- val e = wrapE (L'.EAbs ("x", t, tf,
- (L'.ECon (dk, pc, args,
- SOME (L'.ERel 0,
- loc)),
- loc)), loc)
- val d = (L'.DVal (x', n, wrapT tf,
- e, ""), loc)
- in
- (SM.insert (cmap, x', wrapT tf), d)
- end
-
- val st = St.bindConstructor st x' n pc
-
- val conmap = SM.insert (conmap, x', (x, xs, to, dk))
+ val dk = ElabUtil.classifyDatatype xnts
+ val (st, n') = St.bindCon st x n
+ val (xnts, (ds', st, cmap, conmap)) =
+ ListUtil.foldlMap
+ (fn ((x', n, to), (ds', st, cmap, conmap)) =>
+ let
+ val dt = (L'.CNamed n', loc)
+ val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) xs
+
+ val to = Option.map (corifyCon st) to
+
+ val pc = L'.PConFfi {mod = m,
+ datatyp = x,
+ params = xs,
+ con = x',
+ arg = to,
+ kind = dk}
+
+ fun wrapT t =
+ foldr (fn (x, t) => (L'.TCFun (x, k, t), loc))
+ t xs
+ fun wrapE e =
+ foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc))
+ e xs
+
+ val (cmap, d) =
+ case to of
+ NONE => (SM.insert (cmap, x', wrapT dt),
+ (L'.DVal (x', n, wrapT dt,
+ wrapE
+ (L'.ECon (dk, pc,
+ args,
+ NONE),
+ loc),
+ ""), loc))
+ | SOME t =>
+ let
+ val tf = (L'.TFun (t, dt), loc)
+ val e = wrapE
+ (L'.EAbs ("x", t, tf,
+ (L'.ECon (dk,
+ pc,
+ args,
+ SOME
+ (L'.ERel 0,
+ loc)),
+ loc)), loc)
+ val d = (L'.DVal (x', n, wrapT tf,
+ e, ""), loc)
+ in
+ (SM.insert (cmap, x', wrapT tf), d)
+ end
+
+ val st = St.bindConstructor st x' n pc
+
+ val conmap = SM.insert (conmap, x',
+ (x, xs, to, dk))
+ in
+ ((x', n, to),
+ (d :: ds', st, cmap, conmap))
+ end) (ds', st, cmap, conmap) xnts
in
- ((x', n, to),
- (d :: ds', st, cmap, conmap))
- end) ([], st, cmap, conmap) xnts
+ ((x, n', xs, xnts), (ds', st, cmap, conmap))
+ end)
+ ([], st, cmap, conmap) dts
in
- (ds' @ (L'.DDatatype (x, n', xs, xnts), loc) :: ds,
+ (ds' @ (L'.DDatatype dts, loc) :: ds,
cmap,
conmap,
st,
trans)
- end*)
+ end
| L.SgiVal (x, _, c) =>
let
diff --git a/src/marshalcheck.sml b/src/marshalcheck.sml
index 3dbf93fc..10129aef 100644
--- a/src/marshalcheck.sml
+++ b/src/marshalcheck.sml
@@ -75,12 +75,13 @@ fun check file =
ignore (foldl (fn ((d, _), (cmap, emap)) =>
case d of
DCon (_, n, _, c) => (IM.insert (cmap, n, sins cmap c), emap)
- | DDatatype (_, n, _, xncs) =>
- (IM.insert (cmap, n, foldl (fn ((_, _, co), s) =>
- case co of
- NONE => s
- | SOME c => PS.union (s, sins cmap c))
- PS.empty xncs),
+ | DDatatype dts =>
+ (foldl (fn ((_, n, _, xncs), cmap) =>
+ IM.insert (cmap, n, foldl (fn ((_, _, co), s) =>
+ case co of
+ NONE => s
+ | SOME c => PS.union (s, sins cmap c))
+ PS.empty xncs)) cmap dts,
emap)
| DVal (_, n, t, _, tag) => (cmap, IM.insert (emap, n, (t, tag)))
diff --git a/src/monoize.sml b/src/monoize.sml
index bf250984..e4175015 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -3045,7 +3045,8 @@ fun monoDecl (env, fm) (all as (d, loc)) =
in
case d of
L.DCon _ => NONE
- | L.DDatatype (x, n, [], xncs) =>
+ | 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)
@@ -3064,7 +3065,7 @@ fun monoDecl (env, fm) (all as (d, loc)) =
NONE
else
poly ()
- | L.DDatatype _ => poly ()
+ | L.DDatatype _ => poly ()*)
| L.DVal (x, n, t, e, s) =>
let
val (e, fm) = monoExp (env, St.empty, fm) e
diff --git a/src/reduce.sml b/src/reduce.sml
index 665c10b4..9460d3fe 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -442,13 +442,14 @@ fun reduce file =
((DCon (x, n, k, c), loc),
(IM.insert (namedC, n, c), namedE))
end
- | DDatatype (x, n, ps, cs) =>
- let
- val env = map (fn _ => UnknownC) ps
- in
- ((DDatatype (x, n, ps, map (fn (x, n, co) => (x, n, Option.map (con namedC env) co)) cs), loc),
- st)
- end
+ | DDatatype dts =>
+ ((DDatatype (map (fn (x, n, ps, cs) =>
+ let
+ val env = map (fn _ => UnknownC) ps
+ in
+ (x, n, ps, map (fn (x, n, co) => (x, n, Option.map (con namedC env) co)) cs)
+ end) dts), loc),
+ st)
| DVal (x, n, t, e, s) =>
let
val t = con namedC [] t
diff --git a/src/shake.sml b/src/shake.sml
index 35af7436..4a40d336 100644
--- a/src/shake.sml
+++ b/src/shake.sml
@@ -69,8 +69,9 @@ fun shake file =
| (_, acc) => acc) (IS.empty, IS.empty, []) file
val (cdef, edef) = foldl (fn ((DCon (_, n, _, c), _), (cdef, edef)) => (IM.insert (cdef, n, [c]), edef)
- | ((DDatatype (_, n, _, xncs), _), (cdef, edef)) =>
- (IM.insert (cdef, n, List.mapPartial #3 xncs), edef)
+ | ((DDatatype dts, _), (cdef, edef)) =>
+ (foldl (fn ((_, n, _, xncs), cdef) =>
+ IM.insert (cdef, n, List.mapPartial #3 xncs)) cdef dts, edef)
| ((DVal (_, n, t, e, _), _), (cdef, edef)) => (cdef, IM.insert (edef, n, ([], t, e)))
| ((DValRec vis, _), (cdef, edef)) =>
let
@@ -157,7 +158,7 @@ fun shake file =
val s = foldl (fn (c, s) => shakeCon s c) s table_cs
in
List.filter (fn (DCon (_, n, _, _), _) => IS.member (#con s, n)
- | (DDatatype (_, n, _, _), _) => IS.member (#con s, n)
+ | (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/specialize.sml b/src/specialize.sml
index 03c9004a..b0e0aeae 100644
--- a/src/specialize.sml
+++ b/src/specialize.sml
@@ -115,10 +115,10 @@ fun considerSpecialization (st : state, n, args, dt : datatyp) =
((x, n, SOME t), st)
end) st cons
- val d = (DDatatype (#name dt ^ "_s",
- n',
- [],
- cons), #2 (List.hd args))
+ val d = (DDatatype [(#name dt ^ "_s",
+ n',
+ [],
+ cons)], #2 (List.hd args))
in
(n', cmap, {count = #count st,
datatypes = #datatypes st,
@@ -248,7 +248,7 @@ fun specialize file =
val (d, st) = specDecl st d
in
case #1 d of
- DDatatype (x, n, xs, xnts) =>
+ DDatatype [(x, n, xs, xnts)] =>
(rev (d :: #decls st),
{count = #count st,
datatypes = IM.insert (#datatypes st, n,
diff --git a/tests/mutual.ur b/tests/mutual.ur
index da8eade4..c3d80c89 100644
--- a/tests/mutual.ur
+++ b/tests/mutual.ur
@@ -1,2 +1,10 @@
datatype foo = A | B of bar
and bar = C | D of foo
+
+val q = B (D A)
+
+fun main () = return <xml>
+ {case q of
+ B (D A) => <xml>Good</xml>
+ | _ => <xml>Bad</xml>}
+</xml>
diff --git a/tests/mutual.urs b/tests/mutual.urs
new file mode 100644
index 00000000..6ac44e0b
--- /dev/null
+++ b/tests/mutual.urs
@@ -0,0 +1 @@
+val main : unit -> transaction page
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 09:33:06 +0000