{-# LANGUAGE UndecidableInstances #-} -- tmp show
{-# LANGUAGE FlexibleContexts #-}
{-# OPTIONS_HADDOCK hide #-}
{-|
 Non-abstract definition of e-graphs
 -}
module Data.Equality.Graph.Internal where

import Data.Equality.Graph.ReprUnionFind
import Data.Equality.Graph.Classes
import Data.Equality.Graph.Nodes

-- | E-graph representing terms of language @l@.
--
-- Intuitively, an e-graph is a set of equivalence classes (e-classes). Each e-class is a
-- set of e-nodes representing equivalent terms from a given language, and an e-node is a function
-- symbol paired with a list of children e-classes.
data EGraph analysis language = EGraph
    { forall analysis (language :: * -> *).
EGraph analysis language -> ReprUnionFind
unionFind :: !ReprUnionFind              -- ^ Union find like structure to find canonical representation of an e-class id
    , forall analysis (language :: * -> *).
EGraph analysis language -> ClassIdMap (EClass analysis language)
classes   :: !(ClassIdMap (EClass analysis language)) -- ^ Map canonical e-class ids to their e-classes
    , forall analysis (language :: * -> *).
EGraph analysis language -> Memo language
memo      :: !(Memo language)            -- ^ Hashcons maps all canonical e-nodes to their e-class ids
    , forall analysis (language :: * -> *).
EGraph analysis language -> Worklist language
worklist  :: !(Worklist language)        -- ^ Worklist of e-class ids that need to be upward merged
    , forall analysis (language :: * -> *).
EGraph analysis language -> Worklist language
analysisWorklist :: !(Worklist language) -- ^ Like 'worklist' but for analysis repairing
    }

-- | The hashcons 𝐻  is a map from e-nodes to e-class ids
type Memo l = NodeMap l ClassId

-- | Maintained worklist of e-class ids that need to be “upward merged”
type Worklist l = [(ClassId, ENode l)]

instance (Show a, Show (l ClassId)) => Show (EGraph a l) where
    show :: EGraph a l -> String
show (EGraph ReprUnionFind
a ClassIdMap (EClass a l)
b Memo l
c Worklist l
d Worklist l
e) =
        String
"UnionFind: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ReprUnionFind -> String
forall a. Show a => a -> String
show ReprUnionFind
a String -> ShowS
forall a. Semigroup a => a -> a -> a
<>
            String
"\n\nE-Classes: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ClassIdMap (EClass a l) -> String
forall a. Show a => a -> String
show ClassIdMap (EClass a l)
b String -> ShowS
forall a. Semigroup a => a -> a -> a
<>
                String
"\n\nHashcons: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Memo l -> String
forall a. Show a => a -> String
show Memo l
c String -> ShowS
forall a. Semigroup a => a -> a -> a
<>
                    String
"\n\nWorklist: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Worklist l -> String
forall a. Show a => a -> String
show Worklist l
d String -> ShowS
forall a. Semigroup a => a -> a -> a
<>
                        String
"\n\nAnalWorklist: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Worklist l -> String
forall a. Show a => a -> String
show Worklist l
e