commit b54df0410d20da05e9dc5d064fe16ba62f9beff7
parent 9a8eb672e0e4035f7764ad9c71baaad617dad523
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Wed, 17 Jan 2024 03:41:13 -0800
Pretty printing looking real pretty
Diffstat:
2 files changed, 20 insertions(+), 22 deletions(-)
diff --git a/main.ml b/main.ml
@@ -2,7 +2,6 @@ open Node
module I = Internal
module V = Value
-(*
let buf = Lexing.from_string "\
N := [A: Type, A, A -> A] -> A;\n\
add: [N, N] -> N := fn m, n => fn A, z, s => m A (n A z s) s;\n\
@@ -11,12 +10,14 @@ let buf = Lexing.from_string "\
five := add two three;\n\
five Nat 0 (fn n => n + 1)\n\
"
-*)
+
+(*
let buf = Lexing.from_string "\
f := fn a: Nat, b: Nat, c: Nat, d: Nat, e: Nat, f: Nat, g: Nat, h: Nat =>\
- fn a: Nat, b: Nat, c: Nat, d: Nat, e: Nat, f: Nat, g: Nat, h: Nat => 3; 3\
+ fn a: Nat, b: Nat -> Nat -> Nat -> Nat -> Nat -> Nat -> Nat, c: Nat, d: Nat, e: Nat, f: Nat, g: Nat, h: Nat => 3; 3\
"
+*)
(*
let buf = Lexing.from_string "\
@@ -35,8 +36,8 @@ let buf = Lexing.from_string "\
(*
let buf = Lexing.from_string "\
- T & S := #{@a Nat; @b #()};\n\
- @a 3 : S\n\
+ T & S := #{@a Nat, Nat, Nat, Nat, Nat, Nat, Nat, Nat, Nat, Nat, Nat, Nat; @b #()};\n\
+ @a 0 1 2 3 4 5 6 7 8 9 10 11 : S\n\
"
*)
diff --git a/pretty.ml b/pretty.ml
@@ -15,40 +15,40 @@ and pp_print_term
: int -> F.formatter -> term -> unit
= fun m ppf -> function
| Let (definers, body) ->
- pp_print_with_parens m 0 ppf "@[<v 0>%a;@,@[%a@]@]"
+ pp_print_with_parens m 0 ppf "@[<v>@[%a@];@,%a@]"
(F.pp_print_array ~pp_sep:pp_print_comma pp_print_definer) definers
(pp_print_term 0) body
(* TODO: Match *)
| App (fn, args) ->
- pp_print_with_parens m 5 ppf "%a%a"
+ pp_print_with_parens m 5 ppf "@[<4>%a%a@]"
(pp_print_term 6) fn
pp_print_args args
| Fn {multibinder = {binders; _}; body; codomain} ->
- pp_print_with_parens m 1 ppf "@[<hv>fn@;<1 4>@[<hv 0>%a@]%a:: %a =>@;<1 4>@[<h>%a@]@]"
+ pp_print_with_parens m 1 ppf "@[@[<hv 4>fn@ %a%t::@ %a@;<1 -4>@]=>@;<1 4>%a@]"
pp_print_binders binders
- pp_print_trailing_delim (1, ",")
+ (F.pp_print_custom_break ~fits:(" ", 0, "") ~breaks:(",", -4, ""))
(pp_print_term 2) codomain
(pp_print_term 1) body
| FnType {multibinder = {binders; _}; codomain} ->
- pp_print_with_parens m 3 ppf "[@;<0 4>@[<hv 0>%a@]%a] -> %a"
+ pp_print_with_parens m 3 ppf "@[@[<hv 4>[@,%a%t@]] ->@;<1 4>%a@]"
pp_print_binders binders
- pp_print_trailing_delim (0, ",")
+ (F.pp_print_custom_break ~fits:("", 0, "") ~breaks:(",", -4, ""))
(pp_print_term 3) codomain
| Data {tag; args; datatype; _} ->
- pp_print_with_parens m 5 ppf "@[<4>%a%a: %a@]"
+ pp_print_with_parens m 2 ppf "@[@[<4>%a%a@] ::@;<1 4>%a@]"
Name.Ctor.pp_print tag
pp_print_args args
(pp_print_term 2) (DataType datatype)
| DataType {ctors; names} ->
- pp_print_with_parens m 6 ppf "@[#{@[<hv 4>@,%a@]%a}@]"
+ pp_print_with_parens m 6 ppf "@[@[<hv 4>#{@,%a%t@]}@]"
pp_print_ctors (ctors, names)
- pp_print_trailing_delim (0, ";")
+ (F.pp_print_custom_break ~fits:("", 0, "") ~breaks:(";", -4, ""))
| Nat n ->
pp_print_with_parens m 6 ppf "%a"
@@ -71,8 +71,9 @@ and pp_print_term
and pp_print_definer
: F.formatter -> definer -> unit
= fun ppf {names; rhs; typ} ->
- F.fprintf ppf "@[@[<hv>%a: %a@] :=@;<1 4>@[%a@]@]"
+ F.fprintf ppf "@[@[<hv 4>%a%t%a@;<1 -4>@]:=@;<1 4>%a@]"
pp_print_names names
+ (F.pp_print_custom_break ~fits:(": ", 0, "") ~breaks:(" :", 0, ""))
(pp_print_term 2) typ
(pp_print_term 1) rhs
@@ -92,9 +93,10 @@ and pp_print_binders
and pp_print_binder
: F.formatter -> binder -> unit
= fun ppf {plicity; names; typ} ->
- F.fprintf ppf "@[%a%a: %a@]"
+ F.fprintf ppf "@[%a%a%t%a@]"
pp_print_plicity plicity
pp_print_names names
+ (F.pp_print_custom_break ~fits:(": ", 0, "") ~breaks:(" :", 4, ""))
(pp_print_term 2) typ
and pp_print_ctors
@@ -109,7 +111,7 @@ and pp_print_ctors
match ctors.(tagi).binders with
| [||] -> Name.Ctor.pp_print ppf tag
| binders ->
- F.fprintf ppf "@[<4>%a%a@]"
+ F.fprintf ppf "@[<4>%a@ %a@]"
Name.Ctor.pp_print tag
pp_print_binders binders
) names
@@ -130,11 +132,6 @@ and pp_print_name
: F.formatter -> Name.Var.t node -> unit
= fun ppf {data = name; _} -> Name.Var.pp_print ppf name
-and pp_print_trailing_delim
-: F.formatter -> int * string -> unit
-= fun ppf (n, d) ->
- F.pp_print_custom_break ppf ~fits:("", n, "") ~breaks:(d, 0, "")
-
and pp_print_comma
: F.formatter -> unit -> unit
= fun ppf () -> F.fprintf ppf ",@ "
