Revision 59294251 src/machine_code.ml
src/machine_code.ml  

280  280 
in 
281  281 
aux [] eqs 
282  282  
283 
(* specialize predefined (polymorphic) operators 

284 
wrt their instances, so that the C semantics 

285 
is preserved *) 

286 
let specialize_to_c expr = 

287 
match expr.expr_desc with 

288 
 Expr_appl (id, e, r) > 

289 
if List.exists (fun e > Types.is_bool_type e.expr_type) (expr_list_of_expr e) 

290 
then let id = 

291 
match id with 

292 
 "=" > "equi" 

293 
 "!=" > "xor" 

294 
 _ > id in 

295 
{ expr with expr_desc = Expr_appl (id, e, r) } 

296 
else expr 

297 
 _ > expr 

298  
299 
let specialize_op expr = 

300 
match !Options.output with 

301 
 "C" > specialize_to_c expr 

302 
 _ > expr 

303  
283  304 
let rec translate_expr node ((m, si, j, d, s) as args) expr = 
305 
let expr = specialize_op expr in 

284  306 
match expr.expr_desc with 
285  307 
 Expr_const v > Cst v 
286  308 
 Expr_ident x > translate_ident node args x 
...  ...  
295  317 
 Expr_merge (x, _) > raise NormalizationError 
296  318 
 Expr_appl (id, e, _) when Basic_library.is_internal_fun id > 
297  319 
let nd = node_from_name id in 
298 
(match e.expr_desc with 

299 
 Expr_tuple el > Fun (node_name nd, List.map (translate_expr node args) el) 

300 
 _ > Fun (node_name nd, [translate_expr node args e])) 

320 
Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e)) 

301  321 
 Expr_ite (g,t,e) > ( 
302  322 
(* special treatment depending on the active backend. For horn backend, ite 
303  323 
are preserved in expression. While they are removed for C or Java 
...  ...  
354  374 
j, 
355  375 
d, 
356  376 
control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e2)) :: s) 
357 
 p , Expr_appl (f, arg, r) > 

377  
378 
 p , Expr_appl (f, arg, r) when not (Basic_library.is_internal_fun f) > 

358  379 
let var_p = List.map (fun v > node_var v node) p in 
359  380 
let el = 
360  381 
match arg.expr_desc with 
...  ...  
370  391 
Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock; 
371  392 
(m, 
372  393 
(if Stateless.check_node node_f then si else MReset o :: si), 
373 
(if Basic_library.is_internal_fun f then j else Utils.IMap.add o call_f j),


394 
Utils.IMap.add o call_f j,


374  395 
d, 
375  396 
reset_instance node args o r eq.eq_rhs.expr_clock @ 
376  397 
(control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s) 
...  ...  
393  414 
 [x], _ > ( 
394  415 
let var_x = node_var x node in 
395  416 
(m, si, j, d, 
396 
control_on_clock node args eq.eq_rhs.expr_clock (translate_act node args (var_x, eq.eq_rhs)) :: s) 

417 
control_on_clock 

418 
node 

419 
args 

420 
eq.eq_rhs.expr_clock 

421 
(translate_act node args (var_x, eq.eq_rhs)) :: s 

422 
) 

397  423 
) 
398  424 
 _ > 
399  425 
begin 
...  ...  
404  430 
let translate_eqs node args eqs = 
405  431 
List.fold_right (fun eq args > translate_eq node args eq) eqs args;; 
406  432  
407 
let translate_decl nd = 

433 
let translate_decl nd sch =


408  434 
(*Log.report ~level:1 (fun fmt > Printers.pp_node fmt nd);*) 
409 
let nd, sch = Scheduling.schedule_node nd in 

410  435 
let split_eqs = Splitting.tuple_split_eq_list nd.node_eqs in 
411  436 
let eqs_rev, remainder = 
412  437 
List.fold_left 
...  ...  
462  487 
mannot = nd.node_annot; 
463  488 
} 
464  489  
465  
466 
let translate_prog decls = 

490 
(** takes the global delcarations and the scheduling associated to each node *) 

491 
let translate_prog decls node_schs =


467  492 
let nodes = get_nodes decls in 
468 
(* What to do with Imported/Sensor/Actuators ? *) 

469 
(*arrow_machine ::*) List.map translate_decl nodes 

493 
List.map 

494 
(fun node > 

495 
let sch = List.assoc node.node_id node_schs in 

496 
translate_decl node sch 

497 
) nodes 

470  498  
471  499 
let get_machine_opt name machines = 
472  500 
List.fold_left 
Also available in: Unified diff