Added label to problem

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

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index ce0663a05da2714b8e59f8a2734e5aa2a8c10b82..02ac1e018ff96f1cb1d9cacb8e85dc58be733adb 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -33,6 +33,8 @@ type problem =
  ; trail: discriminating_set list list
 };;
 
+let label_of_problem {label} = label;;
+
 (* exceptions *)
 exception Pacman
 exception Bottom
@@ -77,7 +79,7 @@ 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 (" ^ label ^ ") - ");
+ 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
@@ -817,7 +819,7 @@ let tmp (label, div, conv, nums, var_names) =
  (* TODO: *)
  (* replace div with bottom in problem??? *)
  let all_tms = (match div with None -> [] | Some div -> [(div :> i_n_var)]) @ nums @ conv in
- if all_tms = [] then failwith "FIXME: empty problem"; 
+ if all_tms = [] then failwith "FIXME: empty problem";
  let initialSpecialK = compute_special_k (Listx.from_list (all_tms :> nf list)) in
  let freshno = List.length var_names in
  let deltas =