Copyright	(c) Murdoch J. Gabbay 2020
License	GPL-3
Maintainer	murdoch.gabbay@gmail.com
Stability	experimental
Portability	POSIX
Safe Haskell	None
Language	Haskell2010

Language.Nominal.Examples.Graph

Description

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).

Synopsis

data Graph a
- = Empty
- | Vertex a
- | Overlay (Graph a) (Graph a)
- | Connect (Graph a) (Graph a)
- | Restrict (Nom (Graph a))
foldg :: b -> (a -> b) -> (b -> b -> b) -> (b -> b -> b) -> (Nom b -> b) -> Graph a -> b
filterApart :: Support a => [Atom] -> [a] -> [a]

Documentation

data Graph a Source #

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) Source #	Restriction action just passes the restriction on to the deep embedding
Instance details Defined in Language.Nominal.Examples.Graph Methods restrict :: [KAtom Tom] -> Graph a -> Graph a Source #
Show a => Show (Graph a) Source #
Instance details Defined in Language.Nominal.Examples.Graph Methods showsPrec :: Int -> Graph a -> ShowS # show :: Graph a -> String # showList :: [Graph a] -> ShowS #
Generic (Graph a) Source #
Instance details 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) Source #
Instance details Defined in Language.Nominal.Examples.Graph Methods kswp :: Typeable s => KAtom s -> KAtom s -> Graph a -> Graph a Source #
type Rep (Graph a) Source #
Instance details 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 Source #

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] Source #

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