Source file internals.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
open Constr
open EConstr
open EConstr.Vars
open Names
open Tacexpr
open CErrors
open Util
open Termops
open Namegen
open Tactypes
open Tactics
open Proofview.Notations
let assert_succeeds tac =
let open Proofview in
let exception Succeeded in
tclORELSE (tclONCE tac <*> tclZERO Succeeded) (function
| Succeeded, _ -> tclUNIT ()
| exn, info -> tclZERO ~info exn)
let mytclWithHoles tac with_evars c =
Proofview.Goal.enter begin fun gl ->
let env = Tacmach.pf_env gl in
let sigma = Tacmach.project gl in
let sigma',c = Tactics.force_destruction_arg with_evars env sigma c in
Tacticals.tclWITHHOLES with_evars (tac with_evars (Some c)) sigma'
end
let with_delayed_uconstr ist c tac =
let flags = Pretyping.{
use_coercions = true;
use_typeclasses = NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
program_mode = false;
polymorphic = false;
} in
let c = Tacinterp.type_uconstr ~flags ist c in
Tacticals.tclDELAYEDWITHHOLES false c tac
let replace_in_clause_maybe_by ist c1 c2 cl tac =
with_delayed_uconstr ist c1
(fun c1 -> Equality.replace_in_clause_maybe_by c1 c2 cl (Option.map (Tacinterp.tactic_of_value ist) tac))
let replace_term ist dir_opt c cl =
with_delayed_uconstr ist c (fun c -> Equality.replace_term dir_opt c cl)
let elimOnConstrWithHoles tac with_evars c =
Tacticals.tclDELAYEDWITHHOLES with_evars c
(fun c -> tac with_evars (Some (None,ElimOnConstr c)))
let discr_main c = elimOnConstrWithHoles Equality.discr_tac false c
let discrHyp id =
Proofview.tclEVARMAP >>= fun sigma ->
discr_main (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings)))
let injection_main with_evars c =
elimOnConstrWithHoles (Equality.injClause None None) with_evars c
let injHyp id =
Proofview.tclEVARMAP >>= fun sigma ->
injection_main false (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings)))
let constr_flags () = Pretyping.{
use_coercions = true;
use_typeclasses = UseTC;
solve_unification_constraints = Proof.use_unification_heuristics ();
fail_evar = false;
expand_evars = true;
program_mode = false;
polymorphic = false;
}
let refine_tac ist ~simple ~with_classes c =
let with_classes = if with_classes then Pretyping.UseTC else Pretyping.NoUseTC in
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
let flags =
{ (constr_flags ()) with Pretyping.use_typeclasses = with_classes } in
let expected_type = Pretyping.OfType concl in
let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in
let update = begin fun sigma ->
c env sigma
end in
let refine = Refine.refine ~typecheck:false update in
if simple then refine
else refine <*>
Tactics.reduce_after_refine <*>
Proofview.shelve_unifiable
end
let subst_var_with_hole occ tid t =
let open Glob_term in
let open Glob_ops in
let occref = if occ > 0 then ref occ else Locusops.error_invalid_occurrence [occ] in
let locref = ref 0 in
let rec substrec x = match DAst.get x with
| GVar id ->
if Id.equal id tid
then
(decr occref;
if Int.equal !occref 0 then x
else
(incr locref;
DAst.make ~loc:(Loc.make_loc (!locref,0)) @@
GHole (Evar_kinds.QuestionMark {
Evar_kinds.qm_obligation=Evar_kinds.Define true;
Evar_kinds.qm_name=Anonymous;
Evar_kinds.qm_record_field=None;
}, IntroAnonymous, None)))
else x
| _ -> map_glob_constr_left_to_right substrec x in
let t' = substrec t
in
if !occref > 0 then Locusops.error_invalid_occurrence [occ] else t'
let subst_hole_with_term occ tc t =
let open Glob_term in
let open Glob_ops in
let locref = ref 0 in
let occref = ref occ in
let rec substrec c = match DAst.get c with
| GHole (Evar_kinds.QuestionMark {
Evar_kinds.qm_obligation=Evar_kinds.Define true;
Evar_kinds.qm_name=Anonymous;
Evar_kinds.qm_record_field=None;
}, IntroAnonymous, s) ->
decr occref;
if Int.equal !occref 0 then tc
else
(incr locref;
DAst.make ~loc:(Loc.make_loc (!locref,0)) @@
GHole (Evar_kinds.QuestionMark {
Evar_kinds.qm_obligation=Evar_kinds.Define true;
Evar_kinds.qm_name=Anonymous;
Evar_kinds.qm_record_field=None;
},IntroAnonymous,s))
| _ -> map_glob_constr_left_to_right substrec c
in
substrec t
let hResolve id c occ t =
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Termops.clear_named_body id (Proofview.Goal.env gl) in
let concl = Proofview.Goal.concl gl in
let env_ids = Termops.vars_of_env env in
let c_raw = Detyping.detype Detyping.Now true env_ids env sigma c in
let t_raw = Detyping.detype Detyping.Now true env_ids env sigma t in
let rec resolve_hole t_hole =
try
Pretyping.understand_tcc_ty ~flags:Pretyping.all_and_fail_flags env sigma t_hole
with
| Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e ->
let (e, info) = Exninfo.capture e in
let loc_begin = Option.cata (fun l -> fst (Loc.unloc l)) 0 (Loc.get_loc info) in
resolve_hole (subst_hole_with_term loc_begin c_raw t_hole)
in
let sigma, t_constr, t_constr_type = resolve_hole (subst_var_with_hole occ id t_raw) in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(change_concl (mkLetIn (Context.make_annot Name.Anonymous Sorts.Relevant,t_constr,t_constr_type,concl)))
end
let hResolve_auto id c t =
let rec resolve_auto n =
try
hResolve id c n t
with
| UserError _ as e -> raise e
| e when CErrors.noncritical e -> resolve_auto (n+1)
in
resolve_auto 1
let induction_arg_of_quantified_hyp = function
| AnonHyp n -> None,ElimOnAnonHyp n
| NamedHyp id -> None,ElimOnIdent id
exception Found of unit Proofview.tactic
let rewrite_except h =
Proofview.Goal.enter begin fun gl ->
let hyps = Tacmach.pf_ids_of_hyps gl in
Tacticals.tclMAP (fun id -> if Id.equal id h then Proofview.tclUNIT () else
Tacticals.tclTRY (Equality.general_rewrite ~where:(Some id) ~l2r:true Locus.AllOccurrences ~freeze:true ~dep:true ~with_evars:false (mkVar h, NoBindings)))
hyps
end
let refl_equal () = Coqlib.lib_ref "core.eq.type"
let mkCaseEq a : unit Proofview.tactic =
Proofview.Goal.enter begin fun gl ->
let type_of_a = Tacmach.pf_get_type_of gl a in
Tacticals.pf_constr_of_global (delayed_force refl_equal) >>= fun req ->
Tacticals.tclTHENLIST
[Tactics.generalize [(mkApp(req, [| type_of_a; a|]))];
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env (Evd.from_env env) concl in
change_concl c
end;
simplest_case a]
end
let case_eq_intros_rewrite x =
Proofview.Goal.enter begin fun gl ->
let n = nb_prod (Tacmach.project gl) (Proofview.Goal.concl gl) in
Tacticals.tclTHENLIST [
mkCaseEq x;
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let hyps = Tacmach.pf_ids_set_of_hyps gl in
let n' = nb_prod (Tacmach.project gl) concl in
let h = fresh_id_in_env hyps (Id.of_string "heq") (Proofview.Goal.env gl) in
Tacticals.tclTHENLIST [
Tacticals.tclDO (n'-n-1) intro;
introduction h;
rewrite_except h]
end
]
end
let rec find_a_destructable_match sigma t =
let cl = induction_arg_of_quantified_hyp (NamedHyp (CAst.make @@ Id.of_string "x")) in
let cl = [cl, (None, None), None], None in
let dest = CAst.make @@ TacAtom (TacInductionDestruct(false, false, cl)) in
match EConstr.kind sigma t with
| Case (_,_,_,_,_,x,_) when closed0 sigma x ->
if isVar sigma x then
raise (Found (Tacinterp.eval_tactic dest))
else
raise (Found (case_eq_intros_rewrite x))
| _ -> EConstr.iter sigma (fun c -> find_a_destructable_match sigma c) t
let destauto0 t =
Proofview.tclEVARMAP >>= fun sigma ->
try find_a_destructable_match sigma t;
Tacticals.tclZEROMSG (Pp.str "No destructable match found")
with Found tac -> tac
let destauto =
Proofview.Goal.enter begin fun gl -> destauto0 (Proofview.Goal.concl gl) end
let destauto_in id =
Proofview.Goal.enter begin fun gl ->
let ctype = Tacmach.pf_get_type_of gl (mkVar id) in
destauto0 ctype
end
(** Term introspection *)
let is_evar x =
Proofview.tclEVARMAP >>= fun sigma ->
match EConstr.kind sigma x with
| Evar _ -> Proofview.tclUNIT ()
| _ -> Tacticals.tclFAIL (Pp.str "Not an evar")
let has_evar x =
Proofview.tclEVARMAP >>= fun sigma ->
if Evarutil.has_undefined_evars sigma x
then Proofview.tclUNIT ()
else Tacticals.tclFAIL (Pp.str "No evars")
let is_var x =
Proofview.tclEVARMAP >>= fun sigma ->
match EConstr.kind sigma x with
| Var _ -> Proofview.tclUNIT ()
| _ -> Tacticals.tclFAIL (Pp.str "Not a variable or hypothesis")
let is_fix x =
Proofview.tclEVARMAP >>= fun sigma ->
match EConstr.kind sigma x with
| Fix _ -> Proofview.tclUNIT ()
| _ -> Tacticals.tclFAIL (Pp.str "not a fix definition")
let is_cofix x =
Proofview.tclEVARMAP >>= fun sigma ->
match EConstr.kind sigma x with
| CoFix _ -> Proofview.tclUNIT ()
| _ -> Tacticals.tclFAIL (Pp.str "not a cofix definition")
let is_ind x =
Proofview.tclEVARMAP >>= fun sigma ->
match EConstr.kind sigma x with
| Ind _ -> Proofview.tclUNIT ()
| _ -> Tacticals.tclFAIL (Pp.str "not an (co)inductive datatype")
let is_constructor x =
Proofview.tclEVARMAP >>= fun sigma ->
match EConstr.kind sigma x with
| Construct _ -> Proofview.tclUNIT ()
| _ -> Tacticals.tclFAIL (Pp.str "not a constructor")
let is_proj x =
Proofview.tclEVARMAP >>= fun sigma ->
match EConstr.kind sigma x with
| Proj _ -> Proofview.tclUNIT ()
| _ -> Tacticals.tclFAIL (Pp.str "not a primitive projection")
let is_const x =
Proofview.tclEVARMAP >>= fun sigma ->
match EConstr.kind sigma x with
| Const _ -> Proofview.tclUNIT ()
| _ -> Tacticals.tclFAIL (Pp.str "not a constant")
let unshelve ist t =
Proofview.with_shelf (Tacinterp.tactic_of_value ist t) >>= fun (gls, ()) ->
let gls = List.map Proofview.with_empty_state gls in
Proofview.Unsafe.tclGETGOALS >>= fun ogls ->
Proofview.Unsafe.tclSETGOALS (gls @ ogls)
(** tactic analogous to "OPTIMIZE HEAP" *)
let tclOPTIMIZE_HEAP =
Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> Gc.compact ()))
let onSomeWithHoles tac = function
| None -> tac None
| Some c -> Tacticals.tclDELAYEDWITHHOLES false c (fun c -> tac (Some c))
let decompose l c =
Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.project gl in
let to_ind c =
if isInd sigma c then fst (destInd sigma c)
else user_err Pp.(str "not an inductive type")
in
let l = List.map to_ind l in
Elim.h_decompose l c
end
let exact ist (c : Ltac_pretype.closed_glob_constr) =
let open Tacmach in
Proofview.Goal.enter begin fun gl ->
let expected_type = Pretyping.OfType (pf_concl gl) in
let sigma, c = Tacinterp.type_uconstr ~expected_type ist c (pf_env gl) (project gl) in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Tactics.exact_no_check c)
end
(** ProofGeneral specific command *)
let infoH ~pstate (tac : raw_tactic_expr) : unit =
let (_, oldhyps) = Declare.Proof.get_current_goal_context pstate in
let oldhyps = List.map Context.Named.Declaration.get_id @@ Environ.named_context oldhyps in
let tac = Tacinterp.interp tac in
let tac =
let open Proofview.Notations in
tac <*>
Proofview.Unsafe.tclGETGOALS >>= fun gls ->
Proofview.tclEVARMAP >>= fun sigma ->
let map gl =
let gl = Proofview_monad.drop_state gl in
let hyps = Evd.evar_filtered_context (Evd.find sigma gl) in
List.map Context.Named.Declaration.get_id @@ hyps
in
let hyps = List.map map gls in
let newhyps = List.map (fun hypl -> List.subtract Names.Id.equal hypl oldhyps) hyps in
let s =
let frst = ref true in
List.fold_left
(fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ")
^ (List.fold_left
(fun acc d -> (Names.Id.to_string d) ^ " " ^ acc)
"" lh))
"" newhyps in
let () = Feedback.msg_notice
Pp.(str "<infoH>"
++ (hov 0 (str s))
++ (str "</infoH>")) in
Proofview.tclUNIT ()
in
ignore (Declare.Proof.by tac pstate)
let declare_equivalent_keys c c' =
let get_key c =
let env = Global.env () in
let evd = Evd.from_env env in
let (evd, c) = Constrintern.interp_open_constr env evd c in
let kind c = EConstr.kind evd c in
Keys.constr_key kind c
in
let k1 = get_key c in
let k2 = get_key c' in
match k1, k2 with
| Some k1, Some k2 -> Keys.declare_equiv_keys k1 k2
| _ -> ()