Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

src/typing.ml
6 6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7 7
(*  under the terms of the GNU Lesser General Public License        *)
8 8
(*  version 2.1.                                                    *)
9
(*                                                                  *) 
9
(*                                                                  *)
10 10
(*  This file was originally from the Prelude compiler              *)
11
(*                                                                  *) 
11
(*                                                                  *)
12 12
(********************************************************************)
13 13

  
14 14
(** Main typing module. Classic inference algorithm with destructive
15 15
    unification. *)
16 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. *)
17
let debug _fmt _args = ()
18

  
19
(* Format.eprintf "%a" *)
20
(* Though it shares similarities with the clock calculus module, no code is
21
   shared. Simple environments, very limited identifier scoping, no identifier
22
   redefinition allowed. *)
21 23

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

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

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

  
35
module type EXPR_TYPE_HUB = sig
36
  type type_expr
28 37

  
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 *)
38
  val import : Types.Main.type_expr -> type_expr
33 39

  
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
  val export : type_expr -> Types.Main.type_expr
40 41
end
41 42

  
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 =
43
module Make
44
    (T : Types.S)
45
    (Expr_type_hub : EXPR_TYPE_HUB with type type_expr = T.type_expr) =
46
struct
47
  module TP = Type_predef.Make (T)
48
  include TP
49

  
50
  let pp_typing_env fmt env = 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] occurs in type
57
      [ty]. False otherwise. *)
58
  let rec occurs tvar ty =
59
    let ty = repr ty in
60
    match type_desc ty with
61
    | Tvar ->
62
      ty = tvar
63
    | Tarrow (t1, t2) ->
64
      occurs tvar t1 || occurs tvar t2
65
    | Ttuple tl ->
66
      List.exists (occurs tvar) tl
67
    | Tstruct fl ->
68
      List.exists (fun (_, t) -> occurs tvar t) fl
69
    | Tarray (_, t) | Tstatic (_, t) | Tclock t | Tlink t ->
70
      occurs tvar t
71
    | Tenum _ | Tconst _ | Tunivar | Tbasic _ ->
72
      false
73

  
74
  (* Generalize by side-effects *)
75

  
76
  (** Promote monomorphic type variables to polymorphic type variables. *)
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;
84
      generalize t2
85
    | Ttuple tl ->
86
      List.iter generalize tl
87
    | Tstruct fl ->
88
      List.iter (fun (_, t) -> generalize t) fl
89
    | Tstatic (d, t) | Tarray (d, t) ->
90
      Dimension.generalize d;
91
      generalize t
92
    | Tclock t | Tlink t ->
93
      generalize t
94
    | Tenum _ | Tconst _ | Tunivar | Tbasic _ ->
95
      ()
96

  
97
  (** Downgrade polymorphic type variables to monomorphic type variables *)
98
  let rec instantiate inst_vars inst_dim_vars ty =
99
    let ty = repr ty in
100
    match ty.tdesc with
101
    | Tenum _ | Tconst _ | Tvar | Tbasic _ ->
102
      ty
103
    | Tarrow (t1, t2) ->
104
      {
105
        ty with
106
        tdesc =
107
          Tarrow
108
            ( instantiate inst_vars inst_dim_vars t1,
109
              instantiate inst_vars inst_dim_vars t2 );
110
      }
111
    | Ttuple tlist ->
112
      {
113
        ty with
114
        tdesc = Ttuple (List.map (instantiate inst_vars inst_dim_vars) tlist);
115
      }
116
    | Tstruct flist ->
117
      {
118
        ty with
119
        tdesc =
120
          Tstruct
121
            (List.map
122
               (fun (f, t) -> f, instantiate inst_vars inst_dim_vars t)
123
               flist);
124
      }
125
    | Tclock t ->
126
      { ty with tdesc = Tclock (instantiate inst_vars inst_dim_vars t) }
127
    | Tstatic (d, t) ->
128
      {
129
        ty with
130
        tdesc =
131
          Tstatic
132
            ( Dimension.instantiate inst_dim_vars d,
133
              instantiate inst_vars inst_dim_vars t );
134
      }
135
    | Tarray (d, t) ->
