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