X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=8e77936c8f964bc721b64170a3326ce1db3e3890;hb=2c2b31c242aa81dc6f3c73e7e2a3ec0789a21edd;hp=61d6c0589f3ab9952e670ead382f71633ea00ef8;hpb=571d199acd4e6743a48f8f64f28c62d18182d04d;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 61d6c0589..8e77936c8 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -267,24 +267,24 @@ module Superposition (B : Terms.Blob) =
     (* demodulate and check for subsumption *)
     let simplify table maxvar bag clause = 
       let bag, clause = demodulate bag clause table in
-      if is_identity_clause ~unify:false clause then None
+      if is_identity_clause ~unify:false clause then bag,None
       else
         match is_subsumed ~unify:false bag maxvar clause table with
-	  | None -> Some (bag, clause)
-	  | Some _ -> None
+	  | None -> bag, Some clause
+	  | Some _ -> bag, None
     ;;
 
     let one_pass_simplification new_clause (alist,atable) bag maxvar =
       match simplify atable maxvar bag new_clause with
-	| None -> None (* new_clause has been discarded *)
-	| Some (bag, clause) ->
+	| bag,None -> None (* new_clause has been discarded *)
+	| bag,(Some clause) ->
 	    let ctable = IDX.index_unit_clause IDX.DT.empty clause in
 	    let bag, alist, atable = 
 	      List.fold_left 
 		(fun (bag, alist, atable as acc) c ->
 		   match simplify ctable maxvar bag c with
-		     |None -> acc (* an active clause as been discarded *)
-		     |Some (bag, c1) ->
+		     |bag,None -> acc (* an active clause as been discarded *)
+		     |bag,Some c1 ->
 			bag, c :: alist, IDX.index_unit_clause atable c)
 		(bag,[],IDX.DT.empty) alist
 	    in
@@ -300,8 +300,8 @@ module Superposition (B : Terms.Blob) =
 	 * - actives and cl if new_clause is not cl *
 	 * - only actives otherwise                 *)
 	match simplify atable1 maxvar bag new_clause with
-	  | None -> (Some cl, None) (* new_clause has been discarded *)
-	  | Some (bag, clause) ->
+	  | bag,None -> (Some cl, None) (* new_clause has been discarded *)
+	  | bag,Some clause ->
 	      (* Simplification of each active clause with clause *
 	       * which is the simplified form of new_clause       *)
               let ctable = IDX.index_unit_clause IDX.DT.empty clause in
@@ -309,8 +309,8 @@ module Superposition (B : Terms.Blob) =
 		List.fold_left 
 		  (fun (bag, newa, alist, atable as acc) c ->
 		     match simplify ctable maxvar bag c with
-		       |None -> acc (* an active clause as been discarded *)
-		       |Some (bag, c1) ->
+		       |bag,None -> acc (* an active clause as been discarded *)
+		       |bag,Some c1 ->
 			    if (c1 == c) then 
 			      bag, newa, c :: alist,
 			    IDX.index_unit_clause atable c
@@ -323,10 +323,10 @@ module Superposition (B : Terms.Blob) =
 		else
 		  (* if new_clause is not cl, we simplify cl with clause *)
 		  match simplify ctable maxvar bag cl with
-		    | None ->
+		    | bag,None ->
 			(* cl has been discarded *)
 			(None, Some (clause, (alist,atable), newa, bag))
-		    | Some (bag,cl1) ->
+		    | bag,Some cl1 ->
 			(Some cl1, Some (clause, (alist,atable), newa, bag))
     ;;
 
@@ -492,7 +492,7 @@ module Superposition (B : Terms.Blob) =
 	debug (Printf.sprintf "Demodulating %d clauses"
 		 (List.length new_clauses));
       let bag, new_clauses = 
-        HExtlib.filter_map_acc (simplify atable maxvar) bag new_clauses
+        HExtlib.filter_map_monad (simplify atable maxvar) bag new_clauses
       in
 	debug "Demodulated new clauses";
       bag, maxvar, (alist, atable), new_clauses