Project

General

Profile

Download (37.4 KB) Statistics
| Branch: | Tag: | Revision:
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT - LIFL             *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *) 
10
(*  This file was originally from the Prelude compiler              *)
11
(*                                                                  *) 
12
(********************************************************************)
13

    
14
(** Main typing module. Classic inference algorithm with destructive
15
    unification. *)
16

    
17
let debug fmt args = () (* Format.eprintf "%a"  *)
18
(* Though it shares similarities with the clock calculus module, no code
19
    is shared.  Simple environments, very limited identifier scoping, no
20
    identifier redefinition allowed. *)
21

    
22
open Utils
23
(* Yes, opening both modules is dirty as some type names will be
24
   overwritten, yet this makes notations far lighter.*)
25
open Lustre_types
26
open Corelang
27
open Format
28

    
29

    
30
module type EXPR_TYPE_HUB =
31
sig
32
  type type_expr 
33
  val import: Types.Main.type_expr -> type_expr
34
  val export: type_expr -> Types.Main.type_expr 
35
end
36

    
37
module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.type_expr) =  
38
  struct
39

    
40
    module TP = Type_predef.Make (T)
41
    include TP
42
    
43
    let pp_typing_env fmt env =
44
      Env.pp_env print_ty fmt env
45

    
46
    (****************************************************************)
47
    (* Generic functions: occurs, instantiate and generalize         *)
48
    (****************************************************************)
49
      
50
    (** [occurs tvar ty] returns true if the type variable [tvar]
51
       occurs in type [ty]. False otherwise. *)
52
    let rec occurs tvar ty =
53
      let ty = repr ty in
54
      match type_desc ty with
55
      | Tvar -> ty=tvar
56
      | Tarrow (t1, t2) ->
57
         (occurs tvar t1) || (occurs tvar t2)
58
      | Ttuple tl ->
59
         List.exists (occurs tvar) tl
60
      | Tstruct fl ->
61
         List.exists (fun (f, t) -> occurs tvar t) fl
62
      | Tarray (_, t)
63
        | Tstatic (_, t)
64
        | Tclock t
65
        | Tlink t -> occurs tvar t
66
      | Tenum _ | Tconst _ | Tunivar | Tbasic _ -> false
67

    
68
    (** Promote monomorphic type variables to polymorphic type
69
       variables. *)
70
    (* Generalize by side-effects *)
71
    let rec generalize ty =
72
      match type_desc ty with
73
      | Tvar ->
74
         (* No scopes, always generalize *)
75
         ty.tdesc <- Tunivar
76
      | Tarrow (t1,t2) ->
77
         generalize t1; generalize t2
78
      | Ttuple tl ->
79
         List.iter generalize tl
80
      | Tstruct fl ->
81
         List.iter (fun (f, t) -> generalize t) fl
82
      | Tstatic (d, t)
83
        | Tarray (d, t) -> Dimension.generalize d; generalize t
84
      | Tclock t
85
        | Tlink t ->
86
         generalize t
87
      | Tenum _ | Tconst _ | Tunivar | Tbasic _ -> ()
88

    
89
    (** Downgrade polymorphic type variables to monomorphic type
90
       variables *)
91
    let rec instantiate inst_vars inst_dim_vars ty =
92
      let ty = repr ty in
93
      match ty.tdesc with
94
      | Tenum _ | Tconst _ | Tvar | Tbasic _  -> ty
95
      | Tarrow (t1,t2) ->
96
         {ty with tdesc =
97
                    Tarrow ((instantiate inst_vars inst_dim_vars t1), (instantiate inst_vars inst_dim_vars t2))}
98
      | Ttuple tlist ->
99
         {ty with tdesc = Ttuple (List.map (instantiate inst_vars inst_dim_vars) tlist)}
100
      | Tstruct flist ->
101
         {ty with tdesc = Tstruct (List.map (fun (f, t) -> (f, instantiate inst_vars inst_dim_vars t)) flist)}
102
      | Tclock t ->
103
	 {ty with tdesc = Tclock (instantiate inst_vars inst_dim_vars t)}
104
      | Tstatic (d, t) ->
105
	 {ty with tdesc = Tstatic (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)}
106
      | Tarray (d, t) ->
107
	 {ty with tdesc = Tarray (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)}
108
      | Tlink t ->
109
	 (* should not happen *)
110
	 {ty with tdesc = Tlink (instantiate inst_vars inst_dim_vars t)}
111
      | Tunivar ->
112
         try
113
           List.assoc ty.tid !inst_vars
114
         with Not_found ->
115
           let var = new_var () in
116
	   inst_vars := (ty.tid, var)::!inst_vars;
117
	   var
118

    
119

    
120

    
121
    let basic_coretype_type t =
122
      if is_real_type t then Tydec_real else
123
        if is_int_type t then Tydec_int else
124
          if is_bool_type t then Tydec_bool else
125
	    assert false
126

    
127
    (* [type_coretype cty] types the type declaration [cty] *)
128
    let rec type_coretype type_dim cty =
129
      match (*get_repr_type*) cty with
130
      | Tydec_any -> new_var ()
