Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / typing.ml @ e8f55c25

History | View | Annotate | Download (39.6 KB)

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
(* TODO general remark: except in the add_vdecl, it seems to me that
31
   all the pairs (env, vd_env) should be replace with just env, since
32
   vd_env is never used and the env element is always extract with a
33
   fst *)
34

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

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

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

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

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

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

    
125

    
126

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

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

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

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

    
173
    let get_type_definition tname =
174
      type_coretype (fun d -> ()) (get_coretype_definition tname)
175

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

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

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

    
283

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

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

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

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

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

    
370
    (* emulates a subtyping relation between types t and (d : t),
371
   used during node applications and assignments *)
372
    and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =
373
      let loc = real_arg.expr_loc in
374
      let const = const || ((* Types. *)get_static_value formal_type <> None) in
375
      let real_type = type_add_const env const real_arg (type_expr env in_main const real_arg) in
376
      (*Format.eprintf "subtyping const %B real %a:%a vs formal %a@." const Printers.pp_expr real_arg Types.print_ty real_type Types.print_ty formal_type;*)
377
      try_unify ~sub:sub formal_type real_type loc
378

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

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

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

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

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

    
571

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

    
601

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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