diff options
| -rw-r--r-- | interp/constrintern.ml | 2 | ||||
| -rw-r--r-- | interp/constrintern.mli | 14 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.mli | 2 | ||||
| -rw-r--r-- | library/impargs.ml | 2 | ||||
| -rw-r--r-- | library/impargs.mli | 41 | ||||
| -rw-r--r-- | toplevel/command.mli | 26 |
6 files changed, 54 insertions, 33 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8454b8fef..6072549c2 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1451,8 +1451,6 @@ let intern_pattern env patt = user_err_loc (loc,"internalize",explain_internalization_error e) -type manual_implicits = (explicitation * (bool * bool * bool)) list - (*********************************************************************) (* Functions to parse and interpret constructions *) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 59afcd313..12dc6be16 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -64,8 +64,6 @@ val compute_internalization_env : env -> var_internalization_type -> identifier list -> types list -> Impargs.manual_explicitation list list -> internalization_env -type manual_implicits = (explicitation * (bool * bool * bool)) list - type ltac_sign = identifier list * unbound_ltac_var_map type glob_binder = (name * binding_kind * glob_constr option * glob_constr) @@ -112,15 +110,15 @@ val interp_casted_constr : evar_map -> env -> ?impls:internalization_env -> (** Accepting evars and giving back the manual implicits in addition. *) val interp_casted_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env -> - ?impls:internalization_env -> constr_expr -> types -> constr * manual_implicits + ?impls:internalization_env -> constr_expr -> types -> constr * Impargs.manual_implicits val interp_type_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env -> ?impls:internalization_env -> - constr_expr -> types * manual_implicits + constr_expr -> types * Impargs.manual_implicits val interp_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env -> ?impls:internalization_env -> - constr_expr -> constr * manual_implicits + constr_expr -> constr * Impargs.manual_implicits val interp_casted_constr_evars : evar_map ref -> env -> ?impls:internalization_env -> constr_expr -> types -> constr @@ -155,13 +153,13 @@ val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types val interp_context_gen : (env -> glob_constr -> types) -> (env -> glob_constr -> unsafe_judgment) -> ?global_level:bool -> - evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits + evar_map -> env -> local_binder list -> (env * rel_context) * Impargs.manual_implicits val interp_context : ?global_level:bool -> - evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits + evar_map -> env -> local_binder list -> (env * rel_context) * Impargs.manual_implicits val interp_context_evars : ?global_level:bool -> - evar_map ref -> env -> local_binder list -> (env * rel_context) * manual_implicits + evar_map ref -> env -> local_binder list -> (env * rel_context) * Impargs.manual_implicits (** Locating references of constructions, possibly via a syntactic definition (these functions do not modify the glob file) *) diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 05f54ec75..ce518a9cb 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -42,7 +42,7 @@ val generalizable_vars_of_glob_constr : ?bound:Idset.t -> ?allowed:Idset.t -> val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier -val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> (Topconstr.explicitation * (bool * bool * bool)) list +val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits val combine_params_freevar : Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) -> diff --git a/library/impargs.ml b/library/impargs.ml index 993e33b32..fad81b152 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -588,6 +588,8 @@ let declare_mib_implicits kn = (* Declare manual implicits *) type manual_explicitation = Topconstr.explicitation * (bool * bool * bool) +type manual_implicits = manual_explicitation list + let compute_implicits_with_manual env typ enriching l = let _,autoimpls = compute_auto_implicits env !implicit_args enriching typ in set_manual_implicits env !implicit_args enriching autoimpls l diff --git a/library/impargs.mli b/library/impargs.mli index a4553b0fc..631574591 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -12,9 +12,7 @@ open Term open Environ open Nametab -(** Implicit Arguments *) - -(** {6 ... } *) +(** {6 Implicit Arguments } *) (** Here we store the implicit arguments. Notice that we are outside the kernel, which knows nothing about implicit arguments. *) @@ -44,13 +42,35 @@ type argument_position = | Conclusion | Hyp of int +(** We remember various information about why an argument is + inferable as implicit *) type implicit_explanation = | DepRigid of argument_position + (** means that the implicit argument can be found by + unification along a rigid path (we do not print the arguments of + this kind if there is enough arguments to infer them) *) | DepFlex of argument_position + (** means that the implicit argument can be found by unification + along a collapsable path only (e.g. as x in (P x) where P is another + argument) (we do (defensively) print the arguments of this kind) *) | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position + (** means that the least argument from which the + implicit argument can be inferred is following a collapsable path + but there is a greater argument from where the implicit argument is + inferable following a rigid path (useful to know how to print a + partial application) *) | Manual + (** means the argument has been explicitely set as implicit. *) + +(** We also consider arguments inferable from the conclusion but it is + operational only if [conclusion_matters] is true. *) -type implicit_status = (identifier * implicit_explanation * (bool * bool)) option +type maximal_insertion = bool (** true = maximal contextual insertion *) +type force_inference = bool (** true = always infer, never turn into evar/subgoal *) + +type implicit_status = (identifier * implicit_explanation * + (maximal_insertion * force_inference)) option + (** [None] = Not implicit *) type implicit_side_condition @@ -67,10 +87,13 @@ val positions_of_implicits : implicits_list -> int list (** A [manual_explicitation] is a tuple of a positional or named explicitation with maximal insertion, force inference and force usage flags. Forcing usage makes the argument implicit even if the automatic inference considers it not inferable. *) -type manual_explicitation = Topconstr.explicitation * (bool * bool * bool) +type manual_explicitation = Topconstr.explicitation * + (maximal_insertion * force_inference * bool) + +type manual_implicits = manual_explicitation list val compute_implicits_with_manual : env -> types -> bool -> - manual_explicitation list -> implicit_status list + manual_implicits -> implicit_status list (** {6 Computation of implicits (done using the global environment). } *) @@ -87,19 +110,19 @@ val declare_implicits : bool -> global_reference -> unit Unsets implicits if [l] is empty. *) val declare_manual_implicits : bool -> global_reference -> ?enriching:bool -> - manual_explicitation list list -> unit + manual_implicits list -> unit (** If the list is empty, do nothing, otherwise declare the implicits. *) val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool -> - manual_explicitation list -> unit + manual_implicits -> unit val implicits_of_global : global_reference -> implicits_list list val extract_impargs_data : implicits_list list -> ((int * int) option * implicit_status list) list -val lift_implicits : int -> manual_explicitation list -> manual_explicitation list +val lift_implicits : int -> manual_implicits -> manual_implicits val make_implicits_list : implicit_status list -> implicits_list list diff --git a/toplevel/command.mli b/toplevel/command.mli index b12479b45..2c90b6bd5 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -32,22 +32,22 @@ val set_declare_assumptions_hook : (types -> unit) -> unit val interp_definition : local_binder list -> red_expr option -> constr_expr -> - constr_expr option -> definition_entry * manual_implicits + constr_expr option -> definition_entry * Impargs.manual_implicits val declare_definition : identifier -> locality * definition_object_kind -> - definition_entry -> manual_implicits -> declaration_hook -> unit + definition_entry -> Impargs.manual_implicits -> declaration_hook -> unit (** {6 Parameters/Assumptions} *) val interp_assumption : - local_binder list -> constr_expr -> types * manual_implicits + local_binder list -> constr_expr -> types * Impargs.manual_implicits val declare_assumption : coercion_flag -> assumption_kind -> types -> - manual_implicits -> + Impargs.manual_implicits -> bool (** implicit *) -> inline -> variable located -> unit val declare_assumptions : variable located list -> - coercion_flag -> assumption_kind -> types -> manual_implicits -> + coercion_flag -> assumption_kind -> types -> Impargs.manual_implicits -> bool -> inline -> unit (** {6 Inductive and coinductive types} *) @@ -71,8 +71,8 @@ val extract_mutual_inductive_declaration_components : (** Typing mutual inductive definitions *) type one_inductive_impls = - Impargs.manual_explicitation list (** for inds *)* - Impargs.manual_explicitation list list (** for constrs *) + Impargs.manual_implicits (** for inds *)* + Impargs.manual_implicits list (** for constrs *) val interp_mutual_inductive : structured_inductive_expr -> decl_notation list -> bool -> @@ -103,7 +103,7 @@ type structured_fixpoint_expr = { (** Extracting the semantical components out of the raw syntax of (co)fixpoints declarations *) -val extract_fixpoint_components : bool -> +val extract_fixpoint_components : bool -> (fixpoint_expr * decl_notation list) list -> structured_fixpoint_expr list * decl_notation list @@ -118,20 +118,20 @@ type recursive_preentry = val interp_fixpoint : structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * (name list * manual_implicits * int option) list + recursive_preentry * (name list * Impargs.manual_implicits * int option) list val interp_cofixpoint : structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * (name list * manual_implicits * int option) list + recursive_preentry * (name list * Impargs.manual_implicits * int option) list (** Registering fixpoints and cofixpoints in the environment *) val declare_fixpoint : - recursive_preentry * (name list * manual_implicits * int option) list -> + recursive_preentry * (name list * Impargs.manual_implicits * int option) list -> lemma_possible_guards -> decl_notation list -> unit val declare_cofixpoint : - recursive_preentry * (name list * manual_implicits * int option) list -> + recursive_preentry * (name list * Impargs.manual_implicits * int option) list -> decl_notation list -> unit (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) @@ -147,4 +147,4 @@ val do_cofixpoint : val check_mutuality : Environ.env -> bool -> (identifier * types) list -> unit val declare_fix : definition_object_kind -> identifier -> - constr -> types -> Impargs.manual_explicitation list -> global_reference + constr -> types -> Impargs.manual_implicits -> global_reference |