From 6cb3888614811abc30c6a00a1644e256d1d1c780 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 16 May 2009 15:22:05 -0400 Subject: Mutual datatypes through Corify --- src/expl_print.sml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) (limited to 'src/expl_print.sml') diff --git a/src/expl_print.sml b/src/expl_print.sml index 7aa36c6d..0783facc 100644 --- a/src/expl_print.sml +++ b/src/expl_print.sml @@ -460,9 +460,7 @@ fun p_datatype env (x, n, xs, cons) = 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 @@ fun p_datatype env (x, n, xs, cons) = 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 @@ 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) @@ -609,7 +609,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) -- cgit v1.2.3