]> 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>
Fri, 14 Jul 2017 18:30:55 +0000 (20:30 +0200)
ocaml/lambda4.ml
ocaml/lambda4.mli

index ce0663a05da2714b8e59f8a2734e5aa2a8c10b82..02ac1e018ff96f1cb1d9cacb8e85dc58be733adb 100644 (file)
@@ -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 =
index bbfd13b990dd2f32b263f9e49a0b3bd2162ef3ac..1b6ec0db5d6d492ab76258067be684a75997fb7d 100644 (file)
@@ -1,5 +1,7 @@
 type problem\r
 \r
+val label_of_problem : problem -> string\r
+\r
 type response = [\r
  | `CompleteSeparable of string\r
  | `CompleteUnseparable of string\r