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

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

Update Cminor pretty printer and examples.

File size: 7.1 KB
RevLine 
[1158]1diff --git a/Deliverables/D2.2/8051/src/acc.ml b/Deliverables/D2.2/8051/src/acc.ml
[1633]2index 0a95ef0..56d0cb9 100644
[1158]3--- a/Deliverables/D2.2/8051/src/acc.ml
4+++ b/Deliverables/D2.2/8051/src/acc.ml
[1633]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
[1158]14   let (exact_output, output_filename) = match Options.get_output_files () with
15     | None -> (false, filename)
16     | Some filename' -> (true, filename') in
17-  let save ?(suffix="") ast =
[1633]18-    Languages.save
[1158]19+  let save ?(suffix="") ?(matita=false) ast =
[1633]20+    Languages.save ~matita
21       (Options.is_asm_pretty ()) exact_output output_filename suffix ast
[1158]22   in
[1633]23+  let input_ast =
24+    Languages.parse ~is_lustre_file ~remove_lustre_externals
25+      src_language filename in
[1158]26+  if tgt_language = Languages.Clight &&
[1633]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
[1158]30   let target_asts =
31     (** If debugging is enabled, the compilation function returns all
32        the intermediate programs. *)
[1633]33@@ -49,6 +51,8 @@ let process filename =
[1158]34   in
35   let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in
36   save final_ast;
37+  if tgt_language <> Languages.Clight &&
38+     Options.is_matita_output_enabled () then save ~matita:true final_ast;
39   if Options.annotation_requested () then
40     begin
[1633]41       let (annotated_input_ast, cost_id, cost_incr, extern_cost_variables) =
42@@ -59,8 +63,11 @@ let process filename =
43            extern_cost_variables);
[1158]44     end;
[1633]45 
46-  if Options.is_debug_enabled () then
[1158]47+  if Options.is_debug_enabled () then begin
48     List.iter save intermediate_asts;
49+    if Options.is_matita_output_enabled () then
[1633]50+      List.iter (save ~matita:true) intermediate_asts
[1158]51+  end;
52 
[1633]53   if Options.interpretations_requested () then
[1158]54     begin
55diff --git a/Deliverables/D2.2/8051/src/clight/clightFromC.ml b/Deliverables/D2.2/8051/src/clight/clightFromC.ml
[1633]56index 0b54437..1c84dca 100644
[1158]57--- a/Deliverables/D2.2/8051/src/clight/clightFromC.ml
58+++ b/Deliverables/D2.2/8051/src/clight/clightFromC.ml
59@@ -272,6 +272,8 @@ let ezero = Expr(Econst_int(0), Tint(I32, AST.Signed))
60 let rec convertExpr env e =
61   let ty = convertTyp env e.etyp in
62   match e.edesc with
63+  | C.EConst(C.CInt(i, _, _)) when i = Int64.zero && ty = Tpointer Tvoid ->
64+      Expr(Ecast (ty, Expr (Econst_int 0, Tint (I8, AST.Unsigned))), ty)
65   | C.EConst(C.CInt(i, _, _)) ->
66       Expr(Econst_int( convertInt i), ty)
67   | C.EConst(C.CFloat(f, _, _)) ->
68diff --git a/Deliverables/D2.2/8051/src/driver.ml b/Deliverables/D2.2/8051/src/driver.ml
69index 759eafd..e0bfd69 100644
70--- a/Deliverables/D2.2/8051/src/driver.ml
71+++ b/Deliverables/D2.2/8051/src/driver.ml
72@@ -4,9 +4,9 @@
73 
74 module DataSize32 =
75 struct
76-  let alignment = Some 4
77+  let alignment = Some 1
78   let int_size = 4
79-  let ptr_size = 4
80+  let ptr_size = 2
81 end
82 
83 (* The target architecture: the Intel 8051. *)
84diff --git a/Deliverables/D2.2/8051/src/languages.ml b/Deliverables/D2.2/8051/src/languages.ml
[1633]85index 3048d99..ef7b876 100644
[1158]86--- a/Deliverables/D2.2/8051/src/languages.ml
87+++ b/Deliverables/D2.2/8051/src/languages.ml
[1633]88@@ -257,7 +257,26 @@ let string_output asm_pretty = function
89      else ["Pretty print not requested"]) @
90     [ASMPrinter.print_program p]
[1158]91 
[1633]92-let save asm_pretty exact_output filename suffix ast =
[1158]93+let string_output_matita = function
[1633]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]
[1158]111+
[1633]112+let save asm_pretty ?(matita=false) exact_output filename suffix ast =
[1158]113   let ext_chopped_filename =
114     if exact_output then filename
115     else
[1633]116@@ -265,12 +284,16 @@ let save asm_pretty exact_output filename suffix ast =
[1158]117       with Invalid_argument ("Filename.chop_extension") -> filename in
118   let ext_chopped_filename = ext_chopped_filename ^ suffix in
119   let ext_filenames =
120-    List.map (fun ext -> ext_chopped_filename ^ "." ^ ext)
121+    List.map (fun ext ->
122+        if matita then ext_chopped_filename ^ "." ^ ext ^ ".ma"
123+                  else ext_chopped_filename ^ "." ^ ext)
124       (extension (language_of_ast ast)) in
125   let output_filenames =
126     if exact_output then ext_filenames
127     else List.map Misc.SysExt.alternative ext_filenames in
[1633]128-  let output_strings = string_output asm_pretty ast in
[1158]129+  let output_strings =
130+    if matita then string_output_matita ast
[1633]131+              else string_output asm_pretty ast in
[1158]132   let f filename s =
133     let cout = open_out filename in
134     output_string cout s;
135diff --git a/Deliverables/D2.2/8051/src/languages.mli b/Deliverables/D2.2/8051/src/languages.mli
[1633]136index 26b5a0f..121c53f 100644
[1158]137--- a/Deliverables/D2.2/8051/src/languages.mli
138+++ b/Deliverables/D2.2/8051/src/languages.mli
[1633]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
[1158]145 
[1633]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
[1158]148diff --git a/Deliverables/D2.2/8051/src/options.ml b/Deliverables/D2.2/8051/src/options.ml
[1633]149index 77a7735..b4a2d05 100644
[1158]150--- a/Deliverables/D2.2/8051/src/options.ml
151+++ b/Deliverables/D2.2/8051/src/options.ml
[1633]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
[1158]154 
[1633]155 
[1158]156+let matita_flag                        = ref false
157+let is_matita_output_enabled () = !matita_flag
158+
159 (*
160 let print_result_flag          = ref false
161 let set_print_result           = (:=) print_result_flag
[1633]162@@ -233,4 +236,7 @@ let options = OptionsParsing.register [
[1158]163 
164   "-dev", Arg.Set dev_test,
165   " Playground for developers.";
166+
167+  "-m", Arg.Set matita_flag,
168+  " Output matita term (when available).";
169 ]
170diff --git a/Deliverables/D2.2/8051/src/options.mli b/Deliverables/D2.2/8051/src/options.mli
[1633]171index 2f75755..3af36c9 100644
[1158]172--- a/Deliverables/D2.2/8051/src/options.mli
173+++ b/Deliverables/D2.2/8051/src/options.mli
[1633]174@@ -75,3 +75,6 @@ val is_print_result_enabled : unit -> bool
[1158]175 
176 (** {2 Developers' playground} *)
177 val is_dev_test_enabled : unit -> bool
178+
179+(** {2 Output matita term when available} *)
180+val is_matita_output_enabled : unit -> bool
Note: See TracBrowser for help on using the repository browser.