forked from ocaml/ocaml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
ctype.mli
475 lines (404 loc) · 20.2 KB
/
ctype.mli
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
(**************************************************************************)
(* *)
(* 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. *)
(* *)
(**************************************************************************)
(* Operations on core types *)
open Asttypes
open Types
exception Unify of Errortrace.unification_error
exception Equality of Errortrace.equality_error
exception Moregen of Errortrace.moregen_error
exception Subtype of Errortrace.Subtype.error
exception Escape of type_expr Errortrace.escape
exception Tags of label * label
exception Cannot_expand
exception Cannot_apply
exception Matches_failure of Env.t * Errortrace.unification_error
(* Raised from [matches], hence the odd name *)
exception Incompatible
(* Raised from [mcomp] *)
(* All the following wrapper functions revert to the original level,
even in case of exception. *)
val with_local_level: ?post:('a -> unit) -> (unit -> 'a) -> 'a
(* [with_local_level (fun () -> cmd) ~post] evaluates [cmd] at a
raised level.
If given, [post] is applied to the result, at the original level.
It is expected to contain only level related post-processing. *)
val with_local_level_if: bool -> (unit -> 'a) -> post:('a -> unit) -> 'a
(* Same as [with_local_level], but only raise the level conditionally.
[post] also is only called if the level is raised. *)
val with_local_level_iter: (unit -> 'a * 'b list) -> post:('b -> unit) -> 'a
(* Variant of [with_local_level], where [post] is iterated on the
returned list. *)
val with_local_level_iter_if:
bool -> (unit -> 'a * 'b list) -> post:('b -> unit) -> 'a
(* Conditional variant of [with_local_level_iter] *)
val with_level: level: int -> (unit -> 'a) -> 'a
(* [with_level ~level (fun () -> cmd)] evaluates [cmd] with
[current_level] set to [level] *)
val with_level_if: bool -> level: int -> (unit -> 'a) -> 'a
(* Conditional variant of [with_level] *)
val with_local_level_if_principal: (unit -> 'a) -> post:('a -> unit) -> 'a
val with_local_level_iter_if_principal:
(unit -> 'a * 'b list) -> post:('b -> unit) -> 'a
(* Applications of [with_local_level_if] and [with_local_level_iter_if]
to [!Clflags.principal] *)
val with_local_level_for_class: ?post:('a -> unit) -> (unit -> 'a) -> 'a
(* Variant of [with_local_level], where the current level is raised but
the nongen level is not touched *)
val with_raised_nongen_level: (unit -> 'a) -> 'a
(* Variant of [with_local_level],
raises the nongen level to the current level *)
val reset_global_level: unit -> unit
(* Reset the global level before typing an expression *)
val increase_global_level: unit -> int
val restore_global_level: int -> unit
(* This pair of functions is only used in Typetexp *)
val create_scope : unit -> int
val newty: type_desc -> type_expr
val new_scoped_ty: int -> type_desc -> type_expr
val newvar: ?name:string -> unit -> type_expr
val newvar2: ?name:string -> int -> type_expr
(* Return a fresh variable *)
val new_global_var: ?name:string -> unit -> type_expr
(* Return a fresh variable, bound at toplevel
(as type variables ['a] in type constraints). *)
val newobj: type_expr -> type_expr
val newconstr: Path.t -> type_expr list -> type_expr
val none: type_expr
(* A dummy type expression *)
val object_fields: type_expr -> type_expr
val flatten_fields:
type_expr -> (string * field_kind * type_expr) list * type_expr
(** Transform a field type into a list of pairs label-type.
The fields are sorted.
Beware of the interaction with GADTs:
Due to the introduction of object indexes for GADTs, the row variable of
an object may now be an expansible type abbreviation.
A first consequence is that [flatten_fields] will not completely flatten
the object, since the type abbreviation will not be expanded
([flatten_fields] does not receive the current environment).
Another consequence is that various functions may be called with the
expansion of this type abbreviation, which is a Tfield, e.g. during
printing.
Concrete problems have been fixed, but new bugs may appear in the
future. (Test cases were added to typing-gadts/test.ml)
*)
val associate_fields:
(string * field_kind * type_expr) list ->
(string * field_kind * type_expr) list ->
(string * field_kind * type_expr * field_kind * type_expr) list *
(string * field_kind * type_expr) list *
(string * field_kind * type_expr) list
val opened_object: type_expr -> bool
val set_object_name:
Ident.t -> type_expr list -> type_expr -> unit
val remove_object_name: type_expr -> unit
val find_cltype_for_path: Env.t -> Path.t -> type_declaration * type_expr
val sort_row_fields: (label * row_field) list -> (label * row_field) list
val merge_row_fields:
(label * row_field) list -> (label * row_field) list ->
(label * row_field) list * (label * row_field) list *
(label * row_field * row_field) list
val filter_row_fields:
bool -> (label * row_field) list -> (label * row_field) list
val generalize: type_expr -> unit
(* Generalize in-place the given type *)
val lower_contravariant: Env.t -> type_expr -> unit
(* Lower level of type variables inside contravariant branches;
to be used before generalize for expansive expressions *)
val lower_variables_only: Env.t -> int -> type_expr -> unit
(* Lower all variables to the given level *)
val enforce_current_level: Env.t -> type_expr -> unit
(* Lower whole type to !current_level *)
val generalize_structure: type_expr -> unit
(* Generalize the structure of a type, lowering variables
to !current_level *)
val generalize_class_type : class_type -> unit
(* Generalize the components of a class type *)
val generalize_class_type_structure : class_type -> unit
(* Generalize the structure of the components of a class type *)
val generalize_class_signature_spine : Env.t -> class_signature -> unit
(* Special function to generalize methods during inference *)
val correct_levels: type_expr -> type_expr
(* Returns a copy with decreasing levels *)
val limited_generalize: type_expr -> type_expr -> unit
(* Only generalize some part of the type
Make the remaining of the type non-generalizable *)
val limited_generalize_class_type: type_expr -> class_type -> unit
(* Same, but for class types *)
val fully_generic: type_expr -> bool
val check_scope_escape : Env.t -> int -> type_expr -> unit
(* [check_scope_escape env lvl ty] ensures that [ty] could be raised
to the level [lvl] without any scope escape.
Raises [Escape] otherwise *)
val instance: ?partial:bool -> type_expr -> type_expr
(* Take an instance of a type scheme *)
(* partial=None -> normal
partial=false -> newvar() for non generic subterms
partial=true -> newty2 ty.level Tvar for non generic subterms *)
val generic_instance: type_expr -> type_expr
(* Same as instance, but new nodes at generic_level *)
val instance_list: type_expr list -> type_expr list
(* Take an instance of a list of type schemes *)
val new_local_type:
?loc:Location.t ->
?manifest_and_scope:(type_expr * int) ->
type_origin -> type_declaration
module Pattern_env : sig
type t = private
{ mutable env : Env.t;
equations_scope : int;
(* scope for local type declarations *)
allow_recursive_equations : bool;
(* true iff checking counter examples *)
}
val make: Env.t -> equations_scope:int -> allow_recursive_equations:bool -> t
val copy: ?equations_scope:int -> t -> t
val set_env: t -> Env.t -> unit
end
type existential_treatment =
| Keep_existentials_flexible
| Make_existentials_abstract of Pattern_env.t
val instance_constructor: existential_treatment ->
constructor_description -> type_expr list * type_expr * type_expr list
(* Same, for a constructor. Also returns existentials. *)
val instance_parameterized_type:
?keep_names:bool ->
type_expr list -> type_expr -> type_expr list * type_expr
val instance_declaration: type_declaration -> type_declaration
val generic_instance_declaration: type_declaration -> type_declaration
(* Same as instance_declaration, but new nodes at generic_level *)
val instance_class:
type_expr list -> class_type -> type_expr list * class_type
val instance_poly:
?keep_names:bool -> fixed:bool ->
type_expr list -> type_expr -> type_expr list * type_expr
(* Take an instance of a type scheme containing free univars *)
val polyfy: Env.t -> type_expr -> type_expr list -> type_expr * bool
val instance_label:
fixed:bool ->
label_description -> type_expr list * type_expr * type_expr
(* Same, for a label *)
val apply:
?use_current_level:bool ->
Env.t -> type_expr list -> type_expr -> type_expr list -> type_expr
(* [apply [p1...pN] t [a1...aN]] applies the type function
[fun p1 ... pN -> t] to the arguments [a1...aN] and returns the
resulting instance of [t].
New nodes default to generic level except if [use_current_level] is
set to true.
Exception [Cannot_apply] is raised in case of failure. *)
val try_expand_once_opt: Env.t -> type_expr -> type_expr
val try_expand_safe_opt: Env.t -> type_expr -> type_expr
val expand_head_once: Env.t -> type_expr -> type_expr
val expand_head: Env.t -> type_expr -> type_expr
val expand_head_opt: Env.t -> type_expr -> type_expr
(** The compiler's own version of [expand_head] necessary for type-based
optimisations. *)
(** Expansion of types for error traces; lives here instead of in [Errortrace]
because the expansion machinery lives here. *)
(** Create an [Errortrace.Diff] by expanding the two types *)
val expanded_diff :
Env.t ->
got:type_expr -> expected:type_expr ->
(Errortrace.expanded_type, 'variant) Errortrace.elt
(** Create an [Errortrace.Diff] by *duplicating* the two types, so that each
one's expansion is identical to itself. Despite the name, does create
[Errortrace.expanded_type]s. *)
val unexpanded_diff :
got:type_expr -> expected:type_expr ->
(Errortrace.expanded_type, 'variant) Errortrace.elt
val full_expand: may_forget_scope:bool -> Env.t -> type_expr -> type_expr
type typedecl_extraction_result =
| Typedecl of Path.t * Path.t * type_declaration
(* The original path of the types, and the first concrete
type declaration found expanding it. *)
| Has_no_typedecl
| May_have_typedecl
val extract_concrete_typedecl:
Env.t -> type_expr -> typedecl_extraction_result
val get_new_abstract_name : Env.t -> string -> string
val unify: Env.t -> type_expr -> type_expr -> unit
(* Unify the two types given. Raise [Unify] if not possible. *)
val unify_gadt:
Pattern_env.t -> type_expr -> type_expr -> Btype.TypePairs.t
(* Unify the two types given and update the environment with the
local constraints. Raise [Unify] if not possible.
Returns the pairs of types that have been equated. *)
val unify_var: Env.t -> type_expr -> type_expr -> unit
(* Same as [unify], but allow free univars when first type
is a variable. *)
val filter_arrow: Env.t -> type_expr -> arg_label -> type_expr * type_expr
(* A special case of unification with [l:'a -> 'b]. Raises
[Filter_arrow_failed] instead of [Unify]. *)
val filter_method: Env.t -> string -> type_expr -> type_expr
(* A special case of unification (with {m : 'a; 'b}). Raises
[Filter_method_failed] instead of [Unify]. *)
val occur_in: Env.t -> type_expr -> type_expr -> bool
val deep_occur: type_expr -> type_expr -> bool
val moregeneral: Env.t -> bool -> type_expr -> type_expr -> unit
(* Check if the first type scheme is more general than the second. *)
val is_moregeneral: Env.t -> bool -> type_expr -> type_expr -> bool
val rigidify: type_expr -> type_expr list
(* "Rigidify" a type and return its type variable *)
val all_distinct_vars: Env.t -> type_expr list -> bool
(* Check those types are all distinct type variables *)
val matches: expand_error_trace:bool -> Env.t -> type_expr -> type_expr -> unit
(* Same as [moregeneral false], implemented using the two above
functions and backtracking. Ignore levels. The [expand_error_trace]
flag controls whether the error raised performs expansion; this
should almost always be [true]. *)
val does_match: Env.t -> type_expr -> type_expr -> bool
(* Same as [matches], but returns a [bool] *)
val reify_univars : Env.t -> Types.type_expr -> Types.type_expr
(* Replaces all the variables of a type by a univar. *)
(* Exceptions for special cases of unify *)
type filter_arrow_failure =
| Unification_error of Errortrace.unification_error
| Label_mismatch of
{ got : arg_label
; expected : arg_label
; expected_type : type_expr
}
| Not_a_function
exception Filter_arrow_failed of filter_arrow_failure
type filter_method_failure =
| Unification_error of Errortrace.unification_error
| Not_a_method
| Not_an_object of type_expr
exception Filter_method_failed of filter_method_failure
type class_match_failure =
CM_Virtual_class
| CM_Parameter_arity_mismatch of int * int
| CM_Type_parameter_mismatch of int * Env.t * Errortrace.equality_error
| CM_Class_type_mismatch of Env.t * class_type * class_type
| CM_Parameter_mismatch of int * Env.t * Errortrace.moregen_error
| CM_Val_type_mismatch of string * Env.t * Errortrace.comparison_error
| CM_Meth_type_mismatch of string * Env.t * Errortrace.comparison_error
| CM_Non_mutable_value of string
| CM_Non_concrete_value of string
| CM_Missing_value of string
| CM_Missing_method of string
| CM_Hide_public of string
| CM_Hide_virtual of string * string
| CM_Public_method of string
| CM_Private_method of string
| CM_Virtual_method of string
val match_class_types:
?trace:bool -> Env.t -> class_type -> class_type -> class_match_failure list
(* Check if the first class type is more general than the second. *)
val equal: Env.t -> bool -> type_expr list -> type_expr list -> unit
(* [equal env [x1...xn] tau [y1...yn] sigma]
checks whether the parameterized types
[/\x1.../\xn.tau] and [/\y1.../\yn.sigma] are equivalent. *)
val is_equal : Env.t -> bool -> type_expr list -> type_expr list -> bool
val equal_private :
Env.t -> type_expr list -> type_expr ->
type_expr list -> type_expr -> unit
(* [equal_private env t1 params1 t2 params2] checks that [t1::params1]
equals [t2::params2] but it is allowed to expand [t1] if it is a
private abbreviations. *)
val match_class_declarations:
Env.t -> type_expr list -> class_type -> type_expr list ->
class_type -> class_match_failure list
(* Check if the first class type is more general than the second. *)
val enlarge_type: Env.t -> type_expr -> type_expr * bool
(* Make a type larger, flag is true if some pruning had to be done *)
val subtype: Env.t -> type_expr -> type_expr -> unit -> unit
(* [subtype env t1 t2] checks that [t1] is a subtype of [t2].
It accumulates the constraints the type variables must
enforce and returns a function that enforces this
constraints. *)
(* Operations on class signatures *)
val new_class_signature : unit -> class_signature
val add_dummy_method : Env.t -> scope:int -> class_signature -> unit
type add_method_failure =
| Unexpected_method
| Type_mismatch of Errortrace.unification_error
exception Add_method_failed of add_method_failure
val add_method : Env.t ->
label -> private_flag -> virtual_flag -> type_expr -> class_signature -> unit
type add_instance_variable_failure =
| Mutability_mismatch of mutable_flag
| Type_mismatch of Errortrace.unification_error
exception Add_instance_variable_failed of add_instance_variable_failure
val add_instance_variable : strict:bool -> Env.t ->
label -> mutable_flag -> virtual_flag -> type_expr -> class_signature -> unit
type inherit_class_signature_failure =
| Self_type_mismatch of Errortrace.unification_error
| Method of label * add_method_failure
| Instance_variable of label * add_instance_variable_failure
exception Inherit_class_signature_failed of inherit_class_signature_failure
val inherit_class_signature : strict:bool -> Env.t ->
class_signature -> class_signature -> unit
val update_class_signature :
Env.t -> class_signature -> label list * label list
val hide_private_methods : Env.t -> class_signature -> unit
val close_class_signature : Env.t -> class_signature -> bool
exception Nondep_cannot_erase of Ident.t
val nondep_type: Env.t -> Ident.t list -> type_expr -> type_expr
(* Return a type equivalent to the given type but without
references to any of the given identifiers.
Raise [Nondep_cannot_erase id] if no such type exists because [id],
in particular, could not be erased. *)
val nondep_type_decl:
Env.t -> Ident.t list -> bool -> type_declaration -> type_declaration
(* Same for type declarations. *)
val nondep_extension_constructor:
Env.t -> Ident.t list -> extension_constructor ->
extension_constructor
(* Same for extension constructor *)
val nondep_class_declaration:
Env.t -> Ident.t list -> class_declaration -> class_declaration
(* Same for class declarations. *)
val nondep_cltype_declaration:
Env.t -> Ident.t list -> class_type_declaration -> class_type_declaration
(* Same for class type declarations. *)
(*val correct_abbrev: Env.t -> Path.t -> type_expr list -> type_expr -> unit*)
val is_contractive: Env.t -> Path.t -> bool
val normalize_type: type_expr -> unit
val nongen_vars_in_schema: Env.t -> type_expr -> Btype.TypeSet.t option
(* Return any non-generic variables in the type scheme *)
val nongen_vars_in_class_declaration:class_declaration -> Btype.TypeSet.t option
(* Return any non-generic variables in the class type.
Uses the empty environment. *)
type variable_kind = Row_variable | Type_variable
type closed_class_failure = {
free_variable: type_expr * variable_kind;
meth: string;
meth_ty: type_expr;
}
val free_variables: ?env:Env.t -> type_expr -> type_expr list
(* If env present, then check for incomplete definitions too *)
val closed_type_decl: type_declaration -> type_expr option
val closed_extension_constructor: extension_constructor -> type_expr option
val closed_class:
type_expr list -> class_signature ->
closed_class_failure option
(* Check whether all type variables are bound *)
val unalias: type_expr -> type_expr
val arity: type_expr -> int
(* Return the arity (as for curried functions) of the given type. *)
val collapse_conj_params: Env.t -> type_expr list -> unit
(* Collapse conjunctive types in class parameters *)
val get_current_level: unit -> int
val wrap_trace_gadt_instances: Env.t -> ('a -> 'b) -> 'a -> 'b
val immediacy : Env.t -> type_expr -> Type_immediacy.t
(* Stubs *)
val package_subtype :
(Env.t -> Path.t -> (Longident.t * type_expr) list ->
Path.t -> (Longident.t * type_expr) list ->
(unit,Errortrace.first_class_module) Result.t) ref
(* Raises [Incompatible] *)
val mcomp : Env.t -> type_expr -> type_expr -> unit