blob: 68f6f6aced96aa5fc35d1adf1782400293f877b7 (
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
|
(************************************************************************)
(* 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: tacinterp.mli 7841 2006-01-11 11:24:54Z herbelin $ i*)
(*i*)
open Dyn
open Pp
open Names
open Proof_type
open Tacmach
open Tactic_debug
open Term
open Tacexpr
open Genarg
open Topconstr
open Mod_subst
(*i*)
(* Values for interpretation *)
type value =
| VTactic of Util.loc * tactic (* For mixed ML/Ltac tactics (e.g. Tauto) *)
| VRTactic of (goal list sigma * validation)
| VFun of (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
| VRec of value ref
(* Signature for interpretation: val\_interp and interpretation functions *)
and interp_sign =
{ lfun : (identifier * value) list;
debug : debug_info }
(* Gives the identifier corresponding to an Identifier [tactic_arg] *)
val id_of_Identifier : Environ.env -> value -> identifier
(* Gives the constr corresponding to a Constr [value] *)
val constr_of_VConstr : Environ.env -> value -> constr
(* Transforms an id into a constr if possible *)
val constr_of_id : Environ.env -> identifier -> constr
(* To embed several objects in Coqast.t *)
val tacticIn : (interp_sign -> raw_tactic_expr) -> raw_tactic_expr
val tacticOut : raw_tactic_expr -> (interp_sign -> raw_tactic_expr)
val valueIn : value -> raw_tactic_arg
val valueOut: raw_tactic_arg -> value
val constrIn : constr -> constr_expr
val constrOut : constr_expr -> constr
(* 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 :
bool -> (identifier Util.located * raw_tactic_expr) list -> unit
val add_primitive_tactic : string -> glob_tactic_expr -> unit
(* 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 ->
closed_generic_argument) *
(substitution -> glob_generic_argument -> glob_generic_argument)
-> unit
val interp_genarg :
interp_sign -> goal sigma -> glob_generic_argument -> closed_generic_argument
val intern_genarg :
glob_sign -> raw_generic_argument -> glob_generic_argument
val intern_constr :
glob_sign -> constr_expr -> rawconstr_and_expr
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 redexp arguments *)
val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr
-> Redexpr.red_expr
(* Interprets tactic expressions *)
val interp_tac_gen : (identifier * value) list ->
debug_info -> raw_tactic_expr -> tactic
val interp_hyp : interp_sign -> goal sigma ->
identifier Util.located -> identifier
(* 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 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
|
