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=04aaa75f51fc05e92888e398b9032d172321f42b;hb=bebc917ebff72c2e235cb3062a4c94f10a9aab27;hp=fd68f0fe765cd7cd75be5805dac8c516a0f623fb;hpb=b519aa529779c0a4625eb43fa9557862d8cc6617;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/stats.ml b/helm/software/components/ng_paramodulation/stats.ml
index fd68f0fe7..04aaa75f5 100644
--- a/helm/software/components/ng_paramodulation/stats.ml
+++ b/helm/software/components/ng_paramodulation/stats.ml
@@ -25,7 +25,7 @@ module Stats (B : Terms.Blob) =
     let occ_nbr t = occ_nbr t 0;;
 
     let goal_occ_nbr t = function
-      | (_,Terms.Equation (l,r,_,_),_,_) ->
+      | (_,[],[Terms.Equation (l,r,_,_),_],_,_) ->
 	  occ_nbr t l + occ_nbr t r
       | _ -> assert false
     ;;
@@ -48,11 +48,11 @@ module Stats (B : Terms.Blob) =
       in
 	match l with
 	  | [] -> acc
-	  | (_,hd,_,_)::tl ->
-	      match hd with
-		| Terms.Equation (l,r,_,_) ->
+	  | (_,nlit,plit,_,_)::tl ->
+	      match nlit,plit with
+		| [],[Terms.Equation (l,r,_,_),_] ->
 		    parse_symbols (aux (aux acc l) r) tl
-		| Terms.Predicate _ -> assert false;
+		| _ -> assert false;
     ;;
 
     let goal_pos t goal =
@@ -73,8 +73,9 @@ module Stats (B : Terms.Blob) =
       in 
         aux [] 
           (match goal with
-          | _,Terms.Equation (l,r,ty,_),_,_ -> Terms.Node [ Terms.Leaf B.eqP; ty; l; r ]
-	  | _,Terms.Predicate p,_,_ -> p)
+          | _,[],[Terms.Equation (l,r,ty,_),_],_,_ ->
+               Terms.Node [ Terms.Leaf B.eqP; ty; l; r ]
+	  | _ -> assert false)
     ;;
 
     let parse_symbols l goal = 
@@ -92,11 +93,10 @@ module Stats (B : Terms.Blob) =
     let rec dependencies op clauses acc =
       match clauses with
 	| [] -> acc
-	| (_,lit,_,_)::tl ->
-	    match lit with
-	      | Terms.Predicate _ -> assert false
-	      | Terms.Equation (l,r,_,_) ->
-		  match l,r with
+	| (_,nlit,plit,_,_)::tl ->
+	    match nlit,plit with
+	      | [],[Terms.Equation (l,r,_,_),_] ->
+		  (match l,r with
 		    | (Terms.Node (Terms.Leaf op1::_),Terms.Node
 			 (Terms.Leaf op2::_)) ->
 			if (B.eq op1 op) && not (B.eq op2 op) then
@@ -126,7 +126,8 @@ module Stats (B : Terms.Blob) =
                            dependencies op tl (op1::acc)
                          else
                            dependencies op tl acc
-		    | _ -> dependencies op tl acc
+		    | _ -> dependencies op tl acc)
+		| _ -> assert false
     ;;
 
     let dependencies op clauses = HExtlib.list_uniq (List.sort Pervasives.compare (dependencies op clauses []));;