136
      {
137
        ty with
138
        tdesc =
139
          Tarray
140
            ( Dimension.instantiate inst_dim_vars d,
141
              instantiate inst_vars inst_dim_vars t );
142
      }
143
    | Tlink t ->
144
      (* should not happen *)
145
      { ty with tdesc = Tlink (instantiate inst_vars inst_dim_vars t) }
146
    | Tunivar -> (
147
      try List.assoc ty.tid !inst_vars
148
      with Not_found ->
149
        let var = new_var () in
150
        inst_vars := (ty.tid, var) :: !inst_vars;
151
        var)
152

  
153
  let basic_coretype_type t =
154
    if is_real_type t then Tydec_real
155
    else if is_int_type t then Tydec_int
156
    else if is_bool_type t then Tydec_bool
157
    else assert false
158

  
159
  (* [type_coretype cty] types the type declaration [cty] *)
160
  let rec type_coretype type_dim cty =
161
    match (*get_repr_type*)
162
          cty with
163
    | Tydec_any ->
164
      new_var ()
165
    | Tydec_int ->
166
      type_int
167
    | Tydec_real ->
168
      (* Type_predef. *)
169
      type_real
170
    (* | Tydec_float -> Type_predef.type_real *)
171
    | Tydec_bool ->
172
      (* Type_predef. *)
173
      type_bool
174
    | Tydec_clock ty ->
175
      (* Type_predef. *)
176
      type_clock (type_coretype type_dim ty)
177
    | Tydec_const c ->
178
      (* Type_predef. *)
179
      type_const c
180
    | Tydec_enum tl ->
181
      (* Type_predef. *)
182
      type_enum tl
183
    | Tydec_struct fl ->
184
      (* Type_predef. *)
185
      type_struct (List.map (fun (f, ty) -> f, type_coretype type_dim ty) fl)
186
    | Tydec_array (d, ty) ->
187
      let d = Dimension.copy (ref []) d in
188
      type_dim d;
189
      (* Type_predef. *)
190
      type_array d (type_coretype type_dim ty)
191

  
192
  (* [coretype_type] is the reciprocal of [type_typecore] *)
193
  let rec coretype_type ty =
194
    match (repr ty).tdesc with
195
    | Tvar ->
196
      Tydec_any
197
    | Tbasic _ ->
198
      basic_coretype_type ty
199
    | Tconst c ->
200
      Tydec_const c
201
    | Tclock t ->
202
      Tydec_clock (coretype_type t)
203
    | Tenum tl ->
204
      Tydec_enum tl
205
    | Tstruct fl ->
206
      Tydec_struct (List.map (fun (f, t) -> f, coretype_type t) fl)
207
    | Tarray (d, t) ->
208
      Tydec_array (d, coretype_type t)
209
    | Tstatic (_, t) ->
210
      coretype_type t
211
    | _ ->
212
      assert false
213

  
214
  let get_coretype_definition tname =
215
    try
216
      let top = Hashtbl.find type_table (Tydec_const tname) in
217
      match top.top_decl_desc with
218
      | TypeDef tdef ->
219
        tdef.tydef_desc
220
      | _ ->
221
        assert false
222
    with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname))
223

  
224
  let get_type_definition tname =
225
    type_coretype (fun _ -> ()) (get_coretype_definition tname)
226

  
227
  (* Equality on ground types only *)
228
  (* Should be used between local variables which must have a ground type *)
229
  let rec eq_ground t1 t2 =
230
    let t1 = repr t1 in
231
    let t2 = repr t2 in
232
    t1 == t2
233
    ||
234
    match t1.tdesc, t2.tdesc with
235
    | Tbasic t1, Tbasic t2 when t1 == t2 ->
236
      true
237
    | Tenum tl, Tenum tl' when tl == tl' ->
238
      true
239
    | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->
240
      List.for_all2 eq_ground tl tl'
241
    | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->
