diff options
Diffstat (limited to 'library/impargs.mli')
| -rw-r--r-- | library/impargs.mli | 69 |
1 files changed, 43 insertions, 26 deletions
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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: impargs.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Names open Libnames open Term open Environ open Nametab -(*i*) -(*s Implicit arguments. Here we store the implicit arguments. Notice that we +(** {6 Implicit Arguments } *) +(** Here we store the implicit arguments. Notice that we are outside the kernel, which knows nothing about implicit arguments. *) val make_implicit_args : bool -> 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 |