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

Last change on this file since 1180 was 1158, checked in by campbell, 9 years ago

Record patch needed to use matita pretty printers with acc.

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