242
      List.for_all2 (fun (_, t) (_, t') -> eq_ground t t') fl fl'
243
    | Tconst t, _ ->
244
      let def_t = get_type_definition t in
245
      eq_ground def_t t2
246
    | _, Tconst t ->
247
      let def_t = get_type_definition t in
248
      eq_ground t1 def_t
249
    | Tarrow (t1, t2), Tarrow (t1', t2') ->
250
      eq_ground t1 t1' && eq_ground t2 t2'
251
    | Tclock t1', Tclock t2' ->
252
      eq_ground t1' t2'
253
    | Tstatic (e1, t1'), Tstatic (e2, t2') | Tarray (e1, t1'), Tarray (e2, t2')
254
      ->
255
      Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2'
256
    | _ ->
257
      false
258

  
259
  (** [unify t1 t2] unifies types [t1] and [t2] using standard destructive
260
      unification. Raises [Unify (t1,t2)] if the types are not unifiable. [t1]
261
      is a expected/formal/spec type, [t2] is a computed/real/implem type, so in
262
      case of unification error: expected type [t1], got type [t2]. If
263
      [sub]-typing is allowed, [t2] may be a subtype of [t1]. If [semi]
264
      unification is required, [t1] should furthermore be an instance of [t2]
265
      and constants are handled differently.*)
266
  let unify ?(sub = false) ?(semi = false) t1 t2 =
267
    let rec unif t1 t2 =
178 268
      let t1 = repr t1 in
179 269
      let t2 = repr t2 in
180
      t1==t2 ||
270
      if t1 == t2 then ()
271
      else
181 272
        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
273
        (* strictly subtyping cases first *)
274
        | _, Tclock t2 when sub && get_clock_base_type t1 = None ->
275
          unif t1 t2
276
        | _, Tstatic (_, t2) when sub && get_static_value t1 = None ->
277
          unif t1 t2
278
        (* This case is not mandatory but will keep "older" types *)
279
        | Tvar, Tvar ->
280
          if t1.tid < t2.tid then t2.tdesc <- Tlink t1 else t1.tdesc <- Tlink t2
281
        | Tvar, _ when (not semi) && not (occurs t1 t2) ->
282
          t1.tdesc <- Tlink t2
283
        | _, Tvar when not (occurs t2 t1) ->
284
          t2.tdesc <- Tlink t1
285
        | Tarrow (t1, t2), Tarrow (t1', t2') ->
286
          unif t2 t2';
287
          unif t1' t1
288
        | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->
289
          List.iter2 unif tl tl'
290
        | Ttuple [ t1 ], _ ->
291
          unif t1 t2
292
        | _, Ttuple [ t2 ] ->
293
          unif t1 t2
294
        | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->
295
          List.iter2 (fun (_, t) (_, t') -> unif t t') fl fl'
296
        | Tclock _, Tstatic _ | Tstatic _, Tclock _ ->
297
          raise (Unify (t1, t2))
298
        | Tclock t1', Tclock t2' ->
299
          unif t1' t2'
300
        (* | Tbasic t1, Tbasic t2 when t1 == t2 -> () *)
301
        | Tunivar, _ | _, Tunivar ->
212 302
          ()
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
303
        | Tconst t, _ ->
304
          let def_t = get_type_definition t in
305
          unif def_t t2
306
        | _, Tconst t ->
307
          let def_t = get_type_definition t in
308
          unif t1 def_t
309
        | Tenum tl, Tenum tl' when tl == tl' ->
310
          ()
311
        | Tstatic (e1, t1'), Tstatic (e2, t2')
312
        | Tarray (e1, t1'), Tarray (e2, t2') ->
313
          let eval_const =
314
            if semi then fun c ->
315
              Some (Dimension.mkdim_ident Location.dummy_loc c)
316
            else fun _ -> None
317
          in
318
          unif t1' t2';
319
          Dimension.eval Basic_library.eval_dim_env eval_const e1;
320
          Dimension.eval Basic_library.eval_dim_env eval_const e2;
321
          Dimension.unify ~semi e1 e2
322
        (* Special cases for machine_types. Rules to unify static types infered
323
           for numerical constants with non static ones for variables with
324
           possible machine types *)
325
        | Tbasic bt1, Tbasic bt2 when BasicT.is_unifiable bt1 bt2 ->
326
          BasicT.unify bt1 bt2
327
        | _, _ ->
328
          raise (Unify (t1, t2))
329
    in
330
    unif t1 t2
331

  
332
  (* Expected type ty1, got type ty2 *)
333
  let try_unify ?(sub = false) ?(semi = false) ty1 ty2 loc =
334
    try unify ~sub ~semi ty1 ty2 with
335
    | Unify (t1', t2') ->
336
      raise (Error (loc, Type_clash (ty1, ty2)))
337
    | Dimension.Unify _ ->
338
      raise (Error (loc, Type_clash (ty1, ty2)))
339

  
340
  (************************************************)
341
  (* Typing function for each basic AST construct *)
342
  (************************************************)
343

  
344
  let rec type_struct_const_field ?(is_annot = false) loc (label, c) =
345
    if Hashtbl.mem field_table label then (
346
      let tydef = Hashtbl.find field_table label in
347
      let tydec = (typedef_of_top tydef).tydef_desc in
348
      let tydec_struct = get_struct_type_fields tydec in
349
      let ty_label =
350
        type_coretype (fun _ -> ()) (List.assoc label tydec_struct)
351
      in
352
      try_unify ty_label (type_const ~is_annot loc c) loc;
353
      type_coretype (fun _ -> ()) tydec)
354
    else raise (Error (loc, Unbound_value ("struct field " ^ label)))
355

  
356
  and type_const ?(is_annot = false) loc c =
357
    match c with
358
    | Const_int _ ->
359
      (* Type_predef. *)
360
      type_int
361
    | Const_real _ ->
362
      (* Type_predef. *)
363
      type_real
364
    | Const_array ca ->
365
      let d = Dimension.mkdim_int loc (List.length ca) in
366
      let ty = new_var () in
367
      List.iter (fun e -> try_unify ty (type_const ~is_annot loc e) loc) ca;
368
      (* Type_predef. *)
369
      type_array d ty
370
    | Const_tag t ->
371
      if Hashtbl.mem tag_table t then
372
        let tydef = typedef_of_top (Hashtbl.find tag_table t) in
373
        let tydec =
374
          if is_user_type tydef.tydef_desc then Tydec_const tydef.tydef_id
375
          else tydef.tydef_desc
376
        in
377
        type_coretype (fun _ -> ()) tydec
378
      else raise (Error (loc, Unbound_value ("enum tag " ^ t)))
379
    | Const_struct fl -> (
380
      let ty_struct = new_var () in
381
      let used =
382
        List.fold_left
383
          (fun acc (l, c) ->
384
            if List.mem l acc then
385
              raise (Error (loc, Already_bound ("struct field " ^ l)))
224 386
            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 =
387
              try_unify ty_struct
388
                (type_struct_const_field ~is_annot loc (l, c))
389
                loc;
390
            l :: acc)
391
          [] fl
392
      in
274 393
      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
        let total =
395
          List.map fst (get_struct_type_fields (coretype_type ty_struct))
396
        in
397
        (* List.iter (fun l -> Format.eprintf "total: %s@." l) total; List.iter
398
           (fun l -> Format.eprintf "used: %s@." l) used; *)
399
        let undef = List.find (fun l -> not (List.mem l used)) total in
400
        raise (Error (loc, Unbound_value ("struct field " ^ undef)))
401
      with Not_found -> ty_struct)
402
    | Const_string s | Const_modeid s ->
403
      if is_annot then (* Type_predef. *)
404
        type_string
394 405
      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))