131
      | Tydec_int -> type_int
132
      | Tydec_real -> (* Type_predef. *)type_real
133
      (* | Tydec_float -> Type_predef.type_real *)
134
      | Tydec_bool -> (* Type_predef. *)type_bool
135
      | Tydec_clock ty -> (* Type_predef. *)type_clock (type_coretype type_dim ty)
136
      | Tydec_const c -> (* Type_predef. *)type_const c
137
      | Tydec_enum tl -> (* Type_predef. *)type_enum tl
138
      | Tydec_struct fl -> (* Type_predef. *)type_struct (List.map (fun (f, ty) -> (f, type_coretype type_dim ty)) fl)
139
      | Tydec_array (d, ty) ->
140
         begin
141
           let d = Dimension.copy (ref []) d in
142
           type_dim d;
143
           (* Type_predef. *)type_array d (type_coretype type_dim ty)
144
         end
145

    
146
    (* [coretype_type] is the reciprocal of [type_typecore] *)
147
    let rec coretype_type ty =
148
      match (repr ty).tdesc with
149
      | Tvar           -> Tydec_any
150
      | Tbasic _       -> basic_coretype_type ty
151
      | Tconst c       -> Tydec_const c
152
      | Tclock t       -> Tydec_clock (coretype_type t)
153
      | Tenum tl       -> Tydec_enum tl
154
      | Tstruct fl     -> Tydec_struct (List.map (fun (f, t) -> (f, coretype_type t)) fl)
155
      | Tarray (d, t)  -> Tydec_array (d, coretype_type t)
156
      | Tstatic (_, t) -> coretype_type t
157
      | _         -> assert false
158

    
159
    let get_coretype_definition tname =
160
      try
161
        let top = Hashtbl.find type_table (Tydec_const tname) in
162
        match top.top_decl_desc with
163
        | TypeDef tdef -> tdef.tydef_desc
164
        | _ -> assert false
165
      with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname))
166

    
167
    let get_type_definition tname =
168
      type_coretype (fun d -> ()) (get_coretype_definition tname)
169

    
170
    (* Equality on ground types only *)
171
    (* Should be used between local variables which must have a ground type *)
172
    let rec eq_ground t1 t2 =
173
      let t1 = repr t1 in
174
      let t2 = repr t2 in
175
      t1==t2 ||
176
        match t1.tdesc, t2.tdesc with
177
        | Tbasic t1, Tbasic t2 when t1 == t2 -> true
178
        | Tenum tl, Tenum tl' when tl == tl' -> true
179
        | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' -> List.for_all2 eq_ground tl tl'
180
        | 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'
181
        | (Tconst t, _) ->
182
           let def_t = get_type_definition t in
183
           eq_ground def_t t2
184
        | (_, Tconst t)  ->
185
           let def_t = get_type_definition t in
186
           eq_ground t1 def_t
187
        | Tarrow (t1,t2), Tarrow (t1',t2') -> eq_ground t1 t1' && eq_ground t2 t2'
188
        | Tclock t1', Tclock t2' -> eq_ground t1' t2'
189
        | Tstatic (e1, t1'), Tstatic (e2, t2')
190
          | Tarray (e1, t1'), Tarray (e2, t2') -> Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2'
191
        | _ -> false
192

    
193
    (** [unify t1 t2] unifies types [t1] and [t2]
194
    using standard destructive unification.
195
    Raises [Unify (t1,t2)] if the types are not unifiable.
196
    [t1] is a expected/formal/spec type, [t2] is a computed/real/implem type,
197
    so in case of unification error: expected type [t1], got type [t2].
198
    If [sub]-typing is allowed, [t2] may be a subtype of [t1].
199
    If [semi] unification is required,
200
    [t1] should furthermore be an instance of [t2]
201
    and constants are handled differently.*)
202
    let unify ?(sub=false) ?(semi=false) t1 t2 =
203
      let rec unif t1 t2 =
204
        let t1 = repr t1 in
205
        let t2 = repr t2 in
206
        if t1==t2 then
207
          ()
208
        else
209
          match t1.tdesc,t2.tdesc with
210
          (* strictly subtyping cases first *)
211
          | _ , Tclock t2 when sub && (get_clock_base_type t1 = None) ->
212
	     unif t1 t2
213
          | _ , Tstatic (d2, t2) when sub && (get_static_value t1 = None) ->
214
	     unif t1 t2
215
          (* This case is not mandatory but will keep "older" types *)
216
          | Tvar, Tvar ->
217
             if t1.tid < t2.tid then
218
               t2.tdesc <- Tlink t1
219
             else
220
               t1.tdesc <- Tlink t2
221
          | Tvar, _ when (not semi) && (not (occurs t1 t2)) ->
222
             t1.tdesc <- Tlink t2
223
          | _, Tvar when (not (occurs t2 t1)) ->
224
             t2.tdesc <- Tlink t1
225
          | Tarrow (t1,t2), Tarrow (t1',t2') ->
226
	     begin
227
               unif t2 t2';
228
	       unif t1' t1
229
	     end
230
          | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->
231
	     List.iter2 unif tl tl'
