diff options
Diffstat (limited to 'engine/evarutil.mli')
| -rw-r--r-- | engine/evarutil.mli | 127 |
1 files changed, 79 insertions, 48 deletions
diff --git a/engine/evarutil.mli b/engine/evarutil.mli index e289ca16..0ad323ac 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -12,6 +12,7 @@ open Names open Constr open Evd open Environ +open Namegen open EConstr (** This module provides useful higher-level functions for evar manipulation. *) @@ -25,53 +26,48 @@ val mk_new_meta : unit -> constr (** {6 Creating a fresh evar given their type and context} *) val new_evar_from_context : - named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> evar_map * EConstr.t + ?naming:intro_pattern_naming_expr -> + ?principal:bool -> + named_context_val -> evar_map -> types -> evar_map * EConstr.t + +type naming_mode = + | KeepUserNameAndRenameExistingButSectionNames + | KeepUserNameAndRenameExistingEvenSectionNames + | KeepExistingNames + | FailIfConflict val new_evar : - env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> evar_map * EConstr.t + ?naming:intro_pattern_naming_expr -> + ?principal:bool -> ?hypnaming:naming_mode -> + env -> evar_map -> types -> evar_map * EConstr.t val new_pure_evar : - named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> evar_map * Evar.t + ?naming:intro_pattern_naming_expr -> + ?principal:bool -> + named_context_val -> evar_map -> types -> evar_map * Evar.t val new_pure_evar_full : evar_map -> evar_info -> evar_map * Evar.t -(** the same with side-effects *) -val e_new_evar : - env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> constr - (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) val new_type_evar : - env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> - evar_map * (constr * Sorts.t) - -val e_new_type_evar : env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * Sorts.t - -val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr -val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr + ?naming:intro_pattern_naming_expr -> + ?principal:bool -> ?hypnaming:naming_mode -> + env -> evar_map -> rigid -> + evar_map * (constr * Sorts.t) -val restrict_evar : evar_map -> Evar.t -> Filter.t -> - ?src:Evar_kinds.t Loc.located -> constr list option -> evar_map * Evar.t +val new_Type : ?rigid:rigid -> evar_map -> evar_map * constr (** Polymorphic constants *) -val new_global : evar_map -> Globnames.global_reference -> evar_map * constr -val e_new_global : evar_map ref -> Globnames.global_reference -> constr +val new_global : evar_map -> GlobRef.t -> evar_map * constr (** Create a fresh evar in a context different from its definition context: [new_evar_instance sign evd ty inst] creates a new evar of context @@ -80,10 +76,10 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> constr of [inst] are typed in the occurrence context and their type (seen as a telescope) is [sign] *) val new_evar_instance : - named_context_val -> evar_map -> types -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> - ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> + ?store:Store.t -> ?naming:intro_pattern_naming_expr -> ?principal:bool -> + named_context_val -> evar_map -> types -> constr list -> evar_map * constr val make_pure_subst : evar_info -> 'a array -> (Id.t * 'a) list @@ -132,7 +128,7 @@ val advance : evar_map -> Evar.t -> Evar.t option [nf_evar]. *) val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t -val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t +val undefined_evars_of_named_context : evar_map -> Constr.named_context -> Evar.Set.t val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t type undefined_evars_cache @@ -165,7 +161,7 @@ val jv_nf_evar : val tj_nf_evar : evar_map -> unsafe_type_judgment -> unsafe_type_judgment -val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t +val nf_named_context_evar : evar_map -> Constr.named_context -> Constr.named_context val nf_rel_context_evar : evar_map -> rel_context -> rel_context val nf_env_evar : evar_map -> env -> env @@ -178,11 +174,12 @@ val nf_evar_map_undefined : evar_map -> evar_map val nf_evars_universes : evar_map -> Constr.constr -> Constr.constr val nf_evars_and_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr) -val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * Universes.universe_opt_subst +[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"] (** Normalize the evar map w.r.t. universes, after simplification of constraints. Return the substitution function for constrs as well. *) val nf_evar_map_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr) +[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evar_map and nf_evars_universes"] (** Replacing all evars, possibly raising [Uninstantiated_evar] *) exception Uninstantiated_evar of Evar.t @@ -201,7 +198,7 @@ val kind_of_term_upto : evar_map -> Constr.constr -> universes. The term [t] is interpreted in [sigma1] while [u] is interpreted in [sigma2]. The universe constraints in [sigma2] are assumed to be an extention of those in [sigma1]. *) -val eq_constr_univs_test : evar_map -> evar_map -> Constr.constr -> Constr.constr -> bool +val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool (** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns [Inl sigma'] where [sigma'] is [sigma] augmented with universe @@ -217,20 +214,37 @@ val compare_cumulative_instances : Reduction.conv_pb -> Univ.Variance.t array -> val compare_constructor_instances : evar_map -> Univ.Instance.t -> Univ.Instance.t -> evar_map +(** {6 Unification problems} *) +type unification_pb = conv_pb * env * constr * constr + +(** [add_unification_pb ?tail pb sigma] + Add a unification problem [pb] to [sigma], if not already present. + Put it at the end of the list if [tail] is true, by default it is false. *) +val add_unification_pb : ?tail:bool -> unification_pb -> evar_map -> evar_map + (** {6 Removing hyps in evars'context} raise OccurHypInSimpleClause if the removal breaks dependencies *) type clear_dependency_error = | OccurHypInSimpleClause of Id.t option | EvarTypingBreak of Constr.existential +| NoCandidatesLeft of Evar.t + +exception ClearDependencyError of Id.t * clear_dependency_error * GlobRef.t option -exception ClearDependencyError of Id.t * clear_dependency_error +(** Restrict an undefined evar according to a (sub)filter and candidates. + The evar will be defined if there is only one candidate left, +@raise ClearDependencyError NoCandidatesLeft if the filter turns the candidates + into an empty list. *) -val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types -> - Id.Set.t -> named_context_val * types +val restrict_evar : evar_map -> Evar.t -> Filter.t -> + ?src:Evar_kinds.t Loc.located -> constr list option -> evar_map * Evar.t -val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types -> - Id.Set.t -> named_context_val * types * types +val clear_hyps_in_evi : env -> evar_map -> named_context_val -> types -> + Id.Set.t -> evar_map * named_context_val * types + +val clear_hyps2_in_evi : env -> evar_map -> named_context_val -> types -> types -> + Id.Set.t -> evar_map * named_context_val * types * types type csubst @@ -240,10 +254,11 @@ val csubst_subst : csubst -> constr -> constr type ext_named_context = csubst * Id.Set.t * named_context -val push_rel_decl_to_named_context : +val push_rel_decl_to_named_context : ?hypnaming:naming_mode -> evar_map -> rel_declaration -> ext_named_context -> ext_named_context -val push_rel_context_to_named_context : Environ.env -> evar_map -> types -> +val push_rel_context_to_named_context : ?hypnaming:naming_mode -> + Environ.env -> evar_map -> types -> named_context_val * types * constr list * csubst val generalize_evar_over_rels : evar_map -> existential -> types * constr list @@ -254,13 +269,29 @@ val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a -val subterm_source : Evar.t -> Evar_kinds.t Loc.located -> +val subterm_source : Evar.t -> ?where:Evar_kinds.subevar_kind -> Evar_kinds.t Loc.located -> Evar_kinds.t Loc.located val meta_counter_summary_tag : int Summary.Dyn.tag -(** Deprecated *) -type type_constraint = types option -[@@ocaml.deprecated "use the version in Evardefine"] -type val_constraint = constr option -[@@ocaml.deprecated "use the version in Evardefine"] +val e_new_evar : + env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?candidates:constr list -> ?store:Store.t -> + ?naming:intro_pattern_naming_expr -> + ?principal:bool -> ?hypnaming:naming_mode -> types -> constr +[@@ocaml.deprecated "Use [Evarutil.new_evar]"] + +val e_new_type_evar : env -> evar_map ref -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?naming:intro_pattern_naming_expr -> + ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t +[@@ocaml.deprecated "Use [Evarutil.new_type_evar]"] + +val e_new_Type : ?rigid:rigid -> evar_map ref -> constr +[@@ocaml.deprecated "Use [Evarutil.new_Type]"] + +val e_new_global : evar_map ref -> GlobRef.t -> constr +[@@ocaml.deprecated "Use [Evarutil.new_global]"] + +val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * UnivSubst.universe_opt_subst +[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"] |