/
w_Unify.ml
1345 lines (1272 loc) · 66.3 KB
/
w_Unify.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
(*
Copyright © 2011, 2012 MLstate
This file is part of Opa.
Opa is free software: you can redistribute it and/or modify it under the
terms of the GNU Affero General Public License, version 3, as published by
the Free Software Foundation.
Opa is distributed in the hope that it will be useful, but WITHOUT ANY
WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
FOR A PARTICULAR PURPOSE. See the GNU Affero General Public License for
more details.
You should have received a copy of the GNU Affero General Public License
along with Opa. If not, see <http://www.gnu.org/licenses/>.
*)
(*
@author François Pessaux
*)
(* depends *)
module List = BaseList
type detail_kind =
| DK_none (** No additionnal and more precise information. This is the
general failure case where types are simply incompatible. *)
| DK_fun_type_arity of (int * int) (** Arity mismatch between 2 function
types. *)
| DK_named_type_arity of (W_Algebra.type_name_ident * int * int) (** Arity
mismatch between the arguments of 2 instances of a same named type. *)
| DK_binding_level_mismatch (** Case of unification between 2 type
variables with one being generalized and the other not, or between a
generalized type variable and another type (not being a type
variable). *)
| DK_forall_type_quantification_arity of (int * int) (** Case where the 2
schemes of types forall do not have the same number of generalized
variables. *)
(* ************************************************************************** *)
(** {b Descr}: Information precising a unification conflict when the unification
failed in a case where we can give more accurate description of the issue
to the user.
{b Visibility}: Exported outside this module. *)
(* ************************************************************************** *)
type unification_conflict_detail = {
ucd_kind : detail_kind ;
ucd_through_field : string option (** If the unification conflict appeared
through the unification of 2 record fields of same name, this is the name
of the 2 fields that caused the error. *)
}
(* ************************************************************************** *)
(** {b Descr}: Exception raised in case of unification failure on 2 simple
types.
{b Visibility}: Exported outside this module. *)
(* ************************************************************************** *)
exception Unification_simple_type_conflict of
(W_Algebra.simple_type * W_Algebra.simple_type * unification_conflict_detail)
(* ************************************************************************** *)
(** {b Descr}: Exception raised in case of unification failure on 2 sum
types (i.e. on 2 columns). This exception must not escape when unification
id triggered by a call to the unification between 2 [simple_type]s and
must caught by it ([unify_simple_type]) to issue an explicit error message.
Because we finally needed to export [unify_column_type], this exception
can only escape outside this module if unification is triggered by a call
to unification between 2 column types.
{b Visibility}: Exported outside this module. *)
(* ************************************************************************** *)
exception Unification_column_conflict of
(W_Algebra.column_type * W_Algebra.column_type)
(* ************************************************************************** *)
(** {b Descr}: Lowerize types level inside a [simple_type].
{b Visibility}: Not exported outside this module. *)
(* ************************************************************************** *)
let rec lowerize_level_in_simple_type max_level ty =
assert (max_level < W_CoreTypes.generic_binding_level) ;
(* First, get the canonical representation of the type. *)
let ty = W_CoreTypes.simple_type_repr ty in
match ty.W_Algebra.sty_mark with
| W_Algebra.TM_lowerise_seen -> ()
| W_Algebra.TM_not_seen -> (
(* First, mark the type as as seen to prevent looping. *)
ty.W_Algebra.sty_mark <- W_Algebra.TM_lowerise_seen ;
match ty.W_Algebra.sty_desc with
| W_Algebra.SType_var ty_var_desc -> (
if ty_var_desc.W_Algebra.tv_level > max_level then (
(* Types (variables) marked as generalized are those left marked
under a forall-type, hence remains bound by a scheme, hence must
not be lowerized. So if a variable has the generic binding level,
we don't touch its level. *)
if ty_var_desc.W_Algebra.tv_level <>
W_CoreTypes.generic_binding_level then (
(* Set the level inside the type. *)
W_CoreTypes.change_ty_var_level ty_var_desc max_level
)
)
)
| W_Algebra.SType_arrow (args_tys, res_ty) ->
List.iter (lowerize_level_in_simple_type max_level) args_tys ;
lowerize_level_in_simple_type max_level res_ty
| W_Algebra.SType_named named ->
(match named.W_Algebra.nst_unwinded with
| None -> ()
| Some t' -> lowerize_level_in_simple_type max_level t') ;
List.iter
(lowerize_level_in_simple_type max_level) named.W_Algebra.nst_args
| W_Algebra.SType_sum_of_records sumcases_column ->
lowerize_level_in_column max_level sumcases_column
| W_Algebra.SType_forall scheme ->
lowerize_level_in_simple_type max_level scheme.W_Algebra.body
)
| _ (* Other markers. *) -> assert false
(* ************************************************************************** *)
(** {b Descr}: Lowerize variables level inside a row type.
{b Visibility}: Not exported outside this module. *)
(* ************************************************************************** *)
and lowerize_level_in_row max_level row =
(* First, get the canonical representation of the row type. *)
let (row_fields, row_ending) =
(W_CoreTypes.row_type_repr row).W_Algebra.rt_value in
List.iter
(fun (_, ty) -> lowerize_level_in_simple_type max_level ty) row_fields ;
(match row_ending with
| W_Algebra.Var_row row_variable ->
(* Variables marked as generalized are those left marked under a
forall-type, hence remains bound by a scheme, hence must not be
lowerized. So if a variable has the generic binding level, we
don't touch its level. *)
if row_variable.W_Algebra.rv_level > max_level &&
row_variable.W_Algebra.rv_level <>
W_CoreTypes.generic_binding_level then
W_CoreTypes.change_row_var_level row_variable max_level
| W_Algebra.Closed_row -> ())
(* ************************************************************************** *)
(** {b Descr}: Lowerize variables level inside a column type.
{b Visibility}: Not exported outside this module. *)
(* ************************************************************************** *)
and lowerize_level_in_column max_level column =
(* First, get the canonical representation of the column type. *)
let (col_rows, col_ending) =
(W_CoreTypes.column_type_repr column).W_Algebra.ct_value in
List.iter (lowerize_level_in_row max_level) col_rows ;
(match col_ending with
| W_Algebra.Var_column col_variable ->
(* Variables marked as generalized are those left marked under a
forall-type, hence remains bound by a scheme, hence must not be
lowerized. So if a variable has the generic binding level, we
don't touch its level. *)
if col_variable.W_Algebra.cv_level > max_level &&
col_variable.W_Algebra.cv_level <>
W_CoreTypes.generic_binding_level then
W_CoreTypes.change_column_var_level col_variable max_level
| W_Algebra.Closed_column -> ())
(* ************************************************************************** *)
(** {b Descr}: Computes the min binding level of 2 row endings. This is used
when creating a new row variable for unification, in order to give it
directly a binding level being the smallest one of the 2 endings of the
rows we want to unify.
If none of the endings have a variable, then the returned minimal level is
the current binding level, i.e. the one with which anyway the fresh variable
created before calling this function was initialized.
{b ATTENTION}: This function assumes it is called on row endings that are
canonical representation, i.e. obtained after a call to [row_type_repr].
{b Visibility}: Not exported outside this module. *)
(* ************************************************************************** *)
let min_level_of_row_endings end1 end2 =
match (end1, end2) with
| (W_Algebra.Closed_row, W_Algebra.Closed_row) ->
(* None of the endings is a variable, hence there is no smaller level
than the current one. *)
!W_CoreTypes.current_binding_level
| ((W_Algebra.Var_row rv), W_Algebra.Closed_row)
| (W_Algebra.Closed_row, (W_Algebra.Var_row rv)) ->
(* There is only one ending with a variable. Then the minimal level is
the one of this only variable. *)
rv.W_Algebra.rv_level
| ((W_Algebra.Var_row rv1), (W_Algebra.Var_row rv2)) ->
min rv1.W_Algebra.rv_level rv2.W_Algebra.rv_level
(* ************************************************************************** *)
(** {b Descr}: Computes the min binding level of 2 column endings. This
function works like its counterpart for row, i.e.
[min_level_of_row_endings].
{b ATTENTION}: This function assumes it is called on column endings that are
canonical representation, i.e. obtained after a call to [column_type_repr].
{b Visibility}: Not exported outside this module. *)
(* ************************************************************************** *)
let min_level_of_column_endings end1 end2 =
match (end1, end2) with
| (W_Algebra.Closed_column, W_Algebra.Closed_column) ->
(* None of the endings is a variable, hence there is no smaller level
than the current one. *)
!W_CoreTypes.current_binding_level
| ((W_Algebra.Var_column cv), W_Algebra.Closed_column)
| (W_Algebra.Closed_column, (W_Algebra.Var_column cv)) ->
(* There is only one ending with a variable. Then the minimal level is
the one of this only variable. *)
cv.W_Algebra.cv_level
| ((W_Algebra.Var_column cv1), (W_Algebra.Var_column cv2)) ->
min cv1.W_Algebra.cv_level cv2.W_Algebra.cv_level
(* ************************************************************************* *)
(* bool -> W_Algebra.simple_type list -> W_Algebra.simple_type list -> bool *)
(** {b Descr}: Function checking if 2 type variables lists are in injection
and if the first argument is true, are also in bijection.
In other words, we have 2 lists of types [v_vars] and [w_vars], assumed
all to be *type variables* and we want to ensure that all the variables
from the first list are equal (i.e. were unified with) one variable of
the second list and, if the first argument is true the other way: that
all the variables of the second list are equal (were unified with) to one
variable of the first list.
This obviously means that both lists have the same length.
This function is used to ensure that during unification of 2 types forall,
the generalized variables of both schemes we mapped one-to-one, in other
words that both schemes are as general.
Using this mechanism of bijection allows to be independant on the order
of variables in the quantifications of the schemes. In effect, we take an
instance of each scheme and unify the bodies of these instances. During
this unification, generalized type variables are mapped to their
counterpart in the other type. At the end, we just need to verify that
they were all mapped once to a counterpart variable.
Note by the was that because this applies on qualtified variables, since
unification allows to unify a generalized type variable only with a also
generalized other type variable, we are sure that at the end of unification,
then when we call the present function, all the variables manipulated will
be generalized ones.
{b Visibility}: Not exported outside this module. *)
(* ************************************************************************* *)
let check_type_variables_are_in_injection check_bijection w_vars v_vars =
(* Local function testing if 2 types are physically equal variables. *)
let test_vars_eq t1 t2 =
match (t1.W_Algebra.sty_desc, t2.W_Algebra.sty_desc) with
| ((W_Algebra.SType_var v1), (W_Algebra.SType_var v2)) ->
v1 == v2
| (_, _) -> false in
(* Local function that takes one variable and tries to remove it from the
list of other variables. *)
let check_one_v v ws =
(* If the variable can't be removed because it is not in the list, then
[Not_found] will be raised. *)
List.remove_first_or_fail_eq ~eq: test_vars_eq v ws in
(* Now, iterate the above local function on all the variables "v". At each
iteration, we get a reduced list of variables "w" in which to find the
next variable "v". At the end, we expect the remaining list of variables
"w" to be empty, i.e. meaning that all the variables "v" were found
equal to one unique variable "w" and reciprocally. *)
try
let remaining_ws =
List.fold_left
(fun accu_ws v -> check_one_v v accu_ws)
(List.map W_CoreTypes.simple_type_repr w_vars) v_vars in
if check_bijection then assert (remaining_ws = []) ;
true
with Not_found -> false
(* ************************************************************************* *)
(* bool -> W_Algebra.row_variable list -> W_Algebra.row_variable list -> bool*)
(** {b Descr}: Performs the same job than
[check_type_variables_are_in_injection] above, but on row variables.
See header of [check_type_variables_are_in_injection] for more details.
{b Visibility}: Not exported outside this module. *)
(* ************************************************************************* *)
let check_row_variables_are_in_injection check_bijection w_vars v_vars =
(* We simulate a call to "repr" on a row variable. To do this, we manually
inspect the [W_Algebra.rv_value] fields. If it is [W_Algebra.Row_unknown]
then the variable was not instantiated and we take it as it is.
If it is [W_Algebra.Row_known, then we call [W_CoreTypes.row_type_repr]
to get the canonical representation of the variable's value then we
check that we got a row type with not fields and if so, we take its
ending variable. *)
let repr v =
match v.W_Algebra.rv_value with
| W_Algebra.Row_unknown -> v
| W_Algebra.Row_known row_type -> (
match (W_CoreTypes.row_type_repr row_type).W_Algebra.rt_value with
| ([], W_Algebra.Var_row v') -> v'
| _ -> v
(* Instantiated by something else than a variable. *)
) in
let check_one_v v ws =
(* If the variable can't be removed because it is not in the list, then
[Not_found] will be raised. *)
List.remove_first_or_fail_eq ~eq: (==) v ws in
(* Same explanation than in [check_type_variables_are_in_injection] above. *)
try
let remaining_ws =
List.fold_left
(fun accu_ws v -> check_one_v v accu_ws)
(List.map repr w_vars) v_vars in
if check_bijection then assert (remaining_ws = []) ;
true
with Not_found -> false
(* ************************************************************************* *)
(* bool -> W_Algebra.column_variable list
-> W_Algebra.column_variable list -> bool *)
(** {b Descr}: Performs the same job than
[check_type_variables_are_in_bijection] above, but on column variables.
See header of [check_type_variables_are_in_injection] for more details.
{b Visibility}: Not exported outside this module. *)
(* ************************************************************************* *)
let check_column_variables_are_in_injection check_bijection w_vars v_vars =
(* Same explanation than in [check_row_variables_are_in_injection] above. *)
let repr v =
match v.W_Algebra.cv_value with
| W_Algebra.Col_unknown -> v
| W_Algebra.Col_known col_type -> (
match (W_CoreTypes.column_type_repr col_type).W_Algebra.ct_value with
| ([], W_Algebra.Var_column v') -> v'
| _ -> v
) in
let check_one_v v ws =
List.remove_first_or_fail_eq ~eq: (==) v ws in
(* Same explanation than in [check_type_variables_are_in_bijection] above. *)
try
let remaining_ws =
List.fold_left
(fun accu_ws v -> check_one_v v accu_ws)
(List.map repr w_vars) v_vars in
if check_bijection then assert (remaining_ws = []) ;
true
with Not_found -> false
(* ************************************************************************** *)
(** {b Descr}: Internal function catches the exception thrown by
[__unify_simple_type] and raises a new one that contains the initial type
and not its synonim (i.e. list(string) instead of
{head:string; tl:list(string)} / nil)
@raise Unification_simple_type_conflict
{b Visibility}: Not exported outside this module. *)
(* ************************************************************************** *)
let rec __unify_and_return_higher_type is_under_coercion
env seen_expansions ty1' ty2' ty1 ty2 =
try
__unify_simple_type is_under_coercion env seen_expansions ty1' ty2'
with (Unification_simple_type_conflict (ty3, ty4, context)) ->
if ty1' == ty3 || ty1' == ty3 || ty2' == ty4 || ty2' == ty4
then raise (Unification_simple_type_conflict(ty1, ty2, context))
else raise (Unification_simple_type_conflict(ty3, ty4, context))
(* ************************************************************************** *)
(** {b Descr}: Internal function performing unification of 2 simple types.
In any case (error or success), this function keeps the trace of the
modifications done by the unification. This will be the job of the initial
caller ([unify_simple_type], [unify_row_type] or [unify_column_type]) to
deal with what to do of this trace.
@raise Unification_simple_type_conflict
@raise Unification_binding_level_conflict
{b Visibility}: Not exported outside this module. *)
(* ************************************************************************** *)
and __unify_simple_type is_under_coercion env seen_expansions ty1 ty2 =
#<If:TYPER $minlevel 11> (* <---------- DEBUG *)
OManager.printf "__unify_simple_type:%b %a VERSUS %a@." is_under_coercion
W_PrintTypes.pp_simple_type_start_sequence ty1
W_PrintTypes.pp_simple_type_end_sequence ty2 ;
#<End> ; (* <---------- END DEBUG *)
(* Special case optimization just in case the 2 types are already the same. *)
if ty1 == ty2 then () else
(* First, get the canonical representation of the 2 types to unify. *)
let ty1 = W_CoreTypes.simple_type_repr ty1 in
let ty2 = W_CoreTypes.simple_type_repr ty2 in
if ty1 == ty2 then ()
else
match (ty1.W_Algebra.sty_desc, ty2.W_Algebra.sty_desc) with
| ((W_Algebra.SType_var var1), (W_Algebra.SType_var var2)) -> (
(* Unification between variables must prevent unification of a
generalized variable with something else than another generalized
variable. Otherwise, this would mean that a generalized variable
gets no more generalized, hence one of the 2 unified types would
lose its generality. *)
if (var1.W_Algebra.tv_level <> W_CoreTypes.generic_binding_level &&
var2.W_Algebra.tv_level <> W_CoreTypes.generic_binding_level)
||
(var1.W_Algebra.tv_level = W_CoreTypes.generic_binding_level &&
var2.W_Algebra.tv_level = W_CoreTypes.generic_binding_level) then (
(* To try to preserve as far as we can the names given by the user to
variables, if we are unifying 2 variables with on having no name
and the other having a name, then we make the no-name equal to the
with-name. Note that in case both variables have a name, this
heuristic won't work and there is no principal better choice.
I don't know why, I thought that keeping the most recent name was
better but in fact, it seems that keeping the oldest seems to
give the best results. This is really hackish. *)
let v1_name = QmlTypeVars.TypeVar.name var1.W_Algebra.tv_qml in
let v2_name = QmlTypeVars.TypeVar.name var2.W_Algebra.tv_qml in
(* A bit casual: since there are only 2 ways to assign variables, we
encode the assignment way by a boolean. [true] means that [var1] is
assigned the identity of [var2]. *)
let way =
(match (v1_name, v2_name) with
| ("", "") -> true (* Arbitrary: v1 <- v2. *)
| ("", _) -> true (* v1 <- v2. *)
| (_, "") -> false (* v2 <- v1. *)
| (_, _) ->
(* The most recent variable <- the oldest variable. We use
stamps for this. *)
(QmlTypeVars.TypeVar.to_int var1.W_Algebra.tv_qml) >
(QmlTypeVars.TypeVar.to_int var2.W_Algebra.tv_qml)) in
if way then (
(* [var1] has no name or both have names and [var1] is the most
recent variable. Hence it will be assigned the identity of
[var2]. *)
(* Behave like the general case var U ty. Since we are in a case
of 2 variables. We must not forget to adjust the level of the
first variable. *)
if var2.W_Algebra.tv_level > var1.W_Algebra.tv_level then
W_CoreTypes.change_ty_var_level var2 var1.W_Algebra.tv_level ;
W_CoreTypes.change_ty_link ~receiver: ty1 ~link_val: (Some ty2)
)
else (
(* [var1] has a name or both have names and [var2] is the most
recent variable. So [var2] will be assigned the identity of
[var1] and the process is symetrical than above. *)
if var1.W_Algebra.tv_level > var2.W_Algebra.tv_level then
W_CoreTypes.change_ty_var_level var1 var2.W_Algebra.tv_level ;
W_CoreTypes.change_ty_link ~receiver: ty2 ~link_val: (Some ty1)
)
)
else (
(* This is a failure case where one of the variable is generalized
and not the other. Hence accepting the unification would lead
into one of the type (the more general) to lose its generality
to become equal to the other. And in this case, unification
would not make the 2 types equal. *)
raise
(Unification_simple_type_conflict
(ty1, ty2,
{ ucd_kind = DK_binding_level_mismatch ;
ucd_through_field = None })) ;
)
)
| ((W_Algebra.SType_var var1), _) -> (
(* Prevents creating cycles through unification of ['a] and ['a t] when
['a t] is defined as [type 'a t = 'a u = 'a v ... = 'a]. *)
let are_same =
W_TypeAbbrevs.deep_exact_occur_expand_abbrev
env seen_expansions ~ty_var: ty1 ~in_ty: ty2 in
if are_same then ()
else (
(* If the variable is generalized, then we must not unify since this
would means a loss of generality. In effect, generalized variable
are not instantiable ! *)
if var1.W_Algebra.tv_level = W_CoreTypes.generic_binding_level
then if is_under_coercion
then W_CoreTypes.change_ty_var_level var1
!W_CoreTypes.current_binding_level
else (
raise
(Unification_simple_type_conflict
(ty1, ty2,
{ ucd_kind = DK_binding_level_mismatch ;
ucd_through_field = None }))
);
lowerize_level_in_simple_type var1.W_Algebra.tv_level ty2 ;
(* Don't forget to cleanup the lowerized type. *)
W_CoreTypes.cleanup_simple_type ty2 ;
W_CoreTypes.change_ty_link ~receiver: ty1 ~link_val: (Some ty2)
)
)
| (_, (W_Algebra.SType_var var2)) -> (
(* Case symmetric than the previous one. *)
let are_same =
W_TypeAbbrevs.deep_exact_occur_expand_abbrev
env seen_expansions ~ty_var: ty2 ~in_ty: ty1 in
if are_same then ()
else (
if var2.W_Algebra.tv_level = W_CoreTypes.generic_binding_level then
raise
(Unification_simple_type_conflict
(ty1, ty2,
{ ucd_kind = DK_binding_level_mismatch ;
ucd_through_field = None })) ;
lowerize_level_in_simple_type var2.W_Algebra.tv_level ty1 ;
(* Don't forget to cleanup the lowerized type. *)
W_CoreTypes.cleanup_simple_type ty1 ;
W_CoreTypes.change_ty_link ~receiver: ty2 ~link_val: (Some ty1)
)
)
| (W_Algebra.SType_arrow (args_tys1, res_ty1),
W_Algebra.SType_arrow (args_tys2, res_ty2)) -> (
(* Ensure we are not in the case of an error of arity between the
two function types. Note that this also prevent the [List.iter2]
exception from being raised in case of arity mismatch.
Making the test before unifying allows to issue a smarter error
message about arity before a possible type mismatch is detected and
issued first when unifying 2-by-2 the non-matching expected and
provided types. *)
let n1 = List.length args_tys1 in
let n2 = List.length args_tys2 in
if n1 <> n2 then
raise
(Unification_simple_type_conflict
(ty1, ty2,
{ ucd_kind = DK_fun_type_arity (n1, n2) ;
ucd_through_field = None })) ;
W_CoreTypes.change_ty_link ~receiver: ty1 ~link_val: (Some ty2) ;
(* Unify types of arguments 2 by 2. *)
List.iter2
(__unify_simple_type is_under_coercion env seen_expansions) args_tys1 args_tys2 ;
(* Unify the types of results. *)
__unify_simple_type is_under_coercion env seen_expansions res_ty1 res_ty2
)
| (W_Algebra.SType_named { W_Algebra.nst_name = name ;
W_Algebra.nst_args = args ;
W_Algebra.nst_unwinded = _manifest },
W_Algebra.SType_named { W_Algebra.nst_name = name' ;
W_Algebra.nst_args = args' ;
W_Algebra.nst_unwinded = _manifest' })
when QmlAst.TypeIdent.equal name name' -> (
try
W_CoreTypes.change_ty_link ~receiver: ty1 ~link_val: (Some ty2) ;
List.iter2 (__unify_simple_type is_under_coercion env seen_expansions) args args' ;
(* Two instances of a same named type, as far as they have unifiable
arguments must have unifiable manifest representations. No need
to descend inside in order to save efficiency unless we want
to test assertions.
Moreover, with incremental abbreviations unwinding, this may not
hold anymore... *)
(*
(match (manifest, manifest') with
| (None, None) -> ()
| ((Some m), (Some m')) ->
__unify_simple_type is_under_coercion env m m'
| (_, _) ->
(* Two instances of a same named type should have either no
manifest representation or both one. *)
assert false) ;
*)
with Invalid_argument "List.iter2" ->
(* In fact, we are in the case of an error of arity between the
two type constructors. *)
let n1 = List.length args in
let n2 = List.length args' in
raise
(Unification_simple_type_conflict
(ty1, ty2,
{ ucd_kind = DK_named_type_arity (name, n1, n2) ;
ucd_through_field = None }))
)
| (W_Algebra.SType_named nty1,
W_Algebra.SType_named nty2)
(* name <> name' *) -> (
__unify_different_named_types is_under_coercion env seen_expansions ty1 ty2 nty1 nty2
)
| ((W_Algebra.SType_named { W_Algebra.nst_unwinded = Some manifest }), _) ->
(* Same remark about trivially cyclic types than in the previous
match case. *)
#<If:TYPER $minlevel 11> (* <---------- DEBUG *)
OManager.printf "Case SType_named manifest / other: %a VERSUS %a@."
W_PrintTypes.pp_simple_type_start_sequence ty1
W_PrintTypes.pp_simple_type_end_sequence ty2 ;
#<End> ; (* <---------- END DEBUG *)
if ty1 == (W_CoreTypes.simple_type_repr manifest) then
raise
(Unification_simple_type_conflict
(ty1, ty2,
{ ucd_kind = DK_none ;
ucd_through_field = None })) ;
__unify_simple_type is_under_coercion env seen_expansions ty2 manifest
| (_, (W_Algebra.SType_named { W_Algebra.nst_unwinded = Some manifest })) ->
#<If:TYPER $minlevel 11> (* <---------- DEBUG *)
OManager.printf "Case other / SType_named manifest: %a VERSUS %a@."
W_PrintTypes.pp_simple_type_start_sequence ty1
W_PrintTypes.pp_simple_type_end_sequence ty2 ;
#<End> ; (* <---------- END DEBUG *)
(* Same remark about trivially cyclic types than in the previous
match case. *)
if ty2 == (W_CoreTypes.simple_type_repr manifest) then
raise
(Unification_simple_type_conflict
(ty1, ty2, { ucd_kind = DK_none ; ucd_through_field = None })) ;
__unify_simple_type is_under_coercion env seen_expansions ty1 manifest
| ((W_Algebra.SType_named { W_Algebra.nst_unwinded = None }), _) -> (
#<If:TYPER $minlevel 11> (* <---------- DEBUG *)
OManager.printf "Case SType_named non-manifest / other: %a VERSUS %a@."
W_PrintTypes.pp_simple_type_start_sequence ty1
W_PrintTypes.pp_simple_type_end_sequence ty2 ;
#<End> ; (* <---------- END DEBUG *)
let (ty1', seen_expansions') =
W_TypeAbbrevs.incrementally_expand_abbrev env seen_expansions ty1 in
#<If:TYPER $minlevel 11> (* <---------- DEBUG *)
OManager.printf "SType_named non-manifest expanded: %a@."
W_PrintTypes.pp_simple_type ty1' ;
#<End> ; (* <---------- END DEBUG *)
if ty1 == ty1' then
raise
(Unification_simple_type_conflict
(ty1, ty2, { ucd_kind = DK_none ; ucd_through_field = None })) ;
__unify_and_return_higher_type is_under_coercion
env seen_expansions' ty2 ty1' ty2 ty1
)
| (_, (W_Algebra.SType_named { W_Algebra.nst_unwinded = None })) -> (
#<If:TYPER $minlevel 11> (* <---------- DEBUG *)
OManager.printf "Case other / SType_named non-manifest: %a VERSUS %a@."
W_PrintTypes.pp_simple_type_start_sequence ty1
W_PrintTypes.pp_simple_type_end_sequence ty2 ;
#<End> ; (* <---------- END DEBUG *)
let (ty2', seen_expansions') =
W_TypeAbbrevs.incrementally_expand_abbrev env seen_expansions ty2 in
if ty2 == ty2' then
raise
(Unification_simple_type_conflict
(ty1, ty2, { ucd_kind = DK_none ; ucd_through_field = None })) ;
__unify_and_return_higher_type is_under_coercion
env seen_expansions' ty1 ty2' ty1 ty2
)
| ((W_Algebra.SType_sum_of_records col1),
(W_Algebra.SType_sum_of_records col2)) -> (
try
W_CoreTypes.change_ty_link ~receiver: ty1 ~link_val: (Some ty2) ;
__unify_column_type is_under_coercion env seen_expansions col1 col2
with Unification_column_conflict (_, _) ->
(* At this point, recover the unification on columns failure.
[TODO] There should be a clear error message here, but for the
moment it's rather crude. ^^ *)
raise
(Unification_simple_type_conflict
(ty1, ty2, { ucd_kind = DK_none ; ucd_through_field = None }))
)
| ((W_Algebra.SType_forall scheme1), (W_Algebra.SType_forall scheme2)) -> (
W_CoreTypes.change_ty_link ~receiver: ty1 ~link_val: (Some ty2) ;
(*
Naive unification, just instantiating both schemes then unifying
the obtained bodies is wrong !
For example, on the following program we would get:
if true then {{ id = fun x -> x }} else {{ id = fun x -> 5 }} ;;
- : { id: for all 'Ta . ('Ta -> 'Ta); . } / 'Ca
which is clearly wrong since in the second branch of the
conditional, the type of the function id is not as general as
'a -> 'a !
*)
(* We must take an instance of each scheme body, but make so that
generalized variables keep a generic level. This means that we
must create a copy of the bodies, with fresh variables in place
of the generalized ones, but these fresh variables being still
at generic level. Making a copy prevents from dirtying our
schemes. Forcing copies of generalized variables to be generic
will allow unification not to instantiate them by something else
than another generic variable. *)
(* We count by side effect the number of variables in each scheme
to save a call to List.length. A bit casual, but more efficient. *)
let count_ty_vars1 = ref 0 in
let count_ty_vars2 = ref 0 in
(* Create the mappings of generalized variables of the scheme onto
fresh *also generalized* type variables. *)
let ty_vars_mapping1 =
List.map
(fun sch ->
incr count_ty_vars1 ;
let tyv = W_CoreTypes.__generic_type_variable () in
W_TypeInfo.add_linked_object
tyv.W_Algebra.sty_desc ty1.W_Algebra.sty_desc ;
(sch, tyv))
scheme1.W_Algebra.ty_parameters in
let ty_vars_mapping2 =
List.map
(fun sch ->
incr count_ty_vars2 ;
let tyv = W_CoreTypes.__generic_type_variable () in
W_TypeInfo.add_linked_object
tyv.W_Algebra.sty_desc ty2.W_Algebra.sty_desc ;
(sch, tyv))
scheme2.W_Algebra.ty_parameters in
(* Do the same thing for row variables... *)
let count_row_vars1 = ref 0 in
let count_row_vars2 = ref 0 in
let row_vars_mapping1 =
List.map
(fun sch_var ->
incr count_row_vars1 ;
(sch_var, (W_CoreTypes.__generic_row_variable ())))
scheme1.W_Algebra.row_parameters in
let row_vars_mapping2 =
List.map
(fun sch_var ->
incr count_row_vars2 ;
(sch_var, (W_CoreTypes.__generic_row_variable ())))
scheme2.W_Algebra.row_parameters in
(* Do the same thing for column variables... *)
let count_column_vars1 = ref 0 in
let count_column_vars2 = ref 0 in
let column_vars_mapping1 =
List.map
(fun sch_var ->
incr count_column_vars1 ;
(sch_var, (W_CoreTypes.__generic_column_variable ())))
scheme1.W_Algebra.column_parameters in
let column_vars_mapping2 =
List.map
(fun sch_var ->
incr count_column_vars2 ;
(sch_var, (W_CoreTypes.__generic_column_variable ())))
scheme2.W_Algebra.column_parameters in
(* Ensure that both schemes have the same number of variables. *)
if ( not (is_under_coercion && !count_ty_vars1 > !count_ty_vars2) &&
!count_ty_vars1 <> ! count_ty_vars2) ||
(not (is_under_coercion && !count_row_vars1 > !count_row_vars2) &&
!count_row_vars1 <> !count_row_vars2) ||
(not (is_under_coercion && !count_column_vars1 > !count_column_vars2) &&
!count_column_vars1 <> !count_column_vars2) then (
(* In fact, we are in the case where the 2 schemes do not have the
same number of generalized variables. *)
let n1 = !count_ty_vars1 + !count_row_vars1 + !count_column_vars1 in
let n2 = !count_ty_vars2 + !count_row_vars2 + !count_column_vars2 in
raise
(Unification_simple_type_conflict
(ty1, ty2,
{ ucd_kind = DK_forall_type_quantification_arity (n1, n2) ;
ucd_through_field = None }))
) ;
(* Now, create the instances of the type schemes. *)
let scheme1_instance =
W_SchemeGenAndInst.specialize_with_given_variables_mapping
~deep: false
ty_vars_mapping1 row_vars_mapping1 column_vars_mapping1 scheme1 in
let scheme2_instance =
W_SchemeGenAndInst.specialize_with_given_variables_mapping
~deep: false
ty_vars_mapping2 row_vars_mapping2 column_vars_mapping2 scheme2 in
(* And now, perform the unification. Because variables that were
generalized in the schemes have been copied, unification will
operate on these copies, hence preventing from dirtying the
schemes original generalized variables. *)
__unify_simple_type is_under_coercion
env seen_expansions scheme1_instance scheme2_instance ;
(* Now, ensure that the qualtified variables of both schemes were
mapped one-to-one, i.e. no collapse occurred, i.e. both scheme
were as general. Compute the checks one at time to avoid useless
computation in case one fails. This way, when unifying sums for
which we can backtrack on type error, we avoid checking bijections
if a previous bijection test failed. May be we gain a bit of time
even if lists of variables are generally not very long. *)
let fresh_gen_ty_vars1 = List.map snd ty_vars_mapping1 in
let fresh_gen_ty_vars2 = List.map snd ty_vars_mapping2 in
(* if under coercion check only for injection,
otherwise check for bijection *)
let check_for_bijection = not is_under_coercion in
let bij1 =
check_type_variables_are_in_injection check_for_bijection
fresh_gen_ty_vars1 fresh_gen_ty_vars2 in
if not bij1 then
raise
(Unification_simple_type_conflict
(ty1, ty2, { ucd_kind = DK_none ; ucd_through_field = None })) ;
let fresh_gen_row_vars1 = List.map snd row_vars_mapping1 in
let fresh_gen_row_vars2 = List.map snd row_vars_mapping2 in
let bij2 =
check_row_variables_are_in_injection check_for_bijection
fresh_gen_row_vars1 fresh_gen_row_vars2 in
if not bij2 then
raise
(Unification_simple_type_conflict
(ty1, ty2, { ucd_kind = DK_none ; ucd_through_field = None })) ;
let fresh_gen_column_vars1 = List.map snd column_vars_mapping1 in
let fresh_gen_column_vars2 = List.map snd column_vars_mapping2 in
let bij3 =
check_column_variables_are_in_injection check_for_bijection
fresh_gen_column_vars1 fresh_gen_column_vars2 in
if not bij3 then
raise
(Unification_simple_type_conflict
(ty1, ty2, { ucd_kind = DK_none ; ucd_through_field = None }))
)
| ((W_Algebra.SType_forall schm1), _)
when is_under_coercion -> (
__unify_simple_type is_under_coercion
env seen_expansions (W_SchemeGenAndInst.specialize schm1) ty2
)
| (_, _) ->
raise
(Unification_simple_type_conflict
(ty1, ty2, { ucd_kind = DK_none ; ucd_through_field = None }))
(* [TODO-REFACTOR] DOCUMENTATION. *)
and __unify_different_named_types is_under_coercion env seen_expansions ty1 ty2 nty1 nty2 =
#<If:TYPER $minlevel 11> (* <---------- DEBUG *)
OManager.printf "__unify_different_named_types@." ;
#<End> ; (* <---------- END DEBUG *)
let h_nty1 = W_CoreTypes.named_type_expr_height nty1 in
let h_nty2 = W_CoreTypes.named_type_expr_height nty2 in
if (h_nty1 < 0) && (h_nty2 < 0) then (
#<If:TYPER $minlevel 11> (* <---------- DEBUG *)
OManager.printf "Both negative: expand L & R@." ;
#<End> ; (* <---------- END DEBUG *)
(* Expand both once then unify the 2 resulting types. *)
let (ty1', seen_expansions') =
W_TypeAbbrevs.incrementally_expand_abbrev env seen_expansions ty1 in
let (ty2', seen_expansions'') =
W_TypeAbbrevs.incrementally_expand_abbrev env seen_expansions' ty2 in
if (ty1 == ty1') && (ty2 == ty2') then
raise
(Unification_simple_type_conflict
(ty1, ty2, { ucd_kind = DK_none ; ucd_through_field = None })) ;
__unify_and_return_higher_type is_under_coercion
env seen_expansions'' ty1' ty2' ty1 ty2
)
else ( (* Else 0. *)
(* Not ((h_nty1 < 0) && (h_nty2 < 0)). *)
if h_nty1 < 0 then (
#<If:TYPER $minlevel 11> (* <---------- DEBUG *)
OManager.printf "L negative: expand L@." ;
#<End> ; (* <---------- END DEBUG *)
(* Expand left once then unify expanded left and right. *)
let (ty1', seen_expansions') =
W_TypeAbbrevs.incrementally_expand_abbrev env seen_expansions ty1 in
#<If:TYPER $minlevel 11> (* <---------- DEBUG *)
OManager.printf "L after expand: %a@."
W_PrintTypes.pp_simple_type ty1' ;
#<End> ; (* <---------- END DEBUG *)
if ty1 == ty1' then
raise
(Unification_simple_type_conflict
(ty1, ty2, { ucd_kind = DK_none ; ucd_through_field = None })) ;
__unify_and_return_higher_type is_under_coercion
env seen_expansions' ty2 ty1' ty2 ty1
)
else ( (* Else 1. *)
(* (h_nty1 >= 0). *)
if h_nty2 < 0 then (
#<If:TYPER $minlevel 11> (* <---------- DEBUG *)
OManager.printf "R negative: expand R@." ;
#<End> ; (* <---------- END DEBUG *)
(* Expand right once then unify left and expanded right. *)
let (ty2', seen_expansions') =
W_TypeAbbrevs.incrementally_expand_abbrev env seen_expansions ty2 in
#<If:TYPER $minlevel 11> (* <---------- DEBUG *)
OManager.printf "R after expand: %a@."
W_PrintTypes.pp_simple_type ty2' ;
#<End> ; (* <---------- END DEBUG *)
if ty2 == ty2' then
raise
(Unification_simple_type_conflict
(ty1, ty2, { ucd_kind = DK_none ; ucd_through_field = None })) ;
__unify_and_return_higher_type is_under_coercion
env seen_expansions' ty1 ty2' ty1 ty2
)
else ( (* Else 2. *)
(* None of heights are negative. *)
if h_nty1 = h_nty2 then (
#<If:TYPER $minlevel 11> (* <---------- DEBUG *)
OManager.printf "Both positive and equal (%d): expand both@." h_nty1 ;
#<End> ; (* <---------- END DEBUG *)
(* None of heights are negative and they are equal. *)
let (ty1', seen_expansions') =
W_TypeAbbrevs.incrementally_expand_abbrev env seen_expansions ty1 in
let (ty2', seen_expansions'') =
W_TypeAbbrevs.incrementally_expand_abbrev
env seen_expansions' ty2 in
#<If:TYPER $minlevel 11> (* <---------- DEBUG *)
OManager.printf "L after expand: %a@."
W_PrintTypes.pp_simple_type ty1' ;
OManager.printf "R after expand: %a@."
W_PrintTypes.pp_simple_type ty2' ;
#<End> ; (* <---------- END DEBUG *)
if (ty1 == ty1') && (ty2 == ty2') then
raise
(Unification_simple_type_conflict
(ty1, ty2,
{ ucd_kind = DK_none ; ucd_through_field = None })) ;
__unify_and_return_higher_type is_under_coercion
env seen_expansions'' ty1' ty2' ty1 ty2
)
else ( (* Else 3. *)
(* None of heights are negative and they are not equal.
Expand highest to match lowest's level then unify left (possibly
expanded) and right (possibly expanded).
If both are at the same level: unwind them once. *)
if h_nty1 < h_nty2 then (
#<If:TYPER $minlevel 11> (* <---------- DEBUG *)
OManager.printf "L (%d) < R (%d): expand R@." h_nty1 h_nty2 ;
#<End> ; (* <---------- END DEBUG *)
(* None of heights are negative and left is lower than right.
Expand right. *)
let nb_expansion = h_nty2 - h_nty1 in
let (ty2', seen_expansions') =
W_TypeAbbrevs.expand_abbrev_n_times
nb_expansion env seen_expansions ty2 in
#<If:TYPER $minlevel 11> (* <---------- DEBUG *)
OManager.printf "R after expand: %a@."
W_PrintTypes.pp_simple_type ty2' ;
#<End> ; (* <---------- END DEBUG *)
if ty2 == ty2' then
raise
(Unification_simple_type_conflict
(ty1, ty2,
{ ucd_kind = DK_none ; ucd_through_field = None })) ;
__unify_and_return_higher_type is_under_coercion
env seen_expansions' ty1 ty2' ty1 ty2
)
else ( (* Else 4. *)
#<If:TYPER $minlevel 11> (* <---------- DEBUG *)
OManager.printf "R (%d) < L (%d): expand L@." h_nty2 h_nty1 ;
#<End> ; (* <---------- END DEBUG *)
(* None of heights are negative and left is greater than right.
Expand left. *)
let nb_expansion = h_nty1 - h_nty2 in
let (ty1', seen_expansions') =
W_TypeAbbrevs.expand_abbrev_n_times
nb_expansion env seen_expansions ty1 in
#<If:TYPER $minlevel 11> (* <---------- DEBUG *)
OManager.printf "L after expand: %a@."
W_PrintTypes.pp_simple_type ty1' ;
#<End> ; (* <---------- END DEBUG *)
if ty1 == ty1' then
raise
(Unification_simple_type_conflict
(ty1, ty2,
{ ucd_kind = DK_none ; ucd_through_field = None })) ;
__unify_and_return_higher_type is_under_coercion
env seen_expansions' ty2 ty1' ty2 ty1
) (* End of else 4. *)
) (* End of else 3. *)
) (* End of else 2. *)
) (* End of else 1. *)
) (* End of else 0. *)
(* ************************************************************************** *)
(** {b Descr}: Internal routine performing the unification of 2 row types.
Unification is performed "in place", i.e. by physically modifying the
variables on which a substitution must be applied in order to make the 2
types equal.
Differently from other unification routines, this one returns a boolean
telling if the unification was a success of if it failed due to endings
compatibility.
More in detail, there are 2 cases where unification of rows can fail.
First one, and hardest one, there exist 2 fields in common in the 2 record
types that have incompatible types. In such a case, the unification really
and definitively fails.
The second case is when common fields have compatible types but the 2 rows
can't unify because they have incompatible endings. Intuitively, this
happens when one is closed and the other is open and the list of fields of
the records are not the same. Or, this happens when both are closed and the
list of fields of the records are not the same also. In these cases,
unification is not yet definitively a failure since column unification may
take the precedence and, if it is a success, then will lead to a sum type
instead of a record type, this sum type having cases being the union of the
2 records to initially unify.
In any case (error or success), this function keeps the trace of the
modifications done by the unification. This will be the job of the initial
caller ([unify_simple_type], [unify_row_type] or [unify_column_type]) to
deal with what to do of this trace.
@raise Unification_simple_type_conflict
@raise Unification_binding_level_conflict
{b Visibility}: Not exported outside this module. *)
(* ************************************************************************** *)
and __unify_row_type is_under_coercion env seen_expansions row_ty1 row_ty2 =
(* First, get the canonical representation of the 2 row types to unify. *)
let row_ty1 = W_CoreTypes.row_type_repr row_ty1 in
let row_ty2 = W_CoreTypes.row_type_repr row_ty2 in
if row_ty1 == row_ty2 then
(* Unification is a full success since rows are physically the same. *)
true
else
match (row_ty1.W_Algebra.rt_value, row_ty2.W_Algebra.rt_value) with
| (([], W_Algebra.Closed_row), ([], W_Algebra.Closed_row)) ->
(* This corresponds to the case:
o U o
This is also a full success. *)
true
| (([], (W_Algebra.Var_row rv1)),