Project

General

Profile

Download (11 KB) Statistics
| Branch: | Tag: | Revision:
1 b38ffff3 ploc
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
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
(********************************************************************)
11 0cbf0839 ploc
12
(** Main typing module. Classic inference algorithm with destructive
13
    unification. *)
14
15 ca7ff3f7 Lélio Brun
(* Though it shares similarities with the clock calculus module, no code is
16
   shared. Simple environments, very limited identifier scoping, no identifier
17
   redefinition allowed. *)
18 0cbf0839 ploc
19
open Utils
20 ca7ff3f7 Lélio Brun
21
(* Yes, opening both modules is dirty as some type names will be overwritten,
22
   yet this makes notations far lighter.*)
23 0cbf0839 ploc
open Corelang
24
open Init
25
open Format
26
27 ca7ff3f7 Lélio Brun
(** [occurs tvar ty] returns true if the type variable [tvar] occurs in type
28
    [ty]. False otherwise. *)
29 0cbf0839 ploc
let rec occurs tvar ty =
30
  let ty = repr ty in
31
  match ty.tdesc with
32 ca7ff3f7 Lélio Brun
  | Ivar ->
33
    ty = tvar
34 0cbf0839 ploc
  | Iarrow (t1, t2) ->
35 ca7ff3f7 Lélio Brun
    occurs tvar t1 || occurs tvar t2
36 0cbf0839 ploc
  | Ituple tl ->
37 ca7ff3f7 Lélio Brun
    List.exists (occurs tvar) tl
38
  | Ilink t ->
39
    occurs tvar t
40
  | Isucc t ->
41
    occurs tvar t
42
  | Iunivar ->
43
    false
44 0cbf0839 ploc
45
(* Generalize by side-effects *)
46 ca7ff3f7 Lélio Brun
47
(** Promote monomorphic type variables to polymorphic type variables. *)
48 0cbf0839 ploc
let rec generalize ty =
49
  match ty.tdesc with
50
  | Ivar ->
51 ca7ff3f7 Lélio Brun
    (* No scopes, always generalize *)
52
    ty.idesc <- Iunivar
53
  | Iarrow (t1, t2) ->
54
    generalize t1;
55
    generalize t2
56 0cbf0839 ploc
  | Ituple tlist ->
57 ca7ff3f7 Lélio Brun
    List.iter generalize tlist
58 0cbf0839 ploc
  | Ilink t ->
59 ca7ff3f7 Lélio Brun
    generalize t
60 0cbf0839 ploc
  | Isucc t ->
61 ca7ff3f7 Lélio Brun
    generalize t
62
  | Tunivar ->
63
    ()
64 0cbf0839 ploc
65
(** Downgrade polymorphic type variables to monomorphic type variables *)
66
let rec instanciate inst_vars ty =
67
  let ty = repr ty in
68
  match ty.idesc with
69 ca7ff3f7 Lélio Brun
  | Ivar ->
70
    ty
71
  | Iarrow (t1, t2) ->
72
    {
73
      ty with
74
      idesc = Iarrow (instanciate inst_vars t1, instanciate inst_vars t2);
75
    }
76 0cbf0839 ploc
  | Ituple tlist ->
77 ca7ff3f7 Lélio Brun
    { ty with idesc = Ituple (List.map (instanciate inst_vars) tlist) }
78 0cbf0839 ploc
  | Isucc t ->
79 ca7ff3f7 Lélio Brun
    (* should not happen *)
80
    { ty with idesc = Isucc (instanciate inst_vars t) }
81 0cbf0839 ploc
  | Ilink t ->
82 ca7ff3f7 Lélio Brun
    (* should not happen *)
83
    { ty with idesc = Ilink (instanciate inst_vars t) }
84
  | Iunivar -> (
85
    try List.assoc ty.iid !inst_vars
86
    with Not_found ->
87
      let var = new_var () in
88
      inst_vars := (ty.iid, var) :: !inst_vars;
89
      var)
90 0cbf0839 ploc
91 ca7ff3f7 Lélio Brun
(** [unify env t1 t2] unifies types [t1] and [t2]. Raises [Unify (t1,t2)] if the
92
    types are not unifiable.*)
93 0cbf0839 ploc
94
(* Standard destructive unification *)
95
(* may loop for omega types *)
96
let rec unify t1 t2 =
97
  let t1 = repr t1 in
98
  let t2 = repr t2 in
99 ca7ff3f7 Lélio Brun
  if t1 = t2 then ()
100 0cbf0839 ploc
  else
101
    (* No type abbreviations resolution for now *)
102 ca7ff3f7 Lélio Brun
    match t1.idesc, t2.idesc with
103
    (* This case is not mandory but will keep "older" types *)
104 0cbf0839 ploc
    | Ivar, Ivar ->
105 ca7ff3f7 Lélio Brun
      if t1.iid < t2.iid then t2.idesc <- Ilink t1 else t1.idesc <- Ilink t2
106
    | Ivar, _ when not (occurs t1 t2) ->
107
      t1.idesc <- Ilink t2
108
    | _, Ivar when not (occurs t2 t1) ->
109
      t2.idesc <- Ilink t1
110
    | Isucc t1, Isucc t1' ->
111
      unify t1 t1'
112
    | Iarrow (t1, t2), Iarrow (t1', t2') ->
113
      unify t1 t1';
114
      unify t2 t2'
115 0cbf0839 ploc
    | Ituple tlist1, Ituple tlist2 ->
116 ca7ff3f7 Lélio Brun
      if List.length tlist1 <> List.length tlist2 then raise (Unify (t1, t2))
117
      else List.iter2 unify tlist1 tlist2
118
    | Iunivar, _ | _, Iunivar ->
119
      ()
120
    | _, _ ->
121
      raise (Unify (t1, t2))
122 0cbf0839 ploc
123 ca7ff3f7 Lélio Brun
let init_of_const c = Init_predef.init_zero
124 0cbf0839 ploc
125
let rec init_expect env in_main expr ty =
126
  let texpr = init_expr env in_main expr in
127 ca7ff3f7 Lélio Brun
  try unify texpr ty
128
  with Unify (t1, t2) -> raise (Error (expr.expr_loc, Init_clash (t1, t2)))
129 0cbf0839 ploc
130 ca7ff3f7 Lélio Brun
and init_ident env in_main id loc = init_expr env in_main (expr_of_ident id loc)
131 0cbf0839 ploc
132 ca7ff3f7 Lélio Brun
(** [type_expr env in_main expr] types expression [expr] in environment [env]. *)
133 0cbf0839 ploc
and init_expr env in_main expr =
134
  match expr.expr_desc with
135
  | Expr_const c ->
136 ca7ff3f7 Lélio Brun
    let ty = init_of_const c in
137
    expr.expr_init <- ty;
138
    ty
139 0cbf0839 ploc
  | Expr_ident v ->
140 ca7ff3f7 Lélio Brun
    let tyv =
141
      try Env.lookup_value env v
142
      with Not_found -> raise (Error (expr.expr_loc, Unbound_value v))
143
    in
144
    let ty = instanciate (ref []) tyv in
145
    expr.expr_init <- ty;
146
    ty
147 0cbf0839 ploc
  | Expr_tuple elist ->
148 ca7ff3f7 Lélio Brun
    let ty = new_ty (Ttuple (List.map (type_expr env in_main) elist)) in
149
    expr.expr_init <- ty;
150
    ty
151 0cbf0839 ploc
  | Expr_appl (id, args, r) ->
152
    (match r with
153 ca7ff3f7 Lélio Brun
    | None ->
154
      ()
155
    | Some x ->
156
      let expr_x = expr_of_ident x expr.expr_loc in
157
      init_expect env in_main expr_x Init_predef.init_zero);
158
    let tfun = type_ident env in_main id expr.expr_loc in
159
    let tins, touts = split_arrow tfun in
160
    type_expect env in_main args tins;
161
    expr.expr_type <- touts;
162
    touts
163
  | Expr_arrow (e1, e2) ->
164
    let ty = type_expr env in_main e1 in
165
    type_expect env in_main e2 ty;
166
    expr.expr_type <- ty;
167
    ty
168
  | Expr_fby (init, e) ->
169
    let ty = type_of_const init in
170
    type_expect env in_main e ty;
171
    expr.expr_type <- ty;
172
    ty
173
  | Expr_concat (hd, e) ->
174
    let ty = type_of_const hd in
175
    type_expect env in_main e ty;
176
    expr.expr_type <- ty;
177
    ty
178 0cbf0839 ploc
  | Expr_tail e ->
179 ca7ff3f7 Lélio Brun
    let ty = type_expr env in_main e in
180
    expr.expr_type <- ty;
181
    ty
182 0cbf0839 ploc
  | Expr_pre e ->
183 ca7ff3f7 Lélio Brun
    let ty = type_expr env in_main e in
184
    expr.expr_type <- ty;
185
    ty
186
  | Expr_when (e1, c) | Expr_whennot (e1, c) ->
187
    let expr_c = expr_of_ident c expr.expr_loc in
188
    type_expect env in_main expr_c Type_predef.type_bool;
189
    let tlarg = type_expr env in_main e1 in
190
    expr.expr_type <- tlarg;
191
    tlarg
192
  | Expr_merge (c, e2, e3) ->
193
    let expr_c = expr_of_ident c expr.expr_loc in
194
    type_expect env in_main expr_c Type_predef.type_bool;
195
    let te2 = type_expr env in_main e2 in
196
    type_expect env in_main e3 te2;
197
    expr.expr_type <- te2;
198
    te2
199
  | Expr_uclock (e, k) | Expr_dclock (e, k) ->
200
    let ty = type_expr env in_main e in
201
    expr.expr_type <- ty;
202
    ty
203
  | Expr_phclock (e, q) ->
204
    let ty = type_expr env in_main e in
205
    expr.expr_type <- ty;
206
    ty
207 0cbf0839 ploc
208
(** [type_eq env eq] types equation [eq] in environment [env] *)
209
let type_eq env in_main undefined_vars eq =
210
  (* Check multiple variable definitions *)
211
  let define_var id uvars =
212
    try
213 ca7ff3f7 Lélio Brun
      ignore (IMap.find id uvars);
214 0cbf0839 ploc
      IMap.remove id uvars
215 ca7ff3f7 Lélio Brun
    with Not_found -> raise (Error (eq.eq_loc, Already_defined id))
216 0cbf0839 ploc
  in
217
  let undefined_vars =
218 ca7ff3f7 Lélio Brun
    List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs
219
  in
220 0cbf0839 ploc
  (* Type lhs *)
221
  let get_value_type id =
222 ca7ff3f7 Lélio Brun
    try Env.lookup_value env id
223
    with Not_found -> raise (Error (eq.eq_loc, Unbound_value id))
224 0cbf0839 ploc
  in
225
  let tyl_lhs = List.map get_value_type eq.eq_lhs in
226
  let ty_lhs = type_of_type_list tyl_lhs in
227 ca7ff3f7 Lélio Brun
  (* Type rhs *)
228 0cbf0839 ploc
  type_expect env in_main eq.eq_rhs ty_lhs;
229
  undefined_vars
230
231
(* [type_coretype cty] types the type declaration [cty] *)
232
let type_coretype cty =
233
  match cty with
234 ca7ff3f7 Lélio Brun
  | Tydec_any ->
235
    new_var ()
236
  | Tydec_int ->
237
    Type_predef.type_int
238
  | Tydec_real ->
239
    Type_predef.type_real
240
  | Tydec_float ->
241
    Type_predef.type_real
242
  | Tydec_bool ->
243
    Type_predef.type_bool
244
  | Tydec_clock ->
245
    Type_predef.type_clock
246 0cbf0839 ploc
247 ca7ff3f7 Lélio Brun
(* [type_coreclock env ck id loc] types the type clock declaration [ck] in
248
   environment [env] *)
249 0cbf0839 ploc
let type_coreclock env ck id loc =
250
  match ck.ck_dec_desc with
251 ca7ff3f7 Lélio Brun
  | Ckdec_any | Ckdec_pclock (_, _) ->
252
    ()
253 0cbf0839 ploc
  | Ckdec_bool cl ->
254 ca7ff3f7 Lélio Brun
    let dummy_id_expr = expr_of_ident id loc in
255
    let when_expr =
256
      List.fold_left
257
        (fun expr c ->
258
          match c with
259
          | Wtrue id ->
260
            {
261
              expr_tag = new_tag ();
262
              expr_desc = Expr_when (expr, id);
263
              expr_type = new_var ();
264
              expr_clock = Clocks.new_var true;
265
              expr_loc = loc;
266
            }
267
          | Wfalse id ->
268
            {
269
              expr_tag = new_tag ();
270
              expr_desc = Expr_whennot (expr, id);
271
              expr_type = new_var ();
272
              expr_clock = Clocks.new_var true;
273
              expr_loc = loc;
274
            })
275
        dummy_id_expr cl
276
    in
277
    ignore (type_expr env false when_expr)
278 0cbf0839 ploc
279
let type_var_decl env vdecl =
280 ca7ff3f7 Lélio Brun
  if Env.exists_value env vdecl.var_id then
281
    raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
282 0cbf0839 ploc
  else
283
    let ty = type_coretype vdecl.var_dec_type.ty_dec_desc in
284
    let new_env = Env.add_value env vdecl.var_id ty in
285
    type_coreclock new_env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
286
    vdecl.var_type <- ty;
287
    new_env
288
289 ca7ff3f7 Lélio Brun
let type_var_decl_list env l = List.fold_left type_var_decl env l
290 0cbf0839 ploc
291
let type_of_vlist vars =
292
  let tyl = List.map (fun v -> v.var_type) vars in
293
  type_of_type_list tyl
294 ca7ff3f7 Lélio Brun
295
(** [type_node env nd loc] types node [nd] in environment env. The location is
296
    used for error reports. *)
297 0cbf0839 ploc
let type_node env nd loc =
298
  let is_main = nd.node_id = !Options.main_node in
299
  let delta_env = type_var_decl_list IMap.empty nd.node_inputs in
300
  let delta_env = type_var_decl_list delta_env nd.node_outputs in
301
  let delta_env = type_var_decl_list delta_env nd.node_locals in
302
  let new_env = Env.overwrite env delta_env in
303
  let undefined_vars_init =
304
    List.fold_left
305
      (fun uvs v -> IMap.add v.var_id () uvs)
306 ca7ff3f7 Lélio Brun
      IMap.empty
307
      (nd.node_outputs @ nd.node_locals)
308
  in
309 0cbf0839 ploc
  let undefined_vars =
310
    List.fold_left (type_eq new_env is_main) undefined_vars_init nd.node_eqs
311
  in
312
  (* check that table is empty *)
313 ca7ff3f7 Lélio Brun
  if not (IMap.is_empty undefined_vars) then
314
    raise (Error (loc, Undefined_var undefined_vars));
315 0cbf0839 ploc
  let ty_ins = type_of_vlist nd.node_inputs in
316
  let ty_outs = type_of_vlist nd.node_outputs in
317 ca7ff3f7 Lélio Brun
  let ty_node = new_ty (Tarrow (ty_ins, ty_outs)) in
318 0cbf0839 ploc
  generalize ty_node;
319
  (* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
320
  nd.node_type <- ty_node;
321
  Env.add_value env nd.node_id ty_node
322
323
let type_imported_node env nd loc =
324
  let new_env = type_var_decl_list env nd.nodei_inputs in
325 ca7ff3f7 Lélio Brun
  ignore (type_var_decl_list new_env nd.nodei_outputs);
326 0cbf0839 ploc
  let ty_ins = type_of_vlist nd.nodei_inputs in
327
  let ty_outs = type_of_vlist nd.nodei_outputs in
328 ca7ff3f7 Lélio Brun
  let ty_node = new_ty (Tarrow (ty_ins, ty_outs)) in
329 0cbf0839 ploc
  generalize ty_node;
330 ca7ff3f7 Lélio Brun
  if is_polymorphic ty_node then
331 0cbf0839 ploc
    raise (Error (loc, Poly_imported_node nd.nodei_id));
332
  let new_env = Env.add_value env nd.nodei_id ty_node in
333
  nd.nodei_type <- ty_node;
334
  new_env
335
336
let type_top_decl env decl =
337
  match decl.top_decl_desc with
338 ca7ff3f7 Lélio Brun
  | Node nd ->
339
    type_node env nd decl.top_decl_loc
340 0cbf0839 ploc
  | ImportedNode nd ->
341 ca7ff3f7 Lélio Brun
    type_imported_node env nd decl.top_decl_loc
342
  | SensorDecl _ | ActuatorDecl _ | Consts _ ->
343
    env
344 0cbf0839 ploc
345
let type_top_consts env decl =
346
  match decl.top_decl_desc with
347 ca7ff3f7 Lélio Brun
  | Consts clist ->
348
    List.fold_left
349
      (fun env (id, c) ->
350
        let ty = type_of_const c in
351
        Env.add_value env id ty)
352
      env clist
353
  | Node _ | ImportedNode _ | SensorDecl _ | ActuatorDecl _ ->
354
    env
355 0cbf0839 ploc
356
let type_prog env decls =
357
  let new_env = List.fold_left type_top_consts env decls in
358 ca7ff3f7 Lélio Brun
  ignore (List.fold_left type_top_decl new_env decls)
359 0cbf0839 ploc
360
(* Local Variables: *)
361
(* compile-command:"make -C .." *)
362
(* End: *)