Skip to content
This repository
Newer
Older
100644 450 lines (355 sloc) 14.284 kb
fccc6851 » MLstate
2011-06-21 Initial open-source release
1 (*
2 Copyright © 2011 MLstate
3
4 This file is part of OPA.
5
6 OPA is free software: you can redistribute it and/or modify it under the
7 terms of the GNU Affero General Public License, version 3, as published by
8 the Free Software Foundation.
9
10 OPA is distributed in the hope that it will be useful, but WITHOUT ANY
11 WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
12 FOR A PARTICULAR PURPOSE. See the GNU Affero General Public License for
13 more details.
14
15 You should have received a copy of the GNU Affero General Public License
16 along with OPA. If not, see <http://www.gnu.org/licenses/>.
17 *)
18 (**
19 The types recognized by any bypass standard library.
20
21 @author Mathieu Barbin
22 @author Mehdi Bouaziz
23 *)
24
25
26 (**
27 The standard types (represented by type [t])
28 are the types which can be mapped to all destination
29 targets.
30 They are the types allowed in the interface between opa code and back-end languages.
31
32 What if I need more type ?
33
34 BslTypes are involved in an auto-projection process which can have a cost for
35 complexe data-structures.
36
37 That's why we do not want to allow auto-projection for recursive types for example.
38 There is now a support via the [ServerLib] for a low level management of complexe
39 projection between arbitrary external types and opa structures.
40 This is the sence of the type constuctor {b OpaValue},
41 which is available with the syntax [opa[...]] handled by {b bslregister}.
42 *)
43
44 (** {6 Type alias} *)
45 type pos = FilePos.pos
46
47
48 (** {6 Type Variables} *)
49
50 (**
51 A type for polymorphic type variables.
52
53 [BslTypes] uses TypeVar for e.g. keeping trace of name of parameter names and design
54 For meta generation of loaders, since TypeVar would be abstract, use a let
55 intro with call to TypeVar.next, or maybe let the type t be parametrized
56 by typevariables, so that we can use int locally for code generation.
57 *)
58
59 type typevar = QmlTypeVars.TypeVar.t
60
61 module TypeVar : QmlTypeVars.GEN_VAR with type t = typevar
62 module TypeVarPrint : QmlTypeVars.VAR_PRINT with type t = typevar
63
64 module TypeVarMap : BaseMapSig.S with type key = typevar
65 module TypeVarSet : BaseSetSig.S with type elt = typevar
66
67 (**
68 Used internally and for code generation. Returns a canonical [typevar] given an [int].
69 The typevar returned is always the same for a fixed positive [int].
70 The implementation is [assert false] for negative indexes.
71 *)
72 val (~@) : int -> typevar
73
74 (**
75 Used only for code generation, for keeping trace of type variables name
76 from the implementation. Given the name of the variable in a type definition
77 or coercion, returns always the same [typevar].
78 This is dangerous because for a given string, the typevar returned is always
79 the same.
80 Not for casual user.
81 *)
82 val (~$) : string -> typevar
83
84 (** {6 Types algebra} *)
85
86 (**
87 The albebra of standard types. Some details :
88 + [External of string * t list] : the name of the type * the instance of the parameters if the type is parametric.
89 + [Fun of t list * t] is the representation for functions.
90 + [Void] For a non Nary language (Ocaml), Void is replace by an inserted [unit].
91
92 Positions: it is much more efficient to flat all the data after the constructor.
93 We do not want to use QmlLoc.label for this reason.
94 TODO: do the same in QmlAst and OpaAst.
95
96 *)
97 type t =
98 | Const of pos * QmlAst.const_ty
99 | TypeVar of pos * typevar
100 | Void of pos
101 | Bool of pos
102 | Option of pos * t
103 | OpaValue of pos * t
104 | Fun of pos * t list * t
105 | External of pos * string * t list
106
107 (** {6 GUIDELINES for matching a [t] } *)
108 (**
109 Variables, and module shorthand :
110 + [bslty] is the variable name for a value of type [t]
111 + [B] is the letter for short access (local allias)
112
113 Verbose:
114 {[
115 | Const (pos, const)
116 | TypeVar (pos, typevar)
117 | Void pos
118 | Bool pos
119 | Option (pos, t)
120 | OpaValue (pos, t)
121 | Fun (pos, args, ret)
122 | External (pos, name, params)
123 ]}
124
125 Shorter:
126 {[
127 | Const (p, c)
128 | TypeVar (p, v)
129 | Void p
130 | Bool p
131 | Option (p, t)
132 | OpaValue (p, t)
133 | Fun (p, u, v)
134 | External (p, n, vs)
135 ]}
136 *)
137
138 (** {6 Positions} *)
139 (**
140 This module follows the guidelines for error reporting :
141 + It uses [OManager] for printing localized error messages.
142 *)
143 (** *)
144 val pos : t -> pos
145 val reset_pos : t -> pos -> t
146 val merge_pos : t -> pos -> t
147
148 (** {6 Printing} *)
149 (**
150 This module follows the guidelines for printing.
151 *)
152 (** *)
153 type 't pprinter = 't LangPrint.pprinter
154
155 (**
156 Printer for [t] with the bsl syntax.
157
158 The scope of type vars is fresh for every call to pp.
159
160 Currently the syntax is not really specified, but it should
161 in a near future correspond exactly to the syntax parsed in
162 bslregister directives.
163 *)
164 val pp : t pprinter
165
166 (**
167 Same than [pp] but with a manual initialisation of the scope
168 for printing type variables.
169 *)
170 val pp_scope : scope:TypeVarPrint.scope -> t pprinter
171
172 (**
173 Search for the position of t, if is not empty print the citation,
174 if the type is a builtin, does nothing.
175 *)
176 val pp_citation : t pprinter
177
178 (**
179 Search for the position of t, if is not empty print the citation,
180 if the type is a builtin, print the type.
181 *)
182 val pp_context : t pprinter
183 val pp_multi_context : t list pprinter
184
185 (** {6 Types Manipulations and Transformations} *)
186
187 (** Ocaml does not like [with type t = t], [this_t] is just an allias to type [t] *)
188 type this_t = t
189
190 (** The instance of TRAVERSE module for the type [t] *)
191 module Walk : TraverseInterface.TRAVERSE
192 with type 'a t = this_t constraint 'a = _ * _ * _
193 and type 'a container = this_t constraint 'a = _ * _ * _
194
195 (**
196 The type for representing free type variables.
197 *)
198 type freevars = TypeVarSet.t
199
200 (** Compute the set of free type variables of a given type [t]. *)
201 val freevars : t -> freevars
202
203 (** Like [freevars] but with a non empty initial set. *)
204 val fold_freevars : freevars -> t -> freevars
205
206 (**
207 Canonical representation of types after an type variables alpha conversion.
208
209 This is used for being able to compare two types non sensible to alpha conversion,
210 or for caching, memoizing, etc...
211
212 After a normalization, 2 types equal under alphaconf will be structurally equal.
213
214 Note about the canonical representation of typevars:
215
216 Since we use [TypeVar.t] instead of [int], you cannot reset manually the
217 stamps of [TypeVar.t] but there is an API for such things, used e.g. for typeschemes
218 sharing during the Explicit Instantiation pass, this is the [get_canonical_typevar],
219 defined in [QmlTypeVars].
220 *)
221 val normalize : t -> t
222
223 (**
224 After a projection, a type is an opavalue.
225 *)
226 val opavalue : t -> t
227
228 (**
229 Once all projection have been performed,
230 the opavalue constructor does not mean
231 anything. You can use this function for
232 purging it.
233 *)
234 val purge_opavalue : t -> t
235
236 (** {6 Substitution} *)
237
238 (**
239 A common type for subtitutions.
240 *)
241 type 'a substitution = 'a TypeVarMap.t
242
243 val empty_substitution : t substitution
244
245 (**
978b7c43 » akoprow
2011-07-09 [fix] typo: occurence->occurrence, occured->occurred
246 Given a [substitution] between [typevar] and [t], replace every occurrence
fccc6851 » MLstate
2011-06-21 Initial open-source release
247 of [TypeVar i] by [substitute(i)].
248
249 The maping is the identity if [i] is [Not_found]
250 *)
251 val substitute : t substitution -> t -> t
252
253 (** {6 Comparaison, Set and Map} *)
254
255 (**
256 Compare values of type [t] :
257 if [normalize] is set to [true], the comparaison returns [0] if [a] and [b] are
258 equal under alphaconversion of type variable, which means that we perform an operation
259 of normalization before the comparaison. (can be done in line)
260
261 Otherwise ([normalize] set to [false]) the comparaison is structural, ['a <> 'b]
262 The default value is [alphaconv:false].
263 *)
264 val compare : ?normalize:bool -> t -> t -> int
265
266 (** {6 Checking} *)
267
268 (**
269 Checks if the given type is a function of second order,
270 which means that one of the arguement (or the returned type)
271 is or contains an arrow type.
272 This is used for adding parent continuation to the uncps
273 projection, in order not to loose the context.
274 *)
275 val is_second_order : t -> bool
276
277 (**
278 This function is used e.g. to check the definition of a bsl primitive
279 in opa, regarding to its external definition.
280
281 It is not a unification for checking its utilisation, it is more
282 restrictive than an unification.
283
284 It returns the [subsitution] built during the inclusion check
285 (and it takes a substitution to start with).
286
287 There is mostly 2 utilisations of this :
288
289 + compile time :
290 Example, a primitive defined as:
291 {[##register cmp : 'a, 'a -> int]}
292 and then declared in opa as:
293 {[val cmp_int = %%cmp%% : int, int -> int]}
294 This is allowed, because [int -> int -> int] is included in ['a -> 'a -> int].
295 The [expected] type should be the type of the definition,
296 and the [found] type the type of the coercion.
297 + runtime :
298 e.g. in the interpreter.
299 We perform some runtime checks before applying functions.
300 This feature is used in the interpreter to avoid seg-faults.
301 It is used essentially for debug and pedagogic support.
302 In the real life (compiled opa code), there is no such checks,
303 it is just seg-faults.
304 We are definitly not targetting performances with the interpreter.
305 We'd like rather to get documented error messages for patching part
306 and part of the framework.
307
308 <!> Warning : this function is not as complete as a correct type unification.
309 It is not meant to replace the typer, which implement already (let's hope)
310 a correct unification. This function is just use as a pedagogic issue for
311 the interpreter opatop to notify runtime errors instead of segfaulting,
312 and avoiding mispeling or mistakes in the bsl.
313
314 The {b static_strict_check:true} option is used for failing in case of magic
315 parameters. Exemple :
316 {[
317 expected:[int->int] found:['a->'a]
318 ]}
319 will fail in case of [static_strict_check:true].
320 By default, the behavior is strict. The not strict option is used by opatop.
321
322 @error if the inclusion is not possible (e.g. this would segfault at runtime)
323 *)
324 val check_inclusion :
325 ?static_strict_check:bool ->
326 t substitution -> expected:t -> found:t -> t substitution
327
328 (**
329 The same function, reseting from no substitution, and ignoring the returned subst
330 @error same than [check_inclusion]
331 *)
332 val check :
333 ?static_strict_check:bool ->
334 expected:t -> found:t -> unit
335
336 (**
337 Given a list of instance for type parameters and a value of type [t],
338 return the specialized version of the polymorphic type [t].
339
340 Types that can be specialized are :
341 + [External]
342
343 Error if the type is not a parametric type, or if the list of instance
344 is not of the same length as parameters of the type [t]
345 *)
346 val specialize : t list -> t -> t
347
348 (** {6 Binding with QmlAst.ty} *)
349
350 (** *)
351 val of_const : QmlAst.const_expr -> t
352
353 (**
354 The gamma is needed to distinguate extern-abstract types and other types.
355 This function is used as a runtime type verification (top-level) by
356 building a new bypass function
357 That checks that the coercion given is coherent with the type in the bsl
358
359 <!> Beware, the scope is local to one call to [of_ty]
360
361 TODO: QmlAst should provide some pos for ty as well
362 as OpaAst does.
363
364 @error if some incoherency in gamma, or if the type is not allowed to be
365 a bsl type.
366 *)
367 val of_ty :
368 gamma:QmlTypes.Env.t ->
369 QmlAst.ty -> t
370
371 (** *)
372 val to_ty : ?typeident:(?check:bool -> string -> QmlAst.TypeIdent.t) -> t -> QmlAst.ty
373
374 (** {6 Bypass Types Runtime Restriction} *)
375
376 (**
377 Test about specialization of parameters of parametric extern types.
378
379 Exemple:
380 {[
381 ##register foo : external[foo(void)] -> void
382 ]}
383
384 This is not allowed because there is no way to project an extern type without an explicit
385 function provided with the implementation by the user.
386
387 Type Variables of parametric extern types should be instanciated at runtime with :
388
389 + polymorphic values [('a, 'b, etc...)].
390 In this case, we have the garanty that the ocaml implementation
391 will also work with opa values (if it works for any ['a], wy not with an opa value...)
392 + opa values (not ocaml).
393 In this case, they are manipulated in the implementation with the [ServerLib] API,
394 and we know that there is no need for projection.
395 + external types
396 This means that at runtime, it will be Ocaml values manipulated from opa code,
397 and the opa code does not need to enter the implementation of the type.
398 In this case, there is no projection.
399
400 Since when we compile the bypass lib, we have no idea about the final representation
401 for opa values (even, what backend), we just trust the tag ["backend"].
402 But don't worry, others checks are performed by the back-ends during
403 the bypass projection.
404
405 This function is just a check for detecting this kind of errors sooner. (at compile
406 time of the extern library)
407
408 @warning [bsl_runtime_restriction] if the type is illicit, but the tag ["runtime"]
409 was provided
410
411 @error if the type is illicit
412 *)
413 val check_runtime_restriction :
414 BslTags.t -> (* reading tag runtime *)
415 t -> unit
416
417 (** {6 Bslregister Code Generation} *)
418
419 (**
420 Plugins and Loaders code generation, ocaml syntax.
421
422 The application [bslregister] generates some files in which types are present, as
423 meta ocaml code. It is one of the 2 supported ways of dealing with
424 plugins (cf BslMarsahlLoader, too).
425
426 To avoid conflict and too long strings, we generate [B.] as prefix of every
427 constructor. Bslregister should insert :
428 {[
429 module B = BslTypes
430 module Q = QmlAst
431 ]}
432 in the beginning of the generated files.
433 In will also help the refactoring.
434
435 This could actually be replaced by an [OcamlAst] production.
436 The probleme is that [OcamlAst] is not yet stable, and we need bsl to be operational.
437
438 This can be a possible TODO, for factorizing syntax formatting, and printing.
439 It will also help to perform some optimizations (princiappaly, string sharing)
440 and more safety : static checks, etc... but is actually not really needed.
441
442 Position:
443
444 The meta_pos will be the pos for every generated pos.
445 The scope of typevars is fresh for each call to pp_meta.
446 *)
447 (** *)
448 val meta_pos : pos
449 val pp_meta : t pprinter
450 val pp_meta_fields : (string * t) list pprinter
Something went wrong with that request. Please try again.