232
          | Ttuple [t1]        , _                  -> unif t1 t2
233
          | _                  , Ttuple [t2]        -> unif t1 t2
234
          | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->
235
	     List.iter2 (fun (_, t) (_, t') -> unif t t') fl fl'
236
          | Tclock _, Tstatic _
237
            | Tstatic _, Tclock _ -> raise (Unify (t1, t2))
238
          | Tclock t1', Tclock t2' -> unif t1' t2'
239
          | Tbasic t1, Tbasic t2 when t1 == t2 -> ()
240
          | Tunivar, _ | _, Tunivar -> ()
241
          | (Tconst t, _) ->
242
	     let def_t = get_type_definition t in
243
	     unif def_t t2
244
          | (_, Tconst t)  ->
245
	     let def_t = get_type_definition t in
246
	     unif t1 def_t
247
          | Tenum tl, Tenum tl' when tl == tl' -> ()
248
          | Tstatic (e1, t1'), Tstatic (e2, t2')
249
            | Tarray (e1, t1'), Tarray (e2, t2') ->
250
	     let eval_const =
251
	       if semi
252
	       then (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c))
253
	       else (fun c -> None) in
254
	     begin
255
	       unif t1' t2';
256
	       Dimension.eval Basic_library.eval_env eval_const e1;
257
	       Dimension.eval Basic_library.eval_env eval_const e2;
258
	       Dimension.unify ~semi:semi e1 e2;
259
	     end
260
          (* Special cases for machine_types. Rules to unify static types infered
261
      	 for numerical constants with non static ones for variables with
262
      	 possible machine types *)
263
          | Tbasic bt1, Tbasic bt2 when BasicT.is_unifiable bt1 bt2 -> BasicT.unify bt1 bt2
264
          | _,_ -> raise (Unify (t1, t2))
265
      in unif t1 t2
266

    
267
    (* Expected type ty1, got type ty2 *)
268
    let try_unify ?(sub=false) ?(semi=false) ty1 ty2 loc =
269
      try
270
        (*Format.eprintf "try_unify %B %B %a %a@." sub semi print_ty ty1 print_ty ty2;*)
271
        unify ~sub:sub ~semi:semi ty1 ty2
272
      with
273
      | Unify _ ->
274
         raise (Error (loc, Type_clash (ty1,ty2)))
275
      | Dimension.Unify _ ->
276
         raise (Error (loc, Type_clash (ty1,ty2)))
277

    
278

    
279
    (************************************************)
280
    (* Typing function for each basic AST construct *)
281
    (************************************************)
282

    
283
    let rec type_struct_const_field ?(is_annot=false) loc (label, c) =
284
      if Hashtbl.mem field_table label
285
      then let tydef = Hashtbl.find field_table label in
286
           let tydec = (typedef_of_top tydef).tydef_desc in 
287
           let tydec_struct = get_struct_type_fields tydec in
288
           let ty_label = type_coretype (fun d -> ()) (List.assoc label tydec_struct) in
289
           begin
290
	     try_unify ty_label (type_const ~is_annot loc c) loc;
291
	     type_coretype (fun d -> ()) tydec
292
           end
293
      else raise (Error (loc, Unbound_value ("struct field " ^ label)))
294

    
295
    and type_const ?(is_annot=false) loc c = 
296
      match c with
297
      | Const_int _     -> (* Type_predef. *)type_int
298
      | Const_real _    -> (* Type_predef. *)type_real
299
      | Const_array ca  -> let d = Dimension.mkdim_int loc (List.length ca) in
300
		           let ty = new_var () in
301
		           List.iter (fun e -> try_unify ty (type_const ~is_annot loc e) loc) ca;
302
		           (* Type_predef. *)type_array d ty
303
      | Const_tag t     ->
304
         if Hashtbl.mem tag_table t
305
         then 
306
           let tydef = typedef_of_top (Hashtbl.find tag_table t) in
307
           let tydec =
308
	     if is_user_type tydef.tydef_desc
309
	     then Tydec_const tydef.tydef_id
310
	     else tydef.tydef_desc in
311
           type_coretype (fun d -> ()) tydec
312
         else raise (Error (loc, Unbound_value ("enum tag " ^ t)))
313
      | Const_struct fl ->
314
         let ty_struct = new_var () in
315
         begin
316
           let used =
317
	     List.fold_left
318
	       (fun acc (l, c) ->
319
	         if List.mem l acc
320
	         then raise (Error (loc, Already_bound ("struct field " ^ l)))
321
	         else try_unify ty_struct (type_struct_const_field ~is_annot loc (l, c)) loc; l::acc)
322
	       [] fl in
323
           try
324
	     let total = List.map fst (get_struct_type_fields (coretype_type ty_struct)) in
325
             (*	List.iter (fun l -> Format.eprintf "total: %s@." l) total;
326
	List.iter (fun l -> Format.eprintf "used: %s@." l) used; *)
327
	     let undef = List.find (fun l -> not (List.mem l used)) total
328
	     in raise (Error (loc, Unbound_value ("struct field " ^ undef)))
329
           with Not_found -> 
330
	     ty_struct
331
         end
