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

Deliverables/D2.2/8051/myocamlbuild_config.ml

@@ -1 @@
-let parser_lib = "/home/akuma/Work/CerCo/Bologna/Deliverables/D2.2/8051/lib"
+let parser_lib = "/home/bcampbe2/afs/cerco/cerco-git/Deliverables/D2.2/8051/lib"

Deliverables/D2.2/8051/src/acc.ml

@@ -25 +25 @@
   let _ = Printf.eprintf "Processing %s.\n%!" filename in
   let src_language    = Options.get_source_language () in
   let tgt_language    = Options.get_target_language () in
-  let input_ast       = Languages.parse src_language filename in 
-  let input_ast       = Languages.add_runtime input_ast in 
-  let input_ast       = Languages.labelize input_ast in
   let (exact_output, output_filename) = match Options.get_output_files () with
     | None -> (false, filename)
     | Some filename' -> (true, filename') in
-  let save ?(suffix="") ast = 
-    Languages.save exact_output output_filename suffix ast 
+  let save ?(suffix="") ?(matita=false) ast = 
+    Languages.save ~matita exact_output output_filename suffix ast 
   in
+  let input_ast       = Languages.parse src_language filename in 
+  if tgt_language = Languages.Clight &&
+     Options.is_matita_output_enabled () then save ~matita:true input_ast;
+  let input_ast       = Languages.add_runtime input_ast in 
+  let input_ast       = Languages.labelize input_ast in
   let target_asts =
     (** If debugging is enabled, the compilation function returns all
         the intermediate programs. *)
@@ -42 +44 @@
   in
   let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in
   save final_ast;
+  if tgt_language <> Languages.Clight &&
+     Options.is_matita_output_enabled () then save ~matita:true final_ast;
   if Options.annotation_requested () then
     begin
       let (annotated_input_ast, cost_id, cost_incr) =
@@ -50 +54 @@
           Languages.save_cost output_filename cost_id cost_incr);
     end;
                                              
-  if Options.is_debug_enabled () then 
+  if Options.is_debug_enabled () then begin
     List.iter save intermediate_asts;
+    if Options.is_matita_output_enabled () then
+      List.iter (save ~matita:true) intermediate_asts;
+  end;
 
   if Options.interpretation_requested () || Options.is_debug_enabled () then
     begin

Deliverables/D2.2/8051/src/clight/clightFromC.ml

@@ -272 +272 @@
 let rec convertExpr env e =
   let ty = convertTyp env e.etyp in
   match e.edesc with
+  | C.EConst(C.CInt(i, _, _)) when i = Int64.zero && ty = Tpointer Tvoid ->
+      Expr(Ecast (ty, Expr (Econst_int 0, Tint (I8, AST.Unsigned))), ty)
   | C.EConst(C.CInt(i, _, _)) ->
       Expr(Econst_int( convertInt i), ty)
   | C.EConst(C.CFloat(f, _, _)) ->

Deliverables/D2.2/8051/src/driver.ml

@@ -4 +4 @@
 
 module DataSize32 =
 struct
-  let alignment = Some 4
+  let alignment = Some 1
   let int_size = 4
-  let ptr_size = 4
+  let ptr_size = 2
 end
 
 (* The target architecture: the Intel 8051. *)

Deliverables/D2.2/8051/src/languages.ml

@@ -245 +245 @@
   | AstASM p ->
     [Pretty.print_program p ; ASMPrinter.print_program p]
 
-let save exact_output filename suffix ast =
+let string_output_matita = function
+  | AstClight p -> 
+    [ClightPrintMatita.print_program p]
+  | AstCminor p ->
+    [CminorMatitaPrinter.print_program p]
+  | AstRTLabs p ->
+    [RTLabsMatitaPrinter.print_program p]
+  | AstRTL p ->
+    [RTLPrinter.print_program p]
+  | AstERTL p ->
+    [ERTLPrinter.print_program p]
+  | AstLTL p ->
+    [LTLPrinter.print_program p]
+  | AstLIN p ->
+    [LINPrinter.print_program p]
+  | AstASM p ->
+    [Pretty.print_program p ; ASMPrinter.print_program p]
+
+let save exact_output ?(matita=false) filename suffix ast =
   let ext_chopped_filename =
     if exact_output then filename 
     else
@@ -253 +271 @@
       with Invalid_argument ("Filename.chop_extension") -> filename in
   let ext_chopped_filename = ext_chopped_filename ^ suffix in
   let ext_filenames =
-    List.map (fun ext -> ext_chopped_filename ^ "." ^ ext)
+    List.map (fun ext ->
+        if matita then ext_chopped_filename ^ "." ^ ext ^ ".ma"
+                  else ext_chopped_filename ^ "." ^ ext)
       (extension (language_of_ast ast)) in
   let output_filenames =
     if exact_output then ext_filenames
     else List.map Misc.SysExt.alternative ext_filenames in
-  let output_strings = string_output ast in
+  let output_strings =
+    if matita then string_output_matita ast
+              else string_output ast in
   let f filename s =
     let cout = open_out filename in
     output_string cout s;

Deliverables/D2.2/8051/src/languages.mli

@@ -79 +79 @@
     whose name is prefixed by [filename] and whose extension is deduced from the
     language of the AST. If [exact_output] is false then the written file will
     be fresh. *)
-val save : bool -> string -> string -> ast -> unit
+val save : bool -> ?matita:bool -> string -> string -> ast -> unit
 
 (** [save_cost_incr filename cost_id cost_incr] prints the name [cost_id] of the
     cost variable and then the name [cost_incr] of the cost increment function

Deliverables/D2.2/8051/src/options.ml

@@ -43 +43 @@
 let set_debug                   = (:=) debug_flag
 let is_debug_enabled ()         = !debug_flag
 
+let matita_flag                 = ref false
+let is_matita_output_enabled () = !matita_flag
+
 (*
 let print_result_flag           = ref false
 let set_print_result            = (:=) print_result_flag
@@ -83 +86 @@
 
   "-dev", Arg.Set dev_test,
   " Playground for developers.";
+
+  "-m", Arg.Set matita_flag,
+  " Output matita term (when available).";
 ]

Deliverables/D2.2/8051/src/options.mli

@@ -34 +34 @@
 
 (** {2 Developers' playground} *)
 val is_dev_test_enabled : unit -> bool
+
+(** {2 Output matita term when available} *)
+val is_matita_output_enabled : unit -> bool