Changement dans les boxed values .

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 56 insertions, 0 deletions

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 48331a6870..0d4a246a09 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -61,4 +61,60 @@ type fv_elem = FVnamed of identifier | FVrel of int
 type fv = fv_elem array
 
 
+(* --- Pretty print *)
+open Format
+let rec instruction ppf = function
+  | Klabel lbl -> fprintf ppf "L%i:" lbl
+  | Kacc n -> fprintf ppf "\tacc %i" n
+  | Kenvacc n -> fprintf ppf "\tenvacc %i" n
+  | Koffsetclosure n -> fprintf ppf "\toffsetclosure %i" n
+  | Kpush -> fprintf ppf "\tpush"
+  | Kpop n -> fprintf ppf "\tpop %i" n
+  | Kpush_retaddr lbl -> fprintf ppf "\tpush_retaddr L%i" lbl
+  | Kapply n -> fprintf ppf "\tapply %i" n
+  | Kappterm(n, m) ->
+      fprintf ppf "\tappterm %i, %i" n m
+  | Kreturn n -> fprintf ppf "\treturn %i" n
+  | Kjump -> fprintf ppf "\tjump"
+  | Krestart -> fprintf ppf "\trestart"
+  | Kgrab n -> fprintf ppf "\tgrab %i" n
+  | Kgrabrec n -> fprintf ppf "\tgrabrec %i" n
+  | Kcograb n -> fprintf ppf "\tcograb %i" n
+  | Kclosure(lbl, n) ->
+      fprintf ppf "\tclosure L%i, %i" lbl n
+  | Kclosurerec(fv,init,lblt,lblb) ->
+      fprintf ppf "\tclosurerec";
+      fprintf ppf "%i , %i, " fv init;
+      print_string "types = ";
+      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt;
+      print_string " bodies = ";
+      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
+                   (* nb fv, init, lbl types, lbl bodies *)
+  | Kgetglobal id -> fprintf ppf "\tgetglobal %s" (Names.string_of_kn id)
+  | Kconst cst ->
+      fprintf ppf "\tconst"
+  | Kmakeblock(n, m) ->
+      fprintf ppf "\tmakeblock %i, %i" n m
+  | Kmakeprod -> fprintf ppf "\tmakeprod"
+  | Kmakeswitchblock(lblt,lbls,_,sz) ->
+      fprintf ppf "\tmakeswitchblock %i, %i, %i" lblt lbls sz
+  | Kforce -> fprintf ppf "\tforce"
+  | Kswitch(lblc,lblb) -> 
+      fprintf ppf "\tswitch";
+      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblc;
+      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
+  | Kpushfield n -> 
+      fprintf ppf "\tpushfield %i" n
+  | Kstop -> fprintf ppf "\tstop"
+  | Ksequence (c1,c2) ->
+      fprintf ppf "%a@ %a" instruction_list c1 instruction_list c2 
 
+and instruction_list ppf = function
+    [] -> ()
+  | Klabel lbl :: il ->
+      fprintf ppf "L%i:%a" lbl instruction_list il
+  | instr :: il ->
+      fprintf ppf "%a@ %a" instruction instr instruction_list il
+ 
+let draw_instr c =
+  fprintf std_formatter "@[<v 0>%a@]" instruction_list c