{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TupleSections #-}

-- |

-- Module      : OAlg.Entity.Sequence.Graph

-- Description : graphs of entities

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- graphs of entities in @__x__@.

module OAlg.Entity.Sequence.Graph
  ( -- * Graph

    Graph(..), gphLength, gphxs, gphSqc, gphLookup, gphTakeN
  , gphSetFilter

    -- ** Lattice

  , gphUnion, gphIntersection, gphDifference, isSubGraph

    -- * Conversions

  , gphset, setgph
  ) where

import Control.Monad as M hiding (sequence)

import Data.List (head,map,groupBy)

import OAlg.Prelude

import OAlg.Data.Filterable

import OAlg.Entity.Sequence.Set

import OAlg.Structure.PartiallyOrdered
import OAlg.Structure.Lattice

--------------------------------------------------------------------------------

-- Graph -


-- | mapping from an ordered /index/ type @__i__@ to a 'Entity' type @__x__@.

--

--  __Property__ Let @g = 'Graph' ixs@ be in @'Graph' __i__ __x__@ for a ordered 'Entity'

-- type @__i__@ and 'Entity' type @__x__@, then holds:

--

-- (1) For all @..(i,_)':'(j,_)..@ in @ixs@ holds: @i '<' j@.

--

-- (2) @'lengthN' g '==' 'lengthN' ixs@.

newtype Graph i x = Graph [(i,x)] deriving (Int -> Graph i x -> ShowS
[Graph i x] -> ShowS
Graph i x -> String
(Int -> Graph i x -> ShowS)
-> (Graph i x -> String)
-> ([Graph i x] -> ShowS)
-> Show (Graph i x)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall i x. (Show i, Show x) => Int -> Graph i x -> ShowS
forall i x. (Show i, Show x) => [Graph i x] -> ShowS
forall i x. (Show i, Show x) => Graph i x -> String
$cshowsPrec :: forall i x. (Show i, Show x) => Int -> Graph i x -> ShowS
showsPrec :: Int -> Graph i x -> ShowS
$cshow :: forall i x. (Show i, Show x) => Graph i x -> String
show :: Graph i x -> String
$cshowList :: forall i x. (Show i, Show x) => [Graph i x] -> ShowS
showList :: [Graph i x] -> ShowS
Show,Graph i x -> Graph i x -> Bool
(Graph i x -> Graph i x -> Bool)
-> (Graph i x -> Graph i x -> Bool) -> Eq (Graph i x)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall i x. (Eq i, Eq x) => Graph i x -> Graph i x -> Bool
$c== :: forall i x. (Eq i, Eq x) => Graph i x -> Graph i x -> Bool
== :: Graph i x -> Graph i x -> Bool
$c/= :: forall i x. (Eq i, Eq x) => Graph i x -> Graph i x -> Bool
/= :: Graph i x -> Graph i x -> Bool
Eq,Eq (Graph i x)
Eq (Graph i x) =>
(Graph i x -> Graph i x -> Ordering)
-> (Graph i x -> Graph i x -> Bool)
-> (Graph i x -> Graph i x -> Bool)
-> (Graph i x -> Graph i x -> Bool)
-> (Graph i x -> Graph i x -> Bool)
-> (Graph i x -> Graph i x -> Graph i x)
-> (Graph i x -> Graph i x -> Graph i x)
-> Ord (Graph i x)
Graph i x -> Graph i x -> Bool
Graph i x -> Graph i x -> Ordering
Graph i x -> Graph i x -> Graph i x
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall i x. (Ord i, Ord x) => Eq (Graph i x)
forall i x. (Ord i, Ord x) => Graph i x -> Graph i x -> Bool
forall i x. (Ord i, Ord x) => Graph i x -> Graph i x -> Ordering
forall i x. (Ord i, Ord x) => Graph i x -> Graph i x -> Graph i x
$ccompare :: forall i x. (Ord i, Ord x) => Graph i x -> Graph i x -> Ordering
compare :: Graph i x -> Graph i x -> Ordering
$c< :: forall i x. (Ord i, Ord x) => Graph i x -> Graph i x -> Bool
< :: Graph i x -> Graph i x -> Bool
$c<= :: forall i x. (Ord i, Ord x) => Graph i x -> Graph i x -> Bool
<= :: Graph i x -> Graph i x -> Bool
$c> :: forall i x. (Ord i, Ord x) => Graph i x -> Graph i x -> Bool
> :: Graph i x -> Graph i x -> Bool
$c>= :: forall i x. (Ord i, Ord x) => Graph i x -> Graph i x -> Bool
>= :: Graph i x -> Graph i x -> Bool
$cmax :: forall i x. (Ord i, Ord x) => Graph i x -> Graph i x -> Graph i x
max :: Graph i x -> Graph i x -> Graph i x
$cmin :: forall i x. (Ord i, Ord x) => Graph i x -> Graph i x -> Graph i x
min :: Graph i x -> Graph i x -> Graph i x
Ord,Graph i x -> N
(Graph i x -> N) -> LengthN (Graph i x)
forall x. (x -> N) -> LengthN x
forall i x. Graph i x -> N
$clengthN :: forall i x. Graph i x -> N
lengthN :: Graph i x -> N
LengthN)

relGraph :: (Entity x, Entity i, Ord i) => Graph i x -> Statement
relGraph :: forall x i. (Entity x, Entity i, Ord i) => Graph i x -> Statement
relGraph (Graph [])       = Statement
SValid
relGraph (Graph ((i, x)
ix:[(i, x)]
ixs)) = (i, x) -> Statement
forall a. Validable a => a -> Statement
valid (i, x)
ix Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& N -> (i, x) -> [(i, x)] -> Statement
forall {b} {b} {t}.
(Validable b, Validable b, Ord b, Show t, Show b, Enum t) =>
t -> (b, b) -> [(b, b)] -> Statement
vld (N
0::N) (i, x)
ix [(i, x)]
ixs where
  vld :: t -> (b, b) -> [(b, b)] -> Statement
vld t
_ (b, b)
_ []                 = Statement
SValid
  vld t
k (b
i,b
_) (jx :: (b, b)
jx@(b
j,b
_):[(b, b)]
ixs) = [Statement] -> Statement
And [ (b, b) -> Statement
forall a. Validable a => a -> Statement
valid (b, b)
jx
                                   , (b
ib -> b -> Bool
forall a. Ord a => a -> a -> Bool
<b
j) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"k"String -> String -> Parameter
:=t -> String
forall a. Show a => a -> String
show t
k,String
"(i,j)"String -> String -> Parameter
:=(b, b) -> String
forall a. Show a => a -> String
show (b
i,b
j)]
                                   , t -> (b, b) -> [(b, b)] -> Statement
vld (t -> t
forall a. Enum a => a -> a
succ t
k) (b, b)
jx [(b, b)]
ixs
                                   ]

