From 7aac084c46818921ae8bfc69c890ce8c81bea0d7 Mon Sep 17 00:00:00 2001
From: Yishuai Li <liyishuai.lys@alibaba-inc.com>
Date: Fri, 20 Sep 2024 19:01:22 +0800
Subject: [PATCH] Monad instances

---
 Decode.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/Decode.v b/Decode.v
index b777d68..1a3e265 100644
--- a/Decode.v
+++ b/Decode.v
@@ -80,3 +80,18 @@ Definition dpath' {T} (d : JDecode T) (s : string) (j : json) : string + T :=
   (decode__jpath (this@s) j <|> inr JSON__Null) >>= d.
 
 Definition dpath {T} `{JDecode T} : string -> JDecode T := dpath' decode.
+
+#[global]
+Instance Monad__JDecode: Monad JDecode :=
+  { ret  _         := const ∘ inr;
+    bind _ _ f k j := f j >>= flip k j
+  }.
+
+#[global]
+Instance MonadExc__JDecode: MonadExc string JDecode :=
+  { raise _       := const ∘ inl;
+    catch _ m f j := match m j with
+                     | inl e       => f e j
+                     | inr _ as mj => mj
+                     end
+  }.