Module Bigraph.Link

Operations on link graphs.

type edg

The type of edges.

val pp_edg : Ppx_deriving_runtime.Format.formatter -> edg -> Ppx_deriving_runtime.unit
val show_edg : edg -> Ppx_deriving_runtime.string
val edg_to_yojson : edg -> Yojson.Safe.t
val edg_of_yojson : Yojson.Safe.t -> edg Ppx_deriving_yojson_runtime.error_or
val edge_inner : edg -> Face.t

The inner face of an edge.

val edge_outer : edg -> Face.t

The outer face of an edge.

val edge_ports : edg -> Ports.t

The port multiset of an edge. Ports are tracked as a multiset: each occurrence of a link name in the edge counts separately, so multiplicities matter for pattern matching.

val edge_compare : edg -> edg -> int

Total order on edges by inner face, outer face, and then port multiset; 0 exactly when the two edges are structurally equal, that is, when struct_equal holds.

val struct_equal : edg -> edg -> bool

struct_equal e1 e2 is true when the two edges have the same inner face, outer face, and port multiset.

type t

The type of link graphs -- a multiset of edges.

val pp : Ppx_deriving_runtime.Format.formatter -> t -> Ppx_deriving_runtime.unit
val show : t -> Ppx_deriving_runtime.string
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or

Multiset operations for link graphs.

val empty : t

The empty link graph.

val is_empty : t -> bool

Return true if the link graph is empty.

val add : edg -> t -> t

Add an edge to a link graph.

val singleton : edg -> t

Create a link graph with a single edge.

val union : t -> t -> t

Compute the union of two link graphs.

val equal : t -> t -> bool

Test equality of two link graphs.

val iter : (edg -> unit) -> t -> unit

Iterate over the edges of a link graph.

val fold : (edg -> 'a -> 'a) -> t -> 'a -> 'a

Fold over the edges of a link graph, in elements order.

val for_all : (edg -> bool) -> t -> bool

Test if all edges satisfy a predicate.

val exists : (edg -> bool) -> t -> bool

Test if any edge satisfies a predicate.

val filter : (edg -> bool) -> t -> t

Keep only edges that satisfy a predicate.

val cardinal : t -> int

Return the number of edges.

val elements : t -> edg list

Return the list of edges, sorted ascending by edge_compare with structurally-equal edges in insertion order. The position of an edge in this list is its index in the SAT closed-edge encoding and in the SBC edge generators, so the order is part of the observable behaviour.

val to_dot : t -> string * string * string * string

to_dot l computes a four-elements tuple encoding the dot representation of link graph l. The first two elements represent inner and outer names shape declarations. The third element represent the hyperedges shape declarations. The fourth element specifies the adjacency matrix.

val inner : t -> Face.t

inner l computes the inner face of link graph l.

val outer : t -> Face.t

outer l computes the outer face of link graph l.

val apply : Iso.t -> t -> t

apply i l computes a link graph obtained by applying isomorphism i to l.

val elementary_sub : inner:Face.t -> outer:Face.t -> t

elementary_sub inner outer computes a substitution consisting of a single edge in which inner and outer are the inner and outer face, respectively.

val elementary_ion : Face.t -> t

elementary_ion f computes an elementary ion with outer face f.

val elementary_id : Face.t -> t

elementary_id f computes the identity over face f, that is, one edge for each name in f.

val id_empty : t

id_empty is the empty link graph.

exception NAMES_ALREADY_DEFINED of Face.t * Face.t

Raised when the tensor product between two incompatible link graphs cannot be performed. The first element is the set of inner common names while the second is the set of outer common names.

exception FACES_MISMATCH of Face.t * Face.t

Raised when a composition between two incompatible link graphs cannot be performed.

val tens : t -> t -> int -> t

tens a b n computes the tensor product of link graphs a and b. Argument n is the number of nodes of a.

val ppar : t -> t -> int -> t

ppar a b n computes the parallel composition of link graphs a and b. n is the number of nodes of a.

val comp : t -> t -> int -> t

comp a b n computes the composition of link graphs a and b. Argument n is the number of nodes of a.

Predicates

val is_id : t -> bool

is_id l is true if link graph l is an identity, false otherwise.

val is_mono : t -> bool

is_mono l is true if link graph l is monomorphic, false otherwise. A link graph is monomorphic if every edge has at most one inner name.

val is_epi : t -> bool

is_epi l is true if link graph l is epimorphic, false otherwise. A link graph is epimorphic if no outer name is idle.

val is_ground : t -> bool

is_ground l is true if link graph l has no inner names, false otherwise.

val is_guard : t -> bool

is_guard l is true if no edges in link graph l have both inner and outer names, false otherwise.

val max_ports : t -> int

Compute the maximum number of ports in one edge of a link graph.

val closed_edges : t -> int

Compute the number of closed edges.

val filter_iso : (edg -> bool) -> t -> t * Iso.t

filter_iso p l filters link graph l keeping only the edges satisfying predicate p. The computed isomorphism maps edge indices of the filtered link graph to indices of edges in l.

val closed_edges_iso : t -> t * Iso.t

closed_edges_iso l computes the closed edges of link graph l. The computed isomorphism maps edge indices of the new link graph to indices of edges in l.

Decompositions

val norm : t -> t * t

Normalise link graph l as follows: l = omega o l' where omega is a linking and l' is the same as l but with all links open.

val decomp : target:t -> pattern:t -> i_e:Iso.t -> i_c:Iso.t -> i_d:Iso.t -> Fun.t -> t * t * t

decomp target pattern i_e i_c i_d f_e computes the decomposition of target given pattern, iso i_e, and isos from nodes in t to nodes of c and d, respectively. Argument f_e is a total function from links in the pattern to links in the target. Pattern p is assumed epi and mono and i_e is from edges in p to edges in t. Isos i_c and i_d are obtained by Place.decomp. The results are link graph c, d and id.

val prime_components : t -> Iso.t list -> t list

Compute the prime components of a link graph. See Place.decomp.