summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2012-04-21 15:09:02 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2012-04-21 15:09:02 -0400
commitab2b3d31f0236cf5dec6c5fccd4de6b97ca37851 (patch)
tree284e45d1278dd22ad46b658933da8e24019a8ffc /src
parent00786579bad72b41600a54441dbfc09625ada1ea (diff)
Pretty-print tuple types using tuple syntax
Diffstat (limited to 'src')
-rw-r--r--src/elab_print.sml36
1 files changed, 28 insertions, 8 deletions
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 46ad9285..69607056 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -112,14 +112,34 @@ fun p_con' par env (c, _) =
string "=>",
space,
p_con env c3])
- | TRecord (CRecord (_, xcs), _) => box [string "{",
- p_list (fn (x, c) =>
- box [p_name env x,
- space,
- string ":",
- space,
- p_con env c]) xcs,
- string "}"]
+ | TRecord (CRecord (_, xcs), _) =>
+ let
+ fun isTuple (n, xcs) =
+ case xcs of
+ [] => n > 2
+ | ((CName s, _), _) :: xcs' =>
+ s = Int.toString n andalso isTuple (n+1, xcs')
+ | _ => false
+ in
+ if isTuple (1, xcs) then
+ case xcs of
+ (_, c) :: xcs =>
+ parenIf par (box [p_con' true env c,
+ p_list_sep (box []) (fn (_, c) => box [space,
+ string "*",
+ space,
+ p_con' true env c]) xcs])
+ | _ => raise Fail "ElabPrint: surprise empty tuple"
+ else
+ box [string "{",
+ p_list (fn (x, c) =>
+ box [p_name env x,
+ space,
+ string ":",
+ space,
+ p_con env c]) xcs,
+ string "}"]
+ end
| TRecord c => box [string "$",
p_con' true env c]