-
Notifications
You must be signed in to change notification settings - Fork 125
/
w_SchemeGenAndInst.ml
816 lines (745 loc) · 40.6 KB
/
w_SchemeGenAndInst.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
(*
Copyright © 2011 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
*)
(* ************************************************************************** *)
(** {b Descr}: Exception raised during generalization if a private type appears
to have its opaque name not set. See comment in [find_parameters_in_ty] for
the reasons of raising an error in this case.
{b Visibility}: Exported outside this module. *)
(* ************************************************************************** *)
exception Private_type_not_opaque of W_Algebra.simple_type
(* ************************************************************************** *)
(** {b Descr}: See .mli file for documentation.
{b Visibility}: Exported outside this module. *)
(* ************************************************************************** *)
exception Non_generalizable_type_var of
(W_Algebra.simple_type * (** The global type hosting a non-generalizable type
variable. *)
W_Algebra.simple_type) (** The non-generalizable type variable. *)
(* ************************************************************************** *)
(** {b Descr}: See .mli file for documentation.
{b Visibility}: Exported outside this module. *)
(* ************************************************************************** *)
exception Non_generalizable_row_var of
(W_Algebra.simple_type * (** The global type hosting a non-generalizable row
variable. *)
W_Algebra.simple_type) (** The non-generalizable row variable embedded
in a type. *)
(* ************************************************************************** *)
(** {b Descr}: See .mli file for documentation.
{b Visibility}: Exported outside this module. *)
(* ************************************************************************** *)
exception Non_generalizable_column_var of
(W_Algebra.simple_type * (** The global type hosting a non-generalizable
column variable. *)
W_Algebra.simple_type) (** The non-generalizable column variable embedded
in a type. *)
(* ************************************************************************** *)
(** {b Descr}:
{b Args}:
- [~forbid_non_gen_vars]: raise an error if a variable is found
non-generalizable. ATTENTION: only set to [true] in case of
generalization of a toplevel let-def (not even on modules definitions).
We can't make this test when exporting to QML because wrapping of
toplevel expressions into tuples causes the instantiation of let-defined
idents, hence causes taking an instance of their type schemes which are
taken at the toplevel binding level, causing variables to have this
binding level (i.e. 0) instead of the
[W_CoreTypes.generic_binding_level]
{b Visibility}: Not exported outside this module. *)
(* ************************************************************************** *)
let __generalize ~forbid_non_gen_vars ~extra_variables initial_ty =
let found_ty_parameters = ref ([] : W_Algebra.simple_type list) in
let found_row_parameters = ref ([] : W_Algebra.row_variable list) in
let found_column_parameters = ref ([] : W_Algebra.column_variable list) in
(* ************************************************************************ *)
(** {Descr}: Local function that walks along a simple type, harvesting its
generalized type variables.
We need to have an explicit list of the scheme's parameters. So we need
not only to mark variables as generalized, we also need to record them in
lists. Because schemes can share some variables (e.g. in the case of
mutually recursive functions), we can't say that when we encounter a
generalized variable then if it already marked as generalized then that's
because it was already seen and hence may be already in the list of the
scheme's parameter. That can also be because:
1) This variable is shared with another function whose type was already
generalized. In this case the variable will not yet be in effect in
the list of the scheme's parameters we are bulding.
2) This variable is the one of a type forall present in the type we are
generalizing. In this case, this variable *must* not be inserted in
the list the the parameters of the scheme we are bulding since it
already belongs to the type forall's scheme.
So, to know when to add a variable whose level is generic in the effective
list of the scheme's parameter, this function uses 2 kinds of list:
- [found_ty_parameters], [found_row_parameters] and
[found_column_parameters] to store the scheme's effective future
parameters. A variable is inserted if it really has to be.
- [ignored_tys], [ignored_row_vars] and [ignored_col_vars] to remind
the variables (type, row and column) that must not be considered as
parameters of the scheme even if there level is generic. *)
(* ************************************************************************ *)
let rec find_parameters_in_ty
ignored_tys ignored_row_vars ignored_col_vars ty =
(* First, get the canonical representation of the type. *)
let ty = W_CoreTypes.simple_type_repr ty in
(* Now, check if we already saw it to prevent looping. *)
match ty.W_Algebra.sty_mark with
| W_Algebra.TM_generalize_seen ->
(* Already seen, so, nothing new to explore. *)
()
| W_Algebra.TM_not_seen -> (
(* First, mark the type as seen to prevent looping. *)
ty.W_Algebra.sty_mark <- W_Algebra.TM_generalize_seen ;
(* Now, descend in the type's structure to really hunt for variables
in order to record them in the list of generalized variables. *)
match ty.W_Algebra.sty_desc with
| W_Algebra.SType_var var ->
(* Only mark (add) the variable as generalizable if it has a
binding level strictly greater than the current one and if
this variable is not already marked as generalizable (i.e. is
bound by an already existing scheme or is already marked as to
be generalized in the future type scheme we are currently
trying to create). *)
if var.W_Algebra.tv_level >
!W_CoreTypes.current_binding_level then (
if (List.memq ty ignored_tys)
||
(List.memq ty !found_ty_parameters) then
() (* Do nothing since either this variable is always
generalized for the current future scheme, hence is
already in the list of generalized variables, or this
variable is already marked as generalized because it
is under a type-forall, and then it must not appear as
a parameter of the current future type scheme. *)
else (
(* The variable has a binding level > to the current one, is
not already recorded as a parameter and is not recorded as
to be ignored. Hence, it must be marked as generalized for
the current future type scheme. So, mark now the variable
as generalized. *)
var.W_Algebra.tv_level <- W_CoreTypes.generic_binding_level ;
(* Normally, since this variable was not yet generalized, it
should not always be in the list. *)
assert (not (List.memq ty !found_ty_parameters)) ;
found_ty_parameters := ty :: !found_ty_parameters
)
)
else (
(* The variable has a level <= to the current binding level, hence
can't be generalized. If we are requested to forbid the presence
of non-generalizable type variables, then raise an error. *)
if forbid_non_gen_vars then
raise (Non_generalizable_type_var (initial_ty, ty))
)
| W_Algebra.SType_arrow (args_tys, res_ty) ->
List.iter
(find_parameters_in_ty
ignored_tys ignored_row_vars ignored_col_vars)
args_tys ;
find_parameters_in_ty
ignored_tys ignored_row_vars ignored_col_vars res_ty
| W_Algebra.SType_named named ->
(match named.W_Algebra.nst_unwinded with
| None -> ()
| Some t ->
find_parameters_in_ty
ignored_tys ignored_row_vars ignored_col_vars t) ;
List.iter
(find_parameters_in_ty
ignored_tys ignored_row_vars ignored_col_vars)
named.W_Algebra.nst_args
| W_Algebra.SType_sum_of_records sumcases_column ->
find_parameters_in_column
ignored_tys ignored_row_vars ignored_col_vars sumcases_column
| W_Algebra.SType_forall scheme ->
(* Extend our lists of type variables that must be ignored, i.e.
not considered as parameter of our scheme we will build
because they are already parameter of a type-forall present in
the current type we are generalizing. *)
let ignored_tys' =
scheme.W_Algebra.ty_parameters @ ignored_tys in
let ignored_row_vars' =
scheme.W_Algebra.row_parameters @ ignored_row_vars in
let ignored_col_vars' =
scheme.W_Algebra.column_parameters @ ignored_col_vars in
(* Recurse on the scheme's body with our extended sets of
variables to ignore. *)
find_parameters_in_ty
ignored_tys' ignored_row_vars' ignored_col_vars'
scheme.W_Algebra.body
)
| _ (* Other markers. *) -> assert false
(* ************************************************************************ *)
(** {Descr}: Local function that walks along a row type, harvesting its
generalized row variables and recursing in inner types. *)
(* ************************************************************************ *)
and find_parameters_in_row ignored_tys ignored_row_vars ignored_col_vars row =
(* Get the canonical representation of the row first. *)
let (row_fields, row_ending) =
(W_CoreTypes.row_type_repr row).W_Algebra.rt_value in
(* Recurse search in the record fields. *)
List.iter
(fun (_, ty) ->
find_parameters_in_ty ignored_tys ignored_row_vars ignored_col_vars ty)
row_fields ;
(* Search for a row-variable in the ending. *)
match row_ending with
| W_Algebra.Closed_row -> ()
| W_Algebra.Var_row var ->
(* Only mark (add) the variable as generalizable if it has a binding
level strictly greater than the current one and if this variable
is not already marked as generalizable (i.e. is bound by an
already existing scheme or is already marked as to be generalized
in the future type scheme we are currently trying to create). *)
if var.W_Algebra.rv_level > !W_CoreTypes.current_binding_level then (
if (List.memq var ignored_row_vars)
||
(List.memq var !found_row_parameters) then
() (* Do nothing since either this variable is always generalized
for the current future scheme, hence is already in the
list of generalized variables, or this variable is already
marked as generalized because it is under a type-forall,
and then it must not appear as a parameter of the current
future type scheme. *)
else (
(* The variable has a binding level > to the current one, is not
already recorded as a parameter and is not recorded as to be
ignored. Hence, it must be marked as generalized for the current
future type scheme. So, mark now the variable as generalized. *)
var.W_Algebra.rv_level <- W_CoreTypes.generic_binding_level ;
(* Normally, since this variable was not yet generalized, it
should not always be in the list. *)
assert (not (List.memq var !found_row_parameters)) ;
found_row_parameters := var :: !found_row_parameters
)
)
else (
(* The variable has a level <= to the current binding level, hence
can't be generalized. If we are requested to forbid the presence
of non-generalizable type variables, then raise an error. *)
if forbid_non_gen_vars then (
(* Create a dummy [simple_type] to embedd the row variable. *)
let row = { W_Algebra.rt_value = ([], row_ending) } in
let col =
{ W_Algebra.ct_value = ([row], W_Algebra.Closed_column) } in
let ty = {
W_Algebra.sty_desc = W_Algebra.SType_sum_of_records col ;
W_Algebra.sty_link = None ;
W_Algebra.sty_mark = W_Algebra.TM_not_seen } in
raise (Non_generalizable_row_var (initial_ty, ty))
)
)
(* ************************************************************************ *)
(** {b Descr}: Local function that walks along a column type, harvesting its
generalized column variables and recursing in inner types. *)
(* ************************************************************************ *)
and find_parameters_in_column
ignored_tys ignored_row_vars ignored_col_vars column =
(* Get the canonical representation of the column first. *)
let (col_records, col_ending) =
(W_CoreTypes.column_type_repr column).W_Algebra.ct_value in
(* Recurse search in the records forming the cases of the sum. *)
List.iter
(find_parameters_in_row ignored_tys ignored_row_vars ignored_col_vars)
col_records ;
(* Search for a column-variable in the ending. *)
match col_ending with
| W_Algebra.Closed_column -> ()
| W_Algebra.Var_column var ->
(* Only mark (add) the variable as generalizable if it has a binding
level strictly greater than the current one and if this variable
is not already marked as generalizable (i.e. is bound by an
already existing scheme or is already marked as to be generalized
in the future type scheme we are currently trying to create). *)
if var.W_Algebra.cv_level > !W_CoreTypes.current_binding_level then (
if (List.memq var ignored_col_vars)
||
(List.memq var !found_column_parameters) then
() (* Do nothing since either this variable is always generalized
for the current future scheme, hence is already in the
list of generalized variables, or this variable is already
marked as generalized because it is under a type-forall,
and then it must not appear as a parameter of the current
future type scheme. *)
else (
(* The variable has a binding level > to the current one, is not
already recorded as a parameter and is not recorded as to be
ignored. Hence, it must be marked as generalized for the current
future type scheme. So, mark now the variable as generalized. *)
var.W_Algebra.cv_level <- W_CoreTypes.generic_binding_level ;
(* Normally, since this variable was not yet generalized, it
should always not be in the list. *)
assert (not (List.memq var !found_column_parameters)) ;
found_column_parameters := var :: !found_column_parameters
)
)
else (
(* The variable has a level <= to the current binding level, hence
can't be generalized. If we are requested to forbid the presence
of non-generalizable type variables, then raise an error. *)
if forbid_non_gen_vars then (
(* Create a dummy [simple_type] to embedd the row variable. *)
let col =
{ W_Algebra.ct_value = ([], col_ending) } in
let ty = {
W_Algebra.sty_desc = W_Algebra.SType_sum_of_records col ;
W_Algebra.sty_link = None ;
W_Algebra.sty_mark = W_Algebra.TM_not_seen } in
raise (Non_generalizable_column_var (initial_ty, ty))
)
) in
(* ************************************************************************ *)
(* {b Descr}: Effective body of the generalization function [b __generalize].
It performs the hunt for generalizable types on the types passed as initial
arguments.
{b Visibility}: Not exported outside this module. *)
(* ************************************************************************ *)
let (extra_tys, extra_rows, extra_cols) = extra_variables in
(* Attention: start finding first in the parameters we may have been given.
This ensures that is there are some parameters corresponding to a
pre-existing scheme (in case of generalization via [generalize2]), then
they will be looked-up first, in there order of apparition, hence this
will preserve the order of these parameters in the scheme we generate
here. *)
List.iter (find_parameters_in_ty [] [] []) extra_tys ;
List.iter (find_parameters_in_row [] [] []) extra_rows ;
List.iter (find_parameters_in_column [] [] []) extra_cols ;
find_parameters_in_ty [] [] [] initial_ty ;
(* Don't forget to reset the markers in the type we generalized. *)
W_CoreTypes.cleanup_simple_type initial_ty ;
List.iter W_CoreTypes.cleanup_simple_type extra_tys ;
List.iter W_CoreTypes.cleanup_row_type extra_rows ;
List.iter W_CoreTypes.cleanup_column_type extra_cols ;
(* Reverse the lists of seen variables so that the first ones encountered
appear first in the list.
This is twofold:
1) It makes the correspondence more direct between the order in the list
and the order the variables are seen, hence ease debug inspection.
2) Most important, it guaranties that when generalization is invoked from
[__generalize2], the variables given in the [extra_tys] appears in the
order of this list, which is very important to ensure that the obtained
scheme has its variables in the same order than the original QML scheme
manipulated during this generalization. In effect, [__generalize2] is
used to create a [type_scheme] from a QML scheme. This latter already
exists and appears in the program, with its own already decided order
of generalized type variables. If, when we create our [type_scheme] we
do not respect this order, when later making the variables of these 2
view of the scheme, we will confuse parameters of the scheme, hence
lead to incompatible type instances (parameters instantiated with
arguments in a wrong order). An example:
type t ('a, 'b) = ('a, 'b) in QML
type ('b, 'a) t = ('a, 'b) in the typechecker where the scheme of the
QML body has right be converted correctly, but seen generalized
variables being registered in reverse order, the prenex list shows
them in reverse order, hence leading to an incorrect scheme in which
the parameters are reversed ! *)
{ W_Algebra.ty_parameters = List.rev !found_ty_parameters ;
W_Algebra.row_parameters = List.rev !found_row_parameters ;
W_Algebra.column_parameters = List.rev !found_column_parameters ;
W_Algebra.body = initial_ty }
(* ************************************************************************** *)
(** {b Visibility}: Exported outside this module. *)
(* ************************************************************************** *)
let generalize ~forbid_non_gen_vars ty =
try
let sch =
__generalize ~forbid_non_gen_vars ~extra_variables: ([], [], []) ty in
W_CoreTypes.cleanup_simple_type ty ;
sch
with killed_by ->
(* In any case, even if an error occurred, don't forget to cleanuo the type
otherwise printing routines will encounter unexpected remaining
markers. *)
W_CoreTypes.cleanup_simple_type ty ;
raise killed_by
(* ************************************************************************** *)
(** {b Visibility}: Exported outside this module. *)
(* ************************************************************************** *)
let generalize2 ~extra_variables ty =
__generalize ~forbid_non_gen_vars: false ~extra_variables ty
(* ************************************************************************** *)
(** {b Descr}: Creates a type scheme whose body is the type passed as
argument in which we do not perform any generalization. Hence, the type
scheme is trivially non-polymorphic.
This is very useful to insert the scheme of a recursive function in the
typing environment used to type-check the body of this function.
{b Visibility}: Exported outside this module. *)
(* ************************************************************************** *)
let trivial_scheme ty =
{ W_Algebra.ty_parameters = [] ;
W_Algebra.row_parameters = [] ;
W_Algebra.column_parameters = [] ;
W_Algebra.body = ty
}
(* [TODO-REFACTOR] EST-CE QUE deep DOIT RESSORTIR VISIBLE AU NIVEAU DES
ROUTINES DE SPÉCIALISATION OU EST-CE QUE L'ON DEVRAIT PLUTÔT AVOIR DES
ROUTINES DE "SUBSTITUTIONS" QUI SERAIENT DÉDIÉE AU COMPORTEMENT DE QUAND
deep = true ? *)
let (__specialize, specialize_with_given_variables_mapping) =
(* Internal recursive copy of a type scheme replacing its generalized
variables by their associated new fresh type variables found in the above
mapping. *)
let rec copy_simple_type ~deep ty =
(* 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_copy_copied_as aliased_as ->
(* Type was already seen. Its copy is recorded here. *)
aliased_as
| W_Algebra.TM_not_seen -> (
(* We must say we already saw ourself before recursing on the type
structure, otherwise we can loop. Because we don't still know
our real value, we will refer ourself with a type variable.
Then when copy is finished, we'll put a link between this
variable and the real result found for the copy. *)
let tmp_ty = W_CoreTypes.type_variable () in
ty.W_Algebra.sty_mark <- W_Algebra.TM_copy_copied_as tmp_ty ;
(* And now let's recurse to get the copy of our description. *)
let copied_ty =
(match ty.W_Algebra.sty_desc with
| W_Algebra.SType_var var ->
(* If the type variable is generalized, then we make a copy
of it else, we return the type itself. Variables that
are generalized but must not be instantiated because
under a type-forall's scheme are pre-marked, so are caught
above when inspecting the marker of the hosting type. *)
if var.W_Algebra.tv_level =
W_CoreTypes.generic_binding_level then (
(* Create a fresh QML variable but keep its base name. *)
let qml_var' =
QmlTypeVars.TypeVar.refresh var.W_Algebra.tv_qml in
let var' = {
W_Algebra.tv_level = !W_CoreTypes.current_binding_level ;
W_Algebra.tv_qml = qml_var' ;
W_Algebra.tv_debug_count = -1 } in
{ W_Algebra.sty_desc = W_Algebra.SType_var var' ;
W_Algebra.sty_link = None ;
W_Algebra.sty_mark = W_Algebra.TM_not_seen }
)
else ty
| W_Algebra.SType_arrow (args_tys, res_ty) ->
(* Simply perform a structural recursion to inductively
copy all the type's sub-terms. *)
let args_tys' = List.map (copy_simple_type ~deep) args_tys in
let res_ty' = copy_simple_type ~deep res_ty in
W_CoreTypes.type_arrow args_tys' res_ty'
| W_Algebra.SType_named { W_Algebra.nst_name = name ;
W_Algebra.nst_abbrev_height = height ;
W_Algebra.nst_args = args ;
W_Algebra.nst_unwinded = manifest} ->
(* Unwounded view of the type must also be copied if we are
taking an instance with deep copy. This is the case when
dealing with type definitions' scheme elaboration and
type abbrevs expansion. *)
let manifest' =
if deep then
(match manifest with
| None -> None
| Some t -> Some (copy_simple_type ~deep t))
else None in
(* Finally, build a type description of the named type. *)
W_CoreTypes.type_named
name height (List.map (copy_simple_type ~deep) args) manifest'
| W_Algebra.SType_sum_of_records sumcases_column ->
let sumcases_column' = copy_column_type ~deep sumcases_column in
{ W_Algebra.sty_desc =
W_Algebra.SType_sum_of_records sumcases_column' ;
W_Algebra.sty_link = None ;
W_Algebra.sty_mark = W_Algebra.TM_not_seen }
| W_Algebra.SType_forall scheme ->
(* Specialization is not deep. This means when taking a copy
of a type scheme, we **do not** take a copy of its
generalized variables. To prevent these generalized
variables from being instantiated by fresh ones, we bypass
the regular generalized-stuff-leads-to-fresh by entering
them as pre-mapped in the "mapping", pre-aliased directly
to themselves. *)
List.iter
(fun sch_ty_var ->
let sch_ty_var =
W_CoreTypes.simple_type_repr sch_ty_var in
sch_ty_var.W_Algebra.sty_mark <-
W_Algebra.TM_copy_copied_as sch_ty_var)
scheme.W_Algebra.ty_parameters ;
List.iter
(fun row_var ->
row_var.W_Algebra.rv_mark <-
W_Algebra.VM_copy_copied_as row_var)
scheme.W_Algebra.row_parameters ;
List.iter
(fun col_var ->
col_var.W_Algebra.cv_mark <-
W_Algebra.VM_copy_copied_as col_var)
scheme.W_Algebra.column_parameters ;
let body' = copy_simple_type ~deep scheme.W_Algebra.body in
{ W_Algebra.sty_desc =
W_Algebra.SType_forall
{ scheme with W_Algebra.body = body' } ;
W_Algebra.sty_link = None ;
W_Algebra.sty_mark = W_Algebra.TM_not_seen }) in
(* And now add the famous link. *)
tmp_ty.W_Algebra.sty_link <- Some copied_ty ;
(* Return our copy. *)
copied_ty
)
| _ (* Other markers. *) -> assert false
and copy_row_type ~deep row =
(* First, get the canonical representation of the row. *)
let (row_fields, row_ending) =
(W_CoreTypes.row_type_repr row).W_Algebra.rt_value in
let row_fields' =
List.map
(fun (label, ty) -> (label, copy_simple_type ~deep ty))
row_fields in
let row_ending' =
(match row_ending with
| W_Algebra.Var_row var -> (
match var.W_Algebra.rv_mark with
| W_Algebra.VM_copy_copied_as aliased_as ->
(* Already seen hence return what it is already known to be. *)
W_Algebra.Var_row aliased_as
| W_Algebra.VM_not_seen ->
(* As for [simple_type]s, if the variable is generalized then we
make a copy of it, otherwise we return itself. *)
let var' =
if var.W_Algebra.rv_level =
W_CoreTypes.generic_binding_level then
W_CoreTypes.__row_variable ()
else (
(* Variable is not generalized return the variable
itself, i.e. the original row ending. *)
var
) in
var.W_Algebra.rv_mark <- W_Algebra.VM_copy_copied_as var' ;
W_Algebra.Var_row var'
| _ (* Other markers. *) -> assert false)
| W_Algebra.Closed_row -> row_ending) in
(* Finally, rebuild the copy of the row. *)
{ W_Algebra.rt_value = (row_fields', row_ending') }
and copy_column_type ~deep column =
(* First, get the canonical representation of the column. *)
let (col_records, col_ending) =
(W_CoreTypes.column_type_repr column).W_Algebra.ct_value in
let col_records' = List.map (copy_row_type ~deep) col_records in
let col_ending' =
(match col_ending with
| W_Algebra.Var_column var -> (
match var.W_Algebra.cv_mark with
| W_Algebra.VM_copy_copied_as aliased_as ->
(* Already seen hence return what it is already known to be. *)
W_Algebra.Var_column aliased_as
| W_Algebra.VM_not_seen ->
(* As for [simple_type]s, if the variable is generalized then we
make a copy of it, otherwise we return itself. *)
let var' =
if var.W_Algebra.cv_level =
W_CoreTypes.generic_binding_level then
W_CoreTypes.__column_variable ()
else (
(* Variable is not generalized, hence return the
variable itself, i.e. the original column ending. *)
var
) in
var.W_Algebra.cv_mark <- W_Algebra.VM_copy_copied_as var' ;
W_Algebra.Var_column var'
| _ (* Other markers. *) -> assert false)
| W_Algebra.Closed_column -> col_ending) in
(* Finally, rebuild the copy of the column. *)
{ W_Algebra.ct_value = (col_records', col_ending') } in
(
(* ********************************************************************** *)
(** {b Descr}: Effective body of the instantiation function [__specialize].
This function instantiate a type scheme, i.e. makes a copy of its body
replacing its generalized variables by fresh ones. Hence, from a type
scheme, this function generates a fresh type in which polymorphic parts
of the scheme are fresh.
By the way, it returns the lists of fresh variables created to
instantiate the generic ones found in the scheme.
{b Visibility}: Not exported outside this module. *)
(* ********************************************************************** *)
(fun ~deep scheme ->
(* First we need to build the mappings from the generalized variables of
the scheme to new and fresh variables that will be used in the copy
(i.e. in the instance) of the type represented by the scheme's
body.
These mappings are simulated by directly setting the field [sty_mark]
of the generalized variables to fresh variables created here. Hence
when descending on the type to generalize, we will have the impress
that we already saw generalized variables, hence return what they are
aliased to, i.e. the fresh ones we will create here. *)
let fresh_ty_vars =
List.map
(fun ty_being_var ->
match ty_being_var.W_Algebra.sty_desc with
| W_Algebra.SType_var _ ->
(* Since we instantiate a scheme, no need to keep identity of
the variables of the scheme since they are only meaningful
in the scope of the definition having this scheme.
Avoids "inheriting" variable names from other functions. *)
let fresh_qml_ty_var = QmlTypeVars.TypeVar.next () in
let fresh_ty_var =
W_CoreTypes.__type_variable_with_public_identity
fresh_qml_ty_var in
ty_being_var.W_Algebra.sty_mark <-
W_Algebra.TM_copy_copied_as fresh_ty_var ;
fresh_ty_var
| _ ->
(* By construction, types representing variables should always
be of the form [SType_var], otherwise there's something
buggy around. *)
assert false)
scheme.W_Algebra.ty_parameters in
(* Do the same thing for row variables. *)
let fresh_row_vars =
List.map
(fun row_var ->
(* Same remark than abovefor type variables about why using
[next] instead of [refresh]. *)
let fresh_qml_row_var = QmlTypeVars.RowVar.next () in
let fresh_row_var =
W_CoreTypes.__row_variable_with_public_identity
fresh_qml_row_var in
row_var.W_Algebra.rv_mark <-
W_Algebra.VM_copy_copied_as fresh_row_var ;
(* Return the fresh row variable used to instantiate the
generalized one directly as a [row_type]. This will be more
convenient for further manipulations instead of each time
having to embed it in a [row_type]. *)
{ W_Algebra.rt_value = ([], W_Algebra.Var_row fresh_row_var) })
scheme.W_Algebra.row_parameters in
(* Do the same thing for column variables. *)
let fresh_col_vars =
List.map
(fun col_var ->
(* Same remark than abovefor type variables about why using
[next] instead of [refresh]. *)
let fresh_qml_col_var = QmlTypeVars.ColVar.next () in
let fresh_col_var =
W_CoreTypes.__column_variable_with_public_identity
fresh_qml_col_var in
col_var.W_Algebra.cv_mark <-
W_Algebra.VM_copy_copied_as fresh_col_var ;
(* Return the fresh column variable used to instantiate the
generalized one directly as a [column_type]. *)
{ W_Algebra.ct_value = ([], W_Algebra.Var_column fresh_col_var) })
scheme.W_Algebra.column_parameters in
(* Now, copy the scheme body to instantiate it. *)
let instance = copy_simple_type ~deep scheme.W_Algebra.body in
(* Don't forget to cleanup the body of the scheme. *)
W_CoreTypes.cleanup_simple_type scheme.W_Algebra.body ;
(* Also do on its parameters in case they do not appear in the body. *)
List.iter
(fun ty_var ->
ty_var.W_Algebra.sty_mark <- W_Algebra.TM_not_seen)
scheme.W_Algebra.ty_parameters ;
List.iter
(fun row_var -> row_var.W_Algebra.rv_mark <- W_Algebra.VM_not_seen)
scheme.W_Algebra.row_parameters ;
List.iter
(fun col_var -> col_var.W_Algebra.cv_mark <- W_Algebra.VM_not_seen)
scheme.W_Algebra.column_parameters ;
((fresh_ty_vars, fresh_row_vars, fresh_col_vars), instance))
,
(* ********************************************************************** *)
(** {b Descr}: Effective body of the instantiation function
[specialize_with_given_variables_mapping].
This function instantiate a type scheme, i.e. makes a copy of its body
replacing its generalized variables. Instead of [specialize] that
replaces generalized variables by fresh ones, this function directly
replaces them by types provided in the mappings passed as arguments.
This is especially required when unifying types-forall since we must
unify their body in which original generalized variables have been
replaced by custom *also* generalized variables we manually create
beforehand. *)
(* ********************************************************************** *)
(fun ~deep ty_vars_mapping row_vars_mapping column_vars_mapping scheme ->
(* Like above in [specialize], we must simulate the mapping of
generalized variables to what they must be instantiated. Since, we
receive these mapping from outside, we walk along them setting, for
each variable to map they contain, the marker as "already copied as"
the stuff on what to map the variable to. *)
List.iter
(fun (ty_var, mapped_to) ->
ty_var.W_Algebra.sty_mark <- W_Algebra.TM_copy_copied_as mapped_to)
ty_vars_mapping ;
List.iter
(fun (row_var, mapped_to) ->
row_var.W_Algebra.rv_mark <- W_Algebra.VM_copy_copied_as mapped_to)
row_vars_mapping ;
List.iter
(fun (col_var, mapped_to) ->
col_var.W_Algebra.cv_mark <- W_Algebra.VM_copy_copied_as mapped_to)
column_vars_mapping ;
let instance = copy_simple_type ~deep scheme.W_Algebra.body in
(* Don't forget to cleanup the body of the scheme. *)
W_CoreTypes.cleanup_simple_type scheme.W_Algebra.body ;
(* Also do on its parameters in case they do not appear in the body. *)
List.iter
(fun (ty_var, _) -> ty_var.W_Algebra.sty_mark <- W_Algebra.TM_not_seen)
ty_vars_mapping ;
List.iter
(fun (row_var, _) ->
row_var.W_Algebra.rv_mark <- W_Algebra.VM_not_seen)
row_vars_mapping ;
List.iter
(fun (col_var, _) ->
col_var.W_Algebra.cv_mark <- W_Algebra.VM_not_seen)
column_vars_mapping ;
(* Finally, return the type that is the instantiation of the scheme. *)
instance)
)
let specialize scheme = snd (__specialize ~deep: false scheme)
let specialize2 ~deep scheme = __specialize ~deep scheme
(* ************************************************************************** *)
(** {b Descr}: Creates a type-forall surrounding the type received as argument
if this type has a non trivial type scheme. In other words, this function
tries to generalize the type received as argument. If the resulting scheme
contains variables then a type-forall is created otherwise the initially
passed type is returned as-is.
{b Visibility}: Exported outside this module. *)
(* ************************************************************************** *)
let type_forall ty =
let scheme = generalize ~forbid_non_gen_vars: false ty in
(* Really embed the type inside a forall-type if it contains generalized
variables. *)
if scheme.W_Algebra.ty_parameters <> [] ||
scheme.W_Algebra.row_parameters <> [] ||
scheme.W_Algebra.column_parameters <> [] then
{ W_Algebra.sty_desc = W_Algebra.SType_forall scheme ;
W_Algebra.sty_link = None ;
W_Algebra.sty_mark = W_Algebra.TM_not_seen }
else ty
let get_type_forall_scheme ty =
match (W_CoreTypes.simple_type_repr ty).W_Algebra.sty_desc with
| W_Algebra.SType_forall sch -> Some sch
| _ -> None
(* ************************************************************************** *)
(** {b Descr}: Performs the implicit instantiation of types forall. If the type
received as argument is a type forall, this function creates and returns an
instance of the scheme of this type forall. Otherwise, this function returns
the initial type untouched (more accurately, returns the canonical
representation of the initial type, hence the returned type, even if
semantically identical to the initial one, car by physically different).
By the way, the instantiated scheme is returned as an option. If the type
was not a type forall, then there was no scheme to instantiate, then [None]
is returned.
{b Visibility}: Exported outside this module. *)
(* ************************************************************************** *)
let automatically_instantiate_if_forall ty =
let ty = W_CoreTypes.simple_type_repr ty in
match ty.W_Algebra.sty_desc with
| W_Algebra.SType_forall scheme -> ((specialize scheme), (Some scheme))
| _ -> (ty, None)