module Data.Graph.DAG.Edge.Utils where
import Data.Graph.DAG.Edge
import GHC.TypeLits
import Data.Singletons.TH
import Data.Singletons.Prelude
import Data.Proxy
$(singletons [d|
data Tree a = Node a [Tree a] deriving (Show, Eq)
|])
reflect ::
forall (a :: k).
(SingI a, SingKind ('KProxy :: KProxy k)) =>
Proxy a -> Demote a
reflect _ = fromSing (sing :: Sing a)
type family AppendIfNotElemTrees (c :: k) (trees :: [Tree k]) :: [Tree k] where
AppendIfNotElemTrees c ((Node c xs) ': xss) = (Node c xs) ': xss
AppendIfNotElemTrees c ((Node x xs) ': xss) = (Node x xs) ':
(AppendIfNotElemTrees c xss)
AppendIfNotElemTrees c '[] = (Node c '[]) ': '[]
type family AddChildTo (test :: k)
(child :: k)
(trees :: [Tree k]) :: [Tree k] where
AddChildTo t c ((Node t xs) ': xss) =
(Node t (AppendIfNotElemTrees c xs)) ': (AddChildTo t c xss)
AddChildTo t c ((Node x xs) ': xss) =
(Node x (AddChildTo t c xs)) ': (AddChildTo t c xss)
AddChildTo t c '[] = '[]
type family AddEdge' (edge :: EdgeKind)
(trees :: [Tree Symbol])
(hasFromRoot :: Bool)
(hasToRoot :: Bool):: [Tree Symbol] where
AddEdge' ('EdgeType from to) '[] 'False 'False =
(Node from ((Node to '[]) ': '[])) ': (Node to '[]) ': '[]
AddEdge' ('EdgeType from to) '[] 'True 'False =
(Node to '[]) ': '[]
AddEdge' ('EdgeType from to) '[] 'False 'True =
(Node from ((Node to '[]) ': '[])) ': '[]
AddEdge' x '[] 'True 'True = '[]
AddEdge' ('EdgeType from to) ((Node from xs) ': xss) hasFromRoot hasToRoot =
(Node from (AppendIfNotElemTrees to xs)) ':
(AddEdge' ('EdgeType from to) xss 'True hasToRoot)
AddEdge' ('EdgeType from to) ((Node to xs) ': xss) hasFromRoot hasToRoot =
(Node to (AddEdge' ('EdgeType from to) xs 'True 'True)) ':
(AddEdge' ('EdgeType from to) xss hasFromRoot 'True)
AddEdge' ('EdgeType from to) ((Node x xs) ': xss) hasFromRoot hasToRoot =
(Node x (AddEdge' ('EdgeType from to) xs 'True 'True)) ':
(AddEdge' ('EdgeType from to) xss hasFromRoot hasToRoot)
type family AddEdge (edge :: EdgeKind)
(trees :: [Tree Symbol]) :: [Tree Symbol] where
AddEdge a trees = AddEdge' a trees 'False 'False
type family SpanningTrees' (edges :: [EdgeKind])
(acc :: [Tree Symbol]) :: [Tree Symbol] where
SpanningTrees' '[] trees = trees
SpanningTrees' (('EdgeType from to) ': es) trees =
SpanningTrees' es (AddEdge ('EdgeType from to) trees)
type family SpanningTrees (edges :: [EdgeKind]) :: [Tree Symbol] where
SpanningTrees edges = SpanningTrees' edges '[]
getSpanningTrees :: EdgeSchema es x unique -> Proxy (SpanningTrees es)
getSpanningTrees _ = Proxy