{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Data.Conic.Graph where

import qualified Data.Vinyl as V
import Data.Vinyl.Functor
import Fcf
import Fcf.Data.Graph
import Fcf.Data.Vinyl

data RGraph :: (u -> *) -> Graph u -> * where
  REmpty :: RGraph f 'Empty
  RVertex :: !(f r) -> RGraph f ('Vertex r)
  ROverlay :: !(RGraph f xs) -> !(RGraph f ys) -> RGraph f ('Overlay xs ys)
  RConnect :: !(RGraph f xs) -> !(RGraph f ys) -> RGraph f ('Connect xs ys)

instance Eq (RGraph f 'Empty) where
  RGraph f 'Empty
_ == :: RGraph f 'Empty -> RGraph f 'Empty -> Bool
== RGraph f 'Empty
_ = Bool
True

instance Eq (f r) => Eq (RGraph f ('Vertex r)) where
  RVertex f r
x == :: RGraph f ('Vertex r) -> RGraph f ('Vertex r) -> Bool
== RVertex f r
y = f r
x f r -> f r -> Bool
forall a. Eq a => a -> a -> Bool
== f r
f r
y

instance (Eq (RGraph f x), Eq (RGraph f y)) => Eq (RGraph f ('Overlay x y)) where
  ROverlay RGraph f xs
x RGraph f ys
y == :: RGraph f ('Overlay x y) -> RGraph f ('Overlay x y) -> Bool
== ROverlay RGraph f xs
x' RGraph f ys
y' = RGraph f xs
x RGraph f xs -> RGraph f xs -> Bool
forall a. Eq a => a -> a -> Bool
== RGraph f xs
RGraph f xs
x' Bool -> Bool -> Bool
&& RGraph f ys
y RGraph f ys -> RGraph f ys -> Bool
forall a. Eq a => a -> a -> Bool
== RGraph f ys
RGraph f ys
y'

instance (Eq (RGraph f x), Eq (RGraph f y)) => Eq (RGraph f ('Connect x y)) where
  RConnect RGraph f xs
x RGraph f ys
y == :: RGraph f ('Connect x y) -> RGraph f ('Connect x y) -> Bool
== RConnect RGraph f xs
x' RGraph f ys
y' = RGraph f xs
x RGraph f xs -> RGraph f xs -> Bool
forall a. Eq a => a -> a -> Bool
== RGraph f xs
RGraph f xs
x' Bool -> Bool -> Bool
&& RGraph f ys
y RGraph f ys -> RGraph f ys -> Bool
forall a. Eq a => a -> a -> Bool
== RGraph f ys
RGraph f ys
y'

edge :: f a -> f b -> RGraph f (Eval (Edge a b))
edge :: f a -> f b -> RGraph f (Eval (Edge a b))
edge f a
x f b
y = RGraph f ('Vertex a)
-> RGraph f ('Vertex b)
-> RGraph f ('Connect ('Vertex a) ('Vertex b))
forall a (f :: a -> *) (xs :: Graph a) (ys :: Graph a).
RGraph f xs -> RGraph f ys -> RGraph f ('Connect xs ys)
RConnect (f a -> RGraph f ('Vertex a)
forall a (f :: a -> *) (r :: a). f r -> RGraph f ('Vertex r)
RVertex f a
x) (f b -> RGraph f ('Vertex b)
forall a (f :: a -> *) (r :: a). f r -> RGraph f ('Vertex r)
RVertex f b
y)

data VertexList :: Graph a -> Exp [a]

type instance Eval (VertexList 'Empty) = '[]

type instance Eval (VertexList ('Vertex x)) = '[x]

type instance Eval (VertexList ('Overlay x y)) = Eval (LiftM2 (++) (VertexList x) (VertexList y))

type instance Eval (VertexList ('Connect x y)) = Eval (LiftM2 (++) (VertexList x) (VertexList y))

vertexList :: RGraph f xs -> V.Rec f (Eval (VertexList xs))
vertexList :: RGraph f xs -> Rec f (Eval (VertexList xs))
vertexList RGraph f xs
REmpty = Rec f (Eval (VertexList xs))
forall u (a :: u -> *). Rec a '[]
V.RNil
vertexList (RVertex f r
x) = f r
x f r -> Rec f '[] -> Rec f '[r]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
V.:& Rec f '[]
forall u (a :: u -> *). Rec a '[]
V.RNil
vertexList (ROverlay RGraph f xs
x RGraph f ys
y) = Rec f (Eval (VertexList xs))
-> Rec f (Eval (VertexList ys))
-> Rec f (Eval (Eval (VertexList xs) ++ Eval (VertexList ys)))
forall a (f :: a -> *) (as :: [a]) (bs :: [a]).
Rec f as -> Rec f bs -> Rec f (Eval (as ++ bs))
rappend (RGraph f xs -> Rec f (Eval (VertexList xs))
forall a (f :: a -> *) (xs :: Graph a).
RGraph f xs -> Rec f (Eval (VertexList xs))
vertexList RGraph f xs
x) (RGraph f ys -> Rec f (Eval (VertexList ys))
forall a (f :: a -> *) (xs :: Graph a).
RGraph f xs -> Rec f (Eval (VertexList xs))
vertexList RGraph f ys
y)
vertexList (RConnect RGraph f xs
x RGraph f ys
y) = Rec f (Eval (VertexList xs))
-> Rec f (Eval (VertexList ys))
-> Rec f (Eval (Eval (VertexList xs) ++ Eval (VertexList ys)))
forall a (f :: a -> *) (as :: [a]) (bs :: [a]).
Rec f as -> Rec f bs -> Rec f (Eval (as ++ bs))
rappend (RGraph f xs -> Rec f (Eval (VertexList xs))
forall a (f :: a -> *) (xs :: Graph a).
RGraph f xs -> Rec f (Eval (VertexList xs))
vertexList RGraph f xs
x) (RGraph f ys -> Rec f (Eval (VertexList ys))
forall a (f :: a -> *) (xs :: Graph a).
RGraph f xs -> Rec f (Eval (VertexList xs))
vertexList RGraph f ys
y)

rmap :: (forall x. f x -> g x) -> RGraph f rs -> RGraph g rs
rmap :: (forall (x :: u). f x -> g x) -> RGraph f rs -> RGraph g rs
rmap forall (x :: u). f x -> g x
f RGraph f rs
REmpty = RGraph g rs
forall u (f :: u -> *). RGraph f 'Empty
REmpty
rmap forall (x :: u). f x -> g x
f (RVertex f r
x) = g r -> RGraph g ('Vertex r)
forall a (f :: a -> *) (r :: a). f r -> RGraph f ('Vertex r)
RVertex (f r -> g r
forall (x :: u). f x -> g x
f f r
x)
rmap forall (x :: u). f x -> g x
f (ROverlay RGraph f xs
x RGraph f ys
y) = RGraph g xs -> RGraph g ys -> RGraph g ('Overlay xs ys)
forall a (f :: a -> *) (xs :: Graph a) (ys :: Graph a).
RGraph f xs -> RGraph f ys -> RGraph f ('Overlay xs ys)
ROverlay ((forall (x :: u). f x -> g x) -> RGraph f xs -> RGraph g xs
forall u (f :: u -> *) (g :: u -> *) (rs :: Graph u).
(forall (x :: u). f x -> g x) -> RGraph f rs -> RGraph g rs
rmap forall (x :: u). f x -> g x
f RGraph f xs
x) ((forall (x :: u). f x -> g x) -> RGraph f ys -> RGraph g ys
forall u (f :: u -> *) (g :: u -> *) (rs :: Graph u).
(forall (x :: u). f x -> g x) -> RGraph f rs -> RGraph g rs
rmap forall (x :: u). f x -> g x
f RGraph f ys
y)
rmap forall (x :: u). f x -> g x
f (RConnect RGraph f xs
x RGraph f ys
y) = RGraph g xs -> RGraph g ys -> RGraph g ('Connect xs ys)
forall a (f :: a -> *) (xs :: Graph a) (ys :: Graph a).
RGraph f xs -> RGraph f ys -> RGraph f ('Connect xs ys)
RConnect ((forall (x :: u). f x -> g x) -> RGraph f xs -> RGraph g xs
forall u (f :: u -> *) (g :: u -> *) (rs :: Graph u).
(forall (x :: u). f x -> g x) -> RGraph f rs -> RGraph g rs
rmap forall (x :: u). f x -> g x
f RGraph f xs
x) ((forall (x :: u). f x -> g x) -> RGraph f ys -> RGraph g ys
forall u (f :: u -> *) (g :: u -> *) (rs :: Graph u).
(forall (x :: u). f x -> g x) -> RGraph f rs -> RGraph g rs
rmap forall (x :: u). f x -> g x
f RGraph f ys
y)

rtraverse :: Applicative h => (forall x. f x -> h (g x)) -> RGraph f rs -> h (RGraph g rs)
rtraverse :: (forall (x :: u). f x -> h (g x)) -> RGraph f rs -> h (RGraph g rs)
rtraverse forall (x :: u). f x -> h (g x)
f RGraph f rs
REmpty = RGraph g 'Empty -> h (RGraph g 'Empty)
forall (f :: * -> *) a. Applicative f => a -> f a
pure RGraph g 'Empty
forall u (f :: u -> *). RGraph f 'Empty
REmpty
rtraverse forall (x :: u). f x -> h (g x)
f (RVertex f r
x) = g r -> RGraph g ('Vertex r)
forall a (f :: a -> *) (r :: a). f r -> RGraph f ('Vertex r)
RVertex (g r -> RGraph g ('Vertex r))
-> h (g r) -> h (RGraph g ('Vertex r))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f r -> h (g r)
forall (x :: u). f x -> h (g x)
f f r
x
rtraverse forall (x :: u). f x -> h (g x)
f (ROverlay RGraph f xs
x RGraph f ys
y) = RGraph g xs -> RGraph g ys -> RGraph g ('Overlay xs ys)
forall a (f :: a -> *) (xs :: Graph a) (ys :: Graph a).
RGraph f xs -> RGraph f ys -> RGraph f ('Overlay xs ys)
ROverlay (RGraph g xs -> RGraph g ys -> RGraph g ('Overlay xs ys))
-> h (RGraph g xs) -> h (RGraph g ys -> RGraph g ('Overlay xs ys))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: u). f x -> h (g x)) -> RGraph f xs -> h (RGraph g xs)
forall u (h :: * -> *) (f :: u -> *) (g :: u -> *) (rs :: Graph u).
Applicative h =>
(forall (x :: u). f x -> h (g x)) -> RGraph f rs -> h (RGraph g rs)
rtraverse forall (x :: u). f x -> h (g x)
f RGraph f xs
x h (RGraph g ys -> RGraph g ('Overlay xs ys))
-> h (RGraph g ys) -> h (RGraph g ('Overlay xs ys))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (x :: u). f x -> h (g x)) -> RGraph f ys -> h (RGraph g ys)
forall u (h :: * -> *) (f :: u -> *) (g :: u -> *) (rs :: Graph u).
Applicative h =>
(forall (x :: u). f x -> h (g x)) -> RGraph f rs -> h (RGraph g rs)
rtraverse forall (x :: u). f x -> h (g x)
f RGraph f ys
y
rtraverse forall (x :: u). f x -> h (g x)
f (RConnect RGraph f xs
x RGraph f ys
y) = RGraph g xs -> RGraph g ys -> RGraph g ('Connect xs ys)
forall a (f :: a -> *) (xs :: Graph a) (ys :: Graph a).
RGraph f xs -> RGraph f ys -> RGraph f ('Connect xs ys)
RConnect (RGraph g xs -> RGraph g ys -> RGraph g ('Connect xs ys))
-> h (RGraph g xs) -> h (RGraph g ys -> RGraph g ('Connect xs ys))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: u). f x -> h (g x)) -> RGraph f xs -> h (RGraph g xs)
forall u (h :: * -> *) (f :: u -> *) (g :: u -> *) (rs :: Graph u).
Applicative h =>
(forall (x :: u). f x -> h (g x)) -> RGraph f rs -> h (RGraph g rs)
rtraverse forall (x :: u). f x -> h (g x)
f RGraph f xs
x h (RGraph g ys -> RGraph g ('Connect xs ys))
-> h (RGraph g ys) -> h (RGraph g ('Connect xs ys))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (x :: u). f x -> h (g x)) -> RGraph f ys -> h (RGraph g ys)
forall u (h :: * -> *) (f :: u -> *) (g :: u -> *) (rs :: Graph u).
Applicative h =>
(forall (x :: u). f x -> h (g x)) -> RGraph f rs -> h (RGraph g rs)
rtraverse forall (x :: u). f x -> h (g x)
f RGraph f ys
y

rapply :: RGraph (Lift (->) f g) xs -> RGraph f xs -> RGraph g xs
rapply :: RGraph (Lift (->) f g) xs -> RGraph f xs -> RGraph g xs
rapply RGraph (Lift (->) f g) xs
_ RGraph f xs
REmpty = RGraph g xs
forall u (f :: u -> *). RGraph f 'Empty
REmpty
rapply (RVertex Lift (->) f g r
f) (RVertex f r
x) = g r -> RGraph g ('Vertex r)
forall a (f :: a -> *) (r :: a). f r -> RGraph f ('Vertex r)
RVertex (Lift (->) f g r -> f r -> g r
forall l l' (op :: l -> l' -> *) k (f :: k -> l) (g :: k -> l')
       (x :: k).
Lift op f g x -> op (f x) (g x)
getLift Lift (->) f g r
f f r
x)
rapply (ROverlay RGraph (Lift (->) f g) xs
f RGraph (Lift (->) f g) ys
g) (ROverlay RGraph f xs
x RGraph f ys
y) = RGraph g xs -> RGraph g ys -> RGraph g ('Overlay xs ys)
forall a (f :: a -> *) (xs :: Graph a) (ys :: Graph a).
RGraph f xs -> RGraph f ys -> RGraph f ('Overlay xs ys)
ROverlay (RGraph (Lift (->) f g) xs -> RGraph f xs -> RGraph g xs
forall u (f :: u -> *) (g :: u -> *) (xs :: Graph u).
RGraph (Lift (->) f g) xs -> RGraph f xs -> RGraph g xs
rapply RGraph (Lift (->) f g) xs
f RGraph f xs
RGraph f xs
x) (RGraph (Lift (->) f g) ys -> RGraph f ys -> RGraph g ys
forall u (f :: u -> *) (g :: u -> *) (xs :: Graph u).
RGraph (Lift (->) f g) xs -> RGraph f xs -> RGraph g xs
rapply RGraph (Lift (->) f g) ys
g RGraph f ys
RGraph f ys
y)
rapply (RConnect RGraph (Lift (->) f g) xs
f RGraph (Lift (->) f g) ys
g) (RConnect RGraph f xs
x RGraph f ys
y) = RGraph g xs -> RGraph g ys -> RGraph g ('Connect xs ys)
forall a (f :: a -> *) (xs :: Graph a) (ys :: Graph a).
RGraph f xs -> RGraph f ys -> RGraph f ('Connect xs ys)
RConnect (RGraph (Lift (->) f g) xs -> RGraph f xs -> RGraph g xs
forall u (f :: u -> *) (g :: u -> *) (xs :: Graph u).
RGraph (Lift (->) f g) xs -> RGraph f xs -> RGraph g xs
rapply RGraph (Lift (->) f g) xs
f RGraph f xs
RGraph f xs
x) (RGraph (Lift (->) f g) ys -> RGraph f ys -> RGraph g ys
forall u (f :: u -> *) (g :: u -> *) (xs :: Graph u).
RGraph (Lift (->) f g) xs -> RGraph f xs -> RGraph g xs
rapply RGraph (Lift (->) f g) ys
g RGraph f ys
RGraph f ys
y)

rzipWith :: (forall x. f x -> g x -> h x) -> RGraph f xs -> RGraph g xs -> RGraph h xs
rzipWith :: (forall (x :: u). f x -> g x -> h x)
-> RGraph f xs -> RGraph g xs -> RGraph h xs
rzipWith forall (x :: u). f x -> g x -> h x
f = RGraph (Lift (->) g h) xs -> RGraph g xs -> RGraph h xs
forall u (f :: u -> *) (g :: u -> *) (xs :: Graph u).
RGraph (Lift (->) f g) xs -> RGraph f xs -> RGraph g xs
rapply (RGraph (Lift (->) g h) xs -> RGraph g xs -> RGraph h xs)
-> (RGraph f xs -> RGraph (Lift (->) g h) xs)
-> RGraph f xs
-> RGraph g xs
-> RGraph h xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (x :: u). f x -> Lift (->) g h x)
-> RGraph f xs -> RGraph (Lift (->) g h) xs
forall u (f :: u -> *) (g :: u -> *) (rs :: Graph u).
(forall (x :: u). f x -> g x) -> RGraph f rs -> RGraph g rs
rmap ((g x -> h x) -> Lift (->) g h x
forall l l' k (op :: l -> l' -> *) (f :: k -> l) (g :: k -> l')
       (x :: k).
op (f x) (g x) -> Lift op f g x
Lift ((g x -> h x) -> Lift (->) g h x)
-> (f x -> g x -> h x) -> f x -> Lift (->) g h x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> g x -> h x
forall (x :: u). f x -> g x -> h x
f)