|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** Graphs representing strict orders *)
type constraint_type = Lt | Le | Eq
module type Point = sig
type t
module Set : CSig.SetS with type elt = t
module Map : CMap.ExtS with type key = t and module Set := Set
module Constraint : CSet.S with type elt = (t * constraint_type * t)
val equal : t -> t -> bool
val compare : t -> t -> int
type explanation = (constraint_type * t) list
val error_inconsistency : constraint_type -> t -> t -> explanation lazy_t option -> 'a
val pr : t -> Pp.t
end
module Make (Point:Point) : sig
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
(** @raise 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
end
¤ Dauer der Verarbeitung: 0.24 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
