blob: cdcb8bfd947530cf8a47c373fb38571267fc030b (
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
|
(************************************************************************)
(* 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: tacmach.mli 11639 2008-11-27 17:48:32Z barras $ i*)
(*i*)
open Names
open Term
open Sign
open Environ
open Evd
open Reduction
open Proof_trees
open Proof_type
open Refiner
open Redexpr
open Tacexpr
open Rawterm
(*i*)
(* Operations for handling terms under a local typing context. *)
type 'a sigma = 'a Evd.sigma;;
type validation = Proof_type.validation;;
type tactic = Proof_type.tactic;;
val sig_it : 'a sigma -> 'a
val project : goal sigma -> evar_map
val re_sig : 'a -> evar_map -> 'a sigma
val unpackage : 'a sigma -> evar_map ref * 'a
val repackage : evar_map ref -> 'a -> 'a sigma
val apply_sig_tac :
evar_map ref -> (goal sigma -> (goal list) sigma * validation) -> goal -> (goal list) * validation
val pf_concl : goal sigma -> types
val pf_env : goal sigma -> env
val pf_hyps : goal sigma -> named_context
(*i val pf_untyped_hyps : goal sigma -> (identifier * constr) list i*)
val pf_hyps_types : goal sigma -> (identifier * types) list
val pf_nth_hyp_id : goal sigma -> int -> identifier
val pf_last_hyp : goal sigma -> named_declaration
val pf_ids_of_hyps : goal sigma -> identifier list
val pf_global : goal sigma -> identifier -> constr
val pf_parse_const : goal sigma -> string -> constr
val pf_type_of : goal sigma -> constr -> types
val pf_check_type : goal sigma -> constr -> types -> unit
val hnf_type_of : goal sigma -> constr -> types
val pf_interp_constr : goal sigma -> Topconstr.constr_expr -> constr
val pf_interp_type : goal sigma -> Topconstr.constr_expr -> types
val pf_get_hyp : goal sigma -> identifier -> named_declaration
val pf_get_hyp_typ : goal sigma -> identifier -> types
val pf_get_new_id : identifier -> goal sigma -> identifier
val pf_get_new_ids : identifier list -> goal sigma -> identifier list
val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> constr
val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a
val pf_reduce :
(env -> evar_map -> constr -> constr) ->
goal sigma -> constr -> constr
val pf_whd_betadeltaiota : goal sigma -> constr -> constr
val pf_whd_betadeltaiota_stack : goal sigma -> constr -> constr * constr list
val pf_hnf_constr : goal sigma -> constr -> constr
val pf_red_product : goal sigma -> constr -> constr
val pf_nf : goal sigma -> constr -> constr
val pf_nf_betaiota : goal sigma -> constr -> constr
val pf_reduce_to_quantified_ind : goal sigma -> types -> inductive * types
val pf_reduce_to_atomic_ind : goal sigma -> types -> inductive * types
val pf_compute : goal sigma -> constr -> constr
val pf_unfoldn : (Termops.occurrences * evaluable_global_reference) list
-> goal sigma -> constr -> constr
val pf_const_value : goal sigma -> constant -> constr
val pf_conv_x : goal sigma -> constr -> constr -> bool
val pf_conv_x_leq : goal sigma -> constr -> constr -> bool
type transformation_tactic = proof_tree -> (goal list * validation)
val frontier : transformation_tactic
(*s Functions for handling the state of the proof editor. *)
type pftreestate = Refiner.pftreestate
val proof_of_pftreestate : pftreestate -> proof_tree
val cursor_of_pftreestate : pftreestate -> int list
val is_top_pftreestate : pftreestate -> bool
val evc_of_pftreestate : pftreestate -> evar_map
val top_goal_of_pftreestate : pftreestate -> goal sigma
val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
val traverse : int -> pftreestate -> pftreestate
val weak_undo_pftreestate : pftreestate -> pftreestate
val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate
val solve_pftreestate : tactic -> pftreestate -> pftreestate
val mk_pftreestate : goal -> pftreestate
val extract_open_pftreestate : pftreestate -> constr * Termops.metamap
val extract_pftreestate : pftreestate -> constr
val first_unproven : pftreestate -> pftreestate
val last_unproven : pftreestate -> pftreestate
val nth_unproven : int -> pftreestate -> pftreestate
val node_prev_unproven : int -> pftreestate -> pftreestate
val node_next_unproven : int -> pftreestate -> pftreestate
val next_unproven : pftreestate -> pftreestate
val prev_unproven : pftreestate -> pftreestate
val top_of_tree : pftreestate -> pftreestate
val change_constraints_pftreestate :
evar_map -> pftreestate -> pftreestate
(*s The most primitive tactics. *)
val refiner : rule -> tactic
val introduction_no_check : identifier -> tactic
val internal_cut_no_check : bool -> identifier -> types -> tactic
val internal_cut_rev_no_check : bool -> identifier -> types -> tactic
val refine_no_check : constr -> tactic
val convert_concl_no_check : types -> cast_kind -> tactic
val convert_hyp_no_check : named_declaration -> tactic
val thin_no_check : identifier list -> tactic
val thin_body_no_check : identifier list -> tactic
val move_hyp_no_check :
bool -> identifier -> identifier move_location -> tactic
val rename_hyp_no_check : (identifier*identifier) list -> tactic
val order_hyps : identifier list -> tactic
val mutual_fix :
identifier -> int -> (identifier * int * constr) list -> tactic
val mutual_cofix : identifier -> (identifier * constr) list -> tactic
(*s The most primitive tactics with consistency and type checking *)
val introduction : identifier -> tactic
val internal_cut : bool -> identifier -> types -> tactic
val internal_cut_rev : bool -> identifier -> types -> tactic
val refine : constr -> tactic
val convert_concl : types -> cast_kind -> tactic
val convert_hyp : named_declaration -> tactic
val thin : identifier list -> tactic
val thin_body : identifier list -> tactic
val move_hyp : bool -> identifier -> identifier move_location -> tactic
val rename_hyp : (identifier*identifier) list -> tactic
(*s Tactics handling a list of goals. *)
type validation_list = proof_tree list -> proof_tree list
type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
val first_goal : 'a list sigma -> 'a sigma
val goal_goal_list : 'a sigma -> 'a list sigma
val apply_tac_list : tactic -> tactic_list
val then_tactic_list : tactic_list -> tactic_list -> tactic_list
val tactic_list_tactic : tactic_list -> tactic
val tclFIRSTLIST : tactic_list list -> tactic_list
val tclIDTAC_list : tactic_list
(*s Pretty-printing functions (debug only). *)
val pr_gls : goal sigma -> Pp.std_ppcmds
val pr_glls : goal list sigma -> Pp.std_ppcmds
|
