From d63ba7027e2775bcc9d09981a6cfe93adf22f854 Mon Sep 17 00:00:00 2001
From: Yishuai Li <liyishuai.lys@alibaba-inc.com>
Date: Fri, 20 Sep 2024 21:06:50 +0800
Subject: [PATCH] refactor Decode

---
 Decode.v | 37 ++++++++++++++++++-------------------
 1 file changed, 18 insertions(+), 19 deletions(-)

diff --git a/Decode.v b/Decode.v
index 1a3e265..bd6af43 100644
--- a/Decode.v
+++ b/Decode.v
@@ -18,6 +18,21 @@ Open Scope json_scope.
 
 Class JDecode T := decode : json -> string + T.
 
+#[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
+  }.
+
 #[global]
 Instance JDecode__json : JDecode json := inr.
 
@@ -35,11 +50,11 @@ Instance JDecode__Z : JDecode Z :=
 
 #[global]
 Instance JDecode__N : JDecode N :=
-  fmap Z.to_N ∘ decode.
+  Z.to_N <$> decode.
 
 #[global]
 Instance JDecode__nat : JDecode nat :=
-  fmap Z.to_nat ∘ decode.
+  Z.to_nat <$> decode.
 
 #[global]
 Instance JDecode__bool : JDecode bool :=
@@ -56,8 +71,7 @@ Definition decode__list {T} `{JDecode T} : JDecode (list T) :=
     else inl $ "Not an Array: " ++ to_string j.
 
 Definition decode__option {T} `{JDecode T} : JDecode (option T) :=
-  fun j : json =>
-    catch (Some <$> decode j) (const $ inr None).
+  catch (Some <$> decode) (const $ pure None).
 
 #[global]
 Instance JDecode__unit : JDecode unit :=
@@ -80,18 +94,3 @@ 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
-  }.