1
|
(********************************************************************)
|
2
|
(* *)
|
3
|
(* The LustreC compiler toolset / The LustreC Development Team *)
|
4
|
(* Copyright 2012 - -- ONERA - CNRS - INPT *)
|
5
|
(* *)
|
6
|
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
|
7
|
(* under the terms of the GNU Lesser General Public License *)
|
8
|
(* version 2.1. *)
|
9
|
(* *)
|
10
|
(********************************************************************)
|
11
|
|
12
|
open Clocks
|
13
|
open Corelang
|
14
|
|
15
|
(* Applies variable substitutions *)
|
16
|
let subst_var var_substs vid =
|
17
|
try Hashtbl.find var_substs vid with Not_found -> vid
|
18
|
|
19
|
(* Applies clock substitutions *)
|
20
|
let rec subst_ck ck_substs var_substs ck =
|
21
|
match ck.cdesc with
|
22
|
| Carrow (ck1, ck2) ->
|
23
|
{
|
24
|
ck with
|
25
|
cdesc =
|
26
|
Carrow
|
27
|
(subst_ck ck_substs var_substs ck1, subst_ck ck_substs var_substs ck2);
|
28
|
}
|
29
|
| Ctuple cklist ->
|
30
|
{ ck with cdesc = Ctuple (List.map (subst_ck ck_substs var_substs) cklist) }
|
31
|
| Con (ck', c) ->
|
32
|
{ ck with cdesc = Con (subst_ck ck_substs var_substs ck', c) }
|
33
|
| Connot (ck', c) ->
|
34
|
{ ck with cdesc = Connot (subst_ck ck_substs var_substs ck', c) }
|
35
|
| Pck_up (ck', k) ->
|
36
|
{ ck with cdesc = Pck_up (subst_ck ck_substs var_substs ck', k) }
|
37
|
| Pck_down (ck', k) ->
|
38
|
{ ck with cdesc = Pck_down (subst_ck ck_substs var_substs ck', k) }
|
39
|
| Pck_phase (ck', q) ->
|
40
|
{ ck with cdesc = Pck_phase (subst_ck ck_substs var_substs ck', q) }
|
41
|
| Pck_const _ ->
|
42
|
ck
|
43
|
| Cvar _ | Cunivar _ -> (
|
44
|
try Hashtbl.find ck_substs ck with Not_found -> ck)
|
45
|
| Clink ck' ->
|
46
|
subst_ck ck_substs var_substs ck'
|
47
|
| Ccarrying (_, ck') ->
|
48
|
subst_ck ck_substs var_substs ck'
|
49
|
|
50
|
(* [new_expr_instance ck_substs var_substs e edesc] returns a new "instance" of
|
51
|
expressions [e] of expression [e], where [edesc] is the expanded version of
|
52
|
[e]. *)
|
53
|
let new_expr_instance ck_substs var_substs e edesc =
|
54
|
{
|
55
|
expr_tag = Utils.new_tag ();
|
56
|
expr_desc = edesc;
|
57
|
expr_type = e.expr_type;
|
58
|
expr_clock = subst_ck ck_substs var_substs e.expr_clock;
|
59
|
expr_delay = Delay.new_var ();
|
60
|
expr_loc = e.expr_loc;
|
61
|
expr_annot = e.expr_annot;
|
62
|
}
|
63
|
|
64
|
let locals_cpt = ref 0
|
65
|
|
66
|
(* Returns a new local variable (for the main node) *)
|
67
|
let new_local vtyp vck vdd vloc =
|
68
|
let vid = "_" ^ string_of_int !locals_cpt in
|
69
|
locals_cpt := !locals_cpt + 1;
|
70
|
let ty_dec = { ty_dec_desc = Tydec_any; ty_dec_loc = vloc } in
|
71
|
(* dummy *)
|
72
|
let ck_dec = { ck_dec_desc = Ckdec_any; ck_dec_loc = vloc } in
|
73
|
(* dummy *)
|
74
|
{
|
75
|
var_id = vid;
|
76
|
var_orig = false;
|
77
|
var_dec_type = ty_dec;
|
78
|
var_dec_clock = ck_dec;
|
79
|
var_dec_deadline = vdd;
|
80
|
var_type = vtyp;
|
81
|
var_clock = vck;
|
82
|
var_loc = vloc;
|
83
|
}
|
84
|
|
85
|
(* Returns an expression correponding to variable v *)
|
86
|
let expr_of_var v =
|
87
|
{
|
88
|
expr_tag = Utils.new_tag ();
|
89
|
expr_desc = Expr_ident v.var_id;
|
90
|
expr_type = v.var_type;
|
91
|
expr_clock = v.var_clock;
|
92
|
expr_delay = Delay.new_var ();
|
93
|
expr_loc = v.var_loc;
|
94
|
expr_annot = None;
|
95
|
}
|
96
|
|
97
|
(* [build_ck_substs ck for_ck] computes the variable substitutions corresponding
|
98
|
to the substitution of [ck] for [for_ck] *)
|
99
|
let build_ck_substs ck for_ck =
|
100
|
let substs = Hashtbl.create 10 in
|
101
|
let rec aux ck for_ck =
|
102
|
let ck, for_ck = Clocks.repr ck, Clocks.repr for_ck in
|
103
|
match ck.Clocks.cdesc, for_ck.Clocks.cdesc with
|
104
|
| Clocks.Ctuple cklist1, Clocks.Ctuple cklist2 ->
|
105
|
List.iter2 aux cklist1 cklist2
|
106
|
| _, Clocks.Cunivar _ ->
|
107
|
Hashtbl.add substs for_ck ck
|
108
|
| _, _ ->
|
109
|
()
|
110
|
in
|
111
|
aux ck for_ck;
|
112
|
substs
|
113
|
|
114
|
(* Expands a list of expressions *)
|
115
|
let rec expand_list ck_substs var_substs elist =
|
116
|
List.fold_right
|
117
|
(fun e (eqs, locs, elist) ->
|
118
|
let eqs', locs', e' = expand_expr ck_substs var_substs e in
|
119
|
eqs' @ eqs, locs' @ locs, e' :: elist)
|
120
|
elist ([], [], [])
|
121
|
|
122
|
(* Expands the node instance [nd(args)]. *)
|
123
|
and expand_nodeinst parent_ck_substs parent_vsubsts nd args =
|
124
|
(* Expand arguments *)
|
125
|
let args_eqs, args_locs, args' =
|
126
|
expand_expr parent_ck_substs parent_vsubsts args
|
127
|
in
|
128
|
(* Compute clock substitutions to apply inside node's body *)
|
129
|
let ck_ins = args'.expr_clock in
|
130
|
let for_ck_ins, _ = Clocks.split_arrow nd.node_clock in
|
131
|
let ck_substs = build_ck_substs ck_ins for_ck_ins in
|
132
|
(* Compute variable substitutions to apply inside node's body, due to the
|
133
|
transformation of node variables into local variables of the main node. *)
|
134
|
let var_substs = Hashtbl.create 10 in
|
135
|
(* Add an equation in=arg for each node input + transform node input into a
|
136
|
local variable of the main node *)
|
137
|
let eq_ins, loc_ins =
|
138
|
List.split
|
139
|
(List.map2
|
140
|
(fun i e ->
|
141
|
let i' =
|
142
|
new_local i.var_type i.var_clock i.var_dec_deadline i.var_loc
|
143
|
in
|
144
|
Hashtbl.add var_substs i.var_id i'.var_id;
|
145
|
{ eq_lhs = [ i'.var_id ]; eq_rhs = e; eq_loc = i.var_loc }, i')
|
146
|
nd.node_inputs (expr_list_of_expr args'))
|
147
|
in
|
148
|
(* Transform node local variables into local variables of the main node *)
|
149
|
let loc_sub =
|
150
|
List.map
|
151
|
(fun v ->
|
152
|
let v' =
|
153
|
new_local v.var_type v.var_clock v.var_dec_deadline v.var_loc
|
154
|
in
|
155
|
Hashtbl.add var_substs v.var_id v'.var_id;
|
156
|
v')
|
157
|
nd.node_locals
|
158
|
in
|
159
|
(* Same for outputs *)
|
160
|
let loc_outs =
|
161
|
List.map
|
162
|
(fun o ->
|
163
|
let o' =
|
164
|
new_local o.var_type o.var_clock o.var_dec_deadline o.var_loc
|
165
|
in
|
166
|
Hashtbl.add var_substs o.var_id o'.var_id;
|
167
|
o')
|
168
|
nd.node_outputs
|
169
|
in
|
170
|
(* A tuple made of the node outputs will replace the node call in the parent
|
171
|
node *)
|
172
|
let eout = Expr_tuple (List.map expr_of_var loc_outs) in
|
173
|
let new_eqs, new_locals = expand_eqs ck_substs var_substs nd.node_eqs in
|
174
|
( args_eqs @ eq_ins @ new_eqs,
|
175
|
args_locs @ loc_ins @ loc_outs @ loc_sub @ new_locals,
|
176
|
eout )
|
177
|
|
178
|
(* Expands an expression *)
|
179
|
and expand_expr ck_substs var_substs expr =
|
180
|
match expr.expr_desc with
|
181
|
| Expr_const cst ->
|
182
|
[], [], new_expr_instance ck_substs var_substs expr expr.expr_desc
|
183
|
| Expr_ident id ->
|
184
|
let id' = subst_var var_substs id in
|
185
|
let edesc = Expr_ident id' in
|
186
|
[], [], new_expr_instance ck_substs var_substs expr edesc
|
187
|
| Expr_tuple elist ->
|
188
|
let new_eqs, new_locals, exp_elist =
|
189
|
expand_list ck_substs var_substs elist
|
190
|
in
|
191
|
( new_eqs,
|
192
|
new_locals,
|
193
|
new_expr_instance ck_substs var_substs expr (Expr_tuple exp_elist) )
|
194
|
| Expr_fby (cst, e) ->
|
195
|
let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in
|
196
|
let edesc = Expr_fby (cst, e') in
|
197
|
new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
|
198
|
| Expr_concat (cst, e) ->
|
199
|
let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in
|
200
|
let edesc = Expr_concat (cst, e') in
|
201
|
new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
|
202
|
| Expr_tail e ->
|
203
|
let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in
|
204
|
let edesc = Expr_tail e' in
|
205
|
new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
|
206
|
| Expr_when (e, c) ->
|
207
|
let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in
|
208
|
let edesc = Expr_when (e', c) in
|
209
|
new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
|
210
|
| Expr_whennot (e, c) ->
|
211
|
let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in
|
212
|
let edesc = Expr_whennot (e', c) in
|
213
|
new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
|
214
|
| Expr_merge (c, e1, e2) ->
|
215
|
let new_eqs1, new_locals1, e1' = expand_expr ck_substs var_substs e1 in
|
216
|
let new_eqs2, new_locals2, e2' = expand_expr ck_substs var_substs e2 in
|
217
|
let edesc = Expr_merge (c, e1', e2') in
|
218
|
( new_eqs1 @ new_eqs2,
|
219
|
new_locals1 @ new_locals2,
|
220
|
new_expr_instance ck_substs var_substs expr edesc )
|
221
|
| Expr_appl (id, e, r) -> (
|
222
|
let decl = Hashtbl.find node_table id in
|
223
|
match decl.top_decl_desc with
|
224
|
| ImportedNode _ ->
|
225
|
let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in
|
226
|
let edesc = Expr_appl (id, e', r) in
|
227
|
new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
|
228
|
| Node nd ->
|
229
|
let new_eqs, new_locals, outs =
|
230
|
expand_nodeinst ck_substs var_substs nd e
|
231
|
in
|
232
|
new_eqs, new_locals, new_expr_instance ck_substs var_substs expr outs
|
233
|
| Include _ | Consts _ | SensorDecl _ | ActuatorDecl _ ->
|
234
|
failwith "Internal error expand_expr")
|
235
|
| Expr_uclock (e, k) ->
|
236
|
let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in
|
237
|
let edesc = Expr_uclock (e', k) in
|
238
|
new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
|
239
|
| Expr_dclock (e, k) ->
|
240
|
let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in
|
241
|
let edesc = Expr_dclock (e', k) in
|
242
|
new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
|
243
|
| Expr_phclock (e, q) ->
|
244
|
let new_eqs, new_locals, e' = expand_expr ck_substs var_substs e in
|
245
|
let edesc = Expr_phclock (e', q) in
|
246
|
new_eqs, new_locals, new_expr_instance ck_substs var_substs expr edesc
|
247
|
| Expr_pre _ | Expr_arrow _ ->
|
248
|
assert false
|
249
|
(* Not used in the Prelude part of the code *)
|
250
|
|
251
|
(* Expands an equation *)
|
252
|
and expand_eq ck_substs var_substs eq =
|
253
|
let new_eqs, new_locals, expr = expand_expr ck_substs var_substs eq.eq_rhs in
|
254
|
let lhs' = List.map (subst_var var_substs) eq.eq_lhs in
|
255
|
let eq' = { eq_lhs = lhs'; eq_rhs = expr; eq_loc = eq.eq_loc } in
|
256
|
new_eqs, new_locals, eq'
|
257
|
|
258
|
(* Expands a set of equations *)
|
259
|
and expand_eqs ck_substs var_substs eqs =
|
260
|
List.fold_left
|
261
|
(fun (acc_eqs, acc_locals) eq ->
|
262
|
let new_eqs, new_locals, eq' = expand_eq ck_substs var_substs eq in
|
263
|
eq' :: (new_eqs @ acc_eqs), new_locals @ acc_locals)
|
264
|
([], []) eqs
|
265
|
|
266
|
(* Expands the body of a node, replacing recursively all the node calls it
|
267
|
contains by the body of the corresponding node. *)
|
268
|
let expand_node nd =
|
269
|
let new_eqs, new_locals =
|
270
|
expand_eqs (Hashtbl.create 10) (Hashtbl.create 10) nd.node_eqs
|
271
|
in
|
272
|
{
|
273
|
node_id = nd.node_id;
|
274
|
node_type = nd.node_type;
|
275
|
node_clock = nd.node_clock;
|
276
|
node_inputs = nd.node_inputs;
|
277
|
node_outputs = nd.node_outputs;
|
278
|
node_locals = new_locals @ nd.node_locals;
|
279
|
node_asserts = nd.node_asserts;
|
280
|
node_eqs = new_eqs;
|
281
|
node_spec = nd.node_spec;
|
282
|
node_annot = nd.node_annot;
|
283
|
}
|
284
|
|
285
|
let expand_program () =
|
286
|
if !Options.main_node = "" then raise (Corelang.Error No_main_specified);
|
287
|
let main =
|
288
|
try Hashtbl.find node_table !Options.main_node
|
289
|
with Not_found -> raise (Corelang.Error Main_not_found)
|
290
|
in
|
291
|
match main.top_decl_desc with
|
292
|
| Include _ | Consts _ | ImportedNode _ | SensorDecl _ | ActuatorDecl _ ->
|
293
|
raise (Corelang.Error Main_wrong_kind)
|
294
|
| Node nd ->
|
295
|
expand_node nd
|
296
|
|
297
|
(* Local Variables: *)
|
298
|
(* compile-command:"make -C .." *)
|
299
|
(* End: *)
|