Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / typing.ml @ 45f0f48d

History | View | Annotate | Download (30.4 KB)

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