From 65febb705e4c76c24306a7dc30b8fe5902eefe13 Mon Sep 17 00:00:00 2001 From: mohring Date: Fri, 15 Dec 2000 08:20:10 +0000 Subject: Printer git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1117 85f007b7-540e-0410-9357-904b9bb8a0f7 --- dev/base_db | 2 +- dev/base_include | 1 + dev/top_printers.ml | 127 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 129 insertions(+), 1 deletion(-) (limited to 'dev') diff --git a/dev/base_db b/dev/base_db index 7f1822961..b540aed6c 100644 --- a/dev/base_db +++ b/dev/base_db @@ -2,5 +2,5 @@ load_printer "gramlib.cma" load_printer "top_printers.cmo" install_printer Top_printers.prid install_printer Top_printers.prsp -install_printer Top_printers.constr_display +install_printer Top_printers.print_pure_constr diff --git a/dev/base_include b/dev/base_include index b73f45206..7e233d171 100644 --- a/dev/base_include +++ b/dev/base_include @@ -30,6 +30,7 @@ Topdirs.dir_directory Coq_config.camlp4lib;; #install_printer (* identifier *) prid;; #install_printer (* section_path *) prsp;; +#install_printer (* constr *) print_pure_constr;; (* parsing of terms *) diff --git a/dev/top_printers.ml b/dev/top_printers.ml index d650ec03f..95c85866d 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -137,6 +137,124 @@ let constr_display csr = in mSG [<'sTR (term_display csr);'fNL>] +open Format;; + +let print_pure_constr csr = + let rec term_display c = match kind_of_term c with + | IsRel n -> print_string "#"; print_int n + | IsMeta n -> print_string "Meta("; print_int n; print_string ")" + | IsVar id -> print_string (string_of_id id) + | IsSort s -> sort_display s + | IsXtra s -> print_string ("Xtra("^s^")") + | IsCast (c,t) -> open_hovbox 1; + print_string "("; (term_display c); print_cut(); + print_string "::"; (term_display t); print_string ")"; close_box() + | IsProd (Name(id),t,c) -> + open_hovbox 1; + print_string"("; print_string (string_of_id id); + print_string ":"; box_display t; + print_string ")"; print_cut(); + box_display c; close_box() + | IsProd (Anonymous,t,c) -> + print_string"("; box_display t; print_cut(); print_string "->"; + box_display c; print_string ")"; + | IsLambda (na,t,c) -> + print_string "["; name_display na; + print_string ":"; box_display t; print_string "]"; + print_cut(); box_display c; + | IsLetIn (na,b,t,c) -> + print_string "["; name_display na; print_string "="; + box_display b; print_cut(); + print_string ":"; box_display t; print_string "]"; + print_cut(); box_display c; + | IsApp (c,l) -> + print_string "("; + box_display c; + Array.iter (fun x -> print_space (); box_display x) l; + print_string ")" + | IsEvar (e,l) -> print_string "Evar#"; print_int e; print_string "{"; + Array.iter (fun x -> print_space (); box_display x) l; + print_string"}" + | IsConst (c,l) -> print_string "Cons("; + sp_display c; + print_string "){"; + Array.iter (fun x -> print_space (); box_display x) l; + print_string"}" + | IsMutInd ((sp,i),l) -> + print_string "Ind("; + sp_display sp; + print_string ","; print_int i; + print_string "){"; + Array.iter (fun x -> print_space (); box_display x) l; + print_string"}" + | IsMutConstruct (((sp,i),j),l) -> + print_string "Constr("; + sp_display sp; + print_string ","; + print_int i; print_string ","; print_int j; print_string ")"; + Array.iter (fun x -> print_space (); box_display x) l; + | IsMutCase (ci,p,c,bl) -> + open_vbox 0; + print_string "<"; box_display p; print_string ">"; + print_cut(); print_string "Case"; + print_space(); box_display c; print_space (); print_string "of"; + open_vbox 0; + Array.iter (fun x -> print_cut(); box_display x) bl; + close_box(); + print_cut(); + print_string "end"; + close_box() + | IsFix ((t,i),(tl,lna,bl)) -> + print_string "Fix("; print_int i; print_string ")"; + print_cut(); + open_vbox 0; + let rec print_fix lna k = + match lna with [] -> () + | nf::ln -> open_vbox 0; + name_display nf; print_string "/"; + print_int t.(k); print_cut(); print_string ":"; + box_display tl.(k) ; print_cut(); print_string ":="; + box_display bl.(k); close_box (); + print_cut(); + print_fix ln (k+1) + in print_string"{"; print_fix lna 0; print_string"}" + | IsCoFix(i,(tl,lna,bl)) -> + print_string "CoFix("; print_int i; print_string ")"; + print_cut(); + open_vbox 0; + let rec print_fix lna k = + match lna with [] -> () + | nf::ln -> open_vbox 1; + name_display nf; print_cut(); print_string ":"; + box_display tl.(k) ; print_cut(); print_string ":="; + box_display bl.(k); close_box (); + print_cut(); + print_fix ln (k+1) + in print_string"{"; print_fix lna 0; print_string"}" + + and box_display c = open_hovbox 1; term_display c; close_box() + + and sort_display = function + | Prop(Pos) -> print_string "Set" + | Prop(Null) -> print_string "Prop" + | Type u -> open_hbox(); + print_string "Type("; pP (pr_uni u); print_string ")"; close_box() + + and name_display = function + | Name id -> print_string (string_of_id id) + | Anonymous -> print_string "_" +(* Remove the top names for library and Scratch to avoid long names *) + and sp_display sp = let ls = + match (dirpath sp) with + ("Scratch"::l)-> l + | ("Coq"::_::l) -> l + | l -> l + in List.iter (fun x -> print_string x; print_string ".") ls; + print_string (string_of_id (basename sp)) + + in + box_display csr; print_newline() + let _ = Vernacentries.add "PrintConstr" (function @@ -145,3 +263,12 @@ let _ = let (evmap,sign) = Command.get_current_context () in constr_display (Astterm.interp_constr evmap sign c)) | _ -> bad_vernac_args "PrintConstr") + +let _ = + Vernacentries.add "PrintPureConstr" + (function + | [VARG_CONSTR c] -> + (fun () -> + let (evmap,sign) = Command.get_current_context () in + print_pure_constr (Astterm.interp_constr evmap sign c)) + | _ -> bad_vernac_args "PrintPureConstr") -- cgit v1.2.3