{-# LANGUAGE
  EmptyDataDecls,
  TypeFamilies,
  TypeOperators,
  UndecidableInstances
  #-}
module Types.Data.Graph.Dijkstra
    ( Dijkstra
    , SpTree
    , SpLength
    , Sp
    )
    where

import qualified Types.Data.Heap     as H
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.Graph
import Types.Data.Graph.RootPath
import Types.Data.Maybe
import Types.Data.Num

-- Expand
type family   Expand distance lPath context
type instance Expand d (LPath p) (Context ps n l ss)
    = L.Map (Expand' d p) (M.Assocs ss)

data Expand' distance path
type instance L.App (Expand' d p) (L.Cons n d')
    = H.Unit (d :+: d')
             (LPath (L.Cons (LNode n (d :+: d')) p))

-- Dijkstra
type Dijkstra h g
    = If (H.IsEmpty h :||: IsEmpty g)
         L.Null
         (Dijkstra' h g (H.SplitMin h))

type family   Dijkstra' heap graph min
type instance Dijkstra' h g (L.Cons d (L.Cons (LPath (L.Cons (LNode n d') ps)) h'))
    = Dijkstra'' n d' (LPath (L.Cons (LNode n d) ps)) h' (Match n g)

type family   Dijkstra'' node distance lPath heap' decomp
type instance Dijkstra'' n d p h' (Decomp Nothing  g') = Dijkstra h' g'
type instance Dijkstra'' n d p h' (Decomp (Just c) g')
    = L.Cons p (Dijkstra (H.MergeAll (L.Cons h' (Expand d p c))) g')

-- SpTree
type SpTree node graph
    = Dijkstra (H.Unit D0 (LPath (L.Cons (LNode node D0) L.Null))) graph

-- SpLength
type SpLength node1 node2 graph
    = GetDistance node2 (SpTree node1 graph)

-- Sp
type Sp node1 node2 graph
    = GetLPathNodes node2 (SpTree node1 graph)



test :: SpTree D2 (InsNode (LNode D1 False)
                          (InsNode (LNode D0 True) Empty))
test = undefined