blob: de8d89166992653e884d1964053ff508cc681f7a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Names
open Globnames
open Term
open Environ
open Nametab
(** {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
val make_strict_implicit_args : bool -> unit
val make_strongly_strict_implicit_args : bool -> unit
val make_reversible_pattern_implicit_args : bool -> unit
val make_contextual_implicit_args : bool -> unit
val make_maximal_implicit_args : bool -> unit
val is_implicit_args : unit -> bool
val is_strict_implicit_args : unit -> bool
val is_strongly_strict_implicit_args : unit -> bool
val is_reversible_pattern_implicit_args : unit -> bool
val is_contextual_implicit_args : unit -> bool
val is_maximal_implicit_args : unit -> bool
type implicits_flags
val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b
(** {6 ... } *)
(** An [implicits_list] is a list of positions telling which arguments
of a reference can be automatically infered *)
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 = (Id.t * implicit_explanation *
(maximal_insertion * force_inference)) option
(** [None] = Not implicit *)
type implicit_side_condition
type implicits_list = implicit_side_condition * implicit_status list
val is_status_implicit : implicit_status -> bool
val is_inferable_implicit : bool -> int -> implicit_status -> bool
val name_of_implicit : implicit_status -> Id.t
val maximal_insertion_of : implicit_status -> bool
val force_inference_of : implicit_status -> bool
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 = Constrexpr.explicitation *
(maximal_insertion * force_inference * bool)
type manual_implicits = manual_explicitation list
val compute_implicits_with_manual : env -> types -> bool ->
manual_implicits -> implicit_status list
val compute_implicits_names : env -> types -> Name.t list
(** {6 Computation of implicits (done using the global environment). } *)
val declare_var_implicits : variable -> unit
val declare_constant_implicits : constant -> unit
val declare_mib_implicits : mutual_inductive -> unit
val declare_implicits : bool -> global_reference -> unit
(** [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_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_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_implicits -> manual_implicits
val make_implicits_list : implicit_status list -> implicits_list list
val drop_first_implicits : int -> implicits_list -> implicits_list
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
type implicit_discharge_request =
| ImplLocal
| ImplConstant of constant * implicits_flags
| ImplMutualInductive of mutual_inductive * implicits_flags
| ImplInteractive of global_reference * implicits_flags *
implicit_interactive_request
|