332
      | Const_string _ | Const_modeid _     -> 
333
         if is_annot then (* Type_predef. *)type_string else  assert false (* string datatype should only appear in annotations *)
334

    
335
    (* The following typing functions take as parameter an environment [env]
336
   and whether the element being typed is expected to be constant [const]. 
337
   [env] is a pair composed of:
338
  - a map from ident to type, associating to each ident, i.e. 
339
    variables, constants and (imported) nodes, its type including whether
340
    it is constant or not. This latter information helps in checking constant 
341
    propagation policy in Lustre.
342
  - a vdecl list, in order to modify types of declared variables that are
343
    later discovered to be clocks during the typing process.
344
     *)
345
    let check_constant loc const_expected const_real =
346
      if const_expected && not const_real
347
      then raise (Error (loc, Not_a_constant))
348

    
349
    let rec type_add_const env const arg targ =
350
      (*Format.eprintf "Typing.type_add_const %a %a@." Printers.pp_expr arg Types.print_ty targ;*)
351
      if const
352
      then let d =
353
	     if is_dimension_type targ
354
	     then dimension_of_expr arg
355
	     else Dimension.mkdim_var () in
356
           let eval_const id = (* Types. *)get_static_value (Env.lookup_value (fst env) id) in
357
           Dimension.eval Basic_library.eval_env eval_const d;
358
           let real_static_type = (* Type_predef. *)type_static d ((* Types. *)dynamic_type targ) in
359
           (match (* Types. *)get_static_value targ with
360
            | None    -> ()
361
            | Some d' -> try_unify targ real_static_type arg.expr_loc);
362
           real_static_type
363
      else targ
364

    
365
    (* emulates a subtyping relation between types t and (d : t),
366
   used during node applications and assignments *)
367
    and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =
368
      let loc = real_arg.expr_loc in
369
      let const = const || ((* Types. *)get_static_value formal_type <> None) in
370
      let real_type = type_add_const env const real_arg (type_expr env in_main const real_arg) in
371
      (*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;*)
372
      try_unify ~sub:sub formal_type real_type loc
373

    
374
    (* typing an application implies:
375
   - checking that const formal parameters match real const (maybe symbolic) arguments
376
   - checking type adequation between formal and real arguments
377
   An application may embed an homomorphic/internal function, in which case we need to split
378
   it in many calls
379
     *)
380
    and type_appl env in_main loc const f args =
381
      let targs = List.map (type_expr env in_main const) args in
382
      if Basic_library.is_homomorphic_fun f && List.exists is_tuple_type targs
383
      then
384
        try
385
          let targs = Utils.transpose_list (List.map type_list_of_type targs) in
386
          (* Types. *)type_of_type_list (List.map (type_simple_call env in_main loc const f) targs)
387
        with 
388
          Utils.TransposeError (l, l') -> raise (Error (loc, WrongMorphism (l, l')))
389
	                                
390
      else (
391
        type_dependent_call env in_main loc const f (List.combine args targs)
392
      )
393
      
394
    (* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *)
395
    and type_dependent_call env in_main loc const f targs =
396
      (* Format.eprintf "Typing.type_dependent_call %s@." f; *)
397
      let tins, touts = new_var (), new_var () in
398
      (* Format.eprintf "tin=%a, tout=%a@." print_ty tins print_ty touts; *)
399
      let tfun = (* Type_predef. *)type_arrow tins touts in
400
      (* Format.eprintf "fun=%a@." print_ty tfun; *)
401
      type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
402
      (* Format.eprintf "type subtyping@."; *)
403
      let tins = type_list_of_type tins in
404
      if List.length targs <> List.length tins then
405
        raise (Error (loc, WrongArity (List.length tins, List.length targs)))
406
      else
407
        begin
408
          List.iter2 (
409
	      fun (a,t) ti ->
410
	      let t' = type_add_const env (const || (* Types. *)get_static_value ti <> None) a t in
411
	      (* Format.eprintf "uniying ti=%a t'=%a touts=%a@." print_ty ti print_ty t' print_ty touts;  *)
412
	      try_unify ~sub:true ti t' a.expr_loc;
413
	    (* Format.eprintf "unified ti=%a t'=%a touts=%a@." print_ty ti print_ty t' print_ty touts;  *)
414
	      
415
            )
416
	    targs
417
	    tins;
418
          touts
419
        end
420

    
421
    (* type a simple call without dependent types 
422
   but possible homomorphic extension.
423
   [targs] is here a list of arguments' types. *)
424
    and type_simple_call env in_main loc const f targs =
425
      let tins, touts = new_var (), new_var () in
426
      let tfun = (* Type_predef. *)type_arrow tins touts in
427
      type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
428
      (*Format.eprintf "try unify %a %a@." Types.print_ty tins Types.print_ty (type_of_type_list targs);*)
429
      try_unify ~sub:true tins (type_of_type_list targs) loc;
430
      touts
431

    
432
    (** [type_expr env in_main expr] types expression [expr] in environment
433
    [env], expecting it to be [const] or not. *)
434
    and type_expr ?(is_annot=false) env in_main const expr =
435
      let resulting_ty = 
436
        match expr.expr_desc with
437
        | Expr_const c ->
438
           let ty = type_const ~is_annot expr.expr_loc c in
439
           let ty = (* Type_predef. *)type_static (Dimension.mkdim_var ()) ty in
440
           expr.expr_type <- Expr_type_hub.export ty;
441
           ty
442
        | Expr_ident v ->
443
           let tyv =
444
             try
445
               Env.lookup_value (fst env) v
446
             with Not_found ->
447
	       Format.eprintf "Failure in typing expr %a. Not in typing environement@." Printers.pp_expr expr;
448
               raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v)))
