{-# LANGUAGE
  EmptyDataDecls,
  TypeFamilies,
  UndecidableInstances
  #-}
module Types.Data.Graph
    ( -- * Type Constructors
      Context
    , Decomp
    , LNode
    , LEdge
    , LPath
    , Graph

      -- * Operations
      -- ** Graph inspection
    , IsEmpty
    , Match

      -- ** Graph construction
    , Empty
    , Merge
    , InsNode
    , InsEdge
    )
    where

import qualified Types.Data.List     as L
import qualified Types.Data.List.Ops as L
import qualified Types.Data.Map      as M

import Types.Data.Bool
import Types.Data.Maybe


-- preNodes, sucNodes: map from node ID to edge label
data Context preNodes nodeID nodeLabel sucNodes

-- nodeMap: map from node ID to context
data Graph nodeMap

-- mContext: Maybe Context
data Decomp mContext graph

-- nodeID: natural number
data LNode nodeID nodeLabel

--
data LEdge nodeID1 nodeID2 edgeLabel

-- lNodes: list of LNode
data LPath lNodes

-- Empty
type Empty = Graph M.Empty

-- IsEmpty
type family   IsEmpty g
type instance IsEmpty (Graph m) = M.Null m

-- Merge
type family   Merge context g
type instance Merge (Context ps n l ss) (Graph g)
    = Graph (AddPred (AddSucc (M.Insert n (Context ps n l ss) g) n ps) n ss)

-- InsNode
type family   InsNode lNode g
type instance InsNode (LNode n l) g
    = Merge (Context M.Empty n l M.Empty) g

-- InsEdge
type family   InsEdge lEdge g
type instance InsEdge (LEdge n1 n2 l) g
    = InsEdge' n1 n2 l (Match n1 g)

type family   InsEdge' n1 n2 l decomp
type instance InsEdge' n1 n2 l (Decomp (Just (Context ps n' l' ss)) g')
    = Merge (Context ps n1 l' (M.Insert n2 l ss)) g'

-- AddSucc
type AddSucc g n ps = M.FoldlWithKey (AddSucc' n) g ps

data AddSucc' n
type instance L.App3 (AddSucc' n) g p l
    = M.Adjust (AddSucc'' n l) p g

data AddSucc'' n l
type instance L.App (AddSucc'' n l) (Context ps n' l' ss)
    = Context ps n' l' (M.Insert n l ss)

-- AddPred
type AddPred g n ss = M.FoldlWithKey (AddPred' n) g ss

data AddPred' n
type instance L.App3 (AddPred' n) g s l
    = M.Adjust (AddPred'' n l) s g

data AddPred'' n l
type instance L.App (AddPred'' n l) (Context ps n' l' ss)
    = Context (M.Insert n l ss) n' l' ss

-- Match
type family   Match node g
type instance Match node (Graph g) = Match' (M.Lookup node g) node (Graph g)

type family   Match' mContext node g
type instance Match' Nothing                          node g = Decomp Nothing g
type instance Match' (Just (Context p node' label s)) node (Graph g)
    = Decomp (Just (Context (M.Delete node p)
                            node
                            label
                            (M.Delete node s)))
             (Graph (ClearSucc (ClearPred (M.Delete node g)
                                          node
                                          (M.Keys (M.Delete node s)))
                               node
                               (M.Keys (M.Delete node p))))

-- ClearSucc
type family   ClearSucc g n ns
type instance ClearSucc g n L.Null        = g
type instance ClearSucc g n (L.Cons s ss)
    = ClearSucc (M.Adjust (ClearSucc' n) s g) n ss

data ClearSucc' n
type instance L.App (ClearSucc' n) (Context ps n' l ss)
    = Context ps n' l (M.Delete n ss)

-- ClearPred
type family   ClearPred g n ns
type instance ClearPred g n L.Null        = g
type instance ClearPred g n (L.Cons p ps)
    = ClearPred (M.Adjust (ClearPred' n) p g) n ps

data ClearPred' n
type instance L.App (ClearPred' n) (Context ps n' l ss)
    = Context (M.Delete n ps) n' l ss