From: acondolu <andrea.condoluci@unibo.it>
Date: Fri, 14 Jul 2017 18:30:55 +0000 (+0200)
Subject: Added label to problem
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c7e39970b94c93db45f2629af3fdb1e08371eca1;p=fireball-separation.git

Added label to problem
---

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index ce0663a..02ac1e0 100644
--- 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 =
diff --git a/ocaml/lambda4.mli b/ocaml/lambda4.mli
index bbfd13b..1b6ec0d 100644
--- a/ocaml/lambda4.mli
+++ b/ocaml/lambda4.mli
@@ -1,5 +1,7 @@
 type problem
 
+val label_of_problem : problem -> string
+
 type response = [
  | `CompleteSeparable of string
  | `CompleteUnseparable of string