Project

General

Profile

Download (39.5 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

    
28

    
29
(* TODO general remark: except in the add_vdecl, it seems to me that
30
   all the pairs (env, vd_env) should be replace with just env, since
31
   vd_env is never used and the env element is always extract with a
32
   fst *)
33

    
34
   
35
module type EXPR_TYPE_HUB =
36
sig
37
  type type_expr 
38
  val import: Types.Main.type_expr -> type_expr
39
  val export: type_expr -> Types.Main.type_expr 
40
end
41

    
42
module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.type_expr) =  
43
  struct
44

    
45
    module TP = Type_predef.Make (T)
46
    include TP
47
    
48
    let pp_typing_env fmt env =
49
      Env.pp_env print_ty fmt env
50

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

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

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

    
124

    
125

    
126
    let basic_coretype_type t =
127
      if is_real_type t then Tydec_real else
128
        if is_int_type t then Tydec_int else
129
          if is_bool_type t then Tydec_bool else
130
	    assert false
131

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

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

    
164
    let get_coretype_definition tname =
165
      try
166
        let top = Hashtbl.find type_table (Tydec_const tname) in
167
        match top.top_decl_desc with
168
        | TypeDef tdef -> tdef.tydef_desc
169
        | _ -> assert false
170
      with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname))
171

    
172
    let get_type_definition tname =
173
      type_coretype (fun _ -> ()) (get_coretype_definition tname)
174

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

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

    
272
    (* Expected type ty1, got type ty2 *)
273
    let try_unify ?(sub=false) ?(semi=false) ty1 ty2 loc =
274
      try
275
        unify ~sub:sub ~semi:semi ty1 ty2
276
      with
277
      | Unify _ ->
278
         raise (Error (loc, Type_clash (ty1,ty2)))
279
      | Dimension.Unify _ ->
280
         raise (Error (loc, Type_clash (ty1,ty2)))
281

    
282

    
283
    (************************************************)
284
    (* Typing function for each basic AST construct *)
285
    (************************************************)
286

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

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

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

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

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

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

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

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

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

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

    
570

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

    
600

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

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

    
632
    let type_var_decl vd_env env vdecl =
633
      (*Format.eprintf "Typing.type_var_decl START %a:%a@." Printers.pp_var vdecl Printers.print_dec_ty vdecl.var_dec_type.ty_dec_desc;*)
634
      check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
635
      let eval_const id = (* Types. *)get_static_value (Env.lookup_value env id) in
636
      let type_dim d =
637
        begin
638
          type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) (* Type_predef. *)type_int;
639
          Dimension.eval Basic_library.eval_dim_env eval_const d;
640
        end in
641
      let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
642

    
643
      let ty_static =
644
        if vdecl.var_dec_const
645
        then (* Type_predef. *)type_static (Dimension.mkdim_var ()) ty
646
        else ty in
647
      (match vdecl.var_dec_value with
648
       | None   -> ()
649
       | Some v -> type_subtyping_arg (env, vd_env) false ~sub:false true v ty_static);
650
      try_unify ty_static (Expr_type_hub.import vdecl.var_type) vdecl.var_loc;
651
      let new_env = Env.add_value env vdecl.var_id ty_static in
652
      type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
653
      (*Format.eprintf "END %a@." Types.print_ty ty_static;*)
654
      new_env
655

    
656
    let type_var_decl_list vd_env env l =
657
      List.fold_left (type_var_decl vd_env) env l
658

    
659
    let type_of_vlist vars =
660
      let tyl = List.map (fun v -> Expr_type_hub.import v.var_type) vars in
661
      type_of_type_list tyl
662

    
663
    let add_vdecl vd_env vdecl =
664
      if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env
665
      then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
666
      else vdecl::vd_env
667

    
668
    let check_vd_env vd_env =
669
      ignore (List.fold_left add_vdecl [] vd_env)
670

    
671
    let type_contract env c =