449
           in
450
           let ty = instantiate (ref []) (ref []) tyv in
451
           let ty' =
452
             if const
453
             then (* Type_predef. *)type_static (Dimension.mkdim_var ()) (new_var ())
454
             else new_var () in
455
           try_unify ty ty' expr.expr_loc;
456
           expr.expr_type <- Expr_type_hub.export ty;
457
           ty 
458
        | Expr_array elist ->
459
           let ty_elt = new_var () in
460
           List.iter (fun e -> try_unify ty_elt (type_appl env in_main expr.expr_loc const "uminus" [e]) e.expr_loc) elist;
461
           let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in
462
           let ty = (* Type_predef. *)type_array d ty_elt in
463
           expr.expr_type <- Expr_type_hub.export ty;
464
           ty
465
        | Expr_access (e1, d) ->
466
           type_subtyping_arg env in_main false (* not necessary a constant *) (expr_of_dimension d) (* Type_predef. *)type_int;
467
           let ty_elt = new_var () in
468
           let d = Dimension.mkdim_var () in
469
           type_subtyping_arg env in_main const e1 ((* Type_predef. *)type_array d ty_elt);
470
           expr.expr_type <- Expr_type_hub.export ty_elt;
471
           ty_elt
472
        | Expr_power (e1, d) ->
473
           let eval_const id = (* Types. *)get_static_value (Env.lookup_value (fst env) id) in
474
           type_subtyping_arg env in_main true (expr_of_dimension d) (* Type_predef. *)type_int;
475
           Dimension.eval Basic_library.eval_env eval_const d;
476
           let ty_elt = type_appl env in_main expr.expr_loc const "uminus" [e1] in
477
           let ty = (* Type_predef. *)type_array d ty_elt in
478
           expr.expr_type <- Expr_type_hub.export ty;
479
           ty
480
        | Expr_tuple elist ->
481
           let ty = new_ty (Ttuple (List.map (type_expr ~is_annot env in_main const) elist)) in
482
           expr.expr_type <- Expr_type_hub.export ty;
483
           ty
484
        | Expr_ite (c, t, e) ->
485
           type_subtyping_arg env in_main const c (* Type_predef. *)type_bool;
486
           let ty = type_appl env in_main expr.expr_loc const "+" [t; e] in
487
           expr.expr_type <- Expr_type_hub.export ty;
488
           ty
489
        | Expr_appl (id, args, r) ->
490
           (* application of non internal function is not legal in a constant
491
       expression *)
492
           (match r with
493
            | None        -> ()
494
            | Some c -> 
495
               check_constant expr.expr_loc const false;	
496
               type_subtyping_arg env in_main const c (* Type_predef. *)type_bool);
497
           let args_list = expr_list_of_expr args in
498
           let touts = type_appl env in_main expr.expr_loc const id args_list in
499
           let targs = new_ty (Ttuple (List.map (fun a -> Expr_type_hub.import a.expr_type) args_list)) in
500
           args.expr_type <- Expr_type_hub.export targs;
501
           expr.expr_type <- Expr_type_hub.export touts;
502
           touts
503
        | Expr_fby (e1,e2)
504
          | Expr_arrow (e1,e2) ->
505
           (* fby/arrow is not legal in a constant expression *)
506
           check_constant expr.expr_loc const false;
507
           let ty = type_appl env in_main expr.expr_loc const "+" [e1; e2] in
508
           expr.expr_type <- Expr_type_hub.export ty;
509
           ty
510
        | Expr_pre e ->
511
           (* pre is not legal in a constant expression *)
512
           check_constant expr.expr_loc const false;
513
           let ty = type_appl env in_main expr.expr_loc const "uminus" [e] in
514
           expr.expr_type <- Expr_type_hub.export ty;
515
           ty
516
        | Expr_when (e1,c,l) ->
517
           (* when is not legal in a constant expression *)
518
           check_constant expr.expr_loc const false;
519
           let typ_l = (* Type_predef. *)type_clock (type_const ~is_annot expr.expr_loc (Const_tag l)) in
520
           let expr_c = expr_of_ident c expr.expr_loc in
521
           type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
522
           let ty = type_appl env in_main expr.expr_loc const "uminus" [e1] in
523
           expr.expr_type <- Expr_type_hub.export ty;
524
           ty
525
        | Expr_merge (c,hl) ->
526
           (* merge is not legal in a constant expression *)
527
           check_constant expr.expr_loc const false;
528
           let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in
529
           let expr_c = expr_of_ident c expr.expr_loc in
