lustrec / src / expand.ml @ 54d032f5
History | View | Annotate | Download (10.8 KB)
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: *) |