X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fpp.ml;fp=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fpp.ml;h=061dae2b1f86296bf899df8e98caebfb3eb58ae3;hb=bebc917ebff72c2e235cb3062a4c94f10a9aab27;hp=ddf5726c49d0f6b479958a4e48ca9f969440f30d;hpb=b519aa529779c0a4625eb43fa9557862d8cc6617;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml
index ddf5726c4..061dae2b1 100644
--- a/helm/software/components/ng_paramodulation/pp.ml
+++ b/helm/software/components/ng_paramodulation/pp.ml
@@ -68,8 +68,8 @@ let pp_proof bag ~formatter:f p =
           eq (string_of_rule rule);
 	Format.fprintf f "|%d with %d dir %s))" eq1 eq2
 	  (string_of_direction dir);
-	let (_, _, _, proof1),_,_ = Terms.get_from_bag eq1 bag in
-	let (_, _, _, proof2),_,_ = Terms.get_from_bag eq2 bag in
+	let (_, _, _, _, proof1),_,_ = Terms.get_from_bag eq1 bag in
+	let (_, _, _, _, proof2),_,_ = Terms.get_from_bag eq2 bag in
 	  Format.fprintf f "@[<v 2>";
           aux eq1 proof1;	    
           aux eq2 proof2;
@@ -87,6 +87,38 @@ let string_of_comparison = function
   | Terms.Incomparable -> "=?="
   | Terms.Invertible -> "=<->="
 
+(*let pp_literal ~formatter:f l =
+    match 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 "@]"
+      | Terms.Equation (lhs, rhs, ty, comp) ->
+	  Format.fprintf f "@[<hv>{";
+	  pp_foterm f ty;
+          Format.fprintf f "}:@;@[<hv>";
+	  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 "@]"
+*)
+
 let pp_unit_clause ~formatter:f c =
   let (id, l, vars, proof) = c in
     Format.fprintf f "Id : %3d, " id ;
@@ -121,10 +153,14 @@ let pp_unit_clause ~formatter:f c =
           Format.fprintf f "@]"
 ;;
 
+let pp_clause ~formatter:f c =
+	assert false
+;;
+
 let pp_bag ~formatter:f (_,bag) = 
   Format.fprintf f "@[<v>";
   Terms.M.iter 
-  (fun _ (c,d,_) -> pp_unit_clause ~formatter:f c;
+  (fun _ (c,d,_) -> pp_clause ~formatter:f c;
      if d then Format.fprintf f " (discarded)@;"
      else Format.fprintf f "@;") bag;
   Format.fprintf f "@]"
@@ -160,4 +196,8 @@ let pp_unit_clause ?margin x=
   on_buffer ?margin pp_unit_clause x
 ;;
 
+let pp_clause ?margin x =
+  on_buffer ?margin pp_clause x
+;;
+
 end