lustrec / src / init_calculus.ml @ 0cbf0839
History | View | Annotate | Download (11.5 KB)
1 |
(* ---------------------------------------------------------------------------- |
---|---|
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: *) |