lustrec / src / expand.ml @ 6a1a01d2
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 
(* compilecommand:"make C .." *) 
290 
(* End: *) 