instance (Entity x, Entity i, Ord i) => Validable (Graph i x) where
  valid :: Graph i x -> Statement
valid Graph i x
g = String -> Label
Label String
"Graph" Label -> Statement -> Statement
:<=>: Graph i x -> Statement
forall x i. (Entity x, Entity i, Ord i) => Graph i x -> Statement
relGraph Graph i x
g

-- instance (Entity x, Entity i, Ord i) => Entity (Graph i x)


instance M.Functor (Graph i) where
  fmap :: forall a b. (a -> b) -> Graph i a -> Graph i b
fmap a -> b
f (Graph [(i, a)]
ixs) = [(i, b)] -> Graph i b
forall i x. [(i, x)] -> Graph i x
Graph ([(i, b)] -> Graph i b) -> [(i, b)] -> Graph i b
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((i, a) -> (i, b)) -> [(i, a)] -> [(i, b)]
forall a b. (a -> b) -> [a] -> [b]
map (\(i
i,a
x) -> (i
i, a -> b
f a
x)) [(i, a)]
ixs

instance Filterable (Graph i) where
  filter :: forall x. (x -> Bool) -> Graph i x -> Graph i x
filter x -> Bool
p (Graph [(i, x)]
ixs) = [(i, x)] -> Graph i x
forall i x. [(i, x)] -> Graph i x
Graph ([(i, x)] -> Graph i x) -> [(i, x)] -> Graph i x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((i, x) -> Bool) -> [(i, x)] -> [(i, x)]
forall x. (x -> Bool) -> [x] -> [x]
forall (s :: * -> *) x. Filterable s => (x -> Bool) -> s x -> s x
filter (x -> Bool
p (x -> Bool) -> ((i, x) -> x) -> (i, x) -> Bool
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (i, x) -> x
forall a b. (a, b) -> b
snd) [(i, x)]
ixs

--------------------------------------------------------------------------------

-- gphSetFilter -


-- | filtering elements of the associated sets.

