blob: eb31544cbc73c0ec0eb5a751628900b3f01d0c17 (
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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(*i $Id$ i*)
(*i*)
open Environ
open Evd
open Names
open Stamps
open Term
open Util
(*i*)
(* This module defines the structure of proof tree and the tactic type. So, it
is used by [Proof_tree] and [Refiner] *)
type bindOcc =
| Dep of identifier
| NoDep of int
| Com
type 'a substitution = (bindOcc * 'a) list
type pf_status =
| Complete_proof
| Incomplete_proof
type hyp_location = (* To distinguish body and type of local defs *)
| InHyp of identifier
| InHypType of identifier
type prim_rule_name =
| Intro
| Intro_after
| Intro_replacing
| Cut of bool
| Fix
| Cofix
| Refine
| Convert_concl
| Convert_hyp
| Convert_defbody
| Convert_deftype
| Thin
| ThinBody
| Move of bool
type prim_rule = {
name : prim_rule_name;
hypspecs : identifier list;
newids : identifier list;
params : Coqast.t list;
terms : constr list }
type local_constraints = Intset.t
type ctxtty = {
pgm : constr option;
lc : local_constraints }
type enamed_declarations = ctxtty evar_map
(* A global constraint is a mappings of existential variables
with some extra information for the program tactic *)
type global_constraints = enamed_declarations timestamped
(* The type [goal sigma] is the type of subgoal. It has the following form
\begin{verbatim}
it = { evar_concl = [the conclusion of the subgoal]
evar_hyps = [the hypotheses of the subgoal]
evar_body = Evar_Empty;
evar_info = { pgm : [The Realizer pgm if any]
lc : [Set of evar num occurring in subgoal] }}
sigma = { stamp = [an int characterizing the ed field, for quick compare]
ed : [A set of existential variables depending in the subgoal]
number of first evar,
it = { evar_concl = [the type of first evar]
evar_hyps = [the context of the evar]
evar_body = [the body of the Evar if any]
evar_info = { pgm : [Useless ??]
lc : [Set of evars occurring
in the type of evar] } };
...
number of last evar,
it = { evar_concl = [the type of evar]
evar_hyps = [the context of the evar]
evar_body = [the body of the Evar if any]
evar_info = { pgm : [Useless ??]
lc : [Set of evars occurring
in the type of evar] } } }
}
\end{verbatim}
*)
(* The type constructor ['a sigma] adds an evar map to an object of
type ['a] (see below the form of a [goal sigma] *)
type 'a sigma = {
it : 'a ;
sigma : global_constraints }
(*s Proof trees.
[ref] = [None] if the goal has still to be proved,
and [Some (r,l)] if the rule [r] was applied to the goal
and gave [l] as subproofs to be completed.
[subproof] = [(Some p)] if [ref = (Some(Tactic t,l))];
[p] is then the proof that the goal can be proven if the goals
in [l] are solved. *)
type proof_tree = {
status : pf_status;
goal : goal;
ref : (rule * proof_tree list) option;
subproof : proof_tree option }
and rule =
| Prim of prim_rule
| Tactic of tactic_expression
| Context of ctxtty
| Local_constraints of local_constraints
and goal = ctxtty evar_info
and tactic = goal sigma -> (goal list sigma * validation)
and validation = (proof_tree list -> proof_tree)
and tactic_arg =
| Command of Coqast.t
| Constr of constr
| OpenConstr of Pretyping.open_constr
| Constr_context of constr
| Identifier of identifier
| Qualid of Nametab.qualid
| Integer of int
| Clause of hyp_location list
| Bindings of Coqast.t substitution
| Cbindings of constr substitution
| Quoted_string of string
| Tacexp of Coqast.t
| Tac of tactic * Coqast.t
| Redexp of Tacred.red_expr
| Fixexp of identifier * int * Coqast.t
| Cofixexp of identifier * Coqast.t
| Letpatterns of (int list option * (identifier * int list) list)
| Intropattern of intro_pattern
and intro_pattern =
| WildPat
| IdPat of identifier
| DisjPat of intro_pattern list
| ConjPat of intro_pattern list
| ListPat of intro_pattern list
and tactic_expression = string * tactic_arg list
|
