aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/base_include1
-rw-r--r--dev/top_printers.ml107
-rw-r--r--dev/vm_printers.ml98
3 files changed, 108 insertions, 98 deletions
diff --git a/dev/base_include b/dev/base_include
index 5798a15990..1d2a55ef18 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -15,6 +15,7 @@
#directory "translate";;
#use "top_printers.ml";;
+#use "vm_printers.ml";;
#install_printer (* identifier *) prid;;
#install_printer (* label *) prlab;;
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 5b9d2ac7c3..cef2ab9798 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -21,7 +21,6 @@ open Environ
open Printer
open Tactic_printer
open Refiner
-open Tacmach
open Term
open Termops
open Clenv
@@ -85,6 +84,15 @@ let prevd evd = pp(pr_evar_defs evd)
let prclenv clenv = pp(pr_clenv clenv)
let prgoal g = pp(db_pr_goal g)
+let pr_gls gls =
+ hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls))
+
+open Util
+
+let pr_glls glls =
+ hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++
+ prlist_with_sep pr_fnl db_pr_goal (sig_it glls))
+
let prsigmagoal g = pp(pr_goal (sig_it g))
let prgls gls = pp(pr_gls gls)
let prglls glls = pp(pr_glls glls)
@@ -312,100 +320,3 @@ let _ =
*)
let ppfconstr c = ppterm (Closure.term_of_fconstr c)
-
-open Names
-open Cbytecodes
-open Cemitcodes
-open Vm
-
-let ppripos (ri,pos) =
- (match ri with
- | Reloc_annot a ->
- let sp,i = a.ci.ci_ind in
- print_string
- ("annot : MutInd("^(string_of_kn sp)^","^(string_of_int i)^")\n")
- | Reloc_const _ ->
- print_string "structured constant\n"
- | Reloc_getglobal kn ->
- print_string ("getglob "^(string_of_con kn)^"\n"));
- print_flush ()
-
-let print_vfix () = print_string "vfix"
-let print_vfix_app () = print_string "vfix_app"
-let print_vswith () = print_string "switch"
-
-let ppsort = function
- | Prop(Pos) -> print_string "Set"
- | Prop(Null) -> print_string "Prop"
- | Type u -> print_string "Type"
-
-
-
-let print_idkey idk =
- match idk with
- | ConstKey sp ->
- print_string "Cons(";
- print_string (string_of_con sp);
- print_string ")"
- | VarKey id -> print_string (string_of_id id)
- | RelKey i -> print_string "~";print_int i
-
-let rec ppzipper z =
- match z with
- | Zapp args ->
- let n = nargs args in
- open_hbox ();
- for i = 0 to n-2 do
- ppvalues (arg args i);print_string ";";print_space()
- done;
- if n-1 >= 0 then ppvalues (arg args (n-1));
- close_box()
- | Zfix _ -> print_string "Zfix"
- | Zswitch _ -> print_string "Zswitch"
-
-and ppstack s =
- open_hovbox 0;
- print_string "[";
- List.iter (fun z -> ppzipper z;print_string " | ") s;
- print_string "]";
- close_box()
-
-and ppatom a =
- match a with
- | Aid idk -> print_idkey idk
- | Aiddef(idk,_) -> print_string "&";print_idkey idk
- | Aind(sp,i) -> print_string "Ind(";
- print_string (string_of_kn sp);
- print_string ","; print_int i;
- print_string ")"
- | Afix_app _ -> print_vfix_app ()
- | Aswitch _ -> print_vswith()
-
-and ppwhd whd =
- match whd with
- | Vsort s -> ppsort s
- | Vprod _ -> print_string "product"
- | Vfun _ -> print_string "function"
- | Vfix _ -> print_vfix()
- | Vfix_app _ -> print_vfix_app()
- | Vcofix _ -> print_string "cofix"
- | Vcofix_app _ -> print_string "cofix_app"
- | Vconstr_const i -> print_string "C(";print_int i;print_string")"
- | Vconstr_block b -> ppvblock b
- | Vatom_stk(a,s) ->
- open_hbox();ppatom a;close_box();
- print_string"@";ppstack s
-
-and ppvblock b =
- open_hbox();
- print_string "Cb(";print_int (btag b);
- let n = bsize b in
- for i = 0 to n -1 do
- print_string ",";ppvalues (bfield b i)
- done;
- print_string")";
- close_box()
-
-and ppvalues v =
- open_hovbox 0;ppwhd (whd_val v);close_box();
- print_flush()
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
new file mode 100644
index 0000000000..c037eca7cc
--- /dev/null
+++ b/dev/vm_printers.ml
@@ -0,0 +1,98 @@
+open Format
+open Term
+open Names
+open Cbytecodes
+open Cemitcodes
+open Vm
+
+let ppripos (ri,pos) =
+ (match ri with
+ | Reloc_annot a ->
+ let sp,i = a.ci.ci_ind in
+ print_string
+ ("annot : MutInd("^(string_of_kn sp)^","^(string_of_int i)^")\n")
+ | Reloc_const _ ->
+ print_string "structured constant\n"
+ | Reloc_getglobal kn ->
+ print_string ("getglob "^(string_of_con kn)^"\n"));
+ print_flush ()
+
+let print_vfix () = print_string "vfix"
+let print_vfix_app () = print_string "vfix_app"
+let print_vswith () = print_string "switch"
+
+let ppsort = function
+ | Prop(Pos) -> print_string "Set"
+ | Prop(Null) -> print_string "Prop"
+ | Type u -> print_string "Type"
+
+
+
+let print_idkey idk =
+ match idk with
+ | ConstKey sp ->
+ print_string "Cons(";
+ print_string (string_of_con sp);
+ print_string ")"
+ | VarKey id -> print_string (string_of_id id)
+ | RelKey i -> print_string "~";print_int i
+
+let rec ppzipper z =
+ match z with
+ | Zapp args ->
+ let n = nargs args in
+ open_hbox ();
+ for i = 0 to n-2 do
+ ppvalues (arg args i);print_string ";";print_space()
+ done;
+ if n-1 >= 0 then ppvalues (arg args (n-1));
+ close_box()
+ | Zfix _ -> print_string "Zfix"
+ | Zswitch _ -> print_string "Zswitch"
+
+and ppstack s =
+ open_hovbox 0;
+ print_string "[";
+ List.iter (fun z -> ppzipper z;print_string " | ") s;
+ print_string "]";
+ close_box()
+
+and ppatom a =
+ match a with
+ | Aid idk -> print_idkey idk
+ | Aiddef(idk,_) -> print_string "&";print_idkey idk
+ | Aind(sp,i) -> print_string "Ind(";
+ print_string (string_of_kn sp);
+ print_string ","; print_int i;
+ print_string ")"
+ | Afix_app _ -> print_vfix_app ()
+ | Aswitch _ -> print_vswith()
+
+and ppwhd whd =
+ match whd with
+ | Vsort s -> ppsort s
+ | Vprod _ -> print_string "product"
+ | Vfun _ -> print_string "function"
+ | Vfix _ -> print_vfix()
+ | Vfix_app _ -> print_vfix_app()
+ | Vcofix _ -> print_string "cofix"
+ | Vcofix_app _ -> print_string "cofix_app"
+ | Vconstr_const i -> print_string "C(";print_int i;print_string")"
+ | Vconstr_block b -> ppvblock b
+ | Vatom_stk(a,s) ->
+ open_hbox();ppatom a;close_box();
+ print_string"@";ppstack s
+
+and ppvblock b =
+ open_hbox();
+ print_string "Cb(";print_int (btag b);
+ let n = bsize b in
+ for i = 0 to n -1 do
+ print_string ",";ppvalues (bfield b i)
+ done;
+ print_string")";
+ close_box()
+
+and ppvalues v =
+ open_hovbox 0;ppwhd (whd_val v);close_box();
+ print_flush()
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:30:50 +0000