-
Notifications
You must be signed in to change notification settings - Fork 85
/
Copy pathincludecore.ml
1511 lines (1403 loc) · 56.7 KB
/
includecore.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
(**************************************************************************)
(* *)
(* OCaml *)
(* *)
(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
(* *)
(* Copyright 1996 Institut National de Recherche en Informatique et *)
(* en Automatique. *)
(* *)
(* All rights reserved. This file is distributed under the terms of *)
(* the GNU Lesser General Public License version 2.1, with the *)
(* special exception on linking described in the file LICENSE. *)
(* *)
(**************************************************************************)
(* Inclusion checks for the core language *)
open Asttypes
open Path
open Types
open Mode
open Typedtree
type position = Errortrace.position = First | Second
(* Inclusion between value descriptions *)
type primitive_mismatch =
| Name
| Arity
| No_alloc of position
| Builtin
| Effects
| Coeffects
| Native_name
| Result_repr
| Argument_repr of int
| Layout_poly_attr
type value_mismatch =
| Primitive_mismatch of primitive_mismatch
| Not_a_primitive
| Type of Errortrace.moregen_error
| Zero_alloc of Zero_alloc.error
| Modality of Mode.Modality.Value.error
| Mode of Mode.Value.error
exception Dont_match of value_mismatch
type mmodes =
| All
| Legacy of Env.held_locks option
let native_repr_args nra1 nra2 =
let rec loop i nra1 nra2 =
match nra1, nra2 with
| [], [] -> None
| [], _ :: _ -> assert false
| _ :: _, [] -> assert false
| (_, nr1) :: nra1, (_, nr2) :: nra2 ->
if not (Primitive.equal_native_repr nr1 nr2) then Some (Argument_repr i)
else loop (i+1) nra1 nra2
in
loop 1 nra1 nra2
let primitive_descriptions pd1 pd2 =
let open Primitive in
if not (String.equal pd1.prim_name pd2.prim_name) then
Some Name
else if not (Int.equal pd1.prim_arity pd2.prim_arity) then
Some Arity
else if (not pd1.prim_alloc) && pd2.prim_alloc then
Some (No_alloc First)
else if pd1.prim_alloc && (not pd2.prim_alloc) then
Some (No_alloc Second)
else if not
(Bool.equal pd1.prim_is_layout_poly
pd2.prim_is_layout_poly) then
Some Layout_poly_attr
else if not (Bool.equal pd1.prim_c_builtin pd2.prim_c_builtin) then
Some Builtin
else if not (Primitive.equal_effects pd1.prim_effects pd2.prim_effects) then
Some Effects
else if not
(Primitive.equal_coeffects
pd1.prim_coeffects pd2.prim_coeffects) then
Some Coeffects
else if not (String.equal pd1.prim_native_name pd2.prim_native_name) then
Some Native_name
else if not
(match pd1.prim_native_repr_res, pd2.prim_native_repr_res with
| (_, nr1), (_, nr2) -> Primitive.equal_native_repr nr1 nr2) then
Some Result_repr
else
native_repr_args pd1.prim_native_repr_args pd2.prim_native_repr_args
let value_descriptions ~loc env name
~mmodes
(vd1 : Types.value_description)
(vd2 : Types.value_description) =
Builtin_attributes.check_alerts_inclusion
~def:vd1.val_loc
~use:vd2.val_loc
loc
vd1.val_attributes vd2.val_attributes
name;
begin match Zero_alloc.sub vd1.val_zero_alloc vd2.val_zero_alloc with
| Ok () -> ()
| Error e -> raise (Dont_match (Zero_alloc e))
end;
begin match mmodes with
| All -> begin
match Mode.Modality.Value.sub vd1.val_modalities vd2.val_modalities with
| Ok () -> ()
| Error e -> raise (Dont_match (Modality e))
end;
| Legacy close_over_coercion ->
match Mode.Modality.Value.to_const_opt vd2.val_modalities with
(* [wrap_constraint_with_shape] invokes inclusion check with identical
inferred modalities, which we need to workaround. *)
| None -> ()
| Some val2_modalities ->
let mmode1, mmode2 =
Mode.Value.(disallow_right legacy), Mode.Value.(disallow_left legacy)
in
let mode1 = Mode.Modality.Value.apply vd1.val_modalities mmode1 in
let mode2 = Mode.Modality.Value.(Const.apply val2_modalities mmode2) in
let mode1 =
match close_over_coercion with
| Some held_locks ->
(* Cross modes according to RHS type as it tends to be by the user. *)
let mode1 = Ctype.cross_left env vd2.val_type mode1 in
let mode1 =
Env.walk_locks ~env ~item:Value mode1 (Some vd1.val_type) held_locks
in
mode1.mode
| None -> mode1
in
let mode2 = Ctype.cross_right env vd2.val_type mode2 in
begin match Mode.Value.submode mode1 mode2 with
| Ok () -> ()
| Error e -> raise (Dont_match (Mode e))
end
end;
match vd1.val_kind with
| Val_prim p1 -> begin
match vd2.val_kind with
| Val_prim p2 -> begin
let locality = [ Mode.Locality.global; Mode.Locality.local ] in
let yielding = [ Mode.Yielding.unyielding; Mode.Yielding.yielding ] in
List.iter (fun loc ->
List.iter (fun yield ->
let ty1, _, _, _ = Ctype.instance_prim p1 vd1.val_type in
let ty2, mode_l2, mode_y2, _ = Ctype.instance_prim p2 vd2.val_type in
Option.iter (Mode.Locality.equate_exn loc) mode_l2;
Option.iter (Mode.Yielding.equate_exn yield) mode_y2;
try
Ctype.moregeneral env true ty1 ty2
with Ctype.Moregen err ->
raise (Dont_match (Type err))
) yielding
) locality;
match primitive_descriptions p1 p2 with
| None -> Tcoerce_none
| Some err -> raise (Dont_match (Primitive_mismatch err))
end
| _ ->
let ty1, mode_l1, _, sort1 = Ctype.instance_prim p1 vd1.val_type in
(try Ctype.moregeneral env true ty1 vd2.val_type
with Ctype.Moregen err -> raise (Dont_match (Type err)));
let pc =
{pc_desc = p1; pc_type = vd2.Types.val_type;
pc_poly_mode = Option.map Mode.Locality.disallow_right mode_l1;
pc_poly_sort=sort1;
pc_env = env; pc_loc = vd1.Types.val_loc; } in
Tcoerce_primitive pc
end
| _ ->
match Ctype.moregeneral env true vd1.val_type vd2.val_type with
| exception Ctype.Moregen err -> raise (Dont_match (Type err))
| () -> begin
match vd2.val_kind with
| Val_prim _ -> raise (Dont_match Not_a_primitive)
| _ -> Tcoerce_none
end
(* Inclusion between manifest types (particularly for private row types) *)
let is_absrow env ty =
match get_desc ty with
| Tconstr(Pident _, _, _) ->
(* This function is checking for an abstract row on the side that is being
included into (usually numbered with "2" in this file). In this case,
the abstract row variable has been substituted for an object or variant
type. *)
begin match get_desc (Ctype.expand_head env ty) with
| Tobject _|Tvariant _ -> true
| _ -> false
end
| _ -> false
(* Inclusion between type declarations *)
let choose ord first second =
match ord with
| First -> first
| Second -> second
let choose_other ord first second =
match ord with
| First -> choose Second first second
| Second -> choose First first second
(* Documents which kind of private thing would be revealed *)
type privacy_mismatch =
| Private_type_abbreviation
| Private_variant_type
| Private_record_type
| Private_record_unboxed_product_type
| Private_extensible_variant
| Private_row_type
type type_kind =
| Kind_abstract
| Kind_record
| Kind_record_unboxed_product
| Kind_variant
| Kind_open
let of_kind = function
| Type_abstract _ -> Kind_abstract
| Type_record (_, _, _) -> Kind_record
| Type_record_unboxed_product (_, _, _) -> Kind_record_unboxed_product
| Type_variant (_, _, _) -> Kind_variant
| Type_open -> Kind_open
type kind_mismatch = type_kind * type_kind
type label_mismatch =
| Type of Errortrace.equality_error
| Mutability of position
| Modality of Modality.Value.equate_error
type record_change =
(Types.label_declaration, Types.label_declaration, label_mismatch)
Diffing_with_keys.change
type record_mismatch =
| Label_mismatch of record_change list
| Inlined_representation of position
| Float_representation of position
| Ufloat_representation of position
| Mixed_representation of position
| Mixed_representation_with_flat_floats of position
type constructor_mismatch =
| Type of Errortrace.equality_error
| Arity
| Inline_record of record_change list
| Kind of position
| Explicit_return_type of position
| Modality of int * Modality.Value.equate_error
type extension_constructor_mismatch =
| Constructor_privacy
| Constructor_mismatch of Ident.t
* Types.extension_constructor
* Types.extension_constructor
* constructor_mismatch
type private_variant_mismatch =
| Only_outer_closed (* It's only dangerous in one direction *)
| Missing of position * string
| Presence of string
| Incompatible_types_for of string
| Types of Errortrace.equality_error
type private_object_mismatch =
| Missing of string
| Types of Errortrace.equality_error
type variant_change =
(Types.constructor_declaration as 'l, 'l, constructor_mismatch)
Diffing_with_keys.change
type unsafe_mode_crossing_mismatch =
| Mode_crossing_only_on of position
| Bounds_not_equal of unsafe_mode_crossing * unsafe_mode_crossing
type type_mismatch =
| Arity
| Privacy of privacy_mismatch
| Kind of kind_mismatch
| Constraint of Errortrace.equality_error
| Manifest of Errortrace.equality_error
| Parameter_jkind of type_expr * Jkind.Violation.t
| Private_variant of type_expr * type_expr * private_variant_mismatch
| Private_object of type_expr * type_expr * private_object_mismatch
| Variance
| Record_mismatch of record_mismatch
| Variant_mismatch of variant_change list
| Unboxed_representation of position * attributes
| Extensible_representation of position
| With_null_representation of position
| Jkind of Jkind.Violation.t
| Unsafe_mode_crossing of unsafe_mode_crossing_mismatch
let report_modality_sub_error first second ppf e =
let print_modality id ppf m =
Printtyp.modality ~id:(fun ppf -> Format.pp_print_string ppf id) ppf m
in
let Modality.Value.Error(ax, {left; right}) = e in
Format.fprintf ppf "%s is %a and %s is %a."
(String.capitalize_ascii second)
(print_modality "empty") (Atom (ax, right) : Modality.t)
first
(print_modality "not") (Atom (ax, left) : Modality.t)
let report_mode_sub_error first second ppf e =
let Mode.Value.Error(ax, {left; right}) = e in
Format.fprintf ppf "%s is %a and %s is %a."
(String.capitalize_ascii second)
(Value.Const.print_axis ax) right
first
(Value.Const.print_axis ax) left
let report_modality_equate_error first second ppf ((equate_step, sub_error) : Modality.Value.equate_error) =
match equate_step with
| Left_le_right -> report_modality_sub_error first second ppf sub_error
| Right_le_left -> report_modality_sub_error second first ppf sub_error
module Style = Misc.Style
let report_primitive_mismatch first second ppf err =
let pr fmt = Format.fprintf ppf fmt in
match (err : primitive_mismatch) with
| Name ->
pr "The names of the primitives are not the same"
| Arity ->
pr "The syntactic arities of these primitives were not the same.@ \
(They must have the same number of arrows present in the source.)"
| No_alloc ord ->
pr "%s primitive is %a but %s is not"
(String.capitalize_ascii (choose ord first second))
Style.inline_code "[@@noalloc]"
(choose_other ord first second)
| Builtin ->
pr "The two primitives differ in whether they are builtins"
| Effects ->
pr "The two primitives have different effect annotations"
| Coeffects ->
pr "The two primitives have different coeffect annotations"
| Native_name ->
pr "The native names of the primitives are not the same"
| Result_repr ->
pr "The two primitives' results have different representations"
| Argument_repr n ->
pr "The two primitives' %d%s arguments have different representations"
n (Misc.ordinal_suffix n)
| Layout_poly_attr ->
pr "The two primitives have different [@@layout_poly] attributes"
let report_value_mismatch first second env ppf err =
let pr fmt = Format.fprintf ppf fmt in
pr "@ ";
match (err : value_mismatch) with
| Primitive_mismatch pm ->
report_primitive_mismatch first second ppf pm
| Not_a_primitive ->
pr "The implementation is not a primitive."
| Type trace ->
Printtyp.report_moregen_error ppf Type_scheme env trace
(fun ppf -> Format.fprintf ppf "The type")
(fun ppf -> Format.fprintf ppf "is not compatible with the type")
| Zero_alloc e -> Zero_alloc.print_error ppf e
| Modality e -> report_modality_sub_error first second ppf e
| Mode e -> report_mode_sub_error first second ppf e
let report_type_inequality env ppf err =
Printtyp.report_equality_error ppf Type_scheme env err
(fun ppf -> Format.fprintf ppf "The type")
(fun ppf -> Format.fprintf ppf "is not equal to the type")
let report_privacy_mismatch ppf err =
let singular, item =
match err with
| Private_type_abbreviation -> true, "type abbreviation"
| Private_variant_type -> false, "variant constructor(s)"
| Private_record_type -> true, "record constructor"
| Private_record_unboxed_product_type -> true, "unboxed record constructor"
| Private_extensible_variant -> true, "extensible variant"
| Private_row_type -> true, "row type"
in Format.fprintf ppf "%s %s would be revealed."
(if singular then "A private" else "Private")
item
let report_label_mismatch first second env ppf err =
match (err : label_mismatch) with
| Type err ->
report_type_inequality env ppf err
| Mutability ord ->
Format.fprintf ppf "%s is mutable and %s is not."
(String.capitalize_ascii (choose ord first second))
(choose_other ord first second)
| Modality err_ -> report_modality_equate_error first second ppf err_
let pp_record_diff first second prefix decl env ppf (x : record_change) =
match x with
| Delete cd ->
Format.fprintf ppf "%aAn extra field, %a, is provided in %s %s."
prefix x Style.inline_code (Ident.name cd.delete.ld_id) first decl
| Insert cd ->
Format.fprintf ppf "%aA field, %a, is missing in %s %s."
prefix x Style.inline_code (Ident.name cd.insert.ld_id) first decl
| Change Type {got=lbl1; expected=lbl2; reason} ->
Format.fprintf ppf
"@[<hv>%aFields do not match:@;<1 2>\
%a@ is not the same as:\
@;<1 2>%a@ %a@]"
prefix x
(Style.as_inline_code Printtyp.label) lbl1
(Style.as_inline_code Printtyp.label) lbl2
(report_label_mismatch first second env) reason
| Change Name n ->
Format.fprintf ppf "%aFields have different names, %a and %a."
prefix x
Style.inline_code n.got
Style.inline_code n.expected
| Swap sw ->
Format.fprintf ppf "%aFields %a and %a have been swapped."
prefix x
Style.inline_code sw.first
Style.inline_code sw.last
| Move {name; got; expected } ->
Format.fprintf ppf
"@[<2>%aField %a has been moved@ from@ position %d@ to %d.@]"
prefix x Style.inline_code name expected got
let report_patch pr_diff first second decl env ppf patch =
let nl ppf () = Format.fprintf ppf "@," in
let no_prefix _ppf _ = () in
match patch with
| [ elt ] ->
Format.fprintf ppf "@[<hv>%a@]"
(pr_diff first second no_prefix decl env) elt
| _ ->
let pp_diff = pr_diff first second Diffing_with_keys.prefix decl env in
Format.fprintf ppf "@[<hv>%a@]"
(Format.pp_print_list ~pp_sep:nl pp_diff) patch
let report_record_mismatch first second decl env ppf err =
let pr fmt = Format.fprintf ppf fmt in
match err with
| Label_mismatch patch ->
report_patch pp_record_diff first second decl env ppf patch
| Inlined_representation ord ->
pr "@[<hv>Their internal representations differ:@ %s %s %s.@]"
(choose ord first second) decl
"is an inlined record"
| Float_representation ord ->
pr "@[<hv>Their internal representations differ:@ %s %s %s.@]"
(choose ord first second) decl
"uses unboxed float representation"
| Ufloat_representation ord ->
(* CR layouts: This case should unreachable now. But it may be reachable
when we allow [any] types in structure declarations, using an example
like the "unboxed float representation" one in
[typing-unboxed-types/test.ml]. Add a test then. *)
pr "@[<hv>Their internal representations differ:@ %s %s %s.@]"
(choose ord first second) decl
"uses float# representation"
| Mixed_representation ord ->
(* CR layouts: As above. *)
pr "@[<hv>Their internal representations differ:@ %s %s %s.@]"
(choose ord first second) decl
"uses mixed representation"
| Mixed_representation_with_flat_floats ord ->
pr "@[<hv>Their internal representations differ:@ %s %s %s.@]"
(choose ord first second) decl
"uses a mixed representation where boxed floats are stored flat"
let report_constructor_mismatch first second decl env ppf err =
let pr fmt = Format.fprintf ppf fmt in
match (err : constructor_mismatch) with
| Type err -> report_type_inequality env ppf err
| Arity -> pr "They have different arities."
| Inline_record err ->
report_patch pp_record_diff first second decl env ppf err
| Kind ord ->
pr "%s uses inline records and %s doesn't."
(String.capitalize_ascii (choose ord first second))
(choose_other ord first second)
| Explicit_return_type ord ->
pr "%s has explicit return type and %s doesn't."
(String.capitalize_ascii (choose ord first second))
(choose_other ord first second)
| Modality (i, err) ->
pr "Modality mismatch at argument position %i:@ %a"
(i + 1) (report_modality_equate_error first second) err
(* argument position is one-based; more intuitive *)
let pp_variant_diff first second prefix decl env ppf (x : variant_change) =
match x with
| Delete cd ->
Format.fprintf ppf "%aAn extra constructor, %a, is provided in %s %s."
prefix x Style.inline_code (Ident.name cd.delete.cd_id) first decl
| Insert cd ->
Format.fprintf ppf "%aA constructor, %a, is missing in %s %s."
prefix x Style.inline_code (Ident.name cd.insert.cd_id) first decl
| Change Type {got; expected; reason} ->
Format.fprintf ppf
"@[<hv>%aConstructors do not match:@;<1 2>\
%a@ is not the same as:\
@;<1 2>%a@ %a@]"
prefix x
(Style.as_inline_code Printtyp.constructor) got
(Style.as_inline_code Printtyp.constructor) expected
(report_constructor_mismatch first second decl env) reason
| Change Name n ->
Format.fprintf ppf
"%aConstructors have different names, %a and %a."
prefix x
Style.inline_code n.got
Style.inline_code n.expected
| Swap sw ->
Format.fprintf ppf
"%aConstructors %a and %a have been swapped."
prefix x
Style.inline_code sw.first
Style.inline_code sw.last
| Move {name; got; expected} ->
Format.fprintf ppf
"@[<2>%aConstructor %a has been moved@ from@ position %d@ to %d.@]"
prefix x Style.inline_code name expected got
let report_extension_constructor_mismatch first second decl env ppf err =
let pr fmt = Format.fprintf ppf fmt in
match (err : extension_constructor_mismatch) with
| Constructor_privacy ->
pr "Private extension constructor(s) would be revealed."
| Constructor_mismatch (id, ext1, ext2, err) ->
let constructor =
Style.as_inline_code (Printtyp.extension_only_constructor id)
in
pr "@[<hv>Constructors do not match:@;<1 2>%a@ is not the same as:\
@;<1 2>%a@ %a@]"
constructor ext1
constructor ext2
(report_constructor_mismatch first second decl env) err
let report_private_variant_mismatch first second decl env ppf err =
let pr fmt = Format.fprintf ppf fmt in
let pp_tag ppf x = Format.fprintf ppf "`%s" x in
match (err : private_variant_mismatch) with
| Only_outer_closed ->
(* It's only dangerous in one direction, so we don't have a position *)
pr "%s is private and closed, but %s is not closed"
(String.capitalize_ascii second) first
| Missing (ord, name) ->
pr "The constructor %a is only present in %s %s."
Style.inline_code name (choose ord first second) decl
| Presence s ->
pr "The tag %a is present in the %s %s,@ but might not be in the %s"
(Style.as_inline_code pp_tag) s second decl first
| Incompatible_types_for s -> pr "Types for tag `%s are incompatible" s
| Types err ->
report_type_inequality env ppf err
let report_private_object_mismatch env ppf err =
let pr fmt = Format.fprintf ppf fmt in
match (err : private_object_mismatch) with
| Missing s ->
pr "The implementation is missing the method %a" Style.inline_code s
| Types err -> report_type_inequality env ppf err
let report_kind_mismatch first second ppf (kind1, kind2) =
let pr fmt = Format.fprintf ppf fmt in
let kind_to_string = function
| Kind_abstract -> "abstract"
| Kind_record -> "a record"
| Kind_record_unboxed_product -> "an unboxed record"
| Kind_variant -> "a variant"
| Kind_open -> "an extensible variant" in
pr "%s is %s, but %s is %s."
(String.capitalize_ascii first)
(kind_to_string kind1)
second
(kind_to_string kind2)
let print_unsafe_mode_crossing ppf umc =
Format.fprintf ppf "mod %a@ %a"
Mode.Crossing.print umc.unsafe_mod_bounds
Jkind.With_bounds.format umc.unsafe_with_bounds
let report_unsafe_mode_crossing_mismatch first second ppf e =
let pr fmt = Format.fprintf ppf fmt in
match e with
| Mode_crossing_only_on ord ->
pr "%s has [%@%@unsafe_allow_any_mode_crossing], but %s does not"
(choose ord first second)
(choose_other ord first second)
| Bounds_not_equal (first_umc, second_umc) ->
(* CR layouts v2.8: It'd be nice to specifically highlight the offending axis,
rather than printing all axes here. *)
pr "Both specify [%@%@unsafe_allow_any_mode_crossing], but their \
bounds are not equal@,\
@[%s has:@ %a@]@ \
@[but %s has:@ %a@]"
first print_unsafe_mode_crossing first_umc
second print_unsafe_mode_crossing second_umc
let report_type_mismatch first second decl env ppf err =
let pr fmt = Format.fprintf ppf fmt in
pr "@ ";
match err with
| Arity ->
pr "They have different arities."
| Privacy err ->
report_privacy_mismatch ppf err
| Kind err ->
report_kind_mismatch first second ppf err
| Constraint err ->
(* This error can come from implicit parameter disagreement or from
explicit `constraint`s. Both affect the parameters, hence this choice
of explanatory text *)
pr "Their parameters differ:@,";
report_type_inequality env ppf err
| Manifest err ->
report_type_inequality env ppf err
| Parameter_jkind (ty, v) ->
pr "The problem is in the kinds of a parameter:@,";
Jkind.Violation.report_with_offender
~offender:(fun pp -> Printtyp.type_expr pp ty) ppf v
| Private_variant (_ty1, _ty2, mismatch) ->
report_private_variant_mismatch first second decl env ppf mismatch
| Private_object (_ty1, _ty2, mismatch) ->
report_private_object_mismatch env ppf mismatch
| Variance ->
pr "Their variances do not agree."
| Record_mismatch err ->
report_record_mismatch first second decl env ppf err
| Variant_mismatch err ->
report_patch pp_variant_diff first second decl env ppf err
| Unboxed_representation (ord, attrs) ->
pr "Their internal representations differ:@ %s %s %s."
(choose ord first second) decl
"uses unboxed representation";
if Builtin_attributes.has_unboxed attrs then
pr "@ Hint: %s %s has [%@unboxed]. Did you mean [%@%@unboxed]?"
(choose ord second first) decl
| Extensible_representation ord ->
pr "Their internal representations differ:@ %s %s %s."
(choose ord first second) decl
"is extensible"
| With_null_representation ord ->
pr "Their internal representations differ:@ %s %s %s."
(choose ord first second) decl
"has a null constructor"
| Jkind v ->
Jkind.Violation.report_with_name ~name:first ppf v
| Unsafe_mode_crossing mismatch ->
pr "They have different unsafe mode crossing behavior:@,@[<v 2>%a@]"
(fun ppf (first, second, mismatch) ->
report_unsafe_mode_crossing_mismatch first second ppf mismatch)
(first, second, mismatch)
let compare_unsafe_mode_crossing ~env umc1 umc2 =
match umc1, umc2 with
| None, None -> None
| Some _, None -> Some (Unsafe_mode_crossing (Mode_crossing_only_on First))
| None, Some _ -> Some (Unsafe_mode_crossing (Mode_crossing_only_on Second))
| Some umc1, Some umc2 ->
if equal_unsafe_mode_crossing
~type_equal:(Ctype.type_equal env)
umc1 umc2
then None
else
Some (
Unsafe_mode_crossing (
Bounds_not_equal (umc1, umc2)))
module Record_diffing = struct
let compare_labels env params1 params2
(ld1 : Types.label_declaration)
(ld2 : Types.label_declaration) =
let mut =
match ld1.ld_mutable, ld2.ld_mutable with
| Immutable, Immutable -> None
| Mutable _, Immutable -> Some First
| Immutable, Mutable _ -> Some Second
| Mutable m1, Mutable m2 ->
let open Mode.Alloc.Comonadic.Const in
(if not (eq m1 legacy) then
Misc.fatal_errorf "Unexpected mutable(%a)" print m1);
(if not (eq m2 legacy) then
Misc.fatal_errorf "Unexpected mutable(%a)" print m2);
None
in
begin match mut with
| Some mut -> Some (Mutability mut)
| None ->
match
Modality.Value.Const.equate ld1.ld_modalities ld2.ld_modalities
with
| Ok () ->
let tl1 = params1 @ [ld1.ld_type] in
let tl2 = params2 @ [ld2.ld_type] in
begin
(* Allow renaming: this gets called for inline records in GADT
constructors that may have existentials. *)
match Ctype.equal env true tl1 tl2 with
| exception Ctype.Equality err ->
Some (Type err : label_mismatch)
| () -> None
end
| Error e -> Some (Modality e : label_mismatch)
end
let rec equal ~loc env params1 params2
(labels1 : Types.label_declaration list)
(labels2 : Types.label_declaration list) =
match labels1, labels2 with
| [], [] -> true
| _ :: _ , [] | [], _ :: _ -> false
| ld1 :: rem1, ld2 :: rem2 ->
if Ident.name ld1.ld_id <> Ident.name ld2.ld_id
then false
else begin
Builtin_attributes.check_deprecated_mutable_inclusion
~def:ld1.ld_loc
~use:ld2.ld_loc
loc
ld1.ld_attributes ld2.ld_attributes
(Ident.name ld1.ld_id);
match compare_labels env params1 params2 ld1 ld2 with
| Some _ -> false
(* add arguments to the parameters, cf. PR#7378 *)
| None ->
equal ~loc env
(ld1.ld_type::params1) (ld2.ld_type::params2)
rem1 rem2
end
module Defs = struct
type left = Types.label_declaration
type right = left
type diff = label_mismatch
type state = type_expr list * type_expr list
end
module Diff = Diffing_with_keys.Define(Defs)
let update (d:Diff.change) (params1,params2 as st) =
match d with
| Insert _ | Change _ | Delete _ -> st
| Keep (x,y,_) ->
(* We need to add equality between existential type parameters
(in inline records) *)
x.data.ld_type::params1, y.data.ld_type::params2
let test _loc env (params1,params2)
({pos; data=lbl1}: Diff.left)
({data=lbl2; _ }: Diff.right)
=
let name1, name2 = Ident.name lbl1.ld_id, Ident.name lbl2.ld_id in
if name1 <> name2 then
let types_match =
match compare_labels env params1 params2 lbl1 lbl2 with
| Some _ -> false
| None -> true
in
Error
(Diffing_with_keys.Name {types_match; pos; got=name1; expected=name2})
else
match compare_labels env params1 params2 lbl1 lbl2 with
| Some reason ->
Error (
Diffing_with_keys.Type {pos; got=lbl1; expected=lbl2; reason}
)
| None -> Ok ()
let weight: Diff.change -> _ = function
| Insert _ -> 10
| Delete _ -> 10
| Keep _ -> 0
| Change (_,_,Diffing_with_keys.Name t ) ->
if t.types_match then 10 else 15
| Change _ -> 10
let key (x: Defs.left) = Ident.name x.ld_id
let diffing loc env params1 params2 cstrs_1 cstrs_2 =
let module Compute = Diff.Simple(struct
let key_left = key
let key_right = key
let update = update
let test = test loc env
let weight = weight
end)
in
Compute.diff (params1,params2) cstrs_1 cstrs_2
let compare ~loc env params1 params2 l r =
if equal ~loc env params1 params2 l r then
None
else
Some (diffing loc env params1 params2 l r)
let find_mismatch_in_mixed_record_representations
(s1 : mixed_product_shape) (s2 : mixed_product_shape)
=
if s1 = s2 then None
else
let has_float_boxed_on_read fields =
Array.exists (function
| Float_boxed -> true
| _ -> false)
fields
in
if has_float_boxed_on_read s1
then Some (Mixed_representation_with_flat_floats First)
else if has_float_boxed_on_read s2
then Some (Mixed_representation_with_flat_floats Second)
else
Misc.fatal_error
"Impossible: the only way for mixed blocks to differ in \
representation is if one is a flat float record with a boxed float \
field, and the other isn't."
let compare_with_representation (type rep) ~loc
(record_form : rep record_form) env params1 params2 l r
(rep1 : rep) (rep2 : rep) =
if not (equal ~loc env params1 params2 l r) then
let patch = diffing loc env params1 params2 l r in
Some (Record_mismatch (Label_mismatch patch))
else
match record_form with
| Legacy ->
begin match rep1, rep2 with
| Record_unboxed, Record_unboxed -> None
| Record_unboxed, _ -> Some (Unboxed_representation (First, []))
| _, Record_unboxed -> Some (Unboxed_representation (Second, []))
| Record_inlined _, Record_inlined _ -> None
| Record_inlined _, _ ->
Some (Record_mismatch (Inlined_representation First))
| _, Record_inlined _ ->
Some (Record_mismatch (Inlined_representation Second))
| Record_float, Record_float -> None
| Record_float, _ ->
Some (Record_mismatch (Float_representation First))
| _, Record_float ->
Some (Record_mismatch (Float_representation Second))
| Record_ufloat, Record_ufloat -> None
| Record_ufloat, _ ->
Some (Record_mismatch (Ufloat_representation First))
| _, Record_ufloat ->
Some (Record_mismatch (Ufloat_representation Second))
| Record_mixed m1, Record_mixed m2 ->
begin match find_mismatch_in_mixed_record_representations m1 m2 with
| None -> None
| Some mismatch -> Some (Record_mismatch mismatch)
end
| Record_mixed _, _ ->
Some (Record_mismatch (Mixed_representation First))
| _, Record_mixed _ ->
Some (Record_mismatch (Mixed_representation Second))
| Record_boxed _, Record_boxed _ -> None
end
| Unboxed_product ->
begin match rep1, rep2 with
| Record_unboxed_product, Record_unboxed_product -> None
end
end
(* just like List.find_map, but also gives index if found *)
let rec find_map_idx f ?(off = 0) l =
match l with
| [] -> None
| x :: xs -> begin
match f x with
| None -> find_map_idx f ~off:(off+1) xs
| Some y -> Some (off, y)
end
let get_error = function
| Ok () -> None
| Error e -> Some e
module Variant_diffing = struct
let compare_constructor_arguments ~loc env params1 params2 arg1 arg2 =
match arg1, arg2 with
| Types.Cstr_tuple arg1, Types.Cstr_tuple arg2 ->
if List.length arg1 <> List.length arg2 then
Some (Arity : constructor_mismatch)
else begin
let type_and_mode (ca : Types.constructor_argument) = ca.ca_type, ca.ca_modalities in
let arg1_tys, arg1_gfs = List.split (List.map type_and_mode arg1)
and arg2_tys, arg2_gfs = List.split (List.map type_and_mode arg2)
in
(* Ctype.equal must be called on all arguments at once, cf. PR#7378 *)
(* Allow renaming: in the GADT case, these arguments are distinct from
type parameters (which have been unified). See also
Note [Contravariance of type parameter jkinds]. *)
match Ctype.equal env true (params1 @ arg1_tys) (params2 @ arg2_tys) with
| exception Ctype.Equality err -> Some (Type err)
| () -> List.combine arg1_gfs arg2_gfs
|> find_map_idx
(fun (x,y) -> get_error @@ Modality.Value.Const.equate x y)
|> Option.map (fun (i, err) -> Modality (i, err))
end
| Types.Cstr_record l1, Types.Cstr_record l2 ->
Option.map
(fun rec_err -> Inline_record rec_err)
(Record_diffing.compare env ~loc params1 params2 l1 l2)
| Types.Cstr_record _, _ -> Some (Kind First : constructor_mismatch)
| _, Types.Cstr_record _ -> Some (Kind Second : constructor_mismatch)
let compare_constructors ~loc env params1 params2 res1 res2 args1 args2 =
match res1, res2 with
| Some r1, Some r2 ->
(* Allow renaming here: variables in GADT-syntax constructors are
distinct from the variables in type parameters *)
begin match Ctype.equal env true [r1] [r2] with
| exception Ctype.Equality err -> Some (Type err)
(* Pass the result types in this call to
[compare_constructor_arguments], so that the call to [Ctype.equal]
can see the entire scope of the variables *)
| () -> compare_constructor_arguments ~loc env [r1] [r2] args1 args2
end
| Some _, None -> Some (Explicit_return_type First)
| None, Some _ -> Some (Explicit_return_type Second)
| None, None ->
compare_constructor_arguments ~loc env params1 params2 args1 args2
let equal ~loc env params1 params2
(cstrs1 : Types.constructor_declaration list)
(cstrs2 : Types.constructor_declaration list) =
List.length cstrs1 = List.length cstrs2 &&
List.for_all2 (fun (cd1:Types.constructor_declaration)
(cd2:Types.constructor_declaration) ->
Ident.name cd1.cd_id = Ident.name cd2.cd_id
&&
begin
Builtin_attributes.check_alerts_inclusion
~def:cd1.cd_loc
~use:cd2.cd_loc
loc
cd1.cd_attributes cd2.cd_attributes
(Ident.name cd1.cd_id)
;
match compare_constructors ~loc env params1 params2
cd1.cd_res cd2.cd_res cd1.cd_args cd2.cd_args with
| Some _ -> false
| None -> true
end) cstrs1 cstrs2
module Defs = struct
type left = Types.constructor_declaration
type right = left
type diff = constructor_mismatch
type state = type_expr list * type_expr list
end
module D = Diffing_with_keys.Define(Defs)
let update _ st = st
let weight: D.change -> _ = function
| Insert _ -> 10
| Delete _ -> 10
| Keep _ -> 0
| Change (_,_,Diffing_with_keys.Name t) ->
if t.types_match then 10 else 15
| Change _ -> 10
let test loc env (params1,params2)
({pos; data=cd1}: D.left)
({data=cd2; _}: D.right) =
let name1, name2 = Ident.name cd1.cd_id, Ident.name cd2.cd_id in
if name1 <> name2 then
let types_match =
match compare_constructors ~loc env params1 params2
cd1.cd_res cd2.cd_res cd1.cd_args cd2.cd_args with
| Some _ -> false
| None -> true
in
Error
(Diffing_with_keys.Name {types_match; pos; got=name1; expected=name2})
else
match compare_constructors ~loc env params1 params2
cd1.cd_res cd2.cd_res cd1.cd_args cd2.cd_args with
| Some reason ->