diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-06 19:09:10 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-06 20:09:06 +0200 |
commit | 84add29c036735ceacde73ea98a9a5a454a5e3a0 (patch) | |
tree | baee8c0b023277d43366996685503c9d1f855413 /kernel/uGraph.mli | |
parent | c4db6fc1086d984fd983ff9a6797ad108d220b98 (diff) |
Splitting kernel universe code in two modules.
1. The Univ module now only cares about definitions about universes.
2. The UGraph module contains the algorithm responsible for aciclicity.
Diffstat (limited to 'kernel/uGraph.mli')
-rw-r--r-- | kernel/uGraph.mli | 63 |
1 files changed, 63 insertions, 0 deletions
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli new file mode 100644 index 000000000..e95cf4d1c --- /dev/null +++ b/kernel/uGraph.mli @@ -0,0 +1,63 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Univ + +(** {6 Graphs of universes. } *) + +type t + +type universes = t + +type 'a check_function = universes -> 'a -> 'a -> bool +val check_leq : universe check_function +val check_eq : universe check_function + +(** The empty graph of universes *) +val empty_universes : universes + +(** The initial graph of universes: Prop < Set *) +val initial_universes : universes + +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. *) + +exception AlreadyDeclared + +val add_universe : universe_level -> bool -> universes -> universes + +(** {6 ... } *) +(** Merge of constraints in a universes graph. + The function [merge_constraints] merges a set of constraints in a given + 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 constraints_of_universes : universes -> constraints + +val check_constraint : universes -> univ_constraint -> bool +val check_constraints : constraints -> universes -> bool + +val check_eq_instances : Instance.t check_function +(** Check equality of instances w.r.t. a universe graph *) + +(** {6 Pretty-printing of universes. } *) + +val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds + +(** {6 Dumping to a file } *) + +val dump_universes : + (constraint_type -> string -> string -> unit) -> + universes -> unit |