diff options
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 282 |
1 files changed, 156 insertions, 126 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 86887f3d..911799c4 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -1,15 +1,17 @@ (************************************************************************) -(* 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) *) (************************************************************************) 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 +30,13 @@ open Environ (** {5 Existential variables and unification states} *) -(** {6 Evars} *) - -type evar = existential_key -(** Existential variables. TODO: Should be made opaque one day. *) +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 +128,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 +142,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 +153,44 @@ val has_undefined : evar_map -> bool there are uninstantiated evars in [sigma]. *) val new_evar : evar_map -> - ?naming:Misctypes.intro_pattern_naming_expr -> 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 +201,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,28 +243,31 @@ val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> (** {6 Misc} *) -val restrict : evar -> Filter.t -> ?candidates:constr list -> - 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 downcast : evar -> types -> evar_map -> evar_map +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.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} *) @@ -275,11 +282,13 @@ val drop_side_effects : evar_map -> evar_map (** {5 Future goals} *) -val declare_future_goal : Evar.t -> evar_map -> evar_map +type goal_kind = ToShelve | ToGiveUp + +val declare_future_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map (** Adds an existential variable to the list of future goals. For internal uses only. *) -val declare_principal_goal : Evar.t -> evar_map -> evar_map +val declare_principal_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map (** Adds an existential variable to the list of future goals and make it principal. Only one existential variable can be made principal, an error is raised otherwise. For internal uses only. *) @@ -292,16 +301,41 @@ val principal_future_goal : evar_map -> Evar.t option (** Retrieves the name of the principal existential variable if there is one. Used by the [refine] primitive of the tactic engine. *) +type future_goals + +val save_future_goals : evar_map -> future_goals +(** Retrieves the list of future goals including the principal future + goal. Used by the [refine] primitive of the tactic engine. *) + val reset_future_goals : evar_map -> evar_map (** Clears the list of future goals (as well as the principal future goal). Used by the [refine] primitive of the tactic engine. *) -val restore_future_goals : evar_map -> Evar.t list -> Evar.t option -> evar_map +val restore_future_goals : evar_map -> future_goals -> evar_map (** Sets the future goals (including the principal future goal) to a previous value. Intended to be used after a local list of future goals has been consumed. Used by the [refine] primitive of the tactic engine. *) +val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> future_goals -> evar_map +(** Fold future goals *) + +val map_filter_future_goals : (Evar.t -> Evar.t option) -> future_goals -> future_goals +(** Applies a function on the future goals *) + +val filter_future_goals : (Evar.t -> bool) -> future_goals -> future_goals +(** Applies a filter on the future goals *) + +val dispatch_future_goals : future_goals -> Evar.t list * Evar.t list * Evar.t list * Evar.t option +(** Returns the future_goals dispatched into regular, shelved, given_up + goals; last argument is the goal tagged as principal if any *) + +val extract_given_up_future_goals : future_goals -> Evar.t list * Evar.t list +(** An ad hoc variant for Proof.proof; not for general use *) + +val shelve_on_future_goals : Evar.t list -> future_goals -> future_goals +(** Push goals on the shelve of future goals *) + (** {5 Sort variables} Evar maps also keep track of the universe constraints defined at a given @@ -311,10 +345,10 @@ 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 + @raise UniversesDiffer in case a first-order unification fails. + @raise UniverseInconsistency . *) (** {5 Extra data} @@ -414,16 +448,12 @@ val extract_changed_conv_pbs : evar_map -> (Evar.Set.t -> evar_constraint -> bool) -> evar_map * evar_constraint list val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list -val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t +val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option (** The following functions return the set of evars immediately contained in the object; need the term to be evar-normal otherwise defined evars are returned too. *) -val evar_list : constr -> existential list - (** excluding evars in instances of evars and collected with - redundancies from right to left (used by tactic "instantiate") *) - val evars_of_term : constr -> Evar.Set.t (** including evars in instances of evars *) @@ -487,124 +517,134 @@ 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 : 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 -> Univ.constraints +val evar_universe_context_set : UState.t -> Univ.ContextSet.t +[@@ocaml.deprecated "Alias of UState.context_set"] +val evar_universe_context_constraints : UState.t -> Univ.Constraint.t +[@@ocaml.deprecated "Alias of UState.constraints"] +val evar_context_universe_context : UState.t -> Univ.UContext.t +[@@ocaml.deprecated "alias of UState.context"] + +val evar_universe_context_of : Univ.ContextSet.t -> UState.t +[@@ocaml.deprecated "Alias of UState.of_context_set"] +val empty_evar_universe_context : UState.t +[@@ocaml.deprecated "Alias of UState.empty"] +val union_evar_universe_context : UState.t -> UState.t -> + UState.t +[@@ocaml.deprecated "Alias of UState.union"] +val evar_universe_context_subst : UState.t -> Universes.universe_opt_subst +[@@ocaml.deprecated "Alias of UState.subst"] +val constrain_variables : Univ.LSet.t -> UState.t -> UState.t +[@@ocaml.deprecated "Alias of UState.constrain_variables"] 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 +[@@ocaml.deprecated "Alias of UState.of_binders"] + +val make_evar_universe_context : env -> Misctypes.lident list option -> UState.t +[@@ocaml.deprecated "Use UState.make or UState.make_with_initial_binders"] +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 +[@@ocaml.deprecated "Alias of UState.add_constraints"] -val normalize_evar_universe_context_variables : evar_universe_context -> +val normalize_evar_universe_context_variables : UState.t -> Univ.universe_subst in_evar_universe_context +[@@ocaml.deprecated "Alias of UState.normalize_variables"] -val normalize_evar_universe_context : evar_universe_context -> - evar_universe_context +val normalize_evar_universe_context : UState.t -> UState.t +[@@ocaml.deprecated "Alias of UState.minimize"] -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 -> bool -> Univ.universe_level -> evar_map -val is_sort_variable : evar_map -> sorts -> Univ.universe_level option +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.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 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 -> 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 +(** [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 check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.constant_universes_entry -val merge_universe_context : evar_map -> evar_universe_context -> evar_map -val set_universe_context : evar_map -> evar_universe_context -> 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.universe_context_set -> 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 +[@@ocaml.deprecated "Alias of UState.abstract_undefined_variables"] val fix_undefined_variables : evar_map -> evar_map val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst +(** Universe minimization *) +val minimize_universes : evar_map -> evar_map val nf_constraints : evar_map -> evar_map +[@@ocaml.deprecated "Alias of Evd.minimize_universes"] 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 val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> Globnames.global_reference -> evar_map * constr -(******************************************************************** - Conversion w.r.t. an evar map, not unifying universes. See - [Reductionops.infer_conv] for conversion up-to universes. *) - -val test_conversion : env -> evar_map -> conv_pb -> constr -> constr -> bool -(** WARNING: This does not allow unification of universes *) - -val eq_constr_univs : evar_map -> constr -> constr -> evar_map * bool -(** Syntactic equality up to universes, recording the associated constraints *) - -val e_eq_constr_univs : evar_map ref -> constr -> constr -> bool -(** Syntactic equality up to universes. *) - (********************************************************************) (* constr with holes and pending resolution of classes, conversion *) (* problems, candidates, etc. *) -type pending = (* before: *) evar_map * (* after: *) evar_map - -type pending_constr = pending * constr - type open_constr = evar_map * constr (* Special case when before is empty *) (** Partially constructed constrs. *) @@ -612,26 +652,16 @@ type open_constr = evar_map * constr (* Special case when before is empty *) type unsolvability_explanation = SeveralInstancesFound of int (** Failure explanation. *) -val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds - -val pr_evar_suggested_name : existential_key -> evar_map -> Id.t - -(** {5 Debug pretty-printers} *) +(** {5 Summary names} *) -val pr_evar_info : evar_info -> Pp.std_ppcmds -val pr_evar_constraints : evar_constraint list -> Pp.std_ppcmds -val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds -val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) -> - evar_map -> Pp.std_ppcmds -val pr_metaset : Metaset.t -> Pp.std_ppcmds -val pr_evar_universe_context : evar_universe_context -> Pp.std_ppcmds -val pr_evd_level : evar_map -> Univ.Level.t -> Pp.std_ppcmds +(* 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 |