module SMCDEL.Internal.Help (
  alleq,alleqWith,anydiff,anydiffWith,alldiff,
  groupSortWith,
  apply,(!),set,applyPartial,(!=),
  powerset,restrict,rtc,tc,Erel,bl,fusion,intersection,seteq,subseteq,lfp
  ) where
import Data.List ((\\),foldl',groupBy,sort,sortBy,union,intersect,nub)
import Data.Containers.ListUtils (nubOrd)

-- | A binary relation, represented by a list of tuples.
type Rel a b = [(a,b)]

-- | An equivalence relation given by equivalence classes, as a list of lists.
type Erel a = [[a]]

alleq  :: Eq a => [a] -> Bool
alleq :: forall a. Eq a => [a] -> Bool
alleq = (a -> a) -> [a] -> Bool
forall b a. Eq b => (a -> b) -> [a] -> Bool
alleqWith a -> a
forall a. a -> a
id

alleqWith :: Eq b => (a -> b) -> [a] -> Bool
alleqWith :: forall b a. Eq b => (a -> b) -> [a] -> Bool
alleqWith a -> b
_ [] = Bool
True
alleqWith a -> b
f (a
x:[a]
xs) = (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((a -> b
f a
x b -> b -> Bool
forall a. Eq a => a -> a -> Bool
==) (b -> Bool) -> (a -> b) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f) [a]
xs

anydiff :: Eq a => [a] -> Bool
anydiff :: forall a. Eq a => [a] -> Bool
anydiff = (a -> a) -> [a] -> Bool
forall b a. Eq b => (a -> b) -> [a] -> Bool
anydiffWith a -> a
forall a. a -> a
id

anydiffWith :: Eq b => (a -> b) -> [a] -> Bool
anydiffWith :: forall b a. Eq b => (a -> b) -> [a] -> Bool
anydiffWith a -> b
_ [] = Bool
False
anydiffWith a -> b
f (a
x:[a]
xs) = (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((a -> b
f a
x b -> b -> Bool
forall a. Eq a => a -> a -> Bool
/=) (b -> Bool) -> (a -> b) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f) [a]
xs

alldiff :: Eq a => [a] -> Bool
alldiff :: forall a. Eq a => [a] -> Bool
alldiff [] = Bool
True
alldiff (a
x:[a]
xs) = a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem a
x [a]
xs Bool -> Bool -> Bool
&& [a] -> Bool
forall a. Eq a => [a] -> Bool
alldiff [a]
xs

groupSortWith :: (Eq a, Ord b) => (a -> b) -> [a] -> [[a]]
groupSortWith :: forall a b. (Eq a, Ord b) => (a -> b) -> [a] -> [[a]]
groupSortWith a -> b
f = (a -> a -> Bool) -> [a] -> [[a]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (\ a
x a
y -> a -> a -> Ordering
myCompare a
x a
y Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ) ([a] -> [[a]]) -> ([a] -> [a]) -> [a] -> [[a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a -> Ordering) -> [a] -> [a]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy a -> a -> Ordering
myCompare where
  myCompare :: a -> a -> Ordering
myCompare a
x a
y = b -> b -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (a -> b
f a
x) (a -> b
f a
y)

apply :: Show a => Show b => Eq a => Rel a b -> a -> b
apply :: forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply Rel a b
rel a
left = case a -> Rel a b -> Maybe b
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
left Rel a b
rel of
  Maybe b
Nothing -> [Char] -> b
forall a. HasCallStack => [Char] -> a
error ([Char]
"apply: Relation " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Rel a b -> [Char]
forall a. Show a => a -> [Char]
show Rel a b
rel [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" not defined at " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
left)
  (Just b
this) -> b
this

(!) :: Show a => Show b => Eq a => Rel a b -> a -> b
! :: forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
(!) = Rel a b -> a -> b
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply

set :: Eq a => Rel a b -> a -> b -> Rel a b
set :: forall a b. Eq a => Rel a b -> a -> b -> Rel a b
set []               a
_ b
_    = []
set ((a
x',b
oldY):[(a, b)]
rest) a
x b
newY | a
x' a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x   = (a
x,b
newY) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)]
rest
                            | Bool
otherwise = (a
x',b
oldY) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)] -> a -> b -> [(a, b)]
forall a b. Eq a => Rel a b -> a -> b -> Rel a b
set [(a, b)]
rest a
x b
newY

applyPartial :: Eq a => [(a,a)] -> a -> a
applyPartial :: forall a. Eq a => [(a, a)] -> a -> a
applyPartial [(a, a)]
rel a
left = case a -> [(a, a)] -> Maybe a
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
left [(a, a)]
rel of
  Maybe a
Nothing     -> a
left
  (Just a
this) -> a
this

(!=) :: Eq a => [(a,a)] -> a -> a
!= :: forall a. Eq a => [(a, a)] -> a -> a
(!=) = [(a, a)] -> a -> a
forall a. Eq a => [(a, a)] -> a -> a
applyPartial

powerset :: [a] -> [[a]]
powerset :: forall a. [a] -> [[a]]
powerset []     = [[]]
powerset (a
x:[a]
xs) = ([a] -> [a]) -> [[a]] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
map (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:) [[a]]
pxs [[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
++ [[a]]
pxs where pxs :: [[a]]
pxs = [a] -> [[a]]
forall a. [a] -> [[a]]
powerset [a]
xs

concatRel :: (Ord a, Eq a) => Rel a a -> Rel a a -> Rel a a
concatRel :: forall a. (Ord a, Eq a) => Rel a a -> Rel a a -> Rel a a
concatRel Rel a a
r Rel a a
s = Rel a a -> Rel a a
forall a. Ord a => [a] -> [a]
nubOrd [ (a
x,a
z) | (a
x,a
y) <- Rel a a
r, (a
w,a
z) <- Rel a a
s, a
y a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
w ]

lfp :: Eq a => (a -> a) -> a -> a
lfp :: forall a. Eq a => (a -> a) -> a -> a
lfp a -> a
f a
x | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
f a
x  = a
x
        | Bool
otherwise = (a -> a) -> a -> a
forall a. Eq a => (a -> a) -> a -> a
lfp a -> a
f (a -> a
f a
x)

dom :: (Ord a, Eq a) => Rel a a -> [a]
dom :: forall a. (Ord a, Eq a) => Rel a a -> [a]
dom Rel a a
r = [a] -> [a]
forall a. Ord a => [a] -> [a]
nubOrd (((a, a) -> [a] -> [a]) -> [a] -> Rel a a -> [a]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (a
x,a
y) -> ([a
x,a
y][a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++)) [] Rel a a
r)

restrict :: Ord a => [a] -> Erel a -> Erel a
restrict :: forall a. Ord a => [a] -> Erel a -> Erel a
restrict [a]
domain =  [[a]] -> [[a]]
forall a. Ord a => [a] -> [a]
nubOrd ([[a]] -> [[a]]) -> ([[a]] -> [[a]]) -> [[a]] -> [[a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([a] -> Bool) -> [[a]] -> [[a]]
forall a. (a -> Bool) -> [a] -> [a]
filter ([a] -> [a] -> Bool
forall a. Eq a => a -> a -> Bool
/= []) ([[a]] -> [[a]]) -> ([[a]] -> [[a]]) -> [[a]] -> [[a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([a] -> [a]) -> [[a]] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter (a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
domain))

rtc :: (Ord a, Eq a) => Rel a a -> Rel a a
rtc :: forall a. (Ord a, Eq a) => Rel a a -> Rel a a
rtc Rel a a
r = (Rel a a -> Rel a a) -> Rel a a -> Rel a a
forall a. Eq a => (a -> a) -> a -> a
lfp (\ Rel a a
s -> Rel a a
s Rel a a -> Rel a a -> Rel a a
forall a. Eq a => [a] -> [a] -> [a]
`union` Rel a a -> Rel a a -> Rel a a
forall a. (Ord a, Eq a) => Rel a a -> Rel a a -> Rel a a
concatRel Rel a a
r Rel a a
s) [(a
x,a
x) | a
x <- Rel a a -> [a]
forall a. (Ord a, Eq a) => Rel a a -> [a]
dom Rel a a
r ]

tc :: (Ord a, Eq a) => Rel a a -> Rel a a
tc :: forall a. (Ord a, Eq a) => Rel a a -> Rel a a
tc Rel a a
r = (Rel a a -> Rel a a) -> Rel a a -> Rel a a
forall a. Eq a => (a -> a) -> a -> a
lfp (\ Rel a a
s -> Rel a a
s Rel a a -> Rel a a -> Rel a a
forall a. Eq a => [a] -> [a] -> [a]
`union` Rel a a -> Rel a a -> Rel a a
forall a. (Ord a, Eq a) => Rel a a -> Rel a a -> Rel a a
concatRel Rel a a
r Rel a a
s) Rel a a
r

merge :: Ord a => [a] -> [a] -> [a]
merge :: forall a. Ord a => [a] -> [a] -> [a]
merge [a]
xs [] = [a]
xs
merge [] [a]
ys = [a]
ys
merge (a
x:[a]
xs) (a
y:[a]
ys) = case a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
x a
y of
  Ordering
EQ -> a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a] -> [a] -> [a]
forall a. Ord a => [a] -> [a] -> [a]
merge [a]
xs [a]
ys
  Ordering
LT -> a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a] -> [a] -> [a]
forall a. Ord a => [a] -> [a] -> [a]
merge [a]
xs (a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ys)
  Ordering
GT -> a
y a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a] -> [a] -> [a]
forall a. Ord a => [a] -> [a] -> [a]
merge (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs) [a]
ys

mergeL :: Ord a => [[a]] -> [a]
mergeL :: forall a. Ord a => [[a]] -> [a]
mergeL = ([a] -> [a] -> [a]) -> [a] -> [[a]] -> [a]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' [a] -> [a] -> [a]
forall a. Ord a => [a] -> [a] -> [a]
merge []

overlap :: Ord a => [a] -> [a] -> Bool
overlap :: forall a. Ord a => [a] -> [a] -> Bool
overlap [] [a]
_  = Bool
False
overlap [a]
_  [] = Bool
False
overlap (a
x:[a]
xs) (a
y:[a]
ys) = case a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
x a
y of
  Ordering
EQ -> Bool
True
  Ordering
LT -> [a] -> [a] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
overlap [a]
xs (a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ys)
  Ordering
GT -> [a] -> [a] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
overlap (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs) [a]
ys

bl :: Eq a => Erel a -> a -> [a]
bl :: forall a. Eq a => Erel a -> a -> [a]
bl Erel a
r a
x = Erel a -> [a]
forall a. HasCallStack => [a] -> a
head (([a] -> Bool) -> Erel a -> Erel a
forall a. (a -> Bool) -> [a] -> [a]
filter (a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
x) Erel a
r)

fusion :: Ord a => [[a]] -> Erel a
fusion :: forall a. Ord a => [[a]] -> [[a]]
fusion [] = []
fusion ([a]
b:[[a]]
bs) = let
    cs :: [[a]]
cs = ([a] -> Bool) -> [[a]] -> [[a]]
forall a. (a -> Bool) -> [a] -> [a]
filter ([a] -> [a] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
overlap [a]
b) [[a]]
bs
    xs :: [a]
xs = [[a]] -> [a]
forall a. Ord a => [[a]] -> [a]
mergeL ([a]
b[a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
:[[a]]
cs)
    ds :: [[a]]
ds = ([a] -> Bool) -> [[a]] -> [[a]]
forall a. (a -> Bool) -> [a] -> [a]
filter ([a] -> [a] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
overlap [a]
xs) [[a]]
bs
  in if [[a]]
cs [[a]] -> [[a]] -> Bool
forall a. Eq a => a -> a -> Bool
== [[a]]
ds then [a]
xs [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: [[a]] -> [[a]]
forall a. Ord a => [[a]] -> [[a]]
fusion ([[a]]
bs [[a]] -> [[a]] -> [[a]]
forall a. Eq a => [a] -> [a] -> [a]
\\ [[a]]
cs) else [[a]] -> [[a]]
forall a. Ord a => [[a]] -> [[a]]
fusion ([a]
xs [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: [[a]]
bs)

-- Binary intersection of two equivalence relations. Given equivalence classes
-- lists e and f, all non-empty intersections of an equivalence class x from e
-- with an equivalence class y from f are computed. Then, empty and duplicate
-- intersetions are removed.
binaryIntersection :: Ord a => Erel a -> Erel a -> Erel a
binaryIntersection :: forall a. Ord a => Erel a -> Erel a -> Erel a
binaryIntersection Erel a
e Erel a
f = Erel a -> Erel a
forall a. Eq a => [a] -> [a]
nub [ [a] -> [a]
forall a. Ord a => [a] -> [a]
sort [a]
res | [a]
x <- Erel a
e, [a]
y <- Erel a
f,
  let res :: [a]
res = [a]
x [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [a]
y, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
res]

-- N-ary (finite) intersection of 0 or more equivalence relations. The first
-- parameter, u(niverse), is used to build a trivial, full equivalence relation
-- when the intersection of an empty set is attempted.
intersection :: Ord a => [a] -> [Erel a] -> Erel a
intersection :: forall a. Ord a => [a] -> [Erel a] -> Erel a
intersection [a]
u [] = [[a]
u]
intersection [a]
_ [Erel a]
l = (Erel a -> Erel a -> Erel a) -> [Erel a] -> Erel a
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Erel a -> Erel a -> Erel a
forall a. Ord a => Erel a -> Erel a -> Erel a
binaryIntersection [Erel a]
l

seteq :: Ord a => [a] -> [a] -> Bool
seteq :: forall a. Ord a => [a] -> [a] -> Bool
seteq [a]
as [a]
bs = [a] -> [a]
forall a. Ord a => [a] -> [a]
sort [a]
as [a] -> [a] -> Bool
forall a. Eq a => a -> a -> Bool
== [a] -> [a]
forall a. Ord a => [a] -> [a]
sort [a]
bs

subseteq :: Eq a => [a] -> [a] -> Bool
subseteq :: forall a. Eq a => [a] -> [a] -> Bool
subseteq [a]
xs [a]
ys = (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
ys) [a]
xs