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