Add dFilter to json

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,