{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Fcf.Data.Graph where

import Fcf hiding (Map)
import qualified Fcf.Data.AdjacencyMap as AM
import Fcf.Data.Nat
import qualified Fcf.Data.Set as S

data Graph a where
  Empty :: Graph a
  Vertex :: a -> Graph a
  Overlay :: Graph a -> Graph a -> Graph a
  Connect :: Graph a -> Graph a -> Graph a

-- | Empty
--
-- === __Example__
--
-- >>> :kind! (Eval Empty :: Graph Nat)
-- (Eval Empty :: Graph Nat) :: Graph Nat
-- = 'Empty
data Empty :: Exp (Graph a)

type instance Eval Empty = 'Empty

-- | Vertex
--
-- === __Example__
--
-- >>> :kind! (Eval (Vertex 1) :: Graph Nat)
-- (Eval (Vertex 1) :: Graph Nat) :: Graph Nat
-- = 'Vertex 1
data Vertex :: a -> Exp (Graph a)

type instance Eval (Vertex a) = 'Vertex a

-- | Edge
--
-- === __Example__
--
-- >>> :kind! (Eval (Edge 1 2) :: Graph Nat)
-- (Eval (Edge 1 2) :: Graph Nat) :: Graph Nat
-- = 'Connect ('Vertex 1) ('Vertex 2)
data Edge :: a -> a -> Exp (Graph a)

type instance Eval (Edge x y) = 'Connect ('Vertex x) ('Vertex y)

-- | Overlay
--
-- === __Example__
--
-- >>> :kind! (Eval (Overlay ('Vertex 1) ('Vertex 2)) :: Graph Nat)
-- (Eval (Overlay ('Vertex 1) ('Vertex 2)) :: Graph Nat) :: Graph Nat
-- = 'Overlay ('Vertex 1) ('Vertex 2)
data Overlay :: Graph a -> Graph a -> Exp (Graph a)

type instance Eval (Overlay x y) = 'Overlay x y

-- | Connect
--
-- === __Example__
--
-- >>> :kind! (Eval (Connect ('Vertex 1) ('Vertex 2)) :: Graph Nat)
-- (Eval (Connect ('Vertex 1) ('Vertex 2)) :: Graph Nat) :: Graph Nat
-- = 'Connect ('Vertex 1) ('Vertex 2)
data Connect :: Graph a -> Graph a -> Exp (Graph a)

type instance Eval (Connect x y) = 'Connect x y

-- | Map
--
-- === __Example__
--
-- >>> :kind! Eval (Map ((+) 1) =<< Connect ('Overlay ('Vertex 1) ('Vertex 2)) ('Vertex 3))
-- Eval (Map ((+) 1) =<< Connect ('Overlay ('Vertex 1) ('Vertex 2)) ('Vertex 3)) :: Graph
--                                                                                    Nat
-- = 'Connect ('Overlay ('Vertex 2) ('Vertex 3)) ('Vertex 4)
data Map :: (a -> Exp b) -> Graph a -> Exp (Graph b)

type instance Eval (Map _ 'Empty) = 'Empty

type instance Eval (Map f ('Vertex a)) = 'Vertex (Eval (f $ a))

type instance Eval (Map f ('Overlay x y)) = 'Overlay (Eval (Map f x)) (Eval (Map f y))

type instance Eval (Map f ('Connect x y)) = 'Connect (Eval (Map f x)) (Eval (Map f y))

-- | Foldg
--
-- === __Example__
--
-- >>> :kind! Eval (FoldG (Pure 0) Pure (+) (+) =<< Connect ('Overlay ('Vertex 1) ('Vertex 2)) ('Vertex 3))
-- Eval (FoldG (Pure 0) Pure (+) (+) =<< Connect ('Overlay ('Vertex 1) ('Vertex 2)) ('Vertex 3)) :: Nat
-- = 6
data FoldG :: Exp b -> (a -> Exp b) -> (b -> b -> Exp b) -> (b -> b -> Exp b) -> Graph a -> Exp b

type instance Eval (FoldG e _ _ _ 'Empty) = Eval e

type instance Eval (FoldG _ v _ _ ('Vertex x)) = Eval (v x)

type instance Eval (FoldG e v o c ('Overlay x y)) = Eval (o (Eval (FoldG e v o c x)) (Eval (FoldG e v o c y)))

type instance Eval (FoldG e v o c ('Connect x y)) = Eval (c (Eval (FoldG e v o c x)) (Eval (FoldG e v o c y)))

-- | ToAdjacencyMap
--
-- === __Example__
-- >>> :kind! Eval (ToAdjacencyMap (Eval (Edge 1 2)))
-- Eval (ToAdjacencyMap (Eval (Edge 1 2))) :: AM.AdjacencyMap Nat
-- = 'AM.AM
--     ('Fcf.Data.MapC.MapC '[ '(1, 'S.Set '[2]), '(2, 'S.Set '[])])
data ToAdjacencyMap :: Graph a -> Exp (AM.AdjacencyMap a)

type instance Eval (ToAdjacencyMap x) = Eval (FoldG AM.Empty AM.Vertex AM.Overlay AM.Connect x)

-- | EqR
--
-- === __Example__
-- >>> :kind! Eval (EqR (Eval (Edge 1 3)) (Eval (Edge 1 2)))
-- Eval (EqR (Eval (Edge 1 3)) (Eval (Edge 1 2))) :: Bool
-- = 'False
data EqR :: Graph a -> Graph a -> Exp Bool

type instance Eval (EqR x y) = Eval (TyEq (Eval (ToAdjacencyMap x)) (Eval (ToAdjacencyMap y)))

-- | Size
--
-- === __Example__
--
-- >>> :kind! Eval (Size =<< Connect ('Overlay ('Vertex 1) ('Vertex 2)) ('Vertex 3))
-- Eval (Size =<< Connect ('Overlay ('Vertex 1) ('Vertex 2)) ('Vertex 3)) :: Nat
-- = 3
data Size :: Graph a -> Exp Nat

type instance Eval (Size g) = Eval (FoldG (Pure 1) (ConstFn 1) (+) (+) g)

-- | HasVertex
--
-- === __Example__
--
-- >>> :kind! Eval (HasVertex 3 =<< Connect ('Overlay ('Vertex 1) ('Vertex 2)) ('Vertex 3))
-- Eval (HasVertex 3 =<< Connect ('Overlay ('Vertex 1) ('Vertex 2)) ('Vertex 3)) :: Bool
-- = 'True
data HasVertex :: a -> Graph a -> Exp Bool

type instance Eval (HasVertex x g) = Eval (FoldG (Pure 'False) (TyEq x) (||) (||) g)

-- | VertexSet
--
-- === __Example__
--
-- >>> :kind! Eval (VertexSet =<< Connect ('Overlay ('Vertex 1) ('Vertex 2)) ('Vertex 3))
-- Eval (VertexSet =<< Connect ('Overlay ('Vertex 1) ('Vertex 2)) ('Vertex 3)) :: S.Set
--                                                                                  Nat
-- = 'S.Set '[3, 2, 1]
data VertexSet :: Graph a -> Exp (S.Set a)

type instance Eval (VertexSet g) = Eval (FoldG S.Empty S.Singleton S.Union S.Union g)

-- | Simplify
--
-- === __Example__
--
-- >>> :kind! Eval (Simplify =<< Overlay ('Vertex 1) ('Overlay ('Vertex 2) ('Vertex 1)))
-- Eval (Simplify =<< Overlay ('Vertex 1) ('Overlay ('Vertex 2) ('Vertex 1))) :: Graph
--                                                                                 Nat
-- = 'Overlay ('Vertex 2) ('Vertex 1)
data Simplify :: Graph a -> Exp (Graph a)

type instance Eval (Simplify x) = Eval (FoldG Empty Vertex (Simple Overlay) (Simple Connect) x)

data Simple :: (Graph a -> Graph a -> Exp (Graph a)) -> Graph a -> Graph a -> Exp (Graph a)

type instance Eval (Simple f x y) = Eval (Simple' x y (Eval (f x y)))

data Simple' :: Graph a -> Graph a -> Graph a -> Exp (Graph a)

type instance
  Eval (Simple' x y z) =
    If (Eval (EqR x z)) x (If (Eval (EqR y z)) y z)