{-# 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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` 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
(∈) = 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
(∉) = 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 = 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 = forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map k v
r 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 = forall k a. Ord k => Map k a -> Set k -> Map k a
Map.withoutKeys Map k v
r 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 = forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (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 = forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (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 = 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 = 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 = 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
(∪+) = forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith 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 = forall (f :: * -> *) a. (Foldable f, Ord a) => f a -> Set a
toSet f a
x forall a. Ord a => Set a -> Set a -> Bool
`isSubsetOf` 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 = forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
(∩) = 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 =
  forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
name (\b
arg -> forall s t. Embed s t => Exp t -> s
SA.eval (b -> Exp e
expr b
arg) 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 =
  forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
name (\b
arg1 c
arg2 -> forall s t. Embed s t => Exp t -> s
SA.eval (b -> c -> Exp e
expr b
arg1 c
arg2) 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" forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
SA.dom 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" forall k v s (f :: * -> * -> *).
(Ord k, Ord v, HasExp s (f k v)) =>
s -> Exp (Sett v ())
SA.rng 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 forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
SA.∈ forall m. (Relation m, Ord (Range m)) => m -> Set (Range m)
range M
m) 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 forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
SA.∉ forall m. (Relation m, Ord (Range m)) => m -> Set (Range m)
range M
m) 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 forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
SA.∈ forall m. (Relation m, Ord (Domain m)) => m -> Set (Domain m)
dom M
m) 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
"◁" forall k s1 s2 (f :: * -> * -> *) v.
(Ord k, HasExp s1 (Sett k ()), HasExp s2 (f k v)) =>
s1 -> s2 -> Exp (f k v)
(SA.◁) 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
"⋪" 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.⋪) 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
"▷" 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.▷) 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
"⋫" 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.⋫) 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
"∪" 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.∪) 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
"⨃" 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.⨃) 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
"∪+" 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.∪+) 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 -> forall k v s (f :: * -> * -> *).
(Ord k, Ord v, HasExp s (f k v)) =>
s -> Exp (Sett v ())
SA.rng M
m1 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.⊆ forall k v s (f :: * -> * -> *).
(Ord k, Ord v, HasExp s (f k v)) =>
s -> Exp (Sett v ())
SA.rng M
m2) 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
"∩" 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.∩) forall a. Ord a => Set a -> Set a -> Set a
(∩)
    ]