From 2333a92f0f54a5b6f737398b7a87df86a708e88a Mon Sep 17 00:00:00 2001
From: Tomas Puverle <puverle+github@gmail.com>
Date: Sun, 22 Sep 2024 20:07:26 -0700
Subject: [PATCH] Implemented To/FromJSON and tests.

---
 src/Lean/Data/Json/FromToJson.lean |  3 ++
 tests/lean/run/json_empty.lean     | 52 ++++++++++++++++++++++++++++++
 2 files changed, 55 insertions(+)
 create mode 100644 tests/lean/run/json_empty.lean

diff --git a/src/Lean/Data/Json/FromToJson.lean b/src/Lean/Data/Json/FromToJson.lean
index 1cfbe06ffa09..1dcf5f6288cd 100644
--- a/src/Lean/Data/Json/FromToJson.lean
+++ b/src/Lean/Data/Json/FromToJson.lean
@@ -28,6 +28,9 @@ instance : ToJson Json := ⟨id⟩
 instance : FromJson JsonNumber := ⟨Json.getNum?⟩
 instance : ToJson JsonNumber := ⟨Json.num⟩
 
+instance : FromJson Empty where
+  fromJson? j := throw s!"no constructor matched JSON value '{j}'"
+instance : ToJson Empty := ⟨nofun⟩
 -- looks like id, but there are coercions happening
 instance : FromJson Bool := ⟨Json.getBool?⟩
 instance : ToJson Bool := ⟨fun b => b⟩
diff --git a/tests/lean/run/json_empty.lean b/tests/lean/run/json_empty.lean
new file mode 100644
index 000000000000..057075f239ee
--- /dev/null
+++ b/tests/lean/run/json_empty.lean
@@ -0,0 +1,52 @@
+import Lean
+
+/-!
+# Validation of `Json Empty` instance
+
+This test serves a similar purpose to the `Repr Empty` test in `repr_empty.lean`.
+-/
+
+structure Foo (α : Type) where
+  y : Option α
+deriving Lean.ToJson, Lean.FromJson, Repr
+
+def fromStrHelper (res : Type) [Lean.FromJson res] (s : String) : Except String res :=
+  (Lean.Json.parse s) >>= Lean.fromJson?
+
+/-! First, two basic examples with α not-Empty -/
+/-- info: {"y": 1} -/
+#guard_msgs in
+#eval Lean.toJson (⟨some 1⟩ : Foo Nat)
+
+/-! Ensure we can parse the type back -/
+/-- info: Except.ok { y := some 1 } -/
+#guard_msgs in
+#eval fromStrHelper (Foo Nat) "{\"y\": 1}"
+
+/-- info: {"y": null} -/
+#guard_msgs in
+#eval Lean.toJson (⟨none⟩ : Foo Nat)
+
+/-- info: Except.ok { y := none } -/
+#guard_msgs in
+#eval fromStrHelper (Foo Nat) "{\"y\": null}"
+
+/-! Examples with the `Empty` type -/
+/-- info: {"y": null} -/
+#guard_msgs in
+#eval Lean.toJson (⟨none⟩ : Foo Empty)
+
+/-! Show that we can round-trip from string  -/
+/-- info: Except.ok { y := none } -/
+#guard_msgs in
+#eval fromStrHelper (Foo Empty) "{\"y\": null}"
+
+/-! Show that parsing fails -/
+/-- info: Except.error "no constructor matched JSON value '\"Yo!\"'" -/
+#guard_msgs in
+#eval fromStrHelper (Empty) "\"Yo!\""
+
+/-! Show that parsing fails if we supply anything else but `null` -/
+/-- info: Except.error "Foo.y: no constructor matched JSON value '1'" -/
+#guard_msgs in
+#eval fromStrHelper (Foo Empty) "{\"y\": 1}"