Source file ssrview.ml
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
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
open Util
open Names
open Context
open Ltac_plugin
open Proofview
open Notations
open Ssrcommon
open Ssrast
module AdaptorDb = struct
type kind = Forward | Backward | Equivalence
module AdaptorKind = struct
type t = kind
let compare = pervasives_compare
end
module AdaptorMap = Map.Make(AdaptorKind)
let term_view_adaptor_db =
Summary.ref ~name:"view_adaptor_db" AdaptorMap.empty
let get k =
try AdaptorMap.find k !term_view_adaptor_db
with Not_found -> []
let cache_adaptor (k, t) =
let lk = get k in
if not (List.exists (Glob_ops.glob_constr_eq t) lk) then
term_view_adaptor_db := AdaptorMap.add k (t :: lk) !term_view_adaptor_db
let subst_adaptor (subst, (k, t as a)) =
let t' = Detyping.subst_glob_constr (Global.env()) subst t in
if t' == t then a else k, t'
let in_db =
let open Libobject in
declare_object @@ global_object_nodischarge "VIEW_ADAPTOR_DB"
~cache:cache_adaptor
~subst:(Some subst_adaptor)
let declare kind terms =
List.iter (fun term -> Lib.add_leaf (in_db (kind,term)))
(List.rev terms)
end
let reduce_or l = tclUNIT (List.fold_left (||) false l)
module State : sig
val vsINIT : view:EConstr.t -> subject_name:Id.t list -> to_clear:Id.t list -> unit tactic
val vsPUSH : (EConstr.t -> (EConstr.t * Id.t list) tactic) -> unit tactic
val vsCONSUME : (names:Id.t list -> EConstr.t -> to_clear:Id.t list -> unit tactic) -> unit tactic
val vsCONSUME_IF_PRESENT : (names:Id.t list -> EConstr.t option -> to_clear:Id.t list -> bool tactic) -> bool tactic
val vsASSERT_EMPTY : unit tactic
end = struct
type vstate = {
subject_name : Id.t list;
view : EConstr.t;
to_clear : Id.t list;
}
include Ssrcommon.MakeState(struct
type state = vstate option
let init = None
end)
let vsINIT ~view ~subject_name ~to_clear =
tclSET (Some { subject_name; view; to_clear })
(** Initializes the state in which view data is accumulated when views are
applied to the first assumption in the goal *)
let vsBOOTSTRAP = Goal.enter_one ~__LOC__ begin fun gl ->
let concl = Goal.concl gl in
let id =
let open EConstr in
match kind_of_type (Goal.sigma gl) concl with
| ProdType({binder_name=Name.Name id}, _, _)
when Ssrcommon.is_discharged_id id -> id
| _ -> mk_anon_id "view_subject" (Tacmach.pf_ids_of_hyps gl) in
let view = EConstr.mkVar id in
Ssrcommon.tclINTRO_ID id <*>
tclSET (Some { subject_name = [id]; view; to_clear = [] })
end
let rec vsPUSH k =
tclINDEPENDENT (tclGET (function
| Some { subject_name; view; to_clear } ->
k view >>= fun (view, clr) ->
tclSET (Some { subject_name; view; to_clear = to_clear @ clr })
| None -> vsBOOTSTRAP <*> vsPUSH k))
let rec vsCONSUME k =
tclINDEPENDENT (tclGET (function
| Some { subject_name; view; to_clear } ->
tclSET None <*>
k ~names:subject_name view ~to_clear
| None -> vsBOOTSTRAP <*> vsCONSUME k))
let vsCONSUME_IF_PRESENT k =
tclINDEPENDENTL (tclGET1 (function
| Some { subject_name; view; to_clear } ->
tclSET None <*>
k ~names:subject_name (Some view) ~to_clear
| None -> k ~names:[] None ~to_clear:[])) >>= reduce_or
let vsASSERT_EMPTY =
tclGET (function
| Some _ -> anomaly ("vsASSERT_EMPTY: not empty")
| _ -> tclUNIT ())
end
let intern_constr_expr { Genintern.genv; ltacvars = vars } sigma ce =
let ltacvars = {
Constrintern.empty_ltac_sign with Constrintern.ltac_vars = vars } in
Constrintern.intern_gen Pretyping.WithoutTypeConstraint ~ltacvars genv sigma ce
let is_tac_in_term ? { annotation; body; glob_env; interp_env } =
Goal.(enter_one ~__LOC__ begin fun goal ->
let genv = env goal in
let sigma = sigma goal in
let ist = Ssrcommon.option_assert_get glob_env (Pp.str"not a term") in
let ist =
let open Genintern in
{
ltacvars = ist.ast_ltacvars;
extra = ist.ast_extra;
intern_sign = ist.ast_intern_sign;
genv;
strict_check = true;
}
in
let body =
match extra_scope with
| None -> body
| Some s -> CAst.make (Constrexpr.CDelimiters(s,body))
in
let g = intern_constr_expr ist sigma body in
match DAst.get g with
| Glob_term.GGenarg x
when Genarg.has_type x (Genarg.glbwit Tacarg.wit_tactic)
-> tclUNIT (`Tac (Genarg.out_gen (Genarg.glbwit Tacarg.wit_tactic) x))
| _ -> tclUNIT (`Term (annotation, interp_env, g))
end)
let tclINJ_CONSTR_IST ist p =
let fresh_id = Ssrcommon.mk_internal_id "ssr_inj_constr_in_glob" in
let ist = {
ist with Geninterp.lfun =
Id.Map.add fresh_id (Taccoerce.Value.of_constr p) ist.Geninterp.lfun} in
tclUNIT (ist,Glob_term.GVar fresh_id)
let mkGHole =
DAst.make
(Glob_term.GHole(Evar_kinds.InternalHole, Namegen.IntroAnonymous))
let rec mkGHoles n = if n > 0 then mkGHole :: mkGHoles (n - 1) else []
let mkGApp f args =
if args = [] then f
else DAst.make (Glob_term.GApp (f, args))
let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal ->
let env = Goal.env goal in
let sigma = Goal.sigma goal in
Ssrprinters.debug_ssr (fun () ->
Pp.(str"interp-in: " ++ Printer.pr_glob_constr_env env sigma glob));
try
let sigma,term = Tacinterp.interp_open_constr ist env sigma (glob,None) in
Ssrprinters.debug_ssr (fun () ->
Pp.(str"interp-out: " ++ Printer.pr_econstr_env env sigma term));
tclUNIT (env,sigma,term)
with e when CErrors.noncritical e ->
let e, info = Exninfo.capture e in
Ssrprinters.debug_ssr (fun () ->
Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env sigma glob));
tclZERO ~info e
end
let tclKeepOpenConstr (_env, sigma, t) = Unsafe.tclEVARS sigma <*> tclUNIT t
let tclADD_CLEAR_IF_ID (env, ist, t) x =
Ssrprinters.debug_ssr (fun () ->
Pp.(str"tclADD_CLEAR_IF_ID: " ++ Printer.pr_econstr_env env ist t));
let hd, args = EConstr.decompose_app ist t in
match EConstr.kind ist hd with
| Constr.Var id when Ssrcommon.not_section_id id -> tclUNIT (x, [id])
| _ -> tclUNIT (x,[])
let tclPAIR p x = tclUNIT (x, p)
let guess_max_implicits ist glob =
Proofview.tclORELSE
(interp_glob ist (mkGApp glob (mkGHoles 6)) >>= fun (env,sigma,term) ->
let term_ty = Retyping.get_type_of env sigma term in
let ctx, _ = Reductionops.hnf_decompose_prod env sigma term_ty in
tclUNIT (List.length ctx + 6))
(fun _ -> tclUNIT 5)
let pad_to_inductive ist glob = Goal.enter_one ~__LOC__ begin fun goal ->
interp_glob ist glob >>= fun (env, sigma, term as ot) ->
let term_ty = Retyping.get_type_of env sigma term in
let ctx, i = Reductionops.hnf_decompose_prod env sigma term_ty in
let rel_ctx =
List.map (fun (a,b) -> Context.Rel.Declaration.LocalAssum(a,b)) ctx in
if not (Ssrcommon.isAppInd (EConstr.push_rel_context rel_ctx env) sigma i)
then Tacticals.tclZEROMSG Pp.(str"not an inductive")
else tclUNIT (mkGApp glob (mkGHoles (List.length ctx)))
>>= tclADD_CLEAR_IF_ID ot
end
let interp_view ~clear_if_id ist v p =
let is_specialize hd =
match DAst.get hd with Glob_term.GHole _ -> true | _ -> false in
tclINJ_CONSTR_IST ist p >>= fun (ist, p_id) ->
let p_id = DAst.make p_id in
match DAst.get v with
| Glob_term.GApp (hd, rargs) when is_specialize hd ->
Ssrprinters.debug_ssr (fun () -> Pp.(str "specialize"));
interp_glob ist (mkGApp p_id rargs)
>>= tclKeepOpenConstr >>= tclPAIR []
| _ ->
Ssrprinters.debug_ssr (fun () -> Pp.(str "view"));
let adaptors = AdaptorDb.(get Forward) in
Proofview.tclORELSE
(pad_to_inductive ist v >>= fun (vpad,clr) ->
Ssrcommon.tclFIRSTa (List.map
(fun a -> interp_glob ist (mkGApp a [vpad; p_id])) adaptors)
>>= tclPAIR clr)
(fun _ ->
guess_max_implicits ist v >>= fun n ->
Ssrcommon.tclFIRSTi (fun n ->
interp_glob ist (mkGApp v (mkGHoles n @ [p_id]))) n
>>= fun x -> tclADD_CLEAR_IF_ID x x)
>>= fun (ot,clr) ->
if clear_if_id
then tclKeepOpenConstr ot >>= tclPAIR clr
else tclKeepOpenConstr ot >>= tclPAIR []
let pile_up_view ~clear_if_id (annotation, ist, v) =
let ist = Ssrcommon.option_assert_get ist (Pp.str"not a term") in
let clear_if_id = clear_if_id && annotation <> `Parens in
State.vsPUSH (fun p -> interp_view ~clear_if_id ist v p)
let finalize_view s0 ?(simple_types=true) p =
Goal.enter_one ~__LOC__ begin fun g ->
let env = Goal.env g in
let sigma = Goal.sigma g in
let evars_of_p = Evd.evars_of_term sigma p in
let filter x _ = Evar.Set.mem x evars_of_p in
let sigma = Evd.push_shelf sigma in
let sigma = Typeclasses.resolve_typeclasses ~fail:false ~filter env sigma in
let _, sigma = Evd.pop_shelf sigma in
let p = Reductionops.nf_evar sigma p in
let get_body : type a. a Evd.evar_body -> EConstr.t = function Evd.Evar_defined x -> x | Evd.Evar_empty -> assert false in
let evars_of_econstr sigma t =
Evarutil.undefined_evars_of_term sigma t in
let rigid_of s =
List.fold_left (fun l k ->
if Evd.is_defined sigma k then
let EvarInfo evi = Evd.find sigma k in
let bo = get_body (Evd.evar_body evi) in
k :: l @ Evar.Set.elements (evars_of_econstr sigma bo)
else l
) [] s in
let env0 = Proofview.Goal.env s0 in
let sigma0 = Proofview.Goal.sigma s0 in
let und0 =
let EvarInfo g0info = Evd.find sigma0 (Proofview.Goal.goal s0) in
let g0 = Evd.evars_of_filtered_evar_info sigma0 g0info in
List.filter (fun k -> Evar.Set.mem k g0)
(List.map fst (Evar.Map.bindings (Evd.undefined_map sigma0))) in
let rigid = rigid_of und0 in
let p, to_prune, _ucst = abs_evars env0 sigma0 ~rigid (sigma, p) in
let p = if simple_types then abs_cterm env0 sigma0 (List.length to_prune) p else p in
Ssrprinters.debug_ssr (fun () -> Pp.(str"view@finalized: " ++
Printer.pr_econstr_env env sigma p));
let sigma = List.fold_left Evd.remove sigma to_prune in
Unsafe.tclEVARS sigma <*>
tclUNIT p
end
let pose_proof subject_name p =
Tactics.generalize [p] <*>
begin match subject_name with
| id :: _ -> Ssrcommon.tclRENAME_HD_PROD (Name.Name id)
| _ -> tclUNIT() end
<*>
Tactics.reduce_after_refine
let rec apply_all_views_aux ~clear_if_id vs finalization conclusion s0 =
match vs with
| [] -> finalization s0 (fun name p ->
(match p with
| None -> conclusion ~to_clear:[]
| Some p ->
pose_proof name p <*> conclusion ~to_clear:name) <*>
tclUNIT false)
| v :: vs ->
Ssrprinters.debug_ssr (fun () -> Pp.(str"piling..."));
is_tac_in_term ~extra_scope:"ssripat" v >>= function
| `Term v ->
Ssrprinters.debug_ssr (fun () -> Pp.(str"..a term"));
pile_up_view ~clear_if_id v <*>
apply_all_views_aux ~clear_if_id vs finalization conclusion s0
| `Tac tac ->
Ssrprinters.debug_ssr (fun () -> Pp.(str"..a tactic"));
finalization s0 (fun name p ->
(match p with
| None -> tclUNIT ()
| Some p -> pose_proof name p) <*>
Tacinterp.eval_tactic tac <*>
if vs = [] then begin
Ssrprinters.debug_ssr (fun () -> Pp.(str"..was the last view"));
conclusion ~to_clear:name <*> tclUNIT true
end else
Tactics.clear name <*>
tclINDEPENDENTL begin
Ssrprinters.debug_ssr (fun () -> Pp.(str"..was NOT the last view"));
Proofview.Goal.enter_one begin fun gl ->
apply_all_views_aux ~clear_if_id vs finalization conclusion gl
end
end >>= reduce_or)
let apply_all_views vs ~conclusion ~clear_if_id =
let finalization s0 k =
State.vsCONSUME_IF_PRESENT (fun ~names t ~to_clear ->
match t with
| None -> k [] None
| Some t ->
finalize_view s0 t >>= fun p -> k (names @ to_clear) (Some p)) in
Proofview.Goal.enter_one begin fun gl ->
apply_all_views_aux ~clear_if_id vs finalization conclusion gl
end
let apply_all_views_to subject ~simple_types vs ~conclusion = begin
let rec process_all_vs = function
| [] -> tclUNIT ()
| v :: vs -> is_tac_in_term v >>= function
| `Tac _ -> Ssrcommon.errorstrm Pp.(str"tactic view not supported")
| `Term v -> pile_up_view ~clear_if_id:false v <*> process_all_vs vs in
State.vsASSERT_EMPTY <*>
State.vsINIT ~subject_name:[] ~to_clear:[] ~view:subject <*>
Proofview.Goal.enter_one begin fun s0 ->
process_all_vs vs <*>
State.vsCONSUME (fun ~names:_ t ~to_clear:_ ->
finalize_view s0 ~simple_types t >>= conclusion)
end
end
let tclIPAT_VIEWS ~views:vs ?(clear_if_id=false) ~conclusion () =
tclINDEPENDENTL begin
State.vsASSERT_EMPTY <*>
apply_all_views vs ~conclusion ~clear_if_id >>= fun was_tac ->
State.vsASSERT_EMPTY <*>
tclUNIT was_tac
end >>= reduce_or
let tclWITH_FWD_VIEWS ~simple_types ~subject ~views:vs ~conclusion =
tclINDEPENDENT (apply_all_views_to subject ~simple_types vs ~conclusion)