diff options
Diffstat (limited to 'library/impargs.mli')
| -rw-r--r-- | library/impargs.mli | 41 |
1 files changed, 32 insertions, 9 deletions
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 |