Source file auto.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
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
open Pp
open Util
open Names
open Termops
open Tactics
open Proofview.Notations
open Hints
let compute_secvars gl =
let hyps = Proofview.Goal.hyps gl in
secvars_of_hyps hyps
open Unification
let auto_core_unif_flags_of st1 st2 = {
modulo_conv_on_closed_terms = Some st1;
use_metas_eagerly_in_conv_on_closed_terms = true;
use_evars_eagerly_in_conv_on_closed_terms = false;
modulo_delta = st2;
modulo_delta_types = TransparentState.full;
check_applied_meta_types = false;
use_pattern_unification = false;
use_meta_bound_pattern_unification = true;
allowed_evars = Evarsolve.AllowedEvars.all;
restrict_conv_on_strict_subterms = false;
modulo_betaiota = false;
modulo_eta = true;
}
let auto_unif_flags_of st1 st2 =
let flags = auto_core_unif_flags_of st1 st2 in {
core_unify_flags = flags;
merge_unify_flags = flags;
subterm_unify_flags = { flags with modulo_delta = TransparentState.empty };
allow_K_in_toplevel_higher_order_unification = false;
resolve_evars = true
}
let auto_unif_flags =
auto_unif_flags_of TransparentState.full TransparentState.empty
let unify_resolve flags h = Hints.hint_res_pf ~flags h
let unify_resolve_nodelta h = Hints.hint_res_pf ~flags:auto_unif_flags h
let exact h =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let sigma, c = Hints.fresh_hint env sigma h in
let sigma, t = Typing.type_of env sigma c in
let concl = Proofview.Goal.concl gl in
if occur_existential sigma t || occur_existential sigma concl then
let sigma = Evd.clear_metas sigma in
try
let sigma = Unification.w_unify env sigma CONV ~flags:auto_unif_flags concl t in
Proofview.Unsafe.tclEVARSADVANCE sigma <*>
exact_no_check c
with e when CErrors.noncritical e -> Proofview.tclZERO e
else Proofview.Unsafe.tclEVARS sigma <*> exact_check c
end
let conclPattern concl pat tac =
let constr_bindings env sigma =
match pat with
| None -> Proofview.tclUNIT Id.Map.empty
| Some pat ->
try
Proofview.tclUNIT (Constr_matching.matches env sigma pat concl)
with Constr_matching.PatternMatchingFailure as exn ->
let _, info = Exninfo.capture exn in
Tacticals.tclZEROMSG ~info (str "pattern-matching failed")
in
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
constr_bindings env sigma >>= fun constr_bindings ->
Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
let open Genarg in
let open Geninterp in
let inj c = match val_tag (topwit Stdarg.wit_constr) with
| Val.Base tag -> Val.Dyn (tag, c)
| _ -> assert false
in
let fold id c accu = Id.Map.add id (inj c) accu in
let lfun = Id.Map.fold fold constr_bindings Id.Map.empty in
let ist = { lfun
; poly
; extra = TacStore.empty } in
match tac with
| GenArg (Glbwit wit, tac) ->
Ftactic.run (Geninterp.interp wit ist tac) (fun _ -> Proofview.tclUNIT ())
end
(** A debugging / verbosity framework for trivial and auto *)
(** The following options allow to trigger debugging/verbosity
without having to adapt the scripts.
Note: if Debug and Info are both activated, Debug take precedence. *)
let global_debug_trivial = ref false
let global_debug_auto = ref false
let global_info_trivial = ref false
let global_info_auto = ref false
let add_option ls refe =
Goptions.(declare_bool_option
{ optdepr = false;
optkey = ls;
optread = (fun () -> !refe);
optwrite = (:=) refe })
let () =
add_option ["Debug";"Trivial"] global_debug_trivial;
add_option ["Debug";"Auto"] global_debug_auto;
add_option ["Info";"Trivial"] global_info_trivial;
add_option ["Info";"Auto"] global_info_auto
type debug_kind = ReportForTrivial | ReportForAuto
let no_dbg (_,whatfor,_,_) = (Off,whatfor,0,ref [])
let mk_trivial_dbg debug =
let d =
if debug == Debug || !global_debug_trivial then Debug
else if debug == Info || !global_info_trivial then Info
else Off
in (d,ReportForTrivial,0,ref [])
let mk_auto_dbg debug =
let d =
if debug == Debug || !global_debug_auto then Debug
else if debug == Info || !global_info_auto then Info
else Off
in (d,ReportForAuto,0,ref [])
let incr_dbg = function (dbg,whatfor,depth,trace) -> (dbg,whatfor,depth+1,trace)
(** A tracing tactic for debug/info trivial/auto *)
let tclLOG (dbg,_,depth,trace) pp tac =
match dbg with
| Off -> tac
| Debug ->
let s = String.make (depth+1) '*' in
Proofview.(tclIFCATCH (
tac >>= fun v ->
tclENV >>= fun env ->
tclEVARMAP >>= fun sigma ->
Feedback.msg_notice (str s ++ spc () ++ pp env sigma ++ str ". (*success*)");
tclUNIT v
) tclUNIT
(fun (exn, info) ->
tclENV >>= fun env ->
tclEVARMAP >>= fun sigma ->
Feedback.msg_notice (str s ++ spc () ++ pp env sigma ++ str ". (*fail*)");
tclZERO ~info exn))
| Info ->
Proofview.(tclIFCATCH (
tac >>= fun v ->
trace := (depth, Some pp) :: !trace;
tclUNIT v
) Proofview.tclUNIT
(fun (exn, info) ->
trace := (depth, None) :: !trace;
tclZERO ~info exn))
(** For info, from the linear trace information, we reconstitute the part
of the proof tree we're interested in. The last executed tactic
comes first in the trace (and it should be a successful one).
[depth] is the root depth of the tree fragment we're visiting.
[keep] means we're in a successful tree fragment (the very last
tactic has been successful). *)
let rec cleanup_info_trace depth acc = function
| [] -> acc
| (d,Some pp) :: l -> cleanup_info_trace d ((d,pp)::acc) l
| l -> cleanup_info_trace depth acc (erase_subtree depth l)
and erase_subtree depth = function
| [] -> []
| (d,_) :: l -> if Int.equal d depth then l else erase_subtree depth l
let pr_info_atom env sigma (d,pp) =
str (String.make d ' ') ++ pp env sigma ++ str "."
let pr_info_trace env sigma = function
| (Info,_,_,{contents=(d,Some pp)::l}) ->
Feedback.msg_notice (prlist_with_sep fnl (pr_info_atom env sigma) (cleanup_info_trace d [(d,pp)] l))
| _ -> ()
let pr_info_nop = function
| (Info,_,_,_) -> Feedback.msg_notice (str "idtac.")
| _ -> ()
let = function
| (Off,_,_,_) -> ()
| (Debug,ReportForTrivial,_,_) -> Feedback.msg_notice (str "(* debug trivial: *)")
| (Debug,ReportForAuto,_,_) -> Feedback.msg_notice (str "(* debug auto: *)")
| (Info,ReportForTrivial,_,_) -> Feedback.msg_notice (str "(* info trivial: *)")
| (Info,ReportForAuto,_,_) -> Feedback.msg_notice (str "(* info auto: *)")
let tclTRY_dbg d tac =
let delay f = Proofview.tclUNIT () >>= fun () -> f () in
let tac =
delay (fun () -> pr_dbg_header d; tac) >>= fun () ->
Proofview.tclENV >>= fun env ->
Proofview.tclEVARMAP >>= fun sigma ->
pr_info_trace env sigma d;
Proofview.tclUNIT () in
let after = delay (fun () -> pr_info_nop d; Proofview.tclUNIT ()) in
Tacticals.tclORELSE0 tac after
let auto_flags_of_state st =
auto_unif_flags_of TransparentState.full st
let hintmap_of env sigma secvars hdc concl =
match hdc with
| None -> Hint_db.map_none ~secvars
| Some hdc ->
if occur_existential sigma concl then
(fun db -> match Hint_db.map_eauto env sigma ~secvars hdc concl db with
| ModeMatch (_, l) -> l
| ModeMismatch -> [])
else Hint_db.map_auto env sigma ~secvars hdc concl
let exists_evaluable_reference env = function
| Tacred.EvalConstRef _ -> true
| Tacred.EvalVarRef v -> try ignore(Environ.lookup_named v env); true with Not_found -> false
let dbg_intro dbg = tclLOG dbg (fun _ _ -> str "intro") intro
let dbg_assumption dbg = tclLOG dbg (fun _ _ -> str "assumption") assumption
let intro_register dbg kont db =
Proofview.tclTHEN (dbg_intro dbg) @@
Proofview.Goal.enter begin fun gl ->
let extend_local_db decl db =
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
push_resolve_hyp env sigma (Context.Named.Declaration.get_id decl) db
in
Tacticals.onLastDecl (fun decl -> kont (extend_local_db decl db))
end
let rec trivial_fail_db dbg db_list local_db =
Proofview.tclINDEPENDENT @@
Tacticals.tclORELSE0 (dbg_assumption dbg) @@
Tacticals.tclORELSE0 (intro_register dbg (trivial_fail_db dbg db_list) local_db) @@
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let concl = Proofview.Goal.concl gl in
let secvars = compute_secvars gl in
let hdc = try Some (decompose_app_bound sigma concl) with Bound -> None in
let hintmap = hintmap_of env sigma secvars hdc concl in
let hinttac = tac_of_hint dbg db_list local_db concl in
(local_db::db_list)
|> List.map_append (fun db -> try hintmap db with Not_found -> [])
|> List.filter_map begin fun h ->
if Int.equal (FullHint.priority h) 0 then
Some (Tacticals.tclCOMPLETE (hinttac h))
else None
end
|> Tacticals.tclFIRST
end
and tac_of_hint dbg db_list local_db concl =
let tactic = function
| Res_pf h -> unify_resolve_nodelta h
| ERes_pf _ -> Proofview.Goal.enter (fun gl ->
let info = Exninfo.reify () in
Tacticals.tclZEROMSG ~info (str "eres_pf"))
| Give_exact h -> exact h
| Res_pf_THEN_trivial_fail h ->
Tacticals.tclTHEN
(unify_resolve_nodelta h)
(trivial_fail_db (no_dbg dbg) db_list local_db)
| Unfold_nth c ->
Proofview.Goal.enter begin fun gl ->
if exists_evaluable_reference (Proofview.Goal.env gl) c then
Tacticals.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)
else
let info = Exninfo.reify () in
Tacticals.tclFAIL ~info (str"Unbound reference")
end
| Extern (p, tacast) ->
conclPattern concl p tacast
in
let pr_hint h env sigma =
let origin = match FullHint.database h with
| None -> mt ()
| Some n -> str " (in " ++ str n ++ str ")"
in
FullHint.print env sigma h ++ origin
in
fun h -> tclLOG dbg (pr_hint h) (FullHint.run h tactic)
(** The use of the "core" database can be de-activated by passing
"nocore" amongst the databases. *)
let gen_trivial ?(debug=Off) lems dbnames =
Hints.wrap_hint_warning @@
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let db_list =
match dbnames with
| Some dbnames -> make_db_list dbnames
| None -> current_pure_db ()
in
let d = mk_trivial_dbg debug in
let local_db = make_local_hint_db env sigma false lems in
tclTRY_dbg d (trivial_fail_db d db_list local_db)
end
let trivial ?(debug=Off) lems dbnames = gen_trivial ~debug lems (Some dbnames)
let full_trivial ?(debug=Off) lems = gen_trivial ~debug lems None
let h_trivial ?(debug=Off) lems dbnames = gen_trivial ~debug lems dbnames
exception SearchBound
let search d n db_list lems =
let make_local_db gl =
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
make_local_hint_db env sigma false lems
in
let rec search d n local_db =
if Int.equal n 0 then
let info = Exninfo.reify () in
Proofview.tclZERO ~info SearchBound
else
Tacticals.tclORELSE0 (dbg_assumption d) @@
Tacticals.tclORELSE0 (intro_register d (search d n) local_db) @@
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let concl = Proofview.Goal.concl gl in
let hyps = Proofview.Goal.hyps gl in
let d' = incr_dbg d in
let secvars = compute_secvars gl in
let hdc = try Some (decompose_app_bound sigma concl) with Bound -> None in
let hintmap = hintmap_of env sigma secvars hdc concl in
let hinttac = tac_of_hint d db_list local_db concl in
(local_db::db_list)
|> List.map_append (fun db -> try hintmap db with Not_found -> [])
|> List.map begin fun h ->
Proofview.tclTHEN (hinttac h) @@
Proofview.Goal.enter begin fun gl ->
let hyps' = Proofview.Goal.hyps gl in
let local_db' =
if hyps' == hyps then local_db else make_local_db gl
in
search d' (n-1) local_db'
end
end
|> Tacticals.tclFIRST
end
in
Proofview.Goal.enter begin fun gl ->
search d n (make_local_db gl)
end
let default_search_depth = ref 5
let gen_auto ?(debug=Off) n lems dbnames =
Hints.wrap_hint_warning @@
Proofview.Goal.enter begin fun gl ->
let n = match n with None -> !default_search_depth | Some n -> n in
let db_list =
match dbnames with
| Some dbnames -> make_db_list dbnames
| None -> current_pure_db ()
in
let d = mk_auto_dbg debug in
tclTRY_dbg d (search d n db_list lems)
end
let auto ?(debug=Off) n lems dbnames = gen_auto ~debug (Some n) lems (Some dbnames)
let default_auto = auto !default_search_depth [] []
let full_auto ?(debug=Off) n lems = gen_auto ~debug (Some n) lems None
let default_full_auto = full_auto !default_search_depth []
let h_auto ?(debug=Off) n lems l = gen_auto ~debug n lems l