{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DeriveTraversable #-}
{-|

Module defining e-nodes ('ENode'), the e-node function symbol ('Operator'), and
mappings from e-nodes ('NodeMap').

-}
module Data.Equality.Graph.Nodes where

import Data.Functor.Classes
import Data.Foldable
import Data.Bifunctor

import Data.Kind

import Control.Monad (void)

import qualified Data.Map.Strict as M

import Data.Equality.Graph.Classes.Id


-- * E-node

-- | An e-node is a function symbol paired with a list of children e-classes.
-- 
-- We define an e-node to be the base functor of some recursive data type
-- parametrized over 'ClassId', i.e. all recursive fields are rather e-class ids.
newtype ENode l = Node { forall (l :: * -> *). ENode l -> l ClassId
unNode :: l ClassId }

-- | Get the children e-class ids of an e-node
children :: Traversable l => ENode l -> [ClassId]
children :: forall (l :: * -> *). Traversable l => ENode l -> [ClassId]
children = forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (l :: * -> *). ENode l -> l ClassId
unNode
{-# INLINE children #-}

-- * Operator

-- | An operator is solely the function symbol part of the e-node. Basically,
-- this means children e-classes are ignored.
newtype Operator l = Operator { forall (l :: * -> *). Operator l -> l ()
unOperator :: l () }

-- | Get the operator (function symbol) of an e-node
operator :: Traversable l => ENode l -> Operator l
operator :: forall (l :: * -> *). Traversable l => ENode l -> Operator l
operator = forall (l :: * -> *). l () -> Operator l
Operator forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Functor f => f a -> f ()
void forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (l :: * -> *). ENode l -> l ClassId
unNode
{-# INLINE operator #-}

instance Eq1 l => (Eq (ENode l)) where
    == :: ENode l -> ENode l -> Bool
(==) (Node l ClassId
a) (Node l ClassId
b) = forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq forall a. Eq a => a -> a -> Bool
(==) l ClassId
a l ClassId
b
    {-# INLINE (==) #-}

instance Ord1 l => (Ord (ENode l)) where
    compare :: ENode l -> ENode l -> Ordering
compare (Node l ClassId
a) (Node l ClassId
b) = forall (f :: * -> *) a b.
Ord1 f =>
(a -> b -> Ordering) -> f a -> f b -> Ordering
liftCompare forall a. Ord a => a -> a -> Ordering
compare l ClassId
a l ClassId
b
    {-# INLINE compare #-}

instance Show1 l => (Show (ENode l)) where
    showsPrec :: ClassId -> ENode l -> ShowS
showsPrec ClassId
p (Node l ClassId
l) = forall (f :: * -> *) a.
Show1 f =>
(ClassId -> a -> ShowS)
-> ([a] -> ShowS) -> ClassId -> f a -> ShowS
liftShowsPrec forall a. Show a => ClassId -> a -> ShowS
showsPrec forall a. Show a => [a] -> ShowS
showList ClassId
p l ClassId
l

instance Eq1 l => (Eq (Operator l)) where
    == :: Operator l -> Operator l -> Bool
(==) (Operator l ()
a) (Operator l ()
b) = forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq (\()
_ ()
_ -> Bool
True) l ()
a l ()
b
    {-# INLINE (==) #-}

instance Ord1 l => (Ord (Operator l)) where
    compare :: Operator l -> Operator l -> Ordering
compare (Operator l ()
a) (Operator l ()
b) = forall (f :: * -> *) a b.
Ord1 f =>
(a -> b -> Ordering) -> f a -> f b -> Ordering
liftCompare (\()
_ ()
_ -> Ordering
EQ) l ()
a l ()
b
    {-# INLINE compare #-}

instance Show1 l => (Show (Operator l)) where
    showsPrec :: ClassId -> Operator l -> ShowS
showsPrec ClassId
p (Operator l ()
l) = forall (f :: * -> *) a.
Show1 f =>
(ClassId -> a -> ShowS)
-> ([a] -> ShowS) -> ClassId -> f a -> ShowS
liftShowsPrec (forall a b. a -> b -> a
const forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"") (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"") ClassId
p l ()
l

-- * Node Map

-- | A mapping from e-nodes of @l@ to @a@
newtype NodeMap (l :: Type -> Type) a = NodeMap { forall (l :: * -> *) a. NodeMap l a -> Map (ENode l) a
unNodeMap :: M.Map (ENode l) a }
-- TODO: Investigate whether it would be worth it requiring a trie-map for the
-- e-node definition. Probably it isn't better since e-nodes aren't recursive.
  deriving (ClassId -> NodeMap l a -> ShowS
forall a.
(ClassId -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
forall (l :: * -> *) a.
(Show1 l, Show a) =>
ClassId -> NodeMap l a -> ShowS
forall (l :: * -> *) a. (Show1 l, Show a) => [NodeMap l a] -> ShowS
forall (l :: * -> *) a. (Show1 l, Show a) => NodeMap l a -> String
showList :: [NodeMap l a] -> ShowS
$cshowList :: forall (l :: * -> *) a. (Show1 l, Show a) => [NodeMap l a] -> ShowS
show :: NodeMap l a -> String
$cshow :: forall (l :: * -> *) a. (Show1 l, Show a) => NodeMap l a -> String
showsPrec :: ClassId -> NodeMap l a -> ShowS
$cshowsPrec :: forall (l :: * -> *) a.
(Show1 l, Show a) =>
ClassId -> NodeMap l a -> ShowS
Show, forall a b. a -> NodeMap l b -> NodeMap l a
forall a b. (a -> b) -> NodeMap l a -> NodeMap l b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (l :: * -> *) a b. a -> NodeMap l b -> NodeMap l a
forall (l :: * -> *) a b. (a -> b) -> NodeMap l a -> NodeMap l b
<$ :: forall a b. a -> NodeMap l b -> NodeMap l a
$c<$ :: forall (l :: * -> *) a b. a -> NodeMap l b -> NodeMap l a
fmap :: forall a b. (a -> b) -> NodeMap l a -> NodeMap l b
$cfmap :: forall (l :: * -> *) a b. (a -> b) -> NodeMap l a -> NodeMap l b
Functor, forall a. Eq a => a -> NodeMap l a -> Bool
forall a. Num a => NodeMap l a -> a
forall a. Ord a => NodeMap l a -> a
forall m. Monoid m => NodeMap l m -> m
forall a. NodeMap l a -> Bool
forall a. NodeMap l a -> ClassId
forall a. NodeMap l a -> [a]
forall a. (a -> a -> a) -> NodeMap l a -> a
forall m a. Monoid m => (a -> m) -> NodeMap l a -> m
forall b a. (b -> a -> b) -> b -> NodeMap l a -> b
forall a b. (a -> b -> b) -> b -> NodeMap l a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> ClassId)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
forall (l :: * -> *) a. Eq a => a -> NodeMap l a -> Bool
forall (l :: * -> *) a. Num a => NodeMap l a -> a
forall (l :: * -> *) a. Ord a => NodeMap l a -> a
forall (l :: * -> *) m. Monoid m => NodeMap l m -> m
forall (l :: * -> *) a. NodeMap l a -> Bool
forall (l :: * -> *) a. NodeMap l a -> ClassId
forall (l :: * -> *) a. NodeMap l a -> [a]
forall (l :: * -> *) a. (a -> a -> a) -> NodeMap l a -> a
forall (l :: * -> *) m a. Monoid m => (a -> m) -> NodeMap l a -> m
forall (l :: * -> *) b a. (b -> a -> b) -> b -> NodeMap l a -> b
forall (l :: * -> *) a b. (a -> b -> b) -> b -> NodeMap l a -> b
product :: forall a. Num a => NodeMap l a -> a
$cproduct :: forall (l :: * -> *) a. Num a => NodeMap l a -> a
sum :: forall a. Num a => NodeMap l a -> a
$csum :: forall (l :: * -> *) a. Num a => NodeMap l a -> a
minimum :: forall a. Ord a => NodeMap l a -> a
$cminimum :: forall (l :: * -> *) a. Ord a => NodeMap l a -> a
maximum :: forall a. Ord a => NodeMap l a -> a
$cmaximum :: forall (l :: * -> *) a. Ord a => NodeMap l a -> a
elem :: forall a. Eq a => a -> NodeMap l a -> Bool
$celem :: forall (l :: * -> *) a. Eq a => a -> NodeMap l a -> Bool
length :: forall a. NodeMap l a -> ClassId
$clength :: forall (l :: * -> *) a. NodeMap l a -> ClassId
null :: forall a. NodeMap l a -> Bool
$cnull :: forall (l :: * -> *) a. NodeMap l a -> Bool
toList :: forall a. NodeMap l a -> [a]
$ctoList :: forall (l :: * -> *) a. NodeMap l a -> [a]
foldl1 :: forall a. (a -> a -> a) -> NodeMap l a -> a
$cfoldl1 :: forall (l :: * -> *) a. (a -> a -> a) -> NodeMap l a -> a
foldr1 :: forall a. (a -> a -> a) -> NodeMap l a -> a
$cfoldr1 :: forall (l :: * -> *) a. (a -> a -> a) -> NodeMap l a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> NodeMap l a -> b
$cfoldl' :: forall (l :: * -> *) b a. (b -> a -> b) -> b -> NodeMap l a -> b
foldl :: forall b a. (b -> a -> b) -> b -> NodeMap l a -> b
$cfoldl :: forall (l :: * -> *) b a. (b -> a -> b) -> b -> NodeMap l a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> NodeMap l a -> b
$cfoldr' :: forall (l :: * -> *) a b. (a -> b -> b) -> b -> NodeMap l a -> b
foldr :: forall a b. (a -> b -> b) -> b -> NodeMap l a -> b
$cfoldr :: forall (l :: * -> *) a b. (a -> b -> b) -> b -> NodeMap l a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> NodeMap l a -> m
$cfoldMap' :: forall (l :: * -> *) m a. Monoid m => (a -> m) -> NodeMap l a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> NodeMap l a -> m
$cfoldMap :: forall (l :: * -> *) m a. Monoid m => (a -> m) -> NodeMap l a -> m
fold :: forall m. Monoid m => NodeMap l m -> m
$cfold :: forall (l :: * -> *) m. Monoid m => NodeMap l m -> m
Foldable, forall (l :: * -> *). Functor (NodeMap l)
forall (l :: * -> *). Foldable (NodeMap l)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NodeMap l a -> f (NodeMap l b)
forall (l :: * -> *) (m :: * -> *) a.
Monad m =>
NodeMap l (m a) -> m (NodeMap l a)
forall (l :: * -> *) (f :: * -> *) a.
Applicative f =>
NodeMap l (f a) -> f (NodeMap l a)
forall (l :: * -> *) (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NodeMap l a -> m (NodeMap l b)
forall (l :: * -> *) (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NodeMap l a -> f (NodeMap l b)
sequence :: forall (m :: * -> *) a.
Monad m =>
NodeMap l (m a) -> m (NodeMap l a)
$csequence :: forall (l :: * -> *) (m :: * -> *) a.
Monad m =>
NodeMap l (m a) -> m (NodeMap l a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NodeMap l a -> m (NodeMap l b)
$cmapM :: forall (l :: * -> *) (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NodeMap l a -> m (NodeMap l b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
NodeMap l (f a) -> f (NodeMap l a)
$csequenceA :: forall (l :: * -> *) (f :: * -> *) a.
Applicative f =>
NodeMap l (f a) -> f (NodeMap l a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NodeMap l a -> f (NodeMap l b)
$ctraverse :: forall (l :: * -> *) (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NodeMap l a -> f (NodeMap l b)
Traversable, NonEmpty (NodeMap l a) -> NodeMap l a
NodeMap l a -> NodeMap l a -> NodeMap l a
forall b. Integral b => b -> NodeMap l a -> NodeMap l a
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall (l :: * -> *) a.
Ord1 l =>
NonEmpty (NodeMap l a) -> NodeMap l a
forall (l :: * -> *) a.
Ord1 l =>
NodeMap l a -> NodeMap l a -> NodeMap l a
forall (l :: * -> *) a b.
(Ord1 l, Integral b) =>
b -> NodeMap l a -> NodeMap l a
stimes :: forall b. Integral b => b -> NodeMap l a -> NodeMap l a
$cstimes :: forall (l :: * -> *) a b.
(Ord1 l, Integral b) =>
b -> NodeMap l a -> NodeMap l a
sconcat :: NonEmpty (NodeMap l a) -> NodeMap l a
$csconcat :: forall (l :: * -> *) a.
Ord1 l =>
NonEmpty (NodeMap l a) -> NodeMap l a
<> :: NodeMap l a -> NodeMap l a -> NodeMap l a
$c<> :: forall (l :: * -> *) a.
Ord1 l =>
NodeMap l a -> NodeMap l a -> NodeMap l a
Semigroup, NodeMap l a
[NodeMap l a] -> NodeMap l a
NodeMap l a -> NodeMap l a -> NodeMap l a
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall (l :: * -> *) a. Ord1 l => Semigroup (NodeMap l a)
forall (l :: * -> *) a. Ord1 l => NodeMap l a
forall (l :: * -> *) a. Ord1 l => [NodeMap l a] -> NodeMap l a
forall (l :: * -> *) a.
Ord1 l =>
NodeMap l a -> NodeMap l a -> NodeMap l a
mconcat :: [NodeMap l a] -> NodeMap l a
$cmconcat :: forall (l :: * -> *) a. Ord1 l => [NodeMap l a] -> NodeMap l a
mappend :: NodeMap l a -> NodeMap l a -> NodeMap l a
$cmappend :: forall (l :: * -> *) a.
Ord1 l =>
NodeMap l a -> NodeMap l a -> NodeMap l a
mempty :: NodeMap l a
$cmempty :: forall (l :: * -> *) a. Ord1 l => NodeMap l a
Monoid)

-- | Insert a value given an e-node in a 'NodeMap'
insertNM :: Ord1 l => ENode l -> a -> NodeMap l a -> NodeMap l a
insertNM :: forall (l :: * -> *) a.
Ord1 l =>
ENode l -> a -> NodeMap l a -> NodeMap l a
insertNM ENode l
e a
v (NodeMap Map (ENode l) a
m) = forall (l :: * -> *) a. Map (ENode l) a -> NodeMap l a
NodeMap (forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert ENode l
e a
v Map (ENode l) a
m)
{-# INLINE insertNM #-}

-- | Lookup an e-node in a 'NodeMap'
lookupNM :: Ord1 l => ENode l -> NodeMap l a -> Maybe a
lookupNM :: forall (l :: * -> *) a. Ord1 l => ENode l -> NodeMap l a -> Maybe a
lookupNM ENode l
e = forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup ENode l
e forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (l :: * -> *) a. NodeMap l a -> Map (ENode l) a
unNodeMap
{-# INLINE lookupNM #-}

-- | Delete an e-node in a 'NodeMap'
deleteNM :: Ord1 l => ENode l -> NodeMap l a -> NodeMap l a
deleteNM :: forall (l :: * -> *) a.
Ord1 l =>
ENode l -> NodeMap l a -> NodeMap l a
deleteNM ENode l
e (NodeMap Map (ENode l) a
m) = forall (l :: * -> *) a. Map (ENode l) a -> NodeMap l a
NodeMap (forall k a. Ord k => k -> Map k a -> Map k a
M.delete ENode l
e Map (ENode l) a
m)
{-# INLINE deleteNM #-}

-- | Insert a value and lookup by e-node in a 'NodeMap'
insertLookupNM :: Ord1 l => ENode l -> a -> NodeMap l a -> (Maybe a, NodeMap l a)
insertLookupNM :: forall (l :: * -> *) a.
Ord1 l =>
ENode l -> a -> NodeMap l a -> (Maybe a, NodeMap l a)
insertLookupNM ENode l
e a
v (NodeMap Map (ENode l) a
m) = forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second forall (l :: * -> *) a. Map (ENode l) a -> NodeMap l a
NodeMap forall a b. (a -> b) -> a -> b
$ forall k a.
Ord k =>
(k -> a -> a -> a) -> k -> a -> Map k a -> (Maybe a, Map k a)
M.insertLookupWithKey (\ENode l
_ a
a a
_ -> a
a) ENode l
e a
v Map (ENode l) a
m
{-# INLINE insertLookupNM #-}

-- | As 'Data.Map.foldlWithKeyNM'' but in a 'NodeMap'
foldlWithKeyNM' :: Ord1 l => (b -> ENode l -> a -> b) -> b -> NodeMap l a -> b 
foldlWithKeyNM' :: forall (l :: * -> *) b a.
Ord1 l =>
(b -> ENode l -> a -> b) -> b -> NodeMap l a -> b
foldlWithKeyNM' b -> ENode l -> a -> b
f b
b = forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
M.foldlWithKey' b -> ENode l -> a -> b
f b
b forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (l :: * -> *) a. NodeMap l a -> Map (ENode l) a
unNodeMap
{-# INLINE foldlWithKeyNM' #-}

-- | As 'Data.Map.foldrWithKeyNM'' but in a 'NodeMap'
foldrWithKeyNM' :: Ord1 l => (ENode l -> a -> b -> b) -> b -> NodeMap l a -> b 
foldrWithKeyNM' :: forall (l :: * -> *) a b.
Ord1 l =>
(ENode l -> a -> b -> b) -> b -> NodeMap l a -> b
foldrWithKeyNM' ENode l -> a -> b -> b
f b
b = forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
M.foldrWithKey' ENode l -> a -> b -> b
f b
b forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (l :: * -> *) a. NodeMap l a -> Map (ENode l) a
unNodeMap
{-# INLINE foldrWithKeyNM' #-}

-- | Get the number of entries in a 'NodeMap'.
--
-- This operation takes constant time (__O(1)__)
sizeNM :: NodeMap l a -> Int
sizeNM :: forall (l :: * -> *) a. NodeMap l a -> ClassId
sizeNM = forall k a. Map k a -> ClassId
M.size forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (l :: * -> *) a. NodeMap l a -> Map (ENode l) a
unNodeMap
{-# INLINE sizeNM #-}

-- | As 'Data.Map.traverseWithKeyNM' but in a 'NodeMap'
traverseWithKeyNM :: Applicative t => (ENode l -> a -> t b) -> NodeMap l a -> t (NodeMap l b) 
traverseWithKeyNM :: forall (t :: * -> *) (l :: * -> *) a b.
Applicative t =>
(ENode l -> a -> t b) -> NodeMap l a -> t (NodeMap l b)
traverseWithKeyNM ENode l -> a -> t b
f (NodeMap Map (ENode l) a
m) = forall (l :: * -> *) a. Map (ENode l) a -> NodeMap l a
NodeMap forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) k a b.
Applicative t =>
(k -> a -> t b) -> Map k a -> t (Map k b)
M.traverseWithKey ENode l -> a -> t b
f Map (ENode l) a
m
{-# INLINE traverseWithKeyNM #-}

-- Node Set

-- newtype NodeSet l a = NodeSet { unNodeSet :: IM.IntMap (a, ENode l) }
--   deriving (Semigroup, Monoid)

-- insertNS :: Hashable1 l => ENode l -> NodeSet l -> NodeSet l
-- insertNS v = NodeSet . IM.insert (hashNode v) v . unNodeSet