Logging options to display measure of single terms in string_of_problem

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index f26607bbf730f31a6b364e628880869f240182e9..456dd5b9ec96ae9b62ee68c185067f97cfaa3d5d 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -15,7 +15,10 @@ exception Backtrack of string
  For Scott's encoding, two.
 *)
 let num_more_args = 2;;
+(* verbosity *)
 let _very_verbose = false;;
+(** Display measure of every term when printing problem *)
+let _measure_of_terms = false;;
 
 let verbose s =
  if _very_verbose then prerr_endline s
@@ -88,6 +91,7 @@ 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) =
+ let aux_measure_terms t = if _measure_of_terms then "(" ^ string_of_int (measure_of_term t) ^ ") " else "" in
  let deltas = String.concat ("\n#  ") (List.map (fun r -> String.concat " <> " (List.map (fun (i,_) -> string_of_int i) !r)) deltas) in
  let l = p.var_names in
  String.concat "\n" ([
@@ -99,10 +103,10 @@ let string_of_problem label ({freshno; div; conv; ps; deltas} as p) =
    ) else "# ";
   "#";
   "$" ^ p.label;
-  (match div with None -> "# no D" | Some div -> "D ("^string_of_int (measure_of_term div)^")"^ print ~l (div :> nf));
+  (match div with None -> "# D" | Some div -> "D " ^ aux_measure_terms div ^ print ~l (div :> nf));
   ]
-  @ List.map (fun t -> if t = convergent_dummy then "#C" else "C ("^string_of_int (measure_of_term t)^") " ^ print ~l (t :> nf)) conv
-  @ List.mapi (fun i t -> string_of_int i ^ " ("^string_of_int (measure_of_term t)^") " ^ print ~l (t :> nf)) ps
+  @ List.map (fun t -> if t = convergent_dummy then "# C" else "C " ^ aux_measure_terms t ^ print ~l (t :> nf)) conv
+  @ List.mapi (fun i t -> string_of_int i ^ " " ^ aux_measure_terms t ^ print ~l (t :> nf)) ps
   @ [""])
 ;;