gphSetFilter :: (b -> Bool) -> Graph a (Set b) -> Graph a (Set b)
gphSetFilter :: forall b a. (b -> Bool) -> Graph a (Set b) -> Graph a (Set b)
gphSetFilter b -> Bool
p (Graph [(a, Set b)]
asb) = [(a, Set b)] -> Graph a (Set b)
forall i x. [(i, x)] -> Graph i x
Graph ([(a, Set b)] -> Graph a (Set b))
-> [(a, Set b)] -> Graph a (Set b)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((a, Set b) -> (a, Set b)) -> [(a, Set b)] -> [(a, Set b)]
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(a
x,Set b
ys) -> (a
x,(b -> Bool) -> Set b -> Set b
forall x. (x -> Bool) -> Set x -> Set x
forall (s :: * -> *) x. Filterable s => (x -> Bool) -> s x -> s x
filter b -> Bool
p Set b
ys)) [(a, Set b)]
asb

--------------------------------------------------------------------------------

-- gphLookup -


-- | looks up the mapping of an index.

gphLookup :: Ord i => Graph i x -> i -> Maybe x
gphLookup :: forall i x. Ord i => Graph i x -> i -> Maybe x
gphLookup (Graph [(i, x)]
ixs) = [(i, x)] -> i -> Maybe x
forall {t} {a}. Ord t => [(t, a)] -> t -> Maybe a
lookup [(i, x)]
ixs where
  lookup :: [(t, a)] -> t -> Maybe a
