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