# HG changeset patch # User Adam Chlipala # Date 1242501257 14400 # Node ID e2780d2f4afcb3ffa8d6192f5c269fa59cc43abc # Parent 10fe57e4a8c2afe86dff5809b3600367c79c10b4 Mutual datatypes through Elaborate diff -r 10fe57e4a8c2 -r e2780d2f4afc src/elab.sml --- a/src/elab.sml Sat May 16 13:10:52 2009 -0400 +++ b/src/elab.sml Sat May 16 15:14:17 2009 -0400 @@ -132,7 +132,7 @@ 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 @@ 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 -r 10fe57e4a8c2 -r e2780d2f4afc src/elab_env.sml --- a/src/elab_env.sml Sat May 16 13:10:52 2009 -0400 +++ b/src/elab_env.sml Sat May 16 15:14:17 2009 -0400 @@ -909,7 +909,7 @@ 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 @@ 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 @@ 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 + 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 + end 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 + foldl doOne env dts end | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => let @@ -1288,16 +1293,16 @@ 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 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 @@ 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 @@ 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 @@ 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 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 -r 10fe57e4a8c2 -r e2780d2f4afc src/elab_print.sml --- a/src/elab_print.sml Sat May 16 13:10:52 2009 -0400 +++ b/src/elab_print.sml Sat May 16 15:14:17 2009 -0400 @@ -486,9 +486,7 @@ 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 @@ 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 @@ 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 @@ 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 -r 10fe57e4a8c2 -r e2780d2f4afc src/elab_util.sml --- a/src/elab_util.sml Sat May 16 13:10:52 2009 -0400 +++ b/src/elab_util.sml Sat May 16 15:14:17 2009 -0400 @@ -568,15 +568,17 @@ 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 @@ 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 @@ (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 @@ 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 @@ 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 @@ 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 -r 10fe57e4a8c2 -r e2780d2f4afc src/elaborate.sml --- a/src/elaborate.sml Sat May 16 13:10:52 2009 -0400 +++ b/src/elaborate.sml Sat May 16 15:14:17 2009 -0400 @@ -1971,47 +1971,65 @@ ([(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 @@ 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 @@ | 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ | _ => 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 - - 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 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) + | 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) + + val k = (L'.KType, loc) + val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1 + + 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 - | L'.SgiDatatypeImp (x', n1, _, _, _, xs, xncs1) => - if x' = x then - found (n1, xs, xncs1) - 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 @@ ([(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) + + 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, 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 - (*if positive then - () - else - declError env (Nonpositive d');*) - - ([d'], (env, denv, gs' @ gs)) + ([(L'.DDatatype dts, loc)], (env, denv, gs' @ gs)) end | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp" @@ -3484,24 +3558,31 @@ 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 -r 10fe57e4a8c2 -r e2780d2f4afc src/explify.sml --- a/src/explify.sml Sat May 16 13:10:52 2009 -0400 +++ b/src/explify.sml Sat May 16 15:14:17 2009 -0400 @@ -137,9 +137,10 @@ 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 @@ 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 -r 10fe57e4a8c2 -r e2780d2f4afc src/source.sml --- a/src/source.sml Sat May 16 13:10:52 2009 -0400 +++ b/src/source.sml Sat May 16 15:14:17 2009 -0400 @@ -85,7 +85,7 @@ 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 @@ 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 -r 10fe57e4a8c2 -r e2780d2f4afc src/source_print.sml --- a/src/source_print.sml Sat May 16 13:10:52 2009 -0400 +++ b/src/source_print.sml Sat May 16 15:14:17 2009 -0400 @@ -360,9 +360,7 @@ 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 @@ 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 @@ 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 -r 10fe57e4a8c2 -r e2780d2f4afc src/urweb.grm --- a/src/urweb.grm Sat May 16 13:10:52 2009 -0400 +++ b/src/urweb.grm Sat May 16 15:14:17 2009 -0400 @@ -226,6 +226,8 @@ | 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 @@ 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 @@ | 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 @@ | 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)) diff -r 10fe57e4a8c2 -r e2780d2f4afc tests/mutual.ur --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/mutual.ur Sat May 16 15:14:17 2009 -0400 @@ -0,0 +1,2 @@ +datatype foo = A | B of bar +and bar = C | D of foo diff -r 10fe57e4a8c2 -r e2780d2f4afc tests/mutual.urp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/mutual.urp Sat May 16 15:14:17 2009 -0400 @@ -0,0 +1,3 @@ +debug + +mutual