{-# 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)