[checker] Printer cleanup.

Makes printing rules more explicit and should close #6799.

3 files changed, 75 insertions, 127 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index b2aeb1f14..fd2725c85 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -17,10 +17,10 @@ open Check
 
 let () = at_exit flush_all
 
-let chk_pp = Pp.pp_with Format.std_formatter
+let pp_arrayi pp fmt a = Array.iteri (fun i x -> pp fmt (i,x)) a
 
 let fatal_error info anomaly =
-  flush_all (); Format.eprintf "@[Fatal Error: @[%a@]@]%!@\n" Pp.pp_with info; flush_all ();
+  flush_all (); Format.eprintf "@[Fatal Error: @[%a@]@]@\n%!" Pp.pp_with info; flush_all ();
   exit (if anomaly then 129 else 1)
 
 let coq_root = Id.of_string "Coq"
@@ -269,26 +269,26 @@ let explain_exn = function
       | Generalization _ -> str"Generalization"
       | ActualType _ -> str"ActualType"
       | CantApplyBadType ((n,a,b),(hd,hdty),args) ->
-          Format.printf "====== ill-typed term ====@\n";
-          Format.printf "@[<hov 2>application head=@ ";
-          Print.print_pure_constr hd;
-          Format.printf "@]@\n@[<hov 2>head type=@ ";
-          Print.print_pure_constr hdty;
-          Format.printf "@]@\narguments:@\n@[<hv>";
-          Array.iteri (fun i (t,ty) ->
-            Format.printf "@[<hov 2>arg %d=@ " (i+1);
-            Print.print_pure_constr t;
-            Format.printf "@ type=@ ";
-            Print.print_pure_constr ty) args;
-          Format.printf "@]@\n====== type error ====@\n";
-          Print.print_pure_constr b;
-          Format.printf "@\nis not convertible with@\n";
-          Print.print_pure_constr a;
-          Format.printf "@\n====== universes ====@\n";
-          chk_pp
-            (Univ.pr_universes
-            (ctx.Environ.env_stratification.Environ.env_universes));
-          str "\nCantApplyBadType at argument " ++ int n
+        (* This mix of printf / pp was here before... *)
+        let fmt = Format.std_formatter in
+        let open Format in
+        let open Print in
+        fprintf fmt "====== ill-typed term ====@\n";
+        fprintf fmt "@[<hov 2>application head=@ %a@]@\n" print_pure_constr hd;
+        fprintf fmt "@[<hov 2>head type=@ %a@]@\n" print_pure_constr hdty;
+        let pp_arg fmt (i,(t,ty)) = fprintf fmt "@[<hv>@[<1>arg %d=@ @[%a@]@]@,@[<1>type=@ @[%a@]@]@]@\n@," (i+1)
+            print_pure_constr t print_pure_constr ty
+        in
+        fprintf fmt "arguments:@\n@[<hv>%a@]@\n" (pp_arrayi pp_arg) args;
+        fprintf fmt "====== type error ====@\n";
+        fprintf fmt "%a@\n" print_pure_constr b;
+        fprintf fmt "is not convertible with@\n";
+        fprintf fmt "%a@\n" print_pure_constr a;
+        fprintf fmt "====== universes ====@\n";
+        fprintf fmt "%a@\n%!" Pp.pp_with
+          (Univ.pr_universes
+             (ctx.Environ.env_stratification.Environ.env_universes));
+        str "CantApplyBadType at argument " ++ int n
       | CantApplyNonFunctional _ -> str"CantApplyNonFunctional"
       | IllFormedRecBody _ -> str"IllFormedRecBody"
       | IllTypedRecBody _ -> str"IllTypedRecBody"
diff --git a/checker/print.ml b/checker/print.ml
index c1fa8f94c..fc9cd687e 100644
--- a/checker/print.ml
+++ b/checker/print.ml
@@ -12,137 +12,85 @@ 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
diff --git a/checker/print.mli b/checker/print.mli
index 67562125f..da1362ca5 100644
--- a/checker/print.mli
+++ b/checker/print.mli
@@ -10,4 +10,4 @@
 
 open Cic
 
-val print_pure_constr : constr -> unit
+val print_pure_constr : Format.formatter -> constr -> unit