406
        Format.eprintf "Typing string %s outisde of annot scope@.@?" s;
407
        assert false (* string datatype should only appear in annotations *))
408

  
409
  (* The following typing functions take as parameter an environment [env] and
410
     whether the element being typed is expected to be constant [const]. [env]
411
     is a pair composed of: - a map from ident to type, associating to each
412
     ident, i.e. variables, constants and (imported) nodes, its type including
413
     whether it is constant or not. This latter information helps in checking
414
     constant propagation policy in Lustre. - a vdecl list, in order to modify
415
     types of declared variables that are later discovered to be clocks during
416
     the typing process. *)
417
  let check_constant loc const_expected const_real =
418
    if const_expected && not const_real then raise (Error (loc, Not_a_constant))
419

  
420
  let rec type_add_const env const arg targ =
421
    (*Format.eprintf "Typing.type_add_const %a %a@." Printers.pp_expr arg
422
      Types.print_ty targ;*)
423
    if const then (
424
      let d =
425
        if is_dimension_type targ then dimension_of_expr arg
426
        else Dimension.mkdim_var ()
427
      in
428
      let eval_const id =
429
        (* Types. *)
430
        get_static_value (Env.lookup_value (fst env) id)
431
      in
432
      Dimension.eval Basic_library.eval_dim_env eval_const d;
433
      let real_static_type =
434
        (* Type_predef. *)
435
        type_static d ((* Types. *)
436
                       dynamic_type targ)
584 437
      in
585
      (* check assignment of declared constant, assignment of clock *)
586
      let ty_lhs =
438
      (match (* Types. *)
439
             get_static_value targ with
440
      | None ->
441
        ()
442
      | Some _ ->
443
        try_unify targ real_static_type arg.expr_loc);
444
      real_static_type)
