From ed1eb70808fc525a08f0cfe0bb5db8ca84e58c36 Mon Sep 17 00:00:00 2001
From: James Sully <sullyj3@gmail.com>
Date: Sat, 3 Aug 2024 21:21:24 +1000
Subject: [PATCH] tweak ResponseFor json stuff

---
 src/Sand/Message.lean | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/src/Sand/Message.lean b/src/Sand/Message.lean
index 0da4309..785a0ee 100644
--- a/src/Sand/Message.lean
+++ b/src/Sand/Message.lean
@@ -47,15 +47,23 @@ abbrev ResponseFor : Command → Type
   | .pauseTimer  _ => PauseTimerResponse
   | .resumeTimer _ => ResumeTimerResponse
 
-def toJsonResponse {cmd : Command} (resp : ResponseFor cmd) : Lean.Json := by
-  cases cmd <;> exact toJson resp
+def responseForToJson {cmd : Command} : ToJson (ResponseFor cmd) := by
+  cases cmd <;> exact inferInstance
+
+def responseForFromJson {cmd : Command} : FromJson (ResponseFor cmd) := by
+  cases cmd <;> exact inferInstance
+
+def toJsonResponse {cmd : Command} (resp : ResponseFor cmd) : Lean.Json :=
+  have : ToJson (ResponseFor cmd) := responseForToJson
+  toJson resp
 
 def serializeResponse {cmd : Command} (resp : ResponseFor cmd) : ByteArray :=
   String.toUTF8 <| toString <| toJsonResponse resp
 
 def fromJsonResponse? {cmd : Command}
-  (resp : Json) : Except String (ResponseFor cmd) := by
-  cases cmd <;> exact fromJson? resp
+  (resp : Json) : Except String (ResponseFor cmd) :=
+  have : FromJson (ResponseFor cmd) := responseForFromJson
+  fromJson? resp
 
 
 end Sand