source: Deliverables/D2.2/8051-matita-out/src/acc.ml @ 2383

Last change on this file since 2383 was 2383, checked in by campbell, 8 years ago

Branch prototype so that there's a version with the matita output patch
preinstalled.

File size: 4.4 KB
Line 
1open Options
2
3(** Parse the command line. *)
4let input_files = OptionsParsing.results ()
5
6(** For each input file of the source language:
7
8    1. Parse.
9
10    2. Add runtime functions.
11
12    3. Labelize.
13
14    4. Compile to the target language.
15       (And keep track of annotations if required).
16 
17    5. Annotate the input program with collected costs.
18
19    6. Save the annotated input program.
20
21    Optionnally, we can interpret the intermediate programs
22    if {!Options.interpretation_requested}.
23*)
24let process filename = 
25  let _ = Printf.printf "Processing %s.\n%!" filename in
26  let src_language = Options.get_source_language () in
27  let tgt_language = Options.get_target_language () in
28  let is_lustre_file = Options.is_lustre_file () in
29  let remove_lustre_externals = Options.is_remove_lustre_externals () in
30  let (exact_output, output_filename) = match Options.get_output_files () with
31    | None -> (false, filename)
32    | Some filename' -> (true, filename') in
33  let save ?(suffix="") ?(matita=false) ast = 
34    Languages.save ~matita
35      (Options.is_asm_pretty ()) exact_output output_filename suffix ast
36  in
37  let input_ast =
38    Languages.parse ~is_lustre_file ~remove_lustre_externals
39      src_language filename in
40  if tgt_language = Languages.Clight &&
41       Options.is_matita_output_enabled () then save ~matita:true input_ast;
42  let input_ast = Languages.add_runtime input_ast in 
43  let input_ast = Languages.labelize input_ast in
44  let target_asts =
45    (** If debugging is enabled, the compilation function returns all
46        the intermediate programs. *)
47    Languages.compile
48      (Options.is_debug_enabled ()) 
49      (Options.get_transformations ())
50      src_language tgt_language input_ast
51  in
52  let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in
53  save final_ast;
54  if tgt_language <> Languages.Clight &&
55     Options.is_matita_output_enabled () then save ~matita:true final_ast;
56  if Options.annotation_requested () then
57    begin
58      let (annotated_input_ast, cost_id, cost_incr, extern_cost_variables) =
59        let cost_tern = Options.is_cost_ternary_enabled () in
60        Languages.annotate cost_tern input_ast final_ast in (
61          save ~suffix:"-annotated" annotated_input_ast;
62          Languages.save_cost exact_output output_filename cost_id cost_incr
63            extern_cost_variables);
64    end;
65
66  if Options.is_debug_enabled () then begin
67    List.iter save intermediate_asts;
68    if Options.is_matita_output_enabled () then
69      List.iter (save ~matita:true) intermediate_asts
70  end;
71
72  if Options.interpretations_requested () then
73    begin
74      let asts = target_asts in
75      let debug = Options.is_debug_enabled () in
76      let label_traces = List.map (Languages.interpret debug) asts in
77      Printf.eprintf "Checking execution traces...%!";
78      Checker.same_traces (List.combine asts label_traces);
79      Printf.eprintf "OK.\n%!";
80    end;
81
82  if Options.interpretation_requested () then
83    ignore (Languages.interpret (Options.is_debug_enabled ()) final_ast)
84
85let lustre_test filename =
86  let lustre_test       = match Options.get_lustre_test () with
87    | None -> assert false (* do not use on this argument *)
88    | Some lustre_test -> lustre_test in
89  let lustre_test_cases = Options.get_lustre_test_cases () in
90  let lustre_test_cycles = Options.get_lustre_test_cycles () in
91  let lustre_test_min_int = Options.get_lustre_test_min_int () in
92  let lustre_test_max_int = Options.get_lustre_test_max_int () in
93  let src_language      = Languages.Clight in
94  let tgt_language      = Languages.Clight in
95  let input_ast         = Languages.parse src_language filename in
96  let input_ast         =
97    Languages.add_lustre_main lustre_test lustre_test_cases lustre_test_cycles
98      lustre_test_min_int lustre_test_max_int input_ast in 
99  let (exact_output, output_filename) = match Options.get_output_files () with
100    | None -> (false, filename)
101    | Some filename' -> (true, filename') in
102  let save ast =
103    Languages.save
104      (Options.is_asm_pretty ()) exact_output output_filename "" ast in
105  let target_asts =
106    Languages.compile false (Options.get_transformations ())
107      src_language tgt_language input_ast
108  in
109  let final_ast, _ = Misc.ListExt.cut_last target_asts in
110  save input_ast ;
111  save final_ast
112
113let _ =
114  if Options.is_dev_test_enabled () then Dev_test.do_dev_test input_files
115  else
116    if Options.get_lustre_test () <> None then List.iter lustre_test input_files
117    else List.iter process input_files
Note: See TracBrowser for help on using the repository browser.