forked from coq/coq
-
Notifications
You must be signed in to change notification settings - Fork 2
/
tac2core.ml
2354 lines (2052 loc) · 77 KB
/
tac2core.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
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Util
open Pp
open Names
open Genarg
open Tac2ffi
open Tac2env
open Tac2expr
open Tac2entries.Pltac
open Proofview.Notations
let ltac2_plugin = "coq-core.plugins.ltac2"
let constr_flags =
let open Pretyping in
{
use_coercions = true;
use_typeclasses = Pretyping.UseTC;
solve_unification_constraints = true;
fail_evar = true;
expand_evars = true;
program_mode = false;
polymorphic = false;
}
let open_constr_no_classes_flags =
let open Pretyping in
{
use_coercions = true;
use_typeclasses = Pretyping.NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = false;
program_mode = false;
polymorphic = false;
}
let preterm_flags =
let open Pretyping in
{
use_coercions = true;
use_typeclasses = Pretyping.NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = false;
program_mode = false;
polymorphic = false;
}
(** Standard values *)
let val_format = Tac2print.val_format
let format = repr_ext val_format
let core_prefix path n = KerName.make path (Label.of_id (Id.of_string_soft n))
let std_core n = core_prefix Tac2env.std_prefix n
let coq_core n = core_prefix Tac2env.coq_prefix n
let ltac1_core n = core_prefix Tac2env.ltac1_prefix n
module Core =
struct
let t_int = coq_core "int"
let t_string = coq_core "string"
let t_array = coq_core "array"
let t_unit = coq_core "unit"
let t_list = coq_core "list"
let t_constr = coq_core "constr"
let t_preterm = coq_core "preterm"
let t_pattern = coq_core "pattern"
let t_ident = coq_core "ident"
let t_option = coq_core "option"
let t_exn = coq_core "exn"
let t_reference = std_core "reference"
let t_ltac1 = ltac1_core "t"
let c_nil = coq_core "[]"
let c_cons = coq_core "::"
let c_none = coq_core "None"
let c_some = coq_core "Some"
let c_true = coq_core "true"
let c_false = coq_core "false"
end
open Core
let v_unit = Tac2ffi.of_unit ()
let v_blk = Valexpr.make_block
let of_relevance = function
| Sorts.Relevant -> ValInt 0
| Sorts.Irrelevant -> ValInt 1
| Sorts.RelevanceVar q -> ValBlk (0, [|of_ext val_qvar q|])
let to_relevance = function
| ValInt 0 -> Sorts.Relevant
| ValInt 1 -> Sorts.Irrelevant
| ValBlk (0, [|qvar|]) ->
let qvar = to_ext val_qvar qvar in
Sorts.RelevanceVar qvar
| _ -> assert false
let relevance = make_repr of_relevance to_relevance
let of_binder b =
Tac2ffi.of_ext Tac2ffi.val_binder b
let to_binder b =
Tac2ffi.to_ext Tac2ffi.val_binder b
let of_instance u =
let u = UVars.Instance.to_array (EConstr.Unsafe.to_instance u) in
let toqs = Tac2ffi.of_array (fun v -> Tac2ffi.of_ext Tac2ffi.val_quality v) in
let tous = Tac2ffi.of_array (fun v -> Tac2ffi.of_ext Tac2ffi.val_univ v) in
Tac2ffi.of_pair toqs tous u
let to_instance u =
let toqs = Tac2ffi.to_array (fun v -> Tac2ffi.to_ext Tac2ffi.val_quality v) in
let tous = Tac2ffi.to_array (fun v -> Tac2ffi.to_ext Tac2ffi.val_univ v) in
let u = Tac2ffi.to_pair toqs tous u in
EConstr.EInstance.make (UVars.Instance.of_array u)
let of_rec_declaration (nas, ts, cs) =
let binders = Array.map2 (fun na t -> (na, t)) nas ts in
(Tac2ffi.of_array of_binder binders,
Tac2ffi.of_array Tac2ffi.of_constr cs)
let to_rec_declaration (nas, cs) =
let nas = Tac2ffi.to_array to_binder nas in
(Array.map fst nas,
Array.map snd nas,
Tac2ffi.to_array Tac2ffi.to_constr cs)
let of_case_invert = let open Constr in function
| NoInvert -> ValInt 0
| CaseInvert {indices} ->
v_blk 0 [|of_array of_constr indices|]
let to_case_invert = let open Constr in function
| ValInt 0 -> NoInvert
| ValBlk (0, [|indices|]) ->
let indices = to_array to_constr indices in
CaseInvert {indices}
| _ -> CErrors.anomaly Pp.(str "unexpected value shape")
let of_result f = function
| Inl c -> v_blk 0 [|f c|]
| Inr e -> v_blk 1 [|Tac2ffi.of_exn e|]
let inductive = repr_ext val_inductive
let projection = repr_ext val_projection
(** Stdlib exceptions *)
let err_notfocussed =
Tac2interp.LtacError (coq_core "Not_focussed", [||])
let err_outofbounds =
Tac2interp.LtacError (coq_core "Out_of_bounds", [||])
let err_notfound =
Tac2interp.LtacError (coq_core "Not_found", [||])
let err_matchfailure =
Tac2interp.LtacError (coq_core "Match_failure", [||])
let err_division_by_zero =
Tac2interp.LtacError (coq_core "Division_by_zero", [||])
(** Helper functions *)
let thaw f = Tac2ffi.apply f [v_unit]
let fatal_flag : unit Exninfo.t = Exninfo.make ()
let has_fatal_flag info = match Exninfo.get info fatal_flag with
| None -> false
| Some () -> true
let set_bt info =
if !Tac2bt.print_ltac2_backtrace then
Tac2bt.get_backtrace >>= fun bt ->
Proofview.tclUNIT (Exninfo.add info Tac2bt.backtrace bt)
else Proofview.tclUNIT info
let throw ?(info = Exninfo.null) e =
set_bt info >>= fun info ->
let info = Exninfo.add info fatal_flag () in
Proofview.tclLIFT (Proofview.NonLogical.raise (e, info))
let fail ?(info = Exninfo.null) e =
set_bt info >>= fun info ->
Proofview.tclZERO ~info e
let return x = Proofview.tclUNIT x
let pname ?(plugin=ltac2_plugin) s = { mltac_plugin = plugin; mltac_tactic = s }
let catchable_exception = function
| Logic_monad.Exception _ -> false
| e -> CErrors.noncritical e
(* Adds ltac2 backtrace
With [passthrough:false], acts like [Proofview.wrap_exceptions] + Ltac2 backtrace handling
*)
let wrap_exceptions ?(passthrough=false) f =
try f ()
with e ->
let e, info = Exninfo.capture e in
set_bt info >>= fun info ->
if not passthrough && catchable_exception e
then begin if has_fatal_flag info
then Proofview.tclLIFT (Proofview.NonLogical.raise (e, info))
else Proofview.tclZERO ~info e
end
else Exninfo.iraise (e, info)
let assert_focussed =
Proofview.Goal.goals >>= fun gls ->
match gls with
| [_] -> Proofview.tclUNIT ()
| [] | _ :: _ :: _ -> throw err_notfocussed
let pf_apply ?(catch_exceptions=false) f =
let f env sigma = wrap_exceptions ~passthrough:(not catch_exceptions) (fun () -> f env sigma) in
Proofview.Goal.goals >>= function
| [] ->
Proofview.tclENV >>= fun env ->
Proofview.tclEVARMAP >>= fun sigma ->
f env sigma
| [gl] ->
gl >>= fun gl ->
f (Proofview.Goal.env gl) (Tacmach.project gl)
| _ :: _ :: _ ->
throw err_notfocussed
open Tac2externals
let define ?plugin s = define (pname ?plugin s)
(** Printing *)
let () = define "print" (pp @-> ret unit) Feedback.msg_notice
let () = define "message_of_int" (int @-> ret pp) Pp.int
let () = define "message_of_string" (string @-> ret pp) Pp.str
let () = define "message_to_string" (pp @-> ret string) Pp.string_of_ppcmds
let () =
define "message_of_constr" (constr @-> tac pp) @@ fun c ->
pf_apply @@ fun env sigma -> return (Printer.pr_econstr_env env sigma c)
let () = define "message_of_ident" (ident @-> ret pp) Id.print
let () =
define "message_of_exn" (valexpr @-> eret pp) @@ fun v env sigma ->
Tac2print.pr_valexpr env sigma v (GTypRef (Other Core.t_exn, []))
let () = define "message_concat" (pp @-> pp @-> ret pp) Pp.app
let () = define "format_stop" (ret format) []
let () =
define "format_string" (format @-> ret format) @@ fun s ->
Tac2print.FmtString :: s
let () =
define "format_int" (format @-> ret format) @@ fun s ->
Tac2print.FmtInt :: s
let () =
define "format_constr" (format @-> ret format) @@ fun s ->
Tac2print.FmtConstr :: s
let () =
define "format_ident" (format @-> ret format) @@ fun s ->
Tac2print.FmtIdent :: s
let () =
define "format_literal" (string @-> format @-> ret format) @@ fun lit s ->
Tac2print.FmtLiteral lit :: s
let () =
define "format_alpha" (format @-> ret format) @@ fun s ->
Tac2print.FmtAlpha :: s
let () =
define "format_kfprintf" (closure @-> format @-> tac valexpr) @@ fun k fmt ->
let open Tac2print in
let fold accu = function
| FmtLiteral _ -> accu
| FmtString | FmtInt | FmtConstr | FmtIdent -> 1 + accu
| FmtAlpha -> 2 + accu
in
let pop1 l = match l with [] -> assert false | x :: l -> (x, l) in
let pop2 l = match l with [] | [_] -> assert false | x :: y :: l -> (x, y, l) in
let arity = List.fold_left fold 0 fmt in
let rec eval accu args fmt = match fmt with
| [] -> apply k [of_pp accu]
| tag :: fmt ->
match tag with
| FmtLiteral s ->
eval (Pp.app accu (Pp.str s)) args fmt
| FmtString ->
let (s, args) = pop1 args in
let pp = Pp.str (to_string s) in
eval (Pp.app accu pp) args fmt
| FmtInt ->
let (i, args) = pop1 args in
let pp = Pp.int (to_int i) in
eval (Pp.app accu pp) args fmt
| FmtConstr ->
let (c, args) = pop1 args in
let c = to_constr c in
pf_apply begin fun env sigma ->
let pp = Printer.pr_econstr_env env sigma c in
eval (Pp.app accu pp) args fmt
end
| FmtIdent ->
let (i, args) = pop1 args in
let pp = Id.print (to_ident i) in
eval (Pp.app accu pp) args fmt
| FmtAlpha ->
let (f, x, args) = pop2 args in
Tac2ffi.apply (to_closure f) [of_unit (); x] >>= fun pp ->
eval (Pp.app accu (to_pp pp)) args fmt
in
let eval v = eval (Pp.mt ()) v fmt in
if Int.equal arity 0 then eval []
else return (Tac2ffi.of_closure (Tac2ffi.abstract arity eval))
(** Array *)
let () = define "array_empty" (ret valexpr) (v_blk 0 [||])
let () =
define "array_make" (int @-> valexpr @-> tac valexpr) @@ fun n x ->
try return (v_blk 0 (Array.make n x)) with Invalid_argument _ -> throw err_outofbounds
let () =
define "array_length" (block @-> ret int) @@ fun (_, v) -> Array.length v
let () =
define "array_set" (block @-> int @-> valexpr @-> tac unit) @@ fun (_, v) n x ->
try Array.set v n x; return () with Invalid_argument _ -> throw err_outofbounds
let () =
define "array_get" (block @-> int @-> tac valexpr) @@ fun (_, v) n ->
try return (Array.get v n) with Invalid_argument _ -> throw err_outofbounds
let () =
define "array_blit"
(block @-> int @-> block @-> int @-> int @-> tac unit)
@@ fun (_, v0) s0 (_, v1) s1 l ->
try Array.blit v0 s0 v1 s1 l; return () with Invalid_argument _ ->
throw err_outofbounds
let () =
define "array_fill" (block @-> int @-> int @-> valexpr @-> tac unit) @@ fun (_, d) s l v ->
try Array.fill d s l v; return () with Invalid_argument _ -> throw err_outofbounds
let () =
define "array_concat" (list block @-> ret valexpr) @@ fun l ->
v_blk 0 (Array.concat (List.map snd l))
(** Ident *)
let () = define "ident_equal" (ident @-> ident @-> ret bool) Id.equal
let () = define "ident_to_string" (ident @-> ret string) Id.to_string
let () =
define "ident_of_string" (string @-> ret (option ident)) @@ fun s ->
try Some (Id.of_string s) with e when CErrors.noncritical e -> None
(** Int *)
let () = define "int_equal" (int @-> int @-> ret bool) (==)
let () = define "int_neg" (int @-> ret int) (~-)
let () = define "int_abs" (int @-> ret int) abs
let () = define "int_compare" (int @-> int @-> ret int) Int.compare
let () = define "int_add" (int @-> int @-> ret int) (+)
let () = define "int_sub" (int @-> int @-> ret int) (-)
let () = define "int_mul" (int @-> int @-> ret int) ( * )
let () = define "int_div" (int @-> int @-> tac int) @@ fun m n ->
if n == 0 then throw err_division_by_zero else return (m / n)
let () = define "int_mod" (int @-> int @-> tac int) @@ fun m n ->
if n == 0 then throw err_division_by_zero else return (m mod n)
let () = define "int_asr" (int @-> int @-> ret int) (asr)
let () = define "int_lsl" (int @-> int @-> ret int) (lsl)
let () = define "int_lsr" (int @-> int @-> ret int) (lsr)
let () = define "int_land" (int @-> int @-> ret int) (land)
let () = define "int_lor" (int @-> int @-> ret int) (lor)
let () = define "int_lxor" (int @-> int @-> ret int) (lxor)
let () = define "int_lnot" (int @-> ret int) lnot
(** Char *)
let () = define "char_of_int" (int @-> ret char) Char.chr
let () = define "char_to_int" (char @-> ret int) Char.code
(** String *)
let () =
define "string_make" (int @-> char @-> tac bytes) @@ fun n c ->
try return (Bytes.make n c) with Invalid_argument _ -> throw err_outofbounds
let () = define "string_length" (bytes @-> ret int) Bytes.length
let () =
define "string_set" (bytes @-> int @-> char @-> tac unit) @@ fun s n c ->
try Bytes.set s n c; return () with Invalid_argument _ -> throw err_outofbounds
let () =
define "string_get" (bytes @-> int @-> tac char) @@ fun s n ->
try return (Bytes.get s n) with Invalid_argument _ -> throw err_outofbounds
let () = define "string_concat" (bytes @-> list bytes @-> ret bytes) Bytes.concat
let () =
define "string_app" (bytes @-> bytes @-> ret bytes) @@ fun a b ->
Bytes.concat Bytes.empty [a; b]
let () = define "string_equal" (bytes @-> bytes @-> ret bool) Bytes.equal
let () = define "string_compare" (bytes @-> bytes @-> ret int) Bytes.compare
(** Terms *)
(** constr -> constr *)
let () =
define "constr_type" (constr @-> tac valexpr) @@ fun c ->
let get_type env sigma =
let (sigma, t) = Typing.type_of env sigma c in
let t = Tac2ffi.of_constr t in
Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT t
in
pf_apply ~catch_exceptions:true get_type
(** constr -> constr *)
let () =
define "constr_equal" (constr @-> constr @-> tac bool) @@ fun c1 c2 ->
Proofview.tclEVARMAP >>= fun sigma -> return (EConstr.eq_constr sigma c1 c2)
let () =
define "constr_kind" (constr @-> eret valexpr) @@ fun c env sigma ->
let open Constr in
match EConstr.kind sigma c with
| Rel n ->
v_blk 0 [|Tac2ffi.of_int n|]
| Var id ->
v_blk 1 [|Tac2ffi.of_ident id|]
| Meta n ->
v_blk 2 [|Tac2ffi.of_int n|]
| Evar (evk, args) ->
let args = Evd.expand_existential sigma (evk, args) in
v_blk 3 [|
Tac2ffi.of_evar evk;
Tac2ffi.of_array Tac2ffi.of_constr (Array.of_list args);
|]
| Sort s ->
v_blk 4 [|Tac2ffi.of_ext Tac2ffi.val_sort s|]
| Cast (c, k, t) ->
v_blk 5 [|
Tac2ffi.of_constr c;
Tac2ffi.of_ext Tac2ffi.val_cast k;
Tac2ffi.of_constr t;
|]
| Prod (na, t, u) ->
v_blk 6 [|
of_binder (na, t);
Tac2ffi.of_constr u;
|]
| Lambda (na, t, c) ->
v_blk 7 [|
of_binder (na, t);
Tac2ffi.of_constr c;
|]
| LetIn (na, b, t, c) ->
v_blk 8 [|
of_binder (na, t);
Tac2ffi.of_constr b;
Tac2ffi.of_constr c;
|]
| App (c, cl) ->
v_blk 9 [|
Tac2ffi.of_constr c;
Tac2ffi.of_array Tac2ffi.of_constr cl;
|]
| Const (cst, u) ->
v_blk 10 [|
Tac2ffi.of_constant cst;
of_instance u;
|]
| Ind (ind, u) ->
v_blk 11 [|
Tac2ffi.of_ext Tac2ffi.val_inductive ind;
of_instance u;
|]
| Construct (cstr, u) ->
v_blk 12 [|
Tac2ffi.of_ext Tac2ffi.val_constructor cstr;
of_instance u;
|]
| Case (ci, u, pms, c, iv, t, bl) ->
(* FIXME: also change representation Ltac2-side? *)
let (ci, c, iv, t, bl) = EConstr.expand_case env sigma (ci, u, pms, c, iv, t, bl) in
v_blk 13 [|
Tac2ffi.of_ext Tac2ffi.val_case ci;
Tac2ffi.of_constr c;
of_case_invert iv;
Tac2ffi.of_constr t;
Tac2ffi.of_array Tac2ffi.of_constr bl;
|]
| Fix ((recs, i), def) ->
let (nas, cs) = of_rec_declaration def in
v_blk 14 [|
Tac2ffi.of_array Tac2ffi.of_int recs;
Tac2ffi.of_int i;
nas;
cs;
|]
| CoFix (i, def) ->
let (nas, cs) = of_rec_declaration def in
v_blk 15 [|
Tac2ffi.of_int i;
nas;
cs;
|]
| Proj (p, r, c) ->
v_blk 16 [|
Tac2ffi.of_ext Tac2ffi.val_projection p;
of_relevance r;
Tac2ffi.of_constr c;
|]
| Int n ->
v_blk 17 [|Tac2ffi.of_uint63 n|]
| Float f ->
v_blk 18 [|Tac2ffi.of_float f|]
| Array(u,t,def,ty) ->
v_blk 19 [|
of_instance u;
Tac2ffi.of_array Tac2ffi.of_constr t;
Tac2ffi.of_constr def;
Tac2ffi.of_constr ty;
|]
let () =
define "constr_make" (valexpr @-> eret constr) @@ fun knd env sigma ->
match Tac2ffi.to_block knd with
| (0, [|n|]) ->
let n = Tac2ffi.to_int n in
EConstr.mkRel n
| (1, [|id|]) ->
let id = Tac2ffi.to_ident id in
EConstr.mkVar id
| (2, [|n|]) ->
let n = Tac2ffi.to_int n in
EConstr.mkMeta n
| (3, [|evk; args|]) ->
let evk = to_evar evk in
let args = Tac2ffi.to_array Tac2ffi.to_constr args in
EConstr.mkLEvar sigma (evk, Array.to_list args)
| (4, [|s|]) ->
let s = Tac2ffi.to_ext Tac2ffi.val_sort s in
EConstr.mkSort s
| (5, [|c; k; t|]) ->
let c = Tac2ffi.to_constr c in
let k = Tac2ffi.to_ext Tac2ffi.val_cast k in
let t = Tac2ffi.to_constr t in
EConstr.mkCast (c, k, t)
| (6, [|na; u|]) ->
let (na, t) = to_binder na in
let u = Tac2ffi.to_constr u in
EConstr.mkProd (na, t, u)
| (7, [|na; c|]) ->
let (na, t) = to_binder na in
let u = Tac2ffi.to_constr c in
EConstr.mkLambda (na, t, u)
| (8, [|na; b; c|]) ->
let (na, t) = to_binder na in
let b = Tac2ffi.to_constr b in
let c = Tac2ffi.to_constr c in
EConstr.mkLetIn (na, b, t, c)
| (9, [|c; cl|]) ->
let c = Tac2ffi.to_constr c in
let cl = Tac2ffi.to_array Tac2ffi.to_constr cl in
EConstr.mkApp (c, cl)
| (10, [|cst; u|]) ->
let cst = Tac2ffi.to_constant cst in
let u = to_instance u in
EConstr.mkConstU (cst, u)
| (11, [|ind; u|]) ->
let ind = Tac2ffi.to_ext Tac2ffi.val_inductive ind in
let u = to_instance u in
EConstr.mkIndU (ind, u)
| (12, [|cstr; u|]) ->
let cstr = Tac2ffi.to_ext Tac2ffi.val_constructor cstr in
let u = to_instance u in
EConstr.mkConstructU (cstr, u)
| (13, [|ci; c; iv; t; bl|]) ->
let ci = Tac2ffi.to_ext Tac2ffi.val_case ci in
let c = Tac2ffi.to_constr c in
let iv = to_case_invert iv in
let t = Tac2ffi.to_constr t in
let bl = Tac2ffi.to_array Tac2ffi.to_constr bl in
EConstr.mkCase (EConstr.contract_case env sigma (ci, c, iv, t, bl))
| (14, [|recs; i; nas; cs|]) ->
let recs = Tac2ffi.to_array Tac2ffi.to_int recs in
let i = Tac2ffi.to_int i in
let def = to_rec_declaration (nas, cs) in
EConstr.mkFix ((recs, i), def)
| (15, [|i; nas; cs|]) ->
let i = Tac2ffi.to_int i in
let def = to_rec_declaration (nas, cs) in
EConstr.mkCoFix (i, def)
| (16, [|p; r; c|]) ->
let p = Tac2ffi.to_ext Tac2ffi.val_projection p in
let r = to_relevance r in
let c = Tac2ffi.to_constr c in
EConstr.mkProj (p, r, c)
| (17, [|n|]) ->
let n = Tac2ffi.to_uint63 n in
EConstr.mkInt n
| (18, [|f|]) ->
let f = Tac2ffi.to_float f in
EConstr.mkFloat f
| (19, [|u;t;def;ty|]) ->
let t = Tac2ffi.to_array Tac2ffi.to_constr t in
let def = Tac2ffi.to_constr def in
let ty = Tac2ffi.to_constr ty in
let u = to_instance u in
EConstr.mkArray(u,t,def,ty)
| _ -> assert false
let () =
define "constr_check" (constr @-> tac valexpr) @@ fun c ->
pf_apply @@ fun env sigma ->
try
let (sigma, _) = Typing.type_of env sigma c in
Proofview.Unsafe.tclEVARS sigma >>= fun () ->
return (of_result Tac2ffi.of_constr (Inl c))
with e when CErrors.noncritical e ->
let e = Exninfo.capture e in
return (of_result Tac2ffi.of_constr (Inr e))
let () =
define "constr_liftn" (int @-> int @-> constr @-> ret constr)
EConstr.Vars.liftn
let () =
define "constr_substnl" (list constr @-> int @-> constr @-> ret constr)
EConstr.Vars.substnl
let () =
define "constr_closenl" (list ident @-> int @-> constr @-> tac constr)
@@ fun ids k c ->
Proofview.tclEVARMAP >>= fun sigma ->
return (EConstr.Vars.substn_vars sigma k ids c)
let () =
define "constr_closedn" (int @-> constr @-> tac bool) @@ fun n c ->
Proofview.tclEVARMAP >>= fun sigma ->
return (EConstr.Vars.closedn sigma n c)
let () =
define "constr_occur_between" (int @-> int @-> constr @-> tac bool) @@ fun n m c ->
Proofview.tclEVARMAP >>= fun sigma ->
return (EConstr.Vars.noccur_between sigma n m c)
let () =
define "constr_case" (inductive @-> tac valexpr) @@ fun ind ->
Proofview.tclENV >>= fun env ->
try
let ans = Inductiveops.make_case_info env ind Sorts.Relevant Constr.RegularStyle in
return (Tac2ffi.of_ext Tac2ffi.val_case ans)
with e when CErrors.noncritical e ->
throw err_notfound
let () = define "constr_cast_default" (ret valexpr) (of_cast DEFAULTcast)
let () = define "constr_cast_vm" (ret valexpr) (of_cast VMcast)
let () = define "constr_cast_native" (ret valexpr) (of_cast NATIVEcast)
let () =
define "constr_in_context" (ident @-> constr @-> closure @-> tac constr) @@ fun id t c ->
Proofview.Goal.goals >>= function
| [gl] ->
gl >>= fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let has_var =
try
let _ = Environ.lookup_named id env in
true
with Not_found -> false
in
if has_var then
Tacticals.tclZEROMSG (str "Variable already exists")
else
let open Context.Named.Declaration in
let sigma, t_rel =
let t_ty = Retyping.get_type_of env sigma t in
(* If the user passed eg ['_] for the type we force it to indeed be a type *)
let sigma, j = Typing.type_judgment env sigma {uj_val=t; uj_type=t_ty} in
sigma, EConstr.ESorts.relevance_of_sort sigma j.utj_type
in
let nenv = EConstr.push_named (LocalAssum (Context.make_annot id t_rel, t)) env in
let (sigma, (evt, _)) = Evarutil.new_type_evar nenv sigma Evd.univ_flexible in
let (sigma, evk) = Evarutil.new_pure_evar (Environ.named_context_val nenv) sigma evt in
Proofview.Unsafe.tclEVARS sigma >>= fun () ->
Proofview.Unsafe.tclSETGOALS [Proofview.with_empty_state evk] >>= fun () ->
thaw c >>= fun _ ->
Proofview.Unsafe.tclSETGOALS [Proofview.with_empty_state (Proofview.Goal.goal gl)] >>= fun () ->
let args = EConstr.identity_subst_val (Environ.named_context_val env) in
let args = SList.cons (EConstr.mkRel 1) args in
let ans = EConstr.mkEvar (evk, args) in
return (EConstr.mkLambda (Context.make_annot (Name id) t_rel, t, ans))
| _ ->
throw err_notfocussed
(** preterm -> constr *)
let () =
define "constr_pretype" (repr_ext val_preterm @-> tac constr) @@ fun c ->
let open Pretyping in
let open Ltac_pretype in
let pretype env sigma =
(* For now there are no primitives to create preterms with a non-empty
closure. I do not know whether [closed_glob_constr] is really the type
we want but it does not hurt in the meantime. *)
let { closure; term } = c in
let vars = {
ltac_constrs = closure.typed;
ltac_uconstrs = closure.untyped;
ltac_idents = closure.idents;
ltac_genargs = closure.genargs;
} in
let flags = constr_flags in
let sigma, t = understand_ltac flags env sigma vars WithoutTypeConstraint term in
Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT t
in
pf_apply ~catch_exceptions:true pretype
let () =
define "constr_binder_make" (option ident @-> constr @-> tac valexpr) @@ fun na ty ->
pf_apply @@ fun env sigma ->
match Retyping.relevance_of_type env sigma ty with
| rel ->
let na = match na with None -> Anonymous | Some id -> Name id in
return (Tac2ffi.of_ext val_binder (Context.make_annot na rel, ty))
| exception (Retyping.RetypeError _ as e) ->
let e, info = Exninfo.capture e in
fail ~info (CErrors.UserError Pp.(str "Not a type."))
let () =
define "constr_binder_unsafe_make"
(option ident @-> relevance @-> constr @-> ret valexpr)
@@ fun na rel ty ->
let na = match na with None -> Anonymous | Some id -> Name id in
Tac2ffi.of_ext val_binder (Context.make_annot na rel, ty)
let () =
define "constr_binder_name" (repr_ext val_binder @-> ret (option ident)) @@ fun (bnd, _) ->
match bnd.Context.binder_name with Anonymous -> None | Name id -> Some id
let () =
define "constr_binder_type" (repr_ext val_binder @-> ret constr) @@ fun (_, ty) -> ty
let () =
define "constr_has_evar" (constr @-> tac bool) @@ fun c ->
Proofview.tclEVARMAP >>= fun sigma ->
return (Evarutil.has_undefined_evars sigma c)
(** Extra equalities *)
let () = define "evar_equal" (evar @-> evar @-> ret bool) Evar.equal
let () = define "float_equal" (float @-> float @-> ret bool) Float64.equal
let () = define "uint63_equal" (uint63 @-> uint63 @-> ret bool) Uint63.equal
let () = define "meta_equal" (int @-> int @-> ret bool) Int.equal
let () = define "constr_cast_equal" (cast @-> cast @-> ret bool) Glob_ops.cast_kind_eq
let () =
define "constant_equal"
(constant @-> constant @-> ret bool)
Constant.UserOrd.equal
let () =
let ty = repr_ext val_case in
define "constr_case_equal" (ty @-> ty @-> ret bool) @@ fun x y ->
Ind.UserOrd.equal x.ci_ind y.ci_ind &&
Sorts.relevance_equal x.ci_relevance y.ci_relevance
let () =
let ty = repr_ext val_constructor in
define "constructor_equal" (ty @-> ty @-> ret bool) Construct.UserOrd.equal
let () =
define "projection_equal" (projection @-> projection @-> ret bool) Projection.UserOrd.equal
(** Patterns *)
let () =
define "pattern_empty_context"
(ret (repr_ext val_matching_context))
Constr_matching.empty_context
let () =
define "pattern_matches" (pattern @-> constr @-> tac valexpr) @@ fun pat c ->
pf_apply @@ fun env sigma ->
let ans =
try Some (Constr_matching.matches env sigma pat c)
with Constr_matching.PatternMatchingFailure -> None
in
begin match ans with
| None -> fail err_matchfailure
| Some ans ->
let ans = Id.Map.bindings ans in
let of_pair (id, c) = Tac2ffi.of_tuple [| Tac2ffi.of_ident id; Tac2ffi.of_constr c |] in
return (Tac2ffi.of_list of_pair ans)
end
let () =
define "pattern_matches_subterm" (pattern @-> constr @-> tac valexpr) @@ fun pat c ->
let open Constr_matching in
let rec of_ans s = match IStream.peek s with
| IStream.Nil -> fail err_matchfailure
| IStream.Cons ({ m_sub = (_, sub); m_ctx }, s) ->
let ans = Id.Map.bindings sub in
let of_pair (id, c) =
Tac2ffi.of_tuple [| Tac2ffi.of_ident id; Tac2ffi.of_constr c |]
in
let ans =
Tac2ffi.of_tuple [|
Tac2ffi.of_ext val_matching_context m_ctx;
Tac2ffi.of_list of_pair ans;
|]
in
Proofview.tclOR (return ans) (fun _ -> of_ans s)
in
pf_apply @@ fun env sigma ->
let pat = Constr_matching.instantiate_pattern env sigma Id.Map.empty pat in
let ans = Constr_matching.match_subterm env sigma (Id.Set.empty,pat) c in
of_ans ans
let () =
define "pattern_matches_vect" (pattern @-> constr @-> tac valexpr) @@ fun pat c ->
pf_apply @@ fun env sigma ->
let ans =
try Some (Constr_matching.matches env sigma pat c)
with Constr_matching.PatternMatchingFailure -> None
in
match ans with
| None -> fail err_matchfailure
| Some ans ->
let ans = Id.Map.bindings ans in
let ans = Array.map_of_list snd ans in
return (Tac2ffi.of_array Tac2ffi.of_constr ans)
let () =
define "pattern_matches_subterm_vect" (pattern @-> constr @-> tac valexpr) @@ fun pat c ->
let open Constr_matching in
let rec of_ans s = match IStream.peek s with
| IStream.Nil -> fail err_matchfailure
| IStream.Cons ({ m_sub = (_, sub); m_ctx }, s) ->
let ans = Id.Map.bindings sub in
let ans = Array.map_of_list snd ans in
let ans =
Tac2ffi.of_tuple [|
Tac2ffi.of_ext val_matching_context m_ctx;
Tac2ffi.of_array Tac2ffi.of_constr ans;
|]
in
Proofview.tclOR (return ans) (fun _ -> of_ans s)
in
pf_apply @@ fun env sigma ->
let pat = Constr_matching.instantiate_pattern env sigma Id.Map.empty pat in
let ans = Constr_matching.match_subterm env sigma (Id.Set.empty,pat) c in
of_ans ans
let match_pattern = map_repr
(fun (b,pat) -> if b then Tac2match.MatchPattern pat else Tac2match.MatchContext pat)
(function Tac2match.MatchPattern pat -> (true, pat) | MatchContext pat -> (false, pat))
(pair bool pattern)
let () =
define "pattern_matches_goal"
(bool @-> list (pair (option match_pattern) match_pattern) @-> match_pattern @-> tac valexpr)
@@ fun rev hp cp ->
assert_focussed >>= fun () ->
Proofview.Goal.enter_one @@ fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let concl = Proofview.Goal.concl gl in
Tac2match.match_goal env sigma concl ~rev (hp, cp) >>= fun (hyps, ctx, subst) ->
let empty_context = Constr_matching.empty_context in
let of_ctxopt ctx = Tac2ffi.of_ext val_matching_context (Option.default empty_context ctx) in
let hids = Tac2ffi.of_array Tac2ffi.of_ident (Array.map_of_list pi1 hyps) in
let hbctx = Tac2ffi.of_array of_ctxopt
(Array.of_list (CList.filter_map (fun (_,bctx,_) -> bctx) hyps))
in
let hctx = Tac2ffi.of_array of_ctxopt (Array.map_of_list pi3 hyps) in
let subs = Tac2ffi.of_array Tac2ffi.of_constr (Array.map_of_list snd (Id.Map.bindings subst)) in
let cctx = of_ctxopt ctx in
let ans = Tac2ffi.of_tuple [| hids; hbctx; hctx; subs; cctx |] in
Proofview.tclUNIT ans
let () =
define "pattern_instantiate"
(repr_ext val_matching_context @-> constr @-> ret constr)
Constr_matching.instantiate_context
(** Error *)
let () =
define "throw" (exn @-> tac valexpr) @@ fun (e, info) -> throw ~info e
let () =
define "throw_bt" (exn @-> exninfo @-> tac valexpr) @@ fun (e,_) info ->
Proofview.tclLIFT (Proofview.NonLogical.raise (e, info))
let () =
define "clear_err_info" (err @-> ret err) @@ fun (e,_) -> (e, Exninfo.null)
(** Control *)
(** exn -> 'a *)
let () =
define "zero" (exn @-> tac valexpr) @@ fun (e, info) -> fail ~info e
let () =
define "zero_bt" (exn @-> exninfo @-> tac valexpr) @@ fun (e,_) info ->
Proofview.tclZERO ~info e
(** (unit -> 'a) -> (exn -> 'a) -> 'a *)
let () =
define "plus" (closure @-> closure @-> tac valexpr) @@ fun x k ->
Proofview.tclOR (thaw x) (fun e -> Tac2ffi.apply k [Tac2ffi.of_exn e])
let () =
define "plus_bt" (closure @-> closure @-> tac valexpr) @@ fun run handle ->
Proofview.tclOR (thaw run)
(fun e -> Tac2ffi.apply handle [Tac2ffi.of_exn e; of_exninfo (snd e)])
(** (unit -> 'a) -> 'a *)
let () =
define "once" (closure @-> tac valexpr) @@ fun f ->
Proofview.tclONCE (thaw f)
(** (unit -> unit) list -> unit *)
let () =
define "dispatch" (list closure @-> tac unit) @@ fun l ->
let l = List.map (fun f -> Proofview.tclIGNORE (thaw f)) l in
Proofview.tclDISPATCH l
(** (unit -> unit) list -> (unit -> unit) -> (unit -> unit) list -> unit *)
let () =
define "extend" (list closure @-> closure @-> list closure @-> tac unit) @@ fun lft tac rgt ->
let lft = List.map (fun f -> Proofview.tclIGNORE (thaw f)) lft in
let tac = Proofview.tclIGNORE (thaw tac) in
let rgt = List.map (fun f -> Proofview.tclIGNORE (thaw f)) rgt in
Proofview.tclEXTEND lft tac rgt
(** (unit -> unit) -> unit *)
let () =
define "enter" (closure @-> tac unit) @@ fun f ->
let f = Proofview.tclIGNORE (thaw f) in
Proofview.tclINDEPENDENT f
(** (unit -> 'a) -> ('a * ('exn -> 'a)) result *)
let () =
define "case" (closure @-> tac valexpr) @@ fun f ->
Proofview.tclCASE (thaw f) >>= begin function
| Proofview.Next (x, k) ->
let k = Tac2ffi.mk_closure arity_one begin fun e ->
let (e, info) = Tac2ffi.to_exn e in
set_bt info >>= fun info ->
k (e, info)
end in
return (v_blk 0 [| Tac2ffi.of_tuple [| x; Tac2ffi.of_closure k |] |])
| Proofview.Fail e -> return (v_blk 1 [| Tac2ffi.of_exn e |])
end
(** int -> int -> (unit -> 'a) -> 'a *)
let () =
define "focus" (int @-> int @-> closure @-> tac valexpr) @@ fun i j tac ->