Trace shortening

src/runtime/runtime.ml

@@ -293,6 +293,18 @@ let xppterm ~nice ?(pp_ctx = { Data.uv_names; table = ! C.table }) ?(min_prec=mi
         Fmt.fprintf f "@[<hov 1>%a@ %a@ %a@]"
           (aux (hdlvl+1) depth) a F.pp F.eqf
           (aux (hdlvl+1) depth) b)
+    | Builtin (Pi, [body]) ->
+      let _, hdlvl =
+        Elpi_parser.Parser_config.precedence_of (F.show F.pif) in
+      with_parens prec hdlvl (fun _ ->
+        Fmt.fprintf f "@[<hov 1>%a" F.pp F.pif;
+        let rec pp_pis depth t = 
+          Fmt.fprintf f "@ %a" (aux inf_prec depth) (mkConst depth);
+          match t with
+          | Lam (Builtin (Pi, [body])) -> pp_pis (depth + 1) body
+          | Lam t -> Fmt.fprintf f "@ \\@ %a@]" (aux min_prec depth) t
+          | _ -> assert false in
+        pp_pis depth body)
     | Builtin(b,[]) -> Fmt.fprintf f "%a" ppbuiltin b
     | Builtin(b,x::xs) ->
       (try
@@ -4506,4 +4518,4 @@ module CompileTime = struct
     get_clauses_dt ~check_mut_excl:On ~pp_clause:pp_overlap_clause ~cmp_clause:(fun (c1:overlap_clause) c2 -> lex_insertion c1.timestamp c2.timestamp) ~depth goal args_idx
 
   let fresh_uvar ~depth = oref ~depth C.dummy
-end
+end

trace/runtime/runtime.ml

@@ -326,7 +326,13 @@ let print_tty fmt = (); fun { runtime_id; goal_id; kind; name; step; payload } -
   | Stop { cause; time } ->
     F.fprintf fmt "}}} %s  (%.3fs)\n%!" cause time
   | Info ->
-    F.fprintf fmt "  rid:%d step:%d gid:%d %s =@[<hov1> %a@]\n%!" runtime_id step goal_id name (pplist pp_j) payload
+    let () = F.fprintf fmt "  @[<hov 2>rid:%d step:%d gid:%d %s =@ " runtime_id step goal_id name in
+    let () = match payload with
+      | [] -> ()
+      | j :: payload ->
+        let () = F.fprintf fmt "%a@," pp_j j in
+        F.fprintf fmt "@[<hov 0>%a@]" (pplist pp_j) payload in
+    F.fprintf fmt "@]\n%!"
 
 let () = printer := print_tty F.err_formatter
 
@@ -496,4 +502,4 @@ let parse_argv argv =
 ;;
 
 let set_cur_pred x = cur_pred := x
-let get_cur_step ~runtime_id x = Trace.get_cur_step ~runtime_id x
+let get_cur_step ~runtime_id x = Trace.get_cur_step ~runtime_id x