Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / typing.ml @ e8250987

History | View | Annotate | Download (38.2 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 8446bf03 ploc
open Lustre_types
26 22fe1c93 ploc
open Corelang
27
open Format
28
29 66359a5e ploc
30 217837e2 ploc
(* TODO general remark: expect in the add_vdelc, 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 66359a5e ploc
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 34d3f022 ploc
  struct
45 66359a5e ploc
46 34d3f022 ploc
    module TP = Type_predef.Make (T)
47
    include TP
48 66359a5e ploc
    
49 34d3f022 ploc
    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 22fe1c93 ploc
      try
167 34d3f022 ploc
        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 6afa892a xthirioux
    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 34d3f022 ploc
    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 22fe1c93 ploc
        else
215 34d3f022 ploc
          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 66359a5e ploc
      	 for numerical constants with non static ones for variables with
268
      	 possible machine types *)
269 34d3f022 ploc
          | 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 21485807 xthirioux
      try
276 34d3f022 ploc
        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 21485807 xthirioux
	List.iter (fun l -> Format.eprintf "used: %s@." l) used; *)
332 34d3f022 ploc
	     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 22fe1c93 ploc
   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 34d3f022 ploc
     *)
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 4a840259 xthirioux
   used during node applications and assignments *)
372 34d3f022 ploc
    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 22fe1c93 ploc
   - checking that const formal parameters match real const (maybe symbolic) arguments
381
   - checking type adequation between formal and real arguments
382 b616fe7a xthirioux
   An application may embed an homomorphic/internal function, in which case we need to split
383
   it in many calls
384 34d3f022 ploc
     *)
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 66359a5e ploc
      )
398 307c32f5 ploc
      
399 34d3f022 ploc
    (* 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 a38c681e xthirioux
   but possible homomorphic extension.
428
   [targs] is here a list of arguments' types. *)
429 34d3f022 ploc
    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 22fe1c93 ploc
    [env], expecting it to be [const] or not. *)
439 34d3f022 ploc
    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 5c1184ad ploc
       expression *)
497 34d3f022 ploc
           (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 307c32f5 ploc
           let touts = type_appl env in_main expr.expr_loc const id args_list in
504 34d3f022 ploc
           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 22fe1c93 ploc
     to a (always non-constant) lhs variable *)
598 34d3f022 ploc
      type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;
599
      undefined_vars
600 22fe1c93 ploc
601
602 34d3f022 ploc
    (* [type_coreclock env ck id loc] types the type clock declaration [ck]
603 22fe1c93 ploc
   in environment [env] *)
604 34d3f022 ploc
    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 217837e2 ploc
    let type_spec env spec =
673
      let vd_env = spec.consts @ spec.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) spec.stmts  in
678
      let undefined_vars_init =
679
        List.fold_left
680
          (fun uvs v -> ISet.add v.var_id uvs)
681
          ISet.empty spec.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
      
690 34d3f022 ploc
      (*TODO 
691
        enrich env locally with locals and consts
692
        type each pre/post as a boolean expr
693
        I don't know if we want to update the global env with locally typed variables. 
694
        For the moment, returning the provided env           
695
       *)
696
      env
697
      
698
    (** [type_node env nd loc] types node [nd] in environment env. The
699
    location is used for error reports. *)
700
    let type_node env nd loc =
701
      let is_main = nd.node_id = !Options.main_node in
702
      let vd_env_ol = nd.node_outputs@nd.node_locals in
703
      let vd_env =  nd.node_inputs@vd_env_ol in
704
      check_vd_env vd_env;
705
      let init_env = env in
706
      let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in
707
      let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in
708
      let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in
709
      let new_env = Env.overwrite env delta_env in
710
      let undefined_vars_init =
711 22fe1c93 ploc
        List.fold_left
712 34d3f022 ploc
          (fun uvs v -> ISet.add v.var_id uvs)
713
          ISet.empty vd_env_ol in
714
      let undefined_vars =
715
        let eqs, auts = get_node_eqs nd in
