Module Link

module Link: sig .. end
This module provides operations on link graphs.
Author(s): Michele Sevegnani


Faces


type name = 
| Nam of string
The type of names.
module Face: sig .. end
This module provides set operations for faces.

Ports


module Ports: sig .. end
This module implements multisets of nodes as maps.

Link graphs


type edg = {
   i : Face.t; (*
Inner face
*)
   o : Face.t; (*
Outer face
*)
   p : int Ports.t; (*
Set of ports
*)
}
The type of edges.
module Lg: sig .. end
This module provides set operations for link graphs.
val parse_face : string list -> Face.t
parse_face ns computes a face starting from list of string names ns.
val string_of_face : Face.t -> string
string_of_face f computes the string representation of face f.
val to_string : Lg.t -> string
to_string l computes the string representation of link graph l.
val json_of_link : Lg.t -> string
Return a JSON representation of a link graph. Example:

"link_graph": [
       {
         "inner": [
           {
             "name""x"
           },
           {
             "name""y"
           }
         ],
         "outer": [
           {
             "name""z"
           }
         ],
         "ports": [
           {
             "node_id": 1,
             "port_arity": 2
           },
           {
             "node_id": 2,
             "port_arity": 1
           }
         ]
       },
       {
         "inner": [],
         "outer": [
           {
             "name""n"
           }
         ],
         "ports": [
           {
             "node_id": 1,
             "port_arity": 2
           }
         ]
       }
     ]

val json_of_link_f : Lg.t -> Base.JSON.json_node
val parse : string list -> Lg.t
Parse a list of strings.
val get_dot : Lg.t -> string * string * string * string
get_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 : Lg.t -> Face.t
inner l computes the inner face of link graph l.
val outer : Lg.t -> Face.t
outer l computes the outer face of link graph l.
val apply_exn : int Iso.t -> Lg.t -> Lg.t
apply_exn i l computes a link graph obtained by applying isomorphism i to l.
Raises Not_found when a node is not defined in the iso.

Elementary link graphs


val elementary_sub : inner:Face.t -> outer:Face.t -> Lg.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 -> Lg.t
elementary_ion f computes an elementary ion with outer face f.
val elementary_id : Face.t -> Lg.t
elementary_id f computes the identity over face f, i.e. one edge for each name in f.
val id_empty : Lg.t
id_empty is the empty link graph.
val arities : Lg.t -> int Base.M_int.t

Operations on link graphs


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 : Lg.t -> Lg.t -> int -> Lg.t
tens a b n computes the tensor product of link graphs a and b. Argument n is the number of nodes of a.
Raises NAMES_ALREADY_DEFINED when there are shared names.
val ppar : Lg.t -> Lg.t -> int -> Lg.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 : Lg.t -> Lg.t -> int -> Lg.t
comp a b n computes the composition of link graphs a and b. Argument n is the number of nodes of a.
Raises FACES_MISMATCH when names in the mediating interfaces differ.

Predicates


val is_id : Lg.t -> bool
is_id l is true if link graph l is an identity, false otherwise.
val is_mono : Lg.t -> bool
is_mono l is true if link graph l is monomorphic, false otherwise.
val is_epi : Lg.t -> bool
is_epi l is true if link graph l is epimorphic, false otherwise.
val is_ground : Lg.t -> bool
is_ground l is true if link graph l has no inner names, false otherwise.
val is_guard : Lg.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 : Lg.t -> int
Compute the maximum number of ports in one edge of a link graph.
val cardinal_ports : Lg.t -> int list
Compute a sorted list with the cardinalities of the port sets.
val closed_edges : Lg.t -> int
Compute the number of closed edges.
val closed_edges_iso : Lg.t -> Lg.t * int Iso.t
closed_edges_iso l computes the set of 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 : Lg.t -> Lg.t * Lg.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:Lg.t ->
pattern:Lg.t ->
i_e:int Iso.t ->
i_c:int Iso.t ->
i_d:int Iso.t -> int Fun.t -> Lg.t * Lg.t * Lg.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 : Lg.t -> int Iso.t list -> Lg.t list
Compute the prime components of a link graph. See Place.decomp.

Matching constraints


exception NOT_TOTAL
val match_edges : target:Lg.t ->
pattern:Lg.t ->
n_t:Nodes.t -> n_p:Nodes.t -> Cnf.clause list * IntSet.t * Cnf.clause list
Compute constraints to match closed edges in the pattern to closed edges in the target. Controls are checked to exclude incompatible pairs. The output is a list of clauses a set of blocked columns and a set of blocking pairs.
Raises NOT_TOTAL when no matches are found.
val match_ports : target:Lg.t ->
pattern:Lg.t ->
n_t:Nodes.t -> n_p:Nodes.t -> Cnf.clause list -> Cnf.clause list list
Compute constraints to match isomorphic port sets in closed edges.
val match_peers : target:Lg.t ->
pattern:Lg.t ->
n_t:Nodes.t ->
n_p:Nodes.t ->
int * int * Cnf.clause list list * (int * int) list * Cnf.clause list *
int Iso.t * int Iso.t
Compute constraints to match peers in the pattern with peers in the target. Auxiliary variables are introduced to handle matches with open edges.
Raises NOT_TOTAL when no matches are found.
val match_list_eq : Lg.t ->
Lg.t -> Nodes.t -> Nodes.t -> Cnf.clause list * Cnf.clause list
Similar to Link.match_edges but constraints are for equality.
val match_ports_eq : Lg.t ->
Lg.t -> Nodes.t -> Nodes.t -> Cnf.clause list -> Cnf.clause list list
Similar to Link.match_ports but constraints are for equality.