module Data.Graph.DAG.Edge where
import Data.Constraint
import GHC.TypeLits
import Data.Proxy
data EdgeValue (from :: Symbol) (to :: Symbol) = Edge
data EdgeKind = forall from to. EdgeType from to
type family Deducible (x :: Bool) :: Constraint where
Deducible 'True = ()
type family Excluding (x :: k) (xs :: Maybe [k]) :: Constraint where
Excluding a ('Just '[]) = Deducible 'True
Excluding a 'Nothing = Deducible 'True
Excluding a ('Just (a ': ts)) = Deducible 'False
Excluding a ('Just (b ': ts)) = Excluding a ('Just ts)
type family Lookup (index :: k) ( map :: [(k, k2)] ) :: Maybe k2 where
Lookup a ( '( a, v) ': xs ) = 'Just v
Lookup a (b ': xs) = Lookup a xs
Lookup a '[] = 'Nothing
type family (x :: k1) =/= (y :: k2) :: Constraint where
a =/= a = Deducible 'False
a =/= b = Deducible 'True
class Acceptable (a :: EdgeKind)
( oldLoops :: [(Symbol, [Symbol])] )
(unique :: Bool) where
instance ( Excluding from (Lookup to excludeMap)
, from =/= to ) =>
Acceptable ('EdgeType from to) excludeMap 'False where
instance ( Excluding from (Lookup to excludeMap)
, Excluding to (Lookup from excludeMap)
, from =/= to ) =>
Acceptable ('EdgeType from to) excludeMap 'True where
type family PrependIfElem (test :: k) (a :: k) (xs :: [k]) :: [k] where
PrependIfElem t a (t ': xs) = a ': t ': xs
PrependIfElem t a (u ': xs) = u ': (PrependIfElem t a xs)
PrependIfElem t a '[] = '[]
type family DisallowIn
(new :: EdgeKind)
( oldLoops :: [(Symbol, [Symbol])] )
(keyFound :: Bool) :: [(Symbol, [Symbol])] where
DisallowIn ('EdgeType from to) ( '(from, xs) ': es) 'False =
'(from, (to ': xs)) ':
(DisallowIn ('EdgeType from to) es 'True)
DisallowIn ('EdgeType from to) ( '(key, vs) ': es ) keyFound =
'(key, (PrependIfElem from to vs)) ':
(DisallowIn ('EdgeType from to) es keyFound)
DisallowIn a '[] 'True = '[]
DisallowIn ('EdgeType from to) '[] 'False = ('(from, (to ': '[])) ': '[])
data EdgeSchema (edges :: [EdgeKind])
(nearLoops :: [(Symbol, [Symbol])])
(unique :: Bool) where
ENil :: EdgeSchema '[] '[] unique
ECons :: ( Acceptable b oldLoops unique
, EdgeValue from to ~ a
, EdgeType from to ~ b
, DisallowIn b oldLoops 'False ~ c
) => !a
-> EdgeSchema old oldLoops unique
-> EdgeSchema (b ': old) c unique
unique :: EdgeSchema '[] '[] 'True
unique = ENil
notUnique :: EdgeSchema '[] '[] 'False
notUnique = ENil
data Tree a = Node a [Tree 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