summaryrefslogtreecommitdiff
path: root/checker/print.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/print.ml')
-rw-r--r--checker/print.ml166
1 files changed, 58 insertions, 108 deletions
diff --git a/checker/print.ml b/checker/print.ml
index 7ef752b0..fc9cd687 100644
--- a/checker/print.ml
+++ b/checker/print.ml
@@ -1,146 +1,96 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Format
open Cic
open Names
-let chk_pp = Pp.pp_with Format.std_formatter
+let chk_pp fmt = Pp.pp_with fmt
+let pp_arrayi pp fmt a = Array.iteri (fun i x -> pp fmt (i,x)) a
+let pp_instance fmt i = chk_pp fmt (Univ.Instance.pr i)
+let pp_id fmt id = fprintf fmt "%s" (Id.to_string id)
-let print_instance i = chk_pp (Univ.Instance.pr i)
-
-let print_pure_constr csr =
- let rec term_display c = match c with
- | Rel n -> print_string "#"; print_int n
- | Meta n -> print_string "Meta("; print_int n; print_string ")"
- | Var id -> print_string (Id.to_string id)
- | Sort s -> sort_display s
- | Cast (c,_, t) -> open_hovbox 1;
- print_string "("; (term_display c); print_cut();
- print_string "::"; (term_display t); print_string ")"; close_box()
+let print_pure_constr fmt csr =
+ let rec pp_term fmt c = match c with
+ | Rel n -> fprintf fmt "#%d" n
+ | Meta n -> fprintf fmt "Meta(%d)" n
+ | Var id -> pp_id fmt id
+ | Sort s -> pp_sort fmt s
+ | Cast (c,_, t) ->
+ fprintf fmt "@[<hov 1>(%a@;::%a)@]" pp_term c pp_term t
| Prod (Name(id),t,c) ->
- open_hovbox 1;
- print_string"("; print_string (Id.to_string id);
- print_string ":"; box_display t;
- print_string ")"; print_cut();
- box_display c; close_box()
+ fprintf fmt "@[<hov 1>(%a:%a)@;@[%a@]@]" pp_id id pp_term t pp_term c
| Prod (Anonymous,t,c) ->
- print_string"("; box_display t; print_cut(); print_string "->";
- box_display c; print_string ")";
+ fprintf fmt "(%a@,->@[%a@])" pp_term t pp_term c
| Lambda (na,t,c) ->
- print_string "["; name_display na;
- print_string ":"; box_display t; print_string "]";
- print_cut(); box_display c;
+ fprintf fmt "[%a:@[%a@]]@,@[%a@]" pp_name na pp_term t pp_term c
| LetIn (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;
+ fprintf fmt "[%a=@[%a@]@,:@[%a@]]@,@[%a@]" pp_name na pp_term b pp_term t pp_term c
| App (c,l) ->
- print_string "(";
- box_display c;
- Array.iter (fun x -> print_space (); box_display x) l;
- print_string ")"
- | Evar _ -> print_string "Evar#"
- | Const (c,u) -> print_string "Cons(";
- sp_con_display c;
- print_string ","; print_instance u;
- print_string ")"
+ fprintf fmt "(@[%a@]@, @[<hov 1>%a@])" pp_term c (pp_arrayi (fun _ (_,s) -> fprintf fmt "@[%a@]@," pp_term s)) l;
+ | Evar _ -> pp_print_string fmt "Evar#"
+ | Const (c,u) ->
+ fprintf fmt "Cons(@[%a,%a@])" sp_con_display c pp_instance u
| Ind ((sp,i),u) ->
- print_string "Ind(";
- sp_display sp;
- print_string ","; print_int i;
- print_string ","; print_instance u;
- print_string ")"
+ fprintf fmt "Ind(@[%a,%d,%a@])" sp_display sp i pp_instance u
| Construct (((sp,i),j),u) ->
- print_string "Constr(";
- sp_display sp;
- print_string ",";
- print_int i; print_string ","; print_int j;
- print_string ","; print_instance u; print_string ")"
+ fprintf fmt "Constr(%a,%d,%d,%a)" sp_display sp i j pp_instance u
| Case (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()
+ let pp_match fmt (_,mc) = fprintf fmt " @[%a@]" pp_term mc in
+ fprintf fmt "@[<v><@[%a@]>@,Case@ @[%a@]@ of@[<v>%a@]@,end@]" pp_term p pp_term c (pp_arrayi pp_match) bl
| Fix ((t,i),(lna,tl,bl)) ->
- print_string "Fix("; print_int i; print_string ")";
- print_cut();
- open_vbox 0;
- let print_fix () =
- for k = 0 to (Array.length tl) - 1 do
- open_vbox 0;
- name_display lna.(k); 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()
- done
- in print_string"{"; print_fix(); print_string"}"
+ let pp_fixc fmt (k,_) =
+ fprintf fmt "@[<v 0> %a/%d@,:@[%a@]@,:=@[%a@]@]@," pp_name lna.(k) t.(k) pp_term tl.(k) pp_term bl.(k) in
+ fprintf fmt "Fix(%d)@,@[<v>{%a}@]" i (pp_arrayi pp_fixc) tl
| CoFix(i,(lna,tl,bl)) ->
- print_string "CoFix("; print_int i; print_string ")";
- print_cut();
- open_vbox 0;
- let print_fix () =
- for k = 0 to (Array.length tl) - 1 do
- open_vbox 1;
- name_display lna.(k); print_cut(); print_string ":";
- box_display tl.(k) ; print_cut(); print_string ":=";
- box_display bl.(k); close_box ();
- print_cut();
- done
- in print_string"{"; print_fix (); print_string"}"
+ let pp_fixc fmt (k,_) =
+ fprintf fmt "@[<v 0> %a@,:@[%a@]@,:=@[%a@]@]@," pp_name lna.(k) pp_term tl.(k) pp_term bl.(k) in
+ fprintf fmt "CoFix(%d)@,@[<v>{%a}@]" i (pp_arrayi pp_fixc) tl
| Proj (p, c) ->
- print_string "Proj("; sp_con_display (Projection.constant p); print_string ",";
- box_display c; print_string ")"
+ fprintf fmt "Proj(%a,@,@[%a@])" sp_con_display (Projection.constant p) pp_term c
- and box_display c = open_hovbox 1; term_display c; close_box()
+ and pp_sort fmt = function
+ | Prop(Pos) -> pp_print_string fmt "Set"
+ | Prop(Null) -> pp_print_string fmt "Prop"
+ | Type u -> fprintf fmt "Type(%a)" chk_pp (Univ.pr_uni u)
- and sort_display = function
- | Prop(Pos) -> print_string "Set"
- | Prop(Null) -> print_string "Prop"
- | Type u -> print_string "Type("; chk_pp (Univ.pr_uni u); print_string ")"
+ and pp_name fmt = function
+ | Name id -> pp_id fmt id
+ | Anonymous -> pp_print_string fmt "_"
- and name_display = function
- | Name id -> print_string (Id.to_string id)
- | Anonymous -> print_string "_"
(* Remove the top names for library and Scratch to avoid long names *)
- and sp_display sp =
-(* let dir,l = decode_kn sp in
+ and sp_display fmt sp =
+(* let dir,l = decode_kn sp in
let ls =
match List.rev_map Id.to_string (DirPath.repr dir) with
("Top"::l)-> l
| ("Coq"::_::l) -> l
| l -> l
in List.iter (fun x -> print_string x; print_string ".") ls;*)
- print_string (MutInd.debug_to_string sp)
- and sp_con_display sp =
-(* let dir,l = decode_kn sp in
+ pp_print_string fmt (MutInd.debug_to_string sp)
+
+ and sp_con_display fmt sp =
+ (*
+ let dir,l = decode_kn sp in
let ls =
match List.rev_map Id.to_string (DirPath.repr dir) with
("Top"::l)-> l
| ("Coq"::_::l) -> l
| l -> l
in List.iter (fun x -> print_string x; print_string ".") ls;*)
- print_string (Constant.debug_to_string sp)
+ pp_print_string fmt (Constant.debug_to_string sp)
in
- try
- box_display csr; print_flush()
- with e ->
- print_string (Printexc.to_string e);print_flush ();
- raise e
-
-
-
+ try
+ fprintf fmt "@[%a@]%!" pp_term csr
+ with e ->
+ pp_print_string fmt (Printexc.to_string e);
+ print_flush ();
+ raise e
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 20:14:23 +0000