1
|
(* ----------------------------------------------------------------------------
|
2
|
* SchedMCore - A MultiCore Scheduling Framework
|
3
|
* Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
|
4
|
*
|
5
|
* This file is part of Prelude
|
6
|
*
|
7
|
* Prelude is free software; you can redistribute it and/or
|
8
|
* modify it under the terms of the GNU Lesser General Public License
|
9
|
* as published by the Free Software Foundation ; either version 2 of
|
10
|
* the License, or (at your option) any later version.
|
11
|
*
|
12
|
* Prelude is distributed in the hope that it will be useful, but
|
13
|
* WITHOUT ANY WARRANTY ; without even the implied warranty of
|
14
|
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
|
15
|
* Lesser General Public License for more details.
|
16
|
*
|
17
|
* You should have received a copy of the GNU Lesser General Public
|
18
|
* License along with this program ; if not, write to the Free Software
|
19
|
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
|
20
|
* USA
|
21
|
*---------------------------------------------------------------------------- *)
|
22
|
|
23
|
(** Main typing module. Classic inference algorithm with destructive
|
24
|
unification. *)
|
25
|
|
26
|
let debug fmt args = () (* Format.eprintf "%a" *)
|
27
|
(* Though it shares similarities with the clock calculus module, no code
|
28
|
is shared. Simple environments, very limited identifier scoping, no
|
29
|
identifier redefinition allowed. *)
|
30
|
|
31
|
open Utils
|
32
|
(* Yes, opening both modules is dirty as some type names will be
|
33
|
overwritten, yet this makes notations far lighter.*)
|
34
|
open LustreSpec
|
35
|
open Corelang
|
36
|
open Types
|
37
|
open Format
|
38
|
|
39
|
let pp_typing_env fmt env =
|
40
|
Env.pp_env print_ty fmt env
|
41
|
|
42
|
(** [occurs tvar ty] returns true if the type variable [tvar] occurs in
|
43
|
type [ty]. False otherwise. *)
|
44
|
let rec occurs tvar ty =
|
45
|
let ty = repr ty in
|
46
|
match ty.tdesc with
|
47
|
| Tvar -> ty=tvar
|
48
|
| Tarrow (t1, t2) ->
|
49
|
(occurs tvar t1) || (occurs tvar t2)
|
50
|
| Ttuple tl ->
|
51
|
List.exists (occurs tvar) tl
|
52
|
| Tstruct fl ->
|
53
|
List.exists (fun (f, t) -> occurs tvar t) fl
|
54
|
| Tarray (_, t)
|
55
|
| Tstatic (_, t)
|
56
|
| Tclock t
|
57
|
| Tlink t -> occurs tvar t
|
58
|
| Tenum _ | Tconst _ | Tunivar | Tint | Treal | Tbool | Trat -> false
|
59
|
|
60
|
(** Promote monomorphic type variables to polymorphic type variables. *)
|
61
|
(* Generalize by side-effects *)
|
62
|
let rec generalize ty =
|
63
|
match ty.tdesc with
|
64
|
| Tvar ->
|
65
|
(* No scopes, always generalize *)
|
66
|
ty.tdesc <- Tunivar
|
67
|
| Tarrow (t1,t2) ->
|
68
|
generalize t1; generalize t2
|
69
|
| Ttuple tl ->
|
70
|
List.iter generalize tl
|
71
|
| Tstruct fl ->
|
72
|
List.iter (fun (f, t) -> generalize t) fl
|
73
|
| Tstatic (d, t)
|
74
|
| Tarray (d, t) -> Dimension.generalize d; generalize t
|
75
|
| Tclock t
|
76
|
| Tlink t ->
|
77
|
generalize t
|
78
|
| Tenum _ | Tconst _ | Tunivar | Tint | Treal | Tbool | Trat -> ()
|
79
|
|
80
|
(** Downgrade polymorphic type variables to monomorphic type variables *)
|
81
|
let rec instantiate inst_vars inst_dim_vars ty =
|
82
|
let ty = repr ty in
|
83
|
match ty.tdesc with
|
84
|
| Tenum _ | Tconst _ | Tvar | Tint | Treal | Tbool | Trat -> ty
|
85
|
| Tarrow (t1,t2) ->
|
86
|
{ty with tdesc =
|
87
|
Tarrow ((instantiate inst_vars inst_dim_vars t1), (instantiate inst_vars inst_dim_vars t2))}
|
88
|
| Ttuple tlist ->
|
89
|
{ty with tdesc = Ttuple (List.map (instantiate inst_vars inst_dim_vars) tlist)}
|
90
|
| Tstruct flist ->
|
91
|
{ty with tdesc = Tstruct (List.map (fun (f, t) -> (f, instantiate inst_vars inst_dim_vars t)) flist)}
|
92
|
| Tclock t ->
|
93
|
{ty with tdesc = Tclock (instantiate inst_vars inst_dim_vars t)}
|
94
|
| Tstatic (d, t) ->
|
95
|
{ty with tdesc = Tstatic (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)}
|
96
|
| Tarray (d, t) ->
|
97
|
{ty with tdesc = Tarray (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)}
|
98
|
| Tlink t ->
|
99
|
(* should not happen *)
|
100
|
{ty with tdesc = Tlink (instantiate inst_vars inst_dim_vars t)}
|
101
|
| Tunivar ->
|
102
|
try
|
103
|
List.assoc ty.tid !inst_vars
|
104
|
with Not_found ->
|
105
|
let var = new_var () in
|
106
|
inst_vars := (ty.tid, var)::!inst_vars;
|
107
|
var
|
108
|
|
109
|
(* [type_coretype cty] types the type declaration [cty] *)
|
110
|
let rec type_coretype type_dim cty =
|
111
|
match (*get_repr_type*) cty with
|
112
|
| Tydec_any -> new_var ()
|
113
|
| Tydec_int -> Type_predef.type_int
|
114
|
| Tydec_real -> Type_predef.type_real
|
115
|
| Tydec_float -> Type_predef.type_real
|
116
|
| Tydec_bool -> Type_predef.type_bool
|
117
|
| Tydec_clock ty -> Type_predef.type_clock (type_coretype type_dim ty)
|
118
|
| Tydec_const c -> Type_predef.type_const c
|
119
|
| Tydec_enum tl -> Type_predef.type_enum tl
|
120
|
| Tydec_struct fl -> Type_predef.type_struct (List.map (fun (f, ty) -> (f, type_coretype type_dim ty)) fl)
|
121
|
| Tydec_array (d, ty) ->
|
122
|
begin
|
123
|
type_dim d;
|
124
|
Type_predef.type_array d (type_coretype type_dim ty)
|
125
|
end
|
126
|
|
127
|
(* [coretype_type] is the reciprocal of [type_typecore] *)
|
128
|
let rec coretype_type ty =
|
129
|
match (repr ty).tdesc with
|
130
|
| Tvar -> Tydec_any
|
131
|
| Tint -> Tydec_int
|
132
|
| Treal -> Tydec_real
|
133
|
| Tbool -> Tydec_bool
|
134
|
| Tconst c -> Tydec_const c
|
135
|
| Tclock t -> Tydec_clock (coretype_type t)
|
136
|
| Tenum tl -> Tydec_enum tl
|
137
|
| Tstruct fl -> Tydec_struct (List.map (fun (f, t) -> (f, coretype_type t)) fl)
|
138
|
| Tarray (d, t) -> Tydec_array (d, coretype_type t)
|
139
|
| Tstatic (_, t) -> coretype_type t
|
140
|
| _ -> assert false
|
141
|
|
142
|
let get_type_definition tname =
|
143
|
try
|
144
|
type_coretype (fun d -> ()) (Hashtbl.find type_table (Tydec_const tname))
|
145
|
with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname))
|
146
|
|
147
|
(* Equality on ground types only *)
|
148
|
(* Should be used between local variables which must have a ground type *)
|
149
|
let rec eq_ground t1 t2 =
|
150
|
match t1.tdesc, t2.tdesc with
|
151
|
| Tint, Tint | Tbool, Tbool | Trat, Trat | Treal, Treal -> true
|
152
|
| Tenum tl, Tenum tl' when tl == tl' -> true
|
153
|
| Ttuple tl, Ttuple tl' when List.length tl = List.length tl' -> List.for_all2 eq_ground tl tl'
|
154
|
| 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'
|
155
|
| (Tconst t, _) ->
|
156
|
let def_t = get_type_definition t in
|
157
|
eq_ground def_t t2
|
158
|
| (_, Tconst t) ->
|
159
|
let def_t = get_type_definition t in
|
160
|
eq_ground t1 def_t
|
161
|
| Tarrow (t1,t2), Tarrow (t1',t2') -> eq_ground t1 t1' && eq_ground t2 t2'
|
162
|
| Tclock t1', Tclock t2' -> eq_ground t1' t2'
|
163
|
| Tstatic (e1, t1'), Tstatic (e2, t2')
|
164
|
| Tarray (e1, t1'), Tarray (e2, t2') -> Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2'
|
165
|
| _ -> false
|
166
|
|
167
|
(** [unify t1 t2] unifies types [t1] and [t2]
|
168
|
using standard destructive unification.
|
169
|
Raises [Unify (t1,t2)] if the types are not unifiable.
|
170
|
[t1] is a expected/formal/spec type, [t2] is a computed/real/implem type,
|
171
|
so in case of unification error: expected type [t1], got type [t2].
|
172
|
If [sub]-typing is allowed, [t2] may be a subtype of [t1].
|
173
|
If [semi] unification is required,
|
174
|
[t1] should furthermore be an instance of [t2]
|
175
|
and constants are handled differently.*)
|
176
|
let unify ?(sub=false) ?(semi=false) t1 t2 =
|
177
|
let rec unif t1 t2 =
|
178
|
let t1 = repr t1 in
|
179
|
let t2 = repr t2 in
|
180
|
if t1==t2 then
|
181
|
()
|
182
|
else
|
183
|
match t1.tdesc,t2.tdesc with
|
184
|
(* strictly subtyping cases first *)
|
185
|
| _ , Tclock t2 when sub && (get_clock_base_type t1 = None) ->
|
186
|
unif t1 t2
|
187
|
| _ , Tstatic (d2, t2) when sub && (get_static_value t1 = None) ->
|
188
|
unif t1 t2
|
189
|
(* This case is not mandatory but will keep "older" types *)
|
190
|
| Tvar, Tvar ->
|
191
|
if t1.tid < t2.tid then
|
192
|
t2.tdesc <- Tlink t1
|
193
|
else
|
194
|
t1.tdesc <- Tlink t2
|
195
|
| Tvar, _ when (not semi) && (not (occurs t1 t2)) ->
|
196
|
t1.tdesc <- Tlink t2
|
197
|
| _, Tvar when (not (occurs t2 t1)) ->
|
198
|
t2.tdesc <- Tlink t1
|
199
|
| Tarrow (t1,t2), Tarrow (t1',t2') ->
|
200
|
begin
|
201
|
unif t2 t2';
|
202
|
unif t1' t1
|
203
|
end
|
204
|
| Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->
|
205
|
List.iter2 unif tl tl'
|
206
|
| Ttuple [t1] , _ -> unif t1 t2
|
207
|
| _ , Ttuple [t2] -> unif t1 t2
|
208
|
| Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->
|
209
|
List.iter2 (fun (_, t) (_, t') -> unif t t') fl fl'
|
210
|
| Tclock _, Tstatic _
|
211
|
| Tstatic _, Tclock _ -> raise (Unify (t1, t2))
|
212
|
| Tclock t1', Tclock t2' -> unif t1' t2'
|
213
|
| Tint, Tint | Tbool, Tbool | Trat, Trat | Treal, Treal
|
214
|
| Tunivar, _ | _, Tunivar -> ()
|
215
|
| (Tconst t, _) ->
|
216
|
let def_t = get_type_definition t in
|
217
|
unif def_t t2
|
218
|
| (_, Tconst t) ->
|
219
|
let def_t = get_type_definition t in
|
220
|
unif t1 def_t
|
221
|
| Tenum tl, Tenum tl' when tl == tl' -> ()
|
222
|
| Tstatic (e1, t1'), Tstatic (e2, t2')
|
223
|
| Tarray (e1, t1'), Tarray (e2, t2') ->
|
224
|
let eval_const =
|
225
|
if semi
|
226
|
then (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c))
|
227
|
else (fun c -> None) in
|
228
|
begin
|
229
|
unif t1' t2';
|
230
|
Dimension.eval Basic_library.eval_env eval_const e1;
|
231
|
Dimension.eval Basic_library.eval_env eval_const e2;
|
232
|
Dimension.unify ~semi:semi e1 e2;
|
233
|
end
|
234
|
| _,_ -> raise (Unify (t1, t2))
|
235
|
in unif t1 t2
|
236
|
|
237
|
(* Expected type ty1, got type ty2 *)
|
238
|
let try_unify ?(sub=false) ?(semi=false) ty1 ty2 loc =
|
239
|
try
|
240
|
unify ~sub:sub ~semi:semi ty1 ty2
|
241
|
with
|
242
|
| Unify _ ->
|
243
|
raise (Error (loc, Type_clash (ty1,ty2)))
|
244
|
| Dimension.Unify _ ->
|
245
|
raise (Error (loc, Type_clash (ty1,ty2)))
|
246
|
|
247
|
(* ty1 is a subtype of ty2 *)
|
248
|
(*
|
249
|
let rec sub_unify sub ty1 ty2 =
|
250
|
match (repr ty1).tdesc, (repr ty2).tdesc with
|
251
|
| Ttuple tl1 , Ttuple tl2 ->
|
252
|
if List.length tl1 <> List.length tl2
|
253
|
then raise (Unify (ty1, ty2))
|
254
|
else List.iter2 (sub_unify sub) tl1 tl2
|
255
|
| Ttuple [t1] , _ -> sub_unify sub t1 ty2
|
256
|
| _ , Ttuple [t2] -> sub_unify sub ty1 t2
|
257
|
| Tstruct tl1 , Tstruct tl2 ->
|
258
|
if List.map fst tl1 <> List.map fst tl2
|
259
|
then raise (Unify (ty1, ty2))
|
260
|
else List.iter2 (fun (_, t1) (_, t2) -> sub_unify sub t1 t2) tl1 tl2
|
261
|
| Tclock t1 , Tclock t2 -> sub_unify sub t1 t2
|
262
|
| Tclock t1 , _ when sub -> sub_unify sub t1 ty2
|
263
|
| Tstatic (d1, t1) , Tstatic (d2, t2) ->
|
264
|
begin
|
265
|
sub_unify sub t1 t2;
|
266
|
Dimension.eval Basic_library.eval_env (fun c -> None) d1;
|
267
|
Dimension.eval Basic_library.eval_env (fun c -> None) d2;
|
268
|
Dimension.unify d1 d2
|
269
|
end
|
270
|
| Tstatic (r_d, t1) , _ when sub -> sub_unify sub t1 ty2
|
271
|
| _ -> unify ty1 ty2
|
272
|
*)
|
273
|
|
274
|
let rec type_struct_const_field loc (label, c) =
|
275
|
if Hashtbl.mem field_table label
|
276
|
then let tydec = Hashtbl.find field_table label in
|
277
|
let tydec_struct = get_struct_type_fields tydec in
|
278
|
let ty_label = type_coretype (fun d -> ()) (List.assoc label tydec_struct) in
|
279
|
begin
|
280
|
try_unify ty_label (type_const loc c) loc;
|
281
|
type_coretype (fun d -> ()) tydec
|
282
|
end
|
283
|
else raise (Error (loc, Unbound_value ("struct field " ^ label)))
|
284
|
|
285
|
and type_const loc c =
|
286
|
match c with
|
287
|
| Const_int _ -> Type_predef.type_int
|
288
|
| Const_real _ -> Type_predef.type_real
|
289
|
| Const_float _ -> Type_predef.type_real
|
290
|
| Const_array ca -> let d = Dimension.mkdim_int loc (List.length ca) in
|
291
|
let ty = new_var () in
|
292
|
List.iter (fun e -> try_unify ty (type_const loc e) loc) ca;
|
293
|
Type_predef.type_array d ty
|
294
|
| Const_tag t ->
|
295
|
if Hashtbl.mem tag_table t
|
296
|
then type_coretype (fun d -> ()) (Hashtbl.find tag_table t)
|
297
|
else raise (Error (loc, Unbound_value ("enum tag " ^ t)))
|
298
|
| Const_struct fl ->
|
299
|
let ty_struct = new_var () in
|
300
|
begin
|
301
|
let used =
|
302
|
List.fold_left
|
303
|
(fun acc (l, c) ->
|
304
|
if List.mem l acc
|
305
|
then raise (Error (loc, Already_bound ("struct field " ^ l)))
|
306
|
else try_unify ty_struct (type_struct_const_field loc (l, c)) loc; l::acc)
|
307
|
[] fl in
|
308
|
try
|
309
|
let total = List.map fst (get_struct_type_fields (coretype_type ty_struct)) in
|
310
|
(* List.iter (fun l -> Format.eprintf "total: %s@." l) total;
|
311
|
List.iter (fun l -> Format.eprintf "used: %s@." l) used; *)
|
312
|
let undef = List.find (fun l -> not (List.mem l used)) total
|
313
|
in raise (Error (loc, Unbound_value ("struct field " ^ undef)))
|
314
|
with Not_found ->
|
315
|
ty_struct
|
316
|
end
|
317
|
| Const_string _ -> assert false (* string should only appear in annotations *)
|
318
|
|
319
|
(* The following typing functions take as parameter an environment [env]
|
320
|
and whether the element being typed is expected to be constant [const].
|
321
|
[env] is a pair composed of:
|
322
|
- a map from ident to type, associating to each ident, i.e.
|
323
|
variables, constants and (imported) nodes, its type including whether
|
324
|
it is constant or not. This latter information helps in checking constant
|
325
|
propagation policy in Lustre.
|
326
|
- a vdecl list, in order to modify types of declared variables that are
|
327
|
later discovered to be clocks during the typing process.
|
328
|
*)
|
329
|
let check_constant loc const_expected const_real =
|
330
|
if const_expected && not const_real
|
331
|
then raise (Error (loc, Not_a_constant))
|
332
|
|
333
|
let rec type_standard_args env in_main const expr_list =
|
334
|
let ty_list =
|
335
|
List.map
|
336
|
(fun e -> let ty = dynamic_type (type_expr env in_main const e) in
|
337
|
match get_clock_base_type ty with
|
338
|
| None -> ty
|
339
|
| Some ty -> ty)
|
340
|
expr_list in
|
341
|
let ty_res = new_var () in
|
342
|
List.iter2 (fun e ty -> try_unify ty_res ty e.expr_loc) expr_list ty_list;
|
343
|
ty_res
|
344
|
|
345
|
(* emulates a subtyping relation between types t and (d : t),
|
346
|
used during node applications and assignments *)
|
347
|
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =
|
348
|
let loc = real_arg.expr_loc in
|
349
|
let const = const || (Types.get_static_value formal_type <> None) in
|
350
|
let real_type = type_expr env in_main const real_arg in
|
351
|
let real_type =
|
352
|
if const
|
353
|
then let d =
|
354
|
if is_dimension_type real_type
|
355
|
then dimension_of_expr real_arg
|
356
|
else Dimension.mkdim_var () in
|
357
|
let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
|
358
|
Dimension.eval Basic_library.eval_env eval_const d;
|
359
|
let real_static_type = Type_predef.type_static d (Types.dynamic_type real_type) in
|
360
|
(match Types.get_static_value real_type with
|
361
|
| None -> ()
|
362
|
| Some d' -> try_unify real_type real_static_type loc);
|
363
|
real_static_type
|
364
|
else real_type in
|
365
|
(*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;*)
|
366
|
try_unify ~sub:sub formal_type real_type loc
|
367
|
|
368
|
and type_ident env in_main loc const id =
|
369
|
type_expr env in_main const (expr_of_ident id loc)
|
370
|
|
371
|
(* typing an application implies:
|
372
|
- checking that const formal parameters match real const (maybe symbolic) arguments
|
373
|
- checking type adequation between formal and real arguments
|
374
|
An application may embed an homomorphic/internal function, in which case we need to split
|
375
|
it in many calls
|
376
|
*)
|
377
|
and type_appl env in_main loc const f args =
|
378
|
let args = expr_list_of_expr args in
|
379
|
if Basic_library.is_internal_fun f && List.exists is_tuple_expr args
|
380
|
then
|
381
|
try
|
382
|
let args = Utils.transpose_list (List.map expr_list_of_expr args) in
|
383
|
Types.type_of_type_list (List.map (type_call env in_main loc const f) args)
|
384
|
with
|
385
|
Utils.TransposeError (l, l') -> raise (Error (loc, WrongMorphism (l, l')))
|
386
|
else
|
387
|
type_call env in_main loc const f args
|
388
|
|
389
|
(* type a (single) call. [args] is here a list of arguments. *)
|
390
|
and type_call env in_main loc const f args =
|
391
|
let tins, touts = new_var (), new_var () in
|
392
|
let tfun = Type_predef.type_arrow tins touts in
|
393
|
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
|
394
|
let tins = type_list_of_type tins in
|
395
|
if List.length args <> List.length tins then
|
396
|
raise (Error (loc, WrongArity (List.length tins, List.length args)))
|
397
|
else
|
398
|
List.iter2 (type_subtyping_arg env in_main const) args tins;
|
399
|
touts
|
400
|
|
401
|
(** [type_expr env in_main expr] types expression [expr] in environment
|
402
|
[env], expecting it to be [const] or not. *)
|
403
|
and type_expr env in_main const expr =
|
404
|
let resulting_ty =
|
405
|
match expr.expr_desc with
|
406
|
| Expr_const c ->
|
407
|
let ty = type_const expr.expr_loc c in
|
408
|
let ty = Type_predef.type_static (Dimension.mkdim_var ()) ty in
|
409
|
expr.expr_type <- ty;
|
410
|
ty
|
411
|
| Expr_ident v ->
|
412
|
let tyv =
|
413
|
try
|
414
|
Env.lookup_value (fst env) v
|
415
|
with Not_found ->
|
416
|
Format.eprintf "Failure in typing expr %a@." Printers.pp_expr expr;
|
417
|
raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v)))
|
418
|
in
|
419
|
let ty = instantiate (ref []) (ref []) tyv in
|
420
|
let ty' =
|
421
|
if const
|
422
|
then Type_predef.type_static (Dimension.mkdim_var ()) (new_var ())
|
423
|
else new_var () in
|
424
|
try_unify ty ty' expr.expr_loc;
|
425
|
expr.expr_type <- ty;
|
426
|
ty
|
427
|
| Expr_array elist ->
|
428
|
let ty_elt = type_standard_args env in_main const elist in
|
429
|
let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in
|
430
|
let ty = Type_predef.type_array d ty_elt in
|
431
|
expr.expr_type <- ty;
|
432
|
ty
|
433
|
| Expr_access (e1, d) ->
|
434
|
type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int;
|
435
|
let ty_elt = new_var () in
|
436
|
let d = Dimension.mkdim_var () in
|
437
|
type_subtyping_arg env in_main const e1 (Type_predef.type_array d ty_elt);
|
438
|
expr.expr_type <- ty_elt;
|
439
|
ty_elt
|
440
|
| Expr_power (e1, d) ->
|
441
|
let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
|
442
|
type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int;
|
443
|
Dimension.eval Basic_library.eval_env eval_const d;
|
444
|
let ty_elt = type_standard_args env in_main const [e1] in
|
445
|
let ty = Type_predef.type_array d ty_elt in
|
446
|
expr.expr_type <- ty;
|
447
|
ty
|
448
|
| Expr_tuple elist ->
|
449
|
let ty = new_ty (Ttuple (List.map (type_expr env in_main const) elist)) in
|
450
|
expr.expr_type <- ty;
|
451
|
ty
|
452
|
| Expr_ite (c, t, e) ->
|
453
|
type_subtyping_arg env in_main const c Type_predef.type_bool;
|
454
|
let ty = type_standard_args env in_main const [t; e] in
|
455
|
expr.expr_type <- ty;
|
456
|
ty
|
457
|
| Expr_appl (id, args, r) ->
|
458
|
(* application of non internal function is not legal in a constant
|
459
|
expression *)
|
460
|
(match r with
|
461
|
| None -> ()
|
462
|
| Some (x, l) ->
|
463
|
check_constant expr.expr_loc const false;
|
464
|
let expr_x = expr_of_ident x expr.expr_loc in
|
465
|
let typ_l =
|
466
|
Type_predef.type_clock
|
467
|
(type_const expr.expr_loc (Const_tag l)) in
|
468
|
type_subtyping_arg env in_main ~sub:false const expr_x typ_l);
|
469
|
let touts = type_appl env in_main expr.expr_loc const id args in
|
470
|
expr.expr_type <- touts;
|
471
|
touts
|
472
|
| Expr_fby (e1,e2)
|
473
|
| Expr_arrow (e1,e2) ->
|
474
|
(* fby/arrow is not legal in a constant expression *)
|
475
|
check_constant expr.expr_loc const false;
|
476
|
let ty = type_standard_args env in_main const [e1; e2] in
|
477
|
expr.expr_type <- ty;
|
478
|
ty
|
479
|
| Expr_pre e ->
|
480
|
(* pre is not legal in a constant expression *)
|
481
|
check_constant expr.expr_loc const false;
|
482
|
let ty = type_standard_args env in_main const [e] in
|
483
|
expr.expr_type <- ty;
|
484
|
ty
|
485
|
| Expr_when (e1,c,l) ->
|
486
|
(* when is not legal in a constant expression *)
|
487
|
check_constant expr.expr_loc const false;
|
488
|
let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in
|
489
|
let expr_c = expr_of_ident c expr.expr_loc in
|
490
|
type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
|
491
|
(*update_clock env in_main c expr.expr_loc typ_l;*)
|
492
|
let ty = type_standard_args env in_main const [e1] in
|
493
|
expr.expr_type <- ty;
|
494
|
ty
|
495
|
| Expr_merge (c,hl) ->
|
496
|
(* merge is not legal in a constant expression *)
|
497
|
check_constant expr.expr_loc const false;
|
498
|
let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in
|
499
|
let expr_c = expr_of_ident c expr.expr_loc in
|
500
|
let typ_l = Type_predef.type_clock typ_in in
|
501
|
type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
|
502
|
(*update_clock env in_main c expr.expr_loc typ_l;*)
|
503
|
expr.expr_type <- typ_out;
|
504
|
typ_out
|
505
|
in
|
506
|
Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr Types.print_ty resulting_ty);
|
507
|
resulting_ty
|
508
|
|
509
|
and type_branches env in_main loc const hl =
|
510
|
let typ_in = new_var () in
|
511
|
let typ_out = new_var () in
|
512
|
try
|
513
|
let used_labels =
|
514
|
List.fold_left (fun accu (t, h) ->
|
515
|
unify typ_in (type_const loc (Const_tag t));
|
516
|
type_subtyping_arg env in_main const h typ_out;
|
517
|
if List.mem t accu
|
518
|
then raise (Error (loc, Already_bound t))
|
519
|
else t :: accu) [] hl in
|
520
|
let type_labels = get_enum_type_tags (coretype_type typ_in) in
|
521
|
if List.sort compare used_labels <> List.sort compare type_labels
|
522
|
then let unbound_tag = List.find (fun t -> not (List.mem t used_labels)) type_labels in
|
523
|
raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag)))
|
524
|
else (typ_in, typ_out)
|
525
|
with Unify (t1, t2) ->
|
526
|
raise (Error (loc, Type_clash (t1,t2)))
|
527
|
(*
|
528
|
and update_clock env in_main id loc typ =
|
529
|
(*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "update_clock %s with %a@ " id print_ty typ);*)
|
530
|
try
|
531
|
let vdecl = List.find (fun v -> v.var_id = id) (snd env)
|
532
|
in vdecl.var_type <- typ
|
533
|
with
|
534
|
Not_found ->
|
535
|
raise (Error (loc, Unbound_value ("clock " ^ id)))
|
536
|
*)
|
537
|
(** [type_eq env eq] types equation [eq] in environment [env] *)
|
538
|
let type_eq env in_main undefined_vars eq =
|
539
|
(* Check undefined variables, type lhs *)
|
540
|
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
|
541
|
let ty_lhs = type_expr env in_main false expr_lhs in
|
542
|
(* Check multiple variable definitions *)
|
543
|
let define_var id uvars =
|
544
|
try
|
545
|
ignore(IMap.find id uvars);
|
546
|
IMap.remove id uvars
|
547
|
with Not_found ->
|
548
|
raise (Error (eq.eq_loc, Already_defined id))
|
549
|
in
|
550
|
(* check assignment of declared constant, assignment of clock *)
|
551
|
let ty_lhs =
|
552
|
type_of_type_list
|
553
|
(List.map2 (fun ty id ->
|
554
|
if get_static_value ty <> None
|
555
|
then raise (Error (eq.eq_loc, Assigned_constant id)) else
|
556
|
match get_clock_base_type ty with
|
557
|
| None -> ty
|
558
|
| Some ty -> ty)
|
559
|
(type_list_of_type ty_lhs) eq.eq_lhs) in
|
560
|
let undefined_vars =
|
561
|
List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in
|
562
|
(* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned
|
563
|
to a (always non-constant) lhs variable *)
|
564
|
type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;
|
565
|
undefined_vars
|
566
|
|
567
|
|
568
|
(* [type_coreclock env ck id loc] types the type clock declaration [ck]
|
569
|
in environment [env] *)
|
570
|
let type_coreclock env ck id loc =
|
571
|
match ck.ck_dec_desc with
|
572
|
| Ckdec_any | Ckdec_pclock (_,_) -> ()
|
573
|
| Ckdec_bool cl ->
|
574
|
let dummy_id_expr = expr_of_ident id loc in
|
575
|
let when_expr =
|
576
|
List.fold_left
|
577
|
(fun expr (x, l) ->
|
578
|
{expr_tag = new_tag ();
|
579
|
expr_desc= Expr_when (expr,x,l);
|
580
|
expr_type = new_var ();
|
581
|
expr_clock = Clocks.new_var true;
|
582
|
expr_delay = Delay.new_var ();
|
583
|
expr_loc=loc;
|
584
|
expr_annot = None})
|
585
|
dummy_id_expr cl
|
586
|
in
|
587
|
ignore (type_expr env false false when_expr)
|
588
|
|
589
|
let rec check_type_declaration loc cty =
|
590
|
match cty with
|
591
|
| Tydec_clock ty
|
592
|
| Tydec_array (_, ty) -> check_type_declaration loc ty
|
593
|
| Tydec_const tname ->
|
594
|
if not (Hashtbl.mem type_table cty)
|
595
|
then raise (Error (loc, Unbound_type tname));
|
596
|
| _ -> ()
|
597
|
|
598
|
let type_var_decl vd_env env vdecl =
|
599
|
check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
|
600
|
let eval_const id = Types.get_static_value (Env.lookup_value env id) in
|
601
|
let type_dim d =
|
602
|
begin
|
603
|
type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int;
|
604
|
Dimension.eval Basic_library.eval_env eval_const d;
|
605
|
end in
|
606
|
let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
|
607
|
let ty_status =
|
608
|
if vdecl.var_dec_const
|
609
|
then Type_predef.type_static (Dimension.mkdim_var ()) ty
|
610
|
else ty in
|
611
|
let new_env = Env.add_value env vdecl.var_id ty_status in
|
612
|
type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
|
613
|
vdecl.var_type <- ty_status;
|
614
|
new_env
|
615
|
|
616
|
let type_var_decl_list vd_env env l =
|
617
|
List.fold_left (type_var_decl vd_env) env l
|
618
|
|
619
|
let type_of_vlist vars =
|
620
|
let tyl = List.map (fun v -> v.var_type) vars in
|
621
|
type_of_type_list tyl
|
622
|
|
623
|
let add_vdecl vd_env vdecl =
|
624
|
if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env
|
625
|
then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
|
626
|
else vdecl::vd_env
|
627
|
|
628
|
let check_vd_env vd_env =
|
629
|
ignore (List.fold_left add_vdecl [] vd_env)
|
630
|
|
631
|
(** [type_node env nd loc] types node [nd] in environment env. The
|
632
|
location is used for error reports. *)
|
633
|
let type_node env nd loc =
|
634
|
let is_main = nd.node_id = !Options.main_node in
|
635
|
let vd_env_ol = nd.node_outputs@nd.node_locals in
|
636
|
let vd_env = nd.node_inputs@vd_env_ol in
|
637
|
check_vd_env vd_env;
|
638
|
let init_env = env in
|
639
|
let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in
|
640
|
let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in
|
641
|
let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in
|
642
|
let new_env = Env.overwrite env delta_env in
|
643
|
let undefined_vars_init =
|
644
|
List.fold_left
|
645
|
(fun uvs v -> IMap.add v.var_id () uvs)
|
646
|
IMap.empty vd_env_ol in
|
647
|
let undefined_vars =
|
648
|
List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init nd.node_eqs
|
649
|
in
|
650
|
(* Typing asserts *)
|
651
|
List.iter (fun assert_ ->
|
652
|
let assert_expr = assert_.assert_expr in
|
653
|
type_subtyping_arg (new_env, vd_env) is_main false assert_expr Type_predef.type_bool
|
654
|
) nd.node_asserts;
|
655
|
|
656
|
(* check that table is empty *)
|
657
|
if (not (IMap.is_empty undefined_vars)) then
|
658
|
raise (Error (loc, Undefined_var undefined_vars));
|
659
|
let ty_ins = type_of_vlist nd.node_inputs in
|
660
|
let ty_outs = type_of_vlist nd.node_outputs in
|
661
|
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
|
662
|
generalize ty_node;
|
663
|
(* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
|
664
|
nd.node_type <- ty_node;
|
665
|
Env.add_value env nd.node_id ty_node
|
666
|
|
667
|
let type_imported_node env nd loc =
|
668
|
let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in
|
669
|
let vd_env = nd.nodei_inputs@nd.nodei_outputs in
|
670
|
check_vd_env vd_env;
|
671
|
ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);
|
672
|
let ty_ins = type_of_vlist nd.nodei_inputs in
|
673
|
let ty_outs = type_of_vlist nd.nodei_outputs in
|
674
|
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
|
675
|
generalize ty_node;
|
676
|
(*
|
677
|
if (is_polymorphic ty_node) then
|
678
|
raise (Error (loc, Poly_imported_node nd.nodei_id));
|
679
|
*)
|
680
|
let new_env = Env.add_value env nd.nodei_id ty_node in
|
681
|
nd.nodei_type <- ty_node;
|
682
|
new_env
|
683
|
|
684
|
let type_top_consts env clist =
|
685
|
List.fold_left (fun env cdecl ->
|
686
|
let ty = type_const cdecl.const_loc cdecl.const_value in
|
687
|
let d =
|
688
|
if is_dimension_type ty
|
689
|
then dimension_of_const cdecl.const_loc cdecl.const_value
|
690
|
else Dimension.mkdim_var () in
|
691
|
let ty = Type_predef.type_static d ty in
|
692
|
let new_env = Env.add_value env cdecl.const_id ty in
|
693
|
cdecl.const_type <- ty;
|
694
|
new_env) env clist
|
695
|
|
696
|
let type_top_decl env decl =
|
697
|
match decl.top_decl_desc with
|
698
|
| Node nd -> (
|
699
|
try
|
700
|
type_node env nd decl.top_decl_loc
|
701
|
with Error (loc, err) as exc -> (
|
702
|
if !Options.global_inline then
|
703
|
Format.eprintf "Type error: failing node@.%a@.@?"
|
704
|
Printers.pp_node nd
|
705
|
;
|
706
|
raise exc)
|
707
|
)
|
708
|
| ImportedNode nd ->
|
709
|
type_imported_node env nd decl.top_decl_loc
|
710
|
| Consts clist ->
|
711
|
type_top_consts env clist
|
712
|
| Open _ -> env
|
713
|
|
714
|
let type_prog env decls =
|
715
|
try
|
716
|
List.fold_left type_top_decl env decls
|
717
|
with Failure _ as exc -> raise exc
|
718
|
|
719
|
(* Once the Lustre program is fully typed,
|
720
|
we must get back to the original description of dimensions,
|
721
|
with constant parameters, instead of unifiable internal variables. *)
|
722
|
|
723
|
(* The following functions aims at 'unevaluating' dimension expressions occuring in array types,
|
724
|
i.e. replacing unifiable second_order variables with the original static parameters.
|
725
|
Once restored in this formulation, dimensions may be meaningfully printed.
|
726
|
*)
|
727
|
let uneval_vdecl_generics vdecl =
|
728
|
if vdecl.var_dec_const
|
729
|
then
|
730
|
match get_static_value vdecl.var_type with
|
731
|
| None -> (Format.eprintf "internal error: %a@." Types.print_ty vdecl.var_type; assert false)
|
732
|
| Some d -> Dimension.uneval vdecl.var_id d
|
733
|
|
734
|
let uneval_node_generics vdecls =
|
735
|
List.iter uneval_vdecl_generics vdecls
|
736
|
|
737
|
let uneval_top_generics decl =
|
738
|
match decl.top_decl_desc with
|
739
|
| Node nd ->
|
740
|
uneval_node_generics (nd.node_inputs @ nd.node_outputs)
|
741
|
| ImportedNode nd ->
|
742
|
uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
|
743
|
| Consts clist -> ()
|
744
|
| Open _ -> ()
|
745
|
|
746
|
let uneval_prog_generics prog =
|
747
|
List.iter uneval_top_generics prog
|
748
|
|
749
|
let rec get_imported_node decls id =
|
750
|
match decls with
|
751
|
| [] -> assert false
|
752
|
| decl::q ->
|
753
|
(match decl.top_decl_desc with
|
754
|
| ImportedNode nd when id = nd.nodei_id -> decl
|
755
|
| _ -> get_imported_node q id)
|
756
|
|
757
|
let check_env_compat header declared computed =
|
758
|
uneval_prog_generics header;
|
759
|
Env.iter declared (fun k decl_type_k ->
|
760
|
let computed_t = instantiate (ref []) (ref [])
|
761
|
(try Env.lookup_value computed k
|
762
|
with Not_found ->
|
763
|
let loc = (get_imported_node header k).top_decl_loc in
|
764
|
raise (Error (loc, Declared_but_undefined k))) in
|
765
|
(*Types.print_ty Format.std_formatter decl_type_k;
|
766
|
Types.print_ty Format.std_formatter computed_t;*)
|
767
|
try_unify ~sub:true ~semi:true decl_type_k computed_t Location.dummy_loc
|
768
|
)
|
769
|
|
770
|
(* Local Variables: *)
|
771
|
(* compile-command:"make -C .." *)
|
772
|
(* End: *)
|