blob: ce8cfa7dbc153df26036d07f2338f9f5f031b7bb (
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
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id$ i*)
(*i*)
open Pp
open Util
open Names
open Proof_type
open Tacmach
open Tactic_debug
open Term
open Tacexpr
open Genarg
open Topconstr
open Mod_subst
open Redexpr
(*i*)
(* Values for interpretation *)
type value =
| VRTactic of (goal list sigma * validation)
| VFun of ltac_trace * (identifier*value) list *
identifier option list * glob_tactic_expr
| VVoid
| VInteger of int
| VIntroPattern of intro_pattern_expr
| VConstr of constr
| VConstr_context of constr
| VList of value list
| VRec of (identifier*value) list ref * glob_tactic_expr
(* Signature for interpretation: val\_interp and interpretation functions *)
and interp_sign =
{ lfun : (identifier * value) list;
avoid_ids : identifier list;
debug : debug_info;
trace : ltac_trace }
val extract_ltac_vars : interp_sign -> Evd.evar_map -> Environ.env ->
Pretyping.var_map * Pretyping.unbound_ltac_var_map
(* Transforms an id into a constr if possible *)
val constr_of_id : Environ.env -> identifier -> constr
(* To embed several objects in Coqast.t *)
val tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t
val tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr)
val tacticIn : (interp_sign -> raw_tactic_expr) -> raw_tactic_expr
val globTacticIn : (interp_sign -> glob_tactic_expr) -> raw_tactic_expr
val valueIn : value -> raw_tactic_arg
val constrIn : constr -> constr_expr
(* Sets the debugger mode *)
val set_debug : debug_info -> unit
(* Gives the state of debug *)
val get_debug : unit -> debug_info
(* Adds a definition for tactics in the table *)
val add_tacdef :
Vernacexpr.locality_flag -> bool ->
(Libnames.reference * bool * raw_tactic_expr) list -> unit
val add_primitive_tactic : string -> glob_tactic_expr -> unit
(* Tactic extensions *)
val add_tactic :
string -> (typed_generic_argument list -> tactic) -> unit
val overwriting_add_tactic :
string -> (typed_generic_argument list -> tactic) -> unit
val lookup_tactic :
string -> (typed_generic_argument list) -> tactic
(* Adds an interpretation function for extra generic arguments *)
type glob_sign = {
ltacvars : identifier list * identifier list;
ltacrecvars : (identifier * Nametab.ltac_constant) list;
gsigma : Evd.evar_map;
genv : Environ.env }
val add_interp_genarg :
string ->
(glob_sign -> raw_generic_argument -> glob_generic_argument) *
(interp_sign -> goal sigma -> glob_generic_argument ->
typed_generic_argument) *
(substitution -> glob_generic_argument -> glob_generic_argument)
-> unit
val interp_genarg :
interp_sign -> goal sigma -> glob_generic_argument -> typed_generic_argument
val intern_genarg :
glob_sign -> raw_generic_argument -> glob_generic_argument
val intern_tactic :
glob_sign -> raw_tactic_expr -> glob_tactic_expr
val intern_constr :
glob_sign -> constr_expr -> rawconstr_and_expr
val intern_constr_with_bindings :
glob_sign -> constr_expr * constr_expr Rawterm.bindings ->
rawconstr_and_expr * rawconstr_and_expr Rawterm.bindings
val intern_hyp :
glob_sign -> identifier Util.located -> identifier Util.located
val subst_genarg :
substitution -> glob_generic_argument -> glob_generic_argument
val subst_rawconstr_and_expr :
substitution -> rawconstr_and_expr -> rawconstr_and_expr
(* Interprets any expression *)
val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> value
(* Interprets an expression that evaluates to a constr *)
val interp_ltac_constr : interp_sign -> goal sigma -> glob_tactic_expr ->
constr
(* Interprets redexp arguments *)
val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> red_expr
(* Interprets tactic expressions *)
val interp_tac_gen : (identifier * value) list -> identifier list ->
debug_info -> raw_tactic_expr -> tactic
val interp_hyp : interp_sign -> goal sigma -> identifier located -> identifier
val interp_bindings : interp_sign -> goal sigma -> rawconstr_and_expr Rawterm.bindings ->
Evd.open_constr Rawterm.bindings
(* Initial call for interpretation *)
val glob_tactic : raw_tactic_expr -> glob_tactic_expr
val glob_tactic_env : identifier list -> Environ.env -> raw_tactic_expr -> glob_tactic_expr
val eval_tactic : glob_tactic_expr -> tactic
val interp : raw_tactic_expr -> tactic
val eval_ltac_constr : goal sigma -> raw_tactic_expr -> constr
val subst_tactic : substitution -> glob_tactic_expr -> glob_tactic_expr
(* Hides interpretation for pretty-print *)
val hide_interp : raw_tactic_expr -> tactic option -> tactic
(* Declare the default tactic to fill implicit arguments *)
val declare_implicit_tactic : tactic -> unit
(* Declare the xml printer *)
val declare_xml_printer :
(out_channel -> Environ.env -> Evd.evar_map -> constr -> unit) -> unit
(* printing *)
val print_ltac : Libnames.qualid -> std_ppcmds
(* Internals that can be useful for syntax extensions. *)
exception CannotCoerceTo of string
val interp_ltac_var : (value -> 'a) -> interp_sign -> Environ.env option -> identifier located -> 'a
val interp_int : interp_sign -> identifier located -> int
val error_ltac_variable : loc -> identifier -> Environ.env option -> value -> string -> 'a
|
