Improved pretty-printing

- Num does not use print_name anymore
- Original names of free variables are preserved
- bound variables' names start with x

(cherry picked from commit 137e2373f8875992898f8be0e07c4299ffbf3516)

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 18b0bc0d79b490c18959473b70c0ac7ccaf66a99..612e94cc1d45cddec3df4eee854fe1f1e8874c0e 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -68,22 +68,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
+  @ [""])
 ;;
 
 

diff --git a/ocaml/num.ml b/ocaml/num.ml
index 36234ad31c7a47b15b9af578aab525c379ba5419..2bc253d0554bbdec893c04d6878e2354cfb31020 100644 (file)
--- a/ocaml/num.ml
+++ b/ocaml/num.ml
@@ -112,21 +112,23 @@ end
 
 (************ Pretty-printing ************************************)
 
-let rec string_of_term l =
- let rec string_of_term_w_pars l = function
-  | `Var(n,ar) -> print_name l n ^ ":" ^ string_of_int ar
+(* let rec string_of_term l  = fun _ -> "";; *)
+
+let rec string_of_term l  =
+ let rec string_of_term_w_pars l  = function
+  | `Var(n,ar) -> List.nth l n ^ (if debug_display_arities then ":" ^ string_of_int ar else "")
   | `N n -> string_of_int n
   | `I _ as t -> "(" ^ string_of_term_no_pars_app l (t :> nf) ^ ")"
   | `Lam _ as t -> "(" ^ string_of_term_no_pars_lam l t ^ ")"
   | `Match(t,(v,ar),bs_lift,bs,args) ->
-     "["^ string_of_var v ^ (if debug_display_arities then ":"^ string_of_int ar else "") ^",match " ^ string_of_term_no_pars l (t :> nf) ^
+     "["^ List.nth l v ^ (if debug_display_arities then ":"^ string_of_int ar else "") ^",match " ^ string_of_term_no_pars l (t :> nf) ^
      " with " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ string_of_term l (lift bs_lift (t :> nf))) !bs) ^ "] " ^
      String.concat " " (List.map (string_of_term l) (args :> nf list)) ^ ")"
  and string_of_term_no_pars_app l  = function
-  | `I((n,ar), args) -> print_name l n ^ (if debug_display_arities then ":" ^ string_of_int ar else "") ^ " " ^ String.concat " " (List.map (string_of_term_w_pars l) (Listx.to_list args :> nf list))
+  | `I((n,ar), args) -> List.nth l n ^ (if debug_display_arities then ":" ^ string_of_int ar else "") ^ " " ^ String.concat " " (List.map (string_of_term_w_pars l) (Listx.to_list args :> nf list))
   | #nf as t -> string_of_term_w_pars l t
  and string_of_term_no_pars_lam l  = function
-  | `Lam(_,t) -> let name = string_of_var (List.length l) in
+  | `Lam(_,t) -> let name = "x" ^ string_of_int (List.length l) in
      "λ" ^ name ^ ". " ^ (string_of_term_no_pars_lam (name::l) t)
   | _ as t -> string_of_term_no_pars l t
  and string_of_term_no_pars l : nf -> string = function