]> matita.cs.unibo.it Git - fireball-separation.git/blobdiff - ocaml/lambda4.ml
Added label to problem
[fireball-separation.git] / ocaml / lambda4.ml
index a8899bcbebc2bb31d20b14b6834c94eb449e50fb..1e978f281336137234264b00068e869fa43ade8d 100644 (file)
@@ -31,6 +31,8 @@ type problem =
  ; var_names : string list (* names of the original free variables *)
 };;
 
+let label_of_problem {label} = label;;
+
 let all_terms p =
  (match p.div with None -> [] | Some t -> [(t :> i_n_var)])
  @ p.conv
@@ -67,7 +69,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