Fixed pretty printer and debug printings

[helm.git] / helm / software / components / ng_paramodulation / pp.ml

diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml
index 061dae2b1f86296bf899df8e98caebfb3eb58ae3..d93fade272e9479be851a5dbb33853f6d26ecf8e 100644 (file)
--- a/helm/software/components/ng_paramodulation/pp.ml
+++ b/helm/software/components/ng_paramodulation/pp.ml
@@ -87,20 +87,12 @@ let string_of_comparison = function
   | Terms.Incomparable -> "=?="
   | Terms.Invertible -> "=<->="
 
-(*let pp_literal ~formatter:f l =
-    match l with
+let pp_literal ~formatter:f l =
+    match fst l with
       | Terms.Predicate t ->
          Format.fprintf f "@[<hv>{";
          pp_foterm f t;
-          Format.fprintf f "@;[%s] by "
-            (String.concat ", " (List.map string_of_int vars));
-          (match proof with
-           | Terms.Exact t -> pp_foterm f t
-           | Terms.Step (rule, id1, id2, _, p, _) -> 
-               Format.fprintf f "%s %d with %d at %s" 
-                 (string_of_rule rule) id1 id2 (String.concat
-                  "," (List.map string_of_int p)));
-          Format.fprintf f "@]"
+          Format.fprintf f "}@;"
       | Terms.Equation (lhs, rhs, ty, comp) ->
          Format.fprintf f "@[<hv>{";
          pp_foterm f ty;
@@ -108,16 +100,8 @@ let string_of_comparison = function
          pp_foterm f lhs;
           Format.fprintf f "@;%s@;" (string_of_comparison comp);
          pp_foterm f rhs;
-          Format.fprintf f "@]@;[%s] by "
-            (String.concat ", " (List.map string_of_int vars));
-          (match proof with
-           | Terms.Exact t -> pp_foterm f t
-           | Terms.Step (rule, id1, id2, _, p, _) -> 
-               Format.fprintf f "%s %d with %d at %s" 
-                 (string_of_rule rule) id1 id2 (String.concat
-                  "," (List.map string_of_int p)));
-          Format.fprintf f "@]"
-*)
+          Format.fprintf f "@]@;"
+;;
 
 let pp_unit_clause ~formatter:f c =
   let (id, l, vars, proof) = c in
@@ -150,11 +134,28 @@ let pp_unit_clause ~formatter:f c =
                Format.fprintf f "%s %d with %d at %s" 
                  (string_of_rule rule) id1 id2 (String.concat
                   "," (List.map string_of_int p)));
-          Format.fprintf f "@]"
+           Format.fprintf f "@]"
 ;;
 
 let pp_clause ~formatter:f c =
-       assert false
+   let (id, nlit, plit, vars, proof) = c in
+    Format.fprintf f "Id : %3d, " id ;
+    let pr_literals l =
+      if l <> [] then begin
+       pp_literal f (List.hd l);
+       List.iter (fun lit -> Format.fprintf f "\\/"; pp_literal f lit) (List.tl l);
+      end
+    in
+    pr_literals nlit;
+    Format.fprintf f " -> ";
+    pr_literals plit;
+    Format.fprintf f "[%s] by " (String.concat ", " (List.map string_of_int vars));
+    match proof with
+      | Terms.Exact t -> pp_foterm f t
+      | Terms.Step (rule, id1, id2, _, p, _) -> 
+           Format.fprintf f "%s %d with %d at %s" 
+             (string_of_rule rule) id1 id2 (String.concat
+             "," (List.map string_of_int p))
 ;;
 
 let pp_bag ~formatter:f (_,bag) =