diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2009-05-16 15:14:17 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2009-05-16 15:14:17 -0400 |
| commit | 0159bec5067ac88f3f222595ac6f5e2f94c1d41f (patch) | |
| tree | 6d35712f3fc54d19a3d1a605a45840ded71a914e /src/elab_print.sml | |
| parent | c28e1690efd89b7629bfdc81d5dee2d3d37952ca (diff) | |
Mutual datatypes through Elaborate
Diffstat (limited to 'src/elab_print.sml')
| -rw-r--r-- | src/elab_print.sml | 14 |
1 files changed, 8 insertions, 6 deletions
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) |