tweak ResponseFor json stuff

sullyj3 · Aug 3, 2024 · ed1eb70 · ed1eb70
1 parent 0beb5aa
commit ed1eb70
Showing 1 changed file with 12 additions and 4 deletions.
diff --git 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