Revision 45f0f48d src/main_lustre_compiler.ml
src/main_lustre_compiler.ml  

88  88 
end 
89  89  
90  90  
91 
let functional_backend () = 

92 
match !Options.output with 

93 
 "horn"  "lustre"  "acsl" > true 

94 
 _ > false 

95  
91  96 
(* From prog to prog *) 
92  97 
let stage1 prog dirname basename = 
93  98 
(* Removing automata *) 
...  ...  
122  127  
123  128 
(* Typing *) 
124  129 
let computed_types_env = type_decls type_env prog in 
125 


130  
126  131 
(* Clock calculus *) 
127  132 
let computed_clocks_env = clock_decls clock_env prog in 
128  133  
...  ...  
148  153 
in 
149  154 
*) 
150  155 
(* Delay calculus *) 
151 
(* 

156 
(* TO BE DONE LATER (Xavier)


152  157 
if(!Options.delay_calculus) 
153  158 
then 
154  159 
begin 
...  ...  
213  218 
end 
214  219 
else 
215  220 
begin 
216 
Log.report ~level:1 (fun fmt > fprintf fmt ".. keeping FP numbers@,");


221 
Log.report ~level:1 (fun fmt > fprintf fmt ".. keeping floatingpoint numbers@,");


217  222 
prog 
218  223 
end in 
219  224 
Log.report ~level:2 (fun fmt > fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog); 
...  ...  
221  226 
(* Checking array accesses *) 
222  227 
if !Options.check then 
223  228 
begin 
224 
Log.report ~level:1 (fun fmt > fprintf fmt ".. array access checks@,");


229 
Log.report ~level:1 (fun fmt > fprintf fmt ".. checking array accesses@,");


225  230 
Access.check_prog prog; 
226  231 
end; 
227  232  
...  ...  
257  262 
let machine_code = 
258  263 
if !Options.optimization >= 4 && !Options.output <> "horn" then 
259  264 
begin 
260 
Log.report ~level:1 (fun fmt > fprintf fmt ".. machines optimization (phase 3)@,");


265 
Log.report ~level:1 (fun fmt > fprintf fmt ".. machines optimization: common subexpression elimination@,");


261  266 
Optimize_machine.machines_cse machine_code 
262  267 
end 
263  268 
else 
...  ...  
267  272 
let machine_code, removed_table = 
268  273 
if !Options.optimization >= 2 && !Options.output <> "horn" then 
269  274 
begin 
270 
Log.report ~level:1 (fun fmt > fprintf fmt ".. machines optimization (phase 1)@ ");


275 
Log.report ~level:1 (fun fmt > fprintf fmt ".. machines optimization: constants inlining@,");


271  276 
Optimize_machine.machines_unfold (Corelang.get_consts prog) node_schs machine_code 
272  277 
end 
273  278 
else 
...  ...  
277  282 
let machine_code = 
278  283 
if !Options.optimization >= 3 && !Options.output <> "horn" then 
279  284 
begin 
280 
Log.report ~level:1 (fun fmt > fprintf fmt ".. machines optimization (phase 2)@ ");


285 
Log.report ~level:1 (fun fmt > fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");


281  286 
let node_schs = Scheduling.remove_prog_inlined_locals removed_table node_schs in 
282  287 
let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in 
283  288 
Optimize_machine.machines_fusion (Optimize_machine.machines_reuse_variables machine_code reuse_tables) 
...  ...  
292  297 
if !Options.salsa_enabled then 
293  298 
begin 
294  299 
check_main (); 
295 
Log.report ~level:1 (fun fmt > fprintf fmt ".. salsa machines optimization (phase 3)@ ");


300 
Log.report ~level:1 (fun fmt > fprintf fmt ".. salsa machines optimization: optimizing floatingpoint accuracy with Salsa@,");


296  301 
(* Selecting float constants for Salsa *) 
297  302 
let constEnv = List.fold_left ( 
298  303 
fun accu c_topdecl > 
...  ...  
348  353 
let source_out = open_out source_file in 
349  354 
let fmt = formatter_of_out_channel source_out in 
350  355 
Log.report ~level:1 (fun fmt > fprintf fmt ".. hornification@,"); 
351 
Horn_backend.translate fmt basename prog machine_code;


356 
Horn_backend.translate fmt basename prog (Machine_code.arrow_machine::machine_code);


352  357 
(* Tracability file if option is activated *) 
353  358 
if !Options.traces then ( 
354 
let traces_file = destname ^ ".traces" in (* Could be changed *) 

359 
let traces_file = destname ^ ".traces.xml" in (* Could be changed *)


355  360 
let traces_out = open_out traces_file in 
356  361 
let fmt = formatter_of_out_channel traces_out in 
357  362 
Log.report ~level:1 (fun fmt > fprintf fmt ".. tracing info@,"); 
358 
Horn_backend.traces_file fmt basename prog machine_code; 

363 
Horn_backend_traces.traces_file fmt basename prog machine_code;


359  364 
) 
360  365 
end 
361  366 
 "lustre" > 
Also available in: Unified diff