Various architectural changes

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

diff --git a/helm/software/components/ng_paramodulation/stats.ml b/helm/software/components/ng_paramodulation/stats.ml
index 04aaa75f51fc05e92888e398b9032d172321f42b..b6fe753d3f8ba1bd93cff25d1df52c893ed43578 100644 (file)
--- 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 []));;