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
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Stm
module Util : sig
val simple_goal : Evd.evar_map -> Evar.t -> Evar.t list -> bool
val is_focused_goal_simple : doc:Stm.doc -> Stateid.t -> [ `Simple of Evar.t list | `Not ]
type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ]
val crawl :
document_view -> ?init:document_node option ->
('a -> document_node -> 'a until) -> 'a ->
static_block_declaration option
val unit_val : Stm.DynBlockData.t
val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t
val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t
val of_vernac_control_val : Vernacexpr.vernac_control -> Stm.DynBlockData.t
val to_vernac_control_val : Stm.DynBlockData.t -> Vernacexpr.vernac_control
end = struct
let unit_tag = DynBlockData.create "unit"
let unit_val = DynBlockData.Easy.inj () unit_tag
let of_bullet_val, to_bullet_val = DynBlockData.Easy.make_dyn "bullet"
let of_vernac_control_val, to_vernac_control_val = DynBlockData.Easy.make_dyn "vernac_control"
let simple_goal sigma g gs =
let open Evar in
let open Evd in
let open Evarutil in
let () = assert (not @@ Evd.is_defined sigma g) in
let evi = Evd.find_undefined sigma g in
Set.is_empty (evars_of_term sigma (Evd.evar_concl evi)) &&
Set.is_empty (evars_of_filtered_evar_info sigma (nf_evar_info sigma evi)) &&
not (List.exists (Proofview.depends_on sigma g) gs)
let is_focused_goal_simple ~doc id =
match state_of_id ~doc id with
| Expired | Error _ | Valid None -> `Not
| Valid (Some { interp = { Vernacstate.Interp.lemmas } }) ->
Option.cata (Vernacstate.LemmaStack.with_top ~f:(fun proof ->
let proof = Declare.Proof.get proof in
let Proof.{ goals=focused; stack=r1; sigma } = Proof.data proof in
let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ (Evd.shelf sigma) @ (Evar.Set.elements @@ Evd.given_up sigma) in
if List.for_all (fun x -> simple_goal sigma x rest) focused
then `Simple focused
else `Not)) `Not lemmas
type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ]
let crawl { entry_point; prev_node } ?(init=Some entry_point) f acc =
let rec crawl node acc =
match node with
| None -> None
| Some node ->
match f acc node with
| `Stop -> None
| `Found x -> Some x
| `Cont acc -> crawl (prev_node node) acc in
crawl init acc
end
include Util
(* ****************** - foo - bar - baz *********************************** *)
let static_bullet ({ entry_point; prev_node } as view) =
let open Vernacexpr in
assert (not (Vernacprop.has_query_control entry_point.ast));
match entry_point.ast.CAst.v.expr with
| VernacSynPure (VernacBullet b) ->
let base = entry_point.indentation in
let last_tac = prev_node entry_point in
crawl view ~init:last_tac (fun prev node ->
if node.indentation < base then `Stop else
if node.indentation > base then `Cont node else
if Vernacprop.has_query_control node.ast then `Stop
else match node.ast.CAst.v.expr with
| VernacSynPure (VernacBullet b') when b = b' ->
`Found { block_stop = entry_point.id; block_start = prev.id;
dynamic_switch = node.id; carry_on_data = of_bullet_val b }
| _ -> `Stop) entry_point
| _ -> assert false
let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } =
match is_focused_goal_simple ~doc id with
| `Simple focused ->
ValidBlock {
base_state = id;
goals_to_admit = focused;
recovery_command = Some (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacSynPure (VernacBullet (to_bullet_val b))})
}
| `Not -> Leaks
let () = register_proof_block_delimiter
"bullet" static_bullet dynamic_bullet
(* ******************** { block } ***************************************** *)
let static_curly_brace ({ entry_point; prev_node } as view) =
let open Vernacexpr in
assert(entry_point.ast.CAst.v.expr = VernacSynPure VernacEndSubproof);
crawl view (fun (nesting,prev) node ->
if Vernacprop.has_query_control node.ast then `Cont (nesting,node)
else match node.ast.CAst.v.expr with
| VernacSynPure (VernacSubproof _) when nesting = 0 ->
`Found { block_stop = entry_point.id; block_start = prev.id;
dynamic_switch = node.id; carry_on_data = unit_val }
| VernacSynPure (VernacSubproof _) ->
`Cont (nesting - 1,node)
| VernacSynPure VernacEndSubproof ->
`Cont (nesting + 1,node)
| _ -> `Cont (nesting,node)) (-1, entry_point)
let dynamic_curly_brace doc { dynamic_switch = id } =
match is_focused_goal_simple ~doc id with
| `Simple focused ->
ValidBlock {
base_state = id;
goals_to_admit = focused;
recovery_command = Some (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacSynPure VernacEndSubproof })
}
| `Not -> Leaks
let () = register_proof_block_delimiter
"curly" static_curly_brace dynamic_curly_brace
(* ***************** par: ************************************************* *)
let static_par { entry_point; prev_node } =
match prev_node entry_point with
| None -> None
| Some { id = pid } ->
Some { block_stop = entry_point.id; block_start = pid;
dynamic_switch = pid; carry_on_data = unit_val }
let dynamic_par doc { dynamic_switch = id } =
match is_focused_goal_simple ~doc id with
| `Simple focused ->
ValidBlock {
base_state = id;
goals_to_admit = focused;
recovery_command = None;
}
| `Not -> Leaks
let () = register_proof_block_delimiter "par" static_par dynamic_par
(* ***************** simple indentation *********************************** *)
let static_indent ({ entry_point; prev_node } as view) =
Printf.eprintf "@%d\n" (Stateid.to_int entry_point.id);
match prev_node entry_point with
| None -> None
| Some last_tac ->
if last_tac.indentation <= entry_point.indentation then None
else
crawl view ~init:(Some last_tac) (fun prev node ->
if node.indentation >= last_tac.indentation then `Cont node
else
`Found { block_stop = entry_point.id; block_start = node.id;
dynamic_switch = node.id;
carry_on_data = of_vernac_control_val entry_point.ast }
) last_tac
let dynamic_indent doc { dynamic_switch = id; carry_on_data = e } =
Printf.eprintf "%s\n" (Stateid.to_string id);
match is_focused_goal_simple ~doc id with
| `Simple [] -> Leaks
| `Simple focused ->
let but_last = List.tl (List.rev focused) in
ValidBlock {
base_state = id;
goals_to_admit = but_last;
recovery_command = Some (to_vernac_control_val e);
}
| `Not -> Leaks
let () = register_proof_block_delimiter "indent" static_indent dynamic_indent
|
