Safe Haskell	None
Language	Haskell2010

Data.Graph.DAG.Edge

Synopsis

Documentation

data EdgeValue from to Source

We use promoted symbol values for the from and to type parameters. This is the user-level data type when declaring the list of edges.

Constructors

Edge

data EdgeKind Source

We need this for type-level computation list.

Constructors

forall from to . EdgeType from to

type family Deducible x :: Constraint Source

Some people just want to watch the world burn. Ideally, this shouldn't exist; poor error messages, and is very square peg - round hole.

Equations

Deducible True = ()

type family Excluding x xs :: Constraint Source

not . elem for lists of types, resulting in a constraint.

Equations

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 map :: Maybe k2 Source

A simple Data.List.lookup function for type maps.

Equations

Lookup a (`(a, v)` : xs) = Just v
Lookup a (b : xs) = Lookup a xs
Lookup a [] = Nothing

type family x =/= y :: Constraint Source

Trivial inequality for non-reflexivity of edges

Equations

a =/= a = Deducible False
a =/= b = Deducible True

class Acceptable a oldLoops unique Source

Simply reject anything that's been reached in the other direction. We expect an explicit type signature when uniqueness is needed, otherwise we will wait until invocation to see if the edges are unique.

Instances

(Excluding Symbol from (Lookup [Symbol] Symbol to excludeMap), Excluding Symbol to (Lookup [Symbol] Symbol from excludeMap), (=/=) Symbol Symbol from to) => Acceptable (EdgeType Symbol Symbol from to) excludeMap True
(Excluding Symbol from (Lookup [Symbol] Symbol to excludeMap), (=/=) Symbol Symbol from to) => Acceptable (EdgeType Symbol Symbol from to) excludeMap False

type family PrependIfElem test a xs :: [k] Source

Add an explicit element to the head of a list, if the test is inside that list.

Equations

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 oldLoops keyFound :: [(Symbol, [Symbol])] Source

Update the exclusion map with the new edge: the from key gets to added, likewise with keys that have from in it's value list. We need to track if the key exists yet.

Equations

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 nearLoops unique where Source

edges is a list of types with kind EdgeKind, while nearLoops is a map of the nodes transitively reachable by each node.

Constructors

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 Source

Utility for constructing an EdgeSchema granularly

notUnique :: EdgeSchema [] [] False Source

data Tree a Source

Trivial rose tree for creating spanning trees

Constructors

Node a [Tree a]

type family AppendIfNotElemTrees c trees :: [Tree k] Source

Adds an empty c tree to the list of trees uniquely

Equations

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 child trees :: [Tree k] Source

Adds c as a child of any tree with a root t. Assumes unique roots.

Equations

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 trees hasFromRoot hasToRoot :: [Tree Symbol] Source

We need to track if from has is a root node or not. TODO: Some code repeat.

Equations

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 trees :: [Tree Symbol] Source

Add to as a child to every from node in the accumulator.

Equations

AddEdge a trees = AddEdge' a trees False False

type family SpanningTrees' edges acc :: [Tree Symbol] Source

Auxilliary function normally defined in a where clause for manual folding.

Equations

SpanningTrees' [] trees = trees
SpanningTrees' (EdgeType from to : es) trees = SpanningTrees' es (AddEdge (EdgeType from to) trees)

type family SpanningTrees edges :: [Tree Symbol] Source

Expects edges to already be type-safe

Equations

SpanningTrees edges = SpanningTrees' edges []

getSpanningTrees :: EdgeSchema es x unique -> Proxy (SpanningTrees es) Source