Move debug term printer to kernel

11 files changed, 101 insertions, 87 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index 52880846f8..ada6311067 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -24,84 +24,13 @@ module CompactedDecl = Context.Compacted.Declaration
 
 module Internal = struct
 
-(* Sorts and sort family *)
-
-let print_sort = function
-  | Set -> (str "Set")
-  | Prop -> (str "Prop")
-  | Type u -> (str "Type(" ++ Univ.Universe.pr u ++ str ")")
-
-let pr_sort_family = function
-  | InSet -> (str "Set")
-  | InProp -> (str "Prop")
-  | InType -> (str "Type")
-
-let pr_con sp = str(Constant.to_string sp)
-
-let pr_fix pr_constr ((t,i),(lna,tl,bl)) =
-  let fixl = Array.mapi (fun i na -> (na,t.(i),tl.(i),bl.(i))) lna in
-  hov 1
-      (str"fix " ++ int i ++ spc() ++  str"{" ++
-         v 0 (prlist_with_sep spc (fun (na,i,ty,bd) ->
-           Name.print na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++
-	   cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
-         str"}")
-
-let pr_puniverses p u = 
-  if Univ.Instance.is_empty u then p 
-  else p ++ str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)"
-
-(* Minimalistic constr printer, typically for debugging *)
-
-let rec pr_constr c = match kind c with
-  | Rel n -> str "#"++int n
-  | Meta n -> str "Meta(" ++ int n ++ str ")"
-  | Var id -> Id.print id
-  | Sort s -> print_sort s
-  | Cast (c,_, t) -> hov 1
-      (str"(" ++ pr_constr c ++ cut() ++
-       str":" ++ pr_constr t ++ str")")
-  | Prod (Name(id),t,c) -> hov 1
-      (str"forall " ++ Id.print id ++ str":" ++ pr_constr t ++ str"," ++
-       spc() ++ pr_constr c)
-  | Prod (Anonymous,t,c) -> hov 0
-      (str"(" ++ pr_constr t ++ str " ->" ++ spc() ++
-       pr_constr c ++ str")")
-  | Lambda (na,t,c) -> hov 1
-      (str"fun " ++ Name.print na ++ str":" ++
-       pr_constr t ++ str" =>" ++ spc() ++ pr_constr c)
-  | LetIn (na,b,t,c) -> hov 0
-      (str"let " ++ Name.print na ++ str":=" ++ pr_constr b ++
-       str":" ++ brk(1,2) ++ pr_constr t ++ cut() ++
-       pr_constr c)
-  | App (c,l) ->  hov 1
-      (str"(" ++ pr_constr c ++ spc() ++
-       prlist_with_sep spc pr_constr (Array.to_list l) ++ str")")
-  | Evar (e,l) -> hov 1
-      (str"Evar#" ++ int (Evar.repr e) ++ str"{" ++
-       prlist_with_sep spc pr_constr (Array.to_list l) ++str"}")
-  | Const (c,u) -> str"Cst(" ++ pr_puniverses (pr_con c) u ++ str")"
-  | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i) u ++ str")"
-  | Construct (((sp,i),j),u) ->
-      str"Constr(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")"
-  | Proj (p,c) -> str"Proj(" ++ pr_con (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ pr_constr c ++ str")"
-  | Case (ci,p,c,bl) -> v 0
-      (hv 0 (str"<"++pr_constr p++str">"++ cut() ++ str"Case " ++
-             pr_constr c ++ str"of") ++ cut() ++
-       prlist_with_sep (fun _ -> brk(1,2)) pr_constr (Array.to_list bl) ++
-      cut() ++ str"end")
-  | Fix f -> pr_fix pr_constr f
-  | CoFix(i,(lna,tl,bl)) ->
-      let fixl = Array.mapi (fun i na -> (na,tl.(i),bl.(i))) lna in
-      hov 1
-        (str"cofix " ++ int i ++ spc() ++  str"{" ++
-         v 0 (prlist_with_sep spc (fun (na,ty,bd) ->
-           Name.print na ++ str":" ++ pr_constr ty ++
-           cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
-         str"}")
-
-let debug_print_constr c = pr_constr EConstr.Unsafe.(to_constr c)
-let debug_print_constr_env env sigma c = pr_constr EConstr.(to_constr sigma c)
+let pr_sort_family = Sorts.pr_sort_family
+[@@ocaml.deprecated "Use [Sorts.pr_sort_family]"]
+let pr_fix = Constr.debug_print_fix
+[@@ocaml.deprecated "Use [Constr.debug_print_fix]"]
+
+let debug_print_constr c = Constr.debug_print EConstr.Unsafe.(to_constr c)
+let debug_print_constr_env env sigma c = Constr.debug_print EConstr.(to_constr sigma c)
 let term_printer = ref debug_print_constr_env
 
 let print_constr_env env sigma t = !term_printer (env:env) sigma (t:Evd.econstr)
diff --git a/engine/termops.mli b/engine/termops.mli
index 07c9541f25..6c3d4fa612 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -17,9 +17,10 @@ open Environ
 open EConstr
 
 (** printers *)
-val print_sort : Sorts.t -> Pp.t
 val pr_sort_family : Sorts.family -> Pp.t
+[@@ocaml.deprecated "Use [Sorts.pr_sort_family]"]
 val pr_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t
+[@@ocaml.deprecated "Use [Constr.debug_print_fix]"]
 
 (** about contexts *)
 val push_rel_assum : Name.t * types -> env -> env
diff --git a/kernel/constr.ml b/kernel/constr.ml
index d7f35da10d..704e6de6b8 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -1338,3 +1338,70 @@ type compacted_declaration = (constr, types) Context.Compacted.Declaration.pt
 type rel_context = rel_declaration list
 type named_context = named_declaration list
 type compacted_context = compacted_declaration list
+
+(* Sorts and sort family *)
+
+let debug_print_fix pr_constr ((t,i),(lna,tl,bl)) =
+  let open Pp in
+  let fixl = Array.mapi (fun i na -> (na,t.(i),tl.(i),bl.(i))) lna in
+  hov 1
+      (str"fix " ++ int i ++ spc() ++  str"{" ++
+         v 0 (prlist_with_sep spc (fun (na,i,ty,bd) ->
+           Name.print na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++
+           cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
+         str"}")
+
+let pr_puniverses p u =
+  if Univ.Instance.is_empty u then p
+  else Pp.(p ++ str"(*" ++ Univ.Instance.pr Univ.Level.pr u ++ str"*)")
+
+(* Minimalistic constr printer, typically for debugging *)
+
+let rec debug_print c =
+  let open Pp in
+  match kind c with
+  | Rel n -> str "#"++int n
+  | Meta n -> str "Meta(" ++ int n ++ str ")"
+  | Var id -> Id.print id
+  | Sort s -> Sorts.debug_print s
+  | Cast (c,_, t) -> hov 1
+      (str"(" ++ debug_print c ++ cut() ++
+       str":" ++ debug_print t ++ str")")
+  | Prod (Name(id),t,c) -> hov 1
+      (str"forall " ++ Id.print id ++ str":" ++ debug_print t ++ str"," ++
+       spc() ++ debug_print c)
+  | Prod (Anonymous,t,c) -> hov 0
+      (str"(" ++ debug_print t ++ str " ->" ++ spc() ++
+       debug_print c ++ str")")
+  | Lambda (na,t,c) -> hov 1
+      (str"fun " ++ Name.print na ++ str":" ++
+       debug_print t ++ str" =>" ++ spc() ++ debug_print c)
+  | LetIn (na,b,t,c) -> hov 0
+      (str"let " ++ Name.print na ++ str":=" ++ debug_print b ++
+       str":" ++ brk(1,2) ++ debug_print t ++ cut() ++
+       debug_print c)
+  | App (c,l) ->  hov 1
+      (str"(" ++ debug_print c ++ spc() ++
+       prlist_with_sep spc debug_print (Array.to_list l) ++ str")")
+  | Evar (e,l) -> hov 1
+      (str"Evar#" ++ int (Evar.repr e) ++ str"{" ++
+       prlist_with_sep spc debug_print (Array.to_list l) ++str"}")
+  | Const (c,u) -> str"Cst(" ++ pr_puniverses (Constant.debug_print c) u ++ str")"
+  | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i) u ++ str")"
+  | Construct (((sp,i),j),u) ->
+      str"Constr(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")"
+  | Proj (p,c) -> str"Proj(" ++ Constant.debug_print (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ debug_print c ++ str")"
+  | Case (_ci,p,c,bl) -> v 0
+      (hv 0 (str"<"++debug_print p++str">"++ cut() ++ str"Case " ++
+             debug_print c ++ str"of") ++ cut() ++
+       prlist_with_sep (fun _ -> brk(1,2)) debug_print (Array.to_list bl) ++
+      cut() ++ str"end")
+  | Fix f -> debug_print_fix debug_print f
+  | CoFix(i,(lna,tl,bl)) ->
+      let fixl = Array.mapi (fun i na -> (na,tl.(i),bl.(i))) lna in
+      hov 1
+        (str"cofix " ++ int i ++ spc() ++  str"{" ++
+         v 0 (prlist_with_sep spc (fun (na,ty,bd) ->
+           Name.print na ++ str":" ++ debug_print ty ++
+           cut() ++ str":=" ++ debug_print bd) (Array.to_list fixl)) ++
+         str"}")
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 8753c20eac..1be1f63ff7 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -590,3 +590,6 @@ val case_info_hash : case_info -> int
 (*********************************************************************)
 
 val hcons : constr -> constr
+
+val debug_print : constr -> Pp.t
+val debug_print_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index a7bb08f5b6..566dce04c6 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -102,3 +102,13 @@ module Hsorts =
     end)
 
 let hcons = Hashcons.simple_hcons Hsorts.generate Hsorts.hcons hcons_univ
+
+let debug_print = function
+  | Set -> Pp.(str "Set")
+  | Prop -> Pp.(str "Prop")
+  | Type u -> Pp.(str "Type(" ++ Univ.Universe.pr u ++ str ")")
+
+let pr_sort_family = function
+  | InSet -> Pp.(str "Set")
+  | InProp -> Pp.(str "Prop")
+  | InType -> Pp.(str "Type")
diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index cac6229b91..6c5ce4df80 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -41,3 +41,7 @@ end
 
 val univ_of_sort : t -> Univ.Universe.t
 val sort_of_univ : Univ.Universe.t -> t
+
+val debug_print : t -> Pp.t
+
+val pr_sort_family : family -> Pp.t
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 89f64d328a..bd321d5886 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -618,5 +618,5 @@ let lookup_eliminator ind_sp s =
       (strbrk "Cannot find the elimination combinator " ++
        Id.print id ++ strbrk ", the elimination of the inductive definition " ++
        Nametab.pr_global_env Id.Set.empty (IndRef ind_sp) ++
-       strbrk " on sort " ++ Termops.pr_sort_family s ++
+       strbrk " on sort " ++ Sorts.pr_sort_family s ++
        strbrk " is probably not allowed.")
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 5d74b59b27..4faa753dfb 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -270,7 +270,7 @@ let pr_cs_pattern = function
     Const_cs c -> Nametab.pr_global_env Id.Set.empty c
   | Prod_cs -> str "_ -> _"
   | Default_cs -> str "_"
-  | Sort_cs s -> Termops.pr_sort_family s
+  | Sort_cs s -> Sorts.pr_sort_family s
 
 let warn_redundant_canonical_projection =
   CWarnings.create ~name:"redundant-canonical-projection" ~category:"typechecker"
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index aced97e910..17003cd1dd 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -353,7 +353,7 @@ struct
     | Proj (p,cst) ->
       str "ZProj(" ++ Constant.debug_print (Projection.constant p) ++ str ")"
     | Fix (f,args,cst) ->
-       str "ZFix(" ++ Termops.pr_fix pr_c f
+       str "ZFix(" ++ Constr.debug_print_fix pr_c f
        ++ pr_comma () ++ pr pr_c args ++ str ")"
     | Cst (mem,curr,remains,params,cst_l) ->
       str "ZCst(" ++ pr_cst_member pr_c mem ++ pr_comma () ++ int curr
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index ad6ca3a84e..ba31f73030 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -201,8 +201,8 @@ let explain_elim_arity env sigma ind sorts c pj okinds =
   let pc = pr_leconstr_env env sigma c in
   let msg = match okinds with
   | Some(kp,ki,explanation) ->
-      let pki = pr_sort_family ki in
-      let pkp = pr_sort_family kp in
+      let pki = Sorts.pr_sort_family ki in
+      let pkp = Sorts.pr_sort_family kp in
       let explanation =	match explanation with
 	| NonInformativeToInformative ->
           "proofs can be eliminated only to build proofs"
@@ -210,7 +210,7 @@ let explain_elim_arity env sigma ind sorts c pj okinds =
           "strong elimination on non-small inductive types leads to paradoxes"
 	| WrongArity ->
 	  "wrong arity" in
-      let ppar = pr_disjunction (fun s -> quote (pr_sort_family s)) sorts in
+      let ppar = pr_disjunction (fun s -> quote (Sorts.pr_sort_family s)) sorts in
       let ppt = pr_leconstr_env env sigma (snd (decompose_prod_assum sigma pj.uj_type)) in
       hov 0
 	(str "the return type has sort" ++ spc () ++ ppt ++ spc () ++
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index a0e8f38c0b..1c1faca599 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -312,7 +312,7 @@ open Pputils
         ) ++
           hov 0 ((if dep then keyword "Induction for" else keyword "Minimality for")
                  ++ spc() ++ pr_smart_global ind) ++ spc() ++
-          hov 0 (keyword "Sort" ++ spc() ++ Termops.pr_sort_family s)
+          hov 0 (keyword "Sort" ++ spc() ++ Sorts.pr_sort_family s)
       | CaseScheme (dep,ind,s) ->
         (match idop with
           | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
@@ -320,7 +320,7 @@ open Pputils
         ) ++
           hov 0 ((if dep then keyword "Elimination for" else keyword "Case for")
                  ++ spc() ++ pr_smart_global ind) ++ spc() ++
-          hov 0 (keyword "Sort" ++ spc() ++ Termops.pr_sort_family s)
+          hov 0 (keyword "Sort" ++ spc() ++ Sorts.pr_sort_family s)
       | EqualityScheme ind ->
         (match idop with
           | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()