{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

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
---------------------------------------------------------------------------------

class Relation m where
  type Domain m :: Type
  type Range m :: Type

  -- | Domain
  dom :: Ord (Domain m) => m -> Set (Domain m)

  -- | Range
  range :: Ord (Range m) => m -> Set (Range m)

  -- | Domain restriction
  --
  -- Unicode: 25c1
  (◁) :: Ord (Domain m) => Set (Domain m) -> m -> m

  -- | Domain exclusion
  --
  -- Unicode: 22ea
  (⋪) :: Ord (Domain m) => Set (Domain m) -> m -> m

  -- | Range restriction
  --
  -- Unicode: 25b7
  (▷) :: Ord (Range m) => m -> Set (Range m) -> m

  -- | Range exclusion
  --
  -- Unicode: 22eb
  (⋫) :: 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

  -- | Is this key in the Domain,  Instances should overide this default with
  -- something more efficient
  haskey :: Ord (Domain m) => Domain m -> m -> Bool
  haskey Domain m
key m
m = Domain m
key Domain m -> Set (Domain m) -> Bool
forall a. Eq a => a -> Set a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` m -> Set (Domain m)
forall m. (Relation m, Ord (Domain m)) => m -> Set (Domain m)
dom m
m

-- | Alias for 'elem'.
--
-- Unicode: 2208
(∈) :: (Eq a, Foldable f) => a -> f a -> Bool
∈ :: forall a (f :: * -> *). (Eq a, Foldable f) => a -> f a -> Bool
(∈) = a -> f a -> Bool
forall a. Eq a => a -> f a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem

-- | Alias for not 'elem'.
--
-- Unicode: 2209
(∉) :: (Eq a, Foldable f) => a -> f a -> Bool
∉ :: forall a (f :: * -> *). (Eq a, Foldable f) => a -> f a -> Bool
(∉) = a -> f a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem

instance Relation (Map k v) where
  type Domain (Map k v) = k
  type Range (Map k v) = v

  dom :: Ord (Domain (Map k v)) => Map k v -> Set (Domain (Map k v))
dom = Map k v -> Set k
Map k v -> Set (Domain (Map k v))
forall k a. Map k a -> Set k
Map.keysSet

  range :: Ord (Range (Map k v)) => Map k v -> Set (Range (Map k v))
range = [v] -> Set v
forall a. Ord a => [a] -> Set a
Set.fromList ([v] -> Set v) -> (Map k v -> [v]) -> Map k v -> Set v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map k v -> [v]
forall k a. Map k a -> [a]
Map.elems

  Set (Domain (Map k v))
s ◁ :: Ord (Domain (Map k v)) =>
Set (Domain (Map k v)) -> Map k v -> Map k v
◁ Map k v
r = Map k v -> Set k -> Map k v
forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map k v
r Set k
Set (Domain (Map k v))
s

  Set (Domain (Map k v))
s ⋪ :: Ord (Domain (Map k v)) =>
Set (Domain (Map k v)) -> Map k v -> Map k v
⋪ Map k v
r = Map k v -> Set k -> Map k v
forall k a. Ord k => Map k a -> Set k -> Map k a
Map.withoutKeys Map k v
r Set k
Set (Domain (Map k v))
s

  Map k v
r ▷ :: Ord (Range (Map k v)) =>
Map k v -> Set (Range (Map k v)) -> Map k v
▷ Set (Range (Map k v))
s = (v -> Bool) -> Map k v -> Map k v
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Range (Map k v) -> Set (Range (Map k v)) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (Range (Map k v))
s) Map k v
r

  Map k v
r ⋫ :: Ord (Range (Map k v)) =>
Map k v -> Set (Range (Map k v)) -> Map k v
⋫ Set (Range (Map k v))
s = (v -> Bool) -> Map k v -> Map k v
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Range (Map k v) -> Set (Range (Map k v)) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set (Range (Map k v))
s) Map k v
r

  Map k v
d0 ∪ :: (Ord (Domain (Map k v)), Ord (Range (Map k v))) =>
Map k v -> Map k v -> Map k v
∪ Map k v
d1 = Map k v -> Map k v -> Map k v
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map k v
d0 Map k v
d1

  -- For union override we pass @d1@ as first argument, since 'Map.union' is left biased.
  Map k v
d0 ⨃ :: (Ord (Domain (Map k v)), Ord (Range (Map k v))) =>
Map k v -> Map k v -> Map k v
⨃ Map k v
d1 = Map k v -> Map k v -> Map k v
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map k v
d1 Map k v
d0

  haskey :: Ord (Domain (Map k v)) => Domain (Map k v) -> Map k v -> Bool
haskey = k -> Map k v -> Bool
Domain (Map k v) -> Map k v -> Bool
forall k a. Ord k => k -> Map k a -> Bool
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
∪+ :: forall a b. (Ord a, Num b) => Map a b -> Map a b -> Map a b
(∪+) = (b -> b -> b) -> Map a b -> Map a b -> Map a b
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith b -> b -> b
forall a. Num a => a -> a -> a
(+)

---------------------------------------------------------------------------------
-- Aliases
---------------------------------------------------------------------------------

-- | Inclusion among foldables.
--
-- Unicode: 2286
(⊆) :: (Foldable f, Foldable g, Ord a) => f a -> g a -> Bool
f a
x ⊆ :: forall (f :: * -> *) (g :: * -> *) a.
(Foldable f, Foldable g, Ord a) =>
f a -> g a -> Bool
⊆ g a
y = f a -> Set a
forall (f :: * -> *) a. (Foldable f, Ord a) => f a -> Set a
toSet f a
x Set a -> Set a -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`isSubsetOf` g a -> Set a
forall (f :: * -> *) a. (Foldable f, Ord a) => f a -> Set a
toSet g a
y

toSet :: (Foldable f, Ord a) => f a -> Set a
toSet :: forall (f :: * -> *) a. (Foldable f, Ord a) => f a -> Set a
toSet = [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList ([a] -> Set a) -> (f a -> [a]) -> f a -> Set a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> [a]
forall a. f a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

(∩) :: Ord a => Set a -> Set a -> Set a
∩ :: forall a. Ord a => Set a -> Set a -> Set a
(∩) = Set a -> Set a -> Set a
forall a. 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 :: forall b a e.
(Eq a, Show a, Arbitrary b, Show b, Embed a e) =>
TestName -> (b -> Exp e) -> (b -> a) -> TestTree
propUnary TestName
name b -> Exp e
expr b -> a
relExpr =
  TestName -> (b -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
name (\b
arg -> Exp e -> a
forall s t. Embed s t => Exp t -> s
SA.eval (b -> Exp e
expr b
arg) a -> a -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== b -> a
relExpr b
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 :: forall b c a e.
(Eq a, Show a, Arbitrary b, Show b, Arbitrary c, Show c,
 Embed a e) =>
TestName -> (b -> c -> Exp e) -> (b -> c -> a) -> TestTree
propBinary TestName
name b -> c -> Exp e
expr b -> c -> a
relExpr =
  TestName -> (b -> c -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
name (\b
arg1 c
arg2 -> Exp e -> a
forall s t. Embed s t => Exp t -> s
SA.eval (b -> c -> Exp e
expr b
arg1 c
arg2) a -> a -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== b -> c -> a
relExpr b
arg1 c
arg2)

type M = Map Int (Sum Float)

relationTests :: TestTree
relationTests :: TestTree
relationTests =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"RelationTests - check conformance with the original implementation"
    [ forall b a e.
(Eq a, Show a, Arbitrary b, Show b, Embed a e) =>
TestName -> (b -> Exp e) -> (b -> a) -> TestTree
propUnary @M TestName
"dom" M -> Exp (Sett Int ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
SA.dom M -> Set Int
M -> Set (Domain M)
forall m. (Relation m, Ord (Domain m)) => m -> Set (Domain m)
dom
    , forall b a e.
(Eq a, Show a, Arbitrary b, Show b, Embed a e) =>
TestName -> (b -> Exp e) -> (b -> a) -> TestTree
propUnary @M TestName
"range" M -> Exp (Sett (Sum Float) ())
forall k v s (f :: * -> * -> *).
(Ord k, Ord v, HasExp s (f k v)) =>
s -> Exp (Sett v ())
SA.rng M -> Set (Sum Float)
M -> Set (Range M)
forall m. (Relation m, Ord (Range m)) => m -> Set (Range m)
range
    , forall b c a e.
(Eq a, Show a, Arbitrary b, Show b, Arbitrary c, Show c,
 Embed a e) =>
TestName -> (b -> c -> Exp e) -> (b -> c -> a) -> TestTree
propBinary @_ @M TestName
"∈" (\Sum Float
k M
m -> Sum Float
k Sum Float -> Set (Sum Float) -> Exp Bool
forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
SA.∈ M -> Set (Range M)
forall m. (Relation m, Ord (Range m)) => m -> Set (Range m)
range M
m) Sum Float -> M -> Bool
forall a (f :: * -> *). (Eq a, Foldable f) => a -> f a -> Bool
(∈)
    , forall b c a e.
(Eq a, Show a, Arbitrary b, Show b, Arbitrary c, Show c,
 Embed a e) =>
TestName -> (b -> c -> Exp e) -> (b -> c -> a) -> TestTree
propBinary @_ @M TestName
"∉" (\Sum Float
k M
m -> Sum Float
k Sum Float -> Set (Sum Float) -> Exp Bool
forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
SA.∉ M -> Set (Range M)
forall m. (Relation m, Ord (Range m)) => m -> Set (Range m)
range M
m) Sum Float -> M -> Bool
forall a (f :: * -> *). (Eq a, Foldable f) => a -> f a -> Bool
(∉)
    , forall b c a e.
(Eq a, Show a, Arbitrary b, Show b, Arbitrary c, Show c,
 Embed a e) =>
TestName -> (b -> c -> Exp e) -> (b -> c -> a) -> TestTree
propBinary @_ @M TestName
"haskey" (\Int
k M
m -> Int
k Int -> Set Int -> Exp Bool
forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
SA.∈ M -> Set (Domain M)
forall m. (Relation m, Ord (Domain m)) => m -> Set (Domain m)
dom M
m) Int -> M -> Bool
Domain M -> M -> Bool
forall m. (Relation m, Ord (Domain m)) => Domain m -> m -> Bool
haskey
    , forall b c a e.
(Eq a, Show a, Arbitrary b, Show b, Arbitrary c, Show c,
 Embed a e) =>
TestName -> (b -> c -> Exp e) -> (b -> c -> a) -> TestTree
propBinary @_ @M TestName
"◁" Set Int -> M -> Exp M
forall k s1 s2 (f :: * -> * -> *) v.
(Ord k, HasExp s1 (Sett k ()), HasExp s2 (f k v)) =>
s1 -> s2 -> Exp (f k v)
(SA.◁) Set Int -> M -> M
Set (Domain M) -> M -> M
forall m. (Relation m, Ord (Domain m)) => Set (Domain m) -> m -> m
(◁)
    , forall b c a e.
(Eq a, Show a, Arbitrary b, Show b, Arbitrary c, Show c,
 Embed a e) =>
TestName -> (b -> c -> Exp e) -> (b -> c -> a) -> TestTree
propBinary @_ @M TestName
"⋪" Set Int -> M -> Exp M
forall k (g :: * -> * -> *) s1 s2 (f :: * -> * -> *) v.
(Ord k, Iter g, HasExp s1 (g k ()), HasExp s2 (f k v)) =>
s1 -> s2 -> Exp (f k v)
(SA.⋪) Set Int -> M -> M
Set (Domain M) -> M -> M
forall m. (Relation m, Ord (Domain m)) => Set (Domain m) -> m -> m
(⋪)
    , forall b c a e.
(Eq a, Show a, Arbitrary b, Show b, Arbitrary c, Show c,
 Embed a e) =>
TestName -> (b -> c -> Exp e) -> (b -> c -> a) -> TestTree
propBinary @M TestName
"▷" M -> Set (Sum Float) -> Exp M
forall k (g :: * -> * -> *) v s1 (f :: * -> * -> *) s2.
(Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) =>
s1 -> s2 -> Exp (f k v)
(SA.▷) M -> Set (Sum Float) -> M
M -> Set (Range M) -> M
forall m. (Relation m, Ord (Range m)) => m -> Set (Range m) -> m
(▷)
    , forall b c a e.
(Eq a, Show a, Arbitrary b, Show b, Arbitrary c, Show c,
 Embed a e) =>
TestName -> (b -> c -> Exp e) -> (b -> c -> a) -> TestTree
propBinary @M TestName
"⋫" M -> Set (Sum Float) -> Exp M
forall k (g :: * -> * -> *) v s1 (f :: * -> * -> *) s2.
(Ord k, Iter g, Ord v, HasExp s1 (f k v), HasExp s2 (g v ())) =>
s1 -> s2 -> Exp (f k v)
(SA.⋫) M -> Set (Sum Float) -> M
M -> Set (Range M) -> M
forall m. (Relation m, Ord (Range m)) => m -> Set (Range m) -> m
(⋫)
    , forall b c a e.
(Eq a, Show a, Arbitrary b, Show b, Arbitrary c, Show c,
 Embed a e) =>
TestName -> (b -> c -> Exp e) -> (b -> c -> a) -> TestTree
propBinary @M TestName
"∪" M -> M -> Exp M
forall k v s1 (f :: * -> * -> *) s2 (g :: * -> * -> *).
(Show k, Show v, Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) =>
s1 -> s2 -> Exp (f k v)
(SA.∪) M -> M -> M
forall m.
(Relation m, Ord (Domain m), Ord (Range m)) =>
m -> m -> m
(∪)
    , forall b c a e.
(Eq a, Show a, Arbitrary b, Show b, Arbitrary c, Show c,
 Embed a e) =>
TestName -> (b -> c -> Exp e) -> (b -> c -> a) -> TestTree
propBinary @M TestName
"⨃" M -> M -> Exp M
forall k s1 (f :: * -> * -> *) v s2 (g :: * -> * -> *).
(Ord k, HasExp s1 (f k v), HasExp s2 (g k v)) =>
s1 -> s2 -> Exp (f k v)
(SA.⨃) M -> M -> M
forall m.
(Relation m, Ord (Domain m), Ord (Range m)) =>
m -> m -> m
(⨃)
    , forall b c a e.
(Eq a, Show a, Arbitrary b, Show b, Arbitrary c, Show c,
 Embed a e) =>
TestName -> (b -> c -> Exp e) -> (b -> c -> a) -> TestTree
propBinary @M TestName
"∪+" M -> M -> Exp M
forall k n s1 (f :: * -> * -> *) s2 (g :: * -> * -> *).
(Ord k, Monoid n, HasExp s1 (f k n), HasExp s2 (g k n)) =>
s1 -> s2 -> Exp (f k n)
(SA.∪+) M -> M -> M
forall a b. (Ord a, Num b) => Map a b -> Map a b -> Map a b
(∪+)
    , forall b c a e.
(Eq a, Show a, Arbitrary b, Show b, Arbitrary c, Show c,
 Embed a e) =>
TestName -> (b -> c -> Exp e) -> (b -> c -> a) -> TestTree
propBinary @M @M TestName
"⊆" (\M
m1 M
m2 -> M -> Exp (Sett (Sum Float) ())
forall k v s (f :: * -> * -> *).
(Ord k, Ord v, HasExp s (f k v)) =>
s -> Exp (Sett v ())
SA.rng M
m1 Exp (Sett (Sum Float) ()) -> Exp (Sett (Sum Float) ()) -> Exp Bool
forall k (f :: * -> * -> *) (g :: * -> * -> *) s1 v s2 u.
(Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) =>
s1 -> s2 -> Exp Bool
SA.⊆ M -> Exp (Sett (Sum Float) ())
forall k v s (f :: * -> * -> *).
(Ord k, Ord v, HasExp s (f k v)) =>
s -> Exp (Sett v ())
SA.rng M
m2) M -> M -> Bool
forall (f :: * -> *) (g :: * -> *) a.
(Foldable f, Foldable g, Ord a) =>
f a -> g a -> Bool
(⊆)
    , forall b c a e.
(Eq a, Show a, Arbitrary b, Show b, Arbitrary c, Show c,
 Embed a e) =>
TestName -> (b -> c -> Exp e) -> (b -> c -> a) -> TestTree
propBinary @(Set Int) TestName
"∩" Set Int -> Set Int -> Exp (Sett Int ())
forall k (f :: * -> * -> *) (g :: * -> * -> *) s1 v s2 u.
(Ord k, Iter f, Iter g, HasExp s1 (f k v), HasExp s2 (g k u)) =>
s1 -> s2 -> Exp (Sett k ())
(SA.∩) Set Int -> Set Int -> Set Int
forall a. Ord a => Set a -> Set a -> Set a
(∩)
    ]