diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 18:33:25 +0100 |
commit | 1b92c226e563643da187b8614d5888dc4855eb43 (patch) | |
tree | c4c3d204b36468b58cb71050ba95f06b8dd7bc2e /kernel/uGraph.mli | |
parent | 7c9b0a702976078b813e6493c1284af62a3f093c (diff) |
Imported Upstream version 8.6
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 00000000..e95cf4d1 --- /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 |