lookup [] t
_           = Maybe a
forall a. Maybe a
Nothing
  lookup ((t
i',a
x):[(t, a)]
ixs) t
i = case t
i t -> t -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` t
i' of
    Ordering
LT -> Maybe a
forall a. Maybe a
Nothing
    Ordering
EQ -> a -> Maybe a
forall a. a -> Maybe a
Just a
x
    Ordering
GT -> [(t, a)] -> t -> Maybe a
lookup [(t, a)]
ixs t
i

--------------------------------------------------------------------------------

-- gphLength -


-- | the length of a graph.

gphLength :: Graph i x -> N
gphLength :: forall i x. Graph i x -> N
gphLength (Graph [(i, x)]
ixs) = [(i, x)] -> N
forall x. LengthN x => x -> N
lengthN [(i, x)]
ixs

--------------------------------------------------------------------------------

-- gphxs -


-- | the underlying associations.

gphxs :: Graph i x -> [(i,x)]
gphxs :: forall i x. Graph i x -> [(i, x)]
gphxs (Graph [(i, x)]
ixs) = [(i, x)]
ixs

--------------------------------------------------------------------------------

-- gphSqc -


-- | the induced graph given by a set of indices and a mapping.

gphSqc :: (i -> Maybe x) -> Set i -> Graph i x
gphSqc :: forall i x. (i -> Maybe x) -> Set i -> Graph i x
gphSqc i -> Maybe x
mx (Set [i]
is)
  = [(i, x)] -> Graph i x
forall i x. [(i, x)] -> Graph i x
Graph
  ([(i, x)] -> Graph i x) -> [(i, x)] -> Graph i x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((i, Maybe x) -> (i, x)) -> [(i, Maybe x)] -> [(i, x)]
forall a b. (a -> b) -> [a] -> [b]
map (\(i
i,Maybe x
jx) -> (i
i,Maybe x -> x
forall a. HasCallStack => Maybe a -> a
fromJust Maybe x
jx))
  ([(i, Maybe x)] -> [(i, x)]) -> [(i, Maybe x)] -> [(i, x)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((i, Maybe x) -> Bool) -> [(i, Maybe x)] -> [(i, Maybe x)]
forall x. (x -> Bool) -> [x] -> [x]
forall (s :: * -> *) x. Filterable s => (x -> Bool) -> s x -> s x
filter (Maybe x -> Bool
forall a. Maybe a -> Bool
isJust (Maybe x -> Bool)
-> ((i, Maybe x) -> Maybe x) -> (i, Maybe x) -> Bool
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (i, Maybe x) -> Maybe x
forall a b. (a, b) -> b
snd)
  ([(i, Maybe x)] -> [(i, Maybe x)])
-> [(i, Maybe x)] -> [(i, Maybe x)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (i -> (i, Maybe x)) -> [i] -> [(i, Maybe x)]
forall a b. (a -> b) -> [a] -> [b]
map (\i
i -> (i
i,i -> Maybe x
mx i
i)) [i]
is

--------------------------------------------------------------------------------

-- gphTakeN -


-- | takes the first @n@ elements.

gphTakeN :: N -> Graph i x -> Graph i x
gphTakeN :: forall i x. N -> Graph i x -> Graph i x
gphTakeN N
n (Graph [(i, x)]
ixs) = [(i, x)] -> Graph i x
forall i x. [(i, x)] -> Graph i x
Graph ([(i, x)] -> Graph i x) -> [(i, x)] -> Graph i x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> [(i, x)] -> [(i, x)]
forall a. N -> [a] -> [a]
takeN N
n [(i, x)]
ixs

--------------------------------------------------------------------------------

-- gphset -


-- | converts a graph of sets to a set of pairs. The /inverse/ is given by 'setgph'.

--

-- __Note__

--

-- (1) This works also with infinite graphs of sets.

--

-- (2) It is not true that 'setgph' and 'gphset' are inverse in the strict sense, but almost, i.e.

-- only in one restricts the graph to not empty associations. For example

-- @'Graph' [(1,'Set' []) :: 'Graph' 'N' ('Set' Char)@ and @'Graph' [] :: 'Graph' 'N' ('Set' Char)@

-- both are mapped under 'gphset' to @'Set' [] :: 'Set' ('N',Char)@.

gphset :: Graph a (Set b) -> Set (a,b)
gphset :: forall a b. Graph a (Set b) -> Set (a, b)
gphset (Graph [(a, Set b)]
asb) = [(a, b)] -> Set (a, b)
forall x. [x] -> Set x
Set ([(a, b)] -> Set (a, b)) -> [(a, b)] -> Set (a, b)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [[(a, b)]] -> [(a, b)]
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join ([[(a, b)]] -> [(a, b)]) -> [[(a, b)]] -> [(a, b)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((a, Set b) -> [(a, b)]) -> [(a, Set b)] -> [[(a, b)]]
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(a
a,Set [b]
bs) -> (b -> (a, b)) -> [b] -> [(a, b)]
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (a
a,) [b]
bs) [(a, Set b)]
asb

--------------------------------------------------------------------------------

-- setgph -


-- | converts a set of pairs to a graph of sets. The /inverse/ is given by 'gphset'.

--

-- __Note__ This works also with infinite sets of pairs..

setgph :: Eq a => Set (a,b) -> Graph a (Set b)
setgph :: forall a b. Eq a => Set (a, b) -> Graph a (Set b)
setgph (Set [(a, b)]
ab) = [(a, Set b)] -> Graph a (Set b)
forall i x. [(i, x)] -> Graph i x
Graph ([(a, Set b)] -> Graph a (Set b))
-> [(a, Set b)] -> Graph a (Set b)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ([(a, b)] -> (a, Set b)) -> [[(a, b)]] -> [(a, Set b)]
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 [(a, b)] -> (a, Set b)
forall {a} {b}. [(a, b)] -> (a, Set b)
aggr ([[(a, b)]] -> [(a, Set b)]) -> [[(a, b)]] -> [(a, Set b)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((a, b) -> (a, b) -> Bool) -> [(a, b)] -> [[(a, b)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (a, b) -> (a, b) -> Bool
forall {a} {b} {b}. Eq a => (a, b) -> (a, b) -> Bool
(~) [(a, b)]
ab
  where (a
x,b
_) ~ :: (a, b) -> (a, b) -> Bool
~ (a
y,b
_) = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y
        aggr :: [(a, b)] -> (a, Set b)
aggr [(a, b)]
abs = ((a, b) -> a
forall a b. (a, b) -> a
fst ((a, b) -> a) -> (a, b) -> a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(a, b)] -> (a, b)
forall a. HasCallStack => [a] -> a
head [(a, b)]
abs,[b] -> Set b
forall x. [x] -> Set x
Set ([b] -> Set b) -> [b] -> Set b
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((a, b) -> b) -> [(a, b)] -> [b]
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (a, b) -> b
forall a b. (a, b) -> b
snd [(a, b)]
abs)

--------------------------------------------------------------------------------

-- gphUnion -


-- | the union of two graphs on sets.

gphUnion :: (Ord a, Ord b) => Graph a (Set b) -> Graph a (Set b) -> Graph a (Set b)
gphUnion :: forall a b.
(Ord a, Ord b) =>
Graph a (Set b) -> Graph a (Set b) -> Graph a (Set b)
gphUnion (Graph [(a, Set b)]
xxs) (Graph [(a, Set b)]
yys) = [(a, Set b)] -> Graph a (Set b)
forall i x. [(i, x)] -> Graph i x
Graph ([(a, Set b)] -> Graph a (Set b))
-> [(a, Set b)] -> Graph a (Set b)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(a, Set b)] -> [(a, Set b)] -> [(a, Set b)]
forall {a} {b}.
(Ord a, Logical b) =>
[(a, b)] -> [(a, b)] -> [(a, b)]
uni [(a, Set b)]
xxs [(a, Set b)]
yys where
  uni :: [(a, b)] -> [(a, b)] -> [(a, b)]
uni [] [(a, b)]
yys = [(a, b)]
yys
  uni [(a, b)]
xxs [] = [(a, b)]
xxs
  uni ((a
x,b
xs):[(a, b)]
xxs) ((a
y,b
ys):[(a, b)]
yys) = case a
x a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` a
y of
    Ordering
