Improve printing of n-ary abstraction and type abstraction.

client/MLParser.mly

@@ -67,8 +67,10 @@ let term :=
   | ~ = term_abs ; <>
 
 let term_abs :=
-  | FUN ; x = tevar_ ; "->" ; t = term_abs ;
-                                          { Abs ($loc, x, t) }
+  | FUN ; xs = list (tevar_) ; "->" ; t = term_abs ;
+    {
+      List.fold_right (fun x t -> Abs ($loc, x, t)) xs t
+    }
 
   | (x, t1, t2) = letin(tevar) ;          { Let ($loc, x, t1, t2) }
 

client/Printer.ml

@@ -114,6 +114,29 @@ let print_let_in lhs rhs body =
   ^^ string "in"
   ^^ prefix 0 1 empty body
 
+let rec flatten_tyabs t =
+  match t with
+  | TyAbs (x, t) ->
+      let (xs, t) = flatten_tyabs t in
+      (x::xs, t)
+  | t ->
+      ([], t)
+
+let rec flatten_abs t =
+  match t with
+  | Abs (p, t) ->
+      let (ps, t) = flatten_abs t in
+      (p::ps, t)
+  | t ->
+      ([], t)
+
+let print_nary_abstraction abs print_arg args rhs =
+  string abs
+  ^^ List.fold_left (fun acc arg -> acc ^^ space ^^ print_arg arg) empty args
+  ^^ space
+  ^^ string "->"
+  ^//^ rhs
+
 let print_annot print_elem (rigidity, tyvars, typ) =
   let rigidity_kwd =
     string @@ match rigidity with
@@ -136,21 +159,17 @@ let rec print_term t =
 
 and print_term_abs t =
   group @@ match t with
-  | TyAbs (x, t1) ->
-     string "FUN" ^^ space
-     ^^ print_tyvar x ^^ space
-     ^^ string "->"
-     ^//^ print_term_abs t1
+  | TyAbs _ ->
+      let (xs, t) = flatten_tyabs t in
+      print_nary_abstraction "FUN" print_tyvar xs (print_term_abs t)
   | Let (p, t1, t2) ->
       print_let_in
         (print_pattern p)
         (print_term t1)
         (print_term_abs t2)
-  | Abs (p, t) ->
-      string "fun" ^^ space
-      ^^ print_pattern p ^^ space
-      ^^ string "->"
-      ^//^ print_term_abs t
+  | Abs _ ->
+      let (ps, t) = flatten_abs t in
+      print_nary_abstraction "fun" print_pattern ps (print_term_abs t)
   | Use (t, u) ->
       string "use" ^^ space
       ^^ print_term t

client/test/suite.t/run.t

@@ -103,9 +103,8 @@ Option type
   Type inference and translation to System F...
   Formatting the System F term...
   Pretty-printing the System F term...
-  FUN a0 ->
-    FUN a1 ->
-      Some<option {a1 -> a1*a0 -> a0}> (fun (x : a1) -> x, fun (x : a0) -> x)
+  FUN a0 a1 ->
+    Some<option {a1 -> a1*a0 -> a0}> (fun (x : a1) -> x, fun (x : a0) -> x)
   Converting the System F term to de Bruijn style...
   Type-checking the System F term...
 
@@ -223,12 +222,11 @@ Pattern-matching
   Type inference and translation to System F...
   Formatting the System F term...
   Pretty-printing the System F term...
-  FUN a0 ->
-    FUN a1 ->
-      match<option a0> Some<option (a1 -> a1)> (fun (x : a1) -> x) with
-      | None<option (a1 -> a1)> () -> None<option a0> ()
-      | (Some<option (a1 -> a1)> _ : option (a1 -> a1)) -> None<option a0> ()
-      end
+  FUN a0 a1 ->
+    match<option a0> Some<option (a1 -> a1)> (fun (x : a1) -> x) with
+    | None<option (a1 -> a1)> () -> None<option a0> ()
+    | (Some<option (a1 -> a1)> _ : option (a1 -> a1)) -> None<option a0> ()
+    end
   Converting the System F term to de Bruijn style...
   Type-checking the System F term...
 
@@ -311,7 +309,7 @@ It involves a useless universal quantifier.
   Type inference and translation to System F...
   Formatting the System F term...
   Pretty-printing the System F term...
-  (FUN a1 -> FUN a2 -> (fun (x : a2) -> x : a2 -> a2)) [[a0] a0] [{}] ()
+  (FUN a1 a2 -> (fun (x : a2) -> x : a2 -> a2)) [[a0] a0] [{}] ()
   Converting the System F term to de Bruijn style...
   Type-checking the System F term...
 
@@ -330,12 +328,8 @@ and unreachable from the entry point of a type scheme.
   Type inference and translation to System F...
   Formatting the System F term...
   Pretty-printing the System F term...
-  (FUN a1 ->
-    FUN a2 ->
-      (
-        (fun (x : a1 -> a1) -> fun (y : a2) -> y) (fun (x : a1) -> x)
-        : a2 -> a2
-      ))
+  (FUN a1 a2 ->
+    ((fun (x : a1 -> a1) (y : a2) -> y) (fun (x : a1) -> x) : a2 -> a2))
     [[a0] a0]
     [{}]
     ()