lustrec / src / typing.ml @ f4cba4b8
History | View | Annotate | Download (39.7 KB)
1 |
(********************************************************************) |
---|---|
2 |
(* *) |
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT - LIFL *) |
5 |
(* *) |
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
7 |
(* under the terms of the GNU Lesser General Public License *) |
8 |
(* version 2.1. *) |
9 |
(* *) |
10 |
(* This file was originally from the Prelude compiler *) |
11 |
(* *) |
12 |
(********************************************************************) |
13 |
|
14 |
(** Main typing module. Classic inference algorithm with destructive |
15 |
unification. *) |
16 |
|
17 |
let debug fmt args = () (* Format.eprintf "%a" *) |
18 |
(* Though it shares similarities with the clock calculus module, no code |
19 |
is shared. Simple environments, very limited identifier scoping, no |
20 |
identifier redefinition allowed. *) |
21 |
|
22 |
open Utils |
23 |
(* Yes, opening both modules is dirty as some type names will be |
24 |
overwritten, yet this makes notations far lighter.*) |
25 |
open Lustre_types |
26 |
open Corelang |
27 |
open Format |
28 |
|
29 |
|
30 |
(* TODO general remark: except in the add_vdecl, it seems to me that |
31 |
all the pairs (env, vd_env) should be replace with just env, since |
32 |
vd_env is never used and the env element is always extract with a |
33 |
fst *) |
34 |
|
35 |
|
36 |
module type EXPR_TYPE_HUB = |
37 |
sig |
38 |
type type_expr |
39 |
val import: Types.Main.type_expr -> type_expr |
40 |
val export: type_expr -> Types.Main.type_expr |
41 |
end |
42 |
|
43 |
module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.type_expr) = |
44 |
struct |
45 |
|
46 |
module TP = Type_predef.Make (T) |
47 |
include TP |
48 |
|
49 |
let pp_typing_env fmt env = |
50 |
Env.pp_env print_ty fmt env |
51 |
|
52 |
(****************************************************************) |
53 |
(* Generic functions: occurs, instantiate and generalize *) |
54 |
(****************************************************************) |
55 |
|
56 |
(** [occurs tvar ty] returns true if the type variable [tvar] |
57 |
occurs in type [ty]. False otherwise. *) |
58 |
let rec occurs tvar ty = |
59 |
let ty = repr ty in |
60 |
match type_desc ty with |
61 |
| Tvar -> ty=tvar |
62 |
| Tarrow (t1, t2) -> |
63 |
(occurs tvar t1) || (occurs tvar t2) |
64 |
| Ttuple tl -> |
65 |
List.exists (occurs tvar) tl |
66 |
| Tstruct fl -> |
67 |
List.exists (fun (f, t) -> occurs tvar t) fl |
68 |
| Tarray (_, t) |
69 |
| Tstatic (_, t) |
70 |
| Tclock t |
71 |
| Tlink t -> occurs tvar t |
72 |
| Tenum _ | Tconst _ | Tunivar | Tbasic _ -> false |
73 |
|
74 |
(** Promote monomorphic type variables to polymorphic type |
75 |
variables. *) |
76 |
(* Generalize by side-effects *) |
77 |
let rec generalize ty = |
78 |
match type_desc ty with |
79 |
| Tvar -> |
80 |
(* No scopes, always generalize *) |
81 |
ty.tdesc <- Tunivar |
82 |
| Tarrow (t1,t2) -> |
83 |
generalize t1; generalize t2 |
84 |
| Ttuple tl -> |
85 |
List.iter generalize tl |
86 |
| Tstruct fl -> |
87 |
List.iter (fun (f, t) -> generalize t) fl |
88 |
| Tstatic (d, t) |
89 |
| Tarray (d, t) -> Dimension.generalize d; generalize t |
90 |
| Tclock t |
91 |
| Tlink t -> |
92 |
generalize t |
93 |
| Tenum _ | Tconst _ | Tunivar | Tbasic _ -> () |
94 |
|
95 |
(** Downgrade polymorphic type variables to monomorphic type |
96 |
variables *) |
97 |
let rec instantiate inst_vars inst_dim_vars ty = |
98 |
let ty = repr ty in |
99 |
match ty.tdesc with |
100 |
| Tenum _ | Tconst _ | Tvar | Tbasic _ -> ty |
101 |
| Tarrow (t1,t2) -> |
102 |
{ty with tdesc = |
103 |
Tarrow ((instantiate inst_vars inst_dim_vars t1), (instantiate inst_vars inst_dim_vars t2))} |
104 |
| Ttuple tlist -> |
105 |
{ty with tdesc = Ttuple (List.map (instantiate inst_vars inst_dim_vars) tlist)} |
106 |
| Tstruct flist -> |
107 |
{ty with tdesc = Tstruct (List.map (fun (f, t) -> (f, instantiate inst_vars inst_dim_vars t)) flist)} |
108 |
| Tclock t -> |
109 |
{ty with tdesc = Tclock (instantiate inst_vars inst_dim_vars t)} |
110 |
| Tstatic (d, t) -> |
111 |
{ty with tdesc = Tstatic (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)} |
112 |
| Tarray (d, t) -> |
113 |
{ty with tdesc = Tarray (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)} |
114 |
| Tlink t -> |
115 |
(* should not happen *) |
116 |
{ty with tdesc = Tlink (instantiate inst_vars inst_dim_vars t)} |
117 |
| Tunivar -> |
118 |
try |
119 |
List.assoc ty.tid !inst_vars |
120 |
with Not_found -> |
121 |
let var = new_var () in |
122 |
inst_vars := (ty.tid, var)::!inst_vars; |
123 |
var |
124 |
|
125 |
|
126 |
|
127 |
let basic_coretype_type t = |
128 |
if is_real_type t then Tydec_real else |
129 |
if is_int_type t then Tydec_int else |
130 |
if is_bool_type t then Tydec_bool else |
131 |
assert false |
132 |
|
133 |
(* [type_coretype cty] types the type declaration [cty] *) |
134 |
let rec type_coretype type_dim cty = |
135 |
match (*get_repr_type*) cty with |
136 |
| Tydec_any -> new_var () |
137 |
| Tydec_int -> type_int |
138 |
| Tydec_real -> (* Type_predef. *)type_real |
139 |
(* | Tydec_float -> Type_predef.type_real *) |
140 |
| Tydec_bool -> (* Type_predef. *)type_bool |
141 |
| Tydec_clock ty -> (* Type_predef. *)type_clock (type_coretype type_dim ty) |
142 |
| Tydec_const c -> (* Type_predef. *)type_const c |
143 |
| Tydec_enum tl -> (* Type_predef. *)type_enum tl |
144 |
| Tydec_struct fl -> (* Type_predef. *)type_struct (List.map (fun (f, ty) -> (f, type_coretype type_dim ty)) fl) |
145 |
| Tydec_array (d, ty) -> |
146 |
begin |
147 |
let d = Dimension.copy (ref []) d in |
148 |
type_dim d; |
149 |
(* Type_predef. *)type_array d (type_coretype type_dim ty) |
150 |
end |
151 |
|
152 |
(* [coretype_type] is the reciprocal of [type_typecore] *) |
153 |
let rec coretype_type ty = |
154 |
match (repr ty).tdesc with |
155 |
| Tvar -> Tydec_any |
156 |
| Tbasic _ -> basic_coretype_type ty |
157 |
| Tconst c -> Tydec_const c |
158 |
| Tclock t -> Tydec_clock (coretype_type t) |
159 |
| Tenum tl -> Tydec_enum tl |
160 |
| Tstruct fl -> Tydec_struct (List.map (fun (f, t) -> (f, coretype_type t)) fl) |
161 |
| Tarray (d, t) -> Tydec_array (d, coretype_type t) |
162 |
| Tstatic (_, t) -> coretype_type t |
163 |
| _ -> assert false |
164 |
|
165 |
let get_coretype_definition tname = |
166 |
try |
167 |
let top = Hashtbl.find type_table (Tydec_const tname) in |
168 |
match top.top_decl_desc with |
169 |
| TypeDef tdef -> tdef.tydef_desc |
170 |
| _ -> assert false |
171 |
with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname)) |
172 |
|
173 |
let get_type_definition tname = |
174 |
type_coretype (fun d -> ()) (get_coretype_definition tname) |
175 |
|
176 |
(* Equality on ground types only *) |
177 |
(* Should be used between local variables which must have a ground type *) |
178 |
let rec eq_ground t1 t2 = |
179 |
let t1 = repr t1 in |
180 |
let t2 = repr t2 in |
181 |
t1==t2 || |
182 |
match t1.tdesc, t2.tdesc with |
183 |
| Tbasic t1, Tbasic t2 when t1 == t2 -> true |
184 |
| Tenum tl, Tenum tl' when tl == tl' -> true |
185 |
| Ttuple tl, Ttuple tl' when List.length tl = List.length tl' -> List.for_all2 eq_ground tl tl' |
186 |
| Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' -> List.for_all2 (fun (_, t) (_, t') -> eq_ground t t') fl fl' |
187 |
| (Tconst t, _) -> |
188 |
let def_t = get_type_definition t in |
189 |
eq_ground def_t t2 |
190 |
| (_, Tconst t) -> |
191 |
let def_t = get_type_definition t in |
192 |
eq_ground t1 def_t |
193 |
| Tarrow (t1,t2), Tarrow (t1',t2') -> eq_ground t1 t1' && eq_ground t2 t2' |
194 |
| Tclock t1', Tclock t2' -> eq_ground t1' t2' |
195 |
| Tstatic (e1, t1'), Tstatic (e2, t2') |
196 |
| Tarray (e1, t1'), Tarray (e2, t2') -> Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2' |
197 |
| _ -> false |
198 |
|
199 |
(** [unify t1 t2] unifies types [t1] and [t2] |
200 |
using standard destructive unification. |
201 |
Raises [Unify (t1,t2)] if the types are not unifiable. |
202 |
[t1] is a expected/formal/spec type, [t2] is a computed/real/implem type, |
203 |
so in case of unification error: expected type [t1], got type [t2]. |
204 |
If [sub]-typing is allowed, [t2] may be a subtype of [t1]. |
205 |
If [semi] unification is required, |
206 |
[t1] should furthermore be an instance of [t2] |
207 |
and constants are handled differently.*) |
208 |
let unify ?(sub=false) ?(semi=false) t1 t2 = |
209 |
let rec unif t1 t2 = |
210 |
let t1 = repr t1 in |
211 |
let t2 = repr t2 in |
212 |
if t1==t2 then |
213 |
() |
214 |
else |
215 |
match t1.tdesc,t2.tdesc with |
216 |
(* strictly subtyping cases first *) |
217 |
| _ , Tclock t2 when sub && (get_clock_base_type t1 = None) -> |
218 |
unif t1 t2 |
219 |
| _ , Tstatic (d2, t2) when sub && (get_static_value t1 = None) -> |
220 |
unif t1 t2 |
221 |
(* This case is not mandatory but will keep "older" types *) |
222 |
| Tvar, Tvar -> |
223 |
if t1.tid < t2.tid then |
224 |
t2.tdesc <- Tlink t1 |
225 |
else |
226 |
t1.tdesc <- Tlink t2 |
227 |
| Tvar, _ when (not semi) && (not (occurs t1 t2)) -> |
228 |
t1.tdesc <- Tlink t2 |
229 |
| _, Tvar when (not (occurs t2 t1)) -> |
230 |
t2.tdesc <- Tlink t1 |
231 |
| Tarrow (t1,t2), Tarrow (t1',t2') -> |
232 |
begin |
233 |
unif t2 t2'; |
234 |
unif t1' t1 |
235 |
end |
236 |
| Ttuple tl, Ttuple tl' when List.length tl = List.length tl' -> |
237 |
List.iter2 unif tl tl' |
238 |
| Ttuple [t1] , _ -> unif t1 t2 |
239 |
| _ , Ttuple [t2] -> unif t1 t2 |
240 |
| Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' -> |
241 |
List.iter2 (fun (_, t) (_, t') -> unif t t') fl fl' |
242 |
| Tclock _, Tstatic _ |
243 |
| Tstatic _, Tclock _ -> raise (Unify (t1, t2)) |
244 |
| Tclock t1', Tclock t2' -> unif t1' t2' |
245 |
| Tbasic t1, Tbasic t2 when t1 == t2 -> () |
246 |
| Tunivar, _ | _, Tunivar -> () |
247 |
| (Tconst t, _) -> |
248 |
let def_t = get_type_definition t in |
249 |
unif def_t t2 |
250 |
| (_, Tconst t) -> |
251 |
let def_t = get_type_definition t in |
252 |
unif t1 def_t |
253 |
| Tenum tl, Tenum tl' when tl == tl' -> () |
254 |
| Tstatic (e1, t1'), Tstatic (e2, t2') |
255 |
| Tarray (e1, t1'), Tarray (e2, t2') -> |
256 |
let eval_const = |
257 |
if semi |
258 |
then (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c)) |
259 |
else (fun c -> None) in |
260 |
begin |
261 |
unif t1' t2'; |
262 |
Dimension.eval Basic_library.eval_env eval_const e1; |
263 |
Dimension.eval Basic_library.eval_env eval_const e2; |
264 |
Dimension.unify ~semi:semi e1 e2; |
265 |
end |
266 |
(* Special cases for machine_types. Rules to unify static types infered |
267 |
for numerical constants with non static ones for variables with |
268 |
possible machine types *) |
269 |
| Tbasic bt1, Tbasic bt2 when BasicT.is_unifiable bt1 bt2 -> BasicT.unify bt1 bt2 |
270 |
| _,_ -> raise (Unify (t1, t2)) |
271 |
in unif t1 t2 |
272 |
|
273 |
(* Expected type ty1, got type ty2 *) |
274 |
let try_unify ?(sub=false) ?(semi=false) ty1 ty2 loc = |
275 |
try |
276 |
unify ~sub:sub ~semi:semi ty1 ty2 |
277 |
with |
278 |
| Unify _ -> |
279 |
raise (Error (loc, Type_clash (ty1,ty2))) |
280 |
| Dimension.Unify _ -> |
281 |
raise (Error (loc, Type_clash (ty1,ty2))) |
282 |
|
283 |
|
284 |
(************************************************) |
285 |
(* Typing function for each basic AST construct *) |
286 |
(************************************************) |
287 |
|
288 |
let rec type_struct_const_field ?(is_annot=false) loc (label, c) = |
289 |
if Hashtbl.mem field_table label |
290 |
then let tydef = Hashtbl.find field_table label in |
291 |
let tydec = (typedef_of_top tydef).tydef_desc in |
292 |
let tydec_struct = get_struct_type_fields tydec in |
293 |
let ty_label = type_coretype (fun d -> ()) (List.assoc label tydec_struct) in |
294 |
begin |
295 |
try_unify ty_label (type_const ~is_annot loc c) loc; |
296 |
type_coretype (fun d -> ()) tydec |
297 |
end |
298 |
else raise (Error (loc, Unbound_value ("struct field " ^ label))) |
299 |
|
300 |
and type_const ?(is_annot=false) loc c = |
301 |
match c with |
302 |
| Const_int _ -> (* Type_predef. *)type_int |
303 |
| Const_real _ -> (* Type_predef. *)type_real |
304 |
| Const_array ca -> let d = Dimension.mkdim_int loc (List.length ca) in |
305 |
let ty = new_var () in |
306 |
List.iter (fun e -> try_unify ty (type_const ~is_annot loc e) loc) ca; |
307 |
(* Type_predef. *)type_array d ty |
308 |
| Const_tag t -> |
309 |
if Hashtbl.mem tag_table t |
310 |
then |
311 |
let tydef = typedef_of_top (Hashtbl.find tag_table t) in |
312 |
let tydec = |
313 |
if is_user_type tydef.tydef_desc |
314 |
then Tydec_const tydef.tydef_id |
315 |
else tydef.tydef_desc in |
316 |
type_coretype (fun d -> ()) tydec |
317 |
else raise (Error (loc, Unbound_value ("enum tag " ^ t))) |
318 |
| Const_struct fl -> |
319 |
let ty_struct = new_var () in |
320 |
begin |
321 |
let used = |
322 |
List.fold_left |
323 |
(fun acc (l, c) -> |
324 |
if List.mem l acc |
325 |
then raise (Error (loc, Already_bound ("struct field " ^ l))) |
326 |
else try_unify ty_struct (type_struct_const_field ~is_annot loc (l, c)) loc; l::acc) |
327 |
[] fl in |
328 |
try |
329 |
let total = List.map fst (get_struct_type_fields (coretype_type ty_struct)) in |
330 |
(* List.iter (fun l -> Format.eprintf "total: %s@." l) total; |
331 |
List.iter (fun l -> Format.eprintf "used: %s@." l) used; *) |
332 |
let undef = List.find (fun l -> not (List.mem l used)) total |
333 |
in raise (Error (loc, Unbound_value ("struct field " ^ undef))) |
334 |
with Not_found -> |
335 |
ty_struct |
336 |
end |
337 |
| Const_string _ | Const_modeid _ -> |
338 |
if is_annot then (* Type_predef. *)type_string else assert false (* string datatype should only appear in annotations *) |
339 |
|
340 |
(* The following typing functions take as parameter an environment [env] |
341 |
and whether the element being typed is expected to be constant [const]. |
342 |
[env] is a pair composed of: |
343 |
- a map from ident to type, associating to each ident, i.e. |
344 |
variables, constants and (imported) nodes, its type including whether |
345 |
it is constant or not. This latter information helps in checking constant |
346 |
propagation policy in Lustre. |
347 |
- a vdecl list, in order to modify types of declared variables that are |
348 |
later discovered to be clocks during the typing process. |
349 |
*) |
350 |
let check_constant loc const_expected const_real = |
351 |
if const_expected && not const_real |
352 |
then raise (Error (loc, Not_a_constant)) |
353 |
|
354 |
let rec type_add_const env const arg targ = |
355 |
(*Format.eprintf "Typing.type_add_const %a %a@." Printers.pp_expr arg Types.print_ty targ;*) |
356 |
if const |
357 |
then let d = |
358 |
if is_dimension_type targ |
359 |
then dimension_of_expr arg |
360 |
else Dimension.mkdim_var () in |
361 |
let eval_const id = (* Types. *)get_static_value (Env.lookup_value (fst env) id) in |
362 |
Dimension.eval Basic_library.eval_env eval_const d; |
363 |
let real_static_type = (* Type_predef. *)type_static d ((* Types. *)dynamic_type targ) in |
364 |
(match (* Types. *)get_static_value targ with |
365 |
| None -> () |
366 |
| Some d' -> try_unify targ real_static_type arg.expr_loc); |
367 |
real_static_type |
368 |
else targ |
369 |
|
370 |
(* emulates a subtyping relation between types t and (d : t), |
371 |
used during node applications and assignments *) |
372 |
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type = |
373 |
let loc = real_arg.expr_loc in |
374 |
let const = const || ((* Types. *)get_static_value formal_type <> None) in |
375 |
let real_type = type_add_const env const real_arg (type_expr env in_main const real_arg) in |
376 |
(*Format.eprintf "subtyping const %B real %a:%a vs formal %a@." const Printers.pp_expr real_arg Types.print_ty real_type Types.print_ty formal_type;*) |
377 |
try_unify ~sub:sub formal_type real_type loc |
378 |
|
379 |
(* typing an application implies: |
380 |
- checking that const formal parameters match real const (maybe symbolic) arguments |
381 |
- checking type adequation between formal and real arguments |
382 |
An application may embed an homomorphic/internal function, in which case we need to split |
383 |
it in many calls |
384 |
*) |
385 |
and type_appl env in_main loc const f args = |
386 |
let targs = List.map (type_expr env in_main const) args in |
387 |
if Basic_library.is_homomorphic_fun f && List.exists is_tuple_type targs |
388 |
then |
389 |
try |
390 |
let targs = Utils.transpose_list (List.map type_list_of_type targs) in |
391 |
(* Types. *)type_of_type_list (List.map (type_simple_call env in_main loc const f) targs) |
392 |
with |
393 |
Utils.TransposeError (l, l') -> raise (Error (loc, WrongMorphism (l, l'))) |
394 |
|
395 |
else ( |
396 |
type_dependent_call env in_main loc const f (List.combine args targs) |
397 |
) |
398 |
|
399 |
(* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *) |
400 |
and type_dependent_call env in_main loc const f targs = |
401 |
(* Format.eprintf "Typing.type_dependent_call %s@." f; *) |
402 |
let tins, touts = new_var (), new_var () in |
403 |
(* Format.eprintf "tin=%a, tout=%a@." print_ty tins print_ty touts; *) |
404 |
let tfun = (* Type_predef. *)type_arrow tins touts in |
405 |
(* Format.eprintf "fun=%a@." print_ty tfun; *) |
406 |
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun; |
407 |
(* Format.eprintf "type subtyping@."; *) |
408 |
let tins = type_list_of_type tins in |
409 |
if List.length targs <> List.length tins then |
410 |
raise (Error (loc, WrongArity (List.length tins, List.length targs))) |
411 |
else |
412 |
begin |
413 |
List.iter2 ( |
414 |
fun (a,t) ti -> |
415 |
let t' = type_add_const env (const || (* Types. *)get_static_value ti <> None) a t in |
416 |
(* Format.eprintf "uniying ti=%a t'=%a touts=%a@." print_ty ti print_ty t' print_ty touts; *) |
417 |
try_unify ~sub:true ti t' a.expr_loc; |
418 |
(* Format.eprintf "unified ti=%a t'=%a touts=%a@." print_ty ti print_ty t' print_ty touts; *) |
419 |
|
420 |
) |
421 |
targs |
422 |
tins; |
423 |
touts |
424 |
end |
425 |
|
426 |
(* type a simple call without dependent types |
427 |
but possible homomorphic extension. |
428 |
[targs] is here a list of arguments' types. *) |
429 |
and type_simple_call env in_main loc const f targs = |
430 |
let tins, touts = new_var (), new_var () in |
431 |
let tfun = (* Type_predef. *)type_arrow tins touts in |
432 |
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun; |
433 |
(*Format.eprintf "try unify %a %a@." Types.print_ty tins Types.print_ty (type_of_type_list targs);*) |
434 |
try_unify ~sub:true tins (type_of_type_list targs) loc; |
435 |
touts |
436 |
|
437 |
(** [type_expr env in_main expr] types expression [expr] in environment |
438 |
[env], expecting it to be [const] or not. *) |
439 |
and type_expr ?(is_annot=false) env in_main const expr = |
440 |
let resulting_ty = |
441 |
match expr.expr_desc with |
442 |
| Expr_const c -> |
443 |
let ty = type_const ~is_annot expr.expr_loc c in |
444 |
let ty = (* Type_predef. *)type_static (Dimension.mkdim_var ()) ty in |
445 |
expr.expr_type <- Expr_type_hub.export ty; |
446 |
ty |
447 |
| Expr_ident v -> |
448 |
let tyv = |
449 |
try |
450 |
Env.lookup_value (fst env) v |
451 |
with Not_found -> |
452 |
Format.eprintf "Failure in typing expr %a. Not in typing environement@." Printers.pp_expr expr; |
453 |
raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v))) |
454 |
in |
455 |
let ty = instantiate (ref []) (ref []) tyv in |
456 |
let ty' = |
457 |
if const |
458 |
then (* Type_predef. *)type_static (Dimension.mkdim_var ()) (new_var ()) |
459 |
else new_var () in |
460 |
try_unify ty ty' expr.expr_loc; |
461 |
expr.expr_type <- Expr_type_hub.export ty; |
462 |
ty |
463 |
| Expr_array elist -> |
464 |
let ty_elt = new_var () in |
465 |
List.iter (fun e -> try_unify ty_elt (type_appl env in_main expr.expr_loc const "uminus" [e]) e.expr_loc) elist; |
466 |
let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in |
467 |
let ty = (* Type_predef. *)type_array d ty_elt in |
468 |
expr.expr_type <- Expr_type_hub.export ty; |
469 |
ty |
470 |
| Expr_access (e1, d) -> |
471 |
type_subtyping_arg env in_main false (* not necessary a constant *) (expr_of_dimension d) (* Type_predef. *)type_int; |
472 |
let ty_elt = new_var () in |
473 |
let d = Dimension.mkdim_var () in |
474 |
type_subtyping_arg env in_main const e1 ((* Type_predef. *)type_array d ty_elt); |
475 |
expr.expr_type <- Expr_type_hub.export ty_elt; |
476 |
ty_elt |
477 |
| Expr_power (e1, d) -> |
478 |
let eval_const id = (* Types. *)get_static_value (Env.lookup_value (fst env) id) in |
479 |
type_subtyping_arg env in_main true (expr_of_dimension d) (* Type_predef. *)type_int; |
480 |
Dimension.eval Basic_library.eval_env eval_const d; |
481 |
let ty_elt = type_appl env in_main expr.expr_loc const "uminus" [e1] in |
482 |
let ty = (* Type_predef. *)type_array d ty_elt in |
483 |
expr.expr_type <- Expr_type_hub.export ty; |
484 |
ty |
485 |
| Expr_tuple elist -> |
486 |
let ty = new_ty (Ttuple (List.map (type_expr ~is_annot env in_main const) elist)) in |
487 |
expr.expr_type <- Expr_type_hub.export ty; |
488 |
ty |
489 |
| Expr_ite (c, t, e) -> |
490 |
type_subtyping_arg env in_main const c (* Type_predef. *)type_bool; |
491 |
let ty = type_appl env in_main expr.expr_loc const "+" [t; e] in |
492 |
expr.expr_type <- Expr_type_hub.export ty; |
493 |
ty |
494 |
| Expr_appl (id, args, r) -> |
495 |
(* application of non internal function is not legal in a constant |
496 |
expression *) |
497 |
(match r with |
498 |
| None -> () |
499 |
| Some c -> |
500 |
check_constant expr.expr_loc const false; |
501 |
type_subtyping_arg env in_main const c (* Type_predef. *)type_bool); |
502 |
let args_list = expr_list_of_expr args in |
503 |
let touts = type_appl env in_main expr.expr_loc const id args_list in |
504 |
let targs = new_ty (Ttuple (List.map (fun a -> Expr_type_hub.import a.expr_type) args_list)) in |
505 |
args.expr_type <- Expr_type_hub.export targs; |
506 |
expr.expr_type <- Expr_type_hub.export touts; |
507 |
touts |
508 |
| Expr_fby (e1,e2) |
509 |
| Expr_arrow (e1,e2) -> |
510 |
(* fby/arrow is not legal in a constant expression *) |
511 |
check_constant expr.expr_loc const false; |
512 |
let ty = type_appl env in_main expr.expr_loc const "+" [e1; e2] in |
513 |
expr.expr_type <- Expr_type_hub.export ty; |
514 |
ty |
515 |
| Expr_pre e -> |
516 |
(* pre is not legal in a constant expression *) |
517 |
check_constant expr.expr_loc const false; |
518 |
let ty = type_appl env in_main expr.expr_loc const "uminus" [e] in |
519 |
expr.expr_type <- Expr_type_hub.export ty; |
520 |
ty |
521 |
| Expr_when (e1,c,l) -> |
522 |
(* when is not legal in a constant expression *) |
523 |
check_constant expr.expr_loc const false; |
524 |
let typ_l = (* Type_predef. *)type_clock (type_const ~is_annot expr.expr_loc (Const_tag l)) in |
525 |
let expr_c = expr_of_ident c expr.expr_loc in |
526 |
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; |
527 |
let ty = type_appl env in_main expr.expr_loc const "uminus" [e1] in |
528 |
expr.expr_type <- Expr_type_hub.export ty; |
529 |
ty |
530 |
| Expr_merge (c,hl) -> |
531 |
(* merge is not legal in a constant expression *) |
532 |
check_constant expr.expr_loc const false; |
533 |
let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in |
534 |
let expr_c = expr_of_ident c expr.expr_loc in |
535 |
let typ_l = (* Type_predef. *)type_clock typ_in in |
536 |
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; |
537 |
expr.expr_type <- Expr_type_hub.export typ_out; |
538 |
typ_out |
539 |
in |
540 |
Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr (* Types. *)print_ty resulting_ty); |
541 |
resulting_ty |
542 |
|
543 |
and type_branches ?(is_annot=false) env in_main loc const hl = |
544 |
let typ_in = new_var () in |
545 |
let typ_out = new_var () in |
546 |
try |
547 |
let used_labels = |
548 |
List.fold_left (fun accu (t, h) -> |
549 |
unify typ_in (type_const ~is_annot loc (Const_tag t)); |
550 |
type_subtyping_arg env in_main const h typ_out; |
551 |
if List.mem t accu |
552 |
then raise (Error (loc, Already_bound t)) |
553 |
else t :: accu) [] hl in |
554 |
let type_labels = get_enum_type_tags (coretype_type typ_in) in |
555 |
if List.sort compare used_labels <> List.sort compare type_labels |
556 |
then let unbound_tag = List.find (fun t -> not (List.mem t used_labels)) type_labels in |
557 |
raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag))) |
558 |
else (typ_in, typ_out) |
559 |
with Unify (t1, t2) -> |
560 |
raise (Error (loc, Type_clash (t1,t2))) |
561 |
|
562 |
(* Eexpr are always in annotations. TODO: add the quantifiers variables to the env *) |
563 |
let type_eexpr env eexpr = |
564 |
(type_expr |
565 |
~is_annot:true |
566 |
env |
567 |
false (* not in main *) |
568 |
false (* not a const *) |
569 |
eexpr.eexpr_qfexpr) |
570 |
|
571 |
|
572 |
(** [type_eq env eq] types equation [eq] in environment [env] *) |
573 |
let type_eq env in_main undefined_vars eq = |
574 |
(*Format.eprintf "Typing.type_eq %a@." Printers.pp_node_eq eq;*) |
575 |
(* Check undefined variables, type lhs *) |
576 |
let expr_lhs = expr_of_expr_list eq.eq_loc (List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs) in |
577 |
let ty_lhs = type_expr env in_main false expr_lhs in |
578 |
(* Check multiple variable definitions *) |
579 |
let define_var id uvars = |
580 |
if ISet.mem id uvars |
581 |
then ISet.remove id uvars |
582 |
else raise (Error (eq.eq_loc, Already_defined id)) |
583 |
in |
584 |
(* check assignment of declared constant, assignment of clock *) |
585 |
let ty_lhs = |
586 |
type_of_type_list |
587 |
(List.map2 (fun ty id -> |
588 |
if get_static_value ty <> None |
589 |
then raise (Error (eq.eq_loc, Assigned_constant id)) else |
590 |
match get_clock_base_type ty with |
591 |
| None -> ty |
592 |
| Some ty -> ty) |
593 |
(type_list_of_type ty_lhs) eq.eq_lhs) in |
594 |
let undefined_vars = |
595 |
List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in |
596 |
(* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned |
597 |
to a (always non-constant) lhs variable *) |
598 |
type_subtyping_arg env in_main false eq.eq_rhs ty_lhs; |
599 |
undefined_vars |
600 |
|
601 |
|
602 |
(* [type_coreclock env ck id loc] types the type clock declaration [ck] |
603 |
in environment [env] *) |
604 |
let type_coreclock env ck id loc = |
605 |
match ck.ck_dec_desc with |
606 |
| Ckdec_any -> () |
607 |
| Ckdec_bool cl -> |
608 |
let dummy_id_expr = expr_of_ident id loc in |
609 |
let when_expr = |
610 |
List.fold_left |
611 |
(fun expr (x, l) -> |
612 |
{expr_tag = new_tag (); |
613 |
expr_desc= Expr_when (expr,x,l); |
614 |
expr_type = Types.Main.new_var (); |
615 |
expr_clock = Clocks.new_var true; |
616 |
expr_delay = Delay.new_var (); |
617 |
expr_loc=loc; |
618 |
expr_annot = None}) |
619 |
dummy_id_expr cl |
620 |
in |
621 |
ignore (type_expr env false false when_expr) |
622 |
|
623 |
let rec check_type_declaration loc cty = |
624 |
match cty with |
625 |
| Tydec_clock ty |
626 |
| Tydec_array (_, ty) -> check_type_declaration loc ty |
627 |
| Tydec_const tname -> |
628 |
(* Format.eprintf "TABLE: %a@." print_type_table (); *) |
629 |
if not (Hashtbl.mem type_table cty) |
630 |
then raise (Error (loc, Unbound_type tname)); |
631 |
| _ -> () |
632 |
|
633 |
let type_var_decl vd_env env vdecl = |
634 |
(*Format.eprintf "Typing.type_var_decl START %a:%a@." Printers.pp_var vdecl Printers.print_dec_ty vdecl.var_dec_type.ty_dec_desc;*) |
635 |
check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc; |
636 |
let eval_const id = (* Types. *)get_static_value (Env.lookup_value env id) in |
637 |
let type_dim d = |
638 |
begin |
639 |
type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) (* Type_predef. *)type_int; |
640 |
Dimension.eval Basic_library.eval_env eval_const d; |
641 |
end in |
642 |
let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in |
643 |
|
644 |
let ty_static = |
645 |
if vdecl.var_dec_const |
646 |
then (* Type_predef. *)type_static (Dimension.mkdim_var ()) ty |
647 |
else ty in |
648 |
(match vdecl.var_dec_value with |
649 |
| None -> () |
650 |
| Some v -> type_subtyping_arg (env, vd_env) false ~sub:false true v ty_static); |
651 |
try_unify ty_static (Expr_type_hub.import vdecl.var_type) vdecl.var_loc; |
652 |
let new_env = Env.add_value env vdecl.var_id ty_static in |
653 |
type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc; |
654 |
(*Format.eprintf "END %a@." Types.print_ty ty_static;*) |
655 |
new_env |
656 |
|
657 |
let type_var_decl_list vd_env env l = |
658 |
List.fold_left (type_var_decl vd_env) env l |
659 |
|
660 |
let type_of_vlist vars = |
661 |
let tyl = List.map (fun v -> Expr_type_hub.import v.var_type) vars in |
662 |
type_of_type_list tyl |
663 |
|
664 |
let add_vdecl vd_env vdecl = |
665 |
if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env |
666 |
then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id)) |
667 |
else vdecl::vd_env |
668 |
|
669 |
let check_vd_env vd_env = |
670 |
ignore (List.fold_left add_vdecl [] vd_env) |
671 |
|
672 |
let type_contract env c = |
673 |
let vd_env = c.consts @ c.locals in |
674 |
check_vd_env vd_env; |
675 |
let env = type_var_decl_list ((* this argument seems useless to me, cf TODO at top of the file*) vd_env) env vd_env in |
676 |
(* typing stmts *) |
677 |
let eqs = List.map (fun s -> match s with Eq eq -> eq | _ -> assert false) c.stmts in |
678 |
let undefined_vars_init = |
679 |
List.fold_left |
680 |
(fun uvs v -> ISet.add v.var_id uvs) |
681 |
ISet.empty c.locals |
682 |
in |
683 |
let _ = |
684 |
List.fold_left |
685 |
(type_eq (env, vd_env) (false (*is_main*))) |
686 |
undefined_vars_init |
687 |
eqs |
688 |
in |
689 |
(* Typing each predicate expr *) |
690 |
let type_pred_ee ee : unit= |
691 |
type_subtyping_arg (env, vd_env) (false (* not in main *)) (false (* not a const *)) ee.eexpr_qfexpr type_bool |
692 |
in |
693 |
List.iter type_pred_ee |
694 |
( |
695 |
c.assume |
696 |
@ c.guarantees |
697 |
@ List.flatten (List.map (fun m -> m.ensure @ m.require) c.modes) |
698 |
); |
699 |
(*TODO |
700 |
enrich env locally with locals and consts |
701 |
type each pre/post as a boolean expr |
702 |
I don't know if we want to update the global env with locally typed variables. |
703 |
For the moment, returning the provided env |
704 |
*) |
705 |
env |
706 |
|
707 |
let rec type_spec env spec loc = |
708 |
match spec with |
709 |
| Contract c -> type_contract env c |
710 |
| NodeSpec id -> env |
711 |
|
712 |
(** [type_node env nd loc] types node [nd] in environment env. The |
713 |
location is used for error reports. *) |
714 |
and type_node env nd loc = |
715 |
let is_main = nd.node_id = !Options.main_node in |
716 |
(* In contracts, outputs are considered as input values *) |
717 |
let vd_env_ol = if nd.node_iscontract then nd.node_locals else nd.node_outputs@nd.node_locals in |
718 |
let vd_env = nd.node_inputs@nd.node_outputs@nd.node_locals in |
719 |
check_vd_env vd_env; |
720 |
let init_env = env in |
721 |
let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in |
722 |
let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in |
723 |
let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in |
724 |
let new_env = Env.overwrite env delta_env in |
725 |
let undefined_vars_init = |
726 |
List.fold_left |
727 |
(fun uvs v -> ISet.add v.var_id uvs) |
728 |
ISet.empty vd_env_ol in |
729 |
Format.eprintf "Undef1: %a@ " pp_iset undefined_vars_init; |
730 |
let undefined_vars = |
731 |
let eqs, auts = get_node_eqs nd in |
732 |
(* TODO XXX: il faut typer les handlers de l'automate *) |
733 |
List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init eqs |
734 |
in |
735 |
Format.eprintf "Undef2: %a@ " pp_iset undefined_vars; |
736 |
(* Typing asserts *) |
737 |
List.iter (fun assert_ -> |
738 |
let assert_expr = assert_.assert_expr in |
739 |
type_subtyping_arg (new_env, vd_env) is_main false assert_expr (* Type_predef. *)type_bool |
740 |
) nd.node_asserts; |
741 |
(* Typing spec/contracts *) |
742 |
(match nd.node_spec with |
743 |
| None -> () |
744 |
| Some spec -> ignore (type_spec new_env spec loc)); |
745 |
(* Typing annots *) |
746 |
List.iter (fun annot -> |
747 |
List.iter (fun (_, eexpr) -> ignore (type_eexpr (new_env, vd_env) eexpr)) annot.annots |
748 |
) nd.node_annot; |
749 |
|
750 |
(* check that table is empty *) |
751 |
let local_consts = List.fold_left (fun res vdecl -> if vdecl.var_dec_const then ISet.add vdecl.var_id res else res) ISet.empty nd.node_locals in |
752 |
Format.eprintf "Localconsts: %a@ " pp_iset local_consts; |
753 |
let undefined_vars = ISet.diff undefined_vars local_consts in |
754 |
Format.eprintf "Undef3: %a@ " pp_iset undefined_vars; |
755 |
|
756 |
if (not (ISet.is_empty undefined_vars)) then |
757 |
raise (Error (loc, Undefined_var undefined_vars)); |
758 |
let ty_ins = type_of_vlist nd.node_inputs in |
759 |
let ty_outs = type_of_vlist nd.node_outputs in |
760 |
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in |
761 |
generalize ty_node; |
762 |
(* TODO ? Check that no node in the hierarchy remains polymorphic ? *) |
763 |
nd.node_type <- Expr_type_hub.export ty_node; |
764 |
Env.add_value env nd.node_id ty_node |
765 |
|
766 |
let type_imported_node env nd loc = |
767 |
let vd_env = nd.nodei_inputs@nd.nodei_outputs in |
768 |
check_vd_env vd_env; |
769 |
let delta_env = type_var_decl_list vd_env env nd.nodei_inputs in |
770 |
let delta_env = type_var_decl_list vd_env delta_env nd.nodei_outputs in |
771 |
let new_env = Env.overwrite env delta_env in |
772 |
(* Typing spec *) |
773 |
(match nd.nodei_spec with |
774 |
| None -> () |
775 |
| Some spec -> ignore (type_spec new_env spec loc)); |
776 |
let ty_ins = type_of_vlist nd.nodei_inputs in |
777 |
let ty_outs = type_of_vlist nd.nodei_outputs in |
778 |
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in |
779 |
generalize ty_node; |
780 |
(* |
781 |
if (is_polymorphic ty_node) then |
782 |
raise (Error (loc, Poly_imported_node nd.nodei_id)); |
783 |
*) |
784 |
let new_env = Env.add_value env nd.nodei_id ty_node in |
785 |
nd.nodei_type <- Expr_type_hub.export ty_node; |
786 |
new_env |
787 |
|
788 |
let type_top_const env cdecl = |
789 |
let ty = type_const cdecl.const_loc cdecl.const_value in |
790 |
let d = |
791 |
if is_dimension_type ty |
792 |
then dimension_of_const cdecl.const_loc cdecl.const_value |
793 |
else Dimension.mkdim_var () in |
794 |
let ty = (* Type_predef. *)type_static d ty in |
795 |
let new_env = Env.add_value env cdecl.const_id ty in |
796 |
cdecl.const_type <- Expr_type_hub.export ty; |
797 |
new_env |
798 |
|
799 |
let type_top_consts env clist = |
800 |
List.fold_left type_top_const env clist |
801 |
|
802 |
let rec type_top_decl env decl = |
803 |
match decl.top_decl_desc with |
804 |
| Node nd -> ( |
805 |
try |
806 |
type_node env nd decl.top_decl_loc |
807 |
with Error (loc, err) as exc -> ( |
808 |
if !Options.global_inline then |
809 |
Format.eprintf "Type error: failing node@.%a@.@?" |
810 |
Printers.pp_node nd |
811 |
; |
812 |
raise exc) |
813 |
) |
814 |
| ImportedNode nd -> |
815 |
type_imported_node env nd decl.top_decl_loc |
816 |
| Const c -> |
817 |
type_top_const env c |
818 |
| TypeDef _ -> List.fold_left type_top_decl env (consts_of_enum_type decl) |
819 |
| Include _ | Open _ -> env |
820 |
|
821 |
let get_type_of_call decl = |
822 |
match decl.top_decl_desc with |
823 |
| Node nd -> |
824 |
let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.node_type) in |
825 |
type_list_of_type in_typ, type_list_of_type out_typ |
826 |
| ImportedNode nd -> |
827 |
let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.nodei_type) in |
828 |
type_list_of_type in_typ, type_list_of_type out_typ |
829 |
| _ -> assert false |
830 |
|
831 |
let type_prog env decls = |
832 |
try |
833 |
List.fold_left type_top_decl env decls |
834 |
with Failure _ as exc -> raise exc |
835 |
|
836 |
(* Once the Lustre program is fully typed, we must get back to the |
837 |
original description of dimensions, with constant parameters, |
838 |
instead of unifiable internal variables. *) |
839 |
|
840 |
(* The following functions aims at 'unevaluating' dimension |
841 |
expressions occuring in array types, i.e. replacing unifiable |
842 |
second_order variables with the original static parameters. |
843 |
Once restored in this formulation, dimensions may be |
844 |
meaningfully printed. *) |
845 |
let uneval_vdecl_generics vdecl = |
846 |
if vdecl.var_dec_const |
847 |
then |
848 |
match get_static_value (Expr_type_hub.import vdecl.var_type) with |
849 |
| None -> (Format.eprintf "internal error: %a@." (* Types. *)print_ty (Expr_type_hub.import vdecl.var_type); assert false) |
850 |
| Some d -> Dimension.uneval vdecl.var_id d |
851 |
|
852 |
let uneval_node_generics vdecls = |
853 |
List.iter uneval_vdecl_generics vdecls |
854 |
|
855 |
let uneval_spec_generics spec = |
856 |
List.iter uneval_vdecl_generics (spec.consts@spec.locals) |
857 |
|
858 |
let uneval_top_generics decl = |
859 |
match decl.top_decl_desc with |
860 |
| Node nd -> |
861 |
uneval_node_generics (nd.node_inputs @ nd.node_outputs) |
862 |
| ImportedNode nd -> |
863 |
uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs) |
864 |
| Const _ | TypeDef _ | Open _ | Include _ |
865 |
-> () |
866 |
|
867 |
let uneval_prog_generics prog = |
868 |
List.iter uneval_top_generics prog |
869 |
|
870 |
let rec get_imported_symbol decls id = |
871 |
match decls with |
872 |
| [] -> assert false |
873 |
| decl::q -> |
874 |
(match decl.top_decl_desc with |
875 |
| ImportedNode nd when id = nd.nodei_id && decl.top_decl_itf -> decl |
876 |
| Const c when id = c.const_id && decl.top_decl_itf -> decl |
877 |
| TypeDef _ -> get_imported_symbol (consts_of_enum_type decl @ q) id |
878 |
| _ -> get_imported_symbol q id) |
879 |
|
880 |
let check_env_compat header declared computed = |
881 |
uneval_prog_generics header; |
882 |
Env.iter declared (fun k decl_type_k -> |
883 |
let top = get_imported_symbol header k in |
884 |
let loc = top.top_decl_loc in |
885 |
try |
886 |
let computed_t = Env.lookup_value computed k in |
887 |
let computed_t = instantiate (ref []) (ref []) computed_t in |
888 |
(*Types.print_ty Format.std_formatter decl_type_k; |
889 |
Types.print_ty Format.std_formatter computed_t;*) |
890 |
try_unify ~sub:true ~semi:true decl_type_k computed_t loc |
891 |
with Not_found -> |
892 |
begin |
893 |
(* If top is a contract we do not require the lustre |
894 |
file to provide the same definition. *) |
895 |
match top.top_decl_desc with |
896 |
| Node nd -> ( |
897 |
match nd.node_spec with |
898 |
| Some (Contract _) -> () |
899 |
| _ -> raise (Error (loc, Declared_but_undefined k)) |
900 |
) |
901 |
| _ -> |
902 |
raise (Error (loc, Declared_but_undefined k)) |
903 |
end |
904 |
) |
905 |
|
906 |
let check_typedef_top decl = |
907 |
(*Format.eprintf "check_typedef %a@." Printers.pp_short_decl decl;*) |
908 |
(*Format.eprintf "%a" Printers.pp_typedef (typedef_of_top decl);*) |
909 |
(*Format.eprintf "%a" Corelang.print_type_table ();*) |
910 |
match decl.top_decl_desc with |
911 |
| TypeDef ty -> |
912 |
let owner = decl.top_decl_owner in |
913 |
let itf = decl.top_decl_itf in |
914 |
let decl' = |
915 |
try Hashtbl.find type_table (Tydec_const (typedef_of_top decl).tydef_id) |
916 |
with Not_found -> raise (Error (decl.top_decl_loc, Declared_but_undefined ("type "^ ty.tydef_id))) in |
917 |
let owner' = decl'.top_decl_owner in |
918 |
(*Format.eprintf "def owner = %s@.decl owner = %s@." owner' owner;*) |
919 |
let itf' = decl'.top_decl_itf in |
920 |
(match decl'.top_decl_desc with |
921 |
| Const _ | Node _ | ImportedNode _ -> assert false |
922 |
| TypeDef ty' when coretype_equal ty'.tydef_desc ty.tydef_desc && owner' = owner && itf && (not itf') -> () |
923 |
| _ -> raise (Error (decl.top_decl_loc, Type_mismatch ty.tydef_id))) |
924 |
| _ -> () |
925 |
|
926 |
let check_typedef_compat header = |
927 |
List.iter check_typedef_top header |
928 |
end |
929 |
|
930 |
include Make(Types.Main) (struct |
931 |
type type_expr = Types.Main.type_expr |
932 |
let import x = x |
933 |
let export x = x |
934 |
end) |
935 |
(* Local Variables: *) |
936 |
(* compile-command:"make -C .." *) |
937 |
(* End: *) |