LT -> (a
x,b
xs) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)] -> [(a, b)] -> [(a, b)]
uni [(a, b)]
xxs ((a
y,b
ys)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[(a, b)]
yys)
    Ordering
EQ -> (a
x,b
xs b -> b -> b
forall a. Logical a => a -> a -> a
|| b
ys) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)] -> [(a, b)] -> [(a, b)]
uni [(a, b)]
xxs [(a, b)]
yys
    Ordering
GT -> (a
y,b
ys) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)] -> [(a, b)] -> [(a, b)]
uni ((a
x,b
xs)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[(a, b)]
xxs) [(a, b)]
yys

--------------------------------------------------------------------------------

-- gphIntersection -


-- | the intersection of two graphs on sets.

gphIntersection :: (Ord a, Ord b) => Graph a (Set b) -> Graph a (Set b) -> Graph a (Set b)
gphIntersection :: forall a b.
(Ord a, Ord b) =>
Graph a (Set b) -> Graph a (Set b) -> Graph a (Set b)
gphIntersection (Graph [(a, Set b)]
xxs) (Graph [(a, Set b)]
yys) = [(a, Set b)] -> Graph a (Set b)
forall i x. [(i, x)] -> Graph i x
Graph ([(a, Set b)] -> Graph a (Set b))
-> [(a, Set b)] -> Graph a (Set b)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(a, Set b)] -> [(a, Set b)] -> [(a, Set b)]
forall {a} {b}.
(Ord a, Logical b) =>
[(a, b)] -> [(a, b)] -> [(a, b)]
intr [(a, Set b)]
xxs [(a, Set b)]
yys where
  intr :: [(a, b)] -> [(a, b)] -> [(a, b)]
intr ((a
x,b
xs):[(a, b)]
xxs) ((a
y,b
ys):[(a, b)]
yys) = case a
x a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` a
y of
    Ordering
LT -> [(a, b)] -> [(a, b)] -> [(a, b)]
intr [(a, b)]
xxs ((a
y,b
ys)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[(a, b)]
yys)
    Ordering
EQ -> (a
x,b
xs b -> b -> b
forall a. Logical a => a -> a -> a
&& b
ys) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)] -> [(a, b)] -> [(a, b)]
intr [(a, b)]
xxs [(a, b)]
yys
    Ordering
GT -> [(a, b)] -> [(a, b)] -> [(a, b)]
intr ((a
x,b
xs)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[(a, b)]
xxs) [(a, b)]
yys
  intr [(a, b)]
_ [(a, b)]
_ = []

--------------------------------------------------------------------------------

-- ghpDifference -


-- | the difference of two graphs on sets.

gphDifference :: (Ord a, Ord b) => Graph a (Set b) -> Graph a (Set b) -> Graph a (Set b)
gphDifference :: forall a b.
(Ord a, Ord b) =>
Graph a (Set b) -> Graph a (Set b) -> Graph a (Set b)
gphDifference (Graph [(a, Set b)]
xxs) (Graph [(a, Set b)]
yys) = [(a, Set b)] -> Graph a (Set b)
forall i x. [(i, x)] -> Graph i x
Graph ([(a, Set b)] -> Graph a (Set b))
-> [(a, Set b)] -> Graph a (Set b)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(a, Set b)] -> [(a, Set b)] -> [(a, Set b)]
forall {a} {b}.
(Ord a, Erasable b) =>
[(a, b)] -> [(a, b)] -> [(a, b)]
diff [(a, Set b)]
xxs [(a, Set b)]
yys where
  diff :: [(a, b)] -> [(a, b)] -> [(a, b)]
diff [] [(a, b)]
_   = []
  diff [(a, b)]
xxs [] = [(a, b)]
xxs
  diff ((a
x,b
xs):[(a, b)]
xxs) ((a
y,b
ys):[(a, b)]
yys) = case a
x a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` a
y of
    Ordering
