diff options
Diffstat (limited to 'kernel/uGraph.mli')
| -rw-r--r-- | kernel/uGraph.mli | 76 |
1 files changed, 45 insertions, 31 deletions
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index e95cf4d1..0f078255 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -1,39 +1,34 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* * 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 *) +(* // * 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) *) (************************************************************************) open Univ (** {6 Graphs of universes. } *) - type t - type universes = t +[@@ocaml.deprecated "Use UGraph.t"] -type 'a check_function = universes -> 'a -> 'a -> bool -val check_leq : universe check_function -val check_eq : universe check_function +type 'a check_function = t -> 'a -> 'a -> bool -(** The empty graph of universes *) -val empty_universes : universes +val check_leq : Universe.t check_function +val check_eq : Universe.t check_function +val check_eq_level : Level.t check_function (** The initial graph of universes: Prop < Set *) -val initial_universes : universes +val initial_universes : t -val is_initial_universes : universes -> bool - -val sort_universes : universes -> universes - -(** Adds a universe to the graph, ensuring it is >= or > Set. - @raises AlreadyDeclared if the level is already declared in the graph. *) +(** Check if we are in the initial case *) +val is_initial_universes : t -> bool -exception AlreadyDeclared - -val add_universe : universe_level -> bool -> universes -> universes +(** Check equality of instances w.r.t. a universe graph *) +val check_eq_instances : Instance.t check_function (** {6 ... } *) (** Merge of constraints in a universes graph. @@ -41,23 +36,42 @@ val add_universe : universe_level -> bool -> universes -> universes universes graph. It raises the exception [UniverseInconsistency] if the constraints are not satisfiable. *) -val enforce_constraint : univ_constraint -> universes -> universes -val merge_constraints : constraints -> universes -> universes +val enforce_constraint : univ_constraint -> t -> t +val merge_constraints : Constraint.t -> t -> t -val constraints_of_universes : universes -> constraints +val check_constraint : t -> univ_constraint -> bool +val check_constraints : Constraint.t -> t -> bool -val check_constraint : universes -> univ_constraint -> bool -val check_constraints : constraints -> universes -> bool +(** Picks an arbitrary set of constraints sufficient to ensure [u <= v]. *) +val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t -val check_eq_instances : Instance.t check_function -(** Check equality of instances w.r.t. a universe graph *) +(** Adds a universe to the graph, ensuring it is >= or > Set. + @raise AlreadyDeclared if the level is already declared in the graph. *) + +exception AlreadyDeclared + +val add_universe : Level.t -> bool -> t -> t (** {6 Pretty-printing of universes. } *) -val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds +val pr_universes : (Level.t -> Pp.t) -> t -> Pp.t + +(** The empty graph of universes *) +val empty_universes : t +[@@ocaml.deprecated "Use UGraph.initial_universes"] + +val sort_universes : t -> t + +val constraints_of_universes : t -> Constraint.t + +val check_subtype : AUContext.t check_function +(** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of + [ctx1]. *) (** {6 Dumping to a file } *) val dump_universes : - (constraint_type -> string -> string -> unit) -> - universes -> unit + (constraint_type -> string -> string -> unit) -> t -> unit + +(** {6 Debugging} *) +val check_universes_invariants : t -> unit |