Ignore:
Timestamp:
Jan 4, 2012, 7:19:09 PM (9 years ago)
Author:
campbell
Message:

Update Cminor pretty printer and examples.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/acc-matita-printers.patch

    r1158 r1633  
    1 diff --git a/Deliverables/D2.2/8051/myocamlbuild_config.ml b/Deliverables/D2.2/8051/myocamlbuild_config.ml
    2 index 4abced7..9b3b756 100644
    3 --- a/Deliverables/D2.2/8051/myocamlbuild_config.ml
    4 +++ b/Deliverables/D2.2/8051/myocamlbuild_config.ml
    5 @@ -1 +1 @@
    6 -let parser_lib = "/home/akuma/Work/CerCo/Bologna/Deliverables/D2.2/8051/lib"
    7 +let parser_lib = "/home/bcampbe2/afs/cerco/cerco-git/Deliverables/D2.2/8051/lib"
    81diff --git a/Deliverables/D2.2/8051/src/acc.ml b/Deliverables/D2.2/8051/src/acc.ml
    9 index 6962751..59f03ca 100644
     2index 0a95ef0..56d0cb9 100644
    103--- a/Deliverables/D2.2/8051/src/acc.ml
    114+++ b/Deliverables/D2.2/8051/src/acc.ml
    12 @@ -25,15 +25,17 @@ let process filename =
    13    let _ = Printf.eprintf "Processing %s.\n%!" filename in
    14    let src_language    = Options.get_source_language () in
    15    let tgt_language    = Options.get_target_language () in
    16 -  let input_ast       = Languages.parse src_language filename in
    17 -  let input_ast       = Languages.add_runtime input_ast in
    18 -  let input_ast       = Languages.labelize input_ast in
     5@@ -27,18 +27,20 @@ let process filename =
     6   let tgt_language = Options.get_target_language () in
     7   let is_lustre_file = Options.is_lustre_file () in
     8   let remove_lustre_externals = Options.is_remove_lustre_externals () in
     9-  let input_ast =
     10-    Languages.parse ~is_lustre_file ~remove_lustre_externals
     11-      src_language filename in
     12-  let input_ast = Languages.add_runtime input_ast in
     13-  let input_ast = Languages.labelize input_ast in
    1914   let (exact_output, output_filename) = match Options.get_output_files () with
    2015     | None -> (false, filename)
    2116     | Some filename' -> (true, filename') in
    2217-  let save ?(suffix="") ast =
    23 -    Languages.save exact_output output_filename suffix ast
     18-    Languages.save
    2419+  let save ?(suffix="") ?(matita=false) ast =
    25 +    Languages.save ~matita exact_output output_filename suffix ast
     20+    Languages.save ~matita
     21       (Options.is_asm_pretty ()) exact_output output_filename suffix ast
    2622   in
    27 +  let input_ast       = Languages.parse src_language filename in
     23+  let input_ast =
     24+    Languages.parse ~is_lustre_file ~remove_lustre_externals
     25+      src_language filename in
    2826+  if tgt_language = Languages.Clight &&
    29 +     Options.is_matita_output_enabled () then save ~matita:true input_ast;
    30 +  let input_ast       = Languages.add_runtime input_ast in
    31 +  let input_ast       = Languages.labelize input_ast in
     27+       Options.is_matita_output_enabled () then save ~matita:true input_ast;
     28+  let input_ast = Languages.add_runtime input_ast in
     29+  let input_ast = Languages.labelize input_ast in
    3230   let target_asts =
    3331     (** If debugging is enabled, the compilation function returns all
    3432        the intermediate programs. *)
    35 @@ -42,6 +44,8 @@ let process filename =
     33@@ -49,6 +51,8 @@ let process filename =
    3634   in
    3735   let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in
     
    4139   if Options.annotation_requested () then
    4240     begin
    43        let (annotated_input_ast, cost_id, cost_incr) =
    44 @@ -50,8 +54,11 @@ let process filename =
    45           Languages.save_cost output_filename cost_id cost_incr);
     41       let (annotated_input_ast, cost_id, cost_incr, extern_cost_variables) =
     42@@ -59,8 +63,11 @@ let process filename =
     43            extern_cost_variables);
    4644     end;
    47                                             
    48 -  if Options.is_debug_enabled () then 
     45 
     46-  if Options.is_debug_enabled () then
    4947+  if Options.is_debug_enabled () then begin
    5048     List.iter save intermediate_asts;
    5149+    if Options.is_matita_output_enabled () then
    52 +      List.iter (save ~matita:true) intermediate_asts;
     50+      List.iter (save ~matita:true) intermediate_asts
    5351+  end;
    5452 
    55    if Options.interpretation_requested () || Options.is_debug_enabled () then
     53   if Options.interpretations_requested () then
    5654     begin
    5755diff --git a/Deliverables/D2.2/8051/src/clight/clightFromC.ml b/Deliverables/D2.2/8051/src/clight/clightFromC.ml
    58 index f6c274d..f5f0da8 100644
     56index 0b54437..1c84dca 100644
    5957--- a/Deliverables/D2.2/8051/src/clight/clightFromC.ml
    6058+++ b/Deliverables/D2.2/8051/src/clight/clightFromC.ml
     
    8583 (* The target architecture: the Intel 8051. *)
    8684diff --git a/Deliverables/D2.2/8051/src/languages.ml b/Deliverables/D2.2/8051/src/languages.ml
    87 index dc01a18..0120b68 100644
     85index 3048d99..ef7b876 100644
    8886--- a/Deliverables/D2.2/8051/src/languages.ml
    8987+++ b/Deliverables/D2.2/8051/src/languages.ml
    90 @@ -245,7 +245,25 @@ let string_output = function
    91    | AstASM p ->
    92      [Pretty.print_program p ; ASMPrinter.print_program p]
     88@@ -257,7 +257,26 @@ let string_output asm_pretty = function
     89      else ["Pretty print not requested"]) @
     90     [ASMPrinter.print_program p]
    9391 
    94 -let save exact_output filename suffix ast =
     92-let save asm_pretty exact_output filename suffix ast =
    9593+let string_output_matita = function
    96 +  | AstClight p ->
    97 +    [ClightPrintMatita.print_program p]
    98 +  | AstCminor p ->
    99 +    [CminorMatitaPrinter.print_program p]
    100 +  | AstRTLabs p ->
    101 +    [RTLabsMatitaPrinter.print_program p]
    102 +  | AstRTL p ->
    103 +    [RTLPrinter.print_program p]
    104 +  | AstERTL p ->
    105 +    [ERTLPrinter.print_program p]
    106 +  | AstLTL p ->
    107 +    [LTLPrinter.print_program p]
    108 +  | AstLIN p ->
    109 +    [LINPrinter.print_program p]
    110 +  | AstASM p ->
    111 +    [Pretty.print_program p ; ASMPrinter.print_program p]
     94+ | AstClight p ->
     95+   [ClightPrintMatita.print_program p]
     96+ | AstCminor p ->
     97+   [CminorMatitaPrinter.print_program p]
     98+ | AstRTLabs p ->
     99+   [RTLabsPrinter.print_program p]
     100+   (*[RTLabsMatitaPrinter.print_program p]*)
     101+ | AstRTL p ->
     102+   [RTLPrinter.print_program p]
     103+ | AstERTL p ->
     104+   [ERTLPrinter.print_program p]
     105+ | AstLTL p ->
     106+   [LTLPrinter.print_program p]
     107+ | AstLIN p ->
     108+   [LINPrinter.print_program p]
     109+ | AstASM p ->
     110+   [Pretty.print_program p ; ASMPrinter.print_program p]
    112111+
    113 +let save exact_output ?(matita=false) filename suffix ast =
     112+let save asm_pretty ?(matita=false) exact_output filename suffix ast =
    114113   let ext_chopped_filename =
    115114     if exact_output then filename
    116115     else
    117 @@ -253,12 +271,16 @@ let save exact_output filename suffix ast =
     116@@ -265,12 +284,16 @@ let save asm_pretty exact_output filename suffix ast =
    118117       with Invalid_argument ("Filename.chop_extension") -> filename in
    119118   let ext_chopped_filename = ext_chopped_filename ^ suffix in
     
    127126     if exact_output then ext_filenames
    128127     else List.map Misc.SysExt.alternative ext_filenames in
    129 -  let output_strings = string_output ast in
     128-  let output_strings = string_output asm_pretty ast in
    130129+  let output_strings =
    131130+    if matita then string_output_matita ast
    132 +              else string_output ast in
     131+              else string_output asm_pretty ast in
    133132   let f filename s =
    134133     let cout = open_out filename in
    135134     output_string cout s;
    136135diff --git a/Deliverables/D2.2/8051/src/languages.mli b/Deliverables/D2.2/8051/src/languages.mli
    137 index b96784b..1eb6cbb 100644
     136index 26b5a0f..121c53f 100644
    138137--- a/Deliverables/D2.2/8051/src/languages.mli
    139138+++ b/Deliverables/D2.2/8051/src/languages.mli
    140 @@ -79,7 +79,7 @@ val interpret : bool -> ast -> AST.trace
    141      whose name is prefixed by [filename] and whose extension is deduced from the
    142      language of the AST. If [exact_output] is false then the written file will
    143      be fresh. *)
    144 -val save : bool -> string -> string -> ast -> unit
    145 +val save : bool -> ?matita:bool -> string -> string -> ast -> unit
     139@@ -90,7 +90,7 @@ val interpret : bool -> ast -> AST.trace
     140     whose extension is deduced from the language of the AST. If [exact_output]
     141     is false then the written file will be fresh. If [asm_pretty] is true, then
     142     an additional pretty-printed assembly file is output. *)
     143-val save : bool -> bool -> string -> string -> ast -> unit
     144+val save : bool -> ?matita:bool -> bool -> string -> string -> ast -> unit
    146145 
    147  (** [save_cost_incr filename cost_id cost_incr] prints the name [cost_id] of the
    148      cost variable and then the name [cost_incr] of the cost increment function
     146 (** [save_cost exact_name filename cost_id cost_incr extern_cost_variables]
     147     prints the name [cost_id] of the cost variable, then the name [cost_incr] of
    149148diff --git a/Deliverables/D2.2/8051/src/options.ml b/Deliverables/D2.2/8051/src/options.ml
    150 index a13083c..5ca6481 100644
     149index 77a7735..b4a2d05 100644
    151150--- a/Deliverables/D2.2/8051/src/options.ml
    152151+++ b/Deliverables/D2.2/8051/src/options.ml
    153 @@ -43,6 +43,9 @@ let debug_flag                        = ref false
    154  let set_debug                  = (:=) debug_flag
    155  let is_debug_enabled ()                = !debug_flag
     152@@ -98,6 +98,9 @@ let set_lustre_test_max_int     = (:=) lustre_test_max_int
     153 let get_lustre_test_max_int ()         = !lustre_test_max_int
     154 
    156155 
    157156+let matita_flag                        = ref false
     
    161160 let print_result_flag          = ref false
    162161 let set_print_result           = (:=) print_result_flag
    163 @@ -83,4 +86,7 @@ let options = OptionsParsing.register [
     162@@ -233,4 +236,7 @@ let options = OptionsParsing.register [
    164163 
    165164   "-dev", Arg.Set dev_test,
     
    170169 ]
    171170diff --git a/Deliverables/D2.2/8051/src/options.mli b/Deliverables/D2.2/8051/src/options.mli
    172 index a00c940..13a88c3 100644
     171index 2f75755..3af36c9 100644
    173172--- a/Deliverables/D2.2/8051/src/options.mli
    174173+++ b/Deliverables/D2.2/8051/src/options.mli
    175 @@ -34,3 +34,6 @@ val is_print_result_enabled : unit -> bool
     174@@ -75,3 +75,6 @@ val is_print_result_enabled : unit -> bool
    176175 
    177176 (** {2 Developers' playground} *)
Note: See TracChangeset for help on using the changeset viewer.