530
           let typ_l = (* Type_predef. *)type_clock typ_in in
531
           type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
532
           expr.expr_type <- Expr_type_hub.export typ_out;
533
           typ_out
534
      in 
535
      Log.report ~level:4 (fun fmt -> Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr (* Types. *)print_ty resulting_ty);
536
      resulting_ty
537

    
538
    and type_branches ?(is_annot=false) env in_main loc const hl =
539
      let typ_in = new_var () in
540
      let typ_out = new_var () in
541
      try
542
        let used_labels =
543
          List.fold_left (fun accu (t, h) ->
544
	      unify typ_in (type_const ~is_annot loc (Const_tag t));
545
	      type_subtyping_arg env in_main const h typ_out;
546
	      if List.mem t accu
547
	      then raise (Error (loc, Already_bound t))
548
	      else t :: accu) [] hl in
549
        let type_labels = get_enum_type_tags (coretype_type typ_in) in
550
        if List.sort compare used_labels <> List.sort compare type_labels
551
        then let unbound_tag = List.find (fun t -> not (List.mem t used_labels)) type_labels in
552
	     raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag)))
553
        else (typ_in, typ_out)
554
      with Unify (t1, t2) ->
555
        raise (Error (loc, Type_clash (t1,t2)))
556

    
557
    (* Eexpr are always in annotations. TODO: add the quantifiers variables to the env *)
558
    let type_eexpr env eexpr = 
559
      (type_expr
560
         ~is_annot:true
561
         env
562
         false (* not in main *)
563
         false (* not a const *)
564
         eexpr.eexpr_qfexpr)
565

    
566

    
567
    (** [type_eq env eq] types equation [eq] in environment [env] *)
568
    let type_eq env in_main undefined_vars eq =
569
      (*Format.eprintf "Typing.type_eq %a@." Printers.pp_node_eq eq;*)
570
      (* Check undefined variables, type lhs *)
571
      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
572
      let ty_lhs = type_expr env in_main false expr_lhs in
573
      (* Check multiple variable definitions *)
574
      let define_var id uvars =
575
        if ISet.mem id uvars
576
        then ISet.remove id uvars
577
        else raise (Error (eq.eq_loc, Already_defined id))
578
      in
579
      (* check assignment of declared constant, assignment of clock *)
580
      let ty_lhs =
581
        type_of_type_list
582
          (List.map2 (fun ty id ->
583
	       if get_static_value ty <> None
584
	       then raise (Error (eq.eq_loc, Assigned_constant id)) else
585
	         match get_clock_base_type ty with
586
	         | None -> ty
587
	         | Some ty -> ty)
588
	     (type_list_of_type ty_lhs) eq.eq_lhs) in
589
      let undefined_vars =
590
        List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in
591
      (* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned
592
     to a (always non-constant) lhs variable *)
593
      type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;
594
      undefined_vars
595

    
596

    
597
    (* [type_coreclock env ck id loc] types the type clock declaration [ck]
598
   in environment [env] *)
599
    let type_coreclock env ck id loc =
600
      match ck.ck_dec_desc with
601
      | Ckdec_any -> ()
602
      | Ckdec_bool cl ->
603
         let dummy_id_expr = expr_of_ident id loc in
604
         let when_expr =
605
           List.fold_left
606
             (fun expr (x, l) ->
607
               {expr_tag = new_tag ();
608
                expr_desc= Expr_when (expr,x,l);
609
                expr_type = Types.Main.new_var ();
610
                expr_clock = Clocks.new_var true;
611
                expr_delay = Delay.new_var ();
612
                expr_loc=loc;
613
		expr_annot = None})
614
             dummy_id_expr cl
615
         in
616
         ignore (type_expr env false false when_expr)
617

    
618
    let rec check_type_declaration loc cty =
619
      match cty with
620
      | Tydec_clock ty
621
        | Tydec_array (_, ty) -> check_type_declaration loc ty
622
      | Tydec_const tname   ->
623
         (* Format.eprintf "TABLE: %a@." print_type_table (); *)
624
         if not (Hashtbl.mem type_table cty)
625
         then raise (Error (loc, Unbound_type tname));
626
      | _                   -> ()
627

    
628
    let type_var_decl vd_env env vdecl =
629
      (*Format.eprintf "Typing.type_var_decl START %a in %a@." Printers.pp_var vdecl (Env.pp_env print_ty) env;*)
630
      check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
631
      
632
      let eval_const id = (* Types. *)get_static_value (Env.lookup_value env id) in
633
      let type_dim d =
634
        begin
635
          type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) (* Type_predef. *)type_int;
636
          Dimension.eval Basic_library.eval_env eval_const d;
637
        end in
638
      let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
639
      let ty_static =
640
        if vdecl.var_dec_const
641
        then (* Type_predef. *)type_static (Dimension.mkdim_var ()) ty
642
        else ty in
643
      (match vdecl.var_dec_value with
644
       | None   -> ()
645
       | Some v -> type_subtyping_arg (env, vd_env) false ~sub:false true v ty_static);
646
      try_unify ty_static (Expr_type_hub.import vdecl.var_type) vdecl.var_loc;
