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

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

Record patch needed to use matita pretty printers with acc.

File size: 7.3 KB
  • Deliverables/D2.2/8051/myocamlbuild_config.ml

    diff --git a/Deliverables/D2.2/8051/myocamlbuild_config.ml b/Deliverables/D2.2/8051/myocamlbuild_config.ml
    index 4abced7..9b3b756 100644
    a b  
    1 let parser_lib = "/home/akuma/Work/CerCo/Bologna/Deliverables/D2.2/8051/lib"
     1let parser_lib = "/home/bcampbe2/afs/cerco/cerco-git/Deliverables/D2.2/8051/lib"
  • 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 6962751..59f03ca 100644
    a b let process filename = 
    2525  let _ = Printf.eprintf "Processing %s.\n%!" filename in
    2626  let src_language    = Options.get_source_language () in
    2727  let tgt_language    = Options.get_target_language () in
    28   let input_ast       = Languages.parse src_language filename in
    29   let input_ast       = Languages.add_runtime input_ast in
    30   let input_ast       = Languages.labelize input_ast in
    3128  let (exact_output, output_filename) = match Options.get_output_files () with
    3229    | None -> (false, filename)
    3330    | Some filename' -> (true, filename') in
    34   let save ?(suffix="") ast =
    35     Languages.save exact_output output_filename suffix ast
     31  let save ?(suffix="") ?(matita=false) ast =
     32    Languages.save ~matita exact_output output_filename suffix ast
    3633  in
     34  let input_ast       = Languages.parse src_language filename in
     35  if tgt_language = Languages.Clight &&
     36     Options.is_matita_output_enabled () then save ~matita:true input_ast;
     37  let input_ast       = Languages.add_runtime input_ast in
     38  let input_ast       = Languages.labelize input_ast in
    3739  let target_asts =
    3840    (** If debugging is enabled, the compilation function returns all
    3941        the intermediate programs. *)
    let process filename = 
    4244  in
    4345  let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in
    4446  save final_ast;
     47  if tgt_language <> Languages.Clight &&
     48     Options.is_matita_output_enabled () then save ~matita:true final_ast;
    4549  if Options.annotation_requested () then
    4650    begin
    4751      let (annotated_input_ast, cost_id, cost_incr) =
    let process filename = 
    5054          Languages.save_cost output_filename cost_id cost_incr);
    5155    end;
    5256                                             
    53   if Options.is_debug_enabled () then
     57  if Options.is_debug_enabled () then begin
    5458    List.iter save intermediate_asts;
     59    if Options.is_matita_output_enabled () then
     60      List.iter (save ~matita:true) intermediate_asts;
     61  end;
    5562
    5663  if Options.interpretation_requested () || Options.is_debug_enabled () then
    5764    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 f6c274d..f5f0da8 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 dc01a18..0120b68 100644
    a b let string_output = function 
    245245  | AstASM p ->
    246246    [Pretty.print_program p ; ASMPrinter.print_program p]
    247247
    248 let save exact_output filename suffix ast =
     248let string_output_matita = function
     249  | AstClight p ->
     250    [ClightPrintMatita.print_program p]
     251  | AstCminor p ->
     252    [CminorMatitaPrinter.print_program p]
     253  | AstRTLabs p ->
     254    [RTLabsMatitaPrinter.print_program p]
     255  | AstRTL p ->
     256    [RTLPrinter.print_program p]
     257  | AstERTL p ->
     258    [ERTLPrinter.print_program p]
     259  | AstLTL p ->
     260    [LTLPrinter.print_program p]
     261  | AstLIN p ->
     262    [LINPrinter.print_program p]
     263  | AstASM p ->
     264    [Pretty.print_program p ; ASMPrinter.print_program p]
     265
     266let save exact_output ?(matita=false) filename suffix ast =
    249267  let ext_chopped_filename =
    250268    if exact_output then filename
    251269    else
    let save exact_output filename suffix ast = 
    253271      with Invalid_argument ("Filename.chop_extension") -> filename in
    254272  let ext_chopped_filename = ext_chopped_filename ^ suffix in
    255273  let ext_filenames =
    256     List.map (fun ext -> ext_chopped_filename ^ "." ^ ext)
     274    List.map (fun ext ->
     275        if matita then ext_chopped_filename ^ "." ^ ext ^ ".ma"
     276                  else ext_chopped_filename ^ "." ^ ext)
    257277      (extension (language_of_ast ast)) in
    258278  let output_filenames =
    259279    if exact_output then ext_filenames
    260280    else List.map Misc.SysExt.alternative ext_filenames in
    261   let output_strings = string_output ast in
     281  let output_strings =
     282    if matita then string_output_matita ast
     283              else string_output ast in
    262284  let f filename s =
    263285    let cout = open_out filename in
    264286    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 b96784b..1eb6cbb 100644
    a b val interpret : bool -> ast -> AST.trace 
    7979    whose name is prefixed by [filename] and whose extension is deduced from the
    8080    language of the AST. If [exact_output] is false then the written file will
    8181    be fresh. *)
    82 val save : bool -> string -> string -> ast -> unit
     82val save : bool -> ?matita:bool -> string -> string -> ast -> unit
    8383
    8484(** [save_cost_incr filename cost_id cost_incr] prints the name [cost_id] of the
    8585    cost variable and then the name [cost_incr] of the cost increment function
  • 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 a13083c..5ca6481 100644
    a b let debug_flag = ref false 
    4343let set_debug                   = (:=) debug_flag
    4444let is_debug_enabled ()         = !debug_flag
    4545
     46let matita_flag                 = ref false
     47let is_matita_output_enabled () = !matita_flag
     48
    4649(*
    4750let print_result_flag           = ref false
    4851let set_print_result            = (:=) print_result_flag
    let options = OptionsParsing.register [ 
    8386
    8487  "-dev", Arg.Set dev_test,
    8588  " Playground for developers.";
     89
     90  "-m", Arg.Set matita_flag,
     91  " Output matita term (when available).";
    8692]
  • 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 a00c940..13a88c3 100644
    a b val is_print_result_enabled : unit -> bool 
    3434
    3535(** {2 Developers' playground} *)
    3636val is_dev_test_enabled : unit -> bool
     37
     38(** {2 Output matita term when available} *)
     39val is_matita_output_enabled : unit -> bool
Note: See TracBrowser for help on using the repository browser.