diff options
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 184 |
1 files changed, 100 insertions, 84 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 96e4b6acc..b28ce2a62 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -9,7 +9,7 @@ open Util open Loc open Names -open Term +open Constr open Environ (** This file defines the pervasive unification state used everywhere in Coq @@ -28,12 +28,13 @@ open Environ (** {5 Existential variables and unification states} *) -(** {6 Evars} *) - -type evar = existential_key +type evar = Evar.t +[@@ocaml.deprecated "use Evar.t"] (** Existential variables. *) -val string_of_existential : evar -> string +(** {6 Evars} *) +val string_of_existential : Evar.t -> string +[@@ocaml.deprecated "use Evar.print"] (** {6 Evar filters} *) @@ -125,6 +126,7 @@ val map_evar_info : (constr -> constr) -> evar_info -> evar_info (** {6 Unification state} **) type evar_universe_context = UState.t +[@@ocaml.deprecated "Alias of UState.t"] (** The universe context associated to an evar map *) type evar_map @@ -138,7 +140,7 @@ val from_env : env -> evar_map (** The empty evar map with given universe context, taking its initial universes from env. *) -val from_ctx : evar_universe_context -> evar_map +val from_ctx : UState.t -> evar_map (** The empty evar map with given universe context *) val is_empty : evar_map -> bool @@ -149,44 +151,44 @@ val has_undefined : evar_map -> bool there are uninstantiated evars in [sigma]. *) val new_evar : evar_map -> - ?name:Id.t -> evar_info -> evar_map * evar + ?name:Id.t -> evar_info -> evar_map * Evar.t (** Creates a fresh evar mapping to the given information. *) -val add : evar_map -> evar -> evar_info -> evar_map +val add : evar_map -> Evar.t -> evar_info -> evar_map (** [add sigma ev info] adds [ev] with evar info [info] in sigma. Precondition: ev must not preexist in [sigma]. *) -val find : evar_map -> evar -> evar_info +val find : evar_map -> Evar.t -> evar_info (** Recover the data associated to an evar. *) -val find_undefined : evar_map -> evar -> evar_info +val find_undefined : evar_map -> Evar.t -> evar_info (** Same as {!find} but restricted to undefined evars. For efficiency reasons. *) -val remove : evar_map -> evar -> evar_map +val remove : evar_map -> Evar.t -> evar_map (** Remove an evar from an evar map. Use with caution. *) -val mem : evar_map -> evar -> bool +val mem : evar_map -> Evar.t -> bool (** Whether an evar is present in an evarmap. *) -val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a +val fold : (Evar.t -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a (** Apply a function to all evars and their associated info in an evarmap. *) -val fold_undefined : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a +val fold_undefined : (Evar.t -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a (** Same as {!fold}, but restricted to undefined evars. For efficiency reasons. *) -val raw_map : (evar -> evar_info -> evar_info) -> evar_map -> evar_map +val raw_map : (Evar.t -> evar_info -> evar_info) -> evar_map -> evar_map (** Apply the given function to all evars in the map. Beware: this function expects the argument function to preserve the kind of [evar_body], i.e. it must send [Evar_empty] to [Evar_empty] and [Evar_defined c] to some [Evar_defined c']. *) -val raw_map_undefined : (evar -> evar_info -> evar_info) -> evar_map -> evar_map +val raw_map_undefined : (Evar.t -> evar_info -> evar_info) -> evar_map -> evar_map (** Same as {!raw_map}, but restricted to undefined evars. For efficiency reasons. *) -val define : evar -> constr -> evar_map -> evar_map +val define : Evar.t-> constr -> evar_map -> evar_map (** Set the body of an evar to the given constr. It is expected that: {ul {- The evar is already present in the evarmap.} @@ -197,16 +199,16 @@ val define : evar -> constr -> evar_map -> evar_map val cmap : (constr -> constr) -> evar_map -> evar_map (** Map the function on all terms in the evar map. *) -val is_evar : evar_map -> evar -> bool +val is_evar : evar_map -> Evar.t-> bool (** Alias for {!mem}. *) -val is_defined : evar_map -> evar -> bool +val is_defined : evar_map -> Evar.t-> bool (** Whether an evar is defined in an evarmap. *) -val is_undefined : evar_map -> evar -> bool +val is_undefined : evar_map -> Evar.t-> bool (** Whether an evar is not defined in an evarmap. *) -val add_constraints : evar_map -> Univ.constraints -> evar_map +val add_constraints : evar_map -> Univ.Constraint.t -> evar_map (** Add universe constraints in an evar map. *) val undefined_map : evar_map -> evar_info Evar.Map.t @@ -239,31 +241,31 @@ val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> (** {6 Misc} *) -val restrict : evar -> Filter.t -> ?candidates:constr list -> - ?src:Evar_kinds.t located -> evar_map -> evar_map * evar +val restrict : Evar.t-> Filter.t -> ?candidates:constr list -> + ?src:Evar_kinds.t located -> evar_map -> evar_map * Evar.t (** Restrict an undefined evar into a new evar by filtering context and possibly limiting the instances to a set of candidates *) -val is_restricted_evar : evar_info -> evar option +val is_restricted_evar : evar_info -> Evar.t option (** Tell if an evar comes from restriction of another evar, and if yes, which *) -val downcast : evar -> types -> evar_map -> evar_map +val downcast : Evar.t-> types -> evar_map -> evar_map (** Change the type of an undefined evar to a new type assumed to be a subtype of its current type; subtyping must be ensured by caller *) -val evar_source : existential_key -> evar_map -> Evar_kinds.t located +val evar_source : Evar.t -> evar_map -> Evar_kinds.t located (** Convenience function. Wrapper around {!find} to recover the source of an evar in a given evar map. *) -val evar_ident : existential_key -> evar_map -> Id.t option +val evar_ident : Evar.t -> evar_map -> Id.t option -val rename : existential_key -> Id.t -> evar_map -> evar_map +val rename : Evar.t -> Id.t -> evar_map -> evar_map -val evar_key : Id.t -> evar_map -> existential_key +val evar_key : Id.t -> evar_map -> Evar.t val evar_source_of_meta : metavariable -> evar_map -> Evar_kinds.t located -val dependent_evar_ident : existential_key -> evar_map -> Id.t +val dependent_evar_ident : Evar.t -> evar_map -> Id.t (** {5 Side-effects} *) @@ -314,7 +316,7 @@ val whd_sort_variable : evar_map -> constr -> constr exception UniversesDiffer -val add_universe_constraints : evar_map -> Universes.universe_constraints -> evar_map +val add_universe_constraints : evar_map -> Universes.Constraints.t -> evar_map (** Add the given universe unification constraints to the evar map. @raises UniversesDiffer in case a first-order unification fails. @raises UniverseInconsistency @@ -486,88 +488,97 @@ val univ_rigid : rigid val univ_flexible : rigid val univ_flexible_alg : rigid -type 'a in_evar_universe_context = 'a * evar_universe_context +type 'a in_evar_universe_context = 'a * UState.t + +val evar_universe_context_set : UState.t -> Univ.ContextSet.t +val evar_universe_context_constraints : UState.t -> Univ.Constraint.t +val evar_context_universe_context : UState.t -> Univ.UContext.t +[@@ocaml.deprecated "alias of UState.context"] -val evar_universe_context_set : evar_universe_context -> Univ.universe_context_set -val evar_universe_context_constraints : evar_universe_context -> Univ.constraints -val evar_context_universe_context : evar_universe_context -> Univ.universe_context -val evar_universe_context_of : Univ.universe_context_set -> evar_universe_context -val empty_evar_universe_context : evar_universe_context -val union_evar_universe_context : evar_universe_context -> evar_universe_context -> - evar_universe_context -val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst -val constrain_variables : Univ.LSet.t -> evar_universe_context -> evar_universe_context +val evar_universe_context_of : Univ.ContextSet.t -> UState.t +val empty_evar_universe_context : UState.t +val union_evar_universe_context : UState.t -> UState.t -> + UState.t +val evar_universe_context_subst : UState.t -> Universes.universe_opt_subst +val constrain_variables : Univ.LSet.t -> UState.t -> UState.t val evar_universe_context_of_binders : - Universes.universe_binders -> evar_universe_context - -val make_evar_universe_context : env -> (Id.t located) list option -> evar_universe_context -val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map + Universes.universe_binders -> UState.t + +val make_evar_universe_context : env -> (Id.t located) list option -> UState.t +val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map (** Raises Not_found if not a name for a universe in this map. *) -val universe_of_name : evar_map -> string -> Univ.universe_level -val add_universe_name : evar_map -> string -> Univ.universe_level -> evar_map +val universe_of_name : evar_map -> Id.t -> Univ.Level.t -val add_constraints_context : evar_universe_context -> - Univ.constraints -> evar_universe_context +val universe_binders : evar_map -> Universes.universe_binders +val add_constraints_context : UState.t -> + Univ.Constraint.t -> UState.t -val normalize_evar_universe_context_variables : evar_universe_context -> +val normalize_evar_universe_context_variables : UState.t -> Univ.universe_subst in_evar_universe_context -val normalize_evar_universe_context : evar_universe_context -> - evar_universe_context +val normalize_evar_universe_context : UState.t -> + UState.t -val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level -val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe -val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * sorts +val new_univ_level_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Level.t +val new_univ_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Universe.t +val new_sort_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Sorts.t val add_global_univ : evar_map -> Univ.Level.t -> evar_map val universe_rigidity : evar_map -> Univ.Level.t -> rigid -val make_flexible_variable : evar_map -> algebraic:bool -> Univ.universe_level -> evar_map +val make_flexible_variable : evar_map -> algebraic:bool -> Univ.Level.t -> evar_map (** See [UState.make_flexible_variable] *) -val is_sort_variable : evar_map -> sorts -> Univ.universe_level option +val is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t option (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is not a local sort variable declared in [evm] *) val is_flexible_level : evar_map -> Univ.Level.t -> bool -(* val normalize_universe_level : evar_map -> Univ.universe_level -> Univ.universe_level *) -val normalize_universe : evar_map -> Univ.universe -> Univ.universe -val normalize_universe_instance : evar_map -> Univ.universe_instance -> Univ.universe_instance +(* val normalize_universe_level : evar_map -> Univ.Level.t -> Univ.Level.t *) +val normalize_universe : evar_map -> Univ.Universe.t -> Univ.Universe.t +val normalize_universe_instance : evar_map -> Univ.Instance.t -> Univ.Instance.t -val set_leq_sort : env -> evar_map -> sorts -> sorts -> evar_map -val set_eq_sort : env -> evar_map -> sorts -> sorts -> evar_map -val has_lub : evar_map -> Univ.universe -> Univ.universe -> evar_map -val set_eq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map -val set_leq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map +val set_leq_sort : env -> evar_map -> Sorts.t -> Sorts.t -> evar_map +val set_eq_sort : env -> evar_map -> Sorts.t -> Sorts.t -> evar_map +val has_lub : evar_map -> Univ.Universe.t -> Univ.Universe.t -> evar_map +val set_eq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map +val set_leq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map val set_eq_instances : ?flex:bool -> - evar_map -> Univ.universe_instance -> Univ.universe_instance -> evar_map + evar_map -> Univ.Instance.t -> Univ.Instance.t -> evar_map -val check_eq : evar_map -> Univ.universe -> Univ.universe -> bool -val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool +val check_eq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool +val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool -val evar_universe_context : evar_map -> evar_universe_context -val universe_context_set : evar_map -> Univ.universe_context_set -val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map -> - (Id.t * Univ.Level.t) list * Univ.universe_context +val evar_universe_context : evar_map -> UState.t +val universe_context_set : evar_map -> Univ.ContextSet.t val universe_subst : evar_map -> Universes.universe_opt_subst val universes : evar_map -> UGraph.t -val check_univ_decl : evar_map -> UState.universe_decl -> - Universes.universe_binders * Univ.universe_context +(** [to_universe_context evm] extracts the local universes and + constraints of [evm] and orders the universes the same as + [Univ.ContextSet.to_context]. *) +val to_universe_context : evar_map -> Univ.UContext.t + +val const_univ_entry : poly:bool -> evar_map -> Entries.constant_universes_entry + +(** NB: [ind_univ_entry] cannot create cumulative entries. *) +val ind_univ_entry : poly:bool -> evar_map -> Entries.inductive_universes -val merge_universe_context : evar_map -> evar_universe_context -> evar_map -val set_universe_context : evar_map -> evar_universe_context -> evar_map +val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.constant_universes_entry -val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.universe_context_set -> evar_map +val merge_universe_context : evar_map -> UState.t -> evar_map +val set_universe_context : evar_map -> UState.t -> evar_map + +val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.ContextSet.t -> evar_map val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst -val abstract_undefined_variables : evar_universe_context -> evar_universe_context +val abstract_undefined_variables : UState.t -> UState.t val fix_undefined_variables : evar_map -> evar_map @@ -579,8 +590,8 @@ val update_sigma_env : evar_map -> env -> evar_map (** Polymorphic universes *) -val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts -val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> constant -> evar_map * pconstant +val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> env -> evar_map -> Sorts.family -> evar_map * Sorts.t +val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> Constant.t -> evar_map * pconstant val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor @@ -598,11 +609,16 @@ type open_constr = evar_map * constr (* Special case when before is empty *) type unsolvability_explanation = SeveralInstancesFound of int (** Failure explanation. *) +(** {5 Summary names} *) + +(* This stuff is internal and should not be used. Currently a hack in + the STM relies on it. *) +val evar_counter_summary_tag : int Summary.Dyn.tag + (** {5 Deprecated functions} *) +val create_evar_defs : evar_map -> evar_map +(* XXX: This is supposed to be deprecated by used by ssrmatching, what + should the replacement be? *) -val create_evar_defs : evar_map -> evar_map (** Create an [evar_map] with empty meta map: *) -(** {5 Summary names} *) - -val evar_counter_summary_name : string |