647
      let new_env = Env.add_value env vdecl.var_id ty_static in
648
      type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
649
      (*Format.eprintf "END@.";*)
650
      new_env
651

    
652
    let type_var_decl_list vd_env env l =
653
      List.fold_left (type_var_decl vd_env) env l
654

    
655
    let type_of_vlist vars =
656
      let tyl = List.map (fun v -> Expr_type_hub.import v.var_type) vars in
657
      type_of_type_list tyl
658

    
659
    let add_vdecl vd_env vdecl =
660
      if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env
661
      then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
662
      else vdecl::vd_env
663

    
664
    let check_vd_env vd_env =
665
      ignore (List.fold_left add_vdecl [] vd_env)
666

    
667
    let type_spec env c =
668
      (*TODO 
669
        enrich env locally with locals and consts
670
        type each pre/post as a boolean expr
671
        I don't know if we want to update the global env with locally typed variables. 
672
        For the moment, returning the provided env           
673
       *)
674
      env
675
      
676
    (** [type_node env nd loc] types node [nd] in environment env. The
677
    location is used for error reports. *)
678
    let type_node env nd loc =
679
      (*Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Typing node %s in %a@." nd.node_id (Env.pp_env print_ty) env);*)
680
      let is_main = nd.node_id = !Options.main_node in
681
      let vd_env_ol = nd.node_outputs@nd.node_locals in
682
      let vd_env =  nd.node_inputs@vd_env_ol in
683
      check_vd_env vd_env;
684
      
685
      let init_env = env in
686
      let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in
687
      let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in
688
      let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in
689
      let new_env = Env.overwrite env delta_env in
690
      let undefined_vars_init =
691
        List.fold_left
692
          (fun uvs v -> ISet.add v.var_id uvs)
693
          ISet.empty vd_env_ol in
694
      let undefined_vars =
695
        let eqs, auts = get_node_eqs nd in
696
        (* TODO XXX: il faut typer les handlers de l'automate *)
697
        List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init eqs
698
      in
699
      (* Typing asserts *)
700
      List.iter (fun assert_ ->
701
          let assert_expr =  assert_.assert_expr in
702
          type_subtyping_arg (new_env, vd_env) is_main false assert_expr (* Type_predef. *)type_bool
703
        )  nd.node_asserts;
704
      (* Typing spec/contracts *)
705
      (match nd.node_spec with None -> () | Some spec -> ignore (type_spec (new_env, vd_env) spec));
706
      (* Typing annots *)
707
      List.iter (fun annot ->
708
          List.iter (fun (_, eexpr) -> ignore (type_eexpr (new_env, vd_env) eexpr)) annot.annots
709
        ) nd.node_annot;
710
      
711
      (* check that table is empty *)
712
      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
713
      let undefined_vars = ISet.diff undefined_vars local_consts in
714
      if (not (ISet.is_empty undefined_vars)) then
715
        raise (Error (loc, Undefined_var undefined_vars));
716
      let ty_ins = type_of_vlist nd.node_inputs in
717
      let ty_outs = type_of_vlist nd.node_outputs in
718
      let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
719
      generalize ty_node;
720
      (* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
721
      nd.node_type <- Expr_type_hub.export ty_node;
722
      Env.add_value env nd.node_id ty_node
723

    
724
    let type_imported_node env nd loc =
725
      let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in
726
      let vd_env = nd.nodei_inputs@nd.nodei_outputs in
727
      check_vd_env vd_env;
728
      ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);
729
      let ty_ins = type_of_vlist nd.nodei_inputs in
730
      let ty_outs = type_of_vlist nd.nodei_outputs in
731
      let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
732
      generalize ty_node;
733
      (*
734
  if (is_polymorphic ty_node) then
735
    raise (Error (loc, Poly_imported_node nd.nodei_id));
736
       *)
737
      let new_env = Env.add_value env nd.nodei_id ty_node in
738
      nd.nodei_type <- Expr_type_hub.export ty_node;
739
      new_env
740

    
741
    let type_top_const env cdecl =
742
      let ty = type_const cdecl.const_loc cdecl.const_value in
743
      let d =
744
        if is_dimension_type ty
745
        then dimension_of_const cdecl.const_loc cdecl.const_value
746
        else Dimension.mkdim_var () in
747
      let ty = (* Type_predef. *)type_static d ty in
748
      let new_env = Env.add_value env cdecl.const_id ty in
749
      cdecl.const_type <- Expr_type_hub.export ty;
750
      new_env
751

    
752
    let type_top_consts env clist =
753
      List.fold_left type_top_const env clist
754

    
755
    let rec type_top_decl env decl =
756
      match decl.top_decl_desc with
757
      | Node nd -> (
758
        try
759
          type_node env nd decl.top_decl_loc
760
        with Error (loc, err) as exc -> (
761
          if !Options.global_inline then
762
	    Format.eprintf "Type error: failing node@.%a@.@?"
763
	      Printers.pp_node nd
764
          ;
765
            raise exc)
766
      )
767
      | ImportedNode nd ->
768
         type_imported_node env nd decl.top_decl_loc
769
      | Const c ->
770
         type_top_const env c
771
      | TypeDef _ -> List.fold_left type_top_decl env (consts_of_enum_type decl)
772
      | Open _  -> env
773
    
774
    let get_type_of_call decl =
775
      match decl.top_decl_desc with
776
      | Node nd         ->
777
         let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.node_type) in
778
         type_list_of_type in_typ, type_list_of_type out_typ
779
      | ImportedNode nd ->
780
         let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.nodei_type) in
