]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
Added label to problem
authoracondolu <andrea.condoluci@unibo.it>
Fri, 14 Jul 2017 18:30:55 +0000 (20:30 +0200)
committeracondolu <andrea.condoluci@unibo.it>
Mon, 28 May 2018 09:08:58 +0000 (11:08 +0200)
(cherry picked from commit c7e39970b94c93db45f2629af3fdb1e08371eca1)

ocaml/lambda4.ml
ocaml/lambda4.mli

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
index af249e34972fb5cfa028dad87af48590757d5062..c8a40bfa8c719694f0796ec429c13943ac3cf200 100644 (file)
@@ -1,5 +1,7 @@
 type problem\r
 \r
+val label_of_problem : problem -> string\r
+\r
 type result = [\r
  | `Separable of (int * Num.nf) list\r
  | `Unseparable of string\r