diff options
Diffstat (limited to 'checker/univ.mli')
| -rw-r--r-- | checker/univ.mli | 95 |
1 files changed, 74 insertions, 21 deletions
diff --git a/checker/univ.mli b/checker/univ.mli index 7d4c629a..473159c0 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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) *) (************************************************************************) (** Universes. *) @@ -18,6 +20,11 @@ sig (** Create a new universe level from a unique identifier and an associated module path. *) + val var : int -> t + + val pr : t -> Pp.t + (** Pretty-printing *) + val equal : t -> t -> bool end @@ -48,7 +55,7 @@ type universe = Universe.t (** Alias name. *) -val pr_uni : universe -> Pp.std_ppcmds +val pr_uni : universe -> Pp.t (** The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ... Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0 *) @@ -71,11 +78,13 @@ type 'a check_function = universes -> 'a -> 'a -> bool val check_leq : universe check_function val check_eq : universe check_function + + (** The initial graph of universes: Prop < Set *) val initial_universes : universes (** Adds a universe to the graph, ensuring it is >= or > Set. - @raises AlreadyDeclared if the level is already declared in the graph. *) + @raise AlreadyDeclared if the level is already declared in the graph. *) exception AlreadyDeclared @@ -99,8 +108,6 @@ type 'a constrained = 'a * constraints type 'a constraint_function = 'a -> 'a -> constraints -> constraints -val enforce_leq : universe constraint_function - (** {6 ... } *) (** Merge of constraints in a universes graph. The function [merge_constraints] merges a set of constraints in a given @@ -143,8 +150,6 @@ type universe_level_subst_fn = universe_level -> universe_level type universe_subst = universe universe_map type universe_level_subst = universe_level universe_map -val level_subst_of : universe_subst_fn -> universe_level_subst_fn - (** {6 Universe instances} *) module Instance : @@ -157,7 +162,6 @@ sig val is_empty : t -> bool val equal : t -> t -> bool - (** Equality (note: instances are hash-consed, this is O(1)) *) val subst_fn : universe_level_subst_fn -> t -> t (** Substitution by a level-to-level function. *) @@ -165,11 +169,19 @@ sig val subst : universe_level_subst -> t -> t (** Substitution by a level-to-level function. *) - val pr : t -> Pp.std_ppcmds + val pr : t -> Pp.t (** Pretty-printing, no comments *) val check_eq : t check_function (** Check equality of instances w.r.t. a universe graph *) + + val length : t -> int + (** Compute the length of the instance *) + + val of_array : Level.t array -> t + + val append : t -> t -> t + (** Append two universe instances *) end type universe_instance = Instance.t @@ -187,9 +199,49 @@ sig val make : universe_instance constrained -> t val instance : t -> Instance.t val constraints : t -> constraints + val is_empty : t -> bool + +end + +type universe_context = UContext.t + +module AUContext : +sig + type t + + val size : t -> int + + val instantiate : Instance.t -> t -> Constraint.t + val repr : t -> UContext.t end +type abstract_universe_context = AUContext.t + +module Variance : +sig + (** A universe position in the instance given to a cumulative + inductive can be the following. Note there is no Contravariant + case because [forall x : A, B <= forall x : A', B'] requires [A = + A'] as opposed to [A' <= A]. *) + type t = Irrelevant | Covariant | Invariant + val check_subtype : t -> t -> bool + val leq_constraints : t array -> Instance.t constraint_function + val eq_constraints : t array -> Instance.t constraint_function +end + + +module ACumulativityInfo : +sig + type t + + val univ_context : t -> abstract_universe_context + val variance : t -> Variance.t array + +end + +type abstract_cumulativity_info = ACumulativityInfo.t + module ContextSet : sig type t @@ -198,7 +250,6 @@ module ContextSet : val constraints : t -> constraints end -type universe_context = UContext.t type universe_context_set = ContextSet.t val merge_context : bool -> universe_context -> universes -> universes @@ -221,18 +272,20 @@ val subst_univs_universe : universe_subst_fn -> universe -> universe (** Substitution of instances *) val subst_instance_instance : universe_instance -> universe_instance -> universe_instance val subst_instance_universe : universe_instance -> universe -> universe -val subst_instance_constraints : universe_instance -> constraints -> constraints (* val make_instance_subst : universe_instance -> universe_level_subst *) (* val make_inverse_instance_subst : universe_instance -> universe_level_subst *) -(** Get the instantiated graph. *) -val instantiate_univ_context : universe_context -> universe_context -val instantiate_univ_constraints : universe_instance -> universe_context -> constraints - (** Build the relative instance corresponding to the context *) -val make_abstract_instance : universe_context -> universe_instance - +val make_abstract_instance : abstract_universe_context -> universe_instance + +(** Check instance subtyping *) +val check_subtype : universes -> AUContext.t -> AUContext.t -> bool + (** {6 Pretty-printing of universes. } *) -val pr_universes : universes -> Pp.std_ppcmds +val pr_constraint_type : constraint_type -> Pp.t +val pr_constraints : (Level.t -> Pp.t) -> constraints -> Pp.t +val pr_universe_context : (Level.t -> Pp.t) -> universe_context -> Pp.t + +val pr_universes : universes -> Pp.t |