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
|
(**************************************************************************)
(* *)
(* OCaml *)
(* *)
(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
(* *)
(* Copyright 1996 Institut National de Recherche en Informatique et *)
(* en Automatique. *)
(* *)
(* All rights reserved. This file is distributed under the terms of *)
(* the GNU Lesser General Public License version 2.1, with the *)
(* special exception on linking described in the file LICENSE. *)
(* *)
(**************************************************************************)
(* Inclusion checks for the module language *)
open Typedtree
open Types
module Error: sig
type ('elt,'explanation) diff = {
got:'elt;
expected:'elt;
symptom:'explanation
}
type 'elt core_diff =('elt,unit) diff
type functor_arg_descr =
| Anonymous
| Named of Path.t
| Unit
| Empty_struct
(** For backward compatibility's sake, an empty struct can be implicitly
converted to an unit module. *)
type core_sigitem_symptom =
| Value_descriptions of
(Types.value_description, Includecore.value_mismatch) diff
| Type_declarations of
(Types.type_declaration, Includecore.type_mismatch) diff
| Extension_constructors of
(Types.extension_constructor,
Includecore.extension_constructor_mismatch) diff
| Class_type_declarations of
(Types.class_type_declaration, Ctype.class_match_failure list) diff
| Class_declarations of
(Types.class_declaration, Ctype.class_match_failure list) diff
type core_module_type_symptom =
| Not_an_alias
| Not_an_identifier
| Incompatible_aliases
| Abstract_module_type
| Unbound_module_path of Path.t
type module_type_symptom =
| Mt_core of core_module_type_symptom
| Signature of signature_symptom
| Functor of functor_symptom
| Invalid_module_alias of Path.t
| After_alias_expansion of module_type_diff
and module_type_diff = (Types.module_type, module_type_symptom) diff
and functor_symptom =
| Params of functor_params_diff
| Result of module_type_diff
and ('arg,'path) functor_param_symptom =
| Incompatible_params of 'arg * Types.functor_parameter
| Mismatch of module_type_diff
and arg_functor_param_symptom =
(Types.functor_parameter, Ident.t) functor_param_symptom
and functor_params_diff =
(Types.functor_parameter list * Types.module_type) core_diff
and signature_symptom = {
env: Env.t;
missings: Types.signature_item list;
incompatibles: (Ident.t * sigitem_symptom) list;
oks: (int * Typedtree.module_coercion) list;
leftovers: ((Types.signature_item as 'it) * 'it * int) list
(** signature items that could not be compared due to type divergence *)
}
and sigitem_symptom =
| Core of core_sigitem_symptom
| Module_type_declaration of
(Types.modtype_declaration, module_type_declaration_symptom) diff
| Module_type of module_type_diff
and module_type_declaration_symptom =
| Illegal_permutation of Typedtree.module_coercion
| Not_greater_than of module_type_diff
| Not_less_than of module_type_diff
| Incomparable of
{less_than:module_type_diff; greater_than: module_type_diff}
type all =
| In_Compilation_unit of (string, signature_symptom) diff
| In_Signature of signature_symptom
| In_Module_type of module_type_diff
| In_Module_type_substitution of
Ident.t * (Types.module_type,module_type_declaration_symptom) diff
| In_Type_declaration of Ident.t * core_sigitem_symptom
| In_Expansion of core_module_type_symptom
end
type explanation = Env.t * Error.all
(* Extract name, kind and ident from a signature item *)
type field_kind =
| Field_value
| Field_type
| Field_exception
| Field_typext
| Field_module
| Field_modtype
| Field_class
| Field_classtype
type field_desc = { name: string; kind: field_kind }
val kind_of_field_desc: field_desc -> string
val field_desc: field_kind -> Ident.t -> field_desc
(** Map indexed by both field types and names.
This avoids name clashes between different sorts of fields
such as values and types. *)
module FieldMap: Map.S with type key = field_desc
val item_ident_name: Types.signature_item -> Ident.t * Location.t * field_desc
val is_runtime_component: Types.signature_item -> bool
(* Typechecking *)
val modtypes:
loc:Location.t -> Env.t -> mark:bool ->
module_type -> module_type -> module_coercion
val modtypes_consistency:
loc:Location.t -> Env.t -> module_type -> module_type -> unit
val modtypes_with_shape:
shape:Shape.t -> loc:Location.t -> Env.t -> mark:bool ->
module_type -> module_type -> module_coercion * Shape.t
val strengthened_module_decl:
loc:Location.t -> aliasable:bool -> Env.t -> mark:bool ->
module_declaration -> Path.t -> module_declaration -> module_coercion
val check_modtype_inclusion :
loc:Location.t -> Env.t -> Types.module_type -> Path.t -> Types.module_type ->
explanation option
(** [check_modtype_inclusion ~loc env mty1 path1 mty2] checks that the
functor application F(M) is well typed, where mty2 is the type of
the argument of F and path1/mty1 is the path/unstrenghened type of M. *)
val check_modtype_equiv:
loc:Location.t -> Env.t -> Ident.t -> module_type -> module_type -> unit
val signatures: Env.t -> mark:bool -> signature -> signature -> module_coercion
(** Check an implementation against an interface *)
val check_implementation: Env.t -> signature -> signature -> unit
val compunit:
Env.t -> mark:bool -> string -> signature ->
string -> signature -> Shape.t -> module_coercion * Shape.t
val type_declarations:
loc:Location.t -> Env.t -> mark:bool ->
Ident.t -> type_declaration -> type_declaration -> unit
val print_coercion: Format.formatter -> module_coercion -> unit
type symptom =
Missing_field of Ident.t * Location.t * string (* kind *)
| Value_descriptions of
Ident.t * value_description * value_description
* Includecore.value_mismatch
| Type_declarations of Ident.t * type_declaration
* type_declaration * Includecore.type_mismatch
| Extension_constructors of Ident.t * extension_constructor
* extension_constructor * Includecore.extension_constructor_mismatch
| Module_types of module_type * module_type
| Modtype_infos of Ident.t * modtype_declaration * modtype_declaration
| Modtype_permutation of Types.module_type * Typedtree.module_coercion
| Interface_mismatch of string * string
| Class_type_declarations of
Ident.t * class_type_declaration * class_type_declaration *
Ctype.class_match_failure list
| Class_declarations of
Ident.t * class_declaration * class_declaration *
Ctype.class_match_failure list
| Unbound_module_path of Path.t
| Invalid_module_alias of Path.t
type pos =
| Module of Ident.t
| Modtype of Ident.t
| Arg of functor_parameter
| Body of functor_parameter
exception Error of explanation
type application_name =
| Anonymous_functor (** [(functor (_:sig end) -> struct end)(Int)] *)
| Full_application_path of Longident.t (** [F(G(X).P)(Y)] *)
| Named_leftmost_functor of Longident.t (** [F(struct end)...(...)] *)
exception Apply_error of {
loc : Location.t ;
env : Env.t ;
app_name : application_name ;
mty_f : module_type ;
args : (Error.functor_arg_descr * Types.module_type) list ;
}
val expand_module_alias: strengthen:bool -> Env.t -> Path.t -> Types.module_type
module Functor_inclusion_diff: sig
module Defs: sig
type left = Types.functor_parameter
type right = left
type eq = Typedtree.module_coercion
type diff = (Types.functor_parameter, unit) Error.functor_param_symptom
type state
end
val diff: Env.t ->
Types.functor_parameter list * Types.module_type ->
Types.functor_parameter list * Types.module_type ->
Diffing.Define(Defs).patch
end
module Functor_app_diff: sig
module Defs: sig
type left = Error.functor_arg_descr * Types.module_type
type right = Types.functor_parameter
type eq = Typedtree.module_coercion
type diff = (Error.functor_arg_descr, unit) Error.functor_param_symptom
type state
end
val diff:
Env.t ->
f:Types.module_type ->
args:(Error.functor_arg_descr * Types.module_type) list ->
Diffing.Define(Defs).patch
end
|
