Source file tac2tactics.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
448
449
450
451
452
open Pp
open Util
open Names
open Tac2types
open Tac2extffi
open Genredexpr
open Proofview.Notations
let return = Proofview.tclUNIT
let thaw r f = Tac2ffi.app_fun1 f Tac2ffi.unit r ()
let tactic_infer_flags with_evar = Pretyping.{
use_coercions = true;
use_typeclasses = UseTC;
solve_unification_constraints = true;
fail_evar = not with_evar;
expand_evars = true;
program_mode = false;
polymorphic = false;
}
(** FIXME: export a better interface in Tactics *)
let delayed_of_tactic tac env sigma =
let _, pv = Proofview.init sigma [] in
let name, poly = Id.of_string "ltac2_delayed", false in
let c, pv, _, _ = Proofview.apply ~name ~poly env tac pv in
let _, sigma = Proofview.proofview pv in
(sigma, c)
let delayed_of_thunk r tac env sigma =
delayed_of_tactic (thaw r tac) env sigma
let mk_bindings = function
| ImplicitBindings l -> Tactypes.ImplicitBindings l
| ExplicitBindings l ->
let l = List.map CAst.make l in
Tactypes.ExplicitBindings l
| NoBindings -> Tactypes.NoBindings
let mk_with_bindings (x, b) = (x, mk_bindings b)
let rec mk_intro_pattern = function
| IntroForthcoming b -> CAst.make @@ Tactypes.IntroForthcoming b
| IntroNaming ipat -> CAst.make @@ Tactypes.IntroNaming (mk_intro_pattern_naming ipat)
| IntroAction ipat -> CAst.make @@ Tactypes.IntroAction (mk_intro_pattern_action ipat)
and mk_intro_pattern_naming = function
| IntroIdentifier id -> Namegen.IntroIdentifier id
| IntroFresh id -> Namegen.IntroFresh id
| IntroAnonymous -> Namegen.IntroAnonymous
and mk_intro_pattern_action = function
| IntroWildcard -> Tactypes.IntroWildcard
| IntroOrAndPattern ipat -> Tactypes.IntroOrAndPattern (mk_or_and_intro_pattern ipat)
| IntroInjection ipats -> Tactypes.IntroInjection (List.map mk_intro_pattern ipats)
| IntroApplyOn (c, ipat) ->
let c = CAst.make @@ delayed_of_thunk Tac2ffi.constr c in
Tactypes.IntroApplyOn (c, mk_intro_pattern ipat)
| IntroRewrite b -> Tactypes.IntroRewrite b
and mk_or_and_intro_pattern = function
| IntroOrPattern ipatss ->
Tactypes.IntroOrPattern (List.map (fun ipat -> List.map mk_intro_pattern ipat) ipatss)
| IntroAndPattern ipats ->
Tactypes.IntroAndPattern (List.map mk_intro_pattern ipats)
let mk_intro_patterns ipat = List.map mk_intro_pattern ipat
let mk_occurrences f = function
| AllOccurrences -> Locus.AllOccurrences
| AllOccurrencesBut l -> Locus.AllOccurrencesBut (List.map f l)
| NoOccurrences -> Locus.NoOccurrences
| OnlyOccurrences l -> Locus.OnlyOccurrences (List.map f l)
let mk_occurrences_expr occ =
mk_occurrences (fun i -> Locus.ArgArg i) occ
let mk_hyp_location (id, occs, h) =
((mk_occurrences_expr occs, id), h)
let mk_clause cl = {
Locus.onhyps = Option.map (fun l -> List.map mk_hyp_location l) cl.onhyps;
Locus.concl_occs = mk_occurrences_expr cl.concl_occs;
}
let intros_patterns ev ipat =
let ipat = mk_intro_patterns ipat in
Tactics.intros_patterns ev ipat
let apply adv ev cb cl =
let map c =
let c = thaw constr_with_bindings c >>= fun p -> return (mk_with_bindings p) in
None, CAst.make (delayed_of_tactic c)
in
let cb = List.map map cb in
match cl with
| None -> Tactics.apply_with_delayed_bindings_gen adv ev cb
| Some (id, cl) ->
let cl = Option.map mk_intro_pattern cl in
Tactics.apply_delayed_in adv ev id cb cl Tacticals.tclIDTAC
let mk_destruction_arg = function
| ElimOnConstr c ->
let c = c >>= fun c -> return (mk_with_bindings c) in
Tactics.ElimOnConstr (delayed_of_tactic c)
| ElimOnIdent id -> Tactics.ElimOnIdent CAst.(make id)
| ElimOnAnonHyp n -> Tactics.ElimOnAnonHyp n
let mk_induction_clause (arg, eqn, as_, occ) =
let eqn = Option.map (fun ipat -> CAst.make @@ mk_intro_pattern_naming ipat) eqn in
let as_ = Option.map (fun ipat -> CAst.make @@ mk_or_and_intro_pattern ipat) as_ in
let occ = Option.map mk_clause occ in
((None, mk_destruction_arg arg), (eqn, as_), occ)
let induction_destruct isrec ev (ic : induction_clause list) using =
let ic = List.map mk_induction_clause ic in
let using = Option.map mk_with_bindings using in
Induction.induction_destruct isrec ev (ic, using)
let elim ev c copt =
let c = mk_with_bindings c in
let copt = Option.map mk_with_bindings copt in
Tactics.elim ev None c copt
let generalize pl =
let mk_occ occs = mk_occurrences (fun i -> i) occs in
let pl = List.map (fun (c, occs, na) -> (mk_occ occs, c), na) pl in
Generalize.new_generalize_gen pl
let general_case_analysis ev c =
let c = mk_with_bindings c in
Tactics.general_case_analysis ev None c
let constructor_tac ev n i bnd =
let bnd = mk_bindings bnd in
Tactics.constructor_tac ev n i bnd
let left_with_bindings ev bnd =
let bnd = mk_bindings bnd in
Tactics.left_with_bindings ev bnd
let right_with_bindings ev bnd =
let bnd = mk_bindings bnd in
Tactics.right_with_bindings ev bnd
let split_with_bindings ev bnd =
let bnd = mk_bindings bnd in
Tactics.split_with_bindings ev [bnd]
let specialize c pat =
let c = mk_with_bindings c in
let pat = Option.map mk_intro_pattern pat in
Tactics.specialize c pat
let change pat c cl =
let open Tac2ffi in
Proofview.Goal.enter begin fun gl ->
let c subst env sigma =
let subst = Array.map_of_list snd (Id.Map.bindings subst) in
delayed_of_tactic (Tac2ffi.app_fun1 c (array constr) constr subst) env sigma
in
let cl = mk_clause cl in
Tactics.change ~check:true pat c cl
end
let rewrite ev rw cl by =
let map_rw (orient, repeat, c) =
let c = c >>= fun c -> return (mk_with_bindings c) in
(Option.default true orient, repeat, None, delayed_of_tactic c)
in
let rw = List.map map_rw rw in
let cl = mk_clause cl in
let by = Option.map (fun tac -> Tacticals.tclCOMPLETE (thaw Tac2ffi.unit tac), Equality.Naive) by in
Equality.general_multi_rewrite ev rw cl by
let setoid_rewrite orient c occs id =
let c = c >>= fun c -> return (mk_with_bindings c) in
let occs = mk_occurrences (fun i -> i) occs in
Rewrite.cl_rewrite_clause (delayed_of_tactic c) orient occs id
let symmetry cl =
let cl = mk_clause cl in
Tactics.intros_symmetry cl
let forward fst tac ipat c =
let ipat = Option.map mk_intro_pattern ipat in
Tactics.forward fst tac ipat c
let assert_ = function
| AssertValue (id, c) ->
let ipat = CAst.make @@ Tactypes.IntroNaming (Namegen.IntroIdentifier id) in
Tactics.forward true None (Some ipat) c
| AssertType (ipat, c, tac) ->
let ipat = Option.map mk_intro_pattern ipat in
let tac = Option.map (fun tac -> thaw Tac2ffi.unit tac) tac in
Tactics.forward true (Some tac) ipat c
let letin_pat_tac ev ipat na c cl =
let ipat = Option.map (fun (b, ipat) -> (b, CAst.make @@ mk_intro_pattern_naming ipat)) ipat in
let cl = mk_clause cl in
Tactics.letin_pat_tac ev ipat na c cl
(** Ltac interface treats differently global references than other term
arguments in reduction expressions. In Ltac1, this is done at parsing time.
Instead, we parse indifferently any pattern and dispatch when the tactic is
called. *)
let map_pattern_with_occs (pat, occ) = match pat with
| Pattern.PRef (GlobRef.ConstRef cst) -> (mk_occurrences_expr occ, Inl (Tacred.EvalConstRef cst))
| Pattern.PRef (GlobRef.VarRef id) -> (mk_occurrences_expr occ, Inl (Tacred.EvalVarRef id))
| _ -> (mk_occurrences_expr occ, Inr pat)
let get_evaluable_reference = function
| GlobRef.VarRef id -> Proofview.tclUNIT (Tacred.EvalVarRef id)
| GlobRef.ConstRef cst -> Proofview.tclUNIT (Tacred.EvalConstRef cst)
| r -> Proofview.tclZERO (Tacred.NotEvaluableRef r)
let reduce r cl =
let cl = mk_clause cl in
Tactics.reduce r cl
let simpl flags where cl =
let where = Option.map map_pattern_with_occs where in
let cl = mk_clause cl in
Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
let flags = { flags with rConst } in
Tactics.reduce (Simpl (flags, where)) cl
let cbv flags cl =
let cl = mk_clause cl in
Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
let flags = { flags with rConst } in
Tactics.reduce (Cbv flags) cl
let cbn flags cl =
let cl = mk_clause cl in
Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
let flags = { flags with rConst } in
Tactics.reduce (Cbn flags) cl
let lazy_ flags cl =
let cl = mk_clause cl in
Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
let flags = { flags with rConst } in
Tactics.reduce (Lazy flags) cl
let unfold occs cl =
let cl = mk_clause cl in
let map (gr, occ) =
let occ = mk_occurrences_expr occ in
get_evaluable_reference gr >>= fun gr -> Proofview.tclUNIT (occ, gr)
in
Proofview.Monad.List.map map occs >>= fun occs ->
Tactics.reduce (Unfold occs) cl
let pattern where cl =
let where = List.map (fun (c, occ) -> (mk_occurrences_expr occ, c)) where in
let cl = mk_clause cl in
Tactics.reduce (Pattern where) cl
let vm where cl =
let where = Option.map map_pattern_with_occs where in
let cl = mk_clause cl in
Tactics.reduce (CbvVm where) cl
let native where cl =
let where = Option.map map_pattern_with_occs where in
let cl = mk_clause cl in
Tactics.reduce (CbvNative where) cl
let eval_fun red c =
Tac2core.pf_apply begin fun env sigma ->
let (redfun, _) = Redexpr.reduction_of_red_expr env red in
let (sigma, ans) = redfun env sigma c in
Proofview.Unsafe.tclEVARS sigma >>= fun () ->
Proofview.tclUNIT ans
end
let eval_red c =
eval_fun Red c
let eval_hnf c =
eval_fun Hnf c
let eval_simpl flags where c =
let where = Option.map map_pattern_with_occs where in
Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
let flags = { flags with rConst } in
eval_fun (Simpl (flags, where)) c
let eval_cbv flags c =
Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
let flags = { flags with rConst } in
eval_fun (Cbv flags) c
let eval_cbn flags c =
Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
let flags = { flags with rConst } in
eval_fun (Cbn flags) c
let eval_lazy flags c =
Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
let flags = { flags with rConst } in
eval_fun (Lazy flags) c
let eval_unfold occs c =
let map (gr, occ) =
let occ = mk_occurrences_expr occ in
get_evaluable_reference gr >>= fun gr -> Proofview.tclUNIT (occ, gr)
in
Proofview.Monad.List.map map occs >>= fun occs ->
eval_fun (Unfold occs) c
let eval_fold cl c =
eval_fun (Fold cl) c
let eval_pattern where c =
let where = List.map (fun (pat, occ) -> (mk_occurrences_expr occ, pat)) where in
eval_fun (Pattern where) c
let eval_vm where c =
let where = Option.map map_pattern_with_occs where in
eval_fun (CbvVm where) c
let eval_native where c =
let where = Option.map map_pattern_with_occs where in
eval_fun (CbvNative where) c
let on_destruction_arg tac ev arg =
Proofview.Goal.enter begin fun gl ->
match arg with
| None -> tac ev None
| Some (clear, arg) ->
let arg = match arg with
| ElimOnConstr c ->
let env = Proofview.Goal.env gl in
Proofview.tclEVARMAP >>= fun sigma ->
c >>= fun (c, lbind) ->
let lbind = mk_bindings lbind in
Proofview.tclEVARMAP >>= fun sigma' ->
let flags = tactic_infer_flags ev in
let (sigma', c) = Tactics.finish_evar_resolution ~flags env sigma' (Some sigma, c) in
Proofview.tclUNIT (Some sigma', Tactics.ElimOnConstr (c, lbind))
| ElimOnIdent id -> Proofview.tclUNIT (None, Tactics.ElimOnIdent CAst.(make id))
| ElimOnAnonHyp n -> Proofview.tclUNIT (None, Tactics.ElimOnAnonHyp n)
in
arg >>= fun (sigma', arg) ->
let arg = Some (clear, arg) in
match sigma' with
| None -> tac ev arg
| Some sigma' ->
Tacticals.tclWITHHOLES ev (tac ev arg) sigma'
end
let discriminate ev arg =
let arg = Option.map (fun arg -> None, arg) arg in
on_destruction_arg Equality.discr_tac ev arg
let injection ev ipat arg =
let arg = Option.map (fun arg -> None, arg) arg in
let ipat = Option.map mk_intro_patterns ipat in
let tac ev arg = Equality.injClause None ipat ev arg in
on_destruction_arg tac ev arg
let autorewrite ~all by ids cl =
let conds = if all then Some Equality.AllMatches else None in
let ids = List.map Id.to_string ids in
let cl = mk_clause cl in
match by with
| None -> Autorewrite.auto_multi_rewrite ?conds ids cl
| Some by ->
let by = thaw Tac2ffi.unit by in
Autorewrite.auto_multi_rewrite_with ?conds by ids cl
(** Auto *)
let trivial debug lems dbs =
let lems = List.map (fun c -> delayed_of_thunk Tac2ffi.constr c) lems in
let dbs = Option.map (fun l -> List.map Id.to_string l) dbs in
Auto.h_trivial ~debug lems dbs
let auto debug n lems dbs =
let lems = List.map (fun c -> delayed_of_thunk Tac2ffi.constr c) lems in
let dbs = Option.map (fun l -> List.map Id.to_string l) dbs in
Auto.h_auto ~debug n lems dbs
let eauto debug n lems dbs =
let lems = List.map (fun c -> delayed_of_thunk Tac2ffi.constr c) lems in
let dbs = Option.map (fun l -> List.map Id.to_string l) dbs in
Eauto.gen_eauto ~debug ?depth:n lems dbs
let typeclasses_eauto strategy depth dbs =
let only_classes, dbs = match dbs with
| None ->
true, [Class_tactics.typeclasses_db]
| Some dbs ->
let dbs = List.map Id.to_string dbs in
false, dbs
in
Class_tactics.typeclasses_eauto ~only_classes ?strategy ~depth dbs
let unify x y = Tactics.unify x y
let current_transparent_state () =
Proofview.tclENV >>= fun env ->
let state = Conv_oracle.get_transp_state (Environ.oracle env) in
Proofview.tclUNIT state
let evarconv_unify state x y = Tactics.evarconv_unify ~state x y
(** Inversion *)
let inversion knd arg pat ids =
let ids = match ids with
| None -> []
| Some l -> l
in
begin match pat with
| None -> Proofview.tclUNIT None
| Some (IntroAction (IntroOrAndPattern p)) ->
Proofview.tclUNIT (Some (CAst.make @@ mk_or_and_intro_pattern p))
| Some _ ->
Tacticals.tclZEROMSG (str "Inversion only accept disjunctive patterns")
end >>= fun pat ->
let inversion _ arg =
begin match arg with
| None -> assert false
| Some (_, Tactics.ElimOnAnonHyp n) ->
Inv.inv_clause knd pat ids (AnonHyp n)
| Some (_, Tactics.ElimOnIdent id) ->
Inv.inv_clause knd pat ids (NamedHyp id)
| Some (_, Tactics.ElimOnConstr c) ->
let open Tactypes in
let anon = CAst.make @@ IntroNaming Namegen.IntroAnonymous in
Tactics.specialize c (Some anon) >>= fun () ->
Tacticals.onLastHypId (fun id -> Inv.inv_clause knd pat ids (NamedHyp (CAst.make id)))
end
in
on_destruction_arg inversion true (Some (None, arg))
let contradiction c =
let c = Option.map mk_with_bindings c in
Contradiction.contradiction c