-
Notifications
You must be signed in to change notification settings - Fork 631
/
tac2intern.ml
1933 lines (1818 loc) · 67.8 KB
/
tac2intern.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 Pp
open Util
open CAst
open CErrors
open Names
open Libnames
open Locus
open Tac2env
open Tac2print
open Tac2expr
open Tac2typing_env
(** Hardwired types and constants *)
let coq_type n = KerName.make Tac2env.coq_prefix (Label.make n)
let ltac1_kn n = KerName.make Tac2env.ltac1_prefix (Label.make n)
let t_int = coq_type "int"
let t_string = coq_type "string"
let t_constr = coq_type "constr"
let t_ltac1 = ltac1_kn "t"
let ltac1_lamdba = ltac1_kn "lambda"
let t_preterm = coq_type "preterm"
let t_bool = coq_type "bool"
let ltac2_env : Tac2typing_env.t Genintern.Store.field =
Genintern.Store.field ()
let drop_ltac2_env store =
Genintern.Store.remove store ltac2_env
let error_nargs_mismatch ?loc kn nargs nfound =
let cstr = Tac2env.shortest_qualid_of_constructor kn in
user_err ?loc (str "Constructor " ++ pr_qualid cstr ++ str " expects " ++
int nargs ++ str " arguments, but is applied to " ++ int nfound ++
str " arguments")
let error_nparams_mismatch ?loc nargs nfound =
user_err ?loc (str "Type expects " ++ int nargs ++
str " arguments, but is applied to " ++ int nfound ++
str " arguments")
let rec intern_type env ({loc;v=t} : raw_typexpr) : TVar.t glb_typexpr = match t with
| CTypVar (Name id) -> GTypVar (get_alias (CAst.make ?loc id) env)
| CTypVar Anonymous -> GTypVar (fresh_id env)
| CTypRef (rel, args) ->
let (kn, nparams) = match rel with
| RelId qid ->
begin match (if qualid_is_ident qid then find_rec_var (qualid_basename qid) env else None) with
| Some (kn, n) ->
(Other kn, n)
| None ->
let kn =
try Tac2env.locate_type qid
with Not_found ->
user_err ?loc (str "Unbound type constructor " ++ pr_qualid qid)
in
let (nparams, _) = Tac2env.interp_type kn in
(Other kn, nparams)
end
| AbsKn (Other kn) ->
let (nparams, _) = Tac2env.interp_type kn in
(Other kn, nparams)
| AbsKn (Tuple n) ->
(Tuple n, n)
in
let nargs = List.length args in
let () =
if not (Int.equal nparams nargs) then
let qid = match rel with
| RelId lid -> lid
| AbsKn (Other kn) -> shortest_qualid_of_type ?loc kn
| AbsKn (Tuple _) -> assert false
in
user_err ?loc (strbrk "The type constructor " ++ pr_qualid qid ++
strbrk " expects " ++ int nparams ++ strbrk " argument(s), but is here \
applied to " ++ int nargs ++ strbrk "argument(s)")
in
GTypRef (kn, List.map (fun t -> intern_type env t) args)
| CTypArrow (t1, t2) -> GTypArrow (intern_type env t1, intern_type env t2)
let fresh_type_scheme env (t : type_scheme) : TVar.t glb_typexpr =
let (n, t) = t in
let subst = Array.init n (fun _ -> fresh_id env) in
let substf i = GTypVar subst.(i) in
subst_type substf t
let fresh_mix_type_scheme env (t : mix_type_scheme) : TVar.t glb_typexpr =
let (n, t) = t in
let subst = Array.init n (fun _ -> fresh_id env) in
let substf = function
| LVar i -> GTypVar subst.(i)
| GVar n -> GTypVar n
in
subst_type substf t
(** Term typing *)
let is_pure_constructor kn =
match snd (Tac2env.interp_type kn) with
| GTydAlg _ | GTydOpn -> true
| GTydRec fields ->
let is_pure (_, mut, _) = not mut in
List.for_all is_pure fields
| GTydDef _ -> assert false (** Type definitions have no constructors *)
let rec is_value = function
| GTacAtm (AtmInt _) | GTacVar _ | GTacRef _ | GTacFun _ -> true
| GTacAtm (AtmStr _) | GTacApp _ | GTacLet (true, _, _) -> false
| GTacCst (Tuple _, _, el) -> List.for_all is_value el
| GTacCst (_, _, []) -> true
| GTacOpn (_, el) -> List.for_all is_value el
| GTacCst (Other kn, _, el) -> is_pure_constructor kn && List.for_all is_value el
| GTacLet (false, bnd, e) ->
is_value e && List.for_all (fun (_, e) -> is_value e) bnd
| GTacCse _ | GTacPrj _ | GTacSet _ | GTacExt _ | GTacPrm _
| GTacWth _ | GTacFullMatch _ -> false
let is_rec_rhs = function
| GTacFun _ -> true
| GTacAtm _ | GTacVar _ | GTacRef _ | GTacApp _ | GTacLet _ | GTacPrj _
| GTacSet _ | GTacExt _ | GTacPrm _ | GTacCst _
| GTacCse _ | GTacOpn _ | GTacWth _ | GTacFullMatch _-> false
let warn_not_unit =
CWarnings.create ~name:"not-unit" ~category:"ltac2"
(fun (env, t) ->
strbrk "This expression should have type unit but has type " ++
pr_glbtype env t ++ str ".")
let check_elt_unit loc env t =
let maybe_unit = match kind env t with
| GTypVar _ -> true
| GTypArrow _ -> false
| GTypRef (Tuple 0, []) -> true
| GTypRef _ -> false
in
if not maybe_unit then warn_not_unit ?loc (env, t)
let is_empty_type env t = match kind env t with
| GTypVar _ | GTypArrow _ | GTypRef (Tuple _, _) -> false
| GTypRef (Other kn, _) ->
let def = Tac2env.interp_type kn in
match def with
| _, GTydAlg { galg_constructors = [] } -> true
| _ -> false
let check_elt_empty loc env t = match kind env t with
| GTypVar _ ->
user_err ?loc (str "Cannot infer an empty type for this expression")
| GTypArrow _ | GTypRef (Tuple _, _) ->
user_err ?loc (str "Type" ++ spc () ++ pr_glbtype env t ++ spc () ++ str "is not an empty type")
| GTypRef (Other kn, _) ->
let def = Tac2env.interp_type kn in
match def with
| _, GTydAlg { galg_constructors = [] } -> kn
| _ ->
user_err ?loc (str "Type" ++ spc () ++ pr_glbtype env t ++ spc () ++ str "is not an empty type")
let check_unit ?loc t =
let env = empty_env () in
(* Should not matter, t should be closed. *)
let t = fresh_type_scheme env t in
let maybe_unit = match kind env t with
| GTypVar _ -> true
| GTypArrow _ -> false
| GTypRef (Tuple 0, []) -> true
| GTypRef _ -> false
in
if not maybe_unit then warn_not_unit ?loc (env, t)
let get_constructor env var = match var with
| RelId qid ->
let c = try Some (Tac2env.locate_constructor qid) with Not_found -> None in
begin match c with
| Some knc -> Other knc
| None ->
CErrors.user_err ?loc:qid.CAst.loc (str "Unbound constructor " ++ pr_qualid qid)
end
| AbsKn knc -> knc
let get_projection var = match var with
| RelId qid ->
let kn = try Tac2env.locate_projection qid with Not_found ->
user_err ?loc:qid.CAst.loc (pr_qualid qid ++ str " is not a projection")
in
Tac2env.interp_projection kn
| AbsKn kn ->
Tac2env.interp_projection kn
let intern_atm env = function
| AtmInt n -> (GTacAtm (AtmInt n), GTypRef (Other t_int, []))
| AtmStr s -> (GTacAtm (AtmStr s), GTypRef (Other t_string, []))
(** Internalization *)
(** Used to generate a fresh tactic variable for pattern-expansion *)
let fresh_var avoid =
let bad id =
Id.Set.mem id avoid ||
(try ignore (locate_ltac (qualid_of_ident id)); true with Not_found -> false)
in
Namegen.next_ident_away_from (Id.of_string "p") bad
let add_name accu = function
| Name id -> Id.Set.add id accu
| Anonymous -> accu
let rec ids_of_pattern accu {v=pat} = match pat with
| CPatVar Anonymous | CPatAtm _ -> accu
| CPatVar (Name id) -> Id.Set.add id accu
| CPatAs (p,id) -> ids_of_pattern (Id.Set.add id.v accu) p
| CPatRef (_, pl) | CPatOr pl ->
List.fold_left ids_of_pattern accu pl
| CPatCnv (pat, _) -> ids_of_pattern accu pat
| CPatRecord pats -> List.fold_left (fun accu (_,pat) -> ids_of_pattern accu pat) accu pats
let loc_of_relid = function
| RelId {loc} -> loc
| AbsKn _ -> None
let is_unit_pattern = function
| CPatRef (AbsKn (Tuple 0), []) -> true
| _ -> false
let extract_pattern_type ({loc;v=p} as pat) = match p with
| CPatCnv (pat, ty) -> pat, Some ty
| CPatAtm _ | CPatVar _ | CPatRef _ | CPatOr _ | CPatAs _ | CPatRecord _ ->
if is_unit_pattern p then
(* Special handling of () patterns *)
let t_unit = CAst.make ?loc @@ CTypRef (AbsKn (Tuple 0), []) in
pat, Some t_unit
else pat, None
(** Expand pattern: [p => t] becomes [x => match x with p => t end] *)
let expand_pattern avoid bnd =
let fold (avoid, bnd) (pat, t) =
let na, expand = match pat.v with
| CPatVar na ->
(* Don't expand variable patterns *)
na, None
| _ ->
if is_unit_pattern pat.v then
Anonymous, None
else
let id = fresh_var avoid in
let qid = RelId (qualid_of_ident ?loc:pat.loc id) in
Name id, Some qid
in
let avoid = ids_of_pattern avoid pat in
let avoid = add_name avoid na in
(avoid, (na, pat, expand) :: bnd)
in
let (_, bnd) = List.fold_left fold (avoid, []) bnd in
let fold e (na, pat, expand) = match expand with
| None -> e
| Some qid ->
let loc = loc_of_relid qid in
CAst.make ?loc @@ CTacCse (CAst.make ?loc @@ CTacRef qid, [pat, e])
in
let expand e = List.fold_left fold e bnd in
let nas = List.rev_map (fun (na, _, _) -> na) bnd in
(nas, expand)
let is_alias env qid = match get_variable env qid with
| ArgArg (TacAlias _) -> true
| ArgVar _ | (ArgArg (TacConstant _)) -> false
let is_user_name qid = match qid with
| AbsKn _ -> false
| RelId _ -> true
let deprecated_ltac2_alias =
Deprecation.create_warning
~object_name:"Ltac2 alias"
~warning_name_if_no_since:"deprecated-ltac2-alias"
(fun kn -> pr_qualid (Tac2env.shortest_qualid_of_ltac (TacAlias kn)))
let deprecated_ltac2_def =
Deprecation.create_warning
~object_name:"Ltac2 definition"
~warning_name_if_no_since:"deprecated-ltac2-definition"
(fun kn -> pr_qualid (Tac2env.shortest_qualid_of_ltac (TacConstant kn)))
let check_deprecated_ltac2 ?loc qid def =
if is_user_name qid then match def with
| TacAlias kn ->
begin match (Tac2env.interp_alias kn).alias_depr with
| None -> ()
| Some depr -> deprecated_ltac2_alias ?loc (kn, depr)
end
| TacConstant kn ->
begin match (Tac2env.interp_global kn).gdata_deprecation with
| None -> ()
| Some depr -> deprecated_ltac2_def ?loc (kn, depr)
end
type ('a,'b) field =
| PresentField of 'a
| MissingField of 'b
let intern_record env loc fs =
let map (proj, e) =
let loc = match proj with
| RelId {CAst.loc} -> loc
| AbsKn _ -> None
in
let proj = get_projection proj in
(loc, proj, e)
in
let fs = List.map map fs in
let kn = match fs with
| [] -> user_err ?loc (str "Cannot infer the corresponding record type")
| (_, proj, _) :: _ -> proj.pdata_type
in
let params, typdef = match Tac2env.interp_type kn with
| n, GTydRec def -> n, def
| _ -> assert false
in
let subst = Array.init params (fun _ -> fresh_id env) in
(* Set the answer [args] imperatively *)
let args = Array.make (List.length typdef) None in
let iter (loc, pinfo, e) =
if KerName.equal kn pinfo.pdata_type then
let index = pinfo.pdata_indx in
match args.(index) with
| None ->
let exp = subst_type (fun i -> GTypVar subst.(i)) pinfo.pdata_ptyp in
args.(index) <- Some (e, exp)
| Some _ ->
let (name, _, _) = List.nth typdef pinfo.pdata_indx in
user_err ?loc (str "Field " ++ Id.print name ++ str " is defined \
several times")
else
user_err ?loc (str "Field " ++ (*KerName.print knp ++*) str " does not \
pertain to record definition " ++ pr_typref pinfo.pdata_type)
in
let () = List.iter iter fs in
let args = Array.mapi (fun i arg -> match arg with
| None ->
let field, _, typ = List.nth typdef i in
let typ' = subst_type (fun i -> GTypVar subst.(i)) typ in
MissingField (i, field, typ, typ')
| Some arg -> PresentField arg)
args
in
let tparam = List.init params (fun i -> GTypVar subst.(i)) in
kn, tparam, args
let ctor_data_for_patterns kn data = {
ctyp = Some data.cdata_type;
cnargs = List.length data.cdata_args;
cindx = match data.cdata_indx with None -> Open kn | Some i -> Closed i;
}
let ctor_data_of_tuple n = {
ctyp = None;
cnargs = n;
cindx = Closed 0;
}
type wip_pat_r =
| PatVar of Name.t
| PatAtm of atom
| PatRef of ctor_data_for_patterns * wip_pat list
| PatOr of wip_pat list
| PatAs of wip_pat * lident
and wip_pat = wip_pat_r CAst.t
let catchall = CAst.make (PatVar Anonymous)
let pat_or ?loc = function
| [] -> assert false
| [x] -> x
| pats -> CAst.make ?loc (PatOr pats)
let rec intern_pat_rec env cpat t =
let loc = cpat.loc in
match cpat.v with
| CPatVar x -> begin match x with
| Anonymous -> Id.Map.empty, CAst.make ?loc (PatVar x)
| Name id ->
let patvars = Id.Map.singleton id (loc,t) in
patvars, CAst.make ?loc (PatVar x)
end
| CPatAtm atm ->
let _, t' = intern_atm env atm in
let () = unify ?loc env t t' in
Id.Map.empty, CAst.make ?loc (PatAtm atm)
| CPatAs (p, x) ->
let patvars, p = intern_pat_rec env p t in
let patvars = Id.Map.update x.v (function
| Some _ ->
CErrors.user_err ?loc
Pp.(str "Variable " ++ Id.print x.v ++
str " is bound several times in this matching.")
| None -> Some (x.loc,t))
patvars
in
patvars, CAst.make ?loc (PatAs (p, x))
| CPatRef (ctor,args) ->
let ctor = get_constructor env ctor in
let ctor, argts =
let nargs = List.length args in
match ctor with
| Tuple n ->
assert (Int.equal nargs n);
let ts = List.init n (fun _ -> GTypVar (fresh_id env)) in
let () = unify ?loc env t (GTypRef (ctor, ts)) in
ctor_data_of_tuple n, ts
| Other kn ->
let data = interp_constructor kn in
let nexpectargs = List.length data.cdata_args in
if not (Int.equal nargs nexpectargs) then error_nargs_mismatch ?loc kn nexpectargs nargs;
let subst = Array.init data.cdata_prms (fun _ -> fresh_id env) in
let substf i = GTypVar subst.(i) in
let types = List.map (fun t -> subst_type substf t) data.cdata_args in
let targs = List.init data.cdata_prms substf in
let ans = GTypRef (Other data.cdata_type, targs) in
let () = unify ?loc env t ans in
ctor_data_for_patterns kn data, types
in
let patvars, args = CList.fold_left2_map (fun patvars arg argt ->
let argvars, arg = intern_pat_rec env arg argt in
let patvars = Id.Map.union (fun id _ (loc,_) ->
CErrors.user_err ?loc
Pp.(str "Variable " ++ Id.print id ++
str " is bound several times in this matching."))
patvars argvars
in
patvars, arg)
Id.Map.empty
args
argts
in
patvars, CAst.make ?loc (PatRef (ctor,args))
| CPatRecord pats ->
let kn, tparam, args = intern_record env loc pats in
let () = unify ?loc env t (GTypRef (Other kn, tparam)) in
let args = Array.to_list args in
let patvars, args = CList.fold_left_map (fun patvars -> function
| MissingField _ -> patvars, catchall
| PresentField (arg, argty) ->
let (argvars,arg) = intern_pat_rec env arg argty in
let patvars = Id.Map.union (fun id _ (loc,_) ->
CErrors.user_err ?loc
Pp.(str "Variable " ++ Id.print id ++
str " is bound several times in this matching."))
patvars argvars
in
patvars, arg)
Id.Map.empty
args
in
let ctor = { ctyp = Some kn; cnargs = List.length args; cindx = Closed 0 } in
patvars, CAst.make ?loc (PatRef (ctor, args))
| CPatCnv (pat,typ) ->
let typ = intern_type env typ in
let () = unify ?loc env t typ in
intern_pat_rec env pat typ
| CPatOr [] -> assert false
| CPatOr (first::rest) ->
let patvars, first = intern_pat_rec env first t in
let rest = List.map (fun pat ->
let patvars', pat = intern_pat_rec env pat t in
if not (Id.Map.equal (fun (_,t) (loc,t') ->
unify ?loc env t t';
true)
patvars patvars')
(* TODO say what variables are differently bound *)
then CErrors.user_err ?loc Pp.(str "These patterns do not bind the same variables.");
pat)
rest
in
patvars, CAst.make ?loc (PatOr (first::rest))
let intern_pat env cpat t =
let patvars, pat = intern_pat_rec env cpat t in
Id.Map.map (fun (_,v) -> monomorphic v) patvars, pat
let rec glb_of_wip_pat_r = function
| PatVar x -> GPatVar x
| PatAtm atm -> GPatAtm atm
| PatRef (ctor,pats) -> GPatRef (ctor, List.map glb_of_wip_pat pats)
| PatOr pats -> GPatOr (List.map glb_of_wip_pat pats)
| PatAs (p,x) -> GPatAs (glb_of_wip_pat p, x.v)
and glb_of_wip_pat pat = glb_of_wip_pat_r pat.CAst.v
(** Pattern analysis for non-exhaustiveness and (TODO) useless patterns based on
"Warnings for pattern matching", Luc Maranget, Journal of Functional Programming, 17(3), 2007 *)
let default_matrix =
let rec default_row = function
| [] -> assert false
| {v=PatRef _ | PatAtm _} :: _ -> []
| {v=PatVar _} :: rest -> [rest]
| {v=PatOr pats} :: rest -> List.map_append default_row (List.map (fun x -> x::rest) pats)
| {v=PatAs (p,_)} :: rest -> default_row (p::rest)
in
List.map_append default_row
type generalized_ctor =
| AtomCtor of atom
| OtherCtor of ctor_data_for_patterns
let rec root_ctors = function
| {v=PatVar _} -> []
| {v=PatRef (ctor,_)} -> [OtherCtor ctor]
| {v=PatAtm a} -> [AtomCtor a]
| {v=PatOr pats} -> List.map_append root_ctors pats
| {v=PatAs (p,_)} -> root_ctors p
(* XXX maybe should be ctor_data_for_patterns list or_tuple ??? *)
type missing_ctors =
| Unknown
| Extension of { example : atom option }
| Known of ctor_data_for_patterns list
type maybe_missing_ctors =
| Missing of missing_ctors
| NoMissing of ctor_data_for_patterns list
let make_ctor ctyp tdata is_const n =
let cnargs = if is_const then 0 else
let rec find n = function
| [] -> assert false
| (_, []) :: rem ->
find n rem
| (_, argtys) :: rem ->
if Int.equal n 0 then List.length argtys
else find (pred n) rem
in
find n tdata.galg_constructors
in
{
ctyp;
cindx = Closed n;
cnargs;
}
let make_int_example ints =
let rec aux i = if Int.Set.mem i ints then aux (i+1) else i
in aux 0
let make_string_example strings =
let rec aux s = if String.Set.mem s strings then aux (s^"*") else s
in aux ""
let make_atom_example = function
| AtomCtor (AtmInt i) :: rest ->
let ints = List.fold_left (fun ints c -> match c with
| AtomCtor (AtmInt i) -> Int.Set.add i ints
| _ -> assert false)
(Int.Set.singleton i)
rest
in
AtmInt (make_int_example ints)
| AtomCtor (AtmStr s) :: rest ->
let strings = List.fold_left (fun strings c -> match c with
| AtomCtor (AtmStr s) -> String.Set.add s strings
| _ -> assert false)
(String.Set.singleton s)
rest
in
AtmStr (make_string_example strings)
| OtherCtor _ :: _ | [] -> assert false
(* We assume all the constructors in the list are from the same type t *)
let missing_ctors_from env t = function
| [] -> (* patterns are all wildcards *)
(* TODO handle match on deep empty eg (empty,empty) *)
if is_empty_type env t then NoMissing []
else Missing Unknown
| AtomCtor _ :: _ as l -> Missing (Extension {example=Some (make_atom_example l)})
| OtherCtor {ctyp=None; cnargs} :: _ ->
(* tuple has 1 constructor *) NoMissing [ctor_data_of_tuple cnargs]
| OtherCtor {cindx=Open _} :: _ -> Missing (Extension {example=None})
| OtherCtor ({ctyp=Some ctyp} as data) :: _ as ctors ->
let _, tdata = interp_type ctyp in
match tdata with
| GTydOpn | GTydDef _ -> assert false
| GTydRec _ -> NoMissing [data]
| GTydAlg tdata ->
let const = Array.make tdata.galg_nconst false in
let nonconst = Array.make tdata.galg_nnonconst false in
let () = List.iter (function
| OtherCtor {cindx=Closed i; cnargs} ->
let which = if Int.equal 0 cnargs then const else nonconst in
which.(i) <- true
| AtomCtor _ | OtherCtor {cindx=Open _} -> assert false)
ctors
in
let fold is_const i (missing, present) ispresent =
let ctor = (make_ctor data.ctyp tdata is_const i) in
if ispresent then missing, ctor :: present
else ctor :: missing, present
in
let acc = CArray.fold_left_i (fold false) ([],[]) nonconst in
let missing, present = CArray.fold_left_i (fold true) acc const in
if List.is_empty missing then NoMissing present
else Missing (Known missing)
let specialized_types env ts ctor = match ts with
| [] -> assert false
| t :: rest ->
let argts = match ctor with
| AtomCtor _ -> []
| OtherCtor {ctyp=None; cnargs=n} ->
let argts = List.init n (fun _ -> GTypVar (fresh_id env)) in
let () = unify env t (GTypRef (Tuple n, argts)) in
argts
| OtherCtor {cindx=Open kn} ->
let data = interp_constructor kn in
let subst = Array.init data.cdata_prms (fun _ -> fresh_id env) in
let substf i = GTypVar subst.(i) in
let types = List.map (fun t -> subst_type substf t) data.cdata_args in
let targs = List.init data.cdata_prms substf in
let ans = GTypRef (Other data.cdata_type, targs) in
let () = unify env t ans in
types
| OtherCtor {ctyp=Some ctyp; cnargs; cindx=Closed i} ->
let ntargs, tdata = interp_type ctyp in
match tdata with
| GTydOpn | GTydDef _ -> assert false
| GTydRec tdata ->
let subst = Array.init ntargs (fun _ -> fresh_id env) in
let substf i = GTypVar subst.(i) in
let types = List.map (fun (_,_,t) -> subst_type substf t) tdata in
let targs = List.init ntargs substf in
let ans = GTypRef (Other ctyp, targs) in
let () = unify env t ans in
types
| GTydAlg tdata ->
let ctors = List.filter (fun (_,argts) ->
if cnargs = 0
then List.is_empty argts
else not (List.is_empty argts))
tdata.galg_constructors
in
let _, argts = List.nth ctors i in
let subst = Array.init ntargs (fun _ -> fresh_id env) in
let substf i = GTypVar subst.(i) in
let types = List.map (fun t -> subst_type substf t) argts in
let targs = List.init ntargs substf in
let ans = GTypRef (Other ctyp, targs) in
let () = unify env t ans in
types
in
List.append argts rest
let specialized_multi_matrix (patsP, patsQ, patsR) ctor =
let same_atom atm atm' = match atm, atm' with
| AtmInt i, AtmInt j -> Int.equal i j
| AtmStr i, AtmStr j -> String.equal i j
| AtmInt _, AtmStr _ | AtmStr _, AtmInt _ -> assert false (* by typing *)
in
let same_ctor_indx i j = match i, j with
| Closed i, Closed j -> Int.equal i j
| Open kn, Open kn' -> KerName.equal kn kn'
| Closed _, Open _ | Open _, Closed _ -> false
in
let same_ctor ctor ctor' = match ctor, ctor' with
| AtomCtor atm, AtomCtor atm' -> same_atom atm atm'
| OtherCtor ctor, OtherCtor ctor' ->
Int.equal ctor.cnargs ctor'.cnargs
&& same_ctor_indx ctor.cindx ctor'.cindx
| AtomCtor _, OtherCtor _ | OtherCtor _, AtomCtor _ -> assert false (* by typing *)
in
let rec special_row rowP rowQ rowR = match rowP with
| [] -> assert false
| {v=PatRef (ctor',args)} :: rest ->
if same_ctor ctor (OtherCtor ctor') then [List.append args rest, rowQ, rowR]
else []
| {v=PatAtm atm} :: rest ->
if same_ctor ctor (AtomCtor atm) then [rest, rowQ, rowR]
else []
| {v=PatVar _} :: rest -> begin match ctor with
| OtherCtor ctor -> [List.append (List.make ctor.cnargs catchall) rest, rowQ, rowR]
| AtomCtor _ -> [rest, rowQ, rowR]
end
| {v=PatOr pats} :: rest ->
List.map_append (fun x -> special_row (x::rest) rowQ rowR) pats
| {v=PatAs (p,_)} :: rest -> special_row (p::rest) rowQ rowR
in
let res = List.flatten (List.map3 special_row patsP patsQ patsR) in
List.split3 res
let specialized_matrix pats ctor =
(* because the dummy lists are [unit list] we are guaranteed that
they don't get mixed with [pats], they just get some elements
dropped or copied *)
let dummy = List.make (List.length pats) () in
let pats, _, _ = specialized_multi_matrix (pats, dummy, dummy) ctor in
pats
let rec lift_interned_pat pat = CAst.map lift_interned_pat_r pat
and lift_interned_pat_r = let open PartialPat in function
| PatVar x -> Var x
| PatAtm a -> Atom a
| PatRef (ctor, pats) -> Ref (ctor, List.map lift_interned_pat pats)
| PatOr pats -> Or (List.map lift_interned_pat pats)
| PatAs (p,x) -> As (lift_interned_pat p, x.v)
(*
[ (*row,col*)
[(0,0); (0,1)];
[(1,0); (1,1)];
]
*)
(* invariant: ts is n types, pats is a matrix with n columns ([nth pats i] is row i) *)
let rec missing_matches env ts pats n =
match n with
| 0 -> begin match pats with [] -> Some [] | _::_ -> None end
| _ ->
let root_ctors = List.map_append root_ctors (List.map List.hd pats) in
match missing_ctors_from env (List.hd ts) root_ctors with
| NoMissing ctors -> specialized_missing_matches env ts pats n ctors
| Missing missing_ctors ->
match missing_matches env (List.tl ts) (default_matrix pats) (n-1) with
| None -> None
| Some missing -> match missing_ctors with
| Unknown -> Some (lift_interned_pat catchall :: missing)
| Extension {example} -> Some (CAst.make (PartialPat.Extension {example}) :: missing)
| Known missing_ctors ->
let misspats = List.map (fun ctor ->
CAst.make (PatRef (ctor, List.make ctor.cnargs catchall)))
missing_ctors
in
Some (lift_interned_pat (pat_or misspats) :: missing)
and specialized_missing_matches env ts pats n = function
| [] -> None
| ctor :: rest ->
match missing_matches env
(specialized_types env ts (OtherCtor ctor))
(specialized_matrix pats (OtherCtor ctor))
(ctor.cnargs + n - 1)
with
| None -> specialized_missing_matches env ts pats n rest
| Some missing ->
let args, missing = List.chop ctor.cnargs missing in
(* TODO continue recursing for more exhaustive output? *)
Some (CAst.make (PartialPat.Ref (ctor, args)) :: missing)
let check_no_missing_pattern env t pats =
match missing_matches env [t] (List.map (fun x -> [x]) pats) 1 with
| None -> ()
| Some missing ->
let missing = match missing with [x] -> x | _ -> assert false in
CErrors.user_err Pp.(
str "Non exhaustive match. Values in this pattern are not matched:" ++ fnl() ++
pr_partial_pat missing)
type utility =
| Useless
| PartiallyUseless of Loc.t option list
let combine_utilities us =
let fold (all_useless, useless_locs) = function
| _, None -> (false, useless_locs)
| loc, Some Useless -> (all_useless, [loc]::useless_locs)
| _, Some (PartiallyUseless locs) -> (false, locs::useless_locs)
in
let all_useless, useless_locs = List.fold_left fold (true,[]) us in
if List.is_empty useless_locs then None
else if all_useless then Some Useless
else Some (PartiallyUseless (List.flatten (List.rev useless_locs)))
let rec simple_utility env ts pats q =
match q with
| [] -> begin match pats with [] -> true | _::_ -> false end
| pat :: q -> match pat.CAst.v with
| PatAs (p, _) -> simple_utility env ts pats (p :: q)
| PatRef (ctor, args) ->
let ctor = OtherCtor ctor in
simple_utility env (specialized_types env ts ctor)
(specialized_matrix pats ctor)
(args @ q)
| PatAtm atm ->
let ctor = AtomCtor atm in
simple_utility env (specialized_types env ts ctor)
(specialized_matrix pats ctor)
q
| PatOr ps -> List.exists (fun p -> simple_utility env ts pats (p :: q)) ps
| PatVar _ ->
let root_ctors = List.map_append root_ctors (List.map List.hd pats) in
match missing_ctors_from env (List.hd ts) root_ctors with
| NoMissing ctors ->
List.exists (fun ctor ->
let gctor = OtherCtor ctor in
simple_utility env (specialized_types env ts gctor)
(specialized_matrix pats gctor)
(List.make ctor.cnargs catchall @ q))
ctors
| Missing _ -> simple_utility env (List.tl ts) (default_matrix pats) q
(* each component of a tuple has as many cols as the corresponding component of the other tuples
each component of [prefix] has as many rows as the other components of [prefix]
*)
let rec utility env ((tP, tQ, tR) as t) ((preP, preQ, preR) as prefix) (p, q, r) =
match p with
| p1 :: p -> begin match p1.CAst.v with
| PatAs (p1, _) -> utility env t prefix (p1 :: p, q, r)
| PatRef (ctor, pats) ->
let ctor = OtherCtor ctor in
let t = specialized_types env tP ctor, tQ, tR in
let prefix = specialized_multi_matrix prefix ctor in
utility env t prefix (pats @ p, q, r)
| PatAtm atm ->
let ctor = AtomCtor atm in
let t = specialized_types env tP ctor, tQ, tR in
let prefix = specialized_multi_matrix prefix ctor in
utility env t prefix (p, q, r)
| PatVar _ ->
let t = (List.tl tP, List.hd tP :: tQ, tR) in
let prefix =
(List.map List.tl preP,
List.map2 (fun preP preQ -> List.hd preP :: preQ) preP preQ,
preR)
in
utility env t prefix (p, p1 :: q, r)
| PatOr _ ->
let t = (List.tl tP, tQ, List.hd tP :: tR) in
let prefix =
(List.map List.tl preP,
preQ,
List.map2 (fun preP preR -> List.hd preP :: preR) preP preR)
in
utility env t prefix (p, q, p1 :: r)
end
| [] -> match r with
| [] -> if simple_utility env tQ preQ q then None else Some Useless
| _ :: _ ->
let utilities = List.map_i (fun j rj ->
let t = ([List.nth tR j], (List.filteri (fun j' _ -> not (Int.equal j j')) tR) @ tQ, []) in
let r_no_j = List.filteri (fun j' _ -> not (Int.equal j j')) r in
let preRj = List.map (fun x -> [List.nth x j]) preR in
let preR_no_j = List.map (fun x -> List.filteri (fun j' _ -> not (Int.equal j j')) x) preR in
let r_no_j_plus_q = r_no_j @ q in
let pats = match rj.v with
| PatOr pats -> pats
| _ -> assert false
in
let fold ((preP, preQ, preR) as prefix) pat =
let u = utility env t prefix ([pat], r_no_j_plus_q, []) in
(* [[] :: preR] because the order doesn't matter, they're all empty *)
let prefix = (preP @ [[pat]], preQ @ [r_no_j_plus_q], [] :: preR) in
prefix, (pat.loc, u)
in
let prefix = (preRj, List.map2 (@) preR_no_j preQ, List.make (List.length preRj) []) in
let _, us = List.fold_left_map fold prefix pats in
rj.loc, combine_utilities us)
0 r
in
combine_utilities utilities
let warn_redundant_pattern =
CWarnings.create ~name:"redundant-pattern" ~category:"ltac2"
(fun partial -> str ("This " ^ (if partial then "pattern" else "clause") ^ " is redundant."))
let check_redundant_clauses env t pats =
let fold (prefix, dummies) pat =
let () = match utility env ([t],[],[]) (prefix,dummies,dummies) ([pat],[],[]) with
| None -> ()
| Some Useless -> warn_redundant_pattern ?loc:pat.loc false
| Some (PartiallyUseless locs) -> List.iter (fun loc -> warn_redundant_pattern ?loc true) locs
in
prefix @ [[pat]], [] :: dummies
in
let _, _ = List.fold_left fold ([],[]) pats in
()
(** Pattern view *)
type glb_patexpr =
| GEPatVar of Name.t
| GEPatRef of ctor_data_for_patterns * glb_patexpr list
exception HardCase
let rec to_patexpr env {loc;v=pat} = match pat with
| PatVar na -> GEPatVar na
| PatRef (ctor, pl) ->
GEPatRef (ctor, List.map (fun p -> to_patexpr env p) pl)
| PatAtm _ | PatOr _ | PatAs _ ->
raise HardCase
type pattern_kind =
| PKind_empty
| PKind_variant of type_constant or_tuple
| PKind_open
| PKind_any
let get_pattern_kind env pl = match pl with
| [] -> PKind_empty
| p :: pl ->
let rec get_kind ((p:wip_pat), _) pl = match to_patexpr env p with
| GEPatVar _ ->
begin match pl with
| [] -> PKind_any
| p :: pl -> get_kind p pl
end
| GEPatRef ({ctyp=Some ctyp} as kn, pl) -> begin match kn.cindx with
| Open kn -> PKind_open
| Closed _ -> PKind_variant (Other ctyp)
end
(* let data = Tac2env.interp_constructor kn in *)
(* if Option.is_empty data.cdata_indx then PKind_open data.cdata_type *)
(* else PKind_variant (Other data.cdata_type) *)
| GEPatRef ({ctyp=None; cnargs=k}, tp) -> PKind_variant (Tuple k)
in
get_kind p pl
(** For now, patterns recognized by the pattern-matching compiling are limited
to depth-one where leaves are either variables or catch-all *)
let to_simple_case env ?loc (e,t) pl =
let todo () = raise HardCase in
match get_pattern_kind env pl with
| PKind_any ->
let (pat, b) = List.hd pl in
let na = match to_patexpr env pat with
| GEPatVar na -> na
| _ -> assert false
in
GTacLet (false, [na, e], b)
| PKind_empty ->
let kn = check_elt_empty loc env t in
GTacCse (e, Other kn, [||], [||])
| PKind_variant kn ->
let (nconst, nnonconst, arities) = match kn with
| Tuple 0 -> 1, 0, [0]
| Tuple n -> 0, 1, [n]
| Other kn ->
let (_, def) = Tac2env.interp_type kn in
let galg = match def with
| GTydAlg c -> c
| GTydRec _ -> raise HardCase
| _ -> assert false
in
let arities = List.map (fun (_, args) -> List.length args) galg.galg_constructors in
galg.galg_nconst, galg.galg_nnonconst, arities
in
let const = Array.make nconst None in
let nonconst = Array.make nnonconst None in
let rec intern_branch = function
| [] -> ()
| (pat, br) :: rem ->
let () = match pat.v with
| PatAtm _ | PatOr _ | PatAs _ ->
raise HardCase
| PatVar (Name _) -> todo ()
| PatVar Anonymous ->
(* Fill all remaining branches *)
let fill (ncst, narg) arity =
if Int.equal arity 0 then
let () =
if Option.is_empty const.(ncst) then const.(ncst) <- Some br
in
(succ ncst, narg)
else
let () =
if Option.is_empty nonconst.(narg) then
let ids = Array.make arity Anonymous in
nonconst.(narg) <- Some (ids, br)
in
(ncst, succ narg)
in
let _, _ = List.fold_left fill (0, 0) arities in
()
| PatRef (ctor, args) ->
let index = match ctor.cindx with
| Closed i -> i
| Open _ -> assert false (* Open in PKind_variant is forbidden by typing *)
in
let get_id pat = match pat.v with
| PatVar na -> na
| _ -> todo ()
in
let ids = List.map get_id args in
let () =
if List.is_empty args then
if Option.is_empty const.(index) then const.(index) <- Some br
else ()
else
let ids = Array.of_list ids in
if Option.is_empty nonconst.(index) then nonconst.(index) <- Some (ids, br)
else ()
in
()
in
intern_branch rem