LT -> (a
x,b
xs) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)] -> [(a, b)] -> [(a, b)]
diff [(a, b)]
xxs ((a
y,b
ys)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[(a, b)]
yys)
    Ordering
EQ -> (a
x,b
xs b -> b -> b
forall a. Erasable a => a -> a -> a
// b
ys) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)] -> [(a, b)] -> [(a, b)]
diff [(a, b)]
xxs [(a, b)]
yys
    Ordering
GT -> [(a, b)] -> [(a, b)] -> [(a, b)]
diff ((a
x,b
xs)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[(a, b)]
xxs) [(a, b)]
yys

--------------------------------------------------------------------------------

-- isSubGraph -


-- | testing of being a sub graph.

isSubGraph :: (Ord a, Ord b) => Graph a (Set b) -> Graph a (Set b) -> Bool
isSubGraph :: forall a b.
(Ord a, Ord b) =>
Graph a (Set b) -> Graph a (Set b) -> Bool
isSubGraph (Graph [(a, Set b)]
xxs) (Graph [(a, Set b)]
yys) = [(a, Set b)] -> [(a, Set b)] -> Bool
forall {a} {a}.
(Ord a, PartiallyOrdered a) =>
[(a, a)] -> [(a, a)] -> Bool
sub [(a, Set b)]
xxs [(a, Set b)]
yys where
  sub :: [(a, a)] -> [(a, a)] -> Bool
sub [] [(a, a)]
_ = Bool
True
  sub [(a, a)]
_ [] = Bool
False
  sub ((a
x,a
xs):[(a, a)]
xxs) ((a
y,a
ys):[(a, a)]
yys) = case a
x a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` a
y of
    Ordering
LT -> Bool
False
    Ordering
EQ -> (a
xs a -> a -> Bool
forall a. PartiallyOrdered a => a -> a -> Bool
<<= a
ys) Bool -> Bool -> Bool
forall a. Logical a => a -> a -> a
&& [(a, a)] -> [(a, a)] -> Bool
sub [(a, a)]
xxs [(a, a)]
yys 
    Ordering
GT -> [(a, a)] -> [(a, a)] -> Bool
sub ((a
x,a
xs)(a, a) -> [(a, a)] -> [(a, a)]
forall a. a -> [a] -> [a]
:[(a, a)]
xxs) [(a, a)]
yys
  
--------------------------------------------------------------------------------

-- Graph a (Set b) - Lattice -


instance (Ord a, Ord b) => Logical (Graph a (Set b)) where
  || :: Graph a (Set b) -> Graph a (Set b) -> Graph a (Set b)
(||) = Graph a (Set b) -> Graph a (Set b) -> Graph a (Set b)
forall a b.
(Ord a, Ord b) =>
Graph a (Set b) -> Graph a (Set b) -> Graph a (Set b)
gphUnion
  && :: Graph a (Set b) -> Graph a (Set b) -> Graph a (Set b)
(&&) = Graph a (Set b) -> Graph a (Set b) -> Graph a (Set b)
forall a b.
(Ord a, Ord b) =>
Graph a (Set b) -> Graph a (Set b) -> Graph a (Set b)
gphIntersection

instance (Ord a, Ord b) => Erasable (Graph a (Set b)) where // :: Graph a (Set b) -> Graph a (Set b) -> Graph a (Set b)
(//) = Graph a (Set b) -> Graph a (Set b) -> Graph a (Set b)
forall a b.
(Ord a, Ord b) =>
Graph a (Set b) -> Graph a (Set b) -> Graph a (Set b)
gphDifference

instance (Ord a, Ord b) => PartiallyOrdered (Graph a (Set b)) where <<= :: Graph a (Set b) -> Graph a (Set b) -> Bool
(<<=) = Graph a (Set b) -> Graph a (Set b) -> Bool
forall a b.
(Ord a, Ord b) =>
Graph a (Set b) -> Graph a (Set b) -> Bool
isSubGraph
instance (Ord a, Ord b) => Empty (Graph a (Set b)) where empty :: Graph a (Set b)
empty = [(a, Set b)] -> Graph a (Set b)
forall i x. [(i, x)] -> Graph i x
Graph []

instance (Ord a, Ord b) => Lattice (Graph a (Set b))