Improved pretty-printing

[fireball-separation.git] / ocaml / lambda4.ml

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 7b669ca3789880e524c6d6870d1111a64999cfba..89004a3386ecc673241f43c19d8ffab7878e03bf 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -78,22 +78,23 @@ let problem_measure p = sum_arities p;;
 let string_of_measure = string_of_int;;
 
 let string_of_problem label ({freshno; div; conv; ps; deltas} as p) =
- Console.print_hline ();
- prerr_string ("\n(* DISPLAY PROBLEM (" ^ p.label ^ " - " ^ label ^ ") ");
- let nl = "\n" in
- let deltas = String.concat (nl^"   ") (List.map (fun r -> String.concat " <> " (List.map (fun (i,_) -> string_of_int i) !r)) deltas) in
- let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
- "measure="^string_of_measure(problem_measure p) (* ^ " freshno = " ^ string_of_int freshno*)
- ^ nl ^ "   Discriminating sets (deltas):"
- ^ nl ^ "   " ^ deltas ^ (if deltas = " " then "" else nl) ^ "*)"
- ^"(* DIVERGENT  *)" ^ nl
- ^"     "^ (match div with None -> "None" | Some div -> "(Some\""^ print ~l (div :> nf) ^"\")") ^ nl
- ^"  (* CONVERGENT *) [" ^ nl ^ "  "
- ^ String.concat "\n  " (List.map (fun t -> "(* _ *) " ^ (if t = convergent_dummy then "" else "\""^ print ~l (t :> nf) ^"\";")) conv) ^
- (if conv = [] then "" else nl)
- ^ "] (* NUMERIC    *) [" ^ nl ^ " "
- ^ String.concat "\n " (List.mapi (fun i t -> " (* "^ string_of_int i ^" *) \"" ^ print ~l (t :> nf) ^ "\";") ps)
- ^ nl ^ "] [\"*\"];;" ^ nl
+ let deltas = String.concat ("\n#  ") (List.map (fun r -> String.concat " <> " (List.map (fun (i,_) -> string_of_int i) !r)) deltas) in
+ let nv = List.length p.var_names in
+ let l = p.var_names @ Array.to_list (Array.init (freshno + 1 - nv) (fun x -> "`" ^ string_of_int x)) in
+ String.concat "\n" ([
+  "";
+  "# DISPLAY PROBLEM (" ^ label ^ ") " ^ "measure=" ^ string_of_measure (problem_measure p);
+  if List.length p.deltas > 1 then (
+   "# Discriminating sets (deltas):\n" ^
+   "#  " ^ deltas
+   ) else "# ";
+  "#";
+  "$" ^ p.label;
+  (match div with None -> "# no D" | Some div -> "D " ^ print ~l (div :> nf));
+  ]
+  @ List.map (fun t -> "C " ^ (if t = convergent_dummy then " ... " else print ~l (t :> nf))) conv
+  @ List.mapi (fun i t -> string_of_int i ^ " " ^ print ~l (t :> nf)) ps
+  @ [""])
 ;;