672
      let vd_env = c.consts @ c.locals in
673
      check_vd_env vd_env;
674
      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
675
      (* typing stmts *)
676
      let eqs = List.map (fun s -> match s with Eq eq -> eq | _ -> assert false) c.stmts  in
677
      let undefined_vars_init =
678
        List.fold_left
679
          (fun uvs v -> ISet.add v.var_id uvs)
680
          ISet.empty c.locals
681
      in
682
      let _ =
683
        List.fold_left
684
          (type_eq (env, vd_env) (false (*is_main*)))
685
          undefined_vars_init
686
          eqs
687
      in
688
      (* Typing each predicate expr *)
689
      let type_pred_ee ee : unit=
690
        type_subtyping_arg (env, vd_env) (false (* not in main *)) (false (* not a const *)) ee.eexpr_qfexpr type_bool
691
      in
692
      List.iter type_pred_ee
693
        (
694
          c.assume 
695
          @ c.guarantees
696
          @ List.flatten (List.map (fun m -> m.ensure @ m.require) c.modes) 
697
        );
698
      (*TODO 
699
        enrich env locally with locals and consts
700
        type each pre/post as a boolean expr
701
        I don't know if we want to update the global env with locally typed variables. 
702
        For the moment, returning the provided env           
703
       *)
704
      env
705

    
706
    let rec type_spec env spec =
707
      match spec with
708
      | Contract c -> type_contract env c
709
      | NodeSpec _ -> env
710
                     
711
    (** [type_node env nd loc] types node [nd] in environment env. The
712
    location is used for error reports. *)
713
    and type_node env nd loc =
714
      (* Format.eprintf "Typing node %s@." nd.node_id; *)
715
      let is_main = nd.node_id = !Options.main_node in
716
      (* In contracts, outputs are considered as input values *)
717
      let vd_env_ol = if nd.node_iscontract then nd.node_locals else nd.node_outputs@nd.node_locals in
718
      let vd_env =  nd.node_inputs@nd.node_outputs@nd.node_locals in
719
      check_vd_env vd_env;
720
      let init_env = env in
721
      let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in
722
      let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in
723
      let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in
724
      let new_env = Env.overwrite env delta_env in
725
      let undefined_vars_init =
726
        List.fold_left
727
          (fun uvs v -> ISet.add v.var_id uvs)
728
          ISet.empty vd_env_ol in
729
      let undefined_vars =
730
        let eqs, _ = get_node_eqs nd in
