Ignore:
Timestamp:
Oct 1, 2012, 5:58:58 PM (8 years ago)
Author:
campbell
Message:

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

Location:
Deliverables/D2.2/8051-matita-out
Files:
1 edited
1 copied

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051-matita-out/src/acc.ml

    r1546 r2383  
    2828  let is_lustre_file = Options.is_lustre_file () in
    2929  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
    3037  let input_ast =
    3138    Languages.parse ~is_lustre_file ~remove_lustre_externals
    3239      src_language filename in
     40  if tgt_language = Languages.Clight &&
     41       Options.is_matita_output_enabled () then save ~matita:true input_ast;
    3342  let input_ast = Languages.add_runtime input_ast in
    3443  let input_ast = Languages.labelize input_ast in
    35   let (exact_output, output_filename) = match Options.get_output_files () with
    36     | None -> (false, filename)
    37     | Some filename' -> (true, filename') in
    38   let save ?(suffix="") ast =
    39     Languages.save
    40       (Options.is_asm_pretty ()) exact_output output_filename suffix ast
    41   in
    4244  let target_asts =
    4345    (** If debugging is enabled, the compilation function returns all
     
    5052  let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in
    5153  save final_ast;
     54  if tgt_language <> Languages.Clight &&
     55     Options.is_matita_output_enabled () then save ~matita:true final_ast;
    5256  if Options.annotation_requested () then
    5357    begin
     
    6064    end;
    6165
    62   if Options.is_debug_enabled () then
     66  if Options.is_debug_enabled () then begin
    6367    List.iter save intermediate_asts;
     68    if Options.is_matita_output_enabled () then
     69      List.iter (save ~matita:true) intermediate_asts
     70  end;
    6471
    6572  if Options.interpretations_requested () then
Note: See TracChangeset for help on using the changeset viewer.