blob: 7b612ac5fcd6d66609d7951b76ac340acc2b3368 (
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
|
(* $Id$ *)
(*i*)
open Util
open Stamps
open Names
open Term
open Sign
open Evd
open Environ
(*i*)
(* This module declares the structure of proof trees, global and
readable constraints, and a few utilities on these types *)
type bindOcc =
| Dep of identifier
| NoDep of int
| Com
type 'a substitution = (bindOcc * 'a) list
type tactic_arg =
| Command of Coqast.t
| Constr of constr
| Identifier of identifier
| Integer of int
| Clause of identifier list
| Bindings of Coqast.t substitution
| Cbindings of constr substitution
| Quoted_string of string
| Tacexp of Coqast.t
| Redexp of string * Coqast.t list
| 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 =
| 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
type pf_status = Complete_proof | Incomplete_proof
type prim_rule_name =
| Intro
| Intro_after
| Intro_replacing
| Fix
| Cofix
| Refine
| Convert_concl
| Convert_hyp
| Thin
| 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
(*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 goal = ctxtty evar_info
and rule =
| Prim of prim_rule
| Tactic of tactic_expression
| Context of ctxtty
| Local_constraints of local_constraints
and ctxtty = {
pgm : constr option;
mimick : proof_tree option;
lc : local_constraints }
type evar_declarations = ctxtty evar_map
val mk_goal : ctxtty -> env -> constr -> goal
val mt_ctxt : local_constraints -> ctxtty
val get_ctxt : goal -> ctxtty
val get_pgm : goal -> constr option
val set_pgm : constr option -> ctxtty -> ctxtty
val get_mimick : goal -> proof_tree option
val set_mimick : proof_tree option -> ctxtty -> ctxtty
val get_lc : goal -> local_constraints
val rule_of_proof : proof_tree -> rule
val ref_of_proof : proof_tree -> (rule * proof_tree list)
val children_of_proof : proof_tree -> proof_tree list
val goal_of_proof : proof_tree -> goal
val subproof_of_proof : proof_tree -> proof_tree
val status_of_proof : proof_tree -> pf_status
val is_complete_proof : proof_tree -> bool
val is_leaf_proof : proof_tree -> bool
val is_tactic_proof : proof_tree -> bool
(*s A global constraint is a mappings of existential variables with
some extra information for the program and mimick tactics. *)
type global_constraints = evar_declarations timestamped
(*s A readable constraint is a global constraint plus a focus set
of existential variables and a signature. *)
type evar_recordty = {
focus : local_constraints;
env : env;
decls : evar_declarations }
and readable_constraints = evar_recordty timestamped
val rc_of_gc : global_constraints -> goal -> readable_constraints
val rc_add : readable_constraints -> int * goal -> readable_constraints
val get_env : readable_constraints -> env
val get_focus : readable_constraints -> local_constraints
val get_decls : readable_constraints -> evar_declarations
val get_gc : readable_constraints -> global_constraints
val remap : readable_constraints -> int * goal -> readable_constraints
val ctxt_access : readable_constraints -> int -> bool
|
