Language.Nominal.Examples.Graph

A development file to build on Andrey Mokhov's algebraic-graphs library. THIS FILE IS UNDER DEVELOPMENT Connect should be implemented such that only free vertices are connected; not bound ones. Overlay should be capture-avoiding (which should be automatic).

Documentation

data Graph a

A datatype of graphs with binding. Perhaps should parameterise over atom type (see KAtom). For now, I use the default atom type Tom.

Constructors

Empty

Vertex a

Overlay (Graph a) (Graph a)

Connect (Graph a) (Graph a)

Restrict (Nom (Graph a))

Instances

Swappable a => KRestrict Tom (Graph a)

Restriction action just passes the restriction on to the deep embedding

Defined in Language.Nominal.Examples.Graph

Methods

restrict :: [KAtom Tom] -> Graph a -> Graph a

Show a => Show (Graph a)

Defined in Language.Nominal.Examples.Graph

Methods

showsPrec :: Int -> Graph a -> ShowS

show :: Graph a -> String

showList :: [Graph a] -> ShowS

Generic (Graph a)

Defined in Language.Nominal.Examples.Graph

Associated Types

type Rep (Graph a) :: Type -> Type

Methods

from :: Graph a -> Rep (Graph a) x

to :: Rep (Graph a) x -> Graph a

Swappable a => Swappable (Graph a)

Defined in Language.Nominal.Examples.Graph

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Graph a -> Graph a

type Rep (Graph a)

Defined in Language.Nominal.Examples.Graph

type Rep (Graph a) = D1 (MetaData "Graph" "Language.Nominal.Examples.Graph" "nom-0.1.0.2-Cei0dwnsIrWHLKrPA11A4S" False) ((C1 (MetaCons "Empty" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Vertex" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a))) :+: (C1 (MetaCons "Overlay" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Graph a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Graph a))) :+: (C1 (MetaCons "Connect" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Graph a)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Graph a))) :+: C1 (MetaCons "Restrict" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Nom (Graph a)))))))

foldg :: b -> (a -> b) -> (b -> b -> b) -> (b -> b -> b) -> (Nom b -> b) -> Graph a -> b

Fold on graphs with binding. Just like fold on graphs, but with an extra restriction operation, which we go under in a capture-avoiding manner.

filterApart :: Support a => [Atom] -> [a] -> [a]

Filter a list of vertices to obtain those vertices for which atms :: [KAtom] is fresh