Project

General

Profile

Download (39.7 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 (t1', t2') ->
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 ->
540
          Format.fprintf fmt "Type of expr %a: %a@ "
541
            Printers.pp_expr expr (* Types. *)print_ty resulting_ty);
542
      resulting_ty
543

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

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

    
572

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

    
602

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

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

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

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

    
658
    let type_var_decl_list vd_env env l =
659
      List.fold_left (type_var_decl vd_env) env l
660

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

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

    
670
    let check_vd_env vd_env =
671
      ignore (List.fold_left add_vdecl [] vd_env)
672

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

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

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

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

    
797
    let type_top_consts env clist =
798
      List.fold_left type_top_const env clist
799

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

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

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

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

    
850
    let uneval_node_generics vdecls =
851
      List.iter uneval_vdecl_generics vdecls
852

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

    
865
    let uneval_prog_generics prog =
866
      List.iter uneval_top_generics prog
867

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

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

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

    
924
    let check_typedef_compat header =
925
      List.iter check_typedef_top header
926
  end
927

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