diff src/elab_print.sml @ 1720:30c0ca20bf59

Pretty-print tuple types using tuple syntax
author Adam Chlipala <adam@chlipala.net>
date Sat, 21 Apr 2012 15:09:02 -0400
parents 05ae68e019b6
children 5df85275c0d4
line wrap: on
line diff
--- a/src/elab_print.sml	Sat Apr 21 14:57:00 2012 -0400
+++ b/src/elab_print.sml	Sat Apr 21 15:09:02 2012 -0400
@@ -112,14 +112,34 @@
                                                     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]