Module AcyclicGraph.Make

Parameters

Signature

type t
val empty : t
val check_invariants : required_canonical:(Point.t -> bool) -> t -> unit
exception AlreadyDeclared
val add : ?⁠rank:int -> Point.t -> t -> t

All points must be pre-declared through this function before they can be mentioned in the others. NB: use a large rank to keep the node canonical

exception Undeclared of Point.t
val check_declared : t -> Point.Set.t -> unit
raises Undeclared

if one of the points is not present in the graph.

type 'a check_function = t -> 'a -> 'a -> bool
val check_eq : Point.t check_function
val check_leq : Point.t check_function
val check_lt : Point.t check_function
val enforce_eq : Point.t -> Point.t -> t -> t
val enforce_leq : Point.t -> Point.t -> t -> t
val enforce_lt : Point.t -> Point.t -> t -> t
val constraints_of : t -> Point.Constraint.t * Point.Set.t list
val constraints_for : kept:Point.Set.t -> t -> Point.Constraint.t
val domain : t -> Point.Set.t
val choose : (Point.t -> bool) -> t -> Point.t -> Point.t option
val sort : (int -> Point.t) -> Point.t list -> t -> t

sort mk first g builds a totally ordered graph. The output graph should imply the input graph (and the implication will be strict most of the time), but is not necessarily minimal. The lowest points in the result are identified with first. Moreover, it adds levels Type.n to identify the points (not in first) at level n. An artificial constraint (last first < mk (length first)) is added to ensure that they are not merged. Note: the result is unspecified if the input graph already contains mk n nodes.

val pr : (Point.t -> Pp.t) -> t -> Pp.t
val dump : (constraint_type -> Point.t -> Point.t -> unit) -> t -> unit