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])] )
(keyFoundYet :: 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 ) keyFoundYet =
'(key, (PrependIfElem from to vs)) ':
(DisallowIn ('EdgeType from to) es keyFoundYet)
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