Merge pull request #10 from uvm-plaid/vr/partition

add elim𝔹/partition/partition𝔹

src/UVMHS/Core/Data/Iter.hs

@@ -4,6 +4,7 @@ import UVMHS.Core.Init
 import UVMHS.Core.Classes
 
 import UVMHS.Core.Data.Arithmetic ()
+import UVMHS.Core.Data.Choice
 import UVMHS.Core.Data.List ()
 import UVMHS.Core.Data.String
 import UVMHS.Core.Data.Pair
@@ -464,6 +465,13 @@ dropWhile p xs₀ =
           | otherwise → iter $ 𝑆 $ \ () → Some $ x :* xs'
   in loop $ un𝑆 (stream xs₀) ()
 
+partition ∷ (a → b ∨ c) → 𝐿 a → 𝐿 b ∧ 𝐿 c
+partition decide = foldrFromWith (Nil :* Nil) $
+  elimChoice (mapFst ∘ (:&)) (mapSnd ∘ (:&)) ∘ decide
+
+partition𝔹 ∷ (a → 𝔹) → 𝐿 a → 𝐿 a ∧ 𝐿 a
+partition𝔹 decide = partition (\ a → elim𝔹 (Inl a) (Inr a) (decide a))
+
 ---------
 -- All --
 ---------

src/UVMHS/Core/Init.hs

@@ -107,6 +107,10 @@ b₁ ⩓ ~b₂ = if b₁ then b₂ else False
 cond ∷ 𝔹 → a → a → a
 cond b ~x ~y = case b of { True → x ; False → y }
 
+-- sometimes convenient to have the arguments in this order
+elim𝔹 ∷ a → a → 𝔹 → a
+elim𝔹 ~x ~y b = cond b x y
+
 ---------------------------
 -- Char and String Types --
 ---------------------------