Cleanup and speedup SetAlgebra property tests. Use Data.Relations for…

… testing

eras/babbage/impl/cardano-ledger-babbage.cabal

@@ -57,7 +57,6 @@ library
     cardano-ledger-shelley,
     cardano-ledger-shelley-ma,
     cardano-slotting,
-    vector-map,
     containers,
     data-default,
     deepseq,

eras/shelley/test-suite/src/Test/Cardano/Ledger/Shelley/Rules/TestChain.hs

@@ -284,7 +284,7 @@ incrStakeComp SourceSignalTarget {source = chainSt, signal = block} =
           ptrs = ptrsMap . dpsDState $ dp
           ptrs' = ptrsMap . dpsDState $ dp'
 
--- | Various preservation propertiesC
+-- | Various preservation properties
 adaPreservationChain ::
   forall era ledger.
   ( EraGen era,

libs/set-algebra/src/Control/Iterate/BaseTypes.hs

@@ -204,7 +204,8 @@ instance (Show k, Show v) => Show (Single k v) where
 
 -- ================= Basic Set =====================
 
-data Sett k v where Sett :: (Set.Set k) -> Sett k ()
+data Sett k v where
+  Sett :: Set.Set k -> Sett k ()
 
 instance Basic Sett where
   addpair key _unit (Sett m) = Sett (Set.insert key m)

libs/set-algebra/src/Control/Iterate/Exp.hs

@@ -3,7 +3,6 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 

libs/set-algebra/test/Main.hs

@@ -1,15 +1,17 @@
 module Main where
 
+import Test.Control.Iterate.RelationReference (relationTests)
 import Test.Control.Iterate.SetAlgebra (setAlgTest)
-import Test.Tasty
+import Test.Tasty (TestTree, defaultMain, testGroup)
 
 -- ====================================================================================
 
 tests :: TestTree
 tests =
   testGroup
     "set-algebra"
-    [ setAlgTest
+    [ setAlgTest,
+      relationTests
     ]
 
 main :: IO ()

libs/set-algebra/test/Test/Control/Iterate/RelationReference.hs

@@ -1,46 +1,25 @@
-{-# LANGUAGE ConstrainedClassMethods #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 
-module Test.Control.Iterate.RelationReference
-  ( Relation
-      ( (⨃),
-        (∪),
-        dom,
-        range,
-        (◁),
-        (<|),
-        (▷),
-        (|>),
-        singleton,
-        (⋪),
-        (</|),
-        (⋫),
-        (|/>),
-        Domain,
-        Range,
-        haskey,
-        addpair,
-        removekey,
-        -- below are methods not used anywhere
-        size
-      ),
-    (⊆),
-    (∪+),
-    (∈),
-    (∉),
-    (∩),
-  )
-where
+module Test.Control.Iterate.RelationReference (relationTests) where
 
+import qualified Control.Iterate.BaseTypes as SA
+import qualified Control.Iterate.Exp as SA
+import qualified Control.Iterate.SetAlgebra as SA
 import Data.Foldable (toList)
 import Data.Kind (Type)
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
+import Data.Monoid (Sum)
 import Data.Set (Set, intersection, isSubsetOf)
 import qualified Data.Set as Set
+import Test.Control.Iterate.SetAlgebra ()
+import Test.Tasty (TestName, TestTree, testGroup)
+import Test.Tasty.QuickCheck (Arbitrary, testProperty, (===))
 
 ---------------------------------------------------------------------------------
 -- Domain restriction and exclusion
@@ -50,8 +29,6 @@ class Relation m where
   type Domain m :: Type
   type Range m :: Type
 
-  singleton :: Domain m -> Range m -> m
-
   -- | Domain
   dom :: Ord (Domain m) => m -> Set (Domain m)
 
@@ -61,77 +38,57 @@ class Relation m where
   -- | Domain restriction
   --
   -- Unicode: 25c1
-  (◁), (<|) :: (Ord (Domain m)) => Set (Domain m) -> m -> m
-  s <| r = s ◁ r
+  (◁) :: (Ord (Domain m)) => Set (Domain m) -> m -> m
 
   -- | Domain exclusion
   --
   -- Unicode: 22ea
-  (⋪), (</|) :: (Ord (Domain m)) => Set (Domain m) -> m -> m
-  s </| r = s ⋪ r
+  (⋪) :: (Ord (Domain m)) => Set (Domain m) -> m -> m
 
   -- | Range restriction
   --
   -- Unicode: 25b7
-  (▷), (|>) :: Ord (Range m) => m -> Set (Range m) -> m
-  s |> r = s ▷ r
+  (▷) :: Ord (Range m) => m -> Set (Range m) -> m
 
   -- | Range exclusion
   --
   -- Unicode: 22eb
-  (⋫), (|/>) :: Ord (Range m) => m -> Set (Range m) -> m
-  s |/> r = s ⋫ r
+  (⋫) :: Ord (Range m) => m -> Set (Range m) -> m
 
   -- | Union
   (∪) :: (Ord (Domain m), Ord (Range m)) => m -> m -> m
 
   -- | Union Override Right
   (⨃) :: (Ord (Domain m), Ord (Range m)) => m -> m -> m
 
-  -- | Size of the relation
-  size :: Integral n => m -> n
-
   -- | Is this key in the Domain,  Instances should overide this default with
   -- something more efficient
   haskey :: Ord (Domain m) => Domain m -> m -> Bool
-  haskey key m = key `elem` (dom m)
-
-  -- | Insert (key,value) pair into the Relation.  Instances should overide this
-  -- default with something more efficient
-  addpair :: (Ord (Domain m), Ord (Range m)) => Domain m -> Range m -> m -> m
-  addpair key val m = m ∪ (singleton key val)
-
-  -- | Remove a key (and its associted value at that key) from the Relation.
-  -- Instances should overide this default with something more efficient
-  removekey :: Ord (Domain m) => Domain m -> m -> m
-  removekey k m = Set.singleton k ⋪ m
+  haskey key m = key `elem` dom m
 
 -- | Alias for 'elem'.
 --
 -- Unicode: 2208
 (∈) :: (Eq a, Foldable f) => a -> f a -> Bool
-a ∈ f = elem a f
+(∈) = elem
 
 -- | Alias for not 'elem'.
 --
 -- Unicode: 2209
 (∉) :: (Eq a, Foldable f) => a -> f a -> Bool
-a ∉ f = not $ elem a f
-
-infixl 4 ∉
+(∉) = notElem
 
 instance Relation (Map k v) where
   type Domain (Map k v) = k
   type Range (Map k v) = v
 
-  singleton = Map.singleton
-
   dom = Map.keysSet
+
   range = Set.fromList . Map.elems
 
   s ◁ r = Map.restrictKeys r s
 
-  s ⋪ r = Map.withoutKeys r s -- Uses library fuction which is equivalent to: Map.filterWithKey (\k _ -> k `Set.notMember` s) r
+  s ⋪ r = Map.withoutKeys r s
 
   r ▷ s = Map.filter (`Set.member` s) r
 
@@ -142,78 +99,13 @@ instance Relation (Map k v) where
   -- For union override we pass @d1@ as first argument, since 'Map.union' is left biased.
   d0 ⨃ d1 = Map.union d1 d0
 
-  size = fromIntegral . Map.size
-
-  {-# INLINE haskey #-}
-  haskey x m = case Map.lookup x m of Just _ -> True; Nothing -> False
-
-  {-# INLINE addpair #-}
-  addpair = Map.insertWith (\x _y -> x)
-
-  {-# INLINE removekey #-}
-  removekey k m = Map.delete k m
+  haskey = Map.member
 
 -- | Union override plus is (A\B)∪(B\A)∪{k|->v1+v2 | k|->v1 : A /\ k|->v2 : B}
 -- The library function Map.unionWith is more general, it allows any type for
 -- `b` as long as (+) :: b -> b -> b
 (∪+) :: (Ord a, Num b) => Map a b -> Map a b -> Map a b
-a ∪+ b = (Map.unionWith (+) a b)
-
-instance Relation (Set (a, b)) where
-  type Domain (Set (a, b)) = a
-  type Range (Set (a, b)) = b
-
-  singleton a b = Set.singleton (a, b)
-
-  dom = Set.map fst
-
-  range = Set.map snd
-
-  s ◁ r = Set.filter (\(k, _) -> k `Set.member` toSet s) r
-
-  s ⋪ r = Set.filter (\(k, _) -> k `Set.notMember` toSet s) r
-
-  r ▷ s = Set.filter (\(_, v) -> Set.member v s) r
-
-  r ⋫ s = Set.filter (\(_, v) -> Set.notMember v s) r
-
-  (∪) = Set.union
-
-  d0 ⨃ d1 = d1' ∪ ((dom d1') ⋪ d0)
-    where
-      d1' = toSet d1
-
-  size = fromIntegral . Set.size
-
-  addpair key val set = Set.insert (key, val) set
-
--- The [(a,b)] instance is used in `stakeDistr` in the file LedgerState.hs
-instance Relation [(a, b)] where
-  type Domain [(a, b)] = a
-  type Range [(a, b)] = b
-
-  singleton a b = [(a, b)]
-
-  dom = toSet . fmap fst
-
-  range = toSet . fmap snd
-
-  s ◁ r = filter ((`Set.member` toSet s) . fst) r
-
-  s ⋪ r = filter ((`Set.notMember` toSet s) . fst) r
-
-  r ▷ s = filter ((`Set.member` toSet s) . snd) r
-
-  r ⋫ s = filter ((`Set.notMember` toSet s) . snd) r
-
-  (∪) = (++)
-
-  -- In principle a list of pairs allows for duplicated keys.
-  d0 ⨃ d1 = d0 ++ toList d1
-
-  size = fromIntegral . length
-
-  addpair key val list = (key, val) : list
+(∪+) = Map.unionWith (+)
 
 ---------------------------------------------------------------------------------
 -- Aliases
@@ -230,3 +122,45 @@ toSet = Set.fromList . toList
 
 (∩) :: Ord a => Set a -> Set a -> Set a
 (∩) = intersection
+
+propUnary ::
+  forall b a e.
+  (Eq a, Show a, Arbitrary b, Show b, SA.Embed a e) =>
+  TestName ->
+  (b -> SA.Exp e) ->
+  (b -> a) ->
+  TestTree
+propUnary name expr relExpr =
+  testProperty name (\arg -> SA.eval (expr arg) === relExpr arg)
+
+propBinary ::
+  forall b c a e.
+  (Eq a, Show a, Arbitrary b, Show b, Arbitrary c, Show c, SA.Embed a e) =>
+  TestName ->
+  (b -> c -> SA.Exp e) ->
+  (b -> c -> a) ->
+  TestTree
+propBinary name expr relExpr =
+  testProperty name (\arg1 arg2 -> SA.eval (expr arg1 arg2) === relExpr arg1 arg2)
+
+type M = Map Int (Sum Float)
+
+relationTests :: TestTree
+relationTests =
+  testGroup
+    "RelationTests - check conformance with the original implementation"
+    [ propUnary @M "dom" SA.dom dom,
+      propUnary @M "range" SA.rng range,
+      propBinary @_ @M "∈" (\k m -> k SA.∈ range m) (∈),
+      propBinary @_ @M "∉" (\k m -> k SA.∉ range m) (∉),
+      propBinary @_ @M "haskey" (\k m -> k SA.∈ dom m) haskey,
+      propBinary @_ @M "◁" (SA.◁) (◁),
+      propBinary @_ @M "⋪" (SA.⋪) (⋪),
+      propBinary @M "▷" (SA.▷) (▷),
+      propBinary @M "⋫" (SA.⋫) (⋫),
+      propBinary @M "∪" (SA.∪) (∪),
+      propBinary @M "⨃" (SA.⨃) (⨃),
+      propBinary @M "∪+" (SA.∪+) (∪+),
+      propBinary @M @M "⊆" (\m1 m2 -> SA.rng m1 SA.⊆ SA.rng m2) (⊆),
+      propBinary @(Set Int) "∩" (SA.∩) (∩)
+    ]