Changeset 758 for src

Timestamp:

Apr 18, 2011, 12:33:35 PM (10 years ago)

Author:

campbell

Message:

Implement replacement of global var initialisation data by code in Cminor.

Location:

src

Files:

• Clight/test/sum.c (added)
• Clight/test/sum.ma (added)
• Cminor/cminorMatitaPrinter.ml (modified) (2 diffs)
• Cminor/initialisation.ma (added)
• Cminor/test/sum.c (added)
• Cminor/test/sum.ma (added)
• common/Globalenvs.ma (modified) (1 diff)

src/Cminor/cminorMatitaPrinter.ml

@@ -16 +16 @@
 let print_data = function
   | Data_reserve n -> Printf.sprintf "Init_space %d" n
-  | Data_int8 i -> Printf.sprintf "Init_int8 %d" i
-  | Data_int16 i -> Printf.sprintf "Init_int16 %d" i
-  | Data_int32 i -> Printf.sprintf "Init_int32 %d" i
+  | Data_int8 i -> Printf.sprintf "Init_int8 (repr %d)" i
+  | Data_int16 i -> Printf.sprintf "Init_int16 (repr %d)" i
+  | Data_int32 i -> Printf.sprintf "Init_int32 (repr %d)" i
   | Data_float32 f -> Printf.sprintf "Init_float32 %f" f
   | Data_float64 f -> Printf.sprintf "Init_float64 %f" f
 
 let print_var n (id, init) =
-  Printf.sprintf "(pair ?? (pair ?? (pair ?? %s [%s]) Any) it)"
+  Printf.sprintf "(pair ?? (pair ?? (pair ?? id_%s [%s]) Any) it)"
     id
     (MiscPottier.string_of_list ";" print_data init)
@@ -298 +298 @@
     (match main with Some f -> "id_" ^ f | None -> "ident_of_nat 0 (* None! *)")
 
+let define_var_id (id,_) =
+  Printf.sprintf "definition id_%s := ident_of_nat %d.\n" id (fresh ())
+
+let define_var_ids =
+  List.fold_left (fun s v -> s ^ (define_var_id v)) ""
+
 let print_program p =
-  Printf.sprintf "include \"Cminor/semantics.ma\".\ninclude \"common/Animation.ma\".\n\n%s\n\ndefinition myprog : Cminor_program :=\nmk_program ?? [\n%s\n]%s\n[%s]\n.\n"
+  Printf.sprintf "include \"Cminor/semantics.ma\".\ninclude \"common/Animation.ma\".\n\n%s\n\n%s\n\ndefinition myprog : Cminor_program :=\nmk_program ?? [\n%s\n]%s\n[%s]\n.\n"
+    (define_var_ids p.Cminor.vars)
     (print_functs p.Cminor.functs)
     (print_fun' 2 p.Cminor.functs)

src/common/Globalenvs.ma

@@ -447 +447 @@
   ].
 
-definition size_init_data_list : list init_data → Z ≝ 
-  λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) OZ i_data.
+definition size_init_data_list : list init_data → nat ≝ 
+  λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) O i_data.
 
 (* Nonessential properties that may require arithmetic