From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- library/impargs.mli | 69 +++++++++++++++++++++++++++++++++-------------------- 1 file changed, 43 insertions(+), 26 deletions(-) (limited to 'library/impargs.mli') diff --git a/library/impargs.mli b/library/impargs.mli index 7ec7767b..04251f33 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -1,22 +1,19 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit @@ -36,7 +33,8 @@ val is_maximal_implicit_args : unit -> bool type implicits_flags val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b -(*s An [implicits_list] is a list of positions telling which arguments +(** {6 ... } *) +(** An [implicits_list] is a list of positions telling which arguments of a reference can be automatically infered *) @@ -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 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 * (bool * bool)) option +type implicit_status = (identifier * implicit_explanation * + (maximal_insertion * force_inference)) option + (** [None] = Not implicit *) type implicit_side_condition @@ -64,19 +84,20 @@ val force_inference_of : implicit_status -> bool val positions_of_implicits : implicits_list -> int list -(* Computation of the positions of arguments automatically inferable - for an object of the given type in the given env *) -val compute_implicits : env -> types -> implicits_list list - -(* A [manual_explicitation] is a tuple of a positional or named explicitation with +(** 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 + +val compute_implicits_names : env -> types -> name list -(*s Computation of implicits (done using the global environment). *) +(** {6 Computation of implicits (done using the global environment). } *) val declare_var_implicits : variable -> unit val declare_constant_implicits : constant -> unit @@ -84,28 +105,26 @@ val declare_mib_implicits : mutual_inductive -> unit val declare_implicits : bool -> global_reference -> unit -(* [declare_manual_implicits local ref enriching l] +(** [declare_manual_implicits local ref enriching l] Manual declaration of which arguments are expected implicit. If not set, we decide if it should enrich by automatically inferd implicits depending on the current state. 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. *) +(** 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 merge_impls : implicits_list -> implicits_list -> implicits_list +val lift_implicits : int -> manual_implicits -> manual_implicits val make_implicits_list : implicit_status list -> implicits_list list @@ -115,9 +134,7 @@ val select_impargs_size : int -> implicits_list list -> implicit_status list val select_stronger_impargs : implicits_list list -> implicit_status list -type implicit_interactive_request = - | ImplAuto - | ImplManual of int +type implicit_interactive_request type implicit_discharge_request = | ImplLocal -- cgit v1.2.3