[ new ] Eq, Ord, Semigroup, and Monoid for All

CHANGELOG.md

@@ -142,6 +142,14 @@
 
 * Adds extraction functions to `Data.Singleton`.
 
+* Implemented `Eq`, `Ord`, `Semigroup`, and `Monoid` for `Data.List.Quantifiers.All.All`
+  and `Data.Vect.Quantifiers.All.All`.
+
+* Generalized `imapProperty` in `Data.List.Quantifiers.All.All`
+  and `Data.Vect.Quantifiers.All.All`.
+
+* Add `zipPropertyWith` to `Data.Vect.Quantifiers.All.All`.
+
 #### System
 
 * Changes `getNProcessors` to return the number of online processors rather than

libs/base/Data/List/Quantifiers.idr

@@ -82,10 +82,12 @@ namespace All
 
   ||| Modify the property given a pointwise interface function
   public export
-  imapProperty : (0 i : Type -> Type)
-              -> (f : {0 a : Type} -> i a => p a -> q a)
-              -> {0 types : List Type}
-              -> All i types => All p types -> All q types
+  imapProperty : {0 a : Type}
+              -> {0 p,q : a -> Type}
+              -> (0 i : a -> Type)
+              -> (f : {0 x : a} -> i x => p x -> q x)
+              -> {0 as : List a}
+              -> All i as => All p as -> All q as
   imapProperty i f @{[]} [] = []
   imapProperty i f @{ix :: ixs} (x :: xs) = f @{ix} x :: imapProperty i f @{ixs} xs
 
@@ -119,13 +121,40 @@ namespace All
     = f px qx :: zipPropertyWith f pxs qxs
 
   export
-  All Show (map p xs) => Show (All p xs) where
-    show pxs = "[" ++ show' "" pxs ++ "]"
-      where
-        show' : String -> All Show (map p xs') => All p xs' -> String
-        show' acc @{[]} [] = acc
-        show' acc @{[_]} [px] = acc ++ show px
-        show' acc @{_ :: _} (px :: pxs) = show' (acc ++ show px ++ ", ") pxs
+  All (Show . p) xs => Show (All p xs) where
+    show = show . forget . imapProperty (Show . p) show
+
+  export
+  All (Eq . p) xs => Eq (All p xs) where
+    (==)           [] []             = True
+    (==) @{_ :: _} (h1::t1) (h2::t2) = h1 == h2 && t1 == t2
+
+  %hint
+  allEq : All (Ord . p) xs => All (Eq . p) xs
+  allEq @{[]}     = []
+  allEq @{_ :: _} = %search :: allEq
+
+  export
+  All (Ord . p) xs => Ord (All p xs) where
+    compare            [] []            = EQ
+    compare @{_ :: _} (h1::t1) (h2::t2) = case compare h1 h2 of
+      EQ => compare t1 t2
+      o  => o
+
+  export
+  All (Semigroup . p) xs => Semigroup (All p xs) where
+    (<+>)           [] [] = []
+    (<+>) @{_ :: _} (h1::t1) (h2::t2) = (h1 <+> h2) :: (t1 <+> t2)
+
+  %hint
+  allSemigroup : All (Monoid . p) xs => All (Semigroup . p) xs
+  allSemigroup @{[]}     = []
+  allSemigroup @{_ :: _} = %search :: allSemigroup
+
+  export
+  All (Monoid . p) xs => Monoid (All p xs) where
+    neutral @{[]}   = []
+    neutral @{_::_} = neutral :: neutral
 
   ||| A heterogeneous list of arbitrary types
   public export

libs/base/Data/Vect/Quantifiers.idr

@@ -113,11 +113,12 @@ namespace All
   mapProperty f (p::pl) = f p :: mapProperty f pl
 
   public export
-  imapProperty : (0 i : Type -> Type) ->
-                 (f : forall a. i a => p a -> q a) ->
-                 {0 types : Vect n Type} ->
-                 All i types =>
-                 All p types -> All q types
+  imapProperty : {0 a : Type}
+              -> {0 p,q : a -> Type}
+              -> (0 i : a -> Type)
+              -> (f : {0 x : a} -> i x => p x -> q x)
+              -> {0 as : Vect n a}
+              -> All i as => All p as -> All q as
   imapProperty _ _              []      = []
   imapProperty i f @{ix :: ixs} (x::xs) = f @{ix} x :: imapProperty i f @{ixs} xs
 
@@ -127,13 +128,47 @@ namespace All
   forget (x::xs) = x :: forget xs
 
   export
-  {0 xs : Vect n _} -> All Show (map p xs) => Show (All p xs) where
-    show pxs = "[" ++ show' "" pxs ++ "]"
-      where
-        show' : {0 xs' : Vect n' _} -> String -> All Show (map p xs') => All p xs' -> String
-        show' acc @{[]} [] = acc
-        show' acc @{[_]} [px] = acc ++ show px
-        show' acc @{_ :: _} (px :: pxs) = show' (acc ++ show px ++ ", ") pxs
+  zipPropertyWith : (f : {0 x : a} -> p x -> q x -> r x) ->
+                    All p xs -> All q xs -> All r xs
+  zipPropertyWith f [] [] = []
+  zipPropertyWith f (px :: pxs) (qx :: qxs)
+    = f px qx :: zipPropertyWith f pxs qxs
+
+  export
+  All (Show . p) xs => Show (All p xs) where
+    show = show . forget . imapProperty (Show . p) show
+
+  export
+  All (Eq . p) xs => Eq (All p xs) where
+    (==)           [] []             = True
+    (==) @{_ :: _} (h1::t1) (h2::t2) = h1 == h2 && t1 == t2
+
+  %hint
+  allEq : All (Ord . p) xs => All (Eq . p) xs
+  allEq @{[]}     = []
+  allEq @{_ :: _} = %search :: allEq
+
+  export
+  All (Ord . p) xs => Ord (All p xs) where
+    compare            [] []            = EQ
+    compare @{_ :: _} (h1::t1) (h2::t2) = case compare h1 h2 of
+      EQ => compare t1 t2
+      o  => o
+
+  export
+  All (Semigroup . p) xs => Semigroup (All p xs) where
+    (<+>)           [] [] = []
+    (<+>) @{_ :: _} (h1::t1) (h2::t2) = (h1 <+> h2) :: (t1 <+> t2)
+
+  %hint
+  allSemigroup : All (Monoid . p) xs => All (Semigroup . p) xs
+  allSemigroup @{[]}     = []
+  allSemigroup @{_ :: _} = %search :: allSemigroup
+
+  export
+  All (Monoid . p) xs => Monoid (All p xs) where
+    neutral @{[]}   = []
+    neutral @{_::_} = neutral :: neutral
 
   ||| A heterogeneous vector of arbitrary types
   public export