source: Deliverables/D2.3/8051-memoryspaces-branch/src/acc.ml @ 489

Last change on this file since 489 was 489, checked in by campbell, 9 years ago

Pointer fixes for the temporary version of the compiler that can output matita
terms.

File size: 2.0 KB
RevLine 
[453]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. Labellize.
11       (Only if {!Options.annotation_requested})
12
13    3. Compile to the target language.
14       (And keep track of annotations if required).
15 
16    4. Annotate the input program with collected costs.
17
18    5. Save the annotated input program.
19
20    Optionnally, we can interpret the intermediate programs
21    if {!Options.interpretation_requested}.
22*)
23let process filename = 
24  let src_language = Options.get_source_language () in
25  let tgt_language = Options.get_target_language () in
26  let input_ast    = Languages.parse src_language filename in 
27  let input_ast    = Languages.labelize input_ast in
28  let target_asts =
29    (** If debugging is enabled, the compilation function returns all
30        the intermediate programs. *)
31    Languages.compile (Options.is_debug_enabled ()) 
32      src_language tgt_language input_ast
33  in
[489]34  let final_ast, intermediate_asts = 
35    match target_asts with
36    | [] -> input_ast, []
37    | _ -> Misc.ListExt.cut_last target_asts
38  in
[453]39    Languages.save filename final_ast;
[460]40    if Options.is_matita_output_enabled () then
41      Languages.save_matita filename (input_ast :: target_asts);
[453]42    (if Options.annotation_requested () then
43       let annotated_input_ast = Languages.annotate input_ast final_ast in
44       Languages.save filename annotated_input_ast);
45    (if Options.is_debug_enabled () then 
46      List.iter (Languages.save filename) intermediate_asts);
47    if Options.interpretation_requested () || Options.is_debug_enabled () then
48      begin
49        let asts = input_ast :: target_asts in
50        let label_traces = List.map Languages.interpret asts in
51          Printf.eprintf "Checking execution traces...";
52          Checker.same_traces (List.combine asts label_traces);
53          Printf.eprintf "OK.\n%!";
54      end
55
56let _ =
57  if Options.is_dev_test_enabled () then Dev_test.do_dev_test input_files
58  else List.iter process input_files
Note: See TracBrowser for help on using the repository browser.