445
    else targ
446

  
447
  (* emulates a subtyping relation between types t and (d : t), used during node
448
     applications and assignments *)
449
  and type_subtyping_arg env in_main ?(sub = true) const real_arg formal_type =
450
    let loc = real_arg.expr_loc in
451
    let const =
452
      const
453
      || (* Types. *)
454
      get_static_value formal_type <> None
455
    in
456
    let real_type =
457
      type_add_const env const real_arg (type_expr env in_main const real_arg)
458
    in
459
    (*Format.eprintf "subtyping const %B real %a:%a vs formal %a@." const
460
      Printers.pp_expr real_arg Types.print_ty real_type Types.print_ty
461
      formal_type;*)
462
    try_unify ~sub formal_type real_type loc
463

  
464
  (* typing an application implies: - checking that const formal parameters
465
     match real const (maybe symbolic) arguments - checking type adequation
466
     between formal and real arguments An application may embed an
467
     homomorphic/internal function, in which case we need to split it in many
468
     calls *)
469
  and type_appl env in_main loc const f args =
470
    let targs = List.map (type_expr env in_main const) args in
471
    if Basic_library.is_homomorphic_fun f && List.exists is_tuple_type targs
472
    then
473
      try
474
        let targs = Utils.transpose_list (List.map type_list_of_type targs) in
475
        (* Types. *)
587 476
        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 =
477
          (List.map (type_simple_call env in_main loc const f) targs)