716
        (* TODO XXX: il faut typer les handlers de l'automate *)
717
        List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init eqs
718 22fe1c93 ploc
      in
719 34d3f022 ploc
      (* Typing asserts *)
720
      List.iter (fun assert_ ->
721
          let assert_expr =  assert_.assert_expr in
722
          type_subtyping_arg (new_env, vd_env) is_main false assert_expr (* Type_predef. *)type_bool
723
        )  nd.node_asserts;
724
      (* Typing spec/contracts *)
725 217837e2 ploc
      (match nd.node_spec with None -> () | Some spec -> ignore (type_spec new_env spec));
726 34d3f022 ploc
      (* Typing annots *)
727
      List.iter (fun annot ->
728
          List.iter (fun (_, eexpr) -> ignore (type_eexpr (new_env, vd_env) eexpr)) annot.annots
729
        ) nd.node_annot;
730
      
731
      (* check that table is empty *)
732
      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
733
      let undefined_vars = ISet.diff undefined_vars local_consts in
734
      if (not (ISet.is_empty undefined_vars)) then
735
        raise (Error (loc, Undefined_var undefined_vars));
736
      let ty_ins = type_of_vlist nd.node_inputs in
737
      let ty_outs = type_of_vlist nd.node_outputs in
738
      let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
739
      generalize ty_node;
740
      (* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
741
      nd.node_type <- Expr_type_hub.export ty_node;
742
      Env.add_value env nd.node_id ty_node
743
744
    let type_imported_node env nd loc =
745
      let vd_env = nd.nodei_inputs@nd.nodei_outputs in
746
      check_vd_env vd_env;
747 217837e2 ploc
      let delta_env = type_var_decl_list vd_env env nd.nodei_inputs in
748
      let delta_env = type_var_decl_list vd_env delta_env nd.nodei_outputs in
749
      let new_env = Env.overwrite env delta_env in
750
      (* Typing spec *)
751
      (match nd.nodei_spec with None -> () | Some spec -> ignore (type_spec new_env spec)); 
752 34d3f022 ploc
      let ty_ins = type_of_vlist nd.nodei_inputs in
753
      let ty_outs = type_of_vlist nd.nodei_outputs in
754
      let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
755
      generalize ty_node;
756
      (*
757 22fe1c93 ploc
  if (is_polymorphic ty_node) then
758
    raise (Error (loc, Poly_imported_node nd.nodei_id));
759 34d3f022 ploc
       *)
760
      let new_env = Env.add_value env nd.nodei_id ty_node in
761
      nd.nodei_type <- Expr_type_hub.export ty_node;
762
      new_env
763
764
    let type_top_const env cdecl =
765
      let ty = type_const cdecl.const_loc cdecl.const_value in
766
      let d =
767
        if is_dimension_type ty
768
        then dimension_of_const cdecl.const_loc cdecl.const_value
769
        else Dimension.mkdim_var () in
770
      let ty = (* Type_predef. *)type_static d ty in
771
      let new_env = Env.add_value env cdecl.const_id ty in
772
      cdecl.const_type <- Expr_type_hub.export ty;
773
      new_env
774
775
    let type_top_consts env clist =
776
      List.fold_left type_top_const env clist
777
778
    let rec type_top_decl env decl =
779
      match decl.top_decl_desc with
780
      | Node nd -> (
781
        try
782
          type_node env nd decl.top_decl_loc
783
        with Error (loc, err) as exc -> (
784
          if !Options.global_inline then
785
	    Format.eprintf "Type error: failing node@.%a@.@?"
786
	      Printers.pp_node nd
787
          ;
788
            raise exc)
789
      )
790
      | ImportedNode nd ->
791
         type_imported_node env nd decl.top_decl_loc
792
      | Const c ->
793
         type_top_const env c
794
      | TypeDef _ -> List.fold_left type_top_decl env (consts_of_enum_type decl)
795 19a1e66b ploc
      | Include _ | Open _  -> env
796 0d54d8a8 ploc
    
797 34d3f022 ploc
    let get_type_of_call decl =
798
      match decl.top_decl_desc with
799
      | Node nd         ->
800
         let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.node_type) in
801
         type_list_of_type in_typ, type_list_of_type out_typ
802
      | ImportedNode nd ->
803
         let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.nodei_type) in
804
         type_list_of_type in_typ, type_list_of_type out_typ
805
      | _               -> assert false
806
807
    let type_prog env decls =
808
      try
809
        List.fold_left type_top_decl env decls
810
      with Failure _ as exc -> raise exc
811
812
    (* Once the Lustre program is fully typed, we must get back to the
813
       original description of dimensions, with constant parameters,
814
       instead of unifiable internal variables. *)
815
816
    (* The following functions aims at 'unevaluating' dimension
817
       expressions occuring in array types, i.e. replacing unifiable
818
       second_order variables with the original static parameters.
819
       Once restored in this formulation, dimensions may be
820
       meaningfully printed.  *)
821
    let uneval_vdecl_generics vdecl =
822
      if vdecl.var_dec_const
823
      then
824
        match get_static_value (Expr_type_hub.import vdecl.var_type) with
825
        | None   -> (Format.eprintf "internal error: %a@." (* Types. *)print_ty (Expr_type_hub.import vdecl.var_type); assert false)
826
        | Some d -> Dimension.uneval vdecl.var_id d
827
828
    let uneval_node_generics vdecls =
829
      List.iter uneval_vdecl_generics vdecls
830
831
    let uneval_spec_generics spec =
832
      List.iter uneval_vdecl_generics (spec.consts@spec.locals)
833
      
834
    let uneval_top_generics decl =
835
      match decl.top_decl_desc with
836
      | Node nd ->
837
         uneval_node_generics (nd.node_inputs @ nd.node_outputs)
838
      | ImportedNode nd ->
839
         uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
840 19a1e66b ploc
      | Const _ | TypeDef _ | Open _ | Include _ 
841 34d3f022 ploc
        -> ()
842
843
    let uneval_prog_generics prog =
844
      List.iter uneval_top_generics prog
845
846
    let rec get_imported_symbol decls id =
847
      match decls with
848
      | [] -> assert false
849
      | decl::q ->
850
         (match decl.top_decl_desc with
851
          | ImportedNode nd when id = nd.nodei_id && decl.top_decl_itf -> decl
852
          | Const c when id = c.const_id && decl.top_decl_itf -> decl
853
          | TypeDef _ -> get_imported_symbol (consts_of_enum_type decl @ q) id
854
          | _ -> get_imported_symbol q id)
855
856
    let check_env_compat header declared computed = 
857
      uneval_prog_generics header;
858
      Env.iter declared (fun k decl_type_k ->
859
          let loc = (get_imported_symbol header k).top_decl_loc in 
860
          let computed_t =
861
            instantiate (ref []) (ref []) 
862
	      (try Env.lookup_value computed k
863
	       with Not_found -> raise (Error (loc, Declared_but_undefined k))) in
864
          (*Types.print_ty Format.std_formatter decl_type_k;
865 ef34b4ae xthirioux
      Types.print_ty Format.std_formatter computed_t;*)
866 34d3f022 ploc
          try_unify ~sub:true ~semi:true decl_type_k computed_t loc
867
        )
868
869
    let check_typedef_top decl =
870
      (*Format.eprintf "check_typedef %a@." Printers.pp_short_decl decl;*)
871
      (*Format.eprintf "%a" Printers.pp_typedef (typedef_of_top decl);*)
872
      (*Format.eprintf "%a" Corelang.print_type_table ();*)
873
      match decl.top_decl_desc with
874
      | TypeDef ty ->
875
         let owner = decl.top_decl_owner in
876
         let itf = decl.top_decl_itf in
877
         let decl' =
878
           try Hashtbl.find type_table (Tydec_const (typedef_of_top decl).tydef_id)
879
           with Not_found -> raise (Error (decl.top_decl_loc, Declared_but_undefined ("type "^ ty.tydef_id))) in
880
         let owner' = decl'.top_decl_owner in
881
         (*Format.eprintf "def owner = %s@.decl owner = %s@." owner' owner;*)
882
         let itf' = decl'.top_decl_itf in
883
         (match decl'.top_decl_desc with
884
          | Const _ | Node _ | ImportedNode _ -> assert false
885
          | TypeDef ty' when coretype_equal ty'.tydef_desc ty.tydef_desc && owner' = owner && itf && (not itf') -> ()
886
          | _ -> raise (Error (decl.top_decl_loc, Type_mismatch ty.tydef_id)))
887
      | _  -> ()
888
889
    let check_typedef_compat header =
890
      List.iter check_typedef_top header
891
  end
892 5c1184ad ploc
893 66359a5e ploc
include  Make(Types.Main) (struct
894 34d3f022 ploc
             type type_expr  = Types.Main.type_expr
895
             let import x = x
896
             let export x = x
897
           end)
898
             (* Local Variables: *)
899
             (* compile-command:"make -C .." *)
900 22fe1c93 ploc
(* End: *)