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