X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fstats.ml;fp=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fstats.ml;h=b6fe753d3f8ba1bd93cff25d1df52c893ed43578;hb=38c54dd8e2234836d5f3e8011c478daf7d59fa25;hp=04aaa75f51fc05e92888e398b9032d172321f42b;hpb=8a3045a162622e8a76ffdb267309faff496ee7ec;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/stats.ml b/helm/software/components/ng_paramodulation/stats.ml
index 04aaa75f5..b6fe753d3 100644
--- a/helm/software/components/ng_paramodulation/stats.ml
+++ b/helm/software/components/ng_paramodulation/stats.ml
@@ -15,6 +15,7 @@ module Stats (B : Terms.Blob) =
   struct
 
     module SymbMap = Map.Make(B)
+    module Pp = Pp.Pp(B)
 
     let rec occ_nbr t acc = function
 	| Terms.Leaf u when B.eq t u -> 1+acc
@@ -49,10 +50,13 @@ module Stats (B : Terms.Blob) =
 	match l with
 	  | [] -> acc
 	  | (_,nlit,plit,_,_)::tl ->
-	      match nlit,plit with
-		| [],[Terms.Equation (l,r,_,_),_] ->
-		    parse_symbols (aux (aux acc l) r) tl
-		| _ -> assert false;
+              let acc = List.fold_left (fun acc t ->
+                             	      match t with
+                           		| Terms.Equation (l,r,_,_),_ ->
+                         		    (aux (aux acc l) r)
+                            		| _ -> assert false) acc (nlit@plit)
+              in
+                 parse_symbols acc tl
     ;;
 
     let goal_pos t goal =
@@ -127,7 +131,7 @@ module Stats (B : Terms.Blob) =
                          else
                            dependencies op tl acc
 		    | _ -> dependencies op tl acc)
-		| _ -> assert false
+		| _ -> [] (* TODO : compute dependencies for clauses *)
     ;;
 
     let dependencies op clauses = HExtlib.list_uniq (List.sort Pervasives.compare (dependencies op clauses []));;