blob: 4d1edc7e5b0ef31efbd83faaa98a0c26f9b426ad (
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
|
(* $Id$ *)
(*i*)
open Term
open Sign
open Proof_trees
(*i*)
(* The refiner (handles primitive rules and high-level tactics). *)
type 'a sigma = {
it : 'a ;
sigma : global_constraints }
val sig_it : 'a sigma -> 'a
val sig_sig : 'a sigma -> global_constraints
val project_with_focus : goal sigma -> readable_constraints
val unpackage : 'a sigma -> global_constraints ref * 'a
val repackage : global_constraints ref -> 'a -> 'a sigma
val apply_sig_tac :
global_constraints ref -> ('a sigma -> 'b sigma * 'c) -> 'a -> 'b * 'c
type validation = (proof_tree list -> proof_tree)
type tactic = goal sigma -> (goal list sigma * validation)
type transformation_tactic = proof_tree -> (goal list * validation)
val add_tactic : string -> (tactic_arg list -> tactic) -> unit
val overwriting_add_tactic : string -> (tactic_arg list -> tactic) -> unit
val lookup_tactic : string -> (tactic_arg list) -> tactic
val hide_tactic :
string -> (tactic_arg list -> tactic) -> (tactic_arg list -> tactic)
val overwrite_hidden_tactic :
string -> (tactic_arg list -> tactic) -> (tactic_arg list -> tactic)
val refiner : rule -> tactic
val context : ctxtty -> tactic
val vernac_tactic : tactic_expression -> tactic
val frontier : transformation_tactic
val list_pf : proof_tree -> goal list
val unTAC : tactic -> goal sigma -> proof_tree sigma
val extract_open_proof :
typed_type signature -> proof_tree -> constr * (int * constr) list
(*s Tacticals. *)
val tclIDTAC : tactic
val tclORELSE : tactic -> tactic -> tactic
val tclTHEN : tactic -> tactic -> tactic
val tclTHENLIST : tactic list -> tactic
val tclTHEN_i : tactic -> (int -> tactic) -> int -> tactic
val tclTHENL : tactic -> tactic -> tactic
val tclTHENS : tactic -> tactic list -> tactic
val tclTHENSI : tactic -> tactic list -> tactic
val tclREPEAT : tactic -> tactic
val tclFIRST : tactic list -> tactic
val tclSOLVE : tactic list -> tactic
val tclTRY : tactic -> tactic
val tclTHENTRY : tactic -> tactic -> tactic
val tclCOMPLETE : tactic -> tactic
val tclAT_LEAST_ONCE : tactic -> tactic
val tclFAIL : tactic
val tclDO : int -> tactic -> tactic
val tclPROGRESS : tactic -> tactic
val tclWEAK_PROGRESS : tactic -> tactic
val tclNOTSAMEGOAL : tactic -> tactic
val tclINFO : tactic -> 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 tclFIRSTLIST : tactic_list list -> tactic_list
val tclIDTAC_list : tactic_list
val first_goal : 'a list sigma -> 'a 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 goal_goal_list : 'a sigma -> 'a list sigma
(*s Functions for handling the state of the proof editor. *)
type 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 -> global_constraints
val top_goal_of_pftreestate : pftreestate -> goal sigma
val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
val traverse : int -> pftreestate -> pftreestate
val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate
val solve_pftreestate : tactic -> pftreestate -> pftreestate
(* a weak version of logical undoing, that is really correct only *)
(* if there are no existential variables. *)
val weak_undo_pftreestate : pftreestate -> pftreestate
val mk_pftreestate : goal -> pftreestate
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
: global_constraints -> pftreestate -> pftreestate
(*s Pretty-printers. *)
(*i*)
open Pp
(*i*)
val print_proof : evar_declarations -> var_context -> proof_tree -> std_ppcmds
val pr_rule : rule -> std_ppcmds
val pr_tactic : tactic_expression -> std_ppcmds
val print_script :
bool -> evar_declarations -> var_context -> proof_tree -> std_ppcmds
val print_treescript :
evar_declarations -> var_context -> proof_tree -> std_ppcmds
|
