Source file ssripats.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
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
open Ssrmatching_plugin
open Util
open Names
open Constr
open Context
open Proofview
open Proofview.Notations
open Ssrast
type ssriop =
| IOpId of Names.Id.t
| IOpDrop
| IOpTemporay
| IOpInaccessible of string option
| IOpInaccessibleAll
| IOpAbstractVars of Names.Id.t list
| IOpFastNondep
| IOpInj of ssriops list
| IOpDispatchBlock of id_block
| IOpDispatchBranches of ssriops list
| IOpCaseBlock of id_block
| IOpCaseBranches of ssriops list
| IOpRewrite of ssrocc * ssrdir
| IOpView of ssrclear option * ssrview
| IOpClear of ssrclear * ssrhyp option
| IOpSimpl of ssrsimpl
| IOpEqGen of unit Proofview.tactic
| IOpNoop
and ssriops = ssriop list
let rec pr_ipatop = function
| IOpId id -> Names.Id.print id
| IOpDrop -> Pp.str "_"
| IOpTemporay -> Pp.str "+"
| IOpInaccessible None -> Pp.str "?"
| IOpInaccessible (Some s) -> Pp.str ("?«"^s^"»")
| IOpInaccessibleAll -> Pp.str "*"
| IOpAbstractVars l -> Pp.str ("[:"^String.concat " " (List.map Names.Id.to_string l)^"]")
| IOpFastNondep -> Pp.str ">"
| IOpInj l -> Pp.(str "[=" ++ ppl l ++ str "]")
| IOpDispatchBlock b -> Pp.(str"(" ++ Ssrprinters.pr_block b ++ str")")
| IOpDispatchBranches l -> Pp.(str "(" ++ ppl l ++ str ")")
| IOpCaseBlock b -> Pp.(str"[" ++ Ssrprinters.pr_block b ++ str"]")
| IOpCaseBranches l -> Pp.(str "[" ++ ppl l ++ str "]")
| IOpRewrite (occ,dir) -> Pp.(Ssrprinters.(pr_occ occ ++ pr_dir dir))
| IOpView (None,vs) -> Pp.(prlist_with_sep mt (fun c -> str "/" ++ Ssrprinters.pr_ast_closure_term c) vs)
| IOpView (Some cl,vs) -> Pp.(Ssrprinters.pr_clear Pp.spc cl ++ prlist_with_sep mt (fun c -> str "/" ++ Ssrprinters.pr_ast_closure_term c) vs)
| IOpClear (clmust,clmay) ->
Pp.(Ssrprinters.pr_clear spc clmust ++
match clmay with
| Some cl -> str "(try " ++ Ssrprinters.pr_clear spc [cl] ++ str")"
| None -> mt ())
| IOpSimpl s -> Ssrprinters.pr_simpl s
| IOpEqGen _ -> Pp.str "E:"
| IOpNoop -> Pp.str"-"
and ppl x = Pp.(prlist_with_sep (fun () -> str"|") (prlist_with_sep spc pr_ipatop)) x
module IpatMachine : sig
val main : ?eqtac:unit tactic -> first_case_is_dispatch:bool ->
ssriops -> unit tactic
val tclCompileIPats : ssripats -> ssriops
val tclSEED_SUBGOALS : Names.Name.t list array -> unit tactic -> unit tactic
end = struct
module State : sig
type delayed_gen = {
tmp_id : Id.t;
orig_name : Name.t
}
val isCLR_PUSH : Id.t -> unit tactic
val isCLR_PUSHL : Id.t list -> unit tactic
val isCLR_CONSUME : unit tactic
val isGEN_PUSH : delayed_gen -> unit tactic
val isGEN_CONSUME : unit tactic
val isNSEED_SET : Names.Name.t list -> unit tactic
val isNSEED_CONSUME : (Names.Name.t list option -> unit tactic) -> unit tactic
val isTICK : ssriop -> unit tactic
val isPRINT : Proofview.Goal.t -> Pp.t
end = struct
type istate = {
to_clear : Id.t list;
to_generalize : delayed_gen list;
name_seed : Names.Name.t list option;
}
and delayed_gen = {
tmp_id : Id.t;
orig_name : Name.t
}
let empty_state = {
to_clear = [];
to_generalize = [];
name_seed = None;
}
include Ssrcommon.MakeState(struct
type state = istate
let init = empty_state
end)
let print_name_seed env sigma = function
| None -> Pp.str "-"
| Some nl -> Pp.prlist Names.Name.print nl
let print_delayed_gen { tmp_id; orig_name } =
Pp.(Id.print tmp_id ++ str"->" ++ Name.print orig_name)
let isPRINT g =
let env, sigma = Goal.env g, Goal.sigma g in
let state = get g in
Pp.(str"{{ to_clear: " ++
prlist_with_sep spc Id.print state.to_clear ++ spc () ++
str"to_generalize: " ++
prlist_with_sep spc print_delayed_gen state.to_generalize ++ spc () ++
str"name_seed: " ++ print_name_seed env sigma state.name_seed ++ str" }}")
let isCLR_PUSH id =
tclGET (fun ({ to_clear = ids } as s) ->
tclSET { s with to_clear = id :: ids })
let isCLR_PUSHL more_ids =
tclGET (fun ({ to_clear = ids } as s) ->
tclSET { s with to_clear = more_ids @ ids })
let isCLR_CONSUME =
tclGET (fun ({ to_clear = ids } as s) ->
tclSET { s with to_clear = [] } <*>
Tactics.clear ids)
let isGEN_PUSH dg =
tclGET (fun s ->
tclSET { s with to_generalize = dg :: s.to_generalize })
let gen_astac id new_name =
let gen = ((None,Some(false,[])),Ssrmatching.cpattern_of_id id) in
Ssrcommon.gentac gen
<*> Ssrcommon.tclRENAME_HD_PROD new_name
let isGEN_CONSUME =
tclGET (fun ({ to_generalize = dgs } as s) ->
tclSET { s with to_generalize = [] } <*>
Tacticals.tclTHENLIST
(List.map (fun { tmp_id; orig_name } ->
gen_astac tmp_id orig_name) dgs) <*>
Tactics.clear (List.map (fun gen -> gen.tmp_id) dgs))
let isNSEED_SET ty =
tclGET (fun s ->
tclSET { s with name_seed = Some ty })
let isNSEED_CONSUME k =
tclGET (fun ({ name_seed = x } as s) ->
tclSET { s with name_seed = None } <*>
k x)
let isTICK = function
| IOpSimpl _ | IOpClear _ -> tclUNIT ()
| _ -> tclGET (fun s -> tclSET { s with name_seed = None })
end
open State
(** [nb_assums] returns the number of dependent premises
Warning: unlike [nb_deps_assums], it does not perform reduction *)
let rec nb_assums cur env sigma t =
match EConstr.kind sigma t with
| Prod(name,ty,body) ->
nb_assums (cur+1) env sigma body
| LetIn(name,ty,t1,t2) ->
nb_assums (cur+1) env sigma t2
| Cast(t,_,_) ->
nb_assums cur env sigma t
| _ -> cur
let nb_assums = nb_assums 0
let intro_anon_all = Goal.enter begin fun gl ->
let env = Goal.env gl in
let sigma = Goal.sigma gl in
let g = Goal.concl gl in
let n = nb_assums env sigma g in
Tacticals.tclDO n (Ssrcommon.tclINTRO_ANON ())
end
(** [nb_deps_assums] returns the number of dependent premises *)
let rec nb_deps_assums cur env sigma t =
let t' = Reductionops.whd_allnolet env sigma t in
match EConstr.kind sigma t' with
| Constr.Prod(name,ty,body) ->
if EConstr.Vars.noccurn sigma 1 body &&
not (Typeclasses.is_class_type sigma ty) then cur
else nb_deps_assums (cur+1) env sigma body
| Constr.LetIn(name,ty,t1,t2) ->
nb_deps_assums (cur+1) env sigma t2
| Constr.Cast(t,_,_) ->
nb_deps_assums cur env sigma t
| _ -> cur
let nb_deps_assums = nb_deps_assums 0
let intro_anon_deps = Goal.enter begin fun gl ->
let env = Goal.env gl in
let sigma = Goal.sigma gl in
let g = Goal.concl gl in
let n = nb_deps_assums env sigma g in
Tacticals.tclDO n (Ssrcommon.tclINTRO_ANON ())
end
(** [intro_drop] behaves like [intro_anon] but registers the id of the
introduced assumption for a delayed clear. *)
let intro_drop =
Ssrcommon.tclINTRO ~id:Ssrcommon.Anon
~conclusion:(fun ~orig_name:_ ~new_name -> isCLR_PUSH new_name)
(** [intro_temp] behaves like [intro_anon] but registers the id of the
introduced assumption for a regeneralization. *)
let intro_anon_temp =
Ssrcommon.tclINTRO ~id:Ssrcommon.Anon
~conclusion:(fun ~orig_name ~new_name ->
isGEN_PUSH { tmp_id = new_name; orig_name })
(** [intro_end] performs the actions that have been delayed. *)
let intro_end =
Ssrcommon.tcl0G ~default:() (isCLR_CONSUME <*> isGEN_CONSUME)
(** [=> _] *****************************************************************)
let intro_clear ids =
Goal.enter begin fun gl ->
let _, clear_ids, ren =
List.fold_left (fun (used_ids, clear_ids, ren) id ->
let new_id = Ssrcommon.mk_anon_id (Id.to_string id) used_ids in
(new_id :: used_ids, new_id :: clear_ids, (id, new_id) :: ren))
(Tacmach.pf_ids_of_hyps gl, [], []) ids
in
Tactics.rename_hyp ren <*>
isCLR_PUSHL clear_ids
end
let tacCHECK_HYPS_EXIST hyps = Goal.enter begin fun gl ->
let ctx = Goal.hyps gl in
List.iter (Ssrcommon.check_hyp_exists ctx) hyps;
tclUNIT ()
end
let tacFILTER_HYP_EXIST hyps k = Goal.enter begin fun gl ->
let ctx = Goal.hyps gl in
k (Option.bind hyps (fun h ->
if Ssrcommon.test_hyp_exists ctx h &&
Ssrcommon.(not_section_id (hyp_id h)) then Some h else None))
end
(** [=> []] *****************************************************************)
let tclTHENin t1 t2 =
tclUNIT () >>= begin fun () -> let i = ref (-1) in
t1 <*> numgoals >>= fun n ->
Goal.enter begin fun g -> incr i; t2 !i n end
end
let tclSEED_SUBGOALS seeds tac =
tclTHENin tac (fun i n ->
Ssrprinters.debug_ssr (fun () -> Pp.(str"seeding"));
let = n - Array.length seeds in
if i < extra_goals then tclUNIT ()
else isNSEED_SET seeds.(i - extra_goals))
let tac_case t =
Goal.enter begin fun _ ->
Ssrcommon.tacTYPEOF t >>= fun ty ->
Ssrcommon.tacIS_INJECTION_CASE ~ty t >>= fun is_inj ->
if is_inj then
Ssrelim.perform_injection t
else
Goal.enter begin fun g ->
(Ssrelim.casetac t (fun ?seed k ->
match seed with
| None -> k
| Some seed -> tclSEED_SUBGOALS seed k))
end
end
(** [=> [^ seed ]] *********************************************************)
let tac_intro_seed interp_ipats fix = Goal.enter begin fun gl ->
isNSEED_CONSUME begin fun seeds ->
let seeds =
Ssrcommon.option_assert_get seeds Pp.(str"tac_intro_seed: no seed") in
let ipats = List.map (function
| Anonymous ->
let s = match fix with
| Prefix id -> Id.to_string id ^ "?"
| SuffixNum n -> "?" ^ string_of_int n
| SuffixId id -> "?" ^ Id.to_string id in
IOpInaccessible (Some s)
| Name id ->
let s = match fix with
| Prefix fix -> Id.to_string fix ^ Id.to_string id
| SuffixNum n -> Id.to_string id ^ string_of_int n
| SuffixId fix -> Id.to_string id ^ Id.to_string fix in
IOpId (Id.of_string s)) seeds in
interp_ipats ipats
end end
let mk_abstract_id =
let open Coqlib in
let ssr_abstract_id = Summary.ref ~name:"SSR:abstractid" 0 in
begin fun env sigma ->
let sigma, zero = EConstr.fresh_global env sigma (lib_ref "num.nat.O") in
let sigma, succ = EConstr.fresh_global env sigma (lib_ref "num.nat.S") in
let rec nat_of_n n =
if n = 0 then zero
else EConstr.mkApp (succ, [|nat_of_n (n-1)|]) in
incr ssr_abstract_id;
sigma, nat_of_n !ssr_abstract_id
end
let tclMK_ABSTRACT_VAR id = Goal.enter begin fun gl ->
let env, concl = Goal.(env gl, concl gl) in
let step ablock abstract = begin fun sigma ->
let (sigma, (abstract_proof, abstract_ty)) =
let (sigma, (ty, _)) =
Evarutil.new_type_evar env sigma Evd.univ_flexible_alg in
let (sigma, lock) = Evarutil.new_evar env sigma ablock in
let (sigma, abstract_id) = mk_abstract_id env sigma in
let abstract_ty = EConstr.mkApp(abstract, [|ty; abstract_id; lock|]) in
let sigma, m = Evarutil.new_evar env sigma abstract_ty in
sigma, (m, abstract_ty) in
let sigma, kont =
let rd = Context.Rel.Declaration.LocalAssum (make_annot (Name id) Sorts.Relevant, abstract_ty) in
let sigma, ev = Evarutil.new_evar (EConstr.push_rel rd env) sigma concl in
sigma, ev
in
let term =
EConstr.(mkApp (mkLambda(make_annot (Name id) Sorts.Relevant,abstract_ty,kont),[|abstract_proof|])) in
let sigma, _ = Typing.type_of env sigma term in
sigma, term
end in
Ssrcommon.tacMK_SSR_CONST "abstract_lock" >>= fun ablock ->
Ssrcommon.tacMK_SSR_CONST "abstract" >>= fun abstract ->
Tactics.New.refine ~typecheck:false (step ablock abstract) <*>
tclFOCUS 1 3 Proofview.shelve
end
let tclMK_ABSTRACT_VARS ids =
List.fold_right (fun id tac ->
Tacticals.tclTHENFIRST (tclMK_ABSTRACT_VAR id) tac) ids (tclUNIT ())
let tclLOG p t =
tclUNIT () >>= begin fun () ->
Ssrprinters.debug_ssr (fun () -> Pp.(str "exec: " ++ pr_ipatop p));
tclUNIT ()
end <*>
Goal.enter begin fun g ->
Ssrprinters.debug_ssr (fun () -> Pp.(str" on state:" ++ spc () ++
isPRINT g ++
str" goal:" ++ spc () ++ Printer.Debug.pr_goal g));
tclUNIT ()
end
<*>
t p
>>= fun ret ->
Goal.enter begin fun g ->
Ssrprinters.debug_ssr (fun () -> Pp.(str "done: " ++ isPRINT g));
tclUNIT ()
end
>>= fun () -> tclUNIT ret
let notTAC = tclUNIT false
let duplicate_clear =
CWarnings.create ~name:"duplicate-clear" ~category:"ssr"
(fun id -> Pp.(str "Duplicate clear of " ++ Id.print id))
let rec ipat_tac1 ipat : bool tactic =
match ipat with
| IOpView (glued_clear,l) ->
let clear_if_id, =
match glued_clear with
| None -> false, []
| Some x -> true, List.map Ssrcommon.hyp_id x in
Ssrview.tclIPAT_VIEWS
~views:l ~clear_if_id
~conclusion:(fun ~to_clear:clr ->
let inter = CList.intersect Id.equal clr extra_clear in
List.iter duplicate_clear inter;
let cl = CList.union Id.equal clr extra_clear in
intro_clear cl) ()
| IOpDispatchBranches ipatss ->
tclDISPATCH (List.map ipat_tac ipatss) <*> notTAC
| IOpDispatchBlock id_block ->
tac_intro_seed ipat_tac id_block <*> notTAC
| IOpCaseBlock id_block ->
Ssrcommon.tclWITHTOP tac_case <*> tac_intro_seed ipat_tac id_block <*> notTAC
| IOpCaseBranches ipatss ->
tclIORPAT (Ssrcommon.tclWITHTOP tac_case) ipatss <*> notTAC
| IOpId id -> Ssrcommon.tclINTRO_ID id <*> notTAC
| IOpFastNondep -> intro_anon_deps <*> notTAC
| IOpDrop -> intro_drop <*> notTAC
| IOpInaccessible seed -> Ssrcommon.tclINTRO_ANON ?seed () <*> notTAC
| IOpInaccessibleAll -> intro_anon_all <*> notTAC
| IOpTemporay -> intro_anon_temp <*> notTAC
| IOpSimpl Nop -> assert false
| IOpInj ipatss ->
tclIORPAT (Ssrcommon.tclWITHTOP
(fun t -> Ssrelim.perform_injection t))
ipatss
<*> notTAC
| IOpClear (must,may) ->
tacCHECK_HYPS_EXIST must <*>
tacFILTER_HYP_EXIST may (fun may ->
let must = List.map Ssrcommon.hyp_id must in
let cl = Option.fold_left (fun cls (SsrHyp(_,id)) ->
if CList.mem_f Id.equal id cls then begin
duplicate_clear id;
cls
end else id :: cls) must may in
intro_clear cl) <*>
notTAC
| IOpSimpl x ->
Ssrequality.simpltac x <*> notTAC
| IOpRewrite (occ,dir) ->
Ssrcommon.tclWITHTOP
(fun x -> Ssrequality.ipat_rewrite occ dir x) <*> notTAC
| IOpAbstractVars ids -> tclMK_ABSTRACT_VARS ids <*> notTAC
| IOpEqGen t -> t <*> notTAC
| IOpNoop -> notTAC
and ipat_tac pl : unit tactic =
match pl with
| [] -> tclUNIT ()
| pat :: pl ->
Ssrcommon.tcl0G ~default:false (tclLOG pat ipat_tac1) >>= fun was_tac ->
isTICK pat >>= fun () ->
if was_tac then
let ip_before, case, ip_after = split_at_first_case pl in
let case = ssr_exception true case in
let case = option_to_list case in
ipat_tac (ip_before @ case @ ip_after)
else ipat_tac pl
and tclIORPAT tac = function
| [[]] -> tac
| p -> Tacticals.tclTHENS tac (List.map ipat_tac p)
and ssr_exception is_on = function
| Some (IOpCaseBranches [[]]) when is_on -> Some IOpNoop
| Some (IOpCaseBranches l) when is_on ->
Some (IOpDispatchBranches l)
| Some (IOpCaseBlock s) when is_on ->
Some (IOpDispatchBlock s)
| x -> x
and option_to_list = function None -> [] | Some x -> [x]
and split_at_first_case ipats =
let rec loop acc = function
| (IOpSimpl _ | IOpClear _) as x :: rest -> loop (x :: acc) rest
| (IOpCaseBlock _ | IOpCaseBranches _
| IOpDispatchBlock _ | IOpDispatchBranches _) as x :: xs ->
CList.rev acc, Some x, xs
| pats -> CList.rev acc, None, pats
in
loop [] ipats
;;
let tclCompileIPats l =
let rec elab = function
| (IPatClear cl) :: (IPatView v) :: rest ->
(IOpView(Some cl,v)) :: elab rest
| (IPatClear cl) :: (IPatId id) :: rest ->
(IOpClear (cl,Some (SsrHyp(None,id)))) :: IOpId id :: elab rest
| [] -> []
| IPatId id :: rest -> IOpId id :: elab rest
| IPatAnon (One hint) ::rest -> IOpInaccessible hint :: elab rest
| IPatAnon Drop :: rest -> IOpDrop :: elab rest
| IPatAnon All :: rest -> IOpInaccessibleAll :: elab rest
| IPatAnon Temporary :: rest -> IOpTemporay :: elab rest
| IPatAbstractVars vs :: rest -> IOpAbstractVars vs :: elab rest
| IPatFastNondep :: rest -> IOpFastNondep :: elab rest
| IPatInj pats :: rest -> IOpInj (List.map elab pats) :: elab rest
| IPatRewrite(occ,dir) :: rest -> IOpRewrite(occ,dir) :: elab rest
| IPatView vs :: rest -> IOpView (None,vs) :: elab rest
| IPatSimpl s :: rest -> IOpSimpl s :: elab rest
| IPatClear cl :: rest -> IOpClear (cl,None) :: elab rest
| IPatCase (Block seed) :: rest -> IOpCaseBlock seed :: elab rest
| IPatCase (Regular bs) :: rest -> IOpCaseBranches (List.map elab bs) :: elab rest
| IPatDispatch (Block seed) :: rest -> IOpDispatchBlock seed :: elab rest
| IPatDispatch (Regular bs) :: rest -> IOpDispatchBranches (List.map elab bs) :: elab rest
| IPatNoop :: rest -> IOpNoop :: elab rest
in
elab l
;;
let tclCompileIPats l =
Ssrprinters.debug_ssr (fun () -> Pp.(str "tclCompileIPats input: " ++
prlist_with_sep spc Ssrprinters.pr_ipat l));
let ops = tclCompileIPats l in
Ssrprinters.debug_ssr (fun () -> Pp.(str "tclCompileIPats output: " ++
prlist_with_sep spc pr_ipatop ops));
ops
let main ?eqtac ~first_case_is_dispatch iops =
let ip_before, case, ip_after = split_at_first_case iops in
let case = ssr_exception first_case_is_dispatch case in
let case = option_to_list case in
let eqtac = option_to_list (Option.map (fun x -> IOpEqGen x) eqtac) in
let ipats = ip_before @ case @ eqtac @ ip_after in
Ssrcommon.tcl0G ~default:() (ipat_tac ipats <*> intro_end)
end
let tclIPAT_EQ eqtac ip =
Ssrprinters.debug_ssr (fun () -> Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip));
IpatMachine.(main ~eqtac ~first_case_is_dispatch:true (tclCompileIPats ip))
let tclIPATssr ip =
Ssrprinters.debug_ssr (fun () -> Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip));
IpatMachine.(main ~first_case_is_dispatch:true (tclCompileIPats ip))
let tclCompileIPats = IpatMachine.tclCompileIPats
let with_defective maintac deps clr = Goal.enter begin fun g ->
let sigma, concl = Goal.(sigma g, concl g) in
let top_id =
let open EConstr in
match kind_of_type sigma concl with
| ProdType ({binder_name=Name id}, _, _)
when Ssrcommon.is_discharged_id id -> id
| _ -> Ssrcommon.top_id in
let top_gen = Ssrequality.mkclr clr, Ssrmatching.cpattern_of_id top_id in
Ssrcommon.tclINTRO_ID top_id <*> maintac deps top_gen
end
let with_dgens { dgens; gens; clr } maintac = match gens with
| [] -> with_defective maintac dgens clr
| gen :: gens ->
Ssrcommon.genstac (gens, clr) <*> maintac dgens gen
let mkCoqEq env sigma =
let eq = Coqlib.((build_coq_eq_data ()).eq) in
let sigma, eq = EConstr.fresh_global env sigma eq in
eq, sigma
let mkCoqRefl t c env sigma =
let refl = Coqlib.((build_coq_eq_data()).refl) in
let sigma, refl = EConstr.fresh_global env sigma refl in
EConstr.mkApp (refl, [|t; c|]), sigma
(** Intro patterns processing for elim tactic, in particular when used in
conjunction with equation generation as in [elim E: x] *)
let elim_intro_tac ipats ?seed what eqid ssrelim is_rec clr =
let intro_eq =
match eqid with
| Some (IPatId ipat) when not is_rec ->
let rec intro_eq () = Goal.enter begin fun g ->
let sigma, env, concl = Goal.(sigma g, env g, concl g) in
let open EConstr in
match kind_of_type sigma concl with
| ProdType (_, src, tgt) -> begin
match kind_of_type sigma src with
| AtomicType (hd, _) when Ssrcommon.is_protect hd env sigma ->
Ssrcommon.unprotecttac <*>
Ssrcommon.tclINTRO_ID ipat
| _ -> Ssrcommon.tclINTRO_ANON () <*> intro_eq ()
end
|_ -> Ssrcommon.errorstrm (Pp.str "Too many names in intro pattern")
end in
intro_eq ()
| Some (IPatId ipat) ->
let intro_lhs = Goal.enter begin fun g ->
let sigma = Goal.sigma g in
let elim_name = match clr, what with
| [SsrHyp(_, x)], _ -> x
| _, Ssrelim.EConstr(_,_,t) when EConstr.isVar sigma t ->
EConstr.destVar sigma t
| _ -> Ssrcommon.mk_anon_id "K" (Tacmach.pf_ids_of_hyps g) in
Tacticals.tclFIRST
[ Ssrcommon.tclINTRO_ID elim_name
; Ssrcommon.tclINTRO_ANON ~seed:"K" ()]
end in
let rec gen_eq_tac () = Goal.enter begin fun g ->
let sigma, env, concl = Goal.(sigma g, env g, concl g) in
let sigma, eq =
EConstr.fresh_global env sigma (Coqlib.lib_ref "core.eq.type") in
let ctx, last = EConstr.decompose_prod_assum sigma concl in
let open EConstr in
let args = match kind_of_type sigma last with
| AtomicType (hd, args) ->
if Ssrcommon.is_protect hd env sigma then args
else Ssrcommon.errorstrm
(Pp.str "Too many names in intro pattern")
| _ -> assert false in
let case = args.(Array.length args-1) in
if not(EConstr.Vars.closed0 sigma case)
then Ssrcommon.tclINTRO_ANON () <*> gen_eq_tac ()
else
Ssrcommon.tacTYPEOF case >>= fun case_ty ->
let open EConstr in
let refl =
mkApp (eq, [|Vars.lift 1 case_ty; mkRel 1; Vars.lift 1 case|]) in
let name = Ssrcommon.mk_anon_id "K" (Tacmach.pf_ids_of_hyps g) in
let new_concl =
mkProd (make_annot (Name name) Sorts.Relevant, case_ty, mkArrow refl Sorts.Relevant (Vars.lift 2 concl)) in
let erefl, sigma = mkCoqRefl case_ty case env sigma in
Proofview.Unsafe.tclEVARS sigma <*>
Tactics.apply_type ~typecheck:true new_concl [case;erefl]
end in
gen_eq_tac () <*>
intro_lhs <*>
Ssrcommon.tclINTRO_ID ipat
| _ -> tclUNIT () in
let unprotect =
if eqid <> None && is_rec
then Ssrcommon.unprotecttac else tclUNIT () in
begin match seed with
| None -> ssrelim
| Some s -> IpatMachine.tclSEED_SUBGOALS s ssrelim end <*>
tclIPAT_EQ (intro_eq <*> unprotect) ipats
;;
let mkEq dir cl c t n env sigma =
let open EConstr in
let eqargs = [|t; c; c|] in
eqargs.(Ssrequality.dir_org dir) <- mkRel n;
let eq, sigma = mkCoqEq env sigma in
let refl, sigma = mkCoqRefl t c env sigma in
mkArrow (mkApp (eq, eqargs)) Sorts.Relevant (Vars.lift 1 cl), refl, sigma
(** in [tac/v: last gens..] the first (last to be run) generalization is
"special" in that is it also the main argument of [tac] and is eventually
to be processed forward with view [v]. The behavior implemented is
very close to [tac: (v last) gens..] but:
- [v last] may use a view adaptor
- eventually clear for [last] is taken into account
- [tac/v {clr}] is also supported, and [{clr}] is to be run later
The code here does not "grab" [v last] nor apply [v] to [last], see the
[tacVIEW_THEN_GRAB] combinator. *)
let tclLAST_GEN ~to_ind ((oclr, occ), t) conclusion = tclINDEPENDENTL begin
Goal.enter_one begin fun gl ->
let cl0, env, sigma, hyps = Goal.(concl gl, env gl, sigma gl, hyps gl) in
let sigma0 = sigma in
let pat = Ssrmatching.interp_cpattern env sigma t None in
let cl = Reductionops.nf_evar sigma cl0 in
let sigma, c, cl = Ssrmatching.fill_rel_occ_pattern env sigma cl pat occ in
let clr =
Ssrcommon.interp_clr sigma (oclr, (Ssrmatching.tag_of_cpattern t,c)) in
if not(Termops.occur_existential sigma c) then
if Ssrmatching.tag_of_cpattern t = Ssrmatching.WithAt then
if not (EConstr.isVar sigma c) then
Ssrcommon.errorstrm Pp.(str "@ can be used with variables only")
else match Context.Named.lookup (EConstr.destVar sigma c) hyps with
| Context.Named.Declaration.LocalAssum _ ->
Ssrcommon.errorstrm Pp.(str "@ can be used with let-ins only")
| Context.Named.Declaration.LocalDef (name, b, ty) ->
Unsafe.tclEVARS sigma <*>
tclUNIT (true, EConstr.mkLetIn (map_annot Name.mk_name name,b,ty,cl), c, clr)
else
Unsafe.tclEVARS sigma <*>
Ssrcommon.tacMKPROD c cl >>= fun ccl ->
tclUNIT (false, ccl, c, clr)
else
if to_ind && occ = None then
let p, _, ucst' = Ssrcommon.abs_evars env sigma0 (fst pat, c) in
let sigma = Evd.merge_universe_context sigma ucst' in
Unsafe.tclEVARS sigma <*>
Ssrcommon.tacTYPEOF p >>= fun pty ->
let ccl = EConstr.mkProd (make_annot (Ssrcommon.constr_name sigma c) Sorts.Relevant, pty, cl0) in
tclUNIT (false, ccl, p, clr)
else
Ssrcommon.errorstrm Pp.(str "generalized term didn't match")
end end >>= begin
fun infos -> tclDISPATCH (infos |> List.map conclusion)
end
(** a typical mate of [tclLAST_GEN] doing the job of applying the views [cs]
to [c] and generalizing the resulting term *)
let tacVIEW_THEN_GRAB ?(simple_types=true)
vs ~conclusion (is_letin, new_concl, c, clear)
=
Ssrview.tclWITH_FWD_VIEWS ~simple_types ~subject:c ~views:vs
~conclusion:(fun t ->
Ssrcommon.tacCONSTR_NAME c >>= fun name ->
Goal.enter_one ~__LOC__ begin fun g ->
let sigma, env = Goal.sigma g, Goal.env g in
Ssrcommon.tacMKPROD t ~name
(Termops.subst_term sigma t
(Termops.prod_applist sigma new_concl [c])) >>=
conclusion is_letin t clear
end)
let ssrelimtac (view, (eqid, (dgens, ipats))) =
let ndefectelimtac view eqid ipats deps gen =
match view with
| [v] ->
Ssrcommon.tclINTERP_AST_CLOSURE_TERM_AS_CONSTR v >>= fun cs ->
tclDISPATCH (List.map (fun elim ->
(Ssrelim.ssrelim deps (Ssrelim.EGen gen) ~elim eqid (elim_intro_tac ipats)))
cs)
| [] ->
tclINDEPENDENT
(Ssrelim.ssrelim deps (Ssrelim.EGen gen) eqid (elim_intro_tac ipats))
| _ ->
Ssrcommon.errorstrm
Pp.(str "elim: only one elimination lemma can be provided")
in
with_dgens dgens (ndefectelimtac view eqid ipats)
let ssrcasetac (view, (eqid, (dgens, ipats))) =
let ndefectcasetac view eqid ipats deps ((_, occ), _ as gen) =
tclLAST_GEN ~to_ind:true gen (fun (_, cl, c, clear as info) ->
let conclusion _ vc _clear _cl =
Ssrcommon.tacIS_INJECTION_CASE vc >>= fun inj ->
let simple = (eqid = None && deps = [] && occ = None) in
if simple && inj then
Ssrelim.perform_injection vc <*>
Tactics.clear (List.map Ssrcommon.hyp_id clear) <*>
tclIPATssr ipats
else
let deps, clear, occ =
if view <> [] && eqid <> None && deps = []
then [gen], [], None
else deps, clear, occ in
Ssrelim.ssrelim ~is_case:true deps (Ssrelim.EConstr (clear, occ, vc))
eqid (elim_intro_tac ipats)
in
if view = [] then conclusion false c clear c
else tacVIEW_THEN_GRAB ~simple_types:false view ~conclusion info)
in
with_dgens dgens (ndefectcasetac view eqid ipats)
let ssrscasetoptac = Ssrcommon.tclWITHTOP Ssrelim.ssrscase_or_inj_tac
let ssrselimtoptac = Ssrcommon.tclWITHTOP Ssrelim.elimtac
(** [move] **************************************************************)
let pushmoveeqtac cl c = Goal.enter begin fun g ->
let env, sigma = Goal.(env g, sigma g) in
let x, t, cl1 = EConstr.destProd sigma cl in
let cl2, eqc, sigma = mkEq R2L cl1 c t 1 env sigma in
Unsafe.tclEVARS sigma <*>
Tactics.apply_type ~typecheck:true (EConstr.mkProd (x, t, cl2)) [c; eqc]
end
let eqmovetac _ gen =
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 (sigma, (cl, c, _)) = Ssrcommon.interp_gen env sigma ~concl false gen in
Proofview.Unsafe.tclEVARS sigma <*> pushmoveeqtac cl c
end
let rec eqmoveipats eqpat = function
| (IOpSimpl _ | IOpClear _ as ipat) :: ipats ->
ipat :: eqmoveipats eqpat ipats
| (IOpInaccessibleAll :: _ | []) as ipats ->
IOpInaccessible None :: eqpat @ ipats
| ipat :: ipats ->
ipat :: eqpat @ ipats
let ssrsmovetac = Goal.enter begin fun g ->
let sigma, concl = Goal.(sigma g, concl g) in
match EConstr.kind sigma concl with
| Prod _ | LetIn _ -> tclUNIT ()
| _ -> Tactics.hnf_in_concl
end
let tclIPAT ip =
IpatMachine.main ~first_case_is_dispatch:false ip
let ssrmovetac = function
| _::_ as view, (_, ({ gens = lastgen :: gens; clr }, ipats)) ->
let gentac = Ssrcommon.genstac (gens, []) in
let conclusion _ t clear ccl =
Tactics.apply_type ~typecheck:true ccl [t] <*>
Tactics.clear (List.map Ssrcommon.hyp_id clear) in
gentac <*>
tclLAST_GEN ~to_ind:false lastgen
(tacVIEW_THEN_GRAB view ~conclusion) <*>
tclIPAT (IOpClear (clr,None) :: IpatMachine.tclCompileIPats ipats)
| _::_ as view, (_, ({ gens = []; clr }, ipats)) ->
tclIPAT (IOpView (None,view) :: IOpClear (clr,None) :: IpatMachine.tclCompileIPats ipats)
| _, (Some pat, (dgens, ipats)) ->
let dgentac = with_dgens dgens eqmovetac in
dgentac <*> tclIPAT (eqmoveipats (IpatMachine.tclCompileIPats [pat]) (IpatMachine.tclCompileIPats ipats))
| _, (_, ({ gens = (_ :: _ as gens); dgens = []; clr}, ipats)) ->
let gentac = Ssrcommon.genstac (gens, clr) in
gentac <*> tclIPAT (IpatMachine.tclCompileIPats ipats)
| _, (_, ({ clr }, ipats)) ->
Tacticals.tclTHENLIST [ssrsmovetac; Tactics.clear (List.map Ssrcommon.hyp_id clr); tclIPAT (IpatMachine.tclCompileIPats ipats)]
(** [abstract: absvar gens] **************************************************)
let rec is_Evar_or_CastedMeta sigma x =
EConstr.isEvar sigma x ||
EConstr.isMeta sigma x ||
(EConstr.isCast sigma x &&
is_Evar_or_CastedMeta sigma (pi1 (EConstr.destCast sigma x)))
let occur_existential_or_casted_meta sigma c =
let rec occrec c = match EConstr.kind sigma c with
| Evar _ -> raise Not_found
| Cast (m,_,_) when EConstr.isMeta sigma m -> raise Not_found
| _ -> EConstr.iter sigma occrec c
in
try occrec c; false
with Not_found -> true
let examine_abstract env sigma id =
let (sigma, tid) = Typing.type_of env sigma id in
let abstract = Ssrcommon.mkSsrRef "abstract" in
let err () =
Ssrcommon.errorstrm
Pp.(strbrk"not a proper abstract constant: "++
Printer.pr_econstr_env env sigma id) in
if not (EConstr.isApp sigma tid) then err ();
let hd, args_id = EConstr.destApp sigma tid in
if not (EConstr.isRefX sigma abstract hd) then err ();
if Array.length args_id <> 3 then err ();
if not (is_Evar_or_CastedMeta sigma args_id.(2)) then
Ssrcommon.errorstrm Pp.(strbrk"abstract constant "++
Printer.pr_econstr_env env sigma id++str" already used");
sigma, (tid, args_id)
let tacEXAMINE_ABSTRACT id =
Goal.enter_one ~__LOC__ begin fun g ->
let sigma, env = Goal.(sigma g, env g) in
let sigma, ans = examine_abstract env sigma id in
Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT ans
end
let find_abstract_proof env sigma check_lock abstract_n =
let abstract = Ssrcommon.mkSsrRef "abstract" in
let l = Evd.fold_undefined (fun e ei l ->
match EConstr.kind sigma ei.Evd.evar_concl with
| App(hd, [|ty; n; lock|])
when (not check_lock ||
(occur_existential_or_casted_meta sigma ty &&
is_Evar_or_CastedMeta sigma lock)) &&
EConstr.isRefX sigma abstract hd &&
EConstr.eq_constr_nounivs sigma n abstract_n -> e :: l
| _ -> l) sigma [] in
match l with
| [e] -> e
| _ -> Ssrcommon.errorstrm
Pp.(strbrk"abstract constant "++
Printer.pr_econstr_env env sigma abstract_n ++
strbrk" not found in the evar map exactly once. "++
strbrk"Did you tamper with it?")
let tacFIND_ABSTRACT_PROOF check_lock abstract_n =
Goal.enter_one ~__LOC__ begin fun g ->
let sigma, env = Goal.(sigma g, env g) in
tclUNIT (find_abstract_proof env sigma check_lock abstract_n)
end
let ssrabstract dgens =
let main _ (_,cid) = Goal.enter begin fun g ->
Ssrcommon.tacMK_SSR_CONST "abstract" >>= fun abstract ->
Ssrcommon.tacMK_SSR_CONST "abstract_key" >>= fun abstract_key ->
Ssrcommon.tacINTERP_CPATTERN cid >>= fun cid ->
let id = EConstr.mkVar (Option.get (Ssrmatching.id_of_pattern (Goal.sigma g) cid)) in
tacEXAMINE_ABSTRACT id >>= fun (idty, args_id) ->
let abstract_n = args_id.(1) in
tacFIND_ABSTRACT_PROOF true abstract_n >>= fun abstract_proof ->
let tacFIND_HOLE = Goal.enter_one ~__LOC__ begin fun g ->
let sigma, env, concl = Goal.(sigma g, env g, concl g) in
let t = args_id.(0) in
match EConstr.kind sigma t with
| (Evar _ | Meta _) -> Ssrcommon.tacUNIFY concl t <*> tclUNIT id
| Cast(m,_,_)
when EConstr.isEvar sigma m || EConstr.isMeta sigma m ->
Ssrcommon.tacUNIFY concl t <*> tclUNIT id
| _ ->
Ssrcommon.errorstrm
Pp.(strbrk"abstract constant "++
Printer.pr_econstr_env env sigma abstract_n ++
strbrk" has an unexpected shape. Did you tamper with it?")
end in
tacFIND_HOLE >>= fun proof ->
Ssrcommon.tacUNIFY abstract_key args_id.(2) <*>
Ssrcommon.tacTYPEOF idty >>= fun _ ->
Unsafe.tclGETGOALS >>= fun goals ->
Unsafe.tclSETGOALS
(goals @ [Proofview_monad.with_empty_state abstract_proof]) <*>
tclDISPATCH [
Tacticals.tclSOLVE [Tactics.apply proof];
Ssrcommon.unfold[abstract;abstract_key]
]
end in
let interp_gens { gens } ~conclusion = Goal.enter begin fun gl ->
let open Ssrmatching in
let open Tacmach in
let ipats = List.map (fun (_,cp) ->
match id_of_pattern (project gl) (interp_cpattern (pf_env gl) (project gl) cp None) with
| None -> IPatAnon (One None)
| Some id -> IPatId id)
(List.tl gens) in
conclusion ipats
end in
interp_gens dgens ~conclusion:(fun ipats ->
with_dgens dgens main <*>
tclIPATssr ipats)
module Internal = struct
let find_abstract_proof = find_abstract_proof
let examine_abstract = examine_abstract
end