From d9ce1246e730bac15dcd25cccdba4f7bd5002047 Mon Sep 17 00:00:00 2001
From: Olivier <olivier.martinot@inria.fr>
Date: Fri, 16 Sep 2022 15:14:25 +0200
Subject: [PATCH] Improve printing of n-ary abstraction and type abstraction.

---
 client/MLParser.mly       |  6 ++++--
 client/Printer.ml         | 40 +++++++++++++++++++++++++++++----------
 client/test/suite.t/run.t | 25 ++++++++++--------------
 3 files changed, 44 insertions(+), 27 deletions(-)

diff --git a/client/MLParser.mly b/client/MLParser.mly
index 5ad7ceb..91ecc90 100644
--- a/client/MLParser.mly
+++ b/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) }
 
diff --git a/client/Printer.ml b/client/Printer.ml
index dc9449e..deee934 100644
--- a/client/Printer.ml
+++ b/client/Printer.ml
@@ -110,6 +110,30 @@ 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
+  ^^ space
+  ^^ separate_map space print_arg args
+  ^^ space
+  ^^ string "->"
+  ^//^ rhs
+
 let print_annot print_elem (rigidity, tyvars, typ) =
   let rigidity_kwd =
     string @@ match rigidity with
@@ -132,21 +156,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)
   | t ->
       print_term_app t
 
diff --git a/client/test/suite.t/run.t b/client/test/suite.t/run.t
index 12e69dd..c87f0bd 100644
--- a/client/test/suite.t/run.t
+++ b/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,11 +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]
     [{}]
     ()
-- 
GitLab