Revision 6cbbe1c1
Added by LĂ©lio Brun 8 months ago
src/machine_code.ml  

165  165  
166  166 
(* Datastructure updated while visiting equations *) 
167  167 
type machine_ctx = { 
168 
(* machine name *) 

169 
id: ident; 

168  170 
(* Memories *) 
169  171 
m: VSet.t; 
170  172 
(* Reset instructions *) 
...  ...  
181  183 
t: mc_formula_t list; 
182  184 
} 
183  185  
184 
let ctx_init = { 

186 
let ctx_init id = { 

187 
id; 

185  188 
m = VSet.empty; 
186  189 
si = []; 
187  190 
j = IMap.empty; 
...  ...  
191  194 
t = [] 
192  195 
} 
193  196  
197 
let ctx_dummy = ctx_init "" 

198  
194  199 
(****************************************************************) 
195  200 
(* Main function to translate equations into this machine context we 
196  201 
are building *) 
197  202 
(****************************************************************) 
198  203  
199 
let mk_control id vs v l inst =


204 
let mk_control v l inst = 

200  205 
mkinstr 
201 
(Imply (mk_clocked_on id vs, inst.instr_spec)) 

206 
True 

207 
(* (Imply (mk_clocked_on id vs, inst.instr_spec)) *) 

202  208 
(MBranch (v, [l, [inst]])) 
203  209  
204 
let control_on_clock env ctx ck inst = 

205 
let rec aux (ck_ids, vs, ctx, inst as acc) ck = 

210 
let control_on_clock env ctx ck spec inst =


211 
let rec aux (ck_ids, vs, ctx, spec, inst as acc) ck =


206  212 
match (Clocks.repr ck).cdesc with 
207  213 
 Con (ck, cr, l) > 
208  214 
let id = Clocks.const_of_carrier cr in 
...  ...  
212  218 
let ck_spec = mk_condition v l in 
213  219 
aux (id :: ck_ids, 
214  220 
v :: vs, 
215 
{ ctx 

216 
with c = IMap.add id ck_spec 

217 
(IMap.add id' 

218 
(And [ck_spec; mk_clocked_on ck_ids' vs]) ctx.c) 

221 
{ ctx with 

222 
c = IMap.add id ck_spec 

223 
(IMap.add id' (And [ck_spec; mk_clocked_on ck_ids' vs]) ctx.c) 

219  224 
}, 
220 
mk_control id' (v :: vs) v l inst) ck 

225 
Imply (mk_clocked_on id' (v :: vs), spec), 

226 
mk_control v l inst) ck 

221  227 
 _ > acc 
222  228 
in 
223 
let _, _, ctx, inst = aux ([], [], ctx, inst) ck in


224 
ctx, inst 

229 
let _, _, ctx, spec, inst = aux ([], [], ctx, spec, inst) ck in


230 
ctx, spec, inst


225  231  
226  232 
let reset_instance env i r c = 
227  233 
match r with 
228  234 
 Some r > 
229 
[snd (control_on_clock env ctx_init c 

230 
(mk_conditional 

231 
(translate_guard env r) 

232 
[mkinstr True (MReset i)] 

233 
[mkinstr True (MNoReset i)]))] 

235 
let _, _, inst = control_on_clock env ctx_dummy c True 

236 
(mk_conditional 

237 
(translate_guard env r) 

238 
[mkinstr True (MReset i)] 

239 
[mkinstr True (MNoReset i)]) in 

240 
[ inst ] 

234  241 
 None > [] 
235  242  
236  243  
237 
let translate_eq env ctx eq = 

244 
let translate_eq env ctx i eq =


238  245 
let translate_expr = translate_expr env in 
239  246 
let translate_act = translate_act env in 
240 
let control_on_clock ck inst = 

241 
let ctx, ins = control_on_clock env ctx ck inst in 

242 
{ ctx with s = ins :: ctx.s } 

247 
let control_on_clock ck spec inst = 

248 
let ctx, _spec, inst = control_on_clock env ctx ck spec inst in 

249 
{ ctx with 

250 
s = { inst with 

251 
instr_spec = mk_transition ~i ctx.id [] } :: ctx.s } 

243  252 
in 
244  253 
let reset_instance = reset_instance env in 
245  254 
let mkinstr' = mkinstr ~lustre_eq:eq True in 
246 
let ctl ?(ck=eq.eq_rhs.expr_clock) instr = 

247 
control_on_clock ck (mkinstr' instr) in 

255 
let ctl ?(ck=eq.eq_rhs.expr_clock) spec instr =


256 
control_on_clock ck spec (mkinstr' instr) in


248  257  
249  258 
(* Format.eprintf "translate_eq %a with clock %a@." 
250  259 
Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *) 
251  260 
match eq.eq_lhs, eq.eq_rhs.expr_desc with 
252  261 
 [x], Expr_arrow (e1, e2) > 
253  262 
let var_x = env.get_var x in 
254 
let o = new_instance (Arrow.arrow_top_decl ()) eq.eq_rhs.expr_tag in 

263 
let td = Arrow.arrow_top_decl () in 

264 
let o = new_instance td eq.eq_rhs.expr_tag in 

255  265 
let c1 = translate_expr e1 in 
256  266 
let c2 = translate_expr e2 in 
257 
let ctx = ctl (MStep ([var_x], o, [c1;c2])) in 

267 
let ctx = ctl 

268 
(mk_transition (node_name td) []) 

269 
(MStep ([var_x], o, [c1;c2])) in 

258  270 
{ ctx with 
259  271 
si = mkinstr True (MReset o) :: ctx.si; 
260 
j = IMap.add o (Arrow.arrow_top_decl (), []) ctx.j;


272 
j = IMap.add o (td, []) ctx.j;


261  273 
} 
274  
262  275 
 [x], Expr_pre e1 when env.is_local x > 
263  276 
let var_x = env.get_var x in 
264 
let ctx = ctl (MStateAssign (var_x, translate_expr e1)) in 

277 
let ctx = ctl 

278 
True 

279 
(MStateAssign (var_x, translate_expr e1)) in 

265  280 
{ ctx with 
266  281 
m = VSet.add var_x ctx.m; 
267  282 
} 
283  
268  284 
 [x], Expr_fby (e1, e2) when env.is_local x > 
269  285 
let var_x = env.get_var x in 
270 
let ctx = ctl (MStateAssign (var_x, translate_expr e2)) in 

286 
let ctx = ctl 

287 
True 

288 
(MStateAssign (var_x, translate_expr e2)) in 

271  289 
{ ctx with 
272  290 
m = VSet.add var_x ctx.m; 
273  291 
si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si; 
274  292 
} 
293  
275  294 
 p, Expr_appl (f, arg, r) 
276  295 
when not (Basic_library.is_expr_internal_fun eq.eq_rhs) > 
277  296 
let var_p = List.map (fun v > env.get_var v) p in 
...  ...  
284  303 
el [eq.eq_rhs.expr_clock] in 
285  304 
let call_ck = Clock_calculus.compute_root_clock 
286  305 
(Clock_predef.ck_tuple env_cks) in 
287 
let ctx = ctl ~ck:call_ck (MStep (var_p, o, vl)) in 

306 
let ctx = ctl 

307 
~ck:call_ck 

308 
True 

309 
(MStep (var_p, o, vl)) in 

288  310 
(*Clocks.new_var true in 
289  311 
Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc; 
290  312 
Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*) 
...  ...  
297  319 
else reset_instance o r call_ck) 
298  320 
@ ctx.s 
299  321 
} 
322  
300  323 
 [x], _ > 
301  324 
let var_x = env.get_var x in 
302 
control_on_clock eq.eq_rhs.expr_clock (translate_act (var_x, eq.eq_rhs)) 

325 
control_on_clock eq.eq_rhs.expr_clock True (translate_act (var_x, eq.eq_rhs)) 

326  
303  327 
 _ > 
304  328 
Format.eprintf "internal error: Machine_code.translate_eq %a@?" 
305  329 
Printers.pp_node_eq eq; 
...  ...  
317  341 
locals [] 
318  342  
319  343 
let translate_eqs env ctx eqs = 
320 
List.fold_right (fun eq ctx > translate_eq env ctx eq) eqs ctx 

344 
List.fold_right (fun eq (ctx, i) > 

345 
let ctx = translate_eq env ctx i eq in 

346 
ctx, i  1) 

347 
eqs (ctx, List.length eqs) 

348 
> fst 

321  349  
322  350  
323  351 
(****************************************************************) 
...  ...  
357  385 
in 
358  386 
vars, eql, assertl 
359  387  
360 
let translate_core sorted_eqs locals other_vars = 

388 
let translate_core nid sorted_eqs locals other_vars =


361  389 
let constant_eqs = constant_equations locals in 
362  390  
363  391 
let env = build_env locals other_vars in 
364  392  
365  393 
(* Compute constants' instructions *) 
366 
let ctx0 = translate_eqs env ctx_init constant_eqs in


394 
let ctx0 = translate_eqs env (ctx_init nid) constant_eqs in


367  395 
assert (VSet.is_empty ctx0.m); 
368  396 
assert (ctx0.si = []); 
369  397 
assert (IMap.is_empty ctx0.j); 
370  398  
371  399 
(* Compute ctx for all eqs *) 
372 
let ctx = translate_eqs env ctx_init sorted_eqs in


400 
let ctx = translate_eqs env (ctx_init nid) sorted_eqs in


373  401  
374  402 
ctx, ctx0.s 
375  403  
...  ...  
402  430 
* VSet.pp inout_vars 
403  431 
* ; *) 
404  432  
405 
let ctx, ctx0_s = translate_core (assert_instrs@sorted_eqs) locals inout_vars in 

433 
let ctx, ctx0_s = translate_core 

434 
nd.node_id (assert_instrs@sorted_eqs) locals inout_vars in 

406  435  
407  436 
(* Format.eprintf "ok4@.@?"; *) 
408  437 
Also available in: Unified diff
start again with spec representation