# HG changeset patch # User Adam Chlipala # Date 1242501725 14400 # Node ID 0e554bfd6d6aa7c8a212ebcd8c6104f5e027d4e7 # Parent e2780d2f4afcb3ffa8d6192f5c269fa59cc43abc Mutual datatypes through Corify diff -r e2780d2f4afc -r 0e554bfd6d6a src/corify.sml --- a/src/corify.sml Sat May 16 15:14:17 2009 -0400 +++ b/src/corify.sml Sat May 16 15:22:05 2009 -0400 @@ -621,7 +621,8 @@ in ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st) end - | L.DDatatype (x, n, xs, xncs) => + | L.DDatatype _ => raise Fail "Corify DDatatype" + (*| L.DDatatype (x, n, xs, xncs) => let val (st, n) = St.bindCon st x n val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => @@ -658,7 +659,7 @@ end) xncs in ((L'.DDatatype (x, n, xs, xncs), loc) :: dcons, st) - end + end*) | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) => let val (st, n) = St.bindCon st x n @@ -795,7 +796,8 @@ trans) end - | L.SgiDatatype (x, n, xs, xnts) => + | L.SgiDatatype _ => raise Fail "Corify SgiDatatype" + (*| L.SgiDatatype (x, n, xs, xnts) => let val k = (L'.KType, loc) val dk = ElabUtil.classifyDatatype xnts @@ -856,7 +858,7 @@ conmap, st, trans) - end + end*) | L.SgiVal (x, _, c) => let @@ -1061,7 +1063,7 @@ fun maxName ds = foldl (fn ((d, _), n) => case d of L.DCon (_, n', _, _) => Int.max (n, n') - | L.DDatatype (_, n', _, _) => Int.max (n, n') + | L.DDatatype dts => foldl (fn ((_, n', _, _), n) => Int.max (n, n')) n dts | L.DDatatypeImp (_, n', _, _, _, _, _) => Int.max (n, n') | L.DVal (_, n', _, _) => Int.max (n, n') | L.DValRec vis => foldl (fn ((_, n', _, _), n) => Int.max (n, n)) n vis diff -r e2780d2f4afc -r 0e554bfd6d6a src/expl.sml --- a/src/expl.sml Sat May 16 15:14:17 2009 -0400 +++ b/src/expl.sml Sat May 16 15:22:05 2009 -0400 @@ -115,7 +115,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 | SgiSgn of string * int * sgn @@ -133,7 +133,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 e2780d2f4afc -r 0e554bfd6d6a src/expl_env.sml --- a/src/expl_env.sml Sat May 16 15:14:17 2009 -0400 +++ b/src/expl_env.sml Sat May 16 15:22:05 2009 -0400 @@ -255,22 +255,33 @@ 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) => + | DDatatype dts => let - val env = pushCNamed env x n (KType, loc) NONE + 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 = pushCNamed env x n kb NONE + 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 (x, k, t), loc)) t xs + in + pushENamed 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 (x, k, t), loc)) t xs - in - pushENamed env x' n' t - end) - env xncs + foldl doOne env dts end | DDatatypeImp (x, n, m, ms, x', xs, xncs) => let @@ -337,22 +348,31 @@ case sgi of SgiConAbs (x, n, k) => pushCNamed env x n k NONE | SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c) - | SgiDatatype (x, n, xs, xncs) => + | SgiDatatype dts => let - val env = pushCNamed env x n (KType, loc) NONE + 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 = pushCNamed 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 (x, k, t), loc)) t xs + in + pushENamed 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 (x, k, t), loc)) t xs - in - pushENamed env x' n' t - end) - env xncs + foldl doOne env dts end | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => let diff -r e2780d2f4afc -r 0e554bfd6d6a src/expl_print.sml --- a/src/expl_print.sml Sat May 16 15:14:17 2009 -0400 +++ b/src/expl_print.sml Sat May 16 15:22:05 2009 -0400 @@ -460,9 +460,7 @@ val env = E.pushCNamed 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 "=", @@ -475,7 +473,7 @@ cons] end -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, @@ -495,7 +493,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) @@ -609,7 +609,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 e2780d2f4afc -r 0e554bfd6d6a src/expl_util.sml --- a/src/expl_util.sml Sat May 16 15:14:17 2009 -0400 +++ b/src/expl_util.sml Sat May 16 15:22:05 2009 -0400 @@ -453,15 +453,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 @@ -496,8 +498,15 @@ bind (ctx, NamedC (x, k)) | SgiCon (x, _, k, _) => bind (ctx, NamedC (x, k)) - | SgiDatatype (x, n, _, xncs) => - bind (ctx, NamedC (x, (KType, loc))) + | SgiDatatype dts => + foldl (fn ((x, _, ks, _), ctx) => + let + val k' = (KType, loc) + val k = foldl (fn (_, k) => (KArrow (k', k), loc)) + k' ks + in + bind (ctx, NamedC (x, k)) + end) ctx dts | SgiDatatypeImp (x, _, _, _, _, _, _) => bind (ctx, NamedC (x, (KType, loc))) | SgiVal _ => ctx diff -r e2780d2f4afc -r 0e554bfd6d6a src/explify.sml --- a/src/explify.sml Sat May 16 15:14:17 2009 -0400 +++ b/src/explify.sml Sat May 16 15:22:05 2009 -0400 @@ -137,10 +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, - map (fn (x, n, co) => - (x, n, Option.map explifyCon co)) xncs), loc)*) - | L.SgiDatatype _ => raise Fail "Explify SgiDatatype" + | L.SgiDatatype dts => SOME (L'.SgiDatatype (map (fn (x, n, xs, xncs) => + (x, n, xs, + map (fn (x, n, co) => + (x, n, Option.map explifyCon co)) xncs)) dts), loc) | 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) @@ -164,10 +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, - map (fn (x, n, co) => - (x, n, Option.map explifyCon co)) xncs), loc)*) - | L.DDatatype _ => raise Fail "Explify DDatatype" + | L.DDatatype dts => SOME (L'.DDatatype (map (fn (x, n, xs, xncs) => + (x, n, xs, + map (fn (x, n, co) => + (x, n, Option.map explifyCon co)) xncs)) dts), loc) | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) => SOME (L'.DDatatypeImp (x, n, m1, ms, s, xs, map (fn (x, n, co) =>