lustrec / src / corelang.ml @ 4f26dcf5
History | View | Annotate | Download (39.3 KB)
1 | a2d97a3e | 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 | |||
12 | 22fe1c93 | ploc | open Format |
13 | 8446bf03 | ploc | open Lustre_types |
14 | open Machine_code_types |
||
15 | 7d640c88 | ploc | (*open Dimension*) |
16 | 22fe1c93 | ploc | |
17 | |||
18 | e7cc5186 | ploc | exception Error of Location.t * Error.error_kind |
19 | 22fe1c93 | ploc | |
20 | module VDeclModule = |
||
21 | struct (* Node module *) |
||
22 | type t = var_decl |
||
23 | bb2ca5f4 | xthirioux | let compare v1 v2 = compare v1.var_id v2.var_id |
24 | 22fe1c93 | ploc | end |
25 | |||
26 | module VMap = Map.Make(VDeclModule) |
||
27 | |||
28 | 089f94be | ploc | module VSet : Set.S with type elt = var_decl = Set.Make(VDeclModule) |
29 | 22fe1c93 | ploc | |
30 | 01c7d5e1 | ploc | let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc} |
31 | |||
32 | let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc} |
||
33 | |||
34 | |||
35 | |||
36 | 22fe1c93 | ploc | (************************************************************) |
37 | (* *) |
||
38 | |||
39 | let mktyp loc d = |
||
40 | { ty_dec_desc = d; ty_dec_loc = loc } |
||
41 | |||
42 | let mkclock loc d = |
||
43 | { ck_dec_desc = d; ck_dec_loc = loc } |
||
44 | |||
45 | 66359a5e | ploc | let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value, parentid) = |
46 | ec433d69 | xthirioux | assert (value = None || is_const); |
47 | 22fe1c93 | ploc | { var_id = id; |
48 | 54d032f5 | xthirioux | var_orig = orig; |
49 | 22fe1c93 | ploc | var_dec_type = ty_dec; |
50 | var_dec_clock = ck_dec; |
||
51 | var_dec_const = is_const; |
||
52 | ec433d69 | xthirioux | var_dec_value = value; |
53 | 66359a5e | ploc | var_parent_nodeid = parentid; |
54 | 22fe1c93 | ploc | var_type = Types.new_var (); |
55 | var_clock = Clocks.new_var true; |
||
56 | var_loc = loc } |
||
57 | |||
58 | 2863281f | ploc | let dummy_var_decl name typ = |
59 | { |
||
60 | var_id = name; |
||
61 | var_orig = false; |
||
62 | var_dec_type = dummy_type_dec; |
||
63 | var_dec_clock = dummy_clock_dec; |
||
64 | var_dec_const = false; |
||
65 | var_dec_value = None; |
||
66 | var_parent_nodeid = None; |
||
67 | var_type = typ; |
||
68 | var_clock = Clocks.new_ck Clocks.Cvar true; |
||
69 | var_loc = Location.dummy_loc |
||
70 | } |
||
71 | |||
72 | 22fe1c93 | ploc | let mkexpr loc d = |
73 | { expr_tag = Utils.new_tag (); |
||
74 | expr_desc = d; |
||
75 | expr_type = Types.new_var (); |
||
76 | expr_clock = Clocks.new_var true; |
||
77 | expr_delay = Delay.new_var (); |
||
78 | expr_annot = None; |
||
79 | expr_loc = loc } |
||
80 | |||
81 | 66359a5e | ploc | let var_decl_of_const ?(parentid=None) c = |
82 | 22fe1c93 | ploc | { var_id = c.const_id; |
83 | 54d032f5 | xthirioux | var_orig = true; |
84 | 22fe1c93 | ploc | var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any }; |
85 | var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any }; |
||
86 | var_dec_const = true; |
||
87 | ec433d69 | xthirioux | var_dec_value = None; |
88 | 66359a5e | ploc | var_parent_nodeid = parentid; |
89 | 22fe1c93 | ploc | var_type = c.const_type; |
90 | var_clock = Clocks.new_var false; |
||
91 | var_loc = c.const_loc } |
||
92 | |||
93 | b08ffca7 | xthirioux | let mk_new_name used id = |
94 | 22fe1c93 | ploc | let rec new_name name cpt = |
95 | b08ffca7 | xthirioux | if used name |
96 | 22fe1c93 | ploc | then new_name (sprintf "_%s_%i" id cpt) (cpt+1) |
97 | else name |
||
98 | in new_name id 1 |
||
99 | |||
100 | let mkeq loc (lhs, rhs) = |
||
101 | { eq_lhs = lhs; |
||
102 | eq_rhs = rhs; |
||
103 | eq_loc = loc } |
||
104 | |||
105 | let mkassert loc expr = |
||
106 | { assert_loc = loc; |
||
107 | assert_expr = expr |
||
108 | } |
||
109 | |||
110 | ef34b4ae | xthirioux | let mktop_decl loc own itf d = |
111 | { top_decl_desc = d; top_decl_loc = loc; top_decl_owner = own; top_decl_itf = itf } |
||
112 | 22fe1c93 | ploc | |
113 | let mkpredef_call loc funname args = |
||
114 | mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None)) |
||
115 | |||
116 | ec433d69 | xthirioux | let is_clock_dec_type cty = |
117 | match cty with |
||
118 | | Tydec_clock _ -> true |
||
119 | | _ -> false |
||
120 | ef34b4ae | xthirioux | |
121 | let const_of_top top_decl = |
||
122 | match top_decl.top_decl_desc with |
||
123 | | Const c -> c |
||
124 | | _ -> assert false |
||
125 | |||
126 | let node_of_top top_decl = |
||
127 | match top_decl.top_decl_desc with |
||
128 | | Node nd -> nd |
||
129 | 2475c9e8 | ploc | | _ -> raise Not_found |
130 | ef34b4ae | xthirioux | |
131 | let imported_node_of_top top_decl = |
||
132 | match top_decl.top_decl_desc with |
||
133 | | ImportedNode ind -> ind |
||
134 | | _ -> assert false |
||
135 | |||
136 | let typedef_of_top top_decl = |
||
137 | match top_decl.top_decl_desc with |
||
138 | | TypeDef tdef -> tdef |
||
139 | | _ -> assert false |
||
140 | |||
141 | let dependency_of_top top_decl = |
||
142 | match top_decl.top_decl_desc with |
||
143 | | Open (local, dep) -> (local, dep) |
||
144 | | _ -> assert false |
||
145 | |||
146 | let consts_of_enum_type top_decl = |
||
147 | match top_decl.top_decl_desc with |
||
148 | | TypeDef tdef -> |
||
149 | (match tdef.tydef_desc with |
||
150 | 333e3a25 | ploc | | Tydec_enum tags -> |
151 | List.map |
||
152 | (fun tag -> |
||
153 | let cdecl = { |
||
154 | const_id = tag; |
||
155 | const_loc = top_decl.top_decl_loc; |
||
156 | const_value = Const_tag tag; |
||
157 | const_type = Type_predef.type_const tdef.tydef_id |
||
158 | } in |
||
159 | { top_decl with top_decl_desc = Const cdecl }) |
||
160 | tags |
||
161 | ef34b4ae | xthirioux | | _ -> []) |
162 | | _ -> assert false |
||
163 | |||
164 | 01c7d5e1 | ploc | (************************************************************) |
165 | (* Eexpr functions *) |
||
166 | (************************************************************) |
||
167 | |||
168 | 4f26dcf5 | ploc | let merge_contracts ann1 ann2 = |
169 | 01c7d5e1 | ploc | { requires = ann1.requires @ ann2.requires; |
170 | ensures = ann1.ensures @ ann2.ensures; |
||
171 | behaviors = ann1.behaviors @ ann2.behaviors; |
||
172 | spec_loc = ann1.spec_loc |
||
173 | } |
||
174 | |||
175 | let mkeexpr loc expr = |
||
176 | { eexpr_tag = Utils.new_tag (); |
||
177 | eexpr_qfexpr = expr; |
||
178 | eexpr_quantifiers = []; |
||
179 | eexpr_type = Types.new_var (); |
||
180 | eexpr_clock = Clocks.new_var true; |
||
181 | eexpr_normalized = None; |
||
182 | eexpr_loc = loc } |
||
183 | |||
184 | let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers } |
||
185 | |||
186 | (* |
||
187 | let mkepredef_call loc funname args = |
||
188 | mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None)) |
||
189 | |||
190 | let mkepredef_unary_call loc funname arg = |
||
191 | mkeexpr loc (EExpr_appl (funname, arg, None)) |
||
192 | *) |
||
193 | |||
194 | let merge_expr_annot ann1 ann2 = |
||
195 | match ann1, ann2 with |
||
196 | | None, None -> assert false |
||
197 | | Some _, None -> ann1 |
||
198 | | None, Some _ -> ann2 |
||
199 | | Some ann1, Some ann2 -> Some { |
||
200 | annots = ann1.annots @ ann2.annots; |
||
201 | annot_loc = ann1.annot_loc |
||
202 | } |
||
203 | |||
204 | 566dbf49 | ploc | let update_expr_annot node_id e annot = |
205 | List.iter (fun (key, _) -> |
||
206 | Annotations.add_expr_ann node_id e.expr_tag key |
||
207 | ) annot.annots; |
||
208 | 264a4844 | ploc | e.expr_annot <- merge_expr_annot e.expr_annot (Some annot); |
209 | e |
||
210 | 01c7d5e1 | ploc | |
211 | |||
212 | 1b683c9a | ploc | let mkinstr ?lustre_expr ?lustre_eq i = |
213 | 3ca27bc7 | ploc | { |
214 | instr_desc = i; |
||
215 | 1bff14ac | ploc | (* lustre_expr = lustre_expr; *) |
216 | lustre_eq = lustre_eq; |
||
217 | 3ca27bc7 | ploc | } |
218 | |||
219 | let get_instr_desc i = i.instr_desc |
||
220 | let update_instr_desc i id = { i with instr_desc = id } |
||
221 | |||
222 | 22fe1c93 | ploc | (***********************************************************) |
223 | (* Fast access to nodes, by name *) |
||
224 | let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30 |
||
225 | let consts_table = Hashtbl.create 30 |
||
226 | |||
227 | ef34b4ae | xthirioux | let print_node_table fmt () = |
228 | begin |
||
229 | Format.fprintf fmt "{ /* node table */@."; |
||
230 | Hashtbl.iter (fun id nd -> |
||
231 | Format.fprintf fmt "%s |-> %a" |
||
232 | id |
||
233 | Printers.pp_short_decl nd |
||
234 | ) node_table; |
||
235 | Format.fprintf fmt "}@." |
||
236 | end |
||
237 | |||
238 | let print_consts_table fmt () = |
||
239 | begin |
||
240 | Format.fprintf fmt "{ /* consts table */@."; |
||
241 | Hashtbl.iter (fun id const -> |
||
242 | Format.fprintf fmt "%s |-> %a" |
||
243 | id |
||
244 | Printers.pp_const_decl (const_of_top const) |
||
245 | ) consts_table; |
||
246 | Format.fprintf fmt "}@." |
||
247 | end |
||
248 | |||
249 | 22fe1c93 | ploc | let node_name td = |
250 | match td.top_decl_desc with |
||
251 | | Node nd -> nd.node_id |
||
252 | | ImportedNode nd -> nd.nodei_id |
||
253 | | _ -> assert false |
||
254 | |||
255 | let is_generic_node td = |
||
256 | match td.top_decl_desc with |
||
257 | | Node nd -> List.exists (fun v -> v.var_dec_const) nd.node_inputs |
||
258 | | ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs |
||
259 | | _ -> assert false |
||
260 | |||
261 | let node_inputs td = |
||
262 | match td.top_decl_desc with |
||
263 | | Node nd -> nd.node_inputs |
||
264 | | ImportedNode nd -> nd.nodei_inputs |
||
265 | | _ -> assert false |
||
266 | |||
267 | let node_from_name id = |
||
268 | try |
||
269 | Hashtbl.find node_table id |
||
270 | with Not_found -> (Format.eprintf "Unable to find any node named %s@ @?" id; |
||
271 | assert false) |
||
272 | |||
273 | let is_imported_node td = |
||
274 | match td.top_decl_desc with |
||
275 | | Node nd -> false |
||
276 | | ImportedNode nd -> true |
||
277 | | _ -> assert false |
||
278 | |||
279 | 52cfee34 | xthirioux | |
280 | 22fe1c93 | ploc | (* alias and type definition table *) |
281 | ef34b4ae | xthirioux | |
282 | 990210f3 | ploc | let mktop = mktop_decl Location.dummy_loc !Options.dest_dir false |
283 | 1e48ef45 | ploc | |
284 | let top_int_type = mktop (TypeDef {tydef_id = "int"; tydef_desc = Tydec_int}) |
||
285 | let top_bool_type = mktop (TypeDef {tydef_id = "bool"; tydef_desc = Tydec_bool}) |
||
286 | 04a63d25 | xthirioux | (* let top_float_type = mktop (TypeDef {tydef_id = "float"; tydef_desc = Tydec_float}) *) |
287 | 1e48ef45 | ploc | let top_real_type = mktop (TypeDef {tydef_id = "real"; tydef_desc = Tydec_real}) |
288 | ef34b4ae | xthirioux | |
289 | 22fe1c93 | ploc | let type_table = |
290 | Utils.create_hashtable 20 [ |
||
291 | ef34b4ae | xthirioux | Tydec_int , top_int_type; |
292 | Tydec_bool , top_bool_type; |
||
293 | 04a63d25 | xthirioux | (* Tydec_float, top_float_type; *) |
294 | ef34b4ae | xthirioux | Tydec_real , top_real_type |
295 | 22fe1c93 | ploc | ] |
296 | |||
297 | ef34b4ae | xthirioux | let print_type_table fmt () = |
298 | begin |
||
299 | Format.fprintf fmt "{ /* type table */@."; |
||
300 | Hashtbl.iter (fun tydec tdef -> |
||
301 | Format.fprintf fmt "%a |-> %a" |
||
302 | Printers.pp_var_type_dec_desc tydec |
||
303 | Printers.pp_typedef (typedef_of_top tdef) |
||
304 | ) type_table; |
||
305 | Format.fprintf fmt "}@." |
||
306 | end |
||
307 | |||
308 | 22fe1c93 | ploc | let rec is_user_type typ = |
309 | match typ with |
||
310 | | Tydec_int | Tydec_bool | Tydec_real |
||
311 | 04a63d25 | xthirioux | (* | Tydec_float *) | Tydec_any | Tydec_const _ -> false |
312 | 22fe1c93 | ploc | | Tydec_clock typ' -> is_user_type typ' |
313 | | _ -> true |
||
314 | |||
315 | let get_repr_type typ = |
||
316 | ef34b4ae | xthirioux | let typ_def = (typedef_of_top (Hashtbl.find type_table typ)).tydef_desc in |
317 | 22fe1c93 | ploc | if is_user_type typ_def then typ else typ_def |
318 | |||
319 | b1655a21 | xthirioux | let rec coretype_equal ty1 ty2 = |
320 | ef34b4ae | xthirioux | let res = |
321 | b1655a21 | xthirioux | match ty1, ty2 with |
322 | ed81df06 | xthirioux | | Tydec_any , _ |
323 | | _ , Tydec_any -> assert false |
||
324 | | Tydec_const _ , Tydec_const _ -> get_repr_type ty1 = get_repr_type ty2 |
||
325 | ef34b4ae | xthirioux | | Tydec_const _ , _ -> let ty1' = (typedef_of_top (Hashtbl.find type_table ty1)).tydef_desc |
326 | ed81df06 | xthirioux | in (not (is_user_type ty1')) && coretype_equal ty1' ty2 |
327 | | _ , Tydec_const _ -> coretype_equal ty2 ty1 |
||
328 | | Tydec_int , Tydec_int |
||
329 | | Tydec_real , Tydec_real |
||
330 | 04a63d25 | xthirioux | (* | Tydec_float , Tydec_float *) |
331 | ed81df06 | xthirioux | | Tydec_bool , Tydec_bool -> true |
332 | | Tydec_clock ty1 , Tydec_clock ty2 -> coretype_equal ty1 ty2 |
||
333 | | Tydec_array (d1,ty1), Tydec_array (d2, ty2) -> Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2 |
||
334 | | Tydec_enum tl1 , Tydec_enum tl2 -> List.sort compare tl1 = List.sort compare tl2 |
||
335 | | Tydec_struct fl1 , Tydec_struct fl2 -> |
||
336 | b1655a21 | xthirioux | List.length fl1 = List.length fl2 |
337 | && List.for_all2 (fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2) |
||
338 | (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl1) |
||
339 | (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl2) |
||
340 | | _ -> false |
||
341 | ef34b4ae | xthirioux | in ((*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res;*) res) |
342 | b1655a21 | xthirioux | |
343 | 22fe1c93 | ploc | let tag_true = "true" |
344 | let tag_false = "false" |
||
345 | 77a61575 | xthirioux | let tag_default = "default" |
346 | 22fe1c93 | ploc | |
347 | let const_is_bool c = |
||
348 | match c with |
||
349 | | Const_tag t -> t = tag_true || t = tag_false |
||
350 | | _ -> false |
||
351 | |||
352 | (* Computes the negation of a boolean constant *) |
||
353 | let const_negation c = |
||
354 | assert (const_is_bool c); |
||
355 | match c with |
||
356 | | Const_tag t when t = tag_true -> Const_tag tag_false |
||
357 | | _ -> Const_tag tag_true |
||
358 | |||
359 | let const_or c1 c2 = |
||
360 | assert (const_is_bool c1 && const_is_bool c2); |
||
361 | match c1, c2 with |
||
362 | | Const_tag t1, _ when t1 = tag_true -> c1 |
||
363 | | _ , Const_tag t2 when t2 = tag_true -> c2 |
||
364 | | _ -> Const_tag tag_false |
||
365 | |||
366 | let const_and c1 c2 = |
||
367 | assert (const_is_bool c1 && const_is_bool c2); |
||
368 | match c1, c2 with |
||
369 | | Const_tag t1, _ when t1 = tag_false -> c1 |
||
370 | | _ , Const_tag t2 when t2 = tag_false -> c2 |
||
371 | | _ -> Const_tag tag_true |
||
372 | |||
373 | let const_xor c1 c2 = |
||
374 | assert (const_is_bool c1 && const_is_bool c2); |
||
375 | match c1, c2 with |
||
376 | | Const_tag t1, Const_tag t2 when t1 <> t2 -> Const_tag tag_true |
||
377 | | _ -> Const_tag tag_false |
||
378 | |||
379 | let const_impl c1 c2 = |
||
380 | assert (const_is_bool c1 && const_is_bool c2); |
||
381 | match c1, c2 with |
||
382 | | Const_tag t1, _ when t1 = tag_false -> Const_tag tag_true |
||
383 | | _ , Const_tag t2 when t2 = tag_true -> Const_tag tag_true |
||
384 | | _ -> Const_tag tag_false |
||
385 | |||
386 | (* To guarantee uniqueness of tags in enum types *) |
||
387 | let tag_table = |
||
388 | Utils.create_hashtable 20 [ |
||
389 | ef34b4ae | xthirioux | tag_true, top_bool_type; |
390 | tag_false, top_bool_type |
||
391 | 22fe1c93 | ploc | ] |
392 | |||
393 | fa090c4e | xthirioux | (* To guarantee uniqueness of fields in struct types *) |
394 | let field_table = |
||
395 | Utils.create_hashtable 20 [ |
||
396 | ] |
||
397 | |||
398 | 22fe1c93 | ploc | let get_enum_type_tags cty = |
399 | ef34b4ae | xthirioux | (*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*) |
400 | 22fe1c93 | ploc | match cty with |
401 | | Tydec_bool -> [tag_true; tag_false] |
||
402 | ef34b4ae | xthirioux | | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with |
403 | 22fe1c93 | ploc | | Tydec_enum tl -> tl |
404 | | _ -> assert false) |
||
405 | | _ -> assert false |
||
406 | 6a6abd76 | xthirioux | |
407 | fa090c4e | xthirioux | let get_struct_type_fields cty = |
408 | match cty with |
||
409 | ef34b4ae | xthirioux | | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with |
410 | fa090c4e | xthirioux | | Tydec_struct fl -> fl |
411 | | _ -> assert false) |
||
412 | | _ -> assert false |
||
413 | 6a6abd76 | xthirioux | |
414 | 22fe1c93 | ploc | let const_of_bool b = |
415 | Const_tag (if b then tag_true else tag_false) |
||
416 | |||
417 | (* let get_const c = snd (Hashtbl.find consts_table c) *) |
||
418 | |||
419 | add75bcb | xthirioux | let ident_of_expr expr = |
420 | match expr.expr_desc with |
||
421 | | Expr_ident id -> id |
||
422 | | _ -> assert false |
||
423 | |||
424 | fc886259 | xthirioux | (* Generate a new ident expression from a declared variable *) |
425 | let expr_of_vdecl v = |
||
426 | { expr_tag = Utils.new_tag (); |
||
427 | expr_desc = Expr_ident v.var_id; |
||
428 | expr_type = v.var_type; |
||
429 | expr_clock = v.var_clock; |
||
430 | expr_delay = Delay.new_var (); |
||
431 | expr_annot = None; |
||
432 | expr_loc = v.var_loc } |
||
433 | |||
434 | 22fe1c93 | ploc | (* Caution, returns an untyped and unclocked expression *) |
435 | let expr_of_ident id loc = |
||
436 | {expr_tag = Utils.new_tag (); |
||
437 | expr_desc = Expr_ident id; |
||
438 | expr_type = Types.new_var (); |
||
439 | expr_clock = Clocks.new_var true; |
||
440 | expr_delay = Delay.new_var (); |
||
441 | expr_loc = loc; |
||
442 | expr_annot = None} |
||
443 | |||
444 | b616fe7a | xthirioux | let is_tuple_expr expr = |
445 | match expr.expr_desc with |
||
446 | | Expr_tuple _ -> true |
||
447 | | _ -> false |
||
448 | |||
449 | 22fe1c93 | ploc | let expr_list_of_expr expr = |
450 | match expr.expr_desc with |
||
451 | bb2ca5f4 | xthirioux | | Expr_tuple elist -> elist |
452 | | _ -> [expr] |
||
453 | 22fe1c93 | ploc | |
454 | let expr_of_expr_list loc elist = |
||
455 | match elist with |
||
456 | | [t] -> { t with expr_loc = loc } |
||
457 | 70df2f87 | xthirioux | | t::_ -> |
458 | let tlist = List.map (fun e -> e.expr_type) elist in |
||
459 | let clist = List.map (fun e -> e.expr_clock) elist in |
||
460 | { t with expr_desc = Expr_tuple elist; |
||
461 | expr_type = Type_predef.type_tuple tlist; |
||
462 | expr_clock = Clock_predef.ck_tuple clist; |
||
463 | expr_tag = Utils.new_tag (); |
||
464 | expr_loc = loc } |
||
465 | 22fe1c93 | ploc | | _ -> assert false |
466 | |||
467 | let call_of_expr expr = |
||
468 | match expr.expr_desc with |
||
469 | | Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r) |
||
470 | | _ -> assert false |
||
471 | |||
472 | 7d640c88 | ploc | |
473 | 22fe1c93 | ploc | (* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *) |
474 | let rec expr_of_dimension dim = |
||
475 | 7d640c88 | ploc | let open Dimension in |
476 | match dim.dim_desc with |
||
477 | 22fe1c93 | ploc | | Dbool b -> |
478 | mkexpr dim.dim_loc (Expr_const (const_of_bool b)) |
||
479 | | Dint i -> |
||
480 | mkexpr dim.dim_loc (Expr_const (Const_int i)) |
||
481 | | Dident id -> |
||
482 | mkexpr dim.dim_loc (Expr_ident id) |
||
483 | | Dite (c, t, e) -> |
||
484 | mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e)) |
||
485 | | Dappl (id, args) -> |
||
486 | mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None)) |
||
487 | | Dlink dim' -> expr_of_dimension dim' |
||
488 | | Dvar |
||
489 | fc886259 | xthirioux | | Dunivar -> (Format.eprintf "internal error: Corelang.expr_of_dimension %a@." Dimension.pp_dimension dim; |
490 | 22fe1c93 | ploc | assert false) |
491 | |||
492 | let dimension_of_const loc const = |
||
493 | 7d640c88 | ploc | let open Dimension in |
494 | 22fe1c93 | ploc | match const with |
495 | | Const_int i -> mkdim_int loc i |
||
496 | | Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true) |
||
497 | | _ -> raise InvalidDimension |
||
498 | |||
499 | (* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments |
||
500 | into dimension expressions *) |
||
501 | let rec dimension_of_expr expr = |
||
502 | 7d640c88 | ploc | let open Dimension in |
503 | 22fe1c93 | ploc | match expr.expr_desc with |
504 | | Expr_const c -> dimension_of_const expr.expr_loc c |
||
505 | | Expr_ident id -> mkdim_ident expr.expr_loc id |
||
506 | 04a63d25 | xthirioux | | Expr_appl (f, args, None) when Basic_library.is_expr_internal_fun expr -> |
507 | 22fe1c93 | ploc | let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in |
508 | if k = None then raise InvalidDimension; |
||
509 | mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args)) |
||
510 | | Expr_ite (i, t, e) -> |
||
511 | mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e) |
||
512 | | _ -> raise InvalidDimension (* not a simple dimension expression *) |
||
513 | |||
514 | |||
515 | let sort_handlers hl = |
||
516 | List.sort (fun (t, _) (t', _) -> compare t t') hl |
||
517 | |||
518 | e49b6d55 | xavier.thirioux | let num_10 = Num.num_of_int 10 |
519 | |||
520 | let rec is_eq_const c1 c2 = |
||
521 | match c1, c2 with |
||
522 | | Const_real (n1, i1, _), Const_real (n2, i2, _) |
||
523 | -> Num.(let n1 = n1 // (num_10 **/ (num_of_int i1)) in |
||
524 | let n2 = n2 // (num_10 **/ (num_of_int i2)) in |
||
525 | eq_num n1 n2) |
||
526 | | Const_struct lcl1, Const_struct lcl2 |
||
527 | -> List.length lcl1 = List.length lcl2 |
||
528 | && List.for_all2 (fun (l1, c1) (l2, c2) -> l1 = l2 && is_eq_const c1 c2) lcl1 lcl2 |
||
529 | | _ -> c1 = c2 |
||
530 | |||
531 | 22fe1c93 | ploc | let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with |
532 | e49b6d55 | xavier.thirioux | | Expr_const c1, Expr_const c2 -> is_eq_const c1 c2 |
533 | 22fe1c93 | ploc | | Expr_ident i1, Expr_ident i2 -> i1 = i2 |
534 | | Expr_array el1, Expr_array el2 |
||
535 | | Expr_tuple el1, Expr_tuple el2 -> |
||
536 | List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2 |
||
537 | | Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' |
||
538 | | Expr_fby (e1,e2), Expr_fby (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' |
||
539 | | Expr_ite (i1, t1, e1), Expr_ite (i2, t2, e2) -> is_eq_expr i1 i2 && is_eq_expr t1 t2 && is_eq_expr e1 e2 |
||
540 | (* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' *) |
||
541 | (* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *) |
||
542 | | Expr_pre e, Expr_pre e' -> is_eq_expr e e' |
||
543 | | Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e' |
||
544 | | Expr_merge(i, hl), Expr_merge(i', hl') -> i=i' && List.for_all2 (fun (t, h) (t', h') -> t=t' && is_eq_expr h h') (sort_handlers hl) (sort_handlers hl') |
||
545 | | Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e' |
||
546 | | Expr_power (e1, i1), Expr_power (e2, i2) |
||
547 | | Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2) |
||
548 | | _ -> false |
||
549 | |||
550 | 01c7d5e1 | ploc | let get_node_vars nd = |
551 | 22fe1c93 | ploc | nd.node_inputs @ nd.node_locals @ nd.node_outputs |
552 | |||
553 | fc886259 | xthirioux | let mk_new_node_name nd id = |
554 | let used_vars = get_node_vars nd in |
||
555 | let used v = List.exists (fun vdecl -> vdecl.var_id = v) used_vars in |
||
556 | mk_new_name used id |
||
557 | |||
558 | 01c7d5e1 | ploc | let get_var id var_list = |
559 | 04a63d25 | xthirioux | List.find (fun v -> v.var_id = id) var_list |
560 | 22fe1c93 | ploc | |
561 | df39e35a | xthirioux | let get_node_var id node = |
562 | 76c7023b | ploc | try |
563 | get_var id (get_node_vars node) |
||
564 | with Not_found -> begin |
||
565 | 63f10e14 | ploc | (* Format.eprintf "Unable to find variable %s in node %s@.@?" id node.node_id; *) |
566 | 76c7023b | ploc | raise Not_found |
567 | end |
||
568 | 333e3a25 | ploc | |
569 | |||
570 | b08ffca7 | xthirioux | let get_node_eqs = |
571 | let get_eqs stmts = |
||
572 | List.fold_right |
||
573 | 333e3a25 | ploc | (fun stmt (res_eq, res_aut) -> |
574 | b08ffca7 | xthirioux | match stmt with |
575 | 333e3a25 | ploc | | Eq eq -> eq :: res_eq, res_aut |
576 | | Aut aut -> res_eq, aut::res_aut) |
||
577 | b08ffca7 | xthirioux | stmts |
578 | 333e3a25 | ploc | ([], []) in |
579 | b08ffca7 | xthirioux | let table_eqs = Hashtbl.create 23 in |
580 | (fun nd -> |
||
581 | try |
||
582 | let (old, res) = Hashtbl.find table_eqs nd.node_id |
||
583 | in if old == nd.node_stmts then res else raise Not_found |
||
584 | with Not_found -> |
||
585 | let res = get_eqs nd.node_stmts in |
||
586 | begin |
||
587 | Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res); |
||
588 | res |
||
589 | end) |
||
590 | |||
591 | 01c7d5e1 | ploc | let get_node_eq id node = |
592 | 333e3a25 | ploc | let eqs, auts = get_node_eqs node in |
593 | try |
||
594 | List.find (fun eq -> List.mem id eq.eq_lhs) eqs |
||
595 | with |
||
596 | Not_found -> (* Shall be defined in automata auts *) raise Not_found |
||
597 | |||
598 | 22fe1c93 | ploc | let get_nodes prog = |
599 | List.fold_left ( |
||
600 | fun nodes decl -> |
||
601 | match decl.top_decl_desc with |
||
602 | ef34b4ae | xthirioux | | Node _ -> decl::nodes |
603 | | Const _ | ImportedNode _ | Open _ | TypeDef _ -> nodes |
||
604 | 22fe1c93 | ploc | ) [] prog |
605 | |||
606 | ef34b4ae | xthirioux | let get_imported_nodes prog = |
607 | c1adf235 | ploc | List.fold_left ( |
608 | ef34b4ae | xthirioux | fun nodes decl -> |
609 | c1adf235 | ploc | match decl.top_decl_desc with |
610 | ef34b4ae | xthirioux | | ImportedNode _ -> decl::nodes |
611 | | Const _ | Node _ | Open _ | TypeDef _-> nodes |
||
612 | c1adf235 | ploc | ) [] prog |
613 | 22fe1c93 | ploc | |
614 | ef34b4ae | xthirioux | let get_consts prog = |
615 | List.fold_right ( |
||
616 | fun decl consts -> |
||
617 | b1655a21 | xthirioux | match decl.top_decl_desc with |
618 | ef34b4ae | xthirioux | | Const _ -> decl::consts |
619 | | Node _ | ImportedNode _ | Open _ | TypeDef _ -> consts |
||
620 | ) prog [] |
||
621 | |||
622 | let get_typedefs prog = |
||
623 | List.fold_right ( |
||
624 | fun decl types -> |
||
625 | match decl.top_decl_desc with |
||
626 | | TypeDef _ -> decl::types |
||
627 | | Node _ | ImportedNode _ | Open _ | Const _ -> types |
||
628 | ) prog [] |
||
629 | |||
630 | let get_dependencies prog = |
||
631 | List.fold_right ( |
||
632 | fun decl deps -> |
||
633 | match decl.top_decl_desc with |
||
634 | | Open _ -> decl::deps |
||
635 | | Node _ | ImportedNode _ | TypeDef _ | Const _ -> deps |
||
636 | ) prog [] |
||
637 | e2380d4d | ploc | |
638 | ed81df06 | xthirioux | let get_node_interface nd = |
639 | {nodei_id = nd.node_id; |
||
640 | nodei_type = nd.node_type; |
||
641 | nodei_clock = nd.node_clock; |
||
642 | nodei_inputs = nd.node_inputs; |
||
643 | nodei_outputs = nd.node_outputs; |
||
644 | nodei_stateless = nd.node_dec_stateless; |
||
645 | nodei_spec = nd.node_spec; |
||
646 | 66359a5e | ploc | (* nodei_annot = nd.node_annot; *) |
647 | ed81df06 | xthirioux | nodei_prototype = None; |
648 | 04a63d25 | xthirioux | nodei_in_lib = []; |
649 | ed81df06 | xthirioux | } |
650 | |||
651 | e2380d4d | ploc | (************************************************************************) |
652 | (* Renaming *) |
||
653 | |||
654 | ec433d69 | xthirioux | let rec rename_static rename cty = |
655 | match cty with |
||
656 | | Tydec_array (d, cty') -> Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty') |
||
657 | | Tydec_clock cty -> Tydec_clock (rename_static rename cty) |
||
658 | | Tydec_struct fl -> Tydec_struct (List.map (fun (f, cty) -> f, rename_static rename cty) fl) |
||
659 | | _ -> cty |
||
660 | |||
661 | let rec rename_carrier rename cck = |
||
662 | match cck with |
||
663 | | Ckdec_bool cl -> Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl) |
||
664 | | _ -> cck |
||
665 | |||
666 | 333e3a25 | ploc | (*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*) |
667 | ec433d69 | xthirioux | |
668 | (* applies the renaming function [fvar] to all variables of expression [expr] *) |
||
669 | 333e3a25 | ploc | (* let rec expr_replace_var fvar expr = *) |
670 | (* { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } *) |
||
671 | ec433d69 | xthirioux | |
672 | 333e3a25 | ploc | (* and expr_desc_replace_var fvar expr_desc = *) |
673 | (* match expr_desc with *) |
||
674 | (* | Expr_const _ -> expr_desc *) |
||
675 | (* | Expr_ident i -> Expr_ident (fvar i) *) |
||
676 | (* | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el) *) |
||
677 | (* | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d) *) |
||
678 | (* | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d) *) |
||
679 | (* | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el) *) |
||
680 | (* | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e) *) |
||
681 | (* | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2) *) |
||
682 | (* | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2) *) |
||
683 | (* | Expr_pre e' -> Expr_pre (expr_replace_var fvar e') *) |
||
684 | (* | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l) *) |
||
685 | (* | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl) *) |
||
686 | (* | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (expr_replace_var fvar) i') *) |
||
687 | |||
688 | |||
689 | |||
690 | let rec rename_expr f_node f_var expr = |
||
691 | { expr with expr_desc = rename_expr_desc f_node f_var expr.expr_desc } |
||
692 | and rename_expr_desc f_node f_var expr_desc = |
||
693 | let re = rename_expr f_node f_var in |
||
694 | ec433d69 | xthirioux | match expr_desc with |
695 | | Expr_const _ -> expr_desc |
||
696 | | Expr_ident i -> Expr_ident (f_var i) |
||
697 | | Expr_array el -> Expr_array (List.map re el) |
||
698 | | Expr_access (e1, d) -> Expr_access (re e1, d) |
||
699 | | Expr_power (e1, d) -> Expr_power (re e1, d) |
||
700 | | Expr_tuple el -> Expr_tuple (List.map re el) |
||
701 | | Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e) |
||
702 | | Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2) |
||
703 | | Expr_fby (e1, e2) -> Expr_fby (re e1, re e2) |
||
704 | | Expr_pre e' -> Expr_pre (re e') |
||
705 | | Expr_when (e', i, l)-> Expr_when (re e', f_var i, l) |
||
706 | | Expr_merge (i, hl) -> |
||
707 | Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl) |
||
708 | | Expr_appl (i, e', i') -> |
||
709 | Expr_appl (f_node i, re e', Utils.option_map re i') |
||
710 | 333e3a25 | ploc | |
711 | let rename_dec_type f_node f_var t = assert false (* |
||
712 | Types.rename_dim_type (Dimension.rename f_node f_var) t*) |
||
713 | |||
714 | let rename_dec_clock f_node f_var c = assert false (* |
||
715 | Clocks.rename_clock_expr f_var c*) |
||
716 | |||
717 | let rename_var f_node f_var v = { |
||
718 | v with |
||
719 | var_id = f_var v.var_id; |
||
720 | var_dec_type = rename_dec_type f_node f_var v.var_type; |
||
721 | var_dec_clock = rename_dec_clock f_node f_var v.var_clock |
||
722 | } |
||
723 | |||
724 | let rename_vars f_node f_var = List.map (rename_var f_node f_var) |
||
725 | |||
726 | let rec rename_eq f_node f_var eq = { eq with |
||
727 | eq_lhs = List.map f_var eq.eq_lhs; |
||
728 | eq_rhs = rename_expr f_node f_var eq.eq_rhs |
||
729 | } |
||
730 | and rename_handler f_node f_var h = {h with |
||
731 | hand_state = f_var h.hand_state; |
||
732 | hand_unless = List.map ( |
||
733 | fun (l,e,b,id) -> l, rename_expr f_node f_var e, b, f_var id |
||
734 | ) h.hand_unless; |
||
735 | hand_until = List.map ( |
||
736 | fun (l,e,b,id) -> l, rename_expr f_node f_var e, b, f_var id |
||
737 | ) h.hand_until; |
||
738 | hand_locals = rename_vars f_node f_var h.hand_locals; |
||
739 | hand_stmts = rename_stmts f_node f_var h.hand_stmts; |
||
740 | hand_annots = rename_annots f_node f_var h.hand_annots; |
||
741 | |||
742 | } |
||
743 | and rename_aut f_node f_var aut = { aut with |
||
744 | aut_id = f_var aut.aut_id; |
||
745 | aut_handlers = List.map (rename_handler f_node f_var) aut.aut_handlers; |
||
746 | } |
||
747 | and rename_stmts f_node f_var stmts = List.map (fun stmt -> match stmt with |
||
748 | | Eq eq -> Eq (rename_eq f_node f_var eq) |
||
749 | | Aut at -> Aut (rename_aut f_node f_var at)) |
||
750 | stmts |
||
751 | and rename_annotl f_node f_var annots = |
||
752 | List.map |
||
753 | (fun (key, value) -> key, rename_eexpr f_node f_var value) |
||
754 | annots |
||
755 | and rename_annot f_node f_var annot = |
||
756 | { annot with annots = rename_annotl f_node f_var annot.annots } |
||
757 | and rename_annots f_node f_var annots = |
||
758 | List.map (rename_annot f_node f_var) annots |
||
759 | and rename_eexpr f_node f_var ee = |
||
760 | { ee with |
||
761 | eexpr_tag = Utils.new_tag (); |
||
762 | eexpr_qfexpr = rename_expr f_node f_var ee.eexpr_qfexpr; |
||
763 | eexpr_quantifiers = List.map (fun (typ,vdecls) -> typ, rename_vars f_node f_var vdecls) ee.eexpr_quantifiers; |
||
764 | eexpr_normalized = Utils.option_map |
||
765 | (fun (vdecl, eqs, vdecls) -> |
||
766 | rename_var f_node f_var vdecl, |
||
767 | List.map (rename_eq f_node f_var) eqs, |
||
768 | rename_vars f_node f_var vdecls |
||
769 | ) ee.eexpr_normalized; |
||
770 | |||
771 | } |
||
772 | |||
773 | |||
774 | |||
775 | |||
776 | let rename_node f_node f_var nd = |
||
777 | let rename_var = rename_var f_node f_var in |
||
778 | let rename_expr = rename_expr f_node f_var in |
||
779 | let rename_stmts = rename_stmts f_node f_var in |
||
780 | let inputs = List.map rename_var nd.node_inputs in |
||
781 | let outputs = List.map rename_var nd.node_outputs in |
||
782 | let locals = List.map rename_var nd.node_locals in |
||
783 | let gen_calls = List.map rename_expr nd.node_gencalls in |
||
784 | let node_checks = List.map (Dimension.rename f_node f_var) nd.node_checks in |
||
785 | let node_asserts = List.map |
||
786 | (fun a -> |
||
787 | {a with assert_expr = |
||
788 | let expr = a.assert_expr in |
||
789 | rename_expr expr}) |
||
790 | nd.node_asserts |
||
791 | in |
||
792 | let node_stmts = rename_stmts nd.node_stmts |
||
793 | |||
794 | |||
795 | in |
||
796 | let spec = |
||
797 | Utils.option_map |
||
798 | (fun s -> assert false; (*rename_node_annot f_node f_var s*) ) (* TODO: implement! *) |
||
799 | nd.node_spec |
||
800 | in |
||
801 | let annot = rename_annots f_node f_var nd.node_annot in |
||
802 | { |
||
803 | node_id = f_node nd.node_id; |
||
804 | node_type = nd.node_type; |
||
805 | node_clock = nd.node_clock; |
||
806 | node_inputs = inputs; |
||
807 | node_outputs = outputs; |
||
808 | node_locals = locals; |
||
809 | node_gencalls = gen_calls; |
||
810 | node_checks = node_checks; |
||
811 | node_asserts = node_asserts; |
||
812 | node_stmts = node_stmts; |
||
813 | node_dec_stateless = nd.node_dec_stateless; |
||
814 | node_stateless = nd.node_stateless; |
||
815 | node_spec = spec; |
||
816 | node_annot = annot; |
||
817 | } |
||
818 | ec433d69 | xthirioux | |
819 | |||
820 | let rename_const f_const c = |
||
821 | { c with const_id = f_const c.const_id } |
||
822 | |||
823 | let rename_typedef f_var t = |
||
824 | match t.tydef_desc with |
||
825 | | Tydec_enum tags -> { t with tydef_desc = Tydec_enum (List.map f_var tags) } |
||
826 | | _ -> t |
||
827 | |||
828 | let rename_prog f_node f_var f_const prog = |
||
829 | List.rev ( |
||
830 | List.fold_left (fun accu top -> |
||
831 | (match top.top_decl_desc with |
||
832 | | Node nd -> |
||
833 | 333e3a25 | ploc | { top with top_decl_desc = Node (rename_node f_node f_var nd) } |
834 | ec433d69 | xthirioux | | Const c -> |
835 | { top with top_decl_desc = Const (rename_const f_const c) } |
||
836 | | TypeDef tdef -> |
||
837 | { top with top_decl_desc = TypeDef (rename_typedef f_var tdef) } |
||
838 | | ImportedNode _ |
||
839 | | Open _ -> top) |
||
840 | ::accu |
||
841 | ) [] prog |
||
842 | ) |
||
843 | |||
844 | 333e3a25 | ploc | (* Applies the renaming function [fvar] to every rhs |
845 | only when the corresponding lhs satisfies predicate [pvar] *) |
||
846 | let eq_replace_rhs_var pvar fvar eq = |
||
847 | let pvar l = List.exists pvar l in |
||
848 | let rec replace lhs rhs = |
||
849 | { rhs with expr_desc = |
||
850 | match lhs with |
||
851 | | [] -> assert false |
||
852 | | [_] -> if pvar lhs then rename_expr_desc (fun x -> x) fvar rhs.expr_desc else rhs.expr_desc |
||
853 | | _ -> |
||
854 | (match rhs.expr_desc with |
||
855 | | Expr_tuple tl -> |
||
856 | Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl) |
||
857 | | Expr_appl (f, arg, None) when Basic_library.is_expr_internal_fun rhs -> |
||
858 | let args = expr_list_of_expr arg in |
||
859 | Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None) |
||
860 | | Expr_array _ |
||
861 | | Expr_access _ |
||
862 | | Expr_power _ |
||
863 | | Expr_const _ |
||
864 | | Expr_ident _ |
||
865 | | Expr_appl _ -> |
||
866 | if pvar lhs |
||
867 | then rename_expr_desc (fun x -> x) fvar rhs.expr_desc |
||
868 | else rhs.expr_desc |
||
869 | | Expr_ite (c, t, e) -> Expr_ite (replace lhs c, replace lhs t, replace lhs e) |
||
870 | | Expr_arrow (e1, e2) -> Expr_arrow (replace lhs e1, replace lhs e2) |
||
871 | | Expr_fby (e1, e2) -> Expr_fby (replace lhs e1, replace lhs e2) |
||
872 | | Expr_pre e' -> Expr_pre (replace lhs e') |
||
873 | | Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i |
||
874 | in Expr_when (replace lhs e', i', l) |
||
875 | | Expr_merge (i, hl) -> let i' = if pvar lhs then fvar i else i |
||
876 | in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl) |
||
877 | ) |
||
878 | } |
||
879 | in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs } |
||
880 | |||
881 | |||
882 | ec433d69 | xthirioux | (**********************************************************************) |
883 | (* Pretty printers *) |
||
884 | |||
885 | let pp_decl_type fmt tdecl = |
||
886 | match tdecl.top_decl_desc with |
||
887 | | Node nd -> |
||
888 | fprintf fmt "%s: " nd.node_id; |
||
889 | Utils.reset_names (); |
||
890 | fprintf fmt "%a@ " Types.print_ty nd.node_type |
||
891 | | ImportedNode ind -> |
||
892 | fprintf fmt "%s: " ind.nodei_id; |
||
893 | Utils.reset_names (); |
||
894 | fprintf fmt "%a@ " Types.print_ty ind.nodei_type |
||
895 | | Const _ | Open _ | TypeDef _ -> () |
||
896 | |||
897 | let pp_prog_type fmt tdecl_list = |
||
898 | Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list |
||
899 | |||
900 | let pp_decl_clock fmt cdecl = |
||
901 | match cdecl.top_decl_desc with |
||
902 | | Node nd -> |
||
903 | fprintf fmt "%s: " nd.node_id; |
||
904 | Utils.reset_names (); |
||
905 | fprintf fmt "%a@ " Clocks.print_ck nd.node_clock |
||
906 | | ImportedNode ind -> |
||
907 | fprintf fmt "%s: " ind.nodei_id; |
||
908 | Utils.reset_names (); |
||
909 | fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock |
||
910 | | Const _ | Open _ | TypeDef _ -> () |
||
911 | |||
912 | let pp_prog_clock fmt prog = |
||
913 | Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog |
||
914 | |||
915 | |||
916 | (* filling node table with internal functions *) |
||
917 | let vdecls_of_typ_ck cpt ty = |
||
918 | let loc = Location.dummy_loc in |
||
919 | List.map |
||
920 | (fun _ -> incr cpt; |
||
921 | let name = sprintf "_var_%d" !cpt in |
||
922 | 66359a5e | ploc | mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false, None, None)) |
923 | ec433d69 | xthirioux | (Types.type_list_of_type ty) |
924 | |||
925 | let mk_internal_node id = |
||
926 | let spec = None in |
||
927 | let ty = Env.lookup_value Basic_library.type_env id in |
||
928 | let ck = Env.lookup_value Basic_library.clock_env id in |
||
929 | let (tin, tout) = Types.split_arrow ty in |
||
930 | (*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*) |
||
931 | let cpt = ref (-1) in |
||
932 | mktop |
||
933 | (ImportedNode |
||
934 | {nodei_id = id; |
||
935 | nodei_type = ty; |
||
936 | nodei_clock = ck; |
||
937 | nodei_inputs = vdecls_of_typ_ck cpt tin; |
||
938 | nodei_outputs = vdecls_of_typ_ck cpt tout; |
||
939 | nodei_stateless = Types.get_static_value ty <> None; |
||
940 | nodei_spec = spec; |
||
941 | 66359a5e | ploc | (* nodei_annot = []; *) |
942 | ec433d69 | xthirioux | nodei_prototype = None; |
943 | 04a63d25 | xthirioux | nodei_in_lib = []; |
944 | ec433d69 | xthirioux | }) |
945 | |||
946 | let add_internal_funs () = |
||
947 | List.iter |
||
948 | (fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd) |
||
949 | Basic_library.internal_funs |
||
950 | |||
951 | |||
952 | |||
953 | (* Replace any occurence of a var in vars_to_replace by its associated |
||
954 | expression in defs until e does not contain any such variables *) |
||
955 | let rec substitute_expr vars_to_replace defs e = |
||
956 | let se = substitute_expr vars_to_replace defs in |
||
957 | { e with expr_desc = |
||
958 | let ed = e.expr_desc in |
||
959 | match ed with |
||
960 | | Expr_const _ -> ed |
||
961 | | Expr_array el -> Expr_array (List.map se el) |
||
962 | | Expr_access (e1, d) -> Expr_access (se e1, d) |
||
963 | | Expr_power (e1, d) -> Expr_power (se e1, d) |
||
964 | | Expr_tuple el -> Expr_tuple (List.map se el) |
||
965 | | Expr_ite (c, t, e) -> Expr_ite (se c, se t, se e) |
||
966 | | Expr_arrow (e1, e2)-> Expr_arrow (se e1, se e2) |
||
967 | | Expr_fby (e1, e2) -> Expr_fby (se e1, se e2) |
||
968 | | Expr_pre e' -> Expr_pre (se e') |
||
969 | | Expr_when (e', i, l)-> Expr_when (se e', i, l) |
||
970 | | Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, se h)) hl) |
||
971 | | Expr_appl (i, e', i') -> Expr_appl (i, se e', i') |
||
972 | | Expr_ident i -> |
||
973 | if List.exists (fun v -> v.var_id = i) vars_to_replace then ( |
||
974 | let eq_i eq = eq.eq_lhs = [i] in |
||
975 | if List.exists eq_i defs then |
||
976 | let sub = List.find eq_i defs in |
||
977 | let sub' = se sub.eq_rhs in |
||
978 | sub'.expr_desc |
||
979 | else |
||
980 | assert false |
||
981 | ) |
||
982 | else |
||
983 | ed |
||
984 | |||
985 | } |
||
986 | |||
987 | let rec expr_to_eexpr expr = |
||
988 | { eexpr_tag = expr.expr_tag; |
||
989 | 3e1d20e0 | ploc | eexpr_qfexpr = expr; |
990 | eexpr_quantifiers = []; |
||
991 | ec433d69 | xthirioux | eexpr_type = expr.expr_type; |
992 | eexpr_clock = expr.expr_clock; |
||
993 | 3e1d20e0 | ploc | eexpr_loc = expr.expr_loc; |
994 | eexpr_normalized = None |
||
995 | ec433d69 | xthirioux | } |
996 | 3e1d20e0 | ploc | (* and expr_desc_to_eexpr_desc expr_desc = *) |
997 | (* let conv = expr_to_eexpr in *) |
||
998 | (* match expr_desc with *) |
||
999 | (* | Expr_const c -> EExpr_const (match c with *) |
||
1000 | (* | Const_int x -> EConst_int x *) |
||
1001 | (* | Const_real x -> EConst_real x *) |
||
1002 | (* | Const_float x -> EConst_float x *) |
||
1003 | (* | Const_tag x -> EConst_tag x *) |
||
1004 | (* | _ -> assert false *) |
||
1005 | |||
1006 | (* ) *) |
||
1007 | (* | Expr_ident i -> EExpr_ident i *) |
||
1008 | (* | Expr_tuple el -> EExpr_tuple (List.map conv el) *) |
||
1009 | |||
1010 | (* | Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2) *) |
||
1011 | (* | Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2) *) |
||
1012 | (* | Expr_pre e' -> EExpr_pre (conv e') *) |
||
1013 | (* | Expr_appl (i, e', i') -> *) |
||
1014 | (* EExpr_appl *) |
||
1015 | (* (i, conv e', match i' with None -> None | Some(id, _) -> Some id) *) |
||
1016 | |||
1017 | (* | Expr_when _ *) |
||
1018 | (* | Expr_merge _ -> assert false *) |
||
1019 | (* | Expr_array _ *) |
||
1020 | (* | Expr_access _ *) |
||
1021 | (* | Expr_power _ -> assert false *) |
||
1022 | (* | Expr_ite (c, t, e) -> assert false *) |
||
1023 | (* | _ -> assert false *) |
||
1024 | |||
1025 | |||
1026 | ec433d69 | xthirioux | let rec get_expr_calls nodes e = |
1027 | let get_calls = get_expr_calls nodes in |
||
1028 | 04a63d25 | xthirioux | match e.expr_desc with |
1029 | ec433d69 | xthirioux | | Expr_const _ |
1030 | | Expr_ident _ -> Utils.ISet.empty |
||
1031 | | Expr_tuple el |
||
1032 | | Expr_array el -> List.fold_left (fun accu e -> Utils.ISet.union accu (get_calls e)) Utils.ISet.empty el |
||
1033 | | Expr_pre e1 |
||
1034 | | Expr_when (e1, _, _) |
||
1035 | | Expr_access (e1, _) |
||
1036 | | Expr_power (e1, _) -> get_calls e1 |
||
1037 | | Expr_ite (c, t, e) -> Utils.ISet.union (Utils.ISet.union (get_calls c) (get_calls t)) (get_calls e) |
||
1038 | | Expr_arrow (e1, e2) |
||
1039 | | Expr_fby (e1, e2) -> Utils.ISet.union (get_calls e1) (get_calls e2) |
||
1040 | | Expr_merge (_, hl) -> List.fold_left (fun accu (_, h) -> Utils.ISet.union accu (get_calls h)) Utils.ISet.empty hl |
||
1041 | | Expr_appl (i, e', i') -> |
||
1042 | 04a63d25 | xthirioux | if Basic_library.is_expr_internal_fun e then |
1043 | ec433d69 | xthirioux | (get_calls e') |
1044 | else |
||
1045 | let calls = Utils.ISet.add i (get_calls e') in |
||
1046 | let test = (fun n -> match n.top_decl_desc with Node nd -> nd.node_id = i | _ -> false) in |
||
1047 | if List.exists test nodes then |
||
1048 | match (List.find test nodes).top_decl_desc with |
||
1049 | | Node nd -> Utils.ISet.union (get_node_calls nodes nd) calls |
||
1050 | | _ -> assert false |
||
1051 | else |
||
1052 | calls |
||
1053 | |||
1054 | and get_eq_calls nodes eq = |
||
1055 | get_expr_calls nodes eq.eq_rhs |
||
1056 | 333e3a25 | ploc | and get_aut_handler_calls nodes h = |
1057 | List.fold_left (fun accu stmt -> match stmt with |
||
1058 | | Eq eq -> Utils.ISet.union (get_eq_calls nodes eq) accu |
||
1059 | | Aut aut' -> Utils.ISet.union (get_aut_calls nodes aut') accu |
||
1060 | ) Utils.ISet.empty h.hand_stmts |
||
1061 | and get_aut_calls nodes aut = |
||
1062 | List.fold_left (fun accu h -> Utils.ISet.union (get_aut_handler_calls nodes h) accu) |
||
1063 | Utils.ISet.empty aut.aut_handlers |
||
1064 | ec433d69 | xthirioux | and get_node_calls nodes node = |
1065 | 333e3a25 | ploc | let eqs, auts = get_node_eqs node in |
1066 | let aut_calls = |
||
1067 | List.fold_left |
||
1068 | (fun accu aut -> Utils.ISet.union (get_aut_calls nodes aut) accu) |
||
1069 | Utils.ISet.empty auts |
||
1070 | in |
||
1071 | List.fold_left |
||
1072 | (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) |
||
1073 | aut_calls eqs |
||
1074 | ec433d69 | xthirioux | |
1075 | a6df3992 | Ploc | let get_expr_vars e = |
1076 | let rec get_expr_vars vars e = |
||
1077 | get_expr_desc_vars vars e.expr_desc |
||
1078 | and get_expr_desc_vars vars expr_desc = |
||
1079 | a85ca7df | ploc | (*Format.eprintf "get_expr_desc_vars expr=%a@." Printers.pp_expr (mkexpr Location.dummy_loc expr_desc);*) |
1080 | ec433d69 | xthirioux | match expr_desc with |
1081 | | Expr_const _ -> vars |
||
1082 | a85ca7df | ploc | | Expr_ident x -> Utils.ISet.add x vars |
1083 | ec433d69 | xthirioux | | Expr_tuple el |
1084 | | Expr_array el -> List.fold_left get_expr_vars vars el |
||
1085 | | Expr_pre e1 -> get_expr_vars vars e1 |
||
1086 | | Expr_when (e1, c, _) -> get_expr_vars (Utils.ISet.add c vars) e1 |
||
1087 | | Expr_access (e1, d) |
||
1088 | | Expr_power (e1, d) -> List.fold_left get_expr_vars vars [e1; expr_of_dimension d] |
||
1089 | | Expr_ite (c, t, e) -> List.fold_left get_expr_vars vars [c; t; e] |
||
1090 | | Expr_arrow (e1, e2) |
||
1091 | | Expr_fby (e1, e2) -> List.fold_left get_expr_vars vars [e1; e2] |
||
1092 | | Expr_merge (c, hl) -> List.fold_left (fun vars (_, h) -> get_expr_vars vars h) (Utils.ISet.add c vars) hl |
||
1093 | | Expr_appl (_, arg, None) -> get_expr_vars vars arg |
||
1094 | | Expr_appl (_, arg, Some r) -> List.fold_left get_expr_vars vars [arg; r] |
||
1095 | a6df3992 | Ploc | in |
1096 | get_expr_vars Utils.ISet.empty e |
||
1097 | ec433d69 | xthirioux | |
1098 | let rec expr_has_arrows e = |
||
1099 | expr_desc_has_arrows e.expr_desc |
||
1100 | and expr_desc_has_arrows expr_desc = |
||
1101 | match expr_desc with |
||
1102 | | Expr_const _ |
||
1103 | | Expr_ident _ -> false |
||
1104 | | Expr_tuple el |
||
1105 | | Expr_array el -> List.exists expr_has_arrows el |
||
1106 | | Expr_pre e1 |
||
1107 | | Expr_when (e1, _, _) |
||
1108 | | Expr_access (e1, _) |
||
1109 | | Expr_power (e1, _) -> expr_has_arrows e1 |
||
1110 | | Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e] |
||
1111 | | Expr_arrow (e1, e2) |
||
1112 | | Expr_fby (e1, e2) -> true |
||
1113 | | Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl |
||
1114 | | Expr_appl (i, e', i') -> expr_has_arrows e' |
||
1115 | |||
1116 | and eq_has_arrows eq = |
||
1117 | expr_has_arrows eq.eq_rhs |
||
1118 | 333e3a25 | ploc | and aut_has_arrows aut = List.exists (fun h -> List.exists (fun stmt -> match stmt with Eq eq -> eq_has_arrows eq | Aut aut' -> aut_has_arrows aut') h.hand_stmts ) aut.aut_handlers |
1119 | ec433d69 | xthirioux | and node_has_arrows node = |
1120 | 333e3a25 | ploc | let eqs, auts = get_node_eqs node in |
1121 | List.exists (fun eq -> eq_has_arrows eq) eqs || List.exists (fun aut -> aut_has_arrows aut) auts |
||
1122 | |||
1123 | ec433d69 | xthirioux | |
1124 | 01c7d5e1 | ploc | |
1125 | ec433d69 | xthirioux | let copy_var_decl vdecl = |
1126 | 66359a5e | ploc | mkvar_decl vdecl.var_loc ~orig:vdecl.var_orig (vdecl.var_id, vdecl.var_dec_type, vdecl.var_dec_clock, vdecl.var_dec_const, vdecl.var_dec_value, vdecl.var_parent_nodeid) |
1127 | ec433d69 | xthirioux | |
1128 | let copy_const cdecl = |
||
1129 | { cdecl with const_type = Types.new_var () } |
||
1130 | |||
1131 | let copy_node nd = |
||
1132 | { nd with |
||
1133 | node_type = Types.new_var (); |
||
1134 | node_clock = Clocks.new_var true; |
||
1135 | node_inputs = List.map copy_var_decl nd.node_inputs; |
||
1136 | node_outputs = List.map copy_var_decl nd.node_outputs; |
||
1137 | node_locals = List.map copy_var_decl nd.node_locals; |
||
1138 | node_gencalls = []; |
||
1139 | node_checks = []; |
||
1140 | node_stateless = None; |
||
1141 | } |
||
1142 | |||
1143 | let copy_top top = |
||
1144 | match top.top_decl_desc with |
||
1145 | | Node nd -> { top with top_decl_desc = Node (copy_node nd) } |
||
1146 | | Const c -> { top with top_decl_desc = Const (copy_const c) } |
||
1147 | | _ -> top |
||
1148 | |||
1149 | let copy_prog top_list = |
||
1150 | List.map copy_top top_list |
||
1151 | |||
1152 | e7cc5186 | ploc | |
1153 | let rec expr_contains_expr expr_tag expr = |
||
1154 | let search = expr_contains_expr expr_tag in |
||
1155 | expr.expr_tag = expr_tag || |
||
1156 | ( |
||
1157 | match expr.expr_desc with |
||
1158 | | Expr_const _ -> false |
||
1159 | | Expr_array el -> List.exists search el |
||
1160 | | Expr_access (e1, _) |
||
1161 | | Expr_power (e1, _) -> search e1 |
||
1162 | | Expr_tuple el -> List.exists search el |
||
1163 | | Expr_ite (c, t, e) -> List.exists search [c;t;e] |
||
1164 | | Expr_arrow (e1, e2) |
||
1165 | | Expr_fby (e1, e2) -> List.exists search [e1; e2] |
||
1166 | | Expr_pre e' |
||
1167 | | Expr_when (e', _, _) -> search e' |
||
1168 | | Expr_merge (_, hl) -> List.exists (fun (_, h) -> search h) hl |
||
1169 | | Expr_appl (_, e', None) -> search e' |
||
1170 | | Expr_appl (_, e', Some e'') -> List.exists search [e'; e''] |
||
1171 | | Expr_ident _ -> false |
||
1172 | ) |
||
1173 | |||
1174 | 2863281f | ploc | |
1175 | |||
1176 | |||
1177 | 22fe1c93 | ploc | (* Local Variables: *) |
1178 | (* compile-command:"make -C .." *) |
||
1179 | (* End: *) |