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

    , Empty
    , IsEmpty

    , Match
    )
    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

-- 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

-- Match
type Match node g = Match' (M.Lookup node g) node 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 g
    = Decomp (Just (Context (M.Delete node p)
                            node
                            label
                            (M.Delete node s)))
             (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