478
      with Utils.TransposeError (l, l') ->
479
        raise (Error (loc, WrongMorphism (l, l')))
480
    else type_dependent_call env in_main loc const f (List.combine args targs)
481

  
482
  (* type a call with possible dependent types. [targs] is here a list of
483
     (argument, type) pairs. *)
484
  and type_dependent_call env in_main loc const f targs =
485
    (* Format.eprintf "Typing.type_dependent_call %s@." f; *)
486
    let tins, touts = new_var (), new_var () in
487
    (* Format.eprintf "tin=%a, tout=%a@." print_ty tins print_ty touts; *)
488
    let tfun =
489
      (* Type_predef. *)
490
      type_arrow tins touts
491
    in
492
    (* Format.eprintf "fun=%a@." print_ty tfun; *)
493
    type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
494
    (* Format.eprintf "type subtyping@."; *)
495
    let tins = type_list_of_type tins in
496
    if List.length targs <> List.length tins then
497
      raise (Error (loc, WrongArity (List.length tins, List.length targs)))
498
    else (
499
      List.iter2
500
        (fun (a, t) ti ->
501
          let t' =
502
            type_add_const env
503
              (const
504
              || (* Types. *)
505
              get_static_value ti <> None)
506
              a t
507
          in
508
          (* Format.eprintf "uniying ti=%a t'=%a touts=%a@." print_ty ti
509
             print_ty t' print_ty touts; *)
510
          try_unify ~sub:true ti t' a.expr_loc
511
          (* Format.eprintf "unified ti=%a t'=%a touts=%a@." print_ty ti
512
             print_ty t' print_ty touts; *))
513
        targs tins;
514
      touts)
515

  
516
  (* type a simple call without dependent types but possible homomorphic
517
     extension. [targs] is here a list of arguments' types. *)
518
  and type_simple_call env in_main loc const f targs =
519
    let tins, touts = new_var (), new_var () in
520
    let tfun =
521
      (* Type_predef. *)
522
      type_arrow tins touts
523
    in
524
    type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
525
    (*Format.eprintf "try unify %a %a@." Types.print_ty tins Types.print_ty
526
      (type_of_type_list targs);*)
527
    try_unify ~sub:true tins (type_of_type_list targs) loc;
528
    touts
529

  
530
  (** [type_expr env in_main expr] types expression [expr] in environment [env],
531
      expecting it to be [const] or not. *)
532
  and type_expr ?(is_annot = false) env in_main const expr =
533
    let resulting_ty =
534
      match expr.expr_desc with
535
      | Expr_const c ->
536
        let ty = type_const ~is_annot expr.expr_loc c in
537
        let ty =
538
          (* Type_predef. *)
539
          type_static (Dimension.mkdim_var ()) ty
540
        in
541
        expr.expr_type <- Expr_type_hub.export ty;
542
        ty
543
      | Expr_ident v ->
544
        let tyv =
545
          try Env.lookup_value (fst env) v
546
          with Not_found ->
547
            Format.eprintf
548
              "Failure in typing expr %a. Not in typing environement@."
549
              Printers.pp_expr expr;
550
            raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v)))
551
        in
552
        let ty = instantiate (ref []) (ref []) tyv in
553
        let ty' =
554
          if const then
555
            (* Type_predef. *)
556
            type_static (Dimension.mkdim_var ()) (new_var ())
557
          else new_var ()
558
        in
559
        try_unify ty ty' expr.expr_loc;
560
        expr.expr_type <- Expr_type_hub.export ty;
561
        ty
562
      | Expr_array elist ->
563
        let ty_elt = new_var () in
564
        List.iter
565
          (fun e ->
566
            try_unify ty_elt
567
              (type_appl env in_main expr.expr_loc const "uminus" [ e ])
568
              e.expr_loc)
569
          elist;
570
        let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in
571
        let ty =
572
          (* Type_predef. *)
573
          type_array d ty_elt
574
        in
575
        expr.expr_type <- Expr_type_hub.export ty;
576
        ty
577
      | Expr_access (e1, d) ->
578
        type_subtyping_arg env in_main false
579
          (* not necessary a constant *)
580
          (expr_of_dimension d)
581
          (* Type_predef. *)
582
          type_int;
583
        let ty_elt = new_var () in
584
        let d = Dimension.mkdim_var () in
585
        type_subtyping_arg env in_main const e1
586
          ((* Type_predef. *)
587
           type_array d ty_elt);
588
        expr.expr_type <- Expr_type_hub.export ty_elt;
589
        ty_elt
590
      | Expr_power (e1, d) ->
591
        let eval_const id =
592
          (* Types. *)
593
          get_static_value (Env.lookup_value (fst env) id)
594
        in
595
        type_subtyping_arg env in_main true (expr_of_dimension d)
596
          (* Type_predef. *)
597
          type_int;
598
        Dimension.eval Basic_library.eval_dim_env eval_const d;
599
        let ty_elt =
600
          type_appl env in_main expr.expr_loc const "uminus" [ e1 ]
601
        in
602
        let ty =
603
          (* Type_predef. *)
604
          type_array d ty_elt
605
        in
606
        expr.expr_type <- Expr_type_hub.export ty;
607
        ty
608
      | Expr_tuple elist ->
609
        let ty =
610
          new_ty
611
            (Ttuple (List.map (type_expr ~is_annot env in_main const) elist))
612
        in
613
        expr.expr_type <- Expr_type_hub.export ty;
614
        ty
615
      | Expr_ite (c, t, e) ->
616
        type_subtyping_arg env in_main const c (* Type_predef. *) type_bool;
617
        let ty = type_appl env in_main expr.expr_loc const "+" [ t; e ] in
618
        expr.expr_type <- Expr_type_hub.export ty;
619
        ty
620
      | Expr_appl (id, args, r) ->
621
        (* application of non internal function is not legal in a constant
622
           expression *)
623
        (match r with
624
        | None ->
625
          ()
626
        | Some c ->
627
          check_constant expr.expr_loc const false;
628
          type_subtyping_arg env in_main const c (* Type_predef. *) type_bool);
629
        let args_list = expr_list_of_expr args in
630
        let touts = type_appl env in_main expr.expr_loc const id args_list in
631
        let targs =
632
          new_ty
633
            (Ttuple
634
               (List.map (fun a -> Expr_type_hub.import a.expr_type) args_list))
635
        in
636
        args.expr_type <- Expr_type_hub.export targs;
637
        expr.expr_type <- Expr_type_hub.export touts;
638
        touts
639
      | Expr_fby (e1, e2) | Expr_arrow (e1, e2) ->
640
        (* fby/arrow is not legal in a constant expression *)
641
        check_constant expr.expr_loc const false;
642
        let ty = type_appl env in_main expr.expr_loc const "+" [ e1; e2 ] in
643
        expr.expr_type <- Expr_type_hub.export ty;
644
        ty
645
      | Expr_pre e ->
646
        (* pre is not legal in a constant expression *)
647
        check_constant expr.expr_loc const false;
648
        let ty = type_appl env in_main expr.expr_loc const "uminus" [ e ] in
649
        expr.expr_type <- Expr_type_hub.export ty;
650
        ty
651
      | Expr_when (e1, c, l) ->
652
        (* when is not legal in a constant expression *)
653
        check_constant expr.expr_loc const false;
654
        let typ_l =
655
          (* Type_predef. *)
656
          type_clock (type_const ~is_annot expr.expr_loc (Const_tag l))
657
        in
658
        let expr_c = expr_of_ident c expr.expr_loc in
659
        type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
660
        let ty = type_appl env in_main expr.expr_loc const "uminus" [ e1 ] in
661
        expr.expr_type <- Expr_type_hub.export ty;
662
        ty
663
      | Expr_merge (c, hl) ->
664
        (* merge is not legal in a constant expression *)
665
        check_constant expr.expr_loc const false;
666
        let typ_in, typ_out =
667
          type_branches env in_main expr.expr_loc const hl
668
        in
669
        let expr_c = expr_of_ident c expr.expr_loc in
670
        let typ_l =
671
          (* Type_predef. *)
672
          type_clock typ_in
673
        in
674
        type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
675
        expr.expr_type <- Expr_type_hub.export typ_out;
676
        typ_out
677
    in
678
    Log.report ~level:3 (fun fmt ->
679
        Format.fprintf fmt "Type of expr %a: %a@ " Printers.pp_expr expr
680
          (* Types. *)
681
          print_ty resulting_ty);
682
    resulting_ty
683

  
684
  and type_branches ?(is_annot = false) env in_main loc const hl =
685
    let typ_in = new_var () in
686
    let typ_out = new_var () in
687
    try
688
      let used_labels =
680 689
        List.fold_left
681
          (fun uvs v -> ISet.add v.var_id uvs)
682
          ISet.empty c.locals
690
          (fun accu (t, h) ->
691
            unify typ_in (type_const ~is_annot loc (Const_tag t));
692
            type_subtyping_arg env in_main const h typ_out;
693
            if List.mem t accu then raise (Error (loc, Already_bound t))
694
            else t :: accu)
695
          [] hl
683 696
      in
684
      let _ =
697
      let type_labels = get_enum_type_tags (coretype_type typ_in) in
698
      if List.sort compare used_labels <> List.sort compare type_labels then
699
        let unbound_tag =
700
          List.find (fun t -> not (List.mem t used_labels)) type_labels
701
        in
702
        raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag)))
703
      else typ_in, typ_out
704
    with Unify (t1, t2) -> raise (Error (loc, Type_clash (t1, t2)))
705

  
706
  (* Eexpr are always in annotations. TODO: add the quantifiers variables to the
707
     env *)
708
  let type_eexpr env eexpr =
709
    type_expr ~is_annot:true env false (* not in main *) false (* not a const *)
710
      eexpr.eexpr_qfexpr
711

  
712
  (** [type_eq env eq] types equation [eq] in environment [env] *)
713
  let type_eq env in_main undefined_vars eq =
714
    (*Format.eprintf "Typing.type_eq %a@." Printers.pp_node_eq eq;*)
715
    (* Check undefined variables, type lhs *)
716
    let expr_lhs =
717
      expr_of_expr_list eq.eq_loc
718
        (List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs)
719
    in
720
    let ty_lhs = type_expr env in_main false expr_lhs in
721
    (* Check multiple variable definitions *)
722
    let define_var id uvars =
723
      if ISet.mem id uvars then ISet.remove id uvars
724
      else raise (Error (eq.eq_loc, Already_defined id))
725
    in
726
    (* check assignment of declared constant, assignment of clock *)
727
    let ty_lhs =
728
      type_of_type_list
729
        (List.map2
730
           (fun ty id ->
731
             if get_static_value ty <> None then
732
               raise (Error (eq.eq_loc, Assigned_constant id))
733
             else match get_clock_base_type ty with None -> ty | Some ty -> ty)
734
           (type_list_of_type ty_lhs) eq.eq_lhs)
735
    in
736
    let undefined_vars =
737
      List.fold_left
738
        (fun uvars v -> define_var v uvars)
739
        undefined_vars eq.eq_lhs
740
    in
741
    (* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be
742
       assigned to a (always non-constant) lhs variable *)
743
    type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;
744
    undefined_vars
745

  
746
  (* [type_coreclock env ck id loc] types the type clock declaration [ck] in
747
     environment [env] *)
748
  let type_coreclock env ck id loc =
749
    match ck.ck_dec_desc with
750
    | Ckdec_any ->
751
      ()
752
    | Ckdec_bool cl ->
753
      let dummy_id_expr = expr_of_ident id loc in
754
      let when_expr =
685 755
        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
756
          (fun expr (x, l) ->
757
            {
758
              expr_tag = new_tag ();
759
              expr_desc = Expr_when (expr, x, l);
760
              expr_type = Types.Main.new_var ();
761
              expr_clock = Clocks.new_var true;
762
              expr_delay = Delay.new_var ();
763
              expr_loc = loc;
764
              expr_annot = None;
765
            })
766
          dummy_id_expr cl
693 767
      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
       *)
768
      ignore (type_expr env false false when_expr)
769

  
770
  let rec check_type_declaration loc cty =
771
    match cty with
772
    | Tydec_clock ty | Tydec_array (_, ty) ->
773
      check_type_declaration loc ty
774
    | Tydec_const tname ->
775
      (* Format.eprintf "TABLE: %a@." print_type_table (); *)
776
      if not (Hashtbl.mem type_table cty) then
777
        raise (Error (loc, Unbound_type tname))
778
    | _ ->
779
      ()
780

  
781
  let type_var_decl vd_env env vdecl =
782
    (*Format.eprintf "Typing.type_var_decl START %a:%a@." Printers.pp_var vdecl
783
      Printers.print_dec_ty vdecl.var_dec_type.ty_dec_desc;*)
784
    check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
785
    let eval_const id =
786
      (* Types. *)
787
      get_static_value (Env.lookup_value env id)
788
    in
789
    let type_dim d =
790
      type_subtyping_arg (env, vd_env) false true (expr_of_dimension d)
791
        (* Type_predef. *)
792
        type_int;
793
      Dimension.eval Basic_library.eval_dim_env eval_const d
794
    in
795
    let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
796

  
797
    let ty_static =
798
      if vdecl.var_dec_const then
799
        (* Type_predef. *)
800
        type_static (Dimension.mkdim_var ()) ty
801
      else ty
802
    in
803
    (match vdecl.var_dec_value with
804
    | None ->
805
      ()
806
    | Some v ->
807
      type_subtyping_arg (env, vd_env) false ~sub:false true v ty_static);
808
    try_unify ty_static (Expr_type_hub.import vdecl.var_type) vdecl.var_loc;
809
    let new_env = Env.add_value env vdecl.var_id ty_static in
810
    type_coreclock (new_env, vd_env) vdecl.var_dec_clock vdecl.var_id
811
      vdecl.var_loc;
812
    (*Format.eprintf "END %a@." Types.print_ty ty_static;*)
813
    new_env
814

  
815
  let type_var_decl_list vd_env env l =
816
    List.fold_left (type_var_decl vd_env) env l
817

  
818
  let type_of_vlist vars =
819
    let tyl = List.map (fun v -> Expr_type_hub.import v.var_type) vars in
820
    type_of_type_list tyl
821

  
822
  let add_vdecl vd_env vdecl =
823
    if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env then
824
      raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
825
    else vdecl :: vd_env
826

  
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff