summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-05-16 15:14:17 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-05-16 15:14:17 -0400
commit0159bec5067ac88f3f222595ac6f5e2f94c1d41f (patch)
tree6d35712f3fc54d19a3d1a605a45840ded71a914e /src
parentc28e1690efd89b7629bfdc81d5dee2d3d37952ca (diff)
Mutual datatypes through Elaborate
Diffstat (limited to 'src')
-rw-r--r--src/elab.sml4
-rw-r--r--src/elab_env.sml144
-rw-r--r--src/elab_print.sml14
-rw-r--r--src/elab_util.sml111
-rw-r--r--src/elaborate.sml527
-rw-r--r--src/explify.sml10
-rw-r--r--src/source.sml4
-rw-r--r--src/source_print.sml12
-rw-r--r--src/urweb.grm11
9 files changed, 493 insertions, 344 deletions
diff --git a/src/elab.sml b/src/elab.sml
index 555cc25c..de2db500 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -132,7 +132,7 @@ withtype exp = exp' located
datatype sgn_item' =
SgiConAbs of string * int * kind
| SgiCon of string * int * kind * con
- | SgiDatatype of string * int * string list * (string * int * con option) list
+ | SgiDatatype of (string * int * string list * (string * int * con option) list) list
| SgiDatatypeImp of string * int * int * string list * string * string list * (string * int * con option) list
| SgiVal of string * int * con
| SgiStr of string * int * sgn
@@ -154,7 +154,7 @@ and sgn = sgn' located
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
| DDatatypeImp of string * int * int * string list * string * string list * (string * int * con option) list
| DVal of string * int * con * exp
| DValRec of (string * int * con * exp) list
diff --git a/src/elab_env.sml b/src/elab_env.sml
index efc2b74e..88b2554b 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -909,7 +909,7 @@ fun sgiSeek (sgi, (sgns, strs, cons)) =
case sgi of
SgiConAbs (x, n, _) => (sgns, strs, IM.insert (cons, n, x))
| SgiCon (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x))
- | SgiDatatype (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x))
+ | SgiDatatype dts => (sgns, strs, foldl (fn ((x, n, _, _), cons) => IM.insert (cons, n, x)) cons dts)
| SgiDatatypeImp (x, n, _, _, _, _, _) => (sgns, strs, IM.insert (cons, n, x))
| SgiVal _ => (sgns, strs, cons)
| SgiSgn (x, n, _) => (IM.insert (sgns, n, x), strs, cons)
@@ -929,7 +929,7 @@ fun sgnSeek f sgis =
let
val cons =
case sgi of
- SgiDatatype (x, n, _, _) => IM.insert (cons, n, x)
+ SgiDatatype dts => foldl (fn ((x, n, _, _), cons) => IM.insert (cons, n, x)) cons dts
| SgiDatatypeImp (x, n, _, _, _, _, _) => IM.insert (cons, n, x)
| _ => cons
in
@@ -1209,26 +1209,31 @@ fun sgiBinds env (sgi, loc) =
case sgi of
SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE
| SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
- | SgiDatatype (x, n, xs, xncs) =>
+ | SgiDatatype dts =>
let
- val k = (KType, loc)
- val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs
+ fun doOne ((x, n, xs, xncs), env) =
+ let
+ val k = (KType, loc)
+ val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs
- val env = pushCNamedAs env x n k' NONE
- in
- foldl (fn ((x', n', to), env) =>
- let
- val t =
- case to of
- NONE => (CNamed n, loc)
- | SOME t => (TFun (t, (CNamed n, loc)), loc)
+ val env = pushCNamedAs env x n k' NONE
+ in
+ foldl (fn ((x', n', to), env) =>
+ let
+ val t =
+ case to of
+ NONE => (CNamed n, loc)
+ | SOME t => (TFun (t, (CNamed n, loc)), loc)
- val k = (KType, loc)
- val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
- in
- pushENamedAs env x' n' t
- end)
- env xncs
+ val k = (KType, loc)
+ val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
+ in
+ pushENamedAs env x' n' t
+ end)
+ env xncs
+ end
+ in
+ foldl doOne env dts
end
| SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
let
@@ -1288,16 +1293,16 @@ fun projectCon env {sgn, str, field} =
SgnConst sgis =>
(case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE
| SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE
- | SgiDatatype (x, _, xs, _) =>
- if x = field then
- let
- val k = (KType, #2 sgn)
- val k' = foldl (fn (_, k') => (KArrow (k, k'), #2 sgn)) k xs
- in
- SOME (k', NONE)
- end
- else
- NONE
+ | SgiDatatype dts =>
+ (case List.find (fn (x, _, xs, _) => x = field) dts of
+ SOME (_, _, xs, _) =>
+ let
+ val k = (KType, #2 sgn)
+ val k' = foldl (fn (_, k') => (KArrow (k, k'), #2 sgn)) k xs
+ in
+ SOME (k', NONE)
+ end
+ | NONE => NONE)
| SgiDatatypeImp (x, _, m1, ms, x', xs, _) =>
if x = field then
let
@@ -1325,7 +1330,10 @@ fun projectCon env {sgn, str, field} =
fun projectDatatype env {sgn, str, field} =
case #1 (hnormSgn env sgn) of
SgnConst sgis =>
- (case sgnSeek (fn SgiDatatype (x, _, xs, xncs) => if x = field then SOME (xs, xncs) else NONE
+ (case sgnSeek (fn SgiDatatype dts =>
+ (case List.find (fn (x, _, _, _) => x = field) dts of
+ SOME (_, _, xs, xncs) => SOME (xs, xncs)
+ | NONE => NONE)
| SgiDatatypeImp (x, _, _, _, _, xs, xncs) => if x = field then SOME (xs, xncs) else NONE
| _ => NONE) sgis of
NONE => NONE
@@ -1344,7 +1352,18 @@ fun projectConstructor env {sgn, str, field} =
else
SOME (U.classifyDatatype xncs, n', xs, to, (CNamed n, #2 str))) xncs
in
- case sgnSeek (fn SgiDatatype (_, n, xs, xncs) => consider (n, xs, xncs)
+ case sgnSeek (fn SgiDatatype dts =>
+ let
+ fun search dts =
+ case dts of
+ [] => NONE
+ | (_, n, xs, xncs) :: dts =>
+ case consider (n, xs, xncs) of
+ NONE => search dts
+ | v => v
+ in
+ search dts
+ end
| SgiDatatypeImp (_, n, _, _, _, xs, xncs) => consider (n, xs, xncs)
| _ => NONE) sgis of
NONE => NONE
@@ -1382,7 +1401,18 @@ fun projectVal env {sgn, str, field} =
NONE) xncs
in
case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE
- | SgiDatatype (_, n, xs, xncs) => seek (n, xs, xncs)
+ | SgiDatatype dts =>
+ let
+ fun search dts =
+ case dts of
+ [] => NONE
+ | (_, n, xs, xncs) :: dts =>
+ case seek (n, xs, xncs) of
+ NONE => search dts
+ | v => v
+ in
+ search dts
+ end
| SgiDatatypeImp (_, n, _, _, _, xs, xncs) => seek (n, xs, xncs)
| _ => NONE) sgis of
NONE => NONE
@@ -1406,7 +1436,8 @@ fun sgnSeekConstraints (str, sgis) =
end
| SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
| SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
- | SgiDatatype (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
+ | SgiDatatype dts => seek (sgis, sgns, strs,
+ foldl (fn ((x, n, _, _), cons) => IM.insert (cons, n, x)) cons dts, acc)
| SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
| SgiVal _ => seek (sgis, sgns, strs, cons, acc)
| SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc)
@@ -1431,29 +1462,34 @@ fun edeclBinds env (d, loc) =
fun declBinds env (d, loc) =
case d of
DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
- | DDatatype (x, n, xs, xncs) =>
+ | DDatatype dts =>
let
- val k = (KType, loc)
- val nxs = length xs
- val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) =>
- ((CApp (tb, (CRel (nxs - i - 1), loc)), loc),
- (KArrow (k, kb), loc)))
- ((CNamed n, loc), k) xs
-
- val env = pushCNamedAs env x n kb NONE
- val env = pushDatatype env n xs xncs
+ fun doOne ((x, n, xs, xncs), env) =
+ let
+ val k = (KType, loc)
+ val nxs = length xs
+ val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) =>
+ ((CApp (tb, (CRel (nxs - i - 1), loc)), loc),
+ (KArrow (k, kb), loc)))
+ ((CNamed n, loc), k) xs
+
+ val env = pushCNamedAs env x n kb NONE
+ val env = pushDatatype env n xs xncs
+ in
+ foldl (fn ((x', n', to), env) =>
+ let
+ val t =
+ case to of
+ NONE => tb
+ | SOME t => (TFun (t, tb), loc)
+ val t = foldr (fn (x, t) => (TCFun (Implicit, x, k, t), loc)) t xs
+ in
+ pushENamedAs env x' n' t
+ end)
+ env xncs
+ end
in
- foldl (fn ((x', n', to), env) =>
- let
- val t =
- case to of
- NONE => tb
- | SOME t => (TFun (t, tb), loc)
- val t = foldr (fn (x, t) => (TCFun (Implicit, x, k, t), loc)) t xs
- in
- pushENamedAs env x' n' t
- end)
- env xncs
+ foldl doOne env dts
end
| DDatatypeImp (x, n, m, ms, x', xs, xncs) =>
let
diff --git a/src/elab_print.sml b/src/elab_print.sml
index bbbd9f8d..ab38c2e1 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -486,9 +486,7 @@ fun p_datatype env (x, n, xs, cons) =
val env = E.pushCNamedAs env x n k NONE
val env = foldl (fn (x, env) => E.pushCRel env x k) env xs
in
- box [string "datatype",
- space,
- string x,
+ box [string x,
p_list_sep (box []) (fn x => box [space, string x]) xs,
space,
string "=",
@@ -507,7 +505,7 @@ fun p_named x n =
else
string x
-fun p_sgn_item env (sgi, _) =
+fun p_sgn_item env (sgiAll as (sgi, _)) =
case sgi of
SgiConAbs (x, n, k) => box [string "con",
space,
@@ -527,7 +525,9 @@ fun p_sgn_item env (sgi, _) =
string "=",
space,
p_con env c]
- | SgiDatatype x => p_datatype env x
+ | SgiDatatype x => box [string "datatype",
+ space,
+ p_list_sep (box [space, string "and", space]) (p_datatype (E.sgiBinds env sgiAll)) x]
| SgiDatatypeImp (x, _, m1, ms, x', _, _) =>
let
val m1x = #1 (E.lookupStrNamed env m1)
@@ -669,7 +669,9 @@ fun p_decl env (dAll as (d, _) : decl) =
string "=",
space,
p_con env c]
- | 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]
| DDatatypeImp (x, _, m1, ms, x', _, _) =>
let
val m1x = #1 (E.lookupStrNamed env m1)
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 51a203f2..036aa867 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -568,15 +568,17 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
S.map2 (con ctx c,
fn c' =>
(SgiCon (x, n, k', c'), loc)))
- | SgiDatatype (x, n, xs, xncs) =>
- S.map2 (ListUtil.mapfold (fn (x, n, c) =>
- case c of
- NONE => S.return2 (x, n, c)
- | SOME c =>
- S.map2 (con ctx c,
- fn c' => (x, n, SOME c'))) xncs,
- fn xncs' =>
- (SgiDatatype (x, n, xs, xncs'), loc))
+ | SgiDatatype dts =>
+ S.map2 (ListUtil.mapfold (fn (x, n, xs, xncs) =>
+ S.map2 (ListUtil.mapfold (fn (x, n, c) =>
+ case c of
+ NONE => S.return2 (x, n, c)
+ | SOME c =>
+ S.map2 (con ctx c,
+ fn c' => (x, n, SOME c'))) xncs,
+ fn xncs' => (x, n, xs, xncs'))) dts,
+ fn dts' =>
+ (SgiDatatype dts', loc))
| SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
S.map2 (ListUtil.mapfold (fn (x, n, c) =>
case c of
@@ -627,8 +629,15 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
bind (ctx, NamedC (x, n, k, NONE))
| SgiCon (x, n, k, c) =>
bind (ctx, NamedC (x, n, k, SOME c))
- | SgiDatatype (x, n, _, xncs) =>
- bind (ctx, NamedC (x, n, (KType, loc), NONE))
+ | SgiDatatype dts =>
+ foldl (fn ((x, n, ks, _), ctx) =>
+ let
+ val k' = (KType, loc)
+ val k = foldl (fn (_, k) => (KArrow (k', k), loc))
+ k' ks
+ in
+ bind (ctx, NamedC (x, n, k, NONE))
+ end) ctx dts
| SgiDatatypeImp (x, n, m1, ms, s, _, _) =>
bind (ctx, NamedC (x, n, (KType, loc),
SOME (CModProj (m1, ms, s), loc)))
@@ -753,29 +762,34 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
(case #1 d of
DCon (x, n, k, c) =>
bind (ctx, NamedC (x, n, k, SOME c))
- | DDatatype (x, n, xs, xncs) =>
+ | DDatatype dts =>
let
- val ctx = bind (ctx, NamedC (x, n, (KType, loc), NONE))
+ fun doOne ((x, n, xs, xncs), ctx) =
+ let
+ val ctx = bind (ctx, NamedC (x, n, (KType, loc), NONE))
+ in
+ foldl (fn ((x, _, co), ctx) =>
+ let
+ val t =
+ case co of
+ NONE => CNamed n
+ | SOME t => TFun (t, (CNamed n, loc))
+
+ val k = (KType, loc)
+ val t = (t, loc)
+ val t = foldr (fn (x, t) =>
+ (TCFun (Explicit,
+ x,
+ k,
+ t), loc))
+ t xs
+ in
+ bind (ctx, NamedE (x, t))
+ end)
+ ctx xncs
+ end
in
- foldl (fn ((x, _, co), ctx) =>
- let
- val t =
- case co of
- NONE => CNamed n
- | SOME t => TFun (t, (CNamed n, loc))
-
- val k = (KType, loc)
- val t = (t, loc)
- val t = foldr (fn (x, t) =>
- (TCFun (Explicit,
- x,
- k,
- t), loc))
- t xs
- in
- bind (ctx, NamedE (x, t))
- end)
- ctx xncs
+ foldl doOne ctx dts
end
| DDatatypeImp (x, n, m, ms, x', _, _) =>
bind (ctx, NamedC (x, n, (KType, loc),
@@ -851,15 +865,18 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
S.map2 (mfc ctx c,
fn c' =>
(DCon (x, n, k', c'), loc)))
- | DDatatype (x, n, xs, xncs) =>
- 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))
+ | DDatatype dts =>
+ S.map2 (ListUtil.mapfold (fn (x, n, xs, xncs) =>
+ 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'))) dts,
+ fn dts' =>
+ (DDatatype dts', loc))
| DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
S.map2 (ListUtil.mapfold (fn (x, n, c) =>
case c of
@@ -1059,9 +1076,10 @@ fun maxName ds = foldl (fn (d, count) => Int.max (maxNameDecl d, count)) 0 ds
and maxNameDecl (d, _) =
case d of
DCon (_, n, _, _) => n
- | DDatatype (_, n, _, ns) =>
+ | DDatatype dts =>
+ foldl (fn ((_, n, _, ns), max) =>
foldl (fn ((_, n', _), m) => Int.max (n', m))
- n ns
+ (Int.max (n, max)) ns) 0 dts
| DDatatypeImp (_, n1, n2, _, _, _, ns) =>
foldl (fn ((_, n', _), m) => Int.max (n', m))
(Int.max (n1, n2)) ns
@@ -1101,9 +1119,10 @@ and maxNameSgi (sgi, _) =
case sgi of
SgiConAbs (_, n, _) => n
| SgiCon (_, n, _, _) => n
- | SgiDatatype (_, n, _, ns) =>
- foldl (fn ((_, n', _), m) => Int.max (n', m))
- n ns
+ | SgiDatatype dts =>
+ foldl (fn ((_, n, _, ns), max) =>
+ foldl (fn ((_, n', _), m) => Int.max (n', m))
+ (Int.max (n, max)) ns) 0 dts
| SgiDatatypeImp (_, n1, n2, _, _, _, ns) =>
foldl (fn ((_, n', _), m) => Int.max (n', m))
(Int.max (n1, n2)) ns
diff --git a/src/elaborate.sml b/src/elaborate.sml
index f91f83c7..8b23d91e 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1971,47 +1971,65 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
end
- | L.SgiDatatype (x, xs, xcs) =>
+ | L.SgiDatatype dts =>
let
val k = (L'.KType, loc)
- val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
- val (env, n) = E.pushCNamed env x k' NONE
- 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 (env', denv') = foldl (fn (x, (env', denv')) =>
- (E.pushCRel env' x k,
- D.enter denv')) (env, denv) xs
-
- val (xcs, (used, env, gs)) =
- ListUtil.foldlMap
- (fn ((x, to), (used, env, gs)) =>
- let
- val (to, t, gs') = case to of
- NONE => (NONE, t, gs)
- | SOME t' =>
- let
- val (t', tk, gs') = elabCon (env', denv') t'
- in
- checkKind env' t' tk k;
- (SOME t', (L'.TFun (t', t), loc), gs' @ gs)
- end
- val t = foldl (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs
- val (env, n') = E.pushENamed env x t
- in
- if SS.member (used, x) then
- strError env (DuplicateConstructor (x, loc))
- else
- ();
- ((x, n', to), (SS.add (used, x), env, gs'))
- end)
- (SS.empty, env, []) xcs
-
- val env = E.pushDatatype env n xs xcs
+ val (dts, env) = ListUtil.foldlMap (fn ((x, xs, xcs), env) =>
+ let
+ val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
+ val (env, n) = E.pushCNamed env x k' NONE
+ in
+ ((x, n, xs, xcs), env)
+ end)
+ env dts
+
+ val (dts, env) = ListUtil.foldlMap
+ (fn ((x, n, xs, xcs), env) =>
+ let
+ 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 (env', denv') = foldl (fn (x, (env', denv')) =>
+ (E.pushCRel env' x k,
+ D.enter denv')) (env, denv) xs
+
+ val (xcs, (used, env, gs)) =
+ ListUtil.foldlMap
+ (fn ((x, to), (used, env, gs)) =>
+ let
+ val (to, t, gs') = case to of
+ NONE => (NONE, t, gs)
+ | SOME t' =>
+ let
+ val (t', tk, gs') =
+ elabCon (env', denv') t'
+ in
+ checkKind env' t' tk k;
+ (SOME t',
+ (L'.TFun (t', t), loc),
+ gs' @ gs)
+ end
+ val t = foldl (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc))
+ t xs
+
+ val (env, n') = E.pushENamed env x t
+ in
+ if SS.member (used, x) then
+ strError env (DuplicateConstructor (x, loc))
+ else
+ ();
+ ((x, n', to), (SS.add (used, x), env, gs'))
+ end)
+ (SS.empty, env, []) xcs
+ in
+ ((x, n, xs, xcs), E.pushDatatype env n xs xcs)
+ end)
+ env dts
in
- ([(L'.SgiDatatype (x, n, xs, xcs), loc)], (env, denv, gs))
+ ([(L'.SgiDatatype dts, loc)], (env, denv, gs))
end
| L.SgiDatatypeImp (_, [], _) => raise Fail "Empty SgiDatatypeImp"
@@ -2199,21 +2217,31 @@ and elabSgn (env, denv) (sgn, loc) =
else
();
(SS.add (cons, x), vals, sgns, strs))
- | L'.SgiDatatype (x, _, _, xncs) =>
+ | L'.SgiDatatype dts =>
let
- val vals = foldl (fn ((x, _, _), vals) =>
- (if SS.member (vals, x) then
- sgnError env (DuplicateVal (loc, x))
- else
- ();
- SS.add (vals, x)))
- vals xncs
+ val (cons, vals) =
+ let
+ fun doOne ((x, _, _, xncs), (cons, vals)) =
+ let
+ val vals = foldl (fn ((x, _, _), vals) =>
+ (if SS.member (vals, x) then
+ sgnError env (DuplicateVal (loc, x))
+ else
+ ();
+ SS.add (vals, x)))
+ vals xncs
+ in
+ if SS.member (cons, x) then
+ sgnError env (DuplicateCon (loc, x))
+ else
+ ();
+ (SS.add (cons, x), vals)
+ end
+ in
+ foldl doOne (cons, vals) dts
+ end
in
- if SS.member (cons, x) then
- sgnError env (DuplicateCon (loc, x))
- else
- ();
- (SS.add (cons, x), vals, sgns, strs)
+ (cons, vals, sgns, strs)
end
| L'.SgiDatatypeImp (x, _, _, _, _, _, _) =>
(if SS.member (cons, x) then
@@ -2318,15 +2346,15 @@ and selfify env {str, strs, sgn} =
| L'.SgnVar _ => sgn
| L'.SgnConst sgis =>
- (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) =>
- (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
- | (L'.SgiDatatype (x, n, xs, xncs), loc) =>
- (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)
+ (L'.SgnConst (ListUtil.mapConcat (fn (L'.SgiConAbs (x, n, k), loc) =>
+ [(L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)]
+ | (L'.SgiDatatype dts, loc) =>
+ map (fn (x, n, xs, xncs) => (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)) dts
| (L'.SgiClassAbs (x, n, k), loc) =>
- (L'.SgiClass (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
+ [(L'.SgiClass (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)]
| (L'.SgiStr (x, n, sgn), loc) =>
- (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
- | x => x) sgis), #2 sgn)
+ [(L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)]
+ | x => [x]) sgis), #2 sgn)
| L'.SgnFun _ => sgn
| L'.SgnWhere _ => sgn
| L'.SgnProj (m, ms, x) =>
@@ -2360,46 +2388,47 @@ and dopen env {str, strs, sgn} =
in
case #1 (hnormSgn env sgn) of
L'.SgnConst sgis =>
- ListUtil.foldlMap (fn ((sgi, loc), env') =>
- let
- val d =
- case sgi of
- L'.SgiConAbs (x, n, k) =>
- let
- val c = (L'.CModProj (str, strs, x), loc)
- in
- (L'.DCon (x, n, k, c), loc)
- end
- | L'.SgiCon (x, n, k, c) =>
- (L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
- | L'.SgiDatatype (x, n, xs, xncs) =>
- (L'.DDatatypeImp (x, n, str, strs, x, xs, xncs), loc)
- | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
- (L'.DDatatypeImp (x, n, m1, ms, x', xs, xncs), loc)
- | L'.SgiVal (x, n, t) =>
- (L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc)
- | L'.SgiStr (x, n, sgn) =>
- (L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)
- | L'.SgiSgn (x, n, sgn) =>
- (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)
- | L'.SgiConstraint (c1, c2) =>
- (L'.DConstraint (c1, c2), loc)
- | L'.SgiClassAbs (x, n, k) =>
- let
- val c = (L'.CModProj (str, strs, x), loc)
- in
- (L'.DCon (x, n, k, c), loc)
- end
- | L'.SgiClass (x, n, k, _) =>
- let
- val c = (L'.CModProj (str, strs, x), loc)
- in
- (L'.DCon (x, n, k, c), loc)
- end
- in
- (d, E.declBinds env' d)
- end)
- env sgis
+ ListUtil.foldlMapConcat
+ (fn ((sgi, loc), env') =>
+ let
+ val d =
+ case sgi of
+ L'.SgiConAbs (x, n, k) =>
+ let
+ val c = (L'.CModProj (str, strs, x), loc)
+ in
+ [(L'.DCon (x, n, k, c), loc)]
+ end
+ | L'.SgiCon (x, n, k, c) =>
+ [(L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)]
+ | L'.SgiDatatype dts =>
+ map (fn (x, n, xs, xncs) => (L'.DDatatypeImp (x, n, str, strs, x, xs, xncs), loc)) dts
+ | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
+ [(L'.DDatatypeImp (x, n, m1, ms, x', xs, xncs), loc)]
+ | L'.SgiVal (x, n, t) =>
+ [(L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc)]
+ | L'.SgiStr (x, n, sgn) =>
+ [(L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)]
+ | L'.SgiSgn (x, n, sgn) =>
+ [(L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)]
+ | L'.SgiConstraint (c1, c2) =>
+ [(L'.DConstraint (c1, c2), loc)]
+ | L'.SgiClassAbs (x, n, k) =>
+ let
+ val c = (L'.CModProj (str, strs, x), loc)
+ in
+ [(L'.DCon (x, n, k, c), loc)]
+ end
+ | L'.SgiClass (x, n, k, _) =>
+ let
+ val c = (L'.CModProj (str, strs, x), loc)
+ in
+ [(L'.DCon (x, n, k, c), loc)]
+ end
+ in
+ (d, foldl (fn (d, env') => E.declBinds env' d) env' d)
+ end)
+ env sgis
| _ => (strError env (UnOpenable sgn);
([], env))
end
@@ -2445,12 +2474,11 @@ and subSgn env sgn1 (sgn2 as (_, loc2)) =
let
(*val () = prefaces "folder" [("sgis1", p_sgn env (L'.SgnConst sgis1, loc2))]*)
- fun seek p =
+ fun seek' f p =
let
fun seek env ls =
case ls of
- [] => (sgnError env (UnmatchedSgi sgi2All);
- env)
+ [] => f env
| h :: t =>
case p (env, h) of
NONE =>
@@ -2474,6 +2502,9 @@ and subSgn env sgn1 (sgn2 as (_, loc2)) =
in
seek env sgis1
end
+
+ val seek = seek' (fn env => (sgnError env (UnmatchedSgi sgi2All);
+ env))
in
case sgi of
L'.SgiConAbs (x, n2, k2) =>
@@ -2498,12 +2529,23 @@ and subSgn env sgn1 (sgn2 as (_, loc2)) =
case sgi1 of
L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE)
| L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, SOME c1)
- | L'.SgiDatatype (x', n1, xs, _) =>
+ | L'.SgiDatatype dts =>
let
val k = (L'.KType, loc)
- val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
+
+ fun search dts =
+ case dts of
+ [] => NONE
+ | (x', n1, xs, _) :: dts =>
+ let
+ val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
+ in
+ case found (x', n1, k', NONE) of
+ NONE => search dts
+ | x => x
+ end
in
- found (x', n1, k', NONE)
+ search dts
end
| L'.SgiDatatypeImp (x', n1, m1, ms, s, xs, _) =>
let
@@ -2549,66 +2591,93 @@ and subSgn env sgn1 (sgn2 as (_, loc2)) =
| _ => NONE
end)
- | L'.SgiDatatype (x, n2, xs2, xncs2) =>
- seek (fn (env, sgi1All as (sgi1, _)) =>
- let
- fun found (n1, xs1, xncs1) =
- let
- fun mismatched ue =
- (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue));
- SOME env)
-
- val k = (L'.KType, loc)
- val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1
+ | L'.SgiDatatype dts2 =>
+ let
+ fun found' (sgi1All, (x1, n1, xs1, xncs1), (x2, n2, xs2, xncs2), env) =
+ if x1 <> x2 then
+ NONE
+ else
+ let
+ fun mismatched ue =
+ (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue));
+ SOME env)
- fun good () =
- let
- val env = E.sgiBinds env sgi1All
- val env = if n1 = n2 then
- env
- else
- E.pushCNamedAs env x n2 k'
- (SOME (L'.CNamed n1, loc))
- in
- SOME env
- end
+ val k = (L'.KType, loc)
+ val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1
- val env = E.pushCNamedAs env x n1 k' NONE
- val env = if n1 = n2 then
- env
- else
- E.pushCNamedAs env x n2 k' (SOME (L'.CNamed n1, loc))
- val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1
- fun xncBad ((x1, _, t1), (x2, _, t2)) =
- String.compare (x1, x2) <> EQUAL
- orelse case (t1, t2) of
- (NONE, NONE) => false
- | (SOME t1, SOME t2) =>
- (unifyCons env t1 t2; false)
- | _ => true
- in
- (if xs1 <> xs2
- orelse length xncs1 <> length xncs2
- orelse ListPair.exists xncBad (xncs1, xncs2) then
- mismatched NONE
- else
- good ())
- handle CUnify ue => mismatched (SOME ue)
- end
- in
- case sgi1 of
- L'.SgiDatatype (x', n1, xs, xncs1) =>
- if x' = x then
- found (n1, xs, xncs1)
- else
- NONE
- | L'.SgiDatatypeImp (x', n1, _, _, _, xs, xncs1) =>
- if x' = x then
- found (n1, xs, xncs1)
+ fun good () =
+ let
+ val env = E.sgiBinds env sgi1All
+ val env = if n1 = n2 then
+ env
+ else
+ E.pushCNamedAs env x1 n2 k'
+ (SOME (L'.CNamed n1, loc))
+ in
+ SOME env
+ end
+
+ val env = E.pushCNamedAs env x1 n1 k' NONE
+ val env = if n1 = n2 then
+ env
+ else
+ E.pushCNamedAs env x1 n2 k' (SOME (L'.CNamed n1, loc))
+ val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1
+ fun xncBad ((x1, _, t1), (x2, _, t2)) =
+ String.compare (x1, x2) <> EQUAL
+ orelse case (t1, t2) of
+ (NONE, NONE) => false
+ | (SOME t1, SOME t2) =>
+ (unifyCons env t1 t2; false)
+ | _ => true
+ in
+ (if xs1 <> xs2
+ orelse length xncs1 <> length xncs2
+ orelse ListPair.exists xncBad (xncs1, xncs2) then
+ mismatched NONE
else
- NONE
- | _ => NONE
- end)
+ good ())
+ handle CUnify ue => mismatched (SOME ue)
+ end
+ in
+ seek'
+ (fn _ =>
+ let
+ fun seekOne (dt2, env) =
+ seek (fn (env, sgi1All as (sgi1, _)) =>
+ case sgi1 of
+ L'.SgiDatatypeImp (x', n1, _, _, _, xs, xncs1) =>
+ found' (sgi1All, (x', n1, xs, xncs1), dt2, env)
+ | _ => NONE)
+
+ fun seekAll (dts, env) =
+ case dts of
+ [] => env
+ | dt :: dts => seekAll (dts, seekOne (dt, env))
+ in
+ seekAll (dts2, env)
+ end)
+ (fn (env, sgi1All as (sgi1, _)) =>
+ let
+ fun found dts1 =
+ let
+ fun iter (dts1, dts2, env) =
+ case (dts1, dts2) of
+ ([], []) => SOME env
+ | (dt1 :: dts1, dt2 :: dts2) =>
+ (case found' (sgi1All, dt1, dt2, env) of
+ NONE => NONE
+ | SOME env => iter (dts1, dts2, env))
+ | _ => NONE
+ in
+ iter (dts1, dts2, env)
+ end
+ in
+ case sgi1 of
+ L'.SgiDatatype dts1 => found dts1
+ | _ => NONE
+ end)
+ end
| L'.SgiDatatypeImp (x, n2, m12, ms2, s2, xs, _) =>
seek (fn (env, sgi1All as (sgi1, _)) =>
@@ -3033,58 +3102,63 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
([(L'.DCon (x, n, k', c'), loc)], (env', denv, enD gs' @ gs))
end
- | L.DDatatype (x, xs, xcs) =>
+ | L.DDatatype dts =>
let
- val positive = List.all (fn (_, to) =>
- case to of
- NONE => true
- | SOME t => positive x t) xcs
-
val k = (L'.KType, loc)
- val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
- val (env, n) = E.pushCNamed env x k' NONE
- 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 (env', denv') = foldl (fn (x, (env', denv')) =>
- (E.pushCRel env' x k,
- D.enter denv')) (env, denv) xs
-
- val (xcs, (used, env, gs')) =
- ListUtil.foldlMap
- (fn ((x, to), (used, env, gs)) =>
- let
- val (to, t, gs') = case to of
- NONE => (NONE, t, gs)
- | SOME t' =>
- let
- val (t', tk, gs') = elabCon (env', denv') t'
- in
- checkKind env' t' tk k;
- (SOME t', (L'.TFun (t', t), loc), enD gs' @ gs)
- end
- val t = foldr (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs
- val (env, n') = E.pushENamed env x t
- in
- if SS.member (used, x) then
- strError env (DuplicateConstructor (x, loc))
- else
- ();
- ((x, n', to), (SS.add (used, x), env, gs'))
- end)
- (SS.empty, env, []) xcs
-
- val env = E.pushDatatype env n xs xcs
- val d' = (L'.DDatatype (x, n, xs, xcs), loc)
- in
- (*if positive then
- ()
- else
- declError env (Nonpositive d');*)
+ val (dts, env) = ListUtil.foldlMap
+ (fn ((x, xs, xcs), env) =>
+ let
+ val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
+ val (env, n) = E.pushCNamed env x k' NONE
+ in
+ ((x, n, xs, xcs), env)
+ end)
+ env dts
- ([d'], (env, denv, gs' @ gs))
+ val (dts, (env, gs')) = ListUtil.foldlMap
+ (fn ((x, n, xs, xcs), (env, gs')) =>
+ let
+ 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 (env', denv') = foldl (fn (x, (env', denv')) =>
+ (E.pushCRel env' x k,
+ D.enter denv')) (env, denv) xs
+
+ val (xcs, (used, env, gs')) =
+ ListUtil.foldlMap
+ (fn ((x, to), (used, env, gs)) =>
+ let
+ val (to, t, gs') = case to of
+ NONE => (NONE, t, gs)
+ | SOME t' =>
+ let
+ val (t', tk, gs') = elabCon (env', denv') t'
+ in
+ checkKind env' t' tk k;
+ (SOME t', (L'.TFun (t', t), loc), enD gs' @ gs)
+ end
+ val t = foldr (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs
+
+ val (env, n') = E.pushENamed env x t
+ in
+ if SS.member (used, x) then
+ strError env (DuplicateConstructor (x, loc))
+ else
+ ();
+ ((x, n', to), (SS.add (used, x), env, gs'))
+ end)
+ (SS.empty, env, gs') xcs
+ in
+ ((x, n, xs, xcs), (E.pushDatatype env n xs xcs, gs'))
+ end)
+ (env, []) dts
+ in
+ ([(L'.DDatatype dts, loc)], (env, denv, gs' @ gs))
end
| L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp"
@@ -3484,24 +3558,31 @@ and elabStr (env, denv) (str, loc) =
in
((L'.SgiCon (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs)
end
- | L'.SgiDatatype (x, n, xs, xncs) =>
+ | L'.SgiDatatype dts =>
let
- val (cons, x) =
- if SS.member (cons, x) then
- (cons, "?" ^ x)
- else
- (SS.add (cons, x), x)
-
- val (xncs, vals) =
- ListUtil.foldlMap
- (fn ((x, n, t), vals) =>
- if SS.member (vals, x) then
- (("?" ^ x, n, t), vals)
+ fun doOne ((x, n, xs, xncs), (cons, vals)) =
+ let
+ val (cons, x) =
+ if SS.member (cons, x) then
+ (cons, "?" ^ x)
else
- ((x, n, t), SS.add (vals, x)))
- vals xncs
+ (SS.add (cons, x), x)
+
+ val (xncs, vals) =
+ ListUtil.foldlMap
+ (fn ((x, n, t), vals) =>
+ if SS.member (vals, x) then
+ (("?" ^ x, n, t), vals)
+ else
+ ((x, n, t), SS.add (vals, x)))
+ vals xncs
+ in
+ ((x, n, xs, xncs), (cons, vals))
+ end
+
+ val (dts, (cons, vals)) = ListUtil.foldlMap doOne (cons, vals) dts
in
- ((L'.SgiDatatype (x, n, xs, xncs), loc) :: sgis, cons, vals, sgns, strs)
+ ((L'.SgiDatatype dts, loc) :: sgis, cons, vals, sgns, strs)
end
| L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
let
diff --git a/src/explify.sml b/src/explify.sml
index 2e181771..145fccd2 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -137,9 +137,10 @@ fun explifySgi (sgi, loc) =
case sgi of
L.SgiConAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, explifyKind k), loc)
| L.SgiCon (x, n, k, c) => SOME (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc)
- | L.SgiDatatype (x, n, xs, xncs) => SOME (L'.SgiDatatype (x, n, xs,
+ (*| L.SgiDatatype (x, n, xs, xncs) => SOME (L'.SgiDatatype (x, n, xs,
map (fn (x, n, co) =>
- (x, n, Option.map explifyCon co)) xncs), loc)
+ (x, n, Option.map explifyCon co)) xncs), loc)*)
+ | L.SgiDatatype _ => raise Fail "Explify SgiDatatype"
| L.SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
SOME (L'.SgiDatatypeImp (x, n, m1, ms, s, xs, map (fn (x, n, co) =>
(x, n, Option.map explifyCon co)) xncs), loc)
@@ -163,9 +164,10 @@ and explifySgn (sgn, loc) =
fun explifyDecl (d, loc : EM.span) =
case d of
L.DCon (x, n, k, c) => SOME (L'.DCon (x, n, explifyKind k, explifyCon c), loc)
- | L.DDatatype (x, n, xs, xncs) => SOME (L'.DDatatype (x, n, xs,
+ (*| L.DDatatype (x, n, xs, xncs) => SOME (L'.DDatatype (x, n, xs,
map (fn (x, n, co) =>
- (x, n, Option.map explifyCon co)) xncs), loc)
+ (x, n, Option.map explifyCon co)) xncs), loc)*)
+ | L.DDatatype _ => raise Fail "Explify DDatatype"
| L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
SOME (L'.DDatatypeImp (x, n, m1, ms, s, xs,
map (fn (x, n, co) =>
diff --git a/src/source.sml b/src/source.sml
index 9d3eea79..0f62cadd 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -85,7 +85,7 @@ datatype inference =
datatype sgn_item' =
SgiConAbs of string * kind
| SgiCon of string * kind option * con
- | SgiDatatype of string * string list * (string * con option) list
+ | SgiDatatype of (string * string list * (string * con option) list) list
| SgiDatatypeImp of string * string list * string
| SgiVal of string * con
| SgiTable of string * con * exp * exp
@@ -148,7 +148,7 @@ and edecl = edecl' located
datatype decl' =
DCon of string * kind option * con
- | DDatatype of string * string list * (string * con option) list
+ | DDatatype of (string * string list * (string * con option) list) list
| DDatatypeImp of string * string list * string
| DVal of string * con option * exp
| DValRec of (string * con option * exp) list
diff --git a/src/source_print.sml b/src/source_print.sml
index 0f8b093b..b4f9bfd3 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -360,9 +360,7 @@ and p_vali (x, co, e) =
fun p_datatype (x, xs, cons) =
- box [string "datatype",
- space,
- string x,
+ box [string x,
p_list_sep (box []) (fn x => box [space, string x]) xs,
space,
string "=",
@@ -399,7 +397,9 @@ fun p_sgn_item (sgi, _) =
string "=",
space,
p_con c]
- | SgiDatatype x => p_datatype x
+ | SgiDatatype x => box [string "datatype",
+ space,
+ p_list_sep (box [space, string "and", space]) p_datatype x]
| SgiDatatypeImp (x, ms, x') =>
box [string "datatype",
space,
@@ -530,7 +530,9 @@ fun p_decl ((d, _) : decl) =
string "=",
space,
p_con c]
- | DDatatype x => p_datatype x
+ | DDatatype x => box [string "datatype",
+ space,
+ p_list_sep (box [space, string "and", space]) p_datatype x]
| DDatatypeImp (x, ms, x') =>
box [string "datatype",
space,
diff --git a/src/urweb.grm b/src/urweb.grm
index 4697fef7..bd834b47 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -226,6 +226,8 @@ datatype attr = Class of exp | Normal of con * exp
| dargs of string list
| barOpt of unit
| dcons of (string * con option) list
+ | dtype of string * string list * (string * con option) list
+ | dtypes of (string * string list * (string * con option) list) list
| dcon of string * con option
| pkopt of exp
@@ -394,7 +396,7 @@ decl : CON SYMBOL cargl2 kopt EQ cexp (let
end)
| LTYPE SYMBOL EQ cexp ([(DCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp),
s (LTYPEleft, cexpright))])
- | DATATYPE SYMBOL dargs EQ barOpt dcons([(DDatatype (SYMBOL, dargs, dcons), s (DATATYPEleft, dconsright))])
+ | DATATYPE dtypes ([(DDatatype dtypes, s (DATATYPEleft, dtypesright))])
| DATATYPE SYMBOL dargs EQ DATATYPE CSYMBOL DOT path
(case dargs of
[] => [(DDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright))]
@@ -464,6 +466,11 @@ decl : CON SYMBOL cargl2 kopt EQ cexp (let
| COOKIE SYMBOL COLON cexp ([(DCookie (SYMBOL, cexp), s (COOKIEleft, cexpright))])
| STYLE SYMBOL ([(DStyle SYMBOL, s (STYLEleft, SYMBOLright))])
+dtype : SYMBOL dargs EQ barOpt dcons (SYMBOL, dargs, dcons)
+
+dtypes : dtype ([dtype])
+ | dtype AND dtypes (dtype :: dtypes)
+
kopt : (NONE)
| DCOLON kind (SOME kind)
@@ -652,7 +659,7 @@ sgi : CON SYMBOL DCOLON kind ((SgiConAbs (SYMBOL, kind), s (CONleft,
| CON SYMBOL DCOLON kind EQ cexp ((SgiCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright)))
| LTYPE SYMBOL EQ cexp ((SgiCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp),
s (LTYPEleft, cexpright)))
- | DATATYPE SYMBOL dargs EQ barOpt dcons((SgiDatatype (SYMBOL, dargs, dcons), s (DATATYPEleft, dconsright)))
+ | DATATYPE dtypes ((SgiDatatype dtypes, s (DATATYPEleft, dtypesright)))
| DATATYPE SYMBOL dargs EQ DATATYPE CSYMBOL DOT path
(case dargs of
[] => (SgiDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright))