From 1a17abccd6b92023bd6e658e6237e0d55872331d Mon Sep 17 00:00:00 2001
From: fanghr <chfanghr@gmail.com>
Date: Sat, 16 Apr 2022 18:27:30 +0800
Subject: [PATCH] add `pisDJust` util function

the counterpart of `pisJust`, for type `PMaybeData`
---
 agora/Agora/Utils.hs | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/agora/Agora/Utils.hs b/agora/Agora/Utils.hs
index 7c71c36..9241769 100644
--- a/agora/Agora/Utils.hs
+++ b/agora/Agora/Utils.hs
@@ -29,6 +29,7 @@ module Agora.Utils (
   pkeysEqual,
   pnub,
   pisUniq,
+  pisDJust,
 
   -- * Functions which should (probably) not be upstreamed
   anyOutput,
@@ -357,6 +358,17 @@ pisUniq =
             #&& (self # xs)
       )
       (const $ pcon PTrue)
+      
+-- | Yield True if a given PMaybeData is of form PDJust _.
+pisDJust :: Term s (PMaybeData a :--> PBool)
+pisDJust = phoistAcyclic $
+  plam $ \x ->
+    pmatch
+      x
+      ( \case
+          PDJust _ -> pconstant True
+          _ -> pconstant False
+      )
 
 --------------------------------------------------------------------------------
 {- Functions which should (probably) not be upstreamed