From 286c90caeead63c43c1d791444112d024ec4f511 Mon Sep 17 00:00:00 2001
From: Pol_tta <pol_tta@outlook.jp>
Date: Sat, 22 Apr 2023 02:22:19 +0000
Subject: [PATCH] fix: Fix `Polynomial.repr` (#3442)

I misunderstood the `Repr` instance when I port this file, In Lean 4, `Repr` returns `Format`, not `String`, so my porting of `Polynomial.repr` was unnatural.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Pol_tta <52843868+Komyyy@users.noreply.github.com>
---
 Mathlib/Data/Polynomial/Basic.lean | 37 +++++++++++++++------------
 test/Polynomial.lean               | 41 ++++++++++++++++++++++++++++++
 2 files changed, 62 insertions(+), 16 deletions(-)
 create mode 100644 test/Polynomial.lean

diff --git a/Mathlib/Data/Polynomial/Basic.lean b/Mathlib/Data/Polynomial/Basic.lean
index e062577679d2fc..196aafb25a7d00 100644
--- a/Mathlib/Data/Polynomial/Basic.lean
+++ b/Mathlib/Data/Polynomial/Basic.lean
@@ -1220,22 +1220,27 @@ section repr
 
 variable [Semiring R]
 
-open Classical
-
-protected instance repr [Repr R] : Repr R[X] :=
-  ⟨fun p _ =>
-    if p = 0 then "0"
-    else
-      (p.support.sort (· ≤ ·)).foldr
-        (fun n a =>
-          (a ++ if a = "" then "" else " + ") ++
-            if n = 0 then "C (" ++ repr (coeff p n) ++ ")"
-            else
-              if n = 1 then if coeff p n = 1 then "X" else "C (" ++ repr (coeff p n) ++ ") * X"
-              else
-                if coeff p n = 1 then "X ^ " ++ repr n
-                else "C (" ++ repr (coeff p n) ++ ") * X ^ " ++ repr n)
-        ""⟩
+protected instance repr [Repr R] [DecidableEq R] : Repr R[X] :=
+  ⟨fun p prec =>
+    let termPrecAndReprs : List (WithTop ℕ × Lean.Format) :=
+      List.map (fun
+        | 0 => (max_prec, "C " ++ reprArg (coeff p 0))
+        | 1 => if coeff p 1 = 1
+          then (⊤, "X")
+          else (70, "C " ++ reprArg (coeff p 1) ++ " * X")
+        | n =>
+          if coeff p n = 1
+          then (80, "X ^ " ++ Nat.repr n)
+          else (70, "C " ++ reprArg (coeff p n) ++ " * X ^ " ++ Nat.repr n))
+      (p.support.sort (· ≤ ·));
+    match termPrecAndReprs with
+    | [] => "0"
+    | [(tprec, t)] => if prec ≥ tprec then Lean.Format.paren t else t
+    | ts =>
+      -- multiple terms, use `+` precedence
+      (if prec ≥ 65 then Lean.Format.paren else id)
+      (Lean.Format.fill
+        (Lean.Format.joinSep (ts.map Prod.snd) (" +" ++ Lean.Format.line)))⟩
 #align polynomial.has_repr Polynomial.repr
 
 end repr
diff --git a/test/Polynomial.lean b/test/Polynomial.lean
new file mode 100644
index 00000000000000..ee7f537ecd2aa2
--- /dev/null
+++ b/test/Polynomial.lean
@@ -0,0 +1,41 @@
+import Mathlib.Data.Polynomial.Basic
+
+open Polynomial
+
+def p0 : ℕ[X] :=
+  ⟨⟨{}, Pi.single 0 0, by intro; simp [Pi.single, Function.update_apply]⟩⟩
+example : reprStr p0 = "0" := by native_decide
+example : reprStr (Option.some p0) = "some 0" := by native_decide
+example : (reprPrec p0 65).pretty = "0" := by native_decide
+
+def pX : ℕ[X] :=
+  ⟨⟨{1}, Pi.single 1 1, by intro; simp [Pi.single, Function.update_apply]⟩⟩
+example : reprStr pX = "X" := by native_decide
+example : reprStr (Option.some pX) = "some X" := by native_decide
+
+def pXsq : ℕ[X] :=
+  ⟨⟨{2}, Pi.single 2 1, by intro; simp [Pi.single, Function.update_apply]⟩⟩
+example : reprStr pXsq = "X ^ 2" := by native_decide
+example : reprStr (Option.some pXsq) = "some (X ^ 2)" := by native_decide
+example : (reprPrec pXsq 65).pretty = "X ^ 2" := by native_decide
+example : (reprPrec pXsq 70).pretty = "X ^ 2" := by native_decide
+example : (reprPrec pXsq 80).pretty = "(X ^ 2)" := by native_decide
+
+def p1 : ℕ[X] :=
+  ⟨⟨{1}, Pi.single 1 37, by intro; simp [Pi.single, Function.update_apply]⟩⟩
+example : reprStr p1 = "C 37 * X" := by native_decide
+example : reprStr (Option.some p1) = "some (C 37 * X)" := by native_decide
+example : (reprPrec p1 65).pretty = "C 37 * X" := by native_decide
+example : (reprPrec p1 70).pretty = "(C 37 * X)" := by native_decide
+
+def p2 : ℕ[X] :=
+  ⟨⟨{0, 2}, Pi.single 0 57 + Pi.single 2 22,
+    by intro; simp [Pi.single, Function.update_apply]; tauto⟩⟩
+example : reprStr p2 = "C 57 + C 22 * X ^ 2" := by native_decide
+example : (reprPrec p2 65).pretty = "(C 57 + C 22 * X ^ 2)" := by native_decide
+
+-- test that parens are added inside `C`
+def pu1 : (ULift.{1} ℕ)[X] :=
+  ⟨⟨{1}, Pi.single 1 (ULift.up 37),
+    by intro; simp [Pi.single, Function.update_apply, ←ULift.down_inj]⟩⟩
+example : reprStr pu1 = "C (ULift.up 37) * X" := by native_decide