depth-restricted printing for terms and pterms

src/core/Sidekick_core.ml

@@ -41,7 +41,6 @@ module Lit = Lit
 module Subst = Sidekick_core_logic.Subst
 module Var = Sidekick_core_logic.Var
 module Box = Box
-module Clause_tracer = Clause_tracer
 module Gensym = Gensym
 
 exception Resource_exhausted

src/core/lit.ml

@@ -39,6 +39,12 @@ let pp out l =
   else
     Format.fprintf out "(@[@<1>¬@ %a@])" T_printer.pp l.lit_term
 
+let pp_limit ~max_depth ~max_nodes out l =
+  if l.lit_sign then
+    T_printer.pp_limit ~max_depth ~max_nodes out l.lit_term
+  else
+    Format.fprintf out "(@[@<1>¬@ %a@])" T_printer.pp l.lit_term
+
 let norm_sign l =
   if l.lit_sign then
     l, true

src/core/lit.mli

@@ -16,6 +16,8 @@ type t
 
 include Sidekick_sigs.EQ_ORD_HASH_PRINT with type t := t
 
+val pp_limit : max_depth:int -> max_nodes:int -> t Fmt.printer
+
 val term : t -> term
 (** Get the (positive) term *)
 

src/core/t_printer.ml

@@ -35,8 +35,10 @@ let default_ : Hooks.t = Hooks.(empty |> add pp_builtins_ |> add pp_box)
 let default_hooks = ref default_
 
 (* debug printer *)
-let expr_pp_with_ ~max_depth ~hooks out (e : term) : unit =
+let expr_pp_with_ ~max_depth ~max_nodes ~hooks out (e : term) : unit =
   let open Term in
+  let nodes = ref max_nodes in
+
   let rec loop k ~depth names out e =
     let pp' = loop k ~depth:(depth + 1) names in
 
@@ -53,35 +55,44 @@ let expr_pp_with_ ~max_depth ~hooks out (e : term) : unit =
         | Some n when n <> "" -> Fmt.fprintf out "%s[%d]" n idx
         | _ -> Fmt.fprintf out "_[%d]" idx)
       | E_const c -> Const.pp out c
-      | (E_app _ | E_lam _) when depth > max_depth -> Fmt.fprintf out "@<1>…"
+      | (E_app _ | E_lam _ | E_app_fold _) when depth > max_depth || !nodes <= 0
+        ->
+        Fmt.fprintf out "@<1>…"
       | E_app _ ->
+        decr nodes;
         let f, args = unfold_app e in
         Fmt.fprintf out "(%a@ %a)" pp' f (Util.pp_list pp') args
       | E_app_fold { f; args; acc0 } ->
+        decr nodes;
         Fmt.fprintf out "(@[%a" pp' f;
         List.iter (fun x -> Fmt.fprintf out "@ %a" pp' x) args;
         Fmt.fprintf out "@ %a" pp' acc0;
         Fmt.fprintf out "@])"
       | E_lam ("", _ty, bod) ->
+        decr nodes;
         Fmt.fprintf out "(@[\\_:@[%a@].@ %a@])" pp' _ty
           (loop (k + 1) ~depth:(depth + 1) ("" :: names))
           bod
       | E_lam (n, _ty, bod) ->
+        decr nodes;
         Fmt.fprintf out "(@[\\%s:@[%a@].@ %a@])" n pp' _ty
           (loop (k + 1) ~depth:(depth + 1) (n :: names))
           bod
       | E_pi (_, ty, bod) when is_closed bod ->
         (* actually just an arrow *)
+        decr nodes;
         Fmt.fprintf out "(@[%a@ -> %a@])"
           (loop k ~depth:(depth + 1) names)
           ty
           (loop (k + 1) ~depth:(depth + 1) ("" :: names))
           bod
       | E_pi ("", _ty, bod) ->
+        decr nodes;
         Fmt.fprintf out "(@[Pi _:@[%a@].@ %a@])" pp' _ty
           (loop (k + 1) ~depth:(depth + 1) ("" :: names))
           bod
       | E_pi (n, _ty, bod) ->
+        decr nodes;
         Fmt.fprintf out "(@[Pi %s:@[%a@].@ %a@])" n pp' _ty
           (loop (k + 1) ~depth:(depth + 1) (n :: names))
           bod
@@ -89,5 +100,10 @@ let expr_pp_with_ ~max_depth ~hooks out (e : term) : unit =
   in
   Fmt.fprintf out "@[<1>%a@]" (loop 0 ~depth:0 []) e
 
-let pp_with hooks out e : unit = expr_pp_with_ ~max_depth:max_int ~hooks out e
+let pp_with hooks out e : unit =
+  expr_pp_with_ ~max_depth:max_int ~max_nodes:max_int ~hooks out e
+
 let pp out e = pp_with !default_hooks out e
+
+let pp_limit ~max_depth ~max_nodes out e : unit =
+  expr_pp_with_ ~max_depth ~max_nodes ~hooks:!default_hooks out e

src/core/t_printer.mli

@@ -19,3 +19,7 @@ val pp_with : Hooks.t -> term Fmt.printer
 
 val pp : term Fmt.printer
 (** Print using {!default_hooks} *)
+
+val pp_limit : max_depth:int -> max_nodes:int -> term Fmt.printer
+(** Print with a limit on the number of nodes printed. An ellipsis is
+    displayed otherwise. *)

src/proof/pterm.ml

@@ -27,7 +27,13 @@ let rec pp out = function
     if r.premises <> [] then
       Fmt.fprintf out "@ :prem %a" Fmt.Dump.(list int) r.premises;
     if r.term_args <> [] then
-      Fmt.fprintf out "@ :ts %a" Fmt.Dump.(list Term.pp) r.term_args;
+      Fmt.fprintf out "@ :ts %a"
+        Fmt.Dump.(list @@ Term.pp_limit ~max_nodes:200 ~max_depth:5)
+        r.term_args;
+    if r.lit_args <> [] then
+      Fmt.fprintf out "@ :lits %a"
+        Fmt.Dump.(list @@ Lit.pp_limit ~max_nodes:200 ~max_depth:5)
+        r.lit_args;
     Fmt.fprintf out "@]}"
   | P_let (bs, bod) ->
     let pp_b out (x, t) = Fmt.fprintf out "s%d := %a" x pp t in