diff options
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 108 |
1 files changed, 68 insertions, 40 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 679173ca72..fafaad9a04 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -89,6 +89,15 @@ module Abstraction : sig val abstract_last : t -> t end +module Identity : +sig + type t + (** Identity substitutions *) + + val make : econstr list -> t + val none : unit -> t +end + (** {6 Evar infos} *) type evar_body = @@ -114,6 +123,9 @@ type evar_info = { (** Information about the evar. *) evar_candidates : econstr list option; (** List of possible solutions when known that it is a finite list *) + evar_identity : Identity.t; + (** Default evar instance, i.e. a list of Var nodes projected from the + filtered environment. *) } val make_evar : named_context_val -> etypes -> evar_info @@ -127,6 +139,7 @@ val evar_candidates : evar_info -> constr list option val evar_filter : evar_info -> Filter.t val evar_env : env -> evar_info -> env val evar_filtered_env : env -> evar_info -> env +val evar_identity_subst : evar_info -> econstr list val map_evar_body : (econstr -> econstr) -> evar_body -> evar_body val map_evar_info : (econstr -> econstr) -> evar_info -> evar_info @@ -154,6 +167,14 @@ val has_undefined : evar_map -> bool (** [has_undefined sigma] is [true] if and only if there are uninstantiated evars in [sigma]. *) +val has_given_up : evar_map -> bool +(** [has_given_up sigma] is [true] if and only if + there are given up evars in [sigma]. *) + +val has_shelved : evar_map -> bool +(** [has_shelved sigma] is [true] if and only if + there are shelved evars in [sigma]. *) + val new_evar : evar_map -> ?name:Id.t -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t (** Creates a fresh evar mapping to the given information. *) @@ -263,8 +284,11 @@ val restrict : Evar.t-> Filter.t -> ?candidates:econstr list -> possibly limiting the instances to a set of candidates (candidates are filtered according to the filter) *) -val is_restricted_evar : evar_map -> Evar.t -> Evar.t option -(** Tell if an evar comes from restriction of another evar, and if yes, which *) +val get_aliased_evars : evar_map -> Evar.t Evar.Map.t +(** The map of aliased evars *) + +val is_aliased_evar : evar_map -> Evar.t -> Evar.t option +(** Tell if an evar has been aliased to another evar, and if yes, which *) val set_typeclass_evars : evar_map -> Evar.Set.t -> evar_map (** Mark the given set of evars as available for resolution. @@ -330,59 +354,64 @@ val drop_side_effects : evar_map -> evar_map (** {5 Future goals} *) -type goal_kind = ToShelve | ToGiveUp - -val declare_future_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map +val declare_future_goal : Evar.t -> evar_map -> evar_map (** Adds an existential variable to the list of future goals. For internal uses only. *) -val declare_principal_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map +val declare_principal_goal : 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. *) -val future_goals : evar_map -> Evar.t list -(** Retrieves the list of future goals. Used by the [refine] primitive - of the tactic engine. *) +module FutureGoals : sig -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 t = private { + comb : Evar.t list; + principal : Evar.t option; (** if [Some e], [e] must be + contained in + [future_comb]. The evar + [e] will inherit + properties (now: the + name) of the evar which + will be instantiated with + a term containing [e]. *) + } -type future_goals + val map_filter : (Evar.t -> Evar.t option) -> t -> t + (** Applies a function on the 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 filter : (Evar.t -> bool) -> t -> t + (** Applies a filter on the future goals *) -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. *) +end + +val push_future_goals : evar_map -> evar_map + +val pop_future_goals : evar_map -> FutureGoals.t * evar_map + +val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> evar_map + +val remove_future_goal : evar_map -> Evar.t -> 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 pr_future_goals_stack : evar_map -> Pp.t -val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> future_goals -> evar_map -(** Fold future goals *) +val push_shelf : evar_map -> evar_map -val map_filter_future_goals : (Evar.t -> Evar.t option) -> future_goals -> future_goals -(** Applies a function on the future goals *) +val pop_shelf : evar_map -> Evar.t list * evar_map -val filter_future_goals : (Evar.t -> bool) -> future_goals -> future_goals -(** Applies a filter on the future goals *) +val filter_shelf : (Evar.t -> bool) -> evar_map -> evar_map -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 give_up : Evar.t -> evar_map -> evar_map -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 : evar_map -> Evar.t list -> evar_map -val shelve_on_future_goals : Evar.t list -> future_goals -> future_goals -(** Push goals on the shelve of future goals *) +val unshelve : evar_map -> Evar.t list -> evar_map + +val given_up : evar_map -> Evar.Set.t + +val shelf : evar_map -> Evar.t list + +val pr_shelf : evar_map -> Pp.t (** {5 Sort variables} @@ -643,12 +672,11 @@ val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst 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 update_sigma_env : evar_map -> env -> evar_map +(** Lift [UState.update_sigma_univs] *) +val update_sigma_univs : UGraph.t -> evar_map -> evar_map (** Polymorphic universes *) |