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

Added label to problem

(cherry picked from commit c7e39970b94c93db45f2629af3fdb1e08371eca1)
---

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index a8899bc..1e978f2 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -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
diff --git a/ocaml/lambda4.mli b/ocaml/lambda4.mli
index af249e3..c8a40bf 100644
--- a/ocaml/lambda4.mli
+++ b/ocaml/lambda4.mli
@@ -1,5 +1,7 @@
 type problem
 
+val label_of_problem : problem -> string
+
 type result = [
  | `Separable of (int * Num.nf) list
  | `Unseparable of string