Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / init_calculus.ml @ b38ffff3

History | View | Annotate | Download (11.1 KB)

1
(********************************************************************)
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

    
12
(** Main typing module. Classic inference algorithm with destructive
13
    unification. *)
14

    
15
(* Though it shares similarities with the clock calculus module, no code
16
    is shared.  Simple environments, very limited identifier scoping, no
17
    identifier redefinition allowed. *)
18

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

    
26
(** [occurs tvar ty] returns true if the type variable [tvar] occurs in
27
    type [ty]. False otherwise. *)
28
let rec occurs tvar ty =
29
  let ty = repr ty in
30
  match ty.tdesc with
31
  | Ivar -> ty=tvar
32
  | Iarrow (t1, t2) ->
33
      (occurs tvar t1) || (occurs tvar t2)
34
  | Ituple tl ->
35
      List.exists (occurs tvar) tl
36
  | Ilink t -> occurs tvar t
37
  | Isucc t -> occurs tvar t
38
  | Iunivar -> false
39

    
40
(** Promote monomorphic type variables to polymorphic type variables. *)
41
(* Generalize by side-effects *)
42
let rec generalize ty =
43
  match ty.tdesc with
44
  | Ivar ->
45
      (* No scopes, always generalize *)
46
      ty.idesc <- Iunivar
47
  | Iarrow (t1,t2) ->
48
      generalize t1; generalize t2
49
  | Ituple tlist ->
50
      List.iter generalize tlist
51
  | Ilink t ->
52
      generalize t
53
  | Isucc t ->
54
      generalize t
55
  | Tunivar -> ()
56

    
57
(** Downgrade polymorphic type variables to monomorphic type variables *)
58
let rec instanciate inst_vars ty =
59
  let ty = repr ty in
60
  match ty.idesc with
61
  | Ivar -> ty
62
  | Iarrow (t1,t2) ->
63
      {ty with idesc =
64
       Iarrow ((instanciate inst_vars t1), (instanciate inst_vars t2))}
65
  | Ituple tlist ->
66
      {ty with idesc = Ituple (List.map (instanciate inst_vars) tlist)}
67
  | Isucc t ->
68
	(* should not happen *)
69
	{ty with idesc = Isucc (instanciate inst_vars t)}
70
  | Ilink t ->
71
	(* should not happen *)
72
	{ty with idesc = Ilink (instanciate inst_vars t)}
73
  | Iunivar ->
74
      try
75
        List.assoc ty.iid !inst_vars
76
      with Not_found ->
77
        let var = new_var () in
78
	inst_vars := (ty.iid, var)::!inst_vars;
79
	var
80

    
81
(** [unify env t1 t2] unifies types [t1] and [t2]. Raises [Unify
82
    (t1,t2)] if the types are not unifiable.*)
83

    
84
(* Standard destructive unification *)
85
(* may loop for omega types *)
86
let rec unify t1 t2 =
87
  let t1 = repr t1 in
88
  let t2 = repr t2 in
89
  if t1=t2 then
90
    ()
91
  else
92
    (* No type abbreviations resolution for now *)
93
    match t1.idesc,t2.idesc with
94
      (* This case is not mandory but will keep "older" types *)
95
    | Ivar, Ivar ->
96
        if t1.iid < t2.iid then
97
          t2.idesc <- Ilink t1
98
        else
99
          t1.idesc <- Ilink t2
100
    | (Ivar, _) when (not (occurs t1 t2)) ->
101
        t1.idesc <- Ilink t2
102
    | (_,Ivar) when (not (occurs t2 t1)) ->
103
        t2.idesc <- Ilink t1
104
    | Isucc t1, Isucc t1' -> unify t1 t1'
105
    | Iarrow (t1,t2), Iarrow (t1',t2') ->
106
        unify t1 t1'; unify t2 t2'
107
    | Ituple tlist1, Ituple tlist2 ->
108
        if (List.length tlist1) <> (List.length tlist2) then
109
	  raise (Unify (t1, t2))
110
	else
111
          List.iter2 unify tlist1 tlist2
112
    | Iunivar,_ | _, Iunivar -> 
113
        ()
114
    | _,_ -> raise (Unify (t1, t2))
115

    
116
let init_of_const c = 
117
 Init_predef.init_zero
118

    
119
let rec init_expect env in_main expr ty =
120
  let texpr = init_expr env in_main expr in
121
  try
122
    unify texpr ty
123
  with Unify (t1,t2) ->
124
    raise (Error (expr.expr_loc, Init_clash (t1,t2)))
125

    
126
and init_ident env in_main id loc = 
127
  init_expr env in_main (expr_of_ident id loc)
128

    
129
(** [type_expr env in_main expr] types expression [expr] in environment
130
    [env]. *)
131
and init_expr env in_main expr =
132
  match expr.expr_desc with
133
  | Expr_const c ->
134
      let ty = init_of_const c in
135
      expr.expr_init <- ty;
136
      ty
137
  | Expr_ident v ->
138
      let tyv =
139
        try
140
          Env.lookup_value env v
141
        with Not_found ->
142
          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
  | Expr_tuple elist ->
148
      let ty = new_ty (Ttuple (List.map (type_expr env in_main) elist)) in
149
      expr.expr_init <- ty;
150
      ty
151
  | Expr_appl (id, args, r) ->
152
    (match r with
153
    | None   -> ()
154
    | Some x -> let expr_x = expr_of_ident x expr.expr_loc in
155
		init_expect env in_main expr_x Init_predef.init_zero);
156
      let tfun = type_ident env in_main id expr.expr_loc in
157
      let tins,touts= split_arrow tfun in
158
      type_expect env in_main args tins;
159
      expr.expr_type <- touts;
160
      touts
161
  | Expr_arrow (e1,e2) ->
162
      let ty = type_expr env in_main e1 in
163
      type_expect env in_main e2 ty;
164
      expr.expr_type <- ty;
165
      ty
166
  | Expr_fby (init,e) ->
167
      let ty = type_of_const init in
168
      type_expect env in_main e ty;
169
      expr.expr_type <- ty;
170
      ty
171
  | Expr_concat (hd,e) ->
172
      let ty = type_of_const hd in
173
      type_expect env in_main e ty;
174
      expr.expr_type <- ty;
175
      ty
176
  | Expr_tail e ->
177
      let ty = type_expr env in_main e in
178
      expr.expr_type <- ty;
179
      ty
180
  | Expr_pre e ->
181
      let ty = type_expr env in_main e in
182
      expr.expr_type <- ty;
183
      ty
184
  | Expr_when (e1,c) | Expr_whennot (e1,c) ->
185
      let expr_c = expr_of_ident c expr.expr_loc in
186
      type_expect env in_main expr_c Type_predef.type_bool;
187
      let tlarg = type_expr env in_main e1 in
188
      expr.expr_type <- tlarg;
189
      tlarg
190
  | Expr_merge (c,e2,e3) ->
191
      let expr_c = expr_of_ident c expr.expr_loc in
192
      type_expect env in_main expr_c Type_predef.type_bool;
193
      let te2 = type_expr env in_main e2 in
194
      type_expect env in_main e3 te2;
195
      expr.expr_type <- te2;
196
      te2
197
  | Expr_uclock (e,k) | Expr_dclock (e,k) ->
198
      let ty = type_expr env in_main e in
199
      expr.expr_type <- ty;
200
      ty
201
  | Expr_phclock (e,q) ->
202
      let ty = type_expr env in_main e in
203
      expr.expr_type <- ty;
204
      ty
205

    
206
(** [type_eq env eq] types equation [eq] in environment [env] *)
207
let type_eq env in_main undefined_vars eq =
208
  (* Check multiple variable definitions *)
209
  let define_var id uvars =
210
    try
211
      ignore(IMap.find id uvars);
212
      IMap.remove id uvars
213
    with Not_found ->
214
      raise (Error (eq.eq_loc, Already_defined id))
215
  in
216
  let undefined_vars =
217
    List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in
218
  (* Type lhs *)
219
  let get_value_type id =
220
    try
221
      Env.lookup_value env id
222
    with Not_found ->
223
      raise (Error (eq.eq_loc, Unbound_value id))
224
  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
  (* Type rhs *) 
228
  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
  | Tydec_any -> new_var ()
235
  | Tydec_int -> Type_predef.type_int
236
  | Tydec_real -> Type_predef.type_real
237
  | Tydec_float -> Type_predef.type_real
238
  | Tydec_bool -> Type_predef.type_bool
239
  | Tydec_clock -> Type_predef.type_clock
240

    
241
(* [type_coreclock env ck id loc] types the type clock declaration [ck]
242
   in environment [env] *)
243
let type_coreclock env ck id loc =
244
  match ck.ck_dec_desc with
245
  | Ckdec_any | Ckdec_pclock (_,_) -> ()
246
  | Ckdec_bool cl ->
247
      let dummy_id_expr = expr_of_ident id loc in
248
      let when_expr =
249
        List.fold_left
250
          (fun expr c ->
251
            match c with
252
            | Wtrue id ->
253
                {expr_tag = new_tag ();
254
                 expr_desc=Expr_when (expr,id);
255
                 expr_type = new_var ();
256
                 expr_clock = Clocks.new_var true;
257
                 expr_loc=loc}
258
            | Wfalse id ->
259
                {expr_tag = new_tag ();
260
                 expr_desc=Expr_whennot (expr,id);
261
                 expr_type = new_var ();
262
                 expr_clock = Clocks.new_var true;
263
                 expr_loc=loc})
264
          dummy_id_expr cl
265
      in
266
      ignore (type_expr env false when_expr)
267

    
268
let type_var_decl env vdecl =
269
  if (Env.exists_value env vdecl.var_id) then
270
    raise (Error (vdecl.var_loc,Already_bound vdecl.var_id))
271
  else
272
    let ty = type_coretype vdecl.var_dec_type.ty_dec_desc in
273
    let new_env = Env.add_value env vdecl.var_id ty in
274
    type_coreclock new_env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
275
    vdecl.var_type <- ty;
276
    new_env
277

    
278
let type_var_decl_list env l =
279
  List.fold_left type_var_decl env l
280

    
281
let type_of_vlist vars =
282
  let tyl = List.map (fun v -> v.var_type) vars in
283
  type_of_type_list tyl
284
      
285
(** [type_node env nd loc] types node [nd] in environment env. The
286
    location is used for error reports. *)
287
let type_node env nd loc =
288
  let is_main = nd.node_id = !Options.main_node in
289
  let delta_env = type_var_decl_list IMap.empty nd.node_inputs in
290
  let delta_env = type_var_decl_list delta_env nd.node_outputs in
291
  let delta_env = type_var_decl_list delta_env nd.node_locals in
292
  let new_env = Env.overwrite env delta_env in
293
  let undefined_vars_init =
294
    List.fold_left
295
      (fun uvs v -> IMap.add v.var_id () uvs)
296
      IMap.empty (nd.node_outputs@nd.node_locals) in
297
  let undefined_vars =
298
    List.fold_left (type_eq new_env is_main) undefined_vars_init nd.node_eqs
299
  in
300
  (* check that table is empty *)
301
  if (not (IMap.is_empty undefined_vars)) then
302
    raise (Error (loc,Undefined_var undefined_vars));
303
  let ty_ins = type_of_vlist nd.node_inputs in
304
  let ty_outs = type_of_vlist nd.node_outputs in
305
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
306
  generalize ty_node;
307
  (* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
308
  nd.node_type <- ty_node;
309
  Env.add_value env nd.node_id ty_node
310

    
311
let type_imported_node env nd loc =
312
  let new_env = type_var_decl_list env nd.nodei_inputs in
313
  ignore(type_var_decl_list new_env nd.nodei_outputs);
314
  let ty_ins = type_of_vlist nd.nodei_inputs in
315
  let ty_outs = type_of_vlist nd.nodei_outputs in
316
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
317
  generalize ty_node;
318
  if (is_polymorphic ty_node) then
319
    raise (Error (loc, Poly_imported_node nd.nodei_id));
320
  let new_env = Env.add_value env nd.nodei_id ty_node in
321
  nd.nodei_type <- ty_node;
322
  new_env
323

    
324
let type_top_decl env decl =
325
  match decl.top_decl_desc with
326
  | Node nd -> 
327
      type_node env nd decl.top_decl_loc
328
  | ImportedNode nd ->
329
      type_imported_node env nd decl.top_decl_loc
330
  | SensorDecl _ | ActuatorDecl _ | Consts _ -> env
331

    
332
let type_top_consts env decl =
333
  match decl.top_decl_desc with
334
    | Consts clist -> 
335
      List.fold_left (fun env (id, c) ->
336
	let ty = type_of_const c in
337
	Env.add_value env id ty       
338
      ) env clist
339
    | Node _ | ImportedNode _ | SensorDecl _ | ActuatorDecl _ -> env
340

    
341
let type_prog env decls =
342
  let new_env = List.fold_left type_top_consts env decls in
343
  ignore(List.fold_left type_top_decl new_env decls)
344

    
345
(* Local Variables: *)
346
(* compile-command:"make -C .." *)
347
(* End: *)