Improved pretty-printing

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

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
+  @ [""])
 ;;
 
 

diff --git a/ocaml/num.ml b/ocaml/num.ml
index 962feaf3011efa95e31f0e64e0f995a394800350..1b121efaec576a8cbd0c2ee6b3769af3902ba964 100644 (file)
--- a/ocaml/num.ml
+++ b/ocaml/num.ml
@@ -120,23 +120,23 @@ end
 
 let rec string_of_term l  =
  let rec string_of_term_w_pars l  = function
-  | `Var(n,ar) -> print_name l n ^ (if debug_display_arities then ":" ^ string_of_int ar else "")
+  | `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 ^ ")"
   | `Lam(_,`Bottom) -> "BOMB"
   | `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)) ^ ")"
   | `Bottom -> "BOT"
   | `Pacman -> "PAC"
  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(_,`Bottom) -> "BOMB"
-  | `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  = function