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
|
open Format
|
23
|
open LustreSpec
|
24
|
open Dimension
|
25
|
|
26
|
|
27
|
exception Error of Location.t * error
|
28
|
|
29
|
module VDeclModule =
|
30
|
struct (* Node module *)
|
31
|
type t = var_decl
|
32
|
let compare v1 v2 = compare v1.var_id v2.var_id
|
33
|
end
|
34
|
|
35
|
module VMap = Map.Make(VDeclModule)
|
36
|
|
37
|
module VSet = Set.Make(VDeclModule)
|
38
|
|
39
|
let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc}
|
40
|
|
41
|
|
42
|
|
43
|
let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc}
|
44
|
|
45
|
|
46
|
|
47
|
(************************************************************)
|
48
|
(* *)
|
49
|
|
50
|
let mktyp loc d =
|
51
|
{ ty_dec_desc = d; ty_dec_loc = loc }
|
52
|
|
53
|
let mkclock loc d =
|
54
|
{ ck_dec_desc = d; ck_dec_loc = loc }
|
55
|
|
56
|
let mkvar_decl loc (id, ty_dec, ck_dec, is_const) =
|
57
|
{ var_id = id;
|
58
|
var_dec_type = ty_dec;
|
59
|
var_dec_clock = ck_dec;
|
60
|
var_dec_const = is_const;
|
61
|
var_type = Types.new_var ();
|
62
|
var_clock = Clocks.new_var true;
|
63
|
var_loc = loc }
|
64
|
|
65
|
let mkexpr loc d =
|
66
|
{ expr_tag = Utils.new_tag ();
|
67
|
expr_desc = d;
|
68
|
expr_type = Types.new_var ();
|
69
|
expr_clock = Clocks.new_var true;
|
70
|
expr_delay = Delay.new_var ();
|
71
|
expr_annot = None;
|
72
|
expr_loc = loc }
|
73
|
|
74
|
let var_decl_of_const c =
|
75
|
{ var_id = c.const_id;
|
76
|
var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any };
|
77
|
var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any };
|
78
|
var_dec_const = true;
|
79
|
var_type = c.const_type;
|
80
|
var_clock = Clocks.new_var false;
|
81
|
var_loc = c.const_loc }
|
82
|
|
83
|
let mk_new_name vdecl_list id =
|
84
|
let rec new_name name cpt =
|
85
|
if List.exists (fun v -> v.var_id = name) vdecl_list
|
86
|
then new_name (sprintf "_%s_%i" id cpt) (cpt+1)
|
87
|
else name
|
88
|
in new_name id 1
|
89
|
|
90
|
let mkeq loc (lhs, rhs) =
|
91
|
{ eq_lhs = lhs;
|
92
|
eq_rhs = rhs;
|
93
|
eq_loc = loc }
|
94
|
|
95
|
let mkassert loc expr =
|
96
|
{ assert_loc = loc;
|
97
|
assert_expr = expr
|
98
|
}
|
99
|
|
100
|
let mktop_decl loc d =
|
101
|
{ top_decl_desc = d; top_decl_loc = loc }
|
102
|
|
103
|
let mkpredef_call loc funname args =
|
104
|
mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
|
105
|
|
106
|
(************************************************************)
|
107
|
(* Eexpr functions *)
|
108
|
(************************************************************)
|
109
|
|
110
|
let merge_node_annot ann1 ann2 =
|
111
|
{ requires = ann1.requires @ ann2.requires;
|
112
|
ensures = ann1.ensures @ ann2.ensures;
|
113
|
behaviors = ann1.behaviors @ ann2.behaviors;
|
114
|
spec_loc = ann1.spec_loc
|
115
|
}
|
116
|
|
117
|
let mkeexpr loc expr =
|
118
|
{ eexpr_tag = Utils.new_tag ();
|
119
|
eexpr_qfexpr = expr;
|
120
|
eexpr_quantifiers = [];
|
121
|
eexpr_type = Types.new_var ();
|
122
|
eexpr_clock = Clocks.new_var true;
|
123
|
eexpr_normalized = None;
|
124
|
eexpr_loc = loc }
|
125
|
|
126
|
let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers }
|
127
|
|
128
|
(*
|
129
|
let mkepredef_call loc funname args =
|
130
|
mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None))
|
131
|
|
132
|
let mkepredef_unary_call loc funname arg =
|
133
|
mkeexpr loc (EExpr_appl (funname, arg, None))
|
134
|
*)
|
135
|
|
136
|
let merge_expr_annot ann1 ann2 =
|
137
|
match ann1, ann2 with
|
138
|
| None, None -> assert false
|
139
|
| Some _, None -> ann1
|
140
|
| None, Some _ -> ann2
|
141
|
| Some ann1, Some ann2 -> Some {
|
142
|
annots = ann1.annots @ ann2.annots;
|
143
|
annot_loc = ann1.annot_loc
|
144
|
}
|
145
|
|
146
|
let update_expr_annot e annot =
|
147
|
{ e with expr_annot = merge_expr_annot e.expr_annot (Some annot) }
|
148
|
|
149
|
|
150
|
(***********************************************************)
|
151
|
(* Fast access to nodes, by name *)
|
152
|
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
|
153
|
let consts_table = Hashtbl.create 30
|
154
|
|
155
|
let node_name td =
|
156
|
match td.top_decl_desc with
|
157
|
| Node nd -> nd.node_id
|
158
|
| ImportedNode nd -> nd.nodei_id
|
159
|
| _ -> assert false
|
160
|
|
161
|
let is_generic_node td =
|
162
|
match td.top_decl_desc with
|
163
|
| Node nd -> List.exists (fun v -> v.var_dec_const) nd.node_inputs
|
164
|
| ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs
|
165
|
| _ -> assert false
|
166
|
|
167
|
let node_inputs td =
|
168
|
match td.top_decl_desc with
|
169
|
| Node nd -> nd.node_inputs
|
170
|
| ImportedNode nd -> nd.nodei_inputs
|
171
|
| _ -> assert false
|
172
|
|
173
|
let node_from_name id =
|
174
|
try
|
175
|
Hashtbl.find node_table id
|
176
|
with Not_found -> (Format.eprintf "Unable to find any node named %s@ @?" id;
|
177
|
assert false)
|
178
|
|
179
|
let is_imported_node td =
|
180
|
match td.top_decl_desc with
|
181
|
| Node nd -> false
|
182
|
| ImportedNode nd -> true
|
183
|
| _ -> assert false
|
184
|
|
185
|
|
186
|
(* alias and type definition table *)
|
187
|
let type_table =
|
188
|
Utils.create_hashtable 20 [
|
189
|
Tydec_int , Tydec_int;
|
190
|
Tydec_bool , Tydec_bool;
|
191
|
Tydec_float, Tydec_float;
|
192
|
Tydec_real , Tydec_real
|
193
|
]
|
194
|
|
195
|
let rec is_user_type typ =
|
196
|
match typ with
|
197
|
| Tydec_int | Tydec_bool | Tydec_real
|
198
|
| Tydec_float | Tydec_any | Tydec_const _ -> false
|
199
|
| Tydec_clock typ' -> is_user_type typ'
|
200
|
| _ -> true
|
201
|
|
202
|
let get_repr_type typ =
|
203
|
let typ_def = Hashtbl.find type_table typ in
|
204
|
if is_user_type typ_def then typ else typ_def
|
205
|
|
206
|
let tag_true = "true"
|
207
|
let tag_false = "false"
|
208
|
|
209
|
let const_is_bool c =
|
210
|
match c with
|
211
|
| Const_tag t -> t = tag_true || t = tag_false
|
212
|
| _ -> false
|
213
|
|
214
|
(* Computes the negation of a boolean constant *)
|
215
|
let const_negation c =
|
216
|
assert (const_is_bool c);
|
217
|
match c with
|
218
|
| Const_tag t when t = tag_true -> Const_tag tag_false
|
219
|
| _ -> Const_tag tag_true
|
220
|
|
221
|
let const_or c1 c2 =
|
222
|
assert (const_is_bool c1 && const_is_bool c2);
|
223
|
match c1, c2 with
|
224
|
| Const_tag t1, _ when t1 = tag_true -> c1
|
225
|
| _ , Const_tag t2 when t2 = tag_true -> c2
|
226
|
| _ -> Const_tag tag_false
|
227
|
|
228
|
let const_and c1 c2 =
|
229
|
assert (const_is_bool c1 && const_is_bool c2);
|
230
|
match c1, c2 with
|
231
|
| Const_tag t1, _ when t1 = tag_false -> c1
|
232
|
| _ , Const_tag t2 when t2 = tag_false -> c2
|
233
|
| _ -> Const_tag tag_true
|
234
|
|
235
|
let const_xor c1 c2 =
|
236
|
assert (const_is_bool c1 && const_is_bool c2);
|
237
|
match c1, c2 with
|
238
|
| Const_tag t1, Const_tag t2 when t1 <> t2 -> Const_tag tag_true
|
239
|
| _ -> Const_tag tag_false
|
240
|
|
241
|
let const_impl c1 c2 =
|
242
|
assert (const_is_bool c1 && const_is_bool c2);
|
243
|
match c1, c2 with
|
244
|
| Const_tag t1, _ when t1 = tag_false -> Const_tag tag_true
|
245
|
| _ , Const_tag t2 when t2 = tag_true -> Const_tag tag_true
|
246
|
| _ -> Const_tag tag_false
|
247
|
|
248
|
(* To guarantee uniqueness of tags in enum types *)
|
249
|
let tag_table =
|
250
|
Utils.create_hashtable 20 [
|
251
|
tag_true, Tydec_bool;
|
252
|
tag_false, Tydec_bool
|
253
|
]
|
254
|
|
255
|
(* To guarantee uniqueness of fields in struct types *)
|
256
|
let field_table =
|
257
|
Utils.create_hashtable 20 [
|
258
|
]
|
259
|
|
260
|
let get_enum_type_tags cty =
|
261
|
match cty with
|
262
|
| Tydec_bool -> [tag_true; tag_false]
|
263
|
| Tydec_const _ -> (match Hashtbl.find type_table cty with
|
264
|
| Tydec_enum tl -> tl
|
265
|
| _ -> assert false)
|
266
|
| _ -> assert false
|
267
|
|
268
|
let get_struct_type_fields cty =
|
269
|
match cty with
|
270
|
| Tydec_const _ -> (match Hashtbl.find type_table cty with
|
271
|
| Tydec_struct fl -> fl
|
272
|
| _ -> assert false)
|
273
|
| _ -> assert false
|
274
|
|
275
|
let const_of_bool b =
|
276
|
Const_tag (if b then tag_true else tag_false)
|
277
|
|
278
|
(* let get_const c = snd (Hashtbl.find consts_table c) *)
|
279
|
|
280
|
let ident_of_expr expr =
|
281
|
match expr.expr_desc with
|
282
|
| Expr_ident id -> id
|
283
|
| _ -> assert false
|
284
|
|
285
|
(* Caution, returns an untyped and unclocked expression *)
|
286
|
let expr_of_ident id loc =
|
287
|
{expr_tag = Utils.new_tag ();
|
288
|
expr_desc = Expr_ident id;
|
289
|
expr_type = Types.new_var ();
|
290
|
expr_clock = Clocks.new_var true;
|
291
|
expr_delay = Delay.new_var ();
|
292
|
expr_loc = loc;
|
293
|
expr_annot = None}
|
294
|
|
295
|
let is_tuple_expr expr =
|
296
|
match expr.expr_desc with
|
297
|
| Expr_tuple _ -> true
|
298
|
| _ -> false
|
299
|
|
300
|
let expr_list_of_expr expr =
|
301
|
match expr.expr_desc with
|
302
|
| Expr_tuple elist -> elist
|
303
|
| _ -> [expr]
|
304
|
|
305
|
let expr_of_expr_list loc elist =
|
306
|
match elist with
|
307
|
| [t] -> { t with expr_loc = loc }
|
308
|
| t::_ -> { t with expr_desc = Expr_tuple elist; expr_loc = loc }
|
309
|
| _ -> assert false
|
310
|
|
311
|
let call_of_expr expr =
|
312
|
match expr.expr_desc with
|
313
|
| Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r)
|
314
|
| _ -> assert false
|
315
|
|
316
|
(* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *)
|
317
|
let rec expr_of_dimension dim =
|
318
|
match dim.dim_desc with
|
319
|
| Dbool b ->
|
320
|
mkexpr dim.dim_loc (Expr_const (const_of_bool b))
|
321
|
| Dint i ->
|
322
|
mkexpr dim.dim_loc (Expr_const (Const_int i))
|
323
|
| Dident id ->
|
324
|
mkexpr dim.dim_loc (Expr_ident id)
|
325
|
| Dite (c, t, e) ->
|
326
|
mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e))
|
327
|
| Dappl (id, args) ->
|
328
|
mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None))
|
329
|
| Dlink dim' -> expr_of_dimension dim'
|
330
|
| Dvar
|
331
|
| Dunivar -> (Format.eprintf "internal error: expr_of_dimension %a@." Dimension.pp_dimension dim;
|
332
|
assert false)
|
333
|
|
334
|
let dimension_of_const loc const =
|
335
|
match const with
|
336
|
| Const_int i -> mkdim_int loc i
|
337
|
| Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true)
|
338
|
| _ -> raise InvalidDimension
|
339
|
|
340
|
(* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments
|
341
|
into dimension expressions *)
|
342
|
let rec dimension_of_expr expr =
|
343
|
match expr.expr_desc with
|
344
|
| Expr_const c -> dimension_of_const expr.expr_loc c
|
345
|
| Expr_ident id -> mkdim_ident expr.expr_loc id
|
346
|
| Expr_appl (f, args, None) when Basic_library.is_internal_fun f ->
|
347
|
let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in
|
348
|
if k = None then raise InvalidDimension;
|
349
|
mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args))
|
350
|
| Expr_ite (i, t, e) ->
|
351
|
mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e)
|
352
|
| _ -> raise InvalidDimension (* not a simple dimension expression *)
|
353
|
|
354
|
|
355
|
let sort_handlers hl =
|
356
|
List.sort (fun (t, _) (t', _) -> compare t t') hl
|
357
|
|
358
|
let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with
|
359
|
| Expr_const c1, Expr_const c2 -> c1 = c2
|
360
|
| Expr_ident i1, Expr_ident i2 -> i1 = i2
|
361
|
| Expr_array el1, Expr_array el2
|
362
|
| Expr_tuple el1, Expr_tuple el2 ->
|
363
|
List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2
|
364
|
| Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
|
365
|
| Expr_fby (e1,e2), Expr_fby (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
|
366
|
| 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
|
367
|
(* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' *)
|
368
|
(* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *)
|
369
|
| Expr_pre e, Expr_pre e' -> is_eq_expr e e'
|
370
|
| Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e'
|
371
|
| 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')
|
372
|
| Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e'
|
373
|
| Expr_power (e1, i1), Expr_power (e2, i2)
|
374
|
| Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2)
|
375
|
| _ -> false
|
376
|
|
377
|
let get_node_vars nd =
|
378
|
nd.node_inputs @ nd.node_locals @ nd.node_outputs
|
379
|
|
380
|
let get_var id var_list =
|
381
|
List.find (fun v -> v.var_id = id) var_list
|
382
|
|
383
|
let get_node_var id node = get_var id (get_node_vars node)
|
384
|
|
385
|
let get_node_eq id node =
|
386
|
List.find (fun eq -> List.mem id eq.eq_lhs) node.node_eqs
|
387
|
|
388
|
let get_nodes prog =
|
389
|
List.fold_left (
|
390
|
fun nodes decl ->
|
391
|
match decl.top_decl_desc with
|
392
|
| Node nd -> nd::nodes
|
393
|
| Consts _ | ImportedNode _ | Open _ -> nodes
|
394
|
) [] prog
|
395
|
|
396
|
let get_consts prog =
|
397
|
List.fold_left (
|
398
|
fun consts decl ->
|
399
|
match decl.top_decl_desc with
|
400
|
| Consts clist -> clist@consts
|
401
|
| Node _ | ImportedNode _ | Open _ -> consts
|
402
|
) [] prog
|
403
|
|
404
|
|
405
|
|
406
|
(************************************************************************)
|
407
|
(* Renaming *)
|
408
|
|
409
|
(* applies the renaming function [fvar] to all variables of expression [expr] *)
|
410
|
let rec expr_replace_var fvar expr =
|
411
|
{ expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc }
|
412
|
|
413
|
and expr_desc_replace_var fvar expr_desc =
|
414
|
match expr_desc with
|
415
|
| Expr_const _ -> expr_desc
|
416
|
| Expr_ident i -> Expr_ident (fvar i)
|
417
|
| Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el)
|
418
|
| Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d)
|
419
|
| Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d)
|
420
|
| Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el)
|
421
|
| Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e)
|
422
|
| Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2)
|
423
|
| Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2)
|
424
|
| Expr_pre e' -> Expr_pre (expr_replace_var fvar e')
|
425
|
| Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l)
|
426
|
| Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl)
|
427
|
| Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (fun (x, l) -> fvar x, l) i')
|
428
|
|
429
|
(* Applies the renaming function [fvar] to every rhs
|
430
|
only when the corresponding lhs satisfies predicate [pvar] *)
|
431
|
let eq_replace_rhs_var pvar fvar eq =
|
432
|
let pvar l = List.exists pvar l in
|
433
|
let rec replace lhs rhs =
|
434
|
{ rhs with expr_desc = replace_desc lhs rhs.expr_desc }
|
435
|
and replace_desc lhs rhs_desc =
|
436
|
match lhs with
|
437
|
| [] -> assert false
|
438
|
| [_] -> if pvar lhs then expr_desc_replace_var fvar rhs_desc else rhs_desc
|
439
|
| _ ->
|
440
|
(match rhs_desc with
|
441
|
| Expr_tuple tl ->
|
442
|
Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl)
|
443
|
| Expr_appl (f, arg, None) when Basic_library.is_internal_fun f ->
|
444
|
let args = expr_list_of_expr arg in
|
445
|
Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None)
|
446
|
| Expr_array _
|
447
|
| Expr_access _
|
448
|
| Expr_power _
|
449
|
| Expr_const _
|
450
|
| Expr_ident _
|
451
|
| Expr_appl _ ->
|
452
|
if pvar lhs
|
453
|
then expr_desc_replace_var fvar rhs_desc
|
454
|
else rhs_desc
|
455
|
| Expr_ite (c, t, e) -> Expr_ite (replace lhs c, replace lhs t, replace lhs e)
|
456
|
| Expr_arrow (e1, e2) -> Expr_arrow (replace lhs e1, replace lhs e2)
|
457
|
| Expr_fby (e1, e2) -> Expr_fby (replace lhs e1, replace lhs e2)
|
458
|
| Expr_pre e' -> Expr_pre (replace lhs e')
|
459
|
| Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i
|
460
|
in Expr_when (replace lhs e', i', l)
|
461
|
| Expr_merge (i, hl) -> let i' = if pvar lhs then fvar i else i
|
462
|
in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl)
|
463
|
)
|
464
|
in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs }
|
465
|
|
466
|
|
467
|
let rec rename_expr f_node f_var f_const expr =
|
468
|
{ expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc }
|
469
|
and rename_expr_desc f_node f_var f_const expr_desc =
|
470
|
let re = rename_expr f_node f_var f_const in
|
471
|
match expr_desc with
|
472
|
| Expr_const _ -> expr_desc
|
473
|
| Expr_ident i -> Expr_ident (f_var i)
|
474
|
| Expr_array el -> Expr_array (List.map re el)
|
475
|
| Expr_access (e1, d) -> Expr_access (re e1, d)
|
476
|
| Expr_power (e1, d) -> Expr_power (re e1, d)
|
477
|
| Expr_tuple el -> Expr_tuple (List.map re el)
|
478
|
| Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e)
|
479
|
| Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2)
|
480
|
| Expr_fby (e1, e2) -> Expr_fby (re e1, re e2)
|
481
|
| Expr_pre e' -> Expr_pre (re e')
|
482
|
| Expr_when (e', i, l)-> Expr_when (re e', f_var i, l)
|
483
|
| Expr_merge (i, hl) ->
|
484
|
Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl)
|
485
|
| Expr_appl (i, e', i') ->
|
486
|
Expr_appl (f_node i, re e', Utils.option_map (fun (x, l) -> f_var x, l) i')
|
487
|
|
488
|
let rename_node_annot f_node f_var f_const expr =
|
489
|
expr
|
490
|
(* TODO assert false *)
|
491
|
|
492
|
let rename_expr_annot f_node f_var f_const annot =
|
493
|
annot
|
494
|
(* TODO assert false *)
|
495
|
|
496
|
let rename_node f_node f_var f_const nd =
|
497
|
let rename_var v = { v with var_id = f_var v.var_id } in
|
498
|
let rename_eq eq = { eq with
|
499
|
eq_lhs = List.map f_var eq.eq_lhs;
|
500
|
eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs
|
501
|
}
|
502
|
in
|
503
|
let inputs = List.map rename_var nd.node_inputs in
|
504
|
let outputs = List.map rename_var nd.node_outputs in
|
505
|
let locals = List.map rename_var nd.node_locals in
|
506
|
let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in
|
507
|
let node_checks = List.map (Dimension.expr_replace_var f_var) nd.node_checks in
|
508
|
let node_asserts = List.map
|
509
|
(fun a ->
|
510
|
{a with assert_expr =
|
511
|
let expr = a.assert_expr in
|
512
|
rename_expr f_node f_var f_const expr})
|
513
|
nd.node_asserts
|
514
|
in
|
515
|
let eqs = List.map rename_eq nd.node_eqs in
|
516
|
let spec =
|
517
|
Utils.option_map
|
518
|
(fun s -> rename_node_annot f_node f_var f_const s)
|
519
|
nd.node_spec
|
520
|
in
|
521
|
let annot =
|
522
|
List.map
|
523
|
(fun s -> rename_expr_annot f_node f_var f_const s)
|
524
|
nd.node_annot
|
525
|
in
|
526
|
{
|
527
|
node_id = f_node nd.node_id;
|
528
|
node_type = nd.node_type;
|
529
|
node_clock = nd.node_clock;
|
530
|
node_inputs = inputs;
|
531
|
node_outputs = outputs;
|
532
|
node_locals = locals;
|
533
|
node_gencalls = gen_calls;
|
534
|
node_checks = node_checks;
|
535
|
node_asserts = node_asserts;
|
536
|
node_eqs = eqs;
|
537
|
node_dec_stateless = nd.node_dec_stateless;
|
538
|
node_stateless = nd.node_stateless;
|
539
|
node_spec = spec;
|
540
|
node_annot = annot;
|
541
|
}
|
542
|
|
543
|
|
544
|
let rename_const f_const c =
|
545
|
{ c with const_id = f_const c.const_id }
|
546
|
|
547
|
let rename_prog f_node f_var f_const prog =
|
548
|
List.rev (
|
549
|
List.fold_left (fun accu top ->
|
550
|
(match top.top_decl_desc with
|
551
|
| Node nd ->
|
552
|
{ top with top_decl_desc = Node (rename_node f_node f_var f_const nd) }
|
553
|
| Consts c ->
|
554
|
{ top with top_decl_desc = Consts (List.map (rename_const f_const) c) }
|
555
|
| ImportedNode _
|
556
|
| Open _ -> top)
|
557
|
::accu
|
558
|
) [] prog
|
559
|
)
|
560
|
|
561
|
(**********************************************************************)
|
562
|
(* Pretty printers *)
|
563
|
|
564
|
let pp_decl_type fmt tdecl =
|
565
|
match tdecl.top_decl_desc with
|
566
|
| Node nd ->
|
567
|
fprintf fmt "%s: " nd.node_id;
|
568
|
Utils.reset_names ();
|
569
|
fprintf fmt "%a@ " Types.print_ty nd.node_type
|
570
|
| ImportedNode ind ->
|
571
|
fprintf fmt "%s: " ind.nodei_id;
|
572
|
Utils.reset_names ();
|
573
|
fprintf fmt "%a@ " Types.print_ty ind.nodei_type
|
574
|
| Consts _ | Open _ -> ()
|
575
|
|
576
|
let pp_prog_type fmt tdecl_list =
|
577
|
Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list
|
578
|
|
579
|
let pp_decl_clock fmt cdecl =
|
580
|
match cdecl.top_decl_desc with
|
581
|
| Node nd ->
|
582
|
fprintf fmt "%s: " nd.node_id;
|
583
|
Utils.reset_names ();
|
584
|
fprintf fmt "%a@ " Clocks.print_ck nd.node_clock
|
585
|
| ImportedNode ind ->
|
586
|
fprintf fmt "%s: " ind.nodei_id;
|
587
|
Utils.reset_names ();
|
588
|
fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock
|
589
|
| Consts _ | Open _ -> ()
|
590
|
|
591
|
let pp_prog_clock fmt prog =
|
592
|
Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
|
593
|
|
594
|
let pp_error fmt = function
|
595
|
Main_not_found ->
|
596
|
fprintf fmt "Cannot compile node %s: could not find the node definition.@."
|
597
|
!Options.main_node
|
598
|
| Main_wrong_kind ->
|
599
|
fprintf fmt
|
600
|
"Name %s does not correspond to a (non-imported) node definition.@."
|
601
|
!Options.main_node
|
602
|
| No_main_specified ->
|
603
|
fprintf fmt "No main node specified@."
|
604
|
| Unbound_symbol sym ->
|
605
|
fprintf fmt
|
606
|
"%s is undefined.@."
|
607
|
sym
|
608
|
| Already_bound_symbol sym ->
|
609
|
fprintf fmt
|
610
|
"%s is already defined.@."
|
611
|
sym
|
612
|
|
613
|
(* filling node table with internal functions *)
|
614
|
let vdecls_of_typ_ck cpt ty =
|
615
|
let loc = Location.dummy_loc in
|
616
|
List.map
|
617
|
(fun _ -> incr cpt;
|
618
|
let name = sprintf "_var_%d" !cpt in
|
619
|
mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false))
|
620
|
(Types.type_list_of_type ty)
|
621
|
|
622
|
let mk_internal_node id =
|
623
|
let spec = None in
|
624
|
let ty = Env.lookup_value Basic_library.type_env id in
|
625
|
let ck = Env.lookup_value Basic_library.clock_env id in
|
626
|
let (tin, tout) = Types.split_arrow ty in
|
627
|
(*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*)
|
628
|
let cpt = ref (-1) in
|
629
|
mktop_decl Location.dummy_loc
|
630
|
(ImportedNode
|
631
|
{nodei_id = id;
|
632
|
nodei_type = ty;
|
633
|
nodei_clock = ck;
|
634
|
nodei_inputs = vdecls_of_typ_ck cpt tin;
|
635
|
nodei_outputs = vdecls_of_typ_ck cpt tout;
|
636
|
nodei_stateless = Types.get_static_value ty <> None;
|
637
|
nodei_spec = spec;
|
638
|
nodei_prototype = None;
|
639
|
nodei_in_lib = None;
|
640
|
})
|
641
|
|
642
|
let add_internal_funs () =
|
643
|
List.iter
|
644
|
(fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd)
|
645
|
Basic_library.internal_funs
|
646
|
|
647
|
|
648
|
|
649
|
(* Replace any occurence of a var in vars_to_replace by its associated
|
650
|
expression in defs until e does not contain any such variables *)
|
651
|
let rec substitute_expr vars_to_replace defs e =
|
652
|
let se = substitute_expr vars_to_replace defs in
|
653
|
{ e with expr_desc =
|
654
|
let ed = e.expr_desc in
|
655
|
match ed with
|
656
|
| Expr_const _ -> ed
|
657
|
| Expr_array el -> Expr_array (List.map se el)
|
658
|
| Expr_access (e1, d) -> Expr_access (se e1, d)
|
659
|
| Expr_power (e1, d) -> Expr_power (se e1, d)
|
660
|
| Expr_tuple el -> Expr_tuple (List.map se el)
|
661
|
| Expr_ite (c, t, e) -> Expr_ite (se c, se t, se e)
|
662
|
| Expr_arrow (e1, e2)-> Expr_arrow (se e1, se e2)
|
663
|
| Expr_fby (e1, e2) -> Expr_fby (se e1, se e2)
|
664
|
| Expr_pre e' -> Expr_pre (se e')
|
665
|
| Expr_when (e', i, l)-> Expr_when (se e', i, l)
|
666
|
| Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, se h)) hl)
|
667
|
| Expr_appl (i, e', i') -> Expr_appl (i, se e', i')
|
668
|
| Expr_ident i ->
|
669
|
if List.exists (fun v -> v.var_id = i) vars_to_replace then (
|
670
|
let eq_i eq = eq.eq_lhs = [i] in
|
671
|
if List.exists eq_i defs then
|
672
|
let sub = List.find eq_i defs in
|
673
|
let sub' = se sub.eq_rhs in
|
674
|
sub'.expr_desc
|
675
|
else
|
676
|
assert false
|
677
|
)
|
678
|
else
|
679
|
ed
|
680
|
|
681
|
}
|
682
|
(* FAUT IL RETIRER ?
|
683
|
|
684
|
let rec expr_to_eexpr expr =
|
685
|
{ eexpr_tag = expr.expr_tag;
|
686
|
eexpr_desc = expr_desc_to_eexpr_desc expr.expr_desc;
|
687
|
eexpr_type = expr.expr_type;
|
688
|
eexpr_clock = expr.expr_clock;
|
689
|
eexpr_loc = expr.expr_loc
|
690
|
}
|
691
|
and expr_desc_to_eexpr_desc expr_desc =
|
692
|
let conv = expr_to_eexpr in
|
693
|
match expr_desc with
|
694
|
| Expr_const c -> EExpr_const (match c with
|
695
|
| Const_int x -> EConst_int x
|
696
|
| Const_real x -> EConst_real x
|
697
|
| Const_float x -> EConst_float x
|
698
|
| Const_tag x -> EConst_tag x
|
699
|
| _ -> assert false
|
700
|
|
701
|
)
|
702
|
| Expr_ident i -> EExpr_ident i
|
703
|
| Expr_tuple el -> EExpr_tuple (List.map conv el)
|
704
|
|
705
|
| Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2)
|
706
|
| Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2)
|
707
|
| Expr_pre e' -> EExpr_pre (conv e')
|
708
|
| Expr_appl (i, e', i') ->
|
709
|
EExpr_appl
|
710
|
(i, conv e', match i' with None -> None | Some(id, _) -> Some id)
|
711
|
|
712
|
| Expr_when _
|
713
|
| Expr_merge _ -> assert false
|
714
|
| Expr_array _
|
715
|
| Expr_access _
|
716
|
| Expr_power _ -> assert false
|
717
|
| Expr_ite (c, t, e) -> assert false
|
718
|
| _ -> assert false
|
719
|
|
720
|
*)
|
721
|
let rec get_expr_calls nodes e =
|
722
|
get_calls_expr_desc nodes e.expr_desc
|
723
|
and get_calls_expr_desc nodes expr_desc =
|
724
|
let get_calls = get_expr_calls nodes in
|
725
|
match expr_desc with
|
726
|
| Expr_const _
|
727
|
| Expr_ident _ -> Utils.ISet.empty
|
728
|
| Expr_tuple el
|
729
|
| Expr_array el -> List.fold_left (fun accu e -> Utils.ISet.union accu (get_calls e)) Utils.ISet.empty el
|
730
|
| Expr_pre e1
|
731
|
| Expr_when (e1, _, _)
|
732
|
| Expr_access (e1, _)
|
733
|
| Expr_power (e1, _) -> get_calls e1
|
734
|
| Expr_ite (c, t, e) -> Utils.ISet.union (Utils.ISet.union (get_calls c) (get_calls t)) (get_calls e)
|
735
|
| Expr_arrow (e1, e2)
|
736
|
| Expr_fby (e1, e2) -> Utils.ISet.union (get_calls e1) (get_calls e2)
|
737
|
| Expr_merge (_, hl) -> List.fold_left (fun accu (_, h) -> Utils.ISet.union accu (get_calls h)) Utils.ISet.empty hl
|
738
|
| Expr_appl (i, e', i') ->
|
739
|
if Basic_library.is_internal_fun i then
|
740
|
(get_calls e')
|
741
|
else
|
742
|
let calls = Utils.ISet.add i (get_calls e') in
|
743
|
let test = (fun n -> match n.top_decl_desc with Node nd -> nd.node_id = i | _ -> false) in
|
744
|
if List.exists test nodes then
|
745
|
match (List.find test nodes).top_decl_desc with
|
746
|
| Node nd -> Utils.ISet.union (get_node_calls nodes nd) calls
|
747
|
| _ -> assert false
|
748
|
else
|
749
|
calls
|
750
|
|
751
|
and get_eq_calls nodes eq =
|
752
|
get_expr_calls nodes eq.eq_rhs
|
753
|
and get_node_calls nodes node =
|
754
|
List.fold_left (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty node.node_eqs
|
755
|
|
756
|
|
757
|
let rec expr_has_arrows e =
|
758
|
expr_desc_has_arrows e.expr_desc
|
759
|
and expr_desc_has_arrows expr_desc =
|
760
|
match expr_desc with
|
761
|
| Expr_const _
|
762
|
| Expr_ident _ -> false
|
763
|
| Expr_tuple el
|
764
|
| Expr_array el -> List.exists expr_has_arrows el
|
765
|
| Expr_pre e1
|
766
|
| Expr_when (e1, _, _)
|
767
|
| Expr_access (e1, _)
|
768
|
| Expr_power (e1, _) -> expr_has_arrows e1
|
769
|
| Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e]
|
770
|
| Expr_arrow (e1, e2)
|
771
|
| Expr_fby (e1, e2) -> true
|
772
|
| Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl
|
773
|
| Expr_appl (i, e', i') -> expr_has_arrows e'
|
774
|
|
775
|
and eq_has_arrows eq =
|
776
|
expr_has_arrows eq.eq_rhs
|
777
|
and node_has_arrows node =
|
778
|
List.exists (fun eq -> eq_has_arrows eq) node.node_eqs
|
779
|
|
780
|
(* Local Variables: *)
|
781
|
(* compile-command:"make -C .." *)
|
782
|
(* End: *)
|