781
         type_list_of_type in_typ, type_list_of_type out_typ
782
      | _               -> assert false
783

    
784
    let type_prog env decls =
785
      try
786
        List.fold_left type_top_decl env decls
787
      with Failure _ as exc -> raise exc
788

    
789
    (* Once the Lustre program is fully typed, we must get back to the
790
       original description of dimensions, with constant parameters,
791
       instead of unifiable internal variables. *)
792

    
793
    (* The following functions aims at 'unevaluating' dimension
794
       expressions occuring in array types, i.e. replacing unifiable
795
       second_order variables with the original static parameters.
796
       Once restored in this formulation, dimensions may be
797
       meaningfully printed.  *)
798
    let uneval_vdecl_generics vdecl =
799
      if vdecl.var_dec_const
800
      then
801
        match get_static_value (Expr_type_hub.import vdecl.var_type) with
802
        | None   -> (Format.eprintf "internal error: %a@." (* Types. *)print_ty (Expr_type_hub.import vdecl.var_type); assert false)
803
        | Some d -> Dimension.uneval vdecl.var_id d
804

    
805
    let uneval_node_generics vdecls =
806
      List.iter uneval_vdecl_generics vdecls
807

    
808
    let uneval_spec_generics spec =
809
      List.iter uneval_vdecl_generics (spec.consts@spec.locals)
810
      
811
    let uneval_top_generics decl =
812
      match decl.top_decl_desc with
813
      | Node nd ->
814
         uneval_node_generics (nd.node_inputs @ nd.node_outputs)
815
      | ImportedNode nd ->
816
         uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
817
      | Const _
818
        | TypeDef _
819
        | Open _
820
        -> ()
821

    
822
    let uneval_prog_generics prog =
823
      List.iter uneval_top_generics prog
824

    
825
    let rec get_imported_symbol decls id =
826
      match decls with
827
      | [] -> assert false
828
      | decl::q ->
829
         (match decl.top_decl_desc with
830
          | ImportedNode nd when id = nd.nodei_id && decl.top_decl_itf -> decl
831
          | Const c when id = c.const_id && decl.top_decl_itf -> decl
832
          | TypeDef _ -> get_imported_symbol (consts_of_enum_type decl @ q) id
833
          | _ -> get_imported_symbol q id)
834

    
835
    let check_env_compat header declared computed = 
836
      uneval_prog_generics header;
837
      Env.iter declared (fun k decl_type_k ->
838
          let loc = (get_imported_symbol header k).top_decl_loc in 
839
          let computed_t =
840
            instantiate (ref []) (ref []) 
841
	      (try Env.lookup_value computed k
842
	       with Not_found -> raise (Error (loc, Declared_but_undefined k))) in
843
          (*Types.print_ty Format.std_formatter decl_type_k;
844
      Types.print_ty Format.std_formatter computed_t;*)
845
          try_unify ~sub:true ~semi:true decl_type_k computed_t loc
846
        )
847

    
848
    let check_typedef_top decl =
849
      (*Format.eprintf "check_typedef %a@." Printers.pp_short_decl decl;*)
850
      (*Format.eprintf "%a" Printers.pp_typedef (typedef_of_top decl);*)
851
      (*Format.eprintf "%a" Corelang.print_type_table ();*)
852
      match decl.top_decl_desc with
853
      | TypeDef ty ->
854
         let owner = decl.top_decl_owner in
855
         let itf = decl.top_decl_itf in
856
         let decl' =
857
           try Hashtbl.find type_table (Tydec_const (typedef_of_top decl).tydef_id)
858
           with Not_found -> raise (Error (decl.top_decl_loc, Declared_but_undefined ("type "^ ty.tydef_id))) in
859
         let owner' = decl'.top_decl_owner in
860
         (*Format.eprintf "def owner = %s@.decl owner = %s@." owner' owner;*)
861
         let itf' = decl'.top_decl_itf in
862
         (match decl'.top_decl_desc with
863
          | Const _ | Node _ | ImportedNode _ -> assert false
864
          | TypeDef ty' when coretype_equal ty'.tydef_desc ty.tydef_desc && owner' = owner && itf && (not itf') -> ()
865
          | _ -> raise (Error (decl.top_decl_loc, Type_mismatch ty.tydef_id)))
866
      | _  -> ()
867

    
868
    let check_typedef_compat header =
869
      List.iter check_typedef_top header
870
  end
871

    
872
include  Make(Types.Main) (struct
873
             type type_expr  = Types.Main.type_expr
874
             let import x = x
875
             let export x = x
876
           end)
877
             (* Local Variables: *)
878
             (* compile-command:"make -C .." *)
879
(* End: *)
(59-59/60)