prettier printing of coordinates in ritt-wu proof

lucaferranti · Jan 16, 2022 · 127c7d4 · 127c7d4 · lucaferranti · Jan 16, 2022
1 parent c4f6911
commit 127c7d4
Show file tree

Hide file tree

Showing 5 changed files with 31 additions and 21 deletions.
diff --git a/README.md b/README.md
@@ -76,13 +76,14 @@ prove(hp, th)
 Assigned coordinates:
 ---------------------
 A = (0, 0)
-B = (u[1], 0)
-C = (x[1], u[2])
-M₁ = (x[2], x[3])
-M₂ = (x[4], x[5])
-M₃ = (x[6], x[7])
-H = (x[8], x[9])
-O = (x[10], x[11])
+B = (u₁, 0)
+C = (x₁, u₂)
+M₁ = (x₂, x₃)
+M₂ = (x₄, x₅)
+M₃ = (x₆, x₇)
+H = (x₈, x₉)
+O = (x₁₀, x₁₁)
+
 Goal 1: success
 
 Nondegeneracy conditions:
@@ -113,5 +114,5 @@ u₂ ≠ 0
 [ci-img]: https://github.com/lucaferranti/GeometricTheoremProver.jl/workflows/CI/badge.svg
 [ci-url]: https://github.com/lucaferranti/GeometricTheoremProver.jl/actions
 
-[cov-img]: https://codecov.io/gh/lucaferranti/GeometricTheoremProver.jl/branch/master/graph/badge.svg
-[cov-url]: https://codecov.io/gh/lucaferranti/GeometricTheoremProver.jl
+[cov-img]: https://codecov.io/gh/lucaferranti/GeometricTheoremProver.jl/branch/main/graph/badge.svg?token=EzyZPusnKj
+[cov-url]: https://codecov.io/gh/lucaferranti/GeometricTheoremProver.jl
diff --git a/docs/src/index.md b/docs/src/index.md
@@ -1,6 +1,6 @@
 # GeometricTheoremProver
 
-[![license: MIT](https://img.shields.io/badge/license-MIT-yellow.svg)](../../LICENSE)[![CI](https://github.com/lucaferranti/GeometricTheoremProver.jl/workflows/CI/badge.svg)](https://github.com/lucaferranti/GeometricTheoremProver.jl/actions)[![codecov](https://codecov.io/gh/lucaferranti/GeometricTheoremProver.jl/branch/master/graph/badge.svg)](https://codecov.io/gh/lucaferranti/GeometricTheoremProver.jl)
+[![license: MIT](https://img.shields.io/badge/license-MIT-yellow.svg)](../../LICENSE)[![CI](https://github.com/lucaferranti/GeometricTheoremProver.jl/workflows/CI/badge.svg)](https://github.com/lucaferranti/GeometricTheoremProver.jl/actions)[![codecov](https://codecov.io/gh/lucaferranti/GeometricTheoremProver.jl/branch/main/graph/badge.svg?token=EzyZPusnKj)](https://codecov.io/gh/lucaferranti/GeometricTheoremProver.jl)
 
 ## Overview
 
@@ -76,13 +76,14 @@ prove(hp, th)
 Assigned coordinates:
 ---------------------
 A = (0, 0)
-B = (u[1], 0)
-C = (x[1], u[2])
-M₁ = (x[2], x[3])
-M₂ = (x[4], x[5])
-M₃ = (x[6], x[7])
-H = (x[8], x[9])
-O = (x[10], x[11])
+B = (u₁, 0)
+C = (x₁, u₂)
+M₁ = (x₂, x₃)
+M₂ = (x₄, x₅)
+M₃ = (x₆, x₇)
+H = (x₈, x₉)
+O = (x₁₀, x₁₁)
+
 Goal 1: success
 
 Nondegeneracy conditions:

diff --git a/src/rittwu/coordinates.jl b/src/rittwu/coordinates.jl
@@ -2,7 +2,13 @@ struct Coordinate{T, S}
     x::T
     y::S
 end
-show(io::IO, c::Coordinate) = print(io, "(", c.x, ", ", c.y, ")")
+function show(io::IO, c::Coordinate)
+    print(io, "(")
+    show(io, c.x)
+    print(io, ", ")
+    show(io, c.y)
+    print(io, ")")
+end
 
 function compute_num_variables(hp::Hypothesis)
     total_free = 0

diff --git a/src/rittwu/prove.jl b/src/rittwu/prove.jl
@@ -15,6 +15,7 @@ function show(io::IO, rwp::RittWuProof)
     for (P, c) in rwp.coords
         println(io, P, " = ", c)
     end
+    println(io)
     for (idx, p) in enumerate(eachcol(rwp.R))
         status = iszero(first(p)) ? "success" : "fail"
         println(io, "Goal $idx: $status")

diff --git a/src/theorem/theorem.jl b/src/theorem/theorem.jl
@@ -148,9 +148,10 @@ julia> prove(hp, th)
 Assigned coordinates:
 ---------------------
 A = (0, 0)
-B = (u[1], 0)
-C = (u[2], u[3])
-D = (x[1], x[2])
+B = (u₁, 0)
+C = (u₂, u₃)
+D = (x₁, x₂)
+
 Goal 1: success
 
 Nondegeneracy conditions: