Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / init_calculus.ml @ 22fe1c93

History | View | Annotate | Download (11.5 KB)

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