731
        (* TODO XXX: il faut typer les handlers de l'automate *)
732
        List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init eqs
733
      in
734
      (* Typing asserts *)
735
      List.iter (fun assert_ ->
736
          let assert_expr =  assert_.assert_expr in
737
          type_subtyping_arg (new_env, vd_env) is_main false assert_expr (* Type_predef. *)type_bool
738
        )  nd.node_asserts;
739
      (* Typing spec/contracts *)
740
      (match nd.node_spec with
741
       | None -> ()
742
       | Some spec -> ignore (type_spec new_env spec));
743
      (* Typing annots *)
744
      List.iter (fun annot ->
745
          List.iter (fun (_, eexpr) -> ignore (type_eexpr (new_env, vd_env) eexpr)) annot.annots
746
        ) nd.node_annot;
747
      
748
      (* check that table is empty *)
749
      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
750
      let undefined_vars = ISet.diff undefined_vars local_consts in
751
      
752
      if (not (ISet.is_empty undefined_vars)) then
753
        raise (Error (loc, Undefined_var undefined_vars));
754
      let ty_ins = type_of_vlist nd.node_inputs in
755
      let ty_outs = type_of_vlist nd.node_outputs in
756
      let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
757
      generalize ty_node;
758
      (* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
759
      nd.node_type <- Expr_type_hub.export ty_node;
760
      Env.add_value env nd.node_id ty_node
761

    
762
    let type_imported_node env nd _loc =
763
      let vd_env = nd.nodei_inputs@nd.nodei_outputs in
764
      check_vd_env vd_env;
765
      let delta_env = type_var_decl_list vd_env env nd.nodei_inputs in
766
      let delta_env = type_var_decl_list vd_env delta_env nd.nodei_outputs in
767
      let new_env = Env.overwrite env delta_env in
768
      (* Typing spec *)
769
      (match nd.nodei_spec with
770
       | None -> ()
771
       | Some spec -> ignore (type_spec new_env spec));
772
      let ty_ins = type_of_vlist nd.nodei_inputs in
773
      let ty_outs = type_of_vlist nd.nodei_outputs in
774
      let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
775
      generalize ty_node;
776
      (*
777
  if (is_polymorphic ty_node) then
778
    raise (Error (loc, Poly_imported_node nd.nodei_id));
779
       *)
780
      let new_env = Env.add_value env nd.nodei_id ty_node in
781
      nd.nodei_type <- Expr_type_hub.export ty_node;
782
      new_env
783

    
784
    let type_top_const env cdecl =
785
      let ty = type_const cdecl.const_loc cdecl.const_value in
786
      let d =
787
        if is_dimension_type ty
788
        then dimension_of_const cdecl.const_loc cdecl.const_value
789
        else Dimension.mkdim_var () in
790
      let ty = (* Type_predef. *)type_static d ty in
791
      let new_env = Env.add_value env cdecl.const_id ty in
792
      cdecl.const_type <- Expr_type_hub.export ty;
793
      new_env
794

    
795
    let type_top_consts env clist =
796
      List.fold_left type_top_const env clist
797

    
798
    let rec type_top_decl env decl =
799
      match decl.top_decl_desc with
800
      | Node nd -> (
801
        try
802
          type_node env nd decl.top_decl_loc
803
        with Error _ as exc -> (
804
          if !Options.global_inline then
805
	    Format.eprintf "Type error: failing node@.%a@.@?"
806
	      Printers.pp_node nd
807
          ;
808
            raise exc)
809
      )
810
      | ImportedNode nd ->
811
         type_imported_node env nd decl.top_decl_loc
812
      | Const c ->
813
         type_top_const env c
814
      | TypeDef _ -> List.fold_left type_top_decl env (consts_of_enum_type decl)
815
      | Include _ | Open _  -> env
816
    
817
    let get_type_of_call decl =
818
      match decl.top_decl_desc with
819
      | Node nd         ->
820
         let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.node_type) in
821
         type_list_of_type in_typ, type_list_of_type out_typ
822
      | ImportedNode nd ->
823
         let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.nodei_type) in
824
         type_list_of_type in_typ, type_list_of_type out_typ
825
      | _               -> assert false
826

    
827
    let type_prog env decls =
828
      try
829
        List.fold_left type_top_decl env decls
830
      with Failure _ as exc -> raise exc
831

    
832
    (* Once the Lustre program is fully typed, we must get back to the
833
       original description of dimensions, with constant parameters,
834
       instead of unifiable internal variables. *)
835

    
836
    (* The following functions aims at 'unevaluating' dimension
837
       expressions occuring in array types, i.e. replacing unifiable
838
       second_order variables with the original static parameters.
839
       Once restored in this formulation, dimensions may be
840
       meaningfully printed.  *)
841
    let uneval_vdecl_generics vdecl =
842
      if vdecl.var_dec_const
843
      then
844
        match get_static_value (Expr_type_hub.import vdecl.var_type) with
845
        | None   -> (Format.eprintf "internal error: %a@." (* Types. *)print_ty (Expr_type_hub.import vdecl.var_type); assert false)
846
        | Some d -> Dimension.uneval vdecl.var_id d
847

    
848
    let uneval_node_generics vdecls =
849
      List.iter uneval_vdecl_generics vdecls
850

    
851
    let uneval_spec_generics spec =
852
      List.iter uneval_vdecl_generics (spec.consts@spec.locals)
853
      
854
    let uneval_top_generics decl =
855
      match decl.top_decl_desc with
856
      | Node nd ->
857
         uneval_node_generics (nd.node_inputs @ nd.node_outputs)
858
      | ImportedNode nd ->
859
         uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
860
      | Const _ | TypeDef _ | Open _ | Include _ 
861
        -> ()
862

    
863
    let uneval_prog_generics prog =
864
      List.iter uneval_top_generics prog
865

    
866
    let rec get_imported_symbol decls id =
867
      match decls with
868
      | [] -> assert false
869
      | decl::q ->
870
         (match decl.top_decl_desc with
871
          | ImportedNode nd when id = nd.nodei_id && decl.top_decl_itf -> decl
872
          | Const c when id = c.const_id && decl.top_decl_itf -> decl
873
          | TypeDef _ -> get_imported_symbol (consts_of_enum_type decl @ q) id
874
          | _ -> get_imported_symbol q id)
875

    
876
    let check_env_compat header declared computed = 
877
      uneval_prog_generics header;
878
      Env.iter declared (fun k decl_type_k ->
879
          let top = get_imported_symbol header k in
880
          let loc = top.top_decl_loc in 
881
          try
882
            let computed_t = Env.lookup_value computed k in
883
            let computed_t = instantiate (ref []) (ref []) computed_t in
884
            (*Types.print_ty Format.std_formatter decl_type_k;
885
              Types.print_ty Format.std_formatter computed_t;*)                   
886
            try_unify ~sub:true ~semi:true decl_type_k computed_t loc
887
          with Not_found ->
888
            begin
889
              (* If top is a contract we do not require the lustre
890
                 file to provide the same definition. *)
891
              match top.top_decl_desc with
892
              | Node nd -> (
893
                match nd.node_spec with
894
                | Some (Contract _) -> ()
895
                | _ -> raise (Error (loc, Declared_but_undefined k))
896
              )                                                            
897
              | _ ->
898
                 raise (Error (loc, Declared_but_undefined k))
899
            end
900
        )
901

    
902
    let check_typedef_top decl =
903
      (*Format.eprintf "check_typedef %a@." Printers.pp_short_decl decl;*)
904
      (*Format.eprintf "%a" Printers.pp_typedef (typedef_of_top decl);*)
905
      (*Format.eprintf "%a" Corelang.print_type_table ();*)
906
      match decl.top_decl_desc with
907
      | TypeDef ty ->
908
         let owner = decl.top_decl_owner in
909
         let itf = decl.top_decl_itf in
910
         let decl' =
911
           try Hashtbl.find type_table (Tydec_const (typedef_of_top decl).tydef_id)
912
           with Not_found -> raise (Error (decl.top_decl_loc, Declared_but_undefined ("type "^ ty.tydef_id))) in
913
         let owner' = decl'.top_decl_owner in
914
         (*Format.eprintf "def owner = %s@.decl owner = %s@." owner' owner;*)
915
         let itf' = decl'.top_decl_itf in
916
         (match decl'.top_decl_desc with
917
          | Const _ | Node _ | ImportedNode _ -> assert false
918
          | TypeDef ty' when coretype_equal ty'.tydef_desc ty.tydef_desc && owner' = owner && itf && (not itf') -> ()
919
          | _ -> raise (Error (decl.top_decl_loc, Type_mismatch ty.tydef_id)))
920
      | _  -> ()
921

    
922
    let check_typedef_compat header =
923
      List.iter check_typedef_top header
924
  end
925

    
926
include  Make(Types.Main) (struct
927
             type type_expr  = Types.Main.type_expr
928
             let import x = x
929
             let export x = x
930
           end)
931
             (* Local Variables: *)
932
             (* compile-command:"make -C .." *)
933
(* End: *)
(59-59/63)