summaryrefslogtreecommitdiff
path: root/engine/uState.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/uState.mli')
-rw-r--r--engine/uState.mli95
1 files changed, 73 insertions, 22 deletions
diff --git a/engine/uState.mli b/engine/uState.mli
index 0cdc6277..48c38faf 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -1,9 +1,11 @@
(************************************************************************)
-(* 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) *)
(************************************************************************)
(** This file defines universe unification states which are part of evarmaps.
@@ -24,17 +26,21 @@ val empty : t
val make : UGraph.t -> t
+val make_with_initial_binders : UGraph.t -> Misctypes.lident list -> t
+
val is_empty : t -> bool
val union : t -> t -> t
-val of_context_set : Univ.universe_context_set -> t
+val of_context_set : Univ.ContextSet.t -> t
val of_binders : Universes.universe_binders -> t
+val universe_binders : t -> Universes.universe_binders
+
(** {5 Projections} *)
-val context_set : t -> Univ.universe_context_set
+val context_set : t -> Univ.ContextSet.t
(** The local context of the state, i.e. a set of bound variables together
with their associated constraints. *)
@@ -44,39 +50,50 @@ val subst : t -> Universes.universe_opt_subst
val ugraph : t -> UGraph.t
(** The current graph extended with the local constraints *)
+val initial_graph : t -> UGraph.t
+(** The initial graph with just the declarations of new universes. *)
+
val algebraics : t -> Univ.LSet.t
(** The subset of unification variables that can be instantiated with algebraic
universes as they appear in inferred types only. *)
-val constraints : t -> Univ.constraints
+val constraints : t -> Univ.Constraint.t
(** Shorthand for {!context_set} composed with {!ContextSet.constraints}. *)
-val context : t -> Univ.universe_context
+val context : t -> Univ.UContext.t
(** Shorthand for {!context_set} with {!Context_set.to_context}. *)
+val const_univ_entry : poly:bool -> t -> Entries.constant_universes_entry
+(** Pick from {!context} or {!context_set} based on [poly]. *)
+
+val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes
+(** Pick from {!context} or {!context_set} based on [poly].
+ Cannot create cumulative entries. *)
+
(** {5 Constraints handling} *)
-val add_constraints : t -> Univ.constraints -> t
+val drop_weak_constraints : bool ref
+
+val add_constraints : t -> Univ.Constraint.t -> t
(**
@raise UniversesDiffer when universes differ
*)
-val add_universe_constraints : t -> Universes.universe_constraints -> t
+val add_universe_constraints : t -> Universes.Constraints.t -> t
(**
@raise UniversesDiffer when universes differ
*)
(** {5 Names} *)
-val add_universe_name : t -> string -> Univ.Level.t -> t
-(** Associate a human-readable name to a local variable. *)
-
-val universe_of_name : t -> string -> Univ.Level.t
+val universe_of_name : t -> Id.t -> Univ.Level.t
(** Retrieve the universe associated to the name. *)
(** {5 Unification} *)
-val restrict : t -> Univ.universe_set -> t
+val restrict : t -> Univ.LSet.t -> t
+
+val demote_seff_univs : Safe_typing.private_constants Entries.definition_entry -> t -> t
type rigid =
| UnivRigid
@@ -86,19 +103,31 @@ val univ_rigid : rigid
val univ_flexible : rigid
val univ_flexible_alg : rigid
-val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.universe_context_set -> t
+val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.ContextSet.t -> t
val merge_subst : t -> Universes.universe_opt_subst -> t
val emit_side_effects : Safe_typing.private_constants -> t -> t
-val new_univ_variable : ?loc:Loc.t -> rigid -> string option -> t -> t * Univ.Level.t
+val new_univ_variable : ?loc:Loc.t -> rigid -> Id.t option -> t -> t * Univ.Level.t
val add_global_univ : t -> Univ.Level.t -> t
-val make_flexible_variable : t -> bool -> Univ.Level.t -> t
+
+(** [make_flexible_variable g algebraic l]
+
+ Turn the variable [l] flexible, and algebraic if [algebraic] is true
+ and [l] can be. That is if there are no strict upper constraints on
+ [l] and and it does not appear in the instance of any non-algebraic
+ universe. Otherwise the variable is just made flexible. *)
+val make_flexible_variable : t -> algebraic:bool -> Univ.Level.t -> t
+
+(** Turn all undefined flexible algebraic variables into simply flexible
+ ones. Can be used in case the variables might appear in universe instances
+ (typically for polymorphic program obligations). *)
+val make_flexible_nonalgebraic : t -> t
val is_sort_variable : t -> Sorts.t -> Univ.Level.t option
val normalize_variables : t -> Univ.universe_subst * t
-val constrain_variables : Univ.LSet.t -> t -> Univ.constraints
+val constrain_variables : Univ.LSet.t -> t -> t
val abstract_undefined_variables : t -> t
@@ -106,14 +135,36 @@ val fix_undefined_variables : t -> t
val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
+(** Universe minimization *)
+val minimize : t -> t
val normalize : t -> t
+[@@ocaml.deprecated "Alias of UState.minimize"]
-(** {5 TODO: Document me} *)
+type universe_decl =
+ (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
+
+(** [check_univ_decl ctx decl]
+
+ If non extensible in [decl], check that the local universes (resp.
+ universe constraints) in [ctx] are implied by [decl].
+
+ Return a [Entries.constant_universes_entry] containing the local
+ universes of [ctx] and their constraints.
-val universe_context : ?names:(Id.t Loc.located) list -> t -> (Id.t * Univ.Level.t) list * Univ.universe_context
+ When polymorphic, the universes corresponding to
+ [decl.univdecl_instance] come first in the order defined by that
+ list. *)
+val check_univ_decl : poly:bool -> t -> universe_decl -> Entries.constant_universes_entry
+
+val check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t
+
+(** {5 TODO: Document me} *)
val update_sigma_env : t -> Environ.env -> t
(** {5 Pretty-printing} *)
-val pr_uctx_level : t -> Univ.Level.t -> Pp.std_ppcmds
+val pr_uctx_level : t -> Univ.Level.t -> Pp.t
+val reference_of_level : t -> Univ.Level.t -> Libnames.reference
+
+val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 14:04:50 +0000