From 5760da96eb71876ef1dc4a416fd1a22f67badb6f Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Mon, 27 Jan 2025 22:25:12 -0500
Subject: [PATCH] Add dFilter to json

---
 src/Parser/JSON.md | 46 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)

diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md
index 35f6312..c71d95c 100644
--- a/src/Parser/JSON.md
+++ b/src/Parser/JSON.md
@@ -6,6 +6,8 @@ module Parser.JSON
 import public Parser
 import public Parser.Numbers
 
+import Control.Monad.Eval
+
 import Structures.Dependent.DList
 ```
 
@@ -120,6 +122,50 @@ getProperty prop (VObject xs) =
     Just (type ** (_, val)) => Just (type ** val)
 ```
 
+Recursively apply a filter to a JSON structure.
+
+```idris
+export
+dFilter : (f : (type : JSONType) -> (val : JSONValue type) -> Bool) 
+  -> {t : JSONType} -> JSONValue t -> Maybe (JSONValue t)
+dFilter f value = eval $ dFilter' f value
+  where
+    dFilter' : (f : (type : JSONType) -> (val : JSONValue type) -> Bool) 
+      -> {t : JSONType} -> JSONValue t -> Eval $ Maybe (JSONValue t)
+    dFilter' f (VObject xs) = do
+      True <- pure $ f _ (VObject xs)
+        | _ => pure Nothing
+      let xs = toList xs
+      xs : List (Maybe (x : JSONType ** (String, JSONValue x))) <- 
+        traverse
+          (\(t ** (k, v)) => do
+            Just v <- dFilter' f v
+              | _ => pure Nothing
+            pure $ Just (t ** (k, v)))
+          xs
+      let (_ ** xs) : (t : List JSONType ** DList _ _ t) = 
+        fromList $ catMaybes xs
+      pure . Just $ VObject xs
+    dFilter' f (VArray xs) = do 
+      True <- pure $ f _ (VArray xs)
+        | _ => pure Nothing
+      let xs = toList xs
+      xs : List (Maybe (x : JSONType ** JSONValue x)) <- 
+        traverse
+          (\(t ** v) => do
+            Just v <- dFilter' f v
+              | _ => pure Nothing
+            pure $ Just (t ** v))
+          xs
+      let (_ ** xs) : (t : List JSONType ** DList _ _ t) = 
+        fromList $ catMaybes xs
+      pure . Just $ VArray xs
+    dFilter' f x =
+      pure $ case f _ x of
+        False => Nothing
+        True => Just x
+```
+
 ## Parsers
 
 We are going to get mutually recursive here. Instead of using a `mutual` block,