08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
53 lines
1.6 KiB
Text
53 lines
1.6 KiB
Text
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
|
||
|
||
/-! 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 Lean.fromJson? (α := Foo Nat) <| json% {"y": 1}
|
||
|
||
/-- info: {"y": null} -/
|
||
#guard_msgs in
|
||
#eval Lean.toJson (⟨none⟩ : Foo Nat)
|
||
|
||
/-- info: Except.ok { y := none } -/
|
||
#guard_msgs in
|
||
#eval Lean.fromJson? (α := Foo Nat) <| json% {"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 Lean.fromJson? (α := Foo Empty) <| json% {"y": null}
|
||
|
||
/-! Show that parsing fails -/
|
||
/-- info: Except.error "type Empty has no constructor to match JSON value '\"Yo!\"'.
|
||
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'.
|
||
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}
|