{-# 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.Hspec (Spec, describe)
import Test.Hspec.QuickCheck (prop)
import Test.QuickCheck (Arbitrary, (===))

---------------------------------------------------------------------------------
-- 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) =>
  String ->
  (b -> SA.Exp e) ->
  (b -> a) ->
  Spec
propUnary :: forall b a e.
(Eq a, Show a, Arbitrary b, Show b, Embed a e) =>
String -> (b -> Exp e) -> (b -> a) -> Spec
propUnary String
name b -> Exp e
expr b -> a
relExpr =
  String -> (b -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
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) =>
  String ->
  (b -> c -> SA.Exp e) ->
  (b -> c -> a) ->
  Spec
propBinary :: forall b c a e.
(Eq a, Show a, Arbitrary b, Show b, Arbitrary c, Show c,
 Embed a e) =>
String -> (b -> c -> Exp e) -> (b -> c -> a) -> Spec
propBinary String
name b -> c -> Exp e
expr b -> c -> a
relExpr =
  String -> (b -> c -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
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 :: Spec
relationTests :: Spec
relationTests =
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"RelationTests - check conformance with the original implementation" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    forall b a e.
(Eq a, Show a, Arbitrary b, Show b, Embed a e) =>
String -> (b -> Exp e) -> (b -> a) -> Spec
propUnary @M String
"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) =>
String -> (b -> Exp e) -> (b -> a) -> Spec
propUnary @M String
"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) =>
String -> (b -> c -> Exp e) -> (b -> c -> a) -> Spec
propBinary @_ @M String
"∈" (\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) =>
String -> (b -> c -> Exp e) -> (b -> c -> a) -> Spec
propBinary @_ @M String
"∉" (\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) =>
String -> (b -> c -> Exp e) -> (b -> c -> a) -> Spec
propBinary @_ @M String
"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) =>
String -> (b -> c -> Exp e) -> (b -> c -> a) -> Spec
propBinary @_ @M String
"◁" 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) =>
String -> (b -> c -> Exp e) -> (b -> c -> a) -> Spec
propBinary @_ @M String
"⋪" 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) =>
String -> (b -> c -> Exp e) -> (b -> c -> a) -> Spec
propBinary @M String
"▷" 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) =>
String -> (b -> c -> Exp e) -> (b -> c -> a) -> Spec
propBinary @M String
"⋫" 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) =>
String -> (b -> c -> Exp e) -> (b -> c -> a) -> Spec
propBinary @M String
"∪" 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) =>
String -> (b -> c -> Exp e) -> (b -> c -> a) -> Spec
propBinary @M String
"⨃" 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) =>
String -> (b -> c -> Exp e) -> (b -> c -> a) -> Spec
propBinary @M String
"∪+" 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) =>
String -> (b -> c -> Exp e) -> (b -> c -> a) -> Spec
propBinary @M @M String
"⊆" (\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) =>
String -> (b -> c -> Exp e) -> (b -> c -> a) -> Spec
propBinary @(Set Int) String
"∩" 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
(∩)