From fbd0900c647b285536dbd829941940dd00ba6f43 Mon Sep 17 00:00:00 2001 From: Tomas Puverle Date: Sun, 22 Sep 2024 00:45:03 -0700 Subject: [PATCH 1/7] Implement Repr for Empty, add tests. --- tests/lean/repr_empty.lean | 22 ++++++++++++++++++++++ tests/lean/repr_empty.lean.expected.out | 2 ++ 2 files changed, 24 insertions(+) create mode 100644 tests/lean/repr_empty.lean create mode 100644 tests/lean/repr_empty.lean.expected.out diff --git a/tests/lean/repr_empty.lean b/tests/lean/repr_empty.lean new file mode 100644 index 000000000000..63c4d60417d2 --- /dev/null +++ b/tests/lean/repr_empty.lean @@ -0,0 +1,22 @@ +/-! +This test validates the Repr instance for `Empty`. + +While it may seem unnecessary to have Repr, it prevents the automatic derivation +of Repr for other types when `Empty` is used as a type parameter. + +This is a simplified version of an example from the "Functional Programming in Lean" book. +The Empty type is used to exlude the `other` constructor from the `Prim` type. +-/ + +inductive Prim (special : Type) where + | plus + | minus + | other : special → Prim special +deriving Repr + +-- Check that both Repr's work +open Prim in +#eval (plus: Prim Int) + +open Prim in +#eval (minus: Prim Empty) diff --git a/tests/lean/repr_empty.lean.expected.out b/tests/lean/repr_empty.lean.expected.out new file mode 100644 index 000000000000..c75592bbeb1b --- /dev/null +++ b/tests/lean/repr_empty.lean.expected.out @@ -0,0 +1,2 @@ +Prim.plus +Prim.minus From ea27545dd1369a3954545a24498bf0f2356c2c92 Mon Sep 17 00:00:00 2001 From: TomasPuverle Date: Sun, 22 Sep 2024 14:54:47 -0700 Subject: [PATCH 2/7] Update tests/lean/repr_empty.lean Co-authored-by: Kyle Miller --- tests/lean/repr_empty.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/repr_empty.lean b/tests/lean/repr_empty.lean index 63c4d60417d2..a86264b1ff2c 100644 --- a/tests/lean/repr_empty.lean +++ b/tests/lean/repr_empty.lean @@ -1,5 +1,5 @@ /-! -This test validates the Repr instance for `Empty`. +# Validation of `Repr Empty` instance While it may seem unnecessary to have Repr, it prevents the automatic derivation of Repr for other types when `Empty` is used as a type parameter. From a1c8e0d02d143160510106402155aed49b74673c Mon Sep 17 00:00:00 2001 From: Tomas Puverle Date: Sun, 22 Sep 2024 15:35:06 -0700 Subject: [PATCH 3/7] Moved and updated code as per PR feedback. --- tests/lean/repr_empty.lean | 22 ---------------------- tests/lean/repr_empty.lean.expected.out | 2 -- 2 files changed, 24 deletions(-) delete mode 100644 tests/lean/repr_empty.lean delete mode 100644 tests/lean/repr_empty.lean.expected.out diff --git a/tests/lean/repr_empty.lean b/tests/lean/repr_empty.lean deleted file mode 100644 index a86264b1ff2c..000000000000 --- a/tests/lean/repr_empty.lean +++ /dev/null @@ -1,22 +0,0 @@ -/-! -# Validation of `Repr Empty` instance - -While it may seem unnecessary to have Repr, it prevents the automatic derivation -of Repr for other types when `Empty` is used as a type parameter. - -This is a simplified version of an example from the "Functional Programming in Lean" book. -The Empty type is used to exlude the `other` constructor from the `Prim` type. --/ - -inductive Prim (special : Type) where - | plus - | minus - | other : special → Prim special -deriving Repr - --- Check that both Repr's work -open Prim in -#eval (plus: Prim Int) - -open Prim in -#eval (minus: Prim Empty) diff --git a/tests/lean/repr_empty.lean.expected.out b/tests/lean/repr_empty.lean.expected.out deleted file mode 100644 index c75592bbeb1b..000000000000 --- a/tests/lean/repr_empty.lean.expected.out +++ /dev/null @@ -1,2 +0,0 @@ -Prim.plus -Prim.minus From 5d364cf6af7a89b946b6ca897ab556cc40275be5 Mon Sep 17 00:00:00 2001 From: Tomas Puverle Date: Sun, 22 Sep 2024 20:07:26 -0700 Subject: [PATCH 4/7] 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}" From 18b8ce0b9a96b9e62f44fba570d9d318dbb55510 Mon Sep 17 00:00:00 2001 From: Tomas Puverle Date: Mon, 23 Sep 2024 13:12:02 -0700 Subject: [PATCH 5/7] Updated test with PR review feedback. --- src/Lean/Data/Json/FromToJson.lean | 5 ++++- tests/lean/run/json_empty.lean | 21 +++++++++++---------- 2 files changed, 15 insertions(+), 11 deletions(-) diff --git a/src/Lean/Data/Json/FromToJson.lean b/src/Lean/Data/Json/FromToJson.lean index 1dcf5f6288cd..398be060fe90 100644 --- a/src/Lean/Data/Json/FromToJson.lean +++ b/src/Lean/Data/Json/FromToJson.lean @@ -29,7 +29,10 @@ instance : FromJson JsonNumber := ⟨Json.getNum?⟩ instance : ToJson JsonNumber := ⟨Json.num⟩ instance : FromJson Empty where - fromJson? j := throw s!"no constructor matched JSON value '{j}'" + fromJson? j := throw (s!"type Empty has no constructor to match JSON value '{j}'. " + ++ "This is likely due to invalid JSON input, such as e.g. constructing an `Option Empty` " + ++ "with a non-null value.") + instance : ToJson Empty := ⟨nofun⟩ -- looks like id, but there are coercions happening instance : FromJson Bool := ⟨Json.getBool?⟩ diff --git a/tests/lean/run/json_empty.lean b/tests/lean/run/json_empty.lean index 057075f239ee..6697f08e1008 100644 --- a/tests/lean/run/json_empty.lean +++ b/tests/lean/run/json_empty.lean @@ -10,9 +10,6 @@ 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 @@ -21,7 +18,7 @@ def fromStrHelper (res : Type) [Lean.FromJson res] (s : String) : Except String /-! Ensure we can parse the type back -/ /-- info: Except.ok { y := some 1 } -/ #guard_msgs in -#eval fromStrHelper (Foo Nat) "{\"y\": 1}" +#eval Lean.fromJson? (α := Foo Nat) <| json% {"y": 1} /-- info: {"y": null} -/ #guard_msgs in @@ -29,7 +26,7 @@ def fromStrHelper (res : Type) [Lean.FromJson res] (s : String) : Except String /-- info: Except.ok { y := none } -/ #guard_msgs in -#eval fromStrHelper (Foo Nat) "{\"y\": null}" +#eval Lean.fromJson? (α := Foo Nat) <| json% {"y": null} /-! Examples with the `Empty` type -/ /-- info: {"y": null} -/ @@ -39,14 +36,18 @@ def fromStrHelper (res : Type) [Lean.FromJson res] (s : String) : Except String /-! Show that we can round-trip from string -/ /-- info: Except.ok { y := none } -/ #guard_msgs in -#eval fromStrHelper (Foo Empty) "{\"y\": null}" +#eval Lean.fromJson? (α := Foo Empty) <| json% {"y": null} /-! Show that parsing fails -/ -/-- info: Except.error "no constructor matched JSON value '\"Yo!\"'" -/ +/-- info: Except.error "type Empty has no constructor to match JSON value '\"Yo!\"'. +This is likely due to invalid JSON input, such as e.g. constructing an `Option Empty` +with a non-null value." -/ #guard_msgs in -#eval fromStrHelper (Empty) "\"Yo!\"" +#eval Lean.fromJson? (α := Empty) <| json% "Yo!" /-! Show that parsing fails if we supply anything else but `null` -/ -/-- info: Except.error "Foo.y: no constructor matched JSON value '1'" -/ +/-- info: Except.error "Foo.y: type Empty has no constructor to match JSON value '1'. +This is likely due to invalid JSON input, such as e.g. constructing an `Option Empty` +with a non-null value." -/ #guard_msgs in -#eval fromStrHelper (Foo Empty) "{\"y\": 1}" +#eval Lean.fromJson? (α := Foo Empty) <| json% {"y": 1} From aa80efdf2771918a75821977b1b858fe3c4d3242 Mon Sep 17 00:00:00 2001 From: Tomas Puverle Date: Mon, 23 Sep 2024 18:08:52 -0700 Subject: [PATCH 6/7] Updated error message. --- src/Lean/Data/Json/FromToJson.lean | 6 +++--- tests/lean/run/json_empty.lean | 8 ++++---- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/Lean/Data/Json/FromToJson.lean b/src/Lean/Data/Json/FromToJson.lean index 398be060fe90..a68fe4f6bd3a 100644 --- a/src/Lean/Data/Json/FromToJson.lean +++ b/src/Lean/Data/Json/FromToJson.lean @@ -29,9 +29,9 @@ instance : FromJson JsonNumber := ⟨Json.getNum?⟩ instance : ToJson JsonNumber := ⟨Json.num⟩ instance : FromJson Empty where - fromJson? j := throw (s!"type Empty has no constructor to match JSON value '{j}'. " - ++ "This is likely due to invalid JSON input, such as e.g. constructing an `Option Empty` " - ++ "with a non-null value.") + fromJson? j := throw (s!"type Empty has no constructor to match JSON value '{j}'. \ + deserializing a value for type Empty, e.g. at type \ + Option Empty with code for the 'some' constructor.") instance : ToJson Empty := ⟨nofun⟩ -- looks like id, but there are coercions happening diff --git a/tests/lean/run/json_empty.lean b/tests/lean/run/json_empty.lean index 6697f08e1008..3130fff60beb 100644 --- a/tests/lean/run/json_empty.lean +++ b/tests/lean/run/json_empty.lean @@ -40,14 +40,14 @@ deriving Lean.ToJson, Lean.FromJson, Repr /-! Show that parsing fails -/ /-- info: Except.error "type Empty has no constructor to match JSON value '\"Yo!\"'. -This is likely due to invalid JSON input, such as e.g. constructing an `Option Empty` -with a non-null value." -/ +deserializing a value for type Empty, e.g. at type Option Empty with code for the 'some' +constructor." -/ #guard_msgs in #eval Lean.fromJson? (α := Empty) <| json% "Yo!" /-! Show that parsing fails if we supply anything else but `null` -/ /-- info: Except.error "Foo.y: type Empty has no constructor to match JSON value '1'. -This is likely due to invalid JSON input, such as e.g. constructing an `Option Empty` -with a non-null value." -/ +deserializing a value for type Empty, e.g. at type Option Empty with code for the 'some' +constructor." -/ #guard_msgs in #eval Lean.fromJson? (α := Foo Empty) <| json% {"y": 1} From bd560184a6340587b171c3ab1bbd94a848c64e82 Mon Sep 17 00:00:00 2001 From: Tomas Puverle Date: Mon, 23 Sep 2024 18:15:56 -0700 Subject: [PATCH 7/7] Once more unto the breach --- src/Lean/Data/Json/FromToJson.lean | 4 ++-- tests/lean/run/json_empty.lean | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Lean/Data/Json/FromToJson.lean b/src/Lean/Data/Json/FromToJson.lean index a68fe4f6bd3a..a6774aff3ddd 100644 --- a/src/Lean/Data/Json/FromToJson.lean +++ b/src/Lean/Data/Json/FromToJson.lean @@ -30,8 +30,8 @@ instance : ToJson JsonNumber := ⟨Json.num⟩ instance : FromJson Empty where fromJson? j := throw (s!"type Empty has no constructor to match JSON value '{j}'. \ - deserializing a value for type Empty, e.g. at type \ - Option Empty with code for the 'some' constructor.") + This occurs when deserializing a value for type Empty, \ + e.g. at type Option Empty with code for the 'some' constructor.") instance : ToJson Empty := ⟨nofun⟩ -- looks like id, but there are coercions happening diff --git a/tests/lean/run/json_empty.lean b/tests/lean/run/json_empty.lean index 3130fff60beb..806234255a21 100644 --- a/tests/lean/run/json_empty.lean +++ b/tests/lean/run/json_empty.lean @@ -40,14 +40,14 @@ deriving Lean.ToJson, Lean.FromJson, Repr /-! Show that parsing fails -/ /-- info: Except.error "type Empty has no constructor to match JSON value '\"Yo!\"'. -deserializing a value for type Empty, e.g. at type Option Empty with code for the 'some' -constructor." -/ +This occurs when deserializing a value for type Empty, e.g. at type Option Empty with code +for the 'some' constructor." -/ #guard_msgs in #eval Lean.fromJson? (α := Empty) <| json% "Yo!" /-! Show that parsing fails if we supply anything else but `null` -/ /-- info: Except.error "Foo.y: type Empty has no constructor to match JSON value '1'. -deserializing a value for type Empty, e.g. at type Option Empty with code for the 'some' -constructor." -/ +This occurs when deserializing a value for type Empty, e.g. at type Option Empty with code +for the 'some' constructor." -/ #guard_msgs in #eval Lean.fromJson? (α := Foo Empty) <| json% {"y": 1}