source: src/acc-matita-printers.patch @ 3042

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

Update Cminor pretty printer and examples.

File size: 7.1 KB
  • Deliverables/D2.2/8051/src/acc.ml

    diff --git a/Deliverables/D2.2/8051/src/acc.ml b/Deliverables/D2.2/8051/src/acc.ml
    index 0a95ef0..56d0cb9 100644
    a b let process filename = 
    2727  let tgt_language = Options.get_target_language () in
    2828  let is_lustre_file = Options.is_lustre_file () in
    2929  let remove_lustre_externals = Options.is_remove_lustre_externals () in
    30   let input_ast =
    31     Languages.parse ~is_lustre_file ~remove_lustre_externals
    32       src_language filename in
    33   let input_ast = Languages.add_runtime input_ast in
    34   let input_ast = Languages.labelize input_ast in
    3530  let (exact_output, output_filename) = match Options.get_output_files () with
    3631    | None -> (false, filename)
    3732    | Some filename' -> (true, filename') in
    38   let save ?(suffix="") ast =
    39     Languages.save
     33  let save ?(suffix="") ?(matita=false) ast =
     34    Languages.save ~matita
    4035      (Options.is_asm_pretty ()) exact_output output_filename suffix ast
    4136  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
    4244  let target_asts =
    4345    (** If debugging is enabled, the compilation function returns all
    4446        the intermediate programs. *)
    let process filename = 
    4951  in
    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
    5458      let (annotated_input_ast, cost_id, cost_incr, extern_cost_variables) =
    let process filename = 
    5963            extern_cost_variables);
    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
    6673    begin
  • Deliverables/D2.2/8051/src/clight/clightFromC.ml

    diff --git a/Deliverables/D2.2/8051/src/clight/clightFromC.ml b/Deliverables/D2.2/8051/src/clight/clightFromC.ml
    index 0b54437..1c84dca 100644
    a b let ezero = Expr(Econst_int(0), Tint(I32, AST.Signed)) 
    272272let rec convertExpr env e =
    273273  let ty = convertTyp env e.etyp in
    274274  match e.edesc with
     275  | C.EConst(C.CInt(i, _, _)) when i = Int64.zero && ty = Tpointer Tvoid ->
     276      Expr(Ecast (ty, Expr (Econst_int 0, Tint (I8, AST.Unsigned))), ty)
    275277  | C.EConst(C.CInt(i, _, _)) ->
    276278      Expr(Econst_int( convertInt i), ty)
    277279  | C.EConst(C.CFloat(f, _, _)) ->
  • Deliverables/D2.2/8051/src/driver.ml

    diff --git a/Deliverables/D2.2/8051/src/driver.ml b/Deliverables/D2.2/8051/src/driver.ml
    index 759eafd..e0bfd69 100644
    a b  
    44
    55module DataSize32 =
    66struct
    7   let alignment = Some 4
     7  let alignment = Some 1
    88  let int_size = 4
    9   let ptr_size = 4
     9  let ptr_size = 2
    1010end
    1111
    1212(* The target architecture: the Intel 8051. *)
  • Deliverables/D2.2/8051/src/languages.ml

    diff --git a/Deliverables/D2.2/8051/src/languages.ml b/Deliverables/D2.2/8051/src/languages.ml
    index 3048d99..ef7b876 100644
    a b let string_output asm_pretty = function 
    257257     else ["Pretty print not requested"]) @
    258258    [ASMPrinter.print_program p]
    259259
    260 let save asm_pretty exact_output filename suffix ast =
     260let string_output_matita = function
     261 | AstClight p ->
     262   [ClightPrintMatita.print_program p]
     263 | AstCminor p ->
     264   [CminorMatitaPrinter.print_program p]
     265 | AstRTLabs p ->
     266   [RTLabsPrinter.print_program p]
     267   (*[RTLabsMatitaPrinter.print_program p]*)
     268 | AstRTL p ->
     269   [RTLPrinter.print_program p]
     270 | AstERTL p ->
     271   [ERTLPrinter.print_program p]
     272 | AstLTL p ->
     273   [LTLPrinter.print_program p]
     274 | AstLIN p ->
     275   [LINPrinter.print_program p]
     276 | AstASM p ->
     277   [Pretty.print_program p ; ASMPrinter.print_program p]
     278
     279let save asm_pretty ?(matita=false) exact_output filename suffix ast =
    261280  let ext_chopped_filename =
    262281    if exact_output then filename
    263282    else
    let save asm_pretty exact_output filename suffix ast = 
    265284      with Invalid_argument ("Filename.chop_extension") -> filename in
    266285  let ext_chopped_filename = ext_chopped_filename ^ suffix in
    267286  let ext_filenames =
    268     List.map (fun ext -> ext_chopped_filename ^ "." ^ ext)
     287    List.map (fun ext ->
     288        if matita then ext_chopped_filename ^ "." ^ ext ^ ".ma"
     289                  else ext_chopped_filename ^ "." ^ ext)
    269290      (extension (language_of_ast ast)) in
    270291  let output_filenames =
    271292    if exact_output then ext_filenames
    272293    else List.map Misc.SysExt.alternative ext_filenames in
    273   let output_strings = string_output asm_pretty ast in
     294  let output_strings =
     295    if matita then string_output_matita ast
     296              else string_output asm_pretty ast in
    274297  let f filename s =
    275298    let cout = open_out filename in
    276299    output_string cout s;
  • Deliverables/D2.2/8051/src/languages.mli

    diff --git a/Deliverables/D2.2/8051/src/languages.mli b/Deliverables/D2.2/8051/src/languages.mli
    index 26b5a0f..121c53f 100644
    a b val interpret : bool -> ast -> AST.trace 
    9090    whose extension is deduced from the language of the AST. If [exact_output]
    9191    is false then the written file will be fresh. If [asm_pretty] is true, then
    9292    an additional pretty-printed assembly file is output. *)
    93 val save : bool -> bool -> string -> string -> ast -> unit
     93val save : bool -> ?matita:bool -> bool -> string -> string -> ast -> unit
    9494
    9595(** [save_cost exact_name filename cost_id cost_incr extern_cost_variables]
    9696    prints the name [cost_id] of the cost variable, then the name [cost_incr] of
  • Deliverables/D2.2/8051/src/options.ml

    diff --git a/Deliverables/D2.2/8051/src/options.ml b/Deliverables/D2.2/8051/src/options.ml
    index 77a7735..b4a2d05 100644
    a b let set_lustre_test_max_int = (:=) lustre_test_max_int 
    9898let get_lustre_test_max_int ()  = !lustre_test_max_int
    9999
    100100
     101let matita_flag                 = ref false
     102let is_matita_output_enabled () = !matita_flag
     103
    101104(*
    102105let print_result_flag           = ref false
    103106let set_print_result            = (:=) print_result_flag
    let options = OptionsParsing.register [ 
    233236
    234237  "-dev", Arg.Set dev_test,
    235238  " Playground for developers.";
     239
     240  "-m", Arg.Set matita_flag,
     241  " Output matita term (when available).";
    236242]
  • Deliverables/D2.2/8051/src/options.mli

    diff --git a/Deliverables/D2.2/8051/src/options.mli b/Deliverables/D2.2/8051/src/options.mli
    index 2f75755..3af36c9 100644
    a b val is_print_result_enabled : unit -> bool 
    7575
    7676(** {2 Developers' playground} *)
    7777val is_dev_test_enabled : unit -> bool
     78
     79(** {2 Output matita term when available} *)
     80val is_matita_output_enabled : unit -> bool
Note: See TracBrowser for help on using the repository browser.