Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / plugins / salsa / salsa_plugin.ml @ ad4774b0

History | View | Annotate | Download (1.09 KB)

1 f6acf47b ploc
open Format 
2
open LustreSpec
3
4
let salsa_enabled = ref false
5
    (* "-salsa", Arg.Set salsa_enabled, "activate Salsa optimization <default>"; *)
6
    (* "-no-salsa", Arg.Clear salsa_enabled, "deactivate Salsa optimization"; *)
7
8
9
module Plugin =
10
(struct
11
  include PluginType.Default
12
  let name = "salsa"
13
  
14
  let options = [
15 94c457b7 ploc
        "-debug", Arg.Set SalsaDatatypes.debug, "debug salsa plugin";
16
      ]
17 f6acf47b ploc
18
  let activate () = salsa_enabled := true
19
20
  let refine_machine_code prog machine_code = 
21
    if !salsa_enabled then
22
      begin
23
	Compiler_common.check_main ();
24
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization (phase 3)@ ");
25
	(* Selecting float constants for Salsa *)
26
	let constEnv = List.fold_left (
27
	  fun accu c_topdecl ->
28
	    match c_topdecl.top_decl_desc with
29
	    | Const c when Types.is_real_type c.const_type  ->
30
	      (c.const_id, c.const_value) :: accu
31
	    | _ -> accu
32
	) [] (Corelang.get_consts prog) 
33
	in
34
	List.map 
35
	  (Machine_salsa_opt.machine_t2machine_t_optimized_by_salsa constEnv) 
36
	  machine_code 
37
      end
38
    else
39
      machine_code
40
  
41
  
42 ad4774b